From ec9b22d01cd89aecb95da02067919423a0f1f884 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sat, 20 Jun 2020 17:47:52 +0100 Subject: Finish structure of Aindexed2scaled ILoad proof. --- src/translation/HTLgenproof.v | 186 ++++++++++++++++++++++++++++++++++++++---- src/verilog/Value.v | 5 ++ 2 files changed, 177 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 046ae06..be7538c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -69,20 +69,24 @@ Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe match_stacks mem (RTL.Stackframe r f sp pc rs :: cs) (HTL.Stackframe r m pc asr asa :: lr). +Definition stack_based (v : Values.val) (sp : Values.block) : Prop := + match v with + | Values.Vptr sp' off => sp' = sp + | _ => True + end. + Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := - forall r, match Registers.Regmap.get r rs with - | Values.Vptr sp' off => sp' = sp - | _ => True - end. + forall r, stack_based (Registers.Regmap.get r rs) sp. Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) (sp : Values.val) : Prop := forall ptr, 0 <= ptr < (stack_length / 4) -> - match Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))) with - | Some (Values.Vptr sp' off) => sp' = spb - | _ => True - end. + stack_based (Option.default + Values.Vundef + (Mem.loadv AST.Mint32 m + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) + spb. Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res @@ -514,10 +518,10 @@ Section CORRECTNESS. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. econstructor. simplify. - econstructor. - econstructor. - econstructor. + 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. @@ -526,6 +530,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). econstructor. econstructor. econstructor. @@ -549,7 +554,135 @@ Section CORRECTNESS. unfold Verilog.merge_regs. unfold_merge. apply regs_lessdef_add_match. - all: admit. + 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. + + 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. + + 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. + + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + 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 H3. + 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. + + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r2 dst); subst. + + 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. + + rewrite Registers.Regmap.gso; auto. + invert MARR. simplify. @@ -646,7 +779,32 @@ Section CORRECTNESS. eauto. apply combine_none. assumption. - (* FIXME: RSBP Proof. *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r0 dst); subst. + + 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. + simplify. + assumption. + + rewrite Registers.Regmap.gso; auto. - destruct c, chunk, addr, args; simplify; rt; simplify. + admit. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index b1ee353..818f625 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -294,6 +294,11 @@ Inductive val_value_lessdef: val -> value -> Prop := forall i v', i = valueToInt v' -> val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = Ptrofs.repr (valueToZ v') -> + (Z.modulo (valueToZ v') 4) = 0%Z -> + val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. Inductive opt_val_value_lessdef: option val -> value -> Prop := -- cgit From 2b4a5fcb4b58122d9bf8ae52f03c9855ffeb1d77 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 21 Jun 2020 13:47:32 +0100 Subject: Lea op now checks alignment. --- src/translation/HTLgen.v | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index f661aa6..1c4130b 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -246,18 +246,21 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : end. Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := - match a, args with + 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.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - | Op.Aindexed2scaled scale offset, r1::r2::nil => - ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (* Stack arrays/referenced variables *) - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - ret (Vlit (ZToValue 32 a)) - | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other") + if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + else error (Errors.msg "Veriloggen: translate_eff_addressing 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 + if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vlit (ZToValue 32 a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | _, _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. (** Translate an instruction to a statement. *) @@ -335,7 +338,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := 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 => (* FIXME: Cannot guarantee alignment *) + | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) | Mint32, Op.Ascaled scale offset, r1::nil => if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) @@ -348,7 +351,7 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (boplitz Vmul r2 (scale / 4)))) else error (Errors.msg "Veriloggen: 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 (* FIXME: Assuming stack offsets are +ve; is this ok? *) + let a := Integers.Ptrofs.unsigned a in if (Z.eq_dec (Z.modulo a 4) 0) 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") -- cgit From e05b93c540d2e0e2cb9f4ab01460eba080b65401 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 21 Jun 2020 15:01:15 +0100 Subject: Factor out addressing checks, check signed range. --- src/translation/HTLgen.v | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 1c4130b..1c2d786 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,7 +17,7 @@ *) From compcert Require Import Maps. -From compcert Require Errors Globalenvs. +From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. @@ -245,22 +245,28 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other") end. +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. + 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.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + 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") - | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + | 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)) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") - | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vlit (ZToValue 32 a)) + if (check_address_parameter a) + then ret (Vlit (ZToValue 32 a)) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") - | _, _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. (** Translate an instruction to a statement. *) @@ -341,18 +347,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) | Mint32, Op.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + 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 "Veriloggen: translate_arr_access address misaligned") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + 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 "Veriloggen: 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 - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) + 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") end. -- cgit