diff --git a/setup.py b/setup.py index b9067bc9d..40d6f29a2 100644 --- a/setup.py +++ b/setup.py @@ -10,7 +10,7 @@ setup( name='nagini', - version='0.8.6', + version='0.9.0', author='Viper Team', author_email='viper@inf.ethz.ch', license='MPL-2.0', @@ -30,7 +30,8 @@ 'astunparse==1.6.2', 'typed-ast==1.4.0', 'pytest==4.3.0', - 'z3-solver' + 'pytest-xdist==1.27.0', + 'z3-solver==4.8.7.0' ], entry_points = { 'console_scripts': [ diff --git a/src/nagini_translation/conftest.py b/src/nagini_translation/conftest.py index 3d8c9d350..57942efc3 100644 --- a/src/nagini_translation/conftest.py +++ b/src/nagini_translation/conftest.py @@ -25,7 +25,9 @@ _VERIFICATION_TESTS_SUFFIX = 'verification' _FUNCTIONAL_TESTS_DIR = 'tests/functional/' -_SIF_TESTS_DIR = 'tests/sif/' +_SIF_TRUE_TESTS_DIR = 'tests/sif-true/' +_SIF_POSS_TESTS_DIR = 'tests/sif-poss/' +_SIF_PROB_TESTS_DIR = 'tests/sif-prob/' _IO_TESTS_DIR = 'tests/io/' _OBLIGATIONS_TESTS_DIR = 'tests/obligations/' _ARP_TESTS_DIR = 'tests/arp/' @@ -39,6 +41,7 @@ def __init__(self): self.single_test = None self.verifiers = [] self.store_viper = False + self.force_product = False self.init_from_config_file() @@ -52,10 +55,17 @@ def init_from_config_file(self): self.add_verifier(verifier) def add_test(self, test: str): + if test == 'functional-product': + self._add_test_dir(_FUNCTIONAL_TESTS_DIR) + self.force_product = True if test == 'functional': self._add_test_dir(_FUNCTIONAL_TESTS_DIR) - elif test == 'sif': - self._add_test_dir(_SIF_TESTS_DIR) + elif test == 'sif-true': + self._add_test_dir(_SIF_TRUE_TESTS_DIR) + elif test == 'sif-poss': + self._add_test_dir(_SIF_POSS_TESTS_DIR) + elif test == 'sif-prob': + self._add_test_dir(_SIF_PROB_TESTS_DIR) elif test == 'io': self._add_test_dir(_IO_TESTS_DIR) elif test == 'obligations': @@ -121,7 +131,10 @@ def pytest_addoption(parser: 'pytest.config.Parser'): parser.addoption('--single-test', dest='single_test', action='store', default=None) parser.addoption('--all-tests', dest='all_tests', action='store_true') parser.addoption('--functional', dest='functional', action='store_true') - parser.addoption('--sif', dest='sif', action='store_true') + parser.addoption('--functional-product', dest='functional_product', action='store_true') + parser.addoption('--sif-true', dest='sif_true', action='store_true') + parser.addoption('--sif-poss', dest='sif_poss', action='store_true') + parser.addoption('--sif-prob', dest='sif_prob', action='store_true') parser.addoption('--io', dest='io', action='store_true') parser.addoption('--obligations', dest='obligations', action='store_true') parser.addoption('--arp', dest='arp', action='store_true') @@ -137,24 +150,30 @@ def pytest_configure(config: 'pytest.config.Config'): # Setup tests. tests = [] if config.option.all_tests: - tests = ['functional', 'sif', 'io', 'obligations', 'arp'] + tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp'] else: if config.option.functional: tests.append('functional') - if config.option.sif: - tests.append('sif') + if config.option.sif_true: + tests.append('sif-true') + if config.option.sif_poss: + tests.append('sif-poss') + if config.option.sif_prob: + tests.append('sif-prob') if config.option.io: tests.append('io') if config.option.obligations: tests.append('obligations') if config.option.arp: tests.append('arp') + if config.option.functional_product: + tests = ['functional-product'] if tests: # Overwrite config file options. _pytest_config.clear_tests() for test in tests: _pytest_config.add_test(test) - if 'sif' in tests: + if 'sif-true' in tests or 'sif-poss' in tests or 'sif-prob' in tests: if not jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt): pytest.exit('Viper SIF extension not avaliable on the classpath.') elif config.option.single_test: @@ -165,7 +184,7 @@ def pytest_configure(config: 'pytest.config.Config'): # present. tests = ['functional', 'io', 'obligations'] if jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt): - tests.append('sif') + tests.extend(['sif-true', 'sif-poss', 'sif-prob']) if jvm.is_known_class(jvm.viper.silver.plugin.ARPPlugin): tests.append('arp') for test in tests: @@ -208,11 +227,19 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'): for test_dir in _pytest_config.translation_test_dirs: files = _test_files(test_dir) test_files.extend(files) - reload_triggers.add(files[0]) + if files: + reload_triggers.add(files[0]) if _pytest_config.single_test and 'translation' in _pytest_config.single_test: test_files.append(_pytest_config.single_test) for file in test_files: - sif = 'sif' in file + if 'sif-true' in file: + sif = True + elif 'sif-poss' in file: + sif = 'poss' + elif 'sif-prob' in file: + sif = 'prob' + else: + sif = False reload_resources = file in reload_triggers arp = 'arp' in file base = file.partition('translation')[0] + 'translation' @@ -226,12 +253,23 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'): if _pytest_config.single_test and 'verification' in _pytest_config.single_test: test_files.append(_pytest_config.single_test) for file in test_files: - sif = 'sif' in file + ignore_obligations = 'no_obligations' in file + if 'sif-true' in file: + sif = True + elif 'sif-poss' in file: + sif = 'poss' + elif 'sif-prob' in file: + sif = 'prob' + else: + sif = False + if _pytest_config.force_product: + sif = True reload_resources = file in reload_triggers arp = 'arp' in file base = file.partition('verification')[0] + 'verification' - params.extend([(file, base, verifier, sif, reload_resources, arp, _pytest_config.store_viper) for verifier + params.extend([(file, base, verifier, sif, reload_resources, arp, ignore_obligations, _pytest_config.store_viper) for verifier in _pytest_config.verifiers]) - metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,print', params) + metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print', params) else: pytest.exit('Unrecognized test function.') + diff --git a/src/nagini_translation/lib/config.py b/src/nagini_translation/lib/config.py index 867216a84..e6d3efa23 100644 --- a/src/nagini_translation/lib/config.py +++ b/src/nagini_translation/lib/config.py @@ -51,7 +51,7 @@ def disable_all(self): @disable_all.setter def disable_all(self, val): """Disable all obligation related checks.""" - self._info['disable_all'] = 'True' + self._info['disable_all'] = str(val) @property def disable_measure_check(self): @@ -175,19 +175,16 @@ def _construct_classpath(verifier : str = None): (arpplugin_jar, 'arpplugin')) if jar and v != verifier) - if sys.platform.startswith('linux'): - if os.path.isdir('/usr/lib/viper'): - # Check if we have Viper installed via package manager. - return os.pathsep.join( - glob.glob('/usr/lib/viper/*.jar')) - resources = resources_folder() silicon = os.path.join(resources, 'backends', 'silicon.jar') carbon = os.path.join(resources, 'backends', 'carbon.jar') + silver_sif = os.path.join(resources, 'backends', 'silver-sif-extension.jar') + silicon_sif = os.path.join(resources, 'backends', 'silicon-sif-extension.jar') return os.pathsep.join( jar for jar, v in ((silicon, 'carbon'), (carbon, 'silicon'), - (arpplugin_jar, 'arpplugin')) + (silver_sif, 'silver-sif'), + (silicon_sif, 'silicon-sif')) if jar and v != verifier) @@ -203,11 +200,6 @@ def _get_boogie_path(): if boogie_exe: return boogie_exe - if sys.platform.startswith('linux'): - if (os.path.exists('/usr/bin/boogie') and - os.path.exists('/usr/bin/mono')): - return '/usr/bin/boogie' - def _get_z3_path(): """ Tries to detect path to Z3 executable. @@ -220,12 +212,9 @@ def _get_z3_path(): if z3_exe: return z3_exe - if sys.platform.startswith('linux'): - if os.path.exists('/usr/bin/viper-z3'): - # First check if we have Z3 installed together with Viper. - return '/usr/bin/viper-z3' - if os.path.exists('/usr/bin/z3'): - return '/usr/bin/z3' + script_path = os.path.join(os.path.abspath(os.path.dirname(sys.argv[0])), 'z3') + if os.path.exists(script_path): + return script_path path = os.path.join(os.path.dirname(sys.executable), 'z3.exe' if sys.platform.startswith('win') else 'z3') diff --git a/src/nagini_translation/lib/context.py b/src/nagini_translation/lib/context.py index 63ea2bbc8..1a3b5f68d 100644 --- a/src/nagini_translation/lib/context.py +++ b/src/nagini_translation/lib/context.py @@ -62,6 +62,7 @@ def __init__(self) -> None: self.are_function_constants_used = False self.are_threading_constants_used = False self.sif = False + self.allow_statements = False def get_fresh_int(self) -> int: """ diff --git a/src/nagini_translation/lib/errors/messages.py b/src/nagini_translation/lib/errors/messages.py index d33836b02..ac8f1979e 100644 --- a/src/nagini_translation/lib/errors/messages.py +++ b/src/nagini_translation/lib/errors/messages.py @@ -77,6 +77,10 @@ lambda n: 'Termination channel might exist.', 'lock.invariant.not.established': lambda n: 'Lock invariant might not hold.', + 'probabilistic.sif.violated': + lambda n: 'Probabilistic non-interference might not be satisfied.', + 'possibilistic.sif.violated': + lambda n: 'Possibilistic non-interference might not be satisfied.' } REASONS = { @@ -149,7 +153,7 @@ lambda n: 'May not have permission to start thread.', 'sif.fold': lambda n: 'The low parts of predicate {} might not hold.'.format( - get_target_name(n.args[0])), + get_target_name(n.args[0]) if n.args else 'lock invariant'), 'sif.unfold': lambda n: 'The low parts of predicate {} might not hold.'.format( get_target_name(n.args[0])), @@ -166,7 +170,15 @@ lambda n: 'Function and loop termination must be proved to be low in possibilistic noninterference mode. ' 'Use TerminatesSif(...) as the last precondition/loop invariant.', 'high.branch': - lambda n: 'Branch condition {} might not be low.', + lambda n: 'Branch condition {} might not be low or reaching the loop might not be a low event.'.format(pprint(n)), + 'high.receiver.type': + lambda n: 'Type of call receiver {} might not be low.'.format(pprint(n)), + 'high.exception.type': + lambda n: 'Type of raised exception {} might not be low.'.format(pprint(n)), + 'high.short.circuit': + lambda n: 'Short-circuiting behavior of expression {} might not be low.'.format(pprint(n)), + 'high.comprehension': + lambda n: 'Comprehension {} might introduce high control flow'.format(pprint(n)), } VAGUE_REASONS = { diff --git a/src/nagini_translation/lib/errors/rules.py b/src/nagini_translation/lib/errors/rules.py index c6a371eb6..83b61730e 100644 --- a/src/nagini_translation/lib/errors/rules.py +++ b/src/nagini_translation/lib/errors/rules.py @@ -118,6 +118,30 @@ class Rules(Dict[Tuple[str, str], Tuple[str, str]]): ('fold.failed', 'assertion.false'): ('lock.invariant.not.established', 'assertion.false') } +BRANCH_CONDITION_ASSERT = { + ('assert.failed', 'assertion.false'): + ('probabilistic.sif.violated', 'high.branch') +} +POSS_BRANCH_CONDITION_ASSERT = { + ('assert.failed', 'assertion.false'): + ('possibilistic.sif.violated', 'high.branch') +} +BRANCH_RECEIVER_LOW = { + ('assert.failed', 'assertion.false'): + ('probabilistic.sif.violated', 'high.receiver.type') +} +EXCEPTION_TYPE_LOW = { + ('assert.failed', 'assertion.false'): + ('probabilistic.sif.violated', 'high.exception.type') +} +SHORT_CIRCUIT_LOW = { + ('assert.failed', 'assertion.false'): + ('probabilistic.sif.violated', 'high.short.circuit') +} +COMPREHENSION_LOW = { + ('assert.failed', 'assertion.false'): + ('probabilistic.sif.violated', 'high.comprehension') +} __all__ = ( 'Rules', @@ -135,4 +159,9 @@ class Rules(Dict[Tuple[str, str], Tuple[str, str]]): 'LOCAL_VARIABLE_NOT_DEFINED', 'GLOBAL_NAME_NOT_DEFINED', 'DEPENDENCIES_NOT_DEFINED', + 'BRANCH_CONDITION_ASSERT', + 'BRANCH_RECEIVER_LOW', + 'EXCEPTION_TYPE_LOW', + 'SHORT_CIRCUIT_LOW', + 'COMPREHENSION_LOW', ) diff --git a/src/nagini_translation/lib/resolver.py b/src/nagini_translation/lib/resolver.py index 5c236449e..cbe0cc8eb 100644 --- a/src/nagini_translation/lib/resolver.py +++ b/src/nagini_translation/lib/resolver.py @@ -469,7 +469,7 @@ def _get_call_type(node: ast.Call, module: PythonModule, def get_subscript_type(node: ast.Subscript, module: PythonModule, containers: List[ContainerInterface], container: PythonNode) -> PythonType: - if (node._parent and isinstance(node._parent, ast.Assign) and + if (hasattr(node, '_parent') and node._parent and isinstance(node._parent, ast.Assign) and node is node._parent.value): # Constructor is assigned to variable; # we get the type of the dict from the type of the diff --git a/src/nagini_translation/lib/typedefs.py b/src/nagini_translation/lib/typedefs.py index 5435491b0..155cce08d 100644 --- a/src/nagini_translation/lib/typedefs.py +++ b/src/nagini_translation/lib/typedefs.py @@ -20,6 +20,8 @@ VarAssign = 'silver.ast.LocalVarAssign' +While = 'silver.ast.While' + Domain = 'silver.ast.Domain' DomainAxiom = 'silver.ast.DomainAxiom' diff --git a/src/nagini_translation/resources/backends/carbon.jar b/src/nagini_translation/resources/backends/carbon.jar new file mode 100644 index 000000000..0645393c5 Binary files /dev/null and b/src/nagini_translation/resources/backends/carbon.jar differ diff --git a/src/nagini_translation/resources/backends/silicon-sif-extension.jar b/src/nagini_translation/resources/backends/silicon-sif-extension.jar new file mode 100644 index 000000000..3d77a3156 Binary files /dev/null and b/src/nagini_translation/resources/backends/silicon-sif-extension.jar differ diff --git a/src/nagini_translation/resources/backends/silicon.jar b/src/nagini_translation/resources/backends/silicon.jar new file mode 100644 index 000000000..7136640cd Binary files /dev/null and b/src/nagini_translation/resources/backends/silicon.jar differ diff --git a/src/nagini_translation/resources/backends/silver-sif-extension.jar b/src/nagini_translation/resources/backends/silver-sif-extension.jar new file mode 100644 index 000000000..e0dbf52ff Binary files /dev/null and b/src/nagini_translation/resources/backends/silver-sif-extension.jar differ diff --git a/src/nagini_translation/sif/lib/viper_ast_extended.py b/src/nagini_translation/sif/lib/viper_ast_extended.py index 707b5adb8..d40f2b739 100644 --- a/src/nagini_translation/sif/lib/viper_ast_extended.py +++ b/src/nagini_translation/sif/lib/viper_ast_extended.py @@ -8,7 +8,7 @@ from typing import List, Optional from nagini_translation.lib.typedefs import ( - Expr, Info, Position, Seqn, Stmt, Var, VarAssign + Expr, Info, Position, Seqn, Stmt, Var, VarAssign, While ) from nagini_translation.lib.viper_ast import ViperAST from nagini_translation.sif.lib.util import ( @@ -69,6 +69,10 @@ def SIFExceptionHandler(self, err_var: Var, exception: Expr, handler: Seqn): return self.ast_extensions.SIFExceptionHandler( err_var, exception, handler, self.NoPosition, self.NoInfo, self.NoTrafos) + def SIFWhileElse(self, loop: While, els: Stmt): + return self.ast_extensions.SIFWhileElse( + loop, els, self.NoPosition, self.NoInfo, self.NoTrafos) + def Try(self, body: Seqn, catch_blocks: List['silver.sif.SIFExceptionHandler'], else_block: Optional[Seqn], finally_block: Optional[Seqn], position: Position, info: Info): diff --git a/src/nagini_translation/sif/translators/statement.py b/src/nagini_translation/sif/translators/statement.py index 3b66af2da..3e618539a 100644 --- a/src/nagini_translation/sif/translators/statement.py +++ b/src/nagini_translation/sif/translators/statement.py @@ -9,6 +9,7 @@ from typing import List from nagini_translation.lib.constants import ARBITRARY_BOOL_FUNC +from nagini_translation.lib.errors import rules from nagini_translation.lib.program_nodes import PythonClass, PythonTryBlock, PythonVar from nagini_translation.lib.typedefs import Expr, Position, Seqn, Stmt, Var, VarDecl from nagini_translation.lib.util import flatten, get_body_indices, get_surrounding_try_blocks @@ -110,7 +111,15 @@ def translate_stmt_Try(self, node: ast.Try, ctx: Context) -> List[Stmt]: def translate_stmt_Raise(self, node: ast.Raise, ctx: Context) -> List[Stmt]: err_var = self.get_error_var(node, ctx).ref() stmts = self._translate_stmt_raise_create(node, err_var, ctx) - return stmts[:-1] + [ + ex_type_low = [] + if ctx.sif == 'prob': + position = self.to_position(node.exc, ctx, rules=rules.EXCEPTION_TYPE_LOW) + info = self.no_info(ctx) + exc_expr = stmts[-1].rhs() + exc_type = self.type_factory.typeof(exc_expr, ctx) + + ex_type_low.append(self.viper.Assert(self.viper.Low(exc_type, None, position, info), position, info)) + return stmts[:-1] + ex_type_low + [ self.viper.Raise(stmts[-1], self.to_position(node, ctx), self.no_info(ctx)) ] diff --git a/src/nagini_translation/tests.py b/src/nagini_translation/tests.py index 50b9f6b07..b22eee10c 100644 --- a/src/nagini_translation/tests.py +++ b/src/nagini_translation/tests.py @@ -558,8 +558,9 @@ class VerificationTest(AnnotatedTest): def test_file( self, path: str, base: str, jvm: jvmaccess.JVM, verifier: ViperVerifier, - sif: bool, reload_resources: bool, arp: bool, store_viper: bool): + sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool): """Test specific Python file.""" + config.obligation_config.disable_all = ignore_obligations annotation_manager = self.get_annotation_manager(path, verifier.name) if arp: pytest.skip('Ignoring ARP tests') @@ -617,9 +618,9 @@ def _evaluate_result( _VERIFICATION_TESTER = VerificationTest() -def test_verification(path, base, verifier, sif, reload_resources, arp, print): +def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print): """Execute provided verification test.""" - _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, print) + _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations, print) class TranslationTest(AnnotatedTest): diff --git a/src/nagini_translation/translators/call.py b/src/nagini_translation/translators/call.py index fae3de4bf..12ca33bb4 100644 --- a/src/nagini_translation/translators/call.py +++ b/src/nagini_translation/translators/call.py @@ -16,6 +16,7 @@ ) from nagini_contracts.io_contracts import IO_CONTRACT_FUNCS from nagini_contracts.obligations import OBLIGATION_CONTRACT_FUNCS +from nagini_translation.lib.config import obligation_config from nagini_translation.lib import silver_nodes as sil from nagini_translation.lib.constants import ( BUILTIN_PREDICATES, @@ -511,7 +512,7 @@ def _translate_method_call(self, target: PythonMethod, args: List[Expr], if target.name in ('acquire', 'release'): if (target.cls and target.cls.name == 'Lock' and target.cls.module.type_prefix == 'nagini_contracts.lock'): - if ctx.sif == 'true': + if ctx.sif is True: raise InvalidProgramException(node, 'concurrency.in.sif') # Store receiver for later use (contents of args list get changed by # subsequent call). @@ -1129,6 +1130,10 @@ def translate_normal_call(self, target: PythonMethod, arg_stmts: List[Stmt], # Method called on an object recv_stmts, recv_exprs, recv_types = self._translate_receiver( node, target, ctx) + if ctx.sif == 'prob' and target.method_type == MethodType.normal and not target.pure and not target.predicate: + info = self.no_info(ctx) + recv_pos = self.to_position(node.func.value, ctx, rules=rules.BRANCH_RECEIVER_LOW) + recv_stmts.append(self.viper.Assert(self.viper.Low(self.type_factory.typeof(recv_exprs[0], ctx), None, recv_pos, info), recv_pos, info)) is_predicate = target.predicate receiver_class = target.cls if target.method_type != MethodType.static_method: @@ -1202,9 +1207,17 @@ def translate_Call(self, node: ast.Call, ctx: Context, impure=False, if func_name in CONTRACT_WRAPPER_FUNCS: raise InvalidProgramException(node, 'invalid.contract.position') elif func_name in CONTRACT_FUNCS: - return self.translate_contractfunc_call(node, ctx, impure, statement) + old_allow_statements = ctx.allow_statements + ctx.allow_statements = False + res = self.translate_contractfunc_call(node, ctx, impure, statement) + ctx.allow_statements = old_allow_statements + return res elif func_name in IO_CONTRACT_FUNCS: - return self.translate_io_contractfunc_call(node, ctx, impure, statement) + old_allow_statements = ctx.allow_statements + ctx.allow_statements = False + res = self.translate_io_contractfunc_call(node, ctx, impure, statement) + ctx.allow_statements = old_allow_statements + return res elif func_name in OBLIGATION_CONTRACT_FUNCS: return self.translate_obligation_contractfunc_call(node, ctx, impure) elif func_name in BUILTINS: @@ -1304,7 +1317,7 @@ def _handle_thread_constructor_args(self, node: ast.Call, ctx: Context): def _translate_thread_creation(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: """Translates the instantiation of a Thread object.""" - if ctx.sif == 'true': + if ctx.sif is True: raise InvalidProgramException(node, 'concurrency.in.sif') ctx.are_threading_constants_used = True pos, info = self.to_position(node, ctx), self.no_info(ctx) @@ -1367,7 +1380,7 @@ def _translate_thread_creation(self, node: ast.Call, def _translate_thread_start(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: """Translates a thread start call.""" - if ctx.sif == 'true': + if ctx.sif is True: raise InvalidProgramException(node, 'concurrency.in.sif') ctx.are_threading_constants_used = True pos, info = self.to_position(node, ctx), self.no_info(ctx) @@ -1421,7 +1434,7 @@ def _translate_thread_start(self, node: ast.Call, def _translate_thread_join(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: """Translates a thread join call.""" - if ctx.sif == 'true': + if ctx.sif is True: raise InvalidProgramException(node, 'concurrency.in.sif') ctx.are_threading_constants_used = True pos, info = self.to_position(node, ctx), self.no_info(ctx) @@ -1445,7 +1458,8 @@ def _translate_thread_join(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: obligation_assertion = self.create_level_below(thread_level, residue_var, ctx) obligation_assertion = obligation_assertion.translate(self, ctx, wait_level_pos, info) - stmts.append(self.viper.Assert(obligation_assertion, wait_level_pos, info)) + if not obligation_config.disable_waitlevel_check: + stmts.append(self.viper.Assert(obligation_assertion, wait_level_pos, info)) # Check how much permission is held to ThreadPost. This amount of the thread # postcondition will be inhaled later. diff --git a/src/nagini_translation/translators/expression.py b/src/nagini_translation/translators/expression.py index 45fe37676..bbadd3cf7 100644 --- a/src/nagini_translation/translators/expression.py +++ b/src/nagini_translation/translators/expression.py @@ -165,7 +165,9 @@ def translate_ListComp(self, node: ast.ListComp, ctx: Context) -> StmtsAndExpr: local_name = name + '$' + target.id element_var = ctx.actual_function.special_vars[local_name] ctx.set_alias(target.id, element_var) + ctx.allow_statements = False body_stmt, body = self.translate_expr(node.elt, ctx) + ctx.allow_statements = True result_type = self.get_type(node.elt, ctx) list_type = GenericType(list_class, [result_type]) if body_stmt: @@ -228,7 +230,11 @@ def _create_list_comp_inhale(self, result_var: PythonVar, list_type: PythonType, contents = self.viper.And(len_equal, values, position, info) all = self.viper.And(type_and_perm, contents, position, info) inhale = self.viper.Inhale(all, position, info) - return iter_stmt + [inhale] + sif_checks = [] + if ctx.sif == 'prob': + low_pos = self.to_position(node, ctx, rules=rules.COMPREHENSION_LOW) + sif_checks.append(self.viper.Assert(self.viper.Low(seq_len, None, low_pos, info), low_pos, info)) + return iter_stmt + [inhale] + sif_checks def translate_Num(self, node: ast.Num, ctx: Context) -> StmtsAndExpr: pos = self.to_position(node, ctx) @@ -851,6 +857,7 @@ def translate_UnaryOp(self, node: ast.UnaryOp, def translate_IfExp(self, node: ast.IfExp, ctx: Context, impure=False) -> StmtsAndExpr: position = self.to_position(node, ctx) + info = self.no_info(ctx) cond_stmt, cond = self.translate_expr(node.test, ctx, target_type=self.viper.Bool) then_stmt, then = self.translate_expr(node.body, ctx, @@ -861,17 +868,20 @@ def translate_IfExp(self, node: ast.IfExp, ctx: Context, impure=impure) if then_stmt or else_stmt: then_block = self.translate_block(then_stmt, position, - self.no_info(ctx)) + info) else_block = self.translate_block(else_stmt, position, - self.no_info(ctx)) + info) if_stmt = self.viper.If(cond, then_block, else_block, position, - self.no_info(ctx)) + info) bodystmt = [if_stmt] else: bodystmt = [] + if ctx.sif == 'prob' and ctx.allow_statements: + rule_pos = self.to_position(node.test, ctx, rules=rules.BRANCH_CONDITION_ASSERT) + cond_stmt.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) cond_exp = self.viper.CondExp(cond, then, else_, self.to_position(node, ctx), - self.no_info(ctx)) + info) return cond_stmt + bodystmt, cond_exp def translate_BinOp(self, node: ast.BinOp, ctx: Context) -> StmtsAndExpr: @@ -1172,6 +1182,9 @@ def translate_BoolOp(self, node: ast.BoolOp, ctx: Context, all_pure = False if self._is_expression and statements_part: raise InvalidProgramException(node, 'not_expression') + if ctx.sif == 'prob' and self._is_pure(expression_part) and ctx.allow_statements: + low_pos = self.to_position(node, ctx, rules=rules.SHORT_CIRCUIT_LOW) + statements_part.append(self.viper.Assert(self.viper.Low(bool_expression, None, low_pos, info), low_pos, info)) statements_parts.append(statements_part) if all_pure: expression_parts.append(self.to_ref(expression_part, ctx)) diff --git a/src/nagini_translation/translators/method.py b/src/nagini_translation/translators/method.py index b91c678eb..a7b7c696d 100644 --- a/src/nagini_translation/translators/method.py +++ b/src/nagini_translation/translators/method.py @@ -70,15 +70,6 @@ def _translate_pres(self, method: PythonMethod, Translates the preconditions specified for 'method'. """ pres = [] - if ctx.sif == 'poss': - # Force TerminatesSIF annotation - pre_nodes = method.precondition - if not pre_nodes: - raise InvalidProgramException(method.node, 'missing.termination.annotation') - term_ann = pre_nodes[-1][0] - if not (isinstance(term_ann, ast.Call) and isinstance(term_ann.func, ast.Name) and - term_ann.func.id == 'TerminatesSif'): - raise InvalidProgramException(method.node, 'missing.termination.annotation') for pre, aliases in method.precondition: with ctx.additional_aliases(aliases): stmt, expr = self.translate_expr(pre, ctx, self.viper.Bool, True) @@ -468,9 +459,11 @@ def _translate_method_body(self, method: PythonMethod, ctx: Context) -> List[Stm body_start, body_end = get_body_indices(statements) # Create local variables for parameters body.extend(self._create_local_vars_for_params(method, ctx)) + ctx.allow_statements = True body += flatten( [self.translate_stmt(stmt, ctx) for stmt in method.node.body[body_start:body_end]]) + ctx.allow_statements = False return body def _translate_try_handlers(self, method: PythonMethod, ctx: Context) -> List[Stmt]: @@ -953,8 +946,10 @@ def translate_main_method(self, modules: List[PythonModule], # Translate statements in main module. When an import statement is encountered, # the translation will include executing the statements in the imported module. + ctx.allow_statements = True for stmt in main.node.body: stmts.extend(self.translate_stmt(stmt, ctx)) + ctx.allow_statements = False stmts += self._method_body_postamble(main_method, ctx) stmts += self._create_method_epilog(main_method, ctx) diff --git a/src/nagini_translation/translators/obligation/fork.py b/src/nagini_translation/translators/obligation/fork.py index 9701e166b..25d8a793e 100644 --- a/src/nagini_translation/translators/obligation/fork.py +++ b/src/nagini_translation/translators/obligation/fork.py @@ -11,6 +11,7 @@ from typing import List from nagini_translation.lib import silver_nodes as sil +from nagini_translation.lib.config import obligation_config from nagini_translation.lib.constants import ( GET_ARG_FUNC, GET_METHOD_FUNC, @@ -212,7 +213,8 @@ def _add_waitlevel(self) -> None: level = self.create_level_call(sil.RefExpr(self._thread)) comp = self._create_level_below(level, self._ctx) comp = comp.translate(self._translator, self._ctx, self._position, self._info) - self._statements.append(self.viper.Inhale(comp, self._position, self._info)) + if not obligation_config.disable_waitlevel_check: + self._statements.append(self.viper.Inhale(comp, self._position, self._info)) def _create_level_below( self, expr: sil.PermExpression, diff --git a/src/nagini_translation/translators/statement.py b/src/nagini_translation/translators/statement.py index dfc6c411a..09f0a4842 100644 --- a/src/nagini_translation/translators/statement.py +++ b/src/nagini_translation/translators/statement.py @@ -61,6 +61,7 @@ ) from nagini_translation.translators.abstract import Context from nagini_translation.translators.common import CommonTranslator +from nagini_translation.lib.errors import rules from typing import List, Optional, Tuple, Union @@ -730,6 +731,12 @@ def translate_stmt_For(self, node: ast.For, ctx: Context) -> List[Stmt]: self.viper.NullLit(position, info), position, info) + cond_low = [] + if ctx.sif == 'prob': + rule_pos = self.to_position(node.iter, ctx, rules=rules.BRANCH_CONDITION_ASSERT) + info = self.no_info(ctx) + cond_low.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) + conditional_assign = self.viper.If(cond, self.translate_block(assign_stmt, position, info), self.translate_block([], position, info), @@ -748,7 +755,7 @@ def translate_stmt_For(self, node: ast.For, ctx: Context) -> List[Stmt]: position, info) self.enter_loop_translation(node, post_label, end_label, ctx, err_var) - + ctx.allow_statements = False invariant = self._create_for_loop_invariant(iter_var, seq_temp_var, target_var, err_var, iterable, iterable_type, assign_expr, @@ -760,26 +767,30 @@ def translate_stmt_For(self, node: ast.For, ctx: Context) -> List[Stmt]: # Remember type information about havocked local variables. invariant.extend(self._get_havocked_var_type_info(node.body[start:end], ctx)) - if ctx.sif == 'poss': - # Force TerminatesSIF annotation + # Check if TerminatesSIF annotation present inv_nodes = ctx.actual_function.loop_invariants[node] - if not inv_nodes: - raise InvalidProgramException(node, 'missing.termination.annotation') - term_ann = inv_nodes[-1][0] - if not (isinstance(term_ann, ast.Call) and isinstance(term_ann.func, ast.Name) and - term_ann.func.id == 'TerminatesSif'): - raise InvalidProgramException(node, 'missing.termination.annotation') + term_ann = None + if inv_nodes: + term_ann = inv_nodes[-1][0] + if not (isinstance(term_ann.args[0], ast.Call) and isinstance(term_ann.args[0].func, ast.Name) and + term_ann.args[0].func.id == 'TerminatesSif'): + term_ann = None + if not term_ann: + rule_pos = self.to_position(node.iter, ctx, rules=rules.POSS_BRANCH_CONDITION_ASSERT) + info = self.no_info(ctx) + cond_low.append(self.viper.Assert(self.viper.LowEvent(rule_pos, info), rule_pos, info)) + cond_low.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) for expr, aliases in ctx.actual_function.loop_invariants[node]: with ctx.additional_aliases(aliases): invariant.append(self.translate_contract(expr, ctx)) - + ctx.allow_statements = True body = flatten( [self.translate_stmt(stmt, ctx) for stmt in node.body[start:end]]) # Label for continue to jump to body.append(self.viper.Label(end_label, position, info)) body.extend(next_call) - + body.extend(cond_low) body.extend(assign_stmt) loop = global_stmts + self.create_while_node( @@ -787,13 +798,22 @@ def translate_stmt_For(self, node: ast.For, ctx: Context) -> List[Stmt]: iter_del = self._get_iterator_delete(iter_var, node, ctx) self.leave_loop_translation(ctx) del ctx.loop_iterators[node] - result = (iterable_stmt + iter_assign + next_call + assign_stmt + + result = (iterable_stmt + iter_assign + next_call + cond_low + assign_stmt + [seq_temp_assign] + loop + iter_del) result += self._set_result_none(ctx) if node.orelse: translated_block = flatten([self.translate_stmt(stmt, ctx) for stmt in node.orelse]) - result += translated_block + if ctx.sif: + translated_block = self.translate_block(translated_block, self.no_position(ctx), self.no_info(ctx)) + i = 0 + while i < len(result): + if isinstance(result[i], self.viper.ast.While): + break + i += 1 + result[i] = self.viper.SIFWhileElse(result[i], translated_block) + else: + result += translated_block # Label for break to jump to result.append(self.viper.Label(post_label, position, info)) result += self._set_result_none(ctx) @@ -989,7 +1009,8 @@ def translate_stmt_If(self, node: ast.If, ctx: Context) -> List[Stmt]: info = self.no_info(ctx) cond_low = [] if ctx.sif == 'prob': - cond_low.append(self.viper.Assert(self.viper.Low(cond, None, position, info), position, info)) + rule_pos = self.to_position(node.test, ctx, rules=rules.BRANCH_CONDITION_ASSERT) + cond_low.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) return cond_stmt + cond_low + [self.viper.If(cond, then_block, else_block, position, info)] @@ -1273,21 +1294,30 @@ def translate_stmt_Assign(self, node: ast.Assign, assign_stmts += target_stmt return rhs_stmt + assign_stmts - def _translate_while_invariants(self, node: ast.While, ctx: Context) -> List[Stmt]: + def _translate_while_invariants(self, node: ast.While, cond: Expr, ctx: Context) -> Tuple[List[Expr], List[Stmt]]: + ctx.allow_statements = False invariants = [] + cond_low = [] if ctx.sif == 'poss': - # Force TerminatesSIF annotation + # Check if TerminatesSIF annotation present inv_nodes = ctx.actual_function.loop_invariants[node] - if not inv_nodes: - raise InvalidProgramException(node, 'missing.termination.annotation') - term_ann = inv_nodes[-1][0] - if not (isinstance(term_ann, ast.Call) and isinstance(term_ann.func, ast.Name) and - term_ann.func.id == 'TerminatesSif'): - raise InvalidProgramException(node, 'missing.termination.annotation') + term_ann = None + if inv_nodes: + term_ann = inv_nodes[-1][0] + if not (isinstance(term_ann.args[0], ast.Call) and isinstance(term_ann.args[0].func, ast.Name) and + term_ann.args[0].func.id == 'TerminatesSif'): + term_ann = None + if not term_ann: + rule_pos = self.to_position(node.test, ctx, rules=rules.POSS_BRANCH_CONDITION_ASSERT) + info = self.no_info(ctx) + cond_low.append(self.viper.Assert(self.viper.LowEvent(rule_pos, info), rule_pos, info)) + cond_low.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) + for expr, aliases in ctx.actual_function.loop_invariants[node]: with ctx.additional_aliases(aliases): invariants.append(self.translate_contract(expr, ctx)) - return invariants + ctx.allow_statements = True + return invariants, cond_low def _translate_while_body(self, node: ast.While, ctx: Context, end_label: str) -> List[Stmt]: start, end = get_body_indices(node.body) @@ -1314,25 +1344,36 @@ def translate_stmt_While(self, node: ast.While, target_type=self.viper.Bool) if cond_stmt: raise InvalidProgramException(node, 'purity.violated') - cond_low = [] + invariants, cond_low = self._translate_while_invariants(node, cond, ctx) if ctx.sif == 'prob': - position = self.to_position(node, ctx) + rule_pos = self.to_position(node.test, ctx, rules=rules.BRANCH_CONDITION_ASSERT) info = self.no_info(ctx) - cond_low.append(self.viper.Assert(self.viper.Low(cond, None, position, info), position, info)) - invariants = self._translate_while_invariants(node, ctx) + cond_low.append(self.viper.Assert(self.viper.Low(cond, None, rule_pos, info), rule_pos, info)) locals = [] start, end = get_body_indices(node.body) var_types = self._get_havocked_var_type_info(node.body[start:end], ctx) global_stmts, global_inv = self._get_havocked_module_var_info(ctx) invariants = [global_inv] + var_types + invariants body = self._translate_while_body(node, ctx, end_label) + ctx.allow_statements = False loop = global_stmts + cond_low + self.create_while_node( ctx, cond, invariants, locals, body, node) + ctx.allow_statements = True self.leave_loop_translation(ctx) if node.orelse: translated_block = flatten([self.translate_stmt(stmt, ctx) for stmt in node.orelse]) - loop += translated_block + + if ctx.sif: + translated_block = self.translate_block(translated_block, self.no_position(ctx), self.no_info(ctx)) + i = 0 + while i < len(loop): + if isinstance(loop[i], self.viper.ast.While): + break + i += 1 + loop[i] = self.viper.SIFWhileElse(loop[i], translated_block) + else: + loop += translated_block loop += self._while_postamble(node, post_label, ctx) return loop diff --git a/src/nagini_translation/verifier.py b/src/nagini_translation/verifier.py index 95c93e90f..dfadc3772 100644 --- a/src/nagini_translation/verifier.py +++ b/src/nagini_translation/verifier.py @@ -182,6 +182,6 @@ def verify(self, modules, prog: 'silver.ast.Program', arp=False, sif=False) -> V errors = [] while it.hasNext(): errors += [it.next()] - return Failure(errors, self.jvm, modules, False) + return Failure(errors, self.jvm, modules, sif) else: return Success() diff --git a/tests/functional/verification/test_loop_break.py b/tests/functional/verification/test_loop_break.py index 57193fb38..cd83f35ee 100644 --- a/tests/functional/verification/test_loop_break.py +++ b/tests/functional/verification/test_loop_break.py @@ -41,19 +41,56 @@ def find_divisor_else(product: int) -> int: return i +@Pure +def not_dividing(from_index: int, to_index: int, product: int) -> bool: + Requires(from_index > 1) + if to_index < from_index: + return True + else: + rec = not_dividing(from_index, to_index - 1, product) + return rec and product % to_index != 0 + + +def find_divisor_else_2(product: int) -> int: + Requires(product >= 2) + Ensures(Result() == -1 or (Result() >= 2 and Result() <= product)) + Ensures(Implies(Result() > 0, not_dividing(2, Result() - 1, product))) + Ensures(Implies(Result() == -1, not_dividing(2, product - 1, product))) + Ensures(Implies(Result() > 0, product % Result() == 0)) + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(False) + i = 2 + while i < product: + Invariant(i >= 2 and i <= product) + Invariant(not_dividing(2, i - 1, product)) + # Invariant(Forall(int, lambda x: (Implies(x >= 2 and x < i, product % x != 0), [[product % x]]))) + if product % i == 0: + break + i += 1 + else: + Assert(not (i < product)) + Assert(i == product) + Assert(not_dividing(2, product - 1, product)) + return -1 + return i + + def find_divisor_for(product: int) -> int: Requires(product > 2) - Ensures(Result() >= 2 and Result() <= product) - Ensures(Forall(int, lambda x: (Implies(x >= 2 and x < Result(), product % x != 0), [[product % x]]))) - Ensures(Implies(Result() != product, product % Result() == 0)) + Ensures(Result() == -1 or (Result() >= 2 and Result() <= product)) + Ensures(Implies(Result() > 0, not_dividing(2, Result() - 1, product))) + Ensures(Implies(Result() == -1, not_dividing(2, product - 1, product))) + Ensures(Implies(Result() > 0, product % Result() == 0)) + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(False) for i in range(2, product): Invariant(i >= 2 and i <= product) - Invariant(Forall(Previous(i), lambda x: (product % x != 0, [[product % x]]))) + Invariant(not_dividing(2, len(Previous(i)) + 2 - 1, product)) if product % i == 0: - Assert(Previous(i) == ToSeq(range(2, i))) break else: - i = product + Assert(not_dividing(2, product - 1, product)) + i = -1 return i diff --git a/tests/sif-poss/verification/examples/cav2021-fig12.py b/tests/sif-poss/verification/examples/cav2021-fig12.py new file mode 100644 index 000000000..485cfc4df --- /dev/null +++ b/tests/sif-poss/verification/examples/cav2021-fig12.py @@ -0,0 +1,36 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock +from nagini_contracts.obligations import WaitLevel, Level + +class Cell: + def __init__(self) -> None: + Requires(TerminatesSif(True, 2)) + self.go_1 = False + self.go_2 = False + self.leak = False + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return (Acc(self.get_locked().go_1) and + Acc(self.get_locked().go_2) and + Acc(self.get_locked().leak) and Low(self.get_locked().leak)) + + + +def thread2(l: CellLock, c: Cell, secret: int) -> None: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent() and WaitLevel() < Level(l)) + while secret > 0: + # When writing TerminatesSif(e1, e2) as the last part of the invariant, Nagini does not check that the + # termination condition is low (which is the default), but instead checks that the loop terminates if e1 holds + # initially, using the ranking function e2. This is an alternative sufficient condition. + Invariant(TerminatesSif(True, secret)) + secret -= 1 + l.acquire() + c.leak = False + l.release() diff --git a/tests/sif-poss/verification/examples/cav2021-fig9.py b/tests/sif-poss/verification/examples/cav2021-fig9.py new file mode 100644 index 000000000..b26af0aa6 --- /dev/null +++ b/tests/sif-poss/verification/examples/cav2021-fig9.py @@ -0,0 +1,43 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock +from nagini_contracts.obligations import Level, WaitLevel + +class Cell: + def __init__(self, val: int) -> None: + Requires(TerminatesSif(True, 2)) + self.value = val + Ensures(Acc(self.value) and self.value == val) + + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return Acc(self.get_locked().value) and LowVal(self.get_locked().value) + + +def thread1(l: CellLock, c: Cell) -> None: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent() and WaitLevel() < Level(l)) + ctr = 0 + while ctr < 100: + Invariant(Low(ctr)) + ctr += 1 + l.acquire() + c.value = 1 + l.release() + + +def thread2(l: CellLock, c: Cell, secret: int) -> None: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent() and WaitLevel() < Level(l)) + ctr = 0 + while ctr < secret: + Invariant(TerminatesSif(True, secret - ctr)) + ctr += 1 + l.acquire() + c.value = 2 + l.release() diff --git a/tests/sif-poss/verification/examples/no_obligations/cav2021-fig11.py b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig11.py new file mode 100644 index 000000000..e5882e5ff --- /dev/null +++ b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig11.py @@ -0,0 +1,80 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from "Principles of Secure Information Flow Analysis" +G. Smith +Malware Detection, 2007 +""" + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock +from nagini_contracts.obligations import WaitLevel, Level, MustRelease + +class Cell: + def __init__(self) -> None: + self.go_1 = False + self.go_2 = False + self.leak = False + self.proceed = False + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return (Acc(self.get_locked().go_1) and + Acc(self.get_locked().go_2) and + Acc(self.get_locked().proceed) and Low(self.get_locked().proceed) and + Acc(self.get_locked().leak) and Low(self.get_locked().leak)) + + +def thread_0(l: CellLock, c: Cell, secret: bool) -> bool: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent()) + Ensures(Low(Result())) + l.acquire() + if secret: + c.go_1 = True + else: + c.go_2 = True + l.release() + l.acquire() + Fold(l.invariant()) + while not Unfolding(l.invariant(), c.proceed): + Invariant(l.invariant() and MustRelease(l)) + Unfold(l.invariant()) + l.release() + l.acquire() + Fold(l.invariant()) + Unfold(l.invariant()) + leak = c.leak + l.release() + return leak + + +def thread1(l: CellLock, c: Cell, secret: int) -> None: + Requires(LowEvent() and Low(l) and l.get_locked() is c) + l.acquire() + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + while not c.go_1: + Invariant(Acc(c.go_1)) + #:: ExpectedOutput(carbon)(lock.invariant.not.established:insufficient.permission) + l.release() + l.acquire() + c.leak = True + c.proceed = True + l.release() + + +def thread2(l: CellLock, c: Cell, secret: int) -> None: + Requires(LowEvent() and Low(l) and l.get_locked() is c) + l.acquire() + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + while not c.go_2: + Invariant(Acc(c.go_2)) + #:: ExpectedOutput(carbon)(lock.invariant.not.established:insufficient.permission) + l.release() + l.acquire() + c.leak = False + c.proceed = True + l.release() diff --git a/tests/sif-poss/verification/examples/no_obligations/cav2021-fig7.py b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig7.py new file mode 100644 index 000000000..7e3a52e35 --- /dev/null +++ b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig7.py @@ -0,0 +1,33 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.lock import Lock +from nagini_contracts.contracts import * +from nagini_contracts.obligations import Level, WaitLevel + + +class Cell: + def __init__(self, val: int) -> None: + Requires(TerminatesSif(True, 2)) + self.value = val + Ensures(Acc(self.value) and self.value == val) + + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return Acc(self.get_locked().value) and LowVal(self.get_locked().value) + +def client(secret: bool) -> None: + Requires(LowEvent()) + c = Cell(1) + l = CellLock(c) + l.acquire() + c.value = 4 + if secret: + #:: ExpectedOutput(call.precondition:assertion.false) + l.release() + l.acquire() + c.value = 5 + l.release() \ No newline at end of file diff --git a/tests/sif-poss/verification/examples/no_obligations/cav2021-fig8.py b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig8.py new file mode 100644 index 000000000..b99474fb0 --- /dev/null +++ b/tests/sif-poss/verification/examples/no_obligations/cav2021-fig8.py @@ -0,0 +1,45 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock +from nagini_contracts.thread import Thread + + +class CellLock(Lock[object]): + + @Predicate + def invariant(self) -> bool: + return True + + +@ContractOnly +def _print(i: int) -> None: + Requires(LowEvent()) + Requires(Low(i)) + +def thread1(l: CellLock) -> None: + Requires(LowEvent()) + Requires(Low(l)) + l.acquire() + _print(1) + _print(1) + l.release() + +def thread2(l: CellLock) -> None: + Requires(LowEvent()) + #:: ExpectedOutput(call.precondition:assertion.false) + l.acquire() + _print(2) + _print(2) + + +def thread0(secret: bool) -> None: + Requires(LowEvent()) + l1 = CellLock(object()) + l2 = CellLock(object()) + l = l1 if secret else l2 + t1 = Thread(target=thread1, args=(l1,)) # x aliases l2 depending on secret + t2 = Thread(target=thread2, args=(l,)) + t1.start(thread1) + t2.start(thread2) diff --git a/tests/sif/verification/test_lock.py b/tests/sif-poss/verification/test_lock.py similarity index 100% rename from tests/sif/verification/test_lock.py rename to tests/sif-poss/verification/test_lock.py diff --git a/tests/sif-poss/verification/test_loop.py b/tests/sif-poss/verification/test_loop.py new file mode 100644 index 000000000..3e1346af7 --- /dev/null +++ b/tests/sif-poss/verification/test_loop.py @@ -0,0 +1,104 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +def while_cond_low_fail(n: int) -> None: + Requires(LowEvent()) + i = 0 + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + while i < n: + i += 1 + + +def while_cond_low(n: int) -> None: + Requires(Low(n)) + Requires(LowEvent()) + i = 0 + while i < n: + Invariant(Low(i)) + i += 1 + + +def while_cond_low_fail_not_lowevent(n: int) -> None: + Requires(Low(n)) + i = 0 + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + while i < n: + Invariant(Low(i)) + i += 1 + + +def while_terminatessif(n: int) -> None: + Requires(Low(n)) + Requires(LowEvent()) + i = 0 + while i != n: + Invariant(i >= 0) + Invariant(TerminatesSif(n >= 0, n-i)) + i += 1 + + +def while_terminatessif_fail(n: int) -> None: + Requires(LowEvent()) + i = 0 + while i != n: + #:: ExpectedOutput(termination_channel_check.failed:sif_termination.condition_not_low)|ExpectedOutput(carbon)(termination_channel_check.failed:sif_termination.condition_not_tight) + Invariant(TerminatesSif(n >= 0, n-i)) + i += 1 + + +def for_cond_low_fail(n: int) -> int: + Requires(n > 0) + Requires(LowEvent()) + res = 0 + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + for i in range(0, n): + res += 1 + return res + + +def for_cond_low(n: int) -> int: + Requires(n > 0) + Requires(Low(n)) + Requires(LowEvent()) + res = 0 + for i in range(0, n): + Invariant(Low(Previous(i))) + res += 1 + return res + + +def for_cond_low_fail_not_lowevent(n: int) -> int: + Requires(n > 0) + Requires(Low(n)) + res = 0 + #:: ExpectedOutput(possibilistic.sif.violated:high.branch) + for i in range(0, n): + Invariant(Low(Previous(i))) + res += 1 + return res + + +def for_terminatessif(n: int) -> int: + Requires(n > 0) + Requires(Low(n)) + Requires(LowEvent()) + res = 0 + for i in range(0, n): + Invariant(Low(Previous(i))) + Invariant(TerminatesSif(True, n - len(Previous(i)))) + res += 1 + return res + + +def for_terminatessif_fail(n: int) -> int: + Requires(n > 0) + Requires(LowEvent()) + res = 0 + for i in range(0, n): + #:: ExpectedOutput(termination_channel_check.failed:sif_termination.condition_not_low)|ExpectedOutput(carbon)(termination_channel_check.failed:sif_termination.condition_not_tight) + Invariant(TerminatesSif(n > 1, n - len(Previous(i)))) + res += 1 + return res \ No newline at end of file diff --git a/tests/sif/verification/test_threads.py b/tests/sif-poss/verification/test_threads.py similarity index 100% rename from tests/sif/verification/test_threads.py rename to tests/sif-poss/verification/test_threads.py diff --git a/tests/sif-prob/verification/examples/no_obligations/cav2021-fig9.py b/tests/sif-prob/verification/examples/no_obligations/cav2021-fig9.py new file mode 100644 index 000000000..21adc7a58 --- /dev/null +++ b/tests/sif-prob/verification/examples/no_obligations/cav2021-fig9.py @@ -0,0 +1,42 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock + +class Cell: + def __init__(self, val: int) -> None: + Requires(TerminatesSif(True, 2)) + self.value = val + Ensures(Acc(self.value) and self.value == val) + + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return Acc(self.get_locked().value) and LowVal(self.get_locked().value) + + +def thread1(l: CellLock, c: Cell) -> None: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent()) + ctr = 0 + while ctr < 100: + Invariant(Low(ctr)) + ctr += 1 + l.acquire() + c.value = 1 + l.release() + + +def thread2(l: CellLock, c: Cell, secret: int) -> None: + Requires(Low(l) and l.get_locked() is c) + Requires(LowEvent()) + ctr = 0 + #:: ExpectedOutput(probabilistic.sif.violated:high.branch) + while ctr < secret: + ctr += 1 + l.acquire() + c.value = 2 + l.release() diff --git a/tests/sif-prob/verification/examples/no_obligations/secc-cav2019.py b/tests/sif-prob/verification/examples/no_obligations/secc-cav2019.py new file mode 100644 index 000000000..b63af7186 --- /dev/null +++ b/tests/sif-prob/verification/examples/no_obligations/secc-cav2019.py @@ -0,0 +1,68 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from "SecCSL: Security Concurrent Separation Logic" +G. Ernst and T. Murray +CAV 2019 +https://bitbucket.org/covern/secc/src/master/examples/case-studies/ +""" + +from nagini_contracts.contracts import * +from nagini_contracts.lock import Lock + +class Record: + def __init__(self, ic: bool, data: int) -> None: + self.is_classified = ic + self.data = data + + +class Mutex(Lock[Record]): + + @Predicate + def invariant(self) -> bool: + return (Acc(self.get_locked().is_classified) and + Acc(self.get_locked().data) and + Low(self.get_locked().is_classified) and + Implies(not self.get_locked().is_classified, Low(self.get_locked().data))) + + +# Models OUTPUT_REG from the SecCSL paper +def output(i: int) -> None: + Requires(Low(i)) + + +def thread1(r: Record, m: Mutex) -> None: + Requires(m.get_locked() is r and Low(m)) + while True: + m.acquire() + if not r.is_classified: + output(r.data) + m.release() + + +def thread2(r: Record, m: Mutex) -> None: + Requires(m.get_locked() is r and Low(m)) + m.acquire() + r.is_classified = False + r.data = 0 + m.release() + + +def thread1_insecure(r: Record, m: Mutex) -> None: + Requires(m.get_locked() is r and Low(m)) + while True: + m.acquire() + if r.is_classified: # BUG + #:: ExpectedOutput(call.precondition:assertion.false) + output(r.data) + m.release() + + +def thread2_insecure(r: Record, m: Mutex) -> None: + Requires(m.get_locked() is r and Low(m)) + m.acquire() + r.is_classified = False + # BUG: r.data = 0 + #:: ExpectedOutput(fold.failed:sif.fold) + m.release() diff --git a/tests/sif/verification/secc/cddc.py b/tests/sif-prob/verification/examples/no_obligations/secc-cddc.py similarity index 65% rename from tests/sif/verification/secc/cddc.py rename to tests/sif-prob/verification/examples/no_obligations/secc-cddc.py index c26217d8a..792d665d9 100644 --- a/tests/sif/verification/secc/cddc.py +++ b/tests/sif-prob/verification/examples/no_obligations/secc-cddc.py @@ -1,9 +1,19 @@ -# enums +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/ +""" + +#:: IgnoreFile(carbon)(107) + from nagini_contracts.adt import ADT from nagini_contracts.lock import Lock from nagini_contracts.contracts import * from typing import NamedTuple +#enums + class Button(ADT): pass @@ -53,6 +63,7 @@ class EventNone(Event, NamedTuple('EventNone', [])): class EventMouseDown(Event, NamedTuple('EventMouseDown', [])): pass + # classes and locks class RPCOverlay: @@ -127,7 +138,6 @@ def invariant(self) -> bool: # main class and methods - class CDDC: def __init__(self, ce: Event, b0: Event, b1: Event, ad: Domain, id: Domain, @@ -149,6 +159,8 @@ def __init__(self, ce: Event, b0: Event, b1: Event, ad: Domain, id: Domain, self.compositor_lock = CompositorLock(self.compositor) self.overlay = RPCOverlay(overlay_call, overlay_button, overlay_domain) self.overlay_lock = RPCOverlayLock(self.overlay) + self.switch_state_mouse_down = False + self.overlay_result = DomainInvalid() # type: Domain Ensures(Acc(self.hid, 1 / 2) and Acc(self.hid_lock, 1 / 2) and self.hid_lock.get_locked() is self.hid and Low(self.hid_lock)) Ensures(Acc(self.overlay, 1 / 2) and Acc(self.overlay_lock, 1 / 2) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) Ensures(Acc(self.compositor, 1 / 2) and Acc(self.compositor_lock, 1 / 2) and self.compositor_lock.get_locked() is self.compositor and Low(self.compositor_lock)) @@ -156,10 +168,13 @@ def __init__(self, ce: Event, b0: Event, b1: Event, ad: Domain, id: Domain, Ensures(Acc(self.indicated_domain) and Low(self.indicated_domain)) Ensures(Acc(self.hid.current_event_type) and Low(self.hid.current_event_type)) Ensures(Acc(self.output_event_buffer0) and Low(self.output_event_buffer0)) + Ensures(Acc(self.switch_state_mouse_down) and Low(self.switch_state_mouse_down)) + Ensures(Acc(self.overlay_result) and Low(self.overlay_result)) Ensures(Acc(self.output_event_buffer1)) Ensures(Acc(self.compositor.cursor_position)) Ensures(Acc(self.current_event_data)) + def driver(self) -> None: Requires(Acc(self.overlay, 1 / 2) and Acc(self.overlay_lock, 1 / 2) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) while True: @@ -180,6 +195,7 @@ def driver(self) -> None: self.overlay_lock.release() + def input_switch(self) -> None: Requires(Acc(self.hid, 1/2) and Acc(self.hid_lock, 1/2) and self.hid_lock.get_locked() is self.hid and Low(self.hid_lock)) Requires(Acc(self.overlay, 1 / 2) and Acc(self.overlay_lock, 1 / 2) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) @@ -191,11 +207,12 @@ def input_switch(self) -> None: Requires(Acc(self.output_event_buffer1)) Requires(Acc(self.compositor.cursor_position)) Requires(Acc(self.current_event_data)) + Requires(Acc(self.switch_state_mouse_down)) + Requires(Acc(self.overlay_result)) + temp = False - done_rpc = False - switch_state_mouse_down = False - overlay_result = DomainInvalid() # type: Domain - cursor_domain = DomainInvalid() # type: Domain + self.switch_state_mouse_down = False + self.overlay_result = DomainInvalid() self.current_event_data = EventNone() self.indicated_domain = self.active_domain self.hid.current_event_type = EventTypeNone() @@ -206,8 +223,8 @@ def input_switch(self) -> None: 1 / 2) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) Invariant(Acc(self.compositor, 1 / 2) and Acc(self.compositor_lock, 1 / 2) and self.compositor_lock.get_locked() is self.compositor and Low(self.compositor_lock)) - Invariant(Low(overlay_result)) - Invariant(Low(switch_state_mouse_down)) + Invariant(Acc(self.overlay_result) and Low(self.overlay_result)) + Invariant(Acc(self.switch_state_mouse_down) and Low(self.switch_state_mouse_down)) Invariant(Acc(self.current_event_data) and Low(self.current_event_data)) Invariant(Acc(self.active_domain) and Low(self.active_domain)) Invariant(Acc(self.indicated_domain) and self.indicated_domain is self.active_domain) @@ -221,69 +238,7 @@ def input_switch(self) -> None: self.hid_lock.release() if temp: - self.hid.current_event_type = EventTypeMouse() - self.hid_lock.acquire() - source = self.hid.mouse_source - self.hid_lock.release() - - self.overlay_lock.acquire() - self.overlay.mouse_click_arg = source - self.overlay.mouse_click_call = True - self.overlay_lock.release() - - done_rpc = False - - while not done_rpc: - Invariant(Acc(self.overlay, 1 / 4) and Acc(self.overlay_lock, 1 / 4) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) - Invariant(Low(done_rpc) and Low(overlay_result)) - self.overlay_lock.acquire() - if not self.overlay.mouse_click_call: - overlay_result = self.overlay.mouse_click_ret - done_rpc = True - self.overlay_lock.release() - - if overlay_result != DomainInvalid(): - cursor_domain = DomainOverlay() - else: - self.compositor.cursor_position = self.current_event_data - - self.compositor_lock.acquire() - cursor_domain = self.compositor.domain_under_cursor - self.compositor_lock.release() - - if cursor_domain == DomainInvalid(): - cursor_domain = self.active_domain - - if cursor_domain == DomainOverlay(): - if (overlay_result != DomainOverlay() and overlay_result != DomainInvalid() - and self.current_event_data == EventMouseDown() - and not switch_state_mouse_down and overlay_result != self.active_domain): - self.active_domain = overlay_result - self.indicated_domain = self.active_domain - else: - if (self.current_event_data == EventMouseDown() - and not switch_state_mouse_down - and cursor_domain != self.active_domain): - self.active_domain = cursor_domain - self.indicated_domain = self.active_domain - - if switch_state_mouse_down or self.current_event_data == EventMouseDown(): - if self.active_domain == DomainLow(): - Assert(Low(self.current_event_data)) - self.output_event_buffer0 = self.current_event_data - else: - self.output_event_buffer1 = self.current_event_data - else: - if cursor_domain == DomainLow(): - Assert(Low(self.current_event_data)) - self.output_event_buffer0 = self.current_event_data - else: - self.output_event_buffer1 = self.current_event_data - - if self.current_event_data == EventMouseDown(): - switch_state_mouse_down = True - else: - switch_state_mouse_down = False + self.switch_block_1() self.hid_lock.acquire() temp = self.hid.keyboard_available @@ -303,12 +258,101 @@ def input_switch(self) -> None: self.hid_lock.release() if self.active_domain == DomainLow(): - Assert(self.indicated_domain == self.active_domain) - Assert(self.indicated_domain != DomainHigh()) - Assert(Low(self.current_event_data)) self.output_event_buffer0 = self.current_event_data else: self.output_event_buffer1 = self.current_event_data self.current_event_data = EventNone() - self.hid.current_event_type = EventTypeNone() \ No newline at end of file + self.hid.current_event_type = EventTypeNone() + + + def switch_block_1(self) -> None: + Requires(Acc(self.hid, 1 / 4) and Acc(self.hid_lock, 1 / 4) and self.hid_lock.get_locked() is self.hid and Low(self.hid_lock)) + Requires(Acc(self.overlay, 1 / 4) and Acc(self.overlay_lock, 1 / 4) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) + Requires(Acc(self.compositor, 1 / 4) and Acc(self.compositor_lock, 1 / 4) and self.compositor_lock.get_locked() is self.compositor and Low(self.compositor_lock)) + Requires(Acc(self.overlay_result) and Low(self.overlay_result)) + Requires(Acc(self.switch_state_mouse_down) and Low(self.switch_state_mouse_down)) + Requires(Acc(self.current_event_data, 1/2) and Low(self.current_event_data)) + Requires(Acc(self.active_domain) and Low(self.active_domain)) + Requires(Acc(self.indicated_domain) and self.indicated_domain is self.active_domain) + Requires(Acc(self.hid.current_event_type) and Low(self.hid.current_event_type)) + Requires(Acc(self.output_event_buffer0) and Low(self.output_event_buffer0)) + Requires(Acc(self.output_event_buffer1)) + Requires(Acc(self.compositor.cursor_position)) + Ensures(Acc(self.hid, 1 / 4) and Acc(self.hid_lock, 1 / 4)) + Ensures(Acc(self.overlay, 1 / 4) and Acc(self.overlay_lock, 1 / 4)) + Ensures(Acc(self.compositor, 1 / 4) and Acc(self.compositor_lock, 1 / 4)) + Ensures(Acc(self.overlay_result) and Low(self.overlay_result)) + Ensures(Acc(self.switch_state_mouse_down) and Low(self.switch_state_mouse_down)) + Ensures(Acc(self.current_event_data, 1/2)) + Ensures(Acc(self.active_domain) and Low(self.active_domain)) + Ensures(Acc(self.indicated_domain) and self.indicated_domain is self.active_domain) + Ensures(Acc(self.hid.current_event_type) and Low(self.hid.current_event_type)) + Ensures(Acc(self.output_event_buffer0) and Low(self.output_event_buffer0)) + Ensures(Acc(self.output_event_buffer1)) + Ensures(Acc(self.compositor.cursor_position)) + + cursor_domain = DomainInvalid() # type: Domain + self.hid.current_event_type = EventTypeMouse() + self.hid_lock.acquire() + source = self.hid.mouse_source + self.hid_lock.release() + + self.overlay_lock.acquire() + self.overlay.mouse_click_arg = source + self.overlay.mouse_click_call = True + self.overlay_lock.release() + + done_rpc = False + + self.switch_state_mouse_down = False + + while not done_rpc: + Invariant(Acc(self.overlay, 1 / 8) and Acc(self.overlay_lock, 1 / 8) and self.overlay_lock.get_locked() is self.overlay and Low(self.overlay_lock)) + Invariant(Low(done_rpc) and Acc(self.overlay_result) and Low(self.overlay_result)) + self.overlay_lock.acquire() + if not self.overlay.mouse_click_call: + self.overlay_result = self.overlay.mouse_click_ret + done_rpc = True + self.overlay_lock.release() + + if self.overlay_result != DomainInvalid(): + cursor_domain = DomainOverlay() + else: + self.compositor.cursor_position = self.current_event_data + + self.compositor_lock.acquire() + cursor_domain = self.compositor.domain_under_cursor + self.compositor_lock.release() + + if cursor_domain == DomainInvalid(): + cursor_domain = self.active_domain + + if cursor_domain == DomainOverlay(): + if (self.overlay_result != DomainOverlay() and self.overlay_result != DomainInvalid() + and self.current_event_data == EventMouseDown() + and not self.switch_state_mouse_down and self.overlay_result != self.active_domain): + self.active_domain = self.overlay_result + self.indicated_domain = self.active_domain + else: + if (self.current_event_data == EventMouseDown() + and not self.switch_state_mouse_down + and cursor_domain != self.active_domain): + self.active_domain = cursor_domain + self.indicated_domain = self.active_domain + + if self.switch_state_mouse_down or self.current_event_data == EventMouseDown(): + if self.active_domain == DomainLow(): + self.output_event_buffer0 = self.current_event_data + else: + self.output_event_buffer1 = self.current_event_data + else: + if cursor_domain == DomainLow(): + self.output_event_buffer0 = self.current_event_data + else: + self.output_event_buffer1 = self.current_event_data + + if self.current_event_data == EventMouseDown(): + self.switch_state_mouse_down = True + else: + self.switch_state_mouse_down = False \ No newline at end of file diff --git a/tests/sif-prob/verification/examples/no_obligations/secc-ct.py b/tests/sif-prob/verification/examples/no_obligations/secc-ct.py new file mode 100644 index 000000000..b8721aae5 --- /dev/null +++ b/tests/sif-prob/verification/examples/no_obligations/secc-ct.py @@ -0,0 +1,91 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/ +""" + +from nagini_contracts.contracts import * +from typing import List + +@Pure +def abs_choose(c: bool, a: int, b: int) -> int: + if c: + return a + return b + + +def choose_ct(c: bool, a: int, b: int) -> int: + Ensures(Result() == abs_choose(c, a, b)) + return (c * a) + ((1-c) * b) + + +def not_ct(a: bool) -> int: + Ensures(Result() == (not a)) + return 1 - a + + +def max_ct(a: int, b: int) -> int: + Ensures(Result() == (a if a>b else b)) + return choose_ct(a > b, a, b) + + +def min_ct(a: int, b: int) -> int: + Ensures(Result() == (a if a int: + Requires(Acc(list_pred(l1)) and Acc(list_pred(l2))) + Requires(n >= 0 and i >= 0) + Requires(Low(n) and len(l1) == i + n and len(l2) == i + n) + Ensures(Acc(list_pred(l1)) and Acc(list_pred(l2))) + Ensures(ToSeq(l1) is Old(ToSeq(l1)) and ToSeq(l2) is Old(ToSeq(l2))) + Ensures(Result() == (not (ToSeq(l1).drop(i) == ToSeq(l2).drop(i)))) + if n != 0: + a = l1[i] + b = l2[i] + + # Need reference comparison, otherwise list contents are technically not equal. + c = a is not b + d = memcmp_ct(l1, l2, i + 1, n - 1) + m = max_ct(c, d) + return m + else: + return False + +@Pure +def abs_max_list(s: PSeq[int]) -> int: + Requires(len(s) > 0) + if len(s) == 1: + return s[0] + else: + return max(s[0], abs_max_list(s.drop(1))) + + +def max_list(l: List[int], i: int, n: int) -> int: + Requires(Acc(list_pred(l))) + Requires(n > 0 and i >= 0) + Requires(Low(n) and len(l) == i + n) + Ensures(Acc(list_pred(l))) + Ensures(ToSeq(l) is Old(ToSeq(l))) + Ensures(Result() == abs_max_list(ToSeq(l).drop(i))) + + if n == 1: + res = l[i] + return res + else: + m = max_list(l, i + 1, n - 1) + Assert(ToSeq(l).drop(i).drop(1) == ToSeq(l).drop(i + 1)) + res = max_ct(l[i], m) + return res + + +def password_checker(guess: List[int], stored_password: List[int]) -> int: + Requires(Acc(list_pred(guess)) and Acc(list_pred(stored_password))) + Requires(Low(ToSeq(guess) == ToSeq(stored_password))) + Requires(len(stored_password) == len(guess) and Low(len(guess))) + Ensures(Acc(list_pred(guess)) and Acc(list_pred(stored_password))) + Ensures(LowVal(Result())) + + return memcmp_ct(guess, stored_password, 0, len(guess)) diff --git a/tests/sif-prob/verification/test_control_flow.py b/tests/sif-prob/verification/test_control_flow.py new file mode 100644 index 000000000..2b9c01bdd --- /dev/null +++ b/tests/sif-prob/verification/test_control_flow.py @@ -0,0 +1,189 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from typing import List +from nagini_contracts.contracts import * + + +def test_if_fail(i: int) -> int: + res = 12 + #:: ExpectedOutput(probabilistic.sif.violated:high.branch) + if i: + res = 15 + return res + + +def test_if(i: int) -> int: + Requires(Low(i)) + res = 12 + if i: + res = 15 + return res + +# while + +def test_while_fail(n: int) -> int: + i = 0 + #:: ExpectedOutput(probabilistic.sif.violated:high.branch) + while i < n: + i -= 1 + return 12 + + +def test_while(n: int) -> int: + Requires(Low(n)) + i = 0 + while i < n: + Invariant(Low(i)) + i -= 1 + return 12 + +# for + +def test_for_fail(n: int) -> int: + Requires(n > 0) + res = 0 + #:: ExpectedOutput(probabilistic.sif.violated:high.branch) + for i in range(0, n): + res += 1 + return res + + +def test_for(n: int) -> int: + Requires(n > 0) + Requires(Low(n)) + res = 0 + for i in range(0, n): + Invariant(Low(Previous(i))) + res += 1 + return res + +# call receiver + +class Super: + + def foo(self) -> int: + Ensures(Low(Result())) + return 6 + + +class Sub(Super): + + def foo(self) -> int: + Ensures(Low(Result())) + return 6 + + +def test_receiver_fail(s: Super) -> int: + #:: ExpectedOutput(probabilistic.sif.violated:high.receiver.type) + s.foo() + return 5 + + +def test_receiver(s: Super) -> int: + Requires(Low(type(s))) + s.foo() + return 5 + +# exception + + +def test_exception_fail(e: Exception) -> None: + Ensures(True) + Exsures(Exception, True) + #:: ExpectedOutput(probabilistic.sif.violated:high.exception.type) + raise e + + +def test_exception(e: Exception) -> None: + Requires(Low(type(e))) + Ensures(True) + Exsures(Exception, True) + raise e + +# lowevent trivial + +@ContractOnly +def myprint(i: int) -> None: + Requires(Low(i)) + Requires(LowEvent()) + + +def caller(i: int) -> None: + Requires(Low(i)) + myprint(i) + +# and + +def effects() -> int: + Ensures(Low(Result())) + Ensures(Result() is 5) + return 5 + +def test_and_fail(o: int) -> int: + #:: ExpectedOutput(probabilistic.sif.violated:high.short.circuit) + res = o and effects() + return res + +def test_and_allow_in_spec(o: int) -> int: + Ensures(Result() == (o and 5)) + bo = bool(o) + res = ((1-bo) * o) + (bo * 5) + return res + +def test_and(o: int) -> int: + Requires(LowVal(bool(o))) + res = o and effects() + return res + +# or + +def test_or_fail(o: int) -> int: + #:: ExpectedOutput(probabilistic.sif.violated:high.short.circuit) + res = o or effects() + return res + + +def test_or(o: int) -> int: + Requires(LowVal(bool(o))) + res = o or effects() + return res + +# condexp + +def test_condexp_fail(i: int) -> int: + #:: ExpectedOutput(probabilistic.sif.violated:high.branch) + res = 12 if i else effects() + return res + + +def test_condexp(i: int) -> int: + Requires(Low(i)) + res = 12 if i else effects() + return res + + +def test_condexp_allowed_in_spec(i: bool, i2: int, i3: int) -> int: + Ensures(Result() == (i2 if i else i3)) + res = ((i * i2) + ((1-i)) * i3) + return res + + +def test_condexp_allowed_in_contract_func(i: bool, i2: int, i3: int) -> int: + res = ((i * i2) + ((1-i)) * i3) + Assert(res == (i2 if i else i3)) + return res + + +# comprehensions + +def test_comprehension_fail(l: List[int]) -> List[int]: + Requires(Acc(list_pred(l))) + #:: ExpectedOutput(probabilistic.sif.violated:high.comprehension) + return [5+e for e in l] + + +def test_comprehension(l: List[int]) -> List[int]: + Requires(Acc(list_pred(l))) + Requires(Low(len(l))) + return [5+e for e in l] diff --git a/tests/sif/translation/test_lists.py b/tests/sif-true/translation/test_lists.py similarity index 100% rename from tests/sif/translation/test_lists.py rename to tests/sif-true/translation/test_lists.py diff --git a/tests/sif-true/translation/test_lock_1.py b/tests/sif-true/translation/test_lock_1.py new file mode 100644 index 000000000..8e668bef5 --- /dev/null +++ b/tests/sif-true/translation/test_lock_1.py @@ -0,0 +1,25 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.lock import Lock +from nagini_contracts.contracts import * + + +class Cell: + def __init__(self, val: int) -> None: + self.value = val + Ensures(Acc(self.value) and self.value == val) + + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return Acc(self.get_locked().value) and LowVal(self.get_locked().value) + + +def client(lck: CellLock) -> None: + #:: ExpectedOutput(invalid.program:concurrency.in.sif) + lck.acquire() + + diff --git a/tests/sif-true/translation/test_lock_2.py b/tests/sif-true/translation/test_lock_2.py new file mode 100644 index 000000000..a4a55eb2c --- /dev/null +++ b/tests/sif-true/translation/test_lock_2.py @@ -0,0 +1,24 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.lock import Lock +from nagini_contracts.contracts import * + + +class Cell: + def __init__(self, val: int) -> None: + self.value = val + Ensures(Acc(self.value) and self.value == val) + + +class CellLock(Lock[Cell]): + + @Predicate + def invariant(self) -> bool: + return Acc(self.get_locked().value) and LowVal(self.get_locked().value) + + +def client(lck: CellLock) -> None: + #:: ExpectedOutput(invalid.program:concurrency.in.sif) + lck.release() + diff --git a/tests/sif/translation/test_lowevent.py b/tests/sif-true/translation/test_lowevent.py similarity index 100% rename from tests/sif/translation/test_lowevent.py rename to tests/sif-true/translation/test_lowevent.py diff --git a/tests/sif/translation/test_lowexit.py b/tests/sif-true/translation/test_lowexit.py similarity index 100% rename from tests/sif/translation/test_lowexit.py rename to tests/sif-true/translation/test_lowexit.py diff --git a/tests/sif-true/translation/test_threads.py b/tests/sif-true/translation/test_threads.py new file mode 100644 index 000000000..80138e3da --- /dev/null +++ b/tests/sif-true/translation/test_threads.py @@ -0,0 +1,15 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.thread import ( + Thread, MayStart, getArg, getMethod, Joinable, ThreadPost, getOld, arg +) + + +def printTwice(x: int) -> None: + pass + + +def client(t: Thread) -> None: + #:: ExpectedOutput(invalid.program:concurrency.in.sif) + t.start(printTwice) diff --git a/tests/sif/translation/test_while_purity.py b/tests/sif-true/translation/test_while_purity.py similarity index 100% rename from tests/sif/translation/test_while_purity.py rename to tests/sif-true/translation/test_while_purity.py diff --git a/tests/sif/verification/examples/banerjee.py b/tests/sif-true/verification/examples/banerjee.py similarity index 100% rename from tests/sif/verification/examples/banerjee.py rename to tests/sif-true/verification/examples/banerjee.py diff --git a/tests/sif-true/verification/examples/cav2021-fig4.py b/tests/sif-true/verification/examples/cav2021-fig4.py new file mode 100644 index 000000000..7d326152b --- /dev/null +++ b/tests/sif-true/verification/examples/cav2021-fig4.py @@ -0,0 +1,30 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +class A: + + def foo(self, secret: int) -> int: + Ensures(Low(Result())) + return 0 + + +class B(A): + + def foo(self, secret: int) -> int: + Ensures(Low(Result())) + return 1 + + +def main_incorrect(a: A, secret: int) -> int: + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(Low(Result())) + return a.foo(secret) + + +def main_correct(a: A, secret: int) -> int: + Requires(Low(type(a))) + Ensures(Low(Result())) + return a.foo(secret) diff --git a/tests/sif/verification/examples/constanzo.py b/tests/sif-true/verification/examples/constanzo.py similarity index 100% rename from tests/sif/verification/examples/constanzo.py rename to tests/sif-true/verification/examples/constanzo.py diff --git a/tests/sif/verification/examples/darvas.py b/tests/sif-true/verification/examples/darvas.py similarity index 100% rename from tests/sif/verification/examples/darvas.py rename to tests/sif-true/verification/examples/darvas.py diff --git a/tests/sif/verification/examples/example-decl.py b/tests/sif-true/verification/examples/example-decl.py similarity index 100% rename from tests/sif/verification/examples/example-decl.py rename to tests/sif-true/verification/examples/example-decl.py diff --git a/tests/sif/verification/examples/example-term.py b/tests/sif-true/verification/examples/example-term.py similarity index 100% rename from tests/sif/verification/examples/example-term.py rename to tests/sif-true/verification/examples/example-term.py diff --git a/tests/sif/verification/examples/example.py b/tests/sif-true/verification/examples/example.py similarity index 100% rename from tests/sif/verification/examples/example.py rename to tests/sif-true/verification/examples/example.py diff --git a/tests/sif-true/verification/examples/high-references-low-values.py b/tests/sif-true/verification/examples/high-references-low-values.py new file mode 100644 index 000000000..8589f10d4 --- /dev/null +++ b/tests/sif-true/verification/examples/high-references-low-values.py @@ -0,0 +1,21 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +def add_zero_incorrect(i: int, secret: int) -> int: + Requires(Low(i)) + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(Low(Result())) + if secret == 0: + return i + 0 + return i + + +def add_zero_correct(i: int, secret: int) -> int: + Requires(Low(i)) + Ensures(LowVal(Result())) + if secret == 0: + return i + 0 + return i \ No newline at end of file diff --git a/tests/sif-true/verification/examples/high-references.py b/tests/sif-true/verification/examples/high-references.py new file mode 100644 index 000000000..81cd8c87c --- /dev/null +++ b/tests/sif-true/verification/examples/high-references.py @@ -0,0 +1,29 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +def _print(b: bool) -> None: + Requires(Low(b)) + + +def get_object(o: object, v: int) -> object: + Ensures((Result() is not o) if v > 0 else (Result() is o)) + if v > 0: + return object() + return o + + +def main(v: int) -> None: + o1 = object() + o2 = get_object(o1, v) + #:: ExpectedOutput(call.precondition:assertion.false) + _print(o1 is o2) + + +def main_correct(v: int) -> None: + Requires(Low(v > 0)) + o1 = object() + o2 = get_object(o1, v) + _print(o1 is o2) \ No newline at end of file diff --git a/tests/sif/verification/examples/joana-fig1-tl.py b/tests/sif-true/verification/examples/joana-fig1-tl.py similarity index 100% rename from tests/sif/verification/examples/joana-fig1-tl.py rename to tests/sif-true/verification/examples/joana-fig1-tl.py diff --git a/tests/sif/verification/examples/joana-fig13-l.py b/tests/sif-true/verification/examples/joana-fig13-l.py similarity index 100% rename from tests/sif/verification/examples/joana-fig13-l.py rename to tests/sif-true/verification/examples/joana-fig13-l.py diff --git a/tests/sif/verification/examples/joana-fig2-bl.py b/tests/sif-true/verification/examples/joana-fig2-bl.py similarity index 100% rename from tests/sif/verification/examples/joana-fig2-bl.py rename to tests/sif-true/verification/examples/joana-fig2-bl.py diff --git a/tests/sif/verification/examples/joana-fig2-t.py b/tests/sif-true/verification/examples/joana-fig2-t.py similarity index 100% rename from tests/sif/verification/examples/joana-fig2-t.py rename to tests/sif-true/verification/examples/joana-fig2-t.py diff --git a/tests/sif/verification/examples/joana-fig3-bl.py b/tests/sif-true/verification/examples/joana-fig3-bl.py similarity index 100% rename from tests/sif/verification/examples/joana-fig3-bl.py rename to tests/sif-true/verification/examples/joana-fig3-bl.py diff --git a/tests/sif/verification/examples/joana-fig3-br.py b/tests/sif-true/verification/examples/joana-fig3-br.py similarity index 100% rename from tests/sif/verification/examples/joana-fig3-br.py rename to tests/sif-true/verification/examples/joana-fig3-br.py diff --git a/tests/sif/verification/examples/joana-fig3-tl.py b/tests/sif-true/verification/examples/joana-fig3-tl.py similarity index 100% rename from tests/sif/verification/examples/joana-fig3-tl.py rename to tests/sif-true/verification/examples/joana-fig3-tl.py diff --git a/tests/sif/verification/examples/joana-fig3-tr.py b/tests/sif-true/verification/examples/joana-fig3-tr.py similarity index 100% rename from tests/sif/verification/examples/joana-fig3-tr.py rename to tests/sif-true/verification/examples/joana-fig3-tr.py diff --git a/tests/sif/verification/examples/kusters.py b/tests/sif-true/verification/examples/kusters.py similarity index 100% rename from tests/sif/verification/examples/kusters.py rename to tests/sif-true/verification/examples/kusters.py diff --git a/tests/sif/verification/examples/naumann.py b/tests/sif-true/verification/examples/naumann.py similarity index 95% rename from tests/sif/verification/examples/naumann.py rename to tests/sif-true/verification/examples/naumann.py index 2a18759a1..2bb832420 100644 --- a/tests/sif/verification/examples/naumann.py +++ b/tests/sif-true/verification/examples/naumann.py @@ -32,7 +32,6 @@ def m(x: int, secret: int, l: List[Node]) -> None: Invariant(Low(i)) Invariant(Forall(cast(NodeList, l), lambda e: Acc(e.val))) Invariant(Low(x)) - # TODO: this is unfortunate, it should not be necessary Invariant(Forall(int, lambda k: (Implies(k >= 0 and k < i, l[k] in l and l[k].val is x), [[l[k]]]))) Invariant(Forall(int, lambda k: (Implies(k >= 0 and k < i, l[k] in l and Low(l[k].val)), [[l[k]]]))) assert l[i] in l diff --git a/tests/sif-true/verification/examples/no_obligations/secc-db.py b/tests/sif-true/verification/examples/no_obligations/secc-db.py new file mode 100644 index 000000000..46680f3ff --- /dev/null +++ b/tests/sif-true/verification/examples/no_obligations/secc-db.py @@ -0,0 +1,131 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/ +""" + +from nagini_contracts.contracts import * +from typing import List, Tuple + + +class Elem: + def __init__(self, key: int, value: int) -> None: + self.key = key + self.value = value + + +SUCCESS = 0 +FAILURE = 1 + + +def lookup(elems: List[Elem], key: int) -> Tuple[int, int]: + Requires(Acc(list_pred(elems))) + Requires(Low(len(elems)) and Low(key)) + Requires(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Acc(list_pred(elems))) + Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Implies(Result()[0] == SUCCESS, Low(Result()[1]))) + Ensures(Implies(Result()[0] == FAILURE, Result()[1] == -1)) + Ensures(Result()[0] == SUCCESS or Result()[0] == FAILURE) + + i = 0 + while i < len(elems): + Invariant(Acc(list_pred(elems)) and Low(len(elems))) + Invariant(Low(i) and LowExit()) + Invariant(i >= 0 and i <= len(elems)) + Invariant(Forall(int, lambda j: (Implies(j >= 0 and j < len(elems), Acc(elems[j].key) and Acc(elems[j].value) and Low(elems[j].key) and Implies(elems[j].key is key, Low(elems[j].value))), [[elems[j]]]))) + + if elems[i].key is key: + return (SUCCESS, elems[i].value) + i += 1 + return (FAILURE, -1) + + +def binsearch(elems: List[Elem], from_: int, l: int, key: int) -> Tuple[int, int]: + Requires(Acc(list_pred(elems))) + Requires(Low(l) and Low(key) and Low(from_)) + Requires(0 <= from_ and from_ + l <= len(elems)) + Requires(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Acc(list_pred(elems))) + Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Implies(Result()[0] == SUCCESS, Low(Result()[1]))) + Ensures(Implies(Result()[0] == FAILURE, Result()[1] == -1)) + Ensures(Result()[0] == SUCCESS or Result()[0] == FAILURE) + + if l <= 0: + return FAILURE, -1 + + mid = l // 2 + + e = elems[from_ + mid] + k = e.key + if k is key: + return SUCCESS, elems[from_ + mid].value + else: + if l == 1: + return FAILURE, -1 + if k > key: + return binsearch(elems, from_, mid - 1, key) + else: + return binsearch(elems, from_ + mid + 1, l - (mid + 1), key) + + +def sum_all(elems: List[Elem], key: int) -> int: + Requires(Acc(list_pred(elems))) + Requires(Low(len(elems)) and Low(key)) + Requires(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Acc(list_pred(elems))) + Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Low(Result())) + + sum = 0 + i = 0 + while i < len(elems): + Invariant(Acc(list_pred(elems)) and Low(len(elems))) + Invariant(i >= 0 and i <= len(elems)) + Invariant(Low(sum) and Low(i)) + Invariant(Forall(int, lambda j: (Implies(j >= 0 and j < len(elems), Acc(elems[j].key) and Acc(elems[j].value) and Low(elems[j].key) and Implies(elems[j].key is key, Low(elems[j].value))), [[elems[j]]]))) + + if elems[i].key is key: + sum += elems[i].value + i += 1 + return sum + + +def sum_all_rec(elems: List[Elem], from_: int, l: int, key: int, init: int) -> int: + Requires(Acc(list_pred(elems))) + Requires(Low(l) and Low(key) and Low(from_) and Low(init)) + Requires(0 <= from_ and from_ + l <= len(elems)) + Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))))) + Ensures(Acc(list_pred(elems))) + Ensures(Forall(int, lambda i: Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))))) + Ensures(Low(Result())) + + if l > 0: + e = elems[from_] + if e.key is key: + return sum_all_rec(elems, from_ + 1, l - 1, key, init + e.value) + else: + return sum_all_rec(elems, from_ + 1, l - 1, key, init) + else: + return init + + +def remove_all(elems: List[Elem], key: int) -> None: + Requires(Acc(list_pred(elems))) + Requires(Low(len(elems)) and Low(key)) + Requires(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + Ensures(Acc(list_pred(elems))) + Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(elems), Acc(elems[i].key) and Acc(elems[i].value) and Low(elems[i].key) and Implies(elems[i].key is key, Low(elems[i].value))), [[elems[i]]]))) + + i = 0 + while i < len(elems): + Invariant(Acc(list_pred(elems)) and Low(len(elems))) + Invariant(i >= 0 and i <= len(elems)) + Invariant(Low(i)) + Invariant(Forall(int, lambda j: (Implies(j >= 0 and j < len(elems), Acc(elems[j].key) and Acc(elems[j].value) and Low(elems[j].key) and Implies(elems[j].key is key, Low(elems[j].value))), [[elems[j]]]))) + + if elems[i].key is key: + elems[i].value = 0 + i += 1 diff --git a/tests/sif-true/verification/examples/no_obligations/secc-encrypt.py b/tests/sif-true/verification/examples/no_obligations/secc-encrypt.py new file mode 100644 index 000000000..eeb5cfe5f --- /dev/null +++ b/tests/sif-true/verification/examples/no_obligations/secc-encrypt.py @@ -0,0 +1,42 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +""" +Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/ +""" + +from nagini_contracts.contracts import * +from typing import List + + +def encrypt(cipher: List[int], plain: int, key: int) -> bool: + Requires(list_pred(cipher) and len(cipher) == 0) + Ensures(list_pred(cipher) and len(cipher) == 1) + Ensures(Low(Result())) + Ensures(Implies(not Result(), Low(cipher[0]))) + cipher.append(plain + key) + Declassify(plain + key) + return False + + +def decrypt(plain: List[int], cipher: int, key: int) -> bool: + Requires(Low(cipher)) + Requires(list_pred(plain) and len(plain) == 1) + Ensures(list_pred(plain) and len(plain) == 1) + Ensures(Implies(Result(), Low(plain[0]))) + Ensures(Low(Result())) + plain[0] = cipher - key + return False + + +def secure(plaintext: int, key: int) -> int: + Ensures(Low(Result())) + ciphertext = [] # type: List[int] + res = encrypt(ciphertext, plaintext, key) + if res: + ciphertext[0] = 0 + else: + copy = [plaintext] + if decrypt(copy, ciphertext[0], key): + ciphertext = copy + return ciphertext[0] diff --git a/tests/sif/verification/examples/product.py b/tests/sif-true/verification/examples/product.py similarity index 100% rename from tests/sif/verification/examples/product.py rename to tests/sif-true/verification/examples/product.py diff --git a/tests/sif/verification/examples/smith.py b/tests/sif-true/verification/examples/smith.py similarity index 100% rename from tests/sif/verification/examples/smith.py rename to tests/sif-true/verification/examples/smith.py diff --git a/tests/sif/verification/examples/terauchi-fig1.py b/tests/sif-true/verification/examples/terauchi-fig1.py similarity index 100% rename from tests/sif/verification/examples/terauchi-fig1.py rename to tests/sif-true/verification/examples/terauchi-fig1.py diff --git a/tests/sif/verification/examples/terauchi-fig3.py b/tests/sif-true/verification/examples/terauchi-fig3.py similarity index 100% rename from tests/sif/verification/examples/terauchi-fig3.py rename to tests/sif-true/verification/examples/terauchi-fig3.py diff --git a/tests/sif/verification/examples/terauchi-fig4.py b/tests/sif-true/verification/examples/terauchi-fig4.py similarity index 100% rename from tests/sif/verification/examples/terauchi-fig4.py rename to tests/sif-true/verification/examples/terauchi-fig4.py diff --git a/tests/sif/verification/resources/__init__.py b/tests/sif-true/verification/resources/__init__.py similarity index 100% rename from tests/sif/verification/resources/__init__.py rename to tests/sif-true/verification/resources/__init__.py diff --git a/tests/sif/verification/resources/sif_utils.py b/tests/sif-true/verification/resources/sif_utils.py similarity index 100% rename from tests/sif/verification/resources/sif_utils.py rename to tests/sif-true/verification/resources/sif_utils.py diff --git a/tests/sif/verification/test_ctrl_flow.py b/tests/sif-true/verification/test_ctrl_flow.py similarity index 100% rename from tests/sif/verification/test_ctrl_flow.py rename to tests/sif-true/verification/test_ctrl_flow.py diff --git a/tests/sif/verification/test_dyn_calls.py b/tests/sif-true/verification/test_dyn_calls.py similarity index 100% rename from tests/sif/verification/test_dyn_calls.py rename to tests/sif-true/verification/test_dyn_calls.py diff --git a/tests/sif/verification/test_exception_loop.py b/tests/sif-true/verification/test_exception_loop.py similarity index 100% rename from tests/sif/verification/test_exception_loop.py rename to tests/sif-true/verification/test_exception_loop.py diff --git a/tests/sif/verification/test_fields_assign.py b/tests/sif-true/verification/test_fields_assign.py similarity index 100% rename from tests/sif/verification/test_fields_assign.py rename to tests/sif-true/verification/test_fields_assign.py diff --git a/tests/sif/verification/test_functions.py b/tests/sif-true/verification/test_functions.py similarity index 100% rename from tests/sif/verification/test_functions.py rename to tests/sif-true/verification/test_functions.py diff --git a/tests/sif/verification/test_functions_2.py b/tests/sif-true/verification/test_functions_2.py similarity index 100% rename from tests/sif/verification/test_functions_2.py rename to tests/sif-true/verification/test_functions_2.py diff --git a/tests/sif/verification/test_lists.py b/tests/sif-true/verification/test_lists.py similarity index 100% rename from tests/sif/verification/test_lists.py rename to tests/sif-true/verification/test_lists.py diff --git a/tests/sif/verification/test_localvar_assign.py b/tests/sif-true/verification/test_localvar_assign.py similarity index 100% rename from tests/sif/verification/test_localvar_assign.py rename to tests/sif-true/verification/test_localvar_assign.py diff --git a/tests/sif/verification/test_low_annotation.py b/tests/sif-true/verification/test_low_annotation.py similarity index 100% rename from tests/sif/verification/test_low_annotation.py rename to tests/sif-true/verification/test_low_annotation.py diff --git a/tests/sif/verification/test_lowval.py b/tests/sif-true/verification/test_lowval.py similarity index 100% rename from tests/sif/verification/test_lowval.py rename to tests/sif-true/verification/test_lowval.py diff --git a/tests/sif/verification/test_method_calls.py b/tests/sif-true/verification/test_method_calls.py similarity index 100% rename from tests/sif/verification/test_method_calls.py rename to tests/sif-true/verification/test_method_calls.py diff --git a/tests/sif/verification/test_predicates.py b/tests/sif-true/verification/test_predicates.py similarity index 100% rename from tests/sif/verification/test_predicates.py rename to tests/sif-true/verification/test_predicates.py diff --git a/tests/sif/verification/test_return.py b/tests/sif-true/verification/test_return.py similarity index 100% rename from tests/sif/verification/test_return.py rename to tests/sif-true/verification/test_return.py diff --git a/tests/sif/verification/test_sif1.py b/tests/sif-true/verification/test_sif1.py similarity index 100% rename from tests/sif/verification/test_sif1.py rename to tests/sif-true/verification/test_sif1.py diff --git a/tests/sif/verification/test_termination_channels.py b/tests/sif-true/verification/test_termination_channels.py similarity index 100% rename from tests/sif/verification/test_termination_channels.py rename to tests/sif-true/verification/test_termination_channels.py diff --git a/tests/sif/verification/test_try_catch.py b/tests/sif-true/verification/test_try_catch.py similarity index 100% rename from tests/sif/verification/test_try_catch.py rename to tests/sif-true/verification/test_try_catch.py diff --git a/tests/sif/verification/test_try_catch_call.py b/tests/sif-true/verification/test_try_catch_call.py similarity index 100% rename from tests/sif/verification/test_try_catch_call.py rename to tests/sif-true/verification/test_try_catch_call.py diff --git a/tests/sif/verification/test_while.py b/tests/sif-true/verification/test_while.py similarity index 100% rename from tests/sif/verification/test_while.py rename to tests/sif-true/verification/test_while.py diff --git a/tests/sif/verification/test_while_2.py b/tests/sif-true/verification/test_while_2.py similarity index 100% rename from tests/sif/verification/test_while_2.py rename to tests/sif-true/verification/test_while_2.py diff --git a/tests/sif/verification/test_while_3.py b/tests/sif-true/verification/test_while_3.py similarity index 100% rename from tests/sif/verification/test_while_3.py rename to tests/sif-true/verification/test_while_3.py diff --git a/tests/sif/verification/secc/cav2019.py b/tests/sif/verification/secc/cav2019.py deleted file mode 100644 index d3f8d5014..000000000 --- a/tests/sif/verification/secc/cav2019.py +++ /dev/null @@ -1,6 +0,0 @@ - -class Record: - def __init__(self, ic: bool, data: int) -> None: - self.is_classified = ic - self.data = data -