Finished most of the giblesubpar proof

9 files changed, 138 insertions, 41 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 5950e95..6cd8e1f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -67,6 +67,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
   set_dest Vericert.PrintGibleSeq.destination option_dgblseq ".gblseq";
   set_dest Vericert.PrintGiblePar.destination option_dgblpar ".gblpar";
+  set_dest Vericert.PrintGibleSubPar.destination option_dgblsubpar ".gblsubpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.PrintDHTL.destination option_ddhtl ".dhtl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
@@ -270,6 +271,7 @@ HLS Optimisations:
   -drtl          Save RTL at various optimization points in <file>.rtl.<n>
   -dgblseq       Save GibleSeq <file>.gblseq
   -dgblpar       Save GiblePar <file>.gblpar
+  -dgblsubpar    Save GibleSubPar <file>.gblsubpar
   -dhtl          Save HTL before Verilog generation <file>.htl
   -dltl          Save LTL after register allocation in <file>.ltl
   -dmach         Save generated Mach code in <file>.mach
@@ -412,6 +414,7 @@ let cmdline_actions =
     option_drtl := true;
     option_dgblseq := true;
     option_dgblpar := true;
+    option_dgblsubpar := true;
     option_dhtl := true;
     option_ddhtl := true;
     option_dltl := true;
diff --git a/src/Compiler.v b/src/Compiler.v
index c568374..c4d05b2 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -95,6 +95,7 @@ Parameter print_HTL: Z -> HTL.program -> unit.
 Parameter print_DHTL: Z -> DHTL.program -> unit.
 Parameter print_GibleSeq: Z -> GibleSeq.GibleSeq.program -> unit.
 Parameter print_GiblePar: Z -> GiblePar.GiblePar.program -> unit.
+Parameter print_GibleSubPar: Z -> GibleSubPar.GibleSubPar.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -299,6 +300,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ time "Scheduling" GiblePargen.transl_program
    @@ print (print_GiblePar 0)
   @@@ GibleSubPargen.transl_program
+   @@ print (print_GibleSubPar 0)
   (* @@@ HTLPargen.transl_program *)
   @@@ DHTLgen.transl_program
    @@ print (print_DHTL 0)
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 83a1871..544e3ca 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -7,6 +7,7 @@ let option_dhtl = ref false
 let option_ddhtl = ref false
 let option_dgblseq = ref false
 let option_dgblpar = ref false
+let option_dgblsubpar = ref false
 let option_drtlparfu = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index f78b0bd..f23b184 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -151,6 +151,7 @@ Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_GibleSeq => "PrintGibleSeq.print_if".
 Extract Constant Compiler.print_GiblePar => "PrintGiblePar.print_if".
+Extract Constant Compiler.print_GibleSubPar => "PrintGibleSubPar.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
 Extract Constant Compiler.print_DHTL => "PrintDHTL.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
diff --git a/src/hls/ClockMemory.v b/src/hls/ClockMemory.v
index 3d068ad..549b310 100644
--- a/src/hls/ClockMemory.v
+++ b/src/hls/ClockMemory.v
@@ -44,9 +44,9 @@ Definition pred := positive.
 
 Definition transf_maps (d: stmnt) :=
   match d with
-  | Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2) =>
+  | Vseq (Vseq Vskip (Vblock (Vvari r e1) e2)) ((Vblock (Vvar _) _) as rest) =>
     Vseq rest (Vnonblock (Vvari r e1) e2)
-  | Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2)) =>
+  | Vseq (Vseq Vskip (Vblock (Vvar e1) (Vvari r e2))) (Vblock (Vvar st') e3) =>
     Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vvari r e2))
   | _ => d
   end.
diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v
index 4b931c7..49d2c87 100644
--- a/src/hls/DHTLgen.v
+++ b/src/hls/DHTLgen.v
@@ -103,7 +103,7 @@ Definition translate_predicate (a : assignment)
     | Some _ => a dst (Vternary (pred_expr pos') e dst)
     end
   end.
- 
+
 Definition state_goto (p: option pred_op) (st : reg) (n : node) : stmnt :=
   translate_predicate Vblock p (Vvar st) (Vlit (posToValue n)).
 
@@ -302,12 +302,12 @@ Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
   | RBreturn r =>
     match r with
     | Some r' =>
-      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vvar r')))
+      Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vvar (reg_enc r'))))
     | None =>
-      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vlit (ZToValue 0%Z))))
+      Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vlit (ZToValue 0%Z))))
     end
   | RBjumptable r tbl =>
