1 files changed, 154 insertions, 264 deletions

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 69cc709..d9f3e74 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -28,232 +28,42 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.Sat.
-Require Import vericert.hls.FunctionalUnits.
+Require Import Predicate.
+Require Import Vericertlib.
 
-Local Open Scope rtl.
+(*|
+=====================
+RTLBlock Instructions
+=====================
 
-Definition node := positive.
-Definition predicate := nat.
-
-Inductive pred_op : Type :=
-| Pvar: predicate -> pred_op
-| Pnot: pred_op -> pred_op
-| Pand: pred_op -> pred_op -> pred_op
-| Por: pred_op -> pred_op -> pred_op.
-
-Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
-  match p with
-  | Pvar p' => a p'
-  | Pnot p' => negb (sat_predicate p' a)
-  | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a
-  | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a
-  end.
-
-Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=
-  match a with
-  | nil => nil
-  | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b)
-  end.
-
-Lemma satFormula_concat:
-  forall a b agn,
-  satFormula a agn ->
-  satFormula b agn ->
-  satFormula (a ++ b) agn.
-Proof. induction a; crush. Qed.
-
-Lemma satFormula_concat2:
-  forall a b agn,
-  satFormula (a ++ b) agn ->
-  satFormula a agn /\ satFormula b agn.
-Proof.
-  induction a; simplify;
-    try apply IHa in H1; crush.
-Qed.
-
-Lemma satClause_concat:
-  forall a a1 a0,
-  satClause a a1 ->
-  satClause (a0 ++ a) a1.
-Proof. induction a0; crush. Qed.
-
-Lemma satClause_concat2:
-  forall a a1 a0,
-  satClause a0 a1 ->
-  satClause (a0 ++ a) a1.
-Proof.
-  induction a0; crush.
-  inv H; crush.
-Qed.
-
-Lemma satClause_concat3:
-  forall a b c,
-  satClause (a ++ b) c ->
-  satClause a c \/ satClause b c.
-Proof.
-  induction a; crush.
-  inv H; crush.
-  apply IHa in H0; crush.
-  inv H0; crush.
-Qed.
-
-Lemma satFormula_mult':
-  forall p2 a a0,
-  satFormula p2 a0 \/ satClause a a0 ->
-  satFormula (map (fun x : list lit => a ++ x) p2) a0.
-Proof.
-  induction p2; crush.
-  - inv H. inv H0. apply satClause_concat. auto.
-    apply satClause_concat2; auto.
-  - apply IHp2.
-    inv H; crush; inv H0; crush.
-Qed.
-
-Lemma satFormula_mult2':
-  forall p2 a a0,
-  satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
-  satClause a a0 \/ satFormula p2 a0.
-Proof.
-  induction p2; crush.
-  apply IHp2 in H1. inv H1; crush.
-  apply satClause_concat3 in H0.
-  inv H0; crush.
-Qed.
-
-Lemma satFormula_mult:
-  forall p1 p2 a,
-  satFormula p1 a \/ satFormula p2 a ->
-  satFormula (mult p1 p2) a.
-Proof.
-  induction p1; crush.
-  apply satFormula_concat; crush.
-  inv H. inv H0.
-  apply IHp1. auto.
-  apply IHp1. auto.
-  apply satFormula_mult';
-  inv H; crush.
-Qed.
-
-Lemma satFormula_mult2:
-  forall p1 p2 a,
-  satFormula (mult p1 p2) a ->
-  satFormula p1 a \/ satFormula p2 a.
-Proof.
-  induction p1; crush.
-  apply satFormula_concat2 in H; crush.
-  apply IHp1 in H0.
-  inv H0; crush.
-  apply satFormula_mult2' in H1. inv H1; crush.
-Qed.
-
-Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula :=
-  match bound with
-  | O => None
-  | S n =>
-    match p with
-    | Pvar p' => Some (((true, p') :: nil) :: nil)
-    | Pand p1 p2 =>
-      match trans_pred_temp n p1, trans_pred_temp n p2 with
-      | Some p1', Some p2' =>
-        Some (p1' ++ p2')
-      | _, _ => None
-      end
-    | Por p1 p2 =>
-      match trans_pred_temp n p1, trans_pred_temp n p2 with
-      | Some p1', Some p2' =>
-        Some (mult p1' p2')
-      | _, _ => None
-      end
-    | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil)
-    | Pnot (Pnot p) => trans_pred_temp n p
-    | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2))
-    | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2))
-    end
-  end.
+These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have consistent
+instructions, which greatly simplifies the proofs, as they will by default have the same instruction
+syntax and semantics.  The only changes are therefore at the top-level of the instructions.
 
