diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
commit | e06577fe952a3c268520b280b020bb2bff252529 (patch) | |
tree | 6a96dd75f90a81ea80108c909a98bc78ecdabd66 /src/translation | |
parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
download | vericert-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-e06577fe952a3c268520b280b020bb2bff252529.zip |
Fix compilation moving to PTree
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 24 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 31 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 4 |
3 files changed, 34 insertions, 25 deletions
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 <https://www.gnu.org/licenses/>. *) -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, |