Various small optimizations and output improvements

src/tools/symbexec/aux_moveawayLib.sml

@@ -86,6 +86,69 @@ in (* local *)
       f_wrapped
     end;
 
+fun measure_fun s f v =
+  let
+    val timer = holba_miscLib.timer_start 0;
+    val res = f v;
+    val _ = holba_miscLib.timer_stop (fn delta_s => print (s ^ delta_s ^ "\n")) timer;
+  in
+    res
+  end;
+
+local
+  open bir_programSyntax;
+  open bir_program_labelsSyntax;
+  open bir_immSyntax;
+  open numSyntax;
+  open stringSyntax;
+in
+  fun imm_to_hexstring immv =
+    let
+      val (bw, v) = gen_dest_Imm immv;
+    in
+      "imm(" ^
+      Int.toString bw ^
+      "; 0x" ^
+      (Arbnum.toHexString o wordsSyntax.dest_word_literal) v ^
+      ")"
+    end;
+
+  fun label_to_string label =
+    if is_BL_Label label then
+      "label(" ^
+      ((fromHOLstring o dest_BL_Label) label) ^
+      ")"
+    else if is_BL_Address label then
+      "address(" ^
+      imm_to_hexstring (dest_BL_Address label) ^
+      ")"
+    else if is_BL_Address_HC label then
+      let
+        val (immv, comment) = dest_BL_Address_HC label;
+      in
+        "address(" ^
+        imm_to_hexstring immv ^
+        "; " ^
+        fromHOLstring comment ^
+        ")"
+      end
+    else
+      raise ERR "label_to_string" "unexpected";
+
+  fun pc_to_string pc =
+    let
+      val (label,index) = dest_bir_programcounter pc;
+      val label_str = label_to_string label;
+      val index_str = Arbnum.toString (dest_numeral index);
+    in
+      "pc(" ^
+      label_str ^
+      "; " ^
+      index_str ^
+      ")"
+    end;
+end
+
 end (* local *)
 
 end (* struct *)

src/tools/symbexec/aux_setLib.sml

@@ -172,10 +172,15 @@ in (* local *)
       ((REWR_CONV ((GEN_ALL o (fn x => List.nth(x,1)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES)) THENC
       bir_label_EQ_CONV);
   (*val bir_pc_EQ_CONV = aux_moveawayLib.wrap_cache_result_EQ_BEQ Term.compare bir_pc_EQ_CONV;*)
+  val bir_pc_EQ_CONV = Profile.profile "bir_pc_EQ_CONV" bir_pc_EQ_CONV;
 
 (* ---------------------------------------------------------------------------------- *)
 (*  bir var set equality checker                                                      *)
 (* ---------------------------------------------------------------------------------- *)
+  val bir_varname_EQ_CONV =
+    stringLib.string_EQ_CONV;
+  val bir_varname_EQ_CONV = Profile.profile "bir_varname_EQ_CONV" bir_varname_EQ_CONV;
+
   val bir_var_EQ_thm = prove(``
     !a0 a1 a0' a1'.
       BVar a0 a1 = BVar a0' a1' <=>
@@ -197,9 +202,10 @@ in (* local *)
     IFC
       ((REWR_CONV ((GEN_ALL o (fn x => List.nth(x,0)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES)))
       ((*name*)
-       stringLib.string_EQ_CONV)
+       bir_varname_EQ_CONV)
       ((REWR_CONV ((GEN_ALL o (fn x => List.nth(x,2)) o CONJUNCTS o SPEC_ALL) boolTheory.AND_CLAUSES)));
   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 "bir_var_EQ_CONV" bir_var_EQ_CONV;
 
 (* ---------------------------------------------------------------------------------- *)
 (*  birs state equality checker                                                       *)
@@ -210,7 +216,13 @@ in (* local *)
 
   (* could speed this up, maybe take inspiration from string or word EQ_CONV functions *)
   val bir_exp_EQ_CONV =
-    EVAL (*SIMP_CONV (std_ss++holBACore_ss++birs_state_ss) [] THENC EVAL*);
+    let
+      val rewrite_thms = (((List.concat o List.map (fn t => [t,GSYM t]) o CONJUNCTS) bir_expTheory.bir_exp_t_distinct)@(CONJUNCTS bir_expTheory.bir_exp_t_11))@[birs_auxTheory.BExp_IntervalPred_def];
+    in
+      REWRITE_CONV rewrite_thms THENC
+      EVAL (*SIMP_CONV (std_ss++holBACore_ss++birs_state_ss) [] THENC EVAL*)
+    end;
+  val bir_exp_EQ_CONV = aux_moveawayLib.wrap_cache_result_EQ_BEQ Term.compare bir_exp_EQ_CONV;
 
   fun birs_gen_env_check_eq env1 env2 =
     let
@@ -272,6 +284,7 @@ in (* local *)
          )
        );
   val birs_state_EQ_CONV = aux_moveawayLib.wrap_cache_result_EQ_BEQ Term.compare birs_state_EQ_CONV;
+  val birs_state_EQ_CONV = Profile.profile "birs_state_EQ_CONV" birs_state_EQ_CONV;
 
 (* ---------------------------------------------------------------------------------- *)
 (*  programcounter operations                                                    *)

src/tools/symbexec/bir_vars_ofLib.sml

@@ -35,8 +35,7 @@ in (* local *)
         val t2 = CONV_RULE (RAND_CONV (
         birs_auxLib.GEN_match_conv is_bir_vars_of_exp (f_rec))) t1;
         val union_conv =
-          (aux_setLib.varset_UNION_CONV)
-          (*pred_setLib.UNION_CONV NO_CONV*);
+          (aux_setLib.varset_UNION_CONV);
         val t2_rhs = (rhs o concl) t2;
         val t3 =
           if is_union (t2_rhs) then
@@ -97,11 +96,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.resolve_ite_CONV (pred_setLib.IN_CONV stringLib.string_EQ_CONV)))
+    (TRY_CONV (aux_setLib.resolve_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.resolve_ite_CONV (pred_setLib.IN_CONV stringLib.string_EQ_CONV))
+      (aux_setLib.resolve_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))
         (REFL)
