Fix bug with loop indices not being mapped to int64 in C

This should fix the issue in cheri128

Also introduce a feature to more easily debug the C backend:

sail -dfunction Name

will pretty-print the ANF and IR representation of just the Name
function. I want to make this work for the type-checker as well, but
it's a bit hard to get that to not fire during re-writing passes right
now.

7 files changed, 102 insertions, 15 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 4e1bde7e..0c4ae87d 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -61,7 +61,8 @@ open Anf
 module Big_int = Nat_big_num
 
 let c_verbosity = ref 0
-let opt_ddump_flow_graphs = ref false
+let opt_debug_flow_graphs = ref false
+let opt_debug_function = ref ""
 let opt_trace = ref false
 let opt_static = ref false
 let opt_no_main = ref false
@@ -357,6 +358,8 @@ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
        let aexp2 = analyze_functions ctx f aexp2 in
        let aexp3 = analyze_functions ctx f aexp3 in
        let aexp4 = analyze_functions ctx f aexp4 in
+       (* Currently we assume that loop indexes are always safe to put into an int64 *)
+       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_int64) ctx.locals } in
        AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
 
     | AE_case (aval, cases, typ) ->
@@ -1227,14 +1230,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
-     (* This is a bit of a hack, we force loop_var to be CT_int64 by
-        forcing it's type to be a known nexp that will map to
-        CT_int64. *)
-     let make_small _ _ = function
-       | AV_id (id, Local (Immutable, typ)) when Id.compare id loop_var = 0 -> AV_id (id, Local (Immutable, atom_typ (nint 0)))
-       | aval -> aval
-     in
-     let body = map_aval make_small body in
+     (* We assume that all loop indices are safe to put in a CT_int64. *)
+     let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_int64) ctx.locals } in
 
      let is_inc = match ord with
        | Ord_inc -> true
@@ -1573,7 +1570,18 @@ let rec compile_def ctx = function
      let aexp = no_shadow (pat_ids pat) (anf exp) in
      c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp)));
      let aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) in
-     c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp)));
+
+     if Id.compare (mk_id !opt_debug_function) id = 0 then
+       let header =
+         Printf.sprintf "Sail ANF for %s %s %s. (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id)
+                        (string_of_typquant quant)
+                        Util.(string_of_list ", " (fun typ -> string_of_typ typ |> yellow |> clear) arg_typs)
+                        Util.(string_of_typ ret_typ |> yellow |> clear)
+
+       in
+       prerr_endline (Util.header header (List.length arg_typs + 2));
+       prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp))
+     else ();
 
      (* Compile the function arguments as patterns. *)
      let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in
@@ -2779,9 +2787,7 @@ let codegen_def' ctx = function
        string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
-     if !opt_ddump_flow_graphs then make_dot id (instrs_graph instrs) else ();
-
-     c_debug (lazy (Pretty_print_sail.to_string (separate_map hardline pp_instr instrs)));
+     if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
 
      (* Extract type information about the function from the environment. *)
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
@@ -2800,6 +2806,18 @@ let codegen_def' ctx = function
                                  ^ Util.string_of_list ", " string_of_ctyp arg_ctyps)
      else ();
 
+     (* If this function is set as opt_debug_function, then output its IR *)
+     if Id.compare (mk_id !opt_debug_function) id = 0 then
+       let header =
+         Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id)
+                        (Util.string_of_list ", " string_of_id args)
+                        (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps)
+                        Util.(string_of_ctyp ret_ctyp |> yellow |> clear)
+       in
+       prerr_endline (Util.header header (List.length arg_ctyps + 2));
+       prerr_endline (Pretty_print_sail.to_string (separate_map hardline pp_instr instrs))
+     else ();
+
      let instrs = add_local_labels instrs in
      let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in
      let function_header =
diff --git a/src/c_backend.mli b/src/c_backend.mli
index 170c5bd9..6048f6b6 100644
--- a/src/c_backend.mli
+++ b/src/c_backend.mli
@@ -53,7 +53,8 @@ open Type_check
 
 (** Global compilation options *)
 
-val opt_ddump_flow_graphs : bool ref
+val opt_debug_flow_graphs : bool ref
+val opt_debug_function : string ref
 val opt_trace : bool ref
 val opt_static : bool ref
 val opt_no_main : bool ref
diff --git a/src/sail.ml b/src/sail.ml
index 4fd35902..3505ecf4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -223,7 +223,7 @@ let options = Arg.align ([
     Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
     "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
   ( "-ddump_flow_graphs",
-    Arg.Set C_backend.opt_ddump_flow_graphs,
+    Arg.Set C_backend.opt_debug_flow_graphs,
     " (debug) dump flow analysis for Sail functions when compiling to C");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
@@ -237,6 +237,9 @@ let options = Arg.align ([
   ( "-dmagic_hash",
     Arg.Set Initial_check.opt_magic_hash,
     " (debug) allow special character # in identifiers");
+  ( "-dfunction",
+    Arg.String (fun f -> C_backend.opt_debug_function := f),
+    " (debug) print debugging output for a single function");
   ( "-Xconstraint_synonyms",
     Arg.Set Type_check.opt_constraint_synonyms,
     " (extension) allow constraint synonyms");
diff --git a/src/util.ml b/src/util.ml
index c0b88815..2e121a4f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -455,3 +455,5 @@ let warn str =
 
 let log_line str line msg =
   "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg
+
+let header str n = "\n" ^ str ^ "\n" ^ String.make (String.length str - 9 * n) '='
diff --git a/src/util.mli b/src/util.mli
index 5bb7c559..1d80bc10 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -260,3 +260,4 @@ val zencode_string : string -> string
 val zencode_upper_string : string -> string
 
 val log_line : string -> int -> string -> string
+val header : string -> int -> string
diff --git a/test/c/cheri128_hsb.expect b/test/c/cheri128_hsb.expect
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/c/cheri128_hsb.expect
diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail
new file mode 100644
index 00000000..a06a2ad2
--- /dev/null
+++ b/test/c/cheri128_hsb.sail
@@ -0,0 +1,62 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <option.sail>
+$include <vector_dec.sail>
+$include <exception_basic.sail>
+
+val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
+
+val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+
+overload operator + = {add_range}
+overload operator - = {sub_range}
+
+infix 1 >>
+infix 1 <<
+
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+
+val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+
+overload operator >> = {shift_bits_right, shiftr}
+overload operator << = {shift_bits_left, shiftl}
+
+val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}
+
+function HighestSetBit x = {
+  foreach (i from ('N - 1) to 0 by 1 in dec)
+    if [x[i]] == 0b1 then return (true, i);
+  return (false, 0)
+}
+
+/* hw rounds up E to multiple of 4 */
+function roundUp(e) : range(0, 45) -> range(0, 48) =
+    let 'r = modulus(e, 4) in
+    if (r == 0)
+    then e
+    else (e - r + 4)
+
+function computeE (rlength) : bits(65) -> range(0, 48) =
+    let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+    if nonzero then
+      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
+      {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) }
+    else
+      0
+
+val main : unit -> unit effect {escape}
+
+function main() = {
+  let _ = computeE(0xFFFF_FFFF_FFFF_FFFF @ 0b1);
+  ()
+}
\ No newline at end of file