diff options
| -rw-r--r-- | scheduling/BTL.v | 34 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 30 |
2 files changed, 27 insertions, 37 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 4ae7a6dd..954b4cb4 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -18,6 +18,8 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad. +Import ListNotations. + (** * Abstract syntax *) Definition exit := node. (* we may generalize this with register renamings at exit, @@ -159,12 +161,15 @@ Record outcome := out { _fin: option final }. - - +(* follows RTL semantics to set the result of builtin *) +Definition reg_builtin_res (res: builtin_res reg): option reg := + match res with + | BR r => Some r + | _ => None + end. Section RELSEM. - (** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit. In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start. @@ -286,7 +291,6 @@ Proof. destruct o; try_simplify_someHyps; subst; eauto. Qed. -Import ListNotations. Local Open Scope list_scope. Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := @@ -314,10 +318,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') - (* TODO: not clear that this is the better choice ! - we coud also do something like [regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)] - *) - t (State stack f sp pc' (tr_exit f [pc'] None (regmap_setres res vres rs)) m') + t (State stack f sp pc' (regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> @@ -455,8 +456,6 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f pc or)). - - (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, SetoidList.InA (fun x y => x = y) x l <-> List.In x l. @@ -503,6 +502,21 @@ Qed. Definition fsem (p: program) := Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). +Local Open Scope list_scope. + +Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := + match i with + | Bgoto pc => tr f [pc] None + | Bcall sig ros args res pc => tr f [pc] (Some res) + | Btailcall sig ros args => tr f [] None + | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) + | Breturn or => tr f [] None + | Bjumptable reg tbl => tr f tbl None + end. + +Definition tr_regs: function -> final -> regset -> regset := + poly_tr tr_inputs. + (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) (** Matching BTL and RTL code diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index fb7c650f..d682f776 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -441,10 +441,10 @@ Inductive sem_sfval ctx (rsx: reg -> option val): sfval -> regset -> mem -> trac | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs': seval_builtin_args ctx m sargs vargs -> external_call ef (cge ctx) vargs m t vres m' -> - rs' = tr_inputs ctx.(cf) [pc] None (regmap_setres res vres rs) -> + rs' = tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs -> (forall r, rsx r = Some rs'#r) -> sem_sfval ctx rsx (Sbuiltin ef sargs res pc) rs m - t (State (cstk ctx) (cf ctx) (csp ctx) pc rs' m') + t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs') m') | exec_Sjumptable sv tbl pc' n rs m rs': eval_sval ctx sv = Some (Vint n) -> list_nth_z tbl (Int.unsigned n) = Some pc' -> @@ -611,28 +611,6 @@ Admitted. Local Hint Resolve transfer_sis_correct: core. -(* TODO: move the 3 below functions in [BTL] ? - Could be reused for liveness checking ? -*) -Definition reg_builtin_res (res: builtin_res reg): option reg := - match res with - | BR r => Some r - | _ => None - end. - -Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := - match i with - | Bgoto pc => tr f [pc] None - | Bcall sig ros args res pc => tr f [pc] (Some res) - | Btailcall sig ros args => tr f [] None - | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) - | Breturn or => tr f [] None - | Bjumptable reg tbl => tr f tbl None - end. - -Definition tr_regs: function -> final -> regset -> regset := - poly_tr tr_inputs. - Definition tr_sis: function -> final -> sistate -> sistate := poly_tr transfer_sis. @@ -695,9 +673,8 @@ Proof. - erewrite eval_list_sval_inj; simpl; auto. + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. eapply seval_builtin_args_correct; eauto. - admit. + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. -Admitted. +Qed. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_exact: core. @@ -727,7 +704,6 @@ Proof. congruence. Qed. - (** * symbolic execution of basic instructions *) Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. |