A bunch of stuff

src/nagini_contracts/contracts.py

@@ -433,7 +433,7 @@ def ToMS(s: PSeq[T]) -> PMultiset[T]:
 # The following annotations have no runtime semantics. They are only used for
 # the Python to Viper translation.
 
-def Acc(field, ratio=1) -> bool:
+def Acc(field, ratio: float=1) -> bool:
     """
     Access permission to field.
     0 < ratio < 1 means read-only access.

src/nagini_translation/conftest.py

@@ -42,6 +42,7 @@
 _IO_TESTS_DIR = 'tests/io/'
 _OBLIGATIONS_TESTS_DIR = 'tests/obligations/'
 _ARP_TESTS_DIR = 'tests/arp/'
+_STRICT_INT_TESTS_DIR = 'tests/strict-int/'
 
 
 class PyTestConfig:
@@ -86,6 +87,8 @@ def add_test(self, test: str):
             self._add_test_dir(_OBLIGATIONS_TESTS_DIR)
         elif test == 'arp':
             self._add_test_dir(_ARP_TESTS_DIR)
+        elif test == 'strict-int':
+            self._add_test_dir(_STRICT_INT_TESTS_DIR)
         elif test == _TRANSLATION_TESTS_SUFFIX:
             self._add_test_mode(_TRANSLATION_TESTS_SUFFIX)
         elif test == _VERIFICATION_TESTS_SUFFIX:
@@ -160,6 +163,7 @@ def pytest_addoption(parser: 'pytest.config.Parser'):
     parser.addoption('--io', dest='io', action='store_true')
     parser.addoption('--obligations', dest='obligations', action='store_true')
     parser.addoption('--arp', dest='arp', action='store_true')
+    parser.addoption('--strict-int-tests', dest='strict_int_tests', action='store_true')
     parser.addoption('--all-verifiers', dest='all_verifiers',
                      action='store_true')
     parser.addoption('--silicon', dest='silicon', action='store_true')
@@ -177,7 +181,7 @@ def pytest_configure(config: 'pytest.config.Config'):
     # Setup tests.
     tests = []
     if config.option.all_tests:
-        tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp']
+        tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp', 'strict-int']
     else:
         if config.option.functional:
             tests.append('functional')
@@ -195,6 +199,8 @@ def pytest_configure(config: 'pytest.config.Config'):
             tests.append('obligations')
         if config.option.arp:
             tests.append('arp')
+        if config.option.strict_int_tests:
+            tests.append('strict-int')
         if config.option.translation:
             tests.append('translation')
         if config.option.verification:
@@ -293,9 +299,10 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
                     sif = False
                 reload_resources = file in reload_triggers
                 arp = 'arp' in file
+                strict_int = 'strict-int' in file
                 base = file.partition('translation')[0] + 'translation'
-                params.append((file, base, sif, reload_resources, arp, float_encoding))
-        metafunc.parametrize('path,base,sif,reload_resources,arp,float_encoding', params)
+                params.append((file, base, sif, reload_resources, arp, strict_int, float_encoding))
+        metafunc.parametrize('path,base,sif,reload_resources,arp,strict_int,float_encoding', params)
     elif func_name == _VERIFICATION_TEST_FUNCTION_NAME:
         if not _pytest_config.selected_modes or 'verification' in _pytest_config.selected_modes:
             for test_dir in _pytest_config.verification_test_dirs:
@@ -331,12 +338,13 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
                 reload_resources = (file in reload_triggers) or (new_float_encoding != float_encoding)
                 float_encoding = new_float_encoding
                 arp = 'arp' in file
+                strict_int = 'strict-int' in file
                 base = file.partition('verification')[0] + 'verification'
                 params.extend([(file, base, verifier, sif, reload_resources, arp,
                                 ignore_obligations or (None if verifier == 'silicon' else False),
-                                _pytest_config.store_viper, float_encoding, select) for verifier
+                                _pytest_config.store_viper, float_encoding, select, strict_int) for verifier
                                in _pytest_config.verifiers])
-        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print,float_encoding,selection', params)
+        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print,float_encoding,selection,strict_int', params)
     else:
         pytest.exit('Unrecognized test function.')
 

src/nagini_translation/lib/context.py

@@ -64,6 +64,7 @@ def __init__(self) -> None:
         self.sif = False
         self.allow_statements = False
         self.float_encoding = None
+        self.strict_int = False
 
     def get_fresh_int(self) -> int:
         """

