C: Fix miscompilation of constrained struct field access

For a Int-parameterised struct F('x: Int) = ... the optimizer would
attempt to optimize field access in cases where 'x was known to
constrain the types of the struct fields only locally. Which would
create a type error in the generated C. Now we always use the type
from the global struct type.

However, we previously weren't using struct type quantifiers to
optimize the field representation, which we now do.

Also rename some utility functions to better match the List
functions in the OCaml stdlib.

10 files changed, 101 insertions, 9 deletions

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 8411f464..36a28d9f 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -57,6 +57,7 @@ open Value2
 
 open Anf
 
+let opt_debug_function = ref ""
 let opt_memo_cache = ref false
 
 (**************************************************************************)
@@ -773,9 +774,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      (fun clexp -> icomment "unreachable after throw"),
      []
 
-  | AE_field (aval, id, typ) ->
-     let ctyp = ctyp_of_typ ctx typ in
+  | AE_field (aval, id, _) ->
      let setup, cval, cleanup = compile_aval l ctx aval in
+     let ctyp = match cval_ctyp cval with
+       | CT_struct (struct_id, fields) ->
+          begin match Util.assoc_compare_opt Id.compare id fields with
+          | Some ctyp -> ctyp
+          | None ->
+             raise (Reporting.err_unreachable l __POS__
+                      ("Struct " ^ string_of_id struct_id ^ " does not have expected field " ^ string_of_id id ^ "?"))
+          end
+       | _ ->
+          raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!")
+     in
      setup,
      (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)),
      cleanup
@@ -846,8 +857,11 @@ let compile_type_def ctx (TD_aux (type_def, (l, _))) =
      CTD_enum (id, ids),
      { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums }
 
-  | TD_record (id, _, ctors, _) ->
-     let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in
+  | TD_record (id, typq, ctors, _) ->
+     let record_ctx = { ctx with local_env = add_typquant l typq ctx.local_env } in
+     let ctors =
+       List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ record_ctx typ) ctors) Bindings.empty ctors
+     in
      CTD_struct (id, Bindings.bindings ctors),
      { ctx with records = Bindings.add id ctors ctx.records }
 
@@ -1149,6 +1163,18 @@ and compile_def' n total ctx = function
      let instrs = arg_setup @ destructure @ setup @ [call (CL_return ret_ctyp)] @ cleanup @ destructure_cleanup @ arg_cleanup in
      let instrs = fix_early_return (CL_return ret_ctyp) instrs in
      let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
+
+     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 (List.map fst compiled_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 PPrint.(separate_map hardline pp_instr instrs))
+     else ();
+     
      [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) ->
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 50054149..92a0d06a 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -53,7 +53,10 @@ open Ast
 open Ast_util
 open Jib
 open Type_check
-
+   
+(** Print the IR representation of a specific function. *)
+val opt_debug_function : string ref
+  
 (** Context for compiling Sail to Jib. We need to pass a (global)
    typechecking environment given by checking the full AST. We have to
    provide a conversion function from Sail types into Jib types, as
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index d9c6a541..17227875 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -466,7 +466,7 @@ let pp_id id =
   string (string_of_id id)
 
 let pp_ctyp ctyp =
-  string (string_of_ctyp ctyp |> Util.yellow |> Util.clear)
+  string (full_string_of_ctyp ctyp |> Util.yellow |> Util.clear)
 
 let pp_keyword str =
   string ((str |> Util.red |> Util.clear) ^ " ")
diff --git a/src/sail.ml b/src/sail.ml
index 813d8ec1..50719776 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -307,6 +307,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 -> Jib_compile.opt_debug_function := f),
+    " (debug) print debugging output for a single function");
   ( "-dprofile",
     Arg.Set Profile.opt_profile,
     " (debug) provide basic profiling information for rewriting passes within Sail");
diff --git a/src/util.ml b/src/util.ml
index 0ff00df1..251fb3eb 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -149,11 +149,16 @@ let rec power i tothe =
   then 1
   else i * power i (tothe - 1)
 
-let rec assoc_maybe eq l k =
+let rec assoc_equal_opt eq k l =
   match l with
     | [] -> None
-    | (k',v)::l -> if (eq k k') then Some v else assoc_maybe eq l k
+    | (k',v)::l -> if (eq k k') then Some v else assoc_equal_opt eq k l
 
+let rec assoc_compare_opt cmp k l =
+  match l with
+    | [] -> None
+    | (k',v)::l -> if cmp k k' = 0 then Some v else assoc_compare_opt cmp k l
+                 
 let rec compare_list f l1 l2 = 
   match (l1,l2) with
     | ([],[]) -> 0
diff --git a/src/util.mli b/src/util.mli
index 51504941..013bdcda 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -72,8 +72,13 @@ val remove_duplicates : 'a list -> 'a list
 (** [remove_dups compare eq l] as remove_duplicates but with parameterised comparison and equality *)
 val remove_dups : ('a -> 'a -> int) -> ('a -> 'a -> bool) -> 'a list -> 'a list
 
-val assoc_maybe : ('a -> 'a -> bool) -> ('a * 'b) list -> 'a -> 'b option
+(** [assoc_equal_opt] and [assoc_compare_opt] are like List.assoc_opt
+   but take equality/comparison functions as arguments, rather than
+   relying on OCaml's built in equality *)
+val assoc_equal_opt : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b option
 
+val assoc_compare_opt : ('a -> 'a -> int) -> 'a -> ('a * 'b) list -> 'b option
+  
 val power : int -> int -> int
 
 (** {2 Option Functions} *)
diff --git a/test/c/int_struct.expect b/test/c/int_struct.expect
new file mode 100644
index 00000000..f70f10e4
--- /dev/null
+++ b/test/c/int_struct.expect
@@ -0,0 +1 @@
+A
diff --git a/test/c/int_struct.sail b/test/c/int_struct.sail
new file mode 100644
index 00000000..42554593
--- /dev/null
+++ b/test/c/int_struct.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+
+val print = "print_endline" : string -> unit
+
+struct Foo('n: Int) = {
+  field: bits('n)
+}
+
+type Foo32 = Foo(32)
+
+function bar(foo: Foo32) -> unit = {
+  if foo.field == 0xFFFF_FFFF then {
+    print("A")
+  } else {
+    print("B")
+  }
+}
+
+function main((): unit) -> unit = {
+  let x: Foo32 = struct { field = 0xFFFF_FFFF };
+  bar(x)
+}
\ No newline at end of file
diff --git a/test/c/int_struct_constrained.expect b/test/c/int_struct_constrained.expect
new file mode 100644
index 00000000..f70f10e4
--- /dev/null
+++ b/test/c/int_struct_constrained.expect
@@ -0,0 +1 @@
+A
diff --git a/test/c/int_struct_constrained.sail b/test/c/int_struct_constrained.sail
new file mode 100644
index 00000000..95cb6e9b
--- /dev/null
+++ b/test/c/int_struct_constrained.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+
+val print = "print_endline" : string -> unit
+
+struct Foo('n: Int), 'n <= 64 = {
+  field: bits('n)
+}
+
+type Foo32 = Foo(32)
+
+function bar(foo: Foo32) -> unit = {
+  if foo.field == 0xFFFF_FFFF then {
+    print("A")
+  } else {
+    print("B")
+  }
+}
+
+function main((): unit) -> unit = {
+  let x: Foo32 = struct { field = 0xFFFF_FFFF };
+  bar(x)
+}
\ No newline at end of file