aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2019-05-31 19:15:19 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-06-06 10:58:13 +0200
commit8e3a73448c5ddfa4be3871d7f4fd80281a7549f4 (patch)
tree1d2faaa30db1d4c8d7e236f7ddfbd145d778e6e3 /extraction
parent0025c4db576dbc174946b7adb83d4e0b81ce4b5f (diff)
downloadcompcert-kvx-8e3a73448c5ddfa4be3871d7f4fd80281a7549f4.tar.gz
compcert-kvx-8e3a73448c5ddfa4be3871d7f4fd80281a7549f4.zip
If-conversion optimization
Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 15a64d89..c0286f7b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -72,6 +72,7 @@ Extract Constant Iteration.GenIter.iterate =>
(* Selection *)
Extract Constant Selection.compile_switch => "Switchaux.compile_switch".
+Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic".
(* RTLgen *)
Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".