From 3f922756808ccdf2516f097047d758820cdf5177 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 4 Aug 2020 15:54:19 +0200 Subject: Fix first part of istore --- src/translation/HTLgenproof.v | 83 ++++++++++++++++++++++--------------------- 1 file changed, 43 insertions(+), 40 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index cc41d2a..ab607ef 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1298,11 +1298,11 @@ Section CORRECTNESS. exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. Proof. -(* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. + intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. inv_state. inv_arr_access. + (** Preamble *) - invert MARR. crush. + invert MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1320,11 +1320,11 @@ Section CORRECTNESS. pose proof (H0 r0). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H6 in HPler0. + apply H8 in HPler0. invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. + rewrite EQr0 in H11. + invert H11. + clear H0. clear H8. unfold check_address_parameter_unsigned in *; unfold check_address_parameter_signed in *; crush. @@ -1334,13 +1334,8 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - rewrite Integers.Ptrofs.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. - apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.unsigned_repr_eq. - rewrite <- Zmod_div_mod; crush. } + { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. + apply Zdivide_mod. assumption. } (** Write bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. @@ -1353,12 +1348,9 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. econstructor. econstructor. econstructor. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. @@ -1373,7 +1365,6 @@ Section CORRECTNESS. apply AssocMap.gss. (** Match states *) - rewrite assumption_32bit. econstructor; eauto. (** Match assocmaps *) @@ -1416,7 +1407,7 @@ Section CORRECTNESS. rewrite AssocMap.gss. unfold Verilog.merge_arr. rewrite AssocMap.gss. - setoid_rewrite H5. + setoid_rewrite H7. reflexivity. rewrite combine_length. @@ -1439,26 +1430,27 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.add_zero_l. rewrite e. rewrite Integers.Ptrofs.unsigned_repr. + rewrite HeqOFFSET. exact H1. apply Integers.Ptrofs.unsigned_range_2. } constructor. erewrite combine_lookup_second. - simpl. - assert (Ple src (RTL.max_reg_function f)) + simplify. + assert (HPle : Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H13. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. + apply H0 in HPle. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert HPle; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. rewrite list_repeat_len. auto. - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H13. - rewrite Z_div_mult in H13; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. - rewrite H13. rewrite EXPR_OK. + assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). + rewrite Z.mul_comm in HMul. + rewrite Z_div_mult in HMul; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia. + rewrite HMul. rewrite EXPR_OK. rewrite array_get_error_set_bound. reflexivity. unfold arr_length, arr_repeat. simpl. @@ -1475,11 +1467,14 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H15; try lia. - apply Zmult_lt_compat_r with (p := 4) in H15; try lia. - rewrite ZLib.div_mul_undo in H15; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. + rewrite Z2Nat.id in H16; try lia. + apply Zmult_lt_compat_r with (p := 4) in H16; try lia. + rewrite ZLib.div_mul_undo in H16; try lia. + rewrite HeqOFFSET in MOD_PRESERVE. apply MOD_PRESERVE. + rewrite HeqOFFSET in n. apply n. + admit. admit. admit. + (*split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.*) } rewrite <- EXPR_OK. @@ -1488,7 +1483,7 @@ Section CORRECTNESS. apply Z.mul_cancel_r with (p := 4) in e; try lia. rewrite ZLib.div_mul_undo in e; try lia. rewrite combine_lookup_first. - eapply H7; eauto. + eapply H9; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. @@ -1501,7 +1496,7 @@ Section CORRECTNESS. lia. unfold_constants. intro. - apply Z2Nat.inj_iff in H13; try lia. + apply Z2Nat.inj_iff in H14; try lia. apply Z.div_pos; try lia. apply Integers.Ptrofs.unsigned_range. @@ -1527,7 +1522,7 @@ Section CORRECTNESS. simpl. erewrite Mem.load_store_other with (m1 := m). 2: { exact H1. } - 2: { right. + 2: { (*right. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. rewrite Integers.Ptrofs.unsigned_repr. @@ -1537,10 +1532,11 @@ Section CORRECTNESS. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. invert H0. - apply Zmult_lt_compat_r with (p := 4) in H14; try lia. - rewrite ZLib.div_mul_undo in H14; try lia. + apply Zmult_lt_compat_r with (p := 4) in H15; try lia. + rewrite ZLib.div_mul_undo in H15; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.*) + admit. } apply ASBP; assumption. @@ -1553,7 +1549,7 @@ Section CORRECTNESS. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } + apply ZExtra.mod_0_bounds; crush; try lia. admit. admit. } crush. exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. @@ -1571,6 +1567,13 @@ Section CORRECTNESS. (Integers.Ptrofs.repr ptr))) v). apply X in H0. invert H0. congruence. + constructor; simplify. unfold Verilog.merge_regs. unfold_merge. + rewrite AssocMap.gso. + assumption. lia. + unfold Verilog.merge_regs. unfold_merge. + rewrite AssocMap.gso. + assumption. lia. + + (** Preamble *) invert MARR. crush. -- cgit