From 4bfef56fc99c648371af2418d12c8e6dacd24093 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 May 2022 02:03:58 +0100 Subject: Add new translation passes for if-conversion --- src/hls/CondElim.v | 71 +++++++++++++++++++ src/hls/CondElimproof.v | 179 ++++++++++++++++++++++++++++++++++++++++++++++++ src/hls/DeadBlocks.v | 87 +++++++++++++++++++++++ 3 files changed, 337 insertions(+) create mode 100644 src/hls/CondElim.v create mode 100644 src/hls/CondElimproof.v create mode 100644 src/hls/DeadBlocks.v diff --git a/src/hls/CondElim.v b/src/hls/CondElim.v new file mode 100644 index 0000000..b9bd1e9 --- /dev/null +++ b/src/hls/CondElim.v @@ -0,0 +1,71 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2022 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.Predicate. +Require Import vericert.bourdoncle.Bourdoncle. + +Definition elim_cond_s (fresh: predicate) (i: instr) := + match i with + | RBexit p (RBcond c args n1 n2) => + (Pos.succ fresh, + RBsetpred p c args fresh + :: RBexit (combine_pred (Some (Plit (true, fresh))) p) (RBgoto n1) + :: RBexit (combine_pred (Some (Plit (false, fresh))) p) (RBgoto n2) + :: nil) + | _ => (fresh, i :: nil) + end. + +(* Fixpoint elim_cond (fresh: predicate) (b: SeqBB.t) := *) +(* match b with *) +(* | RBexit p (RBcond c args n1 n2) :: b' => *) +(* let (fresh', b'') := elim_cond fresh b' in *) +(* (Pos.succ fresh', *) +(* RBsetpred p c args fresh' *) +(* :: RBexit (combine_pred (Some (Plit (true, fresh'))) p) (RBgoto n1) *) +(* :: RBexit (combine_pred (Some (Plit (false, fresh'))) p) (RBgoto n1) *) +(* :: b'') *) +(* | i :: b' => *) +(* let (fresh, b'') := elim_cond fresh b' in *) +(* (fresh, i :: b'') *) +(* | nil => (fresh, nil) *) +(* end. *) + +Definition elim_cond_fold (state: predicate * PTree.t SeqBB.t) (n: node) (b: SeqBB.t) := + let (p, ptree) := state in + let (p', b') := replace_section elim_cond_s p b in + (p', PTree.set n b' ptree). + +Definition transf_function (f: function) : function := + mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) + (snd (PTree.fold elim_cond_fold f.(fn_code) (1%positive, PTree.empty _))) + f.(fn_entrypoint). + +Definition transf_fundef (fd: fundef) : fundef := + transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v new file mode 100644 index 0000000..f16a710 --- /dev/null +++ b/src/hls/CondElimproof.v @@ -0,0 +1,179 @@ +(*| +.. + Vericert: Verified high-level synthesis. + Copyright (C) 2022 Yann Herklotz + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +================ +RTLBlockgenproof +================ + +.. coq:: none +|*) + +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Maps. +Require Import compcert.backend.Registers. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Events. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. + +Require Import vericert.common.Vericertlib. +Require Import vericert.common.DecEq. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.CondElim. + +#[local] Open Scope positive. + +Lemma cf_in_step : + forall A B ge sp is_ is_' bb cf, + @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) -> + exists p, In (RBexit p cf) bb + /\ Option.default true (Option.map (eval_predf (is_ps is_')) p) = true. + Proof. Admitted. + +Lemma forbidden_term_trans : + forall A B ge sp i c b i' c', + ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c'). +Proof. induction b; unfold not; intros; inv H. Qed. + +Lemma random1 : + forall A B ge sp is_ b is_' cf, + @SeqBB.step A B ge sp (Iexec is_) b (Iterm is_' cf) -> + exists p b', SeqBB.step ge sp (Iexec is_) (b' ++ (RBexit p cf) :: nil) (Iterm is_' cf) + /\ Forall2 eq (b' ++ (RBexit p cf) :: nil) b. +Proof. +Admitted. + +Lemma replace_section_spec : + forall A B ge sp is_ is_' bb cf, + @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) -> + exists p, + @SeqBB.step A B ge sp (Iexec is_) + (snd (replace_section elim_cond_s p bb)) + (Iterm is_' cf). Admitted. + +Lemma transf_block_spec : + forall f pc b, + f.(fn_code) ! pc = Some b -> + exists p, + (transf_function f).(fn_code) ! pc + = Some (snd (replace_section elim_cond_s p b)). Admitted. + +Variant match_stackframe : stackframe -> stackframe -> Prop := + | match_stackframe_init : + forall res f tf sp pc rs p p' + (TF: transf_function f = tf), + match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p'). + +Variant match_states : state -> state -> Prop := + | match_state : + forall stk stk' f tf sp pc rs p p0 m + (TF: transf_function f = tf) + (STK: Forall2 match_stackframe stk stk'), + match_states (State stk f sp pc rs p m) (State stk' tf sp pc rs p0 m) + | match_callstate : + forall cs cs' f tf args m + (TF: transf_fundef f = tf) + (STK: Forall2 match_stackframe cs cs'), + match_states (Callstate cs f args m) (Callstate cs' tf args m) + | match_returnstate : + forall cs cs' v m + (STK: Forall2 match_stackframe cs cs'), + match_states (Returnstate cs v m) (Returnstate cs' v m) +. + +Definition match_prog (p: program) (tp: program) := + Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Section CORRECTNESS. + + Context (prog tprog : program). + + Let ge : genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + + Context (TRANSL : match_prog prog tprog). + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof using TRANSL. intros; eapply (Genv.senv_transf TRANSL). Qed. + + Lemma function_ptr_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). + Proof (Genv.find_funct_ptr_transf TRANSL). + + Lemma sig_transf_function: + forall (f tf: fundef), + funsig (transf_fundef f) = funsig f. + Proof using. + unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f. + unfold transf_function. auto. auto. + Qed. + + Lemma transf_initial_states : + forall s1, + initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. + Proof using TRANSL. + induction 1. + exploit function_ptr_translated; eauto; intros. + do 2 econstructor; simplify. econstructor. + apply (Genv.init_mem_transf TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. eauto. + erewrite sig_transf_function; eauto. constructor. auto. auto. + Qed. + + Lemma transf_final_states : + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. + Proof using. + inversion 2; crush. subst. inv H. inv STK. econstructor. + Qed. + + Lemma transf_step_correct: + forall (s1 : state) (t : trace) (s1' : state), + 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. + induction 1; intros. + + inv H2. eapply cf_in_step in H0; simplify. + do 2 econstructor. econstructor; eauto. admit. Admitted. + + 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. + Qed. + + +End CORRECTNESS. diff --git a/src/hls/DeadBlocks.v b/src/hls/DeadBlocks.v new file mode 100644 index 0000000..644ed1f --- /dev/null +++ b/src/hls/DeadBlocks.v @@ -0,0 +1,87 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2022 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.Predicate. + +Local Open Scope error_monad_scope. + +Definition not_seen_sons (code:code) (pc : node) (seen: PTree.t unit) : (list positive) * PTree.t unit := + match code ! pc with + | None => (nil, seen) + | Some i => + List.fold_left (fun (ns:(list node) * PTree.t unit) j => + let (new,seen) := ns in + match PTree.get j seen with + | None => (j::new, PTree.set j tt seen) + | Some _ => ns + end) + (all_successors i) + (nil, seen) + end. + +Definition remove_dead (i:option SeqBB.t) (b:option unit) : option SeqBB.t := + match b with + | Some _ => i + | None => None + end. + +Fixpoint acc_succ (c:code) (workl: list node) + (acc: res (PTree.t unit * (list positive) * (list positive))) + : res ((list positive) * code) := + do acc <- acc; + let '(seen_set,seen_list,stack) := acc in + match stack with + | nil => OK (seen_list, PTree.combine remove_dead c seen_set) + | x::q => + match workl with + | nil => Error (msg "workl too small") + | pc::m => + let seen_set' := PTree.set x tt seen_set in + let (new,seen_set) := not_seen_sons c x seen_set' in + acc_succ c m (OK (seen_set,x::seen_list,new++q)) + end + end. + +Definition dfs (tf: function) : res (list node * code) := + do (res, code') <- + (acc_succ + (fn_code tf) + (map (@fst node SeqBB.t) (PTree.elements (fn_code tf))) + (OK (PTree.empty _,nil,(fn_entrypoint tf)::nil))) ; + OK (rev_append res nil, code'). + +Definition transf_function (f: function) : res function := + do (seen,code) <- dfs f ; + OK (mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) + code + f.(fn_entrypoint)). + +Definition transf_fundef (fd: fundef) : res fundef := + transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. -- cgit