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

Repair SimplExport/GraphRefine.

This commit is contained in:
Thomas Sewell 2015-12-03 16:34:11 +11:00
parent 2bb62173e5
commit df40425731
6 changed files with 120 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -16,6 +16,8 @@ imports "../../tools/asmrefine/ProveGraphRefine"
begin
declare ptr_add_assertion_uint[simp del]
ML {*
val funs = ParseGraph.funs @{theory} "CFunDump.txt"
*}
@ -63,13 +65,19 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
"snd (snd ((if P then f else g) gs)) = (if P then snd (snd (f gs)) else snd (snd (g gs)))"
by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
(*
ML {* val nm = "Kernel_C.resolveVAddr" *}
ML {* val nm = "Kernel_C.cancelIPC" *}
(*
local_setup {* define_graph_fun_short funs nm *}
ML {*
val ctxt = @{context}
val hints = SimplToGraphProof.mk_hints funs ctxt nm
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
ctxt
*}
ML {*
val v = ProveSimplToGraphGoals.test_graph_refine_proof funs (csenv ()) ctxt nm
*}
*)

8
tools/asmrefine/CommonOps.thy
View File

@ -87,7 +87,9 @@ where
then typ_clear_region y (unat z)
else if x = 1 then ptr_retyps (unat z) (Ptr y :: 'a ptr)
else if x = 2 then typ_region_bytes y (unat z)
else ptr_retyps (2 ^ unat z) (Ptr y :: 'a ptr))"
else if x = 3 then ptr_retyps (2 ^ unat z) (Ptr y :: 'a ptr)
else if x = 4 then ptr_arr_retyps (unat z) (Ptr y :: 'a ptr)
else ptr_arr_retyps (2 ^ unat z) (Ptr y :: 'a ptr))"
type_synonym ghost_assertions = "word64 \<Rightarrow> word32"
@ -113,5 +115,9 @@ definition
definition
"pglobal_valid htd (v :: ('a :: mem_type) itself) x = ptr_inverse_safe (Ptr x :: 'a ptr) htd"
definition
"parray_valid htd (v :: ('a :: c_type) itself) x n
= array_assertion (Ptr x :: 'a ptr) (unat n) htd"
end

43
tools/asmrefine/CommonOpsLemmas.thy
View File

@ -8,14 +8,18 @@ begin
lemma fold_all_htd_updates':
"ptr_retyp (p :: ('a :: c_type) ptr)
= all_htd_updates TYPE('a) 1 (ptr_val p) 1"
"(if P then (f :: heap_typ_desc \<Rightarrow> heap_typ_desc) else g) s
= (if P then f s else g s)"
"\<lbrakk> n < 2 ^ 32 \<rbrakk> \<Longrightarrow>
ptr_retyps n p = all_htd_updates TYPE('a) 1 (ptr_val p) (of_nat n)"
"\<lbrakk> n < 2 ^ 32 \<rbrakk> \<Longrightarrow>
ptr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 3 (ptr_val p) (of_nat n)"
"n < 2 ^ 32 \<Longrightarrow> typ_clear_region x n = all_htd_updates TYPE(word32) 0 x (of_nat n)"
"n < 2 ^ 32 \<Longrightarrow> typ_region_bytes x n = all_htd_updates TYPE(word32) 2 x (of_nat n)"
"(if P then (f :: heap_typ_desc \<Rightarrow> heap_typ_desc) else g) s
= (if P then f s else g s)"
"\<lbrakk> n < 2 ^ 32 \<rbrakk> \<Longrightarrow>
ptr_arr_retyps n p = all_htd_updates TYPE('a) 4 (ptr_val p) (of_nat n)"
"\<lbrakk> n < 2 ^ 32 \<rbrakk> \<Longrightarrow>
ptr_arr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 5 (ptr_val p) (of_nat n)"
by (simp_all add: all_htd_updates_def unat_of_nat fun_eq_iff of_nat_neq_0)
lemma unat_lt2p_word32:
@ -23,7 +27,7 @@ lemma unat_lt2p_word32:
by (rule order_less_le_trans, rule unat_lt2p, simp)
lemmas fold_all_htd_updates
= fold_all_htd_updates' fold_all_htd_updates'(2-5)[OF unat_lt2p_word32]
= fold_all_htd_updates' fold_all_htd_updates'(3-)[OF unat_lt2p_word32]
lemma signed_div_range_check:
assumes len: "size a > 1"
@ -71,5 +75,38 @@ proof -
done
qed
lemma ptr_add_assertion_uintD:
"ptr_add_assertion ptr (uint (x :: ('a :: len) word)) strong htd
\<longrightarrow> (x = 0 \<or> array_assertion ptr (if strong then unat (x + 1) else unat x) htd)"
using unat_lt2p[where x=x]
by (simp add: ptr_add_assertion_def uint_0_iff Word.unat_def[symmetric]
unat_plus_if_size linorder_not_less word_size
le_Suc_eq array_assertion_shrink_right
del: unat_lt2p)
lemma sint_uint_sless_0_if:
"sint x = (if x <s 0 then - uint (- x) else uint (x :: ('a :: len) word))"
apply (simp add: word_sint_msb_eq word_sless_alt
word_size uint_word_ariths)
apply (clarsimp simp: zmod_zminus1_eq_if uint_0_iff)
done
lemma ptr_add_assertion_sintD:
"ptr_add_assertion ptr (sint (x :: ('a :: len) word)) strong htd
\<longrightarrow> (x = 0 \<or> (x <s 0 \<and> array_assertion (ptr +\<^sub>p sint x)
(unat (- x)) htd)
\<or> (0 <s x \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd))"
using unat_lt2p[where x=x]
apply (simp add: ptr_add_assertion_def word_sless_alt
sint_uint_sless_0_if[THEN arg_cong[where f="\<lambda>x. - x"]]
sint_uint_sless_0_if[THEN arg_cong[where f=nat]]
Word.unat_def[symmetric]
unat_plus_if_size le_Suc_eq linorder_not_less
word_size
del: unat_lt2p)
apply (simp add: array_assertion_shrink_right)
apply auto
done
end

1
tools/asmrefine/GraphLang.thy
View File

@ -580,6 +580,7 @@ val opers = Symtab.make [
("ShiftRight", @{const_name "bvlshr"}),
("SignedShiftRight", @{const_name "bvashr"}),
("PValid", @{const_name pvalid}),
("PArrayValid", @{const_name parray_valid}),
("PAlignValid", @{const_name palign_valid}),
("PGlobalValid", @{const_name pglobal_valid}),
("PWeakValid", @{const_name pweak_valid}),

38
tools/asmrefine/ProveGraphRefine.thy
View File

@ -148,10 +148,22 @@ lemma unat_ucast_if_up:
apply (simp add: is_up_def source_size_def target_size_def word_size)
done
(* FIXME: these 2 duplicated from crefine *)
lemma Collect_const_mem:
"(x \<in> (if P then UNIV else {})) = P"
by simp
lemma typ_uinfo_t_diff_from_typ_name:
"typ_name (typ_info_t TYPE ('a :: c_type)) \<noteq> typ_name (typ_info_t TYPE('b :: c_type))
\<Longrightarrow> typ_uinfo_t (at :: 'a itself) \<noteq> typ_uinfo_t (bt :: 'b itself)"
by (clarsimp simp: typ_uinfo_t_def td_diff_from_typ_name)
lemmas ptr_add_assertion_unfold_numeral
= ptr_add_assertion_def[where offs="numeral n" for n, simplified]
ptr_add_assertion_def[where offs="uminus (numeral n)" for n, simplified]
ptr_add_assertion_def[where offs=0, simplified]
ptr_add_assertion_def[where offs=1, simplified]
definition word32_truncate_nat :: "nat => word32 \<Rightarrow> word32"
where
"word32_truncate_nat n x = (if unat x \<le> n then x else of_nat n)"
@ -556,6 +568,23 @@ fun unat_mono_tac ctxt = resolve_tac ctxt @{thms unat_mono_intro}
})
THEN_ALL_NEW except_tac ctxt "unat_mono_tac: unsolved")
fun dest_ptr_add_assertion ctxt = SUBGOAL (fn (t, i) =>
if Term.exists_Const (fn (s, _) => s = @{const_name parray_valid}) t
then (full_simp_tac (ctxt addsimps @{thms ptr_add_assertion'
typ_uinfo_t_diff_from_typ_name parray_valid_def
ptr_add_assertion_unfold_numeral
extra_sle_sless_unfolds})
THEN_ALL_NEW TRY o REPEAT_ALL_NEW (dresolve_tac ctxt
@{thms ptr_add_assertion_uintD[rule_format]
ptr_add_assertion_sintD[rule_format]})
THEN_ALL_NEW SUBGOAL (fn (t, i) =>
if Term.exists_Const (fn (s, _) => s = @{const_name ptr_add_assertion}
orelse s = @{const_name ptr_add_assertion'}) t
then except_tac ctxt "dest_ptr_add_assertion" i
else all_tac)
) i
else all_tac)
fun tactic_check' (ss, t) = (ss, tactic_check (hd ss) t)
fun graph_refine_proof_tacs csenv ctxt = let
@ -607,13 +636,16 @@ fun graph_refine_proof_tacs csenv ctxt = let
addsimprocs [fold_of_nat_eq_Ifs_simproc, unfold_assertion_data_get_set]
) i)),
(["step 3: split into goals with safe steps",
"also derive ptr_safe assumptions from h_t_valid"],
"also derive ptr_safe assumptions from h_t_valid",
"and adjust ptr_add_assertion facts"],
(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 4: split up memory write problems",
"and expand ptr_add_assertion if needed."],
decompose_mem_goals false ctxt
THEN_ALL_NEW dest_ptr_add_assertion ctxt),
(["step 5: normalise memory reads"],
normalise_mem_accs ctxt),
(["step 6: explicitly apply some inequalities"],

36
tools/asmrefine/SimplExport.thy
View File

@ -138,6 +138,11 @@ fun enums ctxt csenv = let
|> Symtab.make |> Symtab.lookup
end
fun thm_to_rew thm
= ((Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_eq)
handle TERM _ => (Thm.concl_of thm |> Logic.dest_equals))
handle TERM _ => (Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_imp)
fun cons_field_upds ctxt csenv = let
val simps = ProgramAnalysis.get_senv csenv
|> maps (fn (tp, vs) => map (pair tp o fst) vs)
@ -151,7 +156,7 @@ fun cons_field_upds ctxt csenv = let
|> maps (fn (_, [t]) => [t]
| (tp, ts) => ts @ Proof_Context.get_thms ctxt
(tp ^ "_accupd_diff"))
val rews = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (simps @ accups)
val rews = map thm_to_rew (simps @ accups)
in Pattern.rewrite_term (Proof_Context.theory_of ctxt) rews [] end
type export_params = {cons_field_upds: term -> term,
@ -534,13 +539,7 @@ fun phase2_convert_global ctxt params accs
in SOME (t', t_thm) end
| _ => NONE
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_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_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs)
fun 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 : export_params) t)
in case (try dest_nat i) of
@ -659,6 +658,12 @@ and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ 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 (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _))
= convert_ph3 ctxt params (ptr_simp_term ctxt "ptr_add"
(head_of t $ Free ("p", domain_type T) $ Free ("n", @{typ int})) t)
| convert_ph3 ctxt params (t as (Const (@{const_name field_lvalue}, T) $ _ $ s))
= convert_ph3 ctxt params (ptr_simp_term ctxt "field_lvalue"
(head_of t $ Free ("p", domain_type T) $ s) t)
| convert_ph3 ctxt params (Const (@{const_name store_word32}, _) $ p $ w $ m)
= convert_op ctxt params "MemUpdate" "Mem" [m, p, w]
| convert_ph3 ctxt params (Const (@{const_name store_word8}, _) $ p $ w $ m)
@ -691,6 +696,18 @@ and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ x)
| 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_ph3 ctxt params (Const (@{const_name array_assertion}, _) $ p $ n $ htd)
= convert_op ctxt params "PArrayValid" "Bool"
[htd, ptr_to_typ p, p, @{term "of_nat :: nat => word32"} $ n]
| convert_ph3 ctxt params (Const (@{const_name ptr_add_assertion'}, assT)
$ p $ n $ str $ htd)
= convert_ph3 ctxt params let val T = dest_ptr_type (fastype_of p)
val ass' = (Const (@{const_name ptr_add_assertion}, assT)) $ p $ n $ str $ htd
val ass'' = Pattern.rewrite_term (Proof_Context.theory_of ctxt)
(map thm_to_rew @{thms ptr_add_assertion_uintD ptr_add_assertion_sintD
if_True if_False}) [] ass'
in if T = @{typ unit} orelse T = @{typ word8}
then @{term True} else ass'' end
| 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_ph3 ctxt params (Const (@{const_name ptr_safe}, _) $ p $ htd)
@ -1045,7 +1062,8 @@ fun emit_func_body ctxt outfile eparams name = let
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})
insert_iff empty_iff
ptr_add_assertion_def if_True if_False})
|> Thm.concl_of |> Logic.dest_equals |> snd
handle ERROR _ => @{term "Spec S"}