Merge pull request #190 from kth-step/riscv-symbexec

Z3 and SMT improvements, RISC-V work

Holmakefile

@@ -2,8 +2,7 @@ CLINE_OPTIONS = -r
 
 INCLUDES = $(HOLBADIR)/src/extra \
            $(HOLBADIR)/src/shared \
-           $(HOLBADIR)/src/shared/HolSmt \
-           $(HOLBADIR)/src/shared/sml-simplejson \
+           $(HOLBADIR)/src/shared/smt \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/models/l3mod \
@@ -12,6 +11,7 @@ INCLUDES = $(HOLBADIR)/src/extra \
            $(HOLBADIR)/src/theory/tools/wp \
            $(HOLBADIR)/src/theory/tools/comp \
            $(HOLBADIR)/src/theory/tools/backlifter \
+           $(HOLBADIR)/src/theory/tools/symbexec \
            $(HOLBADIR)/src/tools/lifter \
            $(HOLBADIR)/src/tools/wp \
            $(HOLBADIR)/src/tools/comp \

examples/bsl-wp-smt/Holmakefile

@@ -5,7 +5,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
            $(HOLDIR)/examples/l3-machine-code/riscv/model \
            $(HOLDIR)/examples/l3-machine-code/riscv/step \
-           $(HOLBADIR)/src/shared/HolSmt \
+           $(HOLBADIR)/src/shared/smt \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/tools/cfg \

examples/bsl-wp-smt/example-gauss-with-mem.sml

@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 open bslSyntax;
 open pretty_exnLib;
