Merge

README.rst

@@ -1,19 +1,12 @@
 
-Nagini is an automatic verifier for statically typed Python programs, based on the `Viper <http://viper.ethz.ch>`_ verification infrastructure. Nagini is being developed at the `Chair of Programming Methodology <https://www.pm.inf.ethz.ch/research/nagini.html>`_ at ETH Zurich.
+Nagini is an automatic verifier for statically typed Python programs, based on the `Viper <http://viper.ethz.ch>`_ verification infrastructure. Nagini is being developed at the `Programming Methodology Group <https://www.pm.inf.ethz.ch/research/nagini.html>`_ at ETH Zurich.
 
 Our CAV 2018 tool paper describing Nagini can be found `here <http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=EilersMueller18.pdf>`_, and a more detailed description of its encoding can be found in `Marco Eilers' thesis <https://pm.inf.ethz.ch/publications/Eilers2022.pdf>`_. Also see `the Wiki <https://github.com/marcoeilers/nagini/wiki>`_ for the documentation of Nagini's specification language. 
 
-You can try a (rather slow) online version of Nagini `on this website <http://viper.ethz.ch/nagini-examples/>`_.
-
-For use with the PyCharm IDE, try the `Nagini PyCharm plugin <https://github.com/marcoeilers/nagini-pycharm>`_.
-
 Dependencies (Ubuntu Linux)
 ===================================
 
-Install Java 11 or newer (64 bit) and Python 3.10 (64 bit, other versions likely *will not work*) and the required libraries::
-
-    sudo apt-get install python3.10-dev
-
+Install Java 11 or newer (64 bit) and Python 3.10 (64 bit, other versions likely *will not work*) and the required libraries (python3-dev).
 For usage with Viper's verification condition generation backend Carbon, you will also need to install Boogie (version 2.15.9).
 
 Dependencies (Windows)
@@ -75,10 +68,8 @@ The following command line options are available::
     --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 probabilisitc non-
+                    non-intererence (for concurrent programs) or prob for probabilistic non-
                     interference (for concurrent programs).
-                    Requires silver-sif-extension to be on the classpath, and silicon-sif-
-                    extension when used with counterexamples.
 
     --z3           
                     Sets the path of the Z3 executable. Alternatively, the

setup.py

@@ -17,7 +17,7 @@
         packages=find_packages('src'),
         package_dir={'': 'src'},
         package_data={
-            '': ['*.sil', '*.index', '*.typed'],
+            '': ['*.sil', '*.json', '*.typed'],
             'nagini_translation.resources': ['backends/*.jar']
         },
         requires=[

src/nagini_contracts/contracts.py

@@ -26,7 +26,7 @@
 
 CONTRACT_WRAPPER_FUNCS = ['Requires', 'Ensures', 'Exsures', 'Invariant', 'Decreases']
 
-CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'Implies', 'Forall', 'IOForall', 'Forall2', 'Forall3', 'Forall6',
+CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'ResultT', 'Implies', 'Forall', 'IOForall', 'Forall2', 'Forall3', 'Forall6',
                   'Exists', 'Low', 'LowVal', 'LowEvent', 'Declassify', 'TerminatesSif',
                   'Acc', 'Rd', 'Wildcard', 'Fold', 'Unfold', 'Unfolding', 'Previous',
                   'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'ToMS', 'MaySet', 'MayCreate',
@@ -80,6 +80,11 @@ def Old(expr: T) -> T:
 def Result() -> Any:
     pass
 
+def ResultT(t: Type[V]) -> V:
+    """
+    Like Result() but explicitly typed to avoid Any types.
+    """
+    pass
 
 def RaisedException() -> Any:
     pass
@@ -521,6 +526,7 @@ def isNaN(f: float) -> bool:
         'Refute',
         'Old',
         'Result',
+        'ResultT',
         'RaisedException',
         'Implies',
         'Forall',

src/nagini_translation/conftest.py

@@ -174,7 +174,7 @@ def pytest_configure(config: 'pytest.config.Config'):
         for test in tests:
             _pytest_config.add_test(test)
         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):
+            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:
         _pytest_config.clear_tests()

src/nagini_translation/lib/resolver.py

