Most of Ireturn proof

4 files changed, 80 insertions, 17 deletions

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 68a8416..7e616af 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -219,3 +219,11 @@ Lemma find_get_assocmap :
   assoc ! r = Some v ->
   assoc # r = v.
 Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
+
+Lemma fso : forall m v k1 k2, k1 <> k2 -> (m # k1 <- v) # k2 = m # k2.
+Proof.
+  unfold "_ # _".
+  unfold AssocMapExt.get_default.
+  intros.
+  destruct_match; rewrite AssocMap.gso in Heqo by auto; rewrite Heqo; auto.
+Qed.
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index a7e3584..365d981 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -446,12 +446,16 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
+Fixpoint nonblock_all pairs :=
+  match pairs with
+  | (dst, src) :: pairs' => Vseq (nonblock dst (Vvar src)) (nonblock_all pairs')
+  | nil => Vskip
+  end.
+
 (** [fork] a datapath statement which sets up the execution of a function *)
 Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt :=
   let reset_mod := Vnonblock (Vvar rst) (posToLit 1) in
-  let assign_params :=
-      List.fold_left (fun acc (a : reg*reg) => let (dst, src) := a in Vseq (nonblock dst (Vvar src)) acc)
-                     params Vskip in
+  let assign_params := nonblock_all params in
   Vseq reset_mod assign_params.
 
 Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt :=
@@ -459,13 +463,15 @@ Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt :=
   let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in
   Vseq stop_reset set_result.
 
-Definition return_val fin rtrn r :=
-  let retval :=
-      match r with
-      | Some r' => Vvar r'
-      | None => Vlit (ZToValue 0%Z)
-      end in
-  Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval).
+Definition return_val r :=
+  match r with
+  | Some r' => Vvar r'
+  | None => Vlit (ZToValue 0%Z)
+  end.
+
+Definition do_return fin rtrn r :=
+  Vseq (block fin (Vlit (ZToValue 1%Z)))
+       (block rtrn (return_val r)).
 
 Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)).
 
@@ -537,7 +543,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       error (Errors.msg "Ijumptable: Case statement not supported.")
     | Ireturn r =>
       do idle_state <- create_state;
-      do _ <- add_instr n idle_state (return_val fin rtrn r);
+      do _ <- add_instr n idle_state (do_return fin rtrn r);
       add_instr_skip idle_state (idle fin)
     end
   end.
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index d297c80..077a8dc 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1143,12 +1143,11 @@ Section CORRECTNESS.
     - inv CONST. assumption.
     - inv CONST. assumption.
     - repeat econstructor.
-    - repeat econstructor. simpl. apply H5.
+    - repeat econstructor. intuition eauto.
     - big_tac.
-      assert (HPle: Ple res0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-
-      unfold Ple in HPle. lia.
+      assert (Ple res0 (RTL.max_reg_function f))
+        by eauto using RTL.max_reg_function_def.
+      xomega.
     - big_tac.
       + apply regs_lessdef_add_match. assumption.
         apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
@@ -1172,6 +1171,56 @@ Section CORRECTNESS.
   Qed.
   Hint Resolve transl_iop_correct : htlproof.
 
+  Lemma return_val_exec_spec : forall f or asr asa,
+      Verilog.expr_runp f asr asa (return_val or)
+                        (match or with
+                         | Some r => asr#r
+                         | None => ZToValue 0
+                         end).
+  Proof. destruct or; repeat econstructor. Qed.
+
+  Lemma transl_ireturn_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
+      (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg)
+      (m' : mem),
+      (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) ->
+      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2.
+  Proof.
+    intros * H H0 * MSTATE.
+    inv_state.
+    inv CONST. simplify.
+    eexists. split.
+    - eapply Smallstep.plus_two.
+      + eapply HTL.step_module; eauto; try solve [ repeat econstructor ].
+        * repeat econstructor. apply return_val_exec_spec.
+        * big_tac.
+        * admit.
+      + simplify.
+        eapply HTL.step_finish.
+        * big_tac.
+        * big_tac.
+      + eauto with htlproof.
+   - constructor; eauto with htlproof.
+     destruct or.
+     + rewrite fso. (* Return value is not fin *)
+       * big_tac.
+         inv MASSOC.
+         apply H10.
+         eapply RTL.max_reg_function_use; eauto; crush.
+       * assert (Ple r (RTL.max_reg_function f))
+           by (eapply RTL.max_reg_function_use; eauto; crush).
+         xomega.
+     + eauto with htlproof.
+  Unshelve.
+  exact tt. eauto.
+  Admitted.
+  Hint Resolve transl_ireturn_correct : htlproof.
+
   Ltac tac :=
     repeat match goal with
            | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 1c2d090..d02aff6 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -107,7 +107,7 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node)  (stmnts : datapath) (trans : c
       c!pc = Some (RTL.Ireturn r) ->
 
       (exists pc2,
-          stmnts!pc = Some (return_val fin rtrn r) /\
+          stmnts!pc = Some (do_return fin rtrn r) /\
           trans!pc = Some (state_goto st pc2) /\
           stmnts!pc2 = Some (idle fin) /\
           trans!pc2 = Some Vskip) ->