From b9a051d186593fdd3bbf295e20f7ace78e668580 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Dec 2018 22:37:04 +0000 Subject: 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. --- src/constraint.ml | 3 +- src/type_check.ml | 34 ++++------- test/builtins/run_tests.sh | 140 --------------------------------------------- test/c/run_tests.sh | 98 ------------------------------- 4 files changed, 14 insertions(+), 261 deletions(-) delete mode 100755 test/builtins/run_tests.sh delete mode 100755 test/c/run_tests.sh 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+=" \n" -} - -function yellow { - (( fail += 1 )) - printf "$1: ${YELLOW}$2${NC}\n" - XML+=" \n $2\n \n" -} - -function red { - (( fail += 1 )) - printf "$1: ${RED}$2${NC}\n" - XML+=" \n $2\n \n" -} - -function finish_suite { - printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n" - XML=" \n$XML \n" - printf "$XML" >> $DIR/tests.xml - XML="" - pass=0 - fail=0 -} - -printf "\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 "\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+=" \n" -} - -function yellow { - (( fail += 1 )) - printf "$1: ${YELLOW}$2${NC}\n" - XML+=" \n $2\n \n" -} - -function red { - (( fail += 1 )) - printf "$1: ${RED}$2${NC}\n" - XML+=" \n $2\n \n" -} - -function finish_suite { - printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n" - XML=" \n$XML \n" - printf "$XML" >> $DIR/tests.xml - XML="" - pass=0 - fail=0 -} - -printf "\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 "\n" >> $DIR/tests.xml -- cgit v1.2.3