Merge pull request #209 from marcoeilers/update_sif_preamble

Rename preamble file and update SIF preamble
marcoeilers · Oct 6, 2024 · 1ebcdba · 1ebcdba
2 parents 93ee907 + 193990c
commit 1ebcdba
Show file tree

Hide file tree

Showing 5 changed files with 78 additions and 10 deletions.
diff --git a/setup.py b/setup.py
@@ -17,7 +17,7 @@
         packages=find_packages('src'),
         package_dir={'': 'src'},
         package_data={
-            '': ['*.sil', '*.index', '*.typed'],
+            '': ['*.sil', '*.json', '*.typed'],
             'nagini_translation.resources': ['backends/*.jar']
         },
         requires=[

diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py
@@ -114,9 +114,9 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
     error_manager.clear()
     current_path = os.path.dirname(inspect.stack()[0][1])
     if sif:
-        preamble_path = os.path.join(current_path, 'sif', 'resources')
+        builtins_index_path = os.path.join(current_path, 'sif', 'resources')
     else:
-        preamble_path = os.path.join(current_path, 'resources')
+        builtins_index_path = os.path.join(current_path, 'resources')
 
     if sif:
         viper_ast = ViperASTExtended(jvm, jvm.java, jvm.scala, jvm.viper, path)
@@ -133,7 +133,7 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
 
     analyzer = Analyzer(types, path, selected)
     main_module = analyzer.module
-    with open(os.path.join(preamble_path, 'preamble.index'), 'r') as file:
+    with open(os.path.join(builtins_index_path, 'builtins.json'), 'r') as file:
         analyzer.add_native_silver_builtins(json.loads(file.read()))
 
     analyzer.initialize_io_analyzer()

diff --git a/...gini_translation/resources/preamble.index → ...agini_translation/resources/builtins.json b/...gini_translation/resources/preamble.index → ...agini_translation/resources/builtins.json
diff --git a/..._translation/sif/resources/preamble.index → ...i_translation/sif/resources/builtins.json b/..._translation/sif/resources/preamble.index → ...i_translation/sif/resources/builtins.json
@@ -50,7 +50,7 @@
             "args": ["list", "__prim__int", "object"],
             "type": null,
             "MustTerminate": true,
-            "requires": ["__len__"]
+            "requires": ["__len__", "__getitem__"]
         },
         "__iter__": {
             "args": ["list"],
@@ -79,7 +79,7 @@
         "__getitem__": {
             "args": ["list", "int"],
             "type": "object",
-            "requires": ["__len__"]
+            "requires": ["__len__", "int___unbox__"]
         },
         "__contains__": {
             "args": ["list", "object"],
@@ -293,6 +293,36 @@
             "args": ["int"],
             "type": "int",
             "requires": ["__prim__int___box__", "int___unbox__"]
+        },
+        "__and__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__prim__int___box__", "int___unbox__", "__prim__bool___box__", "bool___unbox__"]
+        },
+        "__rand__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__and__"]
+        },
+        "__or__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__prim__int___box__", "int___unbox__", "__prim__bool___box__", "bool___unbox__"]
+        },
+        "__ror__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__and__"]
+        },
+        "__xor__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__prim__int___box__", "int___unbox__", "__prim__bool___box__", "bool___unbox__"]
+        },
+        "__rxor__": {
+            "args": ["int", "int"],
+            "type": "int",
+            "requires": ["__and__"]
         }
     },
     "extends": "float"
@@ -301,7 +331,8 @@
     "functions": {
         "__create__": {
             "args": ["__prim__int"],
-            "type": "float"
+            "type": "float",
+            "requires": ["__prim__perm___box__"]
         },
         "__unbox__": {
             "args": ["float"],
@@ -331,7 +362,7 @@
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
-            "requires": ["int___bool__", "int___unbox__"]
+            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___is_inf__"]
         },
         "__eq__": {
             "args": ["float", "object"],
@@ -412,6 +443,11 @@
             "args": ["float"],
             "type": "int",
             "requires": ["unbox", "__prim__int___box__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__isNaN": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": ["float___is_nan__", "float___unbox__"]
         }
     },
     "extends": "object"
@@ -431,6 +467,18 @@
             "args": ["bool", "object"],
             "type": "__prim__bool",
             "requires": ["__unbox__"]
+        },
+        "__and__": {
+            "args": ["__prim__bool", "__prim__bool"],
+            "type": "__prim__bool"
+        },
+        "__or__": {
+            "args": ["__prim__bool", "__prim__bool"],
+            "type": "__prim__bool"
+        },
+        "__xor__": {
+            "args": ["__prim__bool", "__prim__bool"],
+            "type": "__prim__bool"
         }
     },
     "extends": "int"
@@ -649,6 +697,15 @@
         }
     }
 },
+"__prim__perm": {
+    "functions": {
+        "__box__": {
+            "args": ["__prim__perm"],
+            "type": "int",
+            "requires": ["float___unbox__", "float___is_nan__", "float___is_inf__"]
+        }
+    }
+},
 "__prim__bool": {
     "functions": {
         "__box__": {
@@ -865,7 +922,7 @@
         "__getitem__": {
             "args": ["range", "__prim__int"],
             "type": "__prim__int",
-            "requires": ["__val__"]
+            "requires": ["__val__", "__len__"]
         },
         "__getitem_slice__": {
             "args": ["range", "slice"],
@@ -958,13 +1015,24 @@
         "abs": {
             "args": ["__prim__int"],
             "type": "__prim__int"
+        },
+        "sum": {
+            "args": ["list"],
+            "type": "__prim__int",
+            "requires": ["__seq_ref_to_seq_int", "int___unbox__", "__prim__int___box__", "list___getitem__"]
         }
     },
     "methods": {
         "print": {
             "args": ["object"],
             "type": null,
             "MustTerminate": true
+        },
+        "sorted": {
+            "args": ["list"],
+            "type": "list",
+            "MustTerminate": true,
+            "requires": ["list___len__", "list___getitem__", "__prim__int___box__", "int___unbox__"]
         }
     }
 }

diff --git a/src/nagini_translation/translators/obligation/types/must_terminate.py b/src/nagini_translation/translators/obligation/types/must_terminate.py
@@ -100,7 +100,7 @@
 .. note::
 
     For axiomatic methods (the ones that are defined in
-    ``preamble.index``) we add additional precondition:
+    ``builtins.json``) we add additional precondition:
 
     1.  If method is marked as terminating, we add a check that caller
         termination measure is bigger than 1: