Merge pull request #146 from marcoeilers/sif_merge

Possibilistic and probabilistic noninterference

setup.py

@@ -10,7 +10,7 @@
 
 setup(
         name='nagini',
-        version='0.8.6',
+        version='0.9.0',
         author='Viper Team',
         author_email='viper@inf.ethz.ch',
         license='MPL-2.0',
@@ -30,7 +30,8 @@
             'astunparse==1.6.2',
             'typed-ast==1.4.0',
             'pytest==4.3.0',
-            'z3-solver'
+            'pytest-xdist==1.27.0',
+            'z3-solver==4.8.7.0'
             ],
         entry_points = {
              'console_scripts': [

src/nagini_translation/conftest.py

@@ -25,7 +25,9 @@
 _VERIFICATION_TESTS_SUFFIX = 'verification'
 
 _FUNCTIONAL_TESTS_DIR = 'tests/functional/'
-_SIF_TESTS_DIR = 'tests/sif/'
+_SIF_TRUE_TESTS_DIR = 'tests/sif-true/'
+_SIF_POSS_TESTS_DIR = 'tests/sif-poss/'
+_SIF_PROB_TESTS_DIR = 'tests/sif-prob/'
 _IO_TESTS_DIR = 'tests/io/'
 _OBLIGATIONS_TESTS_DIR = 'tests/obligations/'
 _ARP_TESTS_DIR = 'tests/arp/'
@@ -39,6 +41,7 @@ def __init__(self):
         self.single_test = None
         self.verifiers = []
         self.store_viper = False
+        self.force_product = False
 
         self.init_from_config_file()
 
@@ -52,10 +55,17 @@ def init_from_config_file(self):
             self.add_verifier(verifier)
 
     def add_test(self, test: str):
+        if test == 'functional-product':
+            self._add_test_dir(_FUNCTIONAL_TESTS_DIR)
+            self.force_product = True
         if test == 'functional':
             self._add_test_dir(_FUNCTIONAL_TESTS_DIR)
-        elif test == 'sif':
-            self._add_test_dir(_SIF_TESTS_DIR)
+        elif test == 'sif-true':
+            self._add_test_dir(_SIF_TRUE_TESTS_DIR)
+        elif test == 'sif-poss':
+            self._add_test_dir(_SIF_POSS_TESTS_DIR)
+        elif test == 'sif-prob':
+            self._add_test_dir(_SIF_PROB_TESTS_DIR)
         elif test == 'io':
             self._add_test_dir(_IO_TESTS_DIR)
         elif test == 'obligations':
@@ -121,7 +131,10 @@ def pytest_addoption(parser: 'pytest.config.Parser'):
     parser.addoption('--single-test', dest='single_test', action='store', default=None)
     parser.addoption('--all-tests', dest='all_tests', action='store_true')
     parser.addoption('--functional', dest='functional', action='store_true')
-    parser.addoption('--sif', dest='sif', action='store_true')
+    parser.addoption('--functional-product', dest='functional_product', action='store_true')
+    parser.addoption('--sif-true', dest='sif_true', action='store_true')
+    parser.addoption('--sif-poss', dest='sif_poss', action='store_true')
+    parser.addoption('--sif-prob', dest='sif_prob', action='store_true')
     parser.addoption('--io', dest='io', action='store_true')
     parser.addoption('--obligations', dest='obligations', action='store_true')
     parser.addoption('--arp', dest='arp', action='store_true')
@@ -137,24 +150,30 @@ def pytest_configure(config: 'pytest.config.Config'):
     # Setup tests.
     tests = []
     if config.option.all_tests:
-        tests = ['functional', 'sif', 'io', 'obligations', 'arp']
+        tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp']
     else:
         if config.option.functional:
             tests.append('functional')
-        if config.option.sif:
-            tests.append('sif')
+        if config.option.sif_true:
+            tests.append('sif-true')
+        if config.option.sif_poss:
+            tests.append('sif-poss')
+        if config.option.sif_prob:
+            tests.append('sif-prob')
         if config.option.io:
             tests.append('io')
         if config.option.obligations:
             tests.append('obligations')
         if config.option.arp:
             tests.append('arp')
+        if config.option.functional_product:
+            tests = ['functional-product']
     if tests:
         # Overwrite config file options.
         _pytest_config.clear_tests()
         for test in tests:
             _pytest_config.add_test(test)
-        if 'sif' in tests:
+        if 'sif-true' in tests or 'sif-poss' in tests or 'sif-prob' in tests:
             if not jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt):
                 pytest.exit('Viper SIF extension not avaliable on the classpath.')
     elif config.option.single_test:
@@ -165,7 +184,7 @@ def pytest_configure(config: 'pytest.config.Config'):
         # present.
         tests = ['functional', 'io', 'obligations']
         if jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt):
