Various improvements

kth-step · Nov 24, 2024 · fc70921 · fc70921
1 parent 1c09f87
commit fc70921
Show file tree

Hide file tree

Showing 7 changed files with 293 additions and 183 deletions.
diff --git a/src/tools/symbexec/aux_moveawayLib.sml b/src/tools/symbexec/aux_moveawayLib.sml
@@ -42,6 +42,37 @@ in (* local *)
       f_wrapped
     end;
 
+  val EQ_flip = mk_eq o (fn (x,y) => (y,x)) o dest_eq;
+  fun wrap_cache_result_EQ_BEQ_gen to_intform to_k to_flip_k kcomp f =
+    let
+      val (add, lookup) = result_cache kcomp;
+      fun f_wrapped x =
+        let
+          val (x1,x2) = dest_eq x;
+          val intform = (to_intform x1, to_intform x2);
+          val k = (to_k intform);
+          val v_o = lookup k;
+        in
+          if isSome v_o then valOf v_o else
+          let
+            val v = f x;
+          in
+            add (k, v);
+            add (to_flip_k intform, CONV_RULE (LHS_CONV SYM_CONV) v);
+            v
+          end
+        end;
+    in
+      f_wrapped
+    end;
+
+  fun to_eq_string (s1, s2) =
+    s1^"="^s2;
+  fun to_flip_eq_string (s1, s2) =
+    s2^"="^s1;
+  fun wrap_cache_result_EQ_BEQ_string to_string = wrap_cache_result_EQ_BEQ_gen to_string to_eq_string to_flip_eq_string String.compare;
+
+  (*val wrap_cache_result_EQ_BEQ = wrap_cache_result_EQ_BEQ_gen I EQ_flip; *)
   fun wrap_cache_result_EQ_BEQ kcomp f =
     let
       val (add, lookup) = result_cache kcomp;
@@ -54,7 +85,7 @@ in (* local *)
             val v = f k;
           in
             add (k, v);
-            add ((*(rhs o concl o SYM_CONV)*)(mk_eq o (fn (x,y) => (y,x)) o dest_eq) k, CONV_RULE (LHS_CONV SYM_CONV) v);
+            add ((*(rhs o concl o SYM_CONV)*)EQ_flip k, CONV_RULE (LHS_CONV SYM_CONV) v);
             v
           end
         end;
@@ -86,6 +117,38 @@ in (* local *)
       f_wrapped
     end;
 
+  local
+    datatype res_ex_t = Result of thm | Except of exn;
+    fun capture_res_ex f x =
+      Result(f x)
+      handle e => Except e
+    fun process_res_ex v =
+      case v of
+          Result x => x
+        | Except e => raise e;
+  in
+    fun wrap_res_exn f =
+      let
+        val (add, lookup) = result_cache Term.compare;
+        fun f_wrapped k =
+          let
+            val v_o = lookup k;
+          in
+            case v_o of
+                SOME v => process_res_ex v
+              | _ =>
+                let
+                  val v = capture_res_ex f k;
+                in
+                  add (k, v);
+                  process_res_ex v
+                end
+          end;
+      in
+        f_wrapped
+      end;
+  end
+
 fun measure_fun s f v =
   let
     val timer = holba_miscLib.timer_start 0;

diff --git a/src/tools/symbexec/aux_setLib.sml b/src/tools/symbexec/aux_setLib.sml
@@ -82,127 +82,14 @@ in (* local *)
       )
     end;
   *)
