Fix a bunch of old proofs for CI before big refactor

Gillian-C/lib/gilgen.ml

@@ -888,7 +888,8 @@ let is_builtin_func func_name =
   List.mem func_name builtins
 
 let is_gil_func func_name exec_mode =
-  Exec_mode.is_symbolic_exec exec_mode
+  (Exec_mode.is_symbolic_exec exec_mode
+  || Exec_mode.is_verification_exec exec_mode)
   && (String.equal func_name Builtin_Functions.assume_f
      || String.equal func_name Builtin_Functions.assert_f)
 

Gillian-C/scripts/testSymb.sh

@@ -34,3 +34,22 @@ printf "\n\n"
 echo "--- testing BST ---"
 $WPST symbolic/bst.c -l disabled
 printf "\n\n"
+
+echo "--- testing globalvar ---"
+$WPST symbolic/globalvar.c -l disabled
+printf "\n\n"
+
+echo "--- testing unstructured ---"
+$WPST symbolic/unstructured.c -l disabled
+printf "\n\n"
+
+# Expected-failure test: array_oob.c contains an out-of-bounds bug that
+# symbolic testing must catch, so a zero exit code here is itself a failure.
+echo "--- testing array_oob (expect failure: out-of-bounds bug) ---"
+if $WPST symbolic/bug_examples/array_oob.c -l disabled; then
+  echo "ERROR: expected array_oob.c to fail, but it succeeded"
+  exit 1
+else
+  echo "(failed as expected)"
+fi
+printf "\n\n"

Gillian-C/scripts/testVerif.sh

@@ -23,3 +23,15 @@ printf "\n\n"
 echo "--- verifying sort ---"
 $VERIFY verification/sort.c -l disabled
 printf "\n\n"
+
+echo "--- verifying vector ---"
+$VERIFY verification/vector.c -l disabled
+printf "\n\n"
+
+echo "--- verifying array ---"
+$VERIFY verification/array.c -l disabled
+printf "\n\n"
+
+echo "--- verifying batch ---"
+$VERIFY verification/batch.c -l disabled
+printf "\n\n"

Gillian-JS/scripts/testJaVerT.sh

@@ -4,13 +4,39 @@ set -e
 
 if [[ "${GITHUB_ACTIONS}" ]]; then
 	VERIFY="gillian-js verify"
+	WPST="gillian-js wpst"
 else
   VERIFY="dune exec -- gillian-js verify"
+  WPST="dune exec -- gillian-js wpst"
 fi
 
 # Bash array format: ("one" "two" "three")
-# JS Files to test
-declare -a jsfiles=("BST" "PriQ" "SLL" "DLL" "Sort")
+# JaVerT verification examples to test
+declare -a jsfiles=("BST" "PriQ" "SLL" "DLL" "Sort" "ExprEval" "IDGen" "KVMap" "annotated/SLL")
+
+# Cosette symbolic-testing (wpst) case studies, relative to Examples/
+declare -a wpstfiles=(
+	"Cosette/CaseStudies/BST/bst_find_1"
+	"Cosette/CaseStudies/BST/bst_find_min_1"
+	"Cosette/CaseStudies/BST/bst_insert_1"
+	"Cosette/CaseStudies/BST/bst_remove_1"
+	"Cosette/CaseStudies/DLL/dll"
+	"Cosette/CaseStudies/ExprEval/exprEval_3"
+	"Cosette/CaseStudies/ExprEval/exprEval_4"
+	"Cosette/CaseStudies/ExprEval/exprEval_5"
+	"Cosette/CaseStudies/ExprEval/exprEval_6"
+	"Cosette/CaseStudies/ExprEval/exprEval_7"
+	"Cosette/CaseStudies/IDGen/IdGen"
+	"Cosette/CaseStudies/KVMap/kv_map_1"
+	"Cosette/CaseStudies/KVMap/kv_map_2"
+	"Cosette/CaseStudies/PriQ/pri_q_1"
+	"Cosette/CaseStudies/PriQ/pri_q_2"
+	"Cosette/CaseStudies/SLL/sll"
+	"Cosette/CaseStudies/Sort/sort_1"
+	"Cosette/CaseStudies/Sort/sort_2"
+	"Cosette/simple_example"
+	"Cosette/check_div_by_zero"
+)
 
 FINAL_RETURN=0
 
@@ -36,4 +62,21 @@ do
 	if [[ $rc != 0 ]]; then FINAL_RETURN=1; fi
 	echo "----------------"
 done