-            tests.append('sif')
+            tests.extend(['sif-true', 'sif-poss', 'sif-prob'])
         if jvm.is_known_class(jvm.viper.silver.plugin.ARPPlugin):
             tests.append('arp')
         for test in tests:
@@ -208,11 +227,19 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
         for test_dir in _pytest_config.translation_test_dirs:
             files = _test_files(test_dir)
             test_files.extend(files)
-            reload_triggers.add(files[0])
+            if files:
+                reload_triggers.add(files[0])
         if _pytest_config.single_test and 'translation' in _pytest_config.single_test:
             test_files.append(_pytest_config.single_test)
         for file in test_files:
-            sif = 'sif' in file
+            if 'sif-true' in file:
+                sif = True
+            elif 'sif-poss' in file:
+                sif = 'poss'
+            elif 'sif-prob' in file:
+                sif = 'prob'
+            else:
+                sif = False
             reload_resources = file in reload_triggers
             arp = 'arp' in file
             base = file.partition('translation')[0] + 'translation'
@@ -226,12 +253,23 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
         if _pytest_config.single_test and 'verification' in _pytest_config.single_test:
             test_files.append(_pytest_config.single_test)
         for file in test_files:
-            sif = 'sif' in file
+            ignore_obligations = 'no_obligations' in file
+            if 'sif-true' in file:
+                sif = True
+            elif 'sif-poss' in file:
+                sif = 'poss'
+            elif 'sif-prob' in file:
+                sif = 'prob'
+            else:
+                sif = False
+            if _pytest_config.force_product:
+                sif = True
             reload_resources = file in reload_triggers
             arp = 'arp' in file
             base = file.partition('verification')[0] + 'verification'
-            params.extend([(file, base, verifier, sif, reload_resources, arp, _pytest_config.store_viper) for verifier
+            params.extend([(file, base, verifier, sif, reload_resources, arp, ignore_obligations, _pytest_config.store_viper) for verifier
                            in _pytest_config.verifiers])
-        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,print', params)
+        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print', params)
     else:
         pytest.exit('Unrecognized test function.')
+

src/nagini_translation/lib/config.py

@@ -51,7 +51,7 @@ def disable_all(self):
     @disable_all.setter
     def disable_all(self, val):
         """Disable all obligation related checks."""
-        self._info['disable_all'] = 'True'
+        self._info['disable_all'] = str(val)
 
     @property
     def disable_measure_check(self):
@@ -175,19 +175,16 @@ def _construct_classpath(verifier : str = None):
                                (arpplugin_jar, 'arpplugin'))
             if jar and v != verifier)
 
-    if sys.platform.startswith('linux'):
-        if os.path.isdir('/usr/lib/viper'):
-            # Check if we have Viper installed via package manager.
-            return os.pathsep.join(
-                glob.glob('/usr/lib/viper/*.jar'))
-
     resources = resources_folder()
     silicon = os.path.join(resources, 'backends', 'silicon.jar')
     carbon = os.path.join(resources, 'backends', 'carbon.jar')
+    silver_sif = os.path.join(resources, 'backends', 'silver-sif-extension.jar')
+    silicon_sif = os.path.join(resources, 'backends', 'silicon-sif-extension.jar')
     return os.pathsep.join(
         jar for jar, v in ((silicon, 'carbon'),
                            (carbon, 'silicon'),
-                           (arpplugin_jar, 'arpplugin'))
+                           (silver_sif, 'silver-sif'),
+                           (silicon_sif, 'silicon-sif'))
         if jar and v != verifier)
 
 
@@ -203,11 +200,6 @@ def _get_boogie_path():
     if boogie_exe:
         return boogie_exe
 
