Merge branch 'sail2' into rmem_interpreter

1 files changed, 77 insertions, 36 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index aff2d49e..ab388223 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -61,6 +61,7 @@ open Anf
 module Big_int = Nat_big_num
 
 let c_verbosity = ref 0
+
 let opt_debug_flow_graphs = ref false
 let opt_debug_function = ref ""
 let opt_trace = ref false
@@ -68,6 +69,20 @@ let opt_smt_trace = ref false
 let opt_static = ref false
 let opt_no_main = ref false
 let opt_memo_cache = ref false
+let opt_no_rts = ref false
+let opt_prefix = ref "z"
+let opt_extra_params = ref None
+let opt_extra_arguments = ref None
+
+let extra_params () =
+  match !opt_extra_params with
+  | Some str -> str ^ ", "
+  | _ -> ""
+
+let extra_arguments is_extern =
+  match !opt_extra_arguments with
+  | Some str when not is_extern -> str ^ ", "
+  | _ -> ""
 
 (* Optimization flags *)
 let optimize_primops = ref false
@@ -90,8 +105,8 @@ let zencode_id = function
 (* 2. Converting sail types to C types                                    *)
 (**************************************************************************)
 
-let max_int64 = Big_int.of_int64 Int64.max_int
-let min_int64 = Big_int.of_int64 Int64.min_int
+let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1))
+let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1))
 
 (** The context type contains two type-checking
    environments. ctx.local_env contains the closest typechecking
@@ -111,6 +126,7 @@ type ctx =
     recursive_functions : IdSet.t;
     no_raw : bool;
     optimize_smt : bool;
+    iterate_size : bool;
   }
 
 let initial_ctx env =
@@ -124,8 +140,17 @@ let initial_ctx env =
     recursive_functions = IdSet.empty;
     no_raw = false;
     optimize_smt = true;
+    iterate_size = false;
   }
 