@@ -141,11 +140,9 @@ in (* local *)
           (pred_setLib.IMAGE_CONV
             bir_vars_of_exp_DIRECT_CONV
             NO_CONV)) THENC
-        (*aux_setLib.varset_BIGUNION_CONV*)
-        (aux_setLib.BIGUNION_CONV NO_CONV)
+        (aux_setLib.varset_BIGUNION_CONV)
       )) THENC
-      (*aux_setLib.varset_UNION_CONV*)
-      (pred_setLib.UNION_CONV NO_CONV)
+      (aux_setLib.varset_UNION_CONV)
       (*
       (* basic solution for flattening the set and avoid comparisons *)
       RATOR_CONV (RAND_CONV (REWRITE_CONV [pred_setTheory.BIGUNION_INSERT, pred_setTheory.BIGUNION_EMPTY])) THENC

src/tools/symbexec/birs_composeLib.sml

@@ -66,18 +66,16 @@ in
         (HO_MATCH_MP (HO_MATCH_MP birs_rule_SEQ_thm step_A_thm)) step_B_thm;
 
       val freesymbols_tm = (fst o dest_imp o concl) prep_thm;
-      val freesymbols_thm = birs_rule_SEQ_INTER_freesymbs_fun freesymbols_tm;
-      val _ = print "finished to proof free symbols altogether\n";
+      val freesymbols_thm = Profile.profile "birs_rule_SEQ_fun_p2" birs_rule_SEQ_INTER_freesymbs_fun freesymbols_tm;
 
       val bprog_composed_thm =
             (MP prep_thm freesymbols_thm);
-      val _ = print "composed\n";
 
       (* tidy up set operations to not accumulate (in both, post state set and label set) *)
       val bprog_fixed_thm =
         (CONV_RULE
-         (birs_Pi_CONV birs_state_DIFF_UNION_CONV THENC
-          birs_L_CONV programcounter_UNION_CONV))
+         (Profile.profile "birs_rule_SEQ_fun_p3" (birs_Pi_CONV birs_state_DIFF_UNION_CONV) THENC
+          Profile.profile "birs_rule_SEQ_fun_p4" (birs_L_CONV programcounter_UNION_CONV)))
          bprog_composed_thm
         handle e => (print "\n\n"; print_thm bprog_composed_thm; print "tidy up Pi and programcounter sets failed\n"; raise e);
 
@@ -91,6 +89,7 @@ in
       bprog_fixed_thm
     end;
   val birs_rule_SEQ_fun = fn x => fn y => Profile.profile "birs_rule_SEQ_fun" (birs_rule_SEQ_fun x y);
