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

isabelle2021-1 c-parser: update CParser + tests 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-11-15 16:17:43 +11:00 committed by Gerwin Klein
parent 0f633ce387
commit ed194a6bc4
7 changed files with 30 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -162,7 +162,7 @@ lemma c_guard_mono:
apply clarsimp
apply(drule_tac p=p in field_tag_sub)
apply(clarsimp simp: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def)
apply(metis (mono_tags, hide_lams) export_size_of subsetD typ_uinfo_t_def)
apply(metis (mono_tags) export_size_of subsetD typ_uinfo_t_def)
done
lemma c_guard_NULL_fl:

2
tools/c-parser/umm_heap/Arrays.thy
View File

@ -77,7 +77,7 @@ lemma finite_index_inj:
lemma forall_finite_index:
"(\<forall>k::'a::finite. P k) = (\<forall>i. i < CARD('a) \<longrightarrow> P (finite_index i))"
by (metis (mono_tags, hide_lams) finite_index_works)
by (metis (mono_tags) finite_index_works)
section \<open>Finite Cartesian Products\<close>

6
tools/c-parser/umm_heap/CTypesBase.thy
View File

@ -319,9 +319,9 @@ lemma intvl_plus_sub_Suc:
lemma intvl_neq_start:
"\<lbrakk> (q::'a::len word) \<in> {p..+n}; p \<noteq> q \<rbrakk> \<Longrightarrow> q \<in> {p + 1..+n - Suc 0}"
by (clarsimp simp: intvl_def)
(metis One_nat_def diff_Suc_1 less_Suc_eq_0_disj less_imp_Suc_add of_nat_Suc take_bit_eq_0_iff
take_bit_of_0)
apply (clarsimp simp: intvl_def)
by (metis One_nat_def Suc_eq_plus1 gr0_conv_Suc less_diff_conv not_gr_zero of_nat_Suc
semiring_1_class.of_nat_0)
lemmas unat_simps' =
word_arith_nat_defs unat_of_nat len_of_addr_card mod_less

15
tools/c-parser/umm_heap/SepCode.thy
View File

@ -93,7 +93,7 @@ lemma singleton_t_dom [simp]:
apply(simp add: ptr_retyp_None)
apply(case_tac "a \<in> {ptr_val p..+size_of TYPE('a)}")
apply(simp add: ptr_retyp_footprint list_map_eq split: if_split_asm)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) word_unat.eq_norm)
apply(subst (asm) mod_less)
@ -170,7 +170,7 @@ lemma ptr_retyp_tagd_exc:
apply(case_tac "a \<in> {ptr_val p..+size_of TYPE('a)}")
apply(subst (asm) ptr_retyp_footprint)
apply simp
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(subst (asm )word_unat.eq_norm)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
@ -188,7 +188,7 @@ lemma ptr_retyp_tagd_exc:
apply(case_tac "a \<in> {ptr_val p..+size_of TYPE('a)}")
apply(subst (asm) ptr_retyp_footprint)
apply simp
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(subst (asm )word_unat.eq_norm)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
@ -197,7 +197,7 @@ lemma ptr_retyp_tagd_exc:
apply(subst (asm) list_map_eq)
apply(clarsimp split: if_split_asm)
apply(drule s_footprintD2)
apply(simp del: unsigned_of_nat)
apply simp
apply(subst (asm) unat_of_nat)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
@ -315,7 +315,7 @@ lemma heap_update_list_value':
apply (simp only: heap_update_list_value addr_card_def card_word)
apply (rule if_cong; simp)
apply (rule iffI)
apply (drule intvlD, clarsimp simp: unat_of_nat simp del: unsigned_of_nat)
apply (drule intvlD, clarsimp simp: unat_of_nat)
apply (simp add: intvl_def unat_arith_simps(4) unat_of_nat split: if_split_asm)
apply (rule_tac x="unat x - unat ptr" in exI, simp)
apply (rule_tac x="unat x + 2^addr_bitsize - unat ptr" in exI)
@ -772,7 +772,6 @@ lemma sep_map_field_unfold:
export_uinfo t = typ_uinfo_t TYPE('b) \<rbrakk> \<Longrightarrow>
(p \<mapsto>\<^sub>g\<^sup>F v) = (p \<mapsto>\<^sub>g\<^sup>({f}\<union>F) (v::'a::mem_type) \<and>\<^sup>*
Ptr (&(p\<rightarrow>f)) \<mapsto>\<^sub>g' ((from_bytes (access_ti\<^sub>0 t v))::'b::mem_type))"
supply unsigned_of_nat[simp del]
apply(rule ext)
apply(rule iffI)
apply(rule_tac s\<^sub>0="x |` (dom x - fs_footprint p {f})" and
@ -1103,7 +1102,7 @@ lemma field_access_update_nth_disjD:
lemma intvl_cut:
"\<lbrakk> (x::addr) \<in> {p..+m}; x \<notin> {p+of_nat k..+n}; m < addr_card \<rbrakk> \<Longrightarrow>
unat (x - p) < k \<or> k + n \<le> unat (x - p)"
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(subst unat_of_nat, subst mod_less, subst len_of_addr_card)
apply(erule (1) less_trans)
apply(subst (asm) unat_of_nat, subst (asm) mod_less, subst len_of_addr_card)
@ -1135,7 +1134,7 @@ lemma singleton_t_mask_out:
apply(rule field_access_update_nth_disjD; simp?)
apply(subst (asm) ptr_retyp_d_eq_fst)
apply(clarsimp simp: empty_htd_def split: if_split_asm)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(subst unat_of_nat)
apply(subst mod_less)
apply(subst len_of_addr_card)

4
tools/c-parser/umm_heap/SepFrame.thy
View File

@ -596,7 +596,7 @@ lemma point_eq_mod_safe_ptr_safe_tag:
k = (\<lambda>s. lift_state (h s,d s));
htd_ind p \<rbrakk> \<Longrightarrow>
point_eq_mod_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m k"
supply if_split_asm[split] unsigned_of_nat[simp del]
supply if_split_asm[split]
apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def)
apply(subgoal_tac "(a,b) \<notin> s_footprint (p (restrict_htd s X))")
prefer 2
@ -644,7 +644,7 @@ proof (simp only: comm_restrict_safe_def comm_restrict_def, auto)
apply(clarsimp simp: map_add_def list_map_eq)
apply(subgoal_tac "(x,SIndexTyp y) \<in> s_footprint (p s)")
apply(fastforce simp: dom_s_def split: if_split_asm)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI; assumption?)
apply(metis len_of_addr_card less_trans max_size mod_less word_unat.eq_norm)
done

