adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'master' into ioapic

This commit is contained in:
Joel Beeren 2014-08-29 13:14:53 +10:00
parent b3e2eb1f9d 0346fb20b6
commit 463df8e083
8 changed files with 1624 additions and 572 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

218
lib/LemmaBucket_C.thy
View File

@ -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 \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> 'a ptr"
where
"array_ptr_index p coerce n = CTypesDefs.ptr_add (ptr_coerce p)
(if coerce \<and> n \<ge> 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
= (\<lambda>s. foldl (\<lambda>s n. heap_update (CTypesDefs.ptr_add (Ptr (ptr_val p) :: 'a ptr) (of_nat n))
= (\<lambda>s. foldl (\<lambda>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="\<lambda>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)
\<Longrightarrow> 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 \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs =simp=> f x = g x)
\<Longrightarrow> 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} \<inter> {q ..+ length ys} = {}
\<Longrightarrow> 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:
"\<lbrakk> {ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val q ..+ size_of TYPE('b)} = {};
wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)) \<rbrakk>
\<Longrightarrow> 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: "\<And>x k. \<lbrakk> x < CARD('b); k < size_of TYPE('a) \<rbrakk>
@ -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
\<Longrightarrow> 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':
"\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce \<or> n < CARD('b) \<rbrakk>
\<Longrightarrow> htd \<Turnstile>\<^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 "\<exists>offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs)
\<and> 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 "\<forall>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:
"\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 \<le> n; n < int CARD('b) \<rbrakk>
\<Longrightarrow> htd \<Turnstile>\<^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:
"\<lbrakk> ptr_safe (p :: (('a :: mem_type)['b :: finite]) ptr) htd; coerce \<or> n < CARD('b) \<rbrakk>
\<Longrightarrow> ptr_safe (array_ptr_index p coerce n) htd"
apply (simp add: ptr_safe_def)
apply (erule order_trans[rotated])
apply (subgoal_tac "\<exists>offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs)
\<and> 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 "\<forall>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 \<or> ?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:

96
proof/asmrefine/SEL4GlobalsSwap.thy
View File

@ -129,13 +129,99 @@ lemma unat_ucast_less_helper:
"ucast (x :: word8) < (of_nat m :: word32) \<Longrightarrow> 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 \<in> set xs \<Longrightarrow> globals_list_distinct D symtab xs
\<Longrightarrow> \<not> P x
\<Longrightarrow> 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) \<subseteq> {ptr_val p ..+ size_of TYPE ('a :: c_type)} \<times> UNIV"
by (auto simp: s_footprint_def s_footprint_untyped_def
intvl_def size_of_def)
lemma h_val_globals_swap_in_const_global:
"\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
globals_list_distinct D symtab xs;
const_global_data s (v :: 'a :: c_type) \<in> set xs;
unat offs + size_of TYPE('b) \<le> size_of TYPE('a) \<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
globals_list_distinct D symtab xs;
const_global_data nm v \<in> set xs;
const_globals_in_memory symtab xs (hrs_mem (g_hrs gs)) \<rbrakk>
\<Longrightarrow> 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

155
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -10,8 +10,7 @@
theory SEL4GraphRefine
imports "../../tools/asmrefine/GraphRefine"
"../../tools/asmrefine/FieldAccessors"
imports "../../tools/asmrefine/ProveGraphRefine"
"../../spec/cspec/Substitute"
"SEL4GlobalsSwap"
@ -20,7 +19,7 @@ begin
ML {* Toplevel.debug := true *}
ML {*
val funs = ParseGraph.funs @{theory} "../../spec/cspec/CFunDump.txt"
val funs = ParseGraph.funs @{theory} "CFunDump.txt"
*}
ML {*
@ -30,86 +29,150 @@ 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 \<Rightarrow> unit \<times> nat"
definition
simpl_invariant :: "globals myvars set"
at_addr :: "'a \<Rightarrow> bool"
where
"simpl_invariant = UNIV"
"at_addr addr = True"
lemma eq_impl_at_addrI:
"\<lbrakk> \<And>sst gst. at_addr addr \<Longrightarrow> sst \<in> S \<Longrightarrow> eqs gst sst \<Longrightarrow> eqs2 gst sst \<rbrakk>
\<Longrightarrow> 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" *}
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: "\<exists>ft. (\<forall>s xs. (\<Gamma> \<turnstile> \<langle>com.Call halt_'proc, Normal s\<rangle> \<Rightarrow> 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
"simpl_invariant = {s. const_globals_in_memory symbol_table globals_list
(hrs_mem (t_hrs_' (globals s)))
\<and> 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
val hints = SimplToGraphProof.mk_hints funs @{context} nm
*}
ML {* init_graph_refines_proof funs nm @{context} *}
ML {*
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs [@{thm halt_halts}] hints nm
@{context}
*}
ML {*
ProveSimplToGraphGoals.simpl_to_graph_thm funs (csenv ()) [@{thm halt_halts}] @{context} nm;
*}
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
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 {* 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 (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)
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 (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 {* full_tac @{context} *})[1]
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
apply (auto simp: mex_def meq_def)
done
end

5
proof/infoflow/Noninterference.thy
View File

@ -3393,7 +3393,10 @@ lemma cur_domain_reads: "(s,s') \<in> uwr u \<Longrightarrow> 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]

18
tools/asmrefine/FieldAccessors.thy
View File

@ -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:
"\<lbrakk> field_lookup (typ_info_t TYPE('a)) [s] 0
\<equiv> 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) \<noteq> 0 \<rbrakk>
\<Longrightarrow> 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\<rightarrow>[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 =

519
tools/asmrefine/GraphRefine.thy
View File

@ -595,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 (\<lambda>gst sst. cond gst = (sst \<in> C)) I"
assumes ss: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) UNIV I eqs out_eqs \<rbrakk>
\<Longrightarrow> 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 \<inter> 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: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) UNIV I eqs out_eqs \<rbrakk>
\<Longrightarrow> 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 \<inter> - 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)+)
@ -617,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 (\<lambda>gst sst. cond gst = (sst \<in> C)) (I \<inter> G)"
assumes ss: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (G \<inter> C) I eqs2 out_eqs"
and ss_eq: "eq_impl nn eqs eqs2 (I \<inter> G \<inter> C)"
assumes ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \<inter> (- C)) I eqs3 out_eqs"
and ss: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (G \<inter> C) I eqs2 out_eqs"
and ex_eq: "eq_impl nn eqs eqs3 (I \<inter> G \<inter> - C)"
and ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \<inter> (- C)) I eqs3 out_eqs"
and in_eq: "eq_impl nn eqs (\<lambda>gst sst. sst \<in> G) (I \<inter> 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)
@ -845,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:
"\<lbrakk> GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds);
eq_impl nn eqs (\<lambda>gst sst. eqs2 (upd_vars upds gst) sst) (P \<inter> I);
simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs \<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk> 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 \<inter> I) \<rbrakk>
\<Longrightarrow> 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
@ -1064,7 +1072,7 @@ lemma simpl_to_graph_call_next_step:
((exec_graph_step GGamma) ^^ steps) `` {[(nn', gst', p)]} \<subseteq> {[(nn'', f gst', p)]}
\<and> steps < 2 \<and> (steps = 0 \<or> nn' \<notin> {Ret, Err})"
and rel: "graph_fun_refines SGamma GGamma I inputs proc outputs p'"
and modifies: "\<forall>\<sigma>. SGamma \<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} com.Call proc (Q \<sigma>)"
and modifies: "(\<forall>\<sigma>. SGamma \<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} com.Call proc (Q \<sigma>)) \<or> (Q = (\<lambda>_. UNIV))"
and init: "eq_impl nn eqs (\<lambda>gst sst. initf sst \<in> I
\<and> map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs) (I \<inter> P)"
and ret: "eq_impl nn eqs (\<lambda>gst sst. \<forall>sst' vs. map (\<lambda>i. i sst') outputs = vs
@ -1131,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
@ -1287,6 +1297,14 @@ lemma is_aligned_intvl_disjoint:
apply (simp add: field_simps del: Int_atLeastAtMost)
done
lemma is_aligned_intvl_disjoint_offset:
"\<lbrakk> p \<noteq> p'; is_aligned (p - p') n \<rbrakk>
\<Longrightarrow> {p ..+ 2 ^ n} \<inter> {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:
"\<lbrakk> p \<noteq> p'; is_aligned p 2; is_aligned p' 2 \<rbrakk>
\<Longrightarrow> store_word32 p w (store_word32 p' w' hp)
@ -1305,13 +1323,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 +1379,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:
"\<lbrakk> n \<noteq> 0; (i \<noteq> (n - 1)) \<rbrakk> \<Longrightarrow> (i < (n :: word32)) = (i < (n - 1))"
apply (rule sym, rule trans, rule less_le)
@ -1374,32 +1396,184 @@ 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
\<Longrightarrow> 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: "\<forall>x. x AND 3 = 0 \<longrightarrow> 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: "\<And>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 "\<dots> = (store_word32 ?p (load_word32 ?p hp') hp') x"
by (simp only: X, simp add: eq word_bw_assocs)
also have "\<dots> = hp' x"
by (simp add: store_load_word32)
finally show "hp x = hp' x" .
qed
definition
"apply_store_word32 p = (\<lambda>(offs, w) hp. if offs AND 3 = 0
then store_word32 (p + offs) w hp else hp)"
definition
store_word32s_equality :: "word32 \<Rightarrow> (word32 \<times> word32) list
\<Rightarrow> (word32 \<times> word32) list \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> bool"
where
"store_word32s_equality p xs ys hp hp' \<equiv>
fold (apply_store_word32 p) xs hp = fold (apply_store_word32 p) ys hp'"
lemma store_word32s_equality_fold:
"p' - p AND 3 = 0 \<Longrightarrow>
(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 \<Longrightarrow>
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 \<Longrightarrow>
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 \<Longrightarrow> (y :: ('a :: len) word) AND 3 = 0 \<Longrightarrow> (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 \<Longrightarrow> 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
\<Longrightarrow> load_word32 (p + x) (fold (apply_store_word32 p) (filter (P \<circ> 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
\<and> 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 \<longrightarrow> v = v')"
"store_word32s_equality p [(x, v)] [] hp hp
= (x AND 3 = 0 \<longrightarrow> v = load_word32 (p + x) hp)"
"store_word32s_equality p [] [(x, v')] hp hp
= (x AND 3 = 0 \<longrightarrow> 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 {*
structure UseHints = struct
val dest_word = HOLogic.dest_number
#> snd #> (fn x => x mod 4294967296)
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
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 \<Rightarrow> _"}
else @{term "op \<ge> :: word32 \<Rightarrow> _"})
$ HOLogic.mk_number @{typ word32} pivot
in store_word32_trace "success" (SOME (cterm_instantiate
[(@{cpat "?P :: word32 \<Rightarrow> 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 SimplToGraphProof = struct
fun mk_ptr_val_app p =
Const (@{const_name ptr_val}, fastype_of p --> @{typ word32}) $ p
@ -1435,8 +1609,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 ".")
@ -1457,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)
@ -1540,7 +1718,7 @@ fun mk_graph_refines (funs : ParseGraph.funs) ctxt s = let
(Long_Name.base_name s ^ "_'proc")
val gamma = Syntax.read_term ctxt "\<Gamma>"
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
@ -1581,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}
@ -1619,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]})
@ -1654,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)))
@ -1679,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
@ -1691,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
@ -1715,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 \<Rightarrow> _"} $ _ $ _)) $ Bound 0)
@ -1774,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, [])
@ -1789,15 +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
@ -1805,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
@ -1875,98 +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 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}),
(* 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}), *)
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
})
]
*}
fun mk_graph_refines_proof funs noreturns hints 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))
|> 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

