Fix some small bugs

Now all ARM, RISC-V, and CHERI-MIPS all build successfully with
type-checking changes. All typechecker/c/ocaml/lem/builtin/riscv/arm
tests are now working as well.

Now the python test scripts can run sequentially with TEST_PAR=1 there's
no reason to keep the old shell versions around anymore.

4 files changed, 14 insertions, 261 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index a16b8c73..7ead0cc8 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -104,6 +104,8 @@ let to_smt l vars constr =
     | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_sum (nexp1, nexp2) -> sfun "+" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
+    | Nexp_exp (Nexp_aux (Nexp_constant c, _)) when Big_int.greater c Big_int.zero ->
+       Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c)))
     | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
     | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
   in
@@ -228,7 +230,6 @@ let call_z3 l vars constraints =
   result
 
 let rec solve_z3 l vars constraints var =
-  let problems = [constraints] in
   let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in
 
   (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
diff --git a/src/type_check.ml b/src/type_check.ml
index 8359dac2..1216786e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1244,28 +1244,17 @@ let prove_z3 env (NC_aux (_, l) as nc) =
   | Constraint.Sat -> typ_debug (lazy "sat"); false
   | Constraint.Unknown -> typ_debug (lazy "unknown"); false
 
-let solve env nexp = failwith "WIP"
-
-  (* typ_print (lazy ("Solve " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?"));
+let solve env (Nexp_aux (_, l) as nexp) = 
+  typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
+                   ^ " |- " ^ string_of_nexp nexp ^ " = ?"));
   match nexp with
   | Nexp_aux (Nexp_constant n,_) -> Some n
   | _ ->
-    let bindings = ref KBindings.empty  in
-    let fresh_var kid =
-      let n = KBindings.cardinal !bindings in
-      bindings := KBindings.add kid n !bindings;
-      n
-    in
-    let var_of kid =
-      try KBindings.find kid !bindings with
-      | Not_found -> fresh_var kid
-    in
-    let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") K_int env in
-    let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env))
-                                 (nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp))
-    in
-    Constraint.solve_z3 constr (var_of (mk_kid "solve#"))
-   *)
+    let env = Env.add_typ_var Parse_ast.Unknown (mk_kopt K_int (mk_kid "solve#")) env in
+    let vars = Env.get_typ_vars env in
+    let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
+    let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
+    Constraint.solve_z3 l vars constr (mk_kid "solve#")
 
 let prove env nc =
   typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
@@ -1515,13 +1504,13 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
 
           mod(m, C) = 0 && C != 0 --> (C * n = m <--> n = m / C)
 
-          to help us unify multiplications and divisions.  *)
+          to help us unify multiplications and divisions. 
        let valid n c = prove env (nc_eq (napp (mk_id "mod") [n; c]) (nint 0)) && prove env (nc_neq c (nint 0)) in
        if KidSet.is_empty (nexp_frees n1b) && valid nexp2 n1b then
          unify_nexp l env goals n1a (napp (mk_id "div") [nexp2; n1b])
        else if KidSet.is_empty (nexp_frees n1a) && valid nexp2 n1a then
-         unify_nexp l env goals n1b (napp (mk_id "div") [nexp2; n1a])
-       else if KidSet.is_empty (nexp_frees n1a) then
+         unify_nexp l env goals n1b (napp (mk_id "div") [nexp2; n1a]) *)
+       if KidSet.is_empty (nexp_frees n1a) then
          begin
            match nexp_aux2 with
            | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) ->
