Merge branch 'master' of github.com:TyGuS/synsl

TyGuS · Jul 12, 2018 · 25f7bbb · 25f7bbb
2 parents 7ef103f + 585e27f
commit 25f7bbb
Show file tree

Hide file tree

Showing 31 changed files with 69 additions and 77 deletions.
diff --git a/README.md b/README.md
@@ -1,6 +1,6 @@
 # Synthetic Separation Logic
 
-[![Build Status](https://travis-ci.org/TyGuS/synsl.svg?branch=master)](https://travis-ci.org/TyGuS/synsl)
+[![Build Status](https://travis-ci.org/TyGuS/suslik.svg?branch=master)](https://travis-ci.org/TyGuS/suslik)
 [![License](https://img.shields.io/badge/License-BSD%202--Clause-orange.svg)](https://raw.githubusercontent.com/TyGuS/suslik/master/LICENSE)
 
 Synthesis of Heap-Manipulating Programs from Separation Logic Specifications

diff --git a/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn b/src/test/resources/synthesis/abduct/list-copy-len-ptr.syn
@@ -17,8 +17,8 @@ void list_copy (loc r) {
     list_copy(r);
     let y12 = *r;
     let y2 = malloc(2);
-    *(y2 + 1) = nxt2;
-    *r = y2;
     *(x2 + 1) = y12;
+    *r = y2;
+    *(y2 + 1) = nxt2;
   }
 }
diff --git a/src/test/resources/synthesis/account/alloc-struct.syn b/src/test/resources/synthesis/account/alloc-struct.syn
@@ -6,7 +6,7 @@ should be able to allocate structures
 ###
 void createAccount (loc x, int bal, int lim) {
   let y2 = malloc(2);
-  *(y2 + 1) = bal;
-  *y2 = lim;
   *x = y2;
+  *y2 = lim;
+  *(y2 + 1) = bal;
 }
diff --git a/src/test/resources/synthesis/copy-len/c6-alloc-head.syn b/src/test/resources/synthesis/copy-len/c6-alloc-head.syn
@@ -13,6 +13,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
diff --git a/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn b/src/test/resources/synthesis/copy-len/c7-frame-alloc-head.syn
@@ -17,6 +17,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
diff --git a/src/test/resources/synthesis/copy-len/c8-alloc-close.syn b/src/test/resources/synthesis/copy-len/c8-alloc-close.syn
@@ -17,6 +17,6 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
 }
diff --git a/src/test/resources/synthesis/copy-len/list-copy-len.syn b/src/test/resources/synthesis/copy-len/list-copy-len.syn
@@ -16,7 +16,7 @@ void list_copy (loc r, loc x) {
     list_copy(r, nxt2);
     let y12 = *r;
     let y2 = malloc(2);
-    *(y2 + 1) = y12;
     *r = y2;
+    *(y2 + 1) = y12;
   }
 }
diff --git a/src/test/resources/synthesis/copy/c5-alloc_value.syn b/src/test/resources/synthesis/copy/c5-alloc_value.syn
@@ -13,6 +13,6 @@ void foo(loc r, int v)
 
 void foo (loc r, int v) {
   let Y2 = malloc(2);
-  *Y2 = v;
   *r = Y2;
+  *Y2 = v;
 }
diff --git a/src/test/resources/synthesis/copy/c6-alloc_head.syn b/src/test/resources/synthesis/copy/c6-alloc_head.syn
@@ -16,7 +16,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let y2 = malloc(2);
-  *y2 = v;
-  *(y2 + 1) = t3;
   *r = y2;
+  *(y2 + 1) = t3;
+  *y2 = v;
 }
diff --git a/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn b/src/test/resources/synthesis/copy/c7-frame-alloc-head.syn
@@ -19,7 +19,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *Y2 = v;
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
+  *Y2 = v;
 }
diff --git a/src/test/resources/synthesis/copy/c8-alloc-close.syn b/src/test/resources/synthesis/copy/c8-alloc-close.syn
@@ -19,7 +19,7 @@ void list_copy(loc r, int v, loc t3)
 
 void list_copy (loc r, int v, loc t3) {
   let Y2 = malloc(2);
-  *Y2 = v;
-  *(Y2 + 1) = t3;
   *r = Y2;
+  *(Y2 + 1) = t3;
+  *Y2 = v;
 }
diff --git a/src/test/resources/synthesis/copy/list_copy.syn b/src/test/resources/synthesis/copy/list_copy.syn
@@ -17,8 +17,8 @@ void list_copy (loc r, loc x) {
     list_copy(r, nxt2);
     let y12 = *r;
     let y2 = malloc(2);
-    *y2 = v2;
-    *(y2 + 1) = y12;
     *r = y2;
+    *(y2 + 1) = y12;
+    *y2 = v2;
   }
 }