+  val birs_rule_SEQ_fun = fn x => fn y => aux_moveawayLib.measure_fun ">>>>>>>>>> birs_rule_SEQ_fun in " (birs_rule_SEQ_fun x y);
 
 
 end (* local *)

src/tools/symbexec/birs_driveLib.sml

@@ -108,6 +108,15 @@ in (* local *)
   fun build_tree exec_funs st =
     (birs_check_state_norm ("build_tree", "") st;
      build_tree_rec exec_funs (take_step exec_funs st));
+  (*
+  val build_tree = fn (fetch, step_SING, step, is_continue) =>
+    build_tree
+      (Profile.profile "build_tree_fetch" fetch,
+       Profile.profile "build_tree_step_SING" step_SING,
+       Profile.profile "build_tree_step" step,
+       is_continue);
+  *)
+
 
   fun exec_until (exec_funs, comp_fun) =
     (Profile.profile "reduce_tree" (reduce_tree comp_fun)) o
@@ -119,12 +128,14 @@ in (* local *)
     let
       open birs_execLib;
 
+      (* TODO: make this an input to avoid recomputation *)
+      val has_no_halt_thm =
+        Profile.profile "bir_prog_has_no_halt_fun" bir_prog_has_no_halt_fun bprog_tm;
+
       val birs_rule_STEP_thm =
-        birs_rule_STEP_prog_fun
-          (Profile.profile "bir_prog_has_no_halt_fun" bir_prog_has_no_halt_fun bprog_tm);
+        birs_rule_STEP_prog_fun has_no_halt_thm;
       val birs_rule_STEP_SEQ_thm = MATCH_MP
-        birs_rulesTheory.birs_rule_STEP_SEQ_gen_thm
-        (bir_prog_has_no_halt_fun bprog_tm);
+        birs_rulesTheory.birs_rule_STEP_SEQ_gen_thm has_no_halt_thm;
       val birs_rule_SEQ_thm = birs_rule_SEQ_prog_fun bprog_tm;
       val birs_rule_SUBST_thm = birs_rule_SUBST_prog_fun bprog_tm;
 

src/tools/symbexec/birs_stepLib.sml

@@ -555,15 +555,6 @@ fun get_birs_state_size t =
     n_pcond + n_env
   end;
 
-fun measure_fun s f v =
-  let
-    val timer = holba_miscLib.timer_start 0;
-    val res = f v;
-    val _ = holba_miscLib.timer_stop (fn delta_s => print (s ^ delta_s ^ "\n")) timer;
-  in
-    res
-  end;
-
 
 val birs_state_ss = rewrites (type_rws ``:birs_state_t``);
 
