Add specification syntax for reasoning about pointer blocks

examples/concepts/c/mismatched_provenance.c

@@ -1,14 +1,14 @@
 #include <stdint.h>
 #include <stdbool.h>
 
-int main() {
+int failing() {
     int a[] = {5, 6, 7, 8};
     int b[] = {1, 2, 3, 4};
     intptr_t c = (intptr_t)&a[3];
     int *d = (int *)(c + 4);
-    // UB! comparison d == b only guarantees that the address of d and b are equal but not that they have the same provenance
-    // As far as the compiler is concerned it may assume that d == b is false even if it isn't at runtime
+    // The compiler is allowed to assume d==b includes checking for provenance (i.e. it may be false even if the adress is equal)
     if (d == b) {
+        // At runtime no such provenance check occurs so accessing *d is UB if we do not have provenance
         /*[/expect ptrPerm]*/
         //@ assert *d == 1;
         /*[/end]*/
@@ -26,3 +26,22 @@ bool pointerEq(int *p, int *q) {
     return p == q;
 }
 /*[/end]*/
+
+int passing() {
+    int a[] = {5, 6, 7, 8};
+    intptr_t c = (intptr_t)&a[2];
+    int *d = (int *)(c + 4);
+    if (d == a + 3) {
+        // Here we assume that the pointer acquired through the integer to pointer cast has the same provenance as a
+        // You can do this if you are sure that the compiler will also be able to figure this out (the exact behaviour of the compilers is not yet fully formalized)
+        //@ assume \pointer_block(d) == \pointer_block(a);
+        //@ assert *d == 8;
+        /*[/expect assertFailed:false]*/
+        //@ assert false;
+        /*[/end]*/
+        return 1;
+    } else {
+        return 0;
+    }
+}
+

res/universal/res/adt/pointer.pvl

@@ -75,4 +75,5 @@ ensures \result > 0;
 pure int ptr_address(`pointer` p) = `block`.block_address(`pointer`.pointer_block(p)) + (`pointer`.pointer_offset(p) * `block`.block_stride(`pointer`.pointer_block(p)));
 
 decreases;
+ensures ptr_address(\result) == address;
 pure `pointer` ptr_from_address(int address);

src/main/vct/main/stages/Parsing.scala

@@ -107,7 +107,7 @@ case class Parsing[G <: Generation](
                 blameProvider,
                 cc,
                 cSystemInclude,
-                readable.underlyingPath.map(_.getParent).toSeq ++
+                readable.underlyingPath.map(_.toAbsolutePath.getParent).toSeq ++
                   cOtherIncludes,
                 cDefines,
               )

src/parsers/antlr4/SpecLexer.g4

@@ -156,6 +156,7 @@ MATRIX: '\\matrix';
 ARRAY: '\\array';
 POINTER: '\\pointer';
 POINTER_INDEX: '\\pointer_index';
+POINTER_BLOCK: '\\pointer_block';
 POINTER_BLOCK_LENGTH: '\\pointer_block_length';
 POINTER_BLOCK_OFFSET: '\\pointer_block_offset';
 POINTER_LENGTH: '\\pointer_length';

src/parsers/antlr4/SpecParser.g4

@@ -185,6 +185,7 @@ valPrimaryPermission
  | '\\array'  '(' langExpr ',' langExpr ')' # valArray
  | '\\pointer' '(' langExpr ',' langExpr ',' langExpr ')' # valPointer
  | '\\pointer_index' '(' langExpr ',' langExpr ',' langExpr ')' # valPointerIndex
+ | '\\pointer_block' '(' langExpr ')' # valPointerBlock
  | '\\pointer_block_length' '(' langExpr ')' # valPointerBlockLength
  | '\\pointer_block_offset' '(' langExpr ')' # valPointerBlockOffset
  | '\\pointer_length' '(' langExpr ')' # valPointerLength

src/parsers/vct/parsers/transform/CPPToCol.scala

@@ -2109,6 +2109,7 @@ case class CPPToCol[G](
         PermPointer(convert(ptr), convert(n), convert(perm))
       case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) =>
         PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+      case ValPointerBlock(_, _, ptr, _) => PointerBlock(convert(ptr))(blame(e))
       case ValPointerBlockLength(_, _, ptr, _) =>
         PointerBlockLength(convert(ptr))(blame(e))
       case ValPointerBlockOffset(_, _, ptr, _) =>

src/parsers/vct/parsers/transform/CToCol.scala

@@ -1833,6 +1833,7 @@ case class CToCol[G](
         PermPointer(convert(ptr), convert(n), convert(perm))
       case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) =>
         PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+      case ValPointerBlock(_, _, ptr, _) => PointerBlock(convert(ptr))(blame(e))
       case ValPointerBlockLength(_, _, ptr, _) =>
         PointerBlockLength(convert(ptr))(blame(e))
       case ValPointerBlockOffset(_, _, ptr, _) =>

src/parsers/vct/parsers/transform/JavaToCol.scala

@@ -2370,6 +2370,7 @@ case class JavaToCol[G](
         PermPointer(convert(ptr), convert(n), convert(perm))
       case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) =>
         PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+      case ValPointerBlock(_, _, ptr, _) => PointerBlock(convert(ptr))(blame(e))
       case ValPointerBlockLength(_, _, ptr, _) =>
         PointerBlockLength(convert(ptr))(blame(e))
       case ValPointerBlockOffset(_, _, ptr, _) =>

src/parsers/vct/parsers/transform/LLVMContractToCol.scala

@@ -388,6 +388,7 @@ case class LLVMContractToCol[G](
         PermPointer(convert(ptr), convert(n), convert(perm))
       case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) =>
         PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+      case ValPointerBlock(_, _, ptr, _) => PointerBlock(convert(ptr))(blame(e))
       case ValPointerBlockLength(_, _, ptr, _) =>
         PointerBlockLength(convert(ptr))(blame(e))
       case ValPointerBlockOffset(_, _, ptr, _) =>

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -1790,6 +1790,7 @@ case class PVLToCol[G](
         PermPointer(convert(ptr), convert(n), convert(perm))
       case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) =>
         PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+      case ValPointerBlock(_, _, ptr, _) => PointerBlock(convert(ptr))(blame(e))
       case ValPointerBlockLength(_, _, ptr, _) =>
         PointerBlockLength(convert(ptr))(blame(e))
       case ValPointerBlockOffset(_, _, ptr, _) =>