diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-17 08:05:17 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-17 08:05:17 +0100 |
commit | 0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb (patch) | |
tree | e4c7b2fe161cfc3e963565f0e626e4b4f239d17f /powerpc/DuplicateOpcodeHeuristic.ml | |
parent | 2f19071e865181d9a0c2e61f5e57731fb86e4e5d (diff) | |
download | compcert-kvx-0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb.tar.gz compcert-kvx-0eb778a85b5b76ab6c7fd914ffaff1affcbde7bb.zip |
DuplicateOpcodeHeuristic ppc
Diffstat (limited to 'powerpc/DuplicateOpcodeHeuristic.ml')
-rw-r--r-- | powerpc/DuplicateOpcodeHeuristic.ml | 30 |
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 |