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.

1 files changed, 11 insertions, 1 deletions

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 36a28d9f..27f833d8 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,6 +58,7 @@ open Value2
 open Anf
 
 let opt_debug_function = ref ""
+let opt_debug_flow_graphs = ref false
 let opt_memo_cache = ref false
 
 (**************************************************************************)
@@ -1174,7 +1175,16 @@ and compile_def' n total ctx = function
        prerr_endline (Util.header header (List.length arg_ctyps + 2));
        prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs))
      else ();
-     
+
+     if !opt_debug_flow_graphs then
+       begin
+         let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
+         let cfg = Jib_ssa.ssa instrs in
+         let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
+         Jib_ssa.make_dot out_chan cfg;
+         close_out out_chan;
+       end;
+
      [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) ->