diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
| commit | 4c379d48b35e7c8156f3953fede31d5e47faf8ca (patch) | |
| tree | fa19eb30178fcf74b0768d9f5df4017ab6afc770 /backend | |
| parent | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (diff) | |
| download | compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.tar.gz compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.zip | |
helpers broke compilation
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Selectionaux.ml | 5 | ||||
| -rw-r--r-- | backend/SplitLongproof.v | 6 |
2 files changed, 0 insertions, 11 deletions
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: |