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.

3 files changed, 35 insertions, 6 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) ^ " ")