diff options
Diffstat (limited to 'scheduling/BTL_Scheduler.v')
-rw-r--r-- | scheduling/BTL_Scheduler.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 0662a357..78c597e0 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -46,6 +46,52 @@ Record match_function (f1 f2: BTL.function): Prop := { 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 := |