-  local
-    datatype res_ex_t = Result of thm | Except of exn;
-    fun capture_res_ex f x =
-      Result(f x)
-      handle e => Except e
-    fun process_res_ex v =
-      case v of
-          Result x => x
-        | Except e => raise e;
-  in
-    fun wrap_res_exn f =
-      let
-        val (add, lookup) = aux_moveawayLib.result_cache Term.compare;
-        fun f_wrapped k =
-          let
-            val v_o = lookup k;
-          in
-            case v_o of
-                SOME v => process_res_ex v
-              | _ =>
-                let
-                  val v = capture_res_ex f k;
-                in
-                  add (k, v);
-                  process_res_ex v
-                end
-          end;
-      in
-        f_wrapped
-      end;
-  end
-
-
-  (* eliminate left conjuncts first *)
-  val CONJL_CONV =
-    let
-      val thm_T = (GEN_ALL o (fn x => List.nth(x,0)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES;
-      val thm_F = (GEN_ALL o (fn x => List.nth(x,2)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES;
-    in
-      fn lconv => fn rconv =>
-      (LAND_CONV lconv) THENC
-      (fn tm =>
-        if (identical T o fst o dest_conj) tm then
-          (REWR_CONV thm_T THENC rconv) tm
-        else
-          (REWR_CONV thm_F) tm)
-    end;
-  (* eliminate right conjuncts first *)
-  val CONJR_CONV =
-    let
-      val thm_T = (GEN_ALL o (fn x => List.nth(x,1)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES;
-      val thm_F = (GEN_ALL o (fn x => List.nth(x,3)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES;
-    in
-      fn lconv => fn rconv =>
-      (RAND_CONV rconv) THENC
-      (fn tm =>
-        if (identical T o snd o dest_conj) tm then
-          (REWR_CONV thm_T THENC lconv) tm
-        else
-          (REWR_CONV thm_F) tm)
-    end;
-
-  (* eliminate left disjuncts first *)
-  val DISJL_CONV =
-    let
-      val thm_T = (GEN_ALL o (fn x => List.nth(x,0)) o CONJUNCTS o SPEC_ALL) boolTheory.OR_CLAUSES;
-      val thm_F = (GEN_ALL o (fn x => List.nth(x,2)) o CONJUNCTS o SPEC_ALL) boolTheory.OR_CLAUSES;
-    in
-      fn lconv => fn rconv =>
-      (LAND_CONV rconv) THENC
-      (fn tm =>
-        if (identical F o fst o dest_disj) tm then
-          (REWR_CONV thm_F THENC lconv) tm
-        else
-          (REWR_CONV thm_T) tm)
-    end;
-  (* eliminate right disjuncts first *)
-  val DISJR_CONV =
-    let
-      val thm_T = (GEN_ALL o (fn x => List.nth(x,1)) o CONJUNCTS o SPEC_ALL) boolTheory.OR_CLAUSES;
-      val thm_F = (GEN_ALL o (fn x => List.nth(x,3)) o CONJUNCTS o SPEC_ALL) boolTheory.OR_CLAUSES;
-    in
-      fn lconv => fn rconv =>
-      (RAND_CONV rconv) THENC
-      (fn tm =>
-        if (identical F o snd o dest_disj) tm then
-          (REWR_CONV thm_F THENC lconv) tm
-        else
-          (REWR_CONV thm_T) tm)
-    end;
-
-  fun NEG_CONV conv =
-    RAND_CONV conv THENC
-    REWRITE_CONV [boolTheory.NOT_CLAUSES];
-
-  local
-    val thm_T = (CONJUNCT1 o SPEC_ALL) boolTheory.COND_CLAUSES;
-    val thm_F = (CONJUNCT2 o SPEC_ALL) boolTheory.COND_CLAUSES;
-    fun get_cond_c tm =
-      let val (c,_,_) = dest_cond tm;
-      in c end;
-    fun clean_conv tm =
-      if (identical T o get_cond_c) tm then
-        REWR_CONV thm_T tm
-      else
-        REWR_CONV thm_F tm;
-  in
-    fun ITE_CONV conv =
-      RATOR_CONV (RATOR_CONV (RAND_CONV conv)) THENC
-      clean_conv;
-    val ITE_CONV = fn conv => Profile.profile "auxset_ITE_CONV" (ITE_CONV (Profile.profile "auxset_ITE_CONV_conv" conv));
-  end
-
 
   local
     val inter_empty_thm = CONJUNCT1 pred_setTheory.INTER_EMPTY;
     (* this function is not end-recursive *)
-    fun INTER_CONV_helper ite_conv =
-      IFC
-        (REWR_CONV pred_setTheory.INSERT_INTER)
-        (ite_conv THENC
+    fun INTER_CONV_helper ite_conv tm =
+      (if (is_insert o fst o dest_inter) tm then
+        REWR_CONV pred_setTheory.INSERT_INTER THENC
+        ite_conv THENC
         (fn tm_ =>
           (if is_inter tm_ then
               INTER_CONV_helper ite_conv
@@ -211,18 +98,17 @@ in (* local *)
             else if is_empty tm_ then
               ALL_CONV
             else raise ERR "INTER_CONV" "unexpected")
-          tm_))
-        (REWR_CONV inter_empty_thm);
+          tm_)
+      else
+        REWR_CONV inter_empty_thm) tm;
   in
     fun INTER_CONV el_EQ_CONV tm =
       let
         val ite_conv = ITE_CONV (pred_setLib.IN_CONV el_EQ_CONV);
-        val ite_conv = Profile.profile "auxset_INTER_CONV_ite" ite_conv;
       in
         INTER_CONV_helper ite_conv tm
         handle e => (print_term tm; raise wrap_exn ("@INTER_CONV") e)
       end;
-    val INTER_CONV = fn x => Profile.profile "auxset_INTER_CONV" (INTER_CONV x);
   end
 
   local
@@ -249,15 +135,13 @@ in (* local *)
     fun DIFF_CONV el_EQ_CONV tm =
       let
         val delete_conv = pred_setLib.DELETE_CONV el_EQ_CONV;
-        val delete_conv = Profile.profile "auxset_DIFF_CONV_delete" delete_conv;
       in
         if (is_sing o snd o dest_diff) tm then
           (REWR_CONV delete_thm THENC delete_conv) tm
         else
           DIFF_CONV_helper delete_conv $ REFL $ tm
         handle e => (print_term tm; raise wrap_exn ("@DIFF_CONV") e)
       end;
-    val DIFF_CONV = fn x => Profile.profile "auxset_DIFF_CONV" (DIFF_CONV x);
   end
 
   local
@@ -283,15 +167,13 @@ in (* local *)
     fun BIGUNION_CONV el_EQ_CONV tm =
       let
         val union_conv = pred_setLib.UNION_CONV el_EQ_CONV;
-        val union_conv = Profile.profile "auxset_BIGUNION_CONV_union" union_conv;
       in
         if (is_insert o dest_bigunion) tm then
           BIGUNION_CONV_helper union_conv (REWR_CONV BIGUNION_INSERT tm)
         else
           REWR_CONV BIGUNION_EMPTY tm
         handle e => (print_term tm; raise wrap_exn ("@BIGUNION_CONV") e)
       end;
-    val BIGUNION_CONV = fn x => Profile.profile "auxset_BIGUNION_CONV" (BIGUNION_CONV x);
   end
 
 (* ================================================================================== *)
@@ -370,6 +252,7 @@ in (* local *)
 (* ---------------------------------------------------------------------------------- *)
   val bir_varname_EQ_CONV =
     stringLib.string_EQ_CONV;
+  val bir_varname_EQ_CONV = aux_moveawayLib.wrap_cache_result_EQ_BEQ_string stringLib.fromHOLstring bir_varname_EQ_CONV;
   val bir_varname_EQ_CONV = Profile.profile "auxset_bir_varname_EQ_CONV" bir_varname_EQ_CONV;
 
   val bir_var_EQ_thm = prove(``
@@ -379,16 +262,28 @@ in (* local *)
   ``,
     METIS_TAC [bir_envTheory.bir_var_t_11]
   );
+
+  val bir_immtype_EQ_CONV =
+    REWRITE_CONV [bir_immTheory.bir_immtype_t_distinct, GSYM bir_immTheory.bir_immtype_t_distinct];
+
+  val bir_type_EQ_LImm_thm = CONJUNCT1 bir_valuesTheory.bir_type_t_11;
+  val bir_type_EQ_LMem_thm = CONJUNCT2 bir_valuesTheory.bir_type_t_11;
+  val bir_type_EQ_CONV =
+    REWRITE_CONV [bir_valuesTheory.bir_type_t_distinct,  GSYM bir_valuesTheory.bir_type_t_distinct] THENC
+    (fn tm =>
+      (if identical T tm orelse identical F tm then ALL_CONV else
+       if (bir_valuesSyntax.is_BType_Imm o fst o dest_eq) tm then
+         REWR_CONV bir_type_EQ_LImm_thm THENC
+         bir_immtype_EQ_CONV
+       else
+         REWR_CONV bir_type_EQ_LMem_thm THENC
+         CONJL_CONV bir_immtype_EQ_CONV bir_immtype_EQ_CONV
+      ) tm);
   (* this seems to be well optimized now, maybe need to turn off caching if there are much more variables around so that the dictionary lookups are more expensive *)
   val bir_var_EQ_CONV =
     (REWR_CONV bir_var_EQ_thm) THENC
     (CONJL_CONV
-      (REWRITE_CONV [(*type*)
-        bir_valuesTheory.bir_type_t_distinct,
-        GSYM bir_valuesTheory.bir_type_t_distinct,
-        bir_valuesTheory.bir_type_t_11,
-        bir_immTheory.bir_immtype_t_distinct,
-        GSYM bir_immTheory.bir_immtype_t_distinct])
+      bir_type_EQ_CONV (*type*)
       bir_varname_EQ_CONV (*name*));
   val bir_var_EQ_CONV = aux_moveawayLib.wrap_cache_result_EQ_BEQ Term.compare bir_var_EQ_CONV;
   val bir_var_EQ_CONV = Profile.profile "auxset_bir_var_EQ_CONV" bir_var_EQ_CONV;

diff --git a/src/tools/symbexec/bir_vars_ofLib.sml b/src/tools/symbexec/bir_vars_ofLib.sml
@@ -8,6 +8,7 @@ open HolKernel Parse boolLib bossLib;
 open bir_typing_expTheory;
 open bir_typing_expSyntax;
 open birsSyntax;
+open birs_utilsLib;
 
 open HolBACoreSimps;
 
@@ -96,11 +97,11 @@ in (* local *)
     (*
     (* this implementation of birs_exps_of_senv_COMP_ONCE_CONV works fine, but not as speedy as the one below *)
     (fn x => REWRITE_CONV [Once birs_exps_of_senv_COMP_thm] x) THENC
-    (TRY_CONV (aux_setLib.ITE_CONV (pred_setLib.IN_CONV aux_setLib.bir_varname_EQ_CONV)))
+    (TRY_CONV (ITE_CONV (pred_setLib.IN_CONV aux_setLib.bir_varname_EQ_CONV)))
     *)
     IFC
       (REWR_CONV ((GEN_ALL o (fn x => List.nth(x,1)) o CONJUNCTS o SPEC_ALL) birs_exps_of_senv_COMP_thm))
-      (aux_setLib.ITE_CONV (pred_setLib.IN_CONV aux_setLib.bir_varname_EQ_CONV))
+      (ITE_CONV (pred_setLib.IN_CONV aux_setLib.bir_varname_EQ_CONV))
       (IFC
         (REWR_CONV ((GEN_ALL o (fn x => List.nth(x,0)) o CONJUNCTS o SPEC_ALL) birs_exps_of_senv_COMP_thm))
         (ALL_CONV)

diff --git a/src/tools/symbexec/birsSyntax.sml b/src/tools/symbexec/birsSyntax.sml
@@ -123,6 +123,8 @@ in
  val (birs_eval_label_exp_tm,  mk_birs_eval_label_exp, dest_birs_eval_label_exp, is_birs_eval_label_exp)  = syntax_fns3 "birs_eval_label_exp";
 
  val (birs_eval_exp_tm,  mk_birs_eval_exp, dest_birs_eval_exp, is_birs_eval_exp)  = syntax_fns2 "birs_eval_exp";
+ val (birs_eval_exp_subst_tm,  mk_birs_eval_exp_subst, dest_birs_eval_exp_subst, is_birs_eval_exp_subst)  = syntax_fns2 "birs_eval_exp_subst";
+ val (birs_eval_exp_subst_var_tm,  mk_birs_eval_exp_subst_var, dest_birs_eval_exp_subst_var, is_birs_eval_exp_subst_var)  = syntax_fns2 "birs_eval_exp_subst_var";
 
  val (birs_exec_stmt_jmp_tm,  mk_birs_exec_stmt_jmp, dest_birs_exec_stmt_jmp, is_birs_exec_stmt_jmp)  = syntax_fns3_set "birs_exec_stmt_jmp";
  val (birs_exec_stmt_tm,  mk_birs_exec_stmt, dest_birs_exec_stmt, is_birs_exec_stmt)  = syntax_fns3_set "birs_exec_stmt";

diff --git a/src/tools/symbexec/birs_execLib.sml b/src/tools/symbexec/birs_execLib.sml
@@ -108,9 +108,9 @@ in
         else
         NONE)
       birs_rulesTheory.assert_spec_thm
-      (aux_setLib.DISJR_CONV
-        (aux_setLib.NEG_CONV aux_setLib.bir_pc_EQ_CONV)
-        (aux_setLib.NEG_CONV aux_setLib.bir_status_EQ_CONV))
+      (DISJR_CONV
+        (NEG_CONV aux_setLib.bir_pc_EQ_CONV)
+        (NEG_CONV aux_setLib.bir_status_EQ_CONV))
       thm;
   val birs_rule_tryjustassert_fun = fn x => Profile.profile "birs_rule_tryjustassert_fun" (birs_rule_tryjustassert_fun x);
 
@@ -119,9 +119,9 @@ in
       "tryprune"
       NONE
       prune_thm
-      (aux_setLib.DISJL_CONV
-        (aux_setLib.NEG_CONV aux_setLib.bir_pc_EQ_CONV)
-        (aux_setLib.NEG_CONV aux_setLib.bir_status_EQ_CONV));
+      (DISJL_CONV
+        (NEG_CONV aux_setLib.bir_pc_EQ_CONV)
+        (NEG_CONV aux_setLib.bir_status_EQ_CONV));
   val birs_rule_tryprune_fun = fn x => Profile.profile "birs_rule_tryprune_fun" (birs_rule_tryprune_fun x);
 
   (* ============================================================================ *)