-    Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip))
+    Errors.OK (Vcase (Vvar (reg_enc r)) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip))
   | RBcall sig ri rl r n =>
     Errors.Error (Errors.msg "HTLPargen: RBcall not supported.")
   | RBtailcall sig ri lr =>
@@ -324,15 +324,15 @@ Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
   | RBnop => Errors.OK dc
   | RBop p op args dst => 
     do instr <- translate_instr op args;
-    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in
+    let stmnt := translate_predicate Vblock (npred p) (Vvar (reg_enc dst)) instr in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBload p mem addr args dst =>
     do src <- translate_arr_access mem addr args ctrl.(ctrl_stack);
-    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in
+    let stmnt := translate_predicate Vblock (npred p) (Vvar (reg_enc dst)) src in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBstore p mem addr args src =>
     do dst <- translate_arr_access mem addr args ctrl.(ctrl_stack);
-    let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in
+    let stmnt := translate_predicate Vblock (npred p) dst (Vvar (reg_enc src)) in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBsetpred p' cond args p =>
     do cond' <- translate_condition cond args;
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v
index 846bfad..0c9fd80 100644
--- a/src/hls/DMemorygen.v
+++ b/src/hls/DMemorygen.v
@@ -164,28 +164,28 @@ Definition transf_maps state ram in_ (d: PTree.t stmnt) :=
   | (i, n) =>
     match PTree.get i d with
     (* Conditional store *)
-    | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) (Vternary cond e2 (Vvari r' e1')))) =>
-      if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then
-        let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram))))
-                       (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1)))
-                             (Vseq (Vblock (Vvar (ram_d_in ram)) e2)
-                                   (Vblock (Vvar (ram_addr ram)) e1)))
-        in
-        PTree.set i (Vseq rest nd) d
-      else d
-    | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) =>
-      if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z
-         && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state)
-      then
-        let nd :=
-            Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
-                 (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
-                       (Vblock (Vvar (ram_addr ram)) e2))
-        in
-        let aout := Vblock (Vvar e1) (Vternary cond (Vvar (ram_d_out ram)) edef) in
-        let redirect := Vblock (Vvar state) (Vlit (posToValue n)) in
-        (PTree.set i (Vseq redirect nd) (PTree.set n (Vseq (Vblock (Vvar st') e3) aout) d))
-      else d
+    (* | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) (Vternary cond e2 (Vvari r' e1')))) => *)
+    (*   if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then *)
+    (*     let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram)))) *)
+    (*                    (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) *)
+    (*                          (Vseq (Vblock (Vvar (ram_d_in ram)) e2) *)
+    (*                                (Vblock (Vvar (ram_addr ram)) e1))) *)
+    (*     in *)
+    (*     PTree.set i (Vseq rest nd) d *)
+    (*   else d *)
+    (* | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) => *)
+    (*   if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z *)
+    (*      && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state) *)
+    (*   then *)
+    (*     let nd := *)
+    (*         Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) *)
+    (*              (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) *)
+    (*                    (Vblock (Vvar (ram_addr ram)) e2)) *)
+    (*     in *)
+    (*     let aout := Vblock (Vvar e1) (Vternary cond (Vvar (ram_d_out ram)) edef) in *)
+    (*     let redirect := Vblock (Vvar state) (Vlit (posToValue n)) in *)
+    (*     (PTree.set i (Vseq redirect nd) (PTree.set n (Vseq (Vblock (Vvar st') e3) aout) d)) *)
+    (*   else d *)
     | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) e2)) =>
       if r =? (ram_mem ram) then
         let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
@@ -240,7 +240,7 @@ Proof.
     eapply H. eapply AssocMapExt.elements_iff; eauto.
   + rewrite PTree.gso in H1 by auto. eapply H.
     eapply AssocMapExt.elements_iff; eauto.
-Admitted.
+Qed.
 
 Definition max_pc {A: Type} (m: PTree.t A) :=
   fold_right Pos.max 1%positive (map fst (PTree.elements m)).
@@ -1077,7 +1077,7 @@ Lemma transf_not_changed :
     (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vnonblock e3 (Vvari r e4)))) ->
     d!i = Some d_s ->
     transf_maps state ram (i, n) d = d.
-Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted.
+Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed.
 
 Lemma transf_not_changed_neq :
   forall state ram n d d' i a d_s,
@@ -2270,7 +2270,7 @@ Proof.
          | |- _ = None => apply max_index_2; lia
          | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
          end; auto.
-Admitted.
+Qed.
 
 Lemma transf_alternatives_neq :
   forall state ram a n' n d'' d' i d,
diff --git a/src/hls/DVeriloggen.v b/src/hls/DVeriloggen.v
index 6b47dd0..d751178 100644
--- a/src/hls/DVeriloggen.v
+++ b/src/hls/DVeriloggen.v
@@ -42,6 +42,16 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
 
 Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
+Definition declare_all (start reset clk finish ret st stk: reg) (stk_len: nat) (body: list module_item) :=
+  Vdeclaration (Vdecl (Some Vinput) start 1)
+  :: Vdeclaration (Vdecl (Some Vinput) reset 1)
+  :: Vdeclaration (Vdecl (Some Vinput) clk 1)
+  :: Vdeclaration (Vdecl (Some Voutput) finish 1)
+  :: Vdeclaration (Vdecl (Some Voutput) ret 32)
+  :: Vdeclaration (Vdecl None st 32)
+  :: Vdeclaration (Vdeclarr None stk 32 stk_len)
+  :: (all_reg_declarations (start::reset::clk::finish::ret::st::stk::nil) body).
+
 Definition inst_ram clk ram :=
   Valways (Vnegedge clk)
           (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram)))