-    if sys.platform.startswith('linux'):
-        if (os.path.exists('/usr/bin/boogie') and
-            os.path.exists('/usr/bin/mono')):
-            return '/usr/bin/boogie'
-
 
 def _get_z3_path():
     """ Tries to detect path to Z3 executable.
@@ -220,12 +212,9 @@ def _get_z3_path():
     if z3_exe:
         return z3_exe
 
-    if sys.platform.startswith('linux'):
-        if os.path.exists('/usr/bin/viper-z3'):
-            # First check if we have Z3 installed together with Viper.
-            return '/usr/bin/viper-z3'
-        if os.path.exists('/usr/bin/z3'):
-            return '/usr/bin/z3'
+    script_path = os.path.join(os.path.abspath(os.path.dirname(sys.argv[0])), 'z3')
+    if os.path.exists(script_path):
+        return script_path
 
     path = os.path.join(os.path.dirname(sys.executable),
                         'z3.exe' if sys.platform.startswith('win') else 'z3')

src/nagini_translation/lib/context.py

@@ -62,6 +62,7 @@ def __init__(self) -> None:
         self.are_function_constants_used = False
         self.are_threading_constants_used = False
         self.sif = False
+        self.allow_statements = False
 
     def get_fresh_int(self) -> int:
         """

src/nagini_translation/lib/errors/messages.py

@@ -77,6 +77,10 @@
         lambda n: 'Termination channel might exist.',
     'lock.invariant.not.established':
         lambda n: 'Lock invariant might not hold.',
+    'probabilistic.sif.violated':
+        lambda n: 'Probabilistic non-interference might not be satisfied.',
+    'possibilistic.sif.violated':
+        lambda n: 'Possibilistic non-interference might not be satisfied.'
 }
 
 REASONS = {
@@ -149,7 +153,7 @@
         lambda n: 'May not have permission to start thread.',
     'sif.fold':
         lambda n: 'The low parts of predicate {} might not hold.'.format(
-            get_target_name(n.args[0])),
+            get_target_name(n.args[0]) if n.args else 'lock invariant'),
     'sif.unfold':
         lambda n: 'The low parts of predicate {} might not hold.'.format(
             get_target_name(n.args[0])),
@@ -166,7 +170,15 @@
         lambda n: 'Function and loop termination must be proved to be low in possibilistic noninterference mode. '
                   'Use TerminatesSif(...) as the last precondition/loop invariant.',
     'high.branch':
-        lambda n: 'Branch condition {} might not be low.',
+        lambda n: 'Branch condition {} might not be low or reaching the loop might not be a low event.'.format(pprint(n)),
+    'high.receiver.type':
+        lambda n: 'Type of call receiver {} might not be low.'.format(pprint(n)),
+    'high.exception.type':
+        lambda n: 'Type of raised exception {} might not be low.'.format(pprint(n)),
+    'high.short.circuit':
+        lambda n: 'Short-circuiting behavior of expression {} might not be low.'.format(pprint(n)),
+    'high.comprehension':
+        lambda n: 'Comprehension {} might introduce high control flow'.format(pprint(n)),
 }
 
 VAGUE_REASONS = {

src/nagini_translation/lib/errors/rules.py

@@ -118,6 +118,30 @@ class Rules(Dict[Tuple[str, str], Tuple[str, str]]):
     ('fold.failed', 'assertion.false'):
         ('lock.invariant.not.established', 'assertion.false')
 }
+BRANCH_CONDITION_ASSERT = {
+    ('assert.failed', 'assertion.false'):
+        ('probabilistic.sif.violated', 'high.branch')
+}
+POSS_BRANCH_CONDITION_ASSERT = {
+    ('assert.failed', 'assertion.false'):
+        ('possibilistic.sif.violated', 'high.branch')
+}
+BRANCH_RECEIVER_LOW = {
+    ('assert.failed', 'assertion.false'):
+        ('probabilistic.sif.violated', 'high.receiver.type')
+}
+EXCEPTION_TYPE_LOW = {
+    ('assert.failed', 'assertion.false'):
+        ('probabilistic.sif.violated', 'high.exception.type')
+}
+SHORT_CIRCUIT_LOW = {
+    ('assert.failed', 'assertion.false'):
+        ('probabilistic.sif.violated', 'high.short.circuit')
+}
+COMPREHENSION_LOW = {
+    ('assert.failed', 'assertion.false'):
+        ('probabilistic.sif.violated', 'high.comprehension')
+}
 
 __all__ = (
     'Rules',
@@ -135,4 +159,9 @@ class Rules(Dict[Tuple[str, str], Tuple[str, str]]):
     'LOCAL_VARIABLE_NOT_DEFINED',
     'GLOBAL_NAME_NOT_DEFINED',
     'DEPENDENCIES_NOT_DEFINED',
+    'BRANCH_CONDITION_ASSERT',
+    'BRANCH_RECEIVER_LOW',
+    'EXCEPTION_TYPE_LOW',
+    'SHORT_CIRCUIT_LOW',
+    'COMPREHENSION_LOW',
 )

src/nagini_translation/lib/resolver.py

