From dcfba472e08ba2c25bdc6fbd198c9b0973741c59 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 9 Oct 2024 16:41:04 +0200 Subject: [PATCH 1/4] Update jpype version to one that's less problematic on Windows --- setup.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/setup.py b/setup.py index d0ef1ac9..e92f691a 100644 --- a/setup.py +++ b/setup.py @@ -10,7 +10,7 @@ setup( name='nagini', - version='1.1.0', + version='1.1.1', author='Viper Team', author_email='viper@inf.ethz.ch', license='MPL-2.0', @@ -26,7 +26,7 @@ install_requires=[ 'mypy==0.782', 'toposort==1.5', - 'jpype1==1.0.1', + 'jpype1==1.2.1', 'astunparse==1.6.2', 'pytest==4.3.0', 'pytest-xdist==1.27.0', From bfe17e393309a04834fe09537559cbde966ba81c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 9 Oct 2024 17:49:52 +0200 Subject: [PATCH 2/4] Update README.rst Update Windows installation instructions and added explanations for two recently-added command line parameters. --- README.rst | 32 ++++++++++++++++++++++++++------ 1 file changed, 26 insertions(+), 6 deletions(-) diff --git a/README.rst b/README.rst index a90212b9..4710f627 100644 --- a/README.rst +++ b/README.rst @@ -20,6 +20,8 @@ Dependencies (Windows) 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 @@ -27,6 +29,12 @@ Getting Started 2. Activate it:: source env/bin/activate + + on Linux, or:: + + env\Scripts\activate + + on Windows. 3. Install Nagini:: @@ -49,6 +57,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 +77,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 From 311429f0496058f426742ebe09db92fde334efdb Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 22:15:49 +0200 Subject: [PATCH 3/4] Update README.rst with instructions for server mode --- README.rst | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/README.rst b/README.rst index 4710f627..dc02f16a 100644 --- a/README.rst +++ b/README.rst @@ -112,6 +112,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 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 ========================== From 6716f4b171956ffe3519fed068c5642fc22309e2 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 22:18:55 +0200 Subject: [PATCH 4/4] Update README.rst with a warning about Windows performance --- README.rst | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.rst b/README.rst index dc02f16a..6e1e216d 100644 --- a/README.rst +++ b/README.rst @@ -16,6 +16,8 @@ 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 ===============