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-09-02 11:13:55 +10:00
parent 8fa6226ecc caf0529c7f
commit a5f2cab271
10 changed files with 140 additions and 175 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
lib/WordLib.thy
View File

@ -628,6 +628,23 @@ lemma less_le_mult_nat':
lemmas less_le_mult_nat = less_le_mult_nat'[simplified distrib_right, simplified]
(* FIXME: these should be moved to Word and declared [simp]
but that will probably break everything. *)
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
(*
* Signed division: when the result of a division is negative,
* we will round towards zero instead of towards minus infinity.

65
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -57,6 +57,10 @@ locale graph_refine_locale = kernel_all_substitute
= (xs = Fault ft))"
begin
ML {* SimplToGraphProof.globals_swap
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
*}
local_setup {* add_globals_swap_rewrites @{thms kernel_all_global_addresses.global_data_mems} *}
definition
@ -66,31 +70,26 @@ where
(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 {* ProveSimplToGraphGoals.test_all_fgraph_refine_proofs_after
funs (csenv ()) @{context} (SOME "Kernel_C.alloc_region") *}
ML {* val nm = "Kernel_C.makeUserPDE" *}
ML {* val nm = "Kernel_C.alloc_region" *}
local_setup {* define_graph_fun_short funs nm *}
ML {* SimplToGraphProof.globals_swap
:= (fn t => @{term "globals_swap t_hrs_' t_hrs_'_update symbol_table globals_list"} $ t)
*}
ML {*
val hints = SimplToGraphProof.mk_hints funs @{context} nm
*}
ML {*
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs [@{thm halt_halts}] hints nm
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
@{context}
*}
ML {*
ProveSimplToGraphGoals.simpl_to_graph_thm funs (csenv ()) [@{thm halt_halts}] @{context} nm;
ProveSimplToGraphGoals.simpl_to_graph_thm funs (csenv ()) @{context} nm;
*}
ML {*
val tacs = ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ())
#> map snd
@ -104,53 +103,19 @@ schematic_lemma "PROP ?P"
apply (tactic {* rtac init_thm 1 *})
apply (tactic {* ALLGOALS (TRY o (full_goal_tac @{context} THEN_ALL_NEW K no_tac)) *})
apply (tactic {* ALLGOALS (fn i => fn t =>
let val res = try ((full_goal_tac @{context} THEN_ALL_NEW K no_tac) i #> Seq.hd) t
in case res of NONE => Seq.single t | SOME r => Seq.single r
end) *})
(* apply (tactic {* ALLGOALS (TRY o rtac @{thm eq_impl_at_addrI}) *}) *)
apply -
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 {* full_tac @{context} *})
apply (simp_all add: word_sle_def[THEN arg_cong[where f=Not], THEN iffD2])
defer
apply (tactic {* full_tac @{context} *})[2]
ML_val {* nth (ProveSimplToGraphGoals.graph_refine_proof_tacs (csenv ()) @{context}) 3 *}
apply (tactic {* (nth (tacs @{contfext}) 3) 1 *})
apply (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}) 3) *})
apply (tactic {* ALLGOALS (nth (tacs @{context}) 4) *})

8
proof/crefine/CSpace_C.thy
View File

