diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-12-16 16:03:12 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-12-16 16:03:12 +0100 |
| commit | 26775340b173fd631e850f0a553ddab25c934fbc (patch) | |
| tree | 8c952f60bc6cd750c44c340e2d7e2a938040e3cc | |
| parent | e11a1b3ccac5cb60472ad507a71b0600ac3b5f8f (diff) | |
| download | compcert-kvx-26775340b173fd631e850f0a553ddab25c934fbc.tar.gz compcert-kvx-26775340b173fd631e850f0a553ddab25c934fbc.zip | |
Stub for opcode heuristic
| -rw-r--r-- | backend/DuplicateOpcodeHeuristic.mli | 10 | ||||
| -rw-r--r-- | backend/Duplicateaux.ml | 6 | ||||
| -rw-r--r-- | mppa_k1c/DuplicateOpcodeHeuristic.ml | 4 |
3 files changed, 16 insertions, 4 deletions
diff --git a/backend/DuplicateOpcodeHeuristic.mli b/backend/DuplicateOpcodeHeuristic.mli new file mode 100644 index 00000000..a4cc4848 --- /dev/null +++ b/backend/DuplicateOpcodeHeuristic.mli @@ -0,0 +1,10 @@ +(** Define opcode heuristics used for the instruction duplication oracle + * In particular, it is used to figure out which "branch" should be privileged + * when selecting a trace. + *) + +(* 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, + * and do nothing otherwise *) +val opcode_heuristic : RTL.code -> Op.condition -> RTL.node -> RTL.node -> bool ref -> unit diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 71f44776..1fecd0d9 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -211,9 +211,7 @@ let do_call_heuristic code ifso ifnot is_loop_header preferred = (preferred := true; raise HeuristicSucceeded) else () -let do_opcode_heuristic code cond ifso ifnot is_loop_header preferred = () - (* TODO - the condition is architecture dependent, so each archi should - have a heuristic function in its folder *) +let do_opcode_heuristic code cond ifso ifnot preferred = DuplicateOpcodeHeuristic.opcode_heuristic code cond ifso ifnot preferred let do_return_heuristic code ifso ifnot is_loop_header preferred = let predicate n = (function @@ -257,7 +255,7 @@ let get_directions code entrypoint = let preferred = ref false in (try do_call_heuristic code ifso ifnot is_loop_header preferred; - do_opcode_heuristic code cond ifso ifnot is_loop_header preferred; + do_opcode_heuristic code cond ifso ifnot preferred; do_return_heuristic code ifso ifnot is_loop_header preferred; do_store_heuristic code ifso ifnot is_loop_header preferred; do_loop_heuristic code ifso ifnot is_loop_header preferred; diff --git a/mppa_k1c/DuplicateOpcodeHeuristic.ml b/mppa_k1c/DuplicateOpcodeHeuristic.ml new file mode 100644 index 00000000..fe9307f2 --- /dev/null +++ b/mppa_k1c/DuplicateOpcodeHeuristic.ml @@ -0,0 +1,4 @@ +(* open Camlcoq *) +(* open Op *) + +let opcode_heuristic code cond ifso ifnot preferred = () |