diff options
| -rw-r--r-- | language/jib.ott | 29 | ||||
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 163 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 118 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 2 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 84 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 2 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 154 |
9 files changed, 273 insertions, 283 deletions
diff --git a/language/jib.ott b/language/jib.ott index e54e2ea5..5a0e3eba 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -47,15 +47,19 @@ open import Value2 grammar +name :: '' ::= + | id nat :: :: name + | have_exception nat :: :: have_exception + | current_exception nat :: :: current_exception + | return nat :: :: return + % Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval and cval types. +% expressions, used by the aval (ANF) and cval (Jib) types. fragment :: 'F_' ::= - | id :: :: id - | '&' id :: :: ref + | name :: :: id + | '&' name :: :: ref | value :: :: lit - | have_exception :: :: have_exception - | current_exception :: :: current_exception | fragment op fragment' :: :: op | op fragment :: :: unary | string ( fragment0 , ... , fragmentn ) :: :: call @@ -129,13 +133,10 @@ cval :: 'CV_' ::= {{ lem fragment * ctyp }} clexp :: 'CL_' ::= - | id : ctyp :: :: id + | name : ctyp :: :: id | clexp . string :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple - | current_exception : ctyp :: :: current_exception - | have_exception :: :: have_exception - | return : ctyp :: :: return | void :: :: void ctype_def :: 'CTD_' ::= @@ -152,14 +153,14 @@ instr :: 'I_' ::= {{ aux _ iannot }} % The following are the minimal set of instructions output by % Jib_compile.ml. - | ctyp id :: :: decl - | ctyp id = cval :: :: init + | ctyp name :: :: decl + | ctyp name = cval :: :: init | jump ( cval ) string :: :: jump | goto string :: :: goto | string : :: :: label | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall | clexp = cval :: :: copy - | clear ctyp id :: :: clear + | clear ctyp name :: :: clear | undefined ctyp :: :: undefined | match_failure :: :: match_failure | end :: :: end @@ -187,8 +188,8 @@ instr :: 'I_' ::= | return cval :: :: return % For optimising away allocations and copying. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit + | reset ctyp name :: :: reset + | ctyp name = cval :: :: reinit | alias clexp = cval :: :: alias cdef :: 'CDEF_' ::= diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 025138d0..c83fa8e2 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -158,7 +158,7 @@ let rec aval_rename from_id to_id = function | AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ) | AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ) | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ) - | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename from_id to_id fragment, typ, ctyp) + | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename (name from_id) (name to_id) fragment, typ, ctyp) let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = let recur = aexp_rename from_id to_id in diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 846b619f..301006d4 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -310,21 +310,21 @@ let rec c_aval ctx = function (* We need to check that id's type hasn't changed due to flow typing *) let _, ctyp' = Bindings.find id ctx.locals in if ctyp_equal ctyp ctyp' then - AV_C_fragment (F_id id, typ, ctyp) + AV_C_fragment (F_id (name id), typ, ctyp) else (* id's type changed due to flow typing, so it's really still heap allocated! *) v with (* Hack: Assuming global letbindings don't change from flow typing... *) - Not_found -> AV_C_fragment (F_id id, typ, ctyp) + Not_found -> AV_C_fragment (F_id (name id), typ, ctyp) end else v | Register (_, _, typ) when is_stack_typ ctx typ -> let ctyp = ctyp_of_typ ctx typ in if is_stack_ctyp ctyp then - AV_C_fragment (F_id id, typ, ctyp) + AV_C_fragment (F_id (name id), typ, ctyp) else v | _ -> v @@ -612,24 +612,6 @@ let analyze_primop ctx id args typ = else no_change -let generate_cleanup instrs = - let generate_cleanup' (I_aux (instr, _)) = - match instr with - | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)] - | I_decl (ctyp, id) -> [(id, iclear ctyp id)] - | instr -> [] - in - let is_clear ids = function - | I_aux (I_clear (_, id), _) -> IdSet.add id ids - | _ -> ids - in - let cleaned = List.fold_left is_clear IdSet.empty instrs in - instrs - |> List.map generate_cleanup' - |> List.concat - |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned)) - |> List.map snd - (** Functions that have heap-allocated return types are implemented by passing a pointer a location where the return value should be stored. The ANF -> Sail IR pass for expressions simply outputs an @@ -657,11 +639,11 @@ let fix_early_heap_return ret ret_ctyp instrs = before @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] @ rewrite_return after - | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> + | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after -> before @ [I_aux (I_funcall (CL_addr (CL_id (ret, CT_ref ctyp)), extern, fid, args), aux)] @ rewrite_return after - | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> + | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after -> before @ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)] @ rewrite_return after @@ -694,11 +676,11 @@ let fix_early_stack_return ret ret_ctyp instrs = before @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] @ rewrite_return after - | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> + | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after -> before @ [I_aux (I_funcall (CL_id (ret, ctyp), extern, fid, args), aux)] @ rewrite_return after - | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> + | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after -> before @ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)] @ rewrite_return after @@ -722,10 +704,10 @@ let rec insert_heap_returns ret_ctyps = function | None -> raise (Reporting.err_general (id_loc id) ("Cannot find return type for function " ^ string_of_id id)) | Some ret_ctyp when not (is_stack_ctyp ret_ctyp) -> - CDEF_fundef (id, Some gs, args, fix_early_heap_return gs ret_ctyp body) + CDEF_fundef (id, Some gs, args, fix_early_heap_return (name gs) ret_ctyp body) :: insert_heap_returns ret_ctyps cdefs | Some ret_ctyp -> - CDEF_fundef (id, None, args, fix_early_stack_return gs ret_ctyp (idecl ret_ctyp gs :: body)) + CDEF_fundef (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl ret_ctyp (name gs) :: body)) :: insert_heap_returns ret_ctyps cdefs end @@ -766,32 +748,6 @@ let add_local_labels instrs = (* 5. Optimizations *) (**************************************************************************) -let rec instrs_rename from_id to_id = - let rename id = if Id.compare id from_id = 0 then to_id else id in - let crename = cval_rename from_id to_id in - let irename instrs = instrs_rename from_id to_id instrs in - let lrename = clexp_rename from_id to_id in - function - | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs - | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs - | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs - | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs - | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs - | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> - I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs - | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs - | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> - I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs - | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs - | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs - | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs - | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs - | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs - | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs - | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs - | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs - | [] -> [] - let hoist_ctyp = function | CT_lint | CT_lbits _ | CT_struct _ -> true | _ -> false @@ -800,7 +756,7 @@ let hoist_counter = ref 0 let hoist_id () = let id = mk_id ("gh#" ^ string_of_int !hoist_counter) in incr hoist_counter; - id + name id let hoist_allocations recursive_functions = function | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions -> @@ -871,7 +827,7 @@ let rec specialize_variants ctx prior = if ctyp_equal ctyp suprema then [], (unpoly frag, ctyp), [] else - let gs = gensym () in + let gs = ngensym () in [idecl suprema gs; icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], (F_id gs, suprema), @@ -997,26 +953,26 @@ let remove_alias = let rec scan ctyp id n instrs = match n, !alias, instrs with | 0, None, I_aux (I_copy (CL_id (id', ctyp'), (F_id a, ctyp'')), _) :: instrs - when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> alias := Some a; scan ctyp id 1 instrs | 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), (F_id id', ctyp'')), _) :: instrs - when Id.compare a a' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + when Name.compare a a' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> scan ctyp id 2 instrs | 1, Some a, instr :: instrs -> - if IdSet.mem a (instr_ids instr) then + if NameSet.mem a (instr_ids instr) then None else scan ctyp id 1 instrs | 2, Some a, I_aux (I_clear (ctyp', id'), _) :: instrs - when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' -> + when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' -> scan ctyp id 2 instrs | 2, Some a, instr :: instrs -> - if IdSet.mem id (instr_ids instr) then + if NameSet.mem id (instr_ids instr) then None else scan ctyp id 2 instrs @@ -1031,9 +987,9 @@ let remove_alias = in let remove_alias id alias = function | I_aux (I_copy (CL_id (id', _), (F_id alias', _)), _) - when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed + when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed | I_aux (I_copy (CL_id (alias', _), (F_id id', _)), _) - when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed + when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed | I_aux (I_clear (_, id'), _) -> removed | instr -> instr in @@ -1066,17 +1022,17 @@ let unique_names = let unique_id () = let id = mk_id ("u#" ^ string_of_int !unique_counter) in incr unique_counter; - id + name id in let rec opt seen = function - | I_aux (I_decl (ctyp, id), aux) :: instrs when IdSet.mem id seen -> + | I_aux (I_decl (ctyp, id), aux) :: instrs when NameSet.mem id seen -> let id' = unique_id () in let instrs', seen = opt seen instrs in I_aux (I_decl (ctyp, id'), aux) :: instrs_rename id id' instrs', seen | I_aux (I_decl (ctyp, id), aux) :: instrs -> - let instrs', seen = opt (IdSet.add id seen) instrs in + let instrs', seen = opt (NameSet.add id seen) instrs in I_aux (I_decl (ctyp, id), aux) :: instrs', seen | I_aux (I_block block, aux) :: instrs -> @@ -1103,11 +1059,11 @@ let unique_names = in function | CDEF_fundef (function_id, heap_return, args, body) -> - [CDEF_fundef (function_id, heap_return, args, fst (opt IdSet.empty body))] + [CDEF_fundef (function_id, heap_return, args, fst (opt NameSet.empty body))] | CDEF_reg_dec (id, ctyp, instrs) -> - [CDEF_reg_dec (id, ctyp, fst (opt IdSet.empty instrs))] + [CDEF_reg_dec (id, ctyp, fst (opt NameSet.empty instrs))] | CDEF_let (n, bindings, instrs) -> - [CDEF_let (n, bindings, fst (opt IdSet.empty instrs))] + [CDEF_let (n, bindings, fst (opt NameSet.empty instrs))] | cdef -> [cdef] (** This optimization looks for patterns of the form @@ -1135,26 +1091,26 @@ let combine_variables = scan id 1 instrs | 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), (F_id c', ctyp'')), _) :: instrs - when Id.compare c c' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + when Name.compare c c' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> scan id 2 instrs (* Ignore seemingly early clears of x, as this can happen along exception paths *) | 1, Some c, I_aux (I_clear (_, id'), _) :: instrs - when Id.compare id id' = 0 -> + when Name.compare id id' = 0 -> scan id 1 instrs | 1, Some c, instr :: instrs -> - if IdSet.mem id (instr_ids instr) then + if NameSet.mem id (instr_ids instr) then None else scan id 1 instrs | 2, Some c, I_aux (I_clear (ctyp', c'), _) :: instrs - when Id.compare c c' = 0 && ctyp_equal ctyp ctyp' -> + when Name.compare c c' = 0 && ctyp_equal ctyp ctyp' -> !combine | 2, Some c, instr :: instrs -> - if IdSet.mem c (instr_ids instr) then + if NameSet.mem c (instr_ids instr) then None else scan id 2 instrs @@ -1167,12 +1123,12 @@ let combine_variables = scan id 0 in let remove_variable id = function - | I_aux (I_decl (_, id'), _) when Id.compare id id' = 0 -> removed - | I_aux (I_clear (_, id'), _) when Id.compare id id' = 0 -> removed + | I_aux (I_decl (_, id'), _) when Name.compare id id' = 0 -> removed + | I_aux (I_clear (_, id'), _) when Name.compare id id' = 0 -> removed | instr -> instr in let is_not_self_assignment = function - | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Id.compare id id' = 0 -> false + | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Name.compare id id' = 0 -> false | _ -> true in let rec opt = function @@ -1224,9 +1180,9 @@ let hoist_alias = function return, so we want to make sure we avoid that case. *) | (I_aux (I_copy (clexp, (F_id id', ctyp')), aux) as instr) :: instrs - when not (IdSet.mem heap_return (instr_writes instr)) && Id.compare id id' = 0 + when not (NameSet.mem heap_return (instr_writes instr)) && Name.compare id id' = 0 && ctyp_equal (clexp_ctyp clexp) ctyp && ctyp_equal ctyp ctyp' -> - if List.exists (IdSet.mem id) (List.map instr_ids instrs) then + if List.exists (NameSet.mem id) (List.map instr_ids instrs) then instr :: scan instrs else I_aux (I_alias (clexp, (F_id id', ctyp')), aux) :: instrs @@ -1254,7 +1210,7 @@ let hoist_alias = in function | CDEF_fundef (function_id, Some heap_return, args, body) -> - [CDEF_fundef (function_id, Some heap_return, args, optimize heap_return body)] + [CDEF_fundef (function_id, Some heap_return, args, optimize (name heap_return) body)] | cdef -> [cdef] let concatMap f xs = List.concat (List.map f xs) @@ -1274,6 +1230,7 @@ let optimize recursive_functions cdefs = (**************************************************************************) let sgen_id id = Util.zencode_string (string_of_id id) +let sgen_name id = string_of_name id let codegen_id id = string (sgen_id id) let sgen_function_id id = @@ -1336,23 +1293,23 @@ let sgen_cval_param (frag, ctyp) = let sgen_cval = function (frag, _) -> string_of_fragment frag let rec sgen_clexp = function - | CL_id (id, _) -> "&" ^ sgen_id id + | CL_id (Have_exception _, _) -> "have_exception" + | CL_id (Current_exception _, _) -> "current_exception" + | CL_id (Return _, _) -> assert false + | CL_id (Name (id, _), _) -> "&" ^ sgen_id id | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ Util.zencode_string field ^ ")" | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")" | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" - | CL_have_exception -> "have_exception" - | CL_current_exception _ -> "current_exception" - | CL_return _ -> assert false | CL_void -> assert false let rec sgen_clexp_pure = function - | CL_id (id, _) -> sgen_id id + | CL_id (Have_exception _, _) -> "have_exception" + | CL_id (Current_exception _, _) -> "current_exception" + | CL_id (Return _, _) -> assert false + | CL_id (Name (id, _), _) -> sgen_id id | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ Util.zencode_string field | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" - | CL_have_exception -> "have_exception" - | CL_current_exception _ -> "current_exception" - | CL_return _ -> assert false | CL_void -> assert false (** Generate instructions to copy from a cval to a clexp. This will @@ -1397,10 +1354,10 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = let open Printf in match instr with | I_decl (ctyp, id) when is_stack_ctyp ctyp -> - ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) | I_decl (ctyp, id) -> - ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline - ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline + ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) | I_copy (clexp, cval) -> codegen_conversion l clexp cval @@ -1504,7 +1461,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty | I_clear (ctyp, id) -> - string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) | I_init (ctyp, id, cval) -> codegen_instr fid ctx (idecl ctyp id) ^^ hardline @@ -1515,9 +1472,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval | I_reset (ctyp, id) when is_stack_ctyp ctyp -> - string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) + string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_name id)) | I_reset (ctyp, id) -> - string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) | I_return cval -> string (Printf.sprintf " return %s;" (sgen_cval cval)) @@ -1536,24 +1493,24 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | CT_bool -> "false", [] | CT_enum (_, ctor :: _) -> sgen_id ctor, [] | CT_tup ctyps when is_stack_ctyp ctyp -> - let gs = gensym () in + let gs = ngensym () in let fold (inits, prev) (n, ctyp) = let init, prev' = codegen_exn_return ctyp in Printf.sprintf ".ztup%d = %s" n init :: inits, prev @ prev' in let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in - sgen_id gs, - [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + sgen_name gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev | CT_struct (id, ctors) when is_stack_ctyp ctyp -> - let gs = gensym () in + let gs = ngensym () in let fold (inits, prev) (id, ctyp) = let init, prev' = codegen_exn_return ctyp in Printf.sprintf ".%s = %s" (sgen_id id) init :: inits, prev @ prev' in let inits, prev = List.fold_left fold ([], []) ctors in - sgen_id gs, - [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + sgen_name gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev | ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) in @@ -2014,13 +1971,13 @@ let is_decl = function let codegen_decl = function | I_aux (I_decl (ctyp, id), _) -> - string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id)) | _ -> assert false let codegen_alloc = function | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty | I_aux (I_decl (ctyp, id), _) -> - string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) | _ -> assert false let codegen_def' ctx = function @@ -2101,10 +2058,10 @@ let codegen_def' ctx = function | CDEF_let (number, bindings, instrs) -> let instrs = add_local_labels instrs in let setup = - List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings) + List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (name id)]) bindings) in let cleanup = - List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings) + List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index facf64e9..85a77d2e 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -61,6 +61,8 @@ let opt_debug_function = ref "" let opt_debug_flow_graphs = ref false let opt_memo_cache = ref false +let ngensym () = name (gensym ()) + (**************************************************************************) (* 4. Conversion to low-level AST *) (**************************************************************************) @@ -183,26 +185,26 @@ let rec compile_aval l ctx = function begin try let _, ctyp = Bindings.find id ctx.locals in - [], (F_id id, ctyp), [] + [], (F_id (name id), ctyp), [] with | Not_found -> - [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + [], (F_id (name id), ctyp_of_typ ctx (lvar_typ typ)), [] end | AV_ref (id, typ) -> - [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] + [], (F_ref (name id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] | AV_lit (L_aux (L_string str, _), typ) -> [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> - let gs = gensym () in + let gs = ngensym () in [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], (F_id gs, CT_lint), [iclear CT_lint gs] | AV_lit (L_aux (L_num n, _), typ) -> - let gs = gensym () in + let gs = ngensym () in [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], (F_id gs, CT_lint), [iclear CT_lint gs] @@ -214,7 +216,7 @@ let rec compile_aval l ctx = function | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] | AV_lit (L_aux (L_real str, _), _) -> - let gs = gensym () in + let gs = ngensym () in [iinit CT_real gs (F_lit (V_string str), CT_string)], (F_id gs, CT_real), [iclear CT_real gs] @@ -230,7 +232,7 @@ let rec compile_aval l ctx = function let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in - let gs = gensym () in + let gs = ngensym () in setup @ [idecl tup_ctyp gs] @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals, @@ -240,7 +242,7 @@ let rec compile_aval l ctx = function | AV_record (fields, typ) -> let ctyp = ctyp_of_typ ctx typ in - let gs = gensym () in + let gs = ngensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup @@ -278,7 +280,7 @@ let rec compile_aval l ctx = function let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in let first_chunk = bitstring (Util.take (len mod 64) avals) in let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in - let gs = gensym () in + let gs = ngensym () in [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))] @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true)) (mk_id "append_64") @@ -295,7 +297,7 @@ let rec compile_aval l ctx = function | Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") in - let gs = gensym () in + let gs = ngensym () in let ctyp = CT_fbits (len, direction) in let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in let aval_mask i aval = @@ -323,7 +325,7 @@ let rec compile_aval l ctx = function | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") in let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in - let gs = gensym () in + let gs = ngensym () in let aval_set i aval = let setup, cval, cleanup = compile_aval l ctx aval in setup @@ -346,7 +348,7 @@ let rec compile_aval l ctx = function | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ | _ -> raise (Reporting.err_general l "Invalid list type") in - let gs = gensym () in + let gs = ngensym () in let mk_cons aval = let setup, cval, cleanup = compile_aval l ctx aval in setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup @@ -384,7 +386,7 @@ let compile_funcall l ctx id args typ = else if ctyp_equal ctyp have_ctyp then cval else - let gs = gensym () in + let gs = ngensym () in setup := iinit ctyp gs cval :: !setup; cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) @@ -399,7 +401,7 @@ let compile_funcall l ctx id args typ = if ctyp_equal (clexp_ctyp clexp) ret_ctyp then ifuncall clexp id setup_args else - let gs = gensym () in + let gs = ngensym () in iblock [idecl ret_ctyp gs; ifuncall (CL_id (gs, ret_ctyp)) id setup_args; icopy l clexp (F_id gs, ret_ctyp); @@ -425,19 +427,19 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_global (pid, typ), (frag, ctyp) -> let global_ctyp = ctyp_of_typ ctx typ in - [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx + [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with - | Unbound -> [idecl ctyp pid; icopy l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx - | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx + | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) (frag, ctyp)], [], ctx + | _ -> [ijump (F_op (F_id (name pid), "!=", frag), CT_bool) case_label], [], ctx end | AP_id (pid, typ), _ -> let ctyp = cval_ctyp cval in let id_ctyp = ctyp_of_typ ctx typ in let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in - [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx + [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx | AP_tup apats, (frag, ctyp) -> begin @@ -507,7 +509,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = - [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] + [idecl binding_ctyp (name id); + iblock (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)], + [iclear binding_ctyp (name id)] in let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in let setup, call, cleanup = compile_aexp ctx body in @@ -524,7 +528,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_case (aval, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in - let case_return_id = gensym () in + let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with @@ -536,7 +540,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in + let gs = ngensym () in let case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then @@ -566,7 +570,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_try (aexp, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in - let try_return_id = gensym () in + let try_return_id = ngensym () in let handled_exception_label = label "handled_exception_" in let fallthrough_label = label "fallthrough_exception_" in let compile_case (apat, guard, body) = @@ -576,11 +580,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | _ -> false in let try_label = label "try_" in - let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in + let exn_cval = (F_id current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in + let gs = ngensym () in let case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then @@ -596,11 +600,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [idecl ctyp try_return_id; itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] + ijump (F_unary ("!", F_id have_exception), CT_bool) handled_exception_label] @ List.concat (List.map compile_case cases) @ [igoto fallthrough_label; ilabel handled_exception_label; - icopy l CL_have_exception (F_lit (V_bool false), CT_bool); + icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool false), CT_bool); ilabel fallthrough_label], (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)), [] @@ -631,7 +635,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors | _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type") in - let gs = gensym () in + let gs = ngensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup @@ -650,7 +654,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_short_circuit (SC_and, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval l ctx aval in let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let gs = gensym () in + let gs = ngensym () in left_setup @ [ idecl CT_bool gs; iif cval @@ -663,7 +667,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_short_circuit (SC_or, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval l ctx aval in let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let gs = gensym () in + let gs = ngensym () in left_setup @ [ idecl CT_bool gs; iif cval @@ -681,7 +685,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] + @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), @@ -695,7 +699,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup + setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in @@ -707,8 +711,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let loop_end_label = label "wend_" in let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let unit_gs = gensym () in + let gs = ngensym () in + let unit_gs = ngensym () in let loop_test = (F_unary ("!", F_id gs), CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @@ -729,8 +733,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let loop_end_label = label "until_" in let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let unit_gs = gensym () in + let gs = ngensym () in + let unit_gs = ngensym () in let loop_test = (F_id gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @@ -759,7 +763,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = if ctyp_equal fn_return_ctyp (cval_ctyp cval) then [ireturn cval] else - let gs = gensym () in + let gs = ngensym () in [idecl fn_return_ctyp gs; icopy l (CL_id (gs, fn_return_ctyp)) cval; ireturn (F_id gs, fn_return_ctyp)] @@ -804,11 +808,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* Loop variables *) let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in - let from_gs = gensym () in + let from_gs = ngensym () in let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in - let to_gs = gensym () in + let to_gs = ngensym () in let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in - let step_gs = gensym () in + let step_gs = ngensym () in let variable_init gs setup call cleanup = [idecl (CT_fint 64) gs; iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)] @@ -817,8 +821,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let loop_start_label = label "for_start_" in let loop_end_label = label "for_end_" in let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let body_gs = gensym () in + let body_gs = ngensym () in + let loop_var = name loop_var in + variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup @ variable_init step_gs step_setup step_call step_cleanup @@ -842,7 +848,7 @@ and compile_block ctx = function | exp :: exps -> let setup, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in - let gs = gensym () in + let gs = ngensym () in iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest (** Compile a sail type definition into a IR one. Most of the @@ -892,14 +898,14 @@ let generate_cleanup instrs = | instr -> [] in let is_clear ids = function - | I_aux (I_clear (_, id), _) -> IdSet.add id ids + | I_aux (I_clear (_, id), _) -> NameSet.add id ids | _ -> ids in - let cleaned = List.fold_left is_clear IdSet.empty instrs in + let cleaned = List.fold_left is_clear NameSet.empty instrs in instrs |> List.map generate_cleanup' |> List.concat - |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned)) + |> List.filter (fun (id, _) -> not (NameSet.mem id cleaned)) |> List.map snd let fix_exception_block ?return:(return=None) ctx instrs = @@ -927,8 +933,8 @@ let fix_exception_block ?return:(return=None) ctx instrs = @ rewrite_exception historic after | before, I_aux (I_throw cval, (_, l)) :: after -> before - @ [icopy l (CL_current_exception (cval_ctyp cval)) cval; - icopy l CL_have_exception (F_lit (V_bool true), CT_bool)] + @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval; + icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool true), CT_bool)] @ generate_cleanup (historic @ before) @ [igoto end_block_label] @ rewrite_exception (historic @ before) after @@ -941,7 +947,7 @@ let fix_exception_block ?return:(return=None) ctx instrs = if has_effect effects BE_escape then before @ [funcall; - iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] + iif (F_id have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] @ rewrite_exception (historic @ before) after else before @ funcall :: rewrite_exception (historic @ before) after @@ -979,7 +985,7 @@ let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp = | _ -> let apat = anf_pat pat in let gs = gensym () in - let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in + let destructure, cleanup, _ = compile_match ctx apat (F_id (name gs), ctyp) label in (gs, (destructure, cleanup)) let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = @@ -994,10 +1000,10 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in destructure - @ [idecl (CT_tup ctyps) arg_id] - @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids, + @ [idecl (CT_tup ctyps) (name arg_id)] + @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (F_id (name id), ctyp)) new_ids, List.map (fun (id, _) -> id, ([], [])) new_ids, - [iclear (CT_tup ctyps) arg_id] + [iclear (CT_tup ctyps) (name arg_id)] @ cleanup let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) @@ -1108,7 +1114,7 @@ and compile_def' n total ctx = function | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (id, ctyp_of_typ ctx typ))] @ cleanup in + let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_reg_dec (DEC_aux (_, (l, _))) -> @@ -1161,8 +1167,8 @@ and compile_def' n total ctx = function compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label in - 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 = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in + let instrs = fix_early_return (CL_id (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 @@ -1211,7 +1217,7 @@ and compile_def' n total ctx = function let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in let apat = anf_pat ~global:true pat in - let gs = gensym () in + let gs = ngensym () in let end_label = label "let_end_" in let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in let gs_setup, gs_cleanup = @@ -1278,7 +1284,7 @@ let rec specialize_variants ctx prior = if ctyp_equal ctyp suprema then [], (unpoly frag, ctyp), [] else - let gs = gensym () in + let gs = ngensym () in [idecl suprema gs; icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], (F_id gs, suprema), diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index f3bd8c76..a0cacc3c 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -63,6 +63,8 @@ val opt_debug_flow_graphs : bool ref (** Print the IR representation of a specific function. *) val opt_debug_function : string ref +val ngensym : unit -> name + (** {2 Jib context} *) (** Context for compiling Sail to Jib. We need to pass a (global) diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index 889e650e..ea644bad 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -90,7 +90,7 @@ let flat_counter = ref 0 let flat_id () = let id = mk_id ("local#" ^ string_of_int !flat_counter) in incr flat_counter; - id + name id let rec flatten_instrs = function | I_aux (I_decl (ctyp, decl_id), aux) :: instrs -> diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index 9ce3c3f0..470b646b 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -357,47 +357,47 @@ let dominance_frontiers graph root idom children = (**************************************************************************) type ssa_elem = - | Phi of Ast.id * Ast.id list + | Phi of Jib.name * Jib.name list | Pi of Jib.cval list let place_phi_functions graph df = - let defsites = ref Bindings.empty in + let defsites = ref NameMap.empty in - let all_vars = ref IdSet.empty in + let all_vars = ref NameSet.empty in let rec all_decls = function | I_aux ((I_init (_, id, _) | I_decl (_, id)), _) :: instrs -> - IdSet.add id (all_decls instrs) + NameSet.add id (all_decls instrs) | _ :: instrs -> all_decls instrs - | [] -> IdSet.empty + | [] -> NameSet.empty in let orig_A n = match graph.nodes.(n) with | Some ((_, CF_block instrs), _, _) -> - let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in - let vars = IdSet.diff vars (all_decls instrs) in - all_vars := IdSet.union vars !all_vars; + let vars = List.fold_left NameSet.union NameSet.empty (List.map instr_writes instrs) in + let vars = NameSet.diff vars (all_decls instrs) in + all_vars := NameSet.union vars !all_vars; vars - | Some _ -> IdSet.empty - | None -> IdSet.empty + | Some _ -> NameSet.empty + | None -> NameSet.empty in - let phi_A = ref Bindings.empty in + let phi_A = ref NameMap.empty in for n = 0 to graph.next - 1 do - IdSet.iter (fun a -> - let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in - defsites := Bindings.add a (IntSet.add n ds) !defsites + NameSet.iter (fun a -> + let ds = match NameMap.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in + defsites := NameMap.add a (IntSet.add n ds) !defsites ) (orig_A n) done; - IdSet.iter (fun a -> - let workset = ref (Bindings.find a !defsites) in + NameSet.iter (fun a -> + let workset = ref (NameMap.find a !defsites) in while not (IntSet.is_empty !workset) do let n = IntSet.choose !workset in workset := IntSet.remove n !workset; IntSet.iter (fun y -> - let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in + let phi_A_a = match NameMap.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in if not (IntSet.mem y phi_A_a) then begin begin match graph.nodes.(y) with @@ -405,8 +405,8 @@ let place_phi_functions graph df = graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs) | None -> assert false end; - phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A; - if not (IdSet.mem a (orig_A y)) then + phi_A := NameMap.add a (IntSet.add y phi_A_a) !phi_A; + if not (NameSet.mem a (orig_A y)) then workset := IntSet.add y !workset end ) df.(n) @@ -414,29 +414,34 @@ let place_phi_functions graph df = ) !all_vars let rename_variables graph root children = - let counts = ref Bindings.empty in - let stacks = ref Bindings.empty in + let counts = ref NameMap.empty in + let stacks = ref NameMap.empty in let get_count id = - match Bindings.find_opt id !counts with Some n -> n | None -> 0 + match NameMap.find_opt id !counts with Some n -> n | None -> 0 in let top_stack id = - match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0 + match NameMap.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0 in let push_stack id n = - stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks + stacks := NameMap.add id (n :: match NameMap.find_opt id !stacks with Some s -> s | None -> []) !stacks in + let ssa_name i = function + | Name (id, _) -> Name (id, i) + | Have_exception _ -> Have_exception i + | Current_exception _ -> Current_exception i + | Return _ -> Return i + in + let rec fold_frag = function | F_id id -> let i = top_stack id in - F_id (append_id id ("_" ^ string_of_int i)) + F_id (ssa_name i id) | F_ref id -> let i = top_stack id in - F_ref (append_id id ("_" ^ string_of_int i)) + F_ref (ssa_name i id) | F_lit vl -> F_lit vl - | F_have_exception -> F_have_exception - | F_current_exception -> F_current_exception | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2) | F_unary (op, f) -> F_unary (op, fold_frag f) | F_call (id, fs) -> F_call (id, List.map fold_frag fs) @@ -448,15 +453,12 @@ let rename_variables graph root children = let rec fold_clexp = function | CL_id (id, ctyp) -> let i = get_count id + 1 in - counts := Bindings.add id i !counts; + counts := NameMap.add id i !counts; push_stack id i; - CL_id (append_id id ("_" ^ string_of_int i), ctyp) + CL_id (ssa_name i id, ctyp) | CL_field (clexp, field) -> CL_field (fold_clexp clexp, field) | CL_addr clexp -> CL_addr (fold_clexp clexp) | CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n) - | CL_current_exception ctyp -> CL_current_exception ctyp - | CL_have_exception -> CL_have_exception - | CL_return ctyp -> CL_return ctyp | CL_void -> CL_void in @@ -472,15 +474,15 @@ let rename_variables graph root children = I_copy (fold_clexp clexp, cval) | I_decl (ctyp, id) -> let i = get_count id + 1 in - counts := Bindings.add id i !counts; + counts := NameMap.add id i !counts; push_stack id i; - I_decl (ctyp, append_id id ("_" ^ string_of_int i)) + I_decl (ctyp, ssa_name i id) | I_init (ctyp, id, cval) -> let cval = fold_cval cval in let i = get_count id + 1 in - counts := Bindings.add id i !counts; + counts := NameMap.add id i !counts; push_stack id i; - I_init (ctyp, append_id id ("_" ^ string_of_int i), cval) + I_init (ctyp, ssa_name i id, cval) | I_jump (cval, label) -> I_jump (fold_cval cval, label) | instr -> instr @@ -498,9 +500,9 @@ let rename_variables graph root children = let ssa_ssanode = function | Phi (id, args) -> let i = get_count id + 1 in - counts := Bindings.add id i !counts; + counts := NameMap.add id i !counts; push_stack id i; - Phi (append_id id ("_" ^ string_of_int i), args) + Phi (ssa_name i id, args) | Pi _ -> assert false (* Should not be introduced at this point *) in @@ -509,7 +511,7 @@ let rename_variables graph root children = Phi (id, List.mapi (fun k a -> if k = j then let i = top_stack a in - append_id a ("_" ^ string_of_int i) + ssa_name i a else a) ids) | Pi _ -> assert false (* Should not be introduced at this point *) @@ -603,7 +605,7 @@ let ssa instrs = let string_of_ssainstr = function | Phi (id, args) -> - string_of_id id ^ " = φ(" ^ Util.string_of_list ", " string_of_id args ^ ")" + string_of_name id ^ " = φ(" ^ Util.string_of_list ", " string_of_name args ^ ")" | Pi cvals -> "π(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")" diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli index 75c130cf..8cfdb198 100644 --- a/src/jib/jib_ssa.mli +++ b/src/jib/jib_ssa.mli @@ -79,7 +79,7 @@ val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) val immediate_dominators : 'a array_graph -> int -> int array type ssa_elem = - | Phi of Ast.id * Ast.id list + | Phi of Jib.name * Jib.name list | Pi of Jib.cval list (** Convert a list of instructions into SSA form *) diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 81cd07ef..78eca13b 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -81,6 +81,9 @@ let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals = let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals = I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l)) + +let icall ?loc:(l=Parse_ast.Unknown) clexp extern id cvals = + I_aux (I_funcall (clexp, extern, id, cvals), (instr_number (), l)) let icopy l clexp cval = I_aux (I_copy (clexp, cval), (instr_number (), l)) @@ -125,14 +128,39 @@ let iraw ?loc:(l=Parse_ast.Unknown) str = let ijump ?loc:(l=Parse_ast.Unknown) cval label = I_aux (I_jump (cval, label), (instr_number (), l)) +module Name = struct + type t = name + let compare id1 id2 = + match id1, id2 with + | Name (x, n), Name (y, m) -> + let c1 = Id.compare x y in + if c1 = 0 then compare n m else c1 + | Have_exception n, Have_exception m -> compare n m + | Current_exception n, Current_exception m -> compare n m + | Return n, Return m -> compare n m + | Name _, _ -> 1 + | _, Name _ -> -1 + | Have_exception _, _ -> 1 + | _, Have_exception _ -> -1 + | Current_exception _, _ -> 1 + | _, Current_exception _ -> -1 +end + +module NameSet = Set.Make(Name) +module NameMap = Map.Make(Name) + +let current_exception = Current_exception (-1) +let have_exception = Have_exception (-1) +let return = Return (-1) + +let name id = Name (id, -1) + let rec frag_rename from_id to_id = function - | F_id id when Id.compare id from_id = 0 -> F_id to_id + | F_id id when Name.compare id from_id = 0 -> F_id to_id | F_id id -> F_id id - | F_ref id when Id.compare id from_id = 0 -> F_ref to_id + | F_ref id when Name.compare id from_id = 0 -> F_ref to_id | F_ref id -> F_ref id | F_lit v -> F_lit v - | F_have_exception -> F_have_exception - | F_current_exception -> F_current_exception | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags) | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2) | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f) @@ -143,7 +171,7 @@ let rec frag_rename from_id to_id = function let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp) let rec clexp_rename from_id to_id = function - | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp) + | CL_id (id, ctyp) when Name.compare id from_id = 0 -> CL_id (to_id, ctyp) | CL_id (id, ctyp) -> CL_id (id, ctyp) | CL_field (clexp, field) -> CL_field (clexp_rename from_id to_id clexp, field) @@ -151,17 +179,14 @@ let rec clexp_rename from_id to_id = function CL_addr (clexp_rename from_id to_id clexp) | CL_tuple (clexp, n) -> CL_tuple (clexp_rename from_id to_id clexp, n) - | CL_current_exception ctyp -> CL_current_exception ctyp - | CL_have_exception -> CL_have_exception - | CL_return ctyp -> CL_return ctyp | CL_void -> CL_void let rec instr_rename from_id to_id (I_aux (instr, aux)) = let instr = match instr with - | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id) + | I_decl (ctyp, id) when Name.compare id from_id = 0 -> I_decl (ctyp, to_id) | I_decl (ctyp, id) -> I_decl (ctyp, id) - | I_init (ctyp, id, cval) when Id.compare id from_id = 0 -> + | I_init (ctyp, id, cval) when Name.compare id from_id = 0 -> I_init (ctyp, to_id, cval_rename from_id to_id cval) | I_init (ctyp, id, cval) -> I_init (ctyp, id, cval_rename from_id to_id cval) @@ -180,7 +205,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = | I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval) | I_alias (clexp, cval) -> I_alias (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval) - | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id) + | I_clear (ctyp, id) when Name.compare id from_id = 0 -> I_clear (ctyp, to_id) | I_clear (ctyp, id) -> I_clear (ctyp, id) | I_return cval -> I_return (cval_rename from_id to_id cval) @@ -205,10 +230,10 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = | I_end -> I_end - | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id) + | I_reset (ctyp, id) when Name.compare id from_id = 0 -> I_reset (ctyp, to_id) | I_reset (ctyp, id) -> I_reset (ctyp, id) - | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 -> + | I_reinit (ctyp, id, cval) when Name.compare id from_id = 0 -> I_reinit (ctyp, to_id, cval_rename from_id to_id cval) | I_reinit (ctyp, id, cval) -> I_reinit (ctyp, id, cval_rename from_id to_id cval) @@ -233,11 +258,21 @@ let string_of_value = function | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str | _ -> failwith "Cannot convert value to string" +let string_of_name ?zencode:(zencode=true) = + let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in + function + | Name (id, n) -> + (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n + | Have_exception n -> + "have_exception" ^ ssa_num n + | Return n -> + "return" ^ ssa_num n + | Current_exception n -> + "(*current_exception)" ^ ssa_num n + let rec string_of_fragment ?zencode:(zencode=true) = function - | F_id id when zencode -> Util.zencode_string (string_of_id id) - | F_id id -> string_of_id id - | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id) - | F_ref id -> "&" ^ string_of_id id + | F_id id -> string_of_name ~zencode:zencode id + | F_ref id -> "&" ^ string_of_name ~zencode:zencode id | F_lit v -> string_of_value v | F_call (str, frags) -> Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) @@ -247,8 +282,6 @@ let rec string_of_fragment ?zencode:(zencode=true) = function Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2) | F_unary (op, f) -> op ^ string_of_fragment' ~zencode:zencode f - | F_have_exception -> "have_exception" - | F_current_exception -> "(*current_exception)" | F_raw raw -> raw | F_poly f -> string_of_fragment ~zencode:zencode f and string_of_fragment' ?zencode:(zencode=true) f = @@ -466,6 +499,9 @@ let rec is_polymorphic = function let pp_id id = string (string_of_id id) +let pp_name id = + string (string_of_name ~zencode:false id) + let pp_ctyp ctyp = string (full_string_of_ctyp ctyp |> Util.yellow |> Util.clear) @@ -476,19 +512,16 @@ let pp_cval (frag, ctyp) = string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp let rec pp_clexp = function - | CL_id (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp | CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field | CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n) | CL_addr clexp -> string "*" ^^ pp_clexp clexp - | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp - | CL_have_exception -> string "have_exception" - | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp | CL_void -> string "void" let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = match instr with | I_decl (ctyp, id) -> - pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + pp_keyword "var" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp | I_if (cval, then_instrs, else_instrs, ctyp) -> let pp_if_block = function | [] -> string "{}" @@ -508,11 +541,11 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = | I_try_block instrs -> pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace | I_reset (ctyp, id) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp | I_init (ctyp, id, cval) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval + pp_keyword "create" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval | I_reinit (ctyp, id, cval) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval + pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval | I_funcall (x, _, f, args) -> separate space [ pp_clexp x; string "="; string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ] @@ -521,7 +554,7 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = | I_alias (clexp, cval) -> pp_keyword "alias" ^^ separate space [pp_clexp clexp; string "="; pp_cval cval] | I_clear (ctyp, id) -> - pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + pp_keyword "kill" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp | I_return cval -> pp_keyword "return" ^^ pp_cval cval | I_throw cval -> @@ -584,55 +617,47 @@ let pp_cdef = function ^^ hardline let rec fragment_deps = function - | F_id id | F_ref id -> IdSet.singleton id - | F_lit _ -> IdSet.empty + | F_id id | F_ref id -> NameSet.singleton id + | F_lit _ -> NameSet.empty | F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag - | F_call (_, frags) -> List.fold_left IdSet.union IdSet.empty (List.map fragment_deps frags) - | F_op (frag1, _, frag2) -> IdSet.union (fragment_deps frag1) (fragment_deps frag2) - | F_current_exception -> IdSet.empty - | F_have_exception -> IdSet.empty - | F_raw _ -> IdSet.empty + | F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags) + | F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2) + | F_raw _ -> NameSet.empty let cval_deps = function (frag, _) -> fragment_deps frag let rec clexp_deps = function - | CL_id (id, _) -> IdSet.singleton id + | CL_id (id, _) -> NameSet.singleton id | CL_field (clexp, _) -> clexp_deps clexp | CL_tuple (clexp, _) -> clexp_deps clexp | CL_addr clexp -> clexp_deps clexp - | CL_have_exception -> IdSet.empty - | CL_current_exception _ -> IdSet.empty - | CL_return _ -> IdSet.empty - | CL_void -> IdSet.empty + | CL_void -> NameSet.empty (* Return the direct, read/write dependencies of a single instruction *) let instr_deps = function - | I_decl (ctyp, id) -> IdSet.empty, IdSet.singleton id - | I_reset (ctyp, id) -> IdSet.empty, IdSet.singleton id - | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, IdSet.singleton id - | I_if (cval, _, _, _) -> cval_deps cval, IdSet.empty - | I_jump (cval, label) -> cval_deps cval, IdSet.empty - | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp + | I_decl (ctyp, id) -> NameSet.empty, NameSet.singleton id + | I_reset (ctyp, id) -> NameSet.empty, NameSet.singleton id + | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NameSet.singleton id + | I_if (cval, _, _, _) -> cval_deps cval, NameSet.empty + | I_jump (cval, label) -> cval_deps cval, NameSet.empty + | I_funcall (clexp, _, _, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals), clexp_deps clexp | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp - | I_clear (_, id) -> IdSet.singleton id, IdSet.empty - | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty - | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty - | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty - | I_label label -> IdSet.empty, IdSet.empty - | I_goto label -> IdSet.empty, IdSet.empty - | I_undefined _ -> IdSet.empty, IdSet.empty - | I_match_failure -> IdSet.empty, IdSet.empty - | I_end -> IdSet.empty, IdSet.empty + | I_clear (_, id) -> NameSet.singleton id, NameSet.empty + | I_throw cval | I_return cval -> cval_deps cval, NameSet.empty + | I_block _ | I_try_block _ -> NameSet.empty, NameSet.empty + | I_comment _ | I_raw _ -> NameSet.empty, NameSet.empty + | I_label label -> NameSet.empty, NameSet.empty + | I_goto label -> NameSet.empty, NameSet.empty + | I_undefined _ -> NameSet.empty, NameSet.empty + | I_match_failure -> NameSet.empty, NameSet.empty + | I_end -> NameSet.empty, NameSet.empty let rec map_clexp_ctyp f = function | CL_id (id, ctyp) -> CL_id (id, f ctyp) | CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field) | CL_tuple (clexp, n) -> CL_tuple (map_clexp_ctyp f clexp, n) | CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp) - | CL_current_exception ctyp -> CL_current_exception (f ctyp) - | CL_have_exception -> CL_have_exception - | CL_return ctyp -> CL_return (f ctyp) | CL_void -> CL_void let rec map_instr_ctyp f (I_aux (instr, aux)) = @@ -732,7 +757,7 @@ let map_instrs_list f instrs = let rec instr_ids (I_aux (instr, _)) = let reads, writes = instr_deps instr in - IdSet.union reads writes + NameSet.union reads writes let rec instr_reads (I_aux (instr, _)) = fst (instr_deps instr) @@ -764,7 +789,6 @@ let cval_ctyp = function (_, ctyp) -> ctyp let rec clexp_ctyp = function | CL_id (_, ctyp) -> ctyp - | CL_return ctyp -> ctyp | CL_field (clexp, field) -> begin match clexp_ctyp clexp with | CT_struct (id, ctors) -> @@ -788,8 +812,6 @@ let rec clexp_ctyp = function end | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) end - | CL_have_exception -> CT_bool - | CL_current_exception ctyp -> ctyp | CL_void -> CT_unit let rec instr_ctyps (I_aux (instr, aux)) = @@ -848,12 +870,12 @@ let instr_split_at f = instr_split_at' f [] let rec instrs_rename from_id to_id = - let rename id = if Id.compare id from_id = 0 then to_id else id in + let rename id = if Name.compare id from_id = 0 then to_id else id in let crename = cval_rename from_id to_id in let irename instrs = instrs_rename from_id to_id instrs in let lrename = clexp_rename from_id to_id in function - | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs + | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Name.compare from_id new_id = 0 -> instrs | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs @@ -861,8 +883,8 @@ let rec instrs_rename from_id to_id = | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs - | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> - I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs + | I_aux (I_funcall (clexp, extern, function_id, cvals), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, extern, function_id, List.map crename cvals), aux) :: irename instrs | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs |