From 9aa32499597678e3b0e7ef0b8a85ca5beda44938 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 29 Jun 2020 12:21:38 +0100 Subject: Add missing file. --- src/common/ZExtra.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/common/ZExtra.v diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v new file mode 100644 index 0000000..a0dd717 --- /dev/null +++ b/src/common/ZExtra.v @@ -0,0 +1,34 @@ +Require Import ZArith. +Require Import Lia. + +Local Open Scope Z_scope. + +Module ZExtra. + + Lemma mod_0_bounds : + forall x y m, + 0 < m -> + x mod m = 0 -> + y mod m = 0 -> + x <> y -> + x + m > y -> + y + m <= x. + Proof. + intros x y m. + intros POS XMOD YMOD NEQ H. + destruct (Z_le_gt_dec (y + m) x); eauto. + + apply Znumtheory.Zmod_divide in YMOD; try lia. + apply Znumtheory.Zmod_divide in XMOD; try lia. + inversion XMOD as [x']; subst; clear XMOD. + inversion YMOD as [y']; subst; clear YMOD. + + assert (x' <> y') as NEQ' by lia; clear NEQ. + + rewrite <- Z.mul_succ_l in H. + rewrite <- Z.mul_succ_l in g. + apply Zmult_gt_reg_r in H; + apply Zmult_gt_reg_r in g; lia. + Qed. + +End ZExtra. -- cgit From 8398615fea7ab754854cb10e16e86de6415f1f2d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 Jun 2020 16:55:08 +0100 Subject: Work on addition proof --- src/verilog/Value.v | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index e7b2362..c380ca7 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -108,6 +108,12 @@ Definition boolToValue (sz : nat) (b : bool) : value := Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. intros; subst; assumption. Defined. +Lemma unify_word_unfold : + forall sz w, + unify_word sz sz w eq_refl = w. +Proof. + intros. unfold unify_word. Admitted. + Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. Proof. @@ -382,7 +388,21 @@ Qed. Lemma boolToValue_ValueToBool : forall b, valueToBool (boolToValue 32 b) = b. -Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. +Proof. destruct b; auto. Qed. + +Lemma intToValue_eq_size : + forall n1 n2, + vsize (intToValue n1) = vsize (intToValue n2). +Proof. auto. Qed. + +Local Open Scope Z. + +Lemma zadd_vplus : + forall z1 z2, + valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. +Proof. + intros. unfold valueToZ, ZToValue. simpl. + Admitted. (*Lemma ZToValue_valueToNat : forall x sz, -- cgit From 7e59d2723fb9c5b4631f5eac1e99ae8956871a7f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 Jun 2020 16:59:31 +0100 Subject: Develop compiles again --- Makefile | 1 + src/translation/HTLgen.v | 10 +++++----- src/translation/HTLgenproof.v | 2 +- src/translation/Veriloggenproof.v | 6 ++++-- 4 files changed, 11 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index 3d31b2f..1303b13 100644 --- a/Makefile +++ b/Makefile @@ -67,3 +67,4 @@ clean:: Makefile.coq clean:: rm -f */*.v.d */*.glob */*.vo */*~ *~ + rm -f src/extraction/*.ml src/extraction/*.mli diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 59fb70a..b32ed9d 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -294,24 +294,24 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | Op.Aindexed off, r1::nil => if (check_address_parameter_signed off) then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") | Op.Aindexed2 offset, r1::r2::nil => if (check_address_parameter_signed offset) then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) then ret (Vlit (ZToValue 32 a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2f296f2..6dd0688 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,7 +18,7 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index db96949..ca4ecab 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -69,12 +69,14 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. +(* induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. - apply Smallstep.plus_one. econstructor. eassumption. trivial. - * econstructor. econstructor. + * econstructor. econstructor.*) + Admitted. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). + Admitted. End CORRECTNESS. -- cgit From 1e0d5047d2272fdeb06391d1c5fa4e0472be2365 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 29 Jun 2020 21:29:32 +0100 Subject: Eliminate memory bounds assumption! --- src/common/IntegerExtra.v | 4 +- src/translation/HTLgenproof.v | 244 ++++++++++++++++++++++++++++++++++++------ 2 files changed, 211 insertions(+), 37 deletions(-) diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 8df70d9..7d3156b 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -143,7 +143,7 @@ Module PtrofsExtra. Lemma divu_unsigned : forall x y, 0 < Ptrofs.unsigned y -> - Ptrofs.unsigned x < Ptrofs.max_unsigned -> + Ptrofs.unsigned x <= Ptrofs.max_unsigned -> Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y. Proof. intros. @@ -154,7 +154,7 @@ Module PtrofsExtra. apply Ptrofs.unsigned_range. apply Z.div_le_upper_bound; auto. eapply Z.le_trans. - apply Z.lt_le_incl. exact H0. + exact H0. rewrite Z.mul_comm. apply Z.le_mul_diag_r; simplify; lia. Qed. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2f296f2..f5a55af 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,7 +18,7 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -76,6 +76,13 @@ Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) spb. +Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := + forall ptr v, + hi <= ptr <= Integers.Ptrofs.max_unsigned -> + Z.modulo ptr 4 = 0 -> + Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ + Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. + Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_stacks_nil : match_stacks mem nil nil @@ -87,7 +94,8 @@ Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe (MARR : match_arrs m f sp mem asa) (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), + (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), match_stacks mem (RTL.Stackframe r f sp pc rs :: cs) (HTL.Stackframe r m pc asr asa :: lr). @@ -99,8 +107,9 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (MS : match_stacks mem sf res) (MARR : match_arrs m f sp mem asa) (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), + (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), match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa) | match_returnstate : @@ -601,9 +610,6 @@ Section CORRECTNESS. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - (** Read bounds assumption *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. - (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. @@ -615,6 +621,18 @@ Section CORRECTNESS. rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + (** Read bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H0. + exact H0. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H0. invert H0. congruence. + + (** Preamble *) invert MARR. simplify. @@ -1435,9 +1505,6 @@ Section CORRECTNESS. (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) (Integers.Int.repr z0)))) as OFFSET. - (** Read bounds assumption *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. - (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. @@ -1455,6 +1522,18 @@ Section CORRECTNESS. rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + (** Write bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H0. + exact H0. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H0. invert H0. congruence. + + invert MARR. simplify. unfold Op.eval_addressing in H0. @@ -1668,12 +1774,20 @@ Section CORRECTNESS. remember i0 as OFFSET. - (** Read bounds assumption *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. - (** Modular preservation proof *) rename H0 into MOD_PRESERVE. + (** Write bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H0. + exact H0. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H0. invert H0. congruence. + - eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. apply assumption_32bit. @@ -2090,6 +2231,49 @@ Section CORRECTNESS. repeat constructor. constructor. + Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) + Transparent Mem.load. + Transparent Mem.store. + unfold stack_bounds. + split. + + unfold Mem.alloc in H. + invert H. + simplify. + unfold Mem.load. + intros. + match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. + invert v0. unfold Mem.range_perm in H3. + unfold Mem.perm in H3. simplify. + unfold Mem.perm_order' in H3. + rewrite Integers.Ptrofs.add_zero_l in H3. + rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia. + exploit (H3 ptr). lia. intros. + rewrite Maps.PMap.gss in H8. + match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. + simplify. + apply proj_sumbool_true in H10. lia. + + unfold Mem.alloc in H. + invert H. + simplify. + unfold Mem.store. + intros. + match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. + invert v0. unfold Mem.range_perm in H3. + unfold Mem.perm in H3. simplify. + unfold Mem.perm_order' in H3. + rewrite Integers.Ptrofs.add_zero_l in H3. + rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia. + exploit (H3 ptr). lia. intros. + rewrite Maps.PMap.gss in H8. + match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. + simplify. + apply proj_sumbool_true in H10. lia. + Opaque Mem.alloc. + Opaque Mem.load. + Opaque Mem.store. + - invert MSTATE. invert MS. econstructor. split. apply Smallstep.plus_one. @@ -2104,19 +2288,9 @@ Section CORRECTNESS. rewrite AssocMap.gss. trivial. apply st_greater_than_res. admit. - - Unshelve. - exact (AssocMap.empty value). - exact (AssocMap.empty value). - (* exact (ZToValue 32 0). *) - (* exact (AssocMap.empty value). *) - (* exact (AssocMap.empty value). *) - (* exact (AssocMap.empty value). *) - (* exact (AssocMap.empty value). *) Admitted. Hint Resolve transl_step_correct : htlproof. - Lemma option_inv : forall A x y, @Some A x = Some y -> x = y. -- cgit From 8a260a8b81617e192fc929e0189fd3df1327f80a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 00:04:39 +0100 Subject: Add equivalence between int add value add --- src/verilog/Value.v | 64 ++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 54 insertions(+), 10 deletions(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index c380ca7..3c5ed04 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -111,8 +111,7 @@ intros; subst; assumption. Defined. Lemma unify_word_unfold : forall sz w, unify_word sz sz w eq_refl = w. -Proof. - intros. unfold unify_word. Admitted. +Proof. auto. Qed. Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. @@ -330,6 +329,12 @@ Proof. auto using uwordToZ_ZToWord. Qed. +Lemma uvalueToZ_ZToValue_full : + forall sz : nat, + (0 < sz)%nat -> + forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z. +Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed. + Lemma ZToValue_uvalueToZ : forall v, ZToValue (vsize v) (uvalueToZ v) = v. @@ -390,19 +395,58 @@ Lemma boolToValue_ValueToBool : valueToBool (boolToValue 32 b) = b. Proof. destruct b; auto. Qed. -Lemma intToValue_eq_size : - forall n1 n2, - vsize (intToValue n1) = vsize (intToValue n2). -Proof. auto. Qed. - Local Open Scope Z. +Ltac eq_op H := + intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; + rewrite <- H; rewrite uwordToZ_ZToWord; auto. + Lemma zadd_vplus : forall z1 z2, - valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. + 0 <= z1 + z2 < 2 ^ 32 -> + uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. +Proof. eq_op ZToWord_plus. Qed. + +Lemma zadd_vplus2 : + forall z1 z2, + vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2). Proof. - intros. unfold valueToZ, ZToValue. simpl. - Admitted. + intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl. + rewrite ZToWord_plus; auto. +Qed. + +Lemma intadd_vplus : + forall i1 i2, + valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. +Proof. + intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus2. + rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq. + rewrite Int.repr_unsigned. auto. omega. +Qed. + +Lemma zsub_vminus : + forall z1 z2, + 0 <= z1 - z2 < 2 ^ 32 -> + uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2. +Proof. eq_op ZToWord_minus. Qed. + +Lemma zmul_vmul : + forall z1 z2, + 0 <= z1 * z2 < 2 ^ 32 -> + uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2. +Proof. eq_op ZToWord_mult. Qed. + +Local Open Scope N. +Lemma zdiv_vdiv : + forall n1 n2, + n1 < 2 ^ 32 -> + n2 < 2 ^ 32 -> + n1 / n2 < 2 ^ 32 -> + valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2. +Proof. + intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv. + unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. +Qed. (*Lemma ZToValue_valueToNat : forall x sz, -- cgit From 9a640d4f50b93a9d5f9b48e10b0c4cbfa7f0680f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 00:29:41 +0100 Subject: Make the proofs more concise --- src/verilog/Value.v | 38 +++++++++++++++++++++----------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 3c5ed04..8ba5138 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -397,15 +397,15 @@ Proof. destruct b; auto. Qed. Local Open Scope Z. -Ltac eq_op H := +Ltac word_op_value H := intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord; auto. + rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. Lemma zadd_vplus : - forall z1 z2, - 0 <= z1 + z2 < 2 ^ 32 -> - uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. -Proof. eq_op ZToWord_plus. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_plus. Qed. Lemma zadd_vplus2 : forall z1 z2, @@ -415,26 +415,30 @@ Proof. rewrite ZToWord_plus; auto. Qed. +Lemma wordsize_32 : + Int.wordsize = 32%nat. +Proof. auto. Qed. + Lemma intadd_vplus : forall i1 i2, valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. Proof. - intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus2. - rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq. - rewrite Int.repr_unsigned. auto. omega. + intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus. + rewrite <- Int.unsigned_repr_eq. + rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. Lemma zsub_vminus : - forall z1 z2, - 0 <= z1 - z2 < 2 ^ 32 -> - uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2. -Proof. eq_op ZToWord_minus. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_minus. Qed. Lemma zmul_vmul : - forall z1 z2, - 0 <= z1 * z2 < 2 ^ 32 -> - uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2. -Proof. eq_op ZToWord_mult. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_mult. Qed. Local Open Scope N. Lemma zdiv_vdiv : -- cgit From f26f3887d0b0ac286c317a5425a3a4781871cfc2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 12:34:35 +0100 Subject: Add command line flags for initial block --- driver/CoqupDriver.ml | 8 +++----- src/CoqupClflags.ml | 5 +++++ src/verilog/PrintVerilog.ml | 10 ++++++++++ test/loop.c | 6 ++++-- 4 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 src/CoqupClflags.ml diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml index 2932a50..afbe4d0 100644 --- a/driver/CoqupDriver.ml +++ b/driver/CoqupDriver.ml @@ -36,11 +36,7 @@ open Coqup.Frontend open Coqup.Assembler open Coqup.Linker open Coqup.Diagnostics - -(* Coqup flags *) -let option_simulate = ref false -let option_hls = ref true -let option_debug_hls = ref false +open Coqup.CoqupClflags (* Name used for version string etc. *) let tool_name = "C verified high-level synthesis" @@ -215,6 +211,7 @@ Processing options: --no-hls Do not use HLS and generate standard flow. --simulate Simulate the result with the Verilog semantics. --debug-hls Add debug logic to the Verilog. + --initialise-stack initialise the stack to all 0s. |} ^ prepro_help ^ language_support_help ^ @@ -316,6 +313,7 @@ let cmdline_actions = [Exact "--no-hls", Unset option_hls; Exact "--simulate", Set option_simulate; Exact "--debug-hls", Set option_debug_hls; + Exact "--initialise-stack", Set option_initial; ] (* Getting version info *) @ version_options tool_name @ diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml new file mode 100644 index 0000000..83dd31d --- /dev/null +++ b/src/CoqupClflags.ml @@ -0,0 +1,5 @@ +(* Coqup flags *) +let option_simulate = ref false +let option_hls = ref true +let option_debug_hls = ref false +let option_initial = ref false diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 5dc0386..6d10887 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -22,9 +22,12 @@ open Datatypes open Camlcoq open AST +open Clflags open Printf +open CoqupClflags + let concat = String.concat "" let indent i = String.make (2 * i) ' ' @@ -187,6 +190,12 @@ let debug_always i clk state = concat [ indent i; "end\n" ] +let print_initial i n stk = concat [ + indent i; "integer i;\n"; + indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n"; + indent (i+1); register stk; "[i] = 0;\n" + ] + let pprint_module debug i n m = if (extern_atom n) = "main" then let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in @@ -194,6 +203,7 @@ let pprint_module debug i n m = concat [ indent i; "module "; (extern_atom n); "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; + if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; if debug then debug_always i m.mod_clk m.mod_st else ""; indent i; "endmodule\n\n" ] diff --git a/test/loop.c b/test/loop.c index b459e3a..52e4fe9 100644 --- a/test/loop.c +++ b/test/loop.c @@ -1,10 +1,12 @@ int main() { int max = 5; int acc = 0; + int b = 1; + int c = 2; - for (int i = 0; i < max; i++) { + for (int i = 0; i < max; i = i + b) { acc += i; } - return acc + 2; + return acc + c; } -- cgit