diff options
| -rw-r--r-- | aarch64_small/Makefile | 3 | ||||
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 3 | ||||
| -rwxr-xr-x | test/aarch64_small/run_tests.sh | 7 |
4 files changed, 13 insertions, 2 deletions
diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile index fe4c5841..c1751a45 100644 --- a/aarch64_small/Makefile +++ b/aarch64_small/Makefile @@ -23,6 +23,9 @@ armV8.lem: $(SOURCES) # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem $(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^ +smt: $(SOURCES) + $(SAIL) $(SAILFLAGS) -smt $^ + for-rmem/armV8.lem: $(SOURCES) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 5165904d..dbbb10e0 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -670,7 +670,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_cons", [aval1; aval2], unit_typ)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 7e062c5a..2066021e 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1568,8 +1568,9 @@ let sort_ctype_defs cdefs = let compile_ast ctx (Defs defs) = let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in + let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in if !opt_memo_cache then (try diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh index dc2bdde4..424252de 100755 --- a/test/aarch64_small/run_tests.sh +++ b/test/aarch64_small/run_tests.sh @@ -52,6 +52,13 @@ else red "failed to build lem" "fail" fi +if make -B -C ../../aarch64_small smt SAIL="$SAILDIR/sail" +then + green "compiled aarch64_small for SMT generation" "ok" +else + red "failed to build aarch64_small for SMT generation" "fail" +fi + finish_suite "aarch64_small tests" printf "</testsuites>\n" >> $DIR/tests.xml |