From 936ce165a5ac0da8f3c5d7aa3c398ad8860eeea6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 28 Jun 2022 23:47:07 +0100 Subject: Work on if-conversion proof --- src/hls/GibleSeq.v | 63 +++++++++++ src/hls/IfConversion.v | 17 +-- src/hls/IfConversionproof.v | 249 ++++++++++++++++++++++++++++++++++++-------- 3 files changed, 282 insertions(+), 47 deletions(-) diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index acc47ed..9e2cfc5 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -30,6 +30,7 @@ Require Import compcert.verilog.Op. Require Import vericert.common.Vericertlib. Require Import vericert.hls.Gible. +Require Import vericert.hls.Predicate. (*| ======== @@ -121,6 +122,26 @@ Proof. constructor; auto. Qed. +#[local] Notation "'mki'" := (mk_instr_state) (at level 1). + +Lemma exec_rbexit_truthy : + forall A B bb ge sp rs pr m rs' pr' m' pc', + @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) -> + exists p b1 b2, + truthy pr' p + /\ bb = b1 ++ (RBexit p (RBgoto pc')) :: b2 + /\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')). +Proof. + induction bb; crush. + inv H. inv H. + - destruct state'. exploit IHbb; eauto; simplify. + exists x. exists (a :: x0). exists x1. simplify; auto. + econstructor; eauto. + - inv H3. + exists p. exists nil. exists bb. crush. + constructor. +Qed. + #[local] Open Scope positive. Lemma max_pred_function_use : @@ -130,3 +151,45 @@ Lemma max_pred_function_use : In p (pred_uses i) -> p <= max_pred_function f. Proof. Admitted. + +Ltac truthy_falsy := + match goal with + | H: instr_falsy ?ps (RBop ?p _ _ _), H2: truthy ?ps ?p |- _ => + solve [inv H2; inv H; crush] + | H: instr_falsy ?ps (RBload ?p _ _ _ _), H2: truthy ?ps ?p |- _ => + solve [inv H2; inv H; crush] + | H: instr_falsy ?ps (RBstore ?p _ _ _ _), H2: truthy ?ps ?p |- _ => + solve [inv H2; inv H; crush] + | H: instr_falsy ?ps (RBexit ?p _), H2: truthy ?ps ?p |- _ => + solve [inv H2; inv H; crush] + | H: instr_falsy ?ps (RBsetpred ?p _ _ _), H2: truthy ?ps ?p |- _ => + solve [inv H2; inv H; crush] + end. + +Lemma exec_determ : + forall A B ge sp s1 a s2 s2', + @step_instr A B ge sp s1 a s2 -> + step_instr ge sp s1 a s2' -> + s2 = s2'. +Proof. + inversion 1; subst; crush. + - inv H0; auto. + - inv H2; crush; truthy_falsy. + - inv H3; crush. truthy_falsy. + - inv H3; crush. truthy_falsy. + - inv H2; crush. truthy_falsy. + - inv H1; crush. truthy_falsy. + - destruct st; simplify. inv H1; crush; truthy_falsy. +Qed. + +Lemma append3 : + forall A B l0 l1 sp ge s1 s2 s3, + step_list2 (step_instr ge) sp s1 l0 s2 -> + @SeqBB.step A B ge sp s1 (l0 ++ l1) s3 -> + @SeqBB.step A B ge sp s2 l1 s3. +Proof. + induction l0; crush. inv H. auto. + inv H0. inv H. assert (i1 = (Iexec state')) by (eapply exec_determ; eauto). subst. eauto. + inv H. assert (i1 = (Iterm state' cf)) by (eapply exec_determ; eauto). subst. + exfalso; eapply step_list2_false; eauto. +Qed. diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 01801c3..db4bba6 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -59,15 +59,17 @@ Definition map_if_convert (p: option pred_op) (i: instr) := | _ => i end. -Definition if_convert_block (next: node) (b_next: SeqBB.t) (_: unit) (i: instr) := +Definition if_convert_block (next: node) (b_next: SeqBB.t) (i: instr) := match i with | RBexit p (RBgoto next') => if (next =? next')%positive - then (tt, map (map_if_convert p) b_next) - else (tt, i::nil) - | _ => (tt, i::nil) + then map (map_if_convert p) b_next + else i::nil + | _ => i::nil end. +Definition wrap_unit {A B} (f: A -> B) (_: unit) (a: A) := (tt, f a). + Definition predicated_store i := match i with | RBstore _ _ _ _ _ => true @@ -87,7 +89,7 @@ Definition if_convert (orig_c c: code) (main next: node) := match orig_c ! main, orig_c ! next with | Some b_main, Some b_next => if decide_if_convert b_next then - PTree.set main (snd (replace_section (if_convert_block next b_next) tt b_main)) c + PTree.set main (snd (replace_section (wrap_unit (if_convert_block next b_next)) tt b_main)) c else c | _, _ => c end. @@ -203,12 +205,15 @@ Definition ifconv_list (headers: list node) (c: code) := (* let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in *) (* (S (fst p), PTree.set (fst nb) nbb (snd p)). *) +Definition if_convert_code (c: code) iflist := + fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c. + Definition transf_function (f: function) : function := let (b, _) := build_bourdoncle f in let b' := get_loops b in let iflist := ifconv_list b' f.(fn_code) in mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) - (fold_left (fun s n => if_convert s (fst n) (snd n)) iflist f.(fn_code)) + (if_convert_code f.(fn_code) iflist) f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index 0aac3af..de44118 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -72,13 +72,40 @@ Inductive if_conv_block_spec (c: code): SeqBB.t -> SeqBB.t -> Prop := if_conv_block_spec c b' ta -> if_conv_block_spec c (RBexit p (RBgoto pc')::b) (map (map_if_convert p) ta++tb). -Lemma transf_spec_correct : +Lemma transf_spec_correct' : forall f pc b, f.(fn_code) ! pc = Some b -> exists b', (transf_function f).(fn_code) ! pc = Some b' /\ if_conv_block_spec f.(fn_code) b b'. Proof. Admitted. +Inductive replace_spec_unit (f: instr -> SeqBB.t) + : SeqBB.t -> SeqBB.t -> Prop := +| replace_spec_cons : forall i b b', + replace_spec_unit f b b' -> + replace_spec_unit f (i :: b) (f i ++ b') +| replace_spec_nil : + replace_spec_unit f nil nil +. + +Definition if_conv_replace n nb := replace_spec_unit (if_convert_block n nb). + +Inductive if_conv_spec (c c': code) (pc: node): Prop := +| if_conv_unchanged : + c ! pc = c' ! pc -> + if_conv_spec c c' pc +| if_conv_changed : forall b b' pc' tb, + if_conv_replace pc' b' b tb -> + c ! pc = Some b -> + c ! pc' = Some b' -> + c' ! pc = Some tb -> + if_conv_spec c c' pc. + +Lemma transf_spec_correct : + forall f pc, + if_conv_spec f.(fn_code) (transf_function f).(fn_code) pc. +Proof. Admitted. + Section CORRECTNESS. Context (prog tprog : program). @@ -92,16 +119,28 @@ Section CORRECTNESS. f.(fn_code) ! pc = Some block2 -> SeqBB.step tge sp in_s' block2 out_s. + (* (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) + (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)) + (IS_B: exists b, f.(fn_code)!pc0 = Some b) + (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b), + *) + Variant match_states : option SeqBB.t -> state -> state -> Prop := - | match_state_true : + | match_state_some : forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0 (TF: transf_function f = tf) (STK: Forall2 match_stackframe stk stk') - (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) - (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)) - (IS_B: exists b, f.(fn_code)!pc0 = Some b) - (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b), + (* This can be improved with a recursive relation for a more general structure of the + if-conversion proof. *) + (IS_B: f.(fn_code)!pc = Some b) + (EXTRAP: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) + (SIM: step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)), match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0) + | match_state_none : + forall stk stk' f tf sp pc rs p m + (TF: transf_function f = tf) + (STK: Forall2 match_stackframe stk stk'), + match_states None (State stk f sp pc rs p m) (State stk' tf sp pc rs p m) | match_callstate : forall cs cs' f tf args m (TF: transf_fundef f = tf) @@ -136,8 +175,8 @@ Section CORRECTNESS. funsig (transf_fundef f) = funsig f. Proof using. unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f. - unfold transf_function. destruct_match; auto. auto. - Admitted. + unfold transf_function. destruct_match. auto. auto. + Qed. Lemma functions_translated: forall (v: Values.val) (f: GibleSeq.fundef), @@ -167,7 +206,7 @@ Section CORRECTNESS. repeat ffts. Qed. -(*) Lemma transf_initial_states : + Lemma transf_initial_states : forall s1, initial_state prog s1 -> exists s2, initial_state tprog s2 /\ match_states None s1 s2. @@ -218,22 +257,148 @@ Section CORRECTNESS. Definition measure (b: option SeqBB.t): nat := match b with - | None => 0 - | Some b' => 1 + length b' + | None => 1 + | Some _ => 0 + end. + + Lemma sim_star : + forall s1 b t s, + (exists b' s2, + star step tge s1 t s2 /\ ltof _ measure b' b + /\ match_states b' s s2) -> + exists b' s2, + (plus step tge s1 t s2 \/ + star step tge s1 t s2 /\ ltof _ measure b' b) /\ + match_states b' s s2. + Proof. intros; simplify. do 3 econstructor; eauto. Qed. + + Lemma sim_plus : + forall s1 b t s, + (exists b' s2, plus step tge s1 t s2 /\ match_states b' s s2) -> + exists b' s2, + (plus step tge s1 t s2 \/ + star step tge s1 t s2 /\ ltof _ measure b' b) /\ + match_states b' s s2. + Proof. intros; simplify. do 3 econstructor; eauto. Qed. + + Lemma step_instr : + forall sp s s' a, + step_instr ge sp (Iexec s) a (Iexec s') -> + step_instr tge sp (Iexec s) a (Iexec s'). + Proof. + inversion 1; subst; econstructor; eauto. + - now rewrite <- eval_op_eq. + - now rewrite <- eval_addressing_eq. + - now rewrite <- eval_addressing_eq. + Qed. + + Lemma step_instr_term : + forall sp s s' a cf, + Gible.step_instr ge sp (Iexec s) a (Iterm s' cf) -> + Gible.step_instr tge sp (Iexec s) a (Iterm s' cf). + Proof. inversion 1; subst; constructor; auto. Qed. + + Lemma seqbb_eq : + forall bb sp rs pr m rs' pr' m' cf, + SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> + SeqBB.step tge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf). + Proof. + induction bb; crush; inv H. + - econstructor; eauto. apply step_instr; eassumption. + destruct state'. eapply IHbb; eauto. + - constructor; apply step_instr_term; auto. + Qed. + + Lemma fn_all_eq : + forall f tf, + transf_function f = tf -> + fn_stacksize f = fn_stacksize tf + /\ fn_sig f = fn_sig tf + /\ fn_params f = fn_params tf + /\ fn_entrypoint f = fn_entrypoint tf + /\ exists l, if_convert_code (fn_code f) l = fn_code tf. + Proof. + intros; simplify; unfold transf_function in *; destruct_match; inv H; auto. + eexists; simplify; eauto. + Qed. + + Ltac func_info := + match goal with + H: transf_function _ = _ |- _ => + let H2 := fresh "ALL_EQ" in + pose proof (fn_all_eq _ _ H) as H2; simplify end. - Lemma temp: - forall c b b' sp rs pr m rs' pr' m' cf, - if_conv_block_spec c b b' -> - SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iterm (mki rs' pr' m') cf) -> - SeqBB.step tge sp (Iexec (mki rs pr m)) b' (Iterm (mki rs' pr' m') cf) - \/ (exists pc' nb b'1 b'2 b'3 p, - c ! pc' = Some nb - /\ step_list2 (step_instr tge) sp (Iexec (mki rs pr m)) b'1 (Iexec (mki rs' pr' m')) - /\ b' = b'1 ++ map (map_if_convert p) b'2 ++ b'3 - /\ cf = RBgoto pc' - /\ if_conv_block_spec c nb b'2). - Admitted. + Lemma step_cf_eq : + forall stk stk' f tf sp pc rs pr m cf s t, + step_cf_instr ge (State stk f sp pc rs pr m) cf t s -> + Forall2 match_stackframe stk stk' -> + transf_function f = tf -> + exists s', step_cf_instr tge (State stk' tf sp pc rs pr m) cf t s' + /\ match_states None s s'. + Proof. + inversion 1; subst; simplify; + try solve [func_info; do 2 econstructor; econstructor; eauto]. + - do 2 econstructor. constructor; eauto. constructor; eauto. constructor; auto. + constructor. auto. + - do 2 econstructor. constructor; eauto. + func_info. + rewrite H2 in *. rewrite H12. auto. constructor; auto. + - func_info. do 2 econstructor. econstructor; eauto. rewrite H2 in *. + eauto. econstructor; auto. + Qed. + + (*Lemma event0_trans : + forall stk f sp pc rs' pr' m' cf t f0 sp0 pc0 rs0 pr0 m0 stack, + step_cf_instr ge (State stk f sp pc rs' pr' m') cf t (State stack f0 sp0 pc0 rs0 pr0 m0) -> + t = E0 /\ f = f0 /\ sp = sp0 /\ stk = stack. + Proof. + inversion 1; subst; crush.*) + + Lemma cf_dec : + forall a pc, {a = RBgoto pc} + {a <> RBgoto pc}. + Proof. + destruct a; try solve [right; crush]. + intros. destruct (peq n pc); subst. + left; auto. + right. unfold not in *; intros. inv H. auto. + Qed. + + Lemma exec_if_conv : + forall bb sp rs pr m rs' pr' m' pc' b' tb, + SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) -> + if_conv_replace pc' b' bb tb -> + exists p b rb, + tb = b ++ (map (map_if_convert p) b') ++ rb + /\ SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iexec (mki rs' pr' m')). + Proof. + Admitted. + + Lemma temp2: + forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk', + (fn_code f) ! pc = Some bb -> + SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> + step_cf_instr ge (State stk f sp pc rs' pr' m') cf t s1' -> + Forall2 match_stackframe stk stk' -> + exists b' s2', + (plus step tge (State stk' (transf_function f) sp pc rs pr m) t s2' \/ + star step tge (State stk' (transf_function f) sp pc rs pr m) t s2' + /\ ltof (option SeqBB.t) measure b' None) /\ + match_states b' s1' s2'. + Proof. + intros * H H0 H1 STK. + pose proof (transf_spec_correct f pc) as X; inv X. + - apply sim_plus. rewrite H in H2. symmetry in H2. + exploit step_cf_eq; eauto; simplify. + do 3 econstructor. apply plus_one. econstructor; eauto. + apply seqbb_eq; eauto. eauto. + - simplify. + destruct (cf_dec cf pc'); subst. inv H1. + exploit exec_if_conv; eauto; simplify. + exploit exec_rbexit_truthy; eauto; simplify. + apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m). + simplify; try (unfold ltof; auto). apply star_refl. + constructor; auto. unfold sem_extrap; simplify. Lemma step_cf_matches : forall b s cf t s' ts, @@ -253,22 +418,26 @@ Section CORRECTNESS. Proof using TRANSL. inversion 1; subst; simplify; match goal with H: context[match_states] |- _ => inv H end. - - - exploit temp; eauto; simplify. inv H3. - pose proof (transf_spec_correct _ _ _ H4); simplify. - exploit step_cf_matches; eauto. - econstructor; eauto. unfold sem_extrap; intros. - unfold sem_extrap in EXT. - rewrite H8 in H3; simplify. - do 2 econstructor. split. left. eapply plus_one. econstructor; eauto. - unfold sem_extrap in EXT. eapply EXT. eauto. admit. - instantiate (1 := State stack (transf_function f0) sp0 pc0 rs0 pr0 m0). - admit. constructor; eauto. admit. unfold sem_extrap. intros. admit. - eapply star_refl. intros. admit. - - - simplify. inv H2. do 2 econstructor. split. admit. - econstructor; eauto. admit. admit. intros. - rewrite H3 in H2. inv H2. eauto + - admit. + - eauto using temp2. Admitted. + + + (* - *) + (* exploit temp; eauto; simplify. inv H3. *) + (* pose proof (transf_spec_correct _ _ _ H4); simplify. *) + (* exploit step_cf_matches; eauto. *) + (* econstructor; eauto. unfold sem_extrap; intros. *) + (* unfold sem_extrap in EXT. *) + (* rewrite H8 in H3; simplify. *) + (* do 2 econstructor. split. left. eapply plus_one. econstructor; eauto. *) + (* unfold sem_extrap in EXT. eapply EXT. eauto. admit. *) + (* instantiate (1 := State stack (transf_function f0) sp0 pc0 rs0 pr0 m0). *) + (* admit. constructor; eauto. admit. unfold sem_extrap. intros. admit. *) + (* eapply star_refl. intros. admit. *) + (* - *) + (* simplify. inv H2. do 2 econstructor. split. admit. *) + (* econstructor; eauto. admit. admit. intros. *) + (* rewrite H3 in H2. inv H2. eauto *) Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). @@ -285,6 +454,4 @@ Section CORRECTNESS. - apply senv_preserved. Qed. - -*) End CORRECTNESS. -- cgit