@ -4071,15 +4071,11 @@ lemma deriveCap_ccorres':
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def returnOk_def)
apply (clarsimp simp: errstate_def isCap_simps
Collect_const_mem)
apply (simp add: cap_get_tag_isCap_ArchObject[THEN trans[OF eq_commute]]
cap_get_tag_isCap_ArchObject)
apply (case_tac v0, simp_all add: isCap_simps from_bool_def
cap_get_tag_isArchCap_unfolded_H_cap)
Collect_const_mem from_bool_0
cap_get_tag_isArchCap_unfolded_H_cap)
done
lemma deriveCap_ccorres:
"ccorres (syscall_error_rel \<currency> ccap_relation) deriveCap_xf
(invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. slot_' s = Ptr slot}) []

88
proof/crefine/Fastpath_C.thy
View File

@ -1116,42 +1116,41 @@ lemma switchToThread_fp_ccorres:
apply (simp add: pd_has_hwasid_def)
apply (wp doMachineOp_pd_at_asid')
apply (rule ccorres_bind_assoc_rev)
apply (ctac add: armv_contextSwitch_fp_ccorres)
apply (simp add: storeWordUser_def bind_assoc option_case_If2
split_def
del: Collect_const)
apply (rule ccorres_symb_exec_l[OF _ gets_inv _ empty_fail_gets])
apply (rename_tac "gf")
apply (rule ccorres_pre_threadGet)
apply (rule ccorres_stateAssert)
apply (rule_tac P="pointerInUserData gf and no_0_obj'
and K (is_aligned gf 2)
and (\<lambda>s. gf = armKSGlobalsFrame (ksArchState s))"
in ccorres_cross_over_guard)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_move_c_guard_tcb)
apply (ctac add: storeWord_ccorres'[unfolded fun_app_def])
apply (simp only: dmo_clearExMonitor_setCurThread_swap
dc_def[symmetric])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp del: rf_sr_upd_safe)
apply (clarsimp simp: setCurThread_def simpler_modify_def
rf_sr_def cstate_relation_def Let_def
carch_state_relation_def cmachine_state_relation_def)
apply (ctac add: clearExMonitor_fp_ccorres)
apply wp
apply (simp add: guard_is_UNIV_def)
apply wp
apply vcg
apply wp
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (wp hoare_drop_imps)[1]
apply (wp doMachineOp_no_0')[1]
apply (simp del: Collect_const)
apply (vcg exspec=armv_contextSwitch_fp_modifies)
apply (ctac(no_vcg) add: armv_contextSwitch_fp_ccorres)
apply (simp add: storeWordUser_def bind_assoc option_case_If2
split_def
del: Collect_const)
apply (rule ccorres_symb_exec_l[OF _ gets_inv _ empty_fail_gets])
apply (rename_tac "gf")
apply (rule ccorres_pre_threadGet)
apply (rule ccorres_stateAssert)
apply (rule_tac P="pointerInUserData gf and no_0_obj'
and K (is_aligned gf 2)
and (\<lambda>s. gf = armKSGlobalsFrame (ksArchState s))
and valid_arch_state'"
in ccorres_cross_over_guard)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_move_c_guard_tcb)
apply (ctac add: storeWord_ccorres'[unfolded fun_app_def])
apply (simp only: dmo_clearExMonitor_setCurThread_swap
dc_def[symmetric])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp del: rf_sr_upd_safe)
apply (clarsimp simp: setCurThread_def simpler_modify_def
rf_sr_def cstate_relation_def Let_def
carch_state_relation_def cmachine_state_relation_def)
apply (ctac add: clearExMonitor_fp_ccorres)
apply wp
apply (simp add: guard_is_UNIV_def)
apply wp
apply vcg
apply wp
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (wp hoare_drop_imps)[1]
apply (wp doMachineOp_no_0')[1]
apply (simp add: bind_assoc checkPDNotInASIDMap_def
checkPDASIDMapMembership_def)
apply (rule ccorres_stateAssert)
@ -1183,8 +1182,6 @@ lemma switchToThread_fp_ccorres:
pde_stored_asid_def split: split_if_asm)
apply (clarsimp simp: singleton_eq_o2s pde_stored_asid_def
split: if_splits)
apply (frule(1) h_t_valid_armKSGlobalsFrame)
apply (frule(1) c_guard_abs_word32_armKSGlobalsFrame)
apply (clarsimp simp del: rf_sr_upd_safe
dest!: isValidVTableRootD
simp: cap_get_tag_isCap_ArchObject2 pde_stored_asid_Some
@ -1199,7 +1196,8 @@ lemma switchToThread_fp_ccorres:
simp del: rf_sr_upd_safe)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
carch_globals_def pointerInUserData_c_guard'
pointerInUserData_h_t_valid2 cpspace_relation_def)
pointerInUserData_h_t_valid2 cpspace_relation_def
c_guard_abs_word32_armKSGlobalsFrame)
done
lemma thread_state_ptr_set_tsType_np_spec:
@ -2633,7 +2631,7 @@ lemma fastpath_call_ccorres:
h_t_valid_clift_Some_iff)
apply ceqv
apply (simp only: bind_assoc[symmetric])
apply (rule ccorres_split_nothrow_dc)
apply (rule ccorres_split_nothrow_novcg_dc)
apply simp
apply (rule ccorres_call,
rule_tac v=shw_asid and pd="capUntypedPtr (cteCap pd_cap)"
@ -2652,8 +2650,8 @@ lemma fastpath_call_ccorres:
apply wp
apply (rule_tac P=\<top> in hoare_triv, simp)
apply (simp add: imp_conjL rf_sr_ksCurThread del: all_imp_to_ex)
apply (simp add: ccap_relation_ep_helpers)
apply (vcg exspec=switchToThread_fp_modifies)
apply (clarsimp simp: ccap_relation_ep_helpers guard_is_UNIV_def
mi_from_H_def)
apply (simp add: pd_has_hwasid_def)
apply (wp sts_ct_in_state_neq' sts_valid_objs')
apply (simp del: Collect_const)
@ -3273,7 +3271,7 @@ lemma fastpath_reply_wait_ccorres:
h_t_valid_clift_Some_iff)
apply ceqv
apply (simp only: bind_assoc[symmetric])
apply (rule ccorres_split_nothrow_dc)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule ccorres_call,
rule_tac v=shw_asid and pd="capUntypedPtr (cteCap pd_cap)"
in switchToThread_fp_ccorres,
@ -3291,8 +3289,8 @@ lemma fastpath_reply_wait_ccorres:
apply wp
apply (rule_tac P=\<top> in hoare_triv, simp)
apply (simp add: imp_conjL rf_sr_ksCurThread del: all_imp_to_ex)
apply (simp add: ccap_relation_ep_helpers)
apply (vcg exspec=switchToThread_fp_modifies)
apply (clarsimp simp: ccap_relation_ep_helpers guard_is_UNIV_def
mi_from_H_def)
apply (simp add: pd_has_hwasid_def)
apply (wp sts_ct_in_state_neq' sts_valid_objs')
apply (simp del: Collect_const)

