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 /backend/DuplicateOpcodeHeuristic.mli | |
| parent | e11a1b3ccac5cb60472ad507a71b0600ac3b5f8f (diff) | |
| download | compcert-kvx-26775340b173fd631e850f0a553ddab25c934fbc.tar.gz compcert-kvx-26775340b173fd631e850f0a553ddab25c934fbc.zip | |
Stub for opcode heuristic
Diffstat (limited to 'backend/DuplicateOpcodeHeuristic.mli')
| -rw-r--r-- | backend/DuplicateOpcodeHeuristic.mli | 10 |
1 files changed, 10 insertions, 0 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 |