summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair2018-08-13 19:55:23 +0100
committerAlasdair2018-08-13 19:55:23 +0100
commit82642087083f6c7c548e7c8b14233fde8198e9c7 (patch)
tree41ca0bf065970e1678af30e16247206cae370e82 /src
parent01fd68577abfa98a901b220a9928b397047e9fd4 (diff)
Sort ctype_defs in dependency order after specialisation
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator changes.
Diffstat (limited to 'src')
-rw-r--r--src/bytecode_util.ml9
-rw-r--r--src/c_backend.ml46
2 files changed, 51 insertions, 4 deletions
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 188d71cc..c612660a 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -259,6 +259,15 @@ let rec ctyp_suprema = function
| CT_ref ctyp -> CT_ref (ctyp_suprema ctyp)
| CT_poly -> CT_poly
+let rec ctyp_ids = function
+ | CT_enum (id, _) -> IdSet.singleton id
+ | CT_struct (id, ctors) | CT_variant (id, ctors) ->
+ IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
+ | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
+ | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
+ | CT_int | CT_int64 | CT_bits _ | CT_bits64 _ | CT_unit
+ | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
+
let rec unpoly = function
| F_poly f -> unpoly f
| F_call (call, fs) -> F_call (call, List.map unpoly fs)
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 7d6e2f77..841f9eb1 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1873,10 +1873,12 @@ let rec specialize_variants ctx =
let specialized_ctors = Bindings.bindings !unifications in
let new_ctors = monomorphic_ctors @ specialized_ctors in
- let ctx = { ctx with variants = Bindings.add var_id
- (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors)
- ctx.variants } in
-
+ let ctx = {
+ ctx with variants = Bindings.add var_id
+ (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors)
+ ctx.variants
+ } in
+
let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in
let cdefs, ctx = specialize_variants ctx cdefs in
CDEF_type (CTD_variant (var_id, new_ctors)) :: cdefs, ctx
@@ -1894,6 +1896,41 @@ let rec specialize_variants ctx =
| [] -> [], ctx
+(** Once we specialize variants, there may be additional type
+ dependencies which could be in the wrong order. As such we need to
+ sort the type definitions in the list of cdefs. *)
+let sort_ctype_defs cdefs =
+ (* Split the cdefs into type definitions and non type definitions *)
+ let is_ctype_def = function CDEF_type _ -> true | _ -> false in
+ let ctype_defs = List.filter is_ctype_def cdefs in
+ let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in
+
+ let ctdef_id = function
+ | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id
+ in
+
+ let ctdef_ids = function
+ | CTD_enum _ -> IdSet.empty
+ | CTD_struct (_, ctors) | CTD_variant (_, ctors) ->
+ List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors
+ in
+
+ let depends_on cdef1 cdef2 =
+ match cdef1, cdef2 with
+ | CDEF_type ctdef1, CDEF_type ctdef2 ->
+ let ctdef1_ids = ctdef_ids ctdef1 in
+ let ctdef2_ids = ctdef_ids ctdef2 in
+ if IdSet.mem (ctdef_id ctdef1) ctdef2_ids && IdSet.mem (ctdef_id ctdef2) ctdef1_ids then
+ c_error (Printf.sprintf "Post specialization circular dependency between %s and %s found"
+ (string_of_id (ctdef_id ctdef1))
+ (string_of_id (ctdef_id ctdef2)))
+ else if IdSet.mem (ctdef_id ctdef1) ctdef2_ids then -1
+ else 1
+
+ | _, _ -> assert false (* We only use this on ctype_defs *)
+ in
+ List.sort depends_on ctype_defs @ cdefs
+
(*
(* When this optimization fires we know we have bytecode of the form
@@ -2935,6 +2972,7 @@ let compile_ast ctx (Defs defs) =
let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
let cdefs = List.concat (List.rev chunks) in
let cdefs, ctx = specialize_variants ctx cdefs in
+ let cdefs = sort_ctype_defs cdefs in
let cdefs = optimize ctx cdefs in
prerr_endline (Pretty_print_sail.to_string (separate_map (hardline ^^ hardline) pp_cdef cdefs));
(*