From e06577fe952a3c268520b280b020bb2bff252529 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 18:14:59 +0100 Subject: Fix compilation moving to PTree --- src/translation/HTLgen.v | 24 ++++++++++++------------ src/translation/HTLgenproof.v | 31 ++++++++++++++++++++----------- src/translation/HTLgenspec.v | 4 ++-- src/verilog/AssocMap.v | 4 ++++ src/verilog/HTL.v | 7 +++---- src/verilog/Verilog.v | 14 +++++++------- 6 files changed, 48 insertions(+), 36 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 26dc630..4564237 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -120,8 +120,8 @@ Lemma add_instr_state_incr : s.(st_st) s.(st_freshreg) (st_freshstate s) - (AssocMap.add n st s.(st_datapath)) - (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic))). + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -136,8 +136,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := s.(st_st) s.(st_freshreg) (st_freshstate s) - (AssocMap.add n st s.(st_datapath)) - (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic))) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) (add_instr_state_incr s n n' st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -151,8 +151,8 @@ Lemma add_instr_skip_state_incr : s.(st_st) s.(st_freshreg) (st_freshstate s) - (AssocMap.add n st s.(st_datapath)) - (AssocMap.add n Vskip s.(st_controllogic))). + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -167,8 +167,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := s.(st_st) s.(st_freshreg) (st_freshstate s) - (AssocMap.add n st s.(st_datapath)) - (AssocMap.add n Vskip s.(st_controllogic))) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) (add_instr_skip_state_incr s n st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -274,8 +274,8 @@ Lemma add_branch_instr_state_incr: s.(st_st) (st_freshreg s) (st_freshstate s) - (AssocMap.add n Vskip (st_datapath s)) - (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). Proof. intros. apply state_incr_intro; simpl; try (intros; destruct (peq n0 n); subst); @@ -290,8 +290,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := s.(st_st) (st_freshreg s) (st_freshstate s) - (AssocMap.add n Vskip (st_datapath s)) - (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") end. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index b7b9d27..2d2129c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -26,6 +26,8 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof. Hint Resolve AssocMap.gss : htlproof. Hint Resolve AssocMap.gso : htlproof. +Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. + Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := match_assocmap : forall f rs am, (forall r, Ple r (RTL.max_reg_function f) -> @@ -61,37 +63,39 @@ Inductive match_program : RTL.program -> HTL.module -> Prop := match_program p m. Hint Constructors match_program : htlproof. -Lemma regs_lessdef_regs : +Lemma regs_lessdef_add_greater : forall f rs1 rs2 n v, Plt (RTL.max_reg_function f) n -> match_assocmaps f rs1 rs2 -> - match_assocmaps f rs1 (AssocMap.add n v rs2). + match_assocmaps f rs1 (AssocMap.set n v rs2). Proof. inversion 2; subst. intros. constructor. - intros. unfold find_assocmap. unfold AssocMapExt.find_default. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gso. eauto. apply Pos.le_lt_trans with _ _ n in H2. unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. Qed. +Hint Resolve regs_lessdef_add_greater : htlproof. -Lemma regs_add_match : +Lemma regs_lessdef_add_match : forall f rs am r v v', val_value_lessdef v v' -> match_assocmaps f rs am -> - match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am). + match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). Proof. inversion 2; subst. constructor. intros. destruct (peq r0 r); subst. rewrite Registers.Regmap.gss. - unfold find_assocmap. unfold AssocMapExt.find_default. + unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gss. assumption. rewrite Registers.Regmap.gso; try assumption. - unfold find_assocmap. unfold AssocMapExt.find_default. + unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gso; eauto. Qed. +Hint Resolve regs_lessdef_add_match : htlproof. Lemma valToValue_lessdef : forall v v', @@ -198,6 +202,11 @@ Section CORRECTNESS. exists assoc', HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). + Lemma greater_than_max_func : + forall f st, + Plt (RTL.max_reg_function f) st. + Proof. Admitted. + Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -218,14 +227,14 @@ Section CORRECTNESS. econstructor. (* prove stval *) - unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss. + unfold_merge. simpl. apply AssocMap.gss. (* prove match_state *) rewrite assumption_32bit. constructor; auto. - unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss. - apply regs_lessdef_regs. assumption. - unfold state_st_wf. inversion 1. subst. apply AssocMap.gss. + unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func. + assumption. + unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. - (* Iop *) econstructor. split. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index b9d483c..5a61a9c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -16,8 +16,8 @@ * along with this program. If not, see . *) -From Coq Require Import FSets.FMapPositive. From compcert Require RTL Op Maps Errors. +From compcert Require Import Maps. From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -160,7 +160,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. Hint Constructors tr_instr : htlspec. -Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt) +Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) (fin rtrn st : reg) : Prop := tr_code_intro : forall s t, diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 43f9065..88b13a6 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -198,6 +198,10 @@ Definition empty_assocmap : assocmap := AssocMap.empty value. Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. +Ltac unfold_merge := + unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); + rewrite AssocMapExt.merge_base_1. + Module AssocMapNotation. Notation "a ! b" := (AssocMap.get b a) (at level 1). Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 36e4434..a21064c 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -20,6 +20,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers. +From compcert Require Import Maps. Import HexNotationValue. @@ -29,13 +30,11 @@ hardware-like layout that is still similar to the register transfer language instantiations and that we now describe a state machine instead of a control-flow graph. *) -Notation "a ! b" := (PositiveMap.find b a) (at level 1). - Definition reg := positive. Definition node := positive. -Definition datapath := PositiveMap.t Verilog.stmnt. -Definition controllogic := PositiveMap.t Verilog.stmnt. +Definition datapath := PTree.t Verilog.stmnt. +Definition controllogic := PTree.t Verilog.stmnt. Record module: Type := mkmodule { diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index c1e0a79..ce7ddd9 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -171,13 +171,13 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := PositiveMap.t value. +Definition fext := AssocMap.t value. Definition fextclk := nat -> fext. (** ** State The [state] contains the following items: - +n - Current [module] that is being worked on, so that the state variable can be retrieved and set appropriately. - Current [module_item] which is being worked on. @@ -300,7 +300,7 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. Definition access_fext (f : fext) (r : reg) : res value := - match PositiveMap.find r f with + match AssocMap.get r f with | Some v => OK v | _ => OK (ZToValue 1 0) end. @@ -452,7 +452,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := forall lhs name rhs rhsval assoc assoc' nbassoc f, assign_name lhs = OK name -> expr_runp f assoc rhs rhsval -> - assoc' = (PositiveMap.add name rhsval assoc) -> + assoc' = (AssocMap.set name rhsval assoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vblock lhs rhs) (mkassociations assoc' nbassoc) @@ -460,7 +460,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := forall lhs name rhs rhsval assoc nbassoc nbassoc' f, assign_name lhs = OK name -> expr_runp f assoc rhs rhsval -> - nbassoc' = (PositiveMap.add name rhsval nbassoc) -> + nbassoc' = (AssocMap.set name rhsval nbassoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vnonblock lhs rhs) (mkassociations assoc nbassoc'). @@ -534,8 +534,8 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) - | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) + | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) end. (*Definition module_run (n : nat) (m : module) : res assocmap := -- cgit