Add list of bb to semantics

7 files changed, 99 insertions, 96 deletions

diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
index 643a3a7..3b82b29 100644
--- a/src/hls/RICtransf.v
+++ b/src/hls/RICtransf.v
@@ -58,7 +58,7 @@ Definition add_bb (should_split: bool) (i: list (list instr))
   | (a, b) => if should_split then (a, i::b) else (i::a, b)
   end.
 
-Fixpoint first_split (saw_pred: bool) (bb: bb) :=
+Fixpoint first_split (saw_pred: bool) (bb: list bb) :=
   match bb with
   | a :: b =>
       match includes_setpred a with
@@ -72,7 +72,7 @@ Fixpoint first_split (saw_pred: bool) (bb: bb) :=
   | nil => (None, (nil, nil))
   end.
 
-Definition split_bb (fresh: node) (b: bb) : bb * bb * bb :=
+Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb :=
   match first_split false b with
   | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
   | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 35ae03e..4631b5a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -113,28 +113,28 @@ Definition max_reg_instr (m: positive) (i: instr) :=
   match i with
   | RBnop => m
   | RBop p op args res =>
-    fold_left Pos.max args (Pos.max res m)
+      fold_left Pos.max args (Pos.max res m)
   | RBload p chunk addr args dst =>
-    fold_left Pos.max args (Pos.max dst m)
+      fold_left Pos.max args (Pos.max dst m)
   | RBstore p chunk addr args src =>
-    fold_left Pos.max args (Pos.max src m)
+      fold_left Pos.max args (Pos.max src m)
   | RBsetpred p' c args p =>
-    fold_left Pos.max args m
+      fold_left Pos.max args m
   end.
 
 Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   match i with
   | RBcall sig (inl r) args res s =>
-    fold_left Pos.max args (Pos.max r (Pos.max res m))
+      fold_left Pos.max args (Pos.max r (Pos.max res m))
   | RBcall sig (inr id) args res s =>
-    fold_left Pos.max args (Pos.max res m)
+      fold_left Pos.max args (Pos.max res m)
   | RBtailcall sig (inl r) args =>
-    fold_left Pos.max args (Pos.max r m)
+      fold_left Pos.max args (Pos.max r m)
   | RBtailcall sig (inr id) args =>
-    fold_left Pos.max args m
+      fold_left Pos.max args m
   | RBbuiltin ef args res s =>
       fold_left Pos.max (params_of_builtin_args args)
-        (fold_left Pos.max (params_of_builtin_res res) m)
+                (fold_left Pos.max (params_of_builtin_res res) m)
   | RBcond cond args ifso ifnot => fold_left Pos.max args m
   | RBjumptable arg tbl => Pos.max arg m
   | RBreturn None => m
@@ -150,7 +150,7 @@ 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.
+ Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
 Proof.
   unfold Proper. simplify. unfold "==>".
   intros.
@@ -177,8 +177,8 @@ 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.
+    [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 :=
@@ -200,10 +200,10 @@ Definition of the instruction state, which contains the following:
 |*)
 
 Record instr_state := mk_instr_state {
-  is_rs: regset;
-  is_ps: predset;
-  is_mem: mem;
-}.
+                         is_rs: regset;
+                         is_ps: predset;
+                         is_mem: mem;
+                       }.
 
 (*|
 Top-Level Type Definitions
@@ -215,19 +215,19 @@ Section DEFINITION.
   Context {bblock_body: Type}.
 
   Record bblock : Type := mk_bblock {
-    bb_body: list bblock_body;
-    bb_exit: cf_instr
-  }.
+                             bb_body: list bblock_body;
+                             bb_exit: cf_instr
+                           }.
 
   Definition code: Type := PTree.t bblock.
 
   Record function: Type := mkfunction {
-    fn_sig: signature;
-    fn_params: list reg;
-    fn_stacksize: Z;
-    fn_code: code;
-    fn_entrypoint: node
-  }.
+                              fn_sig: signature;
+                              fn_params: list reg;
+                              fn_stacksize: Z;
+                              fn_code: code;
+                              fn_entrypoint: node
+                            }.
 
   Definition fundef := AST.fundef function.
 
@@ -241,12 +241,12 @@ Section DEFINITION.
 
   Inductive stackframe : Type :=
   | Stackframe:
-      forall (res: reg)            (**r where to store the result *)
-             (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 *)
-             (pr: predset),        (**r predicate state of the calling
+    forall (res: reg)            (**r where to store the result *)
+           (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 *)
+           (pr: predset),        (**r predicate state of the calling
                                         function *)
       stackframe.
 
@@ -258,27 +258,28 @@ Definition of the ``state`` type, which is used by the ``step`` functions.
 |*)
 
   Variant state : Type :=
-  | State:
+    | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r current function *)
              (sp: val)                (**r stack pointer *)
              (pc: node)               (**r current program point in [c] *)
-             (il: list bblock_body)
+             (il: list bblock_body)   (**r basic block body that is
+                                           currently executing. *)
              (rs: regset)             (**r register state *)
              (pr: predset)            (**r predicate register state *)
              (m: mem),                (**r memory state *)
-      state
-  | Callstate:
+        state
+    | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
              (args: list val)         (**r arguments to the call *)
              (m: mem),                (**r memory state *)
-      state
-  | Returnstate:
+        state
+    | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
              (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
-      state.
+        state.
 
 End DEFINITION.
 
@@ -300,26 +301,26 @@ Section RELSEM.
     match ros with
     | inl r => Genv.find_funct ge rs#r
     | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
-      end
+        match Genv.find_symbol ge symb with
+        | None => None
+        | Some b => Genv.find_funct_ptr ge b
+        end
     end.
 
   Inductive eval_pred:
     option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
   | eval_pred_true:
-      forall i i' p,
+    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,
+    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.
+    forall i i', eval_pred None i i' i.
 
-(*|
+  (*|
 .. index::
    triple: semantics; RTLBlockInstr; instruction
 
@@ -329,39 +330,39 @@ Step Instruction
 
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
-      forall sp ist,
-        step_instr sp ist RBnop ist
+    forall sp ist,
+      step_instr sp ist RBnop ist
   | exec_RBop:
-      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
+    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 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
+    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 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
+    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,
+    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 ->
+                (mk_instr_state rs (pr#p <- b) m) ist ->
       step_instr sp (mk_instr_state rs pr m)
-                    (RBsetpred p' c args p) ist.
+                 (RBsetpred p' c args p) ist.
 
-(*|
+  (*|
 .. index::
    triple: semantics; RTLBlockInstr; control-flow instruction
 
@@ -375,44 +376,44 @@ Step Control-Flow Instruction
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       step_cf_instr (State s f sp pc nil rs pr m) (RBcall sig ros args res pc')
-           E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
+                    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 pr,
+    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 nil rs pr m)
                     (RBtailcall sig ros args)
-        E0 (Callstate s fd rs##args m')
+                    E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
-      forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
+    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 nil rs pr m) (RBbuiltin ef args res pc')
-         t (State s f sp pc' nil (regmap_setres res vres rs) pr m')
+                    t (State s f sp pc' nil (regmap_setres res vres rs) pr m')
   | exec_RBcond:
-      forall s f sp rs m cond args ifso ifnot b pc pc' pr,
+    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 nil rs pr m) (RBcond cond args ifso ifnot)
-        E0 (State s f sp pc' nil rs pr m)
+                    E0 (State s f sp pc' nil rs pr m)
   | exec_RBjumptable:
-      forall s f sp rs m arg tbl n pc pc' pr,
+    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 nil rs pr m) (RBjumptable arg tbl)
-        E0 (State s f sp pc' nil rs pr m)
+                    E0 (State s f sp pc' nil rs pr m)
   | exec_RBreturn:
-      forall s f stk rs m or pc m' pr,
+    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 nil rs pr m) (RBreturn or)
-        E0 (Returnstate s (regmap_optget or Vundef rs) m')
+                    E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_RBgoto:
-      forall s f sp pc rs pr m pc',
+    forall s f sp pc rs pr m pc',
       step_cf_instr (State s f sp pc nil rs pr m) (RBgoto pc') E0
                     (State s f sp pc' nil rs pr m)
   | exec_RBpred_cf:
-      forall s f sp pc rs pr m cf1 cf2 st' p t,
+    forall s f sp pc rs pr m cf1 cf2 st' p t,
       step_cf_instr (State s f sp pc nil rs pr m)
                     (if eval_predf pr p then cf1 else cf2) t st' ->
       step_cf_instr (State s f sp pc nil rs pr m)
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index 42d471c..f870278 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -117,7 +117,7 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
          (PC: find_block_spec tf.(fn_code) pc pc')
          (STK: Forall2 match_stackframe stk stk'),
     match_states (RTL.State stk f sp pc rs m)
-                 (State stk' tf sp pc' rs ps m).
+                 (State stk' tf sp pc' nil rs ps m).
 
 Definition match_prog (p: RTL.program) (tp: RTLBlock.program) :=
   Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
@@ -165,5 +165,6 @@ Section CORRECTNESS.
     apply senv_preserved.
     admit.
     eauto using transl_final_states.
+    Admitted.
 
 End CORRECTNESS.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index a36177e..7ae563d 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -69,7 +69,7 @@ Section RELSEM.
       step_instr_seq sp state nil state.
 
   Inductive step_instr_block (sp : val)
-    : instr_state -> bb -> instr_state -> Prop :=
+    : instr_state -> list bb -> instr_state -> Prop :=
   | exec_instr_block_cons:
     forall state i state' state'' instrs,
       step_instr_seq sp state i state' ->
@@ -81,12 +81,12 @@ Section RELSEM.
 
   Inductive step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s f sp pc rs rs' m m' t s' bb pr pr',
+    forall s (f: function) sp pc rs rs' m m' t s' bb pr pr',
       f.(fn_code)!pc = Some bb ->
       step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body)
                           (mk_instr_state rs' pr' m') ->
-      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
-      step (State s f sp pc rs pr m) t s'
+      step_cf_instr ge (State s f sp pc nil rs' pr' m') bb.(bb_exit) t s' ->
+      step (State s f sp pc nil rs pr m) t s'
   | exec_function_internal:
     forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -95,6 +95,7 @@ Section RELSEM.
                   f
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
+                  nil
                   (init_regs args f.(fn_params))
                   (PMap.init false)
                   m')
@@ -106,7 +107,7 @@ Section RELSEM.
   | exec_return:
     forall res f sp pc rs s vres m pr,
       step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
-        E0 (State s f sp pc (rs#res <- vres) pr m).
+        E0 (State s f sp pc nil (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 49ee6e7..a104056 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr))
   | None => ((cycle + 1)%positive, curr :: bb)
   end.
 
-Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body :=
+Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body :=
   do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb;
   let (li, tr) := litr in
   OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)).
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index d425049..214da6f 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -227,7 +227,7 @@ We define the top-level oracle that will check if two basic blocks are
 equivalent after a scheduling transformation.
 |*)
 
-Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
+Definition empty_trees (bb: list RTLBlock.bb) (bbt: list RTLPar.bb) : bool :=
   match bb with
   | nil =>
     match bbt with
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 4e88b13..215aef5 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -812,8 +812,8 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
       (STACKS: list_forall2 match_stackframes sf sf')
       (REG: forall x, rs !! x = rs' !! x)
       (REG: forall x, ps !! x = ps' !! x),
-      match_states (State sf f sp pc rs ps m)
-                   (State sf' tf sp pc rs' ps' m)
+      match_states (State sf f sp pc nil rs ps m)
+                   (State sf' tf sp pc nil rs' ps' m)
 | match_returnstate:
     forall stack stack' v m
       (STACKS: list_forall2 match_stackframes stack stack'),