Fix types with new changes in RTLBlock

Also formatted some files so that they are under 80 columns, which is
much nicer to read.

4 files changed, 133 insertions, 91 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 70c0454..7e6f97c 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -26,11 +26,12 @@ Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.Verilog.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.HTL.
 Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
@@ -81,7 +82,8 @@ Module HTLState <: State.
   Lemma st_trans :
     forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
   Proof.
-    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
+    intros. inv H. inv H0.
+    apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
     destruct H4 with n; destruct H7 with n; intuition congruence.
   Qed.
 
@@ -251,7 +253,8 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
 Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
   Vbinop op (Vvar r) (Vlit (ZToValue l)).
 
-Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
+Definition translate_comparison (c : Integers.comparison) (args : list reg)
+  : mon expr :=
   match c, args with
   | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
   | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
@@ -259,11 +262,12 @@ Definition translate_comparison (c : Integers.comparison) (args : list reg) : mo
   | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
   | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
   | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
-  | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison instruction not implemented: other")
   end.
 
-Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
-  : mon expr :=
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
+           (i: Integers.int) : mon expr :=
   match c, args with
   | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
   | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
@@ -271,37 +275,46 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
   | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
   | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
   | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
-  | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison_imm instruction not implemented: other")
   end.
 
-Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg)
+  : mon expr :=
   match c, args with
   | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
   | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
   | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
   | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
-  | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison instruction not implemented: other")
   end.
 
-Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
-  : mon expr :=
+Definition translate_comparison_immu (c : Integers.comparison)
+           (args : list reg) (i: Integers.int) : mon expr :=
   match c, args with
   | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
   | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
   | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
   | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
-  | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison_imm instruction not implemented: other")
   end.
 
-Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
+Definition translate_condition (c : Op.condition) (args : list reg)
+  : mon expr :=
   match c, args with
   | Op.Ccomp c, _ => translate_comparison c args
   | Op.Ccompu c, _ => translate_comparisonu c args
   | Op.Ccompimm c i, _ => translate_comparison_imm c args i
   | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
-  | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
-  | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
+  | Op.Cmaskzero n, _ =>
+    error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ =>
+    error (Errors.msg
+         "Htlgen: condition instruction not implemented: Cmasknotzero")
+  | _, _ =>
+    error (Errors.msg "Htlgen: condition instruction not implemented: other")
   end.
 
 Definition check_address_parameter_signed (p : Z) : bool :=
@@ -311,30 +324,31 @@ Definition check_address_parameter_signed (p : Z) : bool :=
 Definition check_address_parameter_unsigned (p : Z) : bool :=
   Z.leb p Integers.Ptrofs.max_unsigned.
 
-Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
+Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
+  : mon expr :=
   match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Op.Aindexed off, r1::nil =>
     if (check_address_parameter_signed off)
     then ret (boplitz Vadd r1 off)
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
+    else error (Errors.msg ("HTLPargen: translate_eff_addressing (Aindexed): address out of bounds"))
   | Op.Ascaled scale offset, r1::nil =>
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ascaled): address out of bounds")
   | Op.Aindexed2 offset, r1::r2::nil =>
     if (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2): address out of bounds")
   | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)
     then ret (Vlit (ZToValue a))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
-  | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ainstack): address out of bounds")
+  | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing")
   end.
 
 (** Translate an instruction to a statement. FIX mulhs mulhu *)
@@ -535,7 +549,8 @@ Definition poslength {A : Type} (l : list A) : positive :=
   | _ => 1
   end.
 
-Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l} : list (positive * A) :=
+Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l}
+  : list (positive * A) :=
   match l with
   | x :: xs => (p, x) :: penumerate (Pos.succ p) xs
   | nil => nil
@@ -550,7 +565,8 @@ Lemma add_data_instr_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath))
+       (AssocMap.set n (Vseq (AssocMapExt.get_default
+                            _ Vskip n s.(st_datapath)) st) s.(st_datapath))
        s.(st_controllogic)).
 Proof.
   constructor; intros;
@@ -601,77 +617,92 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
            s.(st_datapath)
            (AssocMap.set n st s.(st_controllogic)))
          (add_control_instr_state_incr s n st CTRL)
-    | _ => Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
+    | _ =>
+      Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
     end.
 
-Definition translate_inst (fin rtrn stack : reg) (n : node) (i : instruction) : mon unit :=
+Definition translate_inst (fin rtrn stack : reg) (n : node) (i : instr)
+  : mon unit :=
   match i with
-  | RPnop =>
+  | RBnop =>
     add_data_instr n Vskip
-  | RPop op args dst =>
+  | RBop op args dst =>
     do instr <- translate_instr op args;
     do _ <- declare_reg None dst 32;
     add_data_instr n (nonblock dst instr)
-  | RPload chunk addr args dst =>
+  | RBload chunk addr args dst =>
     do src <- translate_arr_access chunk addr args stack;
     do _ <- declare_reg None dst 32;
     add_data_instr n (nonblock dst src)