-Fixpoint trans_pred (bound: nat) (p: pred_op) :
-  option {fm: formula | forall a,
-           sat_predicate p a = true <-> satFormula fm a}.
-  refine
-  (match bound with
-   | O => None
-   | S n =>
-     match p with
-     | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
-     | Pand p1 p2 =>
-      match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
-        Some (exist _ (p1' ++ p2') _)
-      | _, _ => None
-      end
-     | Por p1 p2 =>
-      match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
-        Some (exist _ (mult p1' p2') _)
-      | _, _ => None
-      end
-     | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
-     | _ => None
-     end
-   end); split; intros; simpl in *; auto.
-  - inv H. inv H0; auto.
-  - admit.
-  - admit.
-  - apply satFormula_concat.
-    apply andb_prop in H. inv H. apply i in H0. auto.
-    apply andb_prop in H. inv H. apply i0 in H1. auto.
-  - apply satFormula_concat2 in H. simplify. apply andb_true_intro.
-    split. apply i in H0. auto.
-    apply i0 in H1. auto.
-  - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto.
-    apply i0 in H0. auto.
-  - apply orb_true_intro.
-    apply satFormula_mult2 in H. inv H. apply i in H0. auto.
-    apply i0 in H0. auto.
-Admitted.
-
-Definition sat_pred (bound: nat) (p: pred_op) :
-  option ({al : alist | sat_predicate p (interp_alist al) = true}
-          + {forall a : asgn, sat_predicate p a = false}).
-  refine
-  ( match trans_pred bound p with
-    | Some (exist fm _) =>
-      match boundedSat bound fm with
-      | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
-      | Some (inright _) => Some (inright _)
-      | None => None
-      end
-    | None => None
-    end ).
-  - apply i in s2. auto.
-  - intros. specialize (n a). specialize (i a).
-    destruct (sat_predicate p a). exfalso.
-    apply n. apply i. auto. auto.
-Qed.
+Instruction Definition
+======================
 
-Definition sat_pred_simple (bound: nat) (p: pred_op) :=
-  match sat_pred bound p with
-  | Some (inleft (exist al _)) => Some (Some al)
-  | Some (inright _) => Some None
-  | None => None
-  end.
+First, we define the instructions that can be placed into a basic block, meaning they won't branch.
+The main changes to how instructions are defined in ``RTL``, is that these instructions don't have a
+next node, as they will be in a basic block, and they also have an optional predicate (``pred_op``).
+|*)
 
-Definition sat_pred_temp (bound: nat) (p: pred_op) :=
-  match trans_pred_temp bound p with
-  | Some fm => boundedSatSimple bound fm
-  | None => None
-  end.
+Definition node := positive.
 
 Inductive instr : Type :=
 | RBnop : instr
 | RBop : option pred_op -> operation -> list reg -> reg -> instr
 | RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
 | RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBpiped : option pred_op -> funct_node -> list reg -> instr
-| RBassign : option pred_op -> funct_node -> reg -> reg -> instr
-| RBsetpred : condition -> list reg -> predicate -> instr.
+| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
+
+(*|
+Control-Flow Instruction Definition
+===================================
+
+These are the instructions that count as control-flow, and will be placed at the end of the basic
+blocks.
+|*)
 
 Inductive cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
