diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-19 11:24:03 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-26 18:48:06 +0200 |
commit | a9a07e3b672711f74bde27bd72b518631e3a29b4 (patch) | |
tree | b5b030434252a437697e658965f259cc598b1c8c /cparser/Rename.mli | |
parent | 0a09a4fd81e911ae11ec7126c84c58dc10ce4daf (diff) | |
download | compcert-conditional-move.tar.gz compcert-conditional-move.zip |
If-conversion optimization for Cminorconditional-move
Add an experimental pass that converts some if/then/else statements
into "select" built-ins, 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.
To support the optimization, I added a type inference and type checking
pass for Cminor, in backend/Cminortyping.v. The inferred type information
is used to determine the type at which the "select" built-in operates,
and to prove semantic preservation.
Diffstat (limited to 'cparser/Rename.mli')
0 files changed, 0 insertions, 0 deletions