diff options
Diffstat (limited to 'scheduling/BTL_Scheduler.v')
| -rw-r--r-- | scheduling/BTL_Scheduler.v | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v new file mode 100644 index 00000000..78c597e0 --- /dev/null +++ b/scheduling/BTL_Scheduler.v @@ -0,0 +1,176 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking BTL_SEtheory BTL_SEimpl. + +(** External oracle *) +Axiom scheduler: BTL.function -> BTL.code. + +Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". + +Definition equiv_input_regs (f1 f2: BTL.function): Prop := + (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) + /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). + +Lemma equiv_input_regs_union f1 f2: + equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. +Proof. + intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. + generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. + do 2 autodestruct; intuition; try_simplify_someHyps. + intros; exploit EQS; eauto; clear EQS. congruence. +Qed. + +Lemma equiv_input_regs_pre f1 f2 tbl or: + equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. +Proof. + intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. +Qed. + +Lemma equiv_input_regs_tr_inputs f1 f2 l oreg rs: + equiv_input_regs f1 f2 -> + tr_inputs f1 l oreg rs = tr_inputs f2 l oreg rs. +Proof. + intros; unfold tr_inputs; erewrite equiv_input_regs_pre; eauto. +Qed. + +(* a specification of the verification to do on each function *) +Record match_function (f1 f2: BTL.function): Prop := { + preserv_fnsig: fn_sig f1 = fn_sig f2; + preserv_fnparams: fn_params f1 = fn_params f2; + preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; + preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; + preserv_inputs: equiv_input_regs f1 f2; + symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); +}. + +Inductive match_fundef: fundef -> fundef -> Prop := + | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro + res f sp pc rs rs' f' + (EQREGS: forall r, rs # r = rs' # r) + (TRANSF: match_function f f') + : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs'). + +Inductive match_states: state -> state -> Prop := + | match_states_intro + st f sp pc rs rs' m st' f' + (EQREGS: forall r, rs # r = rs' # r) + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function f f') + : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return + st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states (Returnstate st v m) (Returnstate st' v m) + . + +Lemma match_stack_equiv stk1 stk2: + list_forall2 match_stackframes stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 match_stackframes stk1 stk3. +Proof. + induction 1; intros stk3 EQ; inv EQ; constructor; eauto. + inv H3; inv H; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + +Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. +Proof. + Local Hint Resolve match_stack_equiv: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + +Local Open Scope error_monad_scope. + +Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit := + match lpc with + | nil => OK tt + | pc :: lpc' => + match (fn_code f1)!pc, (fn_code f2)!pc with + | Some ibf1, Some ibf2 => + do _ <- simu_check f1 f2 ibf1 ibf2; + check_symbolic_simu_rec f1 f2 lpc' + | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch") + end + end. + +Definition erase_input_regs f1 f2 := + let code := PTree.map (fun pc ibf => + let oibf := match (fn_code f2)!pc with + | None => ibf + | Some oibf => oibf + end in + {| entry:= oibf.(entry); input_regs := ibf.(input_regs); binfo := oibf.(binfo) |}) (fn_code f1) in + BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2). + +Lemma erase_input_regs_correct f1 f2 f3: + erase_input_regs f1 f2 = f3 -> + equiv_input_regs f1 f3. +Proof. + unfold erase_input_regs; simpl; intros. + unfold equiv_input_regs; intuition auto. + - subst; simpl. rewrite PTree.gmap, H0; simpl; auto. + - subst; simpl in H0. rewrite PTree.gmap in H0. + destruct ((fn_code f1)!pc) eqn:EQF; simpl in H0; inv H0; auto. + - subst; simpl in H1. rewrite PTree.gmap in H1. + rewrite H0 in H1; simpl in H1; inv H1; simpl; auto. +Qed. +Global Opaque erase_input_regs. + +Definition check_symbolic_simu (f1 f2: BTL.function): res unit := + check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). + +Definition transf_function (f: BTL.function) := + let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in + let tf' := erase_input_regs f tf in + do _ <- check_symbolic_simu f tf'; + OK tf'. + +Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x, + check_symbolic_simu_rec f1 f2 lpc = OK x -> + forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). +Proof. + induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction. + destruct HIN; subst. + - rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X. + exists i; split; auto. destruct x0. eapply simu_check_correct; eauto. + - destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X. + eapply IHlpc; eauto. +Qed. + +Lemma check_symbolic_simu_correct x f1 f2: + check_symbolic_simu f1 f2 = OK x -> + forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). +Proof. + unfold check_symbolic_simu; intros X pc ib1 PC. + eapply check_symbolic_simu_rec_correct; intuition eauto. + apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto. +Qed. + +Lemma check_symbolic_simu_input_equiv x f1 f2: + transf_function f1 = OK f2 -> + check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Proof. + unfold transf_function; intros TRANSF X; monadInv TRANSF. + exploit erase_input_regs_correct; eauto. +Qed. + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef (fun f => transf_function f) f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. |