Add an -ir option to print the intermediate representation of a file

3 files changed, 28 insertions, 1 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 925c7fd9..14930d47 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -143,6 +143,9 @@ let initial_ctx env =
     iterate_size = false;
   }
 
+let initial_ctx_iterate env =
+  { (initial_ctx env) with iterate_size = true }
+
 let rec iterate_size ctx size n m =
   if size > 64 then
     CT_lint
@@ -3476,6 +3479,7 @@ let bytecode_ast ctx rewrites (Defs defs) =
     List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs
   in
   let cdefs = List.concat (List.rev chunks) in
+  let cdefs, ctx = specialize_variants ctx [] cdefs in
   rewrites cdefs
 
 let rec get_recursive_functions (Defs defs) =
diff --git a/src/c_backend.mli b/src/c_backend.mli
index 3b26acdf..4017130a 100644
--- a/src/c_backend.mli
+++ b/src/c_backend.mli
@@ -122,10 +122,13 @@ type ctx
    should be the environment returned by typechecking the full AST. *)
 val initial_ctx : Env.t -> ctx
 
+(** Same as initial ctx, but iterate to find more precise bounds on
+   integers. *)
+val initial_ctx_iterate : Env.t -> ctx
+
 (** Convert a typ to a IR ctyp *)
 val ctyp_of_typ : ctx -> Ast.typ -> ctyp
 
-
 val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list
 
 val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/sail.ml b/src/sail.ml
index aad7097f..77f0e32d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -61,6 +61,7 @@ let opt_print_verbose = ref false
 let opt_print_lem = ref false
 let opt_print_ocaml = ref false
 let opt_print_c = ref false
+let opt_print_ir = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
 let opt_print_cgen = ref false
@@ -128,6 +129,9 @@ let options = Arg.align ([
   ( "-latex_full_valspecs",
     Arg.Clear Latex.opt_simple_val,
     " print full valspecs in LaTeX output");
+  ( "-ir",
+    Arg.Set opt_print_ir,
+    " print intermediate representation");
   ( "-c",
     Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
     " output a C translated version of the input");
@@ -440,6 +444,22 @@ let main() =
          C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c;
          close_out output_chan
        else ());
+      (if !(opt_print_ir)
+       then
+         let ast_c = rewrite_ast_c type_envs ast in
+         let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+         let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in
+         let output_chan =
+           match !opt_file_out with
+           | Some f -> Util.opt_colors := false; open_out (f ^ ".ir.sail")
+           | None -> stdout
+         in
+         Util.opt_warnings := true;
+         let cdefs = C_backend.(bytecode_ast (initial_ctx_iterate type_envs) (List.map flatten_cdef) ast_c) in
+         let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Bytecode_util.pp_cdef cdefs) in
+         output_string output_chan (str ^ "\n");
+         close_out output_chan
+       else ());
       (if !(opt_print_cgen)
        then Cgen_backend.output type_envs ast
        else ());