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