diff options
Diffstat (limited to 'src/hls/RTLPargenproof.v')
| -rw-r--r-- | src/hls/RTLPargenproof.v | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index fac6455..689c11a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -796,24 +796,25 @@ Qed.*)Admitted. Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. +(* TODO: Fix the `bb` and add matches for them. *) Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: - forall f tf res sp pc rs rs' ps ps', + forall f tf res sp pc rs rs' ps ps' bb bb', transl_function f = OK tf -> (forall x, rs !! x = rs' !! x) -> (forall x, ps !! x = ps' !! x) -> - match_stackframes (Stackframe res f sp pc rs ps) - (Stackframe res tf sp pc rs' ps'). + match_stackframes (Stackframe res f sp pc bb rs ps) + (Stackframe res tf sp pc bb' rs' ps'). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m sf' tf ps ps' + forall sf f sp pc rs rs' m sf' tf ps ps' bb bb' (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') (REG: forall x, rs !! x = rs' !! x) (REG: forall x, ps !! x = ps' !! x), - match_states (State sf f sp pc nil rs ps m) - (State sf' tf sp pc nil rs' ps' m) + match_states (State sf f sp pc bb rs ps m) + (State sf' tf sp pc bb' rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), @@ -1041,14 +1042,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. constructor; eauto. Qed. + (* TODO: Fix these proofs, now the cf_instr is in the State. *) Lemma step_cf_instr_correct: - forall cfi t s s', - step_cf_instr ge s cfi t s' -> + forall t s s', + step_cf_instr ge s t s' -> forall r, match_states s r -> - exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. + exists r', step_cf_instr tge r t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl; + + (*induction 1; repeat semantics_simpl; try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). eapply eval_builtin_args_eq. eapply REG. @@ -1069,7 +1072,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). erewrite eval_predf_pr_equiv; eauto. } - Qed. + Qed.*) Admitted. Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, @@ -1079,12 +1082,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists R2, Smallstep.plus RTLPar.step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; repeat semantics_simpl. + (*induction 1; repeat semantics_simpl. { destruct bb; destruct x. assert (bb_exit = bb_exit0). { unfold schedule_oracle in *. simplify. - unfold check_control_flow_instr in *. + n unfold check_control_flow_instr in *. destruct_match; crush. } subst. @@ -1106,7 +1109,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } { inv STACKS. inv H2. repeat econstructor; eauto. intros. apply PTree_matches; eauto. } - Qed. + Qed.*) Admitted. Lemma transl_initial_states: forall S, |