-  | RPstore chunk addr args src =>
+  | RBstore chunk addr args src =>
     do dst <- translate_arr_access chunk addr args stack;
     add_data_instr n (Vnonblock dst (Vvar src))
   end.
 
-Definition translate_inst_list (fin rtrn stack : reg) (ni : node * list instruction) : mon unit :=
+Definition translate_inst_list (fin rtrn stack : reg) (ni : node * list instr)
+  : mon unit :=
   let (n, li) := ni in
   do _ <- collectlist (translate_inst fin rtrn stack n) li;
   do st <- get;
   add_control_instr n (state_goto st.(st_st) (Pos.succ n)).
 
-Definition translate_cfi (fin rtrn stack : reg) (ni : node * control_flow_inst) : mon unit :=
+Definition translate_cfi (fin rtrn stack : reg) (ni : node * cf_instr)
+  : mon unit :=
   let (n, cfi) := ni in
   match cfi with
-  | RPgoto n' =>
+  | RBgoto n' =>
     do st <- get;
     add_node_skip n (state_goto st.(st_st) n')
-  | RPcond c args n1 n2 =>
+  | RBcond c args n1 n2 =>
     do e <- translate_condition c args;
     add_branch_instr e n n1 n2
-  | RPreturn r =>
+  | RBreturn r =>
     match r with
     | Some r' =>
-      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
+      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z)))
+                             (block rtrn (Vvar r')))
     | None =>
-      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
+      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z)))
+                             (block rtrn (Vlit (ZToValue 0%Z))))
     end
-  | RPjumptable r ln => error (Errors.msg "HTLPargen: RPjumptable not supported.")
-  | RPcall sig ri rl r n => error (Errors.msg "HTLPargen: RPcall not supported.")
-  | RPtailcall sig ri lr => error (Errors.msg "HTLPargen: RPtailcall not supported.")
-  | RPbuiltin e lb b n => error (Errors.msg "HTLPargen: RPbuildin not supported.")
+  | RBjumptable r ln =>
+    error (Errors.msg "HTLPargen: RPjumptable not supported.")
+  | RBcall sig ri rl r n =>
+    error (Errors.msg "HTLPargen: RPcall not supported.")
+  | RBtailcall sig ri lr =>
+    error (Errors.msg "HTLPargen: RPtailcall not supported.")
+  | RBbuiltin e lb b n =>
+    error (Errors.msg "HTLPargen: RPbuildin not supported.")
   end.
 
-Definition transf_bblock (fin rtrn stack : reg) (ni : node * bblock) : mon unit :=
+Definition transf_bblock (fin rtrn stack : reg) (ni : node * bblock)
+  : mon unit :=
   let (n, bb) := ni in
-  do _ <- collectlist (translate_inst_list fin rtrn stack) (penumerate n bb.(bb_body));
-  match bb.(bb_exit) with
-  | Some e => translate_cfi fin rtrn stack ((n + poslength bb.(bb_body))%positive, e)
-  | None => ret tt
-  end.
+  do _ <- collectlist (translate_inst_list fin rtrn stack)
+                      (penumerate n bb.(bb_body));
+  translate_cfi fin rtrn stack
+                ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)).
 
-Definition transf_module (f: function) : mon module :=
+Definition transf_module (f: function) : mon HTL.module :=
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
-    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
-    do _ <- collectlist (transf_bblock fin rtrn stack) (Maps.PTree.elements f.(RTLPar.fn_code));
-    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTLPar.fn_params);
+    do (stack, stack_len) <- create_arr None 32
+                                        (Z.to_nat (f.(fn_stacksize) / 4));
+    do _ <- collectlist (transf_bblock fin rtrn stack)
+                        (Maps.PTree.elements f.(RTLPar.fn_code));
+    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32)
+                        f.(RTLPar.fn_params);
     do start <- create_reg (Some Vinput) 1;
     do rst <- create_reg (Some Vinput) 1;
     do clk <- create_reg (Some Vinput) 1;
     do current_state <- get;
-    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
+    match zle (Z.pos (max_pc_map current_state.(st_datapath)))
+              Integers.Int.max_unsigned,
+          zle (Z.pos (max_pc_map current_state.(st_controllogic)))
+              Integers.Int.max_unsigned with
     | left LEDATA, left LECTRL =>
