diff --git a/language/jib.ott b/language/jib.ott index 52fe1101e..c85ac1c51 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -234,7 +234,11 @@ instr :: 'I_' ::= | reset ctyp name :: :: reset | ctyp name = cval :: :: reinit +def_annot :: '' ::= + {{ phantom }} + cdef :: 'CDEF_' ::= + {{ aux _ def_annot }} | register id : ctyp = { instr0 ; ... ; instrn } :: :: register diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 5301ffac9..74b6496bd 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -254,7 +254,7 @@ let callgraph cdefs = List.fold_left (fun graph cdef -> match cdef with - | CDEF_fundef (id, _, _, body) -> + | CDEF_aux (CDEF_fundef (id, _, _, body), _) -> let graph = ref graph in List.iter (iter_instr (function @@ -1375,7 +1375,7 @@ module Make (C : CONFIG) = struct let letdef_count = ref 0 - let compile_funcl ctx id pat guard exp = + let compile_funcl ctx def_annot id pat guard exp = (* Find the function's type. *) let quant, Typ_aux (fn_typ, _) = try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env @@ -1441,7 +1441,7 @@ module Make (C : CONFIG) = struct let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in let instrs = coverage_function_entry id (exp_loc exp) @ instrs in - ([CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx) + ([CDEF_aux (CDEF_fundef (id, None, List.map fst compiled_args, instrs), def_annot)], orig_ctx) (** Compile a Sail toplevel definition into an IR definition **) let rec compile_def n total ctx (DEF_aux (aux, _) as def) = @@ -1476,15 +1476,16 @@ module Make (C : CONFIG) = struct end | _ -> compile_def' n total ctx def - and compile_def' n total ctx (DEF_aux (aux, _) as def) = + and compile_def' n total ctx (DEF_aux (aux, def_annot) as def) = match aux with - | DEF_register (DEC_aux (DEC_reg (typ, id, None), _)) -> ([CDEF_register (id, ctyp_of_typ ctx typ, [])], ctx) + | DEF_register (DEC_aux (DEC_reg (typ, id, None), _)) -> + ([CDEF_aux (CDEF_register (id, ctyp_of_typ ctx typ, []), def_annot)], ctx) | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), _)) -> let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in let instrs = unique_names instrs in - ([CDEF_register (id, ctyp_of_typ ctx typ, instrs)], ctx) + ([CDEF_aux (CDEF_register (id, ctyp_of_typ ctx typ, instrs), def_annot)], ctx) | DEF_val (VS_aux (VS_val_spec (_, id, ext), _)) -> let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let extern = if Env.is_extern id ctx.tc_env "c" then Some (Env.get_extern id ctx.tc_env "c") else None in @@ -1493,16 +1494,16 @@ module Make (C : CONFIG) = struct in let ctx' = { ctx with local_env = Env.add_typquant (id_loc id) quant ctx.local_env } in let arg_ctyps, ret_ctyp = (List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ) in - ( [CDEF_val (id, extern, arg_ctyps, ret_ctyp)], + ( [CDEF_aux (CDEF_val (id, extern, arg_ctyps, ret_ctyp), def_annot)], { ctx with valspecs = Bindings.add id (extern, arg_ctyps, ret_ctyp) ctx.valspecs } ) | DEF_fundef (FD_aux (FD_function (_, _, [FCL_aux (FCL_funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> Util.progress "Compiling " (string_of_id id) n total; - compile_funcl ctx id pat None exp + compile_funcl ctx def_annot id pat None exp | DEF_fundef (FD_aux (FD_function (_, _, [FCL_aux (FCL_funcl (id, Pat_aux (Pat_when (pat, guard, exp), _)), _)]), _)) -> Util.progress "Compiling " (string_of_id id) n total; - compile_funcl ctx id pat (Some guard) exp + compile_funcl ctx def_annot id pat (Some guard) exp | DEF_fundef (FD_aux (FD_function (_, _, []), (l, _))) -> raise (Reporting.err_general l "Encountered function with no clauses") | DEF_fundef (FD_aux (FD_function (_, _, _ :: _ :: _), (l, _))) -> @@ -1512,7 +1513,7 @@ module Make (C : CONFIG) = struct | DEF_type (TD_aux (TD_abbrev _, _)) -> ([], ctx) | DEF_type type_def -> let tdef, ctx = compile_type_def ctx type_def in - ([CDEF_type tdef], ctx) + ([CDEF_aux (CDEF_type tdef, def_annot)], ctx) | DEF_let (LB_aux (LB_val (pat, exp), _)) -> let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in @@ -1532,7 +1533,7 @@ module Make (C : CONFIG) = struct @ [ilabel end_label] in let instrs = unique_names instrs in - ( [CDEF_let (n, bindings, instrs)], + ( [CDEF_aux (CDEF_let (n, bindings, instrs), def_annot)], { ctx with letbinds = n :: ctx.letbinds; letbind_ids = IdSet.union (pat_ids pat) ctx.letbind_ids } ) (* Only DEF_default that matters is default Order, but all order @@ -1542,7 +1543,7 @@ module Make (C : CONFIG) = struct | DEF_overload _ -> ([], ctx) (* Only the parser and sail pretty printer care about this. *) | DEF_fixity _ -> ([], ctx) - | DEF_pragma ("abstract", id_str, _) -> ([CDEF_pragma ("abstract", id_str)], ctx) + | DEF_pragma ("abstract", id_str, _) -> ([CDEF_aux (CDEF_pragma ("abstract", id_str), def_annot)], ctx) (* We just ignore any pragmas we don't want to deal with. *) | DEF_pragma _ -> ([], ctx) (* Termination measures only needed for Coq, and other theorem prover output *) @@ -1571,7 +1572,7 @@ module Make (C : CONFIG) = struct let polymorphic_functions = List.filter_map (function - | CDEF_val (id, _, param_ctyps, ret_ctyp) -> + | CDEF_aux (CDEF_val (id, _, param_ctyps, ret_ctyp), _) -> if List.exists is_polymorphic param_ctyps || is_polymorphic ret_ctyp then Some id else None | _ -> None ) @@ -1603,7 +1604,8 @@ module Make (C : CONFIG) = struct each of the monomorphic calls we just found. *) let spec_tyargs = ref Bindings.empty in let rec specialize_fundefs ctx prior = function - | (CDEF_val (id, extern, param_ctyps, ret_ctyp) as orig_cdef) :: cdefs when Bindings.mem id !monomorphic_calls -> + | (CDEF_aux (CDEF_val (id, extern, param_ctyps, ret_ctyp), def_annot) as orig_cdef) :: cdefs + when Bindings.mem id !monomorphic_calls -> let tyargs = List.fold_left (fun set ctyp -> KidSet.union (ctyp_vars ctyp) set) KidSet.empty (ret_ctyp :: param_ctyps) in @@ -1620,7 +1622,7 @@ module Make (C : CONFIG) = struct in let param_ctyps = List.map (subst_poly substs) param_ctyps in let ret_ctyp = subst_poly substs ret_ctyp in - Some (CDEF_val (specialized_id, extern, param_ctyps, ret_ctyp)) + Some (CDEF_aux (CDEF_val (specialized_id, extern, param_ctyps, ret_ctyp), def_annot)) ) else None ) @@ -1630,14 +1632,15 @@ module Make (C : CONFIG) = struct List.fold_left (fun ctx cdef -> match cdef with - | CDEF_val (id, _, param_ctyps, ret_ctyp) -> + | CDEF_aux (CDEF_val (id, _, param_ctyps, ret_ctyp), _) -> { ctx with valspecs = Bindings.add id (extern, param_ctyps, ret_ctyp) ctx.valspecs } | cdef -> ctx ) ctx specialized_specs in specialize_fundefs ctx ((orig_cdef :: specialized_specs) @ prior) cdefs - | (CDEF_fundef (id, heap_return, params, body) as orig_cdef) :: cdefs when Bindings.mem id !monomorphic_calls -> + | (CDEF_aux (CDEF_fundef (id, heap_return, params, body), def_annot) as orig_cdef) :: cdefs + when Bindings.mem id !monomorphic_calls -> let tyargs = Bindings.find id !spec_tyargs in let specialized_fundefs = List.filter_map @@ -1651,7 +1654,7 @@ module Make (C : CONFIG) = struct KBindings.empty (KidSet.elements tyargs) instantiation in let body = List.map (map_instr_ctyp (subst_poly substs)) body in - Some (CDEF_fundef (specialized_id, heap_return, params, body)) + Some (CDEF_aux (CDEF_fundef (specialized_id, heap_return, params, body), def_annot)) ) else None ) @@ -1670,7 +1673,7 @@ module Make (C : CONFIG) = struct let monomorphic_roots = List.filter_map (function - | CDEF_val (id, _, param_ctyps, ret_ctyp) -> + | CDEF_aux (CDEF_val (id, _, param_ctyps, ret_ctyp), _) -> if List.exists is_polymorphic param_ctyps || is_polymorphic ret_ctyp then None else Some id | _ -> None ) @@ -1684,8 +1687,8 @@ module Make (C : CONFIG) = struct let cdefs = List.filter_map (function - | CDEF_fundef (id, _, _, _) when IdSet.mem id unreachable_polymorphic_functions -> None - | CDEF_val (id, _, _, _) when IdSet.mem id unreachable_polymorphic_functions -> None + | CDEF_aux (CDEF_fundef (id, _, _, _), _) when IdSet.mem id unreachable_polymorphic_functions -> None + | CDEF_aux (CDEF_val (id, _, _, _), _) when IdSet.mem id unreachable_polymorphic_functions -> None | cdef -> Some cdef ) cdefs @@ -1799,12 +1802,16 @@ module Make (C : CONFIG) = struct let specialize_field ctx struct_id = visit_cdefs (new specialize_field_visitor instantiations ctx struct_id) in let mangled_pragma orig_id mangled_id = - CDEF_pragma - ("mangled", Util.zencode_string (string_of_id orig_id) ^ " " ^ Util.zencode_string (string_of_id mangled_id)) + CDEF_aux + ( CDEF_pragma + ("mangled", Util.zencode_string (string_of_id orig_id) ^ " " ^ Util.zencode_string (string_of_id mangled_id)), + mk_def_annot (gen_loc (id_loc orig_id)) + ) in function - | CDEF_type (CTD_variant (var_id, ctors)) :: cdefs when List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors -> + | CDEF_aux (CDEF_type (CTD_variant (var_id, ctors)), def_annot) :: cdefs + when List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors -> let typ_params = List.fold_left (fun set (_, ctyp) -> KidSet.union (ctyp_vars ctyp) set) KidSet.empty ctors in let _ = visit_cdefs (new scan_variant_visitor instantiations ctx var_id) cdefs in @@ -1866,14 +1873,16 @@ module Make (C : CONFIG) = struct specialize_variants ctx (List.concat (List.map - (fun (id, ctors) -> [CDEF_type (CTD_variant (id, ctors)); mangled_pragma var_id id]) + (fun (id, ctors) -> + [CDEF_aux (CDEF_type (CTD_variant (id, ctors)), def_annot); mangled_pragma var_id id] + ) monomorphized_variants ) @ mangled_ctors @ prior ) cdefs - | CDEF_type (CTD_struct (struct_id, fields)) :: cdefs when List.exists (fun (_, ctyp) -> is_polymorphic ctyp) fields - -> + | CDEF_aux (CDEF_type (CTD_struct (struct_id, fields)), def_annot) :: cdefs + when List.exists (fun (_, ctyp) -> is_polymorphic ctyp) fields -> let typ_params = List.fold_left (fun set (_, ctyp) -> KidSet.union (ctyp_vars ctyp) set) KidSet.empty fields in let cdefs = specialize_field ctx struct_id cdefs in @@ -1932,7 +1941,9 @@ module Make (C : CONFIG) = struct specialize_variants ctx (List.concat (List.map - (fun (id, fields) -> [CDEF_type (CTD_struct (id, fields)); mangled_pragma struct_id id]) + (fun (id, fields) -> + [CDEF_aux (CDEF_type (CTD_struct (id, fields)), def_annot); mangled_pragma struct_id id] + ) monomorphized_structs ) @ mangled_fields @ prior @@ -2018,7 +2029,7 @@ module Make (C : CONFIG) = struct in let rec precise_calls prior = function - | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs -> + | (CDEF_aux (CDEF_type (CTD_variant (var_id, ctors)), _) as cdef) :: cdefs -> List.iter (fun (id, ctyp) -> constructor_types := Bindings.add id ([ctyp], CT_variant (var_id, ctors)) !constructor_types @@ -2035,8 +2046,8 @@ module Make (C : CONFIG) = struct to sort the type definitions in the list of cdefs. *) let sort_ctype_defs reverse cdefs = (* Split the cdefs into type definitions and non type definitions *) - let is_ctype_def = function CDEF_type _ -> true | _ -> false in - let unwrap = function CDEF_type ctdef -> ctdef | _ -> assert false in + let is_ctype_def = function CDEF_aux (CDEF_type _, _) -> true | _ -> false in + let unwrap = function CDEF_aux (CDEF_type ctdef, def_annot) -> (ctdef, def_annot) | _ -> assert false in let ctype_defs = List.map unwrap (List.filter is_ctype_def cdefs) in let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in @@ -2053,7 +2064,7 @@ module Make (C : CONFIG) = struct let module IdGraph = Graph.Make (Id) in let graph = List.fold_left - (fun g ctdef -> + (fun g (ctdef, _) -> List.fold_left (fun g id -> IdGraph.add_edge id (ctdef_id ctdef) g) (IdGraph.add_edges (ctdef_id ctdef) [] g) (* Make sure even types with no dependencies are in graph *) @@ -2065,7 +2076,12 @@ module Make (C : CONFIG) = struct (* Then select the ctypes in the correct order as given by the topsort *) let ids = IdGraph.topsort graph in let ctype_defs = - List.map (fun id -> CDEF_type (List.find (fun ctdef -> Id.compare (ctdef_id ctdef) id = 0) ctype_defs)) ids + List.map + (fun id -> + let ctdef, def_annot = List.find (fun (ctdef, _) -> Id.compare (ctdef_id ctdef) id = 0) ctype_defs in + CDEF_aux (CDEF_type ctdef, def_annot) + ) + ids in (if reverse then List.rev ctype_defs else ctype_defs) @ cdefs @@ -2116,7 +2132,8 @@ module Make (C : CONFIG) = struct let dummy_exn = mk_id "__dummy_exn#" in let cdefs, ctx = if not (Bindings.mem (mk_id "exception") ctx.variants) then - ( CDEF_type (CTD_variant (mk_id "exception", [(dummy_exn, CT_unit)])) :: cdefs, + ( CDEF_aux (CDEF_type (CTD_variant (mk_id "exception", [(dummy_exn, CT_unit)])), mk_def_annot Parse_ast.Unknown) + :: cdefs, { ctx with variants = Bindings.add (mk_id "exception") ([], Bindings.singleton dummy_exn CT_unit) ctx.variants; diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index e6754694f..a78c74853 100644 --- a/src/lib/jib_optimize.ml +++ b/src/lib/jib_optimize.ml @@ -119,7 +119,7 @@ let rec flatten_instrs = function | instr :: instrs -> instr :: flatten_instrs instrs | [] -> [] -let flatten_cdef = function +let flatten_cdef_aux = function | CDEF_fundef (function_id, heap_return, args, body) -> flat_counter := 0; CDEF_fundef (function_id, heap_return, args, flatten_instrs body) @@ -128,6 +128,8 @@ let flatten_cdef = function CDEF_let (n, bindings, flatten_instrs instrs) | cdef -> cdef +let flatten_cdef (CDEF_aux (aux, def_annot)) = CDEF_aux (flatten_cdef_aux aux, def_annot) + let unique_per_function_ids cdefs = let unique_id i = function | Name (id, ssa_num) -> Name (append_id id ("#u" ^ string_of_int i), ssa_num) @@ -146,7 +148,7 @@ let unique_per_function_ids cdefs = | instr :: instrs -> instr :: unique_instrs i instrs | [] -> [] in - let unique_cdef i = function + let unique_cdef_aux i = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, ctyp, unique_instrs i instrs) | CDEF_type ctd -> CDEF_type ctd | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, unique_instrs i instrs) @@ -156,6 +158,7 @@ let unique_per_function_ids cdefs = | CDEF_finish (id, instrs) -> CDEF_finish (id, unique_instrs i instrs) | CDEF_pragma (name, str) -> CDEF_pragma (name, str) in + let unique_cdef i (CDEF_aux (aux, def_annot)) = CDEF_aux (unique_cdef_aux i aux, def_annot) in List.mapi unique_cdef cdefs let rec cval_subst id subst = function @@ -257,7 +260,8 @@ let rec clexp_subst id subst = function | CL_rmw _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot substitute into read-modify-write construct" let rec find_function fid = function - | CDEF_fundef (fid', heap_return, args, body) :: _ when Id.compare fid fid' = 0 -> Some (heap_return, args, body) + | CDEF_aux (CDEF_fundef (fid', heap_return, args, body), _) :: _ when Id.compare fid fid' = 0 -> + Some (heap_return, args, body) | cdef :: cdefs -> find_function fid cdefs | [] -> None @@ -524,12 +528,15 @@ let remove_tuples cdefs ctx = let name = "tuple#" ^ Util.string_of_list "_" string_of_ctyp ctyps in let fields = List.mapi (fun n ctyp -> (mk_id (name ^ string_of_int n), ctyp)) ctyps in [ - CDEF_type (CTD_struct (mk_id name, fields)); - CDEF_pragma - ( "tuplestruct", - Util.string_of_list " " - (fun x -> x) - (Util.zencode_string name :: List.map (fun (id, _) -> Util.zencode_string (string_of_id id)) fields) + CDEF_aux (CDEF_type (CTD_struct (mk_id name, fields)), mk_def_annot Parse_ast.Unknown); + CDEF_aux + ( CDEF_pragma + ( "tuplestruct", + Util.string_of_list " " + (fun x -> x) + (Util.zencode_string name :: List.map (fun (id, _) -> Util.zencode_string (string_of_id id)) fields) + ), + mk_def_annot Parse_ast.Unknown ); ] | _ -> assert false diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index 010df51e9..d30af60fd 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -812,7 +812,7 @@ let rec map_funcall f instrs = in I_aux (instr, aux) :: map_funcall f tail -let cdef_map_funcall f = function +let cdef_aux_map_funcall f = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, ctyp, map_funcall f instrs) | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, map_funcall f instrs) | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, map_funcall f instrs) @@ -822,7 +822,9 @@ let cdef_map_funcall f = function | CDEF_type tdef -> CDEF_type tdef | CDEF_pragma (name, str) -> CDEF_pragma (name, str) -let cdef_concatmap_instr f = function +let cdef_map_funcall f (CDEF_aux (aux, def_annot)) = CDEF_aux (cdef_aux_map_funcall f aux, def_annot) + +let cdef_aux_concatmap_instr f = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, ctyp, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_fundef (id, heap_return, args, instrs) -> @@ -833,13 +835,15 @@ let cdef_concatmap_instr f = function | CDEF_type tdef -> CDEF_type tdef | CDEF_pragma (name, str) -> CDEF_pragma (name, str) +let cdef_concatmap_instr f (CDEF_aux (aux, def_annot)) = CDEF_aux (cdef_aux_concatmap_instr f aux, def_annot) + let ctype_def_map_ctyp f = function | CTD_enum (id, ids) -> CTD_enum (id, ids) | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun (id, ctyp) -> (id, f ctyp)) ctors) | CTD_variant (id, ctors) -> CTD_variant (id, List.map (fun (id, ctyp) -> (id, f ctyp)) ctors) (* Map over each ctyp in a cdef using map_instr_ctyp *) -let cdef_map_ctyp f = function +let cdef_aux_map_ctyp f = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, f ctyp, List.map (map_instr_ctyp f) instrs) | CDEF_let (n, bindings, instrs) -> CDEF_let (n, List.map (fun (id, ctyp) -> (id, f ctyp)) bindings, List.map (map_instr_ctyp f) instrs) @@ -851,6 +855,8 @@ let cdef_map_ctyp f = function | CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef) | CDEF_pragma (name, str) -> CDEF_pragma (name, str) +let cdef_map_ctyp f (CDEF_aux (aux, def_annot)) = CDEF_aux (cdef_aux_map_ctyp f aux, def_annot) + let cdef_map_cval f = cdef_map_instr (map_instr_cval f) (* Map over all sequences of instructions contained within an instruction *) @@ -1039,7 +1045,8 @@ let ctype_def_ctyps = function | CTD_struct (_, fields) -> List.map snd fields | CTD_variant (_, ctors) -> List.map snd ctors -let cdef_ctyps = function +let cdef_ctyps (CDEF_aux (aux, _)) = + match aux with | CDEF_register (_, ctyp, instrs) -> CTSet.add ctyp (instrs_ctyps instrs) | CDEF_val (_, _, ctyps, ctyp) -> CTSet.add ctyp (List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty ctyps) | CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) -> instrs_ctyps instrs @@ -1049,7 +1056,8 @@ let cdef_ctyps = function |> CTSet.union (instrs_ctyps instrs) | CDEF_pragma (_, _) -> CTSet.empty -let cdef_ctyps_exist pred = function +let cdef_ctyps_exist pred (CDEF_aux (aux, _)) = + match aux with | CDEF_register (_, ctyp, instrs) -> pred ctyp || instrs_ctyps_exist pred instrs | CDEF_val (_, _, ctyps, ctyp) -> List.exists pred ctyps || pred ctyp | CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) -> instrs_ctyps_exist pred instrs @@ -1061,7 +1069,7 @@ let cdef_ctyps_exist pred = function let cdef_ctyps_has pred cdef = cdef_ctyps_exist (ctyp_has pred) cdef let rec c_ast_registers = function - | CDEF_register (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast + | CDEF_aux (CDEF_register (id, ctyp, instrs), _) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast | _ :: ast -> c_ast_registers ast | [] -> [] diff --git a/src/lib/jib_visitor.ml b/src/lib/jib_visitor.ml index fe23383b1..59b1a1c36 100644 --- a/src/lib/jib_visitor.ml +++ b/src/lib/jib_visitor.ml @@ -237,40 +237,43 @@ and visit_instrs vis outer_instrs = do_visit vis (vis#vinstrs outer_instrs) aux outer_instrs let visit_cdef vis outer_cdef = - let aux vis no_change = - match no_change with + let aux vis (CDEF_aux (aux, def_annot) as no_change) = + match aux with | CDEF_register (id, ctyp, instrs) -> let id' = visit_id vis id in let ctyp' = visit_ctyp vis ctyp in let instrs' = visit_instrs vis instrs in - if id == id' && ctyp == ctyp' && instrs == instrs' then no_change else CDEF_register (id', ctyp', instrs') + if id == id' && ctyp == ctyp' && instrs == instrs' then no_change + else CDEF_aux (CDEF_register (id', ctyp', instrs'), def_annot) | CDEF_type ctd -> let ctd' = visit_ctype_def vis ctd in - if ctd == ctd' then no_change else CDEF_type ctd' + if ctd == ctd' then no_change else CDEF_aux (CDEF_type ctd', def_annot) | CDEF_let (n, bindings, instrs) -> let bindings' = map_no_copy (visit_binding vis) bindings in let instrs' = visit_instrs vis instrs in - if bindings == bindings' && instrs == instrs' then no_change else CDEF_let (n, bindings', instrs') + if bindings == bindings' && instrs == instrs' then no_change + else CDEF_aux (CDEF_let (n, bindings', instrs'), def_annot) | CDEF_val (id, extern, ctyps, ctyp) -> let id' = visit_id vis id in let ctyps' = visit_ctyps vis ctyps in let ctyp' = visit_ctyp vis ctyp in - if id == id' && ctyps == ctyps' && ctyp == ctyp' then no_change else CDEF_val (id', extern, ctyps', ctyp') + if id == id' && ctyps == ctyps' && ctyp == ctyp' then no_change + else CDEF_aux (CDEF_val (id', extern, ctyps', ctyp'), def_annot) | CDEF_fundef (id, ret_id, params, instrs) -> let id' = visit_id vis id in let ret_id' = map_no_copy_opt (visit_id vis) ret_id in let params' = map_no_copy (visit_id vis) params in let instrs' = visit_instrs vis instrs in if id == id' && ret_id == ret_id' && params == params' && instrs == instrs' then no_change - else CDEF_fundef (id', ret_id', params', instrs') + else CDEF_aux (CDEF_fundef (id', ret_id', params', instrs'), def_annot) | CDEF_startup (id, instrs) -> let id' = visit_id vis id in let instrs' = visit_instrs vis instrs in - if id == id' && instrs == instrs' then no_change else CDEF_startup (id', instrs') + if id == id' && instrs == instrs' then no_change else CDEF_aux (CDEF_startup (id', instrs'), def_annot) | CDEF_finish (id, instrs) -> let id' = visit_id vis id in let instrs' = visit_instrs vis instrs in - if id == id' && instrs == instrs' then no_change else CDEF_finish (id', instrs') + if id == id' && instrs == instrs' then no_change else CDEF_aux (CDEF_finish (id', instrs'), def_annot) | CDEF_pragma (_, _) -> no_change in do_visit vis (vis#vcdef outer_cdef) aux outer_cdef diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 1f7f8ef4d..2dbf6b1c8 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -584,21 +584,29 @@ let fix_early_stack_return ret ret_ctyp instrs = rewrite_return instrs let rec insert_heap_returns ret_ctyps = function - | (CDEF_val (id, _, _, ret_ctyp) as cdef) :: cdefs -> + | (CDEF_aux (CDEF_val (id, _, _, ret_ctyp), _) as cdef) :: cdefs -> cdef :: insert_heap_returns (Bindings.add id ret_ctyp ret_ctyps) cdefs - | CDEF_fundef (id, None, args, body) :: cdefs -> + | CDEF_aux (CDEF_fundef (id, None, args, body), def_annot) :: cdefs -> let gs = gensym () in begin match Bindings.find_opt id ret_ctyps with | 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 (name gs) body) :: insert_heap_returns ret_ctyps cdefs + CDEF_aux (CDEF_fundef (id, Some gs, args, fix_early_heap_return (name gs) body), def_annot) + :: insert_heap_returns ret_ctyps cdefs | Some ret_ctyp -> - CDEF_fundef - (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl (id_loc id) ret_ctyp (name gs) :: body)) + CDEF_aux + ( CDEF_fundef + ( id, + None, + args, + fix_early_stack_return (name gs) ret_ctyp (idecl (id_loc id) ret_ctyp (name gs) :: body) + ), + def_annot + ) :: insert_heap_returns ret_ctyps cdefs end - | CDEF_fundef (id, _, _, _) :: _ -> + | CDEF_aux (CDEF_fundef (id, _, _, _), _) :: _ -> Reporting.unreachable (id_loc id) __POS__ "Found function with return already re-written in insert_heap_returns" | cdef :: cdefs -> cdef :: insert_heap_returns ret_ctyps cdefs | [] -> [] @@ -632,8 +640,8 @@ let hoist_id () = name id let hoist_allocations recursive_functions = function - | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions -> [cdef] - | CDEF_fundef (function_id, heap_return, args, body) -> + | CDEF_aux (CDEF_fundef (function_id, _, _, _), _) as cdef when IdSet.mem function_id recursive_functions -> [cdef] + | CDEF_aux (CDEF_fundef (function_id, heap_return, args, body), def_annot) -> let decls = ref [] in let cleanups = ref [] in let rec hoist = function @@ -658,12 +666,12 @@ let hoist_allocations recursive_functions = function | [] -> [] in let body = hoist body in - if !decls = [] then [CDEF_fundef (function_id, heap_return, args, body)] + if !decls = [] then [CDEF_aux (CDEF_fundef (function_id, heap_return, args, body), def_annot)] else [ - CDEF_startup (function_id, List.rev !decls); - CDEF_fundef (function_id, heap_return, args, body); - CDEF_finish (function_id, !cleanups); + CDEF_aux (CDEF_startup (function_id, List.rev !decls), mk_def_annot (gen_loc def_annot.loc)); + CDEF_aux (CDEF_fundef (function_id, heap_return, args, body), def_annot); + CDEF_aux (CDEF_finish (function_id, !cleanups), mk_def_annot (gen_loc def_annot.loc)); ] | cdef -> [cdef] @@ -732,7 +740,8 @@ let remove_alias = | [] -> [] in function - | CDEF_fundef (function_id, heap_return, args, body) -> [CDEF_fundef (function_id, heap_return, args, opt body)] + | CDEF_aux (CDEF_fundef (function_id, heap_return, args, body), def_annot) -> + [CDEF_aux (CDEF_fundef (function_id, heap_return, args, opt body), def_annot)] | cdef -> [cdef] (** This optimization looks for patterns of the form @@ -798,7 +807,7 @@ module Combine_variables = struct end | _ -> DoChildren - method! vcdef = function CDEF_fundef _ -> DoChildren | _ -> SkipChildren + method! vcdef = function CDEF_aux (CDEF_fundef _, _) -> DoChildren | _ -> SkipChildren end end @@ -1821,7 +1830,8 @@ let codegen_alloc = function | I_aux (I_decl (ctyp, id), _) -> string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) | _ -> assert false -let codegen_def' ctx = function +let codegen_def' ctx (CDEF_aux (aux, _)) = + match aux with | CDEF_register (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline @@ -1956,18 +1966,18 @@ let codegen_def ctx def = separate_map hardline codegen_ctg deps ^^ codegen_def' ctx def ) -let is_cdef_startup = function CDEF_startup _ -> true | _ -> false +let is_cdef_startup = function CDEF_aux (CDEF_startup _, _) -> true | _ -> false let sgen_startup = function - | CDEF_startup (id, _) -> Printf.sprintf " startup_%s();" (sgen_function_id id) + | CDEF_aux (CDEF_startup (id, _), _) -> Printf.sprintf " startup_%s();" (sgen_function_id id) | _ -> assert false let sgen_instr id ctx instr = Pretty_print_sail.to_string (codegen_instr id ctx instr) -let is_cdef_finish = function CDEF_startup _ -> true | _ -> false +let is_cdef_finish = function CDEF_aux (CDEF_startup _, _) -> true | _ -> false let sgen_finish = function - | CDEF_startup (id, _) -> Printf.sprintf " finish_%s();" (sgen_function_id id) + | CDEF_aux (CDEF_startup (id, _), _) -> Printf.sprintf " finish_%s();" (sgen_function_id id) | _ -> assert false let get_recursive_functions cdefs = diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 3b7dce0e9..314f819ec 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -1350,12 +1350,12 @@ let smt_ctype_def ctx = function ] let rec generate_ctype_defs ctx = function - | CDEF_type ctd :: cdefs -> smt_ctype_def ctx ctd :: generate_ctype_defs ctx cdefs + | CDEF_aux (CDEF_type ctd, _) :: cdefs -> smt_ctype_def ctx ctd :: generate_ctype_defs ctx cdefs | _ :: cdefs -> generate_ctype_defs ctx cdefs | [] -> [] let rec generate_reg_decs ctx inits = function - | CDEF_register (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits) -> + | CDEF_aux (CDEF_register (id, ctyp, _), _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits) -> Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs | _ :: cdefs -> generate_reg_decs ctx inits cdefs | [] -> [] @@ -1894,8 +1894,9 @@ let smt_cfnode all_cdefs ctx ssa_elems = keep track of any global letbindings between the spec and the fundef, so they can appear in the generated SMT. *) let rec find_function lets id = function - | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 -> (lets, Some (heap_return, args, body)) - | CDEF_let (_, vars, setup) :: cdefs -> + | CDEF_aux (CDEF_fundef (id', heap_return, args, body), _) :: _ when Id.compare id id' = 0 -> + (lets, Some (heap_return, args, body)) + | CDEF_aux (CDEF_let (_, vars, setup), _) :: cdefs -> let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (name id)) vars in find_function (lets @ vars @ setup) id cdefs | _ :: cdefs -> find_function lets id cdefs @@ -2218,7 +2219,8 @@ let smt_instr_list name ctx all_cdefs instrs = (stack, start, cfg) -let smt_cdef props lets name_file ctx all_cdefs smt_includes = function +let smt_cdef props lets name_file ctx all_cdefs smt_includes (CDEF_aux (aux, _)) = + match aux with | CDEF_val (function_id, _, arg_ctyps, ret_ctyp) when Bindings.mem function_id props -> begin match find_function [] function_id all_cdefs with | intervening_lets, Some (None, args, instrs) -> @@ -2305,7 +2307,7 @@ let smt_cdef props lets name_file ctx all_cdefs smt_includes = function | _ -> () let rec smt_cdefs props lets name_file ctx ast smt_includes = function - | CDEF_let (_, vars, setup) :: cdefs -> + | CDEF_aux (CDEF_let (_, vars, setup), _) :: cdefs -> let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (name id)) vars in smt_cdefs props (lets @ vars @ setup) name_file ctx ast smt_includes cdefs | cdef :: cdefs -> @@ -2319,7 +2321,7 @@ let rec smt_cdefs props lets name_file ctx ast smt_includes = function all the registers that such a reference could be pointing to. *) let rec build_register_map rmap = function - | CDEF_register (reg, ctyp, _) :: cdefs -> + | CDEF_aux (CDEF_register (reg, ctyp, _), _) :: cdefs -> let rmap = match CTMap.find_opt ctyp rmap with | Some regs -> CTMap.add ctyp (reg :: regs) rmap diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index ba68b79ae..f7d69bbfb 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -824,7 +824,7 @@ module Make (Config : CONFIG) = struct List.fold_left (fun rmap cdef -> match cdef with - | CDEF_register (id, ctyp, _) -> + | CDEF_aux (CDEF_register (id, ctyp, _), _) -> CTMap.update ctyp (function Some ids -> Some (id :: ids) | None -> Some [id]) rmap | _ -> rmap ) @@ -910,7 +910,8 @@ module Make (Config : CONFIG) = struct let empty_cdef_doc = { outside_module = empty; inside_module_prefix = empty; inside_module = empty } - let sv_cdef ctx fn_ctyps setup_calls = function + let sv_cdef ctx fn_ctyps setup_calls (CDEF_aux (aux, _)) = + match aux with | CDEF_register (id, ctyp, setup) -> let binding_doc = wrap_type ctyp (sv_id id) ^^ semi ^^ twice hardline in let name = sprintf "sail_setup_reg_%s" (sv_id_string id) in @@ -957,7 +958,7 @@ module Make (Config : CONFIG) = struct let main_args main fn_ctyps = match main with - | Some (CDEF_fundef (f, _, params, body)) -> begin + | Some (CDEF_aux (CDEF_fundef (f, _, params, body), _)) -> begin match Bindings.find_opt f fn_ctyps with | Some (param_ctyps, ret_ctyp) -> begin let main_args = diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 4568c2eda..081a6f3a9 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -321,7 +321,7 @@ end let register_types cdefs = List.fold_left - (fun acc cdef -> match cdef with CDEF_register (id, ctyp, _) -> Bindings.add id ctyp acc | _ -> acc) + (fun acc cdef -> match cdef with CDEF_aux (CDEF_register (id, ctyp, _), _) -> Bindings.add id ctyp acc | _ -> acc) Bindings.empty cdefs let jib_of_ast make_call_precise env ast effect_info = @@ -495,7 +495,7 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = separate empty (List.filter_map (function - | CDEF_register (id, ctyp, _) -> + | CDEF_aux (CDEF_register (id, ctyp, _), _) -> Some (SV.sv_id id ^^ space ^^ equals ^^ space ^^ sv_id id ^^ string "_in" ^^ semi ^^ hardline) | _ -> None ) @@ -509,7 +509,7 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = separate empty (List.filter_map (function - | CDEF_register (id, ctyp, _) -> + | CDEF_aux (CDEF_register (id, ctyp, _), _) -> Some (sv_id id ^^ string "_out" ^^ space ^^ equals ^^ space ^^ sv_id id ^^ semi ^^ hardline) | _ -> None ) @@ -518,7 +518,9 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = else empty in - let main = List.find_opt (function CDEF_fundef (id, _, _, _) -> sv_id_string id = "main" | _ -> false) cdefs in + let main = + List.find_opt (function CDEF_aux (CDEF_fundef (id, _, _, _), _) -> sv_id_string id = "main" | _ -> false) cdefs + in let main_args, main_result, module_main_in_out = main_args main fn_ctyps in let invoke_main_body = @@ -542,7 +544,8 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = if !opt_inregs then List.filter_map (function - | CDEF_register (id, ctyp, _) -> Some (string "input" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_in")) + | CDEF_aux (CDEF_register (id, ctyp, _), _) -> + Some (string "input" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_in")) | _ -> None ) cdefs @@ -553,7 +556,8 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = if !opt_inregs then List.filter_map (function - | CDEF_register (id, ctyp, _) -> Some (string "output" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_out")) + | CDEF_aux (CDEF_register (id, ctyp, _), _) -> + Some (string "output" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_out")) | _ -> None ) cdefs