Add new translation passes for if-conversion

3 files changed, 337 insertions, 0 deletions

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 <yann@yannherklotz.com>
+ *
+ * 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 <https://www.gnu.org/licenses/>.
+ *)
+
+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 <yann@yannherklotz.com>
+
+   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 <https://www.gnu.org/licenses/>.
+
+================
+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 <yann@yannherklotz.com>
+ *
+ * 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 <https://www.gnu.org/licenses/>.
+ *)
+
+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.