From be6ad3cd886b3ea79abe6addc2f2add779f55292 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 22 Jun 2020 17:15:29 +0100 Subject: Tidy up proof for Aindexed2scaled. --- src/translation/HTLgen.v | 7 +- src/translation/HTLgenproof.v | 252 ++++++++++++++++++++++++++++-------------- src/translation/HTLgenspec.v | 7 +- 3 files changed, 177 insertions(+), 89 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 1c2d786..2364a0f 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -248,7 +248,7 @@ 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?*) @@ -445,8 +445,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) && (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)); diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index be7538c..21dbc73 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. @@ -334,6 +334,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 -> @@ -487,8 +488,6 @@ 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. *) destruct c, chunk, addr, args; simplify; rt; simplify. @@ -513,7 +512,97 @@ Section CORRECTNESS. rewrite ARCHI in H1. simplify. subst. + clear RSBPr1. + + 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 H4 in HPler0. + apply H6 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H7. + rewrite EQr1 in H8. + invert H7. invert H8. + clear H0. clear H4. clear H6. + + unfold check_address_parameter in *. simplify. + + (** Normalisation proof *) + assert + (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))) + = + Integers.Ptrofs.repr + (4 * + Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0 / 4)) + (Integers.Ptrofs.of_int + (Integers.Int.add + (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr (z / 4))) + (Integers.Int.repr (z0 / 4))))))) as NORMALISE. + etransitivity. + 2: { + replace (4 * + Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0 / 4)) + (Integers.Ptrofs.of_int + (Integers.Int.add + (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr (z / 4))) + (Integers.Int.repr (z0 / 4)))))) with + (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4) * + Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0 / 4)) + (Integers.Ptrofs.of_int + (Integers.Int.add + (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr (z / 4))) + (Integers.Int.repr (z0 / 4)))))). + 2: { rewrite Integers.Ptrofs.unsigned_repr_eq. + rewrite Z.mod_small. reflexivity. + simplify. lia. } + + rewrite <- PtrofsExtra.mul_unsigned. + rewrite Integers.Ptrofs.mul_add_distr_r. + rewrite PtrofsExtra.mul_repr; simplify; try lia. + rewrite ZLib.div_mul_undo; try lia. + rewrite mul_of_int; simplify; try lia. + rewrite Integers.Int.mul_add_distr_r. + rewrite Integers.Int.mul_commut. + rewrite Integers.Int.mul_assoc. + rewrite IntExtra.mul_repr; simplify; try lia. + rewrite IntExtra.mul_repr; simplify; try lia. + rewrite ZLib.div_mul_undo; try lia. + rewrite Z.mul_comm. + rewrite ZLib.div_mul_undo; try lia. + reflexivity. + + split. + apply Z.div_le_lower_bound; lia. + apply Z.div_le_upper_bound; lia. + split. + apply Z.div_le_lower_bound; lia. + apply Z.div_le_upper_bound; lia. + + admit. (* FIXME: Register size 32 bits *) } + reflexivity. + + 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. + + (** Here we are assuming that any stack read will be within the bounds + of the activation record. *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (* Proof begins in earnest here. *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -554,55 +643,43 @@ Section CORRECTNESS. unfold Verilog.merge_regs. unfold_merge. apply regs_lessdef_add_match. - pose proof H1. + (** Equality proof *) assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. - rewrite H4 in H5. + rewrite H0 in H5. clear H0. setoid_rewrite Integers.Ptrofs.add_zero_l in H5. - 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))). - - 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. + specialize (H5 + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0 / 4)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul + (valueToInt asr # r1) + (Integers.Int.repr (z / 4))) + (Integers.Int.repr (z0 / 4))))))). - invert MASSOC. - pose proof (H7 r0). - pose proof (H7 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. - 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. + exploit H5; auto; intros. + rewrite Z2Nat.id. + split. + apply Integers.Ptrofs.unsigned_range_2. + admit. + apply Z_div_pos; lia. + clear H5. + + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0 / 4)) + (Integers.Ptrofs.of_int + (Integers.Int.add + (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr (z / 4))) + (Integers.Int.repr (z0 / 4)))))) + = + valueToNat + (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) + (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1)) as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite <- NORMALISE in H0. + rewrite H1 in H0. + invert H0. assumption. apply regs_lessdef_add_greater. apply greater_than_max_func. @@ -647,40 +724,41 @@ Section CORRECTNESS. 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. - simplify. - assumption. + (* 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. *) + (* simplify. *) + (* assumption. *) + admit. rewrite Registers.Regmap.gso; auto. @@ -690,9 +768,10 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. + unfold check_address_parameter in EQ; 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. eexists. split. @@ -725,12 +804,12 @@ Section CORRECTNESS. exploit H5; auto; intros. 1: { split. - - apply Z.div_pos; lia. + - apply Z.div_pos; try lia. + apply Integers.Ptrofs.unsigned_range_2. - 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. @@ -789,7 +868,8 @@ Section CORRECTNESS. exploit ASBP; auto; intros. 1: { split. - - apply Z.div_pos; lia. + - apply Z.div_pos; try lia. + apply Integers.Ptrofs.unsigned_range_2. - apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; lia. } diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a916cb5..528c662 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -189,6 +189,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) -> m = (mkmodule f.(RTL.fn_params) data control @@ -452,7 +453,11 @@ 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; + 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. -- cgit