@@ -326,8 +326,9 @@ def _do_get_type(node: ast.AST, containers: List[ContainerInterface],
         left_type = get_type(node.left, containers, container)
         right_type = get_type(node.right, containers, container)
 
+        func = None
         if left_type == right_type or isinstance(right_type, TypeVar):
-            return left_type.get_func_or_method(LEFT_OPERATOR_FUNCTIONS[type(node.op)]).type
+            func = left_type.get_func_or_method(LEFT_OPERATOR_FUNCTIONS[type(node.op)])
 
         else:
             right_func_name = RIGHT_OPERATOR_FUNCTIONS[type(node.op)]
@@ -336,13 +337,17 @@ def _do_get_type(node: ast.AST, containers: List[ContainerInterface],
             if right_type.issubtype(left_type) and right_func:
                 base_right_func = left_type.get_compatible_func_or_method(right_func_name, [right_type, left_type])
                 if right_func.overrides or base_right_func == None:
-                    return right_func.type
-
-            left_func = left_type.get_compatible_func_or_method(LEFT_OPERATOR_FUNCTIONS[type(node.op)], [left_type, right_type])
-            if left_func:
-                return left_func.type
-            if right_func:
-                return right_func.type
+                    func = right_func
+
+            if func is None:
+                left_func = left_type.get_compatible_func_or_method(LEFT_OPERATOR_FUNCTIONS[type(node.op)], [left_type, right_type])
+                if left_func:
+                    func = left_func
+                if right_func:
+                    func = right_func
+        if func is None:
+            raise UnsupportedException(node, 'Unsupported operator')
+        return func.type
 
     elif isinstance(node, ast.UnaryOp):
         if isinstance(node.op, ast.Not):
@@ -452,6 +457,8 @@ def _get_call_type(node: ast.Call, module: PythonModule,
         if node.func.id in CONTRACT_FUNCS:
             if node.func.id  == 'Result':
                 return current_function.type
+            elif node.func.id  == 'ResultT':
+                return get_target(node.args[0], containers, container)
             elif node.func.id == 'RaisedException':
                 ctxs = [cont for cont in containers if
                         hasattr(cont, 'var_aliases')]

src/nagini_translation/lib/typeinfo.py

@@ -213,6 +213,8 @@ def visit_call_expr(self, node: mypy.nodes.CallExpr):
             return
         if isinstance(node.callee, mypy.nodes.SuperExpr):
             return
+        if isinstance(node.callee, mypy.nodes.NameExpr) and node.callee.name == 'ResultT':
+            return
         for a in node.args:
             self.visit(a)
         self.visit(node.callee)

src/nagini_translation/lib/viper_ast.py

@@ -131,10 +131,11 @@ def Program(self, domains, fields, functions, predicates, methods, position, inf
 
     def Function(self, name, args, type, pres, posts, body, position, info):
         body = self.scala.Some(body) if body is not None else self.none
-        return self.ast.Function(name, self.to_seq(args), type,
-                                 self.to_seq(pres),
-                                 self.to_seq(posts),
-                                 body, position, info, self.NoTrafos)
+        function = getobject(self.java, self.ast, 'Function')
+        return function.apply(name, self.to_seq(args), type,
+                              self.to_seq(pres),
+                              self.to_seq(posts),
+                              body, position, info, self.NoTrafos)
 
     def Method(self, name, args, returns, pres, posts, locals, body, position,
                info):

src/nagini_translation/main.py

@@ -58,28 +58,32 @@
 TYPE_ERROR_MATCHER = re.compile(TYPE_ERROR_PATTERN)
 
 
-def parse_sil_file(sil_path: str, jvm, float_option: str = None):
+def parse_sil_file(sil_path: str, bv_path: str, bv_size: int, jvm, float_option: str = None):
     parser = getclass(jvm.java, jvm.viper.silver.parser, "FastParser")()
     tp = jvm.viper.silver.plugin.standard.termination.TerminationPlugin(None, None, None, parser)
     assert parser
     with open(sil_path, 'r') as file:
         text = file.read()
+    with open(bv_path, 'r') as file:
+        int_min = -(2 ** (bv_size - 1))
+        int_max = 2 ** (bv_size - 1) - 1
+        text += "\n" + file.read().replace("NBITS", str(bv_size)).replace("INT_MIN_VAL", str(int_min)).replace("INT_MAX_VAL", str(int_max))
     if float_option == "real":
         text = text.replace("float.sil", "float_real.sil")
     if float_option == "ieee32":
         text = text.replace("float.sil", "float_ieee32.sil")
     path = jvm.java.nio.file.Paths.get(sil_path, [])
     none = getobject(jvm.java, jvm.scala, "None")
     tp.beforeParse(text, False)
-    diskloader = getattr(getattr(jvm.viper.silver.ast.utility, "DiskLoader$"), "MODULE$")
+    diskloader = getobject(jvm.java, jvm.viper.silver.ast.utility, "DiskLoader")
     parsed = parser.parse(text, path, none, diskloader)
 
     parse_result = parsed
     parse_result.initProperties()
     resolver = jvm.viper.silver.parser.Resolver(parse_result)
     resolved = resolver.run()
     resolved = resolved.get()
-    translator = jvm.viper.silver.parser.Translator(resolved)
+    translator = getobject(jvm.java, jvm.viper.silver.parser, 'Translator').apply(resolved)
     # Reset messages in global Consistency object. Otherwise, left-over
     # translation errors from previous translations prevent loading of the
     # built-in silver files.
@@ -88,16 +92,17 @@ def parse_sil_file(sil_path: str, jvm, float_option: str = None):
     return program.get()
 
 
-def load_sil_files(jvm: JVM, sif: bool = False, float_option: str = None):
+def load_sil_files(jvm: JVM, bv_size: int, sif: bool = False, float_option: str = None):
     current_path = os.path.dirname(inspect.stack()[0][1])
+    default_path = os.path.join(current_path, 'resources')
     if sif:
         resources_path = os.path.join(current_path, 'sif', 'resources')
     else:
-        resources_path = os.path.join(current_path, 'resources')
-    return parse_sil_file(os.path.join(resources_path, 'all.sil'), jvm, float_option)
+        resources_path = default_path
+    return parse_sil_file(os.path.join(resources_path, 'all.sil'), os.path.join(default_path, 'intbv.sil'), bv_size, jvm, float_option)
 
 
-def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = None,
+def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), base_dir: str = None,
               sif: bool = False, arp: bool = False, ignore_global: bool = False,
               reload_resources: bool = False, verbose: bool = False,
               check_consistency: bool = False, float_encoding: str = None,
@@ -109,9 +114,9 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
     error_manager.clear()
     current_path = os.path.dirname(inspect.stack()[0][1])
     if sif:
-        preamble_path = os.path.join(current_path, 'sif', 'resources')
+        builtins_index_path = os.path.join(current_path, 'sif', 'resources')
     else:
-        preamble_path = os.path.join(current_path, 'resources')
+        builtins_index_path = os.path.join(current_path, 'resources')
 
     if sif:
         viper_ast = ViperASTExtended(jvm, jvm.java, jvm.scala, jvm.viper, path)
@@ -128,7 +133,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
 
     analyzer = Analyzer(types, path, selected)
     main_module = analyzer.module
-    with open(os.path.join(preamble_path, 'preamble.index'), 'r') as file:
+    with open(os.path.join(builtins_index_path, 'builtins.json'), 'r') as file:
         analyzer.add_native_silver_builtins(json.loads(file.read()))
 
     analyzer.initialize_io_analyzer()
@@ -141,7 +146,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
     analyzer.process(translator)
     if 'sil_programs' not in globals() or reload_resources:
         global sil_programs
-        sil_programs = load_sil_files(jvm, sif, float_encoding)
+        sil_programs = load_sil_files(jvm, bv_size, sif, float_encoding)
     modules = [main_module.global_module] + list(analyzer.modules.values())
     prog = translator.translate_program(modules, sil_programs, selected,
                                         arp=arp, ignore_global=ignore_global, sif=sif, float_encoding=float_encoding)
@@ -158,7 +163,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
                                      func_opt=True,
                                      all_low=analyzer.has_all_low)
         if counterexample:
-            prog = getattr(jvm.viper.silicon.sif, 'CounterexampleSIFTransformerO').transform(prog, False)
+            prog = getobject(jvm.java, jvm.viper.silicon.sif, 'CounterexampleSIFTransformerO').transform(prog, False)
         else:
             prog = getobject(jvm.java, jvm.viper.silver.sif, 'SIFExtendedTransformer').transform(prog, False)
         if verbose:
@@ -337,6 +342,12 @@ def main() -> None:
         action='store_true',
         default=False,
     )
+    parser.add_argument(
+        '--int-bitops-size',
+        help='Maximium size of integers for which bitwise operations are allowed.',
+        type=int,
+        default=8
+    )
     args = parser.parse_args()
 
     config.classpath = args.viper_jar_path
@@ -371,7 +382,7 @@ def main() -> None:
         socket = context.socket(zmq.REP)
         socket.bind(DEFAULT_SERVER_SOCKET)
         global sil_programs
-        sil_programs = load_sil_files(jvm, args.sif, args.float_encoding)
+        sil_programs = load_sil_files(args.int_bitops_size, args.jvm, args.sif, args.float_encoding)
 
         while True:
             file = socket.recv_string()
@@ -396,7 +407,7 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
     try:
         start = time.time()
         selected = set(args.select.split(',')) if args.select else set()
-        modules, prog = translate(python_file, jvm, selected=selected, sif=args.sif, base_dir=base_dir,
+        modules, prog = translate(python_file, jvm, args.int_bitops_size, selected=selected, sif=args.sif, base_dir=base_dir,
                                   ignore_global=args.ignore_global, arp=arp, verbose=args.verbose,
                                   counterexample=args.counterexample, float_encoding=args.float_encoding)
         if args.print_viper: