From e8803586c36512b8fe65ec58de1f1eec990ce1d0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 20 Nov 2020 21:04:47 +0100 Subject: Trying to finish the bisimu reduce proof for builtin (last case admitted) --- aarch64/Asmblockdeps.v | 105 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 76 insertions(+), 29 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 1bccb5dd..d778ddca 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -43,12 +43,15 @@ Open Scope impure. (** auxiliary treatments of builtins *) -Definition has_builtin(bb: bblock): bool := - match exit bb with +Definition is_builtin(ex: option control): bool := + match ex with | Some (Pbuiltin _ _ _) => true | _ => false end. +Definition has_builtin(bb: bblock): bool := + is_builtin (exit bb). + Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}. Proof. intros. @@ -74,16 +77,19 @@ Definition assert_same_builtin (bb1 bb2: bblock): ?? unit := else FAILWITH "Different ef in Pbuiltin" | _ => FAILWITH "Expected a builtin: found something else" (* XXX: on peut raffiner le message d'erreur si nécessaire *) end - | _ => RET tt (* ok *) + | _ => match exit bb2 with + | Some (Pbuiltin ef2 lbar2 brr2) => FAILWITH "Expected a something else: found a builtin" + | _ => RET tt (* ok *) + end end. Lemma assert_same_builtin_correct (bb1 bb2: bblock): WHEN assert_same_builtin bb1 bb2 ~> _ THEN - has_builtin bb1 = true -> exit bb1 = exit bb2. + has_builtin bb1 = true \/ has_builtin bb2 = true -> exit bb1 = exit bb2. Proof. unfold assert_same_builtin, has_builtin. - destruct (exit bb1) as [[]|]; simpl; try (wlp_simplify; congruence). - destruct (exit bb2) as [[]|]; wlp_simplify. + destruct (exit bb1) as [[]|]; simpl; + destruct (exit bb2) as [[]|]; wlp_simplify; try congruence. Qed. Global Opaque assert_same_builtin. Local Hint Resolve assert_same_builtin_correct: wlp. @@ -1057,7 +1063,7 @@ Definition trans_control (ctl: control) : inst := (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil)); (#X16, Op (Constant Vundef) Enil); (#X17, Op (Constant Vundef) Enil)] - | Pbuiltin ef args res => [(# PC, Op (Control OError) Enil)] + | Pbuiltin ef args res => [] end. Definition trans_exit (ex: option control) : L.inst := @@ -1937,14 +1943,23 @@ Qed. Theorem bisimu_exit ex sz rsr mr sr: match_states (State rsr mr) sr -> + (*is_builtin ex = false ->*) match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit ex)) sr sr). Proof. intros MS; unfold estep. destruct ex. - destruct c. + exploit (bisimu_control i sz rsr mr sr); eauto. - + simpl; inv MS. unfold control_eval; destruct Ge. - replace_pc; rewrite H0. reflexivity. + + simpl. inv MS. eexists; split; [| split]. + unfold control_eval; destruct Ge. + replace_pc; rewrite (H0 PC); eauto. + rewrite assign_diff; auto. + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst. + * rewrite sr_gss, Pregmap.gss. reflexivity. + * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto. + + (*simpl; inv MS. unfold control_eval; destruct Ge. + replace_pc; rewrite H0. congruence.*) - simpl. inv MS. eexists; split; [| split]. + unfold control_eval; destruct Ge. replace_pc; rewrite (H0 PC); eauto. @@ -2220,12 +2235,59 @@ Qed. Lemma bblock_simu_reduce: forall p1 p2, L.bblock_simu Ge (trans_block p1) (trans_block p2) -> - (has_builtin p1 = true -> exit p1 = exit p2) -> + (has_builtin p1 = true \/ has_builtin p2 = true -> exit p1 = exit p2) -> Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2. Proof. unfold bblock_simu. intros p1 p2 H0 BLT rs m EBB. unfold exec_bblock. - generalize (H0 (trans_state (State rs m))); clear H0. + generalize (bblock_simu_reduce_aux p1 p2 H0). + unfold bblock_simu_aux. clear H0. + unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2). + assert ((has_builtin p1 = false /\ has_builtin p2 = false) \/ (has_builtin p1 = true \/ has_builtin p2 = true)). { repeat destruct (has_builtin _); simpl; intuition. } + destruct H as [[X1 X2]|H]. + - (* Not a builtin *) + exploit (H0); eauto; erewrite H1; simpl; (*gen*) + unfold estep; unfold has_builtin in *. + { destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *. + inversion H2; subst. rewrite H3; discriminate. } + destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *. + { inversion H2; subst. rewrite H3. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. + intros H4. eexists; eexists; split; try reflexivity. + destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto. + inversion H4. econstructor. } + { inversion H2; subst. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. +intros H4. eexists; eexists; split; try reflexivity. + destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto. + inversion H4. rewrite H3. econstructor. } + - (* Builtin *) + exploit (BLT); eauto. + intros EXIT. + unfold has_builtin in H. + assert (is_builtin (exit p1) = true). { rewrite <- EXIT in H; intuition. } + clear H. + generalize (H0 rs m); eauto; erewrite H1; simpl; + unfold estep. destruct (exit p1) as [[]|] eqn:EQEX1; try discriminate. + rewrite <- EXIT. + intros CONTRA. + exploit (CONTRA); try discriminate. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. + intros H4. eexists; eexists; split; try reflexivity. + inversion H2; subst. inversion H4; subst. + econstructor; eauto. + + unfold incrPC in H5. + replace (rs2 SP) with (rs1 SP). + replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto. + * apply functional_extensionality. + intros r; destruct (PregEq.eq r PC); try discriminate. + replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto. + rewrite H5; rewrite Pregmap.gso; auto. + * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto. + rewrite H5; rewrite Pregmap.gso; auto; try discriminate. + + admit. + +(* generalize (H0 (trans_state (State rs m))); clear H0. intros H0 m' t0 (rs1 & m1 & H1 & H2). exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto. exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto. @@ -2248,25 +2310,10 @@ Proof. - replace (_m0) with (_m); auto. congruence. - apply functional_extensionality. intros r. generalize (H1 r). intros Hr. congruence. - * discriminate. - + * discriminate.*) - (*generalize (bblock_simu_reduce_aux p1 p2 H0).*) - (*unfold bblock_simu_aux. clear H0.*) - (*unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2).*) - (*generalize (H0 rs m); clear H0. rewrite H1. simpl. unfold estep.*) - (*inversion H2.*) - (*- intros H6. exploit (H6); try discriminate; clear H6.*) - (*destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.*) - (*intros H6. eexists; eexists; split; try reflexivity.*) - (*destruct (exit p2) eqn:EQOC.*) - (*destruct (c).*) - (*+ econstructor; eauto.*) - (*+*) - (*generalize (H0 (trans_state (State rs m))); clear H0.*) - (*intro H0.*) - - (*exploit (*) +Admitted. + (*Qed.*) (** Used for debug traces *) -- cgit