From 995e13fa90a75cb503de765a14913e58c708b157 Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Fri, 23 Aug 2024 20:21:41 +0200 Subject: [PATCH] Replace symbolic execution in tutorial --- examples/tutorial/8-symbexec/Holmakefile | 2 +- examples/tutorial/8-symbexec/Makefile | 2 +- examples/tutorial/8-symbexec/README.md | 3 +- examples/tutorial/8-symbexec/exec.sml | 85 ----- .../tutorial/8-symbexec/test-symbexec.sml | 132 +++++++ examples/tutorial/support2/Holmakefile | 13 - .../tutorial/support2/bir_symb2_envScript.sml | 73 ---- .../tutorial/support2/bir_symb2_execLib.sig | 21 - .../tutorial/support2/bir_symb2_execLib.sml | 276 -------------- .../support2/bir_symb2_execScript.sml | 360 ------------------ .../support2/bir_symb2_init_envLib.sig | 17 - .../support2/bir_symb2_init_envLib.sml | 129 ------- .../tutorial/support2/bir_symb2_masterLib.sml | 120 ------ 13 files changed, 136 insertions(+), 1097 deletions(-) delete mode 100644 examples/tutorial/8-symbexec/exec.sml create mode 100644 examples/tutorial/8-symbexec/test-symbexec.sml delete mode 100644 examples/tutorial/support2/Holmakefile delete mode 100644 examples/tutorial/support2/bir_symb2_envScript.sml delete mode 100644 examples/tutorial/support2/bir_symb2_execLib.sig delete mode 100644 examples/tutorial/support2/bir_symb2_execLib.sml delete mode 100644 examples/tutorial/support2/bir_symb2_execScript.sml delete mode 100644 examples/tutorial/support2/bir_symb2_init_envLib.sig delete mode 100644 examples/tutorial/support2/bir_symb2_init_envLib.sml delete mode 100644 examples/tutorial/support2/bir_symb2_masterLib.sml diff --git a/examples/tutorial/8-symbexec/Holmakefile b/examples/tutorial/8-symbexec/Holmakefile index 1fbb19712..aa451a20a 100644 --- a/examples/tutorial/8-symbexec/Holmakefile +++ b/examples/tutorial/8-symbexec/Holmakefile @@ -6,7 +6,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \ $(HOLDIR)/examples/l3-machine-code/riscv/model \ $(HOLDIR)/examples/l3-machine-code/riscv/step \ $(HOLBADIR)/src/shared \ - $(HOLBADIR)/examples/tutorial/support2 \ + $(HOLBADIR)/src/tools/symbexec \ $(HOLBADIR)/examples/tutorial/2-lift \ $(HOLBADIR)/src diff --git a/examples/tutorial/8-symbexec/Makefile b/examples/tutorial/8-symbexec/Makefile index 6f011cf28..1e2f81309 100644 --- a/examples/tutorial/8-symbexec/Makefile +++ b/examples/tutorial/8-symbexec/Makefile @@ -1,6 +1,6 @@ .DEFAULT_GOAL := all all: - make --directory=../../.. examples/tutorial/8-symbexec/exec.sml_run + make --directory=../../.. examples/tutorial/8-symbexec/test-symbexec.sml_run diff --git a/examples/tutorial/8-symbexec/README.md b/examples/tutorial/8-symbexec/README.md index 0cb82db1c..eafd8b748 100644 --- a/examples/tutorial/8-symbexec/README.md +++ b/examples/tutorial/8-symbexec/README.md @@ -2,8 +2,9 @@ ## Experiments -1. See structure of `exec.sml`. +1. See structure of `test-symbexec.sml`. 1. Run the script as it is. +1. The following points are outdated but one might want to revisit them later and showcase these points with the current proof-producing symbolic execution. 1. Change initial path condition, and observe: * the path conditions (see contradictions for infeasible paths), * number of resulting symbolic states (leafs in execution tree). diff --git a/examples/tutorial/8-symbexec/exec.sml b/examples/tutorial/8-symbexec/exec.sml deleted file mode 100644 index 34a805aba..000000000 --- a/examples/tutorial/8-symbexec/exec.sml +++ /dev/null @@ -1,85 +0,0 @@ - -(* ============================================================= *) -open HolKernel Parse; - -open examplesBinaryTheory; - -open bslSyntax; - -open bir_symb2_masterLib; - -val _ = Parse.current_backend := PPBackEnd.vt100_terminal; - -val _ = print "loading...\n"; - -val name = "add_reg"; -val prog = (snd o dest_eq o concl) bir_add_reg_prog_def; -(* ============================================================= *) - -(* define binary inputs *) -val get_x = bconst ``R0:word64``; -val get_sp = bconst ``SP_EL0:word64``; - -(* ============================================================= *) -(* ============================================================= *) - -(* predefined preconditions *) -val precond_0 = btrue; -val precond_1 = beq(bconst64 5, bconst64 7); -val precond_2 = beq(bconst64 5, bconst64 5); -val precond_3 = bslt(get_x, bconst64 2); -val precond_4 = bandl [precond_3, beq(get_sp,bconst64 0x80000000)]; -val precond_5 = bandl [bnot (bslt(get_x, bconst64 0)), precond_3, beq(get_sp,bconst64 0x80000000)]; -val precond_6 = bandl [beq(get_x, bconst64 0), beq(get_sp,bconst64 0x80000000)]; -val precond_7 = bandl [beq(get_x, bconst64 1), beq(get_sp,bconst64 0x80000000)]; - - -(* select precondition *) -val precond = precond_7; - -(* max birblock depth *) -val maxdepth_0 = 10; -val maxdepth_1 = 11; -val maxdepth_2 = 3; -val maxdepth_3 = ~1; -val maxdepth_10 = 11+8; -val maxdepth_11 = 11+9; -val maxdepth_12 = 11+9+2; -val maxdepth_13 = 11+9+3; -val maxdepth_14 = 11+9+3+1; -val maxdepth_15 = 11+3+1; -val maxdepth_16 = 11+3+1+88; - -val maxdepth = maxdepth_16; - - - - -(* ============================================================= *) -(* ============================================================= *) - -(* run the symbolic execution *) -val leafs = symb_exec2_process_to_leafs maxdepth precond prog; - - -(* ============================================================= *) - -(* check leafs *) -val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" -val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" -val _ = print ("number of leafs: " ^ (Int.toString (length leafs)) ^ "\n\n"); - - -(* ============================================================= *) - -(* compute concrete states from path conditions using SMT-solver *) -val wtms = List.map symb_exec2_get_predword leafs; -val states = List.map symb_exec2_get_init_vals wtms; - - -(* print states *) -val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" -val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" -val _ = PolyML.print_depth 10; -val _ = List.foldl (fn (st,_) => (PolyML.print st; print "\n")) () states; - diff --git a/examples/tutorial/8-symbexec/test-symbexec.sml b/examples/tutorial/8-symbexec/test-symbexec.sml new file mode 100644 index 000000000..67ff6ccf4 --- /dev/null +++ b/examples/tutorial/8-symbexec/test-symbexec.sml @@ -0,0 +1,132 @@ +open HolKernel Parse boolLib bossLib; + +open birs_auxLib; +open bir_symbLib; +open birsSyntax; +open bslSyntax; + +open bir_prog_add_regTheory; + +val _ = Parse.current_backend := PPBackEnd.vt100_terminal; + +val _ = print "loading...\n"; + +(* ----------------------------------------- *) +(* input selection *) +(* ----------------------------------------- *) +val progname = "add_reg"; +val prog_def = bir_add_reg_prog_def; +val lift_thm = bir_add_reg_arm8_lift_THM; + +(* define binary inputs *) +val get_x = bden (bvarimm64 "R0"); +val get_sp = bden (bvarimm64 "SP_EL0"); + +(* predefined preconditions *) +val precond_0 = btrue; +val precond_1 = beq(bconst64 5, bconst64 7); +val precond_2 = beq(bconst64 5, bconst64 5); +val precond_3 = bslt(get_x, bconst64 2); +val precond_4 = bandl [precond_3, beq(get_sp,bconst64 0x80000000)]; +val precond_5 = bandl [bnot (bslt(get_x, bconst64 0)), precond_3, beq(get_sp,bconst64 0x80000000)]; +val precond_6 = bandl [beq(get_x, bconst64 0), beq(get_sp,bconst64 0x80000000)]; +val precond_7 = bandl [beq(get_x, bconst64 1), beq(get_sp,bconst64 0x80000000)]; + +(* select precondition *) +val precond = precond_7; + + +(* endpoint *) +val endpoint_0 = ``0x3cw:word64``; (* before loop back *) +val endpoint_1 = ``0x4cw:word64``; (* after loop back, at the function return, practically an endless loop *) + +(* select endpoint *) +val endpoint = endpoint_0; + +(* ----------------------------------------- *) +(* Program variable definitions and theorems *) +(* ----------------------------------------- *) + +val bir_tutorial_prog_def = prog_def; +val _ = gen_prog_vars_birenvtyl_defthms progname bir_tutorial_prog_def; +val tutorial_birenvtyl_def = DB.fetch "scratch" (progname^"_birenvtyl_def");; + +(* --------------------------- *) +(* prepare program lookups *) +(* --------------------------- *) + +val bir_lift_thm = lift_thm; +val _ = birs_auxLib.prepare_program_lookups bir_lift_thm; + +(* ------------------ *) +(* Program boundaries *) +(* ------------------ *) + +val tutorial_init_addr_def = Define `tutorial_init_addr : word64 = 0x0w`; + +(* TODO: fix multiple endpoints here *) +val tutorial_end_addr_def = Define `tutorial_end_addr : word64 = ^endpoint`; + +(* -------------- *) +(* BSPEC contract *) +(* -------------- *) + +val bspec_tutorial_pre_def = Define `bspec_tutorial_pre : bir_exp_t = ^precond`; + +(* --------------------------- *) +(* Symbolic analysis execution *) +(* --------------------------- *) + +val (bsysprecond_thm, symb_analysis_thm) = + bir_symb_analysis_thm + bir_tutorial_prog_def + tutorial_init_addr_def [tutorial_end_addr_def] + bspec_tutorial_pre_def tutorial_birenvtyl_def; + + +(* ============================================================= *) + +(* the result of running the symbolic execution *) +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = print_thm symb_analysis_thm; + +(* ============================================================= *) + +(* check leafs *) +val (sys_i, L_s, Pi_f) = (symb_sound_struct_get_sysLPi_fun o concl) symb_analysis_thm; +val leafs = (pred_setSyntax.strip_set o snd o dest_comb) Pi_f; +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = print ("number of leafs: " ^ (Int.toString (length leafs)) ^ "\n\n"); + + +(* ============================================================= *) + +(* TODO: move this away from here *) +fun model_t2s model = + let + fun pair_t2s (name,tm) = (name, term_to_string tm); + in + List.map pair_t2s model + end; +fun get_init_vals wtm = + let + val model = ((Z3_SAT_modelLib.Z3_GET_SAT_MODEL wtm) + handle HOL_ERR e => []); + val model_w_strs = model_t2s model + in + model_w_strs + end; + +(* compute concrete states from path conditions using SMT-solver *) +val wtms = List.map (bir_exp_to_wordsLib.bir2bool o (fn (_,_,_,pcond_tm) => pcond_tm) o dest_birs_state) leafs; +val states = List.map get_init_vals wtms; + + +(* print states *) +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = print "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n" +val _ = PolyML.print_depth 10; +val _ = List.foldl (fn (st,_) => (PolyML.print st; print "\n")) () states; + diff --git a/examples/tutorial/support2/Holmakefile b/examples/tutorial/support2/Holmakefile deleted file mode 100644 index 46422939f..000000000 --- a/examples/tutorial/support2/Holmakefile +++ /dev/null @@ -1,13 +0,0 @@ -INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \ - $(HOLDIR)/examples/l3-machine-code/arm8/model \ - $(HOLDIR)/examples/l3-machine-code/arm8/step \ - $(HOLDIR)/examples/l3-machine-code/m0/model \ - $(HOLDIR)/examples/l3-machine-code/m0/step \ - $(HOLDIR)/examples/l3-machine-code/riscv/model \ - $(HOLDIR)/examples/l3-machine-code/riscv/step \ - $(HOLBADIR)/src/shared \ - $(HOLBADIR)/src/theory/bir \ - $(HOLBADIR)/src/theory/bir-support - -all: $(DEFAULT_TARGETS) -.PHONY: all diff --git a/examples/tutorial/support2/bir_symb2_envScript.sml b/examples/tutorial/support2/bir_symb2_envScript.sml deleted file mode 100644 index dabc033ea..000000000 --- a/examples/tutorial/support2/bir_symb2_envScript.sml +++ /dev/null @@ -1,73 +0,0 @@ -(* -app load ["HolKernel", "Parse", "boolLib", "bossLib", "finite_mapTheory"]; -app load ["bir_envTheory", "bir_valuesTheory"]; - *) - -open HolKernel Parse boolLib bossLib; -open finite_mapTheory; -open bir_expTheory; -open bir_envTheory; -open bir_valuesTheory; -open listTheory; - -(* --------------------------------------------------------------------- *) -(* Symbolic Environment: *) -(* Same as Concrete Environment, with initially all *) -(* variables / flags set to symbols *) -(* ----------------------------------------------------------------------*) - -val _ = new_theory "bir_symb2_env"; - -val _ = Datatype `bir_symb_var_environment_t = - BEnv (string |-> (bir_type_t # (bir_exp_t)))`; - - -(* -----------------------------------------------------*) -(* Symbolic environment maps Vars to expressions *) -(* ---------------------------------------------------- *) - - -val fmap_update_replace_def = Define ` - fmap_update_replace (map: 'a |-> 'b) (a, b) = - case (FLOOKUP map a) of - | NONE => FUPDATE map (a, b) - | SOME v => FUPDATE (map \\ a ) (a, b)`; - -val bir_symb_env_read_def = Define ` - (bir_symb_env_read v (BEnv env) = - case (FLOOKUP env (bir_var_name v)) of - | NONE => ARB (* this means we don't expect this case, - all variables of expressions should be in the environment *) - | SOME (ty, e) => e)`; - -val bir_symb_env_lookup_def = Define ` - (bir_symb_env_lookup name (BEnv env) = - FLOOKUP env name)`; - -val bir_symb_env_update_def = Define ` - bir_symb_env_update varname vo ty (BEnv env) = - BEnv (fmap_update_replace env (varname, (ty, vo)))`; - -val bir_symb_env_lookup_type_def = Define ` - bir_symb_env_lookup_type var (BEnv env) = - case (FLOOKUP env (bir_var_name var)) of - | NONE => NONE - | SOME (ty, e) => SOME ty`; - -val bir_symb_check_type_def = Define ` - bir_symb_check_type var env = - (bir_symb_env_lookup_type var env = SOME (bir_var_type var))`; - -val bir_symb_varname_is_bound_def = Define ` - bir_symb_varname_is_bound var_name (BEnv env) = - case (FLOOKUP env var_name) of - | NONE => F - | SOME (_) => T`; - -val bir_symb_env_write_def = Define ` - bir_symb_env_write v exp env = - if bir_symb_check_type v env then - SOME (bir_symb_env_update (bir_var_name v) exp (bir_var_type v) env) - else NONE`; - -val _ = export_theory (); diff --git a/examples/tutorial/support2/bir_symb2_execLib.sig b/examples/tutorial/support2/bir_symb2_execLib.sig deleted file mode 100644 index a06678b00..000000000 --- a/examples/tutorial/support2/bir_symb2_execLib.sig +++ /dev/null @@ -1,21 +0,0 @@ -signature bir_symb2_execLib = sig - - type 'a symb_tree_t; - - val symb_is_BST_Running : term -> bool - - val symb_is_BST_AssertionViolated : term -> bool - - (* maxdepth (-1 is unlimited), precond, program, pred decider *) - val symb_exec_program : int -> term -> term -> (term -> bool) -> term symb_tree_t - - val dest_bir_symb_obs : term -> term * term * term - val dest_bir_symb_state : term -> term * term * term * term * term - - val bir_exp_hvar_to_bvar : term -> term - - val symb_exec_leaflist : 'a symb_tree_t -> 'a list - - val bir_exp_rewrite : (term -> term) -> term -> term - -end diff --git a/examples/tutorial/support2/bir_symb2_execLib.sml b/examples/tutorial/support2/bir_symb2_execLib.sml deleted file mode 100644 index 86e48539c..000000000 --- a/examples/tutorial/support2/bir_symb2_execLib.sml +++ /dev/null @@ -1,276 +0,0 @@ -structure bir_symb2_execLib :> bir_symb2_execLib = -struct - -local -(* -app load ["bir_symb2_execTheory", "bir_symb2_envTheory", "bir_symb2_init_envLib"]; -*) - -open HolKernel -open pairLib -open bir_symb2_execTheory; -open bir_symb2_envTheory; -open bir_symb2_init_envLib; -open listSyntax bir_programSyntax; - -open bir_immSyntax; -open bir_expSyntax; -open bir_envSyntax; - -val debug_on = true; - -in - -(* In order to decide when we want to stop execution, we need - * to destruct the symbolic state - * Use method "is_BST_Running to decide wether we want to stop - *) - -(* -------------------- syntax functions ----------------------------- *) -(* val bir_symb_state_t_ty = mk_type ("bir_symb_state_t", []); *) -fun dest_bir_symb_state tm = - let - val (ty, l) = TypeBase.dest_record tm - val _ = if is_type ty andalso - (fst o dest_type) ty = "bir_symb_state_t" andalso - (length o snd o dest_type) ty = 1 - then () else fail() - val pc = Lib.assoc "bsst_pc" l - val env = Lib.assoc "bsst_environ" l - val pred = Lib.assoc "bsst_pred" l - val status = Lib.assoc "bsst_status" l - val obs = Lib.assoc "bsst_obs" l - in - (pc, env, pred, status, obs) - end handle HOL_ERR _ => raise ERR "dest_bir_symb_state" ("cannot destruct term \"" ^ (term_to_string tm) ^ "\""); - -(*val bir_symb_obs_t_ty = mk_type ("bir_symb_obs_t", []);*) -fun dest_bir_symb_obs tm = - let - val (ty, l) = TypeBase.dest_record tm - val _ = if is_type ty andalso - (fst o dest_type) ty = "bir_symb_obs_t" andalso - (length o snd o dest_type) ty = 1 - then () else fail() - val obs_cond = Lib.assoc "obs_cond" l - val obs = Lib.assoc "obs" l - val obs_fun = Lib.assoc "obs_fun" l - in - (obs_cond, obs, obs_fun) - end handle HOL_ERR _ => raise ERR "dest_bir_symb_obs" ("cannot destruct term \"" ^ (term_to_string tm) ^ "\""); -(* ------------------------------------------------------------------- *) - -(* Destruct symbolic state to decide wheter branch is still running *) -fun symb_is_BST_Running state = - let - val (pc, env, pres, status, obs) = dest_bir_symb_state state; - in - is_BST_Running status - end; - -fun symb_is_BST_AssertionViolated state = - let - val (pc, env, pres, status, obs) = dest_bir_symb_state state; - in - status = ``BST_AssertionViolated`` - end; - -(* We represent an Execution as a tree, where branches - * in the Tree represent the Branches in the CFG *) -datatype 'a symb_tree_t = Symb_Node of ('a * 'a symb_tree_t list); - -fun decide_pred pd s = - let - val (pc, env, pred, status, obs) = dest_bir_symb_state s; - in - pd pred - end; - - -(* The main function to execute a BIR Program: - * Builds an Execution Tree *) -(* - val bp = bir_program; - val st = state; - *) -fun symb_exec_run max bp pd st = - if (not (symb_is_BST_Running st)) orelse (max = 0) then - Symb_Node (st, []) - else - let - val max_new = if max < 0 then max else (max-1); - val (sts_running, sts_terminated) = - ((dest_pair o rhs o concl o EVAL) ``bir_symb_exec_label_block ^bp ^st``); - val sts_ter = (#1 (dest_list sts_terminated)); - val sts_run = (#1 (dest_list sts_running)); - val sts = (sts_ter @ sts_run); - val sts_filtered = List.filter (decide_pred pd) sts; - val _ = if not debug_on then () else - let - val _ = print "=========================================\n"; - val _ = print (Int.toString max); - val _ = print "\n=========================================\n"; - in () end; - val sts_rec = List.map (symb_exec_run max_new bp pd) sts_filtered; - in - Symb_Node (st, sts_rec) -(* - Symb_Node (st, (List.map (fn st' => Symb_Node (st', [])) (sts_ter @ sts_run))) -*) - end; - -(* Given a Program, exec until every branch halts *) -(* -val bir_program = ``BirProgram [] : 'observation_type bir_program_t``; - -val bir_program = ``BirProgram - [<|bb_label := BL_Address_HC (Imm64 0w) "F9400023 (ldr x3, [x1])"; - bb_statements := - [BStmt_Assert - (BExp_Const (Imm1 abc)); - BStmt_Assert - (BExp_Aligned Bit64 3 (BExp_Den (BVar "R1" (BType_Imm Bit64)))); - BStmt_Assign (BVar "R3" (BType_Imm Bit64)) - (BExp_Load (BExp_Den (BVar "MEM" (BType_Mem Bit64 Bit8))) - (BExp_Den (BVar "R1" (BType_Imm Bit64))) BEnd_LittleEndian - Bit64); - BStmt_Observe (BExp_Const (Imm1 1w)) - ([BExp_BinExp BIExp_And - (BExp_Const (Imm64 0x1FC0w)) - (BExp_Den (BVar "R1" (BType_Imm Bit64)))]) - (\x. x)]; - bb_last_statement := BStmt_Halt (BExp_Const (Imm64 4w))|>]``; -*) -fun symb_exec_program depth precond bir_program pd = - let - val env = init_env (); - val state = (rhs o concl o EVAL) - ``bir_symb_state_init ^bir_program ^env ^precond``; - val tree = symb_exec_run depth bir_program pd state; - val _ = print ("Execution: Done!\n"); - in - tree - end; - - -fun symb_exec_leaflist (Symb_Node (s, [])) = [s] - | symb_exec_leaflist (Symb_Node (_, l )) = List.concat (List.map symb_exec_leaflist l) -(* | symb_exec_leaflist _ = raise ERR "symb_exec_leaflist" "this should not happen"*) - ; - -(* TODO: move this to lib and possibly merge to bir_expLib *) - fun bir_exp_rewrite rwf exp = - if is_BExp_Const exp then - rwf exp - - else if is_BExp_Den exp then - rwf exp - - else if is_BExp_Cast exp then - let - val (castt, exp, sz) = (dest_BExp_Cast) exp; - val exp_rw = bir_exp_rewrite rwf exp; - in - rwf (mk_BExp_Cast (castt, exp_rw, sz)) - end - - else if is_BExp_UnaryExp exp then - let - val (uop, exp) = (dest_BExp_UnaryExp) exp; - val exp_rw = bir_exp_rewrite rwf exp; - in - rwf (mk_BExp_UnaryExp (uop, exp_rw)) - end - - else if is_BExp_BinExp exp then - let - val (bop, exp1, exp2) = (dest_BExp_BinExp) exp; - val exp1_rw = bir_exp_rewrite rwf exp1; - val exp2_rw = bir_exp_rewrite rwf exp2; - in - rwf (mk_BExp_BinExp (bop, exp1_rw, exp2_rw)) - end - - else if is_BExp_BinPred exp then - let - val (bpredop, exp1, exp2) = (dest_BExp_BinPred) exp; - val exp1_rw = bir_exp_rewrite rwf exp1; - val exp2_rw = bir_exp_rewrite rwf exp2; - in - rwf (mk_BExp_BinPred (bpredop, exp1_rw, exp2_rw)) - end - - else if is_BExp_IfThenElse exp then - let - val (expc, expt, expf) = (dest_BExp_IfThenElse) exp; - val expc_rw = bir_exp_rewrite rwf expc; - val expt_rw = bir_exp_rewrite rwf expt; - val expf_rw = bir_exp_rewrite rwf expf; - in - rwf (mk_BExp_IfThenElse (expc_rw, expt_rw, expf_rw)) - end - - else if is_BExp_Load exp then - let - val (expm, expad, endi, sz) = (dest_BExp_Load) exp; - val expm_rw = bir_exp_rewrite rwf expm; - val expad_rw = bir_exp_rewrite rwf expad; - in - rwf (mk_BExp_Load (expm_rw, expad_rw, endi, sz)) - end - - else if is_BExp_Store exp then - let - val (expm, expad, endi, expv) = (dest_BExp_Store) exp; - val expm_rw = bir_exp_rewrite rwf expm; - val expad_rw = bir_exp_rewrite rwf expad; - val expv_rw = bir_exp_rewrite rwf expv; - in - rwf (mk_BExp_Store (expm_rw, expad_rw, endi, expv_rw)) - end - - else - raise (ERR "bir_exp_rewrite" ("don't know BIR expression: \"" ^ (term_to_string exp) ^ "\"")) - ; - -local - open bir_valuesSyntax; -in -(* -val exp = ``BExp_Const (Imm32 r1)``; -*) - val bir_exp_hvar_to_bvar_bexp = bir_exp_rewrite (fn exp => if not (is_BExp_Const exp) then exp else - let val (imm_t_i, w) = (gen_dest_Imm o dest_BExp_Const) exp in - if not (is_var w) then exp else - let val (v_n, v_t) = dest_var w in - (mk_BExp_Den o mk_BVar_string) (v_n, mk_BType_Imm(bir_immtype_t_of_word_ty v_t)) - end - end); - -(* - this function tolerates lists and maps bir_exp_hvar_to_bvar_bexp - to the list elements, or applies it directly - *) - fun bir_exp_hvar_to_bvar t = - if is_list t then - let - val (t_l, t_t) = dest_list t; - in - mk_list (List.map bir_exp_hvar_to_bvar_bexp t_l, t_t) - end - else - bir_exp_hvar_to_bvar_bexp t; - -end - - -(* -In order to Execute a Program: - -val prog = (snd o dest_comb o concl) toy_arm8_THM; <-- replace program -val (tree, st_assert_lst) = symb_exec_program prog_w_obs; -val sts = symb_exec_leaflist_complete tree st_assert_lst; - *) -end (* local *) - -end (* struct *) diff --git a/examples/tutorial/support2/bir_symb2_execScript.sml b/examples/tutorial/support2/bir_symb2_execScript.sml deleted file mode 100644 index c638baab0..000000000 --- a/examples/tutorial/support2/bir_symb2_execScript.sml +++ /dev/null @@ -1,360 +0,0 @@ -(* Vim users execute the following loads *) -(* -app load ["HolKernel", "Parse", "boolLib" ,"bossLib"]; -app load ["wordsTheory", "bitstringTheory"]; -app load ["holba_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"]; -app load ["bir_symb2_envTheory"]; -app load ["bir_programTheory", "bir_expTheory", "bir_envTheory"]; -app load ["llistTheory", "wordsLib"]; -*) - -open HolKernel Parse boolLib bossLib; -open wordsTheory bitstringTheory; -open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; -open bir_envTheory; -open bir_expTheory; -open bir_programTheory; -open llistTheory wordsLib; - -open bir_envTheory bir_symb2_envTheory; - -val _ = new_theory "bir_symb2_exec"; - - -(* ------------------------------------------------------------------------- *) -(* Datatypes *) -(* ------------------------------------------------------------------------- *) - -(** Observations - * obs_cond : Observation Condition - * obs: Observation - **) -val _ = Datatype `bir_symb_obs_t = <| - obs_cond : bir_exp_t; - obs : bir_exp_t list; - obs_fun : bir_val_t list -> 'a; - |>`; - -(* * - * Symbolic State contains of: - * PC: current program counter - * environment: Mapping vars to expressions - * memory: Mapping memory addresses to expressions - * pred: expression representing the path condition - * bsst_status : a status bit (mainly used for errors) - * obs: list of conditional observations - * *) - -val _ = Datatype `bir_symb_state_t = <| - bsst_pc : bir_programcounter_t; - bsst_environ : bir_symb_var_environment_t; (* Mapping Vars to Exps *) - bsst_pred : bir_exp_t; (* Path predicate *) - bsst_status : bir_status_t; (* State *) - bsst_obs : 'a bir_symb_obs_t list; (* Observations *) - |>`; - -(* Expression that always evaluates to True *) -val TRUE_EXP_def = Define ` - TRUE_EXP = BExp_Const (Imm1 1w)`; - -(* ------------------------------------------------------------------------- *) -(* Symbolic State *) -(* ------------------------------------------------------------------------- *) - -(* Initially, Environment is empty and predicate set to True *) -val bir_symb_state_init_def = Define `bir_symb_state_init (p : 'a bir_program_t) env pred = <| - bsst_pc := bir_pc_first p; - bsst_environ := env; - bsst_pred := pred; - bsst_status := BST_Running; - bsst_obs := ([] : 'a bir_symb_obs_t list) |>`; - -val bir_symb_state_set_failed_def = Define ` - bir_symb_state_set_failed st = - st with bsst_status := BST_Failed`; - -val bir_symb_state_is_terminated_def = Define ` - bir_symb_state_is_terminated st = - if st.bsst_status = BST_Running then F else T`; - -(* ------------------------------------------------------------------------- *) -(* Eval certain expressions *) -(* Different from concrete Execution, this returns a BIR Expression *) -(* ------------------------------------------------------------------------- *) - -val bir_symb_eval_cast_def = Define ` - bir_symb_eval_cast ct e ty = BExp_Cast ct e ty`; - -val bir_symb_eval_unary_def = Define ` - bir_symb_eval_unary et e = BExp_UnaryExp et e`; - -val bir_symb_eval_binary_def = Define ` - bir_symb_eval_binary et e1 e2 = BExp_BinExp et e1 e2`; - -val bir_symb_eval_bin_pred_def = Define ` - bir_symb_eval_bin_pred pt e1 e2 = BExp_BinPred pt e1 e2`; - -val bir_symb_eval_memeq_def = Define ` - bir_symb_eval_memeq e1 e2 = BExp_MemEq e1 e2`; - -val bir_symb_eval_ite_def = Define ` - bir_symb_eval_ite c et ef = BExp_IfThenElse c et ef`; - -val bir_symb_eval_store_def = Define ` - bir_symb_eval_store mem_e a_e v_e = BExp_Store mem_e a_e v_e`; - -val bir_symb_eval_load_def = Define ` - bir_symb_eval_load mem_e a_e en ty = BExp_Load mem_e a_e en ty`; - - -val bir_symb_eval_exp_def = Define ` - (bir_symb_eval_exp (BExp_Const n) env = BExp_Const n) /\ - - (bir_symb_eval_exp (BExp_Den v) env = bir_symb_env_read v env) /\ - - (bir_symb_eval_exp (BExp_Cast ct e ty) env = - bir_symb_eval_cast ct (bir_symb_eval_exp e env) ty) /\ - - (bir_symb_eval_exp (BExp_UnaryExp et e) env = - bir_symb_eval_unary et (bir_symb_eval_exp e env)) /\ - - (bir_symb_eval_exp (BExp_BinExp et e1 e2) env = - bir_symb_eval_binary et - (bir_symb_eval_exp e1 env) (bir_symb_eval_exp e2 env)) /\ - - (bir_symb_eval_exp (BExp_BinPred pt e1 e2) env = - bir_symb_eval_bin_pred pt ( - bir_symb_eval_exp e1 env) (bir_symb_eval_exp e2 env)) /\ - - (bir_symb_eval_exp (BExp_MemEq e1 e2) env = - bir_symb_eval_memeq - (bir_symb_eval_exp e1 env) (bir_symb_eval_exp e2 env)) /\ - - (bir_symb_eval_exp (BExp_IfThenElse c et ef) env = - bir_symb_eval_ite - (bir_symb_eval_exp c env) - (bir_symb_eval_exp et env) (bir_symb_eval_exp ef env)) /\ - - (bir_symb_eval_exp (BExp_Load mem_e a_e en ty) env = - bir_symb_eval_load - (bir_symb_eval_exp mem_e env) - (bir_symb_eval_exp a_e env) en ty) /\ - - (bir_symb_eval_exp (BExp_Store mem_e a_e en v_e) env = - bir_symb_eval_store (bir_symb_eval_exp mem_e env) - (bir_symb_eval_exp a_e env) en (bir_symb_eval_exp v_e env))`; - -val bir_symb_eval_exp_empty_def = Define ` - bir_symb_eval_exp_empty e = bir_eval_exp e (BEnv FEMPTY) - `; - - -(* ------------------------------------------------------------------------- *) -(* Symbolic Execution Semantics *) -(* ------------------------------------------------------------------------- *) - -(* We can have symbolic label expressions, these are to be - * "solved" with SAT solver and every possible solution to be considered *) -val bir_symb_eval_label_exp_def = Define ` - (bir_symb_eval_label_exp (BLE_Label l) env = SOME l) ∧ - (bir_symb_eval_label_exp (BLE_Exp e) env = NONE)`; - -(********************) -(* Jumps/Halt *) -(********************) - -(* direct jump *) -val bir_symb_exec_stmt_jmp_to_label_def = Define` - bir_symb_exec_stmt_jmp_to_label p (l: bir_label_t) (st: 'a bir_symb_state_t) = - if (MEM l (bir_labels_of_program p)) then - st with bsst_pc := bir_block_pc l - else (st with bsst_status := (BST_JumpOutside l))`; - - -(* We ignore symbolic/indirect jump targets currently! *) -val bir_symb_exec_stmt_jmp_def = Define ` - bir_symb_exec_stmt_jmp - (p: 'a bir_program_t) (le: bir_label_exp_t) (st: 'a bir_symb_state_t) = - case bir_symb_eval_label_exp le st.bsst_environ of - | NONE => bir_symb_state_set_failed st - | SOME l => bir_symb_exec_stmt_jmp_to_label p l st`; - -(* End of execution *) -val bir_symb_exec_stmt_halt_def = Define ` - bir_symb_exec_stmt_halt ex (st: 'a bir_symb_state_t) = - (st with bsst_status := BST_Halted (bir_symb_eval_exp_empty (bir_symb_eval_exp ex st.bsst_environ)))`; - -(* Conditional jump: - * Return a list with two states where - * path predicate is updated accordingly *) -val bir_symb_stmt_cjmp_def = Define ` - bir_symb_exec_stmt_cjmp p ex l1 l2 st = - let - st_true = bir_symb_exec_stmt_jmp p l1 st; - st_false = bir_symb_exec_stmt_jmp p l2 st; - ex_subst = (bir_symb_eval_exp ex st.bsst_environ); - in - [ - st_true with bsst_pred := - (BExp_BinExp BIExp_And ex_subst st.bsst_pred) - ; - st_false with bsst_pred := - (BExp_BinExp BIExp_And (BExp_UnaryExp BIExp_Not ex_subst) st.bsst_pred) - ]`; - -(* Execute "End" (Jump/Halt) Statement *) -val bir_symb_exec_stmtE_def = Define ` - (bir_symb_exec_stmtE p (BStmt_Jmp l) st = [bir_symb_exec_stmt_jmp p l st]) /\ - (bir_symb_exec_stmtE p (BStmt_CJmp ex l1 l2 ) st = bir_symb_exec_stmt_cjmp p ex l1 l2 st ) /\ - (bir_symb_exec_stmtE p (BStmt_Halt ex) st = [bir_symb_exec_stmt_halt ex st])`; - - -(********************) -(* Declare / Assign *) -(********************) - - -(* We declare all variables before execution, so raise error if this occurs *) -val bir_symb_exec_stmt_declare_def = Define ` - bir_symb_exec_stmt_declare var_name var_type st = - [bir_symb_state_set_failed st] `; - -(* same behavior for assume *) -val bir_symb_exec_stmt_assume_def = Define ` - bir_symb_exec_stmt_assume ex st = - [bir_symb_state_set_failed st] `; - -(* assign... *) -val bir_symb_exec_stmt_assign_def = Define ` - bir_symb_exec_stmt_assign v ex (st: 'a bir_symb_state_t) = - case (bir_symb_env_write v (bir_symb_eval_exp ex st.bsst_environ) st.bsst_environ) of - | SOME env => [st with bsst_environ := env] - | NONE => [bir_symb_state_set_failed st]`; - -(* Assertions create two follow up states: - * One in which the assertion holds and One in which the Assertion is violated *) -val bir_symb_exec_stmt_assert_def = Define ` - bir_symb_exec_stmt_assert ex st = - let - ex_subst = (bir_symb_eval_exp ex st.bsst_environ); - ex_subst_not = BExp_UnaryExp BIExp_Not ex_subst; - st_true = - st with bsst_pred := BExp_BinExp BIExp_And ex_subst st.bsst_pred; - st_false = - st with - <| bsst_status := BST_AssertionViolated; - bsst_pred := BExp_BinExp BIExp_And ex_subst_not st.bsst_pred |>; - in - [st_true; st_false] - `; - - -(* add observations as symbolic stubstitutions *) -val bir_symb_exec_stmt_observe_def = Define ` - bir_symb_exec_stmt_observe c_ex obs_lst f st = -(* - if f <> (\x. x) then - [bir_symb_state_set_failed st] - else -*) - let - obs_cond_ex = bir_symb_eval_exp c_ex st.bsst_environ; - obs_lst_e = MAP (\o_ex. bir_symb_eval_exp o_ex st.bsst_environ) obs_lst; - obs = <| obs_cond := obs_cond_ex; obs := obs_lst_e; obs_fun := f |>; - in - [st with bsst_obs := (obs :: st.bsst_obs)] - `; - -(* Basic Statement execution *) -val bir_symb_exec_stmtB_def = Define ` - (bir_symb_exec_stmtB (BStmt_Declare v) st - = bir_symb_exec_stmt_declare (bir_var_name v) (bir_var_type v) st) ∧ - (bir_symb_exec_stmtB (BStmt_Assign v ex) st - = bir_symb_exec_stmt_assign v ex st) /\ - (bir_symb_exec_stmtB (BStmt_Assert ex) st - = bir_symb_exec_stmt_assert ex st) /\ - (bir_symb_exec_stmtB (BStmt_Assume ex) st - = bir_symb_exec_stmt_assume ex st) /\ - (bir_symb_exec_stmtB (BStmt_Observe ex ex_lst f) st - = bir_symb_exec_stmt_observe ex ex_lst f st) - `; - -(* Execute one statement *) -val bir_symb_exec_stmt_def = Define` - (bir_symb_exec_stmt (p: 'a bir_program_t) - (BStmtB (bst: 'a bir_stmt_basic_t)) - (st: 'a bir_symb_state_t) - = (bir_symb_exec_stmtB bst st)) /\ - - (bir_symb_exec_stmt p (BStmtE (bst: bir_stmt_end_t)) st - = (bir_symb_exec_stmtE p bst st)) - `; - -(* ---------------------------------------------------- *) -(* Execute a program *) -(* -----------------------------------------------------*) - -(* helper definition to partition a list of states - into running and terminated ones *) -val bir_symb_exec_partition_running_def = Define ` - (bir_symb_exec_partition_running [] (sr, sh) = (REVERSE sr, REVERSE sh)) /\ - (bir_symb_exec_partition_running (st::sts) (sr, sh) = - bir_symb_exec_partition_running (sts) (if bir_symb_state_is_terminated st then (sr, st::sh) else (st::sr, sh))) - `; - -(* Execute the non-ending statements of a BB. - * generalized: produces list of running states and a list of terminated states *) -val bir_symb_exec_stmtB_list_rec_def = Define ` - - (bir_symb_exec_stmtB_list_rec - (p: 'a bir_program_t) - (sts_running: 'a bir_symb_state_t list) - [] - sts_halted - = (sts_running, sts_halted) - ) /\ - - (bir_symb_exec_stmtB_list_rec p sts_running (stmt :: stmt_lst) sts_halted - = - let - st_lst = FLAT (MAP (bir_symb_exec_stmtB stmt) sts_running); - (sts_running', sts_halted') = bir_symb_exec_partition_running st_lst ([],[]); - in - bir_symb_exec_stmtB_list_rec p sts_running' stmt_lst (APPEND sts_halted' sts_halted) - ) - - `; - -(* helper function for the recursive function above ... *) -val bir_symb_exec_bb_statements = Define ` - bir_symb_exec_bb_statements p sts stmt_lst = - bir_symb_exec_stmtB_list_rec p sts stmt_lst [] - `; - -(* Execute the End Statemens of a BB - * same output as above *) -val bir_symb_exec_bb_last_statement = Define ` - bir_symb_exec_bb_last_statement p sts_running stmt = - bir_symb_exec_partition_running (FLAT (MAP (bir_symb_exec_stmtE p stmt) sts_running)) ([],[]) - `; - -(* Execute a single basic block. - * same output as above *) -val bir_symb_exec_blk_def = Define ` - bir_symb_exec_blk (p: 'a bir_program_t) (blk: 'a bir_block_t) sts_running = - let - (sts_running', sts_halted') = bir_symb_exec_bb_statements p sts_running blk.bb_statements; - (sts_running'', sts_halted'') = bir_symb_exec_bb_last_statement p sts_running' blk.bb_last_statement; - in - (sts_running'', APPEND sts_halted' sts_halted'')`; - -(* Given a Program and a State, find the respective block and execute it *) -val bir_symb_exec_label_block_def = Define ` - (bir_symb_exec_label_block (p: 'a bir_program_t) (st: 'a bir_symb_state_t)) - = - case (bir_get_program_block_info_by_label p st.bsst_pc.bpc_label) of - | NONE => ([], [bir_symb_state_set_failed st]) - | SOME (_, blk) => if bir_symb_state_is_terminated st - then ([], [st]) else (bir_symb_exec_blk p blk [st])`; - -val _ = export_theory(); diff --git a/examples/tutorial/support2/bir_symb2_init_envLib.sig b/examples/tutorial/support2/bir_symb2_init_envLib.sig deleted file mode 100644 index 87e8c3261..000000000 --- a/examples/tutorial/support2/bir_symb2_init_envLib.sig +++ /dev/null @@ -1,17 +0,0 @@ -signature bir_symb2_init_envLib = sig - -(* - val add_memory_to_env : term -> term - val add_registers_to_env_1 : string list -> term -> term - val add_registers_to_env_64 : string list -> term -> term - val add_registers_to_env_8 : string list -> term -> term - val add_symbolic_register_to_env_1 : string -> term -> term - val add_symbolic_register_to_env_64 : string -> term -> term - val add_symbolic_register_to_env_8 : string -> term -> term - val generate_symbolic_register_1 : string -> term - val generate_symbolic_register_64 : string -> term - val generate_symbolic_register_8 : string -> term -*) - val init_env : unit -> term - -end diff --git a/examples/tutorial/support2/bir_symb2_init_envLib.sml b/examples/tutorial/support2/bir_symb2_init_envLib.sml deleted file mode 100644 index 5e80077be..000000000 --- a/examples/tutorial/support2/bir_symb2_init_envLib.sml +++ /dev/null @@ -1,129 +0,0 @@ -(********************************************************) -(* Functions definied within this file are use to *) -(* initialize the environment / memory *) -(* This is mostly SML -- not HOL definitions! *) -(********************************************************) - -(* -app load ["bir_symb2_envTheory", "bir_symb2_execTheory", "stringLib"] -*) - -structure bir_symb2_init_envLib :> bir_symb2_init_envLib = -struct - -local - -open HolKernel; -open bir_expTheory; -open bir_symb2_execTheory -open bir_symb2_envTheory; -open bir_valuesTheory; -open bir_immTheory; -open finite_mapTheory; -open bitstringTheory; -open stringLib; -open bir_exp_memTheory; - -in - -(* Initialize all the Registers / Variables we have *) - -(* Functions to generate symolbic registers of _64 _8 and _1 bits *) -fun generate_symbolic_register_64 (name: string) = - mk_var(name, Type `:word64`); - -fun generate_symbolic_register_1 (name : string) = - mk_var(name, Type `:word1`); - -fun generate_symbolic_register_8 (name : string) = - mk_var(name, Type `:word8`); - - -(* Add symbolic registers byte-wise in environment *) -fun add_symbolic_register_to_env_64 name env = - let - val r = - generate_symbolic_register_64 name - val name_hol = fromMLstring name - in - (rhs o concl o EVAL) - `` bir_symb_env_update - ^name_hol (BExp_Const (Imm64 ^r)) (BType_Imm Bit64) ^env - `` - end; - -fun add_symbolic_register_to_env_8 name env = - let - val r = generate_symbolic_register_8 name - val name_hol = fromMLstring name - in - (rhs o concl o EVAL) - `` bir_symb_env_update - ^name_hol (BExp_Const (Imm8 ^r)) (BType_Imm Bit8) ^env - `` - end; - -fun add_symbolic_register_to_env_1 name env = - let - val r = generate_symbolic_register_1 name - val name_hol = fromMLstring name - in - (rhs o concl o EVAL) - `` - bir_symb_env_update - ^name_hol (BExp_Const (Imm1 ^r)) (BType_Imm Bit1) ^env - `` - end; - -fun add_memory_to_env env = - let val mem = fromMLstring "MEM" - in - (rhs o concl o EVAL) - `` - bir_symb_env_update - ^mem (BExp_MemConst Bit64 Bit8 memory) (BType_Mem Bit64 Bit8) ^env - `` - end; - - -fun add_registers_to_env_64 [] env = env - | add_registers_to_env_64 (reg :: regs) env = - add_registers_to_env_64 regs (add_symbolic_register_to_env_64 reg env) - -fun add_registers_to_env_8 [] env = env - | add_registers_to_env_8 (reg :: regs) env = - add_registers_to_env_8 regs (add_symbolic_register_to_env_8 reg env) - -fun add_registers_to_env_1 [] env = env - | add_registers_to_env_1 (reg :: regs) env = - add_registers_to_env_1 regs (add_symbolic_register_to_env_1 reg env) - -fun init_env () = - let - (* 64 Bit Registers *) - val reg_list_64 = [ - "R0", "R1", "R2", "R3", "R4", - "R5", "R6", "R7", "R8", "R9", - "R10","R11","R12", "SP_EL0", - "SP_process", "ADDR"] - (* 1 Byte registers *) - val reg_list_8 = [ "VAL" ] - (* 1 Bit flags *) - val reg_list_1 = [ - "ProcState_N", "ProcState_Z", - "ProcState_C", "ProcState_V" ] - in - let - val e = add_registers_to_env_64 reg_list_64 ``BEnv FEMPTY`` - in - let - val ee = add_registers_to_env_8 reg_list_8 e - in add_memory_to_env ( - add_registers_to_env_1 reg_list_1 ee) - end - end - end; - -end (* local *) - -end (* struct *) diff --git a/examples/tutorial/support2/bir_symb2_masterLib.sml b/examples/tutorial/support2/bir_symb2_masterLib.sml deleted file mode 100644 index f22d520bd..000000000 --- a/examples/tutorial/support2/bir_symb2_masterLib.sml +++ /dev/null @@ -1,120 +0,0 @@ -structure bir_symb2_masterLib = -struct - -local - -open HolKernel Parse; - -open bir_symb2_init_envLib; -open bir_symb2_execLib; - -open bir_exp_to_wordsLib; - -val pdecide_on = true; -val debug_on = false; - - -in - -(* SMT helper *) -(* -val btm = precond; -*) -fun pdecide btm = - if not pdecide_on then true else - let - val _ = if debug_on then print_term btm else (); - val _ = if debug_on then print "\n" else (); - - val wtm = bir2bool btm; - val _ = if debug_on then print_term wtm else (); - val _ = if debug_on then print "\n" else (); - - val taut = ((HolBA_HolSmtLib.Z3_ORACLE_PROVE wtm; true) - handle HOL_ERR e => false); - - val model = ((Z3_SAT_modelLib.Z3_GET_SAT_MODEL wtm; true) - handle HOL_ERR e => false); - - val _ = if debug_on then print ("taut: " ^ (if taut then "true\n" else "false\n")) else (); - val _ = if debug_on then print ("model: " ^ (if model then "true\n" else "false\n")) else (); - in - taut orelse model - end; - - -fun symb_exec2_process_to_leafs maxdepth precond prog = - symb_exec_leaflist (symb_exec_program maxdepth precond prog pdecide); - -(* -val st = hd leafs; -*) -fun symb_exec2_get_predword st = - let - val (pc, env, pred, status, obs) = dest_bir_symb_state st; - val btm = pred; - - val _ = if debug_on then print_term btm else (); - val _ = if debug_on then print "\n" else (); - - val wtm = bir2bool btm; - val _ = if debug_on then print_term wtm else (); - val _ = if debug_on then print "\n" else (); - in - wtm - end; - - -fun symb_exec2_model_t2s model = - let - fun pair_t2s (name,tm) = (name, term_to_string tm); - in - List.map pair_t2s model - end; - - -(* -val wtm = -EVAL (subst [``R0:word64`` |-> ``1w:word64``, ``SP_EL0:word64`` |-> ``0x80000000w:word64``] wtm) - -val get_x = bconst ``R0:word64``; -val get_sp = bconst ``SP_EL0:word64``; -*) -fun symb_exec2_get_init_vals wtm = - let - val model = ((Z3_SAT_modelLib.Z3_GET_SAT_MODEL wtm) - handle HOL_ERR e => []); - val model_w_strs = symb_exec2_model_t2s model - in - model_w_strs - end; - -(* -(* -val subs = [``R0:word64`` |-> ``1w:word64``, ``SP_EL0:word64`` |-> ``0x80000000w:word64``]; -val st = (hd leafs); -*) -fun symb_exec2_concr_state subs st = - let - val (pc, env, pred, status, obs) = dest_bir_symb_state st; - - val pred_subs = subst subs pred; - - val pred_eval_tm = ``bir_eval_exp ^(pred_subs) (BEnv FEMPTY)``; - val pred_val = (snd o dest_eq o concl o EVAL) pred_eval_tm; - in -``<| - bsst_pc := ^pc; - bsst_environ := FEMPTY; - bsst_pred := ^(bconst ); - bsst_status := ^status; - bsst_obs := ^obs; - |>`` - end; -*) - -end - - - -end