Extend pointer encoding

build.sc

@@ -61,7 +61,7 @@ object external extends Module {
 object viper extends ScalaModule {
   object silverGit extends GitModule {
     def url = T { "https://github.com/viperproject/silver.git" }
-    def commitish = T { "10b1b26a20957e5f000bf1bbcd4017145148afd7" }
+    def commitish = T { "08c001b33decce0b16e698be862d7904c7282a99" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")
@@ -71,7 +71,7 @@ object viper extends ScalaModule {
 
   object siliconGit extends GitModule {
     def url = T { "https://github.com/viperproject/silicon.git" }
-    def commitish = T { "2030e3eb63f4b1c92ddc8885f7c937673effc9bd" }
+    def commitish = T { "2257d9c029d368629ed1f831c3c959713b1d1d10" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")
@@ -82,7 +82,7 @@ object viper extends ScalaModule {
 
   object carbonGit extends GitModule {
     def url = T { "https://github.com/viperproject/carbon.git" }
-    def commitish = T { "d14a703fc6428fbae54e7333d8ede7efbbf850f0" }
+    def commitish = T { "2da52018ead6e1f17fb1c67adc65ecdd4ff6c155" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")

examples/concepts/bitvectors/basic.c

@@ -0,0 +1,119 @@
+#include <stdint.h>
+
+void foo() {
+    uint8_t  ushl8  = ((uint8_t) 10) << ((uint8_t) 2);
+    uint16_t ushl16 = ((uint16_t)10) << ((uint16_t)2);
+    uint32_t ushl32 = ((uint32_t)10) << ((uint32_t)2);
+    uint64_t ushl64 = ((uint64_t)10) << ((uint64_t)2);
+    //@ assert ushl8  == 40;
+    //@ assert ushl16 == 40;
+    //@ assert ushl32 == 40;
+    //@ assert ushl64 == 40;
+    int8_t  sshl8  = ((int8_t) 10) << ((int8_t) 2);
+    int16_t sshl16 = ((int16_t)10) << ((int16_t)2);
+    int32_t sshl32 = ((int32_t)10) << ((int32_t)2);
+    int64_t sshl64 = ((int64_t)10) << ((int64_t)2);
+    //@ assert sshl8  == 40;
+    //@ assert sshl16 == 40;
+    //@ assert sshl32 == 40;
+    //@ assert sshl64 == 40;
+    uint8_t  ushr8  = ((uint8_t) 40) >> ((uint8_t) 2);
+    uint16_t ushr16 = ((uint16_t)40) >> ((uint16_t)2);
+    uint32_t ushr32 = ((uint32_t)40) >> ((uint32_t)2);
+    uint64_t ushr64 = ((uint64_t)40) >> ((uint64_t)2);
+    //@ assert ushr8  == 10;
+    //@ assert ushr16 == 10;
+    //@ assert ushr32 == 10;
+    //@ assert ushr64 == 10;
+    int8_t  sshr8  = ((int8_t) 40) >> ((int8_t) 2);
+    int16_t sshr16 = ((int16_t)40) >> ((int16_t)2);
+    int32_t sshr32 = ((int32_t)40) >> ((int32_t)2);
+    int64_t sshr64 = ((int64_t)40) >> ((int64_t)2);
+    //@ assert sshr8  == 10;
+    //@ assert sshr16 == 10;
+    //@ assert sshr32 == 10;
+    //@ assert sshr64 == 10;
+    uint8_t  lshr8  = ((uint8_t)                 128   ) >> ((uint8_t) 3);
+    uint16_t lshr16 = ((uint16_t)              32768   ) >> ((uint16_t)3);
+    uint32_t lshr32 = ((uint32_t)         2147483648   ) >> ((uint32_t)3);
+    uint64_t lshr64 = ((uint64_t)9223372036854775808ULL) >> ((uint64_t)3);
+    //@ assert lshr8  == 16;
+    //@ assert lshr16 == 4096;
+    //@ assert lshr32 == 268435456;
+    //@ assert lshr64 == 1152921504606846976ULL;
+    int8_t  ashr8  = ((int8_t)                 -128  ) >> ((int8_t) 3);
+    int16_t ashr16 = ((int16_t)              -32768  ) >> ((int16_t)3);
+    int32_t ashr32 = ((int32_t)         -2147483648  ) >> ((int32_t)3);
+    int64_t ashr64 = ((int64_t)-9223372036854775808LL) >> ((int64_t)3);
+    //@ assert ashr8  == -16;
+    //@ assert ashr16 == -4096;
+    //@ assert ashr32 == -268435456;
+    //@ assert ashr64 == -1152921504606846976ULL;
+    uint8_t  uand8  = ((uint8_t) 15) & ((uint8_t) 3);
+    uint16_t uand16 = ((uint16_t)15) & ((uint16_t)3);
+    uint32_t uand32 = ((uint32_t)15) & ((uint32_t)3);
+    uint64_t uand64 = ((uint64_t)15) & ((uint64_t)3);
+    //@ assert uand8  == 3;
+    //@ assert uand16 == 3;
+    //@ assert uand32 == 3;
+    //@ assert uand64 == 3;
+    int8_t  sand8  = ((int8_t) 15) & ((int8_t) 3);
+    int16_t sand16 = ((int16_t)15) & ((int16_t)3);
+    int32_t sand32 = ((int32_t)15) & ((int32_t)3);
+    int64_t sand64 = ((int64_t)15) & ((int64_t)3);
+    //@ assert sand8  == 3;
+    //@ assert sand16 == 3;
+    //@ assert sand32 == 3;
+    //@ assert sand64 == 3;
+    uint8_t  uor8  = ((uint8_t) 11) | ((uint8_t) 4);
+    uint16_t uor16 = ((uint16_t)11) | ((uint16_t)4);
+    uint32_t uor32 = ((uint32_t)11) | ((uint32_t)4);
+    uint64_t uor64 = ((uint64_t)11) | ((uint64_t)4);
+    //@ assert uor8  == 15;
+    //@ assert uor16 == 15;
+    //@ assert uor32 == 15;
+    //@ assert uor64 == 15;
+    int8_t  sor8  = ((int8_t) 11) | ((int8_t) 4);
+    int16_t sor16 = ((int16_t)11) | ((int16_t)4);
+    int32_t sor32 = ((int32_t)11) | ((int32_t)4);
+    int64_t sor64 = ((int64_t)11) | ((int64_t)4);
+    //@ assert sor8  == 15;
+    //@ assert sor16 == 15;
+    //@ assert sor32 == 15;
+    //@ assert sor64 == 15;
+    uint8_t  uxor8  = ((uint8_t) 10) ^ ((uint8_t) 2);
+    uint16_t uxor16 = ((uint16_t)10) ^ ((uint16_t)2);
+    uint32_t uxor32 = ((uint32_t)10) ^ ((uint32_t)2);
+    uint64_t uxor64 = ((uint64_t)10) ^ ((uint64_t)2);
+    //@ assert uxor8  == 8;
+    //@ assert uxor16 == 8;
+    //@ assert uxor32 == 8;
+    //@ assert uxor64 == 8;
+    int8_t  sxor8  = ((int8_t) 10) ^ ((int8_t) 2);
+    int16_t sxor16 = ((int16_t)10) ^ ((int16_t)2);
+    int32_t sxor32 = ((int32_t)10) ^ ((int32_t)2);
+    int64_t sxor64 = ((int64_t)10) ^ ((int64_t)2);
+    //@ assert sxor8  == 8;
+    //@ assert sxor16 == 8;
+    //@ assert sxor32 == 8;
+    //@ assert sxor64 == 8;
+    uint8_t  unot8  = ~(uint8_t) 10;
+    uint16_t unot16 = ~(uint16_t)10;
+    uint32_t unot32 = ~(uint32_t)10;
+    uint64_t unot64 = ~(uint64_t)10;
+    //@ assert unot8  == 245;
+    //@ assert unot16 == 65525;
+    //@ assert unot32 == 4294967285;
+    //@ assert unot64 == 18446744073709551605ULL;
+    int8_t  snot8  = ~(int8_t) 10;
+    int16_t snot16 = ~(int16_t)10;
+    int32_t snot32 = ~(int32_t)10;
+    int64_t snot64 = ~(int64_t)10;
+    //@ assert snot8  == -11;
+    //@ assert snot16 == -11;
+    //@ assert snot32 == -11;
+    //@ assert snot64 == -11;
+    /*[/expect assertFailed:false]*/
+    //@ assert false;
+    /*[/end]*/
+}

examples/concepts/c/mismatched_provenance.c

@@ -0,0 +1,47 @@
+#include <stdint.h>
+#include <stdbool.h>
+
+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);
+    // 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]*/
+        return 1;
+    } else {
+        return 0;
+    }
+}
+
+// We can attempt some trickery to see if pointers are equal without knowing the provenance, but it won't work luckily
+/*[/expect postFailed:false]*/
+//@ requires (p == q) || (p != q);
+//@ ensures \result == (p == q);
+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;
+    }
+}
+

examples/concepts/c/pointer_tag.c

@@ -0,0 +1,98 @@
+// Source: Lepigre et. al. 2022: VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
+
+#include <stdint.h>
+#include <stdbool.h>
+
+#define TAG_SIZE 3ULL
+#define TAG_MOD (1ULL << TAG_SIZE)
+#define TAG_MASK (TAG_MOD - 1ULL)
+
+
+//@ pure
+bool is_aligned(void *p) {
+    return ((uintptr_t)p & ((1ULL << 3ULL) - 1ULL)) == 0;
+}
+//@ resource has_tag(void *p, int t) = ((unsigned long long)p & ((1ULL << 3ULL) - 1ULL)) == t;
+//@ resource tagged(void *p, void *pt) = (unsigned long long)p == ((unsigned long long)pt & ~((1ULL << 3ULL) - 1ULL));
+
+//@ given int t2;
+//@ requires 0 <= (unsigned long long)p && (unsigned long long)p <= 18446744073709551615;
+//@ context has_tag(p, t2);
+//@ ensures \result == t2;
+unsigned char tag_of(void *p) {
+    //@ unfold has_tag(p, t2);
+    //@ fold has_tag(p, t2);
+    uintptr_t i = (uintptr_t) p;
+    uintptr_t t = i & TAG_MASK;
+    return t;
+}
+
+//@ requires p != NULL;
+//@ requires 0 <= t && t <= 7;
+//@ ensures (unsigned long long)\result == ((((unsigned long long) p) & ~((1ULL << 3ULL) - 1ULL)) | (unsigned long long)t);
+//@ ensures has_tag(\result, t);
+//@ ensures is_aligned(p) ==> tagged(p, \result);
+void *tag(void *p, unsigned char t) {
+    uintptr_t i = (uintptr_t) p;
+    uintptr_t new_i = (i & ~TAG_MASK) | (uintptr_t)t;
+    void *q = (void *) new_i;
+    //@ assert new_i == (unsigned long long)q;
+    //@ ghost lemma_tag_recoverable(i, new_i, t);
+    //@ fold has_tag(q, t);
+    if (is_aligned(p)) {
+        // For some reason this assume is necessary
+        //@ assume ((unsigned long long)p & ((1ULL << 3ULL) - 1ULL)) == 0;
+        //@ ghost lemma_pointer_preserved(i, new_i, t);
+        //@ ghost lemma_pointer_address_eq(i, p, new_i, q);
+        //@ fold tagged(p, q);
+    }
+    return q;
+}
+
+//@ given void *originalP;
+//@ requires p != NULL;
+//@ context tagged(originalP, p);
+//@ ensures (unsigned long long)\result == ((((unsigned long long) p) & ~((1ULL << 3ULL) - 1ULL)));
+//@ ensures (unsigned long long)\result == (unsigned long long)originalP;
+void *untag(void *p) {
+    //@ unfold tagged(originalP, p);
+    //@ fold tagged(originalP, p);
+    return tag(p, 0);
+}
+
+#include <stddef.h>
+
+//@ requires 0 <= a && a <= 18446744073709551615;
+//@ requires 0 <= b && b <= 18446744073709551615;
+//@ requires 0 <= t && t <= 7;
+//@ ensures b == ((a & ~7ULL) | (unsigned long long)t);
+//@ ensures (b & 7ULL) == t;
+void lemma_tag_recoverable(unsigned long long a, unsigned long long b, unsigned char t);
+
+
+//@ requires 0 <= a && a <= 18446744073709551615;
+//@ requires 0 <= b && b <= 18446744073709551615;
+//@ requires 0 <= t && t <= 7;
+//@ requires (a & 7ULL) == 0;
+//@ requires b == ((a & ~7ULL) | (unsigned long long)t);
+//@ ensures (b & ~7ULL) == a;
+void lemma_pointer_preserved(unsigned long long a, unsigned long long b, unsigned char t);
+
+//@ requires 0 <= a && a <= 18446744073709551615;
+//@ requires 0 <= b && b <= 18446744073709551615;
+//@ requires (unsigned long long)p == a;
+//@ requires (unsigned long long)q == b;
+//@ requires a == (b & ~7ULL);
+//@ ensures (unsigned long long)p == ((unsigned long long)q & ~7ULL);
+void lemma_pointer_address_eq(unsigned long long a, void *p, unsigned long long b, void *q) {}
+
+void client() {
+    size_t x = 0;
+    void *xp = (void*)&x;
+    //@ assume is_aligned(xp);
+    void *tp = tag((void *)&x, 1);
+    //@ assert tag_of(tp)/*@ given {t2 = 1} @*/ == 1;
+    size_t *px = (size_t *) untag(tp) /*@ given {originalP=xp} @*/;
+    //@ assume \pointer_block(xp) == \pointer_block(px);
+    //@ assert *px == 0;
+}

examples/concepts/c/ptr_comparisons.c

@@ -0,0 +1,25 @@
+#include <stdint.h>
+
+//@ requires x != NULL;
+//@ context Perm(x, write);
+void bar(int *x);
+
+void foo() {
+    int a[] = {1, 2, 3, 4};
+    int *start = &a[0];
+    int *p = start;
+    int *end = &a[3];
+    //@ assert end >= start;
+    //@ assert start < end;
+    //@ loop_invariant start <= p && p <= end;
+    //@ loop_invariant (\forall* int i=0 .. 4; Perm(&a[i], write));
+    while (p <= end) {
+
+        if (p == end) {
+            break;
+        } else {
+            //@ assert end > p;
+        }
+    }
+}
+

res/universal/res/adt/bv16.pvl

@@ -0,0 +1,38 @@
+prover_type bv16 \smtlib `(_ BitVec 16)`;
+
+prover_function bv16 bv16_from_sint(int x) \smtlib `(_ int2bv 16)`;
+prover_function bv16 bv16_from_uint(int x) \smtlib `(_ int2bv 16)`;
+prover_function int bv16_to_uint(bv16 x) \smtlib `bv2nat`;
+prover_function bv16 bv16_and(bv16 x, bv16 y) \smtlib `bvand`;
+prover_function bv16 bv16_or(bv16 x, bv16 y) \smtlib `bvor`;
+prover_function bv16 bv16_xor(bv16 x, bv16 y) \smtlib `bvxor`;
+prover_function bv16 bv16_shl(bv16 x, bv16 y) \smtlib `bvshl`;
+prover_function bv16 bv16_shr(bv16 x, bv16 y) \smtlib `bvashr`;
+prover_function bv16 bv16_ushr(bv16 x, bv16 y) \smtlib `bvlshr`;
+prover_function bv16 bv16_not(bv16 x) \smtlib `bvnot`;
+
+prover_function boolean bv16_slt(bv16 a, bv16 b) \smtlib `bvslt`;
+prover_function bv16 bv16_zero() \smtlib `#x0000`;
+
+pure int bv16_to_sint(bv16 x) = bv16_slt(x, bv16_zero()) ? bv16_to_uint(x) - 65536 : bv16_to_uint(x);
+
+ensures \result == (0 <= x && x <= 65535);
+ensures \result == (x == bv16_to_uint(bv16_from_uint(x)));
+pure boolean u16_is_inbounds(int x);
+
+ensures \polarity_dependent(bv16_from_uint(bv16_to_uint(x)) == x, true);
+pure boolean u16_assume_inbounds(bv16 x) = true;
+
+requires u16_is_inbounds(x);
+pure int u16_require_inbounds(int x) = x;
+
+ensures \result == (-32768 <= x && x <= 32767);
+ensures \result == (x == bv16_to_sint(bv16_from_sint(x)));
+pure boolean s16_is_inbounds(int x);
+
+ensures \polarity_dependent(bv16_from_sint(bv16_to_sint(x)) == x, true);
+pure boolean s16_assume_inbounds(bv16 x) = true;
+
+requires s16_is_inbounds(x);
+pure int s16_require_inbounds(int x) = x;
+

res/universal/res/adt/bv32.pvl

@@ -0,0 +1,38 @@
+prover_type bv32 \smtlib `(_ BitVec 32)`;
+
+prover_function bv32 bv32_from_sint(int x) \smtlib `(_ int2bv 32)`;
+prover_function bv32 bv32_from_uint(int x) \smtlib `(_ int2bv 32)`;
+prover_function int bv32_to_uint(bv32 x) \smtlib `bv2nat`;
+prover_function bv32 bv32_and(bv32 x, bv32 y) \smtlib `bvand`;
+prover_function bv32 bv32_or(bv32 x, bv32 y) \smtlib `bvor`;
+prover_function bv32 bv32_xor(bv32 x, bv32 y) \smtlib `bvxor`;
+prover_function bv32 bv32_shl(bv32 x, bv32 y) \smtlib `bvshl`;
+prover_function bv32 bv32_shr(bv32 x, bv32 y) \smtlib `bvashr`;
+prover_function bv32 bv32_ushr(bv32 x, bv32 y) \smtlib `bvlshr`;
+prover_function bv32 bv32_not(bv32 x) \smtlib `bvnot`;
+
+prover_function boolean bv32_slt(bv32 a, bv32 b) \smtlib `bvslt`;
+prover_function bv32 bv32_zero() \smtlib `#x00000000`;
+
+pure int bv32_to_sint(bv32 x) = bv32_slt(x, bv32_zero()) ? bv32_to_uint(x) - 4294967296 : bv32_to_uint(x);
+
+ensures \result == (0 <= x && x <= 4294967295);
+ensures \result == (x == bv32_to_uint(bv32_from_uint(x)));
+pure boolean u32_is_inbounds(int x);
+
+ensures \polarity_dependent(bv32_from_uint(bv32_to_uint(x)) == x, true);
+pure boolean u32_assume_inbounds(bv32 x) = true;
+
+requires u32_is_inbounds(x);
+pure int u32_require_inbounds(int x) = x;
+
+ensures \result == (-2147483648 <= x && x <= 2147483647);
+ensures \result == (x == bv32_to_sint(bv32_from_sint(x)));
+pure boolean s32_is_inbounds(int x);
+
+ensures \polarity_dependent(bv32_from_sint(bv32_to_sint(x)) == x, true);
+pure boolean s32_assume_inbounds(bv32 x) = true;
+
+requires s32_is_inbounds(x);
+pure int s32_require_inbounds(int x) = x;
+