src/nagini_translation/main.py

@@ -111,7 +111,7 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
               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,
-              counterexample: bool = False) -> Tuple[List['PythonModule'], Program]:
+              counterexample: bool = False, strict_int: bool = False) -> Tuple[List['PythonModule'], Program]:
     """
     Translates the Python module at the given path to a Viper program
     """
@@ -154,7 +154,8 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
         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)
+                                        arp=arp, ignore_global=ignore_global, sif=sif, float_encoding=float_encoding,
+                                        strict_int=strict_int)
     if sif:
         set_all_low_methods(jvm, viper_ast.all_low_methods)
         set_preserves_low_methods(jvm, viper_ast.preserves_low_methods)
@@ -384,6 +385,12 @@ def main() -> None:
         type=int,
         default=8
     )
+    parser.add_argument(
+        '--strict-int',
+        action='store_true',
+        default=False,
+        help='Require exact int type (type(x) == int) rather than subtype (isinstance(x, int)) in many places.'
+    )
     parser.add_argument(
         '--disable-branch-conditions',
         help='Disable reporting of branch conditions for verification errors with the Silicon backend..',
@@ -506,7 +513,8 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             selected = set(args.select.split(',')) if args.select else set()
         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)
+                                  counterexample=args.counterexample, float_encoding=args.float_encoding,
+                                  strict_int=args.strict_int)
         if args.print_viper:
             if args.verbose:
                 print('Result:')
