From 60ab47c6ff0db1b690afe6fd2c2b63cf5843ced1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:51:49 +0100 Subject: Add proof of translation correctness Modified-by: Yann Herklotz --- src/translation/HTLgenproof.v | 201 ++++++++++++++++++++++++++++++++++++++++-- src/translation/HTLgenspec.v | 16 ++-- 2 files changed, 200 insertions(+), 17 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 7a4ec34..ff7c24d 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -23,14 +23,22 @@ From compcert Require RTL Registers Globalenvs AST. Import AssocMapNotation. Inductive match_assocmaps : RTL.regset -> assocmap -> Prop := -| match_assocmap : forall r rs am, - val_value_lessdef (Registers.Regmap.get r rs) am#r -> +| match_assocmap : forall rs am, + (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) -> match_assocmaps rs am. +Definition state_st_wf (m : HTL.module) (s : HTL.state) := + forall st assoc, + s = HTL.State m st assoc -> + assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st). + Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st, - match_assocmaps rs assoc -> - tr_module f m -> +| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st + (MASSOC : match_assocmaps rs assoc) + (TF : tr_module f m) + (TC : tr_code f.(RTL.fn_code) st m.(HTL.mod_datapath) m.(HTL.mod_controllogic) + m.(HTL.mod_finish) m.(HTL.mod_return) m.(HTL.mod_st)) + (WF : state_st_wf m (HTL.State m st assoc)), match_states (RTL.State sf f sp st rs mem) (HTL.State m st assoc) | match_returnstate : forall v v' stack m, @@ -46,6 +54,80 @@ Inductive match_program : RTL.program -> HTL.module -> Prop := tr_module f m -> match_program p m. +Lemma regs_lessdef_regs : + forall rs1 rs2 n v, + match_assocmaps rs1 rs2 -> + match_assocmaps rs1 (AssocMap.add n v rs2). +Admitted. + +Lemma regs_add_match : + forall rs am r v v', + match_assocmaps rs am -> + val_value_lessdef v v' -> + match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am). +Admitted. + +Lemma merge_inj : + forall am am' r v, + merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am'). +Admitted. + +Lemma valToValue_lessdef : + forall v, + val_value_lessdef v (valToValue v). +Admitted. + +Lemma assocmap_merge_add : + forall k v assoc, + AssocMap.add k v assoc = merge_assocmap (AssocMap.add k v empty_assocmap) assoc. +Admitted. + +(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) +Lemma assumption_32bit : + forall v, + valueToPos (posToValue 32 v) = v. +Admitted. + +Lemma regset_assocmap_get : + forall r rs am v v', + match_assocmaps rs am -> + v = Registers.Regmap.get r rs -> + v' = am#r -> + val_value_lessdef v v'. +Proof. inversion 1. intros. subst. apply H0. Qed. + +Lemma regset_assocmap_wf : + forall r rs am i, + match_assocmaps rs am -> + Values.Vint i <> Registers.Regmap.get r rs -> + am!r = None. +Admitted. + +Lemma regset_assocmap_wf2 : + forall r rs am i, + match_assocmaps rs am -> + Values.Vint i = Registers.Regmap.get r rs -> + am!r = Some (intToValue i). +Admitted. + +Lemma access_merge_assocmap : + forall nb r v am, + nb!r = Some v -> + (merge_assocmap nb am) ! r = Some v. +Admitted. + +Lemma st_greater_than_res : + forall m res, + (HTL.mod_st m) <> res. +Admitted. + +Ltac subst_eq_hyp := + match goal with + H1: ?x = Some ?i, H2: ?x = Some ?j |- _ => + let H := fresh "H" in + rewrite H1 in H2; injection H2; intro H; clear H2; subst + end. + Section CORRECTNESS. Variable prog : RTL.program. @@ -56,22 +138,123 @@ Section CORRECTNESS. Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. Let tge : HTL.genv := HTL.genv_empty. + Lemma eval_correct : + forall sp op rs args m v e assoc f, + Op.eval_operation ge sp op +(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> + tr_op op args e -> + Verilog.expr_runp f assoc e (valToValue v). + Admitted. + (** The proof of semantic preservation for the translation of instructions is a simulation argument based on diagrams of the following form: << - I /\ P + match_states code st rs ---------------- State m st assoc || | || | || | \/ v code st rs' --------------- State m st assoc' - I /\ Q + I >> where [tr_code c data control fin rtrn st] is assumed to hold. + + The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. *) - Definition transl_code_prop : Prop := - HTL.step tge (HTL.State) + Definition transl_instr_prop (instr : RTL.instruction) : Prop := + forall m assoc fin rtrn st stmt trans, + tr_instr fin rtrn st instr stmt trans -> + exists assoc', + HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). + + Theorem transl_step_correct: + forall (S1 : RTL.state) t S2, + RTL.step ge S1 t S2 -> + forall (R1 : HTL.state), + match_states S1 R1 -> + exists R2, HTL.step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE. + - (* Inop *) + inversion MSTATE. subst. + econstructor. + split. + + inversion TC. + eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H3; subst. + apply H2. + apply H1. + (* processing of state *) + econstructor. + simpl. trivial. + econstructor. trivial. + inversion H3. subst. + econstructor. + + (* prove merge *) + apply assocmap_merge_add. + + (* prove stval *) + apply AssocMap.gss. + apply assumption_32bit. + + (* prove match_state *) + constructor. + apply rs. + apply regs_lessdef_regs. + assumption. + inversion TF. simpl. apply H0. + assumption. + unfold state_st_wf. intros. inversion H0. subst. + apply AssocMap.gss. + - (* Iop *) + inversion MSTATE. subst. + econstructor. + split. + + inversion TC. + eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H4; subst. + apply H3. + apply H2. + econstructor. + simpl. trivial. + constructor. trivial. + econstructor. + simpl. trivial. + eapply eval_correct. apply H0. apply H10. trivial. trivial. + apply access_merge_assocmap. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + trivial. + + (* match_states *) + assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit. + rewrite <- H1. + constructor. apply rs0. + rewrite merge_inj. + apply regs_add_match. + rewrite merge_inj. + unfold merge_assocmap. rewrite AssocMapExt.merge_base. + apply regs_lessdef_regs. + assumption. + apply valToValue_lessdef. + + inversion TF. simpl. apply H2. + assumption. + + unfold state_st_wf. intros. inversion H2. subst. + rewrite merge_inj. + rewrite AssocMap.gso. + rewrite merge_inj. + apply AssocMap.gss. + apply st_greater_than_res. + - inversion MSTATE. inversion TC. subst. + econstructor. constructor. + inversion H12; subst_eq_hyp; discriminate. + apply match_state. apply rs0. + apply regs_add_match. apply MASSOC. apply valToValue_lessdef. + inversion TF. rewrite H3. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index fb1c70d..e2d788c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -70,20 +70,20 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr tr_instr fin rtrn st (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. -Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt) +Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts trans : PositiveMap.t stmnt) (fin rtrn st : reg) : Prop := tr_code_intro : - forall i s t n, - Maps.PTree.get n c = Some i -> - stmnts!n = Some s -> - trans!n = Some t -> + forall i s t, + Maps.PTree.get pc c = Some i -> + stmnts!pc = Some s -> + trans!pc = Some t -> tr_instr fin rtrn st i s t -> - tr_code c stmnts trans fin rtrn st. + tr_code c pc stmnts trans fin rtrn st. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall c data control fin rtrn st, - tr_code c data control fin rtrn st -> + forall data control fin rtrn st, + (forall pc, tr_code f.(RTL.fn_code) pc data control fin rtrn st) -> tr_module f (mkmodule f.(RTL.fn_params) data -- cgit