Merge pull request #13 from woosh/ola-theory-of-heaps-translation

Translation of solutions over the theory of heaps into ACSL contracts

regression-tests/runalldirs

@@ -25,6 +25,7 @@ run_test ./rundir math-arrays  "" -assert -dev -t:60
 run_test ./rundir quantifiers "" -assert -dev -t:60
 run_test ./rundir interpreted-predicates "" -assert -dev -t:60
 run_test ./rundir properties "" -assert -dev -t:60
+run_test ./rundir toh-contract-translation "" -dev -t:60
 #run_test ./rundir ParametricEncoder ""
 
 if [ $ERRORS -ne 0 ]; then

regression-tests/toh-contract-translation/Answers

@@ -0,0 +1,153 @@
+
+get-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for get */
+/*@
+  requires p == n && n_init >= 1;
+  ensures ((\result == 0 && 0 >= \old(*n)) || \result >= 0) && r1 == \old(r1) && n_init == \old(n_init) && \old(n) == n;
+*/
+================================================================================
+
+SAFE
+
+incdec-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for decrement */
+/*@
+  requires \separated(a, b) && \valid(a) && \valid(b);
+  ensures a_init == \old(a_init) && b_init == \old(b_init) && a == \old(a) && b == \old(b) && \separated(a, b) && \valid(a) && \valid(b);
+*/
+/* contracts for increment */
+/*@
+  requires val == a && \separated(val, b) && \valid(val) && \valid(b);
+  ensures \old(val) == a && a_init == \old(a_init) && b_init == \old(b_init) && \old(val) == \old(a) && b == \old(b) && \separated(val, b) && \valid(val) && \valid(b) && *val == 1 + \old(*val);
+*/
+================================================================================
+
+SAFE
+
+incdec-2.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for decrement */
+/*@
+  requires \valid(a);
+  ensures a_init == \old(a_init) && a == \old(a) && \valid(a);
+*/
+/* contracts for increment */
+/*@
+  requires val == a && \valid(val);
+  ensures \old(val) == a && a_init == \old(a_init) && \valid(val) && *val == 1 + \old(*val);
+*/
+================================================================================
+
+SAFE
+
+max-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for findMax */
+/*@
+  requires x == a && y == b && \separated(x, y) && \valid(x) && \valid(y);
+  ensures ((a_init == \result && \result >= b_init) || (b_init - a_init >= 1 && b_init == \result)) && r == \old(r) && a_init == \old(a_init) && b_init == \old(b_init) && \old(a) == a && \old(b) == b;
+*/
+================================================================================
+
+SAFE
+
+max-2.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for findMax */
+/*@
+  requires max == r && x == a && y == b && \separated(x, y) && \separated(x, max) && \separated(y, max) && \valid(x) && \valid(y) && \valid(max);
+  ensures (\old(b_init) - \old(a_init) >= 1 || \old(a_init) >= \old(b_init)) && a == \old(x) && b == \old(y) && r == \old(max) && \old(a_init) == a_init && \old(b_init) == b_init;
+*/
+================================================================================
+
+SAFE
+
+multadd-1.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: The following clause has different terms with the same name (term: b:12)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: result:13)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: a:11)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: b:12)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+Warning: The following clause has different terms with the same name (term: result:13)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+Warning: The following clause has different terms with the same name (term: a:11)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for addTwoNumbers */
+/*@
+  requires \separated(a, b) && \separated(a, result) && \separated(b, result) && \valid(a) && \valid(b) && \valid(result);
+  ensures a == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init) && \separated(a, b) && \separated(a, result) && \separated(b, result) && \valid(a) && \valid(b) && \valid(result);
+*/
+/* contracts for multiplyByTwo */
+/*@
+  requires num == a && \separated(num, b) && \separated(num, result) && \separated(b, result) && \valid(num) && \valid(b) && \valid(result);
+  ensures \old(num) == a && \old(num) == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init) && \separated(num, b) && \separated(num, result) && \separated(b, result) && \valid(num) && \valid(b) && \valid(result) && *num == 2*\old(*num);
+*/
+================================================================================
+
+SAFE
+
+truck-2.c
+
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Init:
+                                                             main21_1(emptyHeap, 0, 0, 0, emptyHeap, 0, 0, 0)                                                              
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+                                                                                     |                                                                                     
+                                                                                     |                                                                                     
+                                                                                     V                                                                                     
+ main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) 
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Final:
+ main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) 
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Failed assertion:
+
+UNSAFE

