From c76ac9be323e3513aa0db2721ecd0f6c3987aef0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jul 2020 18:45:14 +0100 Subject: Fix Inop --- src/translation/HTLgen.v | 33 ++++++++++++++++++++++----------- src/translation/HTLgenproof.v | 25 ++++++++++++++----------- src/translation/HTLgenspec.v | 30 ++++++++++++++++++++++-------- src/translation/Veriloggenspec.v | 17 ----------------- 4 files changed, 58 insertions(+), 47 deletions(-) delete mode 100644 src/translation/Veriloggenspec.v diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index e02d759..b4f6b51 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -428,24 +428,35 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni match ni with (n, i) => match i with - | Inop n' => add_instr n n' Vskip + | Inop n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + add_instr n n' Vskip + else error (Errors.msg "State is larger than 2^32.") | Iop op args dst n' => - do instr <- translate_instr op args; - do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst instr) + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst instr) + else error (Errors.msg "State is larger than 2^32.") | Iload mem addr args dst n' => - do src <- translate_arr_access mem addr args stack; - do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst src) + else error (Errors.msg "State is larger than 2^32.") | Istore mem addr args src n' => - do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do dst <- translate_arr_access mem addr args stack; + add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + else error (Errors.msg "State is larger than 2^32.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") | Icond cond args n1 n2 => - do e <- translate_condition cond args; - add_branch_instr e n n1 n2 + if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then + do e <- translate_condition cond args; + add_branch_instr e n n1 n2 + else error (Errors.msg "State is larger than 2^32.") | Ijumptable r tbl => do s <- get; add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 305c14f..fe4faf5 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -87,11 +87,12 @@ Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_frames_nil : match_frames nil nil. - Lemma assumption_32bit : - forall v, - valueToPos (posToValue v) = v. - Proof. - Admitted. +Inductive match_constants : HTL.module -> assocmap -> Prop := + match_constant : + forall m asr, + asr!(HTL.mod_reset m) = Some (ZToValue 0) -> + asr!(HTL.mod_finish m) = Some (ZToValue 0) -> + match_constants m asr. Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res @@ -103,7 +104,8 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) - (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), + (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) + (CONST : match_constants m asr), match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa) | match_returnstate : @@ -443,8 +445,6 @@ Section CORRECTNESS. Ltac tac0 := match goal with - | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit - | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge @@ -502,7 +502,8 @@ Section CORRECTNESS. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST; assumption. + inv CONST; assumption. (* processing of state *) econstructor. crush. @@ -511,8 +512,10 @@ Section CORRECTNESS. econstructor. all: invert MARR; big_tac. - Unshelve. - constructor. + + inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. + + Unshelve. auto. Qed. Hint Resolve transl_inop_correct : htlproof. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a9626c4..f0508bd 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -17,7 +17,7 @@ *) From compcert Require RTL Op Maps Errors. -From compcert Require Import Maps. +From compcert Require Import Maps Integers. From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. @@ -117,13 +117,17 @@ translations for each of the elements *) Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : forall n, + Z.pos n <= Int.max_unsigned -> tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) | tr_instr_Iop : forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : @@ -135,10 +139,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : forall mem addr args s s' i c dst n, + Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, + Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) (state_goto st n) @@ -415,12 +421,12 @@ Lemma transf_instr_freshreg_trans : Proof. intros. destruct instr eqn:?. subst. unfold transf_instr in H. destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. + - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. Qed. @@ -445,13 +451,16 @@ Ltac rewrite_states := Ltac inv_add_instr' H := match type of H with + | ?f _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H end; repeat unfold_match H; inversion H. Ltac inv_add_instr := - lazymatch goal with + match goal with + | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -491,23 +500,27 @@ Proof. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + apply Z.leb_le. assumption. eapply in_map with (f := fst) in H9. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply Z.leb_le; assumption. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. @@ -516,6 +529,7 @@ Proof. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. + econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v deleted file mode 100644 index 7dc632c..0000000 --- a/src/translation/Veriloggenspec.v +++ /dev/null @@ -1,17 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) -- cgit From 78e549331ba3f136ebe94955f68767bd384df454 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 14:09:54 +0100 Subject: HTLgenproof compiles again - Commented out Iload, Istore proofs for now --- src/Compiler.v | 7 ++++++- src/translation/HTLgenproof.v | 44 +++++++++++++++++++++++++++++-------------- src/verilog/HTL.v | 6 ++++-- src/verilog/Verilog.v | 12 +++++++----- 4 files changed, 47 insertions(+), 22 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index a34b359..17d8921 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -48,7 +48,9 @@ From compcert.driver Require From coqup Require Verilog Veriloggen - HTLgen. + Veriloggenproof + HTLgen + HTLgenproof. Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. @@ -107,6 +109,9 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog + ::: mkpass Inliningproof.match_prog + ::: mkpass HTLgenproof.match_prog + ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. Definition match_prog: Csyntax.program -> RTL.program -> Prop := diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index fe4faf5..338e77d 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -537,7 +537,8 @@ Section CORRECTNESS. econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST. assumption. + inv CONST. assumption. econstructor; simpl; trivial. constructor; trivial. econstructor; simpl; eauto. @@ -555,7 +556,8 @@ Section CORRECTNESS. assert (Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in H12; lia. - unfold_merge. simpl. + Admitted. +(* unfold_merge. simpl. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. @@ -608,7 +610,7 @@ Section CORRECTNESS. apply AssocMap.gss. apply st_greater_than_res. assumption. - Admitted. + Admitted.*) Hint Resolve transl_iop_correct : htlproof. Ltac tac := @@ -680,7 +682,7 @@ Section CORRECTNESS. (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + (*assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. apply PtrofsExtra.add_mod; crush. rewrite Integers.Ptrofs.unsigned_repr_eq. @@ -1024,7 +1026,7 @@ Section CORRECTNESS. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. + rewrite NORMALISE in H0. rewrite H1 in H0. assumption.*) Admitted. Hint Resolve transl_iload_correct : htlproof. @@ -1041,7 +1043,7 @@ Section CORRECTNESS. exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. Proof. - intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. +(* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. inv_state. inv_arr_access. + (** Preamble *) @@ -1838,7 +1840,7 @@ Section CORRECTNESS. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. + apply X in H0. invert H0. congruence.*) Admitted. Hint Resolve transl_istore_correct : htlproof. @@ -1859,8 +1861,9 @@ Section CORRECTNESS. eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. - eapply Verilog.stmnt_runp_Vnonblock_reg with + inv CONST; assumption. + inv CONST; assumption. +(* eapply Verilog.stmnt_runp_Vnonblock_reg with (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). constructor. @@ -1883,7 +1886,8 @@ Section CORRECTNESS. Unshelve. constructor. - Qed. + Qed.*) + Admitted. Hint Resolve transl_icond_correct : htlproof. Lemma transl_ijumptable_correct: @@ -1921,7 +1925,8 @@ Section CORRECTNESS. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST; assumption. + inv CONST; assumption. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -1932,6 +1937,9 @@ Section CORRECTNESS. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. apply HTL.step_finish. unfold Verilog.merge_regs. @@ -1948,7 +1956,8 @@ Section CORRECTNESS. - econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST; assumption. + inv CONST; assumption. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -1957,6 +1966,10 @@ Section CORRECTNESS. unfold state_st_wf in WF; big_tac; eauto. + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. + apply HTL.step_finish. unfold Verilog.merge_regs. unfold_merge. @@ -2001,8 +2014,9 @@ Section CORRECTNESS. all: big_tac. - apply regs_lessdef_add_greater. - unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. apply init_reg_assoc_empty. constructor. @@ -2078,6 +2092,8 @@ Section CORRECTNESS. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. crush. apply proj_sumbool_true in H10. lia. + constructor. simplify. rewrite AssocMap.gss. + simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia. Opaque Mem.alloc. Opaque Mem.load. Opaque Mem.store. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 3ba5b59..b3d1442 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -141,8 +141,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 064474a..9659189 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -736,8 +736,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g res m args, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) - (init_params args m.(mod_args))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) + (init_params args m.(mod_args))))) (empty_stack m)) | step_return : forall g m asr i r sf pc mst asa, @@ -884,9 +886,9 @@ Lemma semantics_determinate : Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. - (*pose proof (mis_stepp_determinate H4 H13)*) - admit. + - invert H; invert H0; crush. assert (f = f0) by admit; subst. + pose proof (mis_stepp_determinate H5 H15). + crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. - red; simplify; intro; invert H0; invert H; crush. -- cgit