+let rec iterate_size ctx size n m =
+  if size > 64 then
+    CT_lint
+  else if prove __POS__ ctx.local_env (nc_and (nc_lteq (nconstant (min_int size)) n) (nc_lteq m (nconstant (max_int size)))) then
+    CT_fint size
+  else
+    iterate_size ctx (size + 1) n m
+
 (** Convert a sail type into a C-type. This function can be quite
    slow, because it uses ctx.local_env and SMT to analyse the Sail
    types and attempts to fit them into the smallest possible C
@@ -151,10 +176,15 @@ let rec ctyp_of_typ ctx typ =
      | Some (kids, constr, n, m) ->
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
-             when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
-           CT_fint 64
+             when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
+           if ctx.iterate_size then
+             iterate_size ctx 2 (nconstant n) (nconstant m)
+           else
+             CT_fint 64
         | n, m when ctx.optimize_smt ->
-           if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
+           if ctx.iterate_size then
+             iterate_size ctx 2 n m
+           else if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
              CT_fint 64
            else
              CT_lint
@@ -264,7 +294,7 @@ let hex_char =
 
 let literal_to_fragment (L_aux (l_aux, _) as lit) =
   match l_aux with
-  | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
+  | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
      Some (F_lit (V_int n), CT_fint 64)
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
@@ -544,9 +574,9 @@ let analyze_primop' ctx id args typ =
      | Some (kids, constr, n, m) ->
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
-               when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
+               when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
            AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
-        | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
+        | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
            AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
         | _ -> no_change
      end
@@ -717,7 +747,7 @@ let rec chunkify n xs =
 let rec compile_aval l ctx = function
   | AV_C_fragment (frag, typ, ctyp) ->
      let ctyp' = ctyp_of_typ ctx typ in
-     if not (ctyp_equal ctyp ctyp') then
+     if not (ctyp_equal ctyp ctyp' || ctx.iterate_size) then
        raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp'));
      [], (frag, ctyp_of_typ ctx typ), []
 
@@ -737,7 +767,7 @@ let rec compile_aval l ctx = function
   | AV_lit (L_aux (L_string str, _), typ) ->
      [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), []
 
-  | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
+  | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
      let gs = gensym () in
      [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
      (F_id gs, CT_lint),
@@ -941,8 +971,7 @@ let compile_funcall l ctx id args typ =
     ifuncall clexp id setup_args
   else
     let gs = gensym () in
-    iblock [icomment "copy call";
-            idecl ret_ctyp gs;
+    iblock [idecl ret_ctyp gs;
             ifuncall (CL_id (gs, ret_ctyp)) id setup_args;
             icopy l clexp (F_id gs, ret_ctyp);
             iclear ret_ctyp gs]
@@ -2405,7 +2434,8 @@ let optimize ctx cdefs =
   |> (if !optimize_alias then concatMap unique_names else nothing)
   |> (if !optimize_alias then concatMap (remove_alias ctx) else nothing)
   |> (if !optimize_alias then concatMap (combine_variables ctx) else nothing)
-  |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing)
+  (* We need the runtime to initialize hoisted allocations *)
+  |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations ctx) else nothing)
   |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap (hoist_alias ctx) else nothing)
 
 (**************************************************************************)
@@ -2415,6 +2445,12 @@ let optimize ctx cdefs =
 let sgen_id id = Util.zencode_string (string_of_id id)
 let codegen_id id = string (sgen_id id)
 
+let sgen_function_id id =
+  let str = Util.zencode_string (string_of_id id) in
+  !opt_prefix ^ String.sub str 1 (String.length str - 1)
+
+let codegen_function_id id = string (sgen_function_id id)
+
 let rec sgen_ctyp = function
   | CT_unit -> "unit"
   | CT_bit -> "fbits"
@@ -2564,13 +2600,14 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_funcall (x, extern, f, args) ->
      let c_args = Util.string_of_list ", " sgen_cval args in
      let ctyp = clexp_ctyp x in
+     let is_extern = Env.is_extern f ctx.tc_env "c" || extern in
      let fname =
        if Env.is_extern f ctx.tc_env "c" then
          Env.get_extern f ctx.tc_env "c"
        else if extern then
          string_of_id f
        else
-         sgen_id f
+         sgen_function_id f
      in
      let fname =
        match fname, ctyp with
@@ -2625,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
          string (Printf.sprintf  "  COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
      else
        if is_stack_ctyp ctyp then
-         string (Printf.sprintf "  %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
+         string (Printf.sprintf "  %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args)
        else
-         string (Printf.sprintf "  %s(%s, %s);" fname (sgen_clexp x) c_args)
+         string (Printf.sprintf "  %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args)
 
   | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
      empty
@@ -2843,7 +2880,7 @@ let codegen_type_def ctx = function
          in
          Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty
        in
-       string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
+       string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
        ^^ surround 2 0 lbrace
                    (tuple
                     ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline
@@ -2994,7 +3031,7 @@ let codegen_list_set id ctyp =
 
 let codegen_cons id ctyp =
   let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in
-  string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+  string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
   ^^ string (Printf.sprintf "  *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = x;\n"
@@ -3159,9 +3196,9 @@ let codegen_def' ctx = function
      if Env.is_extern id ctx.tc_env "c" then
        empty
      else if is_stack_ctyp ret_ctyp then
-       string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
      else
-       string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
      if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -3202,12 +3239,12 @@ let codegen_def' ctx = function
        | None ->
           assert (is_stack_ctyp ret_ctyp);
           (if !opt_static then string "static " else empty)
-          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
+          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline
        | Some gs ->
           assert (not (is_stack_ctyp ret_ctyp));
           (if !opt_static then string "static " else empty)
-          ^^ string "void" ^^ space ^^ codegen_id id
-          ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
+          ^^ string "void" ^^ space ^^ codegen_function_id id
+          ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
           ^^ hardline
      in
      function_header
@@ -3220,7 +3257,7 @@ let codegen_def' ctx = function
 
   | CDEF_startup (id, instrs) ->
      let static = if !opt_static then "static " else "" in
-     let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_id id)) in
+     let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in
      separate_map hardline codegen_decl instrs
      ^^ twice hardline
      ^^ startup_header ^^ hardline
@@ -3230,7 +3267,7 @@ let codegen_def' ctx = function
 
   | CDEF_finish (id, instrs) ->
      let static = if !opt_static then "static " else "" in
-     let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_id id)) in
+     let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in
      separate_map hardline codegen_decl (List.filter is_decl instrs)
      ^^ twice hardline
      ^^ finish_header ^^ hardline
@@ -3484,7 +3521,7 @@ let smt_trace ctx =
 
   | cdef -> cdef
 
-let compile_ast ctx c_includes (Defs defs) =
+let compile_ast ctx output_chan c_includes (Defs defs) =
   try
     c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions"));
     let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in
@@ -3521,9 +3558,10 @@ let compile_ast ctx c_includes (Defs defs) =
     let docs = List.map (codegen_def ctx) cdefs in
 
     let preamble = separate hardline
-                     ([ string "#include \"sail.h\"";
-                        string "#include \"rts.h\"";
-                        string "#include \"elf.h\"" ]
+                     ([ string "#include \"sail.h\"" ]
+                      @ (if !opt_no_rts then [] else
+                           [ string "#include \"rts.h\"";
+                             string "#include \"elf.h\"" ])
                       @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes))
     in
 
@@ -3567,7 +3605,7 @@ let compile_ast ctx c_includes (Defs defs) =
        @ fst exn_boilerplate
        @ startup cdefs
        @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
-       @ (if regs = [] then [] else [ "  zinitializze_registers(UNIT);" ])
+       @ (if regs = [] then [] else [ Printf.sprintf "  %s(UNIT);" (sgen_function_id (mk_id "initialize_registers")) ])
        @ letbind_initializers
        @ [ "}" ] ))
     in
@@ -3588,7 +3626,7 @@ let compile_ast ctx c_includes (Defs defs) =
            "{";
            "  model_init();";
            "  if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
-           "  zmain(UNIT);";
+           Printf.sprintf "  %s(UNIT);" (sgen_function_id (mk_id "main"));
            "  model_fini();";
            "  return EXIT_SUCCESS;";
            "}" ] )
@@ -3604,10 +3642,13 @@ let compile_ast ctx c_includes (Defs defs) =
     let hlhl = hardline ^^ hardline in
 
     Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl
-                                 ^^ model_init ^^ hlhl
-                                 ^^ model_fini ^^ hlhl
-                                 ^^ model_default_main ^^ hlhl
-                                 ^^ model_main)
-    |> print_endline
+                                 ^^ (if not !opt_no_rts then
+                                       model_init ^^ hlhl
+                                       ^^ model_fini ^^ hlhl
+                                       ^^ model_default_main ^^ hlhl
+                                     else
+                                       empty)
+                                 ^^ model_main ^^ hardline)
+    |> output_string output_chan
   with
     Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)