diff --git a/build.sc b/build.sc index 4e1d759c26..b60d9a7487 100644 --- a/build.sc +++ b/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") diff --git a/examples/concepts/bitvectors/basic.c b/examples/concepts/bitvectors/basic.c new file mode 100644 index 0000000000..71c4f9aadf --- /dev/null +++ b/examples/concepts/bitvectors/basic.c @@ -0,0 +1,119 @@ +#include + +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]*/ +} diff --git a/examples/concepts/c/mismatched_provenance.c b/examples/concepts/c/mismatched_provenance.c new file mode 100644 index 0000000000..008cf37f89 --- /dev/null +++ b/examples/concepts/c/mismatched_provenance.c @@ -0,0 +1,47 @@ +#include +#include + +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; + } +} + diff --git a/examples/concepts/c/pointer_tag.c b/examples/concepts/c/pointer_tag.c new file mode 100644 index 0000000000..742eecaa41 --- /dev/null +++ b/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 +#include + +#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 + +//@ 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; +} diff --git a/examples/concepts/c/ptr_comparisons.c b/examples/concepts/c/ptr_comparisons.c new file mode 100644 index 0000000000..a82088589a --- /dev/null +++ b/examples/concepts/c/ptr_comparisons.c @@ -0,0 +1,25 @@ +#include + +//@ 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; + } + } +} + diff --git a/examples/concepts/c/tagged_pointer.c b/examples/concepts/c/tagged_struct.c similarity index 100% rename from examples/concepts/c/tagged_pointer.c rename to examples/concepts/c/tagged_struct.c diff --git a/res/universal/res/adt/bv16.pvl b/res/universal/res/adt/bv16.pvl new file mode 100644 index 0000000000..de088c496e --- /dev/null +++ b/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; + diff --git a/res/universal/res/adt/bv32.pvl b/res/universal/res/adt/bv32.pvl new file mode 100644 index 0000000000..163e350c93 --- /dev/null +++ b/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; + diff --git a/res/universal/res/adt/bv64.pvl b/res/universal/res/adt/bv64.pvl new file mode 100644 index 0000000000..97b7d6a641 --- /dev/null +++ b/res/universal/res/adt/bv64.pvl @@ -0,0 +1,38 @@ +prover_type bv64 \smtlib `(_ BitVec 64)`; + +prover_function bv64 bv64_from_sint(int x) \smtlib `(_ int2bv 64)`; +prover_function bv64 bv64_from_uint(int x) \smtlib `(_ int2bv 64)`; +prover_function int bv64_to_uint(bv64 x) \smtlib `bv2nat`; +prover_function bv64 bv64_and(bv64 x, bv64 y) \smtlib `bvand`; +prover_function bv64 bv64_or(bv64 x, bv64 y) \smtlib `bvor`; +prover_function bv64 bv64_xor(bv64 x, bv64 y) \smtlib `bvxor`; +prover_function bv64 bv64_shl(bv64 x, bv64 y) \smtlib `bvshl`; +prover_function bv64 bv64_shr(bv64 x, bv64 y) \smtlib `bvashr`; +prover_function bv64 bv64_ushr(bv64 x, bv64 y) \smtlib `bvlshr`; +prover_function bv64 bv64_not(bv64 x) \smtlib `bvnot`; + +prover_function boolean bv64_slt(bv64 a, bv64 b) \smtlib `bvslt`; +prover_function bv64 bv64_zero() \smtlib `#x0000000000000000`; + +pure int bv64_to_sint(bv64 x) = bv64_slt(x, bv64_zero()) ? bv64_to_uint(x) - 18446744073709551616 : bv64_to_uint(x); + +ensures \result == (0 <= x && x <= 18446744073709551615); +ensures \result == (x == bv64_to_uint(bv64_from_uint(x))); +pure boolean u64_is_inbounds(int x); + +ensures \polarity_dependent(bv64_from_uint(bv64_to_uint(x)) == x, true); +pure boolean u64_assume_inbounds(bv64 x) = true; + +requires u64_is_inbounds(x); +pure int u64_require_inbounds(int x) = x; + +ensures \result == (-9223372036854775808 <= x && x <= 9223372036854775807); +ensures \result == (x == bv64_to_sint(bv64_from_sint(x))); +pure boolean s64_is_inbounds(int x); + +ensures \polarity_dependent(bv64_from_sint(bv64_to_sint(x)) == x, true); +pure boolean s64_assume_inbounds(bv64 x) = true; + +requires s64_is_inbounds(x); +pure int s64_require_inbounds(int x) = x; + diff --git a/res/universal/res/adt/bv8.pvl b/res/universal/res/adt/bv8.pvl new file mode 100644 index 0000000000..96896d99a9 --- /dev/null +++ b/res/universal/res/adt/bv8.pvl @@ -0,0 +1,38 @@ +prover_type bv8 \smtlib `(_ BitVec 8)`; + +prover_function bv8 bv8_from_sint(int x) \smtlib `(_ int2bv 8)`; +prover_function bv8 bv8_from_uint(int x) \smtlib `(_ int2bv 8)`; +prover_function int bv8_to_uint(bv8 x) \smtlib `bv2nat`; +prover_function bv8 bv8_and(bv8 x, bv8 y) \smtlib `bvand`; +prover_function bv8 bv8_or(bv8 x, bv8 y) \smtlib `bvor`; +prover_function bv8 bv8_xor(bv8 x, bv8 y) \smtlib `bvxor`; +prover_function bv8 bv8_shl(bv8 x, bv8 y) \smtlib `bvshl`; +prover_function bv8 bv8_shr(bv8 x, bv8 y) \smtlib `bvashr`; +prover_function bv8 bv8_ushr(bv8 x, bv8 y) \smtlib `bvlshr`; +prover_function bv8 bv8_not(bv8 x) \smtlib `bvnot`; + +prover_function boolean bv8_slt(bv8 a, bv8 b) \smtlib `bvslt`; +prover_function bv8 bv8_zero() \smtlib `#x00`; + +pure int bv8_to_sint(bv8 x) = bv8_slt(x, bv8_zero()) ? bv8_to_uint(x) - 256 : bv8_to_uint(x); + +ensures \result == (0 <= x && x <= 255); +ensures \result == (x == bv8_to_uint(bv8_from_uint(x))); +pure boolean u8_is_inbounds(int x); + +ensures \polarity_dependent(bv8_from_uint(bv8_to_uint(x)) == x, true); +pure boolean u8_assume_inbounds(bv8 x) = true; + +requires u8_is_inbounds(x); +pure int u8_require_inbounds(int x) = x; + +ensures \result == (-128 <= x && x <= 127); +ensures \result == (x == bv8_to_sint(bv8_from_sint(x))); +pure boolean s8_is_inbounds(int x); + +ensures \polarity_dependent(bv8_from_sint(bv8_to_sint(x)) == x, true); +pure boolean s8_assume_inbounds(bv8 x) = true; + +requires s8_is_inbounds(x); +pure int s8_require_inbounds(int x) = x; + diff --git a/res/universal/res/adt/pointer.pvl b/res/universal/res/adt/pointer.pvl index b2485ab845..6993e92f0e 100644 --- a/res/universal/res/adt/pointer.pvl +++ b/res/universal/res/adt/pointer.pvl @@ -1,15 +1,27 @@ adt `block` { pure int block_length(`block` b); pure ref loc(`block` b, int i); + pure int block_address(`block` b); + pure int block_stride(`block` b); pure `block` loc_inv_1(ref r); pure int loc_inv_2(ref r); + pure `block` addr_inv(int address); + // block length is non-negative axiom (\forall `block` b; block_length(b) >= 0); // loc is injective: a (block, index) pair indicates a unique ref axiom (∀ `block` b, int i; loc_inv_1({:loc(b, i):}) == b && loc_inv_2(loc(b, i)) == i); + + // a block must be based higher than 0 + axiom (∀ `block` b; {:block_address(b):} > 0); + + // every block is uniquely identified by an address + axiom (∀ `block` b; addr_inv({:block_address(b):}) == b); + + axiom (∀ `block` p; {:block_stride(p):} > 0); } adt `pointer` { @@ -32,6 +44,8 @@ adt `pointer` { axiom (∀ `pointer` p; pointer_inv({:ptr_deref(p):}) == p); + axiom (∀ `pointer` p1, `pointer` p2; ({:ptr_address(p1):} == {:ptr_address(p2):} && {:pointer_block(p1):} == {:pointer_block(p2):}) ==> p1 == p2); + axiom ptr_add_axiom(); } @@ -57,3 +71,11 @@ ensures (\forall `pointer` p1, int offset, int i; i < `block`.block_length(`pointer`.pointer_block(p1)) - `pointer`.pointer_offset(p1) - offset; {:ptr_add(ptr_add(p1, offset), i):} == ptr_add(p1, offset + i)); pure boolean ptr_add_axiom() = true; + +decreases; +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); diff --git a/res/universal/res/c/stdint.h b/res/universal/res/c/stdint.h index b23850bc00..c975ef840b 100644 --- a/res/universal/res/c/stdint.h +++ b/res/universal/res/c/stdint.h @@ -1,35 +1,35 @@ #ifndef STDINT_H #define STDINT_H -#define int8_t int -#define int16_t int +#define int8_t signed char +#define int16_t signed short #define int32_t int -#define uint8_t int -#define uint16_t int -#define uint32_t int -#define int64_t int -#define uint64_t int +#define uint8_t unsigned char +#define uint16_t unsigned short +#define uint32_t unsigned int +#define int64_t signed long long +#define uint64_t unsigned long long -#define int_least8_t int -#define int_least16_t int -#define int_least32_t int -#define int_least64_t int -#define uint_least8_t int -#define uint_least16_t int -#define uint_least32_t int -#define uint_least64_t int +#define int_least8_t int8_t +#define int_least16_t int16_t +#define int_least32_t int32_t +#define int_least64_t int64_t +#define uint_least8_t uint8_t +#define uint_least16_t uint16_t +#define uint_least32_t uint32_t +#define uint_least64_t uint64_t -#define int_fast8_t int -#define int_fast16_t int -#define int_fast32_t int -#define int_fast64_t int -#define uint_fast8_t int -#define uint_fast16_t int -#define uint_fast32_t int -#define uint_fast64_t int +#define int_fast8_t int8_t +#define int_fast16_t int16_t +#define int_fast32_t int32_t +#define int_fast64_t int64_t +#define uint_fast8_t uint8_t +#define uint_fast16_t uint16_t +#define uint_fast32_t uint32_t +#define uint_fast64_t uint64_t -#define intptr_t int -#define uintptr_t int +#define intptr_t signed long long +#define uintptr_t unsigned long long #endif diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 9c7c7b8bb2..6cf40ba2e0 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -136,6 +136,9 @@ final case class TPointer[G](element: Type[G])( final case class TNonNullPointer[G](element: Type[G])( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TNonNullPointerImpl[G] +// TODO: Add information for inner type to pointer block type +final case class TPointerBlock[G]()(implicit val o: Origin = DiagnosticOrigin) + extends Type[G] with TPointerBlockImpl[G] final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with TTypeImpl[G] final case class TVar[G](ref: Ref[G, Variable[G]])( @@ -202,6 +205,7 @@ final case class TProcess[G]()(implicit val o: Origin = DiagnosticOrigin) sealed trait NumericType[G] extends PrimitiveType[G] with NumericTypeImpl[G] sealed trait FloatType[G] extends NumericType[G] with FloatTypeImpl[G] sealed trait IntType[G] extends NumericType[G] with IntTypeImpl[G] +sealed trait BitwiseType[G] extends Type[G] with BitwiseTypeImpl[G] final case class TInt[G]()(implicit val o: Origin = DiagnosticOrigin) extends IntType[G] with TIntImpl[G] @@ -682,6 +686,7 @@ final class ByReferenceClass[G]( final class ByValueClass[G]( val typeArgs: Seq[Variable[G]], val decls: Seq[ClassDeclaration[G]], + val packed: Boolean, )(implicit val o: Origin) extends Class[G] with ByValueClassImpl[G] final class Model[G](val declarations: Seq[ModelDeclaration[G]])( @@ -1040,7 +1045,7 @@ final case class CoerceCFloatCInt[G](source: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCFloatCIntImpl[G] final case class CoerceCIntCFloat[G](target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCIntCFloatImpl[G] -final case class CoerceCIntInt[G]()(implicit val o: Origin) +final case class CoerceCIntInt[G](t: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCIntIntImpl[G] final case class CoerceCFloatFloat[G](source: Type[G], target: Type[G])( implicit val o: Origin @@ -1179,8 +1184,9 @@ sealed trait Expr[G] extends NodeFamily[G] with ExprImpl[G] sealed trait Constant[G] extends Expr[G] with ConstantImpl[G] sealed trait ConstantInt[G] extends Constant[G] with ConstantIntImpl[G] -final case class CIntegerValue[G](value: BigInt)(implicit val o: Origin) - extends ConstantInt[G] with Expr[G] with CIntegerValueImpl[G] +final case class CIntegerValue[G](value: BigInt, t: Type[G])( + implicit val o: Origin +) extends ConstantInt[G] with Expr[G] with CIntegerValueImpl[G] final case class IntegerValue[G](value: BigInt)(implicit val o: Origin) extends ConstantInt[G] with Expr[G] with IntegerValueImpl[G] final case class BooleanValue[G](value: Boolean)(implicit val o: Origin) @@ -1538,7 +1544,9 @@ sealed trait UnExpr[G] extends Expr[G] with UnExprImpl[G] final case class UMinus[G](arg: Expr[G])(implicit val o: Origin) extends UnExpr[G] with UMinusImpl[G] -final case class BitNot[G](arg: Expr[G])(implicit val o: Origin) +final case class BitNot[G](arg: Expr[G], bits: Int, signed: Boolean)( + val blame: Blame[IntegerOutOfBounds] +)(implicit val o: Origin) extends UnExpr[G] with BitNotImpl[G] final case class Not[G](arg: Expr[G])(implicit val o: Origin) extends UnExpr[G] with NotImpl[G] @@ -1684,23 +1692,45 @@ final case class StringConcat[G](left: Expr[G], right: Expr[G])( implicit val o: Origin ) extends BinExpr[G] with StringConcatImpl[G] -final case class BitAnd[G](left: Expr[G], right: Expr[G])( - implicit val o: Origin -) extends BinExpr[G] with BitAndImpl[G] -final case class BitOr[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) +final case class BitAnd[G]( + left: Expr[G], + right: Expr[G], + bits: Int, + signed: Boolean, +)(val blame: Blame[IntegerOutOfBounds])(implicit val o: Origin) + extends BinExpr[G] with BitAndImpl[G] +final case class BitOr[G]( + left: Expr[G], + right: Expr[G], + bits: Int, + signed: Boolean, +)(val blame: Blame[IntegerOutOfBounds])(implicit val o: Origin) extends BinExpr[G] with BitOrImpl[G] -final case class BitXor[G](left: Expr[G], right: Expr[G])( - implicit val o: Origin -) extends BinExpr[G] with BitXorImpl[G] -final case class BitShl[G](left: Expr[G], right: Expr[G])( - implicit val o: Origin -) extends BinExpr[G] with BitShlImpl[G] -final case class BitShr[G](left: Expr[G], right: Expr[G])( - implicit val o: Origin -) extends BinExpr[G] with BitShrImpl[G] -final case class BitUShr[G](left: Expr[G], right: Expr[G])( - implicit val o: Origin -) extends BinExpr[G] with BitUShrImpl[G] +final case class BitXor[G]( + left: Expr[G], + right: Expr[G], + bits: Int, + signed: Boolean, +)(val blame: Blame[IntegerOutOfBounds])(implicit val o: Origin) + extends BinExpr[G] with BitXorImpl[G] +final case class BitShl[G]( + left: Expr[G], + right: Expr[G], + bits: Int, + signed: Boolean, +)(val blame: Blame[IntegerOutOfBounds])(implicit val o: Origin) + extends BinExpr[G] with BitShlImpl[G] +final case class BitShr[G](left: Expr[G], right: Expr[G], bits: Int)( + val blame: Blame[IntegerOutOfBounds] +)(implicit val o: Origin) + extends BinExpr[G] with BitShrImpl[G] +final case class BitUShr[G]( + left: Expr[G], + right: Expr[G], + bits: Int, + signed: Boolean, +)(val blame: Blame[IntegerOutOfBounds])(implicit val o: Origin) + extends BinExpr[G] with BitUShrImpl[G] final case class And[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends BinExpr[G] with AndImpl[G] @@ -1731,6 +1761,14 @@ final case class Unfolding[G](res: FoldTarget[G], body: Expr[G])( )(implicit val o: Origin) extends Expr[G] with UnfoldingImpl[G] +final case class Assuming[G](assn: Expr[G], inner: Expr[G])( + implicit val o: Origin +) extends Expr[G] with AssumingImpl[G] +final case class Asserting[G](condition: Expr[G], body: Expr[G])( + val blame: Blame[AssertFailed] +)(implicit val o: Origin) + extends Expr[G] with AssertingImpl[G] + @family sealed trait Location[G] extends NodeFamily[G] with LocationImpl[G] final case class HeapVariableLocation[G](ref: Ref[G, HeapVariable[G]])( @@ -1868,6 +1906,27 @@ final case class SubBagEq[G](left: Expr[G], right: Expr[G])( implicit val o: Origin ) extends SetComparison[G] with SubBagEqImpl[G] +sealed trait PointerComparison[G] + extends OrderOp[G] with PointerComparisonImpl[G] +final case class PointerEq[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerEqImpl[G] +final case class PointerNeq[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerNeqImpl[G] +final case class PointerGreater[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerGreaterImpl[G] +final case class PointerLess[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerLessImpl[G] +final case class PointerGreaterEq[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerGreaterEqImpl[G] +final case class PointerLessEq[G](left: Expr[G], right: Expr[G])( + implicit val o: Origin +) extends PointerComparison[G] with PointerLessEqImpl[G] + final case class Select[G]( condition: Expr[G], whenTrue: Expr[G], @@ -1924,6 +1983,14 @@ final case class Length[G](arr: Expr[G])(val blame: Blame[ArrayNull])( ) extends Expr[G] with LengthImpl[G] final case class Size[G](obj: Expr[G])(implicit val o: Origin) extends Expr[G] with SizeImpl[G] +final case class PointerBlock[G](pointer: Expr[G])( + val blame: Blame[PointerNull] +)(implicit val o: Origin) + extends Expr[G] with PointerBlockImpl[G] +final case class PointerAddress[G](pointer: Expr[G])( + val blame: Blame[PointerNull] +)(implicit val o: Origin) + extends Expr[G] with PointerAddressImpl[G] final case class PointerBlockLength[G](pointer: Expr[G])( val blame: Blame[PointerNull] )(implicit val o: Origin) @@ -2831,13 +2898,16 @@ final case class CLiteralArray[G](exprs: Seq[Expr[G]])(implicit val o: Origin) sealed trait CType[G] extends Type[G] with CTypeImpl[G] final case class TCInt[G]()(implicit val o: Origin = DiagnosticOrigin) - extends IntType[G] with CType[G] with TCIntImpl[G] + extends IntType[G] with CType[G] with TCIntImpl[G] with BitwiseType[G] { + var bits: Option[Int] = None + var signed: Boolean = true +} final case class TCFloat[G](exponent: Int, mantissa: Int)( implicit val o: Origin = DiagnosticOrigin ) extends FloatType[G] with CType[G] with TCFloatImpl[G] final case class CPrimitiveType[G](specifiers: Seq[CDeclarationSpecifier[G]])( implicit val o: Origin = DiagnosticOrigin -) extends CType[G] with CPrimitiveTypeImpl[G] +) extends CType[G] with CPrimitiveTypeImpl[G] with BitwiseType[G] final case class CTPointer[G](innerType: Type[G])( implicit val o: Origin = DiagnosticOrigin ) extends CType[G] with CTPointerImpl[G] diff --git a/src/col/vct/col/ast/expr/heap/read/PointerAddressImpl.scala b/src/col/vct/col/ast/expr/heap/read/PointerAddressImpl.scala new file mode 100644 index 0000000000..cd45dfee09 --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/read/PointerAddressImpl.scala @@ -0,0 +1,15 @@ +package vct.col.ast.expr.heap.read + +import vct.col.ast.ops.PointerAddressOps +import vct.col.ast.{PointerAddress, TInt, Type} +import vct.col.print._ + +trait PointerAddressImpl[G] extends PointerAddressOps[G] { + this: PointerAddress[G] => + override def t: Type[G] = TInt() + + override def precedence: Int = Precedence.ATOMIC + + override def layout(implicit ctx: Ctx): Doc = + Text("\\pointer_address(") <> pointer <> ")" +} diff --git a/src/col/vct/col/ast/expr/heap/read/PointerBlockImpl.scala b/src/col/vct/col/ast/expr/heap/read/PointerBlockImpl.scala new file mode 100644 index 0000000000..7ce70da13a --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/read/PointerBlockImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.expr.heap.read + +import vct.col.ast.ops.PointerBlockOps +import vct.col.ast.{PointerBlock, TPointerBlock, Type} +import vct.col.print._ + +trait PointerBlockImpl[G] extends PointerBlockOps[G] { + this: PointerBlock[G] => + override def t: Type[G] = TPointerBlock() + + override def precedence: Int = Precedence.ATOMIC + override def layout(implicit ctx: Ctx): Doc = + Text("\\pointer_block(") <> pointer <> ")" +} diff --git a/src/col/vct/col/ast/expr/literal/constant/CIntegerValueImpl.scala b/src/col/vct/col/ast/expr/literal/constant/CIntegerValueImpl.scala index 180ceda434..2c02c073ef 100644 --- a/src/col/vct/col/ast/expr/literal/constant/CIntegerValueImpl.scala +++ b/src/col/vct/col/ast/expr/literal/constant/CIntegerValueImpl.scala @@ -1,12 +1,11 @@ package vct.col.ast.expr.literal.constant -import vct.col.ast.{CIntegerValue, TCInt, Type} +import vct.col.ast.CIntegerValue import vct.col.print.{Ctx, Doc, Precedence, Text} import vct.col.ast.ops.CIntegerValueOps trait CIntegerValueImpl[G] extends CIntegerValueOps[G] { this: CIntegerValue[G] => - override def t: Type[G] = TCInt() override def precedence: Int = Precedence.ATOMIC override def layout(implicit ctx: Ctx): Doc = Text(value.toString()) diff --git a/src/col/vct/col/ast/expr/op/BinExprImpl.scala b/src/col/vct/col/ast/expr/op/BinExprImpl.scala index 326e807069..a065f1598b 100644 --- a/src/col/vct/col/ast/expr/op/BinExprImpl.scala +++ b/src/col/vct/col/ast/expr/op/BinExprImpl.scala @@ -3,11 +3,14 @@ package vct.col.ast.expr.op import vct.col.ast.`type`.typeclass.TFloats.getFloatMax import vct.col.ast.{ BinExpr, + BitwiseType, + CPrimitiveType, + CSpecificationType, Expr, IntType, + LLVMTInt, TBool, TCInt, - LLVMTInt, TInt, TProcess, TRational, @@ -16,6 +19,7 @@ import vct.col.ast.{ Type, } import vct.col.origin.Origin +import vct.col.resolve.lang.C import vct.col.typerules.{CoercionUtils, Types} import vct.result.VerificationError @@ -82,14 +86,6 @@ object BinOperatorTypes { TVector[G](sizeL, getNumericType(eL, eR, o))).get } - def getIntType[G](lt: Type[G], rt: Type[G]): IntType[G] = - if (isCIntOp(lt, rt)) - TCInt() - else if (isLLVMIntOp(lt, rt)) - Types.leastCommonSuperType(lt, rt).asInstanceOf[LLVMTInt[G]] - else - TInt() - case class NumericBinError(lt: Type[_], rt: Type[_], o: Origin) extends VerificationError.UserError { override def text: String = @@ -99,7 +95,17 @@ object BinOperatorTypes { def getNumericType[G](lt: Type[G], rt: Type[G], o: Origin): Type[G] = { if (isCIntOp(lt, rt)) - TCInt[G]() + (lt, rt) match { + case (l: BitwiseType[G], r: BitwiseType[G]) + if l.signed == r.signed && l.bits.isDefined && + l.bits.get >= r.bits.getOrElse(0) => + l + case (l: BitwiseType[G], r: BitwiseType[G]) + if l.signed == r.signed && r.bits.isDefined && + r.bits.get >= l.bits.getOrElse(0) => + r + case _ => TCInt[G]() + } else if (isLLVMIntOp(lt, rt)) Types.leastCommonSuperType(lt, rt).asInstanceOf[LLVMTInt[G]] else if (isIntOp(lt, rt)) @@ -139,8 +145,6 @@ trait BinExprImpl[G] { def isVectorOp: Boolean = BinOperatorTypes.isVectorOp(left.t, right.t) def isVectorIntOp: Boolean = BinOperatorTypes.isVectorIntOp(left.t, right.t) - lazy val getIntType: IntType[G] = BinOperatorTypes.getIntType(left.t, right.t) - lazy val getNumericType: Type[G] = BinOperatorTypes .getNumericType(left.t, right.t, o) diff --git a/src/col/vct/col/ast/expr/op/bit/BitAndImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitAndImpl.scala index c90584c2d7..e44876e876 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitAndImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitAndImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitAnd, TInt, Type} +import vct.col.ast.{BitAnd, TCInt, TInt, Type} import vct.col.print._ import vct.col.ast.ops.BitAndOps trait BitAndImpl[G] extends BitAndOps[G] { this: BitAnd[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.BIT_AND override def layout(implicit ctx: Ctx): Doc = lassoc(left, "&", right) diff --git a/src/col/vct/col/ast/expr/op/bit/BitNotImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitNotImpl.scala index 82393b9126..dd943947dc 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitNotImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitNotImpl.scala @@ -8,10 +8,11 @@ import vct.col.ast.ops.BitNotOps trait BitNotImpl[G] extends BitNotOps[G] { this: BitNot[G] => override def t: Type[G] = - if (CoercionUtils.getCoercion(arg.t, TCInt()).isDefined) - TCInt() - else - TInt() + arg.t match { + case cint @ TCInt() => cint + case _ if CoercionUtils.getCoercion(arg.t, TCInt()).isDefined => TCInt() + case _ => TInt() + } override def precedence: Int = Precedence.PREFIX override def layout(implicit ctx: Ctx): Doc = Text("~") <> assoc(arg) diff --git a/src/col/vct/col/ast/expr/op/bit/BitOpImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitOpImpl.scala index d5d4aa9d62..5a53776637 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitOpImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitOpImpl.scala @@ -9,7 +9,7 @@ trait BitOpImpl[G] { if (isBoolOp) TBool() else if (isCIntOp) - TCInt() + getNumericType else TInt() } diff --git a/src/col/vct/col/ast/expr/op/bit/BitOrImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitOrImpl.scala index 78e85a1846..131901c068 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitOrImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitOrImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitOr, TInt, Type} +import vct.col.ast.{BitOr, TCInt, TInt, Type} import vct.col.print.{Ctx, Doc, Precedence} import vct.col.ast.ops.BitOrOps trait BitOrImpl[G] extends BitOrOps[G] { this: BitOr[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.BIT_OR override def layout(implicit ctx: Ctx): Doc = lassoc(left, "|", right) diff --git a/src/col/vct/col/ast/expr/op/bit/BitShlImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitShlImpl.scala index d71d4e2605..cf6e5ddf5b 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitShlImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitShlImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitShl, TInt, Type} +import vct.col.ast.{BitShl, TCInt, TInt, Type} import vct.col.print.{Ctx, Doc, Precedence} import vct.col.ast.ops.BitShlOps trait BitShlImpl[G] extends BitShlOps[G] { this: BitShl[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.SHIFT override def layout(implicit ctx: Ctx): Doc = lassoc(left, "<<", right) diff --git a/src/col/vct/col/ast/expr/op/bit/BitShrImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitShrImpl.scala index 862a6f2d36..affb1d8cd6 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitShrImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitShrImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitShr, TInt, Type} +import vct.col.ast.{BitShr, TCInt, TInt, Type} import vct.col.print.{Ctx, Doc, Precedence} import vct.col.ast.ops.BitShrOps trait BitShrImpl[G] extends BitShrOps[G] { this: BitShr[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.SHIFT override def layout(implicit ctx: Ctx): Doc = lassoc(left, ">>", right) diff --git a/src/col/vct/col/ast/expr/op/bit/BitUShrImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitUShrImpl.scala index 8d99e3f208..8b33c2b06f 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitUShrImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitUShrImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitUShr, TInt, Type} +import vct.col.ast.{BitUShr, TCInt, TInt, Type} import vct.col.print.{Ctx, Doc, Precedence} import vct.col.ast.ops.BitUShrOps trait BitUShrImpl[G] extends BitUShrOps[G] { this: BitUShr[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.SHIFT override def layout(implicit ctx: Ctx): Doc = lassoc(left, ">>>", right) diff --git a/src/col/vct/col/ast/expr/op/bit/BitXorImpl.scala b/src/col/vct/col/ast/expr/op/bit/BitXorImpl.scala index 2eb5d362fa..4feffb451f 100644 --- a/src/col/vct/col/ast/expr/op/bit/BitXorImpl.scala +++ b/src/col/vct/col/ast/expr/op/bit/BitXorImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.expr.op.bit -import vct.col.ast.{BitXor, TInt, Type} +import vct.col.ast.{BitXor, TCInt, TInt, Type} import vct.col.print.{Ctx, Doc, Precedence} import vct.col.ast.ops.BitXorOps trait BitXorImpl[G] extends BitXorOps[G] { this: BitXor[G] => - override def t: Type[G] = getIntType + override def t: Type[G] = + getNumericType match { + case t: TCInt[G] if t.bits.isEmpty && bits != 0 => + t.bits = Some(bits) + t + case t => t + } override def precedence: Int = Precedence.BIT_XOR override def layout(implicit ctx: Ctx): Doc = lassoc(left, "^", right) diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerComparisonImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerComparisonImpl.scala new file mode 100644 index 0000000000..3312d94471 --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerComparisonImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerComparison + +trait PointerComparisonImpl[G] { + this: PointerComparison[G] => + +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerEqImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerEqImpl.scala new file mode 100644 index 0000000000..58cb6324d1 --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerEqImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerEq +import vct.col.ast.ops.PointerEqOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerEqImpl[G] extends PointerEqOps[G] { + this: PointerEq[G] => + override def precedence: Int = Precedence.EQUALITY + override def layout(implicit ctx: Ctx): Doc = lassoc(left, "==", right) +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerGreaterEqImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerGreaterEqImpl.scala new file mode 100644 index 0000000000..8f6f7efcbd --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerGreaterEqImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerGreaterEq +import vct.col.ast.ops.PointerGreaterEqOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerGreaterEqImpl[G] extends PointerGreaterEqOps[G] { + this: PointerGreaterEq[G] => + override def precedence: Int = Precedence.RELATIONAL + override def layout(implicit ctx: Ctx): Doc = lassoc(left, ">=", right) +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerGreaterImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerGreaterImpl.scala new file mode 100644 index 0000000000..9e5bcb2f3d --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerGreaterImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerGreater +import vct.col.ast.ops.PointerGreaterOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerGreaterImpl[G] extends PointerGreaterOps[G] { + this: PointerGreater[G] => + override def precedence: Int = Precedence.RELATIONAL + override def layout(implicit ctx: Ctx): Doc = lassoc(left, ">", right) +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerLessEqImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerLessEqImpl.scala new file mode 100644 index 0000000000..322e8ac0b5 --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerLessEqImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerLessEq +import vct.col.ast.ops.PointerLessEqOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerLessEqImpl[G] extends PointerLessEqOps[G] { + this: PointerLessEq[G] => + override def precedence: Int = Precedence.RELATIONAL + override def layout(implicit ctx: Ctx): Doc = lassoc(left, "<=", right) +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerLessImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerLessImpl.scala new file mode 100644 index 0000000000..d1018f0281 --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerLessImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerLess +import vct.col.ast.ops.PointerLessOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerLessImpl[G] extends PointerLessOps[G] { + this: PointerLess[G] => + override def precedence: Int = Precedence.RELATIONAL + override def layout(implicit ctx: Ctx): Doc = lassoc(left, "<", right) +} diff --git a/src/col/vct/col/ast/expr/op/cmp/PointerNeqImpl.scala b/src/col/vct/col/ast/expr/op/cmp/PointerNeqImpl.scala new file mode 100644 index 0000000000..f52cb36190 --- /dev/null +++ b/src/col/vct/col/ast/expr/op/cmp/PointerNeqImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.expr.op.cmp + +import vct.col.ast.PointerNeq +import vct.col.ast.ops.PointerNeqOps +import vct.col.print.{Ctx, Doc, Precedence} + +trait PointerNeqImpl[G] extends PointerNeqOps[G] { + this: PointerNeq[G] => + override def precedence: Int = Precedence.EQUALITY + override def layout(implicit ctx: Ctx): Doc = lassoc(left, "!=", right) + +} diff --git a/src/col/vct/col/ast/expr/op/num/UMinusImpl.scala b/src/col/vct/col/ast/expr/op/num/UMinusImpl.scala index f3a44e3c11..f03ca142fb 100644 --- a/src/col/vct/col/ast/expr/op/num/UMinusImpl.scala +++ b/src/col/vct/col/ast/expr/op/num/UMinusImpl.scala @@ -20,7 +20,7 @@ trait UMinusImpl[G] extends UMinusOps[G] { override def t: Type[G] = { CoercionUtils.getCoercion(arg.t, TInt()) .orElse(CoercionUtils.getCoercion(arg.t, TRational())) match { - case Some(CoerceCIntInt()) => TCInt() + case Some(CoerceCIntInt(t)) => t case Some(CoerceUnboundInt(TBoundedInt(gte, lt), _)) => TBoundedInt(-lt + 1, -gte + 1) case Some(CoerceFloatRat(source)) => source diff --git a/src/col/vct/col/ast/expr/resource/AssertingImpl.scala b/src/col/vct/col/ast/expr/resource/AssertingImpl.scala new file mode 100644 index 0000000000..1daa8ea363 --- /dev/null +++ b/src/col/vct/col/ast/expr/resource/AssertingImpl.scala @@ -0,0 +1,34 @@ +package vct.col.ast.expr.resource + +import vct.col.ast.node.NodeFamilyImpl +import vct.col.ast.ops.AssertingOps +import vct.col.ast.{Type, Asserting} +import vct.col.print._ + +trait AssertingImpl[G] extends NodeFamilyImpl[G] with AssertingOps[G] { + this: Asserting[G] => + override def t: Type[G] = body.t + + def layoutPVL(implicit ctx: Ctx): Doc = + Group(Text("asserting") <+> condition.show <+> "in" <>> body) + + def layoutSilver(implicit ctx: Ctx): Doc = + Group(Text("asserting") <+> condition.show <+> "in" <>> body) + + def layoutJava(implicit ctx: Ctx): Doc = + Group( + Doc.inlineSpec(Text("\\asserting") <+> condition.show <+> "\\in") <>> body + ) + + def layoutSpec(implicit ctx: Ctx): Doc = + Group(Text("\\asserting") <+> condition.show <+> "\\in" <>> body) + + override def precedence: Int = Precedence.PVL_UNFOLDING + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.PVL => layoutPVL + case Ctx.Silver => layoutSilver + case Ctx.Java => layoutJava + case _ => layoutSpec + } +} diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index a8958f885c..d7baded1ed 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala @@ -83,7 +83,7 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { case CoerceBoundIntFloat(_, _) => false case CoerceCIntCFloat(_) => true - case CoerceCIntInt() => true + case CoerceCIntInt(_) => true case CoerceCFloatFloat(_, _) => true case CoerceDecreasePrecision(_, _) => false case CoerceCFloatCInt(_) => false diff --git a/src/col/vct/col/ast/lang/c/CDeclarationImpl.scala b/src/col/vct/col/ast/lang/c/CDeclarationImpl.scala index c0bf5af319..3e1e161c4f 100644 --- a/src/col/vct/col/ast/lang/c/CDeclarationImpl.scala +++ b/src/col/vct/col/ast/lang/c/CDeclarationImpl.scala @@ -24,6 +24,8 @@ trait CDeclarationImpl[G] Doc.stack(contract.signals), )) + require(true) + override def layout(implicit ctx: Ctx): Doc = Doc.stack(Seq(layoutContract, Group(Doc.spread(specs) <>> Doc.args(inits)))) } diff --git a/src/col/vct/col/ast/lang/c/CPrimitiveTypeImpl.scala b/src/col/vct/col/ast/lang/c/CPrimitiveTypeImpl.scala index 613a7671c7..02dc35924c 100644 --- a/src/col/vct/col/ast/lang/c/CPrimitiveTypeImpl.scala +++ b/src/col/vct/col/ast/lang/c/CPrimitiveTypeImpl.scala @@ -1,10 +1,19 @@ package vct.col.ast.lang.c -import vct.col.ast.CPrimitiveType +import vct.col.ast.{CPrimitiveType, CUnsigned} import vct.col.print.{Ctx, Doc} import vct.col.ast.ops.CPrimitiveTypeOps +import vct.col.resolve.lang.C +import vct.col.typerules.TypeSize trait CPrimitiveTypeImpl[G] extends CPrimitiveTypeOps[G] { this: CPrimitiveType[G] => + override def signed: Boolean = C.isSigned(specifiers) + override def bits: Option[Int] = C.getIntSize(C.LP64, specifiers) + + // TODO: Parameterize on target + override def byteSize: TypeSize = + C.getIntSize(C.LP64, specifiers).map(n => TypeSize.Exact(n / 8)) + .getOrElse(TypeSize.Unknown()) override def layout(implicit ctx: Ctx): Doc = Doc.spread(specifiers) } diff --git a/src/col/vct/col/ast/lang/c/CTArrayImpl.scala b/src/col/vct/col/ast/lang/c/CTArrayImpl.scala index e9e1f5b4ef..9d7fce8b90 100644 --- a/src/col/vct/col/ast/lang/c/CTArrayImpl.scala +++ b/src/col/vct/col/ast/lang/c/CTArrayImpl.scala @@ -3,9 +3,12 @@ package vct.col.ast.lang.c import vct.col.ast.CTArray import vct.col.print.{Ctx, Doc, Group} import vct.col.ast.ops.CTArrayOps +import vct.col.typerules.TypeSize trait CTArrayImpl[G] extends CTArrayOps[G] { this: CTArray[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(8)) override def layout(implicit ctx: Ctx): Doc = Group(innerType.show <> "[" <> Doc.args(size.toSeq) <> "]") } diff --git a/src/col/vct/col/ast/lang/c/CTPointerImpl.scala b/src/col/vct/col/ast/lang/c/CTPointerImpl.scala index 233f297193..56f844cb40 100644 --- a/src/col/vct/col/ast/lang/c/CTPointerImpl.scala +++ b/src/col/vct/col/ast/lang/c/CTPointerImpl.scala @@ -3,9 +3,12 @@ package vct.col.ast.lang.c import vct.col.ast.CTPointer import vct.col.print.{Ctx, Doc, Text} import vct.col.ast.ops.CTPointerOps +import vct.col.typerules.TypeSize trait CTPointerImpl[G] extends CTPointerOps[G] { this: CTPointer[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(8)) override def layout(implicit ctx: Ctx): Doc = Text("pointer") <> open <> innerType <> close } diff --git a/src/col/vct/col/ast/lang/sycl/SYCLTAccessorImpl.scala b/src/col/vct/col/ast/lang/sycl/SYCLTAccessorImpl.scala index 5d29ff9d4e..d35416b086 100644 --- a/src/col/vct/col/ast/lang/sycl/SYCLTAccessorImpl.scala +++ b/src/col/vct/col/ast/lang/sycl/SYCLTAccessorImpl.scala @@ -35,7 +35,7 @@ trait SYCLTAccessorImpl[G] extends SYCLTAccessorOps[G] { genericArgs match { case Seq( CPPExprOrTypeSpecifier(None, Some(typeSpec)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), CPPExprOrTypeSpecifier( None, Some(SYCLClassDefName("access_mode::read_write", Nil)), @@ -55,7 +55,7 @@ trait SYCLTAccessorImpl[G] extends SYCLTAccessorOps[G] { Some(RefSYCLConstructorDefinition(SYCLTAccessor(typ, dimCount))) case Seq( CPPExprOrTypeSpecifier(None, Some(typeSpec)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), CPPExprOrTypeSpecifier( None, Some(SYCLClassDefName("access_mode::read", Nil)), @@ -77,7 +77,7 @@ trait SYCLTAccessorImpl[G] extends SYCLTAccessorOps[G] { )) case Seq( CPPExprOrTypeSpecifier(None, Some(typeSpec)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), ) if dim > 0 && dim <= 3 && Util.compatTypes[G]( args, diff --git a/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala b/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala index 0b09c49414..6e7a9bc252 100644 --- a/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala +++ b/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala @@ -33,7 +33,7 @@ trait SYCLTBufferImpl[G] extends SYCLTBufferOps[G] { genericArgs match { case Seq( CPPExprOrTypeSpecifier(None, Some(typeSpec)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), ) if dim > 0 && dim <= 3 && args.nonEmpty && args.head.t.asPointer.isDefined && diff --git a/src/col/vct/col/ast/lang/sycl/SYCLTLocalAccessorImpl.scala b/src/col/vct/col/ast/lang/sycl/SYCLTLocalAccessorImpl.scala index 204e3cdb22..317dfab904 100644 --- a/src/col/vct/col/ast/lang/sycl/SYCLTLocalAccessorImpl.scala +++ b/src/col/vct/col/ast/lang/sycl/SYCLTLocalAccessorImpl.scala @@ -23,7 +23,7 @@ trait SYCLTLocalAccessorImpl[G] extends SYCLTLocalAccessorOps[G] { genericArgs match { case Seq( CPPExprOrTypeSpecifier(None, Some(typeSpec)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), ) if dim > 0 && dim <= 3 && Util.compatTypes[G]( args, diff --git a/src/col/vct/col/ast/lang/sycl/SYCLTNDRangeImpl.scala b/src/col/vct/col/ast/lang/sycl/SYCLTNDRangeImpl.scala index af20baed47..2d89608fcc 100644 --- a/src/col/vct/col/ast/lang/sycl/SYCLTNDRangeImpl.scala +++ b/src/col/vct/col/ast/lang/sycl/SYCLTNDRangeImpl.scala @@ -18,7 +18,7 @@ trait SYCLTNDRangeImpl[G] extends SYCLTNDRangeOps[G] { args: Seq[Expr[G]], ): Option[CPPInvocationTarget[G]] = genericArgs match { - case Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None)) + case Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None)) if dim > 0 && dim <= 3 && Util.compatTypes( args, Seq(SYCLTRange[G](dim.toInt), SYCLTRange[G](dim.toInt)), diff --git a/src/col/vct/col/ast/lang/sycl/SYCLTRangeImpl.scala b/src/col/vct/col/ast/lang/sycl/SYCLTRangeImpl.scala index 11dcd9c241..7da7416af3 100644 --- a/src/col/vct/col/ast/lang/sycl/SYCLTRangeImpl.scala +++ b/src/col/vct/col/ast/lang/sycl/SYCLTRangeImpl.scala @@ -18,7 +18,7 @@ trait SYCLTRangeImpl[G] extends SYCLTRangeOps[G] { args: Seq[Expr[G]], ): Option[CPPInvocationTarget[G]] = genericArgs match { - case Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None)) + case Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None)) if dim > 0 && dim <= 3 && Util.compatTypes( args, Seq.range(0, dim.toInt).map(_ => TCInt[G]()), diff --git a/src/col/vct/col/ast/type/TBoolImpl.scala b/src/col/vct/col/ast/type/TBoolImpl.scala index b12a553cb0..fc5cceae9b 100644 --- a/src/col/vct/col/ast/type/TBoolImpl.scala +++ b/src/col/vct/col/ast/type/TBoolImpl.scala @@ -3,9 +3,12 @@ package vct.col.ast.`type` import vct.col.ast.TBool import vct.col.print.{Ctx, Doc, Text} import vct.col.ast.ops.TBoolOps +import vct.col.typerules.TypeSize trait TBoolImpl[G] extends TBoolOps[G] { this: TBool[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(1)) override def layout(implicit ctx: Ctx): Doc = ctx.syntax match { case Ctx.PVL => Text("boolean") diff --git a/src/col/vct/col/ast/type/TByValueClassImpl.scala b/src/col/vct/col/ast/type/TByValueClassImpl.scala index 0f8e0f6bdc..1a83cf89e1 100644 --- a/src/col/vct/col/ast/type/TByValueClassImpl.scala +++ b/src/col/vct/col/ast/type/TByValueClassImpl.scala @@ -1,8 +1,18 @@ package vct.col.ast.`type` -import vct.col.ast.TByValueClass +import vct.col.ast.{ByValueClass, InstanceField, TByValueClass} import vct.col.ast.ops.TByValueClassOps +import vct.col.typerules.TypeSize trait TByValueClassImpl[G] extends TByValueClassOps[G] { this: TByValueClass[G] => + + override def byteSize: TypeSize = { + val sizes = cls.decl.decls.collect { case field: InstanceField[G] => + field.t.byteSize + } + if (cls.decl.asInstanceOf[ByValueClass[G]].packed) { + TypeSize.packed(sizes: _*) + } else { TypeSize.struct(sizes: _*) } + } } diff --git a/src/col/vct/col/ast/type/TCIntImpl.scala b/src/col/vct/col/ast/type/TCIntImpl.scala index ffda4c52f0..0f568482c8 100644 --- a/src/col/vct/col/ast/type/TCIntImpl.scala +++ b/src/col/vct/col/ast/type/TCIntImpl.scala @@ -3,8 +3,12 @@ package vct.col.ast.`type` import vct.col.ast.TCInt import vct.col.print.{Ctx, Doc, Text} import vct.col.ast.ops.TCIntOps +import vct.col.typerules.TypeSize trait TCIntImpl[G] extends TCIntOps[G] { this: TCInt[G] => + override def byteSize: TypeSize = + bits.map(b => TypeSize.Exact(b / 8)).getOrElse(TypeSize.Unknown()) + override def layout(implicit ctx: Ctx): Doc = Text("int") } diff --git a/src/col/vct/col/ast/type/TCharImpl.scala b/src/col/vct/col/ast/type/TCharImpl.scala index 5e0b428326..d4abadc59e 100644 --- a/src/col/vct/col/ast/type/TCharImpl.scala +++ b/src/col/vct/col/ast/type/TCharImpl.scala @@ -3,8 +3,11 @@ package vct.col.ast.`type` import vct.col.ast.TChar import vct.col.print.{Ctx, Doc, Group, Text} import vct.col.ast.ops.TCharOps +import vct.col.typerules.TypeSize trait TCharImpl[G] extends TCharOps[G] { this: TChar[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(1)) override def layout(implicit ctx: Ctx): Doc = Text("char") } diff --git a/src/col/vct/col/ast/type/TFloatImpl.scala b/src/col/vct/col/ast/type/TFloatImpl.scala index 7b9430b0af..205d81ee9c 100644 --- a/src/col/vct/col/ast/type/TFloatImpl.scala +++ b/src/col/vct/col/ast/type/TFloatImpl.scala @@ -1,12 +1,18 @@ package vct.col.ast.`type` import vct.col.ast.TFloat -import vct.col.ast import vct.col.ast.ops.TFloatOps import vct.col.ast.`type`.typeclass.TFloats +import vct.col.typerules.TypeSize trait TFloatImpl[G] extends TFloatOps[G] { this: TFloat[G] => + // TODO: Should this be Minimally? + override def byteSize: TypeSize = + TypeSize.Exact(BigInt.int2bigInt( + Math.ceil((exponent + mantissa).asInstanceOf[Double] / 8.0) + .asInstanceOf[Int] + )) override def is_ieee754_32bit: Boolean = this == TFloats.ieee754_32bit override def is_ieee754_64bit: Boolean = this == TFloats.ieee754_64bit diff --git a/src/col/vct/col/ast/type/TNonNullPointerImpl.scala b/src/col/vct/col/ast/type/TNonNullPointerImpl.scala index cd769efa94..4e89c49cfb 100644 --- a/src/col/vct/col/ast/type/TNonNullPointerImpl.scala +++ b/src/col/vct/col/ast/type/TNonNullPointerImpl.scala @@ -3,9 +3,12 @@ package vct.col.ast.`type` import vct.col.ast.TNonNullPointer import vct.col.ast.ops.TNonNullPointerOps import vct.col.print._ +import vct.col.typerules.TypeSize trait TNonNullPointerImpl[G] extends TNonNullPointerOps[G] { this: TNonNullPointer[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(8)) override def layoutSplitDeclarator(implicit ctx: Ctx): (Doc, Doc) = { val (spec, decl) = element.layoutSplitDeclarator (spec, decl <> "*") diff --git a/src/col/vct/col/ast/type/TPointerBlockImpl.scala b/src/col/vct/col/ast/type/TPointerBlockImpl.scala new file mode 100644 index 0000000000..76f43a4397 --- /dev/null +++ b/src/col/vct/col/ast/type/TPointerBlockImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.`type` + +import vct.col.ast.TPointerBlock +import vct.col.ast.ops.TPointerBlockOps +import vct.col.print._ +import vct.col.typerules.TypeSize + +trait TPointerBlockImpl[G] extends TPointerBlockOps[G] { + this: TPointerBlock[G] => + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(8)) + + override def layout(implicit ctx: Ctx): Doc = Text("`block`") +} diff --git a/src/col/vct/col/ast/type/TPointerImpl.scala b/src/col/vct/col/ast/type/TPointerImpl.scala index f0a5302b3c..3a7ce74b0e 100644 --- a/src/col/vct/col/ast/type/TPointerImpl.scala +++ b/src/col/vct/col/ast/type/TPointerImpl.scala @@ -3,9 +3,14 @@ package vct.col.ast.`type` import vct.col.ast.TPointer import vct.col.print._ import vct.col.ast.ops.TPointerOps +import vct.col.typerules.TypeSize trait TPointerImpl[G] extends TPointerOps[G] { this: TPointer[G] => + + // TODO: Parameterize on target + override def byteSize: TypeSize = TypeSize.Exact(BigInt.int2bigInt(8)) + override def layoutSplitDeclarator(implicit ctx: Ctx): (Doc, Doc) = { val (spec, decl) = element.layoutSplitDeclarator (spec, decl <> "*") diff --git a/src/col/vct/col/ast/type/typeclass/BitwiseTypeImpl.scala b/src/col/vct/col/ast/type/typeclass/BitwiseTypeImpl.scala new file mode 100644 index 0000000000..f73b48edaf --- /dev/null +++ b/src/col/vct/col/ast/type/typeclass/BitwiseTypeImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.`type`.typeclass + +import vct.col.ast.BitwiseType + +trait BitwiseTypeImpl[G] { + this: BitwiseType[G] => + + def signed: Boolean + def bits: Option[Int] +} diff --git a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala index 3d9fd87c0c..c5f853936a 100644 --- a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala +++ b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala @@ -4,13 +4,15 @@ import vct.col.ast._ import vct.col.check.{CheckContext, CheckError} import vct.col.ref.Ref import vct.col.rewrite.NonLatchingRewriter -import vct.col.typerules.CoercionUtils +import vct.col.typerules.{CoercionUtils, TypeSize} import vct.col.print._ import vct.col.ast.ops.TypeFamilyOps import vct.col.util.IdentitySuccessorsProvider trait TypeImpl[G] extends TypeFamilyOps[G] { this: Type[G] => + def byteSize: TypeSize = TypeSize.Unknown() + def superTypeOf(other: Type[G]): Boolean = CoercionUtils.getCoercion(other, this).isDefined diff --git a/src/col/vct/col/ast/unsorted/AssumingImpl.scala b/src/col/vct/col/ast/unsorted/AssumingImpl.scala new file mode 100644 index 0000000000..30de2cafe9 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/AssumingImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.unsorted + +import vct.col.ast.{Assuming, Type} +import vct.col.print._ +import vct.col.ast.ops.AssumingOps + +trait AssumingImpl[G] extends AssumingOps[G] { + this: Assuming[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? + override def t: Type[G] = inner.t +} diff --git a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala index 97ef481a94..a59db8998c 100644 --- a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala +++ b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala @@ -137,7 +137,7 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) { } yield i1 % i2 case UMinus(e1) => for { i1 <- isConstantIntRecurse(e1) } yield -i1 - case BitAnd(e1, e2) => + case BitAnd(e1, e2, _, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 & i2 @@ -149,7 +149,7 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) { for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 & i2 - case BitOr(e1, e2) => + case BitOr(e1, e2, _, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 | i2 @@ -161,7 +161,7 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) { for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 | i2 - case BitXor(e1, e2) => + case BitXor(e1, e2, _, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 ^ i2 @@ -173,15 +173,15 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) { for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 ^ i2 - case BitShl(e1, e2) => + case BitShl(e1, e2, _, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 << i2.toInt - case BitShr(e1, e2) => + case BitShr(e1, e2, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1 >> i2.toInt - case BitUShr(e1, e2) => + case BitUShr(e1, e2, _, _) => for { i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2) } yield i1.toInt >>> i2.toInt @@ -388,11 +388,11 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) { // Commutative operators case (lhs @ Plus(_, _), rhs @ Plus(_, _)) => commAssoc[Plus[G]](lhs, rhs) case (lhs @ Mult(_, _), rhs @ Mult(_, _)) => commAssoc[Mult[G]](lhs, rhs) - case (BitAnd(lhs1, lhs2), BitAnd(rhs1, rhs2)) => + case (BitAnd(lhs1, lhs2, _, _), BitAnd(rhs1, rhs2, _, _)) => comm(lhs1, lhs2, rhs1, rhs2) - case (BitOr(lhs1, lhs2), BitOr(rhs1, rhs2)) => + case (BitOr(lhs1, lhs2, _, _), BitOr(rhs1, rhs2, _, _)) => comm(lhs1, lhs2, rhs1, rhs2) - case (BitXor(lhs1, lhs2), BitXor(rhs1, rhs2)) => + case (BitXor(lhs1, lhs2, _, _), BitXor(rhs1, rhs2, _, _)) => comm(lhs1, lhs2, rhs1, rhs2) case (And(lhs1, lhs2), And(rhs1, rhs2)) => comm(lhs1, lhs2, rhs1, rhs2) case (Or(lhs1, lhs2), Or(rhs1, rhs2)) => comm(lhs1, lhs2, rhs1, rhs2) diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index cf7431a270..90a4bf92bf 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -183,7 +183,7 @@ case class CopyClassFailedBeforeCall( s"Insufficient permission for call `$source`." } -case class AssertFailed(failure: ContractFailure, node: Assert[_]) +case class AssertFailed(failure: ContractFailure, node: Node[_]) extends WithContractFailure { override def baseCode: String = "assertFailed" override def descInContext: String = "Assertion may not hold, since" @@ -999,6 +999,16 @@ case class ArrayValuesPerm(node: Values[_]) extends ArrayValuesError { "there may be insufficient permission to access the array at the specified range" } +// TODO: Signed-ness +case class IntegerOutOfBounds(node: Node[_], bits: Int) + extends NodeVerificationFailure { + override def code: String = "intBounds" + override def descInContext: String = + s"Integer may be out of bounds, expected a `$bits`-bit integer" + override def inlineDescWithSource(source: String) = + s"Integer `$source` may be out of bounds, expected a `$bits`-bit integer" +} + sealed trait PointerSubscriptError extends FrontendSubscriptError sealed trait PointerDerefError extends PointerSubscriptError with FrontendDerefError @@ -1536,6 +1546,9 @@ object NonNullPointerNull object UnsafeDontCare { case class Satisfiability(reason: String) extends UnsafeDontCare[NontrivialUnsatisfiable] + case class Contract(reason: String) extends UnsafeDontCare[ContractedFailure] + case class Invocation(reason: String) + extends UnsafeDontCare[InvocationFailure] } trait UnsafeDontCare[T <: VerificationFailure] diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 720f63286e..2ea121d69b 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -7,7 +7,7 @@ import vct.col.ast.util.ExpressionEqualityCheck.isConstantInt import vct.col.origin._ import vct.col.resolve._ import vct.col.resolve.ctx._ -import vct.col.typerules.Types +import vct.col.typerules.{TypeSize, Types} import vct.result.VerificationError.UserError case object C { @@ -30,13 +30,32 @@ case object C { ) val INTEGER_LIKE_TYPES: Seq[Seq[CDeclarationSpecifier[_]]] = Seq( + Seq(CChar()), + Seq(CSigned(), CChar()), + Seq(CUnsigned(), CChar()), Seq(CShort()), + Seq(CSigned(), CShort()), + Seq(CUnsigned(), CShort()), Seq(CShort(), CInt()), + Seq(CSigned(), CShort(), CInt()), + Seq(CUnsigned(), CShort(), CInt()), Seq(CInt()), + Seq(CSigned()), + Seq(CUnsigned()), + Seq(CSigned(), CInt()), + Seq(CUnsigned(), CInt()), Seq(CLong()), + Seq(CSigned(), CLong()), + Seq(CUnsigned(), CLong()), Seq(CLong(), CInt()), + Seq(CSigned(), CLong(), CInt()), + Seq(CUnsigned(), CLong(), CInt()), Seq(CLong(), CLong()), + Seq(CSigned(), CLong(), CLong()), + Seq(CUnsigned(), CLong(), CLong()), Seq(CLong(), CLong(), CInt()), + Seq(CSigned(), CLong(), CLong(), CInt()), + Seq(CUnsigned(), CLong(), CLong(), CInt()), ) // See here for more discussion https://github.com/utwente-fmt/vercors/discussions/1018#discussioncomment-5966388 @@ -45,20 +64,96 @@ case object C { case object LP64 extends DataModel case object LLP64 extends DataModel - def INT_TYPE_TO_SIZE(dm: DataModel): Map[Seq[CDeclarationSpecifier[_]], Int] = + def INT_TYPE_TO_SIZE( + dm: DataModel + ): Map[Seq[CDeclarationSpecifier[_]], Int] = { + val longSize = + (if (dm == LP64) + 64 + else + 32) Map( + (Seq(CChar()) -> 8), + (Seq(CSigned(), CChar()) -> 8), + (Seq(CUnsigned(), CChar()) -> 8), (Seq(CShort()) -> 16), + (Seq(CSigned(), CShort()) -> 16), + (Seq(CUnsigned(), CShort()) -> 16), (Seq(CShort(), CInt()) -> 16), + (Seq(CSigned(), CShort(), CInt()) -> 16), + (Seq(CUnsigned(), CShort(), CInt()) -> 16), (Seq(CInt()) -> 32), - (Seq(CLong()) -> 64), - (Seq(CLong(), CInt()) -> - (if (dm == LP64) - 64 - else - 32)), + (Seq(CSigned()) -> 32), + (Seq(CUnsigned()) -> 32), + (Seq(CSigned(), CInt()) -> 32), + (Seq(CUnsigned(), CInt()) -> 32), + (Seq(CLong()) -> longSize), + (Seq(CSigned(), CLong()) -> longSize), + (Seq(CUnsigned(), CLong()) -> longSize), + (Seq(CLong(), CInt()) -> longSize), + (Seq(CSigned(), CLong(), CInt()) -> longSize), + (Seq(CUnsigned(), CLong(), CInt()) -> longSize), (Seq(CLong(), CLong()) -> 64), + (Seq(CSigned(), CLong(), CLong()) -> 64), + (Seq(CUnsigned(), CLong(), CLong()) -> 64), (Seq(CLong(), CLong(), CInt()) -> 64), + (Seq(CSigned(), CLong(), CLong(), CInt()) -> 64), + (Seq(CUnsigned(), CLong(), CLong(), CInt()) -> 64), + ) + } + + def getIntSize( + dm: DataModel, + specs: Seq[CDeclarationSpecifier[_]], + ): Option[Int] = { + specs.collectFirst { case CSpecificationType(t) => t.byteSize }.collect { + case TypeSize.Exact(size) => size.intValue * 8 + }.orElse(INT_TYPE_TO_SIZE(dm).get(specs.flatMap(_ match { + // Inline/Pure + case _: CSpecificationModifier[_] => Nil + // Extern/static/typedef/... + case _: CStorageClassSpecifier[_] => Nil + // Actual types + case specifier: CTypeSpecifier[_] => + specifier match { + case CVoid() | CChar() | CShort() | CInt() | CLong() | CFloat() | + CDouble() | CSigned() | CUnsigned() | CBool() | + CTypedefName(_) | CFunctionTypeExtensionModifier(_) | + CStructDeclaration(_, _) | CStructSpecifier(_) => + Seq(specifier) + } + // Const/restrict/volatile/... + case CTypeQualifierDeclarationSpecifier(_) => Nil + case _: CFunctionSpecifier[_] => Nil + case _: CAlignmentSpecifier[_] => Nil + case _: CGpgpuKernelSpecifier[_] => Nil + }))) + } + + // XXX: We assume that everything's signed unless specified otherwise, this is not actually defined in the spec though + def isSigned(specs: Seq[CDeclarationSpecifier[_]]): Boolean = { + specs.collectFirst { case CSpecificationType(t: BitwiseType[_]) => + t.signed + }.getOrElse( + specs.map { + case _: CSpecificationModifier[_] => true + case _: CStorageClassSpecifier[_] => true + case specifier: CTypeSpecifier[_] => + specifier match { + case CUnsigned() => false + case CSpecificationType(_) | CVoid() | CChar() | + CShort() | CInt() | CLong() | CFloat() | CDouble() | CSigned() | + CBool() | CTypedefName(_) | CFunctionTypeExtensionModifier(_) | + CStructDeclaration(_, _) | CStructSpecifier(_) => + true + } + case CTypeQualifierDeclarationSpecifier(_) => true + case _: CFunctionSpecifier[_] => true + case _: CAlignmentSpecifier[_] => true + case _: CGpgpuKernelSpecifier[_] => true + }.reduce(_ && _) ) + } case class DeclaratorInfo[G]( params: Option[Seq[CParam[G]]], @@ -171,10 +266,11 @@ case object C { val t: Type[G] = filteredSpecs match { case Seq(CVoid()) => TVoid() - case Seq(CChar()) => TChar() - case CUnsigned() +: t if INTEGER_LIKE_TYPES.contains(t) => TCInt() - case CSigned() +: t if INTEGER_LIKE_TYPES.contains(t) => TCInt() - case t if C.INTEGER_LIKE_TYPES.contains(t) => TCInt() + case t if C.INTEGER_LIKE_TYPES.contains(t) => + val cint = TCInt[G]() + cint.bits = getIntSize(LP64, specs) + cint.signed = isSigned(specs) + cint case Seq(CFloat()) => C_ieee754_32bit() case Seq(CDouble()) => C_ieee754_64bit() case Seq(CLong(), CDouble()) => C_ieee754_64bit() diff --git a/src/col/vct/col/resolve/lang/CPP.scala b/src/col/vct/col/resolve/lang/CPP.scala index 515eb67262..9bb5d25d62 100644 --- a/src/col/vct/col/resolve/lang/CPP.scala +++ b/src/col/vct/col/resolve/lang/CPP.scala @@ -107,7 +107,11 @@ case object CPP { specs.collect { case spec: CPPTypeSpecifier[G] => spec } match { case Seq(CPPVoid()) => TVoid() case Seq(CPPChar()) => TChar() - case t if CPP.NUMBER_LIKE_SPECIFIERS.contains(t) => TCInt() + case t if CPP.NUMBER_LIKE_SPECIFIERS.contains(t) => { + val cint = TCInt[G]() + cint.signed = isSigned(specs); + cint + } case Seq(CPPSpecificationType(t @ TCFloat(_, _))) => t case Seq(CPPBool()) => TBool() case Seq(SYCLClassDefName("event", Seq())) => SYCLTEvent() @@ -116,7 +120,7 @@ case object CPP { case Seq( SYCLClassDefName( name, - Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None)), + Seq(CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None)), ) ) => name match { @@ -131,7 +135,7 @@ case object CPP { name, Seq( CPPExprOrTypeSpecifier(None, Some(typ)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), ), ) ) => @@ -147,7 +151,7 @@ case object CPP { "accessor", Seq( CPPExprOrTypeSpecifier(None, Some(typ)), - CPPExprOrTypeSpecifier(Some(CIntegerValue(dim)), None), + CPPExprOrTypeSpecifier(Some(CIntegerValue(dim, _)), None), CPPExprOrTypeSpecifier( None, Some(SYCLClassDefName(accessMode, Nil)), @@ -170,6 +174,10 @@ case object CPP { case _ => throw CPPTypeNotSupported(context) } + // XXX: We assume that everything's signed unless specified otherwise, this is not actually defined in the spec though + def isSigned(specs: Seq[CPPDeclarationSpecifier[_]]): Boolean = + specs.collect { case t: CPPTypeSpecifier[_] => t }.contains(CPPUnsigned()) + def unwrappedType[G](t: Type[G]): Type[G] = t match { case CPPPrimitiveType(specs) => getBaseTypeFromSpecs(specs) diff --git a/src/col/vct/col/serialize/SerializeOrigin.scala b/src/col/vct/col/serialize/SerializeOrigin.scala index 027e88bc1e..ef3c068850 100644 --- a/src/col/vct/col/serialize/SerializeOrigin.scala +++ b/src/col/vct/col/serialize/SerializeOrigin.scala @@ -95,9 +95,13 @@ object SerializeOrigin extends LazyLogging { ) case ReadableOrigin(readable) => // Not sure how to best deal with directory/filename here - Seq(ser.OriginContent.Content.ReadableOrigin( - ser.ReadableOrigin("", readable.fileName, None, None) - )) + Seq(ser.OriginContent.Content.ReadableOrigin(ser.ReadableOrigin( + "", + readable.underlyingPath.map(_.toString) + .getOrElse(readable.fileName), + None, + None, + ))) case PositionRange(startLineIdx, endLineIdx, startEndColIdx) => Seq(ser.OriginContent.Content.PositionRange(ser.PositionRange( startLineIdx, diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index bd2749d87c..14d3402675 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -302,7 +302,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceDecreasePrecision(_, _) => e case CoerceCFloatCInt(_) => e case CoerceCIntCFloat(_) => e - case CoerceCIntInt() => e + case CoerceCIntInt(_) => e case CoerceCFloatFloat(_, _) => e case CoerceLLVMIntInt() => e @@ -808,7 +808,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case g @ AmbiguousGreater(left, right) => firstOk( e, - s"Expected both operands to be numeric, a set, or a bag, but got ${left + s"Expected both operands to be numeric, a set, a bag, or a pointer but got ${left .t} and ${right.t}.", AmbiguousGreater(int(left), int(right)), floatOp2(g, (l, r) => AmbiguousGreater(l, r)), @@ -831,11 +831,12 @@ abstract class CoercingRewriter[Pre <: Generation]() coerce(coercedRight, TBag(sharedType)), ) }, + AmbiguousGreater(pointer(left)._1, pointer(right)._1), ) case g @ AmbiguousGreaterEq(left, right) => firstOk( e, - s"Expected both operands to be numeric, a set, or a bag, but got ${left + s"Expected both operands to be numeric, a set, a bag, or a pointer but got ${left .t} and ${right.t}.", AmbiguousGreaterEq(int(left), int(right)), floatOp2(g, (l, r) => AmbiguousGreaterEq(l, r)), @@ -858,14 +859,15 @@ abstract class CoercingRewriter[Pre <: Generation]() coerce(coercedRight, TBag(sharedType)), ) }, + AmbiguousGreaterEq(pointer(left)._1, pointer(right)._1), ) - case l @ AmbiguousLess(left, right) => + case less @ AmbiguousLess(left, right) => firstOk( e, - s"Expected both operands to be numeric, a set, or a bag, but got ${left + s"Expected both operands to be numeric, a set, a bag, or a pointer but got ${left .t} and ${right.t}.", AmbiguousLess(int(left), int(right)), - floatOp2(l, (l, r) => AmbiguousLess(l, r)), + floatOp2(less, (l, r) => AmbiguousLess(l, r)), AmbiguousLess(rat(left), rat(right)), { val (coercedLeft, leftSet) = set(left) val (coercedRight, rightSet) = set(right) @@ -885,14 +887,15 @@ abstract class CoercingRewriter[Pre <: Generation]() coerce(coercedRight, TBag(sharedType)), ) }, + AmbiguousLess(pointer(left)._1, pointer(right)._1), ) - case l @ AmbiguousLessEq(left, right) => + case less @ AmbiguousLessEq(left, right) => firstOk( e, - s"Expected both operands to be numeric, a set, or a bag, but got ${left + s"Expected both operands to be numeric, a set, a bag, or a pointer but got ${left .t} and ${right.t}.", AmbiguousLessEq(int(left), int(right)), - floatOp2(l, (l, r) => AmbiguousLessEq(l, r)), + floatOp2(less, (l, r) => AmbiguousLessEq(l, r)), AmbiguousLessEq(rat(left), rat(right)), { val (coercedLeft, leftSet) = set(left) val (coercedRight, rightSet) = set(right) @@ -912,6 +915,7 @@ abstract class CoercingRewriter[Pre <: Generation]() coerce(coercedRight, TBag(sharedType)), ) }, + AmbiguousLessEq(pointer(left)._1, pointer(right)._1), ) case minus @ AmbiguousMinus(left, right) => firstOk( @@ -1160,13 +1164,20 @@ abstract class CoercingRewriter[Pre <: Generation]() ) case bgi @ BipGuardInvocation(obj, ref) => BipGuardInvocation(cls(obj), ref) - case BitAnd(left, right) => BitAnd(int(left), int(right)) - case BitNot(arg) => BitNot(int(arg)) - case BitOr(left, right) => BitOr(int(left), int(right)) - case BitShl(left, right) => BitShl(int(left), int(right)) - case BitShr(left, right) => BitShr(int(left), int(right)) - case BitUShr(left, right) => BitUShr(int(left), int(right)) - case BitXor(left, right) => BitXor(int(left), int(right)) + case op @ BitAnd(left, right, bits, signed) => + BitAnd(int(left), int(right), bits, signed)(op.blame) + case op @ BitNot(arg, bits, signed) => + BitNot(int(arg), bits, signed)(op.blame) + case op @ BitOr(left, right, bits, signed) => + BitOr(int(left), int(right), bits, signed)(op.blame) + case op @ BitShl(left, right, bits, signed) => + BitShl(int(left), int(right), bits, signed)(op.blame) + case op @ BitShr(left, right, bits) => + BitShr(int(left), int(right), bits)(op.blame) + case op @ BitUShr(left, right, bits, signed) => + BitUShr(int(left), int(right), bits, signed)(op.blame) + case op @ BitXor(left, right, bits, signed) => + BitXor(int(left), int(right), bits, signed)(op.blame) case Cast(value, typeValue) => Cast(value, typeValue) case CastFloat(e, t) => firstOk( @@ -1602,6 +1613,8 @@ abstract class CoercingRewriter[Pre <: Generation]() ) case add @ PointerAdd(p, offset) => PointerAdd(pointer(p)._1, int(offset))(add.blame) + case blck @ PointerBlock(p) => PointerBlock(pointer(p)._1)(blck.blame) + case addr @ PointerAddress(p) => PointerAddress(pointer(p)._1)(addr.blame) case len @ PointerBlockLength(p) => PointerBlockLength(pointer(p)._1)(len.blame) case off @ PointerBlockOffset(p) => @@ -1609,6 +1622,13 @@ abstract class CoercingRewriter[Pre <: Generation]() case len @ PointerLength(p) => PointerLength(pointer(p)._1)(len.blame) case get @ PointerSubscript(p, index) => PointerSubscript(pointer(p)._1, int(index))(get.blame) + case PointerEq(l, r) => PointerEq(pointer(l)._1, pointer(r)._1) + case PointerNeq(l, r) => PointerNeq(pointer(l)._1, pointer(r)._1) + case PointerGreater(l, r) => PointerGreater(pointer(l)._1, pointer(r)._1) + case PointerLess(l, r) => PointerLess(pointer(l)._1, pointer(r)._1) + case PointerGreaterEq(l, r) => + PointerGreaterEq(pointer(l)._1, pointer(r)._1) + case PointerLessEq(l, r) => PointerLessEq(pointer(l)._1, pointer(r)._1) case PointsTo(loc, perm, value) => PointsTo(loc, rat(perm), coerce(value, loc.t)) case PolarityDependent(onInhale, onExhale) => @@ -1976,6 +1996,9 @@ abstract class CoercingRewriter[Pre <: Generation]() UMinus(rat(arg)), ) case u @ Unfolding(pred, body) => Unfolding(pred, body)(u.blame) + case a @ Asserting(condition, body) => + Asserting(res(condition), body)(a.blame) + case Assuming(assn, inner) => Assuming(bool(assn), inner) case UntypedLiteralBag(values) => val sharedType = Types.leastCommonSuperType(values.map(_.t)) UntypedLiteralBag(values.map(coerce(_, sharedType))) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index d03d6d8ebd..e1f70f9553 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -198,7 +198,7 @@ case object CoercionUtils { CoerceDecreasePrecision(source, coercedCFloat), CoerceCFloatFloat(coercedCFloat, target), )) - case (TCInt(), TInt()) => CoerceCIntInt() + case (TCInt(), TInt()) => CoerceCIntInt(source) case (LLVMTInt(_), TInt()) => CoerceLLVMIntInt() case (TInt(), LLVMTInt(_)) => CoerceIdentity(target) case (l @ LLVMTFloat(_), TFloat(mantissa, exponent)) @@ -264,7 +264,7 @@ case object CoercionUtils { case (TCInt(), target @ TCFloat(_, _)) => CoerceCIntCFloat(target) case (source @ TCFloat(_, _), TInt()) => - CoercionSequence(Seq(CoerceCFloatCInt(source), CoerceCIntInt())) + CoercionSequence(Seq(CoerceCFloatCInt(source), CoerceCIntInt(TCInt()))) case (TCInt(), target @ TFloat(exponent, mantissa)) => val coercedCFloat = TCFloat[G](exponent, mantissa) CoercionSequence(Seq( diff --git a/src/col/vct/col/typerules/TypeSize.scala b/src/col/vct/col/typerules/TypeSize.scala new file mode 100644 index 0000000000..fbfe4293f6 --- /dev/null +++ b/src/col/vct/col/typerules/TypeSize.scala @@ -0,0 +1,27 @@ +package vct.col.typerules + +case object TypeSize { + case class Unknown() extends TypeSize + case class Exact(size: BigInt) extends TypeSize + case class Minimally(size: BigInt) extends TypeSize + + def struct(sizes: TypeSize*): TypeSize = + sizes.reduce[TypeSize] { + case (Unknown(), _) | (_, Unknown()) => Unknown() + case (Minimally(a), Minimally(b)) => Minimally(a + b) + case (Minimally(a), Exact(b)) => Minimally(a + b) + case (Exact(a), Minimally(b)) => Minimally(a + b) + case (Exact(a), Exact(b)) => Minimally(a + b) + } + + def packed(sizes: TypeSize*): TypeSize = + sizes.reduce[TypeSize] { + case (Unknown(), _) | (_, Unknown()) => Unknown() + case (Minimally(a), Minimally(b)) => Minimally(a + b) + case (Minimally(a), Exact(b)) => Minimally(a + b) + case (Exact(a), Minimally(b)) => Minimally(a + b) + case (Exact(a), Exact(b)) => Exact(a + b) + } +} + +sealed trait TypeSize {} diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 68d6bf8b8d..574040e302 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -572,10 +572,10 @@ object AstBuildHelpers { def const[G](i: BigInt)(implicit o: Origin): IntegerValue[G] = IntegerValue(i) def c_const[G](i: Int)(implicit o: Origin): CIntegerValue[G] = - CIntegerValue(i) + CIntegerValue(i, TCInt()) def c_const[G](i: BigInt)(implicit o: Origin): CIntegerValue[G] = - CIntegerValue(i) + CIntegerValue(i, TCInt()) def contract[G]( blame: Blame[NontrivialUnsatisfiable], diff --git a/src/hre/hre/io/ChecksumReadableFile.scala b/src/hre/hre/io/ChecksumReadableFile.scala index fac5d4c7d8..8903dd51f5 100644 --- a/src/hre/hre/io/ChecksumReadableFile.scala +++ b/src/hre/hre/io/ChecksumReadableFile.scala @@ -18,7 +18,7 @@ case class ChecksumReadableFile( checksumKind: String, ) extends InMemoryCachedReadable { override def underlyingPath: Option[Path] = Some(file) - override def fileName: String = file.toString + override def fileName: String = file.getFileName.toString override def isRereadable: Boolean = true private var checksumCache: Option[String] = None diff --git a/src/hre/hre/io/RWFile.scala b/src/hre/hre/io/RWFile.scala index c7071e0277..659363e2bf 100644 --- a/src/hre/hre/io/RWFile.scala +++ b/src/hre/hre/io/RWFile.scala @@ -7,7 +7,7 @@ import java.nio.file.{Files, Path} case class RWFile(file: Path, doWatch: Boolean = true) extends InMemoryCachedReadable with Writeable { override def underlyingPath: Option[Path] = Some(file) - override def fileName: String = file.toString + override def fileName: String = file.getFileName.toString override def isRereadable: Boolean = true override protected def getWriter: Writer = { diff --git a/src/main/vct/main/stages/Parsing.scala b/src/main/vct/main/stages/Parsing.scala index 77e01baaad..79c1ec9bed 100644 --- a/src/main/vct/main/stages/Parsing.scala +++ b/src/main/vct/main/stages/Parsing.scala @@ -99,8 +99,6 @@ case class Parsing[G <: Generation]( .orElse(Language.fromFilename(readable.fileName)) .getOrElse(throw UnknownFileExtension(readable.fileName)) - val origin = Origin(Seq(ReadableOrigin(readable))) - val parser = language match { case Language.C => @@ -109,7 +107,7 @@ case class Parsing[G <: Generation]( blameProvider, cc, cSystemInclude, - Option(Paths.get(readable.fileName).getParent).toSeq ++ + readable.underlyingPath.map(_.toAbsolutePath.getParent).toSeq ++ cOtherIncludes, cDefines, ) @@ -121,7 +119,7 @@ case class Parsing[G <: Generation]( blameProvider, ccpp, cppSystemInclude, - Option(Paths.get(readable.fileName).getParent).toSeq ++ + readable.underlyingPath.map(_.getParent).toSeq ++ cppOtherIncludes, cppDefines, ) diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index beb49fba1e..12a24a5012 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -27,11 +27,13 @@ import vct.options.types.{Backend, PathOrStd} import vct.parsers.debug.DebugOptions import vct.resources.Resources import vct.result.VerificationError.SystemError -import vct.rewrite.adt.ImportSetCompat +import vct.rewrite.adt.{ImportBitVector, ImportSetCompat} import vct.rewrite.{ DisambiguatePredicateExpression, + EncodeAssuming, EncodeAutoValue, EncodeByValueClassUsage, + EncodePointerComparison, EncodeRange, EncodeResourceValues, ExplicitResourceValues, @@ -116,9 +118,9 @@ object Transformation extends LazyLogging { Of course, this all while still retaining the functionality of making it possible to pass more simplification rules using command line flags. */ - Progress.hiddenStage( - s"Loading PVL library file ${readable.underlyingPath.getOrElse("")}" - ) { Util.loadPVLLibraryFile(readable, debugOptions) } + Progress.hiddenStage(s"Loading PVL library file ${readable.fileName}") { + Util.loadPVLLibraryFile(readable, debugOptions) + } } def simplifierFor(path: PathOrStd, options: Options): RewriterBuilder = @@ -350,9 +352,9 @@ case class SilverTransformation( ) extends Transformation( onPassEvent, Seq( + CFloatIntCoercion, // Replace leftover SYCL types ReplaceSYCLTypes, - CFloatIntCoercion, // BIP transformations ComputeBipGlue, @@ -413,6 +415,8 @@ case class SilverTransformation( RefuteToInvertedAssert, ExplicitResourceValues, EncodeResourceValues, + EncodeAssuming, + EncodePointerComparison, // Assumes no context_everywhere // Encode parallel blocks EncodeSendRecv, @@ -457,6 +461,7 @@ case class SilverTransformation( EncodeNdIndex, ExtractInlineQuantifierPatterns, // Translate internal types to domains + ImportBitVector.withArg(adtImporter), FloatToRat, SmtlibToProverTypes, EnumToDomain, diff --git a/src/main/vct/options/types/PathOrStd.scala b/src/main/vct/options/types/PathOrStd.scala index c5aa7d12c3..06df5330af 100644 --- a/src/main/vct/options/types/PathOrStd.scala +++ b/src/main/vct/options/types/PathOrStd.scala @@ -15,7 +15,7 @@ sealed trait PathOrStd extends InMemoryCachedReadable with Writeable { override def fileName: String = this match { - case PathOrStd.Path(path) => path.toString + case PathOrStd.Path(path) => path.getFileName.toString case PathOrStd.StdInOrOut => "" } diff --git a/src/parsers/antlr4/LangPVLLexer.g4 b/src/parsers/antlr4/LangPVLLexer.g4 index 3ee9cd70e5..8a94c6aaa6 100644 --- a/src/parsers/antlr4/LangPVLLexer.g4 +++ b/src/parsers/antlr4/LangPVLLexer.g4 @@ -103,6 +103,8 @@ UNFOLDING_ESC: '\\unfolding'; UNFOLDING: 'unfolding'; IN_ESC: '\\in'; IN: 'in'; +ASSERTING: 'asserting'; +ASSUMING: 'assuming'; NEW: 'new'; ID: 'id'; diff --git a/src/parsers/antlr4/LangPVLParser.g4 b/src/parsers/antlr4/LangPVLParser.g4 index a0e6b9445c..9299dcd0d1 100644 --- a/src/parsers/antlr4/LangPVLParser.g4 +++ b/src/parsers/antlr4/LangPVLParser.g4 @@ -158,6 +158,10 @@ unit | '(' '\\chor' expr ')' # pvlLongChorExpr | '(' '\\' '[' ']' expr ')' # pvlShortChorExpr | '(' type ')' expr #pvlCastExpr + | '(' 'asserting' expr ')' # pvlBoolAsserting + | '(' 'asserting' expr ';' expr ')' # pvlAsserting + | '(' 'assuming' expr ')' # pvlBoolAssuming + | '(' 'assuming' expr ';' expr ')' # pvlAssuming | 'this' # pvlThis | 'null' # pvlNull | '\\sender' # pvlSender diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index c8a683e390..03784f7a27 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -148,12 +148,15 @@ CHOOSE: '\\choose'; CHOOSE_FRESH: '\\choose_fresh'; LENGTH: '\\length'; OLD: '\\old'; +ASSERT_EXPR: '\\asserting'; +ASSUME_EXPR: '\\assuming'; TYPEOF: '\\typeof'; TYPEVALUE: '\\type'; 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'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index d7b73b3d24..b20fe082cf 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/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 @@ -298,6 +299,10 @@ valPrimary | '\\is_int' '(' langExpr ')' # valIsInt | '\\choose' '(' langExpr ')' # valChoose | '\\choose_fresh' '(' langExpr ')' # valChooseFresh + | '(' '\\assuming' langExpr ')' # valBoolAssuming + | '(' '\\assuming' langExpr ';' langExpr ')' # valAssuming + | '(' '\\asserting' langExpr ')' # valBoolAsserting + | '(' '\\asserting' langExpr ';' langExpr ')' # valAsserting ; // Out spec: defined meaning: a language local diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala index 58f6dff591..33e0c6f9f4 100644 --- a/src/parsers/vct/parsers/transform/CPPToCol.scala +++ b/src/parsers/vct/parsers/transform/CPPToCol.scala @@ -470,21 +470,21 @@ case class CPPToCol[G]( expr match { case InclusiveOrExpression0(inner) => convert(inner) case InclusiveOrExpression1(left, _, right) => - BitOr(convert(left), convert(right)) + BitOr(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: ExclusiveOrExpressionContext): Expr[G] = expr match { case ExclusiveOrExpression0(inner) => convert(inner) case ExclusiveOrExpression1(left, _, right) => - BitXor(convert(left), convert(right)) + BitXor(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: AndExpressionContext): Expr[G] = expr match { case AndExpression0(inner) => convert(inner) case AndExpression1(left, _, right) => - BitAnd(convert(left), convert(right)) + BitAnd(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: EqualityExpressionContext): Expr[G] = @@ -514,9 +514,15 @@ case class CPPToCol[G]( expr match { case ShiftExpression0(inner) => convert(inner) case ShiftExpression1(left, _, _, right) => - BitShl(convert(left), convert(right)) + BitShl(convert(left), convert(right), 0, signed = true)(blame(expr)) case ShiftExpression2(left, _, _, right) => - BitShr(convert(left), convert(right)) + val l = convert(left) + val r = convert(right) + // The true in BitUShr will be replaced in LangSpecificToCol + if (isSigned(l.t) || isSigned(r.t)) + BitShr(l, r, 0)(blame(expr)) + else + BitUShr(l, r, 0, signed = true)(blame(expr)) } def convert(implicit expr: AdditiveExpressionContext): Expr[G] = @@ -759,9 +765,11 @@ case class CPPToCol[G]( } catch { case _: NumberFormatException => None } } - def parseInt(i: String)(implicit o: Origin): Option[Expr[G]] = - try { Some(CIntegerValue(BigInt(i))) } + def parseInt(i: String)(implicit o: Origin): Option[Expr[G]] = { + // TODO: Proper integer parsing and typing + try { Some(CIntegerValue(BigInt(i), CPrimitiveType(Seq(CInt())))) } catch { case _: NumberFormatException => None } + } private def parseChar(value: String)(implicit o: Origin): Option[Expr[G]] = { val fixedValue = fixEscapeAndUnicodeChars(value) @@ -2109,6 +2117,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, _) => @@ -2342,4 +2351,9 @@ case class CPPToCol[G]( Block(Nil)(DiagnosticOrigin) } + def isSigned(t: Type[G]): Boolean = + t match { + case t: BitwiseType[G] => t.signed + case _ => true + } } diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index dfd85752c0..29edf24ee8 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -13,6 +13,7 @@ import vct.col.ref.{Ref, UnresolvedRef} import vct.col.resolve.lang.C import vct.col.util.AstBuildHelpers +import java.util.Locale import scala.annotation.nowarn import scala.collection.mutable import scala.util.Try @@ -683,11 +684,15 @@ case class CToCol[G]( case "%=" => AmbiguousTruncMod(target, value)(blame(expr)) case "+=" => col.AmbiguousPlus(target, value)(blame(valueNode)) case "-=" => col.AmbiguousMinus(target, value)((blame(valueNode))) - case "<<=" => BitShl(target, value) - case ">>=" => BitShr(target, value) - case "&=" => BitAnd(target, value) - case "^=" => BitXor(target, value) - case "|=" => BitOr(target, value) + case "<<=" => BitShl(target, value, 0, signed = true)(blame(expr)) + case ">>=" => + if (isSigned(target.t) || isSigned(value.t)) + BitShr(target, value, 0)(blame(expr)) + else + BitUShr(target, value, 0, signed = true)(blame(expr)) + case "&=" => BitAnd(target, value, 0, signed = true)(blame(expr)) + case "^=" => BitXor(target, value, 0, signed = true)(blame(expr)) + case "|=" => BitOr(target, value, 0, signed = true)(blame(expr)) }, )(blame(expr)) @@ -730,21 +735,21 @@ case class CToCol[G]( expr match { case InclusiveOrExpression0(inner) => convert(inner) case InclusiveOrExpression1(left, _, right) => - BitOr(convert(left), convert(right)) + BitOr(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: ExclusiveOrExpressionContext): Expr[G] = expr match { case ExclusiveOrExpression0(inner) => convert(inner) case ExclusiveOrExpression1(left, _, right) => - BitXor(convert(left), convert(right)) + BitXor(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: AndExpressionContext): Expr[G] = expr match { case AndExpression0(inner) => convert(inner) case AndExpression1(left, _, right) => - BitAnd(convert(left), convert(right)) + BitAnd(convert(left), convert(right), 0, signed = true)(blame(expr)) } def convert(implicit expr: EqualityExpressionContext): Expr[G] = @@ -774,9 +779,15 @@ case class CToCol[G]( expr match { case ShiftExpression0(inner) => convert(inner) case ShiftExpression1(left, _, right) => - BitShl(convert(left), convert(right)) + BitShl(convert(left), convert(right), 0, signed = true)(blame(expr)) case ShiftExpression2(left, _, right) => - BitShr(convert(left), convert(right)) + val l = convert(left) + val r = convert(right) + // The true in BitUShr will be replaced in LangSpecificToCol + if (isSigned(l.t) || isSigned(r.t)) + BitShr(l, r, 0)(blame(expr)) + else + BitUShr(l, r, 0, signed = true)(blame(expr)) } def convert(implicit expr: AdditiveExpressionContext): Expr[G] = @@ -870,7 +881,7 @@ case class CToCol[G]( case "*" => DerefPointer(convert(arg))(blame(expr)) case "+" => convert(arg) case "-" => UMinus(convert(arg)) - case "~" => BitNot(convert(arg)) + case "~" => BitNot(convert(arg), 0, signed = true)(blame(expr)) case "!" => col.Not(convert(arg)) } case UnaryExpression3(_, _) => ??(expr) @@ -959,9 +970,29 @@ case class CToCol[G]( } catch { case _: NumberFormatException => None } } - def parseInt(i: String)(implicit o: Origin): Option[Expr[G]] = - try { Some(CIntegerValue(BigInt(i))) } + def parseInt(i: String)(implicit o: Origin): Option[Expr[G]] = { + val lower = i.toLowerCase(Locale.ROOT) + // TODO: Check if value in range + val (s, t: Seq[CDeclarationSpecifier[G]]) = + if ( + lower.endsWith("uwb") || lower.endsWith("wbu") || lower.endsWith("wb") + ) { + // Bit-precise integers from C23 unimplemented + return None + } else if (lower.endsWith("ull") || lower.endsWith("llu")) { + (i.substring(0, i.length - 3), Seq(CUnsigned(), CLong(), CLong())) + } else if (lower.endsWith("lu") || lower.endsWith("ul")) { + (i.substring(0, i.length - 2), Seq(CUnsigned(), CLong())) + } else if (lower.endsWith("ll")) { + (i.substring(0, i.length - 2), Seq(CLong(), CLong())) + } else if (lower.endsWith("u")) { + (i.substring(0, i.length - 1), Seq(CUnsigned())) + } else if (lower.endsWith("l")) { + (i.substring(0, i.length - 1), Seq(CLong())) + } else { (i, Seq(CInt())) } + try { Some(CIntegerValue(BigInt(s), CPrimitiveType(t))) } catch { case e: NumberFormatException => None } + } def convert(implicit expr: PrimaryExpressionContext): Expr[G] = expr match { @@ -1833,6 +1864,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, _) => @@ -2002,6 +2034,13 @@ case class CToCol[G]( case ValIsInt(_, _, arg, _) => SmtlibIsInt(convert(arg)) case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e)) case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e)) + case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt) + case ValAssuming(_, _, assn, _, inner, _) => + Assuming(convert(assn), convert(inner)) + case ValBoolAsserting(_, _, assn, _) => + Asserting(convert(assn), tt)(blame(e)) + case ValAsserting(_, _, assn, _, inner, _) => + Asserting(convert(assn), convert(inner))(blame(e)) } def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = @@ -2054,4 +2093,10 @@ case class CToCol[G]( args.map(convert(_)).getOrElse(Nil), ) } + + def isSigned(t: Type[G]): Boolean = + t match { + case t: BitwiseType[G] => t.signed + case _ => true + } } diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala index d2eb456364..54f2815623 100644 --- a/src/parsers/vct/parsers/transform/JavaToCol.scala +++ b/src/parsers/vct/parsers/transform/JavaToCol.scala @@ -1042,7 +1042,7 @@ case class JavaToCol[G]( } case JavaPrefixOp2(preOp, inner) => preOp match { - case "~" => BitNot(convert(inner)) + case "~" => BitNot(convert(inner), 0, signed = true)(blame(expr)) case "!" => Not(convert(inner)) } case JavaValPrefix(PrefixOp0(op), inner) => @@ -1067,9 +1067,14 @@ case class JavaToCol[G]( } case JavaShift(left, shift, right) => shift match { - case ShiftOp0(_, _) => BitShl(convert(left), convert(right)) - case ShiftOp1(_, _, _) => BitUShr(convert(left), convert(right)) - case ShiftOp2(_, _) => BitShr(convert(left), convert(right)) + case ShiftOp0(_, _) => + BitShl(convert(left), convert(right), 0, signed = true)(blame(expr)) + case ShiftOp1(_, _, _) => + BitUShr(convert(left), convert(right), 0, signed = true)(blame( + expr + )) + case ShiftOp2(_, _) => + BitShr(convert(left), convert(right), 0)(blame(expr)) } case JavaRel(left, comp, right) => comp match { @@ -1119,11 +1124,11 @@ case class JavaToCol[G]( case "*=" => AmbiguousMult(target, value) case "/=" => AmbiguousTruncDiv(target, value)(blame(expr)) case "&=" => AmbiguousComputationalAnd(target, value) - case "|=" => BitOr(target, value) - case "^=" => BitXor(target, value) - case ">>=" => BitShr(target, value) - case ">>>=" => BitUShr(target, value) - case "<<=" => BitShl(target, value) + case "|=" => BitOr(target, value, 0, signed = true)(blame(expr)) + case "^=" => BitXor(target, value, 0, signed = true)(blame(expr)) + case ">>=" => BitShr(target, value, 0)(blame(expr)) + case ">>>=" => BitUShr(target, value, 0, signed = true)(blame(expr)) + case "<<=" => BitShl(target, value, 0, signed = true)(blame(expr)) case "%=" => AmbiguousTruncMod(target, value)(blame(expr)) }, )(blame(expr)) @@ -2370,6 +2375,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, _) => @@ -2532,6 +2538,13 @@ case class JavaToCol[G]( case ValNdLength(_, _, dims, _) => NdLength(convert(dims)) case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e)) case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e)) + case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt) + case ValAssuming(_, _, assn, _, inner, _) => + Assuming(convert(assn), convert(inner)) + case ValBoolAsserting(_, _, assn, _) => + Asserting(convert(assn), tt)(blame(e)) + case ValAsserting(_, _, assn, _, inner, _) => + Asserting(convert(assn), convert(inner))(blame(e)) } def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = diff --git a/src/parsers/vct/parsers/transform/LLVMContractToCol.scala b/src/parsers/vct/parsers/transform/LLVMContractToCol.scala index d82dd4e0ec..6fc9afe50b 100644 --- a/src/parsers/vct/parsers/transform/LLVMContractToCol.scala +++ b/src/parsers/vct/parsers/transform/LLVMContractToCol.scala @@ -1,19 +1,16 @@ package vct.parsers.transform -import hre.data.BitString import org.antlr.v4.runtime.{ParserRuleContext, Token} import vct.antlr4.generated.LLVMSpecParser._ import vct.antlr4.generated.LLVMSpecParserPatterns import vct.antlr4.generated.LLVMSpecParserPatterns._ import vct.col.ast._ import vct.col.origin.{ExpectedError, Origin} -import vct.col.ref.{Ref, UnresolvedRef} +import vct.col.ref.UnresolvedRef import vct.col.util.AstBuildHelpers.{ff, foldAnd, implies, tt} import vct.parsers.err.ParseError import scala.annotation.nowarn -import scala.collection.immutable.{AbstractSeq, LinearSeq} -import scala.collection.mutable @nowarn("msg=match may not be exhaustive&msg=Some\\(") case class LLVMContractToCol[G]( @@ -177,9 +174,11 @@ case class LLVMContractToCol[G]( } case TInt() => bitOp match { - case LLVMSpecParserPatterns.And(_) => BitAnd(left, right) - case LLVMSpecParserPatterns.Or(_) => BitOr(left, right) - case Xor(_) => BitXor(left, right) + case LLVMSpecParserPatterns.And(_) => + BitAnd(left, right, 0, signed = true)(blame(bitOp)) + case LLVMSpecParserPatterns.Or(_) => + BitOr(left, right, 0, signed = true)(blame(bitOp)) + case Xor(_) => BitXor(left, right, 0, signed = true)(blame(bitOp)) } case other => throw ParseError( @@ -388,6 +387,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, _) => diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 1cd6573deb..01b10c9146 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -479,6 +479,13 @@ case class PVLToCol[G]( case PvlLongChorExpr(_, _, inner, _) => ChorExpr(convert(inner)) case PvlShortChorExpr(_, _, _, _, inner, _) => ChorExpr(convert(inner)) case PvlCastExpr(_, t, _, e) => Cast(convert(e), TypeValue(convert(t))) + case PvlBoolAsserting(_, _, assn, _) => + Asserting(convert(assn), tt)(blame(expr)) + case PvlAsserting(_, _, assn, _, inner, _) => + Asserting(convert(assn), convert(inner))(blame(expr)) + case PvlBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt) + case PvlAssuming(_, _, assn, _, inner, _) => + Assuming(convert(assn), convert(inner)) case PvlSender(_) => PVLSender() case PvlReceiver(_) => PVLReceiver() case PvlMessage(_) => PVLMessage() @@ -1783,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, _) => @@ -1945,6 +1953,13 @@ case class PVLToCol[G]( case ValNdLength(_, _, dims, _) => NdLength(convert(dims)) case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e)) case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e)) + case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt) + case ValAssuming(_, _, assn, _, inner, _) => + Assuming(convert(assn), convert(inner)) + case ValBoolAsserting(_, _, assn, _) => + Asserting(convert(assn), tt)(blame(e)) + case ValAsserting(_, _, assn, _, inner, _) => + Asserting(convert(assn), convert(inner))(blame(e)) } def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = diff --git a/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java b/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java index 5bec2e09fb..33d94d6f19 100644 --- a/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java +++ b/src/parsers/vct/parsers/transform/systemctocol/engine/ExpressionTransformer.java @@ -1063,9 +1063,10 @@ private Assign decode_assignment(Expr left, String op, Expr right) { case "%=" -> new Mod<>(left, right, new GeneratedBlame<>(), OriGen.create()); case "&=" -> new AmbiguousComputationalAnd<>(left, right, OriGen.create()); case "|=" -> new AmbiguousComputationalOr<>(left, right, OriGen.create()); - case "^=" -> new BitXor<>(left, right, OriGen.create()); - case ">>=" -> new BitShr<>(left, right, OriGen.create()); - case "<<=" -> new BitShl<>(left, right, OriGen.create()); + case "^=" -> new BitXor<>(left, right, 0, true, new GeneratedBlame<>(), OriGen.create()); + // Should be UShr for unsigned values + case ">>=" -> new BitShr<>(left, right, 0, new GeneratedBlame<>(), OriGen.create()); + case "<<=" -> new BitShl<>(left, right, 0, true, new GeneratedBlame<>(), OriGen.create()); default -> throw new IllegalOperationException("Trying to transform an expression to a statement!"); }; @@ -1377,9 +1378,10 @@ private Expr transform_binary_expression_to_expression(BinaryExpression expr, case "||" -> new Or<>(left, right, OriGen.create()); case "&" -> new AmbiguousComputationalAnd<>(left, right, OriGen.create()); case "|" -> new AmbiguousComputationalOr<>(left, right, OriGen.create()); - case "^" -> new BitXor<>(left, right, OriGen.create()); - case ">>" -> new BitShr<>(left, right, OriGen.create()); - case "<<" -> new BitShl<>(left, right, OriGen.create()); + case "^" -> new BitXor<>(left, right, 0, true, new GeneratedBlame<>(), OriGen.create()); + // Should be UShr for unsigned values + case ">>" -> new BitShr<>(left, right, 0, new GeneratedBlame<>(), OriGen.create()); + case "<<" -> new BitShl<>(left, right, 0, true, new GeneratedBlame<>(), OriGen.create()); default -> throw new UnsupportedException("Unsupported binary operator " + expr.getOp()); }; } @@ -1635,7 +1637,7 @@ private Expr transform_unary_expression(UnaryExpression expr, SCClassInstance return switch (expr.getOperator()) { case "!" -> new Not<>(original, OriGen.create()); case "-" -> new UMinus<>(original, OriGen.create()); - case "~" -> new BitNot<>(original, OriGen.create()); + case "~" -> new BitNot<>(original, 0, true, new GeneratedBlame<>(), OriGen.create()); case "+" -> original; case "++" -> handle_incr_decr(true, expr.isPrepost(), original); case "--" -> handle_incr_decr(false, expr.isPrepost(), original); diff --git a/src/rewrite/vct/rewrite/CFloatIntCoercion.scala b/src/rewrite/vct/rewrite/CFloatIntCoercion.scala index ea2f730be8..051b63ae2f 100644 --- a/src/rewrite/vct/rewrite/CFloatIntCoercion.scala +++ b/src/rewrite/vct/rewrite/CFloatIntCoercion.scala @@ -4,6 +4,7 @@ import vct.col.ast.`type`.typeclass.TFloats import vct.col.ast.{ BinExpr, CIntegerValue, + Cast, CastFloat, CoerceCFloatCInt, CoerceCIntCFloat, @@ -16,6 +17,7 @@ import vct.col.ast.{ TFloat, TInt, Type, + TypeValue, } import vct.col.origin.Origin import vct.col.rewrite.{Generation, RewriterBuilder} @@ -47,12 +49,15 @@ case class CFloatIntCoercion[Pre <: Generation]() // to an arbitrary big float. case TCFloat(e, m) => TFloats.ieee754_32bit case TFloat(e, m) => TFloats.ieee754_32bit - case other => rewriteDefault(other) + case other => super.postCoerce(other) } override def postCoerce(e: Expr[Pre]): Expr[Post] = e match { - case CIntegerValue(v) => IntegerValue(v)(e.o) - case other => rewriteDefault(other) + // TODO: Do truncation/sign extension + case Cast(e, TypeValue(TCInt())) if e.t.isInstanceOf[TCInt[Pre]] => + dispatch(e) + case CIntegerValue(v, _) => IntegerValue(v)(e.o) + case other => super.postCoerce(other) } } diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala index adbb41288e..bef3edcf35 100644 --- a/src/rewrite/vct/rewrite/ClassToRef.scala +++ b/src/rewrite/vct/rewrite/ClassToRef.scala @@ -8,6 +8,7 @@ import hre.util.ScopedStack import vct.col.rewrite.error.{ExcludedByPassOrder, ExtraNode} import vct.col.ref.Ref import vct.col.resolve.ctx.Referrable +import vct.col.typerules.CoercionUtils import vct.col.util.SuccessionMap import vct.result.VerificationError.UserError @@ -857,6 +858,8 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { const(typeNumber(t.cls.decl))(e.o) // Keep pointer casts intact for the adtPointer stage case _: TPointer[Pre] | _: TNonNullPointer[Pre] => e.rewriteDefault() + // Keep integer casts intact for casting between integers and pointers + case _: TInt[Pre] => e.rewriteDefault() case other => ??? } case TypeOf(value) => @@ -900,10 +903,13 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] { e.rewriteDefault() } - case Cast(value, typeValue) => + case Cast(value, typeValue) + if value.t.asClass.isDefined || + CoercionUtils.getAnyCoercion(value.t, TAnyClass[Pre]()).isDefined => dispatch( value ) // Discard for now, should assert instanceOf(value, typeValue) + case Cast(value, TypeValue(t)) if value.t == t => { dispatch(value) } case Result(Ref(app)) => app match { case function: Function[Pre] => Result[Post](succ(function))(e.o) diff --git a/src/rewrite/vct/rewrite/Disambiguate.scala b/src/rewrite/vct/rewrite/Disambiguate.scala index 792a8b8ba9..4cb1289f26 100644 --- a/src/rewrite/vct/rewrite/Disambiguate.scala +++ b/src/rewrite/vct/rewrite/Disambiguate.scala @@ -231,6 +231,13 @@ case class Disambiguate[Pre <: Generation]() extends Rewriter[Pre] { case AmbiguousNeq(left, right, _) => VectorNeq(dispatch(left), dispatch(right)) } + else if (cmp.isPointerOp) + cmp match { + case e @ AmbiguousEq(left, right, _) => + PointerEq(dispatch(left), dispatch(right)) + case e @ AmbiguousNeq(left, right, _) => + PointerNeq(dispatch(left), dispatch(right)) + } else cmp match { case AmbiguousEq(left, right, _) => @@ -261,6 +268,17 @@ case class Disambiguate[Pre <: Generation]() extends Rewriter[Pre] { case AmbiguousLessEq(left, right) => SubSetEq(dispatch(left), dispatch(right)) } + else if (cmp.isPointerOp) + cmp match { + case e @ AmbiguousGreater(left, right) => + PointerGreater(dispatch(left), dispatch(right)) + case e @ AmbiguousLess(left, right) => + PointerLess(dispatch(left), dispatch(right)) + case e @ AmbiguousGreaterEq(left, right) => + PointerGreaterEq(dispatch(left), dispatch(right)) + case e @ AmbiguousLessEq(left, right) => + PointerLessEq(dispatch(left), dispatch(right)) + } else cmp match { case AmbiguousGreater(left, right) => diff --git a/src/rewrite/vct/rewrite/EncodeAssuming.scala b/src/rewrite/vct/rewrite/EncodeAssuming.scala new file mode 100644 index 0000000000..3959d9eda1 --- /dev/null +++ b/src/rewrite/vct/rewrite/EncodeAssuming.scala @@ -0,0 +1,56 @@ +package vct.rewrite + +import com.typesafe.scalalogging.LazyLogging +import vct.col.ast.{ + Assuming, + Expr, + Function, + Let, + TBool, + UnitAccountedPredicate, + Variable, +} +import vct.col.origin.{DiagnosticOrigin, UnsafeDontCare} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} + +import vct.col.util.AstBuildHelpers._ + +case object EncodeAssuming extends RewriterBuilder { + override def key: String = "encodeAssumeExpr" + override def desc: String = "Encodes assume exprs using plain pure functions" +} + +case class EncodeAssuming[Pre <: Generation]() + extends Rewriter[Pre] with LazyLogging { + + lazy val assumingFunction: Function[Post] = { + implicit val o = DiagnosticOrigin + val assnVar = new Variable[Post](TBool())(o.where(name = "assn")) + globalDeclarations.declare( + function( + blame = UnsafeDontCare.Contract("assumption primitive"), + contractBlame = UnsafeDontCare.Satisfiability("assumption primitive"), + returnType = TBool(), + args = Seq(assnVar), + ensures = UnitAccountedPredicate(assnVar.get), + )(o.where(name = "assume_")) + ) + } + + override def dispatch(expr: Expr[Pre]): Expr[Post] = + expr match { + case Assuming(assn, inner) => + implicit val o = expr.o + Let( + new Variable(TBool())(o.where(name = "_")), + functionInvocation( + ref = assumingFunction.ref, + args = Seq(dispatch(assn)), + blame = UnsafeDontCare.Invocation("assumption"), + ), + dispatch(inner), + ) + + case _ => expr.rewriteDefault() + } +} diff --git a/src/rewrite/vct/rewrite/EncodePointerComparison.scala b/src/rewrite/vct/rewrite/EncodePointerComparison.scala new file mode 100644 index 0000000000..e74bea88b5 --- /dev/null +++ b/src/rewrite/vct/rewrite/EncodePointerComparison.scala @@ -0,0 +1,175 @@ +package vct.rewrite + +import hre.util.ScopedStack +import vct.col.ast._ +import vct.col.origin.{Origin, PanicBlame} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ + +case object EncodePointerComparison extends RewriterBuilder { + override def key: String = "pointerComparison" + override def desc: String = + "Encodes comparison between pointers taking into account pointer provenance." + + private sealed trait Context + private final case class InAxiom() extends Context + private final case class InPrecondition() extends Context + private final case class InPostcondition() extends Context + private final case class InLoopInvariant() extends Context +} + +case class EncodePointerComparison[Pre <: Generation]() extends Rewriter[Pre] { + import EncodePointerComparison._ + + private val context: ScopedStack[Context] = ScopedStack() + + override def dispatch(decl: Declaration[Pre]): Unit = + decl match { + case axiom: ADTAxiom[Pre] => + context.having(InAxiom()) { + allScopes.anySucceed(axiom, axiom.rewriteDefault()) + } + case decl => allScopes.anySucceed(decl, decl.rewriteDefault()) + } + + override def dispatch( + contract: ApplicableContract[Pre] + ): ApplicableContract[Post] = { + contract.rewrite( + requires = + context.having(InPrecondition()) { dispatch(contract.requires) }, + ensures = context.having(InPostcondition()) { dispatch(contract.ensures) }, + ) + } + + override def dispatch(contract: LoopContract[Pre]): LoopContract[Post] = { + implicit val o: Origin = contract.o + contract match { + case inv @ LoopInvariant(invariant, _) => + inv.rewrite(invariant = + context.having(InLoopInvariant()) { dispatch(invariant) } + ) + case contract @ IterationContract(requires, ensures, _) => + contract.rewrite( + requires = context.having(InPrecondition()) { dispatch(requires) }, + ensures = context.having(InPostcondition()) { dispatch(ensures) }, + ) + } + } + + override def dispatch(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case PointerEq(Null(), r) => dispatch(r) === Null() + case PointerEq(l, Null()) => dispatch(l) === Null() + case e @ PointerEq(l, r) => + dispatchPointerComparison( + l, + r, + Eq(_, _), + eitherNull = Eq(_, _), + compareAddress = false, + ) + case PointerNeq(Null(), r) => dispatch(r) !== Null() + case PointerNeq(l, Null()) => dispatch(l) !== Null() + case e @ PointerNeq(l, r) => + dispatchPointerComparison( + l, + r, + Neq(_, _), + eitherNull = Neq(_, _), + compareAddress = false, + ) + case PointerGreater(Null(), _) => ff + case PointerGreater(l, Null()) => dispatch(l) !== Null() + case e @ PointerGreater(l, r) => + dispatchPointerComparison( + l, + r, + Greater(_, _), + eitherNull = (l, r) => And(r === Null(), l !== Null()), + compareAddress = true, + ) + case PointerLess(Null(), r) => dispatch(r) !== Null() + case PointerLess(_, Null()) => ff + case e @ PointerLess(l, r) => + dispatchPointerComparison( + l, + r, + Less(_, _), + eitherNull = (l, r) => And(l === Null(), r !== Null()), + compareAddress = true, + ) + case PointerGreaterEq(Null(), r) => dispatch(r) === Null() + case PointerGreaterEq(_, Null()) => tt + case e @ PointerGreaterEq(l, r) => + dispatchPointerComparison( + l, + r, + GreaterEq(_, _), + eitherNull = (_, r) => r === Null(), + compareAddress = true, + ) + case PointerLessEq(Null(), _) => tt + case PointerLessEq(l, Null()) => dispatch(l) === Null() + case e @ PointerLessEq(l, r) => + dispatchPointerComparison( + l, + r, + LessEq(_, _), + eitherNull = (l, _) => l === Null(), + compareAddress = true, + ) + case e => super.dispatch(e) + } + } + + private def dispatchPointerComparison( + l: Expr[Pre], + r: Expr[Pre], + comparison: (Expr[Post], Expr[Post]) => Expr[Post], + eitherNull: (Expr[Post], Expr[Post]) => Expr[Post], + compareAddress: Boolean, + )(implicit o: Origin): Expr[Post] = { + val newL = dispatch(l) + val newR = dispatch(r) + val addressComp = + (l: Expr[Post], r: Expr[Post]) => { + comparison( + PointerAddress(l)(PanicBlame("Can not be null")), + PointerAddress(r)(PanicBlame("Can not be null")), + ) + } + val comp = + if (compareAddress) { addressComp } + else { comparison } + + val blockEq = + PointerBlock(newL)(PanicBlame("Can not be null")) === + PointerBlock(newR)(PanicBlame("Can not be null")) + + Select( + Or(newL === Null(), newR === Null()), + eitherNull(newL, newR), { + // Change based on context + context.topOption match { + case None => + Select( + ChooseFresh[Post](LiteralSet(TBool(), Seq(tt, ff)))(PanicBlame( + "Set is never empty" + )), + if (compareAddress) { And(blockEq, addressComp(newL, newR)) } + else { comp(newL, newR) }, + addressComp(newL, newR), + ) + case Some( + InAxiom() | InPrecondition() | InPostcondition() | + InLoopInvariant() + ) => + if (compareAddress) { And(blockEq, addressComp(newL, newR)) } + else { comp(newL, newR) } + } + }, + ) + } +} diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala index 2f7d73b34a..5fd4857b33 100644 --- a/src/rewrite/vct/rewrite/adt/ImportADT.scala +++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala @@ -119,14 +119,17 @@ abstract class ImportADT[Pre <: Generation](importer: ImportADTImporter) .map(succProvider.globalDeclarationsSuccProvider.computeSucc).map(_.get) } - protected def find[T](decls: Seq[Declaration[Post]], name: String)( - implicit tag: ClassTag[T] - ): T = + protected def find[T <: Declaration[Post]]( + decls: Seq[Declaration[Post]], + name: String, + )(implicit tag: ClassTag[T]): T = { decls.collectFirst { case decl: T if decl.o.find[SourceName].contains(SourceName(name)) => decl }.get + } - protected def find[T](decls: Declarator[Post], name: String)( - implicit tag: ClassTag[T] - ): T = find(decls.declarations, name)(tag) + protected def find[T <: Declaration[Post]]( + decls: Declarator[Post], + name: String, + )(implicit tag: ClassTag[T]): T = find(decls.declarations, name)(tag) } diff --git a/src/rewrite/vct/rewrite/adt/ImportBitVector.scala b/src/rewrite/vct/rewrite/adt/ImportBitVector.scala new file mode 100644 index 0000000000..3cd5e9b958 --- /dev/null +++ b/src/rewrite/vct/rewrite/adt/ImportBitVector.scala @@ -0,0 +1,406 @@ +package vct.rewrite.adt + +import hre.util.ScopedStack +import vct.col.ast.{ + Applicable, + Asserting, + BitAnd, + BitNot, + BitOr, + BitShl, + BitShr, + BitUShr, + BitXor, + Declaration, + Expr, + Function, + FunctionInvocation, + Node, + ProverFunction, + ProverFunctionInvocation, + SuccessorsProvider, + SuccessorsProviderTrafo, +} +import vct.col.origin.{ + AssertFailed, + Blame, + IntegerOutOfBounds, + Origin, + PanicBlame, + SourceName, + TrueSatisfiable, +} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, NonLatchingRewriter} +import vct.col.rewrite.adt.{ImportADT, ImportADTBuilder, ImportADTImporter} +import vct.col.util.AstBuildHelpers.functionInvocation +import vct.result.VerificationError.UserError + +import scala.collection.mutable +import scala.reflect.ClassTag + +case object ImportBitVector extends ImportADTBuilder("bitvec") { + private case class UnsupportedBitVectorSize(origin: Origin, bits: Int) + extends UserError { + + override def code: String = "unsupportedBVSize" + + override def text: String = + origin.messageInContext( + s"Unsupported bit vector size `$bits` supported sizes are: 8, 16, 32, 64" + ) + } + + private case class OutOfBoundsBlame( + node: Node[_], + blame: Blame[IntegerOutOfBounds], + )(implicit val bits: Int) + extends Blame[AssertFailed] { + override def blame(error: AssertFailed): Unit = + blame.blame(IntegerOutOfBounds(node, bits)) + } +} + +case class ImportBitVector[Pre <: Generation](importer: ImportADTImporter) + extends ImportADT[Pre](importer) { + import ImportBitVector._ + + private val functionMap: mutable.HashMap[String, Applicable[Post]] = mutable + .HashMap() + + // TODO: These could easily be programmatically generated instead of fixing the sizes + private lazy val bv8 = parse("bv8") + private lazy val bv16 = parse("bv16") + private lazy val bv32 = parse("bv32") + private lazy val bv64 = parse("bv64") + + private lazy val u8_require_inbounds = find[Function[Post]]( + bv8, + "u8_require_inbounds", + ) + private lazy val u16_require_inbounds = find[Function[Post]]( + bv16, + "u16_require_inbounds", + ) + private lazy val u32_require_inbounds = find[Function[Post]]( + bv32, + "u32_require_inbounds", + ) + private lazy val u64_require_inbounds = find[Function[Post]]( + bv64, + "u64_require_inbounds", + ) + + private lazy val u8_is_inbounds = find[Function[Post]](bv8, "u8_is_inbounds") + private lazy val u16_is_inbounds = find[Function[Post]]( + bv16, + "u16_is_inbounds", + ) + private lazy val u32_is_inbounds = find[Function[Post]]( + bv32, + "u32_is_inbounds", + ) + private lazy val u64_is_inbounds = find[Function[Post]]( + bv64, + "u64_is_inbounds", + ) + + private lazy val u8_assume_inbounds = find[Function[Post]]( + bv8, + "u8_assume_inbounds", + ) + private lazy val u16_assume_inbounds = find[Function[Post]]( + bv16, + "u16_assume_inbounds", + ) + private lazy val u32_assume_inbounds = find[Function[Post]]( + bv32, + "u32_assume_inbounds", + ) + private lazy val u64_assume_inbounds = find[Function[Post]]( + bv64, + "u64_assume_inbounds", + ) + + private lazy val s8_is_inbounds = find[Function[Post]](bv8, "s8_is_inbounds") + private lazy val s16_is_inbounds = find[Function[Post]]( + bv16, + "s16_is_inbounds", + ) + private lazy val s32_is_inbounds = find[Function[Post]]( + bv32, + "s32_is_inbounds", + ) + private lazy val s64_is_inbounds = find[Function[Post]]( + bv64, + "s64_is_inbounds", + ) + + private lazy val s8_assume_inbounds = find[Function[Post]]( + bv8, + "s8_assume_inbounds", + ) + private lazy val s16_assume_inbounds = find[Function[Post]]( + bv16, + "s16_assume_inbounds", + ) + private lazy val s32_assume_inbounds = find[Function[Post]]( + bv32, + "s32_assume_inbounds", + ) + private lazy val s64_assume_inbounds = find[Function[Post]]( + bv64, + "s64_assume_inbounds", + ) + + private def function[T <: Applicable[Post]]( + name: String + )(implicit o: Origin, bits: Int, tag: ClassTag[T]): Ref[Post, T] = { + val func = s"bv${bits}_$name" + bits match { + case 8 => + functionMap.getOrElseUpdate(func, find[T](bv8, func)).asInstanceOf[T] + .ref + case 16 => + functionMap.getOrElseUpdate(func, find[T](bv16, func)).asInstanceOf[T] + .ref + case 32 => + functionMap.getOrElseUpdate(func, find[T](bv32, func)).asInstanceOf[T] + .ref + case 64 => + functionMap.getOrElseUpdate(func, find[T](bv64, func)).asInstanceOf[T] + .ref + case _ => throw UnsupportedBitVectorSize(o, bits) + } + } + + private def to( + e: Expr[Post], + blame: Blame[IntegerOutOfBounds], + )(implicit bits: Int, signed: Boolean): Expr[Post] = { + implicit val o: Origin = e.o + ProverFunctionInvocation( + function( + if (signed) + "from_sint" + else + "from_uint" + ), + Seq(ensureInRange(e, blame)), + ) + } + + private def from( + e: Expr[Post] + )(implicit bits: Int, signed: Boolean): Expr[Post] = { + implicit val o: Origin = e.o + if (signed) { + FunctionInvocation( + function[Function[Post]]("to_sint"), + Seq(assumeInRange(e)), + Nil, + Nil, + Nil, + )(TrueSatisfiable) + } else { + ProverFunctionInvocation(function("to_uint"), Seq(assumeInRange(e))) + } + } + + private case class StripAsserting[G]() extends NonLatchingRewriter[G, G]() { + case class SuccOrIdentity() + extends SuccessorsProviderTrafo[G, G](allScopes) { + override def postTransform[T <: Declaration[G]]( + pre: Declaration[G], + post: Option[T], + ): Option[T] = Some(post.getOrElse(pre.asInstanceOf[T])) + } + override def succProvider: SuccessorsProvider[G, G] = SuccOrIdentity() + + override def dispatch(e: Expr[G]): Expr[G] = + e match { + case Asserting(_, body) => dispatch(body) + case _ => e.rewriteDefault() + } + } + + private def simplifyBV(e: Expr[Post])(implicit signed: Boolean) = + e match { + case ProverFunctionInvocation( + Ref(r1), + Seq( + Asserting( + _, + ProverFunctionInvocation(Ref(r2), Seq(Asserting(_, inner))), + ) + ), + ) + if r1.o.find[SourceName].map(_.name).exists(n => + functionMap.contains(n) && + ((signed && n.endsWith("_from_sint")) || + (!signed && n.endsWith("_from_uint"))) + ) && r2.o.find[SourceName].map(_.name).exists(n => + functionMap.contains(n) && + ((signed && n.endsWith("_to_sint")) || + (!signed && n.endsWith("_to_uint"))) + ) => + inner + case _ => e + } + + private def ensureInRange( + e: Expr[Post], + blame: Blame[IntegerOutOfBounds], + )(implicit bits: Int, signed: Boolean): Expr[Post] = { + implicit val o: Origin = e.o + val stripped = StripAsserting().dispatch(e) + bits match { + case 8 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s8_is_inbounds.ref + else + u8_is_inbounds.ref, + args = Seq(stripped), + ), + e, + )(OutOfBoundsBlame(e, blame)) + case 16 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s16_is_inbounds.ref + else + u16_is_inbounds.ref, + args = Seq(stripped), + ), + e, + )(OutOfBoundsBlame(e, blame)) + case 32 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s32_is_inbounds.ref + else + u32_is_inbounds.ref, + args = Seq(stripped), + ), + e, + )(OutOfBoundsBlame(e, blame)) + case 64 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s64_is_inbounds.ref + else + u64_is_inbounds.ref, + args = Seq(stripped), + ), + e, + )(OutOfBoundsBlame(e, blame)) + case _ => throw UnsupportedBitVectorSize(o, bits) + } + } + + private def assumeInRange( + e: Expr[Post] + )(implicit bits: Int, signed: Boolean): Expr[Post] = { + implicit val o: Origin = e.o + val stripped = StripAsserting().dispatch(e) + bits match { + case 8 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s8_assume_inbounds.ref + else + u8_assume_inbounds.ref, + args = Seq(stripped), + ), + e, + )(PanicBlame("Assert true")) + case 16 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s16_assume_inbounds.ref + else + u16_assume_inbounds.ref, + args = Seq(stripped), + ), + e, + )(PanicBlame("Assert true")) + case 32 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s32_assume_inbounds.ref + else + u32_assume_inbounds.ref, + args = Seq(stripped), + ), + e, + )(PanicBlame("Assert true")) + case 64 => + Asserting( + functionInvocation[Post]( + TrueSatisfiable, + if (signed) + s64_assume_inbounds.ref + else + u64_assume_inbounds.ref, + args = Seq(stripped), + ), + e, + )(PanicBlame("Assert true")) + case _ => throw UnsupportedBitVectorSize(o, bits) + } + } + + private def binOp( + name: String, + l: Expr[Pre], + r: Expr[Pre], + b: Int, + s: Boolean, + blame: Blame[IntegerOutOfBounds], + )(implicit o: Origin): Expr[Post] = { + implicit val bits: Int = b + implicit val signed: Boolean = s + from(ProverFunctionInvocation( + function(name), + Seq( + simplifyBV(to(dispatch(l), blame)), + simplifyBV(to(dispatch(r), blame)), + ), + )) + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case op @ BitAnd(l, r, b, s) => binOp("and", l, r, b, s, op.blame) + case op @ BitOr(l, r, b, s) => binOp("or", l, r, b, s, op.blame) + case op @ BitXor(l, r, b, s) => binOp("xor", l, r, b, s, op.blame) + case op @ BitShl(l, r, b, s) => binOp("shl", l, r, b, s, op.blame) + case op @ BitShr(l, r, b) => binOp("shr", l, r, b, s = true, op.blame) + case op @ BitUShr(l, r, b, s) => binOp("ushr", l, r, b, s, op.blame) + case op @ BitNot(arg, b, s) => + implicit val bits: Int = b + implicit val signed: Boolean = s + from(ProverFunctionInvocation( + function("not"), + Seq(simplifyBV(to(dispatch(arg), op.blame))), + )) + case _ => super.postCoerce(e) + } + } +} diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala index 5e532534f7..eee4c62036 100644 --- a/src/rewrite/vct/rewrite/adt/ImportPointer.scala +++ b/src/rewrite/vct/rewrite/adt/ImportPointer.scala @@ -23,12 +23,14 @@ case object ImportPointer extends ImportADTBuilder("pointer") { Seq(LabelContext("classToRef, asType function")) ) - case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_]) - extends Blame[OptionNone] { + private case class PointerNullOptNone( + inner: Blame[PointerNull], + expr: Expr[_], + ) extends Blame[OptionNone] { override def blame(error: OptionNone): Unit = inner.blame(PointerNull(expr)) } - case class PointerBoundsPreconditionFailed( + private case class PointerBoundsPreconditionFailed( inner: Blame[PointerBounds], expr: Node[_], ) extends Blame[PreconditionFailed] { @@ -36,7 +38,7 @@ case object ImportPointer extends ImportADTBuilder("pointer") { inner.blame(PointerBounds(expr)) } - case class DerefPointerBoundsPreconditionFailed( + private case class DerefPointerBoundsPreconditionFailed( inner: Blame[PointerDerefError], expr: Expr[_], ) extends Blame[PreconditionFailed] { @@ -44,13 +46,16 @@ case object ImportPointer extends ImportADTBuilder("pointer") { inner.blame(PointerInsufficientPermission(expr)) } - case class PointerFieldInsufficientPermission( + private case class PointerFieldInsufficientPermission( inner: Blame[PointerInsufficientPermission], expr: Expr[_], ) extends Blame[InsufficientPermission] { override def blame(error: InsufficientPermission): Unit = inner.blame(PointerInsufficientPermission(expr)) } + + private sealed trait Context + private final case class InAxiom() extends Context } case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) @@ -84,6 +89,14 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) ) private lazy val pointerDeref = find[Function[Post]](pointerFile, "ptr_deref") private lazy val pointerAdd = find[Function[Post]](pointerFile, "ptr_add") + private lazy val pointerAddress = find[Function[Post]]( + pointerFile, + "ptr_address", + ) + private lazy val pointerFromAddress = find[Function[Post]]( + pointerFile, + "ptr_from_address", + ) private val pointerField: mutable.Map[Type[Post], SilverField[Post]] = mutable .Map() @@ -93,25 +106,28 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) private val asTypeFunctions: mutable.Map[Type[Pre], Function[Post]] = mutable .Map() - private val inAxiom: ScopedStack[Unit] = ScopedStack() + private val context: ScopedStack[Context] = ScopedStack() private var casts: Set[(Type[Pre], Type[Pre])] = Set.empty private def makeAsTypeFunction( typeName: String, adt: Ref[Post, AxiomaticDataType[Post]] = pointerAdt.ref, + block: Ref[Post, ADTFunction[Post]] = pointerBlock.ref, ): Function[Post] = { + implicit val o: Origin = AsTypeOrigin.where(name = "as_" + typeName) val value = new Variable[Post](TAxiomatic(adt, Nil))( AsTypeOrigin.where(name = "value") ) - globalDeclarations.declare( + globalDeclarations.declare(withResult((result: Result[Post]) => function[Post]( AbstractApplicable, TrueSatisfiable, + ensures = UnitAccountedPredicate(result === value.get), returnType = TAxiomatic(adt, Nil), args = Seq(value), - )(AsTypeOrigin.where(name = "as_" + typeName)) - ) + ) + )) } private def makePointerCreationMethod( @@ -195,7 +211,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) implicit o: Origin ): Expr[Post] = coercion match { - case CoerceNullPointer(_) => OptNone() + case CoerceNullPointer(_) => OptNoneTyped(TAxiomatic(pointerAdt.ref, Nil)) case CoerceNonNullPointer(_) => OptSome(e) case other => super.applyCoercion(e, other) } @@ -213,18 +229,20 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) override def postCoerce(decl: Declaration[Pre]): Unit = { decl match { case axiom: ADTAxiom[Pre] => - inAxiom.having(()) { + context.having(InAxiom()) { allScopes.anySucceed(axiom, axiom.rewriteDefault()) } // TODO: This is an ugly way to exempt this one bit of generated code from having ptrAdd's added case proc: Procedure[Pre] if proc.o.find[LabelContext] .exists(_.label == "classToRef cast helpers") => - inAxiom.having(()) { allScopes.anySucceed(proc, proc.rewriteDefault()) } + context.having(InAxiom()) { + allScopes.anySucceed(proc, proc.rewriteDefault()) + } case adt: AxiomaticDataType[Pre] if adt.o.find[SourceName].exists(_.name == "pointer") => implicit val o: Origin = adt.o - inAxiom.having(()) { + context.having(InAxiom()) { globalDeclarations.succeed( adt, adt.rewrite(decls = { @@ -235,11 +253,27 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) case (TVoid(), other) if other != TVoid[Pre]() => other case (other, TVoid()) if other != TVoid[Pre]() => other }.foreach { t => + val adtSucc = succ[AxiomaticDataType[Post]](adt) + val blockSucc = succ[ADTFunction[Post]]( + adt.decls.collectFirst { + case f: ADTFunction[Pre] + if f.o.find[SourceName] + .exists(_.name == "pointer_block") => + f + }.get + ) val trigger: Local[Post] => Expr[Post] = - p => asType(t, asType(TVoid(), p, succ(adt)), succ(adt)) + p => + asType( + t, + asType(TVoid(), p, adtSucc, blockSucc), + adtSucc, + blockSucc, + ) aDTDeclarations.declare(new ADTAxiom[Post](forall( TAxiomatic(succ(adt), Nil), - body = p => { trigger(p) === asType(t, p, succ(adt)) }, + body = + p => { trigger(p) === asType(t, p, adtSucc, blockSucc) }, triggers = p => Seq(Seq(trigger(p))), ))) } @@ -247,6 +281,23 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) }), ) } + case func: Function[Pre] + if func.o.find[SourceName].exists(_.name == "ptr_address") => + globalDeclarations.succeed( + func, + withResult((result: Result[Post]) => + func.rewrite(contract = + func.contract.rewrite(ensures = + (dispatch(func.contract.ensures) &* PolarityDependent( + LessEq(result, const(BigInt("18446744073709551615"))(func.o))( + func.o + ), + tt, + )(func.o))(func.o) + ) + ) + )(func.o), + ) case _ => super.postCoerce(decl) } } @@ -353,7 +404,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) ref = pointerDeref.ref, args = Seq( if ( - inAxiom.isEmpty && + !context.topOption.contains(InAxiom()) && !deref.o.find[LabelContext] .exists(_.label == "classToRef cast helpers") ) { @@ -432,7 +483,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) ref = pointerDeref.ref, args = Seq( if ( - inAxiom.isEmpty && + !context.topOption.contains(InAxiom()) && !deref.o.find[LabelContext] .exists(_.label == "classToRef cast helpers") ) { @@ -475,13 +526,11 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) PointerBlockLength(pointer)(pointerLen.blame) - PointerBlockOffset(pointer)(pointerLen.blame) ) - case Cast(value, typeValue) if value.t.asPointer.isDefined => - // TODO: Check if types are compatible + case Cast(value, typeValue) => val targetType = typeValue.t.asInstanceOf[TType[Pre]].t - val innerType = targetType.asPointer.get.element val newValue = dispatch(value) (targetType, value.t) match { - case (TPointer(_), TPointer(_)) => + case (TPointer(innerType), TPointer(_)) => Select[Post]( OptEmpty(newValue), OptNoneTyped(TAxiomatic(pointerAdt.ref, Nil)), @@ -493,7 +542,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) )), )), ) - case (TNonNullPointer(_), TPointer(_)) => + case (TNonNullPointer(innerType), TPointer(_)) => applyAsTypeFunction( innerType, value, @@ -501,11 +550,72 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) "Casting a pointer to a non-null pointer implies the pointer must be statically known to be non-null" )), ) - case (TPointer(_), TNonNullPointer(_)) => + case (TPointer(innerType), TNonNullPointer(_)) => OptSome(applyAsTypeFunction(innerType, value, newValue)) - case (TNonNullPointer(_), TNonNullPointer(_)) => + case (TNonNullPointer(innerType), TNonNullPointer(_)) => applyAsTypeFunction(innerType, value, newValue) + case (TInt(), TPointer(innerType)) => + Select[Post]( + OptEmpty(newValue), + const(0), + FunctionInvocation[Post]( + ref = pointerAddress.ref, + args = Seq( + OptGet(newValue)(PanicBlame( + "Can never be null since this is ensured in the conditional expression" + )), + const(4), + ), // TODO: Find size of innerType + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("Stride > 0")), + ) + case (TInt(), TNonNullPointer(innerType)) => + FunctionInvocation[Post]( + ref = pointerAddress.ref, + args = Seq(newValue, const(4)), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("Stride > 0")) + case (TPointer(innerType), TInt()) => + Select[Post]( + newValue === const(0), + OptNoneTyped(TAxiomatic(pointerAdt.ref, Nil)), + OptSome( + FunctionInvocation[Post]( + ref = pointerFromAddress.ref, + args = Seq(newValue, const(4)), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("Stride > 0")) + ), + ) + case (TNonNullPointer(innerType), TInt()) => + FunctionInvocation[Post]( + ref = pointerFromAddress.ref, + args = Seq(newValue, const(4)), + typeArgs = Nil, + Nil, + Nil, + )(PanicBlame("Stride > 0")) // TODO: Blame?? } + case blck @ PointerBlock(p) => + ADTFunctionInvocation[Post]( + typeArgs = None, + ref = pointerBlock.ref, + args = Seq(unwrapOption(p, blck.blame)), + ) + case addr @ PointerAddress(p) => + FunctionInvocation[Post]( + ref = pointerAddress.ref, + args = Seq(unwrapOption(p, addr.blame)), + typeArgs = Nil, + Nil, + Nil, + )(TrueSatisfiable) case other => super.postCoerce(other) } } @@ -521,7 +631,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) case PointerAdd(_, _) => postExpr // Don't add ptrAdd in an ADT axiom since we cannot use functions with preconditions there case _ - if inAxiom.nonEmpty || + if context.topOption.contains(InAxiom()) || !preExpr.o.find[LabelContext] .exists(_.label == "classToRef cast helpers") => postExpr @@ -544,11 +654,14 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) t: Type[Pre], expr: Expr[Post], adt: Ref[Post, AxiomaticDataType[Post]] = pointerAdt.ref, + block: Ref[Post, ADTFunction[Post]] = pointerBlock.ref, )(implicit o: Origin): Expr[Post] = { functionInvocation[Post]( PanicBlame("as_type requires nothing"), - asTypeFunctions - .getOrElseUpdate(t, makeAsTypeFunction(t.toString, adt = adt)).ref, + asTypeFunctions.getOrElseUpdate( + t, + makeAsTypeFunction(t.toString, adt = adt, block = block), + ).ref, Seq(expr), ) } diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala index 3a0ccfa6e3..1754af9f97 100644 --- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala @@ -2109,7 +2109,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(implicit o: Origin): IterVariable[Post] = { val variable = new Variable[Post](TCInt())(o.where(name = s"${scope.idName}_$dimension")) - new IterVariable[Post](variable, CIntegerValue(0), maxRange) + new IterVariable[Post](variable, c_const(0), maxRange) } // Used for generation the contract for the method wrapping the parblocks diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 2efd372157..b92e2790a2 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -368,6 +368,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => false } + def isInt(t: Type[Pre]): Boolean = + getBaseType(t) match { + case _: IntType[Pre] => true + case _ => false + } + def isFloat(t: Type[Pre]): Boolean = getBaseType(t) match { case _: FloatType[Pre] => true @@ -391,6 +397,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def cast(c: CCast[Pre]): Expr[Post] = c match { case CCast(e, t) if castIsId(e.t, t) => rw.dispatch(c.expr) + case CCast(e, t @ TCInt()) if isInt(e.t) => + Cast(rw.dispatch(e), TypeValue(rw.dispatch(t))(c.o))(c.o) case CCast(e, t) if (isFloat(t) && isRatFloatOrInt(e.t)) || (isRatFloatOrInt(t) && isFloat(e.t)) => @@ -424,6 +432,13 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) CoercionUtils.firstElementIsType(newTElement, newEElement) ) { Cast(newE, TypeValue(newT)(t.o))(c.o) } else { throw UnsupportedCast(c) } + case CCast(e, t @ TCInt()) if e.t.asPointer.isDefined => + Cast(rw.dispatch(e), TypeValue(rw.dispatch(t))(t.o))(c.o) + case CCast(e, t @ CTPointer(innerType)) + if getBaseType(e.t).isInstanceOf[TCInt[Pre]] => + Cast(rw.dispatch(e), TypeValue(TPointer(rw.dispatch(innerType)))(t.o))( + c.o + ) case _ => throw UnsupportedCast(c) } @@ -659,7 +674,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) // Since we set the size and blame together, we can assume the blame is not None NewNonNullPointerArray[Post]( getInnerType(cNameSuccessor(d).t), - CIntegerValue(size), + c_const(size), )(blame.get), ) declarations ++= Seq(cNameSuccessor(d)) @@ -713,7 +728,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val nonZeroThreads: Expr[Post] = foldStar( (blockDim.indices.values ++ gridDim.indices.values) - .map(v => Less(CIntegerValue(0)(o), v.get(o))(o)).toSeq + .map(v => Less(c_const(0)(o), v.get(o))(o)).toSeq )(o) val UnitAccountedPredicate(contractRequires: Expr[Pre]) = contract.requires @@ -899,7 +914,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) sizeBlame: Option[Blame[ArraySizeError]], ): Unit = arraySize match { - case Some(CIntegerValue(size)) => + case Some(CIntegerValue(size, _)) => val v = new Variable[Post](TPointer[Post](rw.dispatch(t)))(o) staticSharedMemNames(cRef) = (size, sizeBlame) cNameSuccessor(cRef) = v @@ -1014,6 +1029,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) .declare(cStructFieldsSuccessor((decl, fieldDecl))) } }._1, + false, )(CStructOrigin(sdecl)) rw.globalDeclarations.declare(newStruct) @@ -1905,7 +1921,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val arg = if (args.size == 1) { args.head match { - case CIntegerValue(i) if i >= 0 && i < 3 => Some(i.toInt) + case CIntegerValue(i, _) if i >= 0 && i < 3 => Some(i.toInt) case _ => None } } else diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 555cb75da6..ec2060ef50 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -507,6 +507,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) rw.classDeclarations.declare(structFieldMap((t, idx))) } }._1, + t.packed, )(t.o.withContent(TypeName("struct"))) rw.globalDeclarations.declare(newStruct) diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index c1af3d68bd..26e660f3ae 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -2,7 +2,6 @@ package vct.rewrite.lang import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack -import vct.col.ast.RewriteHelpers._ import vct.col.ast._ import vct.col.origin._ import vct.col.ref.Ref @@ -14,8 +13,8 @@ import vct.col.rewrite.{ RewriterBuilderArg, RewriterBuilderArg2, } +import vct.col.typerules.TypeSize import vct.result.VerificationError.UserError -import vct.rewrite.lang.LangSpecificToCol.NotAValue case object LangSpecificToCol extends RewriterBuilderArg[Boolean] { override def key: String = "langSpecific" @@ -30,11 +29,69 @@ case object LangSpecificToCol extends RewriterBuilderArg[Boolean] { override def text: String = value.o.messageInContext("Could not resolve this expression to a value.") } + + private case class IndeterminableBitVectorSize(op: Expr[_]) + extends UserError { + override def code: String = "unknownBVSize" + override def text: String = + op.o.messageInContext( + "Could not determine the size of the bit vector for this bitwise operation" + ) + } + + private case class IncompatibleBitVectorSize( + op: Expr[_], + l: BigInt, + r: BigInt, + ) extends UserError { + override def code: String = "incompatibleBVSize" + override def text: String = + op.o.messageInContext( + s"The sizes of the operands for this bitwise operation are `$l` and `$r` respectively. Only operations on equal sizes are supported" + ) + } + + private case class IndeterminableBitVectorSign(op: Expr[_]) + extends UserError { + override def code: String = "unknownBVSign" + override def text: String = + op.o.messageInContext( + "Could not determine the signedness of the bit vector for this bitwise operation" + ) + } + + private case class IncompatibleBitVectorSign( + op: Expr[_], + l: Boolean, + r: Boolean, + ) extends UserError { + override def code: String = "incompatibleBVSign" + override def text: String = + op.o.messageInContext( + s"The signedness of the operands for this bitwise operation are `${if (l) + "signed" + else + "unsigned"}` and `${if (r) + "signed" + else + "unsigned"}` respectively. Only operations on equal signedness are supported" + ) + } + + private case class UnsignedArithmeticShift(op: Expr[_]) extends UserError { + override def code: String = "unsignedArithShift" + override def text: String = + op.o.messageInContext( + "It is not possible to perform an arithmetic right-shift on an unsigned value" + ) + } } case class LangSpecificToCol[Pre <: Generation]( generatePermissions: Boolean = false ) extends Rewriter[Pre] with LazyLogging { + import LangSpecificToCol._ + val java: LangJavaToCol[Pre] = LangJavaToCol(this) val bip: LangBipToCol[Pre] = LangBipToCol(this) val c: LangCToCol[Pre] = LangCToCol(this) @@ -189,7 +246,7 @@ case class LangSpecificToCol[Pre <: Generation]( case decl: CPPGlobalDeclaration[Pre] => cpp.rewriteGlobalDecl(decl) case decl: CPPLocalDeclaration[Pre] => ??? case func: Function[Pre] => { - rewriteDefault(func) + super.dispatch(func) cpp.storeIfSYCLFunction(func) } @@ -221,7 +278,7 @@ case class LangSpecificToCol[Pre <: Generation]( case chor: PVLChoreography[Pre] => veymont.rewriteChoreography(chor) case v: Variable[Pre] => llvm.rewriteLocalVariable(v) - case other => rewriteDefault(other) + case other => super.dispatch(other) } override def dispatch(stat: Statement[Pre]): Statement[Post] = @@ -346,7 +403,7 @@ case class LangSpecificToCol[Pre <: Generation]( case arrSub @ AmbiguousSubscript(_, _) => cpp.rewriteSubscript(arrSub) case unfolding: Unfolding[Pre] => { cpp.checkPredicateFoldingAllowed(unfolding.res) - rewriteDefault(unfolding) + super.dispatch(unfolding) } case assign: PreAssignExpression[Pre] => @@ -371,7 +428,7 @@ case class LangSpecificToCol[Pre <: Generation]( } assign.target.t match { case CPPPrimitiveType(_) => cpp.preAssignExpr(assign) - case _ => rewriteDefault(assign) + case _ => super.dispatch(assign) } case inv: SilverPartialADTFunctionInvocation[Pre] => @@ -395,7 +452,58 @@ case class LangSpecificToCol[Pre <: Generation]( case trunc: LLVMTruncate[Pre] => llvm.rewriteTruncate(trunc) case fpext: LLVMFloatExtend[Pre] => llvm.rewriteFloatExtend(fpext) - case other => rewriteDefault(other) + case b @ BitAnd(left, right, 0, true) => + BitAnd( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + determineBitVectorSignedness(e, left, right), + )(b.blame)(e.o) + case b @ BitOr(left, right, 0, true) => + BitOr( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + determineBitVectorSignedness(e, left, right), + )(b.blame)(e.o) + case b @ BitXor(left, right, 0, true) => + BitXor( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + determineBitVectorSignedness(e, left, right), + )(b.blame)(e.o) + case b @ BitShl(left, right, 0, true) => + BitShl( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + determineBitVectorSignedness(e, left, right), + )(b.blame)(e.o) + case b @ BitShr(left, right, 0) => + if (!determineBitVectorSignedness(e, left, right)) { + throw UnsignedArithmeticShift(b) + } + BitShr( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + )(b.blame)(e.o) + case b @ BitUShr(left, right, 0, true) => + BitUShr( + dispatch(left), + dispatch(right), + determineBitVectorSize(e, left, right), + determineBitVectorSignedness(e, left, right), + )(b.blame)(e.o) + case b @ BitNot(arg, 0, true) => + BitNot( + dispatch(arg), + determineBitVectorSize(e, arg, arg), + determineBitVectorSignedness(e, arg, arg), + )(b.blame)(e.o) + + case other => super.dispatch(other) } override def dispatch(t: Type[Pre]): Type[Post] = @@ -404,6 +512,11 @@ case class LangSpecificToCol[Pre <: Generation]( case t: CTPointer[Pre] => c.pointerType(t) case t: CTVector[Pre] => c.vectorType(t) case t: TOpenCLVector[Pre] => c.vectorType(t) + case t: TCInt[Pre] => + val cint = t.rewriteDefault() + cint.bits = t.bits + cint.signed = t.signed + cint case t: CTArray[Pre] => c.arrayType(t) case t: CTStruct[Pre] => c.structType(t) case t: LLVMTInt[Pre] => TInt()(t.o) @@ -417,6 +530,35 @@ case class LangSpecificToCol[Pre <: Generation]( t.o ) // TODO: Ignore these by just assuming they're integers... or could we do TVoid? case t: CPPTArray[Pre] => cpp.arrayType(t) - case other => rewriteDefault(other) + case other => super.dispatch(other) + } + + private def determineBitVectorSize( + op: Expr[Pre], + left: Expr[Pre], + right: Expr[Pre], + ): Int = { + (left.t, right.t) match { + case (l: BitwiseType[Pre], r: BitwiseType[Pre]) => + (l.bits, r.bits) match { + case (None, _) | (_, None) => throw IndeterminableBitVectorSize(op) + case (Some(l), Some(r)) if l == r => l + case (Some(l), Some(r)) => throw IncompatibleBitVectorSize(op, l, r) + } + case _ => throw IndeterminableBitVectorSize(op) + } + } + + private def determineBitVectorSignedness( + op: Expr[Pre], + left: Expr[Pre], + right: Expr[Pre], + ): Boolean = { + (left.t, right.t) match { + case (l: BitwiseType[Pre], r: BitwiseType[Pre]) => + if (l.signed == r.signed) { l.signed } + else { throw IncompatibleBitVectorSign(op, l.signed, r.signed) } + case _ => throw IndeterminableBitVectorSign(op) } + } } diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index a19f731c8a..214e005ab9 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -103,6 +103,11 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { dispatch(t.partialTypeArgs.find(_._1.decl == arg).get._2) ), ) + case t @ TCInt() => + val cint = TCInt[Post]() + cint.bits = t.bits + cint.signed = t.signed + cint case other => rewriteDefault(other) } } diff --git a/src/rewrite/vct/rewrite/rasi/AbstractState.scala b/src/rewrite/vct/rewrite/rasi/AbstractState.scala index 549b54e884..c480d86d07 100644 --- a/src/rewrite/vct/rewrite/rasi/AbstractState.scala +++ b/src/rewrite/vct/rewrite/rasi/AbstractState.scala @@ -335,7 +335,8 @@ case class AbstractState[G]( is_contract: Boolean = false, ): UncertainIntegerValue = expr match { - case CIntegerValue(value) => UncertainIntegerValue.single(value.intValue) + case CIntegerValue(value, _) => + UncertainIntegerValue.single(value.intValue) case IntegerValue(value) => UncertainIntegerValue.single(value.intValue) case SizeOf(tname) => UncertainIntegerValue @@ -381,19 +382,19 @@ case class AbstractState[G]( resolve_integer_expression(left, is_old, is_contract) % resolve_integer_expression(right, is_old, is_contract) // Bit operations destroy any knowledge of integer state TODO: Support bit operations? - case BitNot(_) => UncertainIntegerValue.uncertain() + case BitNot(_, _, _) => UncertainIntegerValue.uncertain() case AmbiguousComputationalOr(_, _) => UncertainIntegerValue.uncertain() case AmbiguousComputationalXor(_, _) => UncertainIntegerValue.uncertain() case AmbiguousComputationalAnd(_, _) => UncertainIntegerValue.uncertain() case ComputationalOr(_, _) => UncertainIntegerValue.uncertain() case ComputationalXor(_, _) => UncertainIntegerValue.uncertain() case ComputationalAnd(_, _) => UncertainIntegerValue.uncertain() - case BitAnd(_, _) => UncertainIntegerValue.uncertain() - case BitOr(_, _) => UncertainIntegerValue.uncertain() - case BitXor(_, _) => UncertainIntegerValue.uncertain() - case BitShl(_, _) => UncertainIntegerValue.uncertain() - case BitShr(_, _) => UncertainIntegerValue.uncertain() - case BitUShr(_, _) => UncertainIntegerValue.uncertain() + case BitAnd(_, _, _, _) => UncertainIntegerValue.uncertain() + case BitOr(_, _, _, _) => UncertainIntegerValue.uncertain() + case BitXor(_, _, _, _) => UncertainIntegerValue.uncertain() + case BitShl(_, _, _, _) => UncertainIntegerValue.uncertain() + case BitShr(_, _, _) => UncertainIntegerValue.uncertain() + case BitUShr(_, _, _, _) => UncertainIntegerValue.uncertain() case Select(cond, ift, iff) => var value: UncertainIntegerValue = UncertainIntegerValue.empty() if (resolve_boolean_expression(cond, is_old, is_contract).can_be_true) { diff --git a/src/viper/viper/api/backend/SilverBackend.scala b/src/viper/viper/api/backend/SilverBackend.scala index 59d8c03c93..979a33ecfc 100644 --- a/src/viper/viper/api/backend/SilverBackend.scala +++ b/src/viper/viper/api/backend/SilverBackend.scala @@ -446,7 +446,9 @@ trait SilverBackend case reasons.MapKeyNotContained(_, key) => val get = info(key).mapGet.get get.blame.blame(blame.MapKeyError(get)) - + case reasons.AssertionFalse(expr) => + val asserting = info(expr).asserting.get + asserting.blame.blame(blame.AssertFailed(getFailure(reason), asserting)) case other => throw NotSupported( s"Viper returned an error reason that VerCors does not recognize: $other" diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala index badc42b153..0d318655a5 100644 --- a/src/viper/viper/api/transform/ColToSilver.scala +++ b/src/viper/viper/api/transform/ColToSilver.scala @@ -42,6 +42,7 @@ case class ColToSilver(program: col.Program[_]) { val currentInvariant: ScopedStack[col.LoopInvariant[_]] = ScopedStack() val currentStarall: ScopedStack[col.Starall[_]] = ScopedStack() val currentUnfolding: ScopedStack[col.Unfolding[_]] = ScopedStack() + val currentAsserting: ScopedStack[col.Asserting[_]] = ScopedStack() val currentMapGet: ScopedStack[col.MapGet[_]] = ScopedStack() val currentDividingExpr: ScopedStack[col.DividingExpr[_]] = ScopedStack() @@ -365,6 +366,7 @@ case class ColToSilver(program: col.Program[_]) { result.invariant = currentInvariant.topOption result.starall = currentStarall.topOption result.unfolding = currentUnfolding.topOption + result.asserting = currentAsserting.topOption result.mapGet = currentMapGet.topOption result.dividingExpr = currentDividingExpr.topOption result @@ -590,6 +592,11 @@ case class ColToSilver(program: col.Program[_]) { pos = pos(e), info = expInfo(e), ) + case a @ col.Asserting(cond, body) => + silver.Asserting(currentAsserting.having(a) { exp(cond) }, exp(body))( + pos = pos(e), + info = NodeInfo(e), + ) case col.Select(condition, whenTrue, whenFalse) => silver.CondExp(exp(condition), exp(whenTrue), exp(whenFalse))( pos = pos(e), diff --git a/src/viper/viper/api/transform/NodeInfo.scala b/src/viper/viper/api/transform/NodeInfo.scala index 2f1a55903b..6a2e8ffc1e 100644 --- a/src/viper/viper/api/transform/NodeInfo.scala +++ b/src/viper/viper/api/transform/NodeInfo.scala @@ -11,6 +11,7 @@ case class NodeInfo[T <: Node[_]](node: T) extends Info { var invariant: Option[LoopInvariant[_]] = None var starall: Option[Starall[_]] = None var unfolding: Option[Unfolding[_]] = None + var asserting: Option[Asserting[_]] = None var unfold: Option[Unfold[_]] = None var mapGet: Option[MapGet[_]] = None var dividingExpr: Option[DividingExpr[_]] = None diff --git a/src/viper/viper/api/transform/SilverParserDummyFrontend.scala b/src/viper/viper/api/transform/SilverParserDummyFrontend.scala index 366f483188..0de212b33d 100644 --- a/src/viper/viper/api/transform/SilverParserDummyFrontend.scala +++ b/src/viper/viper/api/transform/SilverParserDummyFrontend.scala @@ -51,7 +51,10 @@ case class SilverParserDummyFrontend() parse(RWFile(path).readToCompletion(), path) def parse(readable: Readable): Either[Seq[AbstractError], Program] = - parse(readable.readToCompletion(), Paths.get(readable.fileName)) + parse( + readable.readToCompletion(), + readable.underlyingPath.getOrElse(Paths.get(readable.fileName)), + ) override def createVerifier(fullCmd: String): Verifier = noVerifier diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala index 28517b466e..9853fb194a 100644 --- a/src/viper/viper/api/transform/SilverToCol.scala +++ b/src/viper/viper/api/transform/SilverToCol.scala @@ -28,8 +28,6 @@ import viper.silver.plugin.standard.termination.{ import viper.silver.verifier.AbstractError import viper.silver.{ast => silver} -import java.nio.file.{Path, Paths} - case object SilverToCol { private def SilverPositionOrigin(node: silver.Positioned): Origin = node.pos match { @@ -66,7 +64,7 @@ case object SilverToCol { }) } - case class SilverFrontendParseError(path: Path, errors: Seq[AbstractError]) + case class SilverFrontendParseError(path: String, errors: Seq[AbstractError]) extends UserError { override def code: String = "silverFrontendError" override def text: String = @@ -78,36 +76,22 @@ case object SilverToCol { } def transform[G]( - diagnosticPath: Path, + diagnosticFilename: String, in: Either[Seq[AbstractError], silver.Program], blameProvider: BlameProvider, ): col.Program[G] = in match { case Right(program) => SilverToCol(program, blameProvider).transform() case Left(errors) => - throw SilverFrontendParseError(diagnosticPath, errors) + throw SilverFrontendParseError(diagnosticFilename, errors) } - def parse[G](path: Path, blameProvider: BlameProvider): col.Program[G] = - transform(path, SilverParserDummyFrontend().parse(path), blameProvider) - - def parse[G]( - input: String, - diagnosticPath: Path, - blameProvider: BlameProvider, - ): col.Program[G] = - transform( - diagnosticPath, - SilverParserDummyFrontend().parse(input, diagnosticPath), - blameProvider, - ) - def parse[G]( readable: Readable, blameProvider: BlameProvider, ): col.Program[G] = transform( - Paths.get(readable.fileName), + readable.fileName, SilverParserDummyFrontend().parse(readable), blameProvider, ) @@ -555,6 +539,7 @@ case class SilverToCol[G]( case silver.TrueLit() => col.BooleanValue(true) case silver.Unfolding(acc, body) => col.Unfolding(col.AmbiguousFoldTarget(f(acc)), f(body))(blame(e)) + case silver.Asserting(a, body) => col.Asserting(f(a), f(body))(blame(e)) case silver.WildcardPerm() => col.ReadPerm() case silver.ForPerm(variables, resource, body) => ??(e) diff --git a/test/main/vct/test/integration/examples/AssertingAssumingSpec.scala b/test/main/vct/test/integration/examples/AssertingAssumingSpec.scala new file mode 100644 index 0000000000..a5cda5f23e --- /dev/null +++ b/test/main/vct/test/integration/examples/AssertingAssumingSpec.scala @@ -0,0 +1,69 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +class AssertingAssumingSpec extends VercorsSpec { + vercors should verify using silicon in + "inline asserting should be verifiable" pvl """ + requires x > 2 && (asserting x > 2; true); + void m(int x) { } + """ + + vercors should fail withCode "assertFailed:false" using silicon in + "inline asserting should be rejectable" pvl """ + requires (asserting x > 2; true); + void m(int x) { } + """ + + vercors should verify using silicon in + "inline assuming should be verifiable" pvl """ + requires x > 2; + ensures \result; + pure boolean f(int x); + + requires (assuming x > 2; f(x)); + void m(int x) { } + """ + + vercors should fail withCode "preFailed:false" using silicon in + "inline assuming should not cause unsoundness" pvl """ + requires x > 2; + ensures \result; + pure boolean f(int x); + + requires (assuming x > 1; f(x)); + void m(int x) { } + """ + + vercors should verify using silicon in + "inline asserting should be verifiable (short form)" pvl """ + requires x > 2 && (asserting x > 2); + void m(int x) { } + """ + + vercors should fail withCode "assertFailed:false" using silicon in + "inline asserting should be rejectable (short form)" pvl """ + requires (asserting x > 2); + void m(int x) { } + """ + + vercors should verify using silicon in + "inline assuming should be verifiable (short form)" pvl """ + requires x > 2; + ensures \result; + pure boolean f(int x); + + requires (assuming x > 2) && f(x); + void m(int x) { } + """ + + vercors should fail withCode "preFailed:false" using silicon in + "inline assuming should not cause unsoundness (short form)" pvl """ + requires x > 2; + ensures \result; + pure boolean f(int x); + + requires (assuming x > 1) && f(x); + void m(int x) { } + """ +} diff --git a/test/main/vct/test/integration/examples/BitVectorSpec.scala b/test/main/vct/test/integration/examples/BitVectorSpec.scala new file mode 100644 index 0000000000..4f2b19e326 --- /dev/null +++ b/test/main/vct/test/integration/examples/BitVectorSpec.scala @@ -0,0 +1,7 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +class BitVectorSpec extends VercorsSpec { + vercors should verify using silicon example "concepts/bitvectors/basic.c" +} diff --git a/test/main/vct/test/integration/examples/CSpec.scala b/test/main/vct/test/integration/examples/CSpec.scala index d67e546347..9d7023b924 100644 --- a/test/main/vct/test/integration/examples/CSpec.scala +++ b/test/main/vct/test/integration/examples/CSpec.scala @@ -13,7 +13,7 @@ class CSpec extends VercorsSpec { vercors should verify using silicon example "concepts/c/vector_type.c" vercors should verify using silicon example "concepts/c/pointer_casts.c" vercors should verify using silicon example "concepts/c/pointer_tests.c" - vercors should verify using silicon flags("--backend-option", "--exhaleMode=2") example "concepts/c/tagged_pointer.c" + vercors should verify using silicon flags("--backend-option", "--exhaleMode=2") example "concepts/c/tagged_struct.c" vercors should verify using silicon example "concepts/c/void.c" vercors should error withCode "resolutionError:type" in "float should not be demoted" c @@ -613,4 +613,7 @@ class CSpec extends VercorsSpec { bool *pointer_to_boolean = (bool *)&struct_b; } """ + vercors should verify using silicon example "concepts/c/mismatched_provenance.c" + vercors should verify using silicon example "concepts/c/ptr_comparisons.c" + vercors should verify using silicon example "concepts/c/pointer_tag.c" } diff --git a/test/main/vct/test/integration/examples/TechnicalSpec.scala b/test/main/vct/test/integration/examples/TechnicalSpec.scala index 1c88ea1c71..b1919c62a8 100644 --- a/test/main/vct/test/integration/examples/TechnicalSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalSpec.scala @@ -25,7 +25,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should error withCode "resolutionError:thisInConsPre" in "constructor using `this`" pvl """ + vercors should error withCode "resolutionError:thisInConsPre" in + "constructor using `this`" pvl """ class err { int x; @@ -37,19 +38,22 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should error withCode "notALocation" in "example asserting read permission over argument" pvl """ + vercors should error withCode "notALocation" in + "example asserting read permission over argument" pvl """ class C {} requires Value(arg); void main(C arg); """ - vercors should error withCode "notALocation" in "example asserting permission over argument" pvl """ + vercors should error withCode "notALocation" in + "example asserting permission over argument" pvl """ class C {} requires Perm(arg, write); void main(C arg); """ - vercors should verify using anyBackend in "example showing comparison of unrelated types" pvl """ + vercors should verify using anyBackend in + "example showing comparison of unrelated types" pvl """ void test() { /*[/expect assertFailed:false]*/ assert 1 == false; @@ -57,7 +61,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should error withCode "resolutionError:type" in "example quantifying a resource with \\forall" pvl """ + vercors should error withCode "resolutionError:type" in + "example quantifying a resource with \\forall" pvl """ class Test { int x; void test() { @@ -66,7 +71,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should error withCode "abstractFoldExpr" in "example unfolding abstract predicate" pvl """ + vercors should error withCode "abstractFoldExpr" in + "example unfolding abstract predicate" pvl """ resource p(); requires p(); @@ -75,14 +81,16 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should error withCode "abstractFoldExpr" in "example unfolding abstract predicate inline" pvl """ + vercors should error withCode "abstractFoldExpr" in + "example unfolding abstract predicate inline" pvl """ resource p(); requires p(); pure int f() = \Unfolding p() \in 0; """ - vercors should verify using anyBackend in "example with incorrect boolean logic" pvl """ + vercors should verify using anyBackend in + "example with incorrect boolean logic" pvl """ /*[/expect postFailed:false]*/ requires false || true; ensures false && true; @@ -90,7 +98,8 @@ class TechnicalSpec extends VercorsSpec { /*[/end]*/ """ - vercors should verify using anyBackend in "example with vacuously quantified read permission" pvl """ + vercors should verify using anyBackend in + "example with vacuously quantified read permission" pvl """ class rewriterIssue { int x; @@ -105,7 +114,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "another example with vacuously quantified read permission" pvl """ + vercors should verify using anyBackend in + "another example with vacuously quantified read permission" pvl """ class rewriterIssue { int x; @@ -120,7 +130,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example showing negative scale of negative permission" pvl """ + vercors should verify using anyBackend in + "example showing negative scale of negative permission" pvl """ class rewriterIssue { int x; @@ -157,13 +168,18 @@ class TechnicalSpec extends VercorsSpec { // } // """ - vercors should verify using anyBackend example "technical/keywords/allowed-c.c" - vercors should verify using anyBackend example "technical/keywords/allowed-java.java" - vercors should error withCode "emptyInlineDecl" example "technical/keywords/disallowed-c-inline.c" - vercors should error withCode "parseError" example "technical/keywords/disallowed-java-assert.java" + vercors should verify using anyBackend example + "technical/keywords/allowed-c.c" + vercors should verify using anyBackend example + "technical/keywords/allowed-java.java" + vercors should error withCode "emptyInlineDecl" example + "technical/keywords/disallowed-c-inline.c" + vercors should error withCode "parseError" example + "technical/keywords/disallowed-java-assert.java" vercors should verify using silicon example "technical/array-item-access.pvl" - vercors should error withCode "parseError" in "example attaching contract to wrong constructor" java """ + vercors should error withCode "parseError" in + "example attaching contract to wrong constructor" java """ class C { void m() { //@ loop_invariant true; @@ -172,7 +188,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example assigning null to array type" java """ + vercors should verify using anyBackend in + "example assigning null to array type" java """ public class BasicArray { public void test() { int[] a = null; @@ -180,7 +197,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example with subscript after parentheses" pvl """ + vercors should verify using anyBackend in + "example with subscript after parentheses" pvl """ requires 0 < |xs|; void test(seq xs, seq ys) { assert xs[0] == (xs + ys)[0]; @@ -188,12 +206,14 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example with function return class, implemented with = null" pvl """ + vercors should verify using anyBackend in + "example with function return class, implemented with = null" pvl """ class Test {} pure Test f() = null; """ - vercors should verify using anyBackend in "example with given within parallel region" pvl """ + vercors should verify using anyBackend in + "example with given within parallel region" pvl """ given frac p; void call(); @@ -204,7 +224,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example showing invocations in conditions are ok" pvl """ + vercors should verify using anyBackend in + "example showing invocations in conditions are ok" pvl """ int bar() { return 0; } int foo() { return 0; } @@ -225,20 +246,25 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example with return containing a non-direct invocation" pvl """ + vercors should verify using anyBackend in + "example with return containing a non-direct invocation" pvl """ boolean isBlack() { return true; } boolean isRed() { return !isBlack(); } """ - vercors should verify using anyBackend in "example with implicit Exception present" java + vercors should verify using anyBackend in + "example with implicit Exception present" java "class Test { void foo() { new Exception(); } }" - vercors should verify using anyBackend in "example with implicit RuntimeException present" java + vercors should verify using anyBackend in + "example with implicit RuntimeException present" java "class Test { void foo() { new RuntimeException(); } }" - vercors should verify using anyBackend in "example containing an empty class" java - "class OnlyClass {}" - vercors should verify using anyBackend in "example containing an empty class extending something" java + vercors should verify using anyBackend in + "example containing an empty class" java "class OnlyClass {}" + vercors should verify using anyBackend in + "example containing an empty class extending something" java "class OnlyClass extends Object {}" - vercors should verify using anyBackend in "example asserting this instanceof the defining class" java """ + vercors should verify using anyBackend in + "example asserting this instanceof the defining class" java """ class MyClass { void foo() { MyClass myClass = new MyClass(); @@ -246,7 +272,8 @@ class TechnicalSpec extends VercorsSpec { } } """ - vercors should verify using anyBackend in "example showing \\pointer iff forall i \\pointer_index" c """ + vercors should verify using anyBackend in + "example showing \\pointer iff forall i \\pointer_index" c """ //@ context \pointer(ar, len, write); void test(int ar[], int len) { for(int i = 0; i < len; i++) @@ -254,9 +281,12 @@ class TechnicalSpec extends VercorsSpec { {} } """ - vercors should error withCode "parseError" in "example with preceding garbage" pvl "} class Test{}" - vercors should error withCode "parseError" in "example with trailing garbage" pvl "class Test{} }" - vercors should verify using anyBackend in "example returning null for class type" java """ + vercors should error withCode "parseError" in + "example with preceding garbage" pvl "} class Test{}" + vercors should error withCode "parseError" in + "example with trailing garbage" pvl "class Test{} }" + vercors should verify using anyBackend in + "example returning null for class type" java """ public class List { public List nothing() { return null; @@ -264,7 +294,8 @@ class TechnicalSpec extends VercorsSpec { } """ vercors should verify using silicon example "technical/satcheck-check.pvl" - vercors should verify using silicon in "example that shows 2*read does not imply disjointness" pvl """ + vercors should verify using silicon in + "example that shows 2*read does not imply disjointness" pvl """ class Test { int x; } requires Value(left.x) ** Value(right.x); @@ -276,7 +307,9 @@ class TechnicalSpec extends VercorsSpec { } } """ - vercors should verify using silicon in "example that shows 2*read does not imply disjointness, even with a nested field" pvl """ + vercors should verify using silicon in + "example that shows 2*read does not imply disjointness, even with a nested field" pvl + """ class Test { Test t; } requires Value(left.t) ** Value(right.t); @@ -289,10 +322,13 @@ class TechnicalSpec extends VercorsSpec { } } """ - vercors should verify using silicon example "technical/TestFuturePermsFail.pvl" - vercors should verify using silicon example "technical/TestFuturePermsPass.pvl" + vercors should verify using silicon example + "technical/TestFuturePermsFail.pvl" + vercors should verify using silicon example + "technical/TestFuturePermsPass.pvl" - vercors should error withCode "resolutionError:outOfWriteScope" in "example writing to variable within par-block" pvl """ + vercors should error withCode "resolutionError:outOfWriteScope" in + "example writing to variable within par-block" pvl """ void test() { int x = 0; par { @@ -301,7 +337,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using silicon in "example that requires correct associativity of scale" pvl """ + vercors should verify using silicon in + "example that requires correct associativity of scale" pvl """ resource p(); requires [1\2]p() ** [1\2]p(); @@ -310,7 +347,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example that shows given parameters clobber fields" java """ + vercors should verify using anyBackend in + "example that shows given parameters clobber fields" java """ public class A { int i; @@ -337,7 +375,9 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "example that shows qualified names are equal types to their unqualified equivalent" java """ + vercors should verify using anyBackend in + "example that shows qualified names are equal types to their unqualified equivalent" java + """ class QualifiedNames { void foo() { Exception e = new java.lang.Exception(); @@ -349,7 +389,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using anyBackend in "assigning results from impure method calls to final fields should preserve information" java + vercors should verify using anyBackend in + "assigning results from impure method calls to final fields should preserve information" java """ class C { final Integer x; @@ -360,8 +401,7 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using silicon in "example using adts" java - """ + vercors should verify using silicon in "example using adts" java """ /*@ adt MyADT { pure boolean f(); axiom f(); @@ -376,8 +416,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using silicon in "example using negative array size" java - """ + vercors should verify using silicon in + "example using negative array size" java """ class C { void m() { /*[/expect arraySize]*/ @@ -387,8 +427,8 @@ class TechnicalSpec extends VercorsSpec { } """ - vercors should verify using silicon in "example using negative array size in pvl" pvl - """ + vercors should verify using silicon in + "example using negative array size in pvl" pvl """ void m() { /*[/expect arraySize]*/ int[] arr = new int[-2]; @@ -396,7 +436,7 @@ class TechnicalSpec extends VercorsSpec { } """ -vercors should verify using silicon in "example using string primitive" pvl + vercors should verify using silicon in "example using string primitive" pvl """ void g() { "xuz"; @@ -410,8 +450,8 @@ vercors should verify using silicon in "example using string primitive" pvl } """ - vercors should verify using silicon in "example using plus operator overloading" pvl - """ + vercors should verify using silicon in + "example using plus operator overloading" pvl """ class C { int x; @@ -432,7 +472,8 @@ vercors should verify using silicon in "example using string primitive" pvl } """ - vercors should verify using anyBackend example "technical/labeledEmbeddedStatement.c" + vercors should verify using anyBackend example + "technical/labeledEmbeddedStatement.c" vercors should verify using anyBackend in "usage of given/yields in C" c """ /*@ @@ -455,5 +496,5 @@ vercors should verify using silicon in "example using string primitive" pvl } } """ -} +} diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala index 203345d877..04d4808a4e 100644 --- a/test/main/vct/test/integration/meta/ExampleCoverage.scala +++ b/test/main/vct/test/integration/meta/ExampleCoverage.scala @@ -2,7 +2,12 @@ package vct.test.integration.meta import org.scalatest.flatspec.AnyFlatSpec import vct.test.integration.examples._ -import vct.test.integration.examples.veymont.{FM2023VeyMontSpec, TechnicalVeyMontSpec, VeyMontExamplesSpec, IFM2024VeyMontPermissionsSpec} +import vct.test.integration.examples.veymont.{ + FM2023VeyMontSpec, + TechnicalVeyMontSpec, + VeyMontExamplesSpec, + IFM2024VeyMontPermissionsSpec, +} import vct.test.integration.helper._ class ExampleCoverage extends AnyFlatSpec { @@ -11,7 +16,9 @@ class ExampleCoverage extends AnyFlatSpec { new AbruptExamplesSpec(), new AlgorithmExamplesSpec(), new ArrayExamplesSpec(), + new AssertingAssumingSpec(), new BasicExamplesSpec(), + new BitVectorSpec(), new CIncludeSpec(), new ClassesSpec(), new CounterSpec(),