Issue with ignoring the result of non-void builtin functions.

In RTL and beyond, the result of a builtin function that has return type different from "void" must be BR, never BR_none.  Otherwise, we get compile-time fatal errors, either in Asmexpand or in Lineartyping.

3 files changed, 20 insertions, 12 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index d818de58..3da961c6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -415,11 +415,12 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
       a1' :: convert_builtin_args al rl1
   end.
 
-Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) :=
-  match r with
-  | BR id => do r <- find_var map id; ret (BR r)
-  | BR_none => ret BR_none
-  | _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
+  match r, oty with
+  | BR id, _ => do r <- find_var map id; ret (BR r)
+  | BR_none, None => ret BR_none
+  | BR_none, Some _ => do r <- new_reg; ret (BR r)
+  | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
   end.
 
 (** Translation of an expression.  [transl_expr map a rd nd]
@@ -598,7 +599,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       let al := exprlist_of_expr_list (params_of_builtin_args args) in
       do rargs <- alloc_regs map al;
       let args' := convert_builtin_args args rargs in
-      do res' <- convert_builtin_res map res;
+      do res' <- convert_builtin_res map (sig_res (ef_sig ef)) res;
       do n1 <- add_instr (Ibuiltin ef args' res' nd);
          transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 559ab3a2..19f6f1f4 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -234,6 +234,7 @@ Proof.
   intros. inv H1; simpl.
 - eapply match_env_update_var; eauto.
 - auto.
+- eapply match_env_update_temp; eauto.
 Qed.
 
 (** Matching and [let]-bound variables. *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 41b5016f..1e665002 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro
       map.(map_vars)!id = Some r ->
       tr_builtin_res map (BR id) (BR r)
   | tr_builtin_res_none: forall map,
-      tr_builtin_res map BR_none BR_none.
+      tr_builtin_res map BR_none BR_none
+  | tr_builtin_res_fresh: forall map r,
+      ~reg_in_map map r ->
+      tr_builtin_res map BR_none (BR r).
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -1214,14 +1217,17 @@ Proof.
 Qed.
 
 Lemma convert_builtin_res_charact:
-  forall map res s res' s' INCR
-    (TR: convert_builtin_res map res s = OK res' s' INCR)
+  forall map oty res s res' s' INCR
+    (TR: convert_builtin_res map oty res s = OK res' s' INCR)
     (WF: map_valid map s),
   tr_builtin_res map res res'.
 Proof.
-  destruct res; simpl; intros; monadInv TR. 
-- constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- constructor.
+  destruct res; simpl; intros.
+- monadInv TR. constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
+- destruct oty; monadInv TR.
++ constructor. eauto with rtlg. 
++ constructor.
+- monadInv TR.
 Qed.
 
 Lemma transl_stmt_charact: