Merge branch 'collected_fixes' into riscv-symbexec

src/shared/examples/test-smtlibLib.sml

@@ -73,7 +73,13 @@ val exporting_exp_testcases = [
   (``BExp_UnaryExp BIExp_Not (BExp_Cast BIExp_LowCast
         (BExp_Den (BVar "xyz" (BType_Imm Bit32)))
         Bit1)``,
-   ("(not (= ((_ extract 0 0) birv_xyz) (_ bv1 1)))", SMTTY_Bool))
+   ("(not (= ((_ extract 0 0) birv_xyz) (_ bv1 1)))", SMTTY_Bool)),
+
+
+  (``(BExp_BinPred BIExp_Equal (BExp_Den (BVar "syf_20" (BType_Imm Bit1)))
+        (BExp_Cast BIExp_LowCast (BExp_Den (BVar "sy_R4" (BType_Imm Bit32)))
+           Bit1))``,
+   ("(= birv_syf_20 (= ((_ extract 0 0) birv_sy_R4) (_ bv1 1)))", SMTTY_Bool))
 ];
 
 (*

src/shared/holba_miscLib.sml

@@ -38,10 +38,14 @@ val s = ""
     end;
 
 (* timers *)
-  fun timer_start level = if (1 >= level) then SOME (Time.now()) else NONE;
+  fun timer_raw_start () = Time.now();
+  fun timer_raw_stop tm = Time.- (Time.now(), tm);
+  fun timer_raw_stop_ms tm = Time.toMilliseconds (timer_raw_stop tm);
+
+  fun timer_start level = if (1 >= level) then SOME (timer_raw_start()) else NONE;
   fun timer_stop f NONE = ()
     | timer_stop f (SOME tm) = let
-       val d_time = Time.- (Time.now(), tm);
+       val d_time = timer_raw_stop tm;
        in f ((Time.toString d_time) ^ "s") end;
 
 end (* local *)

src/shared/smt/bir_smtlibLib.sml

@@ -300,6 +300,18 @@ fun is_bir_eq_abbrevd e =
 fun smtlib_wrap_to_bool   str = "(= #b1 " ^ str ^ ")";
 fun smtlib_wrap_from_bool str = "(ite " ^ str ^ " #b1 #b0)";
 
+(*
+fun unify_args args =
+  let
+    fun bv2bool (str, bvty) = if bvty = SMTTY_BV 1 then ("(= " ^ str ^ " (_ bv1 1))", SMTTY_Bool) else (str, bvty);
+  in
+    if List.exists (fn (_,ty) => ty = SMTTY_Bool) args then
+      List.map bv2bool args
+    else
+      args
+  end;
+*)
+
 fun to_smtlib_bool (str, sty) =
   if sty = SMTTY_Bool then
     (str, sty)
@@ -424,8 +436,13 @@ BExp_Cast BIExp_LowCast
           val caststr = castt_to_smtlib castt stre exp_szi szi;
 
           val castval = (caststr, sty);
+          val castval_fixed =
+            if sty = SMTTY_BV 1 then
+              ("(= " ^ caststr ^ " (_ bv1 1))", SMTTY_Bool)
+            else
+              castval;
         in
-          (exst1, castval)
+          (exst1, castval_fixed)
         end
 
       else if is_BExp_UnaryExp exp then
@@ -468,7 +485,8 @@ BExp_Cast BIExp_LowCast
           val (exst2, val2) = bexp_to_smtlib false exst1 exp2;
           val args = [val1, val2];
 
-          fun probfun () = problem exp "binary predicate operator needs same type for both sides: ";
+          fun probfun () = problem exp ("binary predicate operator needs same type for both sides: ");
+          (*fun probfun () = problem exp ("binary predicate operator needs same type for both sides: (1," ^ (smt_type_to_smtlib (snd val1)) ^ ": " ^ (fst val1) ^ ")(2," ^ (smt_type_to_smtlib (snd val2)) ^ ": " ^ (fst val2) ^ ")  :  ");*)
 
           val bpredopval = bpredop_to_smtlib probfun bpredop args;
         in

src/shared/smt/holba_z3Lib.sml

@@ -38,9 +38,9 @@ val use_stack = true;
 val debug_print = ref false;
 fun kill_z3proc z3p =
   let
-    val _ = endmeexit z3p;
     val _ = z3proc_o := NONE;
     val _ = z3proc_bin_o := NONE;
+    val _ = endmeexit z3p;
   in
     ()
   end;
@@ -59,24 +59,26 @@ fun get_z3proc z3bin =
         val _ = if not (!debug_print) then () else
 	        print ("starting: " ^ z3bin ^ "\n");
         val p = openz3 z3bin;
-	val _ = z3proc_bin_o := SOME z3bin;
-	val _ = if not use_stack then () else
-	 let
-          val (_,s_out) = get_streams p;
-          (* prepare prelude and push *)
-          val () = TextIO.output (s_out, prelude_z3 ^ "\n");
-          val () = TextIO.output (s_out, "(push)\n");
-	 in
-	  ()
-	 end;
-      in (z3proc_o := SOME p; p) end;
+    val _ = z3proc_bin_o := SOME z3bin;
+    val _ = if not use_stack then () else
+    let
+            val (_,s_out) = get_streams p;
+            (* prepare prelude and push *)
+            val () = TextIO.output (s_out, prelude_z3 ^ "\n");
+            val () = TextIO.output (s_out, "(push)\n");
+    in
+      ()
+    end;
+        in (z3proc_o := SOME p; p) end;
   in
     p
   end;
 
 fun reset_z3proc () =
   case !z3proc_o of
-      SOME z3p => kill_z3proc z3p
+      SOME z3p =>
+        (kill_z3proc z3p
+        handle _ => ())
     | NONE => ();
 
 val z3wrapproc_o = ref (NONE : ((TextIO.instream, TextIO.outstream) Unix.proc) option);
@@ -113,6 +115,7 @@ fun inputLines_until m ins acc =
       inputLines_until m ins (line::acc)
   end
 
+exception Z3EXN of exn;
 fun sendreceive_query z3bin q =
  let
    val _ = if not (!debug_print) then () else
@@ -140,7 +143,8 @@ fun sendreceive_query z3bin q =
 	     TextIO.output (s_out, "(push)\n"));
  in
    out_lines
