Merge

README.rst

@@ -16,17 +16,27 @@ Dependencies (Windows)
 
 2.  Install the required version of either Visual C++ Build Tools or Visual Studio. 
 
+Note that we have observed *significantly* worse performance when using Nagini on Windows on some
+systems. We currently do not know why this happens, but will investigate the issue when possible.
 
 Getting Started
 ===============
 
+Execute the following commands (on Windows, you may have to use ``cmd`` and not PowerShell):
+
 1.  Create a virtual environment::
 
         virtualenv --python=python3 <env>
         
 2.  Activate it::
 
         source env/bin/activate
+
+    on Linux, or::
+
+        env\Scripts\activate
+
+    on Windows.
         
 3.  Install Nagini::
 
@@ -49,6 +59,9 @@ To verify a specific file from the nagini directory, run::
 
     nagini [OPTIONS] path-to-file.py
 
+You may have to explicitly supply a path to a Z3 executable (use version 4.8.7, other versions may offer significantly worse performance) using the command line parameter ``--z3=path/to/z3``.
+Additionally, you may have to set the environment variable ``JAVA_HOME`` to point to your Java installation.
+
 
 The following command line options are available::
 
@@ -66,14 +79,23 @@ The following command line options are available::
                     Enable outputting counterexamples for verification errors (experimental).
                     
     --sif=v         
-                    Enable verification of secure information flow. v can be true for ordinary 
-                    non-interference (for sequential programs only), poss for possiblistic 
-                    non-intererence (for concurrent programs) or prob for probabilistic non-
+                    Enable verification of secure information flow. v can be 'true' for ordinary 
+                    non-interference (for sequential programs only), 'poss' for possiblistic 
+                    non-intererence (for concurrent programs) or 'prob' for probabilistic non-
                     interference (for concurrent programs).
 
-    --z3           
-                    Sets the path of the Z3 executable. Alternatively, the
-                    'Z3_EXE' environment variable can be set.
+    --float-encoding           
+                    Selects a different encoding of floating point values. The default is to model floats
+                    as abstract values and all float operations as uninterpreted functions, so that essentially 
+                    nothing can be proved about them. Legal values for this option are 'real' to model floats
+                    as real numbers (i.e., not modeling floating point imprecision), or 'ieee32' to model them
+                    as proper IEEE 32 bit floats. The latter option unfortunately usually leads to very long
+                    verification times or non-termination.
+    --int-bitops-size
+                    Bitwise operations on integers (e.g. 12 ^ -5) are supported only for integers which can
+                    be proven to be in a specific range, namely the range of n-bit signed integers.
+                    This parameter sets the value of n.
+                    Default: 8.
                     
     --boogie        
                     Sets the path of the Boogie executable. Required if the Carbon backend
@@ -92,6 +114,27 @@ The following command line options are available::
 To see all possible command line options, invoke ``nagini`` without arguments.
 
 
+Server Mode / Faster Verification Mode
+======================================
+
+Nagini has to do a significant amount of work on startup, and has to start a JVM to run Viper.
+To avoid some of that startup work and speed up Viper's runtime, Nagini has a server mode.
+To use it,
+
+1. Start a Nagini server::
+
+        nagini --server <otherArgs> dummyFile.py
+   Note that all required arguments, including ``JAVA_HOME`` and other potentially required  
+   environment variables, have to be set here. The dummy file does not need to exist, it is 
+   never read, but some file name has to be supplied.
+
+2. Wait a few seconds to allow the server to start up
+
+3. While the server is running, run a client to instruct the server to verify a specific file::
+
+        nagini_client path/to/file.py 
+   
+
 Alternative Viper Versions
 ==========================
 

setup.py

@@ -10,7 +10,7 @@
 
 setup(
         name='nagini',
-        version='1.1.0',
+        version='1.1.1',
         author='Viper Team',
         author_email='[email protected]',
         license='MPL-2.0',