Support extra specs, ctzl, clzl in SimplExport.
This patch permits the user to supply additional specs for functions whose bodies were not imported (DONT_TRANSLATE or not present in parsed C source). Those specs are exported by SimplExport. The existing apparatus can import builtin functions like ctzl/clzl in C sources by admitting them without bodies (DONT_TRANSLATE) and giving them axiomatic Hoare triples (FNSPEC). Translation validation then requires export of useful semantics. The user can supply a made-up body, and show that it is a refinement of the body that the parser created (derived from the FNSPEC and MODIFIES clauses). The body must export out the graph language correctly. For ctzl/clzl etc this is easy.
This commit is contained in:
Thomas Sewell
parent
6cda8f50d0
commit
971c6782e5
|
|
@ -66,31 +66,8 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
|
|||
"snd (snd ((if P then f else g) gs)) = (if P then snd (snd (f gs)) else snd (snd (g gs)))"
|
||||
by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
|
||||
|
||||
ML {* val nm = "Kernel_C.invert_l1index" *}
|
||||
|
||||
(*
|
||||
|
||||
(* If test_all_graph_refine_proofs_parallel fails, debug it by uncommenting this comment block
|
||||
and setting "nm" to the failed C function. *)
|
||||
|
||||
local_setup {* define_graph_fun_short funs nm *}
|
||||
|
||||
ML {*
|
||||
val ctxt = @{context}
|
||||
val hints = SimplToGraphProof.mk_hints funs ctxt nm
|
||||
val init_thm = SimplToGraphProof.simpl_to_graph_upto_subgoals funs hints nm
|
||||
ctxt
|
||||
*}
|
||||
|
||||
ML {*
|
||||
val v = ProveSimplToGraphGoals.test_graph_refine_proof funs (csenv ()) ctxt nm
|
||||
*}
|
||||
|
||||
schematic_goal "PROP ?P"
|
||||
apply (tactic {* resolve_tac @{context} [init_thm] 1 *})
|
||||
apply (tactic {* ALLGOALS (TRY o ProveSimplToGraphGoals.graph_refine_proof_full_goal_tac
|
||||
(csenv ()) @{context}) *})
|
||||
*)
|
||||
(* If this fails, it can be debugged with the assistance of the
|
||||
script in TestGraphRefine.thy *)
|
||||
|
||||
ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_parallel
|
||||
funs (csenv ()) @{context} *}
|
||||
|
|
|
|||
|
|
@ -26,7 +26,23 @@ val csenv = let
|
|||
|
||||
context kernel_all_substitute begin
|
||||
|
||||
ML {*
|
||||
lemma ctzl_body_refines:
|
||||
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
|
||||
(\<acute>ret__long :== ucast (bv_ctz (\<acute>x)))) ctzl_body"
|
||||
apply (simp add: ctzl_body_def)
|
||||
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
|
||||
apply (clarsimp simp: bv_ctz_def meq_def)
|
||||
done
|
||||
|
||||
lemma clzl_body_refines:
|
||||
"simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
|
||||
(\<acute>ret__long :== ucast (bv_clz (\<acute>x)))) clzl_body"
|
||||
apply (simp add: clzl_body_def)
|
||||
apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
|
||||
apply (clarsimp simp: bv_clz_def meq_def)
|
||||
done
|
||||
|
||||
ML {*
|
||||
emit_C_everything_relative @{context} (csenv ()) "CFunDump.txt";
|
||||
*}
|
||||
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ imports "../../lib/CTranslationNICTA"
|
|||
|
||||
begin
|
||||
|
||||
text {* Additional constants needed to make conversion to graph lang easy *}
|
||||
text {* Additional constants needed to make conversion to and from the graph lang easy *}
|
||||
|
||||
definition
|
||||
bvshl :: "'a :: len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
|
||||
|
|
@ -37,16 +37,20 @@ definition
|
|||
where
|
||||
"bv_shift_amount n = of_nat (min n ((2 ^ len_of TYPE('a)) - 1))"
|
||||
|
||||
definition
|
||||
"count_leading_zeroes z = length (takeWhile Not (to_bl z))"
|
||||
|
||||
definition
|
||||
"count_trailing_zeroes z = length (takeWhile Not (rev (to_bl z)))"
|
||||
|
||||
definition
|
||||
bv_clz :: "('a :: len) word \<Rightarrow> 'a word"
|
||||
where
|
||||
"bv_clz x = of_nat (count_leading_zeroes x)"
|
||||
"bv_clz x = of_nat (word_clz x)"
|
||||
|
||||
definition
|
||||
bv_ctz :: "('a :: len) word \<Rightarrow> 'a word"
|
||||
where
|
||||
"bv_ctz x = of_nat (word_ctz x)"
|
||||
|
||||
definition
|
||||
bv_popcount :: "('a :: len) word \<Rightarrow> 'a word"
|
||||
where
|
||||
"bv_popcount x = of_nat (pop_count x)"
|
||||
|
||||
definition
|
||||
"mem_acc mem addr = h_val mem (Ptr addr)"
|
||||
|
|
|
|||
|
|
@ -0,0 +1,97 @@
|
|||
(*
|
||||
* Copyright 2016, Data61
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_BSD)
|
||||
*)
|
||||
|
||||
theory ExtraSpecs
|
||||
|
||||
imports
|
||||
"../../lib/TypHeapLib"
|
||||
|
||||
begin
|
||||
|
||||
definition
|
||||
"simple_simpl_refines \<Gamma> com com'
|
||||
= (\<forall>s. (\<exists>ft. \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> Fault ft)
|
||||
\<or> ((\<forall>xs. \<Gamma> \<turnstile> \<langle>com, Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> xs)
|
||||
\<and> (\<not> terminates \<Gamma> com (Normal s) \<longrightarrow> \<not> terminates \<Gamma> com' (Normal s))))"
|
||||
|
||||
lemma simple_simpl_refines_no_fault_execD:
|
||||
"\<Gamma> \<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs
|
||||
\<Longrightarrow> simple_simpl_refines \<Gamma> com com'
|
||||
\<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft)
|
||||
\<Longrightarrow> \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> xs"
|
||||
by (auto simp add: simple_simpl_refines_def)
|
||||
|
||||
lemma simple_simpl_refines_no_fault_terminatesD:
|
||||
"simple_simpl_refines \<Gamma> com com'
|
||||
\<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft)
|
||||
\<Longrightarrow> \<not> terminates \<Gamma> com (Normal s) \<longrightarrow> \<not> terminates \<Gamma> com' (Normal s)"
|
||||
by (auto simp add: simple_simpl_refines_def)
|
||||
|
||||
lemma simple_simpl_refines_refl:
|
||||
"simple_simpl_refines \<Gamma> com com"
|
||||
by (auto simp add: simple_simpl_refines_def)
|
||||
|
||||
lemma simple_simpl_refines_from_def_eq:
|
||||
"body \<equiv> body' \<Longrightarrow> simple_simpl_refines \<Gamma> body' body"
|
||||
(* these are flipped, because the "implementation" is on the rhs of
|
||||
definitional equalities, but the lhs of refinement thms. *)
|
||||
by (simp add: simple_simpl_refines_def)
|
||||
|
||||
lemma simple_simpl_refines_trans:
|
||||
"simple_simpl_refines \<Gamma> com com' \<Longrightarrow> simple_simpl_refines \<Gamma> com' com''
|
||||
\<Longrightarrow> simple_simpl_refines \<Gamma> com com''"
|
||||
by (simp add: simple_simpl_refines_def, metis)
|
||||
|
||||
lemma simple_simpl_refines_drop_Guard:
|
||||
"simple_simpl_refines \<Gamma> com (Guard F G com)"
|
||||
apply (clarsimp simp add: simple_simpl_refines_def)
|
||||
apply (case_tac "s \<in> G")
|
||||
apply (auto intro: exec.Guard exec.GuardFault
|
||||
elim!: terminates_Normal_elim_cases)
|
||||
done
|
||||
|
||||
lemma simple_simpl_refines_guarded_Basic_guarded_spec_body:
|
||||
"(\<forall>s s'. (s, s') \<in> R \<longrightarrow> (s \<in> G \<and> (s, f s) \<in> R))
|
||||
\<Longrightarrow> simple_simpl_refines \<Gamma> (Guard F' G (Basic f)) (guarded_spec_body F R)"
|
||||
apply (simp add: guarded_spec_body_def simple_simpl_refines_def)
|
||||
apply (intro allI, drule_tac x=s in spec)
|
||||
apply (erule impCE)
|
||||
apply (rule disjI1)
|
||||
apply (fastforce intro: exec.GuardFault)
|
||||
apply (rule disjI2)
|
||||
apply (auto intro!: exec.Guard terminates.Guard
|
||||
intro: exec.GuardFault exec.Spec terminates.Basic image_eqI[rotated]
|
||||
elim!: exec_Normal_elim_cases terminates_Normal_elim_cases)
|
||||
done
|
||||
|
||||
lemmas simple_simpl_refines_Basic_guarded_spec_body
|
||||
= simple_simpl_refines_trans[OF
|
||||
simple_simpl_refines_drop_Guard[where G=UNIV]
|
||||
simple_simpl_refines_guarded_Basic_guarded_spec_body
|
||||
]
|
||||
|
||||
ML {*
|
||||
structure Get_Body_Refines = struct
|
||||
|
||||
fun get ctxt name = let
|
||||
fun pget sfx = try (Proof_Context.get_thm ctxt o suffix sfx) name
|
||||
val eqv = pget "_body_refines"
|
||||
val def = pget "_body_def"
|
||||
in case (eqv, def) of
|
||||
(SOME eqvt, _) => eqvt
|
||||
| (_, SOME deft) => (deft RS @{thm simple_simpl_refines_from_def_eq})
|
||||
| _ => raise THM ("Get_Body_Refines.get: "
|
||||
^ "no body_def or body_refines: " ^ name, 1, [])
|
||||
end
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
end
|
||||
|
|
@ -570,6 +570,7 @@ val opers = Symtab.make [
|
|||
("WordArrayAccess", @{const_name "fun_app"}),
|
||||
("WordArrayUpdate", @{const_name "fun_upd"}),
|
||||
("CountLeadingZeroes", @{const_name "bv_clz"}),
|
||||
("CountTrailingZeroes", @{const_name "bv_ctz"}),
|
||||
("True", @{const_name "True"}),
|
||||
("False", @{const_name "False"}),
|
||||
("IfThenElse", @{const_name "If"}),
|
||||
|
|
|
|||
|
|
@ -10,8 +10,11 @@
|
|||
|
||||
theory GraphRefine
|
||||
|
||||
imports TailrecPre GraphLangLemmas "../../lib/LemmaBucket_C"
|
||||
|
||||
imports
|
||||
TailrecPre
|
||||
GraphLangLemmas
|
||||
"../../lib/LemmaBucket_C"
|
||||
ExtraSpecs
|
||||
begin
|
||||
|
||||
type_synonym ('s, 'x, 'e) c_trace = "nat \<Rightarrow> (('s, 'x, 'e) com \<times> ('s, 'e) xstate) option"
|
||||
|
|
@ -935,9 +938,10 @@ lemma trace_end_Ret_Err:
|
|||
auto simp: exec_graph_invariant_def)
|
||||
done
|
||||
|
||||
lemma graph_fun_refines_from_simpl_to_graph:
|
||||
lemma graph_fun_refines_from_simpl_to_graph_with_refine:
|
||||
"\<lbrakk> SGamma proc = Some com; GGamma fname = Some gf;
|
||||
\<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com []) 0
|
||||
simple_simpl_refines SGamma com' com;
|
||||
\<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0
|
||||
[Q] UNIV I eqs
|
||||
(\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs);
|
||||
eq_impl (NextNode (entry_point gf))
|
||||
|
|
@ -949,8 +953,8 @@ lemma graph_fun_refines_from_simpl_to_graph:
|
|||
apply (clarsimp simp: graph_fun_refines_def)
|
||||
apply (frule exec_trace_def[THEN eqset_imp_iff, THEN iffD1])
|
||||
apply clarsimp
|
||||
apply (erule_tac x="UNIV \<times> {[0 \<mapsto> (com, Normal s)]}" in meta_allE)
|
||||
apply (drule_tac tr=tr and tr'="[0 \<mapsto> (com, Normal s)]"
|
||||
apply (erule_tac x="UNIV \<times> {[0 \<mapsto> (com', Normal s)]}" in meta_allE)
|
||||
apply (drule_tac tr=tr and tr'="[0 \<mapsto> (com', Normal s)]"
|
||||
and n'=0 and n''=0 and sst=s in simpl_to_graphD)
|
||||
apply (rule conjI, assumption)
|
||||
apply (simp add: suffix_tuple_closure_inter_def exec_trace_def)
|
||||
|
|
@ -967,16 +971,23 @@ lemma graph_fun_refines_from_simpl_to_graph:
|
|||
apply clarsimp
|
||||
apply (drule step_preserves_termination[rotated])
|
||||
apply (erule step.Call)
|
||||
apply (simp add: c_trace_nontermination)
|
||||
apply (drule simple_simpl_refines_no_fault_terminatesD)
|
||||
apply (blast intro: exec.Call)
|
||||
apply (simp add: c_trace_nontermination simple_simpl_refines_def)
|
||||
apply (frule(1) trace_end_Ret_Err)
|
||||
apply (clarsimp simp: exec_final_step_def acc_vars_def)
|
||||
apply metis
|
||||
apply clarsimp
|
||||
apply (erule exec.Call)
|
||||
apply (rule exec.Call, assumption)
|
||||
apply (erule simple_simpl_refines_no_fault_execD[rotated])
|
||||
apply (blast intro: exec.Call)
|
||||
apply (simp add: exec_via_trace)
|
||||
apply metis
|
||||
done
|
||||
|
||||
lemmas graph_fun_refines_from_simpl_to_graph
|
||||
= graph_fun_refines_from_simpl_to_graph_with_refine[OF _ _ simple_simpl_refines_refl]
|
||||
|
||||
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"
|
||||
|
|
@ -2259,17 +2270,17 @@ fun mk_hints (funs : ParseGraph.funs) ctxt nm = case Symtab.lookup funs nm of
|
|||
err_conds = ec} end
|
||||
|
||||
fun init_graph_refines_proof funs nm ctxt = let
|
||||
val body_thm = Proof_Context.get_thm ctxt
|
||||
(Long_Name.base_name nm ^ "_body_def")
|
||||
val body_ref_thm = Get_Body_Refines.get ctxt (Long_Name.base_name nm)
|
||||
val ct = mk_graph_refines funs ctxt nm |> Thm.cterm_of ctxt
|
||||
in Thm.trivial ct
|
||||
|> (resolve0_tac [@{thm graph_fun_refines_from_simpl_to_graph}] 1
|
||||
|> (resolve_tac ctxt [@{thm graph_fun_refines_from_simpl_to_graph_with_refine}] 1
|
||||
THEN apply_impl_thm ctxt 1
|
||||
THEN graph_gamma_tac ctxt 1
|
||||
THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [body_thm]
|
||||
THEN resolve_tac ctxt [body_ref_thm] 1
|
||||
THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt
|
||||
addsimps @{thms entry_point.simps function_inputs.simps
|
||||
function_outputs.simps list.simps}))
|
||||
THEN TRY ((resolve0_tac [@{thm simpl_to_graph_noop_same_eqs}]
|
||||
THEN TRY ((resolve_tac ctxt [@{thm simpl_to_graph_noop_same_eqs}]
|
||||
THEN' inst_graph_tac ctxt) 1)
|
||||
)
|
||||
|> Seq.hd
|
||||
|
|
|
|||
|
|
@ -136,6 +136,22 @@ lemma drop_sign_isomorphism_bitwise:
|
|||
| safe
|
||||
| simp add: test_bit_bin)+
|
||||
|
||||
lemma drop_sign_of_nat:
|
||||
"drop_sign (of_nat n) = of_nat n"
|
||||
by (simp add: drop_sign_def ucast_of_nat is_down_def
|
||||
target_size_def source_size_def word_size)
|
||||
|
||||
lemma drop_sign_to_bl:
|
||||
"to_bl (drop_sign w) = to_bl w"
|
||||
by (simp add: drop_sign_def to_bl_ucast)
|
||||
|
||||
lemma drop_sign_extra_bl_ops:
|
||||
"drop_sign (bv_clz w) = bv_clz (drop_sign w)"
|
||||
"drop_sign (bv_ctz w) = bv_ctz (drop_sign w)"
|
||||
"drop_sign (bv_popcount w) = bv_popcount (drop_sign w)"
|
||||
by (simp_all add: bv_clz_def bv_ctz_def bv_popcount_def drop_sign_of_nat
|
||||
word_ctz_def word_clz_def pop_count_def drop_sign_to_bl)
|
||||
|
||||
lemma drop_sign_number[simp]:
|
||||
"drop_sign (numeral n) = numeral n"
|
||||
"drop_sign (- numeral n) = - numeral n"
|
||||
|
|
@ -153,8 +169,8 @@ lemma drop_sign_projections:
|
|||
|
||||
lemmas drop_sign_isomorphism
|
||||
= drop_sign_isomorphism_ariths drop_sign_projections
|
||||
drop_sign_isomorphism_bitwise
|
||||
ucast_id
|
||||
drop_sign_isomorphism_bitwise drop_sign_of_nat
|
||||
drop_sign_extra_bl_ops ucast_id
|
||||
|
||||
lemma drop_sign_h_val[simp]:
|
||||
"drop_sign (h_val hp p :: ('a :: len8) signed word) = h_val hp (ptr_coerce p)"
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@
|
|||
|
||||
theory SimplExport
|
||||
|
||||
imports GraphLang CommonOpsLemmas GlobalsSwap
|
||||
imports GraphLang CommonOpsLemmas GlobalsSwap ExtraSpecs
|
||||
|
||||
begin
|
||||
|
||||
|
|
@ -75,6 +75,8 @@ val ops = Symtab.make [
|
|||
(@{const_name "shiftl"}, ("ShiftLeft", false)),
|
||||
(@{const_name "shiftr"}, ("ShiftRight", false)),
|
||||
(@{const_name "sshiftr"}, ("SignedShiftRight", false)),
|
||||
(@{const_name "bv_clz"}, ("CountLeadingZeroes", true)),
|
||||
(@{const_name "bv_ctz"}, ("CountTrailingZeroes", true)),
|
||||
(@{const_name "all_htd_updates"}, ("HTDUpdate", false))
|
||||
] |> Symtab.lookup
|
||||
|
||||
|
|
@ -736,11 +738,6 @@ and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ x)
|
|||
in if t1 = t2 then convert_ph3 ctxt params x
|
||||
else convert_ph3 ctxt params (Const (@{const_name ucast}, t1 --> t2) $ x)
|
||||
end
|
||||
| convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $
|
||||
(Const (@{const_name count_leading_zeroes}, _) $ x)))
|
||||
= convert_op ctxt params "CountLeadingZeroes" (convert_type false ctxt (fastype_of t)) [x]
|
||||
(* | convert_ph3 ctxt params (t as (Const (@{const_name unat}, _) $ _))
|
||||
= convert_ph3 ctxt params (@{term "of_nat :: nat \<Rightarrow> word32"} $ t) *)
|
||||
| convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $ _))
|
||||
= convert_ph3 ctxt params (ptr_simp_term ctxt "of_nat" t t)
|
||||
| convert_ph3 ctxt params (t as (Const (@{const_name power}, _) $ x $ y))
|
||||
|
|
@ -868,7 +865,7 @@ fun reduce_set_mem ctxt x S = let
|
|||
|
||||
fun is_spec_body_const @{const_name Spec} = true
|
||||
| is_spec_body_const @{const_name guarded_spec_body} = true
|
||||
| is_spec_body_const c = false
|
||||
| is_spec_body_const _ = false
|
||||
|
||||
fun has_reads body = exists_Const (fn (s, T) =>
|
||||
snd (strip_type T) = @{typ heap_raw_state}
|
||||
|
|
@ -1083,13 +1080,18 @@ fun emit_func_body ctxt outfile eparams name = let
|
|||
val outputs = (filter (fn p => fst p = HoarePackage.Out) params
|
||||
|> maps snd) @ (if no_write then [] else all_c_params)
|
||||
|
||||
val body = Proof_Context.get_thm ctxt (name ^ "_body_def")
|
||||
|> simplify (put_simpset HOL_basic_ss ctxt
|
||||
val body = Get_Body_Refines.get ctxt name
|
||||
|> simplify (put_simpset HOL_basic_ss ctxt
|
||||
addsimps @{thms switch.simps fst_conv snd_conv
|
||||
insert_iff empty_iff
|
||||
ptr_add_assertion_def if_True if_False})
|
||||
|> Thm.concl_of |> Logic.dest_equals |> snd
|
||||
handle ERROR _ => @{term "Spec S"}
|
||||
ptr_add_assertion_def if_True if_False
|
||||
bv_clz_def[symmetric] bv_ctz_def[symmetric]
|
||||
})
|
||||
|> Thm.concl_of |> HOLogic.dest_Trueprop
|
||||
|> (fn t => (case t of Const (@{const_name simple_simpl_refines}, _) $ _ $ lhs $ _ => lhs
|
||||
| _ => raise Option))
|
||||
handle Option => @{term "Spec S"}
|
||||
| THM _ => @{term "Spec S"}
|
||||
|
||||
val full_nm = read_const ctxt (name ^ "_'proc")
|
||||
|> dest_Const |> fst |> unsuffix "_'proc"
|
||||
|
|
|
|||
Loading…
Reference in New Issue