diff --git a/lib/WordLib.thy b/lib/WordLib.thy index 6bb767bb3..872628e82 100644 --- a/lib/WordLib.thy +++ b/lib/WordLib.thy @@ -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. diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index c230661e2..3a60d9472 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -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))) \ 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) *}) diff --git a/proof/crefine/CSpace_C.thy b/proof/crefine/CSpace_C.thy index 75a4fab70..69fc28633 100644 --- a/proof/crefine/CSpace_C.thy +++ b/proof/crefine/CSpace_C.thy @@ -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 \ ccap_relation) deriveCap_xf (invs') (UNIV \ {s. ccap_relation cap (cap_' s)} \ {s. slot_' s = Ptr slot}) [] diff --git a/proof/crefine/Fastpath_C.thy b/proof/crefine/Fastpath_C.thy index abf16890d..5c647b92e 100644 --- a/proof/crefine/Fastpath_C.thy +++ b/proof/crefine/Fastpath_C.thy @@ -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 (\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=\ 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 (\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=\ 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=\ 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=\ 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) diff --git a/proof/crefine/Finalise_C.thy b/proof/crefine/Finalise_C.thy index fa45914d7..0129cb0da 100644 --- a/proof/crefine/Finalise_C.thy +++ b/proof/crefine/Finalise_C.thy @@ -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) diff --git a/proof/crefine/Machine_C.thy b/proof/crefine/Machine_C.thy index d259a5578..3a2cef807 100644 --- a/proof/crefine/Machine_C.thy +++ b/proof/crefine/Machine_C.thy @@ -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 diff --git a/spec/cspec/Substitute.thy b/spec/cspec/Substitute.thy index b4b21ea9e..1935d4a55 100644 --- a/spec/cspec/Substitute.thy +++ b/spec/cspec/Substitute.thy @@ -323,6 +323,11 @@ val guard_htd_updates_with_domain = com_rewrite \ 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.\} (CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the) diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index 4caa4ee22..c85ca7441 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -984,23 +984,6 @@ lemma graph_fun_refines_from_simpl_to_graph: apply metis done -lemma simpl_to_graph_call_noreturn: - "(\ft. \s xs. (SGamma \ \com.Call p, Normal s\ \ xs) - = (xs = Fault ft)) - \ simpl_to_graph SGamma GGamma gf nn - (add_cont (call initf p ret (\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: "(\sst. sst \ P \ simpl_to_graph SGamma GGamma gf nn com n traces {sst} I inp_eqs out_eqs) \ 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: + "\ 0 <=s x; 0 <=s y \ \ (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) \ 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 \ _"} $ _ $ _)) $ 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 diff --git a/tools/asmrefine/ProveGraphRefine.thy b/tools/asmrefine/ProveGraphRefine.thy index 6c8366ee5..94e84ffb0 100644 --- a/tools/asmrefine/ProveGraphRefine.thy +++ b/tools/asmrefine/ProveGraphRefine.thy @@ -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) \ 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 diff --git a/tools/c-parser/CProof.thy b/tools/c-parser/CProof.thy index d453611b3..0ccc25ed2 100644 --- a/tools/c-parser/CProof.thy +++ b/tools/c-parser/CProof.thy @@ -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