From 337d9e45bb6b96ec89f905cf0192d732c7bd53ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 Apr 2022 18:22:30 +0100 Subject: Work on the match_states definition --- src/hls/RTLBlockgenproof.v | 7 ++++++- src/hls/RTLPar.v | 5 +++-- src/hls/RTLPargenproof.v | 31 +++++++++++++++++-------------- 3 files changed, 26 insertions(+), 17 deletions(-) diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index f57af34..a0a1ee8 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -115,7 +115,12 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop := forall stk stk' f tf sp pc rs m pc' ps bb (TF: transl_function f = OK tf) (PC: find_block_spec tf.(fn_code) pc pc') - (STK: Forall2 match_stackframe stk stk'), + (STK: Forall2 match_stackframe stk stk') + (BB: forall i bb', + f.(RTL.fn_code) ! pc = Some i -> + tf.(fn_code) ! pc' = Some bb' -> + list_drop (Pos.to_nat pc' - Pos.to_nat pc)%nat bb'.(bb_body) = i' :: bb + ), match_states (RTL.State stk f sp pc rs m) (State stk' tf sp pc' bb rs ps m). diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 61e968e..2c60116 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -46,8 +46,9 @@ Section RELSEM. Context (ge: genv). - Definition step_instr_block := - step_list (step_list (step_list (step_instr ge))). + Definition step_instr_list := step_list (step_instr ge). + Definition step_instr_seq := step_list step_instr_list. + Definition step_instr_block := step_list step_instr_seq. Inductive step: state -> trace -> state -> Prop := | exec_bblock: 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, -- cgit