Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-work

Conflicts:
	configure
	mppa_k1c/Archi.v
	mppa_k1c/Asmexpand.ml

6 files changed, 81 insertions, 38 deletions

diff --git a/riscV/Archi.v b/riscV/Archi.v
index 3758d686..61d129d0 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for RISC-V *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -40,26 +40,33 @@ Qed.
    except the MSB, a.k.a. the quiet bit."
    Exceptions are operations manipulating signs. *)
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  false.                        (**r irrelevant *)
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  default_nan_64.
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  default_nan_32.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  false.                        (**r irrelevant *)
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
 
-Definition fpu_returns_default_qNaN := true.
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
+
+Definition fma_order {A: Type} (x y z: A) := (x, y, z).
+
+Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
+              fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
 
 (** Whether to generate position-independent code or not *)
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
new file mode 100644
index 00000000..f6e643d2
--- /dev/null
+++ b/riscV/Builtins1.v
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type := .
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+  nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with end.
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 0c981d11..a2087cb7 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -18,16 +18,13 @@
 open C
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list", TPtr(TVoid [], [])
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Synchronization *)
     "__builtin_fence",
       (TVoid [], [], false);
-    (* Integer arithmetic *)
-    "__builtin_bswap64",
-      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
     (* Float arithmetic *)
     "__builtin_fmadd",
       (TFloat(FDouble, []),
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index ba7c5664..e9920e46 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -44,11 +44,8 @@
 Require Archi.
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats Builtins.
+Require Import Op CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -461,3 +458,8 @@ Definition divf_base (e1: expr) (e2: expr) :=
 
 Definition divfs_base (e1: expr) (e2: expr) :=
   Eop Odivfs (e1 ::: e2 ::: Enil).
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 46cc1bbc..52a535fb 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -17,18 +17,10 @@
 
 (** Correctness of instruction selection for operators *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Zbits.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import Coqlib Zbits.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
@@ -941,7 +933,6 @@ Proof.
 - constructor; auto.
 Qed.
 
-
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
   forall le a b x y,
@@ -962,4 +953,17 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
+
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 92df7a76..64bcea4c 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -93,7 +93,7 @@ module Target : TARGET =
       | X0 -> output_string oc "x0"
       | X r -> ireg oc r
 
-    let preg oc = function
+    let preg_asm oc ty = function
       | IR r -> ireg oc r
       | FR r -> freg oc r
       | _    -> assert false
@@ -582,7 +582,7 @@ module Target : TARGET =
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+              print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false