532
tools/asmrefine/ProveGraphRefine.thy Normal file
View File

@ -0,0 +1,532 @@
theory ProveGraphRefine
imports GraphRefine
GlobalsSwap FieldAccessors
begin
lemma const_globals_in_memory_heap_updateE:
"\<lbrakk> 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 \<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk> 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 \<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk> 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 \<rbrakk>
\<Longrightarrow> 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
\<Longrightarrow> heap_update p v hp = hp'
\<Longrightarrow> (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 \<Longrightarrow> h_t_valid d g p \<and> 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)
\<Longrightarrow> 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) \<le> unat a + unat b"
"unat (a * b) \<le> unat a * unat b"
by (simp_all add: unat_word_ariths)
lemma unat_mono_intro:
"unat a \<le> x \<Longrightarrow> x < b \<Longrightarrow> unat a < b"
"unat a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> unat a \<le> b"
by simp_all
lemma word_neq_0_conv_neg_conv:
"(\<not> 0 < (n :: ('a :: len) word)) = (n = 0)"
by (cases "n = 0", simp_all)
definition
drop_sign :: "('a :: len) signed word \<Rightarrow> '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 \<le> y) = (drop_sign x \<le> drop_sign y)"
"(x <s y) = (drop_sign x <s drop_sign y)"
"(x <=s y) = (drop_sign x <=s drop_sign y)"
"drop_sign (x + y) = drop_sign x + drop_sign y"
"drop_sign (x - y) = drop_sign x - drop_sign y"
"drop_sign (x * y) = drop_sign x * drop_sign y"
"drop_sign (- y) = - drop_sign y"
"drop_sign (if P then x else y) = (if P then drop_sign x else drop_sign y)"
by (simp_all add: drop_sign_def word_less_def
word_le_def word_sless_def word_sle_def
sint_drop_sign_isomorphism[unfolded drop_sign_def]
word_uint.Rep_inject[symmetric]
uint_up_ucast is_up_def source_size_def
target_size_def word_size
uint_word_arith_bintrs
del: word_uint.Rep_inject)
lemma drop_sign_isomorphism_bitwise:
"drop_sign (x AND y) = drop_sign x AND drop_sign y"
"drop_sign (bitOR x y) = bitOR (drop_sign x) (drop_sign y)"
"drop_sign (x XOR y) = drop_sign x XOR drop_sign y"
"drop_sign (~~ y) = ~~ drop_sign y"
"drop_sign (shiftl x n) = shiftl (drop_sign x) n"
"drop_sign (shiftr x n) = shiftr (drop_sign x) n"
"drop_sign (sshiftr x n) = sshiftr (drop_sign x) n"
"drop_sign (ucast z) = ucast z"
"drop_sign (scast z) = scast z"
"ucast x = ucast (drop_sign x)"
"scast x = scast (drop_sign x)"
by (rule word_eqI
| simp add: word_size drop_sign_def nth_ucast nth_shiftl
nth_shiftr nth_sshiftr word_ops_nth_size
nth_scast
| safe
| simp add: test_bit_bin)+
lemma drop_sign_number[simp]:
"drop_sign (numeral n) = numeral n"
"drop_sign (neg_numeral n) = neg_numeral n"
"drop_sign 0 = 0" "drop_sign 1 = 1"
by (simp_all add: drop_sign_def ucast_def)
lemmas drop_sign_isomorphism
= drop_sign_isomorphism_ariths
drop_sign_isomorphism_bitwise
ucast_id
lemma ptr_equalities_to_ptr_val:
"(Ptr addr = p) = (addr = ptr_val p)"
"(p = Ptr addr) = (ptr_val p = addr)"
by (simp | cases p)+
(* FIXME move to Lib then to Word *)
lemmas extra_sle_sless_unfolds
= word_sle_def[where a=0 and b=1]
word_sle_def[where a=0 and b="numeral n"]
word_sle_def[where a=1 and b=0]
word_sle_def[where a=1 and b="numeral n"]
word_sle_def[where a="numeral n" and b=0]
word_sle_def[where a="numeral n" and b=1]
word_sless_alt[where a=0 and b=1]
word_sless_alt[where a=0 and b="numeral n"]
word_sless_alt[where a=1 and b=0]
word_sless_alt[where a=1 and b="numeral n"]
word_sless_alt[where a="numeral n" and b=0]
word_sless_alt[where a="numeral n" and b=1]
for n
ML {*
fun wrap_tac tac i t = let
val t' = Goal.restrict i 1 t
val r = tac 1 t'
in case Seq.pull r of NONE => 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 \<Rightarrow> _"} $ 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

653
tools/asmrefine/SimplExport.thy
View File

@ -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 \<Rightarrow> '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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> _"} $ 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> 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);
@ -759,37 +914,24 @@ 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 [] (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"}