regression-tests/toh-contract-translation/get-1.c

@@ -0,0 +1,34 @@
+
+int r1;
+int n_init;
+
+/*@contract@*/
+int get(int* p) {
+    if (*p <= 0) {
+        return 0;
+    } else {
+        *p = *p - 1;
+        return 1 + get(p);
+    }
+}
+
+int* n;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  r1 = non_det_int();
+  n_init = non_det_int();
+  n = non_det_int_ptr();
+
+  assume((n_init > 0));
+
+  n = (int*) malloc(sizeof(*n));
+  *n = n_init;
+  r1 = get(n);
+
+  assert(((r1 >= n_init) && (r1 <= n_init)));
+}

regression-tests/toh-contract-translation/get-2.c

@@ -0,0 +1,42 @@
+// TODO: This test currently results in 
+//
+// java.lang.Exception: Predicate generation failed
+// (error "Predicate generation failed")
+// Other Error: Predicate generation failed
+// 
+// 
+int r1;
+int n_init;
+
+
+int get(int* p) {
+    if (*p <= 0) {
+        return 0;
+    } else {
+        *p = *p - 1;
+        return 1 + get(p);
+    }
+}
+
+int* n;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  r1 = non_det_int();
+  n_init = non_det_int();
+  n = non_det_int_ptr();
+
+  assume((n_init > 0));
+
+  n = (int*) malloc(sizeof(*n));
+  // Commenting out the following line makes the test pass,
+  // but leads to undefined behavior. 
+  *n = n_init;
+  r1 = get(n);
+
+  assert(((r1 >= n_init) && (r1 <= (n_init * n_init))));
+}

regression-tests/toh-contract-translation/incdec-1.c

@@ -0,0 +1,40 @@
+int a_init;
+int b_init;
+
+/*@contract@*/
+void increment(int* val) {
+    (*val)++;
+}
+
+/*@contract@*/
+void decrement(int* val) {
+    (*val)--;
+}
+
+int *a;
+int *b;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  a_init = non_det_int();
+  b_init = non_det_int();
+  a = non_det_int_ptr();
+  b = non_det_int_ptr();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+  b = (int*) malloc(sizeof(*b));
+
+  *a = a_init;
+  *b = b_init;
+
+  increment(a);
+  decrement(b);
+
+  assert(((*a == (a_init + 1)) && (*b == (b_init - 1))));
+}

regression-tests/toh-contract-translation/incdec-2.c

@@ -0,0 +1,34 @@
+int a_init;
+
+/*@contract@*/
+void increment(int* val) {
+    (*val)++;
+}
+
+/*@contract@*/
+void decrement(int* val) {
+    (*val)--;
+}
+
+int *a;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  a_init = non_det_int();
+  a = non_det_int_ptr();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+
+  *a = a_init;
+
+  increment(a);
+  decrement(a);
+
+  assert((*a == a_init));
+}

regression-tests/toh-contract-translation/incdec-3.c

@@ -0,0 +1,37 @@
+int a_init;
+int b_init;
+
+/*@contract@*/
+void increment(int* val) {
+    (*val)++;
+}
+
+/*@contract@*/
+void decrement(int* val) {
+    increment(val);
+    *val = *val - 2;
+}
+
+int *a;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  a_init = non_det_int();
+  b_init = non_det_int();
+  a = non_det_int_ptr();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+
+  *a = a_init;
+
+  increment(a);
+  decrement(a);
+
+  assert((*a == a_init));
+}

regression-tests/toh-contract-translation/max-1.c

@@ -0,0 +1,40 @@
+int r;
+
+/*@contract@*/
+int findMax(int* x, int* y) {
+    if(*x >= *y)
+        return *x;
+    else
+        return *y;
+}
+
+int* a;
+int* b;
+int a_init;
+int b_init;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  r = non_det_int();
+  a = non_det_int_ptr();
+  b = non_det_int_ptr();
+  a_init = non_det_int();
+  b_init = non_det_int();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+  b = (int*) malloc(sizeof(*b));
+
+  *a = a_init;
+  *b = b_init;
+
+  r = findMax(a, b);
+
+  assert(!((a_init >= b_init) && !(r == a_init)));
+  assert(!((b_init > a_init) && !(r == b_init)));
+}