@@ -65,9 +75,7 @@ Definition transl_module (m : DHTL.module) : Verilog.module :=
         (*         :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *)
         (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *)
                 :: inst_ram m.(DHTL.mod_clk) ram
-                :: List.map Vdeclaration ((* Vdecl None nstate 32 ::  *)
-                     (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
-                     ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls)))) in
+                :: nil in
     Verilog.mkmodule m.(DHTL.mod_start)
                      m.(DHTL.mod_reset)
                      m.(DHTL.mod_clk)
@@ -77,7 +85,14 @@ Definition transl_module (m : DHTL.module) : Verilog.module :=
                      m.(DHTL.mod_stk)
                      m.(DHTL.mod_stk_len)
                      m.(DHTL.mod_params)
-                     body
+                     (body ++ declare_all m.(DHTL.mod_start)
+                     m.(DHTL.mod_reset)
+                     m.(DHTL.mod_clk)
+                     m.(DHTL.mod_finish)
+                     m.(DHTL.mod_return)
+                     m.(DHTL.mod_st)
+                     m.(DHTL.mod_stk)
+                     m.(DHTL.mod_stk_len) body)
                      m.(DHTL.mod_entrypoint)
   | None =>
     let body :=
@@ -87,8 +102,7 @@ Definition transl_module (m : DHTL.module) : Verilog.module :=
                 (* :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *)
         (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) *)
         (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *)
