From d1a6bdc08bc067cf74451a5ffa2aefd4e9e6b79f Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 29 Sep 2021 14:49:46 +0100 Subject: [WIP] Updating proof for new state matching --- src/hls/HTLgenproof.v | 108 ++++++++++++++++++++++++++++++++------------------ 1 file changed, 69 insertions(+), 39 deletions(-) (limited to 'src/hls') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index c0338ed..18551a3 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -524,11 +524,6 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. - Axiom no_pointer_return : forall (rs : RTL.regset) r s (f : RTL.function) sp pc rs mem f S, - (RTL.fn_code f) ! pc = Some (RTL.Ireturn (Some r)) -> - match_states ge (RTL.State s f sp pc rs mem) S -> - (not_pointer rs !! r). - (** The following are assumed to be guaranteed by an inlining pass previous to this translation. [ only_main_stores ] should be a direct result of that inlining. @@ -549,17 +544,23 @@ Section CORRECTNESS. match_states ge (RTL.Callstate rtl_stk (AST.Internal f) args mem) S -> (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. + Lemma match_sp_exists : forall sp stk blk, + match_sp stk sp blk -> exists blk', sp = Values.Vptr blk' Ptrofs.zero. + Proof. inversion 1; subst; eexists; eauto. Qed. + Lemma mem_free_zero_match_frames : forall rtl_stk htl_stk mem mem' blk id, Mem.free mem blk 0 0 = Some mem' -> match_frames ge id mem rtl_stk htl_stk -> match_frames ge id mem' rtl_stk htl_stk. Proof. - Lemma mem_free_match_arrs : forall m f sp blk mem mem' asa, + Lemma mem_free_match_arrs : forall m f rtl_stk sp blk blk' mem mem' asa, Mem.free mem blk 0 0 = Some mem' -> - match_arrs m f (Values.Vptr sp (Ptrofs.repr 0)) mem asa -> - match_arrs m f (Values.Vptr sp (Ptrofs.repr 0)) mem' asa. + match_sp rtl_stk sp blk' -> + match_arrs m f sp mem asa -> + match_arrs m f sp mem' asa. Proof. - intros * Hfree Hmatch. + intros * Hfree SP Hmatch. + destruct (match_sp_exists _ _ _ SP); subst. inv Hmatch. apply match_arr with (stack:=stack); crush. intros. @@ -567,12 +568,12 @@ Section CORRECTNESS. Qed. Hint Resolve mem_free_match_arrs : htlproof. - Lemma mem_free_stack_based_pointers : forall mem mem' blk sp sz, + Lemma mem_free_stack_based_pointers : forall mem mem' blk blk' sp sz, Mem.free mem blk 0 0 = Some mem' -> - arr_stack_based_pointers sp mem sz (Values.Vptr sp (Ptrofs.repr 0)) -> - arr_stack_based_pointers sp mem' sz (Values.Vptr sp (Ptrofs.repr 0)). + arr_stack_based_pointers blk' mem sz sp -> + arr_stack_based_pointers blk' mem' sz sp. Proof. - intros * Hfree Hstk. + intros * Hfree SP Hstk. unfold arr_stack_based_pointers in *. intros. erewrite <- (mem_free_zero_loadv mem mem'); eauto. @@ -602,12 +603,14 @@ Section CORRECTNESS. match_frames ge id mem rtl_stk htl_stk -> match_frames ge id mem' rtl_stk htl_stk. Proof. - Lemma mem_alloc_zero_match_arrs : forall m f sp blk mem mem' asa, + Lemma mem_alloc_zero_match_arrs : forall m f rtl_stk sp blk blk' mem mem' asa, Mem.alloc mem 0 0 = (mem', blk) -> - match_arrs m f (Values.Vptr sp (Ptrofs.repr 0)) mem asa -> - match_arrs m f (Values.Vptr sp (Ptrofs.repr 0)) mem' asa. + match_sp rtl_stk sp blk' -> + match_arrs m f sp mem asa -> + match_arrs m f sp mem' asa. Proof. - intros * Halloc Hmatch. + intros * Halloc SP Hmatch. + destruct (match_sp_exists _ _ _ SP); subst. inv Hmatch. apply match_arr with (stack:=stack); crush. intros. @@ -615,10 +618,10 @@ Section CORRECTNESS. Qed. Hint Resolve mem_alloc_zero_match_arrs : htlproof. - Lemma mem_alloc_zero_stack_based_pointers : forall mem mem' blk sp sz, + Lemma mem_alloc_zero_stack_based_pointers : forall mem mem' blk blk' sp sz, Mem.alloc mem 0 0 = (mem', blk) -> - arr_stack_based_pointers sp mem sz (Values.Vptr sp (Ptrofs.repr 0)) -> - arr_stack_based_pointers sp mem' sz (Values.Vptr sp (Ptrofs.repr 0)). + arr_stack_based_pointers blk' mem sz sp -> + arr_stack_based_pointers blk' mem' sz sp. Proof. intros * Hfree Hstk. unfold arr_stack_based_pointers in *. @@ -717,15 +720,16 @@ Section CORRECTNESS. Qed. Lemma op_stack_based : - forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, + forall F V sp blk rtl_stk v m args rs op ge pc' res0 pc f e fin rtrn st stk, tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') (Verilog.Vnonblock (Verilog.Vvar res0) e) (state_goto st pc') -> - reg_stack_based_pointers sp rs -> + reg_stack_based_pointers blk rs -> + match_sp rtl_stk sp blk -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> - @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op + @Op.eval_operation F V ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> - stack_based v sp. + stack_based v blk. Proof. Ltac solve_no_ptr := match goal with @@ -753,10 +757,16 @@ Section CORRECTNESS. | |- context[match ?g with _ => _ end] => destruct g; try discriminate | |- _ => simplify; solve [auto] end. - intros F V sp v m args rs op g pc' res0 pc f e fin rtrn st stk INSTR RSBP SEL EVAL. - inv INSTR. unfold translate_instr in H5. + intros * INSTR RSBP SP SEL EVAL. + inversion INSTR. subst. unfold translate_instr in H5. unfold_match H5; repeat (unfold_match H5); repeat (simplify; solve_no_ptr). - Qed. + (** Ainstack *) { + simplify. + inv SP; crush. + (** rtl_stk = stk_hd::stk_tl, should be impossible *) + admit. + } + Admitted. Lemma int_inj : forall x y, @@ -1111,6 +1121,11 @@ Section CORRECTNESS. rewrite H3 in H2. discriminate. Qed. + Lemma match_sp_zero_ofs : forall ofs stk b1 b2, + match_sp stk (Values.Vptr b1 ofs) b2 -> + ofs = (Ptrofs.repr 0). + Proof. induction stk; simplify; inv H; crush. Qed. + Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res mid ml st , match_states ge (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> @@ -1264,9 +1279,9 @@ Section CORRECTNESS. rewrite Heqv2 in H4. inv H4. + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. - inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). - all: repeat (unfold_match Heqv). - eexists. split. constructor. + eexists. repeat (simplify; eval_correct_tac). + replace i1 with (Ptrofs.repr 0) by (symmetry; eauto using match_sp_zero_ofs). + constructor. unfold valueToPtr, ZToValue. rewrite Ptrofs.add_zero_l. unfold Ptrofs.of_int. rewrite Int.unsigned_repr. symmetry. apply Ptrofs.repr_unsigned. unfold check_address_parameter_unsigned in *. apply Ptrofs.unsigned_range_2. @@ -1432,7 +1447,7 @@ Section CORRECTNESS. + repeat constructor. + constructor. + big_tac. - - inv CONST. inv MARR. simplify. big_tac. + - inv CONST. inv MARR. simplify. big_tac; auto. + constructor; rewrite AssocMap.gso; crush. + trans_externctrl. Unshelve. exact tt. @@ -1600,6 +1615,8 @@ Section CORRECTNESS. hauto unfold: reg, AssocMapExt.get_default. Qed. + Hint Constructors match_sp : htlproof. + Lemma transl_callstate_correct: forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) (m : mem) (m' : Mem.mem') (stk : Values.block), @@ -1616,6 +1633,19 @@ Section CORRECTNESS. inversion MSTATE. inversion TF. simplify. + Lemma match_frames_match_sp : forall rtl_stk htl_stk mid m stk, + match_frames ge mid m rtl_stk htl_stk -> + exists blk, match_sp rtl_stk (Values.Vptr stk Ptrofs.zero) blk. + Proof. + induction rtl_stk; simplify. + - repeat econstructor. + - destruct a. + inv H. + eauto with htlproof. + Qed. + edestruct (match_frames_match_sp) as [blk ?]; eauto. + + eexists. split. apply Smallstep.plus_one. solve [constructor]. @@ -1631,7 +1661,10 @@ Section CORRECTNESS. - big_tac. destruct (Mem.load AST.Mint32 m' stk (Ptrofs.unsigned (Ptrofs.repr (4 * ptr)))) eqn:eq_load; repeat constructor. erewrite (Mem.load_alloc_same m 0 (RTL.fn_stacksize f) m' _ _ _ _ v); eauto; repeat econstructor. - - auto using stack_based_non_pointers. + - + eapply match_frames_match_sp. + (* SP *) admit. + - (* RSBP *) admit. - unfold arr_stack_based_pointers; intros. destruct (Mem.loadv AST.Mint32 m' (Values.Val.offset_ptr (Values.Vptr stk Ptrofs.zero) (Ptrofs.repr (4 * ptr)))) eqn:eq_load. @@ -1659,7 +1692,7 @@ Section CORRECTNESS. + not_control_reg. Unshelve. all: eauto. - Qed. + Admitted. Hint Resolve transl_callstate_correct : htlproof. Lemma only_internal_calls : forall fd fn rs, @@ -2114,7 +2147,6 @@ Section CORRECTNESS. rewrite AssocMap.gso by crush. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gempty. - + (* Non-pointers *) admit. + (* Argument values match *) big_tac. replace (((AssocMapExt.merge value @@ -2133,7 +2165,7 @@ Section CORRECTNESS. -- eauto using separate_params_reset. Unshelve. all: eauto; exact tt. - Admitted. + Qed. Hint Resolve transl_icall_correct : htlproof. Close Scope rtl. @@ -2188,7 +2220,6 @@ Section CORRECTNESS. by (eapply RTL.max_reg_function_use; eauto; crush). xomega. * simpl. eauto with htlproof. - + destruct or; simpl; eauto using no_pointer_return. Unshelve. try exact tt; eauto. Qed. Hint Resolve transl_ireturn_correct : htlproof. @@ -2253,8 +2284,7 @@ Section CORRECTNESS. * not_control_reg. + auto using match_arrs_empty. + eapply stack_based_set; eauto. - unfold not_pointer in *. - destruct vres; crush. + (* RSBP *) admit. + (* match_constants *) inv CONST. big_tac. @@ -2266,7 +2296,7 @@ Section CORRECTNESS. repeat rewrite AssocMap.gso; auto; not_control_reg. + unfold match_externctrl. simplify. Unshelve. all: try exact tt; eauto. - Qed. + Admitted. Hint Resolve transl_returnstate_correct : htlproof. Ltac tac := -- cgit