+
+echo "Symbolic-testing (wpst) Cosette case studies"
+echo "--------------------------------------------"
+for f in "${wpstfiles[@]}"
+do
+  sleep 1
+	echo "Testing: $f.js"
+	if [[ $1 == "count" ]]; then
+		$WPST Examples/$f.js -l disabled --stats
+		rc=$?
+	else
+		$WPST Examples/$f.js -l disabled
+		rc=$?
+	fi
+	if [[ $rc != 0 ]]; then FINAL_RETURN=1; fi
+	echo "----------------"
+done
 exit $FINAL_RETURN

GillianCore/smt/smt.ml

@@ -607,7 +607,9 @@ let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t
   | FPlus -> num_add (get_num p1) (get_num p2) >- NumberType
   | FMinus -> num_sub (get_num p1) (get_num p2) >- NumberType
   | FTimes -> num_mul (get_num p1) (get_num p2) >- NumberType
-  | FDiv -> num_div (get_num p1) (get_num p2) >- NumberType
+  (* Numbers are encoded as reals, so float division must use SMT-LIB real
+     division ["/" *)
+  | FDiv -> app_ "/" [ get_num p1; get_num p2 ] >- NumberType
   | FLessThan -> num_lt (get_num p1) (get_num p2) >- BooleanType
   | FLessThanEqual -> num_leq (get_num p1) (get_num p2) >- BooleanType
   | Equal -> encode_equality p1 p2

wisl/examples/SLL_ex_complete.wisl

@@ -52,7 +52,7 @@ lemma list_member_concat {
 }
 
 // 00. Allocating an SLL node with the given value
-{ v == #v }
+{ (v == #v) }
 function SLL_allocate_node(v){
   t := new(2);
   [t] := v;
@@ -146,7 +146,7 @@ function SLL_length(x) {
   };
   return n
 }
-{ ret == len(#vs) }
+{ (ret == len(#vs)) }
 
 // 07. Reversing a given SLL
 { (x == #x) *  SLL(#x, #vs) }
@@ -296,7 +296,7 @@ function SLL_append_iter(x, k){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while(next != null){
-      [[ assert {bind: #prev} prev == #prev ]];
+      [[ assert {bind: #prev} (prev == #prev) ]];
       prev := next;
       next := [next + 1];
       [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -324,7 +324,7 @@ function SLL_append_node_iter(x, y){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while(next != null){
-      [[ assert {bind: #prev} prev == #prev ]];
+      [[ assert {bind: #prev} (prev == #prev) ]];
       prev := next;
       next := [next + 1];
       [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -352,7 +352,7 @@ function SLL_concat_iter(x, y){
           SLLseg(head, prev, #vs1) * (prev -b> #v, next) * SLL(next,  #vs2) *
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while (next != null) {
-        [[ assert {bind: #prev} prev == #prev ]];
+        [[ assert {bind: #prev} (prev == #prev) ]];
         prev := next;
         next := [next + 1];
         [[ apply SLLseg_append(head,  #vs1, #v, prev) ]]
@@ -413,7 +413,7 @@ function SLL_length_iter(x) {
       SLLseg(x, y,  #nvx) * SLL(y, #nvy) *
          (#vx == (#nvx@#nvy)) * (n == len #nvx) ]];
   while (y != null) {
-    [[ assert {bind: #y} y == #y ]];
+    [[ assert {bind: #y} (y == #y) ]];
     [[ assert {bind: #v, #z} #y -b> #v, #z ]];
     y := [y+1];
     n := n+1;
@@ -451,8 +451,8 @@ function SLL_member_iter(x, k) {
          (#alpha == (#beta @ #gamma)) * (#r == (found || #rg)) *
            list_member(#beta, k, found) * list_member(#gamma, k, #rg) ]];
   while ((found == false) && (next != null)){
-    [[ assert found == false ]];
-    [[ assert {bind: #next} next == #next ]];
+    [[ assert (found == false) ]];
+    [[ assert {bind: #next} (next == #next) ]];
     [[ assert {bind: #v, #z} #next -b> #v, #z ]];
     v := [next];
     found := (v == k);

wisl/examples/SLL_ex_ongoing.wisl

@@ -57,7 +57,7 @@ predicate SLL_len(+x, n : Int) {
 // With length
 predicate SLLseg_len(+x, y, n : Int) {
   (x == y) * (n == 0);
-  (x -b> #v, #z) * SLLseg_len(#z, y, n - 1) * (0 <# n)
+  (x -b> #v, #z) * SLLseg_len(#z, y, n - 1) * (0 < n)
 }
 
 // With values
@@ -146,7 +146,7 @@ lemma SLLseg_vals_to_SLL_vals {
 lemma SLLseg_len_append_lr {
   statement:
     forall x.
-      SLLseg_len(#x, #y, #n) * (#y -b> #v, #z) |- SLLseg_len(#x, #z, #n + 1) * (0 <=# #n)
+      SLLseg_len(#x, #y, #n) * (#y -b> #v, #z) |- SLLseg_len(#x, #z, #n + 1) * (0 <= #n)
 
   variant: #n
 
@@ -163,7 +163,7 @@ lemma SLLseg_len_append_lr {
 lemma SLLseg_len_append_rl {
   statement:
     forall x.
-      SLLseg_len(#x, #z, #n + 1) * (0 <=# #n) |- SLLseg_len(#x, #y, #n) * (#y -b> #v, #z)
+      SLLseg_len(#x, #z, #n + 1) * (0 <= #n) |- SLLseg_len(#x, #y, #n) * (#y -b> #v, #z)
 
   variant: #n
 
@@ -461,7 +461,7 @@ function SLL_member_iter(x, k) {
            list_member(#beta, k, found) * list_member(#gamma, k, #rg)
      with variant: (len #gamma) ]] ;
   while ((found == false) && (next != null)) {
-    [[ assert found == false ]];
+    [[ assert (found == false) ]];
     [[ assert {bind: #v} next -> #v ]];
     v := [ next ];
     found := (v == k);

wisl/examples/loop.wisl

@@ -9,35 +9,33 @@ predicate lseg(+x, +y, alpha) {
   (x -> #a, #z) * (alpha == #a :: #beta) * lseg(#z, y, #beta)
 }
 
-lemma lseg_to_list(x, alpha) {
+lemma lseg_to_list {
+  statement:
+    forall x, alpha.
+      (x == #x) * (alpha == #alpha) * lseg(#x, null, #alpha) |- list(#x, #alpha)
   variant: len alpha
-  hypothesis: (x == #x) * (alpha == #alpha) * lseg(#x, null, #alpha)
-  conclusion: list(#x, #alpha)
   proof: unfold lseg(#x, null, #alpha);
          if (#x == null) {
            fold list(#x, #alpha)
          } else {
-           assert {exists: #next, #beta} (#x + 1 -> #next) * lseg(#next, null, #beta);
+           assert {bind: #next, #beta} (#x + 1 -> #next) * lseg(#next, null, #beta);
            apply lseg_to_list(#next, #beta);
            fold list(#x, #alpha)
          }
 }
 
-lemma lseg_append(x, y, alpha, a, z) {
+lemma lseg_append {
+  statement:
+    forall x, y, alpha, a, z.
+      (x == #x) * (y == #y) * (alpha == #alpha) * (a == #a) * (z == #z) *
+      lseg(#x, #y, #alpha) *
+      (#y -> #a, #z) |- lseg(#x, #z, #alpha @ [ #a ])
   variant: len alpha
-
-  hypothesis: (x == #x) * (y == #y) * (alpha == #alpha) * (a == #a) * (z == #z) *
-              lseg(#x, #y, #alpha) * 
-              (#y -> #a, #z) 
-
-  conclusion: lseg(#x, #z, #alpha @ [ #a ])
-
-
   proof: unfold lseg(#x, #y, #alpha);
          if (#alpha == []) {
            fold lseg(#x, #z, #alpha @ [#a])
          } else {
-           assert {exists: #next, #beta} (#x + 1 -> #next) * lseg(#next, #y, #beta);
+           assert {bind: #next, #beta} (#x + 1 -> #next) * lseg(#next, #y, #beta);
            apply lseg_append(#next, #y, #beta, #a, #z); 
            fold lseg(#x, #z, #alpha @ [#a])
          } 
@@ -47,16 +45,17 @@ lemma lseg_append(x, y, alpha, a, z) {
 function llen(x) {
   y := x;
   n := 0;
-  [[ fold lseg(#x, y, []) ]];
-  [[ invariant {exists: #a1, #a2} lseg(#x, y, #a1) * list(y, #a2) * (#alpha == #a1 @ #a2) * (n == len #a1) ]];
+  [[ fold lseg(x, y, []) ]];
+  [[ invariant {bind: y, n, #a1, #a2} lseg(x, y, #a1) * list(y, #a2) * (#alpha == #a1 @ #a2) * (n == len #a1) ]];
   while (y != null) {
     [[ unfold list(y, #a2) ]];
-    [[ assert {exists: #y, #b, #t} (y == #y) * (#y -> #b, #t) ]];
+    [[ assert {bind: #y, #b, #t} (y == #y) * (#y -> #b, #t) ]];
     y := [y+1];
     n := n+1;
-    [[ apply lseg_append(#x, #y, #a1, #b, #t) ]]
+    [[ apply lseg_append(x, #y, #a1, #b, #t) ]]
   };
-  [[ apply lseg_to_list(#x, #alpha) ]];
+  [[ unfold list(y, #a2) ]];
+  [[ apply lseg_to_list(x, #alpha) ]];
   return n
 }
 { list(#x, alpha) * (ret == len(#alpha)) }