diff --git a/src/test/resources/synthesis/copy/list_copy_hard.syn b/src/test/resources/synthesis/copy/list_copy_hard.syn
@@ -18,9 +18,9 @@ void listcopy (loc r) {
     listcopy(r);
     let y12 = *r;
     let y2 = malloc(2);
-    *y2 = v2;
-    *(y2 + 1) = nxt2;
-    *r = y2;
     *(x2 + 1) = y12;
+    *r = y2;
+    *(y2 + 1) = nxt2;
+    *y2 = v2;
   }
 }
diff --git a/src/test/resources/synthesis/dllist/dllist-to-llist.syn b/src/test/resources/synthesis/dllist/dllist-to-llist.syn
@@ -18,9 +18,9 @@ void dll_to_sll (loc f) {
     dll_to_sll(f);
     let i12 = *f;
     let i2 = malloc(2);
+    *f = i2;
+    *(i2 + 1) = i12;
     free(x2);
     *i2 = v2;
-    *(i2 + 1) = i12;
-    *f = i2;
   }
 }
diff --git a/src/test/resources/synthesis/entail/duplicator.syn b/src/test/resources/synthesis/entail/duplicator.syn
@@ -11,8 +11,8 @@ void duplicate(loc x, loc r)
 void duplicate (loc x, loc r) {
   let a2 = *x;
   let z2 = malloc(2);
-  free(x);
-  *(z2 + 1) = a2;
-  *z2 = a2;
   *r = z2;
+  *z2 = a2;
+  *(z2 + 1) = a2;
+  free(x);
 }
diff --git a/src/test/resources/synthesis/flatten/tree-flatten-acc.syn b/src/test/resources/synthesis/flatten/tree-flatten-acc.syn
@@ -18,9 +18,9 @@ void tree_flatten (loc x, loc z) {
     tree_flatten(r2, z);
     let t22 = *z;
     let t3 = malloc(2);
+    *z = t3;
+    *(t3 + 1) = t22;
     free(x);
     *t3 = v2;
-    *(t3 + 1) = t22;
-    *z = t3;
   }
 }
diff --git a/src/test/resources/synthesis/flatten/tree-flatten.syn b/src/test/resources/synthesis/flatten/tree-flatten.syn
@@ -23,9 +23,9 @@ void tree_flatten (loc z) {
     list_append(z, y22);
     let z12 = *z;
     let y3 = malloc(2);
+    *z = y3;
+    *(y3 + 1) = z12;
     free(x2);
     *y3 = v2;
-    *(y3 + 1) = z12;
-    *z = y3;
   }
 }
diff --git a/src/test/resources/synthesis/llist/llist-nil.syn b/src/test/resources/synthesis/llist/llist-nil.syn
@@ -9,6 +9,6 @@ should be able to allocate a linked list
 
 void create_llist (loc z, loc r) {
   let x2 = malloc(1);
-  *x2 = 0;
   *r = x2;
+  *x2 = 0;
 }
diff --git a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-insert.syn
@@ -14,23 +14,15 @@ void srtl_insert (loc x, loc r) {
   if (x == 0) {
     let y2 = malloc(2);
     *r = y2;
+    *y2 = k2 <= 7 ? k2 : 7;
     *(y2 + 1) = 0;
-    *y2 = k2;
   } else {
-    let v2 = *x;
-    if (v2 <= k2) {
-      let nxt2 = *(x + 1);
-      srtl_insert(nxt2, r);
-      let y12 = *r;
-      *(x + 1) = y12;
-      *r = x;
-    } else {
-      let nxt2 = *(x + 1);
-      srtl_insert(nxt2, x);
-      let y12 = *x;
-      *r = x;
-      *(x + 1) = y12;
-      *x = k2;
-    }
+    let lo2 = *x;
+    let nxt2 = *(x + 1);
+    srtl_insert(nxt2, r);
+    let y12 = *r;
+    *x = k2 <= lo2 ? k2 : lo2;
+    *(x + 1) = y12;
+    *r = x;
   }
 }
diff --git a/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn b/src/test/resources/synthesis/paper-benchmarks/srtl/srtl-prepend.syn
@@ -11,6 +11,6 @@ void srtl_prepend (loc x, int k, loc r)
 void srtl_prepend (loc x, int k, loc r) {
   let y2 = malloc(2);
   *r = y2;
-  *(y2 + 1) = x;
   *y2 = k;
+  *(y2 + 1) = x;
 }
diff --git a/src/test/resources/synthesis/simple/alloc.syn b/src/test/resources/synthesis/simple/alloc.syn
@@ -9,6 +9,6 @@ void create(loc x)
 
 void create (loc x) {
   let y2 = malloc(1);
-  *y2 = 42;
   *x = y2;
+  *y2 = 42;
 }