- end;
+ end
+ handle e => raise Z3EXN e;
 
 fun sendreceive_wrap_query q =
  let
@@ -183,23 +187,61 @@ fun sendreceive_wrap_query q =
       raise ERR "get_default_z3"
         "Z3 not configured: set the HOL4_Z3_EXECUTABLE environment variable to point to the Z3 executable file.";
 
+  fun querysmt_raw_retry retries is_nok do_if_nok sendrec_qf q =
+    let
+      val timer = holba_miscLib.timer_raw_start ();
+      val out_lines = sendrec_qf q;
+      val time = Int.fromLarge (holba_miscLib.timer_raw_stop_ms timer);
+      val is_nok_res = is_nok out_lines;
+      (*val _ = List.app print out_lines;*)
+    in
+      if is_nok_res andalso retries > 0 then (
+        do_if_nok ();
+        querysmt_raw_retry (retries-1) is_nok do_if_nok sendrec_qf q
+      ) else
+        (time, out_lines, not is_nok_res)
+    end;
+
+  val querysmt_raw_timeout_override = ref (NONE: int option);
+  val querysmt_raw_retries = ref 0;
+  val querysmt_raw_query_times = ref (NONE: int list option);
+  val querysmt_raw_unknown_as_timeout = ref false;
+  exception Z3TIMEOUT of int * string; (* time of query, query string *)
+  fun is_timeout out_lines = out_lines = ["unknown\n"];
   fun querysmt_raw z3bin_o timeout_o q =
