diff --git a/lib/sv/sail_modules.sv b/lib/sv/sail_modules.sv index 69d1e7278..55a07687e 100644 --- a/lib/sv/sail_modules.sv +++ b/lib/sv/sail_modules.sv @@ -4,6 +4,9 @@ // The Sail unit type. typedef enum logic [0:0] {SAIL_UNIT=0} sail_unit; +// The Sail zero-width bitvector. +typedef enum logic [0:0] {SAIL_ZWBV=0} sail_zwbv; + module print (input string in_str, input string in_sail_stdout, diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index 4f49cdf9d..814771a58 100644 --- a/src/lib/jib_optimize.ml +++ b/src/lib/jib_optimize.ml @@ -185,8 +185,13 @@ let rec cval_map_id f = function | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_map_id f cval)) fields, ctyp) | V_tuple (members, ctyp) -> V_tuple (List.map (cval_map_id f) members, ctyp) -let remove_undefined = - let gensym, _ = symbol_generator "gz" in +module Remove_undefined = struct + open Jib + open Jib_util + open Jib_visitor + + let gensym, _ = symbol_generator "gz" + let rec create_value l = function | CT_unit -> ([], V_lit (VL_unit, CT_unit)) | CT_bool -> ([], V_lit (VL_bool false, CT_bool)) @@ -205,16 +210,56 @@ let remove_undefined = | ctyp -> let gs = name (gensym ()) in ([idecl l ctyp gs], V_id (gs, ctyp)) - in - let rewrite_instr = function - | I_aux (I_undefined ctyp, (_, l)) -> - let setup, value = create_value l ctyp in - begin - match setup with [] -> ireturn value | _ -> iblock (setup @ [ireturn value]) - end - | instr -> instr - in - map_instr_list rewrite_instr + + class visitor : jib_visitor = + object + inherit empty_jib_visitor + + method! vctyp _ = SkipChildren + method! vcval _ = SkipChildren + + method! vinstr = + function + | I_aux (I_undefined ctyp, (_, l)) -> + let setup, value = create_value l ctyp in + ChangeTo (iblock (setup @ [icopy l (CL_id (return, ctyp)) value; iend l])) + | _ -> DoChildren + end +end + +let remove_undefined = Jib_visitor.visit_instrs (new Remove_undefined.visitor) + +module Remove_functions_to_references = struct + open Jib + open Jib_util + open Jib_visitor + + let gensym, _ = symbol_generator "gref" + + class visitor : jib_visitor = + object + inherit empty_jib_visitor + + method! vctyp _ = SkipChildren + method! vcval _ = SkipChildren + + method! vinstr = + function + | I_aux (I_funcall (CR_one (CL_addr (CL_id (id, CT_ref reg_ctyp))), ext, f, args), (n, l)) -> + let gs = name (gensym ()) in + ChangeTo + (iblock + [ + idecl l reg_ctyp gs; + I_aux (I_funcall (CR_one (CL_id (gs, reg_ctyp)), ext, f, args), (n, l)); + icopy l (CL_addr (CL_id (id, CT_ref reg_ctyp))) (V_id (gs, reg_ctyp)); + ] + ) + | _ -> DoChildren + end +end + +let remove_functions_to_references = Jib_visitor.visit_instrs (new Remove_functions_to_references.visitor) let rec instrs_subst id subst = function | I_aux (I_decl (_, id'), _) :: _ as instrs when Name.compare id id' = 0 -> instrs diff --git a/src/lib/jib_optimize.mli b/src/lib/jib_optimize.mli index d856813cb..2393601b7 100644 --- a/src/lib/jib_optimize.mli +++ b/src/lib/jib_optimize.mli @@ -86,6 +86,8 @@ val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list val remove_undefined : instr list -> instr list +val remove_functions_to_references : instr list -> instr list + val remove_clear : instr list -> instr list (** Remove gotos immediately followed by the label it jumps to *) diff --git a/src/lib/jib_ssa.ml b/src/lib/jib_ssa.ml index f23f72624..8b71543ce 100644 --- a/src/lib/jib_ssa.ml +++ b/src/lib/jib_ssa.ml @@ -532,7 +532,7 @@ let phi_dependencies cfg = done; (!deps, !decl_nodes) -let rename_variables graph root children = +let rename_variables globals graph root children = let counts = ref NameMap.empty in let stacks = ref NameMap.empty in @@ -554,8 +554,11 @@ let rename_variables graph root children = let rec fold_cval = function | V_id (id, ctyp) -> - let i = top_stack id in - V_id (ssa_name i id, ctyp) + if NameSet.mem id globals then V_id (id, ctyp) + else ( + let i = top_stack id in + V_id (ssa_name i id, ctyp) + ) | V_member (id, ctyp) -> V_member (id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) | V_call (id, fs) -> V_call (id, List.map fold_cval fs) @@ -862,8 +865,16 @@ let make_dominators_dot out_chan idom graph = output_string out_chan "}\n"; Util.opt_colors := true -let ssa ?debug_prefix instrs = +let ssa ?globals ?debug_prefix instrs = let start, finish, cfg = control_flow_graph instrs in + begin + match debug_prefix with + | Some prefix -> + let out_chan = open_out (prefix ^ "_cfg.gv") in + make_dot out_chan cfg; + close_out out_chan + | None -> () + end; let idom = immediate_dominators cfg start in let post_idom = immediate_dominators ~post:true cfg finish in begin @@ -879,6 +890,6 @@ let ssa ?debug_prefix instrs = let df = dominance_frontiers cfg start idom children in let post_df = dominance_frontiers ~post:true cfg finish post_idom post_children in place_phi_functions cfg df; - rename_variables cfg start children; + rename_variables (Option.value ~default:NameSet.empty globals) cfg start children; place_pi_functions ~start ~finish ~post_idom ~post_df cfg; (start, cfg) diff --git a/src/lib/jib_ssa.mli b/src/lib/jib_ssa.mli index 0f5383bec..5f50eb276 100644 --- a/src/lib/jib_ssa.mli +++ b/src/lib/jib_ssa.mli @@ -131,7 +131,7 @@ end val phi_dependencies : (ssa_elem list * cf_node) array_graph -> NameGraph.graph * int NameMap.t (** Convert a list of instructions into SSA form *) -val ssa : ?debug_prefix:string -> Jib.instr list -> int * (ssa_elem list * cf_node) array_graph +val ssa : ?globals:NameSet.t -> ?debug_prefix:string -> Jib.instr list -> int * (ssa_elem list * cf_node) array_graph (** Output the control-flow graph in graphviz format for debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index 242138bca..fa1fd1019 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -1091,6 +1091,13 @@ let ctype_def_ctyps = function | CTD_struct (_, fields) -> List.map snd fields | CTD_variant (_, ctors) -> List.map snd ctors +let ctype_def_id = function CTD_enum (id, _) -> id | CTD_struct (id, _) -> id | CTD_variant (id, _) -> id + +let ctype_def_to_ctyp = function + | CTD_enum (id, ids) -> CT_enum (id, ids) + | CTD_struct (id, fields) -> CT_struct (id, fields) + | CTD_variant (id, ctors) -> CT_variant (id, ctors) + let cdef_ctyps (CDEF_aux (aux, _)) = match aux with | CDEF_register (_, ctyp, instrs) -> CTSet.add ctyp (instrs_ctyps instrs) diff --git a/src/lib/jib_util.mli b/src/lib/jib_util.mli index 4cdfcc58e..56c39d59f 100644 --- a/src/lib/jib_util.mli +++ b/src/lib/jib_util.mli @@ -191,6 +191,12 @@ val cdef_ctyps : cdef -> CTSet.t val cdef_ctyps_has : (ctyp -> bool) -> cdef -> bool +(** {2 Type definitions} *) + +val ctype_def_id : ctype_def -> id + +val ctype_def_to_ctyp : ctype_def -> ctyp + (** {1 Functions for mapping over and extracting information from instructions, values, and definitions} *) val instr_ids : instr -> NameSet.t diff --git a/src/lib/smt_exp.ml b/src/lib/smt_exp.ml index 38b84c35c..8bd97f19a 100644 --- a/src/lib/smt_exp.ml +++ b/src/lib/smt_exp.ml @@ -108,6 +108,8 @@ type smt_exp = | Hd of string * smt_exp | Tl of string * smt_exp +let var_id id = Var (Name (id, -1)) + let rec fold_smt_exp f = function | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args)) | Ite (cond, t, e) -> f (Ite (fold_smt_exp f cond, fold_smt_exp f t, fold_smt_exp f e)) @@ -164,9 +166,13 @@ let simp_or xs = | [x] -> x | _ -> if List.exists (function Bool_lit true -> true | _ -> false) xs then Bool_lit true else Fn ("or", xs) +let simp_eq x y = + match (x, y) with Bool_lit x, Bool_lit y -> Some (x = y) | Bitvec_lit x, Bitvec_lit y -> Some (x = y) | _ -> None + let simp_fn f args = let open Sail2_operators_bitlists in match (f, args) with + | "=", [x; y] -> begin match simp_eq x y with Some b -> Bool_lit b | None -> Fn (f, args) end | "not", [Fn ("not", [exp])] -> exp | "not", [Bool_lit b] -> Bool_lit (not b) | "contents", [Fn ("Bits", [_; bv])] -> bv @@ -233,8 +239,13 @@ let rec simp vars exp = | exp -> Extract (n, m, exp) end | Store (info, store_fn, arr, i, x) -> Store (info, store_fn, simp vars arr, simp vars i, simp vars x) - | Ite (Fn ("not", [cond]), then_exp, else_exp) -> simp vars (Ite (cond, else_exp, then_exp)) - | Ite (cond, then_exp, else_exp) -> Ite (simp vars cond, simp vars then_exp, simp vars else_exp) + | Ite (cond, then_exp, else_exp) -> begin + match Ite (simp vars cond, simp vars then_exp, simp vars else_exp) with + | Ite (Bool_lit true, then_exp, _) -> then_exp + | Ite (Bool_lit false, _, else_exp) -> else_exp + | Ite (Fn ("not", [cond]), then_exp, else_exp) -> Ite (cond, else_exp, then_exp) + | exp -> exp + end | Tester (ctor, exp) -> Tester (ctor, simp vars exp) | Unwrap (ctor, b, exp) -> Unwrap (ctor, b, simp vars exp) | Field (struct_id, field_id, exp) -> Field (struct_id, field_id, simp vars exp) diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index ed24448b1..15695e6d7 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -919,7 +919,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* vec = smt_cval vec in let* i = bind (smt_cval i) - (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp)) + (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp)) in return (Fn ("select", [vec; i])) (* @@ -998,7 +998,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* x = smt_cval x in let* i = bind (smt_cval i) - (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp)) + (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp)) in return (Store (Fixed len, store_fn, vec, i, x)) (* diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 7c161a1f0..1378f5809 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -320,7 +320,7 @@ module Make (Config : CONFIG) = struct return (mk_variant (zencode_upper_id id) ctors) | CT_fvector (n, ctyp) -> let* ctyp = smt_ctyp ctyp in - return (Array (Bitvec (required_width (Big_int.of_int (n - 1))), ctyp)) + return (Array (Bitvec (required_width (Big_int.of_int (n - 1)) - 1), ctyp)) | CT_vector ctyp -> let* ctyp = smt_ctyp ctyp in return (Array (Bitvec vector_index_width, ctyp)) @@ -571,10 +571,10 @@ module Make (Config : CONFIG) = struct else if extern && string_of_id function_id = "internal_vector_update" then begin match args with | [vec; i; x] -> - let sz = required_width (Big_int.of_int (Smt.generic_vector_length (cval_ctyp vec) - 1)) in + let sz = required_width (Big_int.of_int (Smt.generic_vector_length (cval_ctyp vec) - 1)) - 1 in let* vec = Smt.smt_cval vec in let* i = - Smt_gen.bind (Smt.smt_cval i) (Smt_gen.signed_size ~into:sz ~from:(Smt.int_size (cval_ctyp i))) + Smt_gen.bind (Smt.smt_cval i) (Smt_gen.unsigned_size ~into:sz ~from:(Smt.int_size (cval_ctyp i))) in let* x = Smt.smt_cval x in singleton (define_const id ret_ctyp (Fn ("store", [vec; i; x]))) @@ -841,6 +841,8 @@ module Make (Config : CONFIG) = struct List.iter (fun include_file -> output_string out_chan (Util.read_whole_file include_file)) smt_includes; let queue = Queue_optimizer.optimize stack in + + (* let queue = Queue.of_seq (List.to_seq (List.rev (List.of_seq (Stack.to_seq stack)))) in *) Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); @@ -848,7 +850,6 @@ module Make (Config : CONFIG) = struct ) queue; - (* (Queue.of_seq (List.to_seq (List.rev (List.of_seq (Stack.to_seq stack))))); *) output_string out_chan "(check-sat)\n"; if prop_type = "counterexample" then output_string out_chan "(get-model)\n"; diff --git a/src/sail_sv_backend/generate_primop2.ml b/src/sail_sv_backend/generate_primop2.ml index d9b456d74..96e035719 100644 --- a/src/sail_sv_backend/generate_primop2.ml +++ b/src/sail_sv_backend/generate_primop2.ml @@ -74,6 +74,8 @@ module type S = sig val get_generated_library_defs : unit -> sv_def list + val string_of_fbits : int -> string + val hex_str : unit -> string val dec_str : unit -> string @@ -244,6 +246,38 @@ module Make } ) + let string_of_fbits width = + let function_name = pf "sail_string_of_bits_%d" width in + register_library_def function_name (fun () -> + let b = primop_name "b" in + let bstr = primop_name "bstr" in + let zeros = primop_name "zeros" in + let vars = [SVS_var (bstr, CT_string, None); SVS_var (zeros, CT_string, None)] in + let body = + if width mod 4 = 0 then + [ + svs_raw "bstr.hextoa(b)" ~inputs:[b] ~outputs:[bstr]; + svs_raw (pf "zeros = \"%s\"" (String.make (width / 4) '0')) ~outputs:[zeros]; + svs_raw + (pf "return {\"0x\", zeros.substr(0, %d - bstr.len()), bstr.toupper()}" ((width / 4) - 1)) + ~inputs:[zeros; bstr]; + ] + else + [ + svs_raw "bstr.bintoa(b)" ~inputs:[b] ~outputs:[bstr]; + svs_raw (pf "zeros = \"%s\"" (String.make width '0')) ~outputs:[zeros]; + svs_raw (pf "return {\"0b\", zeros.substr(0, %d - bstr.len()), bstr}" (width - 1)) ~inputs:[zeros; bstr]; + ] + in + SVD_fundef + { + function_name = SVN_string function_name; + return_type = Some CT_string; + params = [(mk_id "b", CT_fbits width)]; + body = mk_statement (SVS_block (List.map mk_statement (vars @ body))); + } + ) + let print_int () = let name = "sail_print_int" in register_library_def name (fun () -> diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 3559e49e6..36466eb44 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -82,16 +82,11 @@ open Sv_ir module IntSet = Util.IntSet -class footprint_visitor ctx registers references reads writes need_stdout need_stderr : jib_visitor = +class footprint_visitor ctx registers references reads writes throws need_stdout need_stderr : jib_visitor = object inherit empty_jib_visitor - method! vctyp = - function - | CT_ref ctyp -> - references := CTSet.add ctyp !references; - DoChildren - | _ -> DoChildren + method! vctyp _ = SkipChildren method! vcval = function @@ -109,19 +104,32 @@ class footprint_visitor ctx registers references reads writes need_stdout need_s method! vinstr = function - | I_aux (I_funcall (_, _, (id, _), _), _) -> + | I_aux (I_funcall (_, _, (id, _), args), _) -> if ctx_is_extern id ctx then ( let name = ctx_get_extern id ctx in if name = "print" || name = "print_endline" || name = "print_bits" || name = "print_int" then need_stdout := true else if name = "prerr" || name = "prerr_endline" || name = "prerr_bits" || name = "prerr_int" then need_stderr := true + else if name = "reg_deref" then ( + match args with + | [cval] -> begin + match cval_ctyp cval with CT_ref reg_ctyp -> references := CTSet.add reg_ctyp !references | _ -> () + end + | _ -> () + ) ); DoChildren | _ -> DoChildren method! vclexp = function + | CL_addr clexp -> + references := CTSet.add (clexp_ctyp clexp) !references; + DoChildren + | CL_id (Have_exception _, _) -> + throws := true; + SkipChildren | CL_id (Name (id, _), local_ctyp) -> begin match Bindings.find_opt id registers with @@ -138,8 +146,10 @@ class footprint_visitor ctx registers references reads writes need_stdout need_s type footprint = { direct_reads : IdSet.t; direct_writes : IdSet.t; + direct_throws : bool; all_reads : IdSet.t; all_writes : IdSet.t; + throws : bool; need_stdout : bool; need_stderr : bool; } @@ -151,10 +161,16 @@ type spec_info = { registers : ctyp Bindings.t; (* A list of constructor functions *) constructors : IdSet.t; + (* Global letbindings *) + global_lets : NameSet.t; + (* Global let numbers *) + global_let_numbers : IntSet.t; (* Function footprint information *) footprints : footprint Bindings.t; (* Specification callgraph *) callgraph : IdGraph.graph; + (* The type of exceptions *) + exception_ctyp : ctyp; } let collect_spec_info ctx cdefs = @@ -182,6 +198,16 @@ let collect_spec_info ctx cdefs = ) IdSet.empty cdefs in + let global_lets, global_let_numbers = + List.fold_left + (fun (names, nums) cdef -> + match cdef with + | CDEF_aux (CDEF_let (n, bindings, _), _) -> + (List.fold_left (fun acc (id, _) -> NameSet.add (name id) acc) names bindings, IntSet.add n nums) + | _ -> (names, nums) + ) + (NameSet.empty, IntSet.empty) cdefs + in let footprints = List.fold_left (fun footprints cdef -> @@ -189,11 +215,14 @@ let collect_spec_info ctx cdefs = | CDEF_aux (CDEF_fundef (f, _, _, body), _) -> let reads = ref IdSet.empty in let writes = ref IdSet.empty in + let throws = ref false in let references = ref CTSet.empty in let need_stdout = ref false in let need_stderr = ref false in let _ = - visit_cdef (new footprint_visitor ctx registers references reads writes need_stdout need_stderr) cdef + visit_cdef + (new footprint_visitor ctx registers references reads writes throws need_stdout need_stderr) + cdef in CTSet.iter (fun ctyp -> @@ -206,8 +235,10 @@ let collect_spec_info ctx cdefs = { direct_reads = !reads; direct_writes = !writes; + direct_throws = !throws; all_reads = IdSet.empty; all_writes = IdSet.empty; + throws = false; need_stdout = !need_stdout; need_stderr = !need_stderr; } @@ -224,29 +255,54 @@ let collect_spec_info ctx cdefs = | CDEF_aux (CDEF_fundef (f, _, _, body), _) -> let footprint = Bindings.find f footprints in let callees = cfg |> IdGraph.reachable (IdSet.singleton f) IdSet.empty |> IdSet.remove f in - let all_reads, all_writes, need_stdout, need_stderr = + let all_reads, all_writes, throws, need_stdout, need_stderr = List.fold_left - (fun (all_reads, all_writes, need_stdout, need_stderr) callee -> + (fun (all_reads, all_writes, throws, need_stdout, need_stderr) callee -> match Bindings.find_opt callee footprints with | Some footprint -> ( IdSet.union all_reads footprint.direct_reads, IdSet.union all_writes footprint.direct_writes, + throws || footprint.direct_throws, need_stdout || footprint.need_stdout, need_stderr || footprint.need_stderr ) - | _ -> (all_reads, all_writes, need_stdout, need_stderr) + | _ -> (all_reads, all_writes, throws, need_stdout, need_stderr) + ) + ( footprint.direct_reads, + footprint.direct_writes, + footprint.direct_throws, + footprint.need_stdout, + footprint.need_stderr ) - (footprint.direct_reads, footprint.direct_writes, footprint.need_stdout, footprint.need_stderr) (IdSet.elements callees) in Bindings.update f - (fun _ -> Some { footprint with all_reads; all_writes; need_stdout; need_stderr }) + (fun _ -> Some { footprint with all_reads; all_writes; throws; need_stdout; need_stderr }) footprints | _ -> footprints ) footprints cdefs in - { register_ctyp_map; registers; constructors; footprints; callgraph = cfg } + let exception_ctyp = + List.fold_left + (fun ctyp cdef -> + match cdef with + | CDEF_aux (CDEF_type ctd, _) when Id.compare (ctype_def_id ctd) (mk_id "exception") = 0 -> + ctype_def_to_ctyp ctd + | _ -> ctyp + ) + CT_unit cdefs + in + { + register_ctyp_map; + registers; + constructors; + global_lets; + global_let_numbers; + footprints; + callgraph = cfg; + exception_ctyp; + } module type CONFIG = sig val max_unknown_integer_width : int @@ -330,6 +386,7 @@ module Make (Config : CONFIG) = struct let rec sv_ctyp = function | CT_bool -> simple_type "bit" | CT_bit -> simple_type "logic" + | CT_fbits 0 -> simple_type "sail_zwbv" | CT_fbits width -> ksprintf simple_type "logic [%d:0]" (width - 1) | CT_sbits max_width -> let logic = sprintf "logic [%d:0]" (max_width - 1) in @@ -382,7 +439,7 @@ module Make (Config : CONFIG) = struct let string_of_bits l = function | CT_lbits -> "sail_string_of_bits" | CT_fbits sz when Config.nostrings -> Generate_primop.string_of_fbits_stub sz - | CT_fbits sz -> Generate_primop.string_of_fbits sz + | CT_fbits sz -> Primops.string_of_fbits sz | _ -> Reporting.unreachable l __POS__ "string_of_bits" let dec_str l = function @@ -474,11 +531,6 @@ module Make (Config : CONFIG) = struct ) ^^ space ^^ sv_type_id id ^^ semi | CTD_variant (id, ctors) -> - let exception_boilerplate = - if Id.compare id (mk_id "exception") = 0 then - twice hardline ^^ ksprintf string "%s sail_current_exception;" (sv_type_id_string id) - else empty - in let kind_id (id, _) = string_of_id id |> Util.zencode_string |> String.uppercase_ascii |> string in let sv_ctor (id, ctyp) = wrap_type ctyp (pp_id id) in let tag_type = string ("sailtag_" ^ pp_id_string id) in @@ -632,7 +684,6 @@ module Make (Config : CONFIG) = struct ] ^^ twice hardline ^^ separate (twice hardline) constructors - ^^ exception_boilerplate ) else ( let constructors = @@ -673,7 +724,6 @@ module Make (Config : CONFIG) = struct ] ^^ twice hardline ^^ separate (twice hardline) constructors - ^^ exception_boilerplate ) let sv_signed x = string "signed'" ^^ parens x @@ -713,6 +763,7 @@ module Make (Config : CONFIG) = struct let pp_smt_parens exp = pp_smt ~need_parens:true exp in let opt_parens doc = if need_parens then parens doc else doc in function + | Bitvec_lit [] -> string "SAIL_ZWBV" | Bitvec_lit bits -> let len = List.length bits in if len mod 4 = 0 && not (has_undefined_bit bits) then ksprintf string "%d'h%s" len (hex_bitvector bits) @@ -849,21 +900,21 @@ module Make (Config : CONFIG) = struct (updates, SVP_field (lexp, field)) | CL_void -> ([], SVP_void) | CL_rmw (id_from, id, ctyp) -> - let rec assignments lexp ctyp = function + let rec assignments lexp subpart ctyp = function | parent :: parents -> begin match ctyp with | CT_struct (struct_id, fields) -> let _, field_ctyp = List.find (fun (f, _) -> Id.compare f parent = 0) fields in let other_fields = List.filter (fun (f, _) -> Id.compare f parent <> 0) fields in - assignments (SVP_field (lexp, parent)) field_ctyp parents + assignments (SVP_field (lexp, parent)) (Field (struct_id, parent, subpart)) field_ctyp parents @ List.map - (fun (f, _) -> SVS_assign (SVP_field (lexp, f), Field (struct_id, f, Var id_from))) + (fun (f, _) -> SVS_assign (SVP_field (lexp, f), Field (struct_id, f, subpart))) other_fields | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "expected struct type" end | [] -> [] in - let updates = assignments (SVP_id id) ctyp parents in + let updates = assignments (SVP_id id) (Var id_from) ctyp parents in (updates, SVP_id id) | CL_addr _ | CL_tuple _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "addr/tuple" @@ -949,16 +1000,40 @@ module Make (Config : CONFIG) = struct | [arr; i; x] -> begin match cval_ctyp arr with | CT_fvector (len, _) -> + let* arr = Smt.smt_cval arr in + let sz = required_width (Big_int.of_int (len - 1)) - 1 in let* i = Smt_gen.bind (Smt.smt_cval i) - (Smt_gen.unsigned_size ~checked:false - ~into:(required_width (Big_int.of_int (len - 1)) - 1) - ~from:(Smt.int_size (cval_ctyp i)) - ) + (Smt_gen.unsigned_size ~checked:false ~into:sz ~from:(Smt.int_size (cval_ctyp i))) in let* x = Smt.smt_cval x in + let j = mk_id "j" in let updates, ret = svir_creturn creturn in - wrap (with_updates l updates (SVS_assign (SVP_index (ret, i), x))) + begin + match (ret, arr) with + | SVP_id id1, Var id2 when Name.compare id1 id2 = 0 -> + wrap (with_updates l updates (SVS_assign (SVP_index (ret, i), x))) + | _ -> + wrap + (with_updates l updates + (SVS_foreach + ( SVN_id j, + arr, + SVS_aux + ( SVS_assign + ( SVP_index (ret, var_id j), + Ite + ( Fn ("=", [Extract (sz - 1, 0, var_id j); i]), + x, + Fn ("select", [arr; var_id j]) + ) + ), + l + ) + ) + ) + ) + end | _ -> Reporting.unreachable l __POS__ "Invalid vector type for internal vector update" end | _ -> Reporting.unreachable l __POS__ "Invalid number of arguments to internal vector update" @@ -1009,6 +1084,10 @@ module Make (Config : CONFIG) = struct | SVS_assert (cond, msg) -> separate space [string "assert"; parens (pp_smt cond); string "else"; string "$error" ^^ parens (pp_smt msg)] ^^ terminator + | SVS_foreach (i, exp, stmt) -> + separate space [string "foreach"; parens (pp_smt exp ^^ brackets (pp_sv_name i))] + ^^ nest 4 (hardline ^^ pp_statement ~terminator:empty stmt) + ^^ terminator | SVS_var (id, ctyp, init_opt) -> begin match init_opt with | Some init -> ld ^^ separate space [wrap_type ctyp (pp_name id); equals; pp_smt init] ^^ terminator @@ -1152,6 +1231,11 @@ module Make (Config : CONFIG) = struct (fun id -> CL_id (Name (id, -1), Bindings.find id spec_info.registers)) (IdSet.elements footprint.all_writes) in + let throws = + if footprint.throws then + [CL_id (Have_exception (-1), CT_bool); CL_id (Current_exception (-1), spec_info.exception_ctyp)] + else [] + in let channels = (if footprint.need_stdout then [Channel (Chan_stdout, -1)] else []) @ if footprint.need_stderr then [Channel (Chan_stderr, -1)] else [] @@ -1161,7 +1245,11 @@ module Make (Config : CONFIG) = struct ChangeTo (I_aux ( I_funcall - (CR_multi ((clexp :: writes) @ output_channels), ext, (f, []), args @ reads @ input_channels), + ( CR_multi ((clexp :: writes) @ throws @ output_channels), + ext, + (f, []), + args @ reads @ input_channels + ), iannot ) ) @@ -1300,10 +1388,20 @@ module Make (Config : CONFIG) = struct | _ -> ssa_name in if num_succs = 0 then ssa_name - else ( - assert (num_succs = 1); + else + (* Note if we have successors like + + A + / \ + B C + \ / + D + + There could be updates in D, but there cannot be any in + B or C because then D would have a phi function, and we + would then have started from there. Therefore we can + just choose a single successor here. *) explore_successors (IntSet.min_elt succs) name ssa_name - ) | None -> assert false in let final_names = @@ -1357,7 +1455,11 @@ module Make (Config : CONFIG) = struct (List.map (fun (I_aux (_, (_, l)) as instr) -> string_of_instr instr ^ " " ^ Reporting.short_loc_to_string l) body); let open Jib_ssa in - let start, cfg = ssa (visit_instrs (new thread_registers ctx spec_info) body) in + let start, cfg = + ssa ~globals:spec_info.global_lets + ?debug_prefix:(Option.map (fun _ -> string_of_id f) debug_attr) + (visit_instrs (new thread_registers ctx spec_info) body) + in if Option.is_some debug_attr && not (debug_attr_skip_graph debug_attr) then dump_graph (string_of_id f) cfg; @@ -1452,17 +1554,39 @@ module Make (Config : CONFIG) = struct else [] in + let register_passthroughs = Queue.create () in + let output_register name = + match NameMap.find name final_names with + | Name (id, 0) -> + Queue.add + (SVS_aux (SVS_assign (SVP_id (Name (id, 1)), Var (Name (id, 0))), Parse_ast.Unknown)) + register_passthroughs; + Name (id, 1) + | name -> name + in + let output_ports : sv_module_port list = [{ name = NameMap.find Jib_util.return final_names; external_name = "sail_return"; typ = ret_ctyp }] @ List.map (fun id -> { - name = NameMap.find (Name (id, -1)) final_names; + name = output_register (Name (id, -1)); external_name = string_of_id (prepend_id "out_" id); typ = Bindings.find id spec_info.registers; } ) (IdSet.elements footprint.all_writes) + @ ( if footprint.throws then + [ + { name = NameMap.find (Have_exception (-1)) final_names; external_name = "have_exception"; typ = CT_bool }; + { + name = NameMap.find (Current_exception (-1)) final_names; + external_name = "current_exception"; + typ = spec_info.exception_ctyp; + }; + ] + else [] + ) @ ( if footprint.need_stdout then [ { @@ -1486,38 +1610,50 @@ module Make (Config : CONFIG) = struct NameMap.iter (fun name nums -> let get_ctyp = function - | Return _ -> ret_ctyp + | Return _ -> Some ret_ctyp | Name (id, _) -> begin match Bindings.find_opt id spec_info.registers with - | Some ctyp -> ctyp + | Some ctyp -> Some ctyp | None -> ( match Bindings.find_opt id !declvars with - | Some ctyp -> ctyp + | Some ctyp -> Some ctyp | None -> ( match Util.list_index (fun p -> Id.compare p id = 0) params with - | Some i -> List.nth param_ctyps i - | None -> failwith ("Not sure what this is: " ^ string_of_id id) + | Some i -> Some (List.nth param_ctyps i) + | None -> None ) ) end - | Channel _ -> CT_string - | Have_exception _ -> CT_bool - | Throw_location _ -> CT_string - | Current_exception _ -> failwith "current_exception" + | Channel _ -> Some CT_string + | Have_exception _ -> Some CT_bool + | Throw_location _ -> Some CT_string + | Current_exception _ -> Some spec_info.exception_ctyp in - let ctyp = get_ctyp name in - IntSet.iter - (fun n -> - let name = Jib_ssa.ssa_name n name in - if - List.for_all (fun (port : sv_module_port) -> Name.compare name port.name <> 0) (input_ports @ output_ports) - then Queue.add (SVD_var (name, ctyp)) module_vars - ) - nums + match get_ctyp name with + | Some ctyp -> + IntSet.iter + (fun n -> + let name = Jib_ssa.ssa_name n name in + if + List.for_all + (fun (port : sv_module_port) -> Name.compare name port.name <> 0) + (input_ports @ output_ports) + then Queue.add (SVD_var (name, ctyp)) module_vars + ) + nums + | None -> () ) !ssa_vars; - let defs = List.of_seq (Queue.to_seq module_vars) @ List.rev module_instantiation_defs @ always_comb_def in + let passthroughs = + match List.of_seq (Queue.to_seq register_passthroughs) with + | [] -> [] + | statements -> [SVD_always_comb (SVS_aux (SVS_block statements, Parse_ast.Unknown))] + in + + let defs = + passthroughs @ List.of_seq (Queue.to_seq module_vars) @ List.rev module_instantiation_defs @ always_comb_def + in { name = SVN_id f; input_ports; output_ports; defs } let toplevel_module spec_info = @@ -1533,6 +1669,11 @@ module Make (Config : CONFIG) = struct ) spec_info.registers ([], []) in + let throws_outputs = + if footprint.throws then + [SVD_var (Have_exception (-1), CT_bool); SVD_var (Current_exception (-1), spec_info.exception_ctyp)] + else [] + in let channel_outputs = (if footprint.need_stdout then [SVD_var (Name (mk_id "out_stdout", -1), CT_string)] else []) @ if footprint.need_stderr then [SVD_var (Name (mk_id "out_stderr", -1), CT_string)] else [] @@ -1553,12 +1694,19 @@ module Make (Config : CONFIG) = struct output_connections = ([SVP_id Jib_util.return] @ List.map (fun reg -> SVP_id (Name (prepend_id "out_" reg, -1))) (IdSet.elements footprint.all_writes) + @ (if footprint.throws then [SVP_id (Have_exception (-1)); SVP_id (Current_exception (-1))] else []) @ (if footprint.need_stdout then [SVP_id (Name (mk_id "out_stdout", -1))] else []) @ if footprint.need_stderr then [SVP_id (Name (mk_id "out_stderr", -1))] else [] ); } in let always_comb = + let let_initializers = + IntSet.fold + (fun n stmts -> mk_statement (svs_raw (sprintf "sail_setup_let_%d()" n)) :: stmts) + spec_info.global_let_numbers [] + |> List.rev + in let unchanged_registers = Bindings.fold (fun reg _ unchanged -> @@ -1586,7 +1734,9 @@ module Make (Config : CONFIG) = struct else [] in SVD_always_comb - (mk_statement (SVS_block (unchanged_registers @ channel_writes @ [mk_statement (svs_raw "$finish")]))) + (mk_statement + (SVS_block (let_initializers @ unchanged_registers @ channel_writes @ [mk_statement (svs_raw "$finish")])) + ) in Some { @@ -1594,7 +1744,7 @@ module Make (Config : CONFIG) = struct input_ports = []; output_ports = []; defs = - register_inputs @ register_outputs @ channel_outputs + register_inputs @ register_outputs @ throws_outputs @ channel_outputs @ [SVD_var (Jib_util.return, CT_unit)] @ [instantiate_main; always_comb]; } @@ -1706,8 +1856,8 @@ module Make (Config : CONFIG) = struct let sv_setup_function ctx name setup = let setup = Jib_optimize.( - setup |> flatten_instrs |> remove_dead_code |> variable_decls_to_top |> structure_control_flow_block - |> remove_undefined |> filter_clear + setup |> remove_undefined |> flatten_instrs |> remove_dead_code |> variable_decls_to_top + |> structure_control_flow_block |> filter_clear ) in separate space [string "function"; string "automatic"; string "void"; string name] @@ -1715,6 +1865,22 @@ module Make (Config : CONFIG) = struct ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) setup) ^^ hardline ^^ string "endfunction" ^^ twice hardline + let svir_setup_function l ctx name setup = + let setup = + Jib_optimize.( + setup |> remove_undefined |> flatten_instrs |> remove_dead_code |> variable_decls_to_top + |> structure_control_flow_block |> filter_clear + ) + in + let statements, _ = Smt_gen.run (fmap Util.option_these (mapM (svir_instr ctx) setup)) (gen_loc l) in + SVD_fundef + { + function_name = SVN_string name; + return_type = None; + params = []; + body = SVS_aux (SVS_block statements, gen_loc l); + } + let collect_registers cdefs = List.fold_left (fun rmap cdef -> @@ -1839,10 +2005,14 @@ module Make (Config : CONFIG) = struct let debug_attr = get_def_attribute "jib_debug" def_annot in if List.mem (string_of_id f) Config.ignore then ([], fn_ctyps) else ( + if Option.is_some debug_attr then ( + prerr_endline Util.("Pre-SV IR for " ^ string_of_id f ^ ":" |> yellow |> bold |> clear); + List.iter (fun instr -> prerr_endline (string_of_instr instr)) body + ); let body = Jib_optimize.( - body |> flatten_instrs |> remove_dead_code |> variable_decls_to_top (* |> structure_control_flow_block *) - |> remove_undefined |> filter_clear + body |> remove_undefined |> remove_functions_to_references |> flatten_instrs |> remove_dead_code + |> variable_decls_to_top |> filter_clear ) in if Option.is_some debug_attr then ( @@ -1855,6 +2025,9 @@ module Make (Config : CONFIG) = struct | None -> Reporting.unreachable (id_loc f) __POS__ ("No function type found for " ^ string_of_id f) ) | CDEF_type type_def -> ([SVD_type type_def], fn_ctyps) + | CDEF_let (n, bindings, setup) -> + let setup_function = svir_setup_function def_annot.loc ctx (sprintf "sail_setup_let_%d" n) setup in + (List.map (fun (id, ctyp) -> SVD_var (name id, ctyp)) bindings @ [setup_function], fn_ctyps) | _ -> ([], fn_ctyps) let sv_cdef spec_info ctx fn_ctyps setup_calls (CDEF_aux (aux, _)) = diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 1360db0cb..2093d2b2b 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -217,6 +217,7 @@ module Verilog_config (C : JIB_CONFIG) : Jib_compile.CONFIG = struct | Typ_id id when string_of_id id = "nat" -> CT_lint | Typ_id id when string_of_id id = "unit" -> CT_unit | Typ_id id when string_of_id id = "string" -> CT_string + | Typ_id id when string_of_id id = "string_literal" -> CT_string | Typ_id id when string_of_id id = "real" -> CT_real | Typ_id id when string_of_id id = "float16" -> CT_float 16 | Typ_id id when string_of_id id = "float32" -> CT_float 32 @@ -317,7 +318,7 @@ module Verilog_config (C : JIB_CONFIG) : Jib_compile.CONFIG = struct let ignore_64 = true let struct_value = false let tuple_value = false - let track_throw = true + let track_throw = false let branch_coverage = None let use_real = false let use_void = false diff --git a/src/sail_sv_backend/sv_ir.ml b/src/sail_sv_backend/sv_ir.ml index 00da0bede..327f626e8 100644 --- a/src/sail_sv_backend/sv_ir.ml +++ b/src/sail_sv_backend/sv_ir.ml @@ -148,6 +148,7 @@ and sv_statement_aux = | SVS_if of smt_exp * sv_statement option * sv_statement option | SVS_block of sv_statement list | SVS_assert of smt_exp * smt_exp + | SVS_foreach of sv_name * smt_exp * sv_statement | SVS_raw of string * Jib.name list * Jib.name list let filter_skips = List.filter (function SVS_aux (SVS_skip, _) -> false | _ -> true) @@ -280,6 +281,10 @@ let rec visit_sv_statement (vis : svir_visitor) outer_statement = let cond' = visit_smt_exp vis cond in let msg' = visit_smt_exp vis msg in if cond == cond' && msg == msg' then no_change else SVS_aux (SVS_assert (cond', msg'), l) + | SVS_foreach (i, exp, stmt) -> + let exp' = visit_smt_exp vis exp in + let stmt' = visit_sv_statement vis stmt in + if exp == exp' && stmt == stmt' then no_change else SVS_aux (SVS_foreach (i, exp', stmt'), l) | SVS_if (exp, then_stmt_opt, else_stmt_opt) -> let exp' = visit_smt_exp vis exp in let then_stmt_opt' = map_no_copy_opt (visit_sv_statement vis) then_stmt_opt in diff --git a/src/sail_sv_backend/sv_ir.mli b/src/sail_sv_backend/sv_ir.mli index 3c8fc1104..3b4574124 100644 --- a/src/sail_sv_backend/sv_ir.mli +++ b/src/sail_sv_backend/sv_ir.mli @@ -144,6 +144,7 @@ and sv_statement_aux = | SVS_if of smt_exp * sv_statement option * sv_statement option | SVS_block of sv_statement list | SVS_assert of smt_exp * smt_exp + | SVS_foreach of sv_name * smt_exp * sv_statement | SVS_raw of string * Jib.name list * Jib.name list val svs_raw : ?inputs:Jib.name list -> ?outputs:Jib.name list -> string -> sv_statement_aux diff --git a/test/c/exn_hello_world.expect b/test/c/exn_hello_world.expect new file mode 100644 index 000000000..8ab686eaf --- /dev/null +++ b/test/c/exn_hello_world.expect @@ -0,0 +1 @@ +Hello, World! diff --git a/test/c/exn_hello_world.sail b/test/c/exn_hello_world.sail new file mode 100644 index 000000000..d14d50542 --- /dev/null +++ b/test/c/exn_hello_world.sail @@ -0,0 +1,20 @@ +default Order dec + +$include + +union exception = { + E_string : string +} + +val f : unit -> unit + +$[jib_debug] +function f() = throw E_string("Hello, World!") + +val main : unit -> unit + +function main() = { + try f() catch { + E_string(msg) => print_endline(msg) + } +} diff --git a/test/c/vector_example.sail b/test/c/vector_example.sail index 6b3f538aa..0e62a653d 100644 --- a/test/c/vector_example.sail +++ b/test/c/vector_example.sail @@ -152,7 +152,7 @@ function main() = { decode(0b0110 @ 0xFFFFF @ 0b00 @ 0b10 @ 0b00 @ 0b01); // add V0 to V1 in 16 groups of 16, storing the result in V3 decode(0b0100 @ 0xFFFFF @ 0b00 @ 0b11 @ 0b00 @ 0b01); - + print_bits("V2 = ", V2); print_bits("V3 = ", V3); diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py index 31e3f40fb..d36926662 100755 --- a/test/sv/run_tests.py +++ b/test/sv/run_tests.py @@ -21,7 +21,6 @@ 'cheri128_hsb', 'cheri_capreg', # behavior? 'empty_list', # recursion - 'eq_struct', 'flow_restrict', # contains very large integer literal 'for_shadow', 'foreach_none', @@ -43,13 +42,10 @@ 'split', # generic vectors 'string_of_bits', 'string_take', - 'tuple_conversion', # verilator fails? 'vector_example', - 'vector_subrange_pattern', 'warl', 'warl_undef', 'xlen_val', # Calls external C function - 'zero_length_bv', 'spc_mappings', }