From 0c52978dd8a87043d9a6beadaadaed9c49c946bd Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Thu, 21 Aug 2014 14:13:46 +1000 Subject: [PATCH 1/2] More asmrefine work, global swapping ready. --- proof/asmrefine/SEL4GraphRefine.thy | 43 +- tools/asmrefine/GraphRefine.thy | 247 ++++++++++- tools/asmrefine/SimplExport.thy | 651 +++++++++++++++++----------- 3 files changed, 659 insertions(+), 282 deletions(-) diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index 9474260fa..c1664c3a3 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -19,8 +19,10 @@ begin ML {* Toplevel.debug := true *} +thm take_heap_list_min + ML {* -val funs = ParseGraph.funs @{theory} "../../spec/cspec/CFunDump.txt" +val funs = ParseGraph.funs @{theory} "CFunDump.txt" *} ML {* @@ -34,13 +36,18 @@ consts encode_machine_state :: "machine_state \ unit \ nat" definition - simpl_invariant :: "globals myvars set" + at_addr :: "'a \ bool" where - "simpl_invariant = UNIV" + "at_addr addr = True" + +lemma eq_impl_at_addrI: + "\ \sst gst. at_addr addr \ sst \ S \ eqs gst sst \ eqs2 gst sst \ + \ eq_impl addr eqs eqs2 S" + by (simp add: eq_impl_def at_addr_def) local_setup {* add_field_h_val_rewrites #> add_field_to_bytes_rewrites *} -ML {* val nm = "Kernel_C.lookupSlotForCNodeOp" *} +ML {* val nm = "Kernel_C.getSyscallArg" *} locale graph_refine = kernel_all_substitute + assumes globals_list_distinct: @@ -49,6 +56,13 @@ locale graph_refine = kernel_all_substitute = (xs = Fault ft))" begin +definition + simpl_invariant :: "globals myvars set" +where + "simpl_invariant = {s. const_globals_in_memory symbol_table globals_list + (hrs_mem (t_hrs_' (globals s))) + \ htd_safe domain (hrs_htd (t_hrs_' (globals s)))}" + local_setup {* define_graph_fun_short funs nm *} ML {* UseHints.globals_swap @@ -80,9 +94,21 @@ val globals_swap_rewrites2 *} +ML {* +mk_graph_refines_proof funs [] hints globals_swap_rewrites2 nm + (@{context} addsimps @{thms simpl_invariant_def}) +*} + +lemma store_word32s_equality_refl: + "store_word32s_equality addr xs xs hp hp" + by (simp add: store_word32s_equality_def) + schematic_lemma "PROP ?P" apply (tactic {* rtac it 1 *}) apply (tactic {* full_simpl_to_graph_tac funs [] hints nm @{context} *}) + apply (tactic {* ALLGOALS (TRY o rtac @{thm eq_impl_at_addrI}) *}) + apply (tactic {* ALLGOALS (simp_tac ((put_simpset HOL_basic_ss @{context}) + addsimps @{thms mex_def meq_def simpl_invariant_def})) *}) apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 0) *}) @@ -99,16 +125,21 @@ schematic_lemma "PROP ?P" apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 5) *}) apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 6) *}) + apply (simp_all add: field_h_val_rewrites field_to_bytes_rewrites heap_update_def to_bytes_array upt_rec take_heap_list_min drop_heap_list_general heap_update_list_append heap_list_update_ptr heap_list_update_word32 store_store_word32_commute_offset field_simps heap_access_Array_element h_val_word32 h_val_ptr - field_lvalue_offset_eq) + field_lvalue_offset_eq ucast_eq_0s) + apply (tactic {* simp_tac (@{context} addsimps @{thms store_word32s_equality_fold store_word32s_equality_final add_commute} + ) |>ALLGOALS *}) + apply (tactic {* simp_tac (@{context} addsimprocs [store_word32s_equality_simproc] + addsimps @{thms store_word32s_equality_final add_commute} + ) |>ALLGOALS *}) - apply (auto simp: mex_def meq_def) done diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index 4598ea6dc..58851dd50 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -11,6 +11,7 @@ theory GraphRefine imports TailrecPre GraphLangLemmas "../../lib/LemmaBucket_C" + FieldAccessors begin @@ -1287,6 +1288,14 @@ lemma is_aligned_intvl_disjoint: apply (simp add: field_simps del: Int_atLeastAtMost) done +lemma is_aligned_intvl_disjoint_offset: + "\ p \ p'; is_aligned (p - p') n \ + \ {p ..+ 2 ^ n} \ {p' ..+ 2 ^ n} = {}" + apply (rule intvl_disj_offset[where x="- p'", THEN iffD1]) + apply (rule is_aligned_intvl_disjoint) + apply (simp_all del: word_neq_0_conv add: field_simps) + done + lemma store_store_word32_commute: "\ p \ p'; is_aligned p 2; is_aligned p' 2 \ \ store_word32 p w (store_word32 p' w' hp) @@ -1305,13 +1314,10 @@ lemma store_store_word32_commute_offset: using prems apply (clarsimp simp: store_word32_def) apply (rule heap_list_update_commute) - apply (rule intvl_disj_offset[where x="- p'", THEN iffD1]) - apply (simp add: length_word_rsplit_even_size[OF refl] word_size - del: Int_atLeastAtMost) - apply (rule is_aligned_intvl_disjoint[where n=2, simplified]) - apply (simp add: field_simps word_neq_0_conv[symmetric] del: word_neq_0_conv) - apply (simp add: field_simps is_aligned_mask mask_def) - apply simp + apply (simp add: length_word_rsplit_even_size[OF refl] word_size) + apply (rule is_aligned_intvl_disjoint_offset[where n=2, simplified]) + apply (simp add: field_simps word_neq_0_conv[symmetric] del: word_neq_0_conv) + apply (simp add: field_simps is_aligned_mask mask_def) done lemma c_guard_to_word_ineq: @@ -1364,6 +1370,13 @@ lemma store_load_word32: apply (simp add: word_rsplit_rcat_size word_size) done +lemma load_store_word32: + "load_word32 p (store_word32 p v m) = v" + using heap_list_update[where p=p and h=m and v="rev (word_rsplit v)"] + by (simp add: store_word32_def load_word32_def + length_word_rsplit_exp_size' word_size addr_card + word_rcat_rsplit) + lemma word32_lt_bounds_reduce: "\ n \ 0; (i \ (n - 1)) \ \ (i < (n :: word32)) = (i < (n - 1))" apply (rule sym, rule trans, rule less_le) @@ -1374,6 +1387,181 @@ lemma word32_lt_bounds_reduce: lemma length_Cons: "length (x # xs) = Suc (length xs)" by simp +lemma ucast_eq_0: + "(ucast (x :: ('a :: len) word) = (0 :: ('b :: len) word)) + = (if len_of TYPE('a) <= len_of TYPE('b) + then x = 0 else (x && mask (len_of TYPE('b)) = 0))" + by (simp, fastforce intro!: word_eqI dest: word_eqD simp: nth_ucast word_size)+ + +lemmas ucast_eq_0s = ucast_eq_0 ucast_eq_0[THEN arg_cong[where f=Not], simplified] + +text {* Proof process for store_word32 equalities. *} + +lemma load_store_word32_offset: + "(p - p') AND 3 = 0 + \ load_word32 p (store_word32 p' v hp) + = (if p = p' then v else load_word32 p hp)" + using is_aligned_intvl_disjoint_offset[where p=p and p'=p' and n=2] + apply (clarsimp simp: load_store_word32) + apply (simp add: load_word32_def store_word32_def) + apply (subst heap_list_update_disjoint_same, simp_all) + apply (simp add: length_word_rsplit_exp_size' word_size + is_aligned_mask mask_def Int_commute) + done + +lemma load_word32_offset_represents: + assumes eq: "\x. x AND 3 = 0 \ load_word32 (p + x) hp = load_word32 (p + x) hp'" + shows "hp = hp'" +proof (rule ext) + fix x + let ?p = "p + ((x - p) AND ~~ 3)" + have X: "\hp v. store_word32 ?p v hp x = rev (word_rsplit v) ! unat ((x - p) AND 3)" + apply (simp add: store_word32_def + mask_out_sub_mask[where n=2 and 'a=32, unfolded mask_def, simplified]) + apply (subst heap_update_mem_same_point, simp_all add: field_simps + length_word_rsplit_exp_size' word_size addr_card) + apply (simp add: intvl_def) + apply (rule_tac x="unat ((x - p) && 3)" in exI) + apply (simp add: algebra_simps unat_mask_2_less_4[unfolded mask_def, simplified]) + done + have "hp x = (store_word32 ?p (load_word32 ?p hp) hp) x" + by (simp add: store_load_word32) + also have "\ = (store_word32 ?p (load_word32 ?p hp') hp') x" + by (simp only: X, simp add: eq word_bw_assocs) + also have "\ = hp' x" + by (simp add: store_load_word32) + finally show "hp x = hp' x" . +qed + +definition + "apply_store_word32 p = (\(offs, w) hp. if offs AND 3 = 0 + then store_word32 (p + offs) w hp else hp)" + +definition + store_word32s_equality :: "word32 \ (word32 \ word32) list + \ (word32 \ word32) list \ (word32 \ word8) \ (word32 \ word8) \ bool" +where + "store_word32s_equality p xs ys hp hp' \ + fold (apply_store_word32 p) xs hp = fold (apply_store_word32 p) ys hp'" + +lemma store_word32s_equality_fold: + "p' - p AND 3 = 0 \ + (store_word32 p w hp = store_word32 p' w' hp') + = store_word32s_equality p [(0, w)] [(p' - p, w')] hp hp'" + "p' - p AND 3 = 0 \ + store_word32s_equality p xs ys (store_word32 p' w' hp) hp' + = store_word32s_equality p ((p' - p, w') # xs) ys hp hp'" + "p' - p AND 3 = 0 \ + store_word32s_equality p xs ys hp (store_word32 p' w' hp') + = store_word32s_equality p xs ((p' - p, w') # ys) hp hp'" + by (simp_all add: store_word32s_equality_def apply_store_word32_def + split_def) + +lemma and_3_eq_0_subtract: + "x AND 3 = 0 \ (y :: ('a :: len) word) AND 3 = 0 \ (x - y) AND 3 = 0" + apply (rule trans, rule mask_eqs[symmetric, where n=2, unfolded mask_def, simplified]) + apply simp + apply (simp add: mask_eqs[symmetric, where n=2, unfolded mask_def, simplified]) + done + +lemma load_apply_store_word32: + "x AND 3 = 0 \ load_word32 (p + x) (apply_store_word32 p y hp) + = (if x = fst y then snd y else load_word32 (p + x) hp)" + apply (simp add: apply_store_word32_def split_def + load_store_word32_offset) + apply (simp add: load_store_word32_offset field_simps and_3_eq_0_subtract) + apply auto + done + +lemma load_fold_filter_apply_store_word32: + "x AND 3 = 0 + \ load_word32 (p + x) (fold (apply_store_word32 p) (filter (P \ fst) ys) hp) + = load_word32 (p + x) (if P x then fold (apply_store_word32 p) ys hp else hp)" + apply (induct ys rule: rev_induct) + apply simp + apply (auto simp add: load_apply_store_word32) + done + +lemma store_word32s_equality_split: + "store_word32s_equality p xs ys hp hp + = (store_word32s_equality p (filter (P o fst) xs) (filter (P o fst) ys) hp hp + \ store_word32s_equality p (filter (Not o P o fst) xs) (filter (Not o P o fst) ys) hp hp)" + apply (simp add: store_word32s_equality_def) + apply (safe intro!: load_word32_offset_represents[where p=p]) + apply (simp_all add: load_fold_filter_apply_store_word32) + apply (drule_tac f="load_word32 (p + x)" in arg_cong)+ + apply (simp add: load_fold_filter_apply_store_word32 split: split_if_asm) + done + +lemma apply_store_word32_over_store: + "apply_store_word32 p (x, v') (apply_store_word32 p (x, v) hp) + = apply_store_word32 p (x, v') hp" + by (clarsimp simp: load_apply_store_word32 + intro!: load_word32_offset_represents[where p=p]) + +lemma apply_store_load_word32: + "apply_store_word32 p (x, load_word32 (p + x) hp) hp = hp" + by (clarsimp simp: load_apply_store_word32 + intro!: load_word32_offset_represents[where p=p]) + +lemma store_word32s_equality_final: + "store_word32s_equality p ((x, v) # (x, v') # xs) ys hp hp' + = store_word32s_equality p ((x, v') # xs) ys hp hp'" + "store_word32s_equality p xs ((y, v) # (y, v') # ys) hp hp' + = store_word32s_equality p xs ((y, v') # ys) hp hp'" + "store_word32s_equality p [(x, v)] [(x, v')] hp hp + = (x AND 3 = 0 \ v = v')" + "store_word32s_equality p [(x, v)] [] hp hp + = (x AND 3 = 0 \ v = load_word32 (p + x) hp)" + "store_word32s_equality p [] [(x, v')] hp hp + = (x AND 3 = 0 \ v' = load_word32 (p + x) hp)" + apply (auto simp add: store_word32s_equality_def + apply_store_word32_over_store + load_apply_store_word32 + apply_store_load_word32 + dest: arg_cong[where f="load_word32 (p + x)"] + split: split_if_asm simp del: word_neq_0_conv) + apply (simp_all add: apply_store_word32_def del: word_neq_0_conv) + done + +ML {* + +val dest_word = HOLogic.dest_number + #> snd #> (fn x => x mod 4294967296) + +val trace_store_word32s = ref false + +fun store_word32_trace s v = if ! trace_store_word32s + then (tracing ("store_word32s: " ^ s); v) else v + +val store_word32s_equality_simproc = Simplifier.simproc_global_i + @{theory} "store_word32s_equality_simproc" + [@{term "store_word32s_equality p xs ys hp hp"}] + (fn ctxt => fn tm => case tm of (Const (@{const_name store_word32s_equality}, _) + $ _ $ xs $ ys $ hp $ hp') => (let + val _ = (hp aconv hp') orelse raise TERM ("foo", []) + val xs = HOLogic.dest_list xs + |> map (HOLogic.dest_prod #> fst #> dest_word) + val ys = HOLogic.dest_list ys + |> map (HOLogic.dest_prod #> fst #> dest_word) + val zs = sort int_ord (xs @ ys) + val _ = (not (null zs) andalso hd zs < List.last zs) + orelse raise TERM ("foo", []) + val pivot = nth zs (length zs div 2) + val pred = (if pivot = List.last zs + then @{term "op = :: word32 \ _"} + else @{term "op \ :: word32 \ _"}) + $ HOLogic.mk_number @{typ word32} pivot + in store_word32_trace "success" (SOME (cterm_instantiate + [(@{cpat "?P :: word32 \ bool"}, + cterm_of (Proof_Context.theory_of ctxt) pred)] + @{thm store_word32s_equality_split} + |> mk_meta_eq)) + end handle TERM _ => store_word32_trace "failed" NONE) + | _ => store_word32_trace "mismatch" NONE) + +*} + ML {* structure UseHints = struct @@ -1435,8 +1623,9 @@ fun mk_simpl_acc ctxt sT nm = let | mk_sst_acc "PMS" = do_pms_encode (pms $ globals_sst) | mk_sst_acc nm = if String.isPrefix "rv#space#" nm then mk_sst_acc (unprefix "rv#space#" nm) - else if String.isSuffix "_'" nm - then Syntax.read_term ctxt (nm ^ " :: globals myvars => _") $ sst + else if String.isSuffix "#v" nm + then Syntax.read_term ctxt + (suffix "_'" (unsuffix "#v" nm) ^ " :: globals myvars => _") $ sst else let val (head, tail) = Library.space_explode "." nm |> Library.split_last |> apfst (Library.space_implode ".") @@ -1540,7 +1729,7 @@ fun mk_graph_refines (funs : ParseGraph.funs) ctxt s = let (Long_Name.base_name s ^ "_'proc") val gamma = Syntax.read_term ctxt "\" val invs = Syntax.read_term ctxt "simpl_invariant" - val _ = case invs of Const _ => () + val _ = case head_of invs of Const _ => () | _ => raise TERM ("mk_graph_refines: requires simpl_invariant constant", []) val sT = fastype_of gamma |> gammaT_to_stateT val (xs, ys, _) = Symtab.lookup funs s |> the @@ -1791,6 +1980,7 @@ fun get_var_deps nodes ep outputs = let val node = Inttab.lookup nodes point |> the val conts = map dest_next_node (get_conts node) val (lvs, rvs) = get_lvals_rvals node + |> pairself (Ord_List.make string_ord) val cont_vars = maps (Inttab.lookup_list tab) conts |> Ord_List.make string_ord val vars = Ord_List.merge string_ord (rvs, @@ -1889,7 +2079,7 @@ fun full_simpl_to_graph_tac funs noreturns hints nm ctxt = fun safe_goal_tac ctxt = REPEAT_ALL_NEW (DETERM o CHANGED o safe_steps_tac ctxt) -fun graph_refine_proof_tacs ctxt = [ +fun graph_refine_proof_tacs globals_swap_rewrites2 ctxt = [ asm_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps @{thms signed_arith_ineq_checks_to_eq_word32 signed_arith_eq_checks_to_ord @@ -1899,11 +2089,8 @@ fun graph_refine_proof_tacs ctxt = [ var_htd_def var_acc_var_upd pvalid_def var_ms_def init_vars_def return_vars_def upd_vars_def save_vals_def - mem_upd_def mem_acc_def hrs_mem_update}), -(* simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps @{thms forall_swap_madness}), *) -(* simp_tac (ctxt addsimps @{thms - globals_update_globals_swap_twice globals_swap_twice - hrs_htd_globals_swap mex_def meq_def}), *) + mem_upd_def mem_acc_def hrs_mem_update + mex_def meq_def}), TRY o safe_goal_tac ctxt, asm_full_simp_tac (ctxt addsimps @{thms (* h_t_valid_disjoint_globals_swap @@ -1919,8 +2106,8 @@ fun graph_refine_proof_tacs ctxt = [ *) unat_less_helper word32_lt_bounds_reduce palign_valid_def pweak_valid_def} - (* addsimps globals_swap_rewrites2 - addsimps const_global_simps + addsimps globals_swap_rewrites2 + (* addsimps const_global_simps addsimps pglobal_valids *) ), (* TRY o REPEAT_ALL_NEW (etac @{thm const_globals_in_memory_heap_update_subset[rotated]} @@ -1952,20 +2139,34 @@ fun graph_refine_proof_tacs ctxt = [ addsimps (enum_simps ctxt) addsimprocs [Word_Bitwise_Tac.expand_upt_simproc] delsimps @{thms ptr_val_inj}), - asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps @{thms word_neq_0_conv[symmetric]}), - asm_full_simp_tac (ctxt addsimps @{thms + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps @{thms word_neq_0_conv[symmetric]}), + asm_full_simp_tac (ctxt addsimps @{thms typ_uinfo_t_def c_guard_to_word_ineq bvshl_def bvlshr_def bvashr_def bv_clz_def scast_def mask_def word_sle_def[THEN iffD2] word_sless_alt[THEN iffD2] store_load_word32 - }) + }), + asm_full_simp_tac (ctxt addsimps @{thms + to_bytes_array heap_update_def + upt_rec take_heap_list_min drop_heap_list_general + heap_update_list_append heap_list_update_ptr heap_list_update_word32 + store_store_word32_commute_offset field_simps + heap_access_Array_element h_val_word32 h_val_ptr + field_lvalue_offset_eq ucast_eq_0s} + addsimps (Proof_Context.get_thms ctxt "field_h_val_rewrites") + addsimps (Proof_Context.get_thms ctxt "field_to_bytes_rewrites") + ), + simp_tac (ctxt addsimps @{thms store_word32s_equality_fold + store_word32s_equality_final add_commute}), + simp_tac (ctxt addsimprocs [store_word32s_equality_simproc] + addsimps @{thms store_word32s_equality_final add_commute}) ] -fun mk_graph_refines_proof funs noreturns hints s ctxt +fun mk_graph_refines_proof funs noreturns hints globals_swap_rewrites s ctxt = init_graph_refines_proof funs s ctxt |> full_simpl_to_graph_tac funs noreturns hints s ctxt |> Seq.hd - |> EVERY (map ALLGOALS (graph_refine_proof_tacs ctxt)) + |> EVERY (map ALLGOALS (graph_refine_proof_tacs globals_swap_rewrites ctxt)) |> Seq.hd *} diff --git a/tools/asmrefine/SimplExport.thy b/tools/asmrefine/SimplExport.thy index d3a4b1e94..d02a8e22f 100644 --- a/tools/asmrefine/SimplExport.thy +++ b/tools/asmrefine/SimplExport.thy @@ -93,10 +93,11 @@ fun get_field ctxt s = let val xs = space_explode "." s val fld = List.last xs val tp = rev xs |> tl |> rev |> space_implode "." - val fld = unsuffix "_update" fld handle Fail _ => fld + val is_upd = String.isSuffix "_update" fld + val fld = if is_upd then unsuffix "_update" fld else fld val _ = Proof_Context.get_thm ctxt (tp ^ "_" ^ fld ^ "_fl_Some") - in SOME (tp, fld) end + in SOME (tp, fld, is_upd) end handle ERROR _ => NONE | Bind => NONE @@ -213,7 +214,101 @@ fun convert_type _ _ @{typ bool} = "Bool" else (Proof_Context.get_thm ctxt (Long_Name.base_name s ^ "_td_names"); "Struct " ^ s) | convert_type _ _ T = raise TYPE ("convert_type", [T], []) +*} +consts + pseudo_acc :: "'a \ 'a" + +text {* + +Phase 1 of the conversion, converts accs and upds on SIMPL +state (a record) to accs of named vars, using the pseudo_acc +constant above to guard the accesses and lists of upds with strings. +*} + +ML {* + +fun naming localname = Long_Name.base_name localname + |> unsuffix "_'" |> suffix "#v" + +fun mk_pseudo_acc s T = Const (@{const_name pseudo_acc}, T --> T) + $ Free (s, T) + +fun dest_global_mem_acc_addr (params : export_params) t = let + val acc = case head_of t of Const (c, _) => #rw_global_accs params c + | _ => NONE + val const = #const_globals params t + val T = fastype_of t + in case (const, acc) of + (SOME nm, _) => SOME (TermsTypes.mk_global_addr_ptr (nm, T)) + | (NONE, SOME nm) => SOME (TermsTypes.mk_global_addr_ptr (nm, T)) + | (NONE, NONE) => NONE + end + +fun dest_ptr_type (Type (@{type_name ptr}, [a])) = a + | dest_ptr_type T = raise TYPE ("dest_ptr_type", [T], []) + +fun mk_memacc p = let + val T = fastype_of p + in Const (@{const_name h_val}, @{typ heap_mem} --> T --> dest_ptr_type T) + $ mk_pseudo_acc "Mem" @{typ heap_mem} $ p end + +fun convert_fetch_phase1 _ (@{term hrs_mem} $ _) = mk_pseudo_acc "Mem" @{typ heap_mem} + | convert_fetch_phase1 _ (@{term hrs_htd} $ _) = mk_pseudo_acc "HTD" @{typ heap_typ_desc} + | convert_fetch_phase1 params (Abs (s, T, t)) + = Abs (s, T, convert_fetch_phase1 params t) + | convert_fetch_phase1 params t = if not (is_Const (head_of t)) then t + else let + val (f, xs) = strip_comb t + val (c, _) = dest_Const f + val T = fastype_of t + in case (#locals params c, dest_global_mem_acc_addr params t, #enums params c) of + (true, _, _) => (case xs of [Free ("s", _)] => mk_pseudo_acc (naming c) T + | [Free ("rv", _)] => mk_pseudo_acc ("rv#space#" ^ naming c) T + | _ => raise TERM ("convert_fetch_phase1: acc?", [t]) + ) + | (_, SOME p, _) => mk_memacc p + | (_, _, SOME n) => HOLogic.mk_number T n + | _ => list_comb (f, map (convert_fetch_phase1 params) xs) + end + +fun mk_memupd1 ptr v m = if dest_ptr_type (fastype_of ptr) = fastype_of v + then Const (@{const_name heap_update}, fastype_of ptr --> fastype_of v + --> @{typ "heap_mem \ heap_mem"}) + $ ptr $ v $ m + else raise TERM ("mk_memupd1: types disagree", [ptr, v]) + +fun mk_memupd2 ptr v = mk_memupd1 ptr v (mk_pseudo_acc "Mem" @{typ heap_mem}) + +fun convert_upd_phase1 params (t as (Const (@{const_name globals_update}, _) + $ (Const (c, _) $ f) $ s)) = (case (f, String.isPrefix NameGeneration.ghost_state_name + (Long_Name.base_name c), #rw_global_upds params c) of + (Const (@{const_name hrs_mem_update}, _) + $ (Const (@{const_name heap_update}, _) $ p $ v), _, _) + => [("Mem", convert_fetch_phase1 params (mk_memupd2 p v))] + | (Const (@{const_name hrs_htd_update}, _) $ g, _, _) + => [("HTD", (convert_fetch_phase1 params + (betapply (g, mk_pseudo_acc "HTD" @{typ heap_typ_desc}))))] + | (_, true, _) => [] + | (_, _, SOME nm) => let + val acc = the (Symtab.lookup (#rw_globals_tab params) nm) |> fst + val v = convert_fetch_phase1 params (betapply (f, acc $ s)) + val ptr = TermsTypes.mk_global_addr_ptr (nm, fastype_of v) + in [("Mem", mk_memupd2 ptr v)] end + | _ => raise TERM ("convert_upd", [t])) + | convert_upd_phase1 params (t as (Const (c, _) $ f $ s)) = let + val c' = unsuffix Record.updateN c + val cT' = fastype_of s --> fastype_of (f $ s) + val _ = (#local_upds params c) orelse raise TERM ("convert_upd_phase1: nonlocal", [t]) + val v = betapply (f, Const (c', cT') $ s) + in [(naming c', convert_fetch_phase1 params v)] end + | convert_upd_phase1 _ t = raise TERM ("convert_upd_phase1", [t]) +*} + +text {* Phase 2 eliminates compound types, so we access and +update only words from memory and local values. *} + +ML {* fun ptr_simp ctxt = ctxt addsimps @{thms CTypesDefs.ptr_add_def size_of_def size_td_array field_lvalue_offset_eq align_td_array' word_of_int scast_def[symmetric] sint_sbintrunc' sdiv_word_def sdiv_int_def} @@ -231,9 +326,6 @@ fun ptr_simp_term ctxt s pat t = let Syntax.pretty_term ctxt t |> Pretty.writeln) in Pattern.rewrite_term (Proof_Context.theory_of ctxt) [rew] [] t end -fun dest_ptr_type (Type (@{type_name ptr}, [a])) = a - | dest_ptr_type T = raise TYPE ("dest_ptr_type", [T], []) - fun dest_arrayT (Type (@{type_name array}, [elT, nT])) = let in (elT, dest_binT nT) end | dest_arrayT T = raise TYPE ("dest_arrayT", [T], []) @@ -249,19 +341,6 @@ fun get_c_type_size ctxt T = let val ptr_to_typ = Logic.mk_type o dest_ptr_type o fastype_of -val space_pad = space_implode " " - -fun space_pad_list xs = space_pad (string_of_int (length xs) :: xs) - -fun s_st ctxt = Syntax.read_term ctxt "s :: globals myvars" - -fun mk_acc_array i T xs = let - in fold (fn (j, x) => fn s => "Op IfThenElse " ^ T - ^ " 3 Op Equals Bool 2 " ^ i ^ " Num " ^ string_of_int j ^ " Word 32 " - ^ x ^ " " ^ s) - (1 upto (length xs - 1) ~~ tl xs) (hd xs) - end - fun mk_arr_idx arr i = let val arrT = fastype_of arr val elT = case arrT of Type (@{type_name "array"}, [elT, _]) @@ -284,46 +363,60 @@ fun mk_ptr_offs opt_T p offs = let end fun get_acc_type [] T = T - | get_acc_type accs _ = head_of (List.last accs) - |> type_of |> strip_type |> snd + | get_acc_type accs _ = (List.last accs $ @{term x}) + |> fastype_of -fun dest_mem_acc_addr _ (Const (@{const_name h_val}, _) $ _ $ p) +val normalise_ring_ops = let + fun gather_plus (Const (@{const_name "plus"}, _) $ a $ b) + = gather_plus a @ gather_plus b + | gather_plus x = [x] + fun gather_times (Const (@{const_name "times"}, _) $ a $ b) + = gather_times a @ gather_times b + | gather_times x = [x] + fun fold_op _ [x] = x + | fold_op oper (x :: xs) = oper $ x $ (fold_op oper xs) + | fold_op _ [] = error "fold_op: shouldn't get empty list" + fun inner (x as (Const (@{const_name "plus"}, _) $ _ $ _)) + = gather_plus x |> map inner + |> sort Term_Ord.fast_term_ord + |> fold_op (head_of x) + | inner (x as (Const (@{const_name "times"}, _) $ _ $ _)) + = gather_times x |> map inner + |> sort Term_Ord.fast_term_ord + |> fold_op (head_of x) + | inner (f $ x) = inner f $ inner x + | inner x = x + in inner end + +fun dest_mem_acc_addr (Const (@{const_name h_val}, _) $ _ $ p) = SOME p - | dest_mem_acc_addr (params : export_params) t = let - val acc = case head_of t of Const (c, _) => #rw_global_accs params c - | _ => NONE - val const = #const_globals params t - val T = fastype_of t - in case (const, acc) of - (SOME nm, _) => SOME (TermsTypes.mk_global_addr_ptr (nm, T)) - | (NONE, SOME nm) => SOME (TermsTypes.mk_global_addr_ptr (nm, T)) - | (NONE, NONE) => NONE - end + | dest_mem_acc_addr _ = NONE fun narrow_mem_upd ctxt (params : export_params) p v = let val T = fastype_of v - val mk_offs = mk_ptr_offs NONE p - val mk_offs2 = mk_offs o HOLogic.mk_number @{typ word32} + fun mk_offs T = mk_ptr_offs (SOME T) p + fun mk_offs2 T = mk_offs T o HOLogic.mk_number @{typ word32} val sterm = Syntax.pretty_term ctxt #> Pretty.string_of val styp = Syntax.pretty_typ ctxt #> Pretty.string_of - in if (dest_mem_acc_addr params v = SOME p) then [] + in if (dest_mem_acc_addr v = SOME p) then [] else if #structs_by_typ params (fst (dest_Type T)) <> NONE then let val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T))) - val fld_writes = map (fn (_, (acc, offs)) => (mk_offs2 offs, - #cons_field_upds params (acc $ v))) flds + val fld_writes = map (fn (_, (acc, offs)) + => (mk_offs2 (fastype_of (acc $ v)) offs, + #cons_field_upds params (acc $ v))) flds in maps (uncurry (narrow_mem_upd ctxt params)) fld_writes end else if fst (dest_Type T) = @{type_name array} then let val (elT, n) = dest_arrayT T val elT_size = get_c_type_size ctxt elT in case v of (Const (@{const_name Arrays.update}, _) $ arr $ i $ x) - => narrow_mem_upd ctxt params (mk_offs (@{term "op * :: word32 => _"} + => narrow_mem_upd ctxt params (mk_offs elT (@{term "op * :: word32 => _"} $ HOLogic.mk_number @{typ word32} elT_size $ (@{term "of_nat :: nat \ word32"} $ i))) x @ narrow_mem_upd ctxt params p arr | _ => let - val addrs = map (fn i => (mk_offs2 (i * elT_size))) + val addrs = map (fn i => (mk_offs2 elT (i * elT_size))) (0 upto (n - 1)) val elems = dest_array_init v handle TERM _ => map @@ -340,6 +433,16 @@ fun narrow_mem_upd ctxt (params : export_params) p v = let else [(p, v)] end +fun triv_mem_upd ctxt p v = case dest_mem_acc_addr v of + NONE => false + | SOME p' => p aconv p' orelse let + val t = @{term "op - :: word32 \ _"} $ get_ptr_val p $ get_ptr_val p' + val thm = ptr_simp ctxt (cterm_of (Proof_Context.theory_of ctxt) t) + val t' = Thm.rhs_of thm |> term_of + in t' = @{term "0 :: word32"} + orelse (Display.pretty_thm ctxt thm |> Pretty.writeln; false) + end + fun narrow_mem_acc _ _ [] p = p | narrow_mem_acc ctxt params accs p = let fun get_offs (Const (@{const_name Arrays.index}, idxT) $ i) = let @@ -361,189 +464,241 @@ fun narrow_mem_acc _ _ [] p = p (map get_offs accs) in mk_ptr_offs (SOME T') p offs end -fun convert_mem_acc ctxt params accs p m = let - val p' = narrow_mem_acc ctxt params accs p - val T = dest_ptr_type (fastype_of p') - handle TYPE _ => raise TERM ("convert_mem_acc", p :: p' :: accs) - in "Op MemAcc " ^ (convert_type false ctxt T) ^ " 2 " ^ m ^ " " ^ convert_fetch ctxt params [] p' end +fun try_norm_index ctxt i = let + val i' = ptr_simp_term ctxt "idx_simp" i i + in dest_nat i'; i' end handle TERM _ => i -and convert_op_accs ctxt params accs nm tp xs = "Op " ^ nm ^ " " ^ tp - ^ " " ^ space_pad_list (map (convert_fetch ctxt params accs) xs) +fun mk_acc_array i xs = let + val n = length xs + val _ = warning ("expanding acc array, width " ^ string_of_int n) + val i = @{term "of_nat :: nat \ word32"} $ i + fun inner [(x, _)] = x + | inner ((x, j) :: xs) = let + val y = inner xs + val T = fastype_of x + in Const (@{const_name "If"}, HOLogic.boolT --> T --> T --> T) + $ HOLogic.mk_eq (i, HOLogic.mk_number @{typ word32} j) $ x $ y end + | inner [] = error "mk_acc_array: empty" + in inner (xs ~~ (0 upto (n - 1))) end -and convert_op ctxt params nm tp xs = convert_op_accs ctxt params [] nm tp xs - -and convert_fetch ctxt params [] (Const (@{const_name Collect}, _) $ S $ x) - = convert_fetch ctxt params [] (betapply (S, x)) - | convert_fetch ctxt params [] (Const (@{const_name Lattices.inf}, _) $ S $ T $ x) - = convert_op ctxt params "And" "Bool" [betapply (S, x), betapply (T, x)] - | convert_fetch ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _)) - = convert_fetch ctxt params [] (ptr_simp_term ctxt "ptr_add" +fun convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _)) + = convert_fetch_ph2 ctxt params [] (ptr_simp_term ctxt "ptr_add" (head_of t $ Free ("p", domain_type T) $ Free ("n", @{typ int})) t) - | convert_fetch ctxt params [] (t as (Const (@{const_name field_lvalue}, T) $ _ $ s)) - = convert_fetch ctxt params [] (ptr_simp_term ctxt "field_lvalue" + | convert_fetch_ph2 ctxt params [] (t as (Const (@{const_name field_lvalue}, T) $ _ $ s)) + = convert_fetch_ph2 ctxt params [] (ptr_simp_term ctxt "field_lvalue" (head_of t $ Free ("p", domain_type T) $ s) t) - | convert_fetch ctxt params [] (Const (@{const_name Ptr}, _) $ p) = convert_fetch ctxt params [] p - | convert_fetch ctxt params [] (Const (@{const_name ptr_val}, _) $ p) = convert_fetch ctxt params [] p - | convert_fetch ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) + | convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) (t as (Const (@{const_name fupdate}, _) $ _ $ _ $ _)) = let - val xs = dest_array_init (#cons_field_upds params t) - in case (try dest_nat i) of - SOME i => convert_fetch ctxt params accs (nth xs i) - | NONE => mk_acc_array (convert_fetch ctxt params [] i) - (convert_type false ctxt (get_acc_type accs (fastype_of (hd xs)))) - (map (convert_fetch ctxt params accs) xs) + val xs = dest_array_init (#cons_field_upds (params : export_params) t) + in case (try dest_nat (try_norm_index ctxt i)) of + SOME i => convert_fetch_ph2 ctxt params accs (nth xs i) + | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i) + (map (convert_fetch_ph2 ctxt params accs) xs) end - | convert_fetch ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) + | convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs) (t as (Const (@{const_name FCP}, _) $ _)) = let val xs = dest_array_init (#cons_field_upds params t) - in case (try dest_nat i) of - SOME i => convert_fetch ctxt params accs (nth xs i) - | NONE => mk_acc_array (convert_fetch ctxt params [] i) (convert_type false ctxt (fastype_of (hd xs))) - (map (convert_fetch ctxt params accs) xs) + in case (try dest_nat (try_norm_index ctxt i)) of + SOME i => convert_fetch_ph2 ctxt params accs (nth xs i) + | NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i) + (map (convert_fetch_ph2 ctxt params accs) xs) end - | convert_fetch ctxt params accs ((idx as Const (@{const_name Arrays.index}, _)) $ arr $ i) = let - val i' = ptr_simp_term ctxt "idx_simp" i i handle TERM _ => i - in case try dest_nat i' of SOME _ => convert_fetch ctxt params (idx $ i' :: accs) arr - | NONE => convert_fetch ctxt params (idx $ i :: accs) arr end - | convert_fetch ctxt params ((idx as Const (@{const_name Arrays.index}, _)) $ i :: accs) + | convert_fetch_ph2 ctxt params accs ((idx as Const (@{const_name Arrays.index}, _)) $ arr $ i) = let + val i' = try_norm_index ctxt i + in convert_fetch_ph2 ctxt params (idx $ i' :: accs) arr end + | convert_fetch_ph2 ctxt params ((idx as Const (@{const_name Arrays.index}, _)) $ i :: accs) (Const (@{const_name Arrays.update}, _) $ arr' $ i' $ v) = let val eq = HOLogic.mk_eq (i, i') val eq = ptr_simp_term ctxt "idx_eq_simp" eq eq handle TERM _ => eq - val x = convert_fetch ctxt params accs v - val y = convert_fetch ctxt params (idx $ i :: accs) arr' + val x = convert_fetch_ph2 ctxt params accs v + val y = convert_fetch_ph2 ctxt params (idx $ try_norm_index ctxt i :: accs) arr' + val T = fastype_of x in case eq of @{term True} => x | @{term False} => y - | eq => "Op IfThenElse " ^ (convert_type false ctxt (fastype_of v)) - ^ " " ^ space_pad_list [convert_fetch ctxt params [] eq, x, y] end - | convert_fetch ctxt params [] (Const (@{const_name store_word32}, _) $ p $ w $ m) + | _ => Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) + $ convert_fetch_ph2 ctxt params [] eq $ x $ y end + | convert_fetch_ph2 ctxt params accs (Const (@{const_name h_val}, _) $ _ $ p) + = let + val p = convert_fetch_ph2 ctxt params [] p + val p = narrow_mem_acc ctxt params accs p + in mk_memacc p end + | convert_fetch_ph2 ctxt params [] (Const (@{const_name heap_update}, _) $ p $ v $ m) + = let + val xs = narrow_mem_upd ctxt params p v + |> map (pairself (convert_fetch_ph2 ctxt params [])) + |> filter_out (uncurry (triv_mem_upd ctxt)) + val m = convert_fetch_ph2 ctxt params [] m + in fold (uncurry mk_memupd1) xs m end + | convert_fetch_ph2 _ _ [] (t as (Const (@{const_name pseudo_acc}, _) $ _)) = t + | convert_fetch_ph2 ctxt params accs (Const (@{const_name pseudo_acc}, _) $ Free (s, T)) = let + val T = get_acc_type accs T + fun canon s [] = mk_pseudo_acc s T + | canon s (Const (@{const_name Arrays.index}, idxT) $ i :: accs) = (case + (try dest_nat (try_norm_index ctxt i)) + of SOME i => canon (s ^ "." ^ string_of_int i) accs + | NONE => let val (_, n) = dest_arrayT (domain_type idxT) + in mk_acc_array (convert_fetch_ph2 ctxt params [] i) + (map (fn j => canon (s ^ "." ^ string_of_int j) accs) + (0 upto (n - 1))) end) + | canon s (Const (acc_nm, _) :: accs) + = canon (s ^ "." ^ Long_Name.base_name acc_nm) accs + | canon _ (t :: _) = raise TERM ("convert_fetch_ph2: canon: ", [t]) + in canon s accs end + | convert_fetch_ph2 _ _ [] (t as (Free ("symbol_table", _) $ _)) + = t + | convert_fetch_ph2 _ _ [] (t as Free ("domain", _)) + = t + | convert_fetch_ph2 ctxt params accs t = let + val (f, xs) = strip_comb t + val (c, _) = dest_Const f + in if (get_field ctxt c |> Option.map #3) = SOME false + then case xs of [x] => convert_fetch_ph2 ctxt params (f :: accs) x + | _ => raise TERM ("convert_fetch_ph2: expected single", f :: xs) + else if (get_field ctxt c <> NONE orelse #cons_fields params c <> NONE) + then let + val _ = (accs <> []) orelse raise TERM ("convert_fetch_ph2: no accs", [t]) + val t' = hd accs $ t + val t'' = #cons_field_upds params t' + in if t'' aconv t' then raise TERM ("convert_fetch_ph2: irreducible upd:", [t']) + else convert_fetch_ph2 ctxt params (tl accs) t'' end + else list_comb (f, map (convert_fetch_ph2 ctxt params []) xs) end + +fun convert_upd_ph2_worker ctxt params s v T accs = + if #structs_by_typ params (fst (dest_Type T)) <> NONE + then let + val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T))) + in maps (fn (fld_nm, (acc, _)) => convert_upd_ph2_worker ctxt params (s ^ "." ^ fld_nm) + v (range_type (fastype_of acc)) (accs @ [acc])) flds end + else if fst (dest_Type T) = @{type_name array} + then let + val (elT, n) = dest_arrayT T + in maps (fn i => convert_upd_ph2_worker ctxt params (s ^ "." ^ string_of_int i) + v elT (accs @ [Const (@{const_name Arrays.index}, T --> @{typ nat} --> elT) + $ HOLogic.mk_number @{typ nat} i])) (0 upto (n - 1)) + end + else [(s, convert_fetch_ph2 ctxt params accs v)] + +fun convert_upd_ph2 ctxt params (s, v) + = convert_upd_ph2_worker ctxt params s v (fastype_of v) [] +(* |> tap (map (snd #> Syntax.pretty_term ctxt #> Pretty.writeln)) *) +*} + +text {* The final conversion reduces Isabelle terms to strings *} + +ML {* +val space_pad = space_implode " " + +fun space_pad_list xs = space_pad (string_of_int (length xs) :: xs) + +fun s_st ctxt = Syntax.read_term ctxt "s :: globals myvars" +fun rv_st ctxt = Syntax.read_term ctxt "rv :: globals myvars" + +fun convert_op ctxt params nm tp xs = "Op " ^ nm ^ " " ^ tp + ^ " " ^ space_pad_list (map (convert_ph3 ctxt params) xs) + +and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ x) + = convert_ph3 ctxt params (betapply (S, x)) + | convert_ph3 ctxt params (Const (@{const_name Lattices.inf}, _) $ S $ T $ x) + = convert_op ctxt params "And" "Bool" [betapply (S, x), betapply (T, x)] + | convert_ph3 ctxt params (Const (@{const_name Ptr}, _) $ p) = convert_ph3 ctxt params p + | convert_ph3 ctxt params (Const (@{const_name ptr_val}, _) $ p) = convert_ph3 ctxt params p + | convert_ph3 ctxt params (Const (@{const_name store_word32}, _) $ p $ w $ m) = convert_op ctxt params "MemUpdate" "Mem" [m, p, w] - | convert_fetch ctxt params [] (Const (@{const_name store_word8}, _) $ p $ w $ m) + | convert_ph3 ctxt params (Const (@{const_name store_word8}, _) $ p $ w $ m) = convert_op ctxt params "MemUpdate" "Mem" [m, p, w] - | convert_fetch ctxt params accs (Const (@{const_name h_val}, _) $ m $ p) - = convert_mem_acc ctxt params accs p (convert_fetch ctxt params [] m) - | convert_fetch ctxt params [] (Const (@{const_name load_word32}, _) $ p $ m) - = convert_op ctxt params "MemAcc" "Word 32" [m, p] - | convert_fetch ctxt params [] (Const (@{const_name load_word8}, _) $ p $ m) - = convert_op ctxt params "MemAcc" "Word 8" [m, p] - | convert_fetch ctxt params [] ((m as Free (_, @{typ "word32 \ word8"})) $ p) - = convert_op ctxt params "MemAcc" "Word 8" [m, p] - | convert_fetch ctxt params [] (Const (@{const_name fun_upd}, _) - $ (m as Free (_, @{typ "word32 \ word8"})) $ p $ v) + | convert_ph3 ctxt params (Const (@{const_name heap_update}, _) $ p $ v $ m) = convert_op ctxt params "MemUpdate" "Mem" [m, p, v] - | convert_fetch ctxt params [] ((le as Const (@{const_name less_eq}, _)) + | convert_ph3 ctxt params (t as (Const (@{const_name h_val}, _) $ m $ p)) + = convert_op ctxt params "MemAcc" (convert_type false ctxt (fastype_of t)) [m, p] + | convert_ph3 ctxt params (Const (@{const_name load_word32}, _) $ p $ m) + = convert_op ctxt params "MemAcc" "Word 32" [m, p] + | convert_ph3 ctxt params (Const (@{const_name load_word8}, _) $ p $ m) + = convert_op ctxt params "MemAcc" "Word 8" [m, p] + | convert_ph3 ctxt params ((le as Const (@{const_name less_eq}, _)) $ (Const (@{const_name insert}, _) $ p $ S) $ D) = convert_op ctxt params "And" "Bool" [HOLogic.mk_mem (p, D), le $ S $ D] - | convert_fetch ctxt params [] (Const (@{const_name less_eq}, _) - $ Const (@{const_name bot_class.bot}, _) $ _) = convert_fetch ctxt params [] @{term True} - | convert_fetch ctxt params [] (Const (@{const_name htd_safe}, _) $ _ $ _) = convert_fetch ctxt params [] @{term True} - | convert_fetch ctxt params [] (Const (@{const_name uminus}, T) $ v) + | convert_ph3 ctxt params (Const (@{const_name less_eq}, _) + $ Const (@{const_name bot_class.bot}, _) $ _) = convert_ph3 ctxt params @{term True} + | convert_ph3 ctxt params (Const (@{const_name htd_safe}, _) $ _ $ _) + = convert_ph3 ctxt params @{term True} + | convert_ph3 ctxt params (Const (@{const_name uminus}, T) $ v) = let val T = domain_type T - in convert_fetch ctxt params [] (Const (@{const_name minus}, T --> T --> T) + in convert_ph3 ctxt params (Const (@{const_name minus}, T --> T --> T) $ Const (@{const_name zero_class.zero}, T) $ v) end - | convert_fetch ctxt params [] (Const (@{const_name h_t_valid}, _) $ htd + | convert_ph3 ctxt params (Const (@{const_name h_t_valid}, _) $ htd $ Const (@{const_name c_guard}, _) $ p) = convert_op ctxt params "PValid" "Bool" [htd, ptr_to_typ p, p] - | convert_fetch ctxt params [] (Const (@{const_name ptr_inverse_safe}, _) $ p $ htd) + | convert_ph3 ctxt params (Const (@{const_name ptr_inverse_safe}, _) $ p $ htd) = convert_op ctxt params "PGlobalValid" "Bool" [htd, ptr_to_typ p, p] - | convert_fetch ctxt params [] (Const (@{const_name ptr_safe}, _) $ p $ htd) + | convert_ph3 ctxt params (Const (@{const_name ptr_safe}, _) $ p $ htd) = convert_op ctxt params "PWeakValid" "Bool" [htd, ptr_to_typ p, p] - | convert_fetch ctxt params [] (Const (@{const_name globals_list_distinct}, _) $ + | convert_ph3 ctxt params (Const (@{const_name globals_list_distinct}, _) $ (Const (@{const_name image}, _) $ Const (@{const_name fst}, _) $ (Const (@{const_name s_footprint}, _) $ _)) $ _ $ _) - = convert_fetch ctxt params [] @{term True} - | convert_fetch ctxt params [] (Const (@{const_name c_guard}, _) $ p) + = convert_ph3 ctxt params @{term True} + | convert_ph3 ctxt params (Const (@{const_name c_guard}, _) $ p) = convert_op ctxt params "PAlignValid" "Bool" [ptr_to_typ p, p] - | convert_fetch _ _ [] (Const (@{const_name hrs_htd}, _) $ _) - = "Var HTD HTD" - | convert_fetch _ _ [] (Const (@{const_name hrs_mem}, _) $ _) - = "Var Mem Mem" - | convert_fetch ctxt params [] (Const (@{const_name bot}, _) $ _) = convert_fetch ctxt params [] @{term False} - | convert_fetch ctxt params [] (Const (@{const_name top_class.top}, _) $ _) = convert_fetch ctxt params [] @{term True} - | convert_fetch ctxt params [] (Const (@{const_name insert}, _) $ v $ S $ x) + | convert_ph3 ctxt params (Const (@{const_name bot}, _) $ _) + = convert_ph3 ctxt params @{term False} + | convert_ph3 ctxt params (Const (@{const_name top_class.top}, _) $ _) + = convert_ph3 ctxt params @{term True} + | convert_ph3 ctxt params (Const (@{const_name insert}, _) $ v $ S $ x) = convert_op ctxt params "Or" "Bool" [HOLogic.mk_eq (v, x), betapply (S, x)] - | convert_fetch _ _ [] (Free ("symbol_table", _) $ s) + | convert_ph3 _ _ (Free ("symbol_table", _) $ s) = "Symbol " ^ HOLogic.dest_string s ^ " Word 32" - | convert_fetch ctxt params [] (Const (@{const_name of_nat}, T) $ (Const (@{const_name unat}, _) $ x)) + | convert_ph3 ctxt params (Const (@{const_name of_nat}, T) $ (Const (@{const_name unat}, _) $ x)) = let val t1 = fastype_of x val t2 = range_type T - in if t1 = t2 then convert_fetch ctxt params [] x - else convert_fetch ctxt params [] (Const (@{const_name ucast}, t1 --> t2) $ x) + in if t1 = t2 then convert_ph3 ctxt params x + else convert_ph3 ctxt params (Const (@{const_name ucast}, t1 --> t2) $ x) end - | convert_fetch ctxt params [] (t as (Const (@{const_name of_nat}, _) $ + | convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $ (Const (@{const_name count_leading_zeroes}, _) $ x))) = convert_op ctxt params "CountLeadingZeroes" (convert_type false ctxt (fastype_of t)) [x] - | convert_fetch ctxt params [] (t as (Const (@{const_name unat}, _) $ _)) - = convert_fetch ctxt params [] (@{term "of_nat :: nat \ word32"} $ t) - | convert_fetch ctxt params [] (t as (Const (@{const_name of_nat}, _) $ _)) - = convert_fetch ctxt params [] (ptr_simp_term ctxt "of_nat" t t) - | convert_fetch ctxt params [] (t as (Const (@{const_name power}, _) $ _ $ _)) - = convert_fetch ctxt params [] (ptr_simp_term ctxt "power" t t) - | convert_fetch ctxt params [] (Const (@{const_name ptr_coerce}, _) $ p) = convert_fetch ctxt params [] p - | convert_fetch ctxt params [] (Const (@{const_name fst}, _) $ tp) - = convert_fetch ctxt params [] (fst (HOLogic.dest_prod tp)) - | convert_fetch ctxt params [] (Const (@{const_name snd}, _) $ tp) - = convert_fetch ctxt params [] (snd (HOLogic.dest_prod tp)) - | convert_fetch ctxt params [] (t as (Const (@{const_name word_of_int}, _) $ _)) +(* | convert_ph3 ctxt params (t as (Const (@{const_name unat}, _) $ _)) + = convert_ph3 ctxt params (@{term "of_nat :: nat \ word32"} $ t) *) + | convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $ _)) + = convert_ph3 ctxt params (ptr_simp_term ctxt "of_nat" t t) + | convert_ph3 ctxt params (t as (Const (@{const_name power}, _) $ _ $ _)) + = convert_ph3 ctxt params (ptr_simp_term ctxt "power" t t) + | convert_ph3 ctxt params (Const (@{const_name ptr_coerce}, _) $ p) + = convert_ph3 ctxt params p + | convert_ph3 ctxt params (t as (Const (@{const_name word_of_int}, _) $ _)) = let val thy = Proof_Context.theory_of ctxt val t' = Pattern.rewrite_term thy (map (concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) @{thms word_uint.Rep_inverse word_sint.Rep_inverse}) [] t - in if t' aconv t then convert_fetch ctxt params [] (ptr_simp_term ctxt "word_of_int" t t) - else convert_fetch ctxt params [] t' end - | convert_fetch ctxt params [] (t as (Const (@{const_name sdiv}, _) $ _ $ _)) - = convert_fetch ctxt params [] (ptr_simp_term ctxt "sdiv" t t) - | convert_fetch ctxt _ [] (t as (Const (@{const_name numeral}, _) $ _)) + in if t' aconv t then convert_ph3 ctxt params (ptr_simp_term ctxt "word_of_int" t t) + else convert_ph3 ctxt params t' end + | convert_ph3 ctxt params (t as (Const (@{const_name sdiv}, _) $ _ $ _)) + = convert_ph3 ctxt params (ptr_simp_term ctxt "sdiv" t t) + | convert_ph3 ctxt _ (t as (Const (@{const_name numeral}, _) $ _)) = let val n = HOLogic.dest_number t |> snd - handle TERM _ => raise TERM ("convert_fetch", [t]) - val _ = (fastype_of t <> @{typ int}) orelse raise TERM ("convert_fetch: int", [t]) + handle TERM _ => raise TERM ("convert_ph3", [t]) + val _ = (fastype_of t <> @{typ int}) orelse raise TERM ("convert_ph3: int", [t]) in "Num " ^ signed_string_of_int n ^ " " ^ convert_type false ctxt (fastype_of t) end - | convert_fetch ctxt _ [] (Const (@{const_name TYPE}, Type (_, [T]))) + | convert_ph3 ctxt _ (Const (@{const_name TYPE}, Type (_, [T]))) = "Type " ^ convert_type true ctxt T - | convert_fetch ctxt params accs t = let + | convert_ph3 ctxt _ (Const (@{const_name pseudo_acc}, _) $ Free (s, T)) + = "Var " ^ s ^ " " ^ convert_type false ctxt T + | convert_ph3 ctxt params t = let val (f, xs) = strip_comb t val (c, _) = dest_Const f - val T = convert_type false ctxt (get_acc_type accs (fastype_of t)) - in case (#locals params c, (get_field ctxt c <> NONE) orelse (#cons_fields params c <> NONE), ops c) of - (true, _, _) => let - fun canon s [] = "Var " ^ s ^ " " ^ T - | canon s (Const (@{const_name Arrays.index}, idxT) $ i :: accs) = (case - (try dest_nat i) - of SOME i => canon (s ^ "." ^ string_of_int i) accs - | NONE => let val (_, n) = dest_arrayT (domain_type idxT) - in mk_acc_array (convert_fetch ctxt params [] i) T - (map (fn j => canon (s ^ "." ^ string_of_int j) accs) - (0 upto (n - 1))) end) - | canon s (Const (acc_nm, _) :: accs) - = canon (s ^ "." ^ Long_Name.base_name acc_nm) accs - | canon _ (t :: _) = raise TERM ("convert_fetch: canon: ", [t]) - in if xs = [s_st ctxt] then canon c accs - else if xs = [@{term t}] then canon ("rv#space#" ^ c) accs - else raise TERM ("convert_fetch: state", [t] @ xs) end - | (false, true, _) => (case xs of - [x] => convert_fetch ctxt params (f :: accs) x - | [_, _] => let - val _ = (accs <> []) orelse raise TERM ("convert_fetch: no accs", [t]) - val t' = hd accs $ t - val t'' = #cons_field_upds params t' - in if t'' aconv t' then raise TERM ("convert_fetch: irreducible upd:", [t']) - else convert_fetch ctxt params (tl accs) t'' end - | _ => raise TERM ("convert_fetch", [t])) - | (false, false, SOME (nm, _)) => if accs = [] - then convert_op ctxt params nm (convert_type false ctxt (fastype_of t)) xs - else raise TERM ("convert_fetch:", t :: accs) - | (false, false, NONE) => (case (dest_mem_acc_addr params t, #enums params c) of - (SOME p, _) => convert_mem_acc ctxt params accs p "Var Mem Mem" - | (NONE, SOME n) => "Num " ^ signed_string_of_int n ^ " " ^ convert_type false ctxt (fastype_of t) - | (NONE, NONE) => "Num " ^ signed_string_of_int (snd (HOLogic.dest_number t)) + val xs = if member (op =) [@{const_name shiftl}, + @{const_name shiftr}, @{const_name sshiftr}] c + then case xs of + [x, y] => [x, Const (@{const_name of_nat}, @{typ nat} --> fastype_of x) $ y] + | _ => raise TERM ("convert_ph3: shift", [t]) + else xs + in case ops c of + (SOME (nm, _)) => convert_op ctxt params nm (convert_type false ctxt (fastype_of t)) xs + | NONE => ("Num " ^ signed_string_of_int (snd (HOLogic.dest_number t)) ^ " " ^ convert_type false ctxt (fastype_of t) - handle TERM _ => raise TERM ("convert_fetch", [t])) + handle TERM _ => raise TERM ("convert_ph3", [t])) end -*} - -ML {* fun htd_simp ctxt = ctxt addsimps @{thms fold_all_htd_updates unat_lt2p[where 'a=32, simplified]} |> Simplifier.add_cong @{thm if_cong} |> Simplifier.rewrite @@ -551,64 +706,39 @@ fun htd_simp ctxt = ctxt addsimps @{thms fold_all_htd_updates fun simp_htd ctxt t = let val rew_thm = cterm_of (Proof_Context.theory_of ctxt) t |> htd_simp ctxt in term_of (Thm.rhs_of rew_thm) end + +fun convert_upd_ph3 ctxt params (s, v) = + let + val nm = if s = "HTD" then "HTD HTD" + else s ^ " " ^ convert_type false ctxt (fastype_of v) + val v = if s = "HTD" then simp_htd ctxt v else v + val v = convert_ph3 ctxt params v + in (nm, v) end + handle TERM (s, ts) => raise TERM ("convert_upd_ph3: " ^ s, v :: ts) *} ML {* -fun convert_mem_upd ctxt params p v hp = let - val upds = narrow_mem_upd ctxt params p v - in fold_rev (fn (p, v) => fn hp => "Op MemUpdate Mem " - ^ space_pad_list [hp, convert_fetch ctxt params [] p, convert_fetch ctxt params [] v]) upds hp - end +fun convert_fetch ctxt params t = + Envir.beta_eta_contract t + |> convert_fetch_phase1 params + |> convert_fetch_ph2 ctxt params [] + |> convert_ph3 ctxt params -fun get_local_var_upds ctxt params nm T v accs = - if #structs_by_typ params (fst (dest_Type T)) <> NONE - then let - val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T))) - in maps (fn (fld_nm, (acc, _)) => get_local_var_upds ctxt params (nm ^ "." ^ fld_nm) - (range_type (fastype_of acc)) v (accs @ [acc])) flds end - else if fst (dest_Type T) = @{type_name array} - then let - val (elT, n) = dest_arrayT T - in maps (fn i => get_local_var_upds ctxt params (nm ^ "." ^ string_of_int i) - elT v (accs @ [Const (@{const_name Arrays.index}, T --> @{typ nat} --> elT) - $ HOLogic.mk_number @{typ nat} i])) (0 upto (n - 1)) - end - else [(nm ^ " " ^ convert_type false ctxt T, convert_fetch ctxt params accs v)] +fun tracet (s, t) = ((Syntax.pretty_term @{context} t |> Pretty.writeln); (s, t)) -fun convert_upd ctxt params (t as (Const (@{const_name globals_update}, _) - $ (Const (c, _) $ f) $ s)) = (case (f, String.isPrefix NameGeneration.ghost_state_name - (Long_Name.base_name c), #rw_global_upds params c) of - (Const (@{const_name hrs_mem_update}, _) - $ (Const (@{const_name heap_update}, _) $ p $ v), _, _) - => ["Mem Mem " ^ convert_mem_upd ctxt params p v "Var Mem Mem"] - | (Const (@{const_name hrs_htd_update}, _) $ g, _, _) - => ["HTD HTD " ^ convert_fetch ctxt params [] (simp_htd ctxt (betapply (g, - @{term "hrs_htd thrs"})))] - | (_, true, _) => ["PMS PMS Var PMS PMS"] - | (_, _, SOME nm) => let - val acc = the (Symtab.lookup (#rw_globals_tab params) nm) |> fst - val v = betapply (f, acc $ s) - val ptr = TermsTypes.mk_global_addr_ptr (nm, fastype_of v) - in ["Mem Mem " ^ convert_mem_upd ctxt params ptr v "Var Mem Mem"] end - | _ => raise TERM ("convert_upd", [t])) - | convert_upd ctxt params (t as (Const (c, cT) $ f $ s)) = let - val v = betapply (f, Const (c, cT) $ s) - val T = fastype_of v - in case (#local_upds params c) of - true => get_local_var_upds ctxt params (unsuffix Record.updateN c) T v [] - |> map (fn (a, b) => a ^ " " ^ b) - | false => raise TERM ("convert_upd", [t]) - end - | convert_upd _ _ t = raise TERM ("convert_upd", [t]) - -fun convert_param_upds ctxt params (t as (Const (c, cT) $ f $ s)) - = (case #local_upds params c - of true => convert_param_upds ctxt params s @ let - val c' = unsuffix Record.updateN c - val v = betapply (f, Const (c', cT) $ s) - val T = fastype_of v - in get_local_var_upds ctxt params c' T v [] |> map snd end - | false => raise TERM ("convert_param_upds", [t])) +fun convert_param_upds ctxt params (t as (Const (c, _) $ _ $ s)) + = if #local_upds params c orelse c = @{const_name globals_update} + then convert_param_upds ctxt params s + @ (Envir.beta_eta_contract t +(* |> tap (Syntax.pretty_term ctxt #> Pretty.writeln) *) + |> convert_upd_phase1 params +(* |> map tracet *) +(* |> map (apsnd (Syntax.check_term ctxt)) *) + |> maps (convert_upd_ph2 ctxt params) +(* |> map (apsnd (Syntax.check_term ctxt)) *) + |> map (convert_upd_ph3 ctxt params) + ) + else raise TERM ("convert_param_upds", [t]) | convert_param_upds ctxt _ t = (if t = s_st ctxt then [] else raise TERM ("convert_param_upds", [t])) @@ -636,6 +766,17 @@ fun mk_set_int s t = let val T = fastype_of s in Const (@{const_name Lattices.inf}, T --> T --> T) $ s $ t end +val reduce_set_mem_eqs = @{thms mem_Collect_eq Int_iff Un_iff empty_iff iffI[OF TrueI UNIV_I]} + |> map (mk_meta_eq #> Thm.concl_of #> Logic.dest_equals) + +fun reduce_set_mem ctxt x S = let + val t = HOLogic.mk_mem (x, S) + val t' = Pattern.rewrite_term (Proof_Context.theory_of ctxt) + reduce_set_mem_eqs [] t + in if t aconv t' then Pretty.writeln (Syntax.pretty_term ctxt (HOLogic.mk_prod (t, t'))) + else (); t' + end + fun has_reads body = exists_Const (fn (s, T) => snd (strip_type T) = @{typ heap_raw_state} orelse s = @{const_name Spec}) body @@ -671,13 +812,26 @@ fun is_no_write ctxt s = let val mex = exists_Const (fn (s, _) => s = @{const_name mex}) (concl_of thm) in not mex end +fun synthetic_updates ctxt params pref (Const (c, T)) = let + val s = s_st ctxt + val sT = fastype_of s + val xT = range_type T + val upd = Const (suffix Record.updateN c, (xT --> xT) --> sT --> sT) + $ Abs ("v", xT, Bound 0) $ s + |> Syntax.check_term ctxt + val upds = convert_param_upds ctxt params upd + in map (apfst (prefix pref)) upds end + | synthetic_updates _ _ _ t = raise TERM ("synthetic_updates", [t]) + fun is_no_read_globals ctxt params = is_no_read ctxt params true fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let val (n, nm) = emit_body ctxt params b n c e handle TERM (s, ts) => raise TERM (s, b :: ts) + | Empty => raise TERM ("emit_body: got Empty", [b]) val (n, nm) = emit_body ctxt params a n nm e handle TERM (s, ts) => raise TERM (s, a :: ts) + | Empty => raise TERM ("emit_body: got Empty", [a]) in (n, nm) end | emit_body ctxt params (Const (@{const_name Catch}, _) $ a $ b) n c e = (case b of Const (@{const_name com.Skip}, _) => emit_body ctxt params a n c (c, c) @@ -693,7 +847,7 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let | emit_body ctxt params (Const (@{const_name com.Cond}, _) $ S $ a $ b) n c e = let val (n, nm_a) = emit_body ctxt params a n c e val (n, nm_b) = emit_body ctxt params b n c e - val s = convert_fetch ctxt params [] (betapply (S, s_st ctxt)) + val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) S) in emit (string_of_int n ^ " Cond " ^ nm_a ^ " " ^ nm_b ^ " " ^ s); (n + 1, string_of_int n) @@ -712,7 +866,7 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let sdiv_word32_min[THEN eqTrueI] sdiv_word32_max_ineq signed_shift_guard_to_word_32} |> map (concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)) [] G - val s = convert_fetch ctxt params [] (betapply (G, s_st ctxt)) + val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) G) in emit (string_of_int n ^ " Cond " ^ nm ^ " Err " ^ s); (n + 1, string_of_int n) @@ -720,7 +874,9 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let | emit_body _ _ (Const (@{const_name com.Basic}, _) $ Abs (_, _, Bound 0)) n c _ = (n, c) | emit_body ctxt params (Const (@{const_name com.Basic}, _) $ f) n c _ = let - val upds = convert_upd ctxt params (betapply (f, s_st ctxt)) + val upds = convert_param_upds ctxt params (betapply (f, s_st ctxt)) + |> filter_out (fn (s, v) => v = "Var " ^ s) + |> map (fn (s, v) => s ^ " " ^ v) in emit (string_of_int n ^ " Basic " ^ c ^ " " ^ space_pad_list upds); (n + 1, string_of_int n) @@ -728,13 +884,11 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let | emit_body ctxt params (Const (@{const_name call}, _) $ f $ Const (p, _) $ _ $ r2) n c e = let val proc_info = Hoare.get_data ctxt |> #proc_info - val ret_val = Symtab.lookup proc_info (Long_Name.base_name p) + val ret_vals = Symtab.lookup proc_info (Long_Name.base_name p) |> the |> #params |> filter (fn (v, _) => v = HoarePackage.Out) |> maps (snd #> Proof_Context.read_const_proper ctxt true - #> dest_Const - #> (fn (s, T) => get_local_var_upds ctxt params ("rv#space#" ^ s) (range_type T) - (Const (s, T) $ s_st ctxt) [])) + #> synthetic_updates ctxt params "rv#space#") |> map fst val p_short = unsuffix "_'proc" (Long_Name.base_name p) @@ -743,13 +897,14 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let (* writes implicitly require reads, really *) val no_read = no_read andalso no_write - val args = (convert_param_upds ctxt params (betapply (f, s_st ctxt)) + val args = ((convert_param_upds ctxt params (betapply (f, s_st ctxt)) + |> map snd (* discard the local names of the updated variables *)) @ (if no_read then [] else all_c_in_params)) handle TERM (s, ts) => raise TERM ("emit_body call: " ^ s, f :: ts) - val out = ret_val @ (if no_write then [] else all_c_params) + val out = ret_vals @ (if no_write then [] else all_c_params) - val (n, nm_save) = emit_body ctxt params (betapplys (r2, [@{term i}, @{term t}])) n c e + val (n, nm_save) = emit_body ctxt params (betapplys (r2, [@{term i}, rv_st ctxt])) n c e in emit (string_of_int n ^ " Call " ^ nm_save ^ " " ^ (unsuffix "_'proc" p) ^ " " ^ space_pad_list args ^ " " ^ space_pad_list out); @@ -761,35 +916,22 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let fun sn i = string_of_int (n + i) val lc = "loop#count" ^ sn 0 ^ " Word 32" val (n', nm) = emit_body ctxt params a (n + 3) (sn 0) e - val cond = convert_fetch ctxt params [] (betapply (C, s_st ctxt)) + val cond = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) C) in emit (sn 0 ^ " Basic " ^ sn 1 ^ " 1 " ^ lc ^ " Op Plus Word 32 2 Var " ^ lc ^ " Num 1 Word 32"); emit (sn 1 ^ " Cond " ^ nm ^ " " ^ c ^ " " ^ cond); emit (sn 2 ^ " Basic " ^ sn 1 ^ " 1 " ^ lc ^ " Num 0 Word 32"); (n', sn 2) end - | emit_body ctxt params ((sw as Const (@{const_name switch}, _)) $ f - $ ((Const (@{const_name Cons}, _)) - $ (Const (@{const_name Pair}, _) $ C $ a) $ xs)) n c e = let - val (n, nm_xs) = emit_body ctxt params (sw $ f $ xs) n c e - val (n, nm_a) = emit_body ctxt params a n c e - val s = convert_fetch ctxt params [] (betapply (C, betapply (f, s_st ctxt))) - in emit (string_of_int n ^ " Cond " ^ nm_a ^ " " ^ nm_xs ^ " " ^ s); - (n + 1, string_of_int n) end - | emit_body _ _ (Const (@{const_name switch}, _) - $ _ $ Const (@{const_name Nil}, _)) n c _ - = (n, c) | emit_body _ _ t _ _ _ = raise TERM ("emit_body", [t]) fun emit_func_body ctxt eparams name = let val proc_info = Hoare.get_data ctxt |> #proc_info val params = Symtab.lookup proc_info (name ^ "_'proc") - |> the |> #params - |> map (apsnd (fn c => Proof_Context.read_const_proper ctxt true c - |> dest_Const - |> (fn (s, T) => get_local_var_upds ctxt eparams s (range_type T) - (Const (s, T) $ s_st ctxt) []) - |> map fst)) + |> the |> #params + |> map (apsnd (Proof_Context.read_const_proper ctxt true + #> synthetic_updates ctxt eparams "" + #> map fst)) val no_read = mk_safe is_no_read_globals ctxt eparams name val no_write = mk_safe (K o is_no_write) ctxt eparams name @@ -803,6 +945,9 @@ fun emit_func_body ctxt eparams name = let |> maps snd) @ (if no_write then [] else all_c_params) val body = Proof_Context.get_thm ctxt (name ^ "_body_def") + |> simplify (put_simpset HOL_basic_ss ctxt + addsimps @{thms switch.simps fst_conv snd_conv + insert_iff empty_iff}) |> concl_of |> Logic.dest_equals |> snd handle ERROR _ => @{term "Spec S"} From 0346fb20b62a57a2b9e05d09c166a3be230e6650 Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Wed, 27 Aug 2014 15:30:34 +1000 Subject: [PATCH 2/2] SIMPL->Graph proofs largely working. --- lib/LemmaBucket_C.thy | 218 ++++++++--- proof/asmrefine/SEL4GlobalsSwap.thy | 96 ++++- proof/asmrefine/SEL4GraphRefine.thy | 158 ++++---- proof/infoflow/Noninterference.thy | 5 +- tools/asmrefine/FieldAccessors.thy | 18 +- tools/asmrefine/GraphRefine.thy | 324 ++++++---------- tools/asmrefine/ProveGraphRefine.thy | 532 +++++++++++++++++++++++++++ tools/asmrefine/SimplExport.thy | 2 +- 8 files changed, 1014 insertions(+), 339 deletions(-) create mode 100644 tools/asmrefine/ProveGraphRefine.thy diff --git a/lib/LemmaBucket_C.thy b/lib/LemmaBucket_C.thy index a6a966ed8..acc9bbe8e 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/LemmaBucket_C.thy @@ -676,16 +676,26 @@ lemma scast_of_nat [simp]: by (metis (hide_lams, no_types) len_signed scast_def uint_sint word_of_nat word_ubin.Abs_norm word_ubin.eq_norm) +definition + array_ptr_index :: "(('a :: c_type)['b :: finite]) ptr \ bool \ nat \ 'a ptr" +where + "array_ptr_index p coerce n = CTypesDefs.ptr_add (ptr_coerce p) + (if coerce \ n \ CARD ('b) then 0 else of_nat n)" + +lemmas array_ptr_index_simps + = array_ptr_index_def[where coerce=False, simplified] + array_ptr_index_def[where coerce=True, simplified] + lemma heap_update_Array: "heap_update (p ::('a::packed_type['b::finite]) ptr) arr - = (\s. foldl (\s n. heap_update (CTypesDefs.ptr_add (Ptr (ptr_val p) :: 'a ptr) (of_nat n)) + = (\s. foldl (\s n. heap_update (array_ptr_index p False n) (Arrays.index arr n) s) s [0 ..< card (UNIV :: 'b set)])" apply (rule ext, simp add: heap_update_def) apply (subst coerce_heap_update_to_heap_updates [OF _ refl, where chunk="size_of TYPE('a)" and m="card (UNIV :: 'b set)"]) apply simp apply (rule foldl_cong[OF refl refl]) - apply (simp add: CTypesDefs.ptr_add_def) + apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def) apply (rule_tac f="\xs. heap_update_list ?p xs ?s" in arg_cong) apply (simp add: to_bytes_def size_of_def packed_type_access_ti) @@ -700,14 +710,14 @@ lemma heap_update_Array: apply simp done -lemma heap_access_Array_element: +lemma heap_access_Array_element': fixes p :: "('a::mem_type['b::finite]) ptr" assumes less: "of_nat n < card (UNIV :: 'b set)" shows "index (h_val hp p) n - = h_val hp (CTypesDefs.ptr_add (ptr_coerce p) (of_nat n))" + = h_val hp (array_ptr_index p False n)" using less - apply (simp add: CTypesDefs.ptr_add_def h_val_def) + apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def h_val_def) apply (simp add: from_bytes_def size_of_def typ_info_array') apply (subst update_ti_list_array'[OF refl]) apply simp @@ -731,6 +741,9 @@ lemma heap_access_Array_element: apply (simp add: size_of_def) done +lemmas heap_access_Array_element + = heap_access_Array_element'[simplified array_ptr_index_simps] + lemma heap_update_id: "h_val hp ptr = (v :: 'a :: packed_type) \ heap_update ptr v hp = hp" @@ -742,15 +755,42 @@ lemma heap_update_id: td_fafu_idem wf_fd) done -lemma heap_update_Array_element': - fixes p' :: "(('a :: packed_type)['b::finite]) ptr" - fixes p :: "('a :: packed_type) ptr" - fixes hp w - assumes p: "p = CTypesDefs.ptr_add (ptr_coerce p') (of_nat n)" - assumes n: "n < CARD('b)" - assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ 32" - shows "heap_update p' (Arrays.update (h_val hp p') n w) hp - = heap_update p w hp" +lemma fold_cong': + "a = b \ xs = ys \ (\x. x \ set xs =simp=> f x = g x) + \ fold f xs a = fold g ys b" + unfolding simp_implies_def + by (metis fold_cong) + +lemma intvl_empty2: + "({p ..+ n} = {}) = (n = 0)" + by (auto simp add: intvl_def) + +lemma heap_update_list_commute: + "{p ..+ length xs} \ {q ..+ length ys} = {} + \ heap_update_list p xs (heap_update_list q ys hp) + = heap_update_list q ys (heap_update_list p xs hp)" + apply (cases "length xs < addr_card") + apply (cases "length ys < addr_card") + apply (rule ext, simp add: heap_update_list_value) + apply blast + apply (simp_all add: addr_card intvl_overflow intvl_empty2) + done + +lemma heap_update_commute: + "\ {ptr_val p ..+ size_of TYPE('a)} \ {ptr_val q ..+ size_of TYPE('b)} = {}; + wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)) \ + \ heap_update p v (heap_update q (u :: 'b :: c_type) h) + = heap_update q u (heap_update p (v :: 'a :: c_type) h)" + apply (simp add: heap_update_def) + apply (simp add: heap_update_list_commute heap_list_update_disjoint_same + to_bytes_def length_fa_ti size_of_def Int_commute) + done + +lemma heap_update_Array_update: + assumes n: "n < CARD('b :: finite)" + assumes size: "CARD('b) * size_of TYPE('a :: packed_type) < 2 ^ 32" + shows "heap_update p (Arrays.update (arr :: 'a['b]) n v) hp + = heap_update (array_ptr_index p False n) v (heap_update p arr hp)" proof - have P: "\x k. \ x < CARD('b); k < size_of TYPE('a) \ @@ -772,20 +812,19 @@ proof - apply (simp add: unat_of_nat unat_add_lem[THEN iffD1]) done + let ?key_upd = "heap_update (array_ptr_index p False n) v" + note commute = fold_commute_apply[where h="?key_upd" + and xs="[Suc n ..< CARD('b)]", where g=f' and f=f', standard] + show ?thesis using n - apply (simp add: heap_update_Array) - apply (subst split_upt_on_n[OF n]) - apply (simp add: index_update p) - apply (subst foldl_does_nothing[where s=hp]) - apply (simp add: index_update2) - apply (rule heap_update_id) - apply (simp add: heap_access_Array_element) - apply (rule foldl_does_nothing) - apply (rule heap_update_id) - apply (simp add: heap_access_Array_element index_update2) - apply (simp add: h_val_def heap_update_def) - apply (subst heap_list_update_disjoint_same, simp_all) - apply (simp add: CTypesDefs.ptr_add_def intvl_def Suc_le_eq) + apply (simp add: heap_update_Array split_upt_on_n[OF n] + foldl_conv_fold) + apply (subst commute) + apply (simp_all add: packed_heap_update_collapse + cong: fold_cong') + apply (rule ext, simp) + apply (rule heap_update_commute, simp_all add: ptr_add_def) + apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def intvl_def Suc_le_eq) apply (rule set_eqI, clarsimp) apply (drule word_unat.Rep_inject[THEN iffD2]) apply (clarsimp simp: P nat_eq_add_iff1) @@ -793,6 +832,31 @@ proof - done qed +lemma heap_update_id_Array: + fixes arr :: "('a :: packed_type)['b :: finite]" + shows "arr = h_val hp p + \ heap_update p arr hp = hp" + apply (simp add: heap_update_Array) + apply (rule foldl_does_nothing[where s=hp]) + apply (simp add: heap_access_Array_element' heap_update_id) + done + +lemma heap_update_Array_element'': + fixes p' :: "(('a :: packed_type)['b::finite]) ptr" + fixes p :: "('a :: packed_type) ptr" + fixes hp w + assumes p: "p = array_ptr_index p' False n" + assumes n: "n < CARD('b)" + assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ 32" + shows "heap_update p' (Arrays.update (h_val hp p') n w) hp + = heap_update p w hp" + apply (subst heap_update_Array_update[OF n size]) + apply (simp add: heap_update_id_Array p) + done + +lemmas heap_update_Array_element' + = heap_update_Array_element''[simplified array_ptr_index_simps] + lemma fourthousand_size: "CARD('b :: fourthousand_count) * size_of TYPE('a :: oneMB_size) < 2 ^ 32" using oneMB_size_ax[where 'a='a] fourthousand_count_ax[where 'a='b] @@ -840,40 +904,82 @@ lemma typ_slice_t_array: apply (simp only: size_of_def mult_le_mono1) done +lemma h_t_valid_Array_element': + "\ htd \\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce \ n < CARD('b) \ + \ htd \\<^sub>t array_ptr_index p coerce n" + apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def + c_guard_def c_null_guard_def) + apply (subgoal_tac "\offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs) + \ offs < CARD ('b)") + apply (clarsimp simp: size_td_array size_of_def typ_uinfo_t_def + typ_info_array array_tag_def) + apply (intro conjI) + apply (clarsimp simp: CTypesDefs.ptr_add_def + field_simps) + apply (drule_tac x="offs * size_of TYPE('a) + y" in spec) + apply (drule mp) + apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) + apply (simp add: size_of_def) + apply (simp only: size_of_def mult_le_mono1) + apply (clarsimp simp: field_simps) + apply (erule map_le_trans[rotated]) + apply (rule list_map_mono) + apply (subst mult_commute, rule typ_slice_t_array[unfolded array_tag_def]) + apply assumption + apply (simp add: size_of_def) + apply (simp add: ptr_aligned_def align_of_def align_td_array + array_ptr_index_def + CTypesDefs.ptr_add_def unat_word_ariths unat_of_nat) + using align_size_of[where 'a='a] align[where 'a='a] + apply (simp add: align_of_def size_of_def addr_card_def card_word) + apply (simp add: dvd_mod dvd_add dvd_mult) + apply (thin_tac "\x. ?P x") + apply (clarsimp simp: intvl_def) + apply (drule_tac x="offs * size_of TYPE('a) + k" in spec) + apply (drule mp) + apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def field_simps of_nat_nat) + apply (erule notE) + apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) + apply (simp add: size_of_def) + apply (simp only: size_of_def mult_le_mono1) + apply (auto simp add: array_ptr_index_def intro: exI[where x=0]) + done + lemma h_t_valid_Array_element: "\ htd \\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 \ n; n < int CARD('b) \ \ htd \\<^sub>t ((ptr_coerce p :: 'a ptr) +\<^sub>p n)" - apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def - c_guard_def c_null_guard_def) - apply (clarsimp simp: size_td_array size_of_def typ_uinfo_t_def - typ_info_array array_tag_def) - apply (intro conjI) - apply clarsimp - apply (drule_tac x="nat n * size_of TYPE('a) + y" in spec) - apply (drule mp) - apply (rule_tac y="Suc (nat n) * size_of TYPE('a)" in order_less_le_trans) - apply (simp add: size_of_def) - apply (simp only: size_of_def mult_le_mono1) - apply (clarsimp simp: CTypesDefs.ptr_add_def field_simps of_nat_nat) - apply (erule map_le_trans[rotated]) - apply (rule list_map_mono) - apply (rule typ_slice_t_array[unfolded array_tag_def]) - apply simp + apply (drule_tac n="nat n" and coerce=False in h_t_valid_Array_element') + apply simp + apply (simp add: array_ptr_index_def) + done + +lemma ptr_safe_Array_element: + "\ ptr_safe (p :: (('a :: mem_type)['b :: finite]) ptr) htd; coerce \ n < CARD('b) \ + \ ptr_safe (array_ptr_index p coerce n) htd" + apply (simp add: ptr_safe_def) + apply (erule order_trans[rotated]) + apply (subgoal_tac "\offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs) + \ offs < CARD ('b)") + prefer 2 + apply (auto simp: array_ptr_index_def intro: exI[where x=0])[1] + apply (clarsimp simp: s_footprint_def s_footprint_untyped_def + CTypesDefs.ptr_add_def + size_td_array size_of_def) + apply (rule_tac x="offs * size_of TYPE('a) + x" in exI) + apply (simp add: size_of_def) + apply (rule conjI) + apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) apply (simp add: size_of_def) - apply (simp add: ptr_aligned_def align_of_def align_td_array - CTypesDefs.ptr_add_def unat_word_ariths unat_of_nat) - using align_size_of[where 'a='a] align[where 'a='a] - apply (simp add: align_of_def size_of_def addr_card_def card_word) - apply (simp add: dvd_mod dvd_add dvd_mult) - apply (thin_tac "\x. ?P x") - apply (clarsimp simp: intvl_def) - apply (drule_tac x="nat n * size_of TYPE('a) + k" in spec) - apply (drule mp) - apply (simp add: CTypesDefs.ptr_add_def field_simps of_nat_nat) - apply (erule notE) - apply (rule_tac y="Suc (nat n) * size_of TYPE('a)" in order_less_le_trans) + apply (simp only: size_of_def) + apply (rule mult_le_mono1) + apply simp + apply (thin_tac "coerce \ ?P") + apply (elim disjE exE conjE, simp_all add: typ_uinfo_t_def) + apply (erule order_less_le_trans) + apply (rule prefix_length_le) + apply (rule order_trans, erule typ_slice_t_array) apply (simp add: size_of_def) - apply (simp only: size_of_def mult_le_mono1) + apply (simp add: size_of_def field_simps typ_info_array) done lemma from_bytes_eq: diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy index 3f2170d2d..e15f43c0b 100644 --- a/proof/asmrefine/SEL4GlobalsSwap.thy +++ b/proof/asmrefine/SEL4GlobalsSwap.thy @@ -129,13 +129,99 @@ lemma unat_ucast_less_helper: "ucast (x :: word8) < (of_nat m :: word32) \ unat x < m" by (simp add: unat_ucast_8_32[symmetric] unat_less_helper) -lemmas globals_list_mems = kernel_all_global_addresses.global_data_mems +lemma globals_list_distinct_filter_member: + "x \ set xs \ globals_list_distinct D symtab xs + \ \ P x + \ globals_list_distinct (global_data_region symtab x) symtab + (filter P xs)" + apply (clarsimp simp: globals_list_distinct_def) + apply (rule conjI) + apply (clarsimp simp: in_set_conv_decomp[where x="x"] + distinct_prop_append) + apply auto[1] + apply (simp add: distinct_prop_map distinct_prop_filter) + apply (erule distinct_prop_weaken, simp) + done + +lemma s_footprint_intvl: + "s_footprint (p :: 'a ptr) \ {ptr_val p ..+ size_of TYPE ('a :: c_type)} \ UNIV" + by (auto simp: s_footprint_def s_footprint_untyped_def + intvl_def size_of_def) + +lemma h_val_globals_swap_in_const_global: + "\ global_acc_valid g_hrs g_hrs_upd; + globals_list_distinct D symtab xs; + const_global_data s (v :: 'a :: c_type) \ set xs; + unat offs + size_of TYPE('b) \ size_of TYPE('a) \ + \ h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) + (Ptr (symtab s + offs) :: ('b :: c_type) ptr) + = h_val (hrs_mem (g_hrs gs)) (Ptr (symtab s + offs))" + apply (erule disjoint_h_val_globals_swap_filter, + erule(1) globals_list_distinct_filter_member) + apply simp + apply (rule order_trans, rule s_footprint_intvl) + apply (simp add: global_data_region_def const_global_data_def + Times_subset_cancel2) + apply (erule intvl_sub_offset) + done + +lemmas h_val_globals_swap_in_const_global_both + = h_val_globals_swap_in_const_global + h_val_globals_swap_in_const_global[where offs=0, simplified] + +lemma const_globals_in_memory_to_h_val_with_swap: + "\ global_acc_valid g_hrs g_hrs_upd; + globals_list_distinct D symtab xs; + const_global_data nm v \ set xs; + const_globals_in_memory symtab xs (hrs_mem (g_hrs gs)) \ + \ v = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) + (Ptr (symtab nm))" + apply (subst disjoint_h_val_globals_swap_filter, assumption, + erule(1) globals_list_distinct_filter_member) + apply simp + apply (simp add: global_data_region_def const_global_data_def) + apply (rule order_trans, rule s_footprint_intvl) + apply simp + apply (erule(1) const_globals_in_memory_h_val[symmetric]) + done ML {* -val globals_swap_rewrites = @{thms globals_list_mems[unfolded global_data_defs]} - RL @{thms - globals_swap_update_mem2[OF _ global_acc_valid globals_list_valid] - globals_swap_access_mem2[OF _ global_acc_valid globals_list_valid]} +fun add_globals_swap_rewrites member_thms ctxt = let + val gav = Proof_Context.get_thm ctxt "global_acc_valid" + val glv = Proof_Context.get_thm ctxt "globals_list_valid" + val gld = Proof_Context.get_thm ctxt "globals_list_distinct" + val acc = [Thm.trivial @{cpat "PROP ?P"}, gav, glv, gld] + MRS @{thm globals_swap_access_mem2} + val upd = [Thm.trivial @{cpat "PROP ?P"}, gav, glv, gld] + MRS @{thm globals_swap_update_mem2} + val cg_with_swap = [gav, gld] + MRS @{thm const_globals_in_memory_to_h_val_with_swap} + val empty_ctxt = put_simpset HOL_basic_ss ctxt + fun unfold_mem thm = let + val (x, _) = HOLogic.dest_mem (HOLogic.dest_Trueprop (concl_of thm)) + val (s, _) = dest_Const (head_of x) + in if s = @{const_name global_data} orelse s = @{const_name const_global_data} + orelse s = @{const_name addressed_global_data} + then thm + else simplify (empty_ctxt addsimps [Proof_Context.get_thm ctxt (s ^ "_def")]) thm + end + + val member_thms = map unfold_mem member_thms + + val globals_swap_rewrites = member_thms RL [acc, upd] + val const_globals_rewrites = member_thms RL @{thms const_globals_in_memory_h_val[symmetric]} + val const_globals_swap_rewrites = member_thms RL [cg_with_swap] + in ctxt + |> Local_Theory.note ((@{binding "globals_swap_rewrites"}, []), + globals_swap_rewrites) + |> snd + |> Local_Theory.note ((@{binding "const_globals_rewrites"}, []), + const_globals_rewrites) + |> snd + |> Local_Theory.note ((@{binding "const_globals_rewrites_with_swap"}, []), + const_globals_swap_rewrites) + |> snd + end *} end diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index c1664c3a3..c230661e2 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -10,8 +10,7 @@ theory SEL4GraphRefine -imports "../../tools/asmrefine/GraphRefine" - "../../tools/asmrefine/FieldAccessors" +imports "../../tools/asmrefine/ProveGraphRefine" "../../spec/cspec/Substitute" "SEL4GlobalsSwap" @@ -19,8 +18,6 @@ begin ML {* Toplevel.debug := true *} -thm take_heap_list_min - ML {* val funs = ParseGraph.funs @{theory} "CFunDump.txt" *} @@ -32,6 +29,12 @@ fun define_all funs = fold (fn s => let val s' = Long_Name.base_name s (Symtab.dest funs |> filter (fn (_, v) => #3 v <> NONE) |> map fst) *} +ML {* +val csenv = let + val the_csenv = CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the + in fn () => the_csenv end +*} + consts encode_machine_state :: "machine_state \ unit \ nat" @@ -47,15 +50,15 @@ lemma eq_impl_at_addrI: local_setup {* add_field_h_val_rewrites #> add_field_to_bytes_rewrites *} -ML {* val nm = "Kernel_C.getSyscallArg" *} - -locale graph_refine = kernel_all_substitute +locale graph_refine_locale = kernel_all_substitute + assumes globals_list_distinct: "globals_list_distinct domain symbol_table globals_list" assumes halt_halts: "\ft. (\s xs. (\ \ \com.Call halt_'proc, Normal s\ \ xs) = (xs = Fault ft))" begin +local_setup {* add_globals_swap_rewrites @{thms kernel_all_global_addresses.global_data_mems} *} + definition simpl_invariant :: "globals myvars set" where @@ -63,84 +66,113 @@ where (hrs_mem (t_hrs_' (globals s))) \ htd_safe domain (hrs_htd (t_hrs_' (globals s)))}" +ML {* ProveSimplToGraphGoals.test_afll_graph_refine_proofs_after + funs (csenv ()) [] @{context} (SOME "Kernel_C.makeUserPDE") *} + +ML {* val nm = "Kernel_C.makeUserPDE" *} + local_setup {* define_graph_fun_short funs nm *} -ML {* UseHints.globals_swap +ML {* SimplToGraphProof.globals_swap := (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t) *} ML {* -val hints = UseHints.mk_var_deps_hints funs @{context} @{typ "globals myvars"} nm -*} - -ML {* init_graph_refines_proof funs nm @{context} *} - -ML {* - -val global_data_mems = @{thms kernel_all_global_addresses.global_data_mems[ - unfolded global_data_defs]} - -val pglobal_valids = (* -(global_data_mems RL - @{thms ptr_inverse_safe_htd_safe_global_data[OF globals_list_distinct] - ptr_inverse_safe_htd_safe_const_global_data[OF globals_list_distinct]}) - |> map (full_simplify (HOL_basic_ss addsimps @{thms symbols_in_table_simps - pglobal_valid_fold c_guard_to_word_ineq})) - |> map (full_simplify (@{simpset} addsimps @{thms align_td_array' mask_def})) -*) [] - -val globals_swap_rewrites2 - = @{thms globals_list_distinct} RL globals_swap_rewrites - +val hints = SimplToGraphProof.mk_hints funs @{context} nm *} ML {* -mk_graph_refines_proof funs [] hints globals_swap_rewrites2 nm - (@{context} addsimps @{thms simpl_invariant_def}) +val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs [@{thm halt_halts}] hints nm + @{context} *} -lemma store_word32s_equality_refl: - "store_word32s_equality addr xs xs hp hp" - by (simp add: store_word32s_equality_def) +ML {* +ProveSimplToGraphGoals.simpl_to_graph_thm funs (csenv ()) [@{thm halt_halts}] @{context} nm; +*} + + +ML {* +val tacs = ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ()) + #> map snd +val full_tac = ProveSimplToGraphGoals.graph_refine_proof_full_tac + (csenv ()) +val full_goal_tac = ProveSimplToGraphGoals.graph_refine_proof_full_goal_tac + (csenv ()) +*} schematic_lemma "PROP ?P" - apply (tactic {* rtac it 1 *}) - apply (tactic {* full_simpl_to_graph_tac funs [] hints nm @{context} *}) - apply (tactic {* ALLGOALS (TRY o rtac @{thm eq_impl_at_addrI}) *}) - apply (tactic {* ALLGOALS (simp_tac ((put_simpset HOL_basic_ss @{context}) - addsimps @{thms mex_def meq_def simpl_invariant_def})) *}) + apply (tactic {* rtac init_thm 1 *}) + + + apply (tactic {* ALLGOALS (TRY o (full_goal_tac @{context} THEN_ALL_NEW K no_tac)) *}) + +(* apply (tactic {* ALLGOALS (TRY o rtac @{thm eq_impl_at_addrI}) *}) *) + + apply (tactic {* ALLGOALS (nth (tacs @{context}) 0) *}) +apply simp + apply (tactic {* ALLGOALS (nth (tacs @{context}) 1) *}) + apply (tactic {* ALLGOALS (nth (tacs @{context}) 2) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 0) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 1) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 2) *}) + apply (tactic {* full_tac @{context} *}) - apply (tactic {* ALLGOALS (simp_tac (@{context} addsimps @{thms - hrs_mem_update - hrs_htd_globals_swap mex_def meq_def} - addsimps globals_swap_rewrites2)) *}) + apply (simp_all add: word_sle_def[THEN arg_cong[where f=Not], THEN iffD2]) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 3) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 4) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 5) *}) - apply (tactic {* ALLGOALS (nth (graph_refine_proof_tacs @{context}) 6) *}) +defer + + apply (tactic {* full_tac @{context} *})[2] + +ML_val {* nth (ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ()) @{context}) 3 *} + + apply (tactic {* (nth (tacs @{contfext}) 3) 1 *}) - apply (simp_all add: field_h_val_rewrites field_to_bytes_rewrites heap_update_def - to_bytes_array upt_rec take_heap_list_min drop_heap_list_general - heap_update_list_append heap_list_update_ptr heap_list_update_word32 - store_store_word32_commute_offset field_simps - heap_access_Array_element h_val_word32 h_val_ptr - field_lvalue_offset_eq ucast_eq_0s) + apply (tactic {* ProveSimplToGraphGoals.decompose_graph_refine_memory_problems false + (@{context} |> Splitter.del_split @{thm split_if} + (* |> Simplifier.del_cong @{thm if_weak_cong} *)) 1 *})[1] - apply (tactic {* simp_tac (@{context} addsimps @{thms store_word32s_equality_fold store_word32s_equality_final add_commute} - ) |>ALLGOALS *}) + apply (tactic {* full_tac @{context} *})[1] - apply (tactic {* simp_tac (@{context} addsimprocs [store_word32s_equality_simproc] - addsimps @{thms store_word32s_equality_final add_commute} - ) |>ALLGOALS *}) + apply (rule sym, tactic {* ProveSimplToGraphGoals.clean_heap_upd_swap @{context} 1 *}) + + apply (tactic {* ProveSimplToGraphGoals.prove_mem_equality @{context} 1 *}) + + apply (simp add: heap_update_def to_bytes_array + heap_update_list_append heap_list_update_ptr heap_list_update_word32 + field_lvalue_offset_eq ptr_add_def + array_ptr_index_def + h_val_word32 h_val_ptr + upt_rec take_heap_list_min drop_heap_list_general + field_to_bytes_rewrites) + + apply (rule double_heap_update_eq[symmetric]) + +thm cteInsert_body_def + + + apply (tafctic {* ALLGOALS (nth (tacs @{context}) 3) *})[1] + + apply (tactic {* ALLGOALS (nth (tacs @{context}) 4) *}) + + apply (tactic {* ALLGOALS (nth (tacs @{context}) 5) *}) + + apply (tactic {* ALLGOALS (nth (tacs @{context}) 6) *}) + + apply (simp_all add: h_val_ptr h_val_word32) +using [[show_consts]] + +term "drop_sign x" +using [[show_types]] +thm drop_sign_isomorphism_bitwise(10)[where 'a=32] +using [[simp_trace]] +apply (tactic {* ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss @{context} + addsimps @{thms drop_sign_isomorphism_bitwise(10)})) *}) + + + apply (tactifc {* ALLGOALS (nth (tacs @{context}) 7) *}) + +done - done end diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 3f5caf26d..887e4c35e 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -3393,7 +3393,10 @@ lemma cur_domain_reads: "(s,s') \ uwr u \ is_domain initial_ prefer 2 apply simp apply (simp add: reads_scheduler_def)+ - apply (clarsimp simp add: uwr_def sameFor_def sameFor_subject_def) + apply (simp add: uwr_def sameFor_def sameFor_subject_def) + apply clarify + apply (simp(no_asm_use)) + apply simp done lemmas domain_can_read_context = cur_domain_reads[THEN conjunct1] diff --git a/tools/asmrefine/FieldAccessors.thy b/tools/asmrefine/FieldAccessors.thy index 07d1a5e24..d14297dff 100644 --- a/tools/asmrefine/FieldAccessors.thy +++ b/tools/asmrefine/FieldAccessors.thy @@ -235,13 +235,27 @@ lemma drop_heap_list_general: apply (simp_all add: drop_heap_list_le) done +lemma heap_update_mono_to_field_rewrite: + "\ field_lookup (typ_info_t TYPE('a)) [s] 0 + \ field_lookup (adjust_ti (typ_info_t TYPE('b)) f upds) [] n; + export_uinfo (adjust_ti (typ_info_t TYPE('b)) f upds) + = export_uinfo (typ_info_t TYPE('b)); + align_of TYPE('a) + size_of TYPE('a) < 2 ^ 32; align_of TYPE('a) \ 0 \ + \ heap_update (p::'a::packed_type ptr) + (update_ti_t (adjust_ti (typ_info_t TYPE('b)) f upds) (to_bytes_p v) + str) hp + = heap_update (Ptr (&(p\[s]))::'b::packed_type ptr) v (heap_update p str hp)" + by (simp add: typ_uinfo_t_def heap_update_field2 + packed_heap_update_collapse h_val_heap_update + field_ti_def update_ti_t_def size_of_def) + ML {* fun get_field_h_val_rewrites lthy = (simpset_of lthy |> dest_ss |> #simps |> map snd |> map (Thm.transfer (Proof_Context.theory_of lthy)) RL @{thms h_val_mono_to_field_rewrite - (* heap_update_mono_to_field_rewrite - [unfolded align_of_def size_of_def] *) }) + heap_update_mono_to_field_rewrite + [unfolded align_of_def size_of_def] }) |> map (asm_full_simplify lthy); fun add_field_h_val_rewrites lthy = diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index 58851dd50..4caa4ee22 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -11,7 +11,6 @@ theory GraphRefine imports TailrecPre GraphLangLemmas "../../lib/LemmaBucket_C" - FieldAccessors begin @@ -596,13 +595,13 @@ lemma simpl_to_graph_While_lemma: done lemma simpl_to_graph_While_UNIV: - assumes ps: "GGamma f = Some gf" "nn = NextNode m" "function_graph gf m = Some (Cond l r cond)" + assumes ps: "nn = NextNode m" "GGamma f = Some gf" "function_graph gf m = Some (Cond l r cond)" "eq_impl nn eqs (\gst sst. cond gst = (sst \ C)) I" - assumes ss: "\k S. \ simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) UNIV I eqs out_eqs \ - \ simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) C I eqs2 out_eqs" and ss_eq: "eq_impl nn eqs eqs2 (I \ C)" - assumes ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (- C) I eqs3 out_eqs" + and ss: "\k S. \ simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) UNIV I eqs out_eqs \ + \ simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) C I eqs2 out_eqs" and ex_eq: "eq_impl nn eqs eqs3 (I \ - C)" + and ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (- C) I eqs3 out_eqs" shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS P I eqs out_eqs" apply (rule simpl_to_graph_weaken) apply (rule simpl_to_graph_While_lemma[where P=UNIV], (rule ps)+) @@ -618,13 +617,13 @@ lemma simpl_to_graph_While_UNIV: lemma simpl_to_graph_While_Guard: fixes c' F G defines "c == c' ;; com.Guard F G com.Skip" - assumes ps: "GGamma f = Some gf" "nn = NextNode m" "function_graph gf m = Some (Cond l r cond)" + assumes ps: "nn = NextNode m" "GGamma f = Some gf" "function_graph gf m = Some (Cond l r cond)" "eq_impl nn eqs (\gst sst. cond gst = (sst \ C)) (I \ G)" - assumes ss: "\k S. \ simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \ - \ simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (G \ C) I eqs2 out_eqs" and ss_eq: "eq_impl nn eqs eqs2 (I \ G \ C)" - assumes ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \ (- C)) I eqs3 out_eqs" + and ss: "\k S. \ simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \ + \ simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (G \ C) I eqs2 out_eqs" and ex_eq: "eq_impl nn eqs eqs3 (I \ G \ - C)" + and ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \ (- C)) I eqs3 out_eqs" and in_eq: "eq_impl nn eqs (\gst sst. sst \ G) (I \ G')" shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS G' I eqs out_eqs" apply (rule simpl_to_graph_weaken) @@ -846,15 +845,23 @@ lemma simpl_to_graph_done2: "simpl_to_graph SGamma GGamma gf Ret (add_cont com.Skip []) n Q P I eqs eqs" by (auto intro: simpl_to_graph_done simp: eq_impl_def) +lemma simpl_to_graph_noop_Basic: + "\ GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds); + eq_impl nn eqs (\gst sst. eqs2 (upd_vars upds gst) sst) (P \ I); + simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs \ + \ simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs" + apply (rule simpl_to_graph_step_general[where i=1 and j=0, rotated]) + apply simp+ + apply (simp add: exec_graph_step_image_node eq_impl_def K_def) + done + lemma simpl_to_graph_noop: "\ GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn []); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs; eq_impl nn eqs eqs2 (P \ I) \ \ simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs" - apply (rule simpl_to_graph_step_general[where i=1 and j=0, rotated]) - apply simp+ - apply (simp add: exec_graph_step_image_node upd_vars_def save_vals_def K_def - eq_impl_def) + apply (erule(1) simpl_to_graph_noop_Basic, simp_all) + apply (simp add: upd_vars_def save_vals_def eq_impl_def) done lemmas simpl_to_graph_nearly_done @@ -1065,7 +1072,7 @@ lemma simpl_to_graph_call_next_step: ((exec_graph_step GGamma) ^^ steps) `` {[(nn', gst', p)]} \ {[(nn'', f gst', p)]} \ steps < 2 \ (steps = 0 \ nn' \ {Ret, Err})" and rel: "graph_fun_refines SGamma GGamma I inputs proc outputs p'" - and modifies: "\\. SGamma \\<^bsub>/UNIV\<^esub> {\} com.Call proc (Q \)" + and modifies: "(\\. SGamma \\<^bsub>/UNIV\<^esub> {\} com.Call proc (Q \)) \ (Q = (\_. UNIV))" and init: "eq_impl nn eqs (\gst sst. initf sst \ I \ map (\i. i gst) args = map (\i. i (initf sst)) inputs) (I \ P)" and ret: "eq_impl nn eqs (\gst sst. \sst' vs. map (\i. i sst') outputs = vs @@ -1132,10 +1139,12 @@ lemma simpl_to_graph_call_next_step: apply (drule ret[THEN eq_implD], simp) apply (simp only: conj_assoc[symmetric], rule conjI[rotated], assumption) apply (simp add: return_vars_def conj_ac) - apply (frule cvalidD[OF hoare_sound, OF modifies[THEN spec], rotated], - simp, clarsimp, simp) + apply (rule disjE[OF modifies]) + apply (drule spec, drule cvalidD[OF hoare_sound], simp+) + apply clarsimp + apply auto[1] apply clarsimp - apply auto[1] + apply metis apply (metis restrict_map_eq_mono[OF le_add1]) done @@ -1564,30 +1573,7 @@ val store_word32s_equality_simproc = Simplifier.simproc_global_i ML {* -structure UseHints = struct - -fun parse_compile_hints fname = let - val f = TextIO.openIn fname - val parse_int = ParseGraph.parse_int - fun get () = case TextIO.inputLine f - of NONE => [] - | SOME s => unsuffix "\n" s :: get () - fun group hs (["Hints", s] :: sss) - = (s, hs) :: group [] sss - | group hs (ss :: sss) = group (ss :: hs) sss - | group _ [] = [] - val groups = group [] (rev (map (Library.space_explode " ") (get ()))) - fun proc_var_deps [] = [] - | proc_var_deps (nm :: ss) = let - val (typ, ss) = ParseGraph.parse_typ ss - in ((nm, typ) :: proc_var_deps ss) end - fun proc ("VarDeps" :: n :: ss) - = ((parse_int n, proc_var_deps ss)) - | proc ss = error (String.concat ("parse_compile_hints: " :: ss)) - fun proc_group hs = let - val vds = map proc hs - in Inttab.make vds end - in Symtab.make (map (apsnd proc_group) groups) end +structure SimplToGraphProof = struct fun mk_ptr_val_app p = Const (@{const_name ptr_val}, fastype_of p --> @{typ word32}) $ p @@ -1646,8 +1632,11 @@ fun mk_simpl_acc ctxt sT nm = let fun foldr1_default _ v [] = v | foldr1_default f _ xs = foldr1 f xs -fun mk_graph_eqs Gamma deps nm n = let - val vs = case (Inttab.lookup deps n) of +datatype hints = Hints of { deps: (string * term) list Inttab.table, + loop_basics: thm list } + +fun mk_graph_eqs Gamma (Hints hints) nm n = let + val vs = case (Inttab.lookup (#deps hints) n) of SOME vs => vs | NONE => raise TERM ("mk_graph_eqs: " ^ nm ^ " " ^ string_of_int n, []) val sT = gammaT_to_stateT (fastype_of Gamma) @@ -1770,8 +1759,9 @@ fun apply_modifies_thm ctxt = SUBGOAL (fn (t, i) => case get_Call_args (Envir.beta_eta_contract t) of [Const (s, _)] => let val s = unsuffix "_'proc" (Long_Name.base_name s) - val thm = Proof_Context.get_thm ctxt (s ^ "_modifies") - in rtac thm i end + val thms = (@{thm disjI1}, Proof_Context.get_thm ctxt (s ^ "_modifies")) + handle ERROR _ => (@{thm disjI2}, @{thm refl}) + in rtac (fst thms) i THEN rtac (snd thms) i end | _ => no_tac) fun is_safe_eq_impl (p as (@{term Trueprop} @@ -1808,7 +1798,7 @@ fun simpl_ss ctxt = put_simpset HOL_basic_ss ctxt val immediates = @{thms simpl_to_graph_Skip_immediate simpl_to_graph_Throw_immediate} -fun apply_simpl_to_graph_tac funs noreturns ctxt nm = +fun apply_simpl_to_graph_tac funs (Hints hints) noreturns ctxt = simp_tac (simpl_ss ctxt addsimps @{thms One_nat_def whileAnno_def creturn_def[folded creturn_void_def]}) @@ -1843,6 +1833,8 @@ fun apply_simpl_to_graph_tac funs noreturns ctxt nm = THEN' apply_graph_refines_ex_tac funs ctxt THEN' apply_modifies_thm ctxt, rtac @{thm simpl_to_graph_nearly_done} + THEN' inst_graph_tac ctxt, + resolve_tac (#loop_basics hints) THEN' inst_graph_tac ctxt ] THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (resolve_tac immediates))) @@ -1868,7 +1860,7 @@ and mk_simpl_to_graph_thm funs noreturns hints cache nm ctxt tm = let val thy = Proof_Context.theory_of ctxt val ct = cterm_of thy (HOLogic.mk_Trueprop tm) in Thm.trivial ct - |> (apply_simpl_to_graph_tac funs noreturns ctxt nm + |> (apply_simpl_to_graph_tac funs hints noreturns ctxt THEN_ALL_NEW (TRY o simpl_to_graph_cache_tac funs noreturns hints cache nm ctxt) THEN_ALL_NEW (TRY o eq_impl_assume_tac ctxt)) 1 |> Seq.hd @@ -1880,11 +1872,17 @@ and mk_simpl_to_graph_thm funs noreturns hints cache nm ctxt tm = let NONE) | Option => NONE +fun dest_next_node (@{term NextNode} $ n) + = dest_nat n + | dest_next_node @{term Ret} = ~1 + | dest_next_node @{term Err} = ~2 + | dest_next_node t = raise TERM ("dest_next_node", [t]) + fun get_while (Const (@{const_name simpl_to_graph}, _) - $ _ $ _ $ _ $ _ + $ _ $ _ $ _ $ nn $ (Const (@{const_name add_cont}, _) $ (Const (@{const_name While}, _) $ C $ c) $ _) $ _ $ _ $ _ $ _ $ _ $ _) - = (C, c) + = (dest_next_node nn, C, c) | get_while t = raise TERM ("get_while", [t]) fun check_while_assums t = let @@ -1904,43 +1902,41 @@ fun simpl_to_graph_While_tac hints nm ctxt = val thy = Proof_Context.theory_of ctxt val ct = cterm_of thy (HOLogic.mk_Trueprop skel) in - rtac (Thm.trivial ct |> Drule.generalize ([], ["n"])) i + rtac (Thm.trivial ct |> Drule.generalize ([], ["n", "trS"])) i THEN resolve_tac @{thms simpl_to_graph_While_Guard[OF refl] simpl_to_graph_While_UNIV[OF refl]} i THEN inst_graph_tac ctxt i end handle TERM _ => no_tac) -fun trace_fail_tac ctxt = SUBGOAL (fn (t, i) => +fun trace_fail_tac ctxt s = SUBGOAL (fn (t, _) => (Syntax.pretty_term ctxt t |> Pretty.string_of - |> prefix "Tactic failed on: " |> tracing; + |> prefix ("Tactic " ^ s ^ " failed on: ") |> tracing; no_tac)) -fun trace_fail_tac2 ctxt = K no_tac +fun trace_fail_tac2 _ = K no_tac fun simpl_to_graph_tac funs noreturns hints nm ctxt = let val cache = ref (Termtab.empty) in REPEAT_ALL_NEW (DETERM o (full_simp_tac (simpl_ss ctxt) THEN' SUBGOAL (fn (t, i) => fn thm => ((simpl_to_graph_cache_tac funs noreturns hints cache nm ctxt - ORELSE' etac @{thm use_simpl_to_graph_While_assum} + ORELSE' (etac @{thm use_simpl_to_graph_While_assum} + THEN' simp_tac ctxt) ORELSE' simpl_to_graph_While_tac hints nm ctxt - ORELSE' trace_fail_tac ctxt) i thm + ORELSE' trace_fail_tac ctxt "simpl_to_graph_tac") i thm handle Empty => (tracing "simpl_to_graph_tac: raised Empty on:"; tracing (Syntax.pretty_term ctxt t |> Pretty.string_of); Seq.empty))) )) end -fun dest_next_node (@{term NextNode} $ n) - = dest_nat n - | dest_next_node @{term Ret} = ~1 - | dest_next_node @{term Err} = ~2 - | dest_next_node t = raise TERM ("dest_next_node", [t]) - -fun get_conts (@{term node.Basic} $ nn $ _) = [nn] - | get_conts (@{term node.Cond} $ l $ r $ _) = [l, r] - | get_conts (@{term node.Call} $ nn $ _ $ _ $ _) = [nn] - | get_conts n = raise TERM ("get_conts", [n]) +fun get_conts norets (@{term node.Basic} $ nn $ _) = [nn] + | get_conts norets (@{term node.Cond} $ l $ _ $ Abs (_, _, @{term True})) = [l] + | get_conts norets (@{term node.Cond} $ _ $ r $ Abs (_, _, @{term False})) = [r] + | get_conts norets (@{term node.Cond} $ l $ r $ _) = [l, r] + | get_conts norets (@{term node.Call} $ nn $ s $ _ $ _) + = if member (op =) norets (HOLogic.dest_string s) then [] else [nn] + | get_conts norets n = raise TERM ("get_conts", [n]) fun get_rvals (Abs (_, _, t)) = let fun inner (Const _ $ (s as (@{term "op # :: char \ _"} $ _ $ _)) $ Bound 0) @@ -1963,12 +1959,12 @@ fun get_lvals_rvals (@{term node.Basic} $ _ $ upds) = let HOLogic.dest_list args |> maps get_rvals) | get_lvals_rvals n = raise TERM ("get_conts", [n]) -fun get_var_deps nodes ep outputs = let +fun get_var_deps norets nodes ep outputs = let fun forward tab (point :: points) = if point < 0 then forward tab points else let val node = Inttab.lookup nodes point |> the - val conts = map dest_next_node (get_conts node) + val conts = map dest_next_node (get_conts norets node) val upds = filter_out (Inttab.lookup_list tab #> flip (Ord_List.member int_ord) point) conts val tab = fold (fn c => Inttab.map_default (c, []) @@ -1978,16 +1974,16 @@ fun get_var_deps nodes ep outputs = let val preds = forward (Inttab.make [(ep, [])]) [ep] fun backward tab (point :: points) = let val node = Inttab.lookup nodes point |> the - val conts = map dest_next_node (get_conts node) + val conts = map dest_next_node (get_conts norets node) val (lvs, rvs) = get_lvals_rvals node |> pairself (Ord_List.make string_ord) val cont_vars = maps (Inttab.lookup_list tab) conts |> Ord_List.make string_ord val vars = Ord_List.merge string_ord (rvs, Ord_List.subtract string_ord lvs cont_vars) - val prev_vars = Inttab.lookup_list tab point + val prev_vars = Inttab.lookup tab point val tab = Inttab.update (point, vars) tab - val upds = if prev_vars <> vars + val upds = if prev_vars <> SOME vars then Inttab.lookup_list preds point else [] in backward tab (upds @ points) end | backward tab [] = tab @@ -1995,57 +1991,40 @@ fun get_var_deps nodes ep outputs = let (maps (Inttab.lookup_list preds) [~1, ~2]) in (preds, deps) end -fun mk_var_deps_hints (funs : ParseGraph.funs) ctxt sT nm = case Symtab.lookup funs nm of - NONE => raise TERM ("mk_var_deps_hints: miss " ^ nm, []) - | SOME (_, _, NONE) => Inttab.empty - | SOME (_, outputs, SOME (ep, nodes, _)) => let - in snd (get_var_deps (Inttab.make nodes) ep outputs) - |> Inttab.map (fn _ => map (fn s => (s, mk_simpl_acc ctxt sT s))) end +fun get_loop_var_upd_nodes nodes = + nodes + |> filter (snd #> (fn (@{term Basic} $ _ $ _) => true | _ => false)) + |> filter (snd #> get_lvals_rvals #> fst + #> (fn xs => not (null xs) andalso forall (String.isSuffix "#count") xs)) + |> map fst -end - -*} - -ML {* -fun define_graph_fun_short funs s - = ParseGraph.define_graph_fun funs (Long_Name.base_name s ^ "_graph") - (Binding.name (Long_Name.base_name s ^ "_graph_fun")) s - #> Local_Theory.restore -*} - -ML {* -open UseHints - -fun enum_simps ctxt = let - val csenv = CalculateState.get_csenv - (Proof_Context.theory_of ctxt) "c/kernel_all.c_pp" |> the - val Absyn.CE ecenv = ProgramAnalysis.cse2ecenv csenv; - in - #enumenv ecenv |> Symtab.dest - |> map (Proof_Context.get_thm ctxt o suffix "_def" o fst) +fun mk_loop_var_upd_thm ctxt n = let + val thy = Proof_Context.theory_of ctxt + val n_c = HOLogic.mk_number @{typ nat} n + |> cterm_of thy + in @{thm simpl_to_graph_noop_Basic} + |> cterm_instantiate [(@{cpat "?m :: nat"}, n_c)] + |> simplify (simpl_ss ctxt addsimps @{thms One_nat_def}) end -(* -val global_data_mems = @{thms kernel_all_global_addresses.global_data_mems[ - unfolded global_data_defs]} +fun noreturn_thms_call_names noreturn_thms = [] -val const_global_simps = global_data_mems - RL [@{thm const_globals_in_memory_h_val_swap}] - -val pglobal_valids = (global_data_mems RL - @{thms ptr_inverse_safe_htd_safe_global_data[OF globals_list_distinct] - ptr_inverse_safe_htd_safe_const_global_data[OF globals_list_distinct]}) - |> map (full_simplify (HOL_basic_ss addsimps @{thms symbols_in_table_simps - pglobal_valid_fold c_guard_to_word_ineq})) - |> map (full_simplify (@{simpset} addsimps @{thms align_td_array' mask_def})) - -val globals_swap_rewrites2 - = @{thms globals_list_distinct} RL globals_swap_rewrites -*) - -val thin_While_assums_rule = - @{thm thin_rl[where V="simpl_to_graph SG GG f nn (add_cont (com.While C c) con) n tS P I e e2"]} - |> Drule.generalize ([], ["SG", "GG", "f", "nn", "C", "c", "con", "n", "tS", "P", "I", "e", "e2"]) +fun mk_hints (funs : ParseGraph.funs) noreturns ctxt nm = case Symtab.lookup funs nm of + NONE => raise TERM ("mk_var_deps_hints: miss " ^ nm, []) + | SOME (_, _, NONE) => Hints {deps = Inttab.empty, loop_basics = []} + | SOME (_, outputs, SOME (ep, nodes, _)) => let + val norets = noreturn_thms_call_names noreturns + val sT = Syntax.read_typ ctxt "globals myvars" + val deps = snd (get_var_deps norets (Inttab.make nodes) ep outputs) + val deps_hints = nodes + |> map (fst #> ` (Inttab.lookup_list deps + #> filter_out (fn s => String.isSuffix "#count" s) + #> map (fn s => (s, mk_simpl_acc ctxt sT s)))) + |> map swap |> Inttab.make + val loop_thms = get_loop_var_upd_nodes nodes + |> map (mk_loop_var_upd_thm ctxt) + in Hints {deps = deps_hints, + loop_basics = loop_thms} end fun init_graph_refines_proof funs nm ctxt = let val thy = Proof_Context.theory_of ctxt @@ -2065,109 +2044,32 @@ fun init_graph_refines_proof funs nm ctxt = let |> Seq.hd end +val thin_While_assums_rule = + @{thm thin_rl[where V="simpl_to_graph SG GG f nn (add_cont (com.While C c) con) n tS P I e e2"]} + |> Drule.generalize ([], ["SG", "GG", "f", "nn", "C", "c", "con", "n", "tS", "P", "I", "e", "e2"]) + fun eq_impl_unassume_tac t = let val hyps = t |> Thm.crep_thm |> #hyps |> filter (term_of #> is_safe_eq_impl) in (* tracing ("Restoring " ^ string_of_int (length hyps) ^ " hyps.") ; *) fold Thm.implies_intr hyps t |> Seq.single end -fun full_simpl_to_graph_tac funs noreturns hints nm ctxt = - UseHints.simpl_to_graph_tac funs noreturns hints nm ctxt 1 - THEN ALLGOALS (TRY o REPEAT_ALL_NEW (etac thin_While_assums_rule)) - THEN eq_impl_unassume_tac +fun simpl_to_graph_upto_subgoals funs noreturns hints nm ctxt = + init_graph_refines_proof funs nm ctxt + |> (simpl_to_graph_tac funs noreturns hints nm ctxt 1 + THEN ALLGOALS (TRY o REPEAT_ALL_NEW (etac thin_While_assums_rule)) + THEN eq_impl_unassume_tac + ) |> Seq.hd -fun safe_goal_tac ctxt = - REPEAT_ALL_NEW (DETERM o CHANGED o safe_steps_tac ctxt) +end -fun graph_refine_proof_tacs globals_swap_rewrites2 ctxt = [ - asm_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps @{thms - signed_arith_ineq_checks_to_eq_word32 - signed_arith_eq_checks_to_ord - signed_mult_eq_checks32_to_64}), - asm_simp_tac (ctxt addsimps @{thms eq_impl_def - var_word32_def var_word8_def var_mem_def - var_htd_def var_acc_var_upd - pvalid_def var_ms_def init_vars_def - return_vars_def upd_vars_def save_vals_def - mem_upd_def mem_acc_def hrs_mem_update - mex_def meq_def}), - TRY o safe_goal_tac ctxt, - asm_full_simp_tac (ctxt addsimps @{thms -(* h_t_valid_disjoint_globals_swap - ptr_safe_disjoint_globals_swap - h_t_valid_field hrs_mem_update - disjoint_h_val_globals_swap[OF global_acc_valid _ image_fst_cart_UNIV_subset] - disjoint_heap_update_globals_swap[OF global_acc_valid _ image_fst_cart_UNIV_subset] - globals_swap_hrs_htd_update[OF global_acc_valid globals_list_valid] - all_htd_updates_def globals_swap_ghost_state - globals_update_globals_swap_twice - globals_swap_twice hrs_htd_globals_swap hrs_htd_update - inj_eq[OF bij_is_inj[OF globals_swap_bij]] -*) - unat_less_helper word32_lt_bounds_reduce - palign_valid_def pweak_valid_def} - addsimps globals_swap_rewrites2 - (* addsimps const_global_simps - addsimps pglobal_valids *) ), -(* TRY o REPEAT_ALL_NEW - (etac @{thm const_globals_in_memory_heap_update_subset[rotated]} - ORELSE' (rtac @{thm const_globals_in_memory_heap_update[ - OF _ globals_list_distinct, rotated -1]} - THEN' atac) - ORELSE' (resolve_tac @{thms h_t_valid_field[rotated] ptr_safe_field[rotated]} - THEN' simp_tac @{simpset})), -*) - asm_full_simp_tac (ctxt addsimps @{thms - mem_upd_def hrs_mem_update heap_update_ptr - heap_update_word32 h_val_ptr h_val_word32 - field_lvalue_offset_eq NULL_ptr_val - (* field_h_val_rewrites *) heap_access_Array_element - heap_update_Array_element'[OF refl] - scast_id ucast_id word32_sint_1 - unat_less_helper word_of_int_hom_syms - unat_ucast_less_helper ucast_nat_def - word_sless_to_less word_sle_def[THEN iffD2] - word32_lt_bounds_reduce - CTypesDefs.ptr_add_def ptr_val_inj[symmetric] - (* heap_update_words_of_upd_eq words_of_simps *) - store_store_word32_commute_offset - store_load_word32 - h_t_valid_ptr_safe typ_uinfo_t_def - (* symbols_in_table_simps *) - fupdate_def - } - addsimps (enum_simps ctxt) - addsimprocs [Word_Bitwise_Tac.expand_upt_simproc] - delsimps @{thms ptr_val_inj}), - asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps @{thms word_neq_0_conv[symmetric]}), - asm_full_simp_tac (ctxt addsimps @{thms - typ_uinfo_t_def c_guard_to_word_ineq bvshl_def - bvlshr_def bvashr_def bv_clz_def scast_def mask_def - word_sle_def[THEN iffD2] word_sless_alt[THEN iffD2] - store_load_word32 - }), - asm_full_simp_tac (ctxt addsimps @{thms - to_bytes_array heap_update_def - upt_rec take_heap_list_min drop_heap_list_general - heap_update_list_append heap_list_update_ptr heap_list_update_word32 - store_store_word32_commute_offset field_simps - heap_access_Array_element h_val_word32 h_val_ptr - field_lvalue_offset_eq ucast_eq_0s} - addsimps (Proof_Context.get_thms ctxt "field_h_val_rewrites") - addsimps (Proof_Context.get_thms ctxt "field_to_bytes_rewrites") - ), - simp_tac (ctxt addsimps @{thms store_word32s_equality_fold - store_word32s_equality_final add_commute}), - simp_tac (ctxt addsimprocs [store_word32s_equality_simproc] - addsimps @{thms store_word32s_equality_final add_commute}) -] +*} -fun mk_graph_refines_proof funs noreturns hints globals_swap_rewrites s ctxt - = init_graph_refines_proof funs s ctxt - |> full_simpl_to_graph_tac funs noreturns hints s ctxt - |> Seq.hd - |> EVERY (map ALLGOALS (graph_refine_proof_tacs globals_swap_rewrites ctxt)) - |> Seq.hd +ML {* +fun define_graph_fun_short funs s + = ParseGraph.define_graph_fun funs (Long_Name.base_name s ^ "_graph") + (Binding.name (Long_Name.base_name s ^ "_graph_fun")) s + #> Local_Theory.restore *} end diff --git a/tools/asmrefine/ProveGraphRefine.thy b/tools/asmrefine/ProveGraphRefine.thy new file mode 100644 index 000000000..6c8366ee5 --- /dev/null +++ b/tools/asmrefine/ProveGraphRefine.thy @@ -0,0 +1,532 @@ +theory ProveGraphRefine + +imports GraphRefine + GlobalsSwap FieldAccessors + +begin + +lemma const_globals_in_memory_heap_updateE: + "\ globals_list_distinct D symtab gs; + const_globals_in_memory symtab gs hmem; + htd_safe D htd; + ptr_safe (p :: ('a :: wf_type) ptr) htd \ + \ const_globals_in_memory symtab gs (heap_update p val hmem)" + by (simp add: const_globals_in_memory_heap_update) + +lemma disjoint_h_val_globals_swap_insert: + "\ global_acc_valid g_hrs g_hrs_upd; + globals_list_distinct D symtab xs; + htd_safe D htd; + ptr_safe (p :: ('a :: wf_type) ptr) htd \ + \ h_val (hrs_mem (g_hrs (globals s))) p + = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (globals s)))) p" + (* the current apparatus produces goals where the Simpl-derived + h_vals are applied to a globals swap and the graph-derived + h_vals lack it. we thus *add* a globals swap since that is the + case where we can prove ptr_safe *) + apply (rule disjoint_h_val_globals_swap[symmetric], assumption+) + apply (clarsimp simp: ptr_safe_def htd_safe_def del: subsetI) + apply blast + done + +lemma disjoint_heap_update_globals_swap_rearranged: + "\ global_acc_valid g_hrs g_hrs_upd; + globals_list_distinct D symtab xs; + htd_safe D htd; + ptr_safe (p :: ('a :: wf_type) ptr) htd \ + \ hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update p v)) gs))) + = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)))" + apply (subst disjoint_heap_update_globals_swap[symmetric], assumption+) + apply (clarsimp simp: ptr_safe_def htd_safe_def del: subsetI) + apply blast + apply (simp add: global_acc_valid_def hrs_mem_update) + done + +lemma double_heap_update_eq: + "heap_update p' (h_val hp'' p') hp = hp + \ heap_update p v hp = hp' + \ (heap_update p v (heap_update p' (h_val hp'' p') hp)) = hp'" + by simp + +lemma h_t_valid_orig_and_ptr_safe: + "h_t_valid d g p \ h_t_valid d g p \ ptr_safe p d" + by (simp add: h_t_valid_ptr_safe) + +lemma array_ptr_index_coerce: + fixes p :: "(('a :: c_type)['b :: finite]) ptr" + shows "n < CARD ('b) + \ array_ptr_index p False n = array_ptr_index p True n" + by (simp add: array_ptr_index_def) + +lemma unat_mono_thms: + "unat (a + b :: ('a :: len) word) \ unat a + unat b" + "unat (a * b) \ unat a * unat b" + by (simp_all add: unat_word_ariths) + +lemma unat_mono_intro: + "unat a \ x \ x < b \ unat a < b" + "unat a \ x \ x \ b \ unat a \ b" + by simp_all + +lemma word_neq_0_conv_neg_conv: + "(\ 0 < (n :: ('a :: len) word)) = (n = 0)" + by (cases "n = 0", simp_all) + +definition + drop_sign :: "('a :: len) signed word \ 'a word" +where + "drop_sign = ucast" + +lemma sint_drop_sign_isomorphism: + "sint (drop_sign x) = sint x" + by (simp add: drop_sign_def word_sint_msb_eq uint_up_ucast is_up_def + source_size_def target_size_def word_size msb_ucast_eq) + +lemma drop_sign_isomorphism_ariths: + "(x = y) = (drop_sign x = drop_sign y)" + "(x < y) = (drop_sign x < drop_sign y)" + "(x \ y) = (drop_sign x \ drop_sign y)" + "(x Seq.empty + | SOME (t'', _) => Seq.single (Goal.unrestrict i t'') + end + +fun eqsubst_wrap_tac ctxt thms = wrap_tac (EqSubst.eqsubst_tac ctxt [0] thms) +fun eqsubst_asm_wrap_tac ctxt thms = wrap_tac (EqSubst.eqsubst_asm_tac ctxt [0] thms) +*} + +ML {* +structure ProveSimplToGraphGoals = struct + +fun goal_eq (g, g') = + (eq_list (op aconv) (Logic.strip_assums_hyp g, Logic.strip_assums_hyp g')) + andalso (Logic.strip_assums_concl g aconv Logic.strip_assums_concl g') + andalso (map snd (Logic.strip_params g) = map snd (Logic.strip_params g')) + +fun tactic_check s tac = let + in fn i => fn t => case Seq.list_of (tac i t) + of [] => Seq.empty + | [t'] => let + val orig_goals = Thm.prems_of t + val new_goals = Thm.prems_of t' + in (eq_list goal_eq (take (i - 1) orig_goals, take (i - 1) new_goals) + andalso eq_list goal_eq (drop i orig_goals, + drop (i + length new_goals - length orig_goals) new_goals)) + orelse raise THM ("tactic " ^ s ^ " broke the rules!", i, [t, t']) + ; Seq.single t' + end + | _ => raise THM ("tactic " ^ s ^ " nondeterministic", i, [t]) + end + +(* FIXME: shadows SimplExport *) +fun get_c_type_size ctxt (Type (@{type_name array}, [elT, nT])) = + get_c_type_size ctxt elT * Word_Lib.dest_binT nT + | get_c_type_size _ @{typ word8} = 1 + | get_c_type_size _ @{typ word16} = 2 + | get_c_type_size _ @{typ word32} = 4 + | get_c_type_size _ @{typ word64} = 8 + | get_c_type_size _ (Type (@{type_name ptr}, [_])) = 4 + | get_c_type_size ctxt (T as Type (s, _)) = let + val thm = Proof_Context.get_thm ctxt (s ^ "_size") + handle ERROR _ => raise TYPE ("get_c_type_size: couldn't get size", [T], []) + in Thm.rhs_of thm |> term_of |> HOLogic.dest_number |> snd end + | get_c_type_size _ T = raise TYPE ("get_c_type_size:", [T], []) + +fun enum_simps csenv ctxt = let + val Absyn.CE ecenv = ProgramAnalysis.cse2ecenv csenv; + in + #enumenv ecenv |> Symtab.dest + |> map (Proof_Context.get_thm ctxt o suffix "_def" o fst) + end + +fun safe_goal_tac ctxt = + REPEAT_ALL_NEW (DETERM o CHANGED o safe_steps_tac ctxt) + +fun heap_upd_kind (Const (@{const_name heap_update}, _) $ _ $ _ $ _) + = "HeapUpd" + | heap_upd_kind (Const (@{const_name hrs_mem}, _) $ v) + = let + val gs = exists_Const (fn (s, _) => s = @{const_name globals_swap}) v + val hu = exists_Const (fn (s, _) => s = @{const_name heap_update}) v + in (gs orelse raise TERM ("heap_upd_kind: hrs_mem but no globals_swap", [v])); + if hu then "HeapUpdWithSwap" else "GlobalUpd" + end + | heap_upd_kind t = raise TERM ("heap_upd_kind: unknown", [t]) + +fun except_tac ctxt msg = SUBGOAL (fn (t, _) => let + in warning msg; Syntax.pretty_term ctxt t |> Pretty.writeln; + raise TERM (msg, [t]) end) + +fun res_from_ctxt tac_name thm_name ctxt thm = let + val thm_from_ctxt = Proof_Context.get_thm ctxt thm_name + handle ERROR _ => raise THM (tac_name ^ ": need thm " ^ thm_name, 1, []) + in thm_from_ctxt RS thm + handle THM _ => raise THM (tac_name ^ ": need thm to resolve: " ^ thm_name, + 1, [thm_from_ctxt, thm]) + end + +fun prove_ptr_safe reason ctxt = DETERM o + (TRY o REPEAT_ALL_NEW (eqsubst_asm_wrap_tac ctxt + @{thms array_ptr_index_coerce} + ORELSE' eqsubst_wrap_tac ctxt + @{thms array_ptr_index_coerce} + ) + THEN_ALL_NEW asm_simp_tac (ctxt addsimps + @{thms ptr_safe_field[unfolded typ_uinfo_t_def] + ptr_safe_Array_element unat_less_helper + h_t_valid_Array_element' h_t_valid_field}) + THEN_ALL_NEW except_tac ctxt + ("prove_ptr_safe: failed for " ^ reason) + ) + +fun get_disjoint_h_val_globals_swap ctxt = + @{thm disjoint_h_val_globals_swap_insert} + |> res_from_ctxt "prove_heap_update_id" "global_acc_valid" ctxt + |> res_from_ctxt "prove_heap_update_id" "globals_list_distinct" ctxt + +fun prove_heap_update_id ctxt = DETERM o let + val thm = get_disjoint_h_val_globals_swap ctxt + in fn i => (resolve_tac @{thms heap_update_id_Array heap_update_id + heap_update_id_Array[symmetric] heap_update_id[symmetric]} i + ORELSE except_tac ctxt "prove_heap_update_id: couldn't init" i) + THEN (simp_tac ctxt + THEN_ALL_NEW (* simp_tac will solve goal unless globals swap involved *) + ((rtac thm + ORELSE' (rtac @{thm sym} THEN' rtac thm) + ORELSE' except_tac ctxt "prove_heap_update_id: couldn't rtac") + THEN' (atac (* htd_safe assumption *) + ORELSE' except_tac ctxt "prove_heap_update_id: couldn't atac") + THEN' prove_ptr_safe "prove_heap_update" ctxt)) i + end + +fun get_field_h_val_rewrites ctxt = + Proof_Context.get_thms ctxt "field_h_val_rewrites" + handle ERROR _ => raise THM + ("run add_field_h_val_rewrites on ctxt", 1, []) + +fun get_globals_rewrites ctxt = let + val gsr = Proof_Context.get_thms ctxt "globals_swap_rewrites" + val cgr = Proof_Context.get_thms ctxt "const_globals_rewrites_with_swap" + in (gsr, cgr) end + handle ERROR _ => raise THM + ("run add_globals_swap_rewrites on ctxt", 1, []) + +fun normalise_mem_accs ctxt = DETERM o let + val init_simps = @{thms hrs_mem_update + heap_access_Array_element' + o_def + } @ get_field_h_val_rewrites ctxt + @ #2 (get_globals_rewrites ctxt) + @ #1 (get_globals_rewrites ctxt) + val h_val = get_disjoint_h_val_globals_swap ctxt + val disjoint_h_val_tac + = (eqsubst_asm_wrap_tac ctxt [h_val] ORELSE' eqsubst_wrap_tac ctxt [h_val]) + THEN' (atac ORELSE' except_tac ctxt "normalise_mem_accs: couldn't atac") + in + asm_full_simp_tac (ctxt addsimps init_simps addsimps [h_val]) + THEN_ALL_NEW + (TRY o REPEAT_ALL_NEW ((eqsubst_wrap_tac ctxt + @{thms heap_access_Array_element'} + ORELSE' disjoint_h_val_tac) + THEN_ALL_NEW asm_simp_tac (ctxt addsimps init_simps))) + THEN_ALL_NEW + SUBGOAL (fn (t, i) => case + Envir.beta_eta_contract (Logic.strip_assums_concl t) + of @{term Trueprop} $ (Const (@{const_name h_t_valid}, _) $ _ $ _ $ _) + => prove_ptr_safe "normalise_mem_accs" ctxt i + | @{term Trueprop} $ (Const (@{const_name ptr_safe}, _) $ _ $ _) + => prove_ptr_safe "normalise_mem_accs" ctxt i + | _ => all_tac) + THEN_ALL_NEW full_simp_tac (ctxt addsimps @{thms h_val_ptr h_val_word32}) + end + +fun prove_mem_equality ctxt = DETERM o let + val init_simpset = ctxt + addsimps @{thms hrs_mem_update heap_update_Array_update + heap_access_Array_element' + o_def + } @ get_field_h_val_rewrites ctxt + val unpack_simpset = ctxt + addsimps @{thms heap_update_def to_bytes_array + heap_update_list_append heap_list_update_ptr heap_list_update_word32 + field_lvalue_offset_eq ptr_add_def + array_ptr_index_def + h_val_word32 h_val_ptr + take_heap_list_min drop_heap_list_general + } @ Proof_Context.get_thms ctxt "field_to_bytes_rewrites" + addsimprocs [Word_Bitwise_Tac.expand_upt_simproc] + handle ERROR _ => raise THM + ("prove_mem_equality: run add_field_to_bytes_rewrites on ctxt", 1, []) + + fun double_heap_update_strategy ctxt = + resolve_tac @{thms double_heap_update_eq double_heap_update_eq[THEN sym]} + THEN' (TRY o SUBGOAL (fn (_, i) => double_heap_update_strategy ctxt i)) + THEN' prove_heap_update_id ctxt + + in simp_tac init_simpset + THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (eqsubst_wrap_tac ctxt + @{thms heap_access_Array_element' heap_update_Array_update})) + THEN_ALL_NEW TRY o double_heap_update_strategy ctxt + THEN_ALL_NEW SUBGOAL (fn (t, i) => if + exists_Const (fn (s, T) => s = @{const_name heap_update} + andalso get_c_type_size ctxt (domain_type (range_type T)) > 256 + ) t + then except_tac ctxt "prove_mem_equality: unfolding large heap_update" i + else all_tac) + (* need to normalise mem accs before unfolding unpack_simps + as some of this process depends on structured pointer constructions *) + THEN_ALL_NEW normalise_mem_accs ctxt + THEN_ALL_NEW simp_tac unpack_simpset + THEN_ALL_NEW simp_tac (ctxt addsimps @{thms store_word32s_equality_fold + store_word32s_equality_final add_commute}) + THEN_ALL_NEW simp_tac (ctxt addsimprocs [store_word32s_equality_simproc] + addsimps @{thms store_word32s_equality_final add_commute}) + THEN_ALL_NEW SUBGOAL (fn (t, i) => if exists_Const + (fn (s, _) => s = @{const_name store_word32} + orelse s = @{const_name heap_update}) t + then except_tac ctxt "prove_mem_equality: remaining mem upds" i + else all_tac) + end + +fun prove_global_equality ctxt + = simp_tac (ctxt addsimps (#1 (get_globals_rewrites ctxt))) + THEN' prove_mem_equality ctxt + +fun clean_heap_upd_swap ctxt = DETERM o let + val thm = @{thm disjoint_heap_update_globals_swap_rearranged} + val thm = res_from_ctxt "clean_heap_upd_swap" "global_acc_valid" ctxt thm + val thm = res_from_ctxt "clean_heap_upd_swap" "globals_list_distinct" ctxt thm + in fn i => rtac @{thm trans} i + THEN (rtac thm i + ORELSE except_tac ctxt "clean_heap_upd_swap: couldn't rtac" i) + THEN (atac i (* htd_safe assumption *) + ORELSE except_tac ctxt "clean_heap_upd_swap: couldn't atac" i) + THEN prove_ptr_safe "clean_upd_upd_swap" ctxt i + end + +fun decompose_mem_goals trace ctxt = SUBGOAL (fn (t, i) => + case Envir.beta_eta_contract (Logic.strip_assums_concl t) of + @{term Trueprop} $ (Const (@{const_name const_globals_in_memory}, _) $ _ $ _ $ _) + => let val thm = res_from_ctxt "decompose_mem_goals" + "globals_list_distinct" ctxt + @{thm const_globals_in_memory_heap_updateE} + in (etac thm THEN' atac THEN' prove_ptr_safe "const_globals" ctxt) + ORELSE' except_tac ctxt "decompose_mem_goals: const globals" + end i + | @{term Trueprop} $ (@{term "op = :: heap_mem \ _"} $ x $ y) => let + val query = (heap_upd_kind x, heap_upd_kind y) + val _ = if trace then writeln ("decompose_mem_goals: " ^ @{make_string} query) + else () + in case (heap_upd_kind x, heap_upd_kind y) of + ("HeapUpd", "HeapUpd") => prove_mem_equality ctxt i + | ("HeapUpdWithSwap", "HeapUpd") + => clean_heap_upd_swap ctxt i THEN prove_mem_equality ctxt i + | ("HeapUpd", "HeapUpdWithSwap") => + rtac @{thm sym} i THEN clean_heap_upd_swap ctxt i THEN prove_mem_equality ctxt i + | ("HeapUpd", "GlobalUpd") => prove_global_equality ctxt i + | ("GlobalUpd", "HeapUpd") => prove_global_equality ctxt i + | _ => raise TERM ("decompose_mem_goals: mixed up " + ^ heap_upd_kind x ^ "," ^ heap_upd_kind y, [x, y]) + end + | _ => all_tac) + +fun unat_mono_tac ctxt = resolve_tac @{thms unat_mono_intro} + THEN' ((((TRY o REPEAT_ALL_NEW (resolve_tac @{thms unat_mono_thms})) + THEN_ALL_NEW rtac @{thm order_refl}) + THEN_ALL_NEW except_tac ctxt "unat_mono_tac: escaped order_refl") + ORELSE' except_tac ctxt "unat_mono_tac: couldn't get started") + THEN' (asm_full_simp_tac (ctxt addsimps @{thms word_less_nat_alt word_le_nat_alt}) + THEN_ALL_NEW except_tac ctxt "unat_mono_tac: unsolved") + +fun tactic_check' (ss, t) = (ss, tactic_check (hd ss) t) + +fun graph_refine_proof_tacs csenv ctxt = let + (* FIXME: fix shiftr_no and sshiftr_no in Word *) + val ctxt = ctxt delsimps @{thms shiftr_no sshiftr_no} + |> Splitter.del_split @{thm split_if} + |> Simplifier.del_cong @{thm if_weak_cong} + + in [ + (["step 1: normalise some word arithmetic. this needs", + "to be done before any general simplification.", + "also unfold some things that may be in assumptions", + "and should be unfolded"], + full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps @{thms + signed_arith_ineq_checks_to_eq_word32 + signed_arith_eq_checks_to_ord + signed_mult_eq_checks32_to_64 + signed_shift_guard_to_word_32 + mex_def meq_def} + addsimps [Proof_Context.get_thm ctxt "simpl_invariant_def"])), + (["step 2: normalise a lot of things that occur in", + "simpl->graph that are extraneous"], + asm_full_simp_tac (ctxt addsimps @{thms eq_impl_def + var_word32_def var_word8_def var_mem_def + var_htd_def var_acc_var_upd + var_ms_def init_vars_def + return_vars_def upd_vars_def save_vals_def + mem_upd_def mem_acc_def hrs_mem_update + + (* this includes wrappers for word arithmetic *) + bvlshr_def bvashr_def bvshl_def bv_clz_def + } + (* we should also unfold enumerations, since the graph + representation does this, and we need to normalise + word arithmetic the same way on both sides. *) + addsimps (enum_simps csenv ctxt) + )), + (["step 3: split into goals with safe steps", + "also derive ptr_safe assumptions from h_t_valid"], + (TRY o safe_goal_tac ctxt) + THEN_ALL_NEW (TRY o DETERM o REPEAT_ALL_NEW (dtac @{thm h_t_valid_orig_and_ptr_safe})) + THEN_ALL_NEW (TRY o safe_goal_tac ctxt)), + (["step 4: split up memory write problems."], + decompose_mem_goals false ctxt), + (["step 5: normalise memory reads"], + normalise_mem_accs ctxt), + (["step 7: try to simplify out all remaining word logic"], + asm_full_simp_tac (ctxt addsimps @{thms + pvalid_def pweak_valid_def palign_valid_def + field_lvalue_offset_eq array_ptr_index_def ptr_add_def + mask_def unat_less_helper + word_sle_def[THEN iffD2] word_sless_alt[THEN iffD2] + field_simps NULL_ptr_val + drop_sign_isomorphism max_word_minus + ptr_equalities_to_ptr_val + extra_sle_sless_unfolds + word_neq_0_conv_neg_conv + } + )), + (["step 8: attack unat less-than properties explicitly"], + TRY o unat_mono_tac ctxt) + +(* not sure if any of this is useful. + asm_full_simp_tac (ctxt addsimps @{thms + to_bytes_array heap_update_def + upt_rec take_heap_list_min drop_heap_list_general + heap_update_list_append heap_list_update_ptr heap_list_update_word32 + store_store_word32_commute_offset field_simps + heap_access_Array_element h_val_word32 h_val_ptr + ucast_eq_0s} + addsimps (Proof_Context.get_thms ctxt "field_h_val_rewrites") + addsimps (Proof_Context.get_thms ctxt "field_to_bytes_rewrites") + ), + simp_tac (ctxt addsimps @{thms store_word32s_equality_fold + store_word32s_equality_final add_commute}), + simp_tac (ctxt addsimprocs [store_word32s_equality_simproc] + addsimps @{thms store_word32s_equality_final add_commute}) +*) + ] + + end + +fun graph_refine_proof_full_tac csenv ctxt = EVERY + (map (fn (ss, t) => ALLGOALS + (t ORELSE' except_tac ctxt ("FAILED: " ^ space_implode "\n" ss))) + (graph_refine_proof_tacs csenv ctxt)) + +fun graph_refine_proof_full_goal_tac csenv ctxt + = (foldr1 (op THEN_ALL_NEW) + (map snd (graph_refine_proof_tacs csenv ctxt))) + +fun simpl_to_graph_thm funs csenv noreturns ctxt nm = let + val hints = SimplToGraphProof.mk_hints funs ctxt nm + val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs noreturns hints nm + ctxt + val res_thm = init_thm |> graph_refine_proof_full_tac csenv ctxt |> Seq.hd + val _ = if Thm.nprems_of res_thm = 0 then () + else raise THM ("simpl_to_graph_thm: unsolved subgoals", 1, [res_thm]) + (* FIXME: make hidden assumptions explicit *) + in res_thm end + +fun test_graph_refine_proof funs csenv noreturns ctxt nm = case + Symtab.lookup funs nm of SOME (_, _, NONE) => "skipped " ^ nm + | _ => let + val ctxt = define_graph_fun_short funs nm ctxt + in simpl_to_graph_thm funs csenv noreturns ctxt nm; + "success on " ^ nm end + +fun test_all_graph_refine_proofs_after funs csenv noreturns ctxt nm = let + val ss = Symtab.keys funs + val n = case nm of NONE => ~1 | SOME nm' => find_index (fn s => s = nm') ss + val ss = if n = ~1 then ss else drop (n + 1) ss + val err = prefix "ERROR for: " #> error + val _ = map (fn s => (writeln ("testing: " ^ s); + writeln (test_graph_refine_proof funs csenv noreturns ctxt s)) + handle TERM _ => err s | TYPE _ => err s | THM _ => err s) ss + in "success" end + +end +*} + +end diff --git a/tools/asmrefine/SimplExport.thy b/tools/asmrefine/SimplExport.thy index d02a8e22f..136564c2f 100644 --- a/tools/asmrefine/SimplExport.thy +++ b/tools/asmrefine/SimplExport.thy @@ -914,7 +914,7 @@ fun emit_body ctxt params (Const (@{const_name Seq}, _) $ a $ b) n c e = let = (n, c) | emit_body ctxt params (Const (@{const_name whileAnno}, _) $ C $ _ $ _ $ a) n c e = let fun sn i = string_of_int (n + i) - val lc = "loop#count" ^ sn 0 ^ " Word 32" + val lc = "loop#" ^ sn 0 ^ "#count" ^ " Word 32" val (n', nm) = emit_body ctxt params a (n + 3) (sn 0) e val cond = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) C) in emit (sn 0 ^ " Basic " ^ sn 1 ^ " 1 " ^ lc