@@ -721,16 +712,18 @@ val birs_eval_label_exp_CONV = (
 
 fun birs_exec_step_CONV_pre t =
 let
- val bprog_tm = (snd o dest_comb o fst o dest_comb) t;
- val _ = print_term bprog_tm;
- val _ = if is_const bprog_tm then () else
-         raise ERR "birs_exec_step_CONV" "program term is not a constant";
+  val bprog_tm = (snd o dest_comb o fst o dest_comb) t;
+  (*val _ = print_term bprog_tm;*)
+  val pc = (dest_birs_state_pc o snd o dest_comb) t;
+  val pc_string = aux_moveawayLib.pc_to_string pc;
+  val state_size = (get_birs_state_size o snd o dest_comb) t;
+  val _ = print ("symb state exp sizes = " ^ (Int.toString state_size) ^ "\n");
+  (*val _ = print ("symb state term size = " ^ ((Int.toString o term_size) t) ^ "\n");*)
+  val _ = print ("pc = " ^ pc_string ^ "\n");
+  val _ = if is_const bprog_tm then () else
+          raise ERR "birs_exec_step_CONV" "program term is not a constant";
 in
- t |>
- (fn t => ((print_term o (fn (x,_,_,_) => x) o dest_birs_state o snd o dest_comb) t; t)) |>
- (fn t => (print ("symb state term size = " ^ ((Int.toString o term_size) t) ^ "\n"); t)) |>
- (fn t => (print ("symb state bir expression sizes = " ^ ((Int.toString o get_birs_state_size o snd o dest_comb) t) ^ "\n"); t)) |>
- (fn t => (bprog_tm)) 
+  bprog_tm
 end;
 val birs_exec_step_CONV_pre = Profile.profile "exec_step_CONV_pre" birs_exec_step_CONV_pre;
 
@@ -773,35 +766,32 @@ fun pc_lookup_fun (bprog_tm, pc_tm) =
   end;
 
 fun birs_exec_step_CONV_p1 (bprog_tm, t) = (* get the statement *)
- ((fn t =>
-   let
-     val st_tm = (snd o dest_comb) t;
-     val (pc_tm,env_tm,_,pcond_tm) = (dest_birs_state) st_tm;
-     val pc_lookup_thm = pc_lookup_fun (bprog_tm, pc_tm);
-     (*val _ = print_thm pc_lookup_thm;*)
-
-     val (abbr_thm, eq_thms) = abbr_app (t, env_tm, pcond_tm);
-
-     val rhs_tm = (snd o dest_eq o concl) abbr_thm;
-     val res = (
-             REWRITE_CONV [birs_exec_step_def, bir_symbTheory.birs_state_t_accfupds, combinTheory.K_THM, pc_lookup_thm]
-       THENC RESTR_EVAL_CONV ([bprog_tm, birs_exec_stmt_tm])
-       ) rhs_tm;
-     val res = TRANS abbr_thm res;
-
-(*
-val res = abbr_rev (res, env_tm, pcond_tm);
-*)
-(*
-     val _ = print_thm abbr_thm;
-     val _ = print_thm res;
-     val _ = raise ERR "" "";
-*)
-   in
-     (res, env_tm, pcond_tm, eq_thms)
-   end
-  )
- ) t;
+  let
+    val st_tm = (snd o dest_comb) t;
+    val (pc_tm,env_tm,_,pcond_tm) = (dest_birs_state) st_tm;
+    val pc_lookup_thm = pc_lookup_fun (bprog_tm, pc_tm);
+    (*val _ = print_thm pc_lookup_thm;*)
+
+    val (abbr_thm, eq_thms) = abbr_app (t, env_tm, pcond_tm);
+
+    val rhs_tm = (snd o dest_eq o concl) abbr_thm;
+    val res = (
+            REWRITE_CONV [birs_exec_step_def, bir_symbTheory.birs_state_t_accfupds, combinTheory.K_THM, pc_lookup_thm]
+      THENC RESTR_EVAL_CONV ([bprog_tm, birs_exec_stmt_tm])
+      ) rhs_tm;
+    val res = TRANS abbr_thm res;
+    (*
+    val res = abbr_rev (res, env_tm, pcond_tm);
+    *)
+    (*
+    val _ = print_thm abbr_thm;
+    val _ = print_thm res;
+    val _ = raise ERR "" "";
+    *)
+  in
+    (res, env_tm, pcond_tm, eq_thms)
+  end;
+val birs_exec_step_CONV_p1 = Profile.profile "exec_step_CONV_p1" birs_exec_step_CONV_p1;
 
 (*
 val birs_exec_step_CONV_p2 =
@@ -964,13 +954,10 @@ end;
 
 val birs_exec_step_CONV_E = Profile.profile "exec_step_CONV_E" birs_exec_step_CONV_E;
 
-val birs_exec_step_CONV =
-  measure_fun "\n>>>>>>>> step_CONV in " (fn t =>
+fun birs_exec_step_CONV t =
   let
-    val bprog_tm =
-      (measure_fun "\n>>>>>>>>>> step_CONV_pre in " birs_exec_step_CONV_pre t);
-    val (res_p1, env_tm, pcond_tm, eq_thms) =
-      (measure_fun "\n>>>>>>>>>> step_CONV_p1 in " birs_exec_step_CONV_p1 (bprog_tm, t));
+    val bprog_tm = birs_exec_step_CONV_pre t;
+    val (res_p1, env_tm, pcond_tm, eq_thms) = birs_exec_step_CONV_p1 (bprog_tm, t);
   (*val _ = (print "P1: GET STATEMENT\n"; print_thm res_p1);*)
     val stmt_tm = (snd o dest_comb o fst o dest_comb o snd o dest_eq o concl) res_p1;
   (*val _ = print_term stmt_tm;
@@ -985,8 +972,7 @@ val birs_exec_step_CONV =
        else
          raise ERR "birs_exec_step_CONV" "something is wrong, should be BStmtB or BStmtE here"
   )
-  end
- );
+  end;
 val birs_exec_step_CONV = Profile.profile "exec_step_CONV" birs_exec_step_CONV;