@@ -526,7 +534,8 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             for i in range(args.benchmark):
                 start = time.time()
                 modules, prog = translate(python_file, jvm, args.int_bitops_size, selected=selected, sif=args.sif, arp=arp, base_dir=base_dir,
-                                          ignore_global=args.ignore_global, float_encoding=args.float_encoding)
+                                          ignore_global=args.ignore_global, float_encoding=args.float_encoding,
+                                          strict_int=args.strict_int)
                 vresult = verify(modules, prog, python_file, jvm, viper_args, backend=backend, arp=arp)
                 end = time.time()
                 print("{}, {}, {}, {}, {}".format(
@@ -540,7 +549,7 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             vresult = verify(modules, prog, python_file, jvm, viper_args,
                              backend=backend, arp=arp, counterexample=args.counterexample,
                              sif=args.sif, disable_branch_conditions=args.disable_branch_conditions)
-            
+
             if submitter is not None:
                 submitter.setSuccess(vresult.__bool__())
                 submitter.submit()

src/nagini_translation/mcp_server.py

@@ -136,7 +136,7 @@ def configure(options: dict) -> dict:
 
     Recognized keys: `verifier` ('silicon' or 'carbon'), `z3Path`, `boogiePath`,
     `mypyPath`, `sif`, `intBitopsSize`, `floatEncoding`, `useViperServer`,
-    `disableBranchConditions`. `viperJarPath` cannot be changed after startup and
+    `disableBranchConditions`, `strictInt`. `viperJarPath` cannot be changed after startup and
     is ignored. Unknown or null keys are ignored. Changing
     `sif`/`intBitopsSize`/`floatEncoding` reloads the Silver resources;
     already-running verifications are unaffected.

src/nagini_translation/resources/bool.sil

@@ -325,6 +325,7 @@ function int___eq__(self: Ref, other: Ref): Bool
     ensures issubtype(typeof(other), int()) ==> result == int___unbox__(self) == int___unbox__(other)
     ensures issubtype(typeof(other), int()) ==> result == object___eq__(self, other)
     ensures issubtype(typeof(other), float()) ==> result == float___eq__(self, other)
+    ensures result == object___eq__(self, other)
 
 
 function bool___eq__(self: Ref, other: Ref): Bool

src/nagini_translation/resources/list.sil

@@ -20,7 +20,8 @@ function list___contains__(self: Ref, item: Ref): Bool
     decreases _
     requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
     requires acc(self.list_acc, wildcard)
-    ensures result == (item in self.list_acc)
+    ensures result == exists i: Ref :: object___eq__(item, i) && i in self.list_acc
+    ensures item in self.list_acc ==> result
 
 function list___bool__(self: Ref) : Bool
     decreases _

src/nagini_translation/resources/seq.sil

@@ -17,7 +17,8 @@ function PSeq___sil_seq__(box: Ref): Seq[Ref]
 function PSeq___contains__(self: Ref, item: Ref): Bool
     decreases _
     requires issubtype(typeof(self), PSeq(PSeq_arg(typeof(self), 0)))
-    ensures result == (item in PSeq___sil_seq__(self))
+    ensures result == exists i: Ref :: object___eq__(item, i) && i in PSeq___sil_seq__(self)
+    ensures item in PSeq___sil_seq__(self) ==> result
     ensures result ==> issubtype(typeof(item), PSeq_arg(typeof(self), 0))
 
 function PSeq___getitem__(self: Ref, index: Ref): Ref

src/nagini_translation/service.py

@@ -127,7 +127,9 @@ def __init__(self, *, z3_path: str = None, viper_jar_path: str = None,
                  int_bitops_size: int = 8, use_viper_server: bool = True,
                  verifier_backend: str = 'silicon', sif=False,
                  float_encoding: str = None,
-                 disable_branch_conditions: bool = False):
+                 disable_branch_conditions: bool = False,
+                 strict_int: bool = False,
+                 force_obligations: bool = False):
         if viper_jar_path:
             config.classpath = viper_jar_path
         if z3_path:
@@ -151,6 +153,10 @@ def __init__(self, *, z3_path: str = None, viper_jar_path: str = None,
         self._float_encoding = float_encoding
         self._bv_size = int_bitops_size
         self._disable_branch_conditions = disable_branch_conditions
+        self._strict_int = strict_int
+        if force_obligations:
+            # False instead of None: force the obligation encoding (see main.py).
+            config.obligation_config.disable_all = False
         # The obligation encoding is auto-detected per program by translate(),
         # which persistently sets obligation_config.disable_all once a program
         # without obligations is seen. In a long-lived service that would then
@@ -280,6 +286,7 @@ def current_options(self) -> dict:
             'floatEncoding': self._float_encoding,
             'useViperServer': config.use_viper_server,
             'disableBranchConditions': self._disable_branch_conditions,
+            'strictInt': self._strict_int,
             'z3Path': config.z3_path,
             'boogiePath': config.boogie_path,
             'mypyPath': config.mypy_path,
@@ -313,6 +320,8 @@ def reconfigure(self, **options) -> dict:
             if options.get('disable_branch_conditions') is not None:
                 self._disable_branch_conditions = bool(
                     options['disable_branch_conditions'])
+            if options.get('strict_int') is not None:
+                self._strict_int = bool(options['strict_int'])
             reload_needed = False
             if options.get('sif') is not None and options['sif'] != self._sif:
                 self._sif = options['sif']
@@ -349,7 +358,8 @@ def _verify_concurrent(self, path, selected, base_dir, counterexample,
                     path, self.jvm, self._bv_size,
                     selected=set(selected) if selected else set(), sif=False,
                     base_dir=base_dir, arp=False, counterexample=counterexample,
-                    ignore_global=ignore_global, float_encoding=self._float_encoding)
+                    ignore_global=ignore_global, float_encoding=self._float_encoding,
+                    strict_int=self._strict_int)
             except (TypeException, InvalidProgramException, UnsupportedException) as e:
                 return VerifyResult(False, self._exception_diagnostics(e, path),
                                     time.time() - start, translation_failed=True)
@@ -427,7 +437,8 @@ def _verify_serial(self, path, selected, base_dir, arp,
                 path, self.jvm, self._bv_size, selected=selected_set,
                 sif=self._sif, base_dir=base_dir, arp=arp,
                 counterexample=counterexample, ignore_global=ignore_global,
-                float_encoding=self._float_encoding)
+                float_encoding=self._float_encoding,
+                strict_int=self._strict_int)
             if translated is None:
                 return VerifyResult(False, [self._point_diagnostic(
                     path, 'Type checking failed.', 'type.error')],
@@ -550,6 +561,7 @@ def _point_diagnostic(path: str, message: str, code: str) -> Diagnostic:
     'floatEncoding': 'float_encoding',
     'useViperServer': 'use_viper_server',
     'disableBranchConditions': 'disable_branch_conditions',
+    'strictInt': 'strict_int',
 }
 
 
@@ -586,6 +598,12 @@ def add_service_arguments(parser: argparse.ArgumentParser) -> argparse.ArgumentP
                              'errors (Silicon backend)')
     parser.add_argument('--no-viper-server', action='store_true',
                         help='disable the in-process ViperServer backend')
+    parser.add_argument('--strict-int', action='store_true', default=False,
+                        help='require exact int type (type(x) == int) rather '
+                             'than subtype (isinstance(x, int)) in many places')
+    parser.add_argument('--force-obligations', action='store_true', default=False,
+                        help='force use of the obligations encoding used to '
+                             'verify liveness properties')
     return parser
 
 
@@ -601,7 +619,8 @@ def service_kwargs_from_args(args: argparse.Namespace) -> dict:
         mypy_path=args.mypy_path, int_bitops_size=args.int_bitops_size,
         use_viper_server=not args.no_viper_server, verifier_backend=args.verifier,
         sif=args.sif, float_encoding=args.float_encoding,
-        disable_branch_conditions=args.disable_branch_conditions)
+        disable_branch_conditions=args.disable_branch_conditions,
+        strict_int=args.strict_int, force_obligations=args.force_obligations)
 
 
 def make_service(args: argparse.Namespace) -> VerificationService:

src/nagini_translation/tests.py

@@ -582,7 +582,7 @@ class VerificationTest(AnnotatedTest):
     def test_file(
             self, path: str, base: str, jvm: jvmaccess.JVM, verifier: ViperVerifier,
             sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool,
-            float_encoding: Optional[str], selection: Set[str]):
+            float_encoding: Optional[str], selection: Set[str], strict_int: bool = False):
         """Test specific Python file."""
         config.obligation_config.disable_all = ignore_obligations
         annotation_manager = self.get_annotation_manager(path, verifier.name)
@@ -593,7 +593,7 @@ def test_file(
         abspath = os.path.abspath(path)
         absbase = os.path.abspath(base)
         modules, prog = translate(abspath, jvm, 8, base_dir=absbase, sif=sif, arp=arp, reload_resources=reload_resources,
-                                  float_encoding=float_encoding, selected=selection)
+                                  float_encoding=float_encoding, selected=selection, strict_int=strict_int)
         assert prog is not None
         if store_viper:
             import string
@@ -643,17 +643,18 @@ def _evaluate_result(
 _VERIFICATION_TESTER = VerificationTest()
 
 
-def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print, float_encoding, selection):
+def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print, float_encoding, selection, strict_int):
     """Execute provided verification test."""
     _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations,
-                                   print, float_encoding, selection)
+                                   print, float_encoding, selection, strict_int)
 
 
 class TranslationTest(AnnotatedTest):
     """Test for testing translation errors."""
 
     def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
-                  reload_resources: bool, arp: bool, float_encoding: Optional[str]):
+                  reload_resources: bool, arp: bool, float_encoding: Optional[str],
+                  strict_int: bool = False):
         """Test specific Python file."""
         annotation_manager = self.get_annotation_manager(path, _BACKEND_ANY)
         if annotation_manager.ignore_file():
@@ -662,7 +663,7 @@ def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
         base = os.path.abspath(base)
         try:
             translate(path, jvm, 8, base_dir=base, sif=sif, arp=arp, reload_resources=reload_resources,
-                      float_encoding=float_encoding)
+                      float_encoding=float_encoding, strict_int=strict_int)
             actual_errors = []
         except InvalidProgramException as exp1:
             actual_errors = [InvalidProgramError(exp1)]
@@ -680,6 +681,6 @@ def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
 _TRANSLATION_TESTER = TranslationTest()
 
 
-def test_translation(path, base, sif, reload_resources, arp, float_encoding):
+def test_translation(path, base, sif, reload_resources, arp, strict_int, float_encoding):
     """Execute provided translation test."""
-    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp, float_encoding)
+    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp, float_encoding, strict_int)

src/nagini_translation/translator.py

@@ -91,14 +91,16 @@ def translate_program(self, modules: List[PythonModule], sil_progs: List,
                           ignore_global: bool = False,
                           arp: bool = False,
                           float_encoding : str = None,
-                          sif = False) -> 'silver.ast.Program':
+                          sif = False,
+                          strict_int: bool = False) -> 'silver.ast.Program':
         ctx = Context()
         ctx.sif = sif
         ctx.current_class = None
         ctx.current_function = None
         ctx.module = modules[0]
         ctx.arp = arp
         ctx.float_encoding = float_encoding
+        ctx.strict_int = strict_int
         return self.prog_translator.translate_program(modules, sil_progs, ctx,
                                                       selected, ignore_global)