From e72ef9094c1d8239e56c4da126bb3f05341702a2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 28 Jun 2022 18:26:23 +0100 Subject: Add if-conversion spec --- src/hls/IfConversion.v | 9 ++-- src/hls/IfConversionproof.v | 104 +++++++++++++++++++++++++++++++++++++------- 2 files changed, 92 insertions(+), 21 deletions(-) (limited to 'src') diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 53ca944..aec9df2 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -200,16 +200,13 @@ 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 transf_function' (f: function) (n: node * node) : function := - mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) - (if_convert f.(fn_code) (fst n) (snd n)) - f.(fn_entrypoint). - 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 - fold_left transf_function' iflist f. + 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)) + f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index c303da9..addc223 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -54,6 +54,27 @@ Variant match_stackframe : stackframe -> stackframe -> Prop := Definition bool_order (b: bool): nat := if b then 1 else 0. +Inductive if_conv_block_spec (c: code): SeqBB.t -> SeqBB.t -> Prop := +| if_conv_block_intro : + if_conv_block_spec c nil nil +| if_conv_block_eq : + forall a b tb, + if_conv_block_spec c b tb -> + if_conv_block_spec c (a::b) (a::tb) +| if_conv_block_conv : + forall b tb ta p pc' b', + if_conv_block_spec c b tb -> + c ! pc' = Some b' -> + 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. + Section CORRECTNESS. Context (prog tprog : program). @@ -73,7 +94,9 @@ Section CORRECTNESS. (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)), + (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), match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0) | match_callstate : forall cs cs' f tf args m @@ -143,7 +166,7 @@ Section CORRECTNESS. Lemma transf_initial_states : forall s1, initial_state prog s1 -> - exists s2, initial_state tprog s2 /\ match_states s1 s2. + exists s2, initial_state tprog s2 /\ match_states None s1 s2. Proof using TRANSL. induction 1. exploit function_ptr_translated; eauto; intros. @@ -155,8 +178,8 @@ Section CORRECTNESS. Qed. Lemma transf_final_states : - forall s1 s2 r, - match_states s1 s2 -> final_state s1 r -> final_state s2 r. + forall s1 s2 r b, + match_states b s1 s2 -> final_state s1 r -> final_state s2 r. Proof using. inversion 2; crush. subst. inv H. inv STK. econstructor. Qed. @@ -189,22 +212,73 @@ Section CORRECTNESS. #[local] Hint Resolve find_function_translated : core. #[local] Hint Resolve sig_transf_function : core. - Lemma transf_step_correct: - forall (s1 : state) (t : trace) (s1' : state), + Definition measure (b: option SeqBB.t): nat := + match b with + | None => 0 + | Some b' => 1 + length b' + 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_matches : + forall b s cf t s' ts, + step_cf_instr ge s cf t s' -> + match_states b s ts -> + exists b' ts', step_cf_instr tge ts cf t ts' /\ match_states b' s' ts'. + Proof. Admitted. + + Lemma transf_correct: + forall s1 t s1', step ge s1 t s1' -> - forall s2 : state, - match_states s1 s2 -> - exists s2' : state, step tge s2 t s2' /\ match_states s1' s2'. - Proof using TRANSL. Admitted. + forall b s2, match_states b s1 s2 -> + exists b' s2', + (plus step tge s2 t s2' \/ + (star step tge s2 t s2' /\ ltof _ measure b' b)) + /\ match_states b' s1' s2'. + 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 Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof using TRANSL. - eapply forward_simulation_step. - + apply senv_preserved. - + apply transf_initial_states. - + apply transf_final_states. - + apply transf_step_correct. + eapply (Forward_simulation + (L1:=semantics prog) + (L2:=semantics tprog) + (ltof _ measure) match_states). + constructor. + - apply well_founded_ltof. + - eauto using transf_initial_states. + - intros; eapply transf_final_states; eauto. + - eapply transf_correct. + - apply senv_preserved. Qed. End CORRECTNESS. -- cgit