diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_compile.ml | 34 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 5 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 2 | ||||
| -rw-r--r-- | src/sail.ml | 3 | ||||
| -rw-r--r-- | src/util.ml | 9 | ||||
| -rw-r--r-- | src/util.mli | 7 |
6 files changed, 51 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} *) |