2
proof/crefine/Finalise_C.thy
View File

@ -1195,7 +1195,7 @@ lemma unmapPageTable_ccorres:
apply (ctac add: cleanByVA_PoU_ccorres)
apply (ctac(no_vcg) add:flushTable_ccorres)
apply wp
apply vcg
apply (vcg exspec=cleanByVA_PoU_modifies)
apply wp
apply (fastforce simp: guard_is_UNIV_def Collect_const_mem Let_def
shiftl_t2n field_simps lookup_pd_slot_def)

12
proof/crefine/Machine_C.thy
View File

@ -484,7 +484,7 @@ lemma cleanCacheRange_PoC_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=cleanByVA_modifies)
apply clarsimp
done
@ -516,7 +516,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=cleanInvalByVA_modifies)
apply (rule ceqv_refl)
apply (ctac (no_vcg) add: dsb_ccorres[simplified dc_def])
apply (wp | clarsimp simp: guard_is_UNIVI)+
@ -560,7 +560,7 @@ lemma cleanCacheRange_PoU_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=cleanByVA_PoU_modifies)
apply clarsimp
done
@ -609,7 +609,7 @@ lemma invalidateCacheRange_RAM_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=invalidateByVA_modifies)
apply ceqv
apply (ctac add: dsb_ccorres[unfolded dc_def])
apply wp
@ -648,7 +648,7 @@ lemma invalidateCacheRange_I_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=invalidateByVA_I_modifies)
apply clarsimp
done
@ -674,7 +674,7 @@ lemma branchFlushRange_ccorres:
apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
mask_out_sub_mask)
apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper)
apply vcg
apply (vcg exspec=branchFlush_modifies)
apply clarsimp
done

6
spec/cspec/Substitute.thy
View File

@ -323,6 +323,11 @@ val guard_htd_updates_with_domain = com_rewrite
\<and> htd_safe domain (hrs_htd (t_hrs_' (globals (f s))))}"}, t))])
else (t, []))
val guard_halt = com_rewrite
(fn t => if t = @{term "halt_'proc"}
then (t, [(@{term DontReach}, @{term "{} :: globals myvars set"})])
else (t, []))
end
*}
@ -336,6 +341,7 @@ SubstituteSpecs.take_all_actions
(fn ctxt => fn s => guard_rewritable_globals NONE ctxt
o (strengthen_c_guards ["memset_body", "memcpy_body", "memzero_body"]
(Proof_Context.theory_of ctxt) s)
o guard_halt
o guard_htd_updates_with_domain)
@{term kernel_all_global_addresses.\<Gamma>}
(CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the)

71
tools/asmrefine/GraphRefine.thy
View File

