Correct lookup for called funcs, simplify tr_module

3 files changed, 61 insertions, 32 deletions

diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index bacee9c..2e4cf48 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -488,7 +488,13 @@ Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) :=
 
 Definition map_externctrl_params := xmap_externctrl_params 0.
 
-Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
+Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) :=
+  match Globalenvs.Genv.find_symbol ge symb with
+  | None => None
+  | Some b => Globalenvs.Genv.find_funct_ptr ge b
+  end.
+
+Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
     match i with
@@ -516,7 +522,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni:
     | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
     | Icall sig (inr fn) args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned
-      then match funmap ! fn with
+      then match rtl_find_func ge fn with
            | Some (AST.Internal _) =>
              do params <- map_externctrl_params fn args;
 
@@ -526,6 +532,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni:
              do finish_reg <- map_externctrl fn ctrl_finish;
              do reset_reg <- map_externctrl fn ctrl_reset;
              do return_reg <- map_externctrl fn ctrl_return;
+             do _ <- map_externctrl fn ctrl_clk;
 
              let fork_instr := fork reset_reg params in
              let join_instr := join return_reg reset_reg dst in
@@ -568,16 +575,18 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
 
-Definition transf_module (funmap : PTree.t RTL.fundef) (main : ident) (f: function) : mon HTL.module :=
+Definition declare_params params := collectlist (fun r => declare_reg (Some Vinput) r 32) params.
+
+Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.module :=
   if stack_correct f.(fn_stacksize) then
+    do _ <- declare_params (RTL.fn_params f);
     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_instr funmap fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
-    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
     do start <- create_reg (Some Vinput) 1;
     do rst <- create_reg (Some Vinput) 1;
-    do clk <- map_externctrl main ctrl_clk;
+    do clk <- create_reg (Some Vinput) 1;
+    do _ <- collectlist (transf_instr ge fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
     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
@@ -614,10 +623,17 @@ Definition max_state (f: function) : state :=
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
 
-Definition prog_funmap (prog : RTL.program) : (PTree.t ) :=
+Definition prog_funmap (prog : RTL.program) : (PTree.t RTL.fundef) :=
+  AssocMap_Properties.of_list (
+    Option.map_option (fun '(ident, def) => match def with
+                                         | AST.Gfun f => Some (ident, f)
+                                         | _ => None
+                                         end)
+                      (AST.prog_defs prog)
+  ).
 
 Definition transl_module (prog : RTL.program) (f : function) : Errors.res HTL.module :=
-  run_mon (max_state f) (transf_module  f).
+  run_mon (max_state f) (transf_module (Globalenvs.Genv.globalenv prog) (AST.prog_main prog) f).
 
 Definition transl_fundef prog := transf_partial_fundef (transl_module prog).
 
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index cba21b0..eb7326a 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -179,7 +179,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop :=
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
-  Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp /\
+  Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\
   main_is_internal p = true.
 
 Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
@@ -201,7 +201,7 @@ Proof.
 Qed.
 
 Definition match_prog' (p: RTL.program) (tp: HTL.program) :=
-  Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp.
+  Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp.
 
 Lemma match_prog_matches :
   forall p tp, match_prog p tp -> match_prog' p tp.
@@ -386,9 +386,8 @@ Ltac not_control_reg :=
   solve [
       unfold Ple, Plt in *;
       try multimatch goal with
-          | [ H : forall r,
-                (exists x, _ ! r = Some x) -> (r > _)%positive /\ (_ > r)%positive
-                |- context[?r']
+          | [ H : forall r, (exists x, _ ! r = Some x) -> (_ < r < _)%positive
+                       |- context[?r']
             ] => destruct (H r' ltac:(eauto))
           end;
       lia
@@ -467,7 +466,7 @@ Section CORRECTNESS.
   Admitted.
 
   Lemma TRANSL' :
-    Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog.
+    Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog.
   Proof. intros; apply match_prog_matches; assumption. Qed.
 
   Lemma symbols_preserved:
@@ -478,7 +477,7 @@ Section CORRECTNESS.
     forall (b: Values.block) (f: RTL.fundef),
       Genv.find_funct_ptr ge b = Some f ->
       exists tf,
-        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf.
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef prog f = Errors.OK tf.
   Proof.
     intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
@@ -488,7 +487,7 @@ Section CORRECTNESS.
     forall (v: Values.val) (f: RTL.fundef),
       Genv.find_funct ge v = Some f ->
       exists tf,
-        Genv.find_funct tge v = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf.
+        Genv.find_funct tge v = Some tf /\ transl_fundef prog f = Errors.OK tf.
   Proof.
     intros. exploit (Genv.find_funct_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
@@ -3069,7 +3068,7 @@ Section CORRECTNESS.
       rewrite symbols_preserved; eauto.
     - eauto.
     - constructor; auto with htlproof.
-      apply transl_module_correct with (AST.prog_main prog).
+      apply transl_module_correct.
       assert (Some (AST.Internal x) = Some (AST.Internal m)) as Heqm.
       { rewrite <- H6. setoid_rewrite <- A. trivial. }
       inv Heqm.
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 387def0..b666620 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -134,10 +134,10 @@ Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop :=
       (fin > st)%positive ->
       (rtrn > fin)%positive ->
       (stk > rtrn)%positive ->
-      (forall r, (exists x, externctrl!r = Some x) -> (r > stk /\ start > r)%positive) ->
       (start > stk)%positive ->
       (rst > start)%positive ->
       (clk > rst)%positive ->
+      (forall r, (exists x, externctrl!r = Some x) -> (r > clk)%positive) ->
       tr_module ge f m.
 Hint Constructors tr_module : htlspec.
 
@@ -341,12 +341,12 @@ Proof. sauto use: helper__map_externctrl_params_spec. Qed.
 Hint Resolve map_externctrl_params_spec : htlspec.
 
 Lemma iter_expand_instr_spec :
-  forall l ge fin rtrn stack s s' i x c,
-    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
+  forall l prog fin rtrn stack s s' i x c,
+    HTLMonadExtra.collectlist (transf_instr (Globalenvs.Genv.globalenv prog) fin rtrn stack) l s = OK x s' i ->
     list_norepet (List.map fst l) ->
     (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
     (forall pc instr, In (pc, instr) l -> c!pc = Some instr ->
-                 tr_code ge c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr).
+                 tr_code (Globalenvs.Genv.globalenv prog) c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr).
 Proof.
   (** Used to solve the simpler cases of tr_code: those involving tr_instr *)
   Ltac tr_code_simple_tac :=
@@ -377,17 +377,16 @@ Proof.
       inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction].
       inversion H.
 
-      assert (exists fd, rtl_find_func ge i0 = Some (AST.Internal fd)) by admit.
-
       eapply tr_code_call; eauto; crush.
 
       destruct (map_externctrl_params_combine _ _ _ _ _ _ EQ1) as [? [? ?]]; subst.
       repeat (eapply ex_intro).
+
       repeat split; try monad_crush. (* slow *)
       * intros.
         destruct (map_externctrl_params_spec _ _ _ _ _ _ _ _ EQ1 ltac:(eauto)) as [param [? ?]].
         exists param; crush; trans_step s3 s'.
-      * monadInv EQ2. crush.
+      * admit. (* (* FIXME: Causes Qed to hang *) monadInv EQ2. crush. *)
     + (* Icond *) tr_code_simple_tac.
     + (* Ireturn *)
       inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction].
@@ -441,9 +440,22 @@ Proof.
 Qed.
 Hint Resolve tr_code_trans : htlspec.
 
+Lemma declare_params_freshreg_trans : forall params s s' x i,
+    declare_params params s = OK x s' i ->
+    st_freshreg s = st_freshreg s'.
+Proof.
+  induction params; unfold declare_params in *; intros * H.
+  - inv H. trivial.
+  - monadInv H.
+    transitivity (st_freshreg s0).
+    + monadInv EQ. auto.
+    + eauto.
+Qed.
+Hint Resolve declare_params_freshreg_trans : htlspec.
+
 Theorem transl_module_correct :
-  forall i f m ge,
-    transl_module i f = Errors.OK m -> tr_module ge f m.
+  forall p f m,
+    transl_module p f = Errors.OK m -> tr_module (Globalenvs.Genv.globalenv p) f m.
 Proof.
   intros * H.
   unfold transl_module in *.
@@ -464,10 +476,12 @@ Proof.
          | [ EQ : get _ = OK _ _ _ |- _ ] => monadInv EQ
          end.
 
-  econstructor; eauto with htlspec; try lia;
-    try solve [some_monad_inv; repeat ((simpl in *; some_monad_inv) + idtac);
-               some_incr; simplify;
-               unfold Ple in *; lia
-              ].
-  admit. (* No control registers are in externctrl *)
+  econstructor;
+    eauto with htlspec;
+    try solve [ repeat some_monad_inv; crush ].
+  - auto_apply declare_params_freshreg_trans.
+    some_monad_inv; monad_crush.
+  - (* forall r, (exists x, externctrl!r = Some x) -> (r >= clk)%positive *)
+    (* Problematic because it does not cover  *)
+    admit.
 Admitted.