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

autocorres: upgrade from Named_Thm to named_theorems 

This gets rid of the attribute setup boilerplate (but see Utils.get_rules).
Closes issue VER-293.
This commit is contained in:
Japheth Lim 2016-05-30 14:49:50 +10:00
parent 5a98b61127
commit 5b0f2ebbcd
20 changed files with 84 additions and 195 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

78
tools/autocorres/AutoCorresAttributes.thy
View File

@ -1,78 +0,0 @@
(*
* Copyright 2014, NICTA
*
* 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 AutoCorresAttributes
imports "~~/src/HOL/Main"
begin
ML_file "attributes.ML"
attribute_setup L1opt = {*
Attrib.add_del
(Thm.declaration_attribute L1PeepholeThms.add_thm)
(Thm.declaration_attribute L1PeepholeThms.del_thm) *}
"Peephole optimisations carried out after L1 SIMPL to monadic conversion."
attribute_setup L1unfold = {*
Attrib.add_del
(Thm.declaration_attribute L1UnfoldThms.add_thm)
(Thm.declaration_attribute L1UnfoldThms.del_thm) *}
"Definitions unfolded prior to L1 SIMPL to monadic conversion."
attribute_setup L1except = {*
Attrib.add_del
(Thm.declaration_attribute L1ExceptionThms.add_thm)
(Thm.declaration_attribute L1ExceptionThms.del_thm) *}
"Definitions used to rewrite control flow to reduce exception usage."
attribute_setup L2opt = {*
Attrib.add_del
(Thm.declaration_attribute L2PeepholeThms.add_thm)
(Thm.declaration_attribute L2PeepholeThms.del_thm) *}
"Peephole optimisations carried out after L2 monadic conversion."
attribute_setup L2unfold = {*
Attrib.add_del
(Thm.declaration_attribute L2UnfoldThms.add_thm)
(Thm.declaration_attribute L2UnfoldThms.del_thm) *}
"Definitions unfolded prior to L2 monadic conversion from L1."
attribute_setup heap_abs = {*
Attrib.add_del
(Thm.declaration_attribute HeapAbsThms.add_thm)
(Thm.declaration_attribute HeapAbsThms.del_thm) *}
"Heap abstraction rules."
attribute_setup heap_abs_fo = {*
Attrib.add_del
(Thm.declaration_attribute HeapAbsFOThms.add_thm)
(Thm.declaration_attribute HeapAbsFOThms.del_thm) *}
"First-order Heap abstraction rules."
attribute_setup word_abs = {*
Attrib.add_del
(Thm.declaration_attribute WordAbsThms.add_thm)
(Thm.declaration_attribute WordAbsThms.del_thm) *}
"Word abstraction rules."
attribute_setup polish = {*
Attrib.add_del
(Thm.declaration_attribute PolishSimps.add_thm)
(Thm.declaration_attribute PolishSimps.del_thm) *}
"Final simplification rules."
(* Set up the ts_rule attribute. *)
ML_file "monad_types.ML"
setup {*
Attrib.setup (Binding.name "ts_rule") Monad_Types.ts_attrib
"AutoCorres type strengthening rule"
*}
end

13
tools/autocorres/HeapLift.thy
View File

@ -45,6 +45,12 @@ definition "struct_rewrite_expr P A C \<equiv> \<forall>s. P s \<longrightar
definition "struct_rewrite_modifies P A C \<equiv> \<forall>s. P s \<longrightarrow> C s = A s"
(* Standard heap abstraction rules. *)
named_theorems heap_abs
(* Rules that require first-order matching. *)
named_theorems heap_abs_fo
(* fun_app2 is like fun_app, but it skips an abstraction.
* We use this for terms like "\<lambda>s a. Array.update a k (f s)".
* FIXME: ideally, the first order conversion code can skip abstractions. *)
@ -1122,12 +1128,7 @@ lemma abs_spec_modify_global[heap_abs]:
abs_spec st \<top> {(a, b). mex (\<lambda>x. C (new_setter (\<lambda>_. x) a) b)} {(a, b). mex (\<lambda>x. C' (old_setter (\<lambda>_. x) a) b)}"
apply (fastforce simp: abs_spec_def mex_def valid_globals_field_def)
done
(* Remove the Hoare modifies constants after we're finished,
* as they have very buggy print translations.
* In particular, applying abs_spec_modify_global replaces the bound variable by "x"
* and confuses the print translation into producing "may_only_modify_globals [x]". *)
lemmas [polish] = mex_def meq_def
(* NB: meq and mex are unfolded in Polish. *)
(* Signed words are stored on the heap as unsigned words. *)

8
tools/autocorres/L1Defs.thy
View File

@ -13,7 +13,7 @@
*)
theory L1Defs
imports CCorresE AutoCorresAttributes MonadMono
imports CCorresE MonadMono
begin
(* Definitions of constants used in the SimplConv output. *)
@ -493,4 +493,10 @@ lemma monad_mono_step_L1_recguard_0:
"monad_mono_step (\<lambda>m. L1_recguard m (x m)) 0"
by (monad_eq simp: monad_mono_step_def L1_recguard_def)
(* Unfolding rules to run prior to L1 translation. *)
named_theorems L1unfold
(* L1 postprocessing rules, used by ExceptionRewrite and SimplConv. *)
named_theorems L1except
end

5
tools/autocorres/L1Peephole.thy
View File

@ -11,9 +11,12 @@
(* Peep-hole L1 optimisations. *)
theory L1Peephole
imports L1Defs AutoCorresAttributes
imports L1Defs
begin
(* Simplification rules run after L1. *)
named_theorems L1opt
lemma L1_seq_assoc [L1opt]: "(L1_seq (L1_seq X Y) Z) = (L1_seq X (L1_seq Y Z))"
apply (clarsimp simp: L1_seq_def bindE_assoc)
done

3
tools/autocorres/L2Defs.thy
View File

@ -617,6 +617,9 @@ lemmas L2_split_fixups =
lemmas L2_split_fixups_congs =
prod.case_cong
(* Peephole simplification rules for L2 programs (including HeapLift and WordAbstract). *)
named_theorems L2opt
(* L2 monad_mono rules *)
lemma L2_seq_monad_mono_step:
"\<lbrakk> monad_mono_step f m; \<And>x. monad_mono_step (\<lambda>m. g m x) m \<rbrakk>

15
tools/autocorres/L2Opt.thy
View File

@ -12,19 +12,8 @@ theory L2Opt
imports L2Defs L2Peephole
begin
ML {*
structure L2FlowThms =
Named_Thms (
val name = Binding.name "L2flow"
val description = "Flow-sensitive optimisations carried out after L2 monadic conversion."
)
*}
attribute_setup L2flow = {*
Attrib.add_del
(Thm.declaration_attribute L2FlowThms.add_thm)
(Thm.declaration_attribute L2FlowThms.del_thm) *}
"Peephole optimisations carried out after L2 monadic conversion."
(* Flow-sensitive simplification rules for L2 programs. *)
named_theorems L2flow
(*
* The monads "A" and "B" are equivalent under precondition "P".

2
tools/autocorres/L2Peephole.thy
View File

@ -233,7 +233,7 @@ declare ucast_id [L2opt]
declare scast_id [L2opt]
(* Other misc lemmas. *)
declare singleton_iff [L2opt, polish]
declare singleton_iff [L2opt]
(* Optimising "if" structres. *)

21
tools/autocorres/Polish.thy
View File

@ -13,9 +13,28 @@
*)
theory Polish
imports TypeStrengthen
imports WordAbstract TypeStrengthen
begin
(* Final simplification after type strengthening. *)
named_theorems polish
(* Remove the Hoare modifies constants after heap abstraction, as they have
* very buggy print translations.
* In particular, applying abs_spec_modify_global replaces the bound variable by "x"
* and confuses the print translation into producing "may_only_modify_globals [x]". *)
lemmas [polish] = mex_def meq_def
(* Clean up "WORD_MAX TYPE(32)", etc. after word abstraction. *)
lemmas [polish] =
WORD_MAX_simps
WORD_MIN_simps
UWORD_MAX_simps
WORD_signed_to_unsigned
INT_MIN_MAX_lemmas
declare singleton_iff [polish]
lemma L2polish [polish]:
"L2_seq = bindE"
"L2_unknown n = unknownE"

1
tools/autocorres/SimplConv.thy
View File

@ -19,6 +19,7 @@ begin
(*
* Lemmas to unfold prior to L1 conversion.
*)
named_theorems L1unfold
declare creturn_def [L1unfold]
declare creturn_void_def [L1unfold]
declare cbreak_def [L1unfold]

7
tools/autocorres/TypeStrengthen.thy
View File

@ -22,6 +22,13 @@ imports
ExecConcrete
begin
(* Set up the database and ts_rule attribute. *)
ML_file "monad_types.ML"
setup {*
Attrib.setup (Binding.name "ts_rule") Monad_Types.ts_attrib
"AutoCorres type strengthening rule"
*}
(*
* Helpers for exception polymorphism lemmas (L2_call_Foo_polymorphic).
*

24
tools/autocorres/WordAbstract.thy
View File

@ -55,32 +55,33 @@ lemmas [L1unfold] =
WORD_values_add1 [symmetric]
WORD_values_minus1 [symmetric]
lemma WORD_MAX_simps [polish]:
(* These are added to the Polish simps after translation *)
lemma WORD_MAX_simps:
"WORD_MAX TYPE(32) = INT_MAX"
"WORD_MAX TYPE(16) = SHORT_MAX"
"WORD_MAX TYPE(8) = CHAR_MAX"
by (auto simp: INT_MAX_def SHORT_MAX_def CHAR_MAX_def WORD_MAX_def)
lemma WORD_MIN_simps [polish]:
lemma WORD_MIN_simps:
"WORD_MIN TYPE(32) = INT_MIN"
"WORD_MIN TYPE(16) = SHORT_MIN"
"WORD_MIN TYPE(8) = CHAR_MIN"
by (auto simp: INT_MIN_def SHORT_MIN_def CHAR_MIN_def WORD_MIN_def)
lemma UWORD_MAX_simps [polish]:
lemma UWORD_MAX_simps:
"UWORD_MAX TYPE(32) = UINT_MAX"
"UWORD_MAX TYPE(16) = USHORT_MAX"
"UWORD_MAX TYPE(8) = UCHAR_MAX"
by (auto simp: UINT_MAX_def USHORT_MAX_def UCHAR_MAX_def UWORD_MAX_def)
lemma WORD_signed_to_unsigned [polish, simp]:
lemma WORD_signed_to_unsigned [simp]:
"WORD_MAX TYPE('a signed) = WORD_MAX TYPE('a::len)"
"WORD_MIN TYPE('a signed) = WORD_MIN TYPE('a::len)"
"UWORD_MAX TYPE('a signed) = UWORD_MAX TYPE('a::len)"
by (auto simp: WORD_MAX_def WORD_MIN_def UWORD_MAX_def)
lemma INT_MIN_MAX_lemmas [simp, polish]:
lemma INT_MIN_MAX_lemmas [simp]:
"unat (u :: word32) \<le> UINT_MAX"
"sint (s :: sword32) \<le> INT_MAX"
"INT_MIN \<le> sint (s :: sword32)"
@ -808,7 +809,7 @@ lemma abstract_val_abs_var_give_up [consumes 1]:
(* Misc *)
lemma len_of_word_comparisons [word_abs, L2opt]:
lemma len_of_word_comparisons [L2opt]:
"len_of TYPE(32) \<le> len_of TYPE(32)"
"len_of TYPE(16) \<le> len_of TYPE(32)"
"len_of TYPE( 8) \<le> len_of TYPE(32)"
@ -852,17 +853,17 @@ lemma scast_ucast_simps [simp, L2opt]:
declare len_signed [L2opt]
lemmas [L2opt, polish] = zero_sle_ucast_up
lemmas [L2opt] = zero_sle_ucast_up
lemma zero_sle_ucast_WORD_MAX [L2opt, polish]:
lemma zero_sle_ucast_WORD_MAX [L2opt]:
"(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word))
= (uint b \<le> WORD_MAX (TYPE('a)))"
by (clarsimp simp: WORD_MAX_def zero_sle_ucast)
lemmas [L2opt, polish] =
lemmas [L2opt] =
is_up is_down unat_ucast_upcast sint_ucast_eq_uint
lemmas [L2opt, polish] =
lemmas [L2opt] =
ucast_down_add scast_down_add
ucast_down_minus scast_down_minus
ucast_down_mult scast_down_mult
@ -871,6 +872,8 @@ lemmas [L2opt, polish] =
* Setup word abstraction rules.
*)
named_theorems word_abs
(* Common word abstraction rules. *)
lemmas [word_abs] =
@ -922,6 +925,7 @@ lemmas word_abs_base [word_abs] =
valid_typ_abs_fn_unit
valid_typ_abs_fn_sint
valid_typ_abs_fn_unat
len_of_word_comparisons
(*
* Signed word abstraction rules: sword32 \<rightarrow> int

70
tools/autocorres/attributes.ML
View File

@ -1,70 +0,0 @@
(*
* Copyright 2014, NICTA
*
* 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)
*)
(*
* Definition of various attributes.
*
* We define it early so that we can tag theorems that are defined prior to
* the code that uses them.
*)
structure L1UnfoldThms =
Named_Thms (
val name = Binding.name "L1unfold"
val description = "Definitions unfolded prior to L1 SIMPL to monadic conversion."
)
structure L1PeepholeThms =
Named_Thms (
val name = Binding.name "L1opt"
val description = "Peephole optimisations carried out after L1 SIMPL to monadic conversion."
)
structure L1ExceptionThms =
Named_Thms (
val name = Binding.name "L1exception"
val description = "Exception control flow rewriting"
)
structure L2UnfoldThms =
Named_Thms (
val name = Binding.name "L2unfold"
val description = "Definitions unfolded prior to L2 monadic conversion from L1."
)
structure L2PeepholeThms =
Named_Thms (
val name = Binding.name "L2peephole"
val description = "Peephole optimisations carried out after L2 monadic conversion."
)
structure HeapAbsThms =
Named_Thms (
val name = Binding.name "heap_abs"
val description = "Heap Abstraction Rule"
)
structure HeapAbsFOThms =
Named_Thms (
val name = Binding.name "heap_abs_fo"
val description = "First-Order Heap Abstraction Rule"
)
structure WordAbsThms =
Named_Thms (
val name = Binding.name "word_abs"
val description = "Word Abstraction Rule"
)
structure PolishSimps =
Named_Thms (
val name = Binding.name "polish"
val description = "Final simplification rules."
)

4
tools/autocorres/exception_rewrite.ML
View File

@ -307,8 +307,8 @@ end
fun except_rewrite_conv ctxt do_opt =
Simplifier.asm_full_rewrite (
put_simpset HOL_basic_ss (Utils.set_hidden_ctxt ctxt)
addsimps (L1ExceptionThms.get ctxt)
addsimps (if do_opt then L1PeepholeThms.get ctxt else [])
addsimps (Utils.get_rules ctxt @{named_theorems L1except})
addsimps (if do_opt then Utils.get_rules ctxt @{named_theorems L1opt} else [])
addsimprocs simprocs)
end

4
tools/autocorres/heap_lift.ML
View File

@ -582,7 +582,7 @@ let
* "valid_globals_field", "valid_typ_heap" etc with the predicates generated
* above.
*)
val base_rules = HeapAbsThms.get lthy
val base_rules = Utils.get_rules lthy @{named_theorems heap_abs}
(* FIXME: make an attribute for these rules? *)
val base_nolift_rules = @{thms struct_rewrite_expr_id}
val [rules, nolift_rules] =
@ -631,7 +631,7 @@ let
val rules = rules @ (map (snd #> #3) (Symtab.dest callee_terms)) @ callee_mono_thms
val rules = if Symset.contains unliftable_functions fn_name
then rules @ nolift_rules else rules
val fo_rules = HeapAbsFOThms.get ctxt
val fo_rules = Utils.get_rules ctxt @{named_theorems heap_abs_fo}
(* Apply a conversion to the concrete side of the given L2T term.
* By convention, the concrete side is the last argument (index ~1). *)

4
tools/autocorres/l2_opt.ML
View File

@ -135,7 +135,7 @@ let
(no_tac t)
(* Fetch theorms used in the simplification process. *)
val thms = L2FlowThms.get ctxt
val thms = Utils.get_rules ctxt @{named_theorems L2flow}
(* Tactic to blindly apply simplification rules. *)
fun solve_goal_tac _ =
@ -247,7 +247,7 @@ let
(* Setup basic simplifier. *)
fun basic_ss ctxt =
put_simpset AUTOCORRES_SIMPSET ctxt
|> (fn ctxt => if fast_mode < 2 then ctxt addsimps (L2PeepholeThms.get ctxt) else ctxt)
|> (fn ctxt => if fast_mode < 2 then ctxt addsimps (Utils.get_rules ctxt @{named_theorems L2opt}) else ctxt)
|> (fn ctxt => if fast_mode < 2 then ctxt addsimprocs [l2_gets_bind_simproc] else ctxt)
|> (fn ctxt => ctxt addsimprocs [l2_guard_simproc (simpset_of ctxt)])
|> map_opt_simpset false

4
tools/autocorres/local_var_extract.ML
View File

@ -1277,10 +1277,8 @@ fun get_l2corres_thm ctxt prog_info fn_info do_opt trace_opt fn_name
* We do some basic conversions here to convert common sets into lambda
* functions.
*)
val l2_unfolds = map (fn x => (mk_meta_eq x) handle (THM _) => x) (L2UnfoldThms.get ctxt)
val init_rule = Thm.cterm_of ctxt l1_term
|> (Conv.rewr_conv (safe_mk_meta_eq init_unfold)
then_conv Raw_Simplifier.rewrite (put_simpset HOL_basic_ss ctxt) false l2_unfolds)
|> Conv.rewr_conv (safe_mk_meta_eq init_unfold)
(* Extract the term we will be working with. *)
val source_term = Thm.concl_of init_rule |> Logic.dest_equals |> snd

2
tools/autocorres/monad_convert.ML
View File

@ -139,7 +139,7 @@ fun polish ctxt (mt : Monad_Types.monad_type) do_opt thm =
let
(* Apply any polishing rules. *)
val ctxt = Utils.set_hidden_ctxt ctxt
val simps = if do_opt then PolishSimps.get ctxt else []
val simps = if do_opt then Utils.get_rules ctxt @{named_theorems polish} else []
(* Simplify using polish rules. *)
val rules = Monad_Types.monad_type_rules mt

7
tools/autocorres/simpl_conv.ML
View File

@ -275,8 +275,8 @@ let
val (thm, guard_opt_trace) = AutoCorresTrace.fconv_rule_maybe_traced ctxt (l1conv guard_conv) thm trace_opt
val (thm, peephole_opt_trace) =
AutoCorresTrace.fconv_rule_maybe_traced ctxt
(l1conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
addsimps (if do_opt then L1PeepholeThms.get ctxt else []))))
(l1conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps
(if do_opt then Utils.get_rules ctxt @{named_theorems L1opt} else []))))
thm trace_opt
val _ = gather_stats "L1peep" thm
@ -307,7 +307,8 @@ let
(* Unfold terms in the body which we don't want to deal with. *)
val unfolded_simpl_thm =
Conv.fconv_rule (Utils.rhs_conv
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps (L1UnfoldThms.get ctxt))))
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps
(Utils.get_rules ctxt @{named_theorems L1unfold}))))
simpl_thm
val unfolded_simpl_term = Thm.concl_of unfolded_simpl_thm |> Utils.rhs_of;

4
tools/autocorres/utils.ML
View File

@ -998,6 +998,10 @@ fun mk_simproc' ctxt (name : string, pats : string list, proc : Proof.context ->
{lhss = map (Proof_Context.read_term_pattern ctxt) pats,
proc = K proc, identifier = []} end
(* Get named_theorems in reverse order. We use this for translation rulesets
* so that user-added rules can override the built-in ones. *)
fun get_rules ctxt = Named_Theorems.get ctxt #> rev
end
(* Insist the the given tactic solves a subgoal. *)

3
tools/autocorres/word_abstract.ML
View File

@ -229,7 +229,8 @@ let
(*
* Fetch rules from the theory.
*)
val rules = WordAbsThms.get lthy @ List.concat (map #rules wa_rules)
val rules = Utils.get_rules lthy @{named_theorems word_abs}
@ List.concat (map #rules wa_rules)
@ @{thms word_abs_default}
val fo_rules = [@{thm abstract_val_fun_app}]