aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/DuplicateOpcodeHeuristic.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-17 07:44:45 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-17 07:44:45 +0100
commitfac63511aaf3fd3c77db69802c24474559365879 (patch)
treeae966ab2c714ac5da1dc68ca6f24da2133558b55 /aarch64/DuplicateOpcodeHeuristic.ml
parent1b111e3658b3f79a9814fd9799e2dbe0a921c768 (diff)
downloadcompcert-kvx-fac63511aaf3fd3c77db69802c24474559365879.tar.gz
compcert-kvx-fac63511aaf3fd3c77db69802c24474559365879.zip
fix for aarch64 DuplicateOpcodeHeuristic.ml
Diffstat (limited to 'aarch64/DuplicateOpcodeHeuristic.ml')
-rw-r--r--aarch64/DuplicateOpcodeHeuristic.ml30
1 files changed, 27 insertions, 3 deletions
diff --git a/aarch64/DuplicateOpcodeHeuristic.ml b/aarch64/DuplicateOpcodeHeuristic.ml
index 85505245..5fc2156c 100644
--- a/aarch64/DuplicateOpcodeHeuristic.ml
+++ b/aarch64/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred = ()
+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 | Ccompfs c -> (match c with
+ | Ceq -> Some false
+ | Cne -> Some true
+ | _ -> None
+ )
+ | Cnotcompf c | Cnotcompfs c -> (match c with
+ | Ceq -> Some true
+ | Cne -> Some false
+ | _ -> None
+ )
+ | _ -> None
+