From 8151bbfa57bac1a302d3330f8b51fa23eb3a0082 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 30 Jan 2021 11:27:36 +0000 Subject: Fix proofs with better defined equality --- src/hls/RTLPargen.v | 17 ++++-------- src/hls/RTLPargenproof.v | 71 ++++++++++++++++++++++++++++++++++-------------- 2 files changed, 57 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 7acf6d2..0b79d2d 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -460,17 +460,10 @@ Lemma ge_preserved_same: Proof. unfold ge_preserved; auto. Qed. Hint Resolve ge_preserved_same : rtlpar. -Definition reg_lessdef (rs rs': regset) := forall x, rs !! x = rs' !! x. - -Lemma regs_lessdef_regs: - forall rs1 rs2, reg_lessdef rs1 rs2 -> - forall rl, rs1##rl = rs2##rl. -Proof. induction rl; crush. Qed. - Inductive sem_state_ld : sem_state -> sem_state -> Prop := | sem_state_ld_intro: forall rs rs' m m', - reg_lessdef rs rs' -> + regs_lessdef rs rs' -> m = m' -> sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m'). @@ -527,14 +520,16 @@ Proof. simplify; eauto with rtlpar. Qed. +Hint Resolve Val.lessdef_same : rtlpar. + Lemma sem_regset_det: forall FF ge tge sp st f v v', ge_preserved ge tge -> sem_regset FF ge sp st f v -> sem_regset FF tge sp st f v' -> - reg_lessdef v v'. + regs_lessdef v v'. Proof. - intros; unfold reg_lessdef; + intros; unfold regs_lessdef. inv H0; inv H1; eauto with rtlpar. Qed. @@ -666,7 +661,7 @@ Lemma abstract_execution_correct: schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m') - /\ reg_lessdef rs' rs''. + /\ regs_lessdef rs' rs''. Proof. Admitted. (*| diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 01d4542..c19e80a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -21,6 +21,8 @@ Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. @@ -36,29 +38,34 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs rs', transl_function f = OK tf -> - reg_lessdef rs rs' -> + regs_lessdef rs rs' -> match_stackframes (Stackframe res f sp pc rs) (Stackframe res tf sp pc rs'). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' mem sf' tf + 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: reg_lessdef rs rs'), - match_states (State sf f sp pc rs mem) - (State sf' tf sp pc rs' mem) + (REG: regs_lessdef rs rs') + (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 mem - (STACKS: list_forall2 match_stackframes stack stack'), - match_states (Returnstate stack v mem) - (Returnstate stack' v mem) + forall stack stack' v v' m m' + (STACKS: list_forall2 match_stackframes stack stack') + (MEM: Mem.extends m m') + (LD: Val.lessdef v v'), + match_states (Returnstate stack v m) + (Returnstate stack' v' m') | match_callstate: - forall stack stack' f tf args m + forall stack stack' f tf args args' m m' (TRANSL: transl_fundef f = OK tf) - (STACKS: list_forall2 match_stackframes stack stack'), + (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. @@ -109,17 +116,29 @@ Section CORRECTNESS. Qed. Hint Resolve sig_transl_function : rtlgp. + Hint Resolve Val.lessdef_same : rtlgp. + Hint Resolve regs_lessdef_regs : rtlgp. + Lemma find_function_translated: forall ros rs rs' f, - reg_lessdef rs rs' -> + regs_lessdef rs rs' -> find_function ge ros rs = Some f -> exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. Proof using TRANSL. - unfold reg_lessdef; destruct ros; simplify; try rewrite <- H; - [ exploit functions_translated; eauto - | rewrite symbols_preserved; destruct_match; - try (apply function_ptr_translated); crush ]. + Ltac ffts := match goal with + | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] => + specialize (H r); inv H + | [ H: Vundef = ?r, H1: Genv.find_funct _ ?r = Some _ |- _ ] => + rewrite <- H in H1 + | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H] + | _ => solve [exploit functions_translated; eauto] + end. + unfold regs_lessdef; destruct ros; simplify; try rewrite <- H; + [| rewrite symbols_preserved; destruct_match; + try (apply function_ptr_translated); crush ]; + intros; + repeat ffts. Qed. Lemma schedule_oracle_nil: @@ -190,6 +209,9 @@ Section CORRECTNESS. Hint Resolve Events.eval_builtin_args_preserved : rtlgp. Hint Resolve Events.external_call_symbols_preserved : rtlgp. + Hint Resolve set_res_lessdef : rtlgp. + Hint Resolve set_reg_lessdef : rtlgp. + Hint Resolve Op.eval_condition_lessdef : rtlgp. Lemma step_cf_instr_correct: forall cfi t s s', @@ -199,9 +221,18 @@ Section CORRECTNESS. exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. induction 1; repeat semantics_simpl. - - { repeat econstructor. eauto with rtlgp. } - repeat econstructor; eauto with rtlgp. + repeat (econstructor; eauto with rtlgp). + exploit Mem.free_parallel_extends; eauto; intros. inv H4. inv H8. + repeat (econstructor; eauto with rtlgp). + exploit Events.eval_builtin_args_lessdef. apply REG. apply MEM. apply H. intros. inv H2. inv H3. + exploit Events.external_call_mem_extends. eauto. eauto. eauto. intros. inv H3. inv H5. simplify. + repeat (econstructor; eauto with rtlgp). + repeat (econstructor; eauto with rtlgp). + repeat (econstructor; eauto with rtlgp). + unfold regs_lessdef in REG; specialize (REG arg); inv REG; crush. + exploit Mem.free_parallel_extends; eauto; intros. inv H1. simplify. + repeat (econstructor; eauto with rtlgp). + unfold regmap_optget. destruct or; crush. Qed. Theorem transl_step_correct : -- cgit