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/RTLPargenproof.v | 82 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 63 insertions(+), 19 deletions(-) (limited to 'src/hls/RTLPargenproof.v') 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