-      let
-        val z3bin = case z3bin_o of
-	     NONE => get_default_z3 ()
-	   | SOME x => x;
-	val (timeout_s_before, timeout_s_after) =
-	  case timeout_o of
-             NONE => ("", "")
-           | SOME timeout => ("(set-option :timeout " ^ (Int.toString timeout) ^ ")\n\n", "(set-option :timeout 4294967295)\n");
-	val q_wto =
-	  (timeout_s_before ^
-           q ^
-	   timeout_s_after)
-        val out_lines = sendreceive_query z3bin q_wto;
-      in
-        out_lines
-      end;
+    let
+      val z3bin = case z3bin_o of
+          NONE => get_default_z3 ()
+        | SOME x => x;
+      val timeout_o =
+        case !querysmt_raw_timeout_override of
+            NONE => timeout_o
+          | SOME x => SOME x;
+      val (timeout_s_before, timeout_s_after) =
+        case timeout_o of
+                NONE => ("", "")
+              | SOME timeout => ("(set-option :timeout " ^ (Int.toString timeout) ^ ")\n\n", "(set-option :timeout 4294967295)\n");
+      val q_wto =
+        (timeout_s_before ^
+              q ^
+        timeout_s_after);
+
+      val retries = (!querysmt_raw_retries);
+      val (time, out_lines) =
+        case querysmt_raw_retry retries is_timeout reset_z3proc (sendreceive_query z3bin) q_wto of
+            (time, x, is_ok) =>
+              if is_ok orelse (not (!querysmt_raw_unknown_as_timeout)) then
+                (time, x)
+              else
+                raise Z3TIMEOUT (time, q);
+
+      val querysmt_raw_query_times_o = !querysmt_raw_query_times;
+      val _ = case querysmt_raw_query_times_o of
+          NONE => ()
+        | SOME x => querysmt_raw_query_times := SOME (time::x);
+    in
+      out_lines
+    end;
 
   fun querysmt_prepare_getmodel z3bin_o =
     querysmt_raw z3bin_o NONE "(set-option :model.compact false)\n";

src/theory/tools/symbexec/bir_symb_simpScript.sml

@@ -207,6 +207,14 @@ Definition birs_exp_imp_def:
     )
 End
 