@@ -469,7 +469,7 @@ def _get_call_type(node: ast.Call, module: PythonModule,
 def get_subscript_type(node: ast.Subscript, module: PythonModule,
                         containers: List[ContainerInterface],
                         container: PythonNode) -> PythonType:
-    if (node._parent and isinstance(node._parent, ast.Assign) and
+    if (hasattr(node, '_parent') and node._parent and isinstance(node._parent, ast.Assign) and
             node is node._parent.value):
         # Constructor is assigned to variable;
         # we get the type of the dict from the type of the

src/nagini_translation/lib/typedefs.py

@@ -20,6 +20,8 @@
 
 VarAssign = 'silver.ast.LocalVarAssign'
 
+While = 'silver.ast.While'
+
 Domain = 'silver.ast.Domain'
 
 DomainAxiom = 'silver.ast.DomainAxiom'

src/nagini_translation/sif/lib/viper_ast_extended.py

@@ -8,7 +8,7 @@
 from typing import List, Optional
 
 from nagini_translation.lib.typedefs import (
-    Expr, Info, Position, Seqn, Stmt, Var, VarAssign
+    Expr, Info, Position, Seqn, Stmt, Var, VarAssign, While
 )
 from nagini_translation.lib.viper_ast import ViperAST
 from nagini_translation.sif.lib.util import (
@@ -69,6 +69,10 @@ def SIFExceptionHandler(self, err_var: Var, exception: Expr, handler: Seqn):
         return self.ast_extensions.SIFExceptionHandler(
             err_var, exception, handler, self.NoPosition, self.NoInfo, self.NoTrafos)
 
+    def SIFWhileElse(self, loop: While, els: Stmt):
+        return self.ast_extensions.SIFWhileElse(
+            loop, els, self.NoPosition, self.NoInfo, self.NoTrafos)
+
     def Try(self, body: Seqn, catch_blocks: List['silver.sif.SIFExceptionHandler'],
             else_block: Optional[Seqn], finally_block: Optional[Seqn],
             position: Position, info: Info):

src/nagini_translation/sif/translators/statement.py

@@ -9,6 +9,7 @@
 from typing import List
 
 from nagini_translation.lib.constants import ARBITRARY_BOOL_FUNC
+from nagini_translation.lib.errors import rules
 from nagini_translation.lib.program_nodes import PythonClass, PythonTryBlock, PythonVar
 from nagini_translation.lib.typedefs import Expr, Position, Seqn, Stmt, Var, VarDecl
 from nagini_translation.lib.util import flatten, get_body_indices, get_surrounding_try_blocks
@@ -110,7 +111,15 @@ def translate_stmt_Try(self, node: ast.Try, ctx: Context) -> List[Stmt]:
     def translate_stmt_Raise(self, node: ast.Raise, ctx: Context) -> List[Stmt]:
         err_var = self.get_error_var(node, ctx).ref()
         stmts = self._translate_stmt_raise_create(node, err_var, ctx)
-        return stmts[:-1] + [
+        ex_type_low = []
+        if ctx.sif == 'prob':
+            position = self.to_position(node.exc, ctx, rules=rules.EXCEPTION_TYPE_LOW)
+            info = self.no_info(ctx)
+            exc_expr = stmts[-1].rhs()
+            exc_type = self.type_factory.typeof(exc_expr, ctx)
+
+            ex_type_low.append(self.viper.Assert(self.viper.Low(exc_type, None, position, info), position, info))
+        return stmts[:-1] + ex_type_low + [
             self.viper.Raise(stmts[-1], self.to_position(node, ctx), self.no_info(ctx))
             ]
 

src/nagini_translation/tests.py

@@ -558,8 +558,9 @@ class VerificationTest(AnnotatedTest):
 
     def test_file(
             self, path: str, base: str, jvm: jvmaccess.JVM, verifier: ViperVerifier,
-            sif: bool, reload_resources: bool, arp: bool, store_viper: bool):
+            sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool):
         """Test specific Python file."""
+        config.obligation_config.disable_all = ignore_obligations
         annotation_manager = self.get_annotation_manager(path, verifier.name)
         if arp:
             pytest.skip('Ignoring ARP tests')
@@ -617,9 +618,9 @@ def _evaluate_result(
 _VERIFICATION_TESTER = VerificationTest()
 
 
-def test_verification(path, base, verifier, sif, reload_resources, arp, print):
+def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print):
     """Execute provided verification test."""
-    _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, print)
+    _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations, print)
 
 
 class TranslationTest(AnnotatedTest):