From fdd6af98c91b6f1206e5f1aef3bfc1f02c7d64aa Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 15 May 2021 21:06:10 +0100 Subject: Fix the top-level proofs with new state_match --- src/hls/RTLPargen.v | 109 +++++++++++++++++++++++++++++++++++++++++++---- src/hls/RTLPargenproof.v | 82 ++++++++++++++++++++++++++--------- 2 files changed, 164 insertions(+), 27 deletions(-) (limited to 'src') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index f64a796..d2a7174 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -978,6 +978,62 @@ Proof. { eapply sem_update_store; eauto. } Qed. +Lemma sem_update2_Op : + forall A ge sp st f r l o0 o m rs v, + @sem A ge sp st f (InstrState rs m) -> + Op.eval_operation ge sp o0 rs ## l m = Some v -> + sem ge sp st (update f (RBop o o0 l r)) (InstrState (Regmap.set r v rs) m). +Proof. + intros. destruct st. constructor. + inv H. inv H6. + { constructor; intros. simplify. + destruct (Pos.eq_dec r x); subst. + { rewrite map2. econstructor. eauto. + apply gen_list_base. eauto. + rewrite Regmap.gss. auto. } + { rewrite genmap1; crush. rewrite Regmap.gso; auto. } } + { simplify. rewrite genmap1; crush. inv H. eauto. } +Qed. + +Lemma sem_update2_load : + forall A ge sp st f r o m a l m0 rs v a0, + @sem A ge sp st f (InstrState rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.loadv m m0 a0 = Some v -> + sem ge sp st (update f (RBload o m a l r)) (InstrState (Regmap.set r v rs) m0). +Proof. + intros. simplify. inv H. inv H7. constructor. + { constructor; intros. destruct (Pos.eq_dec r x); subst. + { rewrite map2. rewrite Regmap.gss. econstructor; eauto. + apply gen_list_base; eauto. } + { rewrite genmap1; crush. rewrite Regmap.gso; eauto. } + } + { simplify. rewrite genmap1; crush. } +Qed. + +Lemma sem_update2_store : + forall A ge sp a0 m a l r o f st m' rs m0, + @sem A ge sp st f (InstrState rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.storev m m0 a0 rs !! r = Some m' -> + sem ge sp st (update f (RBstore o m a l r)) (InstrState rs m'). +Proof. + intros. simplify. inv H. inv H7. constructor; simplify. + { econstructor; intros. rewrite genmap1; crush. } + { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. } +Qed. + +Lemma sem_update2 : + forall A ge sp st x st' st'' f, + sem ge sp st f st' -> + @step_instr A ge sp st' x st'' -> + sem ge sp st (update f x) st''. +Proof. + intros. + destruct x; inv H0; + eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store. +Qed. + Lemma rtlblock_trans_correct : forall bb ge sp st st', RTLBlock.step_instr_list ge sp st bb st' -> @@ -997,13 +1053,6 @@ Proof. auto. } Qed. -Lemma rtlpar_trans_correct : - forall ge sp bb sem_st' sem_st, - sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> - exists st', RTLPar.step_instr_block ge sp sem_st bb st' - /\ match_states sem_st' st'. -Proof. Admitted. - Lemma abstr_sem_val_mem : forall A B ge tge st tst sp a, ge_preserved ge tge -> @@ -1203,6 +1252,50 @@ Proof. exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto. Qed. +Lemma sem_update' : + forall A ge sp st a x st', + sem ge sp st (update (abstract_sequence empty a) x) st' -> + exists st'', + @step_instr A ge sp st'' x st' /\ + sem ge sp st (abstract_sequence empty a) st''. +Proof. + Admitted. + +Lemma sem_separate : + forall A (ge: @RTLBlockInstr.genv A) b a sp st st', + sem ge sp st (abstract_sequence empty (a ++ b)) st' -> + exists st'', + sem ge sp st (abstract_sequence empty a) st'' + /\ sem ge sp st'' (abstract_sequence empty b) st'. +Proof. + induction b using rev_ind; simplify. + { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } + { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. + exploit sem_update'; eauto; inv_simp. + exploit IHb; eauto; inv_simp. + econstructor; split; eauto. + rewrite abstract_seq. + eapply sem_update2; eauto. + } +Qed. + +Lemma rtlpar_trans_correct : + forall bb ge sp sem_st' sem_st st, + sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> + match_states sem_st st -> + exists st', RTLPar.step_instr_block ge sp st bb st' + /\ match_states sem_st' st'. +Proof. + induction bb using rev_ind. + { repeat econstructor. eapply abstract_interp_empty3 in H. + inv H. inv H0. constructor; congruence. } + { simplify. inv H0. repeat rewrite concat_app in H. simplify. + rewrite app_nil_r in H. + exploit sem_separate; eauto; inv_simp. + repeat econstructor. admit. admit. + } +Admitted. + Lemma abstract_execution_correct: forall bb bb' cfi ge tge sp st st' tst, RTLBlock.step_instr_list ge sp st bb st' -> @@ -1219,7 +1312,7 @@ Proof. try solve [eassumption | apply state_lessdef_match_sem; eassumption]. apply match_states_commut. eauto. inv_simp. exploit rtlpar_trans_correct; try eassumption; []; inv_simp. - exploit step_instr_block_matches; eauto; inv_simp. + exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp. repeat match goal with | H: match_states _ _ |- _ => inv H end. do 2 econstructor; eauto. econstructor; congruence. diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index eb7931e..e8167e9 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -38,7 +38,7 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs rs', transl_function f = OK tf -> - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> match_stackframes (Stackframe res f sp pc rs) (Stackframe res tf sp pc rs'). @@ -47,25 +47,23 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := forall sf f sp pc rs rs' m m' sf' tf (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: regs_lessdef rs rs') + (REG: forall x, rs !! x = rs' !! x) (MEM: Mem.extends m m'), match_states (State sf f sp pc rs m) (State sf' tf sp pc rs' m') | match_returnstate: - forall stack stack' v v' m m' + forall stack stack' v m m' (STACKS: list_forall2 match_stackframes stack stack') - (MEM: Mem.extends m m') - (LD: Val.lessdef v v'), + (MEM: Mem.extends m m'), match_states (Returnstate stack v m) - (Returnstate stack' v' m') + (Returnstate stack' v m') | match_callstate: - forall stack stack' f tf args args' m m' + forall stack stack' f tf args m m' (TRANSL: transl_fundef f = OK tf) (STACKS: list_forall2 match_stackframes stack stack') - (LD: Val.lessdef_list args args') (MEM: Mem.extends m m'), match_states (Callstate stack f args m) - (Callstate stack' tf args' m'). + (Callstate stack' tf args m'). Section CORRECTNESS. @@ -121,7 +119,7 @@ Section CORRECTNESS. Lemma find_function_translated: forall ros rs rs' f, - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> find_function ge ros rs = Some f -> exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. @@ -134,7 +132,7 @@ Section CORRECTNESS. | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H] | _ => solve [exploit functions_translated; eauto] end. - unfold regs_lessdef; destruct ros; simplify; try rewrite <- H; + destruct ros; simplify; try rewrite <- H; [| rewrite symbols_preserved; destruct_match; try (apply function_ptr_translated); crush ]; intros; @@ -160,8 +158,8 @@ Section CORRECTNESS. Qed. Lemma eval_op_eq: - forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val), - Op.eval_operation ge sp0 op vl = Op.eval_operation tge sp0 op vl. + forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m, + Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m. Proof using TRANSL. intros. destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32; @@ -197,6 +195,16 @@ Section CORRECTNESS. Proof using. destruct or; crush. Qed. Hint Resolve lessdef_regmap_optget : rtlgp. + Lemma regmap_equiv_lessdef: + forall rs rs', + (forall x, rs !! x = rs' !! x) -> + regs_lessdef rs rs'. + Proof using. + intros; unfold regs_lessdef; intros. + rewrite H. apply Val.lessdef_refl. + Qed. + Hint Resolve regmap_equiv_lessdef : rtlgp. + Lemma int_lessdef: forall rs rs', regs_lessdef rs rs' -> @@ -227,8 +235,8 @@ Section CORRECTNESS. let H2 := fresh "SCHED" in learn H as H2; apply schedule_oracle_nil in H2 - | [ H: find_function _ _ _ = Some _ |- _ ] => - learn H; exploit find_function_translated; eauto; inversion 1 + | [ H: find_function _ _ _ = Some _, H2: forall x, ?rs !! x = ?rs' !! x |- _ ] => + learn H; exploit find_function_translated; try apply H2; eauto; inversion 1 | [ H: Mem.free ?m _ _ _ = Some ?m', H2: Mem.extends ?m ?m'' |- _ ] => learn H; exploit Mem.free_parallel_extends; eauto; intros | [ H: Events.eval_builtin_args _ _ _ _ _ _, H2: regs_lessdef ?rs ?rs' |- _ ] => @@ -249,6 +257,29 @@ Section CORRECTNESS. Hint Resolve set_reg_lessdef : rtlgp. Hint Resolve Op.eval_condition_lessdef : rtlgp. + Hint Constructors Events.eval_builtin_arg: barg. + + Lemma eval_builtin_arg_eq: + forall A ge a v1 m1 e1 e2 sp, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_arg A ge e1 sp m1 a v1 -> + Events.eval_builtin_arg ge e2 sp m1 a v1. +Proof. induction 2; try rewrite H; eauto with barg. Qed. + + Lemma eval_builtin_args_lessdef: + forall A ge e1 sp m1 e2 al vl1, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_args A ge e1 sp m1 al vl1 -> + Events.eval_builtin_args ge e2 sp m1 al vl1. + Proof. + induction 2. + - econstructor; split. + - exploit eval_builtin_arg_eq; eauto. intros. + destruct IHlist_forall2 as [| y]. constructor; eauto. + constructor. constructor; auto. + constructor; eauto. + Qed. + Lemma step_cf_instr_correct: forall cfi t s s', step_cf_instr ge s cfi t s' -> @@ -256,8 +287,20 @@ Section CORRECTNESS. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl; + induction 1; repeat semantics_simpl. + { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } + { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } + { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + exploit Events.eval_builtin_args_lessdef. + } repeat (econstructor; eauto with rtlgp). + erewrite match_states_list; eauto. + repeat (econstructor; eauto with rtlgp). + } + repeat (econstructor; eauto with rtlgp). + exploit find_function_translated. eauto. Qed. Theorem transl_step_correct : @@ -269,11 +312,12 @@ Section CORRECTNESS. Proof. induction 1; repeat semantics_simpl. - Abort. -(* { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. + { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. assert (bbe = bbe') by admit. rewrite H3 in H5. + exploit abstract_execution_correct. eauto. apply ge_preserved_lem. + eauto. eapply abstract_execution_correct in H5; eauto with rtlgp. repeat econstructor; eauto with rtlgp. simplify. exploit step_cf_instr_correct. eauto. @@ -283,6 +327,6 @@ Section CORRECTNESS. repeat econstructor; eauto. } { 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. } - Qed.*) + Qed. End CORRECTNESS. -- cgit