Fix RTLPar to use instr list list list

3 files changed, 33 insertions, 25 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index fcd4441..9213514 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -39,6 +39,8 @@ Hint Resolve AssocMap.gss : htlh.
 Hint Resolve Ple_refl : htlh.
 Hint Resolve Ple_succ : htlh.
 
+Definition assignment : Type := expr -> expr -> stmnt.
+
 Record state: Type := mkstate {
   st_st: reg;
   st_freshreg: reg;
@@ -666,35 +668,33 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) :=
     Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
   end.
 
-Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) :=
+Definition translate_predicate (a : assignment)
+           (preg: reg) (p: option pred_op) (dst e: expr) :=
   match p with
-  | None => ret (Vnonblock dst e)
+  | None => ret (a dst e)
   | Some pos =>
-    ret (Vnonblock dst (Vternary (pred_expr preg pos) e dst))
+    ret (a dst (Vternary (pred_expr preg pos) e dst))
   end.
 
-Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr)
-  : mon unit :=
+Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
+  : mon stmnt :=
   match i with
   | RBnop =>
-    add_data_instr n Vskip
+    ret Vskip
   | RBop p op args dst =>
     do instr <- translate_instr op args;
     do _ <- declare_reg None dst 32;
-    do pred <- translate_predicate preg p (Vvar dst) instr;
-    add_data_instr n pred
+    translate_predicate a preg p (Vvar dst) instr
   | RBload p chunk addr args dst =>
     do src <- translate_arr_access chunk addr args stack;
     do _ <- declare_reg None dst 32;
-    do pred <- translate_predicate preg p (Vvar dst) src;
-    add_data_instr n pred
+    translate_predicate a preg p (Vvar dst) src
   | RBstore p chunk addr args src =>
     do dst <- translate_arr_access chunk addr args stack;
-    do pred <- translate_predicate preg p dst (Vvar src);
-    add_data_instr n pred
+    translate_predicate a preg p dst (Vvar src)
   | RBsetpred c args p =>
     do cond <- translate_condition c args;
-    add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond)
+    ret (a (pred_expr preg (Pvar p)) cond)
   end.
 
 Lemma create_new_state_state_incr:
@@ -722,10 +722,13 @@ Definition create_new_state (p: node): mon node :=
                 s.(st_controllogic))
               (create_new_state_state_incr s p).
 
-Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list instr) :=
+Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) :=
   match ni with
   | (n, p, li) =>
-    do _ <- collectlist (translate_inst fin rtrn stack preg n) li;
+    do _ <- collectlist
+          (fun l =>
+             do stmnt <- translate_inst Vblock fin rtrn stack preg n l;
+             add_data_instr n stmnt) (concat li);
     do st <- get;
     add_control_instr n (state_goto st.(st_st) p)
   end.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index be9ff22..2e78d36 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -30,7 +30,7 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.RTLBlockInstr.
 
-Definition bb := list (list instr).
+Definition bb := list (list (list instr)).
 
 Definition bblock := @bblock bb.
 Definition code := @code bb.
@@ -56,11 +56,22 @@ Section RELSEM.
         forall state sp,
         step_instr_list sp state nil state.
 
+  Inductive step_instr_seq (sp : val)
+    : instr_state -> list (list instr) -> instr_state -> Prop :=
+  | exec_instr_seq_cons:
+    forall state i state' state'' instrs,
+      step_instr_list sp state i state' ->
+      step_instr_seq sp state' instrs state'' ->
+      step_instr_seq sp state (i :: instrs) state''
+  | exec_instr_seq_nil:
+    forall state,
+      step_instr_seq sp state nil state.
+
   Inductive step_instr_block (sp : val)
     : instr_state -> bb -> instr_state -> Prop :=
   | exec_instr_block_cons:
     forall state i state' state'' instrs,
-      step_instr_list sp state i state' ->
+      step_instr_seq sp state i state' ->
       step_instr_block sp state' instrs state'' ->
       step_instr_block sp state (i :: instrs) state''
   | exec_instr_block_nil:
@@ -113,7 +124,7 @@ Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
-  let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in
+  let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
   max_reg_cfi max_body bb.(bb_exit).
 
 Definition max_reg_function (f: function) :=
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 39c57df..e2e9a90 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -591,12 +591,6 @@ Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   | i :: l => update (abstract_sequence f l) i
   end.
 
-Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest :=
-  match b with
-  | nil => f
-  | i :: l => abstract_sequence (abstract_sequence_par f l) i
-  end.
-
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks should have been moved,
 none of the labels should be different, meaning the control-flow instructions should match exactly.
@@ -622,7 +616,7 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
 
 Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool :=
   check (abstract_sequence empty (bb_body bb))
-        (abstract_sequence_par empty (bb_body bbt)) &&
+        (abstract_sequence empty (concat (concat (bb_body bbt)))) &&
   check_control_flow_instr (bb_exit bb) (bb_exit bbt) &&
   empty_trees (bb_body bb) (bb_body bbt).