diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/common/Coquplib.v | 65 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 214 | ||||
| -rw-r--r-- | src/translation/HTLgen.v | 42 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 624 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 12 | ||||
| -rw-r--r-- | src/verilog/Value.v | 1 |
6 files changed, 773 insertions, 185 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index efa1323..b4ca906 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -28,6 +28,7 @@ From coqup Require Import Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) From compcert.lib Require Export Coqlib. +From compcert Require Integers. Ltac unfold_rec c := unfold c; fold c. @@ -50,9 +51,71 @@ Ltac clear_obvious := | [ H : _ /\ _ |- _ ] => invert H end. -Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. +Ltac kill_bools := + repeat match goal with + | [ H : _ && _ = true |- _ ] => apply andb_prop in H + | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H + + | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H + | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H + | [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H + | [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H + | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H + | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H + + | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H + | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H + end. + +Ltac unfold_constants := + repeat match goal with + | [ _ : _ |- context[Integers.Ptrofs.modulus] ] => + replace Integers.Ptrofs.modulus with 4294967296 by reflexivity + | [ H : context[Integers.Ptrofs.modulus] |- _ ] => + replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity + + | [ _ : _ |- context[Integers.Ptrofs.min_signed] ] => + replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity + | [ H : context[Integers.Ptrofs.min_signed] |- _ ] => + replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity + + | [ _ : _ |- context[Integers.Ptrofs.max_signed] ] => + replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity + | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => + replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity + + | [ _ : _ |- context[Integers.Ptrofs.max_unsigned] ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity + + | [ _ : _ |- context[Integers.Int.modulus] ] => + replace Integers.Int.modulus with 4294967296 by reflexivity + | [ H : context[Integers.Int.modulus] |- _ ] => + replace Integers.Int.modulus with 4294967296 in H by reflexivity + + | [ _ : _ |- context[Integers.Int.min_signed] ] => + replace Integers.Int.min_signed with (-2147483648) by reflexivity + | [ H : context[Integers.Int.min_signed] |- _ ] => + replace Integers.Int.min_signed with (-2147483648) in H by reflexivity + + | [ _ : _ |- context[Integers.Int.max_signed] ] => + replace Integers.Int.max_signed with 2147483647 by reflexivity + | [ H : context[Integers.Int.max_signed] |- _ ] => + replace Integers.Int.max_signed with 2147483647 in H by reflexivity + + | [ _ : _ |- context[Integers.Int.max_unsigned] ] => + replace Integers.Int.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Int.max_unsigned] |- _ ] => + replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity + end. + +Ltac simplify := unfold_constants; simpl in *; + repeat (clear_obvious; kill_bools); + simpl in *; try discriminate. Global Opaque Nat.div. +Global Opaque Z.mul. (* Definition const (A B : Type) (a : A) (b : B) : A := a. diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v new file mode 100644 index 0000000..2f9aae6 --- /dev/null +++ b/src/common/IntegerExtra.v @@ -0,0 +1,214 @@ +Require Import BinInt. +Require Import Lia. +Require Import ZBinary. + +From bbv Require Import ZLib. +From compcert Require Import Integers Coqlib. + +Require Import Coquplib. + +Local Open Scope Z_scope. + +Module PtrofsExtra. + + Ltac ptrofs_mod_match m := + match goal with + | [ H : ?x = 0 |- context[?x] ] => rewrite H + | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r + | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l + | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r + | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l + | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r + | [ _ : _ |- context[?m mod ?m] ] => + rewrite Z_mod_same_full with (a := m) + | [ _ : _ |- context[0 mod _] ] => + rewrite Z.mod_0_l + | [ _ : _ |- context[(_ mod ?m) mod ?m] ] => + rewrite Zmod_mod + | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] => + rewrite <- Zmod_div_mod; + try (simplify; lia || assumption) + + | [ _ : _ |- context[Ptrofs.modulus mod m] ] => + rewrite Zdivide_mod with (a := Ptrofs.modulus); + try (lia || assumption) + + | [ _ : _ |- context[Ptrofs.signed ?a mod Ptrofs.modulus] ] => + rewrite Z.mod_small with (a := Ptrofs.signed a) (b := Ptrofs.modulus) + + | [ _ : _ |- context[(?x - ?y) mod ?m] ] => + rewrite Zminus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + | [ _ : _ |- context[(?x + ?y) mod ?m] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[(?x * ?y) mod ?m] ] => + rewrite Zmult_mod with (a := x) (b := y) (n := m) + end. + + Ltac ptrofs_mod_tac m := + repeat (ptrofs_mod_match m); lia. + + Lemma of_int_mod : + forall x m, + Int.signed x mod m = 0 -> + Ptrofs.signed (Ptrofs.of_int x) mod m = 0. + Proof. + intros. + pose proof (Integers.Ptrofs.agree32_of_int eq_refl x) as A. + pose proof Ptrofs.agree32_signed. + apply H0 in A; try reflexivity. + rewrite A. assumption. + Qed. + + Lemma mul_mod : + forall x y m, + 0 < m -> + (m | Ptrofs.modulus) -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.signed y mod m = 0 -> + (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0. + Proof. + intros. unfold Ptrofs.mul. + rewrite Ptrofs.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + + Lemma add_mod : + forall x y m, + 0 < m -> + (m | Ptrofs.modulus) -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.signed y mod m = 0 -> + (Ptrofs.signed (Ptrofs.add x y)) mod m = 0. + Proof. + intros. unfold Ptrofs.add. + rewrite Ptrofs.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + + Lemma mul_divs : + forall x y, + 0 <= Ptrofs.signed y -> + 0 < Ptrofs.signed x -> + Ptrofs.signed y mod Ptrofs.signed x = 0 -> + (Integers.Ptrofs.mul x (Integers.Ptrofs.divs y x)) = y. + Proof. + intros. + + pose proof (Ptrofs.mods_divs_Euclid y x). + pose proof (Zquot.Zrem_Zmod_zero (Ptrofs.signed y) (Ptrofs.signed x)). + apply <- H3 in H1; try lia; clear H3. + unfold Ptrofs.mods in H2. + rewrite H1 in H2. + replace (Ptrofs.repr 0) with (Ptrofs.zero) in H2 by reflexivity. + rewrite Ptrofs.add_zero in H2. + rewrite Ptrofs.mul_commut. + congruence. + Qed. + + Lemma mul_unsigned : + forall x y, + Ptrofs.mul x y = + Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y). + Proof. + intros; unfold Ptrofs.mul. + apply Ptrofs.eqm_samerepr. + apply Ptrofs.eqm_mult; exists 0; lia. + Qed. +End PtrofsExtra. + +Module IntExtra. + + Ltac int_mod_match m := + match goal with + | [ H : ?x = 0 |- context[?x] ] => rewrite H + | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r + | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l + | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r + | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l + | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r + | [ _ : _ |- context[?m mod ?m] ] => + rewrite Z_mod_same_full with (a := m) + | [ _ : _ |- context[0 mod _] ] => + rewrite Z.mod_0_l + | [ _ : _ |- context[(_ mod ?m) mod ?m] ] => + rewrite Zmod_mod + | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] => + rewrite <- Zmod_div_mod; + try (simplify; lia || assumption) + + | [ _ : _ |- context[Int.modulus mod m] ] => + rewrite Zdivide_mod with (a := Int.modulus); + try (lia || assumption) + + | [ _ : _ |- context[Int.signed ?a mod Int.modulus] ] => + rewrite Z.mod_small with (a := Int.signed a) (b := Int.modulus) + + | [ _ : _ |- context[(?x - ?y) mod ?m] ] => + rewrite Zminus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + | [ _ : _ |- context[(?x + ?y) mod ?m] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[(?x * ?y) mod ?m] ] => + rewrite Zmult_mod with (a := x) (b := y) (n := m) + end. + + Ltac int_mod_tac m := + repeat (int_mod_match m); lia. + + Lemma mul_mod : + forall x y m, + 0 < m -> + (m | Int.modulus) -> + Int.signed x mod m = 0 -> + Int.signed y mod m = 0 -> + (Int.signed (Int.mul x y)) mod m = 0. + Proof. + intros. unfold Int.mul. + rewrite Int.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Int.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed + end; try (simplify; lia); int_mod_tac m. + Qed. + + Lemma add_mod : + forall x y m, + 0 < m -> + (m | Int.modulus) -> + Int.signed x mod m = 0 -> + Int.signed y mod m = 0 -> + (Int.signed (Int.add x y)) mod m = 0. + Proof. + intros. unfold Int.add. + rewrite Int.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Int.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed + end; try (simplify; lia); int_mod_tac m. + Qed. +End IntExtra. diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 66170bc..dc82fb1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -283,15 +283,22 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : Definition check_address_parameter (p : Z) : bool := Z.eqb (Z.modulo p 4) 0 && Z.leb Integers.Ptrofs.min_signed p - && Z.leb p Integers.Ptrofs.min_signed. + && Z.leb p Integers.Ptrofs.max_signed. Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) + | Op.Aindexed off, r1::nil => + if (check_address_parameter off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter offset) + then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) @@ -385,23 +392,26 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Mint32, Op.Aindexed off, r1::nil => - ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) + if (check_address_parameter off) + then ret (Vvari stack (Vbinop Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Ascaled scale offset, r1::nil => if (check_address_parameter scale) && (check_address_parameter offset) - then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) - else error (Errors.msg "Htlgen: translate_arr_access address misaligned") + then ret (Vvari stack (Vbinop Vdiv (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) (Vlit (ZToValue 32 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vvari stack - (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4)))) - (boplitz Vmul r2 (scale / 4)))) - else error (Errors.msg "Htlgen: translate_arr_access address misaligned") + (Vbinop Vdiv + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (ZToValue 32 4))) + else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in + let a := Integers.Ptrofs.signed a in if (check_address_parameter a) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") - | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") + else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -499,8 +509,11 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (st_controllogic s)) (create_arr_state_incr s sz ln i). +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). + Definition transf_module (f: function) : mon module := - if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then + if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); @@ -559,7 +572,8 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := +Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. +(* let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -568,7 +582,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := | _ => false end | _ => false - end. + end. *) Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9b59269..24191ae 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. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -348,6 +348,7 @@ Section CORRECTNESS. exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). + Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -393,7 +394,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H1. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -501,33 +502,89 @@ Section CORRECTNESS. | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x end. - Opaque Z.mul. - - - (* FIXME: Should be able to use the spec to avoid destructing here. *) + - (* FIXME: Should be able to use the spec to avoid destructing here? *) destruct c, chunk, addr, args; simplify; rt; simplify. - + admit. (* FIXME: Alignment *) - - + (* FIXME: Why is this degenerate? Should we support this mode? *) - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate. - - + invert MARR. simplify. + + (** Preamble *) + invert MARR. simplify. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; simplify. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. - pose proof (RSBP r1) as RSBPr1. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. rewrite ARCHI in H1. simplify. subst. + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + apply H6 in HPler0. + invert HPler0; try congruence. + rewrite EQr0 in H8. + invert H8. + clear H0. clear H6. + + unfold check_address_parameter in *. simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + + (** Read bounds assumption *) + assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divs; auto. + rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. + unfold Integers.Ptrofs.divs at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.signed_repr; simplify; try lia. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + rewrite Integers.Ptrofs.signed_repr. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + split. + apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. + simplify; lia. } + + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -535,99 +592,302 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. simplify. eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *) eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. (* FIXME: Oh dear. *) + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. - unfold Verilog.arr_assocmap_lookup. simplify. setoid_rewrite H3. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. f_equal. - simplify. unfold Verilog.merge_regs. + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. - simplify. rewrite assumption_32bit. - econstructor; simplify; eauto. + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. - unfold Verilog.merge_regs. unfold_merge. + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. apply regs_lessdef_add_match. - pose proof H1. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. - rewrite H4 in H5. - setoid_rewrite Integers.Ptrofs.add_zero_l in H5. + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match arrays *) + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + (** RSBP preservation *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r1 dst); try rewrite e. (* FIXME: Prepare this for automation *) + + rewrite Registers.Regmap.gss. + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. + simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. + assumption. + simplify. + + rewrite Registers.Regmap.gso; auto. + + + (* FIXME: Why is this degenerate? Should we support this mode? *) + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate. + + + (** Preamble *) + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. - specialize (H5 (uvalueToZ - (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1))). + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. - assert (0 <= uvalueToZ - (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1) < - Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. - apply H5 in H6. + rewrite ARCHI in H1. simplify. + subst. + clear RSBPr1. - invert MASSOC. - pose proof (H7 r0). - pose proof (H7 r1). + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). assert (HPler1 : Ple r1 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H8 in HPler0. - apply H10 in HPler1. + apply H6 in HPler0. + apply H8 in HPler1. invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H12. - rewrite EQr1 in H13. - - assert ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) = - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.repr - (4 * - uvalueToZ - (vplus - (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) - (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) - ?EQ1))))) by admit. - - rewrite <- H19 in H6. - rewrite H0 in H6. - invert H6. - assert (forall x, Z.to_nat (uvalueToZ x) = valueToNat x) as VALUE_IDENTITY by admit. - rewrite VALUE_IDENTITY in H21. - assumption. + rewrite EQr0 in H10. + rewrite EQr1 in H12. + invert H10. invert H12. + clear H0. clear H6. clear H8. + + unfold check_address_parameter in *. simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. + + (** Read bounds assumption *) + assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + apply IntExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + apply IntExtra.mul_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + admit. (* FIXME: Register bounds. *) + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divs; auto. + rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. + unfold Integers.Ptrofs.divs at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.signed_repr; simplify; try lia. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + rewrite Integers.Ptrofs.signed_repr. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + split. + apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. + simplify; lia. } + + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). (* FIXME: These will be shelved and cause sadness. *) + eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ5]). + econstructor. econstructor. econstructor. econstructor. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. + f_equal. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = valueToNat + (vdivs (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) + (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. + (** States well formed *) unfold state_st_wf. inversion 1. simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + (** Match arrays *) econstructor. repeat split; simplify. unfold HTL.empty_stack. @@ -638,7 +898,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H3. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -655,46 +915,24 @@ Section CORRECTNESS. eauto. apply combine_none. assumption. + (** RSBP preservation *) unfold reg_stack_based_pointers. intros. - destruct (Pos.eq_dec r2 dst); subst. + destruct (Pos.eq_dec r2 dst); try rewrite e. (* FIXME: Prepare this for automation *) rewrite Registers.Regmap.gss. - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) / 4)). - exploit ASBP; auto; intros. - 1: { - split. - - admit. (*apply Z.div_pos; lia.*) - - admit. (* apply Zmult_lt_reg_r with (p := 4); try lia. *) - (* repeat rewrite ZLib.div_mul_undo; lia. *) - } - replace (4 * ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) / 4)) with (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) in H0. - 2: { - rewrite Z.mul_comm. - admit. - (* rewrite ZLib.div_mul_undo; lia. *) - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - simplify. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. - rewrite H4 in H0. - setoid_rewrite Integers.Ptrofs.add_zero_l in H0. - rewrite H1 in H0. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. assumption. + simplify. rewrite Registers.Regmap.gso; auto. @@ -704,68 +942,126 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. - (** Here we are assuming that any stack read will be within the bounds - of the activation record. *) - assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + unfold check_address_parameter in EQ; simplify. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H1. clear ZERO. + rewrite Integers.Ptrofs.add_zero_l in H1. + + remember i0 as OFFSET. + + (** Read bounds assumption *) + assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + rename H8 into MOD_PRESERVE. + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divs; auto. + rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. + unfold Integers.Ptrofs.divs at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.signed_repr; simplify; try lia. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + rewrite Integers.Ptrofs.signed_repr. + rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. + split. + apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. + apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. + simplify; lia. } + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + + (** Start of proof proper *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. econstructor. econstructor. econstructor. simplify. econstructor. econstructor. econstructor. econstructor. simplify. - unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. f_equal. - simplify. unfold Verilog.merge_regs. + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. - simplify. rewrite assumption_32bit. - econstructor; simplify; eauto. + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. - unfold Verilog.merge_regs. unfold_merge. + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. apply regs_lessdef_add_match. (** Equality proof *) - (* FIXME: 32-bit issue. *) - assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit. - rewrite VALUE_IDENTITY. - specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)). - rewrite Z2Nat.id in H5; try lia. - exploit H5; auto; intros. - 1: { - split. - - apply Z.div_pos; lia. - - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; lia. - } - 2: { - assert (0 < RTL.fn_stacksize f) by lia. - apply Z.div_pos; lia. - } - replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. - 2: { - rewrite Z.mul_comm. - rewrite ZLib.div_mul_undo; lia. - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - rewrite H1 in H0. - invert H0. assumption. - + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (ZToValue 32 (Integers.Ptrofs.signed OFFSET / 4))) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. + (** States well formed *) unfold state_st_wf. inversion 1. simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + (** Match arrays *) econstructor. repeat split; simplify. unfold HTL.empty_stack. @@ -776,7 +1072,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H3. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -793,30 +1089,24 @@ Section CORRECTNESS. eauto. apply combine_none. assumption. + (** RSBP preservation *) unfold reg_stack_based_pointers. intros. - destruct (Pos.eq_dec r0 dst); subst. + destruct (Pos.eq_dec r0 dst); try rewrite e. (* FIXME: Prepare this for automation *) rewrite Registers.Regmap.gss. - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned i0 / 4)). - exploit ASBP; auto; intros. - 1: { - split. - - apply Z.div_pos; lia. - - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; lia. - } - replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. - 2: { - rewrite Z.mul_comm. - rewrite ZLib.div_mul_undo; lia. - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - simplify. - rewrite H1 in H0. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. assumption. + simplify. rewrite Registers.Regmap.gso; auto. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 7d89a76..a78256b 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -140,7 +140,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c src n, 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). + (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> @@ -165,6 +165,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> m = (mkmodule f.(RTL.fn_params) data control @@ -421,13 +422,18 @@ Proof. inversion s; subst. unfold transf_module in *. - destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; + destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; + simplify; + monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. rewrite <- STK_LEN. - econstructor; simpl; trivial. + econstructor; simpl; auto. intros. inv_incr. assert (EQ3D := EQ3). diff --git a/src/verilog/Value.v b/src/verilog/Value.v index bde98b8..becc44c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -388,3 +388,4 @@ Proof. (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. +Admitted. |