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

isabelle-2021: cparser+tests update 

This includes a tweak to Word_Lib to simplify ucast(-1) which
is now a term that occurs more often.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2021-01-20 16:04:40 +11:00 committed by Gerwin Klein
parent f2fc2345fe
commit 9d7efd75e2
23 changed files with 118 additions and 236 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/Word_Lib/Word_Lemmas.thy
View File

@ -769,7 +769,7 @@ lemma bin_cat_eqD1: "bin_cat a n b = bin_cat c n d \<Longrightarrow> a = c"
lemma bin_cat_eqD2: "bin_cat a n b = bin_cat c n d \<Longrightarrow> bintrunc n b = bintrunc n d"
by (metis take_bit_bin_cat_eq)
lemma bin_cat_inj: "(bin_cat a n b) = bin_cat c n d \<longleftrightarrow> a = c \<and> bintrunc n b = bintrunc n d"
by (auto intro: bin_cat_cong bin_cat_eqD1 bin_cat_eqD2)
@ -867,7 +867,7 @@ lemma word_and_or_mask_aligned:
lemma word_and_or_mask_aligned2:
\<open>is_aligned b n \<Longrightarrow> a \<le> mask n \<Longrightarrow> a + b = a OR b\<close>
using word_and_or_mask_aligned [of b n a] by (simp add: ac_simps)
lemma is_aligned_ucastI:
"is_aligned w n \<Longrightarrow> is_aligned (ucast w) n"
apply transfer
@ -1096,6 +1096,10 @@ lemma scast_1[simp]:
"scast (1 :: 'a :: len signed word) = (1 :: 'a word)"
by simp
lemma unsigned_uminus1 [simp]:
\<open>(unsigned (-1::'b::len word)::'c::len word) = mask LENGTH('b)\<close>
by word_eqI
lemma ucast_ucast_mask_eq:
"\<lbrakk> UCAST('a::len \<rightarrow> 'b::len) x = y; x AND mask LENGTH('b) = x \<rbrakk> \<Longrightarrow> x = ucast y"
by word_eqI_solve
@ -1483,7 +1487,7 @@ lemma is_up_compose:
lemma of_int_sint_scast:
"of_int (sint (x :: 'a :: len word)) = (scast x :: 'b :: len word)"
by (fact Word.of_int_sint)
by (fact Word.of_int_sint)
lemma scast_of_nat_to_signed [simp]:
"scast (of_nat x :: 'a :: len word) = (of_nat x :: 'a signed word)"
@ -1605,7 +1609,7 @@ next
using less_imp_le_nat apply blast
done
qed
lemma scast_ucast_mask_compare:
"scast (ucast w :: 'b::len word) = w
\<longleftrightarrow> (w \<le> mask (LENGTH('b) - 1) \<or> NOT(mask (LENGTH('b) - 1)) \<le> w)"

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

@ -50,7 +50,6 @@ lemma guarded_spec_body_wp [vcg_hoare]:
apply (auto simp: image_def Bex_def)
done
ML_file "tools/mlyacc/mlyacclib/MLY_base-sig.ML"
ML_file "tools/mlyacc/mlyacclib/MLY_join.ML"
ML_file "tools/mlyacc/mlyacclib/MLY_lrtable.ML"

15
tools/c-parser/HPInter.ML
View File

@ -189,7 +189,7 @@ fun mkSpecFunction thy gloc cse styargs (f : fninfo) = let
val speclocalename = Binding.name_of speclocalename_b
(* jump into an lthy corresponding to globloc to parse the tstr; this lthy
is dropped and not used again *)
val lthy = Named_Target.init gloc thy
val lthy = Named_Target.init [] gloc thy
val tm = Syntax.read_term lthy tstr
val (vs, body) = strip_forall tm
val PQopt =
@ -397,7 +397,7 @@ let
fninfo
val name_specs = map (fn {fname,spec,...} => (fname,spec)) fninfo
val thy = List.foldr (uncurry add_syntax) thy name_pars
val lthy = Named_Target.init globloc thy
val lthy = Named_Target.init [] globloc thy
val name_body = compile_fninfos globloc cse styargs compfn lthy fninfo
val _ = Feedback.informStr (0, "Translated all functions")
val globs = extract_fixes globals_elems
@ -409,9 +409,9 @@ let
val _ = Feedback.informStr (0, "Adding body_def for " ^ Binding.name_of (#1 (#1 e)))
in
lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.begin_nested |> snd
|> Local_Theory.define e |> #2
|> Local_Theory.close_target
|> Local_Theory.end_nested
end
in
List.foldl foldthis lthy elems
@ -422,7 +422,7 @@ let
(* set up _impl by defining \<Gamma> *)
val thy =
if List.exists (isSome o #body) fninfo then let
val lthy = Named_Target.init globloc thy
val lthy = Named_Target.init [] globloc thy
fun get_body fni = let
val nm = #fname fni
in
@ -455,7 +455,7 @@ let
val speclocalename = Binding.name_of speclocalename_b
(* jump into an lthy corresponding to globloc to parse the tstr; this lthy
is dropped and not used again *)
val lthy = Named_Target.init globloc thy
val lthy = Named_Target.init [] globloc thy
val t = Syntax.read_term lthy tstr
val _ = Feedback.informStr (0, "Adding spec locale "^speclocalename^
(if speclocalename = "" then "" else " ")^
@ -471,6 +471,7 @@ let
Expression.add_locale
speclocalename_b
speclocalename_b
[]
globloc_expr
[e']
thy
@ -491,7 +492,7 @@ let
List.foldl add_spec_locales (Symtab.empty, thy) name_specs
val (globloc, ctxt) =
Expression.add_locale localename_b localename_b globloc_expr [] thy
Expression.add_locale localename_b localename_b [] globloc_expr [] thy
in
(globloc, Local_Theory.exit_global ctxt)

57
tools/c-parser/PackedTypes.thy
View File

@ -779,10 +779,7 @@ proof (simp add: packed_type_access_ti, rule ext)
from cgrd have al: "ptr_val p \<le> ptr_val p + of_nat (size_of TYPE('b) - 1)" by (rule c_guard_no_wrap)
have szb: "size_of TYPE('b) < 2 ^ len_of TYPE(addr_bitsize)"
apply (fold card_word)
apply (fold addr_card_def)
apply (rule max_size)
done
by (metis len_of_addr_card max_size)
have szt: "n + size_td t \<le> size_of TYPE('b)"
unfolding size_of_def
@ -798,7 +795,7 @@ proof (simp add: packed_type_access_ti, rule ext)
by (rule wf_size_desc_gt)
have uofn: "unat (of_nat n :: addr_bitsize word) = n" using szn szb
by (simp add: nat_less_le unat_of_nat_eq)
by (metis le_unat_uoi nat_less_le unat_of_nat_len)
from eu have std: "size_td t = size_of TYPE('a)" using fl
by (simp add: export_size_of)
@ -814,17 +811,10 @@ proof (simp add: packed_type_access_ti, rule ext)
have "c_guard (Ptr &(p\<rightarrow>f) :: 'a ptr)" using cgrd fl eu
by (rule c_guard_field_lvalue)
hence pft: "&(p\<rightarrow>f) \<le> &(p\<rightarrow>f) + of_nat (size_td t - 1)"
apply -
apply (drule c_guard_no_wrap)
apply (simp add: std)
done
by (metis c_guard_no_wrap ptr_val.ptr_val_def std)
have szt': "size_td t < 2 ^ len_of TYPE(addr_bitsize)"
apply (subst std)
apply (fold card_word)
apply (fold addr_card_def)
apply (rule max_size)
done
by (metis len_of_addr_card max_size std)
have ofn: "of_nat n \<le> x - ptr_val p"
proof (rule le_minus')
@ -833,36 +823,23 @@ proof (simp add: packed_type_access_ti, rule ext)
by (rule intvl_le_lower)
next
from szb szn have "of_nat n \<le> (of_nat (size_of TYPE('b) - 1) :: addr_bitsize word)"
apply -
apply (rule of_nat_mono_maybe_le)
apply simp_all
done
by (metis One_nat_def of_nat_mono_maybe_le b0 less_imp_diff_less nat_le_Suc_less)
with al show "ptr_val p \<le> ptr_val p + of_nat n"
by (rule word_plus_mono_right2)
qed
thus nlt: "n \<le> unat (x - ptr_val p)"
by (simp add: word_le_nat_alt uofn)
by (metis uofn word_le_nat_alt)
have "x \<le> ptr_val p + (of_nat n + of_nat (size_td t - 1))" using xin pft szt' t0
unfolding field_lvalue_def field_lookup_offset_eq [OF fl]
apply -
apply (drule (2) intvl_less_upper)
apply (simp add: add.assoc)
done
by (metis (no_types) add.assoc intvl_less_upper)
moreover have "x \<in> {ptr_val p..+size_of TYPE('b)}" using fl xin
by (rule subsetD [OF field_tag_sub])
ultimately have "x - ptr_val p \<le> (of_nat n + of_nat (size_td t - 1))" using al szb
apply -
apply (rule word_diff_ls(4)[where xa=x and x=x for x, simplified])
apply (metis (hide_lams, mono_tags) add.commute of_nat_add)
apply (erule (2) intvl_le_lower)
done
by (metis add_diff_cancel_left' intvl_le_lower word_diff_ls(4))
moreover have "unat (of_nat n + of_nat (size_td t - 1) :: addr_bitsize word) = n + size_td t - 1"
using t0 order_le_less_trans [OF szt1 szb]
apply (subst Abs_fnat_homs(1))
apply (subst unat_of_nat)
apply simp
done
by (metis Nat.add_diff_assoc One_nat_def Suc_leI of_nat_add unat_of_nat_len)
ultimately have "unat (x - ptr_val p) \<le> n + size_td t - 1"
by (simp add: word_le_nat_alt)
thus "unat (x - ptr_val p) < n + size_td t" using t0
@ -884,7 +861,7 @@ proof (simp add: packed_type_access_ti, rule ext)
have "unat (x - &(p\<rightarrow>f)) = unat ((x - ptr_val p) - of_nat n)"
by (simp add: field_lvalue_def field_lookup_offset_eq [OF fl])
also have "\<dots> = unat (x - ptr_val p) - n"
by (simp add: unat_sub [OF ofn] uofn)
by (metis ofn unat_sub uofn)
finally have "unat (x - &(p\<rightarrow>f)) = unat (x - ptr_val p) - n" .
thus "access_ti (typ_info_t TYPE('a)) v (replicate (size_of TYPE('a)) 0) ! unat (x - &(p\<rightarrow>f)) =
@ -919,15 +896,12 @@ proof (simp add: packed_type_access_ti, rule ext)
by (rule intvl_le_lower)
qed
thus unx: "unat (x - ptr_val p) < size_td (typ_info_t TYPE('b))" using szb b0
by (simp add: word_le_nat_alt size_of_def unat_of_nat)
by (metis (no_types) One_nat_def Suc_leI le_m1_iff_lt of_nat_1 of_nat_diff of_nat_mono_maybe
semiring_1_class.of_nat_0 size_of_def unat_less_helper)
show "unat (x - ptr_val p) < n - 0 \<or> n - 0 + size_td t \<le> unat (x - ptr_val p)" using xin xni
unfolding field_lvalue_def field_lookup_offset_eq [OF fl]
apply -
apply (erule intvl_cut)
apply simp
apply (rule max_size)
done
using intvl_cut by auto
show "wf_fd (typ_info_t TYPE('b))" by (rule wf_fd)
(* clag *)
@ -939,10 +913,7 @@ proof (simp add: packed_type_access_ti, rule ext)
by (simp add: size_of_def)
have "heap_list hp (size_td (typ_info_t TYPE('b))) (ptr_val p) ! unat (x - ptr_val p) = hp x"
apply (subst heap_list_nth)
apply (rule unx)
apply simp
done
by (subst heap_list_nth, rule unx) simp
thus "access_ti (typ_info_t TYPE('b)) (h_val hp p) (replicate (size_of TYPE('b)) 0) ! unat (x - ptr_val p) = hp x"
unfolding h_val_def

8
tools/c-parser/expression_translation.ML
View File

@ -245,9 +245,9 @@ in
val oldity = TermsTypes.IntInfo.ity2wty oldty
val newity = TermsTypes.IntInfo.ity2wty newty
fun tf t = if is_signed oldty then
Const(@{const_name "scast"}, oldity --> newity) $ t
Const(@{const_name "signed"}, oldity --> newity) $ t
else
Const(@{const_name "ucast"}, oldity --> newity) $ t
Const(@{const_name "unsigned"}, oldity --> newity) $ t
(* strictly, "overflow" here results in an implementation-defined value, or an
"implementation-defined signal" (???) [6.3.1.3].
@ -588,7 +588,7 @@ in
end
in
if is_result_signed (ei1, ei2) then
add_guard div_zero_check (check_signed_binop(@{const_name "sdiv"}, mk_sdiv, ei1, ei2))
add_guard div_zero_check (check_signed_binop(@{const_name "signed_divide"}, mk_sdiv, ei1, ei2))
else
add_guard div_zero_check (mk_arithop(@{const_name "divide"}, ei1, ei2))
end
@ -600,7 +600,7 @@ in
end
in
if is_result_signed (ei1, ei2) then
add_guard div_zero_check (check_signed_binop(@{const_name "smod"}, mk_smod, ei1, ei2))
add_guard div_zero_check (check_signed_binop(@{const_name "signed_modulo"}, mk_smod, ei1, ei2))
else
add_guard div_zero_check (mk_arithop(@{const_name "modulo"}, ei1, ei2))
end

4
tools/c-parser/isa_termstypes.ML
View File

@ -612,12 +612,12 @@ end
fun mk_sdiv(t1,t2) = let
val ty = type_of t1
in
Const(@{const_name "sdiv"}, ty --> ty --> ty) $ t1 $ t2
Const(@{const_name "signed_divide"}, ty --> ty --> ty) $ t1 $ t2
end
fun mk_smod(t1,t2) = let
val ty = type_of t1
in
Const(@{const_name "smod"}, ty --> ty --> ty) $ t1 $ t2
Const(@{const_name "signed_modulo"}, ty --> ty --> ty) $ t1 $ t2
end
fun mk_uminus t = let

8
tools/c-parser/isar_install.ML
View File

@ -180,10 +180,10 @@ fun define_function_names fninfo thy = let
val b = Binding.name cname
val ((_, (_, th)), lthy) =
lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.begin_nested |> snd
|>Local_Theory.define ((b, NoSyn),
((Thm.def_binding b, []), mk_int_numeral n))
val lthy' = Local_Theory.close_target lthy
val lthy' = Local_Theory.end_nested lthy
val morph = Proof_Context.export_morphism lthy lthy'
val th' = Morphism.thm morph th
@ -213,7 +213,7 @@ end
fun define_global_initializers globloc msgpfx name_munger mungedb cse globs thy = let
open ProgramAnalysis Absyn
val lthy = Named_Target.init globloc thy
val lthy = Named_Target.init [] globloc thy
val globinits = let
val inittab = get_globinits cse
fun foldthis (gnm : MString.t, gty) defs = let
@ -364,7 +364,7 @@ in
state {owners=owners,gstate_ty=gstate_ty,mstate_ty=mstate_ty} thy
val loc_b = Binding.name (suffix HPInter.globalsN localename)
val (globloc, ctxt) =
Expression.add_locale loc_b loc_b ([], []) globs thy
Expression.add_locale loc_b loc_b [] ([], []) globs thy
val thy = Local_Theory.exit_global ctxt
val _ = Output.state ("Created locale for globals (" ^ Binding.print loc_b ^
")- with " ^ Int.toString (length globs) ^

6
tools/c-parser/modifies_proofs.ML
View File

@ -429,12 +429,12 @@ end
fun prove_all_modifies_goals thy csenv includeP tyargs globloc =
if Config.get_global thy calculate_modifies_proofs then
let
val lthy = Named_Target.init globloc thy
val lthy = Named_Target.init [] globloc thy
in
lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.begin_nested |> snd
|> prove_all_modifies_goals_local csenv includeP tyargs
|> Local_Theory.close_target
|> Local_Theory.end_nested
|> Local_Theory.exit_global
end
else

6
tools/c-parser/termstypes.ML
View File

@ -60,7 +60,7 @@ in
Const("Word.unat", ty --> nat) $ t
end
fun mk_i2w_t rty = Const(@{const_name "Word.word_of_int"},
fun mk_i2w_t rty = Const(@{const_name "of_int"},
int --> rty)
fun mk_lshift(t1 : term, t2 : term) : term =
@ -73,10 +73,10 @@ fun mk_rshift(t1, t2) =
fun mk_w2ui t =
Const(@{const_name "Word.uint"}, type_of t --> int) $ t
Const(@{const_name "Word.unsigned"}, type_of t --> int) $ t
fun mk_w2si t =
Const(@{const_name "Word.sint"}, type_of t --> int) $ t
Const(@{const_name "Word.signed"}, type_of t --> int) $ t
(* ----------------------------------------------------------------------

11
tools/c-parser/testfiles/factorial.thy
View File

@ -47,11 +47,7 @@ lemma fac_list_length [simp]:
lemma fac_list_unfold:
"unat n \<noteq> 0 \<Longrightarrow> fac_list (unat n) = fac (unat n) # fac_list (unat (n - 1))"
apply(case_tac "unat n")
apply clarsimp
apply(subst unat_minus_one)
apply clarsimp+
done
by (metis Suc_unat_minus_one fac_list.simps(2) unat_eq_zero)
primrec
sep_list :: "machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> heap_assert"
@ -333,9 +329,6 @@ lemma (in factorial_global_addresses) mem_safe_factorial:
apply(simp_all add: restrict_map_def call_def block_def whileAnno_def
free_body_def alloc_body_def factorial_body_def creturn_def
split: if_split_asm option.splits)
apply((erule disjE)?, simp,
(thin_tac "C=x" for x, (thin_tac "\<Gamma> x = y" for x y)+,
force simp: intra_sc)?)+
done
by (force simp: intra_sc)
end

4
tools/c-parser/testfiles/globals_fn.thy
View File

@ -27,8 +27,6 @@ end
lemma (in globals_fn_global_addresses) returns40:
"\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== PROC test2() \<lbrace> \<acute>ret__int = 40 \<rbrace>"
apply vcg
apply unat_arith
done
by vcg simp
end

18
tools/c-parser/testfiles/longlong.thy
View File

@ -13,7 +13,6 @@ install_C_file "longlong.c"
ML \<open>NameGeneration.return_var_name (Absyn.Signed Absyn.LongLong)\<close>
context longlong
begin
@ -22,17 +21,16 @@ thm shifts1_body_def
thm shifts2_body_def
lemma "(ucast :: 16 word \<Rightarrow> 8 word) 32768 = 0"
apply simp
done
by simp
lemma "(scast :: 16 word \<Rightarrow> 8 word) 32768 = 0"
by simp
by simp
lemma "(scast :: 16 word \<Rightarrow> 8 word) 65535 = 255"
by simp
by simp
lemma "(ucast :: 16 word \<Rightarrow> 8 word) 65535 = 255"
by simp
by simp
lemma "(ucast :: 16 word \<Rightarrow> 8 word) 32767 = 255" by simp
lemma "(scast :: 16 word \<Rightarrow> 8 word) 32767 = 255" by simp
@ -42,17 +40,13 @@ lemma "(ucast :: 8 word \<Rightarrow> 16 word) 255 = 255" by simp
lemma g_result:
"\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== CALL callg() \<lbrace> \<acute>ret__int = 0 \<rbrace>"
apply vcg
apply (simp add: max_word_def)
done
by vcg (simp add: mask_def)
thm literals_body_def
lemma literals_result:
"\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== CALL literals() \<lbrace> \<acute>ret__int = 31 \<rbrace>"
apply vcg
apply simp
done
by vcg simp
end (* context *)

2
tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy
View File

@ -5,7 +5,7 @@
*)
theory Word_Mem_Encoding
imports Vanilla32_Preliminaries
imports Vanilla32_Preliminaries "Word_Lib.Rsplit"
begin
(* Little-endian encoding *)

3
tools/c-parser/umm_heap/ArrayAssertion.thy
View File

@ -137,8 +137,7 @@ lemma ptr_add_assertion_uint[simp]:
"ptr_add_assertion ptr (uint offs) strong htd
= (offs = 0 \<or> array_assertion ptr
(case strong of True \<Rightarrow> Suc (unat offs) | False \<Rightarrow> unat offs) htd)"
by (simp add: ptr_add_assertion_positive uint_0_iff unat_def
split: bool.split)
by (metis ptr_add_assertion_positive uint_nonnegative unat_def unsigned_eq_0_iff)
text \<open>Ignore char and void pointers. The C standard specifies that arithmetic on
char and void pointers doesn't create any special checks.\<close>

9
tools/c-parser/umm_heap/CTypes.thy
View File

@ -1791,7 +1791,7 @@ lemma fi_fa_consistentD:
lemma length_super_update_bs [simp]:
"n + length v \<le> length bs \<Longrightarrow> length (super_update_bs v bs n) = length bs"
by (clarsimp simp: super_update_bs_def)
unfolding super_update_bs_def by simp
lemma drop_super_update_bs:
"\<lbrakk> k \<le> n; n \<le> length bs \<rbrakk> \<Longrightarrow> drop k (super_update_bs v bs n) = super_update_bs v (drop k bs) (n - k)"
@ -2202,10 +2202,7 @@ lemma final_intvl_disj:
apply clarsimp
apply(case_tac q; simp)
apply(drule intvlD, clarsimp)
apply(subst (asm) word_unat.norm_eq_iff [symmetric])
apply(subst (asm) len_of_addr_card)
apply simp
done
by (metis add.commute add_leD1 len_of_addr_card less_trans nat_less_le of_nat_inverse)
lemma fa_fu_lookup_disj_inter:
"\<forall>f m d n f' d' n'. field_lookup t f m = Some (d,n) \<longrightarrow>
@ -2309,7 +2306,7 @@ proof -
have "int (align_of TYPE('a)) dvd (i * int (size_of TYPE('a)))"
by (simp add: align_size_of)
with aligned show ?thesis
apply (case_tac p, simp add: ptr_aligned_def ptr_add_def scast_id)
apply (case_tac p, simp add: ptr_aligned_def ptr_add_def)
apply (simp only: unat_simps len_signed)
apply (metis align align_size_of dvd_add dvd_mod dvd_mult2 mult.commute)
done

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

@ -324,20 +324,19 @@ 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 (no_types) Suc_diff_1 add.commute add_Suc_right diff_diff_left neq0_conv
of_nat_Suc semiring_1_class.of_nat_0 zero_less_diff)
(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)
lemmas unat_simps' =
word_arith_nat_defs word_unat.eq_norm len_of_addr_card mod_less
word_arith_nat_defs unat_of_nat len_of_addr_card mod_less
lemma intvl_offset_nmem:
"\<lbrakk> q \<in> {(p::'a::len word)..+unat x}; y \<le> 2^len_of TYPE('a) - unat x \<rbrakk> \<Longrightarrow>
q \<notin> {p + x..+y}"
apply (clarsimp simp: intvl_def)
apply (simp only: unat_simps')
apply (subst (asm) word_unat.Abs_inject)
apply (auto simp: unats_def)
done
apply (subst (asm) word_of_nat_eq_iff)
using take_bit_nat_eq_self by auto
lemma intvl_Suc_nmem' [simp]:
"n < 2^len_of TYPE('a) \<Longrightarrow> (p::'a::len word) \<notin> {p + 1..+n - Suc 0}"
@ -353,9 +352,9 @@ lemma intvl_sub_eq:
shows "{p + x..+unat (y - x)} = {p..+unat y} - {p..+unat x}"
proof -
have "unat y - unat x \<le> 2 ^ len_of TYPE('a) - unat x"
by (insert unat_lt2p [of y], arith)
by (meson diff_le_mono less_or_eq_imp_le unsigned_less)
moreover have "x \<le> y" by fact
moreover hence "unat (y - x) = unat y - unat x"
moreover from this have "unat (y - x) = unat y - unat x"
by (simp add: word_le_nat_alt, unat_arith)
ultimately show ?thesis
by (force dest: intvl_offset_nmem intvl_mem_offset elim: intvl_plus_sub_offset

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

@ -439,7 +439,7 @@ where
lemma ptr_add_def':
"ptr_add (Ptr p :: ('a::c_type) ptr) n
= (Ptr (p + of_int n * of_nat (size_of TYPE('a))))"
by (cases p, auto simp: ptr_add_def scast_id)
by (cases p, auto simp: ptr_add_def)
definition
ptr_sub :: "('a::c_type) ptr \<Rightarrow> ('a::c_type) ptr \<Rightarrow> 32 signed word" (infixl "-\<^sub>p" 65)

3
tools/c-parser/umm_heap/CompoundCTypes.thy
View File

@ -431,9 +431,6 @@ lemma fu_eq_mask_ti_typ_combine:
apply(rename_tac xs')
apply(clarsimp simp: fu_eq_mask_def update_ti_adjust_ti)
apply(clarsimp simp: update_ti_list_t_def size_of_def)
apply(rule conjI; clarsimp)
prefer 2
apply fastforce
apply(subst upd [where w="f undefined"])
apply(simp add: size_of_def)
apply(subst upd [where w="f undefined" and v="f (h v')" for v'])

16
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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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
apply(simp del: unsigned_of_nat)
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 add: unat_of_nat)
apply (drule intvlD, clarsimp simp: unat_of_nat simp del: unsigned_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)
@ -607,7 +607,6 @@ lemma field_access_take_drop:
apply(induct t and st and ts and x, all \<open>clarsimp simp: access_ti\<^sub>0_def\<close>)
apply(fastforce dest: wf_fd_cons_structD
simp: fd_cons_struct_def fd_cons_desc_def fd_cons_length_def)
apply(clarsimp simp: min_def)
apply(drule wf_fd_cons_pairD)
apply(clarsimp simp: fd_cons_pair_def fd_cons_desc_def fd_cons_length_def)
apply(clarsimp split: option.splits)
@ -773,6 +772,7 @@ 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 +1103,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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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 +1135,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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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]
supply if_split_asm[split] unsigned_of_nat[simp del]
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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
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)
apply(drule intvlD, clarsimp simp del: unsigned_of_nat)
apply(rename_tac k)
apply(drule_tac x=k in spec)
apply(erule impE)

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

@ -253,7 +253,7 @@ lemma wf_heap_val_SIndexVal_STyp_simp [simp]:
apply(clarsimp simp: wf_heap_val_def)
apply(drule_tac x=x in spec)
apply clarsimp
apply(case_tac t, simp)
apply(cases t, simp)
apply fast
done
@ -282,12 +282,12 @@ lemma field_tag_sub:
lemma typ_slice_t_not_empty [simp]:
"typ_slice_t t n \<noteq> []"
by (case_tac t, simp)
by (cases t, 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(case_tac "typ_slice_t t n", fastforce)
apply(cases "typ_slice_t t n", fastforce)
by (simp add: upt_rec)
lemma s_footprint:
@ -299,24 +299,16 @@ lemma s_footprint:
lemma ptr_val_SIndexVal_in_s_footprint [simp]:
"(ptr_val p, SIndexVal) \<in> s_footprint (p::'a::mem_type ptr)"
apply(simp add: s_footprint)
apply(rule_tac x=0 in exI)
by auto
by (force simp: s_footprint)
lemma s_footprintI:
"\<lbrakk> n < length (typ_slice_t (typ_uinfo_t TYPE('a)) x); x < size_of TYPE('a) \<rbrakk> \<Longrightarrow>
(ptr_val p + of_nat x, SIndexTyp n) \<in> s_footprint (p::'a::c_type ptr)"
apply(simp add: s_footprint)
apply(rule_tac x=x in exI)
apply auto
done
by (auto simp: s_footprint)
lemma s_footprintI2:
"x < size_of TYPE('a) \<Longrightarrow> (ptr_val p + of_nat x, SIndexVal) \<in> s_footprint (p::'a::c_type ptr)"
apply(simp add: s_footprint)
apply(rule_tac x=x in exI)
apply auto
done
by (auto simp: s_footprint)
lemma s_footprintD:
"(x,k) \<in> s_footprint p \<Longrightarrow> x \<in> {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)}"
@ -325,14 +317,8 @@ lemma s_footprintD:
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)))"
apply(clarsimp simp: s_footprint)
apply(subst word_unat.eq_norm)
apply(subst mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply(rule max_size)
apply simp
done
by (clarsimp simp: s_footprint)
(metis len32 len_of_addr_card less_trans max_size take_bit_nat_eq_self_iff)
lemma s_footprint_restrict:
"x \<in> s_footprint p \<Longrightarrow> (s |` s_footprint p) x = s x"
@ -469,7 +455,7 @@ lemma lift_state_proj [simp]:
lemma lift_state_Some:
"lift_state (h,d) (p,SIndexTyp n) = Some t \<Longrightarrow> snd (d p) n = Some (s_heap_tag t)"
apply (simp add: lift_state_def split: option.splits split: if_split_asm)
apply (case_tac t; simp)
apply (cases t; simp)
done
lemma lift_state_Some2:
@ -814,22 +800,11 @@ lemma tag_prefix_True:
done
lemma valid_footprint_neq_nmem:
assumes valid_p: "valid_footprint d p f" and
valid_q: "valid_footprint d q g" and
neq: "p \<noteq> q" and
disj: "f \<bottom>\<^sub>t g \<or> f=g"
shows "p \<notin> {q..+size_td g}" (is ?G)
proof -
from assms show ?thesis
apply(clarsimp simp: valid_footprint_def intvl_def Let_def)
apply(erule disjE)
apply(drule_tac x=0 in spec)
apply (fastforce dest: map_prefix_same_cases)
apply(drule_tac x=0 in spec)
apply(drule_tac x=k in spec)
apply clarsimp
by (meson of_nat_gt_0 typ_slice_0_prefix map_prefix_same_cases)
qed
"\<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
tag_disj_def tag_disj_prefix typ_slice_0_prefix zero_less_iff_neq_zero)
lemma valid_footprint_sub:
assumes valid_p: "valid_footprint d p s"
@ -849,18 +824,9 @@ proof -
apply clarsimp
apply(drule (1) map_prefix_same_cases)
apply(erule disjE)
prefer 2
apply(frule typ_slice_sub)
apply(subgoal_tac "k = 0")
prefer 2
apply(rule ccontr, simp)
apply(simp add: typ_slice_0_prefix)
apply simp
(* given by the fd_tag_consistent condition *)
apply(drule typ_slice_True_prefix)
apply(clarsimp simp: field_of_def)
apply(simp only: unat_simps)
done
apply(drule typ_slice_True_prefix)
apply(metis field_of_def len_of_addr_card less_le_trans of_nat_inverse)
by (metis field_of_self le_less semiring_1_class.of_nat_0 tag_prefix_True typ_slice_sub)
qed
lemma valid_footprint_sub2:
@ -1554,21 +1520,14 @@ 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(subst word_unat.eq_norm)
apply(subst len_of_addr_card)
apply(subst mod_less)
apply (metis add_leD2 le_trans max_size not_le size_of_def)
apply fastforce
apply (metis add.commute add_leD1 len32 len_of_addr_card less_le_trans max_size nat_less_le
size_of_def take_bit_nat_eq_self_iff)
apply(rule intvl_sub_offset)
apply(simp add: size_of_def)
apply(drule td_set_field_lookupD)
apply(drule td_set_offset_size)
apply(subst word_unat.eq_norm)
apply(subst len_of_addr_card)
apply(subst mod_less)
apply (metis le_Suc_ex le_add2 max_size not_le size_of_def trans_le_add1)
apply simp
done
by (metis add.commute len32 len_of_addr_card less_le_trans max_size nat_le_iff_add nat_less_le
size_of_def take_bit_nat_eq_self_iff)
@ -1593,34 +1552,18 @@ lemma field_of_t_less_size:
apply(simp add: size_of_def [symmetric, where t="TYPE('a)"])
done
lemma unat_minus:
"x \<noteq> 0 \<Longrightarrow> unat (- (x::addr)) = addr_card - unat x"
apply(simp add: unat_def)
apply(subst uint_word_ariths)
apply(subst zmod_zminus1_eq_if)
apply(simp split: if_split_asm)
apply(rule conjI; clarsimp)
apply(fastforce simp: uint_0_iff word_uint.inverse_norm dest: word_uint.Rep_inverse')
apply(simp add: nat_diff_distrib addr_card)
apply(subst mod_pos_pos_trivial; simp?)
apply(rule order_less_le_trans, rule uint_lt2p)
apply simp
done
lemma addr_card_unat_minus:
"x \<noteq> 0 \<Longrightarrow> unat (- x) = addr_card - unat x" for x::"32 word"
by (simp add: unat_minus addr_card word_size)
lemma field_of_t_nmem:
"\<lbrakk> field_of_t p q; ptr_val p \<noteq> ptr_val (q::'b::mem_type ptr) \<rbrakk> \<Longrightarrow>
ptr_val q \<notin> {ptr_val (p::'a::mem_type ptr)..+size_of TYPE('a)}"
apply(clarsimp simp: field_of_t_def field_of_def intvl_def)
apply(drule td_set_offset_size)
apply(simp add: unat_minus size_of_def)
apply(subgoal_tac "size_td (typ_info_t TYPE('b)) < addr_card")
apply(simp only: unat_simps)
apply(subst (asm) mod_less; simp)
apply(simp flip: size_of_def [where t="TYPE('a)"])
apply(erule less_trans)
apply simp
apply(simp flip: size_of_def[where t="TYPE('b)"])
done
apply(simp add: addr_card_unat_minus size_of_def)
by (metis (no_types) Nat.add_diff_assoc add.commute add_leD1 len32 len_of_addr_card less_trans
max_size nat_less_le size_of_def take_bit_nat_eq_self_iff)
lemma field_of_t_init_neq_disjoint:
"field_of_t p (x::'b::mem_type ptr) \<Longrightarrow>
@ -1629,13 +1572,16 @@ lemma field_of_t_init_neq_disjoint:
apply(cases "ptr_val p = ptr_val x", simp)
apply(rule ccontr)
apply(drule intvl_inter)
apply(fastforce simp: field_of_t_nmem le_unat_uoi nat_less_le dest: intvlD)
done
apply(clarsimp simp: field_of_t_nmem)
apply(drule intvlD)
apply clarsimp
by (meson linorder_not_less take_bit_nat_less_eq_self)
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)
@ -1961,11 +1907,7 @@ lemma dom_tll_cons [simp]:
"dom_tll p (x#xs) = dom_tll (p + 1) xs \<union> {(p,SIndexVal)} \<union> {(p,SIndexTyp n) | n. x n \<noteq> None}"
unfolding dom_tll_def
apply (rule equalityI; clarsimp)
apply (rule conjI; clarsimp)
apply (metis (no_types) One_nat_def Suc_pred add_cancel_right_right less_Suc_eq less_trans
neq0_conv of_nat_1 of_nat_Suc)
apply (metis (no_types) One_nat_def Suc_less_eq Suc_pred not_gr_zero nth_Cons_0 nth_Cons_pos
of_nat_Suc semiring_1_class.of_nat_0 surj_pair)
subgoal using less_Suc_eq_0_disj by force
apply (rule conjI, force)+
apply force
done
@ -2073,13 +2015,7 @@ lemma ptr_retyp_footprint:
apply(subst htd_update_list_index; simp)
apply(subst typ_slices_index; simp?)
apply(drule intvlD, clarsimp)
apply(subst unat_simps)
apply(subst mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply(rule max_size)
apply simp
done
by (meson le_less_trans take_bit_nat_less_eq_self)
lemma ptr_retyp_Some:
"ptr_retyp (p::'a::mem_type ptr) d (ptr_val p) =
@ -2207,15 +2143,8 @@ lemma ptr_retyp_valid_footprint:
apply(subst ptr_retyp_footprint)
apply(rule intvlI)
apply(simp add: size_of_def)
apply clarsimp
apply(subst unat_of_nat)
apply(subst mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply(subst size_of_def [symmetric, where t="TYPE('a)"])
apply(rule max_size)
apply simp
done
apply(clarsimp simp del: unsigned_of_nat)
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:
"g p \<Longrightarrow> ptr_retyp p d,g \<Turnstile>\<^sub>t (p::'a::mem_type ptr)"
@ -2241,7 +2170,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(simp only: lt_size_of_unat_simps)
apply (meson le_less_trans take_bit_nat_less_eq_self)
apply(fastforce intro: map_add_le_mapI)
done
@ -2312,6 +2241,7 @@ 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)

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

@ -7,7 +7,7 @@
(* License: BSD, terms see file ./LICENSE *)
theory Vanilla32
imports Word_Mem_Encoding "Word_Lib.Word_Lib" CTypes
imports Word_Mem_Encoding "Word_Lib.Word_Lib_Sumo" CTypes
begin