@@ -266,6 +76,11 @@ Inductive cf_instr : Type :=
 | RBgoto : node -> cf_instr
 | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
 
+(*|
+Helper functions
+================
+|*)
+
 Fixpoint successors_instr (i : cf_instr) : list node :=
   match i with
   | RBcall sig ros args res s => s :: nil
@@ -287,11 +102,7 @@ Definition max_reg_instr (m: positive) (i: instr) :=
     fold_left Pos.max args (Pos.max dst m)
   | RBstore p chunk addr args src =>
     fold_left Pos.max args (Pos.max src m)
-  | RBpiped p f args =>
-    fold_left Pos.max args m
-  | RBassign p f src dst =>
-    Pos.max src (Pos.max dst m)
-  | RBsetpred c args p =>
+  | RBsetpred p' c args p =>
     fold_left Pos.max args m
   end.
 
@@ -317,6 +128,41 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   end.
 
 Definition regset := Regmap.t val.
+Definition predset := PMap.t bool.
+
+Definition eval_predf (pr: predset) (p: pred_op) :=
+  sat_predicate p (fun x => pr !! (Pos.of_nat x)).
+
+#[global]
+Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
+Proof.
+  unfold Proper. simplify. unfold "==>".
+  intros.
+  unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0.
+Qed.
+
+#[local] Open Scope pred_op.
+
+Lemma eval_predf_Pand :
+  forall ps p p',
+    eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_Por :
+  forall ps p p',
+    eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_pr_equiv :
+  forall p ps ps',
+    (forall x, ps !! x = ps' !! x) ->
+    eval_predf ps p = eval_predf ps' p.
+Proof.
+  induction p; simplify; auto;
+    try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+  [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
+  erewrite IHp1; try eassumption; erewrite IHp2; eauto.
+Qed.
 
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   match rl, vl with
@@ -324,11 +170,28 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | _, _ => Regmap.init Vundef
   end.
 
-Inductive instr_state : Type :=
-| InstrState:
-    forall (rs: regset)
-           (m: mem),
-    instr_state.
+(*|
+Instruction State
+-----------------
+
+Definition of the instruction state, which contains the following:
+
+:is_rs: This is the current state of the registers.
+:is_ps: This is the current state of the predicate registers, which is in a separate namespace and
+        area compared to the standard registers in ``is_rs``.
+:is_mem: The current state of the memory.
+|*)
+
+Record instr_state := mk_instr_state {
+  is_rs: regset;
+  is_ps: predset;
+  is_mem: mem;
+}.
+
+(*|
+Top-Level Type Definitions
+==========================
+|*)
 
 Section DEFINITION.
 
@@ -346,7 +209,6 @@ Section DEFINITION.
     fn_params: list reg;
     fn_stacksize: Z;
     fn_code: code;
-    fn_funct_units: funct_units;
     fn_entrypoint: node
   }.
 
@@ -366,7 +228,8 @@ Section DEFINITION.
              (f: function)         (**r calling function *)
              (sp: val)             (**r stack pointer in calling function *)
              (pc: node)            (**r program point in calling function *)
-             (rs: regset),         (**r register state in calling function *)
+             (rs: regset)          (**r register state in calling function *)
+             (pr: predset),        (**r predicate state of the calling function *)
       stackframe.
 
   Inductive state : Type :=
@@ -376,6 +239,7 @@ Section DEFINITION.
              (sp: val)                (**r stack pointer *)
              (pc: node)               (**r current program point in [c] *)
              (rs: regset)             (**r register state *)
+             (pr: predset)            (**r predicate register state *)
              (m: mem),                (**r memory state *)
       state
   | Callstate:
@@ -392,6 +256,11 @@ Section DEFINITION.
 
 End DEFINITION.
 
+(*|
+Semantics
+=========
+|*)
+
 Section RELSEM.
 
   Context {bblock_body : Type}.
@@ -411,67 +280,88 @@ Section RELSEM.
       end
     end.
 
+  Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+  | eval_pred_true:
+      forall i i' p,
+      eval_predf (is_ps i) p = true ->
+      eval_pred (Some p) i i' i'
+  | eval_pred_false:
+      forall i i' p,
+      eval_predf (is_ps i) p = false ->
+      eval_pred (Some p) i i' i
+  | eval_pred_none:
+      forall i i', eval_pred None i i' i.
+
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
-      forall rs m sp,
-      step_instr sp (InstrState rs m) RBnop (InstrState rs m)
+      forall sp ist,
+        step_instr sp ist RBnop ist
   | exec_RBop:
-      forall op v res args rs m sp p,
-      eval_operation ge sp op rs##args m = Some v ->
-      step_instr sp (InstrState rs m)
-                 (RBop p op args res)
-                 (InstrState (rs#res <- v) m)
+      forall op v res args rs m sp p ist pr,
+        eval_operation ge sp op rs##args m = Some v ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
   | exec_RBload:
-      forall addr rs args a chunk m v dst sp p,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      step_instr sp (InstrState rs m)
-                 (RBload p chunk addr args dst)
-                 (InstrState (rs#dst <- v) m)
+      forall addr rs args a chunk m v dst sp p pr ist,
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.loadv chunk m a = Some v ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist
   | exec_RBstore:
-      forall addr rs args a chunk m src m' sp p,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      step_instr sp (InstrState rs m)
-                 (RBstore p chunk addr args src)
-                 (InstrState rs m').
+      forall addr rs args a chunk m src m' sp p pr ist,
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.storev chunk m a rs#src = Some m' ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist
+  | exec_RBsetpred:
+      forall sp rs pr m p c b args p' ist,
+      Op.eval_condition c rs##args m = Some b ->
+      eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
+      step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
 
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
-    forall s f sp rs m res fd ros sig args pc pc',
+    forall s f sp rs m res fd ros sig args pc pc' pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      step_cf_instr (State s f sp pc rs m) (RBcall sig ros args res pc')
-           E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
+      step_cf_instr (State s f sp pc rs pr m) (RBcall sig ros args res pc')
+           E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
   | exec_RBtailcall:
-      forall s f stk rs m sig ros args fd m' pc,
+      forall s f stk rs m sig ros args fd m' pc pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBtailcall sig ros args)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args)
         E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
-      forall s f sp rs m ef args res pc' vargs t vres m' pc,
+      forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      step_cf_instr (State s f sp pc rs m) (RBbuiltin ef args res pc')
-         t (State s f sp pc' (regmap_setres res vres rs) m')
+      step_cf_instr (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
+         t (State s f sp pc' (regmap_setres res vres rs) pr m')
   | exec_RBcond:
-      forall s f sp rs m cond args ifso ifnot b pc pc',
+      forall s f sp rs m cond args ifso ifnot b pc pc' pr,
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
-      step_cf_instr (State s f sp pc rs m) (RBcond cond args ifso ifnot)
-        E0 (State s f sp pc' rs m)
+      step_cf_instr (State s f sp pc rs pr m) (RBcond cond args ifso ifnot)
+        E0 (State s f sp pc' rs pr m)
   | exec_RBjumptable:
-      forall s f sp rs m arg tbl n pc pc',
+      forall s f sp rs m arg tbl n pc pc' pr,
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      step_cf_instr (State s f sp pc rs m) (RBjumptable arg tbl)
-        E0 (State s f sp pc' rs m)
-  | exec_Ireturn:
-      forall s f stk rs m or pc m',
+      step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl)
+        E0 (State s f sp pc' rs pr m)
+  | exec_RBreturn:
+      forall s f stk rs m or pc m' pr,
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBreturn or)
-        E0 (Returnstate s (regmap_optget or Vundef rs) m').
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
+  | exec_RBgoto:
+      forall s f sp pc rs pr m pc',
+      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m)
+  | exec_RBpred_cf:
+      forall s f sp pc rs pr m cf1 cf2 st' p t,
+      step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
+      step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'.
 
 End RELSEM.