-                :: List.map Vdeclaration ((* Vdecl None (DHTL.mod_st m) 32 ::  *)arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
-                                                          ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
+        :: nil in
     Verilog.mkmodule m.(DHTL.mod_start)
                      m.(DHTL.mod_reset)
                      m.(DHTL.mod_clk)
@@ -98,7 +112,14 @@ Definition transl_module (m : DHTL.module) : Verilog.module :=
                      m.(DHTL.mod_stk)
                      m.(DHTL.mod_stk_len)
                      m.(DHTL.mod_params)
-                     body
+                     (body ++ declare_all m.(DHTL.mod_start)
+                     m.(DHTL.mod_reset)
+                     m.(DHTL.mod_clk)
+                     m.(DHTL.mod_finish)
+                     m.(DHTL.mod_return)
+                     m.(DHTL.mod_st)
+                     m.(DHTL.mod_stk)
+                     m.(DHTL.mod_stk_len) body)
                      m.(DHTL.mod_entrypoint)
   end.
 
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 79ee723..69252ec 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -904,3 +904,72 @@ with max_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
             (Pos.max (max_reg_stmnt s)
                      (max_reg_stmnt_expr_list stl'))
   end.
+
+Definition combine_reg (r1 r2 : option unit) := 
+  match r1, r2 with
+  | Some _, _ => Some tt
+  | _, Some _ => Some tt
+  | _, _ => None
+  end.
+
+Import Maps.
+
+Fixpoint all_reg_expr (e: expr): PTree.t unit :=
+  match e with
+  | Vlit _ => PTree.empty _
+  | Vvar r => PTree.set r tt (PTree.empty _)
+  | Vvari r e => all_reg_expr e
+  | Vrange r e1 e2 => PTree.set r tt (PTree.empty _)
+  | Vinputvar r => PTree.empty _
+  | Vbinop _ e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2)
+  | Vunop _ e => all_reg_expr e
+  | Vternary e1 e2 e3 => 
+    PTree.combine combine_reg (all_reg_expr e1) (PTree.combine combine_reg (all_reg_expr e2) (all_reg_expr e3))
+  end.
+
+Fixpoint all_reg_stmnt (st: stmnt): PTree.t unit :=
+  match st with
+  | Vskip => PTree.empty _
+  | Vseq s1 s2 => PTree.combine combine_reg (all_reg_stmnt s1) (all_reg_stmnt s2)
+  | Vcond e s1 s2 =>
+    PTree.combine combine_reg (all_reg_expr e) (PTree.combine combine_reg (all_reg_stmnt s1) (all_reg_stmnt s2))
+  | Vcase e stl None => PTree.combine combine_reg (all_reg_expr e) (all_reg_stmnt_expr_list stl)
+  | Vcase e stl (Some s) =>
+    PTree.combine combine_reg (all_reg_stmnt s)
+            (PTree.combine combine_reg (all_reg_expr e) (all_reg_stmnt_expr_list stl))
+  | Vblock e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2)
+  | Vnonblock e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2)
+  end
+with all_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
+  match stl with
+  | Stmntnil => PTree.empty _
+  | Stmntcons e s stl' =>
+    PTree.combine combine_reg (all_reg_expr e)
+            (PTree.combine combine_reg (all_reg_stmnt s)
+                     (all_reg_stmnt_expr_list stl'))
+  end.
+
+Fixpoint all_reg_edge (e: edge): PTree.t unit :=
+  match e with
+  | Vposedge r => PTree.set r tt (PTree.empty _)
+  | Vnegedge r => PTree.set r tt (PTree.empty _)
+  | Valledge => PTree.empty _
+  | Voredge e1 e2 => PTree.combine combine_reg (all_reg_edge e1) (all_reg_edge e2)
+  end.
+
+Definition all_reg_module_item (m: module_item): PTree.t unit :=
+  match m with
+  | Vdeclaration d => PTree.empty _
+  | Valways e s
+  | Valways_ff e s
+  | Valways_comb e s => PTree.combine combine_reg (all_reg_edge e) (all_reg_stmnt s)
+  end.
+
+Definition all_reg_module_item_l (ml: list module_item): PTree.t unit :=
+  List.fold_left (fun a b => PTree.combine combine_reg a (all_reg_module_item b)) ml (PTree.empty _).
+
+Definition all_reg_to_declaration (tree: PTree.t unit): list module_item :=
+  PTree.fold (fun ml p _ => Vdeclaration (Vdecl None p 32) :: ml) tree nil.
+
+Definition all_reg_declarations (rem: list positive) (ml: list module_item): list module_item :=
+  all_reg_to_declaration (List.fold_left (fun a b => PTree.remove b a) rem (all_reg_module_item_l ml)).