Asn1

.gitignore

@@ -1,6 +1,7 @@
 syntax: glob
 env
 bin
+build
 deps/JPype1
 __pycache__
 .virtualenv
@@ -14,4 +15,4 @@ tmp
 docs/build
 .idea
 *.pyc
-viper_out
+viper_out

.vscode/launch.json

@@ -61,23 +61,20 @@
         },
         {
             "name": "Debug Nagini verifying Python",
-            "type": "python",
+            "type": "debugpy",
             "request": "launch",
-            "stopOnEntry": false,
-            "pythonPath": "${workspaceRoot}/nagini/env/bin/python3",
-            "program": "${workspaceRoot}/nagini/env/bin/nagini",
+            "program": "${workspaceFolder}/src/nagini_translation/main.py",
             "args": [
+                "--base-dir=${fileDirname}/..",
                 "${file}"
             ],
-            "cwd": "${workspaceRoot}",
-            "env": {},
-            "envFile": "${workspaceRoot}/.env",
+            "cwd": "${workspaceFolder}",
             "console": "integratedTerminal",
-            "debugOptions": [
-                "WaitOnAbnormalExit",
-                "WaitOnNormalExit",
-                "RedirectOutput"
-            ]
+            "justMyCode": false,
+            "python": "${command:python.interpreterPath}",
+            "env": {
+                "PYTHONPATH": "${workspaceFolder}/src"
+            }
         },
         {
             "name": "Translate Python to Viper",

setup.py

@@ -29,8 +29,9 @@
             'toposort==1.5',
             'jpype1==1.5.0',
             'astunparse==1.6.2',
-            'pytest==7.0.0',
-            'z3-solver==4.8.7.0'
+            'pytest',
+            'z3-solver==4.8.7.0',
+            'setuptools==68.2.0'
             ],
         entry_points={
              'console_scripts': [

src/nagini_contracts/contracts.py

@@ -30,7 +30,7 @@
 CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'ResultT', 'Implies', 'Forall', 'IOForall', 'Forall2', 'Forall3', 'Forall6',
                   'Exists', 'Low', 'LowVal', 'LowEvent', 'Declassify', 'TerminatesSif',
                   'Acc', 'Rd', 'Wildcard', 'Fold', 'Unfold', 'Unfolding', 'Previous',
-                  'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'ToMS', 'MaySet', 'MayCreate',
+                  'RaisedException', 'PSeq', 'PByteSeq', 'PSet', 'ToSeq', 'ToByteSeq', 'ToMS', 'MaySet', 'MayCreate',
                   'getMethod', 'getArg', 'getOld', 'arg', 'Joinable', 'MayStart', 'Let',
                   'PMultiset', 'LowExit', 'Refute', 'isNaN', 'Reveal']
 
@@ -205,6 +205,10 @@ def TerminatesSif(cond: bool, rank: int) -> bool:
     """
     pass
 
+PBool = bool
+
+PInt = int
+
 class PSeq(Generic[T], Sized, Iterable[T]):
     """
     A PSeq[T] represents a pure sequence of instances of subtypes of T, and
@@ -265,6 +269,66 @@ def __iter__(self) -> Iterator[T]:
         can be used as arguments for Forall.
         """
 
+class PByteSeq(Sized, Iterable[int]):
+    """
+    A PByteSeq represents a pure sequence of instances of int, and
+    is translated to native Viper sequences.
+    """
+
+    def __init__(self, *args: int) -> None:
+        """
+        ``PByteSeq(a, b, c)`` creates a PByteSeq instance containing the objects
+        a, b and c in that order.
+        """
+
+    def __contains__(self, item: object) -> bool:
+        """
+        True iff this PByteSeq contains the given object (not taking ``__eq__``
+        into account).
+        """
+
+    def __getitem__(self, item: int) -> int:
+        """
+        Returns the item at the given position.
+        """
+
+    def __len__(self) -> int:
+        """
+        Returns the length of this PByteSeq.
+        """
+
+    def __add__(self, other: 'PByteSeq') -> 'PByteSeq':
+        """
+        Concatenates two PByteSeqs to get a new PByteSeq.
+        """
+
+    def take(self, until: int) -> 'PByteSeq':
+        """
+        Returns a new PByteSeq containing all elements starting
+        from the beginning until the given index. ``PByteSeq(3,2,5,6).take(3)``
+        is equal to ``PByteSeq(3,2,5)``.
+        """
+
+    def drop(self, until: int) -> 'PByteSeq':
+        """
+        Returns a new PByteSeq containing all elements starting
+        from the given index (i.e., drops all elements until that index).
+        ``PByteSeq(2,3,5,6).drop(2)`` is equal to ``PByteSeq(5,6)``.
+        """
+
+    def update(self, index: int, new_val: int) -> 'PByteSeq':
+        """
+        Returns a new PByteSeq, containing the same elements
+        except for the element at index ``index``, which is replaced by
+        ``new_val``.
+        """
+
+    def __iter__(self) -> Iterator[int]:
+        """
+        PByteSeqs can be quantified over; this is only here so thatPByteSeqs
+        can be used as arguments for Forall.
+        """
+
 def Previous(it: T) -> PSeq[T]:
     """
     Within the body of a loop 'for x in xs', Previous(x) represents the list of
@@ -356,6 +420,12 @@ def ToSeq(l: Iterable[T]) -> PSeq[T]:
     Converts the given iterable of a built-in type (list, set, dict, range) to
     a pure PSeq.
     """
+
+def ToByteSeq(l: Iterable[int]) -> PByteSeq:
+    """
+    Converts the given iterable of a compatible built-in type (bytearray) to
+    a pure PByteSeq.
+    """
 
 
 def ToMS(s: PSeq[T]) -> PMultiset[T]:
@@ -542,6 +612,13 @@ def dict_pred(d: object) -> bool:
     be folded or unfolded.
     """
 
+def bytearray_pred(d: object) -> bool:
+    """
+    Special, predefined predicate that represents the permissions belonging
+    to a bytearray. To be used like normal predicates, except it does not need to
+    be folded or unfolded.
+    """
+
 def isNaN(f: float) -> bool:
     pass
 
@@ -595,10 +672,15 @@ def isNaN(f: float) -> bool:
         'list_pred',
         'dict_pred',
         'set_pred',
+        'bytearray_pred',
+        'PBool',
+        'PInt',
         'PSeq',
+        'PByteSeq',
         'PSet',
         'PMultiset',
         'ToSeq',
+        'ToByteSeq',
         'ToMS',
         'MaySet',
         'MayCreate',