-        ret (mkmodule
+        ret (HTL.mkmodule
            f.(RTLPar.fn_params)
            current_state.(st_datapath)
            current_state.(st_controllogic)
@@ -701,7 +732,7 @@ Definition max_state (f: function) : state :=
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
 
-Definition transl_module (f : function) : Errors.res module :=
+Definition transl_module (f : function) : Errors.res HTL.module :=
   run_mon (max_state f) (transf_module f).
 
 Definition transl_fundef := transf_partial_fundef transl_module.
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 32d7674..2a388e6 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -31,8 +31,9 @@ Require Import compcert.verilog.Op.
 Require Import vericert.hls.RTLBlockInstr.
 
 Definition bblock_body : Type := list instr.
+Definition bblock := bblock bblock_body.
 
-Definition code : Type := PTree.t (@bblock bblock_body).
+Definition code : Type := PTree.t bblock.
 
 Record function: Type := mkfunction {
   fn_sig: signature;
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index af6b0ab..94a1a20 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -30,7 +30,8 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.RTLBlockInstr.
 
-Definition bblock := RTLBlockInstr.bblock (list (list instr)).
+Definition bblock_body := list (list instr).
+Definition bblock := RTLBlockInstr.bblock bblock_body.
 
 Definition code : Type := PTree.t bblock.
 
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v
index 7c22995..fdcb8bb 100644
--- a/src/hls/Scheduleoracle.v
+++ b/src/hls/Scheduleoracle.v
@@ -31,6 +31,7 @@ Require Import compcert.lib.Maps.
 Require compcert.verilog.Op.
 Require vericert.hls.RTLBlock.
 Require vericert.hls.RTLPar.
+Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.common.Vericertlib.
 
 (*|
@@ -132,7 +133,12 @@ Proof.
   decide equality.
 Defined.
 
-Lemma instruction_eq: forall (x y : RTLBlock.instruction), {x = y} + {x <> y}.
+Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Defined.
+
+Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
 Proof.
   generalize Pos.eq_dec; intro.
   generalize typ_eq; intro.
@@ -148,6 +154,26 @@ Proof.
   decide equality.
 Defined.
 
+Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intro.
+  generalize typ_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  generalize memory_chunk_eq; intro.
+  generalize addressing_eq; intro.
+  generalize operation_eq; intro.
+  generalize condition_eq; intro.
+  generalize signature_eq; intro.
+  generalize list_operation_eq; intro.
+  generalize list_reg_eq; intro.
+  generalize AST.ident_eq; intro.
+  repeat decide equality.
+Defined.
+
 (*|
 We then create equality lemmas for a resource and a module to index resources uniquely.  The
 indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be
@@ -437,25 +463,14 @@ Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_li
   | i :: l => Econs (f # (Reg i)) (list_translation l f)
   end.
 
-Definition update_block (f : forest) (i : RTLBlock.instruction) : forest :=
-  match i with
-  | RTLBlock.RBnop => f
-  | RTLBlock.RBop op rl r =>
-    f # (Reg r) <- (Eop op (list_translation rl f))
-  | RTLBlock.RBload chunk addr rl r =>
-    f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem))
-  | RTLBlock.RBstore chunk addr rl r =>
-    f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r)))
-  end.
-
-Definition update_par (f : forest) (i : RTLPar.instruction) : forest :=
+Definition update (f : forest) (i : instr) : forest :=
   match i with
-  | RTLPar.RPnop => f
-  | RTLPar.RPop op rl r =>
+  | RBnop => f
+  | RBop op rl r =>
     f # (Reg r) <- (Eop op (list_translation rl f))
-  | RTLPar.RPload chunk addr rl r =>
+  | RBload chunk addr rl r =>
     f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem))
-  | RTLPar.RPstore chunk addr rl r =>
+  | RBstore chunk addr rl r =>
     f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r)))
   end.
 
@@ -470,22 +485,16 @@ that there aren't any more effects in the resultant RTLPar code than in the RTLB
 Get a sequence from the basic block.
 |*)
 
-Fixpoint abstract_sequence_block (f : forest) (b : list RTLBlock.instruction) : forest :=
-  match b with
-  | nil => f
-  | i :: l => abstract_sequence_block (update_block f i) l
-  end.
-
-Fixpoint abstract_sequence_par' (f : forest) (b : list RTLPar.instruction) : forest :=
+Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
   | nil => f
-  | i :: l => abstract_sequence_par' (update_par f i) l
+  | i :: l => abstract_sequence (update f i) l
   end.
 
-Fixpoint abstract_sequence_par (f : forest) (b : list (list RTLPar.instruction)) : forest :=
+Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest :=
   match b with
   | nil => f
-  | i :: l => abstract_sequence_par (abstract_sequence_par' f i) l
+  | i :: l => abstract_sequence_par (abstract_sequence f i) l
   end.
 
 (*|
@@ -493,8 +502,8 @@ Check equivalence of control flow instructions.  As none of the basic blocks sho
 none of the labels should be different, meaning the control-flow instructions should match exactly.
 |*)
 
-Definition check_control_flow_instr (c1 : RTLBlock.control_flow_inst) (c2 : RTLPar.control_flow_inst) : bool :=
-  true.
+Definition check_control_flow_instr (c1 c2: cf_instr) : bool :=
+  if cf_instr_eq c1 c2 then true else false.
 
 (*|
 We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling
@@ -502,5 +511,5 @@ transformation.
 |*)
 
 Definition schedule_oracle (bb : RTLBlock.bblock) (bbt : RTLPar.bblock) : bool :=
-  check (abstract_sequence_block empty (RTLBlock.bb_body bb))
-        (abstract_sequence_par empty (RTLPar.bb_body bbt)).
+  check (abstract_sequence empty (bb_body bb))
+        (abstract_sequence_par empty (bb_body bbt)).