summaryrefslogtreecommitdiff
path: root/src/initial_check.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-03-13 14:26:59 +0000
committerAlasdair Armstrong2019-03-13 15:01:30 +0000
commitec8cad1daa76fb265014d3d313173905925c9922 (patch)
treef8daf3918a8c4ed2fec58edf6c244933c1748f33 /src/initial_check.ml
parentee54fe8fc8a4afc8fb9f6cc0bd8e2930162f49ad (diff)
C: Improve Jib IR, add SSA representation
Add a CL_void l-expression so we don't have redundant unit-typed variables everywhere, and add an optimization in Jib_optimize called optimize_unit which introduces these. Remove the basic control-flow graph in Jib_util and add a new mutable control-flow graph type in Jib_ssa which allows the IR to be converted into SSA form. The mutable graph allows for more efficient updates, and includes both back and forwards references making it much more convenient to traverse. Having an SSA representation should make some optimizations much simpler, and is also probably more natural for SMT generation where variables have to be defined once using declare-const anyway. Debug option -ddump_flow_graphs now outputs SSA'd graphs of the functions in a specification.
Diffstat (limited to 'src/initial_check.ml')
0 files changed, 0 insertions, 0 deletions