+open bir_smtLib;
 
 (* Load dependencies in interactive sessions *)
 val _ = if !Globals.interactive then (
@@ -11,8 +12,10 @@ val _ = if !Globals.interactive then (
 val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
 val _ = Globals.show_tags := true;
 
+val use_holsmt = true;
+
 val _ = if !Globals.interactive then () else (
-  Feedback.set_trace "HolBA_HolSmtLib" 0;
+  bir_smt_set_trace use_holsmt 0;
   Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 0;
   Feedback.set_trace "easy_noproof_wpLib" 2;
   Feedback.set_trace "Define.storage_message" 0;
@@ -24,8 +27,8 @@ val _ = Globals.linewidth := 100;
 val _ = Globals.show_types := true;
 val _ = Globals.show_assums := true;
 val _ = wordsLib.add_word_cast_printer ();
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 0;
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 4;
+val _ = bir_smt_set_trace use_holsmt 0;
+val _ = bir_smt_set_trace use_holsmt 4;
 val _ = Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 2;
 val _ = Feedback.set_trace "easy_noproof_wpLib" logLib.TRACE;
 val _ = Feedback.set_trace "Define.storage_message" 1;
@@ -92,8 +95,8 @@ fun prove_mem_gauss addr_len val_len =
 
         (* Prove it using an SMT solver *)
         val start_time = timer_start ();
-        val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-          handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+        val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+          handle e => raise pp_exn_s "bir_smt_prove failed" e
         val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
       in
         smt_thm
@@ -135,8 +138,8 @@ fun prove_mem_gauss addr_len val_len =
 
         (* Prove it using an SMT solver *)
         val start_time = timer_start ();
-        val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-          handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+        val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+          handle e => raise pp_exn_s "bir_smt_prove failed" e
         val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
       in
         smt_thm

examples/bsl-wp-smt/test-addrs-eq-imp-x42.sml

@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 open pretty_exnLib;
 open bir_programTheory;
+open bir_smtLib;
 
 (* Load dependencies in interactive sessions *)
 val _ = if !Globals.interactive then (
@@ -11,12 +12,14 @@ val _ = if !Globals.interactive then (
 val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
 val _ = Globals.show_tags := true;
 
+val use_holsmt = true;
+
 (*
 val _ = Globals.linewidth := 100;
 val _ = Globals.show_types := true;
 val _ = Globals.show_assums := true;
 val _ = wordsLib.add_word_cast_printer ();
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 0;
+val _ = bir_smt_set_trace use_holsmt 0;
 val _ = Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 2;
 val _ = Feedback.set_trace "easy_noproof_wpLib" logLib.TRACE;
 val _ = Feedback.set_trace "Define.storage_message" 1;
@@ -115,8 +118,8 @@ val addrs_eq_imp_x42_thm =
     val smt_ready_tm = bir_exp_to_wordsLib.bir2bool p_imp_wp_bir_tm
       handle e => raise pp_exn_s "bir2bool failed" e
   in
-    HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-      handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+    bir_smt_prove use_holsmt smt_ready_tm
+      handle e => raise pp_exn_s "bir_smt_prove failed" e
   end;
 val _ = (Hol_pp.print_thm addrs_eq_imp_x42_thm; print "\n");
 

examples/bsl-wp-smt/test-cjmp.sml

@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 open bslSyntax;
 open pretty_exnLib;
+open bir_smtLib;
 
 (* Load dependencies in interactive sessions *)
 val _ = if !Globals.interactive then (
@@ -11,13 +12,15 @@ val _ = if !Globals.interactive then (
 val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
 val _ = Globals.show_tags := true;
 
+val use_holsmt = true;
+
 (*
 val _ = Globals.linewidth := 100;
 val _ = Globals.show_types := true;
 val _ = Globals.show_assums := true;
 val _ = wordsLib.add_word_cast_printer ();
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 0;
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 4;
+val _ = bir_smt_set_trace use_holsmt 0;
+val _ = bir_smt_set_trace use_holsmt 4;
 val _ = Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 2;
 val _ = Feedback.set_trace "easy_noproof_wpLib" logLib.TRACE;
 val _ = Feedback.set_trace "Define.storage_message" 1;
@@ -81,7 +84,7 @@ val cjmp_thm =
 
     val _ = (Hol_pp.print_term smt_ready_tm; print "\n")
   in
-    HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-      handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+    bir_smt_prove use_holsmt smt_ready_tm
+      handle e => raise pp_exn_s "bir_smt_prove failed" e
   end;
 val _ = (Hol_pp.print_thm cjmp_thm; print "\n");

examples/bsl-wp-smt/test-gauss-no-mem.sml

@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 open bslSyntax;
 open pretty_exnLib;
+open bir_smtLib;
 
 (* Load dependencies in interactive sessions *)
 val _ = if !Globals.interactive then (
@@ -11,8 +12,10 @@ val _ = if !Globals.interactive then (
 val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
 val _ = Globals.show_tags := true;
 
+val use_holsmt = true;
+
 val _ = if !Globals.interactive then () else (
-  Feedback.set_trace "HolBA_HolSmtLib" 0;
+  bir_smt_set_trace use_holsmt 0;
   Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 0;
   Feedback.set_trace "easy_noproof_wpLib" 2;
   Feedback.set_trace "Define.storage_message" 0;
@@ -24,8 +27,8 @@ val _ = Globals.linewidth := 100;
 val _ = Globals.show_types := true;
 val _ = Globals.show_assums := true;
 val _ = wordsLib.add_word_cast_printer ();
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 0;
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 4;
+val _ = bir_smt_set_trace use_holsmt 0;
+val _ = bir_smt_set_trace use_holsmt 4;
 val _ = Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 2;
 val _ = Feedback.set_trace "easy_noproof_wpLib" logLib.TRACE;
 val _ = Feedback.set_trace "Define.storage_message" 1;
@@ -112,8 +115,8 @@ val s3_thm =
 
     (* Prove it using an SMT solver *)
     val start_time = timer_start ();
-    val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-      handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+    val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+      handle e => raise pp_exn_s "bir_smt_prove failed" e
     val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
   in
     smt_thm
@@ -156,8 +159,8 @@ val s2_thm =
 
     (* Prove it using an SMT solver *)
     val start_time = timer_start ();
-    val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-      handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+    val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+      handle e => raise pp_exn_s "bir_smt_prove failed" e
     val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
   in
     smt_thm

examples/bsl-wp-smt/wpsimp_test-gauss-no-mult.sml

@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 open bslSyntax;
 open pretty_exnLib;
+open bir_smtLib;
 
 (* Load dependencies in interactive sessions *)
 val _ = if !Globals.interactive then (
@@ -11,8 +12,10 @@ val _ = if !Globals.interactive then (
 val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
 val _ = Globals.show_tags := true;
 
+val use_holsmt = true;
+
 val _ = if !Globals.interactive then () else (
-  Feedback.set_trace "HolBA_HolSmtLib" 0;
+  bir_smt_set_trace use_holsmt 0;
   Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 0;
   Feedback.set_trace "easy_noproof_wpLib" logLib.INFO;
   Feedback.set_trace "Define.storage_message" 0;
@@ -24,8 +27,8 @@ val _ = Globals.linewidth := 100;
 val _ = Globals.show_types := true;
 val _ = Globals.show_assums := true;
 val _ = wordsLib.add_word_cast_printer ();
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 0;
-val _ = Feedback.set_trace "HolBA_HolSmtLib" 4;
+val _ = bir_smt_set_trace use_holsmt 0;
+val _ = bir_smt_set_trace use_holsmt 4;
 val _ = Feedback.set_trace "bir_wpLib.DEBUG_LEVEL" 2;
 val _ = Feedback.set_trace "easy_noproof_wpLib" logLib.TRACE;
 val _ = Feedback.set_trace "Define.storage_message" 1;
@@ -92,8 +95,8 @@ fun prove_mem_gauss addr_len val_len =
 
         (* Prove it using an SMT solver *)
         val start_time = timer_start ();
-        val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-          handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+        val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+          handle e => raise pp_exn_s "bir_smt_prove failed" e
         val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
       in
         smt_thm
@@ -139,8 +142,8 @@ fun prove_mem_gauss addr_len val_len =
 
         (* Prove it using an SMT solver *)
         val start_time = timer_start ();
-        val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
-          handle e => raise pp_exn_s "Z3_ORACLE_PROVE failed" e
+        val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
+          handle e => raise pp_exn_s "bir_smt_prove failed" e
 
         val _ = print ("SMT solver took: " ^ (timer_stop start_time) ^ " sec\n");
       in

examples/ijr/resolveFullyLib.sml

@@ -5,7 +5,8 @@ open HolKernel Parse boolLib bossLib;
 open optionSyntax bir_htSyntax bir_wm_instSyntax;
 
 open bir_wp_interfaceLib;
-open tutorial_smtSupportLib;
+open bslSyntax;
+open bir_smtLib;
 open bir_compositionLib;
 
 open listTheory;
@@ -92,7 +93,7 @@ fun prove_and_transfer_contract(prog'_thm, prefix, pre_tm, entry_label_tm, endin
     (*Prove implication using SMT solvers*)
     val smt_start = timer_start ()
     val contract_imp = bimp (pre_tm, (lhs o concl) wp_def)
-    val contract_imp_taut_thm = prove_exp_is_taut contract_imp
+    val contract_imp_taut_thm = bir_smt_prove_is_taut contract_imp
     val contract = label_ct_to_simp_ct_predset ht_thm' contract_imp_taut_thm
     val _ = print ("SMT time: " ^ timer_stop_str smt_start ^ "\n")
 

examples/nic/Holmakefile

@@ -5,7 +5,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
            $(HOLDIR)/examples/l3-machine-code/riscv/model \
            $(HOLDIR)/examples/l3-machine-code/riscv/step \
-           $(HOLBADIR)/src/shared/HolSmt \
+           $(HOLBADIR)/src/shared/smt \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

examples/nic/nic_helpersLib.sml

@@ -3,8 +3,11 @@ struct
 
   open HolKernel Parse boolLib bossLib;
   open bslSyntax;
+  open bir_smtLib;
   open pretty_exnLib;
 
+  val use_holsmt = true;
+
   val ERR = mk_HOL_ERR "nic_helpersLib";
   val wrap_exn = Feedback.wrap_exn "nic_helpersLib";
 
@@ -132,20 +135,20 @@ struct
 
       (* Prove it using an SMT solver *)
       val start_time = timer_start ();
-      val smt_thm = HolBA_HolSmtLib.Z3_ORACLE_PROVE smt_ready_tm
+      val smt_thm = bir_smt_prove use_holsmt smt_ready_tm
         handle sat_exn => (* Pretty-exn + try to show a SAT model if level_log=DEBUG *)
           let
             (* Wrap the exn, and pretty-print it to the user *)
-            val wrapped_exn = pp_exn_s (proof_prefix ^ "Z3_ORACLE_PROVE failed") (wrap_exn sat_exn);
+            val wrapped_exn = pp_exn_s (proof_prefix ^ "bir_smt_prove failed") (wrap_exn sat_exn);
 
             (* Show a SAT model if level_log=DEBUG *)
             val _ = if not (!level_log >= logLib.DEBUG) then () else
               let
                 fun print_model model = List.foldl
                   (fn ((name, tm), _) => (print (" - " ^ name ^ ": "); pprint_term tm))
                   () (rev model)
-                val _ = debug "Asking Z3 for a SAT model..."
-                val model = Z3_SAT_modelLib.Z3_GET_SAT_MODEL (mk_neg smt_ready_tm)
+                val _ = debug "Asking bir_smt for a SAT model..."
+                val model = bir_smt_get_model use_holsmt (mk_neg smt_ready_tm)
                 val _ = (debug "SAT model:"; print_model model; print "\n")
               in () end
                 handle _ => debug "Failed to compute a SAT model. Ignoring.";

examples/nic/prove_hol_triple_using_bir_progScript.sml

@@ -525,7 +525,7 @@ val (wp_thm, triple_thm) =
         FULL_SIMP_TAC bir_to_words_ss [] >>
 
         (REPEAT o PAT_X_TAC) `_` >>
-        HolBA_HolSmtLib.Z3_ORACLE_TAC
+        bir_smt_tac use_holsmt
       ) >>
       METIS_TAC [bir_exec_to_labels_triple_def]
 *)

examples/riscv/Holmakefile

@@ -4,7 +4,8 @@ INCLUDES = $(HOLBADIR)/examples/riscv/swap \
            $(HOLBADIR)/examples/riscv/incr \
            $(HOLBADIR)/examples/riscv/incr-mem \
            $(HOLBADIR)/examples/riscv/mod2-mem \
-           $(HOLBADIR)/examples/riscv/isqrt
+           $(HOLBADIR)/examples/riscv/isqrt \
+           $(HOLBADIR)/examples/riscv/aes
 
 all: $(DEFAULT_TARGETS) test-riscv.exe
 .PHONY: all

examples/riscv/aes-unopt/Holmakefile

@@ -15,16 +15,15 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/src/tools/comp \
            $(HOLBADIR)/src/tools/wp \
            $(HOLBADIR)/src/tools/backlifter \
-           $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common
+           $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all
 
 ifdef POLY
 ifndef HOLBA_POLYML_HEAPLESS
-HOLHEAP = $(HOLBADIR)/examples/riscv/common/holba-riscv-heap
+HOLHEAP = $(HOLBADIR)/src/holba-heap
 endif
 endif

examples/riscv/aes-unopt/aes_symb_execScript.sml

@@ -12,7 +12,7 @@ val _ = new_theory "aes_symb_exec";
 (* prepare program lookups     *)
 (* --------------------------- *)
 
-val bir_lift_thm = birs_auxLib.patch_lifter_thm bir_aes_riscv_lift_THM;
+val bir_lift_thm = bir_aes_riscv_lift_THM;
 val _ = birs_auxLib.prepare_program_lookups bir_lift_thm;
 
 (* --------------------------- *)

examples/riscv/aes/Holmakefile

@@ -15,16 +15,15 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/src/tools/comp \
            $(HOLBADIR)/src/tools/wp \
            $(HOLBADIR)/src/tools/backlifter \
-           $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common
+           $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all
 
 ifdef POLY
 ifndef HOLBA_POLYML_HEAPLESS
-HOLHEAP = $(HOLBADIR)/examples/riscv/common/holba-riscv-heap
+HOLHEAP = $(HOLBADIR)/src/holba-heap
 endif
 endif