Eliminate known builtins whose result is ignored

A typical example is `(void) __builtin_sel(a, b, c)`.

It is safe to generate zero code for these uses of builtins
because builtins whose semantics are known to the compiler
are pure.  Other builtins with side effects (e.g. `__builtin_trap`)
are not known and will remain in the compiled code.

It is useful to generate zero code for these uses of builtins
because some of them (e.g. `__builtin_sel`) must be transformed
into proper CminorSel expressions during instruction selection.
Otherwise, they propagate all the way to ExpandAsm, causing
a "not implemented" error there.

1 files changed, 15 insertions, 6 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index c9771d99..480b09a2 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -252,6 +252,10 @@ Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
       None
   end.
 
+(** A CminorSel statement that does nothing, like [Sskip], but reduces. *)
+
+Definition Sno_op := Sseq Sskip Sskip.
+
 (** Builtin functions in general *)
 
 Definition sel_builtin_default (optid: option ident) (ef: external_function)
@@ -261,17 +265,22 @@ Definition sel_builtin_default (optid: option ident) (ef: external_function)
 
 Definition sel_builtin (optid: option ident) (ef: external_function)
                                (args: list Cminor.expr) :=
-  match optid, ef with
-  | Some id, EF_builtin name sg =>
+  match ef with
+  | EF_builtin name sg =>
       match lookup_builtin_function name sg with
       | Some bf =>
-          match sel_known_builtin bf (sel_exprlist args) with
-          | Some a => Sassign id a
-          | None => sel_builtin_default optid ef args
+          match optid with
+          | Some id =>
+              match sel_known_builtin bf (sel_exprlist args) with
+              | Some a => Sassign id a
+              | None => sel_builtin_default optid ef args
+              end
+          | None =>
+              Sno_op   (**r builtins with semantics are pure *)
           end
       | None => sel_builtin_default optid ef args
       end
-  | _, _ =>
+  | _ =>
       sel_builtin_default optid ef args
   end.