From 59ab44d3d139121c67cc8811ba9359f0ae38fd07 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 26 Mar 2026 11:35:27 +0100 Subject: [PATCH 01/17] better error message for unsupported --- src/nagini_translation/lib/util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/nagini_translation/lib/util.py b/src/nagini_translation/lib/util.py index f11f2fb45..cd021268b 100644 --- a/src/nagini_translation/lib/util.py +++ b/src/nagini_translation/lib/util.py @@ -55,6 +55,8 @@ class UnsupportedException(Exception): def __init__(self, ast_element: ast.AST, desc=""): self.node = ast_element + if not desc: + desc = type(ast_element).__name__ self.desc = desc super().__init__(desc) From e676cce2199f9abb17536030d6ef61b986ca554a Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 26 Mar 2026 11:35:58 +0100 Subject: [PATCH 02/17] added support for list.insert and fixed list mul bug --- .../resources/builtins.json | 5 +++++ src/nagini_translation/resources/list.sil | 13 +++++++++++- tests/functional/verification/test_lists.py | 20 +++++++++++++++++++ 3 files changed, 37 insertions(+), 1 deletion(-) diff --git a/src/nagini_translation/resources/builtins.json b/src/nagini_translation/resources/builtins.json index fdd6e2b24..34137ea8e 100644 --- a/src/nagini_translation/resources/builtins.json +++ b/src/nagini_translation/resources/builtins.json @@ -42,6 +42,11 @@ "type": null, "MustTerminate": true }, + "insert": { + "args": ["list", "__prim__int", "object"], + "type": null, + "MustTerminate": true + }, "extend": { "args": ["list", "list"], "type": null, diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index a335abb69..3759f5c3e 100644 --- a/src/nagini_translation/resources/list.sil +++ b/src/nagini_translation/resources/list.sil @@ -72,6 +72,17 @@ method list___setitem__(self: Ref, key: Int, item: Ref) returns () assume false } +method list_insert(self: Ref, index: Int, item: Ref) returns () + requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) + requires acc(self.list_acc) + requires issubtype(typeof(item), list_arg(typeof(self), 0)) + ensures acc(self.list_acc) + ensures let clamped == ((index < 0 ? 0 : (index > |old(self.list_acc)| ? |old(self.list_acc)| : index))) in + self.list_acc == old(self.list_acc)[..clamped] ++ Seq(item) ++ old(self.list_acc)[clamped..] +{ + assume false +} + method list_append(self: Ref, item: Ref) returns () requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) requires acc(self.list_acc) @@ -112,7 +123,7 @@ method list___mul__(self: Ref, factor: Int) returns (res: Ref) ensures acc(res.list_acc) ensures |res.list_acc| == (factor > 0 ? factor : 0) * |self.list_acc| ensures factor > 0 ==> (forall i: Int :: {res.list_acc[i]} - i >= 0 && i < |res.list_acc| ==> res.list_acc[i] == self.list_acc[i \ factor]) + i >= 0 && i < |res.list_acc| ==> res.list_acc[i] == self.list_acc[i % |self.list_acc|]) method list_reverse(self: Ref) returns (res: Ref) requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) diff --git a/tests/functional/verification/test_lists.py b/tests/functional/verification/test_lists.py index 3b054bba7..4ba97f771 100644 --- a/tests/functional/verification/test_lists.py +++ b/tests/functional/verification/test_lists.py @@ -103,6 +103,26 @@ def test_append() -> None: #:: ExpectedOutput(assert.failed:assertion.false) Assert(mylist[0] == super4) +def test_insert() -> None: + super1 = Super() + super2 = Super() + super3 = Super() + mylist = [super1, super2] + Assert(len(mylist) == 2) + super4 = Super() + mylist.insert(1, super4) + Assert(len(mylist) == 3) + Assert(mylist[0] == super1) + Assert(mylist[1] == super4) + Assert(mylist[2] == super2) + mylist.insert(0, super3) + Assert(len(mylist) == 4) + Assert(mylist[0] == super3) + Assert(mylist[1] == super1) + #:: ExpectedOutput(assert.failed:assertion.false) + Assert(mylist[0] == super1) + + def test_extend() -> None: super1 = Super() super2 = Super() From 17c03036d63e566bb5505356271ee203d6d231d3 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 26 Mar 2026 12:21:37 +0100 Subject: [PATCH 03/17] correct support for list.insert negative indexes --- src/nagini_translation/resources/list.sil | 5 +++-- tests/functional/verification/test_lists.py | 19 +++++++++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index 3759f5c3e..5eb554bdb 100644 --- a/src/nagini_translation/resources/list.sil +++ b/src/nagini_translation/resources/list.sil @@ -77,8 +77,9 @@ method list_insert(self: Ref, index: Int, item: Ref) returns () requires acc(self.list_acc) requires issubtype(typeof(item), list_arg(typeof(self), 0)) ensures acc(self.list_acc) - ensures let clamped == ((index < 0 ? 0 : (index > |old(self.list_acc)| ? |old(self.list_acc)| : index))) in - self.list_acc == old(self.list_acc)[..clamped] ++ Seq(item) ++ old(self.list_acc)[clamped..] + ensures let resolved == ((index < 0 ? index + |old(self.list_acc)| : index)) in + let clamped == ((resolved < 0 ? 0 : (resolved > |old(self.list_acc)| ? |old(self.list_acc)| : resolved))) in + self.list_acc == old(self.list_acc)[..clamped] ++ Seq(item) ++ old(self.list_acc)[clamped..] { assume false } diff --git a/tests/functional/verification/test_lists.py b/tests/functional/verification/test_lists.py index 4ba97f771..9a184e351 100644 --- a/tests/functional/verification/test_lists.py +++ b/tests/functional/verification/test_lists.py @@ -109,16 +109,35 @@ def test_insert() -> None: super3 = Super() mylist = [super1, super2] Assert(len(mylist) == 2) + # Insert in the middle super4 = Super() mylist.insert(1, super4) Assert(len(mylist) == 3) Assert(mylist[0] == super1) Assert(mylist[1] == super4) Assert(mylist[2] == super2) + # Insert at the beginning mylist.insert(0, super3) Assert(len(mylist) == 4) Assert(mylist[0] == super3) Assert(mylist[1] == super1) + # Insert with negative index (from end) + super5 = Super() + mylist.insert(-1, super5) + Assert(len(mylist) == 5) + Assert(mylist[3] == super5) + Assert(mylist[4] == super2) + # Insert past the end (should append) + super6 = Super() + mylist.insert(100, super6) + Assert(len(mylist) == 6) + Assert(mylist[5] == super6) + # Insert with negative index past the beginning (should prepend, no wrap) + super7 = Super() + mylist.insert(-100, super7) + Assert(len(mylist) == 7) + Assert(mylist[0] == super7) + Assert(mylist[1] == super3) #:: ExpectedOutput(assert.failed:assertion.false) Assert(mylist[0] == super1) From f1ceae93cf8b991a09467de6379d7591ccf13830 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 26 Mar 2026 14:54:01 +0100 Subject: [PATCH 04/17] Better list contains encoding for ints --- src/nagini_translation/resources/bool.sil | 1 + src/nagini_translation/resources/list.sil | 3 ++- src/nagini_translation/resources/seq.sil | 3 ++- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index 3718a3d7d..66f6ec6e7 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -154,6 +154,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 diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index 5eb554bdb..2fc1d89bf 100644 --- a/src/nagini_translation/resources/list.sil +++ b/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 _ diff --git a/src/nagini_translation/resources/seq.sil b/src/nagini_translation/resources/seq.sil index 38e1fd88d..9e467f75e 100644 --- a/src/nagini_translation/resources/seq.sil +++ b/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 From ea0c7895dc2f3f27cb7b0538520985ea768a1316 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 30 Mar 2026 11:22:51 +0200 Subject: [PATCH 05/17] Added strict-int mode --- src/nagini_translation/lib/context.py | 1 + src/nagini_translation/main.py | 13 ++++++++++--- src/nagini_translation/translator.py | 4 +++- .../translators/type_domain_factory.py | 4 ++++ 4 files changed, 18 insertions(+), 4 deletions(-) diff --git a/src/nagini_translation/lib/context.py b/src/nagini_translation/lib/context.py index 21f859e4d..69eb287c3 100644 --- a/src/nagini_translation/lib/context.py +++ b/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: """ diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py index 9bad89d54..940b9e74e 100755 --- a/src/nagini_translation/main.py +++ b/src/nagini_translation/main.py @@ -103,7 +103,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 """ @@ -146,7 +146,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) @@ -350,6 +351,11 @@ def main() -> None: type=int, default=8 ) + parser.add_argument( + '--strict-int', + action='store_true', + help='Require exact int type (type(x) == int) rather than subtype (isinstance(x, int)) in many places.' + ) args = parser.parse_args() config.classpath = args.viper_jar_path @@ -415,7 +421,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:') diff --git a/src/nagini_translation/translator.py b/src/nagini_translation/translator.py index 8950df903..e10215fd5 100644 --- a/src/nagini_translation/translator.py +++ b/src/nagini_translation/translator.py @@ -91,7 +91,8 @@ 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 @@ -99,6 +100,7 @@ def translate_program(self, modules: List[PythonModule], sil_progs: List, 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) diff --git a/src/nagini_translation/translators/type_domain_factory.py b/src/nagini_translation/translators/type_domain_factory.py index 6082137a5..7f27ac2b8 100644 --- a/src/nagini_translation/translators/type_domain_factory.py +++ b/src/nagini_translation/translators/type_domain_factory.py @@ -819,6 +819,10 @@ def type_check(self, lhs: 'Expr', type: 'PythonType', is a subtype of (or, if ``concrete`` is true, equivalent to) the given ``type``. """ + if (ctx.strict_int + and isinstance(type, PythonClass) + and type.name == 'int'): + concrete = True info = self.no_info(ctx) type_func = self.typeof(lhs, ctx) if isinstance(type, OptionalType): From 64844bba8af2ecabc4c50c0d6076648e0d67fa49 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 30 Mar 2026 15:14:02 +0200 Subject: [PATCH 06/17] strict-int tests --- src/nagini_translation/conftest.py | 18 ++++++++---- src/nagini_translation/tests.py | 17 ++++++----- .../verification/test_strict_int.py | 29 +++++++++++++++++++ 3 files changed, 51 insertions(+), 13 deletions(-) create mode 100644 tests/strict-int/verification/test_strict_int.py diff --git a/src/nagini_translation/conftest.py b/src/nagini_translation/conftest.py index 41130311c..757a0bad6 100644 --- a/src/nagini_translation/conftest.py +++ b/src/nagini_translation/conftest.py @@ -33,6 +33,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: @@ -77,6 +78,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: @@ -151,6 +154,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') @@ -165,7 +169,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') @@ -183,6 +187,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: @@ -270,9 +276,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: @@ -308,12 +315,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.') diff --git a/src/nagini_translation/tests.py b/src/nagini_translation/tests.py index 1539da33f..67b2fd893 100644 --- a/src/nagini_translation/tests.py +++ b/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) diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py new file mode 100644 index 000000000..3d172deab --- /dev/null +++ b/tests/strict-int/verification/test_strict_int.py @@ -0,0 +1,29 @@ +""" +Copyright (c) 2019 ETH Zurich +This Source Code Form is subject to the terms of the Mozilla Public +License, v. 2.0. If a copy of the MPL was not distributed with this +file, You can obtain one at http://mozilla.org/MPL/2.0/. +""" +from nagini_contracts.contracts import * + + +def takes_int(x: int) -> None: + Requires(True) + + +def test_int_arg_accepted() -> None: + takes_int(42) + + +def test_bool_arg_rejected() -> None: + #:: ExpectedOutput(call.precondition:assertion.false) + takes_int(True) + + +def returns_bool_as_int() -> int: + #:: ExpectedOutput(postcondition.violated:assertion.false) + return True + + +def test_forall_int_verifies() -> None: + Assert(Forall(int, lambda k: (k is not True and k is not False, []))) From fe6569d220ce73745fcdf696457bdfceb1193f07 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 8 Apr 2026 14:15:07 +0200 Subject: [PATCH 07/17] client server cli arguments --- src/nagini_translation/client.py | 39 ++++++++++++++++++++++++++++++-- src/nagini_translation/main.py | 14 ++++++++++-- 2 files changed, 49 insertions(+), 4 deletions(-) diff --git a/src/nagini_translation/client.py b/src/nagini_translation/client.py index aebfc6f01..1373a96da 100644 --- a/src/nagini_translation/client.py +++ b/src/nagini_translation/client.py @@ -6,6 +6,7 @@ """ import argparse +import json import zmq from nagini_translation.lib.constants import DEFAULT_CLIENT_SOCKET @@ -20,13 +21,47 @@ def main(): parser.add_argument( 'python_file', help='Python file to verify') + parser.add_argument( + '--write-viper-to-file', + default=None, + help='write generated Viper program to specified file') + parser.add_argument( + '-v', '--verbose', + action='store_true', + default=None, + help='increase output verbosity') + parser.add_argument( + '--show-viper-errors', + action='store_true', + default=None, + help='show Viper-level error messages if no Python errors are available') + parser.add_argument( + '--select', + default=None, + help='select specific methods or classes to verify, separated by commas') + parser.add_argument( + '--counterexample', + action='store_true', + default=None, + help='return a counterexample for every verification error if possible') + parser.add_argument( + '--viper-arg', + default=None, + help='Arguments to be forwarded to Viper, separated by commas') args = parser.parse_args() - socket.send_string(args.python_file) + # Build request: always include python_file, only include other args + # if explicitly provided (non-None), so the server uses its own defaults. + request = {'python_file': args.python_file} + for key, value in vars(args).items(): + if key != 'python_file' and value is not None: + request[key] = value + + socket.send_string(json.dumps(request)) response = socket.recv_string() print(response) if __name__ == '__main__': - main() \ No newline at end of file + main() diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py index 940b9e74e..750fa1e6e 100755 --- a/src/nagini_translation/main.py +++ b/src/nagini_translation/main.py @@ -7,6 +7,7 @@ import argparse import astunparse +import copy import inspect import json import logging @@ -397,13 +398,22 @@ def main() -> None: sil_programs = load_sil_files(jvm, args.int_bitops_size, args.sif, args.float_encoding) while True: - file = socket.recv_string() + message = socket.recv_string() response = [''] + request = json.loads(message) + file = request['python_file'] + + # Build per-request args: start from server args, apply client overrides + req_args = copy.copy(args) + for key, value in request.items(): + if key != 'python_file': + setattr(req_args, key, value) + def add_response(part): response[0] = response[0] + '\n' + part - translate_and_verify(file, jvm, args, add_response, arp=args.arp, base_dir=args.base_dir) + translate_and_verify(file, jvm, req_args, add_response, arp=req_args.arp, base_dir=req_args.base_dir) socket.send_string(response[0]) else: success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir) From 9635db218cfef2d0b63f9e05324b98cd50e1856c Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 8 Apr 2026 14:15:38 +0200 Subject: [PATCH 08/17] handle siliocn timeouts --- src/nagini_translation/lib/errors/manager.py | 10 +++++--- src/nagini_translation/lib/errors/wrappers.py | 25 +++++++++++++------ 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/src/nagini_translation/lib/errors/manager.py b/src/nagini_translation/lib/errors/manager.py index 8c922d021..b4cf25961 100644 --- a/src/nagini_translation/lib/errors/manager.py +++ b/src/nagini_translation/lib/errors/manager.py @@ -115,15 +115,17 @@ def transformError(self, error: 'AbstractVerificationError') -> 'AbstractVerific def _convert_error( self, original_error: 'AbstractVerificationError', jvm: JVM, modules, sif) -> Error: + if 'Timeout' in original_error.getClass().getSimpleName(): + return Error(original_error, {}, None) error = self.transformError(original_error) - reason_pos = error.reason().offendingNode().pos() - reason_item = self._get_item(reason_pos) + viper_reason = error.reason() if hasattr(error, 'reason') else None + reason_item = self._get_item(viper_reason.offendingNode().pos()) if viper_reason is not None else None position = error.pos() rules = self._try_get_rules_workaround( error.offendingNode(), jvm) - if rules is None: + if rules is None and viper_reason is not None: rules = self._try_get_rules_workaround( - error.reason().offendingNode(), jvm) + viper_reason.offendingNode(), jvm) if rules is None: rules = {} error_item = self._get_item(position) diff --git a/src/nagini_translation/lib/errors/wrappers.py b/src/nagini_translation/lib/errors/wrappers.py index d9c747131..aa7cf6235 100644 --- a/src/nagini_translation/lib/errors/wrappers.py +++ b/src/nagini_translation/lib/errors/wrappers.py @@ -102,12 +102,15 @@ def __init__(self, error: 'AbstractVerificationError', rules: Rules, vias: List[Any] = None, inputs: List[Any] = None) -> None: # Translate error id. - viper_reason = error.reason() - error_id = error.id() - reason_id = viper_reason.id() - key = error_id, reason_id - if key in rules: - error_id, reason_id = rules[key] + viper_reason = error.reason() if hasattr(error, 'reason') else None + error_id = error.id() if hasattr(error, 'id') else error.getClass().getSimpleName() + if viper_reason is not None: + reason_id = viper_reason.id() + key = error_id, reason_id + if key in rules: + error_id, reason_id = rules[key] + else: + reason_id = None # Construct object. self._error = error @@ -115,12 +118,14 @@ def __init__(self, error: 'AbstractVerificationError', rules: Rules, self._vias = vias self._inputs = inputs self.identifier = error_id - if reason_item: + if viper_reason is not None and reason_item: self.reason = Reason( reason_id, viper_reason, reason_item.node, reason_item.vias, reason_item.reason_string) - else: + elif viper_reason is not None: self.reason = Reason(reason_id, viper_reason) + else: + self.reason = None self.position = Position(error.pos()) def pos(self) -> 'ast.AbstractSourcePosition': @@ -181,6 +186,10 @@ def string(self, ide_mode: bool, show_viper_errors: bool) -> str: The second parameter determines if the message may show Viper-level error explanations if no Python-level explanation is available. """ + if self.reason is None: + if 'Timeout' in self._error.getClass().getSimpleName(): + return 'Verification timed out' + return self._error.readableMessage() if ide_mode: return '{0}:{1}:{2}:{3}:{4}: error: {5} {6}'.format( self.position.file_name, From 40db43ca2d88877dac3afe6edb286dd8b8d1763b Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 15 Apr 2026 16:06:33 +0200 Subject: [PATCH 09/17] Better client error reporting --- src/nagini_translation/client.py | 6 ++++-- src/nagini_translation/main.py | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/nagini_translation/client.py b/src/nagini_translation/client.py index 1373a96da..e58abea98 100644 --- a/src/nagini_translation/client.py +++ b/src/nagini_translation/client.py @@ -7,6 +7,7 @@ import argparse import json +import sys import zmq from nagini_translation.lib.constants import DEFAULT_CLIENT_SOCKET @@ -59,9 +60,10 @@ def main(): request[key] = value socket.send_string(json.dumps(request)) - response = socket.recv_string() + response = json.loads(socket.recv_string()) - print(response) + print(response['output']) + sys.exit(0 if response['success'] else 1) if __name__ == '__main__': main() diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py index 750fa1e6e..88bf477f3 100755 --- a/src/nagini_translation/main.py +++ b/src/nagini_translation/main.py @@ -355,6 +355,7 @@ def main() -> None: parser.add_argument( '--strict-int', action='store_true', + default=True, help='Require exact int type (type(x) == int) rather than subtype (isinstance(x, int)) in many places.' ) args = parser.parse_args() @@ -413,8 +414,8 @@ def main() -> None: def add_response(part): response[0] = response[0] + '\n' + part - translate_and_verify(file, jvm, req_args, add_response, arp=req_args.arp, base_dir=req_args.base_dir) - socket.send_string(response[0]) + success = translate_and_verify(file, jvm, req_args, add_response, arp=req_args.arp, base_dir=req_args.base_dir) + socket.send_string(json.dumps({'output': response[0], 'success': success})) else: success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir) sys.exit(0 if success else 1) From 9e382af1242d1ff3a395cc024d3fd07b7d660320 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 16 Apr 2026 14:29:19 +0200 Subject: [PATCH 10/17] more try/catch for silicon crashing --- src/nagini_translation/main.py | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py index 88bf477f3..6b4d2eae0 100755 --- a/src/nagini_translation/main.py +++ b/src/nagini_translation/main.py @@ -402,19 +402,24 @@ def main() -> None: message = socket.recv_string() response = [''] - request = json.loads(message) - file = request['python_file'] - - # Build per-request args: start from server args, apply client overrides - req_args = copy.copy(args) - for key, value in request.items(): - if key != 'python_file': - setattr(req_args, key, value) - def add_response(part): response[0] = response[0] + '\n' + part - success = translate_and_verify(file, jvm, req_args, add_response, arp=req_args.arp, base_dir=req_args.base_dir) + try: + request = json.loads(message) + file = request['python_file'] + + # Build per-request args: start from server args, apply client overrides + req_args = copy.copy(args) + for key, value in request.items(): + if key != 'python_file': + setattr(req_args, key, value) + + success = translate_and_verify(file, jvm, req_args, add_response, arp=req_args.arp, base_dir=req_args.base_dir) + except Exception: + add_response("Server error while handling request:") + add_response(traceback.format_exc()) + success = False socket.send_string(json.dumps({'output': response[0], 'success': success})) else: success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir) @@ -466,7 +471,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) - + if submitter is not None: submitter.setSuccess(vresult.__bool__()) submitter.submit() From 64eb851c087458148ae74aad0998d193e86463bc Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 21 Apr 2026 11:27:21 +0200 Subject: [PATCH 11/17] added list.copy() --- .../resources/builtins.json | 5 +++++ src/nagini_translation/resources/list.sil | 9 ++++++++ tests/functional/verification/test_lists.py | 22 ++++++++++++++++++- 3 files changed, 35 insertions(+), 1 deletion(-) diff --git a/src/nagini_translation/resources/builtins.json b/src/nagini_translation/resources/builtins.json index 34137ea8e..7736a0982 100644 --- a/src/nagini_translation/resources/builtins.json +++ b/src/nagini_translation/resources/builtins.json @@ -57,6 +57,11 @@ "type": "list", "MustTerminate": true }, + "copy": { + "args": ["list"], + "type": "list", + "MustTerminate": true + }, "__setitem__": { "args": ["list", "__prim__int", "object"], "type": null, diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index 2fc1d89bf..2c799fe1a 100644 --- a/src/nagini_translation/resources/list.sil +++ b/src/nagini_translation/resources/list.sil @@ -136,6 +136,15 @@ method list_reverse(self: Ref) returns (res: Ref) ensures |res.list_acc| == |self.list_acc| ensures forall i: Int :: {res.list_acc[i]} ((i >= 0 && i < |res.list_acc|) ==> (res.list_acc[i] == self.list_acc[|self.list_acc| - 1 - i])) +method list_copy(self: Ref) returns (res: Ref) + requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) + requires acc(self.list_acc, 1/100) + ensures issubtype(typeof(res), list(list_arg(typeof(self), 0))) + ensures res != self + ensures acc(self.list_acc, 1/100) + ensures acc(res.list_acc) + ensures res.list_acc == self.list_acc + method list___iter__(self: Ref) returns (_res: Ref) requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) requires acc(self.list_acc, 1 / 10) diff --git a/tests/functional/verification/test_lists.py b/tests/functional/verification/test_lists.py index 9a184e351..7193d4893 100644 --- a/tests/functional/verification/test_lists.py +++ b/tests/functional/verification/test_lists.py @@ -190,4 +190,24 @@ def test_mul() -> None: assert newlist[2] is super1 assert newlist[5] is super2 #:: ExpectedOutput(assert.failed:assertion.false) - assert mylist[1] is super1 \ No newline at end of file + assert mylist[1] is super1 + + +def test_copy() -> None: + super1 = Super() + super2 = Super() + super3 = Super() + mylist = [super1, super2, super3] + mylist2 = mylist.copy() + assert len(mylist2) == 3 + assert mylist2[0] is super1 + assert mylist2[1] is super2 + assert mylist2[2] is super3 + mylist.append(super1) + assert len(mylist) == 4 + assert len(mylist2) == 3 + mylist2[0] = super3 + assert mylist[0] is super1 + assert mylist2[0] is super3 + #:: ExpectedOutput(assert.failed:assertion.false) + assert mylist2[1] is super3 \ No newline at end of file From 31927b3e731878d8f80a643aeeca1577bc3c83c7 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 22 Apr 2026 17:59:05 +0200 Subject: [PATCH 12/17] list remove and index --- .../resources/builtins.json | 9 +++++++ src/nagini_translation/resources/list.sil | 22 +++++++++++++++ tests/functional/verification/test_lists.py | 27 ++++++++++++++++++- 3 files changed, 57 insertions(+), 1 deletion(-) diff --git a/src/nagini_translation/resources/builtins.json b/src/nagini_translation/resources/builtins.json index 7736a0982..4c6271fda 100644 --- a/src/nagini_translation/resources/builtins.json +++ b/src/nagini_translation/resources/builtins.json @@ -62,6 +62,11 @@ "type": "list", "MustTerminate": true }, + "remove": { + "args": ["list", "object"], + "type": null, + "MustTerminate": true + }, "__setitem__": { "args": ["list", "__prim__int", "object"], "type": null, @@ -109,6 +114,10 @@ "__sil_seq__": { "args": ["list"], "type": "__prim__Seq" + }, + "index": { + "args": ["list", "object"], + "type": "__prim__int" } }, "type_vars": 1, diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil index 2c799fe1a..aea6b09b2 100644 --- a/src/nagini_translation/resources/list.sil +++ b/src/nagini_translation/resources/list.sil @@ -145,6 +145,28 @@ method list_copy(self: Ref) returns (res: Ref) ensures acc(res.list_acc) ensures res.list_acc == self.list_acc +method list_remove(self: Ref, item: Ref) returns () + requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) + requires acc(self.list_acc) + requires issubtype(typeof(item), list_arg(typeof(self), 0)) + requires @error("Item may not be in list.")(item in self.list_acc) + ensures acc(self.list_acc) + ensures |self.list_acc| == |old(self.list_acc)| - 1 + ensures exists i: Int :: 0 <= i && i < |old(self.list_acc)| + && old(self.list_acc)[i] == item + && (forall j: Int :: 0 <= j && j < i ==> old(self.list_acc)[j] != item) + && self.list_acc == old(self.list_acc)[..i] ++ old(self.list_acc)[i+1..] + +function list_index(self: Ref, item: Ref): Int + decreases _ + requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) + requires acc(self.list_acc, wildcard) + requires @error("Item may not be in list.")(item in self.list_acc) + ensures result >= 0 + ensures result < |self.list_acc| + ensures self.list_acc[result] == item + ensures forall j: Int :: {self.list_acc[j]} 0 <= j && j < result ==> self.list_acc[j] != item + method list___iter__(self: Ref) returns (_res: Ref) requires issubtype(typeof(self), list(list_arg(typeof(self), 0))) requires acc(self.list_acc, 1 / 10) diff --git a/tests/functional/verification/test_lists.py b/tests/functional/verification/test_lists.py index 7193d4893..bed6d715d 100644 --- a/tests/functional/verification/test_lists.py +++ b/tests/functional/verification/test_lists.py @@ -210,4 +210,29 @@ def test_copy() -> None: assert mylist[0] is super1 assert mylist2[0] is super3 #:: ExpectedOutput(assert.failed:assertion.false) - assert mylist2[1] is super3 \ No newline at end of file + assert mylist2[1] is super3 + + +def test_remove() -> None: + super1 = Super() + super2 = Super() + super3 = Super() + mylist = [super1, super2, super3] + mylist.remove(super2) + assert len(mylist) == 2 + assert mylist[0] is super1 + assert mylist[1] is super3 + #:: ExpectedOutput(assert.failed:assertion.false) + assert mylist[0] is super2 + + +def test_index() -> None: + super1 = Super() + super2 = Super() + super3 = Super() + mylist = [super1, super2, super3, super1] + assert mylist.index(super1) == 0 + assert mylist.index(super2) == 1 + assert mylist.index(super3) == 2 + #:: ExpectedOutput(assert.failed:assertion.false) + assert mylist.index(super1) == 3 \ No newline at end of file From 7a2a2c0e56e5e5e030ef9550ca252414ce0d1f05 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 23 Apr 2026 11:57:08 +0200 Subject: [PATCH 13/17] Better strict int for lists --- .../translators/contract.py | 42 ++++++++++++++++++- .../translators/statement.py | 21 ++++++++++ .../verification/test_strict_int.py | 28 +++++++++++++ 3 files changed, 90 insertions(+), 1 deletion(-) diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py index 5ecf51bf0..932a8340b 100644 --- a/src/nagini_translation/translators/contract.py +++ b/src/nagini_translation/translators/contract.py @@ -140,7 +140,13 @@ def translate_builtin_predicate(self, node: ast.Call, perm: Expr, pos = self.to_position(node, ctx) if name == 'list_pred': # field list_acc : Seq[Ref] - return self._get_field_perm('list_acc', seq_ref, perm, args[0], pos, ctx) + field_perm = self._get_field_perm('list_acc', seq_ref, perm, + args[0], pos, ctx) + strict_inv = self._strict_int_list_invariant(node.args[0], args[0], + pos, ctx) + if strict_inv is None: + return field_perm + return self.viper.And(field_perm, strict_inv, pos, self.no_info(ctx)) elif name == 'set_pred': # field set_acc : Set[Ref] return self._get_field_perm('set_acc', set_ref, perm, args[0], pos, ctx) @@ -163,6 +169,40 @@ def _get_field_perm(self, field_name: str, field_type: 'silver.ast.Type', perm: pred = self.viper.FieldAccessPredicate(field_acc, perm, pos, info) return pred + def _strict_int_list_invariant(self, list_py_node: ast.AST, list_ref: Expr, + pos: Position, ctx: Context) -> Expr: + # In strict-int mode, List[int] elements must be exactly int (not bool + # or any other int subtype). Returns a quantified invariant: + # forall i :: 0 <= i < |l.list_acc| ==> typeof(l.list_acc[i]) == int() + # or None when the invariant doesn't apply. + if not ctx.strict_int: + return None + list_type = self.get_type(list_py_node, ctx) + if list_type is None or not getattr(list_type, 'type_args', None): + return None + if list_type.type_args[0].name != INT_TYPE: + return None + info = self.no_info(ctx) + seq_ref = self.viper.SeqType(self.viper.Ref) + field = self.viper.Field('list_acc', seq_ref, pos, info) + field_acc = self.viper.FieldAccess(list_ref, field, pos, info) + i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info) + i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info) + seq_at_i = self.viper.SeqIndex(field_acc, i_ref, pos, info) + zero = self.viper.IntLit(0, pos, info) + length = self.viper.SeqLength(field_acc, pos, info) + bounds = self.viper.And( + self.viper.LeCmp(zero, i_ref, pos, info), + self.viper.LtCmp(i_ref, length, pos, info), + pos, info) + int_cls = ctx.module.global_module.classes[INT_TYPE] + int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx) + typeof_at_i = self.type_factory.typeof(seq_at_i, ctx) + eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info) + body = self.viper.Implies(bounds, eq, pos, info) + trigger = self.viper.Trigger([seq_at_i], pos, info) + return self.viper.Forall([i_decl], [trigger], body, pos, info) + def translate_may_start(self, node: ast.Call, args: List[Expr], perm: Expr, ctx: Context) -> Expr: pos = self.to_position(node, ctx) diff --git a/src/nagini_translation/translators/statement.py b/src/nagini_translation/translators/statement.py index 24954f9f6..3a3091985 100644 --- a/src/nagini_translation/translators/statement.py +++ b/src/nagini_translation/translators/statement.py @@ -597,6 +597,27 @@ def _create_for_loop_invariant(self, iter_var: PythonVar, seq_temp_var: PythonVa invariant.append(self.viper.Implies(some_error, previous_is_all, pos, info)) invariant.append(self.viper.Implies(empty_iterator, some_error, pos, info)) + + if ctx.strict_int and target_var.type.name == INT_TYPE: + # Carry the strict element-type fact across the loop body. Without + # this, __next__'s `issubtype(typeof(_res), int())` postcondition + # cannot establish the strict `typeof(target) == int()` that the + # target_type invariant above requires in strict-int mode. + i_decl = self.viper.LocalVarDecl('__si_i', self.viper.Int, pos, info) + i_ref = self.viper.LocalVar('__si_i', self.viper.Int, pos, info) + seq_at_i = self.viper.SeqIndex(iter_acc, i_ref, pos, info) + bounds = self.viper.And( + self.viper.LeCmp(zero, i_ref, pos, info), + self.viper.LtCmp(i_ref, iter_list_len, pos, info), + pos, info) + int_cls = ctx.module.global_module.classes[INT_TYPE] + int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx) + typeof_eq = self.viper.EqCmp(self.type_factory.typeof(seq_at_i, ctx), + int_lit, pos, info) + forall_body = self.viper.Implies(bounds, typeof_eq, pos, info) + trigger = self.viper.Trigger([seq_at_i], pos, info) + invariant.append(self.viper.Forall([i_decl], [trigger], forall_body, + pos, info)) return invariant def _get_iterator(self, iterable: Expr, iterable_type: PythonType, diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py index 3d172deab..cb82cb3df 100644 --- a/tests/strict-int/verification/test_strict_int.py +++ b/tests/strict-int/verification/test_strict_int.py @@ -5,6 +5,7 @@ file, You can obtain one at http://mozilla.org/MPL/2.0/. """ from nagini_contracts.contracts import * +from typing import List def takes_int(x: int) -> None: @@ -27,3 +28,30 @@ def returns_bool_as_int() -> int: def test_forall_int_verifies() -> None: Assert(Forall(int, lambda k: (k is not True and k is not False, []))) + + +def sum_int_list(lst: List[int]) -> int: + Requires(Acc(list_pred(lst), 1 / 2)) + Ensures(Acc(list_pred(lst), 1 / 2)) + total = 0 + for x in lst: + Invariant(Acc(list_pred(lst), 1 / 4)) + takes_int(x) + total = total + x + return total + + +def test_append_int_accepted() -> None: + lst = [1, 2, 3] + lst.append(4) + assert lst[3] == 4 + + +def append_bool_breaks_list_pred(lst: List[int]) -> None: + # Appending a bool to a List[int] verifies (list_append only requires + # issubtype), but the bool then poisons the element-type invariant, so + # list_pred cannot be re-established at the postcondition. + Requires(Acc(list_pred(lst))) + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(Acc(list_pred(lst))) + lst.append(True) From 769865308844665355581a11cd58aad3ab5f3ca0 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 27 Apr 2026 12:32:24 +0200 Subject: [PATCH 14/17] strict int for pseqs --- src/nagini_translation/translators/type.py | 43 +++++++++++++++++++ .../verification/test_strict_int.py | 25 +++++++++++ 2 files changed, 68 insertions(+) diff --git a/src/nagini_translation/translators/type.py b/src/nagini_translation/translators/type.py index 431c2712c..d9e531deb 100644 --- a/src/nagini_translation/translators/type.py +++ b/src/nagini_translation/translators/type.py @@ -9,7 +9,9 @@ from nagini_translation.lib.constants import ( CALLABLE_TYPE, + INT_TYPE, PRIMITIVES, + PSEQ_TYPE, ) from nagini_translation.lib.program_nodes import ( PythonClass, @@ -99,4 +101,45 @@ def type_check(self, lhs: Expr, type: PythonType, return self.viper.TrueLit(position, self.no_info(ctx)) else: result = self.type_factory.type_check(lhs, type, position, ctx) + strict_inv = self._strict_int_pseq_invariant(lhs, type, position, ctx) + if strict_inv is not None: + result = self.viper.And(result, strict_inv, position, + self.no_info(ctx)) return result + + def _strict_int_pseq_invariant(self, pseq_ref: Expr, pseq_type: PythonType, + pos: 'silver.ast.Position', + ctx: Context) -> Optional[Expr]: + # Mirror of _strict_int_list_invariant for PSeq[int]: in strict-int + # mode, every element of a PSeq[int] must have exactly type int. Since + # PSeq is a value type with no permission to attach the invariant to, + # we conjoin it with the type check that establishes + # `typeof(s) == PSeq(int())`. Returns None when not applicable. + if not ctx.strict_int: + return None + if pseq_type is None or pseq_type.name != PSEQ_TYPE: + return None + if not getattr(pseq_type, 'type_args', None): + return None + if pseq_type.type_args[0].name != INT_TYPE: + return None + info = self.no_info(ctx) + seq_class = ctx.module.global_module.classes[PSEQ_TYPE] + sil_seq = self.get_function_call(seq_class, '__sil_seq__', + [pseq_ref], [None], None, ctx, pos) + i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info) + i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info) + seq_at_i = self.viper.SeqIndex(sil_seq, i_ref, pos, info) + zero = self.viper.IntLit(0, pos, info) + length = self.viper.SeqLength(sil_seq, pos, info) + bounds = self.viper.And( + self.viper.LeCmp(zero, i_ref, pos, info), + self.viper.LtCmp(i_ref, length, pos, info), + pos, info) + int_cls = ctx.module.global_module.classes[INT_TYPE] + int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx) + typeof_at_i = self.type_factory.typeof(seq_at_i, ctx) + eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info) + body = self.viper.Implies(bounds, eq, pos, info) + trigger = self.viper.Trigger([seq_at_i], pos, info) + return self.viper.Forall([i_decl], [trigger], body, pos, info) diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py index cb82cb3df..396fea0eb 100644 --- a/tests/strict-int/verification/test_strict_int.py +++ b/tests/strict-int/verification/test_strict_int.py @@ -55,3 +55,28 @@ def append_bool_breaks_list_pred(lst: List[int]) -> None: #:: ExpectedOutput(postcondition.violated:assertion.false) Ensures(Acc(list_pred(lst))) lst.append(True) + + +def reads_pseq_int_param(s: PSeq[int]) -> None: + Requires(len(s) > 0) + takes_int(s[0]) + + +def reads_pseq_via_toseq(lst: List[int]) -> None: + Requires(Acc(list_pred(lst))) + Requires(len(lst) > 0) + Ensures(Acc(list_pred(lst))) + s = ToSeq(lst) + takes_int(s[0]) + + +def reads_pseq_int_literal() -> None: + s = PSeq(1, 2, 3) + takes_int(s[0]) + + +def reads_pseq_bool_param_rejected(s: PSeq[bool]) -> None: + # PSeq[bool] elements must NOT be promoted to strict int. + Requires(len(s) > 0) + #:: ExpectedOutput(call.precondition:assertion.false) + takes_int(s[0]) From 1ffc399888fd0b990280e82f48a3d671fc030a82 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 7 Jul 2026 16:34:25 +0200 Subject: [PATCH 15/17] strict-int: Acc ratio annotation, tuple invariants, tuple tests Co-Authored-By: Claude Fable 5 --- src/nagini_contracts/contracts.py | 2 +- src/nagini_translation/translators/type.py | 73 +++++++++++++++++++ .../verification/test_strict_int.py | 54 +++++++++++++- 3 files changed, 127 insertions(+), 2 deletions(-) diff --git a/src/nagini_contracts/contracts.py b/src/nagini_contracts/contracts.py index 6ff201183..b37f29f54 100644 --- a/src/nagini_contracts/contracts.py +++ b/src/nagini_contracts/contracts.py @@ -367,7 +367,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. diff --git a/src/nagini_translation/translators/type.py b/src/nagini_translation/translators/type.py index d9e531deb..8c0f69efa 100644 --- a/src/nagini_translation/translators/type.py +++ b/src/nagini_translation/translators/type.py @@ -12,6 +12,7 @@ INT_TYPE, PRIMITIVES, PSEQ_TYPE, + TUPLE_TYPE, ) from nagini_translation.lib.program_nodes import ( PythonClass, @@ -105,6 +106,10 @@ def type_check(self, lhs: Expr, type: PythonType, if strict_inv is not None: result = self.viper.And(result, strict_inv, position, self.no_info(ctx)) + tuple_inv = self._strict_int_tuple_invariant(lhs, type, position, ctx) + if tuple_inv is not None: + result = self.viper.And(result, tuple_inv, position, + self.no_info(ctx)) return result def _strict_int_pseq_invariant(self, pseq_ref: Expr, pseq_type: PythonType, @@ -143,3 +148,71 @@ def _strict_int_pseq_invariant(self, pseq_ref: Expr, pseq_type: PythonType, body = self.viper.Implies(bounds, eq, pos, info) trigger = self.viper.Trigger([seq_at_i], pos, info) return self.viper.Forall([i_decl], [trigger], body, pos, info) + + def _strict_int_tuple_invariant(self, tuple_ref: Expr, + tuple_type: PythonType, + pos: 'silver.ast.Position', + ctx: Context) -> Optional[Expr]: + # In strict-int mode, tuple element access only guarantees a subtype + # of the slot type because `tuple___getitem__` ensures + # `issubtype(typeof(result), tuple_arg(typeof(self), key))`. For int + # slots we need exact equality. Anchor on `tuple___sil_seq__(t)` (which + # carries `|result| == tuple___len__(self)` for in-bounds SeqIndex) and + # also offer `tuple___val__(t)[i]` as an alternate trigger so the + # quantifier fires on the term `tuple___getitem__`'s ensures puts in + # scope at the call site. + if not ctx.strict_int: + return None + if tuple_type is None or tuple_type.name != TUPLE_TYPE: + return None + type_args = getattr(tuple_type, 'type_args', None) + if not type_args: + return None + info = self.no_info(ctx) + tuple_class = ctx.module.global_module.classes[TUPLE_TYPE] + sil_seq = self.get_function_call(tuple_class, '__sil_seq__', + [tuple_ref], [None], None, ctx, pos) + seq_ref_type = self.viper.SeqType(self.viper.Ref) + tuple_val = self.viper.FuncApp('tuple___val__', [tuple_ref], pos, info, + seq_ref_type) + int_cls = ctx.module.global_module.classes[INT_TYPE] + int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx) + if getattr(tuple_type, 'exact_length', True): + # Heterogeneous tuple: emit a conjunct per int slot. Indexing into + # `tuple___sil_seq__` carries the length axiom so in-bounds checks + # succeed for known slot indices. + conjuncts = [] + for i, arg_type in enumerate(type_args): + if arg_type is None or arg_type.name != INT_TYPE: + continue + idx = self.viper.IntLit(i, pos, info) + at_i = self.viper.SeqIndex(sil_seq, idx, pos, info) + typeof_at_i = self.type_factory.typeof(at_i, ctx) + conjuncts.append(self.viper.EqCmp(typeof_at_i, int_lit, pos, + info)) + if not conjuncts: + return None + result = conjuncts[0] + for c in conjuncts[1:]: + result = self.viper.And(result, c, pos, info) + return result + # Variadic Tuple[T, ...]: single element type. + if type_args[0] is None or type_args[0].name != INT_TYPE: + return None + i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info) + i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info) + sil_at_i = self.viper.SeqIndex(sil_seq, i_ref, pos, info) + val_at_i = self.viper.SeqIndex(tuple_val, i_ref, pos, info) + zero = self.viper.IntLit(0, pos, info) + length = self.viper.SeqLength(sil_seq, pos, info) + bounds = self.viper.And( + self.viper.LeCmp(zero, i_ref, pos, info), + self.viper.LtCmp(i_ref, length, pos, info), + pos, info) + typeof_at_i = self.type_factory.typeof(sil_at_i, ctx) + eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info) + body = self.viper.Implies(bounds, eq, pos, info) + trig_sil = self.viper.Trigger([sil_at_i], pos, info) + trig_val = self.viper.Trigger([val_at_i], pos, info) + return self.viper.Forall([i_decl], [trig_sil, trig_val], body, pos, + info) diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py index 396fea0eb..043e977b0 100644 --- a/tests/strict-int/verification/test_strict_int.py +++ b/tests/strict-int/verification/test_strict_int.py @@ -5,7 +5,7 @@ file, You can obtain one at http://mozilla.org/MPL/2.0/. """ from nagini_contracts.contracts import * -from typing import List +from typing import List, Tuple def takes_int(x: int) -> None: @@ -80,3 +80,55 @@ def reads_pseq_bool_param_rejected(s: PSeq[bool]) -> None: Requires(len(s) > 0) #:: ExpectedOutput(call.precondition:assertion.false) takes_int(s[0]) + + +def reads_tuple_int_param(t: Tuple[int, int]) -> None: + takes_int(t[0]) + takes_int(t[1]) + + +def reads_single_int_tuple(t: Tuple[int]) -> None: + takes_int(t[0]) + + +def reads_homogeneous_tuple(t: Tuple[int, ...]) -> None: + Requires(len(t) > 0) + takes_int(t[0]) + + +def reads_mixed_tuple(t: Tuple[int, str]) -> None: + # Only the int slot can be passed to takes_int. + takes_int(t[0]) + + +def tuple_literal_strict() -> None: + t = (1, 2, 3) + takes_int(t[0]) + takes_int(t[2]) + + +def unpacks_tuple_int(t: Tuple[int, int]) -> None: + a, b = t + takes_int(a) + takes_int(b) + + +def _make_int_pair() -> Tuple[int, int]: + return (1, 2) + + +def returns_tuple_int_used() -> None: + t = _make_int_pair() + takes_int(t[0]) + + +def reads_bool_tuple_rejected(t: Tuple[bool, bool]) -> None: + # Tuple[bool, bool] elements must NOT be promoted to strict int. + #:: ExpectedOutput(call.precondition:assertion.false) + takes_int(t[0]) + + +def reads_bool_variadic_tuple_rejected(t: Tuple[bool, ...]) -> None: + Requires(len(t) > 0) + #:: ExpectedOutput(call.precondition:assertion.false) + takes_int(t[0]) From b5d1629a68c71b52f416f1fac5a3baa303ab9427 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 7 Jul 2026 16:39:04 +0200 Subject: [PATCH 16/17] service/MCP: expose --strict-int and --force-obligations Threads strict_int through both service translate call sites, the configure tool (strictInt), and the shared service CLI arguments so nagini_mcp/nagini_lsp can run in strict-int mode. force_obligations pins the obligation encoding via the existing snapshot mechanism. Also threads strict_int through the CLI benchmark path. Co-Authored-By: Claude Fable 5 --- src/nagini_translation/mcp_server.py | 2 +- src/nagini_translation/service.py | 27 ++++++++++++++++++---- tests/servers/test_verification_options.py | 23 ++++++++++++++++++ 3 files changed, 47 insertions(+), 5 deletions(-) diff --git a/src/nagini_translation/mcp_server.py b/src/nagini_translation/mcp_server.py index f5b146399..887f3fed5 100644 --- a/src/nagini_translation/mcp_server.py +++ b/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. diff --git a/src/nagini_translation/service.py b/src/nagini_translation/service.py index cbafa6e08..ffd469bee 100644 --- a/src/nagini_translation/service.py +++ b/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: diff --git a/tests/servers/test_verification_options.py b/tests/servers/test_verification_options.py index e6b2a39ae..475334e4a 100644 --- a/tests/servers/test_verification_options.py +++ b/tests/servers/test_verification_options.py @@ -150,3 +150,26 @@ def test_include_viper_returns_translated_program(service, tmp_path): default = service.verify(_write(tmp_path, "iv2.py", _NO_OBLIGATIONS_SRC)) assert default.viper_program is None assert "viperProgram" not in default.to_dict() + + +# -- strictInt -------------------------------------------------------------- + +_BOOL_AS_INT_SRC = ( + "from nagini_contracts.contracts import *\n\n" + "def f() -> int:\n" + " return True\n" +) + + +def test_strict_int_toggles_bool_int_conformance(service, tmp_path): + path = _write(tmp_path, "strict_int.py", _BOOL_AS_INT_SRC) + # Off by default: bool is a subtype of int. + assert service.verify(path).success + service.reconfigure(strict_int=True) + try: + strict = service.verify(path) + assert not strict.success + assert any("postcondition" in d.code for d in strict.diagnostics) + finally: + service.reconfigure(strict_int=False) + assert service.verify(path).success From df5b4aca7b57a4ebba075036fb22ff58807b7a17 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 7 Jul 2026 17:18:22 +0200 Subject: [PATCH 17/17] strict-int: move return-type annotation to new error position The implicit 'return type is correct' postcondition error is now reported on the function definition rather than the return statement. Co-Authored-By: Claude Fable 5 --- tests/strict-int/verification/test_strict_int.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py index 043e977b0..87e76c484 100644 --- a/tests/strict-int/verification/test_strict_int.py +++ b/tests/strict-int/verification/test_strict_int.py @@ -21,8 +21,8 @@ def test_bool_arg_rejected() -> None: takes_int(True) +#:: ExpectedOutput(postcondition.violated:assertion.false) def returns_bool_as_int() -> int: - #:: ExpectedOutput(postcondition.violated:assertion.false) return True