From e1ab123ed3a695ff212a018108d42284778385b6 Mon Sep 17 00:00:00 2001 From: Zafer Esen Date: Thu, 15 Oct 2020 19:20:48 +0200 Subject: [PATCH] cleaned up examples --- .../{unsafe-access-001.c => invalid-access.c} | 0 ...ccess-001.c-1.smt2 => invalid-access.smt2} | 0 .../{list-002-fail.c => list-002-unsafe.c} | 0 ...002-fail.c-1.smt2 => list-002-unsafe.smt2} | 0 .../{list-004.c-1.smt2 => list-004.smt2} | 0 .../mutually-referential-structs-fail.c | 25 ----------- ... mutually-referential-structs-unsafe.smt2} | 0 .../mutually-referential-structs.c | 2 +- ...smt2 => mutually-referential-structs.smt2} | 0 ...n-struct.c-1.smt2 => opassign-struct.smt2} | 0 heap-theory-examples/simple-arith.c | 2 +- ...imple-arith.c-1.smt2 => simple-arith.smt2} | 0 ...struct-2.c-1.smt2 => simple-struct-2.smt2} | 0 ...ple-struct.c-1.smt2 => simple-struct.smt2} | 0 ...pptr.c-1.smt2 => stackptr-to-heapptr.smt2} | 0 heap-theory-examples/swap-1-fail.c | 14 ------- heap-theory-examples/swap-1.c | 2 +- heap-theory-examples/swap-1.c-1.smt2 | 30 ------------- .../{swap-1-fail.c-1.smt2 => swap-1.smt2} | 0 heap-theory-examples/swap-2-fail.c | 16 ------- heap-theory-examples/swap-2.c | 2 +- .../{swap-2-fail.c-1.smt2 => swap-2.smt2} | 0 heap-theory-examples/swap-3.c-1.smt2 | 42 ------------------- .../{swap-2.c-1.smt2 => swap-3.smt2} | 0 ...afe-001.c-1.smt2 => typecastSafe-001.smt2} | 0 ...e-001.c-1.smt2 => typecastUnsafe-001.smt2} | 0 26 files changed, 4 insertions(+), 131 deletions(-) rename heap-theory-examples/{unsafe-access-001.c => invalid-access.c} (100%) rename heap-theory-examples/{unsafe-access-001.c-1.smt2 => invalid-access.smt2} (100%) rename heap-theory-examples/{list-002-fail.c => list-002-unsafe.c} (100%) rename heap-theory-examples/{list-002-fail.c-1.smt2 => list-002-unsafe.smt2} (100%) rename heap-theory-examples/{list-004.c-1.smt2 => list-004.smt2} (100%) delete mode 100644 heap-theory-examples/mutually-referential-structs-fail.c rename heap-theory-examples/{mutually-referential-structs-unsafe.c-1.smt2 => mutually-referential-structs-unsafe.smt2} (100%) rename heap-theory-examples/{mutually-referential-structs-fail.c-1.smt2 => mutually-referential-structs.smt2} (100%) rename heap-theory-examples/{opassign-struct.c-1.smt2 => opassign-struct.smt2} (100%) rename heap-theory-examples/{simple-arith.c-1.smt2 => simple-arith.smt2} (100%) rename heap-theory-examples/{simple-struct-2.c-1.smt2 => simple-struct-2.smt2} (100%) rename heap-theory-examples/{simple-struct.c-1.smt2 => simple-struct.smt2} (100%) rename heap-theory-examples/{stackptr-to-heapptr.c-1.smt2 => stackptr-to-heapptr.smt2} (100%) delete mode 100644 heap-theory-examples/swap-1-fail.c delete mode 100644 heap-theory-examples/swap-1.c-1.smt2 rename heap-theory-examples/{swap-1-fail.c-1.smt2 => swap-1.smt2} (100%) delete mode 100644 heap-theory-examples/swap-2-fail.c rename heap-theory-examples/{swap-2-fail.c-1.smt2 => swap-2.smt2} (100%) delete mode 100644 heap-theory-examples/swap-3.c-1.smt2 rename heap-theory-examples/{swap-2.c-1.smt2 => swap-3.smt2} (100%) rename heap-theory-examples/{typecastSafe-001.c-1.smt2 => typecastSafe-001.smt2} (100%) rename heap-theory-examples/{typecastUnsafe-001.c-1.smt2 => typecastUnsafe-001.smt2} (100%) diff --git a/heap-theory-examples/unsafe-access-001.c b/heap-theory-examples/invalid-access.c similarity index 100% rename from heap-theory-examples/unsafe-access-001.c rename to heap-theory-examples/invalid-access.c diff --git a/heap-theory-examples/unsafe-access-001.c-1.smt2 b/heap-theory-examples/invalid-access.smt2 similarity index 100% rename from heap-theory-examples/unsafe-access-001.c-1.smt2 rename to heap-theory-examples/invalid-access.smt2 diff --git a/heap-theory-examples/list-002-fail.c b/heap-theory-examples/list-002-unsafe.c similarity index 100% rename from heap-theory-examples/list-002-fail.c rename to heap-theory-examples/list-002-unsafe.c diff --git a/heap-theory-examples/list-002-fail.c-1.smt2 b/heap-theory-examples/list-002-unsafe.smt2 similarity index 100% rename from heap-theory-examples/list-002-fail.c-1.smt2 rename to heap-theory-examples/list-002-unsafe.smt2 diff --git a/heap-theory-examples/list-004.c-1.smt2 b/heap-theory-examples/list-004.smt2 similarity index 100% rename from heap-theory-examples/list-004.c-1.smt2 rename to heap-theory-examples/list-004.smt2 diff --git a/heap-theory-examples/mutually-referential-structs-fail.c b/heap-theory-examples/mutually-referential-structs-fail.c deleted file mode 100644 index be2d2592..00000000 --- a/heap-theory-examples/mutually-referential-structs-fail.c +++ /dev/null @@ -1,25 +0,0 @@ -struct parent; -struct child; - -struct child { - struct parent *p; - int data; -}; - -struct parent { - struct child *child1, *child2; -}; - -void main() -{ - struct parent* list = calloc(sizeof(struct parent)); - list->child1 = calloc(sizeof(struct child)); - list->child1->p = list; - list->child2 = calloc(sizeof(struct child)); - list->child2->p = list; - - struct parent *cp1 = list->child1->p; //commenting out this line - //removes the assertion error - struct parent *cp2 = list->child2->p; - assert(list->child1->p == list); //should succeed after refinements -} diff --git a/heap-theory-examples/mutually-referential-structs-unsafe.c-1.smt2 b/heap-theory-examples/mutually-referential-structs-unsafe.smt2 similarity index 100% rename from heap-theory-examples/mutually-referential-structs-unsafe.c-1.smt2 rename to heap-theory-examples/mutually-referential-structs-unsafe.smt2 diff --git a/heap-theory-examples/mutually-referential-structs.c b/heap-theory-examples/mutually-referential-structs.c index 19db1f29..c90f9c8f 100644 --- a/heap-theory-examples/mutually-referential-structs.c +++ b/heap-theory-examples/mutually-referential-structs.c @@ -20,5 +20,5 @@ void main() struct parent *cp1 = list->child1->p; struct parent *cp2 = list->child2->p; - assert(cp1 == list || cp1 == 0); + assert(list->child1->p == list); } diff --git a/heap-theory-examples/mutually-referential-structs-fail.c-1.smt2 b/heap-theory-examples/mutually-referential-structs.smt2 similarity index 100% rename from heap-theory-examples/mutually-referential-structs-fail.c-1.smt2 rename to heap-theory-examples/mutually-referential-structs.smt2 diff --git a/heap-theory-examples/opassign-struct.c-1.smt2 b/heap-theory-examples/opassign-struct.smt2 similarity index 100% rename from heap-theory-examples/opassign-struct.c-1.smt2 rename to heap-theory-examples/opassign-struct.smt2 diff --git a/heap-theory-examples/simple-arith.c b/heap-theory-examples/simple-arith.c index 6318dcfe..3c179f25 100644 --- a/heap-theory-examples/simple-arith.c +++ b/heap-theory-examples/simple-arith.c @@ -5,7 +5,7 @@ void main() { *x = 3; int y = *x + *x; assert(y == 0 || y == 3 || y == 6 || y == 42 || y == 45 || y == 84); - /* possible values for y without refinements + /* possible values for y using the invariant encoding without refinements 0 + 0 = 0 0 + 3 = 3 3 + 3 = 6 diff --git a/heap-theory-examples/simple-arith.c-1.smt2 b/heap-theory-examples/simple-arith.smt2 similarity index 100% rename from heap-theory-examples/simple-arith.c-1.smt2 rename to heap-theory-examples/simple-arith.smt2 diff --git a/heap-theory-examples/simple-struct-2.c-1.smt2 b/heap-theory-examples/simple-struct-2.smt2 similarity index 100% rename from heap-theory-examples/simple-struct-2.c-1.smt2 rename to heap-theory-examples/simple-struct-2.smt2 diff --git a/heap-theory-examples/simple-struct.c-1.smt2 b/heap-theory-examples/simple-struct.smt2 similarity index 100% rename from heap-theory-examples/simple-struct.c-1.smt2 rename to heap-theory-examples/simple-struct.smt2 diff --git a/heap-theory-examples/stackptr-to-heapptr.c-1.smt2 b/heap-theory-examples/stackptr-to-heapptr.smt2 similarity index 100% rename from heap-theory-examples/stackptr-to-heapptr.c-1.smt2 rename to heap-theory-examples/stackptr-to-heapptr.smt2 diff --git a/heap-theory-examples/swap-1-fail.c b/heap-theory-examples/swap-1-fail.c deleted file mode 100644 index f7226e09..00000000 --- a/heap-theory-examples/swap-1-fail.c +++ /dev/null @@ -1,14 +0,0 @@ -void swap(int *x, int *y){ - int tmp = *x; - *x = *y; - *y = tmp; -} - -void main() { - int a = 3; - int *b = calloc(sizeof(int)); - *b = 42; - swap(&a, b); - assert(a == 42); -} - diff --git a/heap-theory-examples/swap-1.c b/heap-theory-examples/swap-1.c index 4ec6f5cf..f7226e09 100644 --- a/heap-theory-examples/swap-1.c +++ b/heap-theory-examples/swap-1.c @@ -9,6 +9,6 @@ void main() { int *b = calloc(sizeof(int)); *b = 42; swap(&a, b); - assert(a == 0 || a == 3 || a == 42); + assert(a == 42); } diff --git a/heap-theory-examples/swap-1.c-1.smt2 b/heap-theory-examples/swap-1.c-1.smt2 deleted file mode 100644 index 6be857fb..00000000 --- a/heap-theory-examples/swap-1.c-1.smt2 +++ /dev/null @@ -1,30 +0,0 @@ -(set-logic HORN) -(set-info :source | - Benchmark: C_VC - Output by Princess (http://www.philipp.ruemmer.org/princess.shtml) -|) -(set-info :status unknown) -(declare-heap Heap Addr HeapObject - defObj - ((HeapObject 0)) ( - ( - (O_Int (getInt Int)) - (O_Addr (getAddr Addr)) - (defObj) - ) -)) -(declare-fun inv_main10 (Heap Int Addr Int Addr Int) Bool) -(declare-fun inv_main11 (Heap Int Addr Int Addr Int) Bool) -(declare-fun inv_main3 (Heap Int) Bool) -(declare-fun inv_main4 (Heap Int Addr) Bool) -(declare-fun inv_main6 (Heap Int Addr) Bool) -(assert (forall ((var0 Heap)) (or (not (= var0 (as emptyHeap Heap))) (inv_main3 var0 3)))) -(assert (forall ((var0 Addr) (var1 Heap) (var2 Heap) (var3 Int) (var4 Int) (var5 Addr)) (or (not (and (inv_main4 var1 var4 var0) (and (and (= var2 (write var1 var0 (O_Int 42))) (= var3 var4)) (= var5 var0)))) (inv_main10 var2 var3 var5 1 var5 var3)))) -(assert (forall ((var0 Addr) (var1 Heap) (var2 Int) (var3 Addr) (var4 Heap) (var5 Int) (var6 Int) (var7 Addr) (var8 Int) (var9 Addr) (var10 Int)) (or (not (and (inv_main11 var4 var5 var3 var2 var9 var8) (and (and (and (and (= var1 (write var4 var9 (O_Int var8))) (= var10 var5)) (= var7 var3)) (= var6 var2)) (= var0 var9)))) (inv_main6 var1 var10 var7)))) -(assert (forall ((var0 Int) (var1 Int) (var2 Addr) (var3 Addr) (var4 Int) (var5 Addr) (var6 Heap) (var7 Int) (var8 Int) (var9 Int) (var10 Addr) (var11 Heap) (var12 Int)) (or (not (and (inv_main10 var6 var7 var5 var4 var10 var9) (and (and (and (and (and (and (= var11 var6) (= var12 var7)) (= var2 var5)) (= var0 var4)) (= var3 var10)) (= var1 var9)) (= var8 (getInt (read var6 var10)))))) (inv_main11 var11 var8 var2 var0 var3 var1)))) -(assert (forall ((var0 Heap) (var1 Int)) (or (not (inv_main3 var0 var1)) (inv_main4 (newHeap (alloc var0 (O_Int 0))) var1 (newAddr (alloc var0 (O_Int 0))))))) -(assert (forall ((var0 Addr) (var1 Heap) (var2 Int)) (not (and (inv_main4 var1 var2 var0) (not (is-O_Int (read var1 var0))))))) -(assert (forall ((var0 Int) (var1 Addr) (var2 Heap) (var3 Int) (var4 Int) (var5 Addr)) (not (and (inv_main10 var2 var3 var1 var0 var5 var4) (not (is-O_Int (read var2 var5))))))) -(assert (forall ((var0 Int) (var1 Addr) (var2 Heap) (var3 Int) (var4 Int) (var5 Addr)) (not (and (inv_main11 var2 var3 var1 var0 var5 var4) (not (is-O_Int (read var2 var5))))))) -(assert (forall ((var0 Addr) (var1 Heap) (var2 Int)) (not (and (inv_main6 var1 var2 var0) (and (and (not (= var2 0)) (not (= var2 3))) (not (= var2 42))))))) -(check-sat) diff --git a/heap-theory-examples/swap-1-fail.c-1.smt2 b/heap-theory-examples/swap-1.smt2 similarity index 100% rename from heap-theory-examples/swap-1-fail.c-1.smt2 rename to heap-theory-examples/swap-1.smt2 diff --git a/heap-theory-examples/swap-2-fail.c b/heap-theory-examples/swap-2-fail.c deleted file mode 100644 index 6a689f6b..00000000 --- a/heap-theory-examples/swap-2-fail.c +++ /dev/null @@ -1,16 +0,0 @@ -void swap(int *x, int *y){ - int tmp = *x; - *x = *y; - *y = tmp; -} - -void main() { - int *a = calloc(sizeof(int)); - *a = 3; - int *b = calloc(sizeof(int)); - *b = 42; - swap(a, b); - int tmp = *a; - assert(tmp == 42); // should pass after refinements -} - diff --git a/heap-theory-examples/swap-2.c b/heap-theory-examples/swap-2.c index 2b68ac2b..ee065661 100644 --- a/heap-theory-examples/swap-2.c +++ b/heap-theory-examples/swap-2.c @@ -11,6 +11,6 @@ void main() { *b = 42; swap(a, b); int tmp = *a; - assert(tmp == 0 || tmp == 3 || tmp == 42); + assert(tmp == 42); } diff --git a/heap-theory-examples/swap-2-fail.c-1.smt2 b/heap-theory-examples/swap-2.smt2 similarity index 100% rename from heap-theory-examples/swap-2-fail.c-1.smt2 rename to heap-theory-examples/swap-2.smt2 diff --git a/heap-theory-examples/swap-3.c-1.smt2 b/heap-theory-examples/swap-3.c-1.smt2 deleted file mode 100644 index 3a3e123b..00000000 --- a/heap-theory-examples/swap-3.c-1.smt2 +++ /dev/null @@ -1,42 +0,0 @@ -(set-logic HORN) -(set-info :source | - Benchmark: C_VC - Output by Princess (http://www.philipp.ruemmer.org/princess.shtml) -|) -(set-info :status unknown) -(declare-heap Heap Addr HeapObject - defObj - ((HeapObject 0)) ( - ( - (O_Int (getInt Int)) - (O_Addr (getAddr Addr)) - (defObj) - ) -)) -(declare-fun inv_main11 (Heap Addr Addr Addr Addr Int) Bool) -(declare-fun inv_main12 (Heap Addr Addr Addr Addr Int) Bool) -(declare-fun inv_main13 (Heap Addr Addr Addr Addr Int Int) Bool) -(declare-fun inv_main14 (Heap Addr Addr Int) Bool) -(declare-fun inv_main2 (Heap) Bool) -(declare-fun inv_main3 (Heap Addr) Bool) -(declare-fun inv_main5 (Heap Addr Addr) Bool) -(declare-fun inv_main7 (Heap Addr Addr) Bool) -(declare-fun inv_main8 (Heap Addr Addr Addr Addr) Bool) -(assert (inv_main2 (as emptyHeap Heap))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Heap) (var3 Addr) (var4 Addr) (var5 Addr)) (or (not (and (inv_main5 var2 var4 var5) (and (and (= var0 (write var2 var5 (O_Int 42))) (= var3 var4)) (= var1 var5)))) (inv_main8 var0 var3 var1 var3 var1)))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Int) (var4 Addr) (var5 Addr) (var6 Int)) (or (not (inv_main13 var0 var2 var5 var4 var1 var3 var6)) (inv_main12 (write var0 var4 (O_Int var6)) var2 var5 var4 var1 var3)))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Addr) (var4 Heap) (var5 Addr) (var6 Addr) (var7 Addr) (var8 Int) (var9 Addr) (var10 Addr)) (or (not (and (inv_main12 var0 var6 var10 var9 var5 var8) (and (and (and (and (= var4 (write var0 var5 (O_Int var8))) (= var1 var6)) (= var7 var10)) (= var3 var9)) (= var2 var5)))) (inv_main7 var4 var1 var7)))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Addr) (var4 Addr)) (or (not (inv_main8 var0 var2 var4 var3 var1)) (inv_main11 var0 var2 var4 var3 var1 (getInt (read var0 var3)))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Heap) (var3 Addr)) (or (not (and (inv_main3 var0 var3) (and (= var2 (write var0 var3 (O_Int 3))) (= var1 var3)))) (inv_main5 (newHeap (alloc var2 (O_Int 0))) var1 (newAddr (alloc var2 (O_Int 0))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Int) (var4 Addr) (var5 Addr)) (or (not (inv_main11 var0 var2 var5 var4 var1 var3)) (inv_main13 var0 var2 var5 var4 var1 var3 (getInt (read var0 var1)))))) -(assert (forall ((var0 Heap)) (or (not (inv_main2 var0)) (inv_main3 (newHeap (alloc var0 (O_Int 0))) (newAddr (alloc var0 (O_Int 0))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr)) (or (not (inv_main7 var0 var1 var2)) (inv_main14 var0 var1 var2 (getInt (read var0 var1)))))) -(assert (forall ((var0 Heap) (var1 Addr)) (not (and (inv_main3 var0 var1) (not (is-O_Int (read var0 var1))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr)) (not (and (inv_main5 var0 var1 var2) (not (is-O_Int (read var0 var2))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Addr) (var4 Addr)) (not (and (inv_main8 var0 var2 var4 var3 var1) (not (is-O_Int (read var0 var3))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Int) (var4 Addr) (var5 Addr)) (not (and (inv_main11 var0 var2 var5 var4 var1 var3) (not (is-O_Int (read var0 var1))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Int) (var4 Addr) (var5 Addr) (var6 Int)) (not (and (inv_main13 var0 var2 var5 var4 var1 var3 var6) (not (is-O_Int (read var0 var4))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr) (var3 Int) (var4 Addr) (var5 Addr)) (not (and (inv_main12 var0 var2 var5 var4 var1 var3) (not (is-O_Int (read var0 var1))))))) -(assert (forall ((var0 Heap) (var1 Addr) (var2 Addr)) (not (and (inv_main7 var0 var1 var2) (not (is-O_Int (read var0 var1))))))) -(assert (forall ((var0 Int) (var1 Heap) (var2 Addr) (var3 Addr)) (not (and (inv_main14 var1 var2 var3 var0) (and (and (not (= var0 0)) (not (= var0 3))) (not (= var0 42))))))) -(check-sat) diff --git a/heap-theory-examples/swap-2.c-1.smt2 b/heap-theory-examples/swap-3.smt2 similarity index 100% rename from heap-theory-examples/swap-2.c-1.smt2 rename to heap-theory-examples/swap-3.smt2 diff --git a/heap-theory-examples/typecastSafe-001.c-1.smt2 b/heap-theory-examples/typecastSafe-001.smt2 similarity index 100% rename from heap-theory-examples/typecastSafe-001.c-1.smt2 rename to heap-theory-examples/typecastSafe-001.smt2 diff --git a/heap-theory-examples/typecastUnsafe-001.c-1.smt2 b/heap-theory-examples/typecastUnsafe-001.smt2 similarity index 100% rename from heap-theory-examples/typecastUnsafe-001.c-1.smt2 rename to heap-theory-examples/typecastUnsafe-001.smt2