diff --git a/src/test/resources/synthesis/simple/blocks.syn b/src/test/resources/synthesis/simple/blocks.syn
@@ -10,8 +10,8 @@ void create(loc x)
 
 void create (loc x) {
   let y2 = malloc(3);
-  *(y2 + 2) = x;
-  *(y2 + 1) = 2;
-  *y2 = 1;
   *x = y2;
+  *y2 = 1;
+  *(y2 + 1) = 2;
+  *(y2 + 2) = x;
 }
diff --git a/src/test/resources/synthesis/simple/kareem.syn b/src/test/resources/synthesis/simple/kareem.syn
@@ -6,8 +6,8 @@ void kareem1(loc x, loc y, loc z)
 ###
 void kareem1 (loc x, loc y, loc z) {
   let v2 = *x;
-  *v2 = x;
+  *x = y;
   *z = x;
   *y = z;
-  *x = y;
+  *v2 = x;
 }
diff --git a/src/test/resources/synthesis/simple/kareem2.syn b/src/test/resources/synthesis/simple/kareem2.syn
@@ -12,8 +12,8 @@ void kareem3 (loc x) {
   let a2 = *x;
   let b2 = *a2;
   let c2 = *b2;
-  *c2 = b2;
+  *x = 42;
   *a2 = c2;
+  *c2 = b2;
   *b2 = a2;
-  *x = 42;
 }
diff --git a/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn b/src/test/resources/synthesis/tree/tree-copy-len-ptr.syn
@@ -21,10 +21,10 @@ void tree_copy (loc r) {
     tree_copy(x2);
     let y22 = *x2;
     let y3 = malloc(3);
-    *(y3 + 2) = r12;
-    *(y3 + 1) = l2;
-    *r = y3;
-    *(x2 + 2) = y22;
     *(x2 + 1) = y12;
+    *(x2 + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = l2;
+    *(y3 + 2) = r12;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-copy-len.syn b/src/test/resources/synthesis/tree/tree-copy-len.syn
@@ -19,9 +19,9 @@ void tree_copy (loc x, loc r) {
     tree_copy(r12, x);
     let y22 = *x;
     let y3 = malloc(3);
-    *(y3 + 2) = r12;
-    *(y3 + 1) = y12;
-    *r = y3;
     *(x + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = y12;
+    *(y3 + 2) = r12;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-copy-ptr.syn b/src/test/resources/synthesis/tree/tree-copy-ptr.syn
@@ -22,12 +22,12 @@ void tree_copy (loc r) {
     tree_copy(x2);
     let y22 = *x2;
     let y3 = malloc(3);
-    *x2 = v2;
-    *y3 = v2;
-    *(y3 + 2) = r12;
-    *(y3 + 1) = l2;
-    *r = y3;
-    *(x2 + 2) = y22;
     *(x2 + 1) = y12;
+    *(x2 + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = l2;
+    *(y3 + 2) = r12;
+    *y3 = v2;
+    *x2 = v2;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-copy.syn b/src/test/resources/synthesis/tree/tree-copy.syn
@@ -20,11 +20,11 @@ void tree_copy (loc x, loc r) {
     tree_copy(r12, x);
     let y22 = *x;
     let y3 = malloc(3);
-    *y3 = v2;
-    *x = v2;
-    *(y3 + 2) = r12;
-    *(y3 + 1) = y12;
-    *r = y3;
     *(x + 2) = y22;
+    *r = y3;
+    *(y3 + 1) = y12;
+    *(y3 + 2) = r12;
+    *x = v2;
+    *y3 = v2;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-morph.syn b/src/test/resources/synthesis/tree/tree-morph.syn
@@ -14,8 +14,8 @@ void morhp_tree (loc x, int i) {
     let r2 = *(x + 2);
     morhp_tree(l2, i);
     morhp_tree(r2, i);
+    *x = i;
     *(x + 1) = r2;
     *(x + 2) = l2;
-    *x = i;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-size-ptr.syn b/src/test/resources/synthesis/tree/tree-size-ptr.syn
@@ -21,8 +21,8 @@ void tree_size (loc r) {
     *x2 = r12;
     tree_size(x2);
     let n22 = *x2;
-    *r = 1 + n12 + n22;
     *(x2 + 1) = r12;
     *(x2 + 2) = l2;
+    *r = 1 + n12 + n22;
   }
 }
diff --git a/src/test/resources/synthesis/tree/tree-size.syn b/src/test/resources/synthesis/tree/tree-size.syn
@@ -19,8 +19,8 @@ void tree_size (loc x, loc r) {
     *x = 0;
     tree_size(r12, x);
     let n22 = *x;
-    *r = 1 + n12 + n22;
     *(x + 1) = r12;
     *(x + 2) = l2;
+    *r = 1 + n12 + n22;
   }
 }