+Theorem symb_exp_imp_EQ_pcondwiden_thm:
+  !sr pcond pcond'.
+  (symb_exp_imp sr pcond pcond') <=>
+  (symb_pcondwiden sr pcond pcond')
+Proof
+  rw [symb_exp_imp_def, symb_rulesTheory.symb_pcondwiden_def]
+QED
+
 Theorem birs_exp_imp_thm:
   !prog.
 !pcond pcond'.
@@ -342,6 +350,22 @@ Proof
   subexpression_simp_TAC
 QED
 
+Theorem birs_simplification_Store_val_thm:
+  !pcond symbexp1 symbexp1' bme bade en.
+  (birs_simplification pcond symbexp1 symbexp1') ==>
+  (birs_simplification pcond (BExp_Store bme bade en symbexp1) (BExp_Store bme bade en symbexp1'))
+Proof
+  subexpression_simp_TAC
+QED
+
+Theorem birs_simplification_Store_mem_thm:
+  !pcond symbexp1 symbexp1' bme bad en bve.
+  (birs_simplification pcond symbexp1 symbexp1') ==>
+  (birs_simplification pcond (BExp_Store symbexp1 bad en bve) (BExp_Store symbexp1' bad en bve))
+Proof
+  subexpression_simp_TAC
+QED
+
 
 
 

src/theory/tools/symbexec/bir_symb_soundScript.sml

@@ -294,6 +294,31 @@ QED
 symb_mk_exp_conj_f_sound sr
 =========================================================================
  *)
+Definition birs_symb_expr_conj_eq_def:
+  birs_symb_expr_conj_eq e1 e2 conj1 =
+      BExp_BinExp BIExp_And
+        (if option_CASE (type_of_bir_exp e1) F bir_type_is_Mem then BExp_MemEq e1 e2 else BExp_BinPred BIExp_Equal e1 e2)
+        conj1
+End
+
+Theorem birs_symb_expr_conj_eq_thm:
+  !prog e1 e2 conj1.
+    (symb_expr_conj_eq (bir_symb_rec_sbir prog) e1 e2 conj1 =
+     birs_symb_expr_conj_eq e1 e2 conj1)
+Proof
+  SIMP_TAC (std_ss++symb_TYPES_ss) [bir_symb_rec_sbir_def, birs_symb_expr_conj_eq_def, symb_record_soundTheory.symb_expr_conj_eq_def] >>
+  METIS_TAC []
+QED
+
+Theorem birs_symb_expr_conj_eq_thm2:
+  !e1 e2 conj1.
+    (?bt. type_of_bir_exp e1 = SOME (BType_Imm bt)) ==>
+    (birs_symb_expr_conj_eq e1 e2 conj1 =
+     BExp_BinExp BIExp_And (BExp_BinPred BIExp_Equal e1 e2) conj1)
+Proof
+  rpt strip_tac >>
+  gvs [birs_symb_expr_conj_eq_def, bir_valuesTheory.bir_type_is_Mem_def]
+QED
 
 Theorem birs_symb_mk_exp_conj_f_sound_thm:
   !prog.
@@ -429,6 +454,78 @@ SIMP_TAC (std_ss++symb_TYPES_ss) [symb_subst_f_sound_def, bir_symb_rec_sbir_def]
   METIS_TAC [bir_exp_subst1_USED_VARS]
 QED
 
+Definition birs_symb_env_subst_def:
+  birs_symb_env_subst s env =
+    OPTION_MAP (bir_exp_subst s) o env
+End
+
+Definition birs_symb_subst_def:
+  birs_symb_subst s bs =
+    (bs
+      with bsst_pcond := bir_exp_subst s bs.bsst_pcond)
+      with bsst_environ := birs_symb_env_subst s bs.bsst_environ
+End
+
+Definition birs_symb_env_subst1_def:
+  birs_symb_env_subst1 v e env =
+    OPTION_MAP (bir_exp_subst1 v e) o env
+End
+
+Definition birs_symb_subst1_def:
+  birs_symb_subst1 (v,e) bs =
+    (bs
+      with bsst_pcond := bir_exp_subst1 v e bs.bsst_pcond)
+    with bsst_environ := birs_symb_env_subst1 v e bs.bsst_environ
+End
+
+Theorem birs_symb_subst1_REWR_thm:
+  !v e pc env status pcond.
+  birs_symb_subst1 (v,e)
+    <|bsst_pc := pc;
+      bsst_environ := env;
+      bsst_status := status;
+      bsst_pcond := pcond|> =
+  <|bsst_pc := pc;
+    bsst_environ := birs_symb_env_subst1 v e env;
+    bsst_status := status;
+    bsst_pcond := bir_exp_subst1 v e pcond|>
+Proof
+  rpt strip_tac >>
+  rw [birs_symb_subst1_def]
+QED
+
+Theorem birs_symb_subst1_thm:
+  !s.
+  birs_symb_subst1 s =
+    birs_symb_subst (FEMPTY |+ s)
+Proof
+  Cases_on `s` >>
+  CONV_TAC FUN_EQ_CONV >>
+  rpt gen_tac >>
+  rw [birs_symb_subst_def, birs_symb_subst1_def] >>
+  rw [birs_symb_env_subst1_def, birs_symb_env_subst_def, bir_exp_substitutionsTheory.bir_exp_subst1_def]
+QED
+
+Theorem birs_symb_subst1_EQ_thm:
+  !prog s bs.
+    symb_subst (bir_symb_rec_sbir prog) s (birs_symb_to_symbst bs) =
+    birs_symb_to_symbst (birs_symb_subst1 s bs)
+Proof
+  Cases_on `bs` >>
+  Cases_on `s` >>
+  fs [symb_subst_def, birs_symb_to_symbst_def, birs_symb_subst1_def, symb_symbst_pc_def, symb_symbst_store_def, symb_symbst_pcond_def, symb_symbst_extra_def, symb_subst_store_def] >>
+  fs [bir_symb_rec_sbir_def, combinTheory.o_DEF, birs_symb_env_subst1_def]
+QED
+
+Theorem birs_symb_subst1_set_EQ_thm:
+  !prog s Pi.
+    symb_subst_set (bir_symb_rec_sbir prog) s (IMAGE birs_symb_to_symbst Pi) =
+    IMAGE birs_symb_to_symbst (IMAGE (birs_symb_subst1 s) Pi)
+Proof
+  fs [symb_subst_set_def, pred_setTheory.IMAGE_IMAGE, combinTheory.o_DEF] >>
+  fs [birs_symb_subst1_EQ_thm]
+QED
+
 
 (*
 =========================================================================