diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:45:42 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:45:42 +0200 |
| commit | 63915fbebe707cc1de7c0ed5a24148cac45a742c (patch) | |
| tree | da503cba224f14281a2ee841930b8843459cb42b /arm/DuplicateOpcodeHeuristic.ml | |
| parent | f78d61faf3db94ac1704ce0d11291211b5307629 (diff) | |
| parent | e326ed9f28a2ed6869f0cb356ef9a8e189cb0a47 (diff) | |
| download | compcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.tar.gz compcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-thread
Diffstat (limited to 'arm/DuplicateOpcodeHeuristic.ml')
| -rw-r--r-- | arm/DuplicateOpcodeHeuristic.ml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml index 85505245..9b6a6409 100644 --- a/arm/DuplicateOpcodeHeuristic.ml +++ b/arm/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,22 @@ -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 + | 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 + |