2
tools/c-parser/umm_heap/Separation.thy
View File

@ -117,7 +117,7 @@ lemma lift_state_dom:
apply(fastforce dest: s_footprintD intvlD simp: size_of_def)
apply(frule s_footprintD2)
apply(drule s_footprintD)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(drule intvlD, clarsimp)
apply(rename_tac k)
apply(drule_tac x=k in spec)
apply(erule impE)

33
tools/c-parser/umm_heap/TypHeap.thy
View File

@ -286,9 +286,7 @@ lemma typ_slice_t_not_empty [simp]:
lemma list_map_typ_slice_t_not_empty [simp]:
"list_map (typ_slice_t t n) \<noteq> Map.empty"
apply(simp add: list_map_def)
apply(cases "typ_slice_t t n", fastforce)
by (simp add: upt_rec)
by (simp add: list_map_def)
lemma s_footprint:
"s_footprint (p::'a::c_type ptr) =
@ -299,7 +297,7 @@ lemma s_footprint:
lemma ptr_val_SIndexVal_in_s_footprint [simp]:
"(ptr_val p, SIndexVal) \<in> s_footprint (p::'a::mem_type ptr)"
by (force simp: s_footprint)
by (clarsimp simp: s_footprint) (metis Abs_fnat_hom_0 sz_nzero)
lemma s_footprintI:
"\<lbrakk> n < length (typ_slice_t (typ_uinfo_t TYPE('a)) x); x < size_of TYPE('a) \<rbrakk> \<Longrightarrow>
@ -318,7 +316,7 @@ lemma s_footprintD2:
"(x,SIndexTyp n) \<in> s_footprint (p::'a::mem_type ptr) \<Longrightarrow>
n < length (typ_slice_t (typ_uinfo_t TYPE('a)) (unat (x - ptr_val p)))"
by (clarsimp simp: s_footprint)
(metis addr_bitsize_def addr_card less_trans max_size take_bit_nat_eq_self)
(metis len_of_addr_card max_size nat_less_le of_nat_inverse order_less_le_trans)
lemma s_footprint_restrict:
"x \<in> s_footprint p \<Longrightarrow> (s |` s_footprint p) x = s x"
@ -503,7 +501,7 @@ lemma h_t_valid_ptr_safe:
"d,g \<Turnstile>\<^sub>t (p::'a::c_type ptr) \<Longrightarrow> ptr_safe p d"
apply(clarsimp simp: ptr_safe_def h_t_valid_def valid_footprint_def s_footprint_def
s_footprint_untyped_def dom_s_def size_of_def Let_def)
by (metis (mono_tags, hide_lams) domIff list_map map_le_def option.simps(3) surj_pair)
by (metis (mono_tags) domIff list_map map_le_def option.simps(3) surj_pair)
lemma lift_t_ptr_safe:
"lift_t g (h,d) (p::'a::c_type ptr) = Some x \<Longrightarrow> ptr_safe p d"
@ -803,7 +801,7 @@ lemma valid_footprint_neq_nmem:
"\<lbrakk> valid_footprint d p f; valid_footprint d q g; p \<noteq> q; f \<bottom>\<^sub>t g \<or> f=g \<rbrakk> \<Longrightarrow> p \<notin> {q..+size_td g}"
unfolding valid_footprint_def intvl_def Let_def
by clarsimp
(metis add.right_neutral dvd_0_right map_prefix_same_cases semiring_1_class.of_nat_0
(metis add.right_neutral map_prefix_same_cases semiring_1_class.of_nat_0
tag_disj_def tag_disj_prefix typ_slice_0_prefix zero_less_iff_neq_zero)
lemma valid_footprint_sub:
@ -1520,13 +1518,13 @@ lemma lift_t_field_ind:
apply(simp add: size_of_def)
apply(drule td_set_field_lookupD[where k="(c,da)"])
apply(drule td_set_offset_size)
apply (metis (full_types) add.commute add_le_cancel_right le_trans take_bit_nat_less_eq_self)
apply(smt (verit) add.commute add_le_imp_le_right le_trans le_unat_uoi nat_le_linear)
apply(rule intvl_sub_offset)
apply(simp add: size_of_def)
apply(drule td_set_field_lookupD)
apply(drule td_set_offset_size)
by (metis (full_types) add.commute add_le_cancel_right le_trans take_bit_nat_less_eq_self)
apply(smt (verit) add.commute add_le_imp_le_right le_trans le_unat_uoi nat_le_linear)
done
(* case where 'b contains a field of type of 'a *)
@ -1559,8 +1557,9 @@ lemma field_of_t_nmem:
apply(clarsimp simp: field_of_t_def field_of_def intvl_def)
apply(drule td_set_offset_size)
apply(simp add: addr_card_unat_minus size_of_def)
by (metis (no_types) addr_bitsize_def addr_card diff_diff_cancel le_diff_conv le_less_trans
max_size nat_less_le size_of_def take_bit_nat_eq_self_iff)
apply(thin_tac "ptr_val q = x" for x)
by (metis (no_types, opaque_lifting) Nat.add_diff_assoc add.commute le_unat_uoi less_irrefl_nat
linorder_not_le max_size order_less_trans size_of_def trans_less_add1)
lemma field_of_t_init_neq_disjoint:
"field_of_t p (x::'b::mem_type ptr) \<Longrightarrow>
@ -1572,13 +1571,12 @@ lemma field_of_t_init_neq_disjoint:
apply(clarsimp simp: field_of_t_nmem)
apply(drule intvlD)
apply clarsimp
by (meson linorder_not_less take_bit_nat_less_eq_self)
by (metis le_unat_uoi nat_less_le)
lemma field_of_t_final_neq_disjoint:
"field_of_t (p::'a ptr) (x::'b ptr) \<Longrightarrow> {ptr_val p..+size_of TYPE('a::mem_type)} \<inter>
{ptr_val p + of_nat (size_of TYPE('a))..+size_of TYPE('b::mem_type) -
(unat (ptr_val p - ptr_val x) + size_of TYPE('a))} = {}"
supply unsigned_of_nat[simp del]
apply(rule ccontr)
apply(drule intvl_inter)
apply(erule disjE)
@ -2012,7 +2010,7 @@ lemma ptr_retyp_footprint:
apply(subst htd_update_list_index; simp)
apply(subst typ_slices_index; simp?)
apply(drule intvlD, clarsimp)
by (meson le_less_trans take_bit_nat_less_eq_self)
by (metis le_def le_unat_uoi order_less_trans)
lemma ptr_retyp_Some:
"ptr_retyp (p::'a::mem_type ptr) d (ptr_val p) =
@ -2140,7 +2138,7 @@ lemma ptr_retyp_valid_footprint:
apply(subst ptr_retyp_footprint)
apply(rule intvlI)
apply(simp add: size_of_def)
apply(clarsimp simp del: unsigned_of_nat)
apply clarsimp
by (metis (no_types) len_of_addr_card less_trans map_le_map_add max_size of_nat_inverse size_of_def)
lemma ptr_retyp_h_t_valid:
@ -2167,7 +2165,7 @@ lemma ptr_retyp_h_t_valid_same:
apply(erule impE)
apply(simp only: size_of_def [symmetric, where t="TYPE('a)"])
apply(drule intvlD, clarsimp)
apply (meson le_less_trans take_bit_nat_less_eq_self)
apply (simp add: lt_size_of_unat_simps)
apply(fastforce intro: map_add_le_mapI)
done
@ -2238,7 +2236,6 @@ proof -
apply simp
done
from assms show ?thesis
supply unsigned_of_nat[simp del]
apply(clarsimp simp: super_field_update_t_def)
apply(rule ext)
apply(clarsimp simp: field_lvalue_def split: option.splits)