aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/SelectOp.vp4
-rw-r--r--backend/Selectionaux.ml5
-rw-r--r--backend/SplitLongproof.v6
-rw-r--r--driver/Driver.ml4
-rw-r--r--extraction/extraction.v5
-rw-r--r--mppa_k1c/Archi.v36
-rw-r--r--mppa_k1c/Builtins1.v33
-rw-r--r--mppa_k1c/SelectOp.vp3
-rw-r--r--powerpc/SelectOp.vp15
-rw-r--r--powerpc/SelectOpproof.v3
-rw-r--r--riscV/SelectOp.vp4
-rw-r--r--riscV/SelectOpproof.v5
-rw-r--r--x86/SelectOp.vp7
-rw-r--r--x86/SelectOpproof.v5
14 files changed, 68 insertions, 67 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index ed4c2c95..5506157c 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -516,16 +516,14 @@ Nondetfunction builtin_arg (e: expr) :=
| _ => BA e
end.
-<<<<<<< HEAD
(* floats *)
Definition divf_base (e1: expr) (e2: expr) :=
Eop Odivf (e1 ::: e2 ::: Enil).
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.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 60a1eccd..574c31f0 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -96,17 +96,12 @@ If-conversion seems beneficial if:
Intuition: on a modern processor, the "then" and the "else" branches
can generally be computed in parallel, there is enough ILP for that.
So, the bad case is if the most taken branch is much cheaper than the
-<<<<<<< HEAD
-other branch. Since our cost estimates are very imprecise, the
-bound on the total cost acts as a safety guard,
-=======
other branch. Another bad case is if both branches are big: since the
code for one branch precedes entirely the code for the other branch,
if the first branch contains a lot of instructions,
dynamic reordering of instructions will not look ahead far enough
to execute instructions from the other branch in parallel with
instructions from the first branch.
->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
*)
let if_conversion_heuristic cond ifso ifnot ty =
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index df77b322..b13bd1f7 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -23,8 +23,6 @@ Require Import SelectOp SelectOpproof SplitLong.
Local Open Scope cminorsel_scope.
Local Open Scope string_scope.
-<<<<<<< HEAD
-=======
(** * Properties of the helper functions *)
Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
@@ -47,7 +45,6 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F)
/\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l
/\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
(** * Correctness of the instruction selection functions for 64-bit operators *)
Section CMCONSTR.
@@ -60,10 +57,7 @@ Variable sp: val.
Variable e: env.
Variable m: mem.
-<<<<<<< HEAD
Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
-=======
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
Lemma eval_helper:
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 05d51402..288bb436 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -258,11 +258,7 @@ let dump_mnemonics destfile =
let optimization_options = [
option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
-<<<<<<< HEAD
option_fpostpass; option_fredundancy; option_finline_functions_called_once;
-=======
- option_fredundancy; option_finline; option_finline_functions_called_once;
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
]
let set_all opts () = List.iter (fun r -> r := true) opts
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 5a1ca0be..caf4330b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -34,11 +34,6 @@ Require Clight.
Require Compiler.
Require Parser.
Require Initializers.
-<<<<<<< HEAD
-Require Int31.
-Require Asmaux.
-=======
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
(* Standard lib *)
Require Import ExtrOcamlBasic.
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 113f5d51..800c9fe5 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/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.
@@ -34,6 +34,8 @@ Proof.
unfold splitlong. destruct ptr64; simpl; congruence.
Qed.
+(** THIS IS NOT CHECKED ! NONE OF THIS ! *)
+
(** Section 7.3: "Except when otherwise stated, if the result of a
floating-point operation is NaN, it is the canonical NaN. The
canonical NaN has a positive sign and all significand bits clear
@@ -41,26 +43,36 @@ Qed.
We need to extend the [choose_binop_pl] functions to account for
this case. *)
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
- exist _ (B754_nan 53 1024 true (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 always choose first NaN *)
+(* Always choose the first NaN argument, if any *)
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
- exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+ match l with nil => default_nan_64 | n :: _ => n end.
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
- false. (**r always choose first NaN *)
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+ match l with nil => default_nan_32 | n :: _ => n end.
-(* TODO check *)
Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_64_idem: forall n,
+ choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
+
+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, z, y).
+
+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
+ 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/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v
new file mode 100644
index 00000000..f6e643d2
--- /dev/null
+++ b/mppa_k1c/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/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3df0c682..688820b3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -54,6 +54,7 @@ Require Import OpHelpers.
Require Import ExtValues.
Require Import DecBoolOps.
Require Import Chunks.
+Require Import Builtins.
Require Compopts.
Local Open Scope cminorsel_scope.
@@ -673,6 +674,8 @@ Definition divfs_base (e1: expr) (e2: expr) :=
Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).
End SELECT.
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+ None.
(* Local Variables: *)
(* mode: coq *)
(* End: *) \ No newline at end of file
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 07c325c1..50b1bdd6 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -38,17 +38,8 @@
Require Import Coqlib.
Require Import Compopts.
-<<<<<<< HEAD
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
-Require Import OpHelpers.
-=======
Require Import AST Integers Floats Builtins.
-Require Import Op CminorSel.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
+Require Import Op OpHelpers CminorSel.
Require Archi.
Local Open Scope cminorsel_scope.
@@ -573,16 +564,14 @@ Nondetfunction builtin_arg (e: expr) :=
| _ => BA e
end.
-<<<<<<< HEAD
(* floats *)
Definition divf_base (e1: expr) (e2: expr) :=
Eop Odivf (e1 ::: e2 ::: Enil).
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.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 3e34244d..63066135 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -1062,7 +1062,6 @@ Proof.
- constructor; auto.
Qed.
-<<<<<<< HEAD
(* floating-point division without HELPERS *)
Theorem eval_divf_base:
forall le a b x y,
@@ -1083,7 +1082,7 @@ Proof.
intros; unfold divfs_base.
TrivialExists.
Qed.
-=======
+
(** Platform-specific known builtins *)
Theorem eval_platform_builtin:
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 23235d95..e9920e46 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -452,16 +452,14 @@ Nondetfunction builtin_arg (e: expr) :=
| _ => BA e
end.
-<<<<<<< HEAD
(* floats *)
Definition divf_base (e1: expr) (e2: expr) :=
Eop Odivf (e1 ::: e2 ::: Enil).
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.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index ca271342..52a535fb 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -933,8 +933,6 @@ Proof.
- constructor; auto.
Qed.
-<<<<<<< HEAD
-
(* floating-point division without HELPERS *)
Theorem eval_divf_base:
forall le a b x y,
@@ -955,7 +953,7 @@ Proof.
intros; unfold divfs_base.
TrivialExists.
Qed.
-=======
+
(** Platform-specific known builtins *)
Theorem eval_platform_builtin:
@@ -968,5 +966,4 @@ Proof.
intros. discriminate.
Qed.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
End CMCONSTR.
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index d734ecc6..a23c37d5 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,11 +40,8 @@ Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats Builtins.
Require Import Op CminorSel.
-<<<<<<< HEAD
Require Import OpHelpers.
-=======
Require Archi.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
Local Open Scope cminorsel_scope.
@@ -580,16 +577,14 @@ Nondetfunction builtin_arg (e: expr) :=
| _ => BA e
end.
-<<<<<<< HEAD
(* floats *)
Definition divf_base (e1: expr) (e2: expr) :=
Eop Odivf (e1 ::: e2 ::: Enil).
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.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index b59f4a87..5703c758 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -1016,8 +1016,6 @@ Proof.
- constructor; auto.
Qed.
-<<<<<<< HEAD
-
(* floating-point division without HELPERS *)
Theorem eval_divf_base:
forall le a b x y,
@@ -1038,7 +1036,7 @@ Proof.
intros; unfold divfs_base.
TrivialExists.
Qed.
-=======
+
(** Platform-specific known builtins *)
Theorem eval_platform_builtin:
@@ -1051,5 +1049,4 @@ Proof.
intros. discriminate.
Qed.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
End CMCONSTR.
generated by cgit (git 2.34.1) at 2024-05-20 09:43:20 +0000