Opcode heuristic done for K1c

3 files changed, 33 insertions, 3 deletions

diff --git a/backend/DuplicateOpcodeHeuristic.mli b/backend/DuplicateOpcodeHeuristic.mli
index a4cc4848..b4c9f1ef 100644
--- a/backend/DuplicateOpcodeHeuristic.mli
+++ b/backend/DuplicateOpcodeHeuristic.mli
@@ -3,6 +3,8 @@
  * when selecting a trace.
  *)
 
+exception HeuristicSucceeded
+
 (* The bool reference should be updated to [true] if the condition is supposed
  * to hold, [false] if it is supposed to not hold
  * The function should raise HeuristicSucceeded if it succeeded to predict a branch,
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 1fecd0d9..a987d73f 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -261,7 +261,7 @@ let get_directions code entrypoint =
             do_loop_heuristic code ifso ifnot is_loop_header preferred;
             Printf.printf "Random choice for %d\n" (P.to_int n);
             preferred := Random.bool ()
-            with HeuristicSucceeded -> ()
+            with HeuristicSucceeded | DuplicateOpcodeHeuristic.HeuristicSucceeded -> ()
           ); directions := PTree.set n !preferred !directions
       | _ -> ()
     ) bfs_order;
diff --git a/mppa_k1c/DuplicateOpcodeHeuristic.ml b/mppa_k1c/DuplicateOpcodeHeuristic.ml
index fe9307f2..690553ce 100644
--- a/mppa_k1c/DuplicateOpcodeHeuristic.ml
+++ b/mppa_k1c/DuplicateOpcodeHeuristic.ml
@@ -1,4 +1,32 @@
 (* open Camlcoq *)
-(* open Op *)
+open Op
+open Integers
 
-let opcode_heuristic code cond ifso ifnot preferred = ()
+exception HeuristicSucceeded
+
+let opcode_heuristic code cond ifso ifnot preferred =
+  let decision = 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
+  in match decision with
+  | Some b -> (preferred := b; raise HeuristicSucceeded)
+  | None -> ()