diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py index e816c80a5..2363456a2 100644 --- a/src/nagini_translation/main.py +++ b/src/nagini_translation/main.py @@ -97,7 +97,10 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N path = os.path.abspath(path) error_manager.clear() current_path = os.path.dirname(inspect.stack()[0][1]) - resources_path = os.path.join(current_path, 'resources') + if sif: + preamble_path = os.path.join(current_path, 'sif', 'resources') + else: + preamble_path = os.path.join(current_path, 'resources') if sif: viper_ast = ViperASTExtended(jvm, jvm.java, jvm.scala, jvm.viper, path) @@ -114,7 +117,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N analyzer = Analyzer(types, path, selected) main_module = analyzer.module - with open(os.path.join(resources_path, 'preamble.index'), 'r') as file: + with open(os.path.join(preamble_path, 'preamble.index'), 'r') as file: analyzer.add_native_silver_builtins(json.loads(file.read())) analyzer.initialize_io_analyzer() diff --git a/src/nagini_translation/resources/all.sil b/src/nagini_translation/resources/all.sil index 33ea0ca7e..a61f76d7f 100644 --- a/src/nagini_translation/resources/all.sil +++ b/src/nagini_translation/resources/all.sil @@ -12,10 +12,15 @@ domain SIFDomain[T] { axiom low_true { forall x: T :: {Low(x)} Low(x) } + axiom lowevent_true { + LowEvent() + } + function LowEvent(): Bool } import "bool.sil" +import "references.sil" import "bytes.sil" import "iterator.sil" import "list.sil" diff --git a/src/nagini_translation/resources/backends/silver-sif-extension.jar b/src/nagini_translation/resources/backends/silver-sif-extension.jar index 686b75e30..4e38f9859 100644 Binary files a/src/nagini_translation/resources/backends/silver-sif-extension.jar and b/src/nagini_translation/resources/backends/silver-sif-extension.jar differ diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index bc0daa373..2aefc63b8 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -18,10 +18,6 @@ function NoneType___bool__(self: Ref) : Bool decreases _ ensures self == null ==> !result -function object___str__(self: Ref) : Ref - decreases _ - ensures issubtype(typeof(result), str()) - function bool___bool__(self: Ref) : Bool decreases _ requires self != null ==> issubtype(typeof(self), bool()) @@ -258,4 +254,6 @@ function abs(a: Int): Int decreases _ ensures result == (a >= 0 ? a : -a) -method print(r: Ref) \ No newline at end of file +method print(r: Ref) + requires Low(r) + requires LowEvent() \ No newline at end of file diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index index be03978a7..476adc66b 100644 --- a/src/nagini_translation/resources/preamble.index +++ b/src/nagini_translation/resources/preamble.index @@ -542,7 +542,8 @@ }, "__len__": { "args": ["tuple"], - "type": "__prim__int" + "type": "__prim__int", + "requires": ["__val__", "args"] }, "__val__": { "args": ["tuple"], diff --git a/src/nagini_translation/resources/references.sil b/src/nagini_translation/resources/references.sil new file mode 100644 index 000000000..bd944557b --- /dev/null +++ b/src/nagini_translation/resources/references.sil @@ -0,0 +1,11 @@ +/* + * Copyright (c) 2019 ETH Zurich + * This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + + + function object___str__(self: Ref) : Ref + decreases _ + ensures issubtype(typeof(result), str()) \ No newline at end of file diff --git a/src/nagini_translation/sif/resources/all.sil b/src/nagini_translation/sif/resources/all.sil index d5e032e6a..58d47c9de 100644 --- a/src/nagini_translation/sif/resources/all.sil +++ b/src/nagini_translation/sif/resources/all.sil @@ -5,11 +5,15 @@ * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ +import + domain SIFDomain[T] { function Low(x: T): Bool + function LowEvent(): Bool } import "../../resources/bool.sil" +import "references.sil" import "../../resources/bytes.sil" import "../../resources/iterator.sil" import "../../resources/list.sil" diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index new file mode 100644 index 000000000..4f8551d20 --- /dev/null +++ b/src/nagini_translation/sif/resources/preamble.index @@ -0,0 +1,897 @@ +{ +"object": { + "functions": { + "__bool__": { + "args": ["object"], + "type": "__prim__bool", + "requires": ["list", "list_arg", "set", "set_arg", "dict", "dict_arg"] + }, + "__eq__": { + "args": ["object", "object"], + "type": "__prim__bool" + }, + "__cast__": { + "args": ["type", "object"], + "type": "object" + } + }, + "methods": { + "__str__": { + "args": ["object"], + "type": "str", + "MustTerminate": true + } + } +}, +"list": { + "methods": { + "__init__": { + "args": [], + "type": null, + "MustTerminate": true + }, + "append": { + "args": ["list", "object"], + "type": null, + "requires": ["__sil_seq__"], + "MustTerminate": true + }, + "extend": { + "args": ["list", "list"], + "type": null, + "MustTerminate": true + }, + "reverse": { + "args": ["list"], + "type": "list", + "MustTerminate": true + }, + "__setitem__": { + "args": ["list", "__prim__int", "object"], + "type": null, + "MustTerminate": true, + "requires": ["__len__"] + }, + "__iter__": { + "args": ["list"], + "type": "Iterator", + "MustTerminate": true + }, + "__getitem_slice__": { + "args": ["list", "slice"], + "type": "list", + "display_name": "__getitem__", + "requires": ["__len__", "slice___start__", "slice___stop__"], + "MustTerminate": true + }, + "__add__": { + "args": ["list", "list"], + "type": "list", + "MustTerminate": true + }, + "__mul__": { + "args": ["list", "__prim__int"], + "type": "list", + "MustTerminate": true + } + }, + "functions": { + "__getitem__": { + "args": ["list", "int"], + "type": "object", + "requires": ["__len__"] + }, + "__contains__": { + "args": ["list", "object"], + "type": "__prim__bool" + }, + "__len__": { + "args": ["list"], + "type": "__prim__int" + }, + "__bool__": { + "args": ["list"], + "type": "__prim__bool" + }, + "__sil_seq__": { + "args": ["list"], + "type": "__prim__Seq" + } + }, + "type_vars": 1, + "extends": "object", + "generate_sif": true +}, +"set":{ + "methods": { + "__init__": { + "args": [], + "type": null, + "MustTerminate": true + }, + "add": { + "args": ["set", "object"], + "type": null, + "MustTerminate": true + }, + "remove": { + "args": ["set", "object"], + "type": null, + "MustTerminate": true + }, + "clear": { + "args": ["set"], + "type": null, + "MustTerminate": true + }, + "__iter__": { + "args": ["set"], + "type": "Iterator", + "MustTerminate": true, + "requires": ["__sil_seq__"] + } + }, + "functions": { + "__contains__": { + "args": ["dict", "object"], + "type": "__prim__bool" + }, + "__bool__": { + "args": ["set"], + "type": "__prim__bool" + }, + "__len__": { + "args": ["set"], + "type": "__prim__int" + }, + "__sil_seq__": { + "args": ["set"], + "type": "__prim__Seq" + } + }, + "type_vars": 1, + "extends": "object" +}, +"dict": { + "methods": { + "__init__": { + "args": [], + "type": null, + "MustTerminate": true + }, + "keys": { + "args": ["dict"], + "type": "set", + "MustTerminate": true + }, + "__setitem__": { + "args": ["dict", "object", "object"], + "type": null, + "MustTerminate": true, + "requires": ["__getitem__", "__contains__"] + }, + "__iter__": { + "args": ["dict"], + "type": "Iterator", + "MustTerminate": true, + "requires": ["__sil_seq__"] + }, + "values": { + "args": ["dict"], + "type": "list", + "MustTerminate": true, + "requires": ["__contains__", "__getitem__"] + } + }, + "functions": { + "__contains__": { + "args": ["dict", "object"], + "type": "__prim__bool" + }, + "__getitem__": { + "args": ["dict", "object"], + "type": "object", + "requires": ["__contains__"] + }, + "get": { + "args": ["dict", "object"], + "type": "object", + "generic_type": 1, + "requires": ["__contains__", "__getitem__"] + }, + "__bool__": { + "args": ["dict"], + "type": "__prim__bool" + }, + "__len__": { + "args": ["dict"], + "type": "__prim__int" + }, + "__sil_seq__": { + "args": ["dict"], + "type": "__prim__Seq" + } + }, + "type_vars": 2, + "extends": "object" +}, +"int": { + "functions": { + "__bool__": { + "args": ["int"], + "type": "__prim__bool" + }, + "__unbox__": { + "args": ["int"], + "type": "__prim__int", + "requires": ["__prim__int___box__", "__prim__bool___box__"] + }, + "__eq__": { + "args": ["int", "object"], + "type": "__prim__bool", + "requires": ["__unbox__"] + }, + "__add__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__int" + }, + "__sub__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__int", + "requires": ["__unbox__"] + }, + "__mul__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__int" + }, + "__div__": { + "args": ["__prim__int", "__prim__int"], + "type": "float" + }, + "__floordiv__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__int" + }, + "__mod__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__int" + }, + "__ge__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__bool" + }, + "__gt__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__bool" + }, + "__lt__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__bool" + }, + "__le__": { + "args": ["__prim__int", "__prim__int"], + "type": "__prim__bool" + }, + "__int__": { + "args": ["int"], + "type": "int" + } + }, + "extends": "float" +}, +"float": { + "functions": { + "__create__": { + "args": ["__prim__int"], + "type": "float" + }, + "__bool__": { + "args": ["float"], + "type": "__prim__bool", + "requires": ["int___bool__", "int___unbox__"] + }, + "__eq__": { + "args": ["float", "object"], + "type": "__prim__bool", + "requires": ["int___eq__"] + }, + "__add__": { + "args": ["float", "float"], + "type": "float", + "requires": ["int___add__", "int___unbox__"] + }, + "__sub__": { + "args": ["float", "float"], + "type": "float", + "requires": ["int___sub__", "int___unbox__"] + }, + "__mul__": { + "args": ["float", "float"], + "type": "float", + "requires": ["int___mul__", "int___unbox__"] + }, + "__div__": { + "args": ["float", "float"], + "type": "float", + "requires": ["int___div__", "int___unbox__"] + }, + "__ge__": { + "args": ["float", "float"], + "type": "__prim__bool", + "requires": ["int___ge__", "int___unbox__"] + }, + "__gt__": { + "args": ["float", "float"], + "type": "__prim__bool", + "requires": ["int___gt__", "int___unbox__"] + }, + "__lt__": { + "args": ["float", "float"], + "type": "__prim__bool", + "requires": ["int___lt__", "int___unbox__"] + }, + "__le__": { + "args": ["float", "float"], + "type": "__prim__bool", + "requires": ["int___le__", "int___unbox__"] + }, + "__int__": { + "args": ["float"], + "type": "int" + } + }, + "extends": "object" +}, +"bool": { + "functions": { + "__unbox__": { + "args": ["bool"], + "type": "__prim__bool", + "requires": ["__prim__bool___box__"] + }, + "__bool__": { + "args": ["bool"], + "type": "__prim__bool" + }, + "__eq__": { + "args": ["bool", "object"], + "type": "__prim__bool", + "requires": ["__unbox__"] + } + }, + "extends": "int" +}, +"NoneType": { + "functions": { + "__bool__": { + "args": ["object"], + "type": "__prim__bool" + } + }, + "extends": "object" +}, +"Exception": { + "extends": "object" +}, +"ConnectionRefusedError": { + "extends": "Exception" +}, +"traceback": { + "extends": "object" +}, +"str": { + "functions": { + "__len__": { + "args": ["str"], + "type": "__prim__int" + }, + "__bool__": { + "args": ["str"], + "type": "__prim__bool", + "requires": ["__len__"] + }, + "__eq__": { + "args": ["str", "object"], + "type": "__prim__bool" + }, + "__add__": { + "args": ["str", "str"], + "type": "str" + }, + "__create__": { + "args": ["__prim__int", "__prim__int"], + "type": "str", + "requires": ["__len__", "__val__"] + }, + "__val__": { + "args": ["str"], + "type": "int" + }, + "join": { + "args": ["str", "list"], + "type": "str" + }, + "__mod__": { + "args": ["str", "tuple"], + "type": "str" + } + }, + "methods": { + "split": { + "args": ["str"], + "type": "list", + "MustTerminate": true + } + }, + "extends": "object" +}, +"bytes": { + "functions": { + "__len__": { + "args": ["bytes"], + "type": "__prim__int", + "requires": ["__val__"] + }, + "__bool__": { + "args": ["bytes"], + "type": "__prim__bool", + "requires": ["__len__"] + }, + "__eq__": { + "args": ["bytes", "object"], + "type": "__prim__bool", + "requires": ["__val__", "__len__"] + }, + "__add__": { + "args": ["bytes", "bytes"], + "type": "bytes", + "requires": ["__val__", "__len__"] + }, + "__mul__": { + "args": ["bytes", "__prim__int"], + "type": "bytes", + "requires": ["__val__", "__len__", "bytes___mul__helper"] + }, + "__sil_seq__": { + "args": ["bytes"], + "type": "__prim__Seq", + "requires": ["__val__"] + }, + "__create__": { + "args": ["__prim__Seq", "__prim__int"], + "type": "bytes", + "requires": ["__len__", "__val__"] + }, + "__val__": { + "args": ["bytes"], + "type": "__prim__Seq" + }, + "__getitem_slice__": { + "args": ["bytes", "slice"], + "type": "int", + "display_name": "__getitem__", + "requires": ["__len__", "__val__", "slice___start__", "slice___stop__"] + }, + "__getitem__": { + "args": ["bytes", "__prim__int"], + "type": "int", + "requires": ["__len__", "__val__"] + }, + "join": { + "args": ["bytes", "list"], + "type": "bytes", + "requires": ["__val__", "__len__", "bytes_join_val_helper", "list___len__", "list___getitem__"] + } + }, + "extends": "object" +}, +"tuple": { + "functions": { + "__create0__": { + "args": [], + "type": "tuple", + "requires": ["__val__", "__len__"] + }, + "__create__": { + "args": ["__prim__Seq", "__prim__Seq_type", "__prim__int"], + "type": "tuple", + "requires": ["__val__", "__len__"] + }, + "__create1__": { + "args": ["object", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__create2__": { + "args": ["object", "object", "type", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__create3__": { + "args": ["object", "object", "object", "type", "type", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__create4__": { + "args": ["object", "object", "object", "object", "type", "type", "type", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__create5__": { + "args": ["object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__create6__": { + "args": ["object", "object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "type", "__prim__int"], + "type": "tuple", + "requires": ["__len__", "__getitem__"] + }, + "__getitem__": { + "args": ["tuple", "__prim__int"], + "type": "object", + "requires": ["__len__", "__val__", "__len__"] + }, + "__getitem_slice__": { + "args": ["tuple", "slice"], + "type": "object", + "display_name": "__getitem__", + "requires": ["__len__", "__getitem__", "__val__", "slice___start__", "slice___stop__"] + }, + "__contains__": { + "args": ["tuple", "object"], + "type": "__prim__bool", + "requires": ["__val__"] + }, + "__len__": { + "args": ["tuple"], + "type": "__prim__int", + "requires": ["__val__", "args"] + }, + "__val__": { + "args": ["tuple"], + "type": "__prim__Seq" + }, + "__eq__": { + "args": ["tuple", "object"], + "type": "__prim__bool", + "requires": ["__len__", "__getitem__"] + }, + "__sil_seq__": { + "args": ["tuple"], + "type": "__prim__Seq", + "requires": ["__len__", "__val__"] + } + }, + "type_vars": -1, + "extends": "object" +}, +"__prim__int": { + "functions": { + "__box__": { + "args": ["__prim__int"], + "type": "int", + "requires": ["int___unbox__"] + } + } +}, +"__prim__bool": { + "functions": { + "__box__": { + "args": ["__prim__bool"], + "type": "bool", + "requires": ["bool___unbox__", "int___unbox__"] + } + } +}, +"__prim__Seq": {}, +"__prim__Set": {}, +"__prim__Multiset": {}, +"PSeq": { + "functions": { + "__create__": { + "args": ["__prim__Seq", "type"], + "type": "PSeq", + "requires": ["__sil_seq__"] + }, + "__unbox__": { + "args": ["PSeq"], + "type": "__prim__Seq", + "requires": [] + }, + "__contains__": { + "args": ["PSeq", "object"], + "type": "__prim__bool", + "requires": ["__sil_seq__"] + }, + "__getitem__": { + "args": ["PSeq", "int"], + "type": "object", + "requires": ["__sil_seq__", "__len__", "int___unbox__"] + }, + "__sil_seq__": { + "args": ["PSeq"], + "type": "__prim__Seq" + }, + "__len__": { + "args": ["PSeq"], + "type": "__prim__int", + "requires": ["__sil_seq__"] + }, + "take": { + "args": ["PSeq", "__prim__int"], + "type": "PSeq", + "generic_type": -2, + "requires": ["__sil_seq__", "__create__"] + }, + "drop": { + "args": ["PSeq", "__prim__int"], + "type": "PSeq", + "generic_type": -2, + "requires": ["__sil_seq__", "__create__"] + }, + "update": { + "args": ["PSeq", "__prim__int", "object"], + "type": "PSeq", + "requires": ["__sil_seq__", "__create__"] + }, + "__add__": { + "args": ["PSeq", "PSeq"], + "type": "PSeq", + "requires": ["__sil_seq__", "__create__"] + }, + "__eq__": { + "args": ["PSeq", "PSeq"], + "type": "__prim__bool", + "requires": ["__sil_seq__"] + } + }, + "type_vars": 1, + "extends": "object" +}, +"PSet": { + "functions": { + "__create__": { + "args": ["__prim__Set", "type"], + "type": "PSet", + "requires": ["__unbox__"] + }, + "__unbox__": { + "args": ["PSet"], + "type": "__prim__Set", + "requires": [] + }, + "__contains__": { + "args": ["PSet", "object"], + "type": "__prim__bool", + "requires": ["__unbox__"] + }, + "__sil_seq__": { + "args": ["PSet"], + "type": "__prim__Seq", + "requires": ["__unbox__"] + }, + "__len__": { + "args": ["PSet"], + "type": "__prim__int", + "requires": ["__unbox__"] + }, + "__add__": { + "args": ["PSet", "PSet"], + "type": "PSet", + "requires": ["__unbox__", "__create__"] + }, + "__sub__": { + "args": ["PSet", "PSet"], + "type": "PSet", + "requires": ["__unbox__", "__create__"] + }, + "__eq__": { + "args": ["PSet", "PSet"], + "type": "__prim__bool", + "requires": ["__unbox__"] + } + }, + "type_vars": 1, + "extends": "object" +}, +"PMultiset": { + "functions": { + "__create__": { + "args": ["__prim__Multiset", "type"], + "type": "PMultiset", + "requires": ["__unbox__"] + }, + "__unbox__": { + "args": ["PMultiset"], + "type": "__prim__Multiset", + "requires": [] + }, + "num": { + "args": ["PMultiset", "object"], + "type": "__prim__int", + "requires": ["__unbox__"] + }, + "__sil_seq__": { + "args": ["PMultiset"], + "type": "__prim__Seq", + "requires": ["__unbox__"] + }, + "__len__": { + "args": ["PMultiset"], + "type": "__prim__int", + "requires": ["__unbox__"] + }, + "__add__": { + "args": ["PMultiset", "PMultiset"], + "type": "PMultiset", + "requires": ["__unbox__", "__create__"] + }, + "__sub__": { + "args": ["PMultiset", "PMultiset"], + "type": "PMultiset", + "requires": ["__unbox__", "__create__"] + }, + "__eq__": { + "args": ["PMultiset", "PMultiset"], + "type": "__prim__bool", + "requires": ["__unbox__"] + } + }, + "type_vars": 1, + "extends": "object" +}, +"slice": { + "functions": { + "__create__": { + "args": ["int", "int"], + "type": "slice", + "requires": ["__internal_start__", "__internal_stop__"] + }, + "__internal_start__": { + "args": ["slice"], + "type": "int" + }, + "__internal_stop__": { + "args": ["slice"], + "type": "int" + }, + "__start__": { + "args": ["slice"], + "type": "int", + "requires": ["__internal_start__"] + }, + "__stop__": { + "args": ["slice"], + "type": "int", + "requires": ["__internal_stop__"] + } + }, + "extends": "object" +}, +"range": { + "functions": { + "__create__": { + "args": ["__prim__int", "__prim__int", "__prim__int"], + "type": "range", + "requires": ["__val__", "__start__", "__stop__"] + }, + "__val__": { + "args": ["range"], + "type": "object" + }, + "__start__": { + "args": ["range"], + "type": "object" + }, + "__stop__": { + "args": ["range"], + "type": "object" + }, + "__getitem__": { + "args": ["range", "__prim__int"], + "type": "__prim__int", + "requires": ["__val__"] + }, + "__getitem_slice__": { + "args": ["range", "slice"], + "type": "range", + "display_name": "__getitem__", + "requires": ["__val__", "int___unbox__", "slice___start__", "slice___stop__"] + }, + "__contains__": { + "args": ["range", "int"], + "type": "__prim__bool", + "requires": ["__sil_seq__"] + }, + "__len__": { + "args": ["range"], + "type": "__prim__int", + "requires": ["__val__"] + }, + "__bool__": { + "args": ["range"], + "type": "__prim__bool" + }, + "__sil_seq__": { + "args": ["range"], + "type": "__prim__Seq", + "requires": ["__val__", "__len__", "__prim__int___box__", "int___unbox__", "__start__", "__stop__"] + }, + "__eq__": { + "args": ["range", "object"], + "type": "__prim__bool", + "requires": ["__val__", "__len__"] + } + }, + "methods": { + "__iter__": { + "args": ["range"], + "type": "Iterator", + "MustTerminate": true + } + }, + "extends": "object" +}, +"Iterator": { + "methods":{ + "__next__": { + "args": ["Iterator"], + "type": "object", + "MustTerminate": true + }, + "__del__": { + "args": ["Iterator"], + "type": null, + "MustTerminate": true + } + }, + "type_vars": 1, + "extends": "object" +}, +"Thread": { + "extends": "object" +}, +"LevelType": { +}, +"type": { + "extends": "object" +}, +"Callable": { + "extends": "object" +}, +"Place": { + "functions": { + "__eq__": { + "args": ["Place", "object"], + "type": "__prim__bool" + } + }, + "extends": "object" +}, +"global": { + "functions": { + "max": { + "args": ["object", "object"], + "type": "__prim__int", + "requires": ["int___unbox__", "list___len__", "list___contains__", "__prim__int___box__"] + }, + "min": { + "args": ["object", "object"], + "type": "__prim__int", + "requires": ["int___unbox__", "list___len__", "list___contains__", "__prim__int___box__"] + }, + "abs": { + "args": ["__prim__int"], + "type": "__prim__int" + } + }, + "methods": { + "print": { + "args": ["object"], + "type": null, + "MustTerminate": true + } + } +} +} diff --git a/src/nagini_translation/sif/resources/references.sil b/src/nagini_translation/sif/resources/references.sil new file mode 100644 index 000000000..a7d894019 --- /dev/null +++ b/src/nagini_translation/sif/resources/references.sil @@ -0,0 +1,10 @@ +/* + * Copyright (c) 2019 ETH Zurich + * This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + + +method object___str__(self: Ref) returns (res: Ref) + ensures issubtype(typeof(res), str()) \ No newline at end of file diff --git a/src/nagini_translation/translators/program.py b/src/nagini_translation/translators/program.py index 0f096f2b6..f2d25da71 100644 --- a/src/nagini_translation/translators/program.py +++ b/src/nagini_translation/translators/program.py @@ -296,6 +296,13 @@ def create_override_check(self, method: PythonMethod, params.append(method.overrides.args[arg].decl) args.append(method.overrides.args[arg].ref()) + if method.overrides.var_arg: + params.append(method.overrides.var_arg.decl) + args.append(method.overrides.var_arg.ref()) + if method.overrides.kw_arg: + params.append(method.overrides.kw_arg.decl) + args.append(method.overrides.kw_arg.ref()) + self.bind_type_vars(method.overrides, ctx) mname = ctx.module.get_fresh_name(method.sil_name + '_override_check') diff --git a/tests/functional/verification/issues/00052.py b/tests/functional/verification/issues/00052.py new file mode 100644 index 000000000..4f5b1fdde --- /dev/null +++ b/tests/functional/verification/issues/00052.py @@ -0,0 +1,62 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from nagini_contracts.contracts import ( + Acc, + Assert, + Requires, + Invariant, + Implies, + Predicate, + Fold, + Ensures, + Unfold, + Unfolding, +) +from nagini_contracts.obligations import * + + +class Tree: + + @Predicate + def valid(self) -> bool: + return (Acc(self.left) and Acc(self.right) and + Acc(self.height, 1/10) and self.height >= 0 and + Implies( + self.left is not None, + self.left.valid() and Acc(self.left.height, 1/10) and + self.left.height == self.height - 1) and + Implies( + self.right is not None, + self.right.valid() and Acc(self.right.height, 1/10) and + self.right.height == self.height - 1) + ) + + def __init__(self, left: 'Tree', right: 'Tree', height: int) -> None: + Requires(left.valid() and Acc(left.height, 1/10) and + left.height == height-1) + Requires(right.valid() and Acc(right.height, 1/10) and + right.height == height-1) + Requires(height >= 0) + Ensures(self.valid()) + self.left = left # type: Tree + self.right = right # type: Tree + self.height = height # type: int + Fold(self.valid()) + + + def work(self, call_height: int) -> None: + Requires(self.valid()) + Requires(call_height >= 0) + Requires(Unfolding(self.valid(), self.height == call_height)) + Requires(MustTerminate(call_height + 1)) + Ensures(self.valid()) + + if call_height > 0: + Unfold(self.valid()) + if self.left is not None: + self.left.work(call_height - 1) + if self.right is not None: + self.right.work(call_height - 1) + Fold(self.valid()) \ No newline at end of file diff --git a/tests/functional/verification/issues/00074.py b/tests/functional/verification/issues/00074.py new file mode 100644 index 000000000..ab5ffc9cc --- /dev/null +++ b/tests/functional/verification/issues/00074.py @@ -0,0 +1,48 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from typing import Tuple, Dict +from nagini_contracts.contracts import Requires, Ensures, Result + +class Super: + + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 3) + #:: ExpectedOutput(postcondition.violated:assertion.false,L1) + Ensures(Result() > 2) + return 5 + + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 3) + #:: ExpectedOutput(postcondition.violated:assertion.false,L2) + Ensures(Result() > 2) + return 5 + + +class Sub(Super): + + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 2) + Ensures(Result() > 4) + return 5 + + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 2) + Ensures(Result() > 4) + return 5 + + +class Sub2(Super): + + #:: Label(L1) + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 2) + Ensures(Result() > 0) + return 5 + + #:: Label(L2) + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 2) + Ensures(Result() > 0) + return 5 diff --git a/tests/functional/verification/issues/00119.py b/tests/functional/verification/issues/00119.py new file mode 100644 index 000000000..7ec3b7c20 --- /dev/null +++ b/tests/functional/verification/issues/00119.py @@ -0,0 +1,18 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + +class A: + def __init__(self, value: int) -> None: + self.value = value # type: int + Ensures(Acc(self.value) and self.value is value) + + +def test() -> None: + Assert(A(5).value == 5) + + +def test2() -> None: + #:: ExpectedOutput(assert.failed:assertion.false) + Assert(A(3).value == 5) \ No newline at end of file diff --git a/tests/functional/verification/issues/00150.py b/tests/functional/verification/issues/00150.py new file mode 100644 index 000000000..019de2af5 --- /dev/null +++ b/tests/functional/verification/issues/00150.py @@ -0,0 +1,31 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from typing import Optional, List, Tuple +from nagini_contracts.contracts import * + +class Node: + def __init__(self, function_name: str, children:List['Node']) -> None: + self.function_name = function_name # type: str + self.children = children # type: List['Node'] + Ensures(Acc(self.function_name) and self.function_name is function_name and + Acc(self.children) and self.children is children) + +@Pure +def can_node_be_compressed(marked_execution_tree: 'Node') -> int: + """Searches for the longest compression possible. Returns: + - int: number of nodes that can be compressed. 0 if None""" + Requires(Acc(marked_execution_tree.children)) + Requires(Acc(list_pred(marked_execution_tree.children))) + Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children), + Acc(marked_execution_tree.children[i].function_name)))) + Requires(Acc(marked_execution_tree.function_name)) + #:: ExpectedOutput(postcondition.violated:assertion.false) + Ensures(Implies(len(marked_execution_tree.children) != 1, Result() == 0)) + Ensures(Result() == 0) + if len(marked_execution_tree.children) != 1: + return 1 + if marked_execution_tree.children[0].function_name != marked_execution_tree.function_name: + return 0 + return can_node_be_compressed(marked_execution_tree.children[0]) + 1 \ No newline at end of file diff --git a/tests/functional/verification/test_print.py b/tests/functional/verification/test_print.py new file mode 100644 index 000000000..88fb85d05 --- /dev/null +++ b/tests/functional/verification/test_print.py @@ -0,0 +1,25 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +def foo(i: int) -> None: + Requires(LowEvent()) + print(i) + + +def foo2(i: int) -> None: + print(6) + + +class MyObject(object): + pass + + +def test(x: int) -> None: + Requires(LowEvent()) + if x > 0: + m1 = MyObject() + m2 = MyObject() + print(str(m2)) diff --git a/tests/sif-true/verification/test_print.py b/tests/sif-true/verification/test_print.py new file mode 100644 index 000000000..d740e2a4f --- /dev/null +++ b/tests/sif-true/verification/test_print.py @@ -0,0 +1,28 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + + +def foo(i: int) -> None: + Requires(LowEvent()) + #:: ExpectedOutput(call.precondition:assertion.false) + print(i) + + +def foo2(i: int) -> None: + #:: ExpectedOutput(call.precondition:assertion.false) + print(6) + + +class MyObject(object): + pass + + +def test(x: int) -> None: + Requires(LowEvent()) + if x > 0: + m1 = MyObject() + m2 = MyObject() + #:: ExpectedOutput(call.precondition:assertion.false) + print(str(m2))