aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-17 08:05:17 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-17 08:05:17 +0100
commit0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb (patch)
treee4c7b2fe161cfc3e963565f0e626e4b4f239d17f /powerpc
parent2f19071e865181d9a0c2e61f5e57731fb86e4e5d (diff)
downloadcompcert-kvx-0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb.tar.gz
compcert-kvx-0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb.zip
DuplicateOpcodeHeuristic ppc
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/DuplicateOpcodeHeuristic.ml30
1 files changed, 27 insertions, 3 deletions
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
index 85505245..33be79e8 100644
--- a/powerpc/DuplicateOpcodeHeuristic.ml
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+ match cond with
+ | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+ | Clt | Cle -> Some false
+ | Cgt | Cge -> Some true
+ | _ -> None
+ ) else None
+ | Ccompf c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None