@ -984,23 +984,6 @@ lemma graph_fun_refines_from_simpl_to_graph:
apply metis
done
lemma simpl_to_graph_call_noreturn:
"(\<exists>ft. \<forall>s xs. (SGamma \<turnstile> \<langle>com.Call p, Normal s\<rangle> \<Rightarrow> xs)
= (xs = Fault ft))
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn
(add_cont (call initf p ret (\<lambda>x y. com.Basic (f x y))) con)
n Q P I eqs out_eqs"
apply (clarsimp simp: call_def block_def)
apply (rule simpl_to_graph_steps_Fault)
apply clarsimp
apply (rule exI)
apply (rule exec_impl_steps_Fault)
apply (rule exec.DynCom exec.Seq exec.CatchMiss exec.Basic)+
apply blast
apply simp
apply (rule exec.FaultProp)
done
lemma simpl_to_graph_name_simpl_state:
"(\<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces {sst} I inp_eqs out_eqs)
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs"
@ -1366,6 +1349,12 @@ lemma word_sless_to_less:
apply (simp add: sint_eq_uint word_msb_sint)
done
lemma word_sle_to_le:
"\<lbrakk> 0 <=s x; 0 <=s y \<rbrakk> \<Longrightarrow> (x <=s y) = (x <= y)"
apply (simp add: word_sle_def word_le_def)
apply (simp add: sint_eq_uint word_msb_sint)
done
lemma unat_ucast_less_helper:
"ucast x < (of_nat n :: word32) \<Longrightarrow> unat (x :: word8) < n"
apply (drule unat_less_helper)
@ -1798,7 +1787,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 (Hints hints) noreturns ctxt =
fun apply_simpl_to_graph_tac funs (Hints hints) ctxt =
simp_tac (simpl_ss ctxt
addsimps @{thms One_nat_def whileAnno_def
creturn_def[folded creturn_void_def]})
@ -1821,8 +1810,6 @@ fun apply_simpl_to_graph_tac funs (Hints hints) noreturns ctxt =
THEN' inst_graph_tac ctxt,
rtac @{thm simpl_to_graph_Basic}
THEN' inst_graph_tac ctxt,
rtac @{thm simpl_to_graph_call_noreturn}
THEN' resolve_tac noreturns,
rtac @{thm simpl_to_graph_call_triv[OF refl]}
THEN' inst_graph_tac ctxt
THEN' apply_graph_refines_ex_tac funs ctxt
@ -1843,11 +1830,11 @@ fun trace_cache _ (SOME thm) = tracing
("Adding thm to cache with " ^ string_of_int (nprems_of thm) ^ " prems.")
| trace_cache _ NONE = tracing "Adding NONE to cache."
fun simpl_to_graph_cache_tac funs noreturns hints cache nm ctxt =
fun simpl_to_graph_cache_tac funs hints cache nm ctxt =
simp_tac (simpl_ss ctxt)
THEN_ALL_NEW DETERM o FIRST' [
SUBGOAL (fn (t, i) => (case
with_cache cache (mk_simpl_to_graph_thm funs noreturns hints cache nm ctxt) (K (K ()))
with_cache cache (mk_simpl_to_graph_thm funs hints cache nm ctxt) (K (K ()))
(simpl_to_graph_skel hints nm (HOLogic.dest_Trueprop
(Logic.strip_assums_concl (Envir.beta_eta_contract t)))) of
SOME thm => rtac thm i | _ => no_tac)
@ -1856,12 +1843,12 @@ fun simpl_to_graph_cache_tac funs noreturns hints cache nm ctxt =
eq_impl_assume_tac ctxt
]
and mk_simpl_to_graph_thm funs noreturns hints cache nm ctxt tm = let
and mk_simpl_to_graph_thm funs 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 hints noreturns ctxt
THEN_ALL_NEW (TRY o simpl_to_graph_cache_tac funs noreturns hints cache nm ctxt)
|> (apply_simpl_to_graph_tac funs hints ctxt
THEN_ALL_NEW (TRY o simpl_to_graph_cache_tac funs hints cache nm ctxt)
THEN_ALL_NEW (TRY o eq_impl_assume_tac ctxt)) 1
|> Seq.hd
|> Drule.generalize ([], ["n", "trS"])
@ -1915,11 +1902,11 @@ fun trace_fail_tac ctxt s = SUBGOAL (fn (t, _) =>
fun trace_fail_tac2 _ = K no_tac
fun simpl_to_graph_tac funs noreturns hints nm ctxt = let
fun simpl_to_graph_tac funs 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
((simpl_to_graph_cache_tac funs hints cache nm ctxt
ORELSE' (etac @{thm use_simpl_to_graph_While_assum}
THEN' simp_tac ctxt)
ORELSE' simpl_to_graph_While_tac hints nm ctxt
@ -1930,13 +1917,12 @@ fun simpl_to_graph_tac funs noreturns hints nm ctxt = let
))
end
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_conts (@{term node.Basic} $ nn $ _) = [nn]
| get_conts (@{term node.Cond} $ l $ _ $ Abs (_, _, @{term True})) = [l]
| get_conts (@{term node.Cond} $ _ $ r $ Abs (_, _, @{term False})) = [r]
| 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_rvals (Abs (_, _, t)) = let
fun inner (Const _ $ (s as (@{term "op # :: char \<Rightarrow> _"} $ _ $ _)) $ Bound 0)
@ -1959,12 +1945,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 norets nodes ep outputs = let
fun get_var_deps 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 norets node)
val conts = map dest_next_node (get_conts 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, [])
@ -1974,7 +1960,7 @@ fun get_var_deps norets 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 norets node)
val conts = map dest_next_node (get_conts node)
val (lvs, rvs) = get_lvals_rvals node
|> pairself (Ord_List.make string_ord)
val cont_vars = maps (Inttab.lookup_list tab) conts
@ -2007,15 +1993,12 @@ fun mk_loop_var_upd_thm ctxt n = let
|> simplify (simpl_ss ctxt addsimps @{thms One_nat_def})
end
fun noreturn_thms_call_names noreturn_thms = []
fun mk_hints (funs : ParseGraph.funs) noreturns ctxt nm = case Symtab.lookup funs nm of
fun mk_hints (funs : ParseGraph.funs) 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 = snd (get_var_deps (Inttab.make nodes) ep outputs)
val deps_hints = nodes
|> map (fst #> ` (Inttab.lookup_list deps
#> filter_out (fn s => String.isSuffix "#count" s)
@ -2054,9 +2037,9 @@ fun eq_impl_unassume_tac t = let
in (* tracing ("Restoring " ^ string_of_int (length hyps) ^ " hyps.") ; *)
fold Thm.implies_intr hyps t |> Seq.single end
fun simpl_to_graph_upto_subgoals funs noreturns hints nm ctxt =
fun simpl_to_graph_upto_subgoals funs hints nm ctxt =
init_graph_refines_proof funs nm ctxt
|> (simpl_to_graph_tac funs noreturns hints nm ctxt 1
|> (simpl_to_graph_tac funs hints nm ctxt 1
THEN ALLGOALS (TRY o REPEAT_ALL_NEW (etac thin_While_assums_rule))
THEN eq_impl_unassume_tac
) |> Seq.hd

45
tools/asmrefine/ProveGraphRefine.thy
View File

@ -137,21 +137,12 @@ lemma ptr_equalities_to_ptr_val:
"(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
lemma unat_ucast_if_up:
"unat (ucast (x :: ('a :: len) word) :: ('b :: len) word)
= (if len_of TYPE('a) \<le> len_of TYPE('b) then unat x else unat x mod 2 ^ len_of TYPE ('b))"
apply (simp, safe intro!: unat_ucast unat_ucast_upcast)
apply (simp add: is_up_def source_size_def target_size_def word_size)
done
ML {*
fun wrap_tac tac i t = let
@ -323,6 +314,7 @@ fun prove_mem_equality ctxt = DETERM o let
array_ptr_index_def
h_val_word32 h_val_ptr
take_heap_list_min drop_heap_list_general
ucast_nat_def[symmetric]
} @ Proof_Context.get_thms ctxt "field_to_bytes_rewrites"
addsimprocs [Word_Bitwise_Tac.expand_upt_simproc]
handle ERROR _ => raise THM
@ -405,7 +397,14 @@ fun unat_mono_tac ctxt = resolve_tac @{thms unat_mono_intro}
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' (asm_full_simp_tac (ctxt addsimps @{thms
word_sless_to_less word_sle_to_le
extra_sle_sless_unfolds
})
THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps @{thms
word_less_nat_alt word_le_nat_alt
unat_ucast_if_up extra_sle_sless_unfolds
})
THEN_ALL_NEW except_tac ctxt "unat_mono_tac: unsolved")
fun tactic_check' (ss, t) = (ss, tactic_check (hd ss) t)
@ -499,30 +498,30 @@ 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
fun simpl_to_graph_thm funs csenv ctxt nm = let
val hints = SimplToGraphProof.mk_hints funs ctxt nm
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs noreturns hints nm
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs 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 *)
(* FIXME: make the hidden assumptions of the thm appear again *)
in res_thm end
fun test_graph_refine_proof funs csenv noreturns ctxt nm = case
fun test_graph_refine_proof funs csenv 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;
in simpl_to_graph_thm funs csenv ctxt nm;
"success on " ^ nm end
fun test_all_graph_refine_proofs_after funs csenv noreturns ctxt nm = let
fun test_all_graph_refine_proofs_after funs csenv 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))
writeln (test_graph_refine_proof funs csenv ctxt s))
handle TERM _ => err s | TYPE _ => err s | THM _ => err s) ss
in "success" end

1
tools/c-parser/CProof.thy
View File

@ -365,6 +365,7 @@ datatype strictc_errortype =
| GhostStateError
| OwnershipError
| UndefinedFunction
| AdditionalError string
lemmas hrs_simps = hrs_mem_update_def hrs_mem_def hrs_htd_update_def
hrs_htd_def