Give formal semantics to some built-in functions and run-time functions

This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
  list of values to values;
- interpret external calls to these functions according to this semantics
  (pure function from values to values, memory unchanged, no observable
  events in the trace);
- external calls to unknown built-in and run-time functions remain
  interpreted as generating observable events and possibly changing
  memory, like before.

The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).

Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
  of the target processor.  Currently, this is done for
  __builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
  library.  More precisely, the behavior of these functions is
  still axiomatized, but now it is specified using the more general
  machinery introduced in this commit, rather than ad-hoc axioms
  in backend/SplitLongproof.

The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86).  More built-ins will be
added later.

1 files changed, 47 insertions, 6 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 4154659c..c9771d99 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -24,7 +24,7 @@
 
 Require String.
 Require Import Coqlib Maps.
-Require Import AST Errors Integers Globalenvs Switch.
+Require Import AST Errors Integers Globalenvs Builtins Switch.
 Require Cminor.
 Require Import Op CminorSel Cminortyping.
 Require Import SelectOp SplitLong SelectLong SelectDiv.
@@ -162,6 +162,13 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.
 
+Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr :=
+   let (cond, args) := condition_of_expr cnd in
+   match SelectOp.select ty cond args ifso ifnot with
+   | Some a => a
+   | None => Econdition (condexpr_of_expr cnd) ifso ifnot
+   end.
+
 (** Conversion from Cminor expression to Cminorsel expressions *)
 
 Fixpoint sel_expr (a: Cminor.expr) : expr :=
@@ -231,6 +238,43 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
   | Some id => BR id
   end.
 
+(** Known builtin functions *)
+
+Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
+  match bf, args with
+  | BI_platform b, _ =>
+      SelectOp.platform_builtin b args
+  | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil =>
+      Some (sel_select ty a1 a2 a3)
+  | BI_standard BI_fabs, a1 ::: Enil =>
+      Some (SelectOp.absf a1)
+  | _, _ =>
+      None
+  end.
+
+(** Builtin functions in general *)
+
+Definition sel_builtin_default (optid: option ident) (ef: external_function)
+                               (args: list Cminor.expr) :=
+  Sbuiltin (sel_builtin_res optid) ef
+           (sel_builtin_args args (Machregs.builtin_constraints ef)).
+
+Definition sel_builtin (optid: option ident) (ef: external_function)
+                               (args: list Cminor.expr) :=
+  match optid, ef with
+  | Some id, 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
+          end
+      | None => sel_builtin_default optid ef args
+      end
+  | _, _ =>
+      sel_builtin_default optid ef args
+  end.
+
 (** Conversion of Cminor [switch] statements to decision trees. *)
 
 Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -342,13 +386,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :
       OK (match classify_call fn with
       | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
       | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
-      | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
-                                    (sel_builtin_args args
-                                       (Machregs.builtin_constraints ef))
+      | Call_builtin ef => sel_builtin optid ef args
       end)
   | Cminor.Sbuiltin optid ef args =>
-      OK (Sbuiltin (sel_builtin_res optid) ef
-                   (sel_builtin_args args (Machregs.builtin_constraints ef)))
+      OK (sel_builtin optid ef args)
   | Cminor.Stailcall sg fn args =>
       OK (match classify_call fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)