Check that only main has a stacksize

2 files changed, 47 insertions, 12 deletions

diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 908c627..73f8993 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -707,7 +707,31 @@ Definition main_is_internal (p : RTL.program) : bool :=
   | _ => false
   end.
 
+Definition only_main_has_stack (p : RTL.program) : Prop :=
+  Forall (fun '(name, def) =>
+            match def with
+            | AST.Gfun (Internal f) => name <> (AST.prog_main p) -> RTL.fn_stacksize f = 0
+            | _ => True
+            end)
+         (PTree.elements (Globalenvs.Genv.genv_defs (Globalenvs.Genv.globalenv p))).
+
+Definition only_main_has_stack_dec (p : RTL.program) : {only_main_has_stack p} + {~ only_main_has_stack p}.
+Proof.
+  refine (Forall_dec _
+                     (fun '(name, def) => match def with
+                                       | AST.Gfun (Internal f) =>
+                                         if (Pos.eq_dec (prog_main p) name)
+                                         then left _
+                                         else if (Z.eq_dec (fn_stacksize f) 0)
+                                              then left _
+                                              else right _
+                                       | _ => left _
+                                       end)
+                     _).
+  all: crush.
+Qed.
+
 Definition transl_program (p : RTL.program) : Errors.res HTL.program :=
-  if main_is_internal p
+  if main_is_internal p && only_main_has_stack_dec p
   then transform_partial_program (transl_fundef p) p
   else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf08600..39394b6 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -213,24 +213,35 @@ Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
   Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\
-  main_is_internal p = true.
+  main_is_internal p = true /\
+  only_main_has_stack p.
 
 Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
   TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2).
 Proof.
-  red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  red. intros. exfalso.
+  destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   apply link_prog_inv in H.
 
-  unfold match_prog in *.
-  unfold main_is_internal in *. simplify. repeat (unfold_match H4).
-  repeat (unfold_match H3). simplify.
-  subst. rewrite H0 in *. specialize (H (AST.prog_main p2)).
+  unfold match_prog, main_is_internal in *.
+
+  simplify.
+  repeat (unfold_match H0).
+  repeat (unfold_match H1).
+  simplify.
+
+  subst.
+  rewrite H5 in *.
+  specialize (H (AST.prog_main p2)).
+
   exploit H.
-  apply Genv.find_def_symbol. exists b. split.
-  assumption. apply Genv.find_funct_ptr_iff. eassumption.
-  apply Genv.find_def_symbol. exists b0. split.
-  assumption. apply Genv.find_funct_ptr_iff. eassumption.
-  intros. inv H3. inv H5. destruct H6. inv H5.
+  - apply Genv.find_def_symbol. exists b. split.
+    + assumption.
+    + apply Genv.find_funct_ptr_iff. eassumption.
+  - apply Genv.find_def_symbol. exists b0. split.
+    + assumption.
+    + apply Genv.find_funct_ptr_iff. eassumption.
+  - crush.
 Qed.
 
 Definition match_prog' (p: RTL.program) (tp: HTL.program) :=