diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-06-30 18:02:39 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-30 18:02:39 +0100 |
commit | a641f7094f9cdcfb56fe63b798ba3d86f6537b6c (patch) | |
tree | 0742de5daddf877c6cb3ceee129855b7868001cd /src | |
parent | c90b9ba8d6f37c58519298cfa1ff8960373fcafa (diff) | |
download | vericert-a641f7094f9cdcfb56fe63b798ba3d86f6537b6c.tar.gz vericert-a641f7094f9cdcfb56fe63b798ba3d86f6537b6c.zip |
Nearly finished if-conversion proof
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/IfConversion.v | 18 | ||||
-rw-r--r-- | src/hls/IfConversionproof.v | 345 |
2 files changed, 298 insertions, 65 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index db4bba6..0b1c852 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -37,6 +37,8 @@ Require Import vericert.bourdoncle.Bourdoncle. Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). +#[local] Open Scope positive. + (*| ============= If-Conversion @@ -59,10 +61,22 @@ Definition map_if_convert (p: option pred_op) (i: instr) := | _ => i end. +Definition wf_transition (pl: list predicate) (i: instr) := + match i with + | RBsetpred _ _ _ p => negb (existsb (Pos.eqb p) pl) + | _ => true + end. + +Definition wf_transition_block (p: pred_op) (b: SeqBB.t) := + forallb (wf_transition (predicate_use p)) b. + +Definition wf_transition_block_opt (p: option pred_op) b := + Option.default true (Option.map (fun p' => wf_transition_block p' b) p). + Definition if_convert_block (next: node) (b_next: SeqBB.t) (i: instr) := match i with | RBexit p (RBgoto next') => - if (next =? next')%positive + if (next =? next') && wf_transition_block_opt p b_next then map (map_if_convert p) b_next else i::nil | _ => i::nil @@ -179,7 +193,7 @@ Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * SeqB Module TupOrder <: TotalLeBool. Definition t : Type := positive * positive. - Definition leb (x y: t) := (fst x <=? fst y)%positive. + Definition leb (x y: t) := fst x <=? fst y. Infix "<=?" := leb (at level 70, no associativity). Theorem leb_total : forall a1 a2, (a1 <=? a2) = true \/ (a2 <=? a1) = true. Proof. unfold leb; intros; repeat rewrite Pos.leb_le; lia. Qed. diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index ca4d18b..8b02e37 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -72,13 +72,6 @@ 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' : - 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', @@ -106,6 +99,47 @@ Lemma transf_spec_correct : if_conv_spec f.(fn_code) (transf_function f).(fn_code) pc. Proof. Admitted. +Inductive wf_trans : option pred_op -> SeqBB.t -> Prop := +| wf_trans_None: forall b, wf_trans None b +| wf_trans_Some: forall p b, + (forall op c args p', + In (RBsetpred op c args p') b -> + ~ In p' (predicate_use p)) -> + wf_trans (Some p) b. + +Lemma wf_transition_block_opt_prop : + forall b p, + wf_transition_block_opt p b = true <-> wf_trans p b. +Proof. + destruct p. + 2: { + split. unfold wf_transition_block_opt; intros. + constructor. + intros. unfold wf_transition_block_opt. simplify; auto. + } + generalize dependent p. induction b; split; crush. + - constructor; crush. + - unfold wf_transition_block_opt in H. simplify. + constructor; auto. intros. unfold wf_transition in H0. + unfold not; intros. inv H. + assert (existsb (Pos.eqb p') (predicate_use p) = true). + { apply existsb_exists; econstructor. split; eauto. apply Pos.eqb_refl. } + now rewrite H in H0. + unfold wf_transition_block in *. eapply forallb_forall in H1; eauto. + unfold wf_transition in *. + assert (existsb (Pos.eqb p') (predicate_use p) = true). + { apply existsb_exists; econstructor. split; eauto. apply Pos.eqb_refl. } + now rewrite H in H1. + - inv H. unfold wf_transition_block_opt. cbn [Option.default Option.map]. + unfold wf_transition_block. apply forallb_forall. intros. + unfold wf_transition. destruct x; auto. + apply H1 in H. + rewrite <- negb_involutive. f_equal; cbn. + destruct (existsb (Pos.eqb p0) (predicate_use p)) eqn:?; auto. + exfalso; apply H. apply existsb_exists in Heqb0; simplify. + apply Pos.eqb_eq in H3. subst. auto. +Qed. + Section CORRECTNESS. Context (prog tprog : program). @@ -133,7 +167,9 @@ Section CORRECTNESS. (* 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) - (IS_TB: forall b', f.(fn_code)!pc0 = Some b' -> tf.(fn_code)!pc0 = if_conv_replace) + (IS_TB: forall b', + f.(fn_code)!pc0 = Some b' -> + exists tb, tf.(fn_code)!pc0 = Some tb /\ if_conv_replace pc b b' tb) (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) @@ -335,11 +371,11 @@ Section CORRECTNESS. end. Lemma step_cf_eq : - forall stk stk' f tf sp pc rs pr m cf s t, + forall stk stk' f tf sp pc rs pr m cf s t pc', 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' + 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; @@ -353,51 +389,236 @@ Section CORRECTNESS. 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 : + Definition 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. + Defined. + + Definition wf_trans_dec : + forall p b, {wf_trans p b} + {~ wf_trans p b}. + Proof. + intros; destruct (wf_transition_block_opt p b) eqn:?. + left. apply wf_transition_block_opt_prop; auto. + right. unfold not; intros. apply wf_transition_block_opt_prop in H. + rewrite H in Heqb0. discriminate. + Defined. + + Definition cf_wf_dec : + forall p b a pc, {a = RBgoto pc /\ wf_trans p b} + {a <> RBgoto pc \/ ~ wf_trans p b}. + Proof. + intros; destruct (cf_dec a pc); destruct (wf_trans_dec p b); tauto. Qed. - Lemma exec_if_conv : - forall A B ge sp pc' b' tb i i' x0 x x1, - step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') -> - if_conv_replace pc' b' (x0 ++ RBexit x (RBgoto pc') :: x1) tb -> - exists b rb, - tb = b ++ (map (map_if_convert x) b') ++ rb - /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). + Lemma wf_trans_comp_false : + forall n pc' x b', + RBgoto n <> RBgoto pc' \/ ~ wf_trans x b' -> + (pc' =? n) && wf_transition_block_opt x b' = false. + Proof. + inversion 1; subst; simplify. + destruct (peq n pc'); subst; [exfalso; auto|]; []. + apply Pos.eqb_neq in n0. rewrite Pos.eqb_sym in n0. + rewrite n0. auto. + destruct (wf_transition_block_opt x b') eqn:?. + - exfalso; apply H0. apply wf_transition_block_opt_prop; auto. + - apply andb_false_r. + Qed. + + Lemma step_list2_app : + forall A B (ge: Genv.t A B) sp a b i i' i'', + step_list2 (Gible.step_instr ge) sp i'' b i' -> + step_list2 (Gible.step_instr ge) sp i a i'' -> + step_list2 (Gible.step_instr ge) sp i (a ++ b) i'. + Proof. + induction a; crush. + - inv H0; auto. + - inv H0. econstructor. + eauto. eapply IHa; eauto. + Qed. + + Lemma map_if_convert_None : + forall b', + map (map_if_convert None) b' = b'. + Proof. + induction b'; crush. + rewrite IHb'; f_equal. destruct a; crush; destruct o; auto. + Qed. + + Lemma truthy_true : + forall pr x p, + truthy pr x -> + truthy pr p -> + truthy pr (combine_pred x p). + Proof. + intros. + inv H; inv H0; cbn [combine_pred] in *; constructor; auto; + rewrite eval_predf_Pand; apply andb_true_intro; auto. + Qed. + #[local] Hint Resolve truthy_true : core. + + Lemma falsy_false : + forall i' a x, + instr_falsy (is_ps i') a -> + instr_falsy (is_ps i') (map_if_convert x a). + Proof. + inversion 1; subst; destruct x; crush; constructor; rewrite eval_predf_Pand; + auto using andb_false_intro2. + Qed. + #[local] Hint Resolve falsy_false : core. + + Lemma map_truthy_instr : + forall A B (ge: Genv.t A B) sp i a x i', + truthy (is_ps i) x -> + Gible.step_instr ge sp (Iexec i) a i' -> + Gible.step_instr ge sp (Iexec i) (map_if_convert x a) i'. + Proof. + inversion 2; subst; crush; + try (solve [econstructor; eauto]). + Qed. + + Lemma map_falsy_instr : + forall A B (ge: Genv.t A B) sp i a x, + eval_predf (is_ps i) x = false -> + Gible.step_instr ge sp (Iexec i) (map_if_convert (Some x) a) (Iexec i). Proof. - Admitted. + intros; destruct a; constructor; cbn; destruct o; constructor; auto; + rewrite eval_predf_Pand; rewrite H; auto. + Qed. + + Lemma map_falsy_list : + forall A B (ge: Genv.t A B) sp b' p i0, + eval_predf (is_ps i0) p = false -> + step_list2 (Gible.step_instr ge) sp (Iexec i0) (map (map_if_convert (Some p)) b') (Iexec i0). + Proof. + induction b'; crush; try constructor. + econstructor; eauto. + apply map_falsy_instr; auto. + Qed. + + Lemma exec_if_conv3 : + forall A B (ge: Genv.t A B) sp a pc' b' i i0, + Gible.step_instr ge sp (Iexec i) a (Iexec i0) -> + step_list2 (Gible.step_instr ge) sp (Iexec i) (if_convert_block pc' b' a) (Iexec i0). + Proof with (simplify; try (solve [econstructor; eauto; constructor])). + inversion 1; subst... destruct a... destruct c... + destruct ((pc' =? n) && wf_transition_block_opt o b') eqn:?... + apply wf_transition_block_opt_prop in H1. inv H1. inv H4. + inv H4. apply map_falsy_list; auto. + Qed. Lemma exec_if_conv2 : - forall A B ge sp pc' b' tb i i' x0 x x1 cf, + forall A B x0 ge sp pc' b' tb i i' x x1 cf, step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') -> - cf <> RBgoto pc' -> + cf <> RBgoto pc' \/ ~ wf_trans x b' -> if_conv_replace pc' b' (x0 ++ RBexit x cf :: x1) tb -> exists b rb, tb = b ++ RBexit x cf :: rb /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof. - Admitted. + induction x0; simplify. + - inv H1. inv H. exists nil. exists b'0. + split; [|constructor]. rewrite app_nil_l. + replace (RBexit x cf :: b'0) with ((RBexit x cf :: nil) ++ b'0) by auto. + f_equal. simplify. destruct cf; auto. + rewrite wf_trans_comp_false; auto. + - inv H1. inv H. + destruct i1; [|exfalso; eapply step_list2_false; eauto]. + exploit IHx0; eauto; simplify. + exists (if_convert_block pc' b' a ++ x2). exists x3. + split. rewrite app_assoc. auto. + eapply step_list2_app; eauto. + apply exec_if_conv3; auto. + Qed. + + Lemma predicate_use_eval_predf : + forall p1 pr p0 b0 b1, + ~ In p0 (predicate_use p1) -> + eval_predf pr p1 = b1 -> + eval_predf pr # p0 <- b0 p1 = b1. + Proof. + induction p1; crush. + - destruct_match. inv Heqp1. simplify. + unfold not in *. + destruct (peq p1 p0); subst; try solve [exfalso; auto]. + unfold eval_predf. simplify. rewrite ! Pos2Nat.id. + rewrite ! Regmap.gso; auto. + - rewrite eval_predf_Pand in *. + assert ((~ In p0 (predicate_use p1_1)) /\ (~ In p0 (predicate_use p1_2))). + { unfold not in *; split; intros; apply H; apply in_or_app; tauto. } + simplify. + erewrite IHp1_1; eauto. + erewrite IHp1_2; eauto. + - rewrite eval_predf_Por in *. + assert ((~ In p0 (predicate_use p1_1)) /\ (~ In p0 (predicate_use p1_2))). + { unfold not in *; split; intros; apply H; apply in_or_app; tauto. } + simplify. + erewrite IHp1_1; eauto. + erewrite IHp1_2; eauto. + Qed. + + Lemma wf_trans_stays_truthy : + forall A B (ge: Genv.t A B) sp i a i' p b, + Gible.step_instr ge sp (Iexec i) a (Iexec i') -> + wf_trans p b -> + In a b -> + truthy (is_ps i) p -> + truthy (is_ps i') p. + Proof. + inversion 1; subst; auto; intros; + cbn [ is_ps ] in *. + inv H0; constructor; []. + apply H4 in H1. inv H2. + apply predicate_use_eval_predf; auto. + Qed. + + Lemma wf_trans_cons : + forall x a b', + wf_trans x (a :: b') -> + wf_trans x b'. + Proof. inversion 1; subst; cbn in *; constructor; eauto. Qed. Lemma map_truthy_step: - forall sp rs' m' pr' x b' i c, - truthy pr' x -> - SeqBB.step tge sp (Iexec (mki rs' pr' m')) b' (Iterm i c) -> - SeqBB.step tge sp (Iexec (mki rs' pr' m')) (map (map_if_convert x) b') (Iterm i c). + forall A B (ge: Genv.t A B) b' sp i x i' c, + truthy (is_ps i) x -> + wf_trans x b' -> + SeqBB.step tge sp (Iexec i) b' (Iterm i' c) -> + SeqBB.step tge sp (Iexec i) (map (map_if_convert x) b') (Iterm i' c). Proof. - intros * H1 H2. - Admitted. + induction b'; crush. + inv H1. + - econstructor. + apply map_truthy_instr; eauto. + eapply IHb'; auto. + eapply wf_trans_stays_truthy; eauto. constructor; auto. + apply wf_trans_cons with (a:=a); auto. + - constructor; apply map_truthy_instr; auto. + Qed. + + Lemma exec_if_conv : + forall A B ge sp x0 pc' b' tb i i' x x1, + step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') -> + wf_trans x b' -> + if_conv_replace pc' b' (x0 ++ RBexit x (RBgoto pc') :: x1) tb -> + exists b rb, + tb = b ++ (map (map_if_convert x) b') ++ rb + /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). + Proof. + induction x0; simplify. + - inv H1. inv H. exists nil. exists b'0. + split; [|constructor]. rewrite app_nil_l. + f_equal. simplify. apply wf_transition_block_opt_prop in H0. rewrite H0. + rewrite Pos.eqb_refl. auto. + - inv H1. inv H. + destruct i1; [|exfalso; eapply step_list2_false; eauto]. + exploit IHx0; eauto; simplify. + exists (if_convert_block pc' b' a ++ x2). exists x3. + split. rewrite app_assoc. auto. + eapply step_list2_app; eauto. + apply exec_if_conv3; auto. + Qed. Lemma match_none_correct : forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk', @@ -418,20 +639,21 @@ Section CORRECTNESS. do 3 econstructor. apply plus_one. econstructor; eauto. apply seqbb_eq; eauto. eauto. - simplify. - destruct (cf_dec cf pc'); subst. + exploit exec_rbexit_truthy; eauto; simplify. + destruct (cf_wf_dec x b' cf pc'); subst; simplify. + inv H1. - exploit exec_rbexit_truthy; eauto; simplify. exploit exec_if_conv; 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. + constructor; auto. + simplify. econstructor; eauto. + unfold sem_extrap; simplify. destruct out_s. exfalso; eapply step_list_false; eauto. apply append. exists (mki rs' pr' m'). split. eapply step_list_2_eq; eauto. apply append2. eapply map_truthy_step; eauto. econstructor; eauto. constructor; auto. - + exploit exec_rbexit_truthy; eauto; simplify. - exploit exec_if_conv2; eauto; simplify. + + exploit exec_if_conv2; eauto; simplify. exploit step_cf_eq; eauto; simplify. apply sim_plus. exists None. exists x4. split. apply plus_one. econstructor; eauto. @@ -449,13 +671,16 @@ Section CORRECTNESS. Forall2 match_stackframe s stk' -> (fn_code f) ! pc = Some b0 -> sem_extrap (transf_function f) pc1 sp (Iexec (mki rs pr m)) (Iexec (mki rs1 p0 m1)) b0 -> + (forall b', + f.(fn_code)!pc1 = Some b' -> + exists tb, (transf_function f).(fn_code)!pc1 = Some tb /\ if_conv_replace pc b0 b' tb) -> step ge (State s f sp pc1 rs1 p0 m1) E0 (State s f sp pc rs pr m) -> exists b' s2', (plus step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' \/ star step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' /\ ltof (option SeqBB.t) measure b' (Some b0)) /\ match_states b' s1' s2'. Proof. - intros * H H0 H1 H2 STK IS_B EXTRAP SIM. + intros * H H0 H1 H2 STK IS_B EXTRAP IS_TB SIM. rewrite IS_B in H0; simplify. exploit step_cf_eq; eauto; simplify. apply sim_plus. @@ -463,8 +688,10 @@ Section CORRECTNESS. split; auto. unfold sem_extrap in *. inv SIM. - pose proof (transf_spec_correct f pc1) as X. inv X. - eapply plus_two. econstructor; eauto. + pose proof (IS_TB _ H13); simplify. + apply plus_one. + econstructor; eauto. eapply EXTRAP; auto. eapply seqbb_eq; eauto. + Qed. Lemma transf_correct: forall s1 t s1', @@ -477,27 +704,19 @@ Section CORRECTNESS. Proof using TRANSL. inversion 1; subst; simplify; match goal with H: context[match_states] |- _ => inv H end. - - + - eauto using match_some_correct. - eauto using match_none_correct. - - 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 *) + - apply sim_plus. remember (transf_function f) as tf. symmetry in Heqtf. func_info. + exists None. eexists. split. + apply plus_one. constructor; eauto. rewrite <- H1. eassumption. + rewrite <- H4. rewrite <- H2. constructor; auto. + - apply sim_plus. exists None. eexists. split. + apply plus_one. constructor; eauto. + constructor; auto. + - apply sim_plus. remember (transf_function f) as tf. symmetry in Heqtf. func_info. + exists None. inv STK. inv H7. eexists. split. apply plus_one. constructor. + constructor; auto. + Qed. Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). |