@@ -2329,6 +2318,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
         let else_branch' = crule check_exp (Env.add_constraint (nc_not flow) env) else_branch typ in
         annot_exp (E_if (cond', then_branch', else_branch')) typ
      | _ ->
+        let cond' = type_coercion env cond' bool_typ in
         let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in
         let else_branch' = crule check_exp (add_opt_constraint (option_map nc_not (assert_constraint env false cond')) env) else_branch typ in
         annot_exp (E_if (cond', then_branch', else_branch')) typ
diff --git a/test/builtins/run_tests.sh b/test/builtins/run_tests.sh
deleted file mode 100755
index eeb57a79..00000000
--- a/test/builtins/run_tests.sh
+++ /dev/null
@@ -1,140 +0,0 @@
-
-#!/usr/bin/env bash
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-cd $DIR
-SAILDIR="$DIR/../.."
-LEMBUILDDIR="$DIR/_lembuild"
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-rm -f $DIR/tests.xml
-
-pass=0
-fail=0
-XML=""
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $DIR/tests.xml
-    XML=""
-    pass=0
-    fail=0
-}
-
-printf "<testsuites>\n" >> $DIR/tests.xml
-
-shopt -s nullglob;
-for file in $DIR/*.sail;
-do
-    if $SAILDIR/sail -no_warn -c -O $file 1> ${file%.sail}.c 2> /dev/null;
-    then
-	green "compiling $(basename $file) (C)" "ok";
-	if gcc -I $SAILDIR/lib/ ${file%.sail}.c -lgmp;
-	then
-	    green "compiling $(basename ${file%.sail}.c)" "ok";
-	    if $DIR/a.out;
-	    then
-		green "tested $(basename ${file%.sail}) (C)" "ok"
-	    else
-		red "tested $(basename ${file%.sail}) (C)" "fail"
-	    fi
-	else
-	    red "compiling $file" "fail"
-	fi
-    else
-	red "compiling $file" "fail"
-    fi;
-
-    # if $SAILDIR/sail -no_warn -o out -ocaml $file 1> /dev/null 2> /dev/null;
-    # then
-    # 	green "compiling $(basename $file) (OCaml)" "ok"
-    # 	if $DIR/out;
-    # 	then
-    # 	    green "tested $(basename ${file%.sail}) (OCaml)" "ok"
-    # 	else
-    # 	    red "tested $(basename ${file%.sail}) (OCaml)" "fail"
-    # 	fi
-    # else
-    # 	red "compiling $(basename $file) (OCaml)" "fail"
-    # fi;
-
-    # mkdir -p "$LEMBUILDDIR"
-
-    # if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null;
-    # then
-    #     mv out.lem out_types.lem "$LEMBUILDDIR"
-    #     if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
-    #            -outdir "$LEMBUILDDIR" \
-    #            "$SAILDIR/src/gen_lib/sail_values.lem" \
-    #            "$SAILDIR/src/gen_lib/sail_operators.lem" \
-    #            "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
-    #            "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
-    #            "$SAILDIR/src/gen_lib/prompt.lem" \
-    #            "$SAILDIR/src/gen_lib/state_monad.lem" \
-    #            "$SAILDIR/src/gen_lib/state.lem" \
-    #            "$SAILDIR/src/gen_lib/prompt_monad.lem" \
-    #            "test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null;
-    #     then
-    #         cd "$LEMBUILDDIR"
-    #         if ocamlfind ocamlc -linkpkg -package zarith -package lem \
-    #                      sail_values.ml sail_operators.ml \
-    #                      sail_instr_kinds.ml prompt_monad.ml prompt.ml \
-    #                      sail_operators_mwords.ml state_monad.ml state.ml \
-    #                      test_extras.ml out_types.ml out.ml ../test.ml \
-    #                      -o test 1> /dev/null 2> /dev/null
-    #         then
-    #             green "compiling $(basename $file) (Lem)" "ok"
-    #             if ./test 1> /dev/null 2> /dev/null
-    #             then
-    # 	            green "tested $(basename ${file%.sail}) (Lem)" "ok"
-    #             else
-    # 	            red "tested $(basename ${file%.sail}) (Lem)" "fail"
-    #             fi
-    #         else
-    #             red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail"
-    #         fi
-    #         cd "$DIR"
-    #     else
-    #         red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail"
-    #     fi
-    # else
-    #     red "compiling $(basename $file) (Sail->Lem)" "fail"
-    # fi;
-
-    rm -rf $DIR/_sbuild/;
-    rm -rf "$LEMBUILDDIR";
-    rm -f Out_lemmas.thy;
-    rm -f out_types.lem;
-    rm -f out.lem;
-    rm -f ${file%.sail}.c;
-    rm -f a.out;
-    rm -f out
-done
-
-finish_suite "builtin testing"
-
-printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
deleted file mode 100755
index 37787605..00000000
--- a/test/c/run_tests.sh
+++ /dev/null
@@ -1,98 +0,0 @@
-
-#!/usr/bin/env bash
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-cd $DIR
-SAILDIR="$DIR/../.."
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-rm -f $DIR/tests.xml
-
-pass=0
-fail=0
-XML=""
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $DIR/tests.xml
-    XML=""
-    pass=0
-    fail=0
-}
-
-printf "<testsuites>\n" >> $DIR/tests.xml
-
-shopt -s nullglob;
-
-function run_c_tests {
-    for file in $DIR/*.sail;
-    do
-	if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null;
-	then
-	    green "compiling $(basename $file) ($SAIL_OPTS)" "ok";
-	    if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -lz -I $SAILDIR/lib;
-	    then
-		green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok";
-		$DIR/a.out 1> ${file%.sail}.result 2> /dev/null;
-		if diff ${file%.sail}.result ${file%.sail}.expect;
-		then
-		    green "executing $(basename ${file%.sail})" "ok"
-		else
-		    red "executing $(basename ${file%.sail})" "fail"
-		fi;
-		if valgrind -q --leak-check=full --errors-for-leak-kinds=all --error-exitcode=1 $DIR/a.out 1> /dev/null 2> /dev/null;
-		then
-		    green "executing $(basename ${file%.sail}) with valgrind" "ok"
-		else
-		    red "executing $(basename ${file%.sail}) with valgrind" "fail"
-		fi
-	    else
-		red "compiling generated C" "fail"
-	    fi
-	else
-	    red "compiling $file" "fail"
-	fi;
-	rm -f ${file%.sail}.c
-	rm -f ${file%.sail}.result
-    done
-}
-
-SAIL_OPTS=""
-CC_OPTS="-O0"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2 -fsanitize=undefined"
-run_c_tests
-
-finish_suite "C testing"
-
-printf "</testsuites>\n" >> $DIR/tests.xml