diff --git a/.gitignore b/.gitignore index f16c2b6e6..a9dcc1416 100644 --- a/.gitignore +++ b/.gitignore @@ -88,6 +88,11 @@ lib/hol/sail-heap /test/mono/test.cmi /test/mono/test.cmo /test/mono/test-output +/test/sv/*.sv +/test/sv/*.out +/test/sv/*.result +/test/sv/*.cpp +/test/sv/obj_dir/ /language/*.pdf /language/*.uo diff --git a/dune-project b/dune-project index 0c1d630a2..a14ff443b 100644 --- a/dune-project +++ b/dune-project @@ -76,7 +76,13 @@ http://www.cl.cam.ac.uk/~pes20/sail/. (name sail_smt_backend) (synopsis "Sail to C translation") (depends - (libsail (= :version)))) + (libsail (= :version)))) + +(package + (name sail_sv_backend) + (synopsis "Sail to Systemverilog translation") + (depends + (libsail (= :version)))) (package (name sail_lem_backend) @@ -130,6 +136,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/. (sail_ocaml_backend (and (= :version) :post)) (sail_c_backend (and (= :version) :post)) (sail_smt_backend (and (= :version) :post)) + (sail_sv_backend (and (= :version) :post)) (sail_lem_backend (and (= :version) :post)) (sail_coq_backend (and (= :version) :post)) (sail_latex_backend (and (= :version) :post)) diff --git a/language/jib.ott b/language/jib.ott index 89f110bd2..7ff5905ef 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -74,6 +74,7 @@ op :: '' ::= | and :: :: band | hd :: :: list_hd | tl :: :: list_tl + | is_empty :: :: list_is_empty | eq :: :: eq | neq :: :: neq % Integer ops @@ -240,8 +241,7 @@ cdef :: 'CDEF_' ::= } :: :: register | ctype_def :: :: type -% The first list of instructions sets up the global letbinding, while -% the second clears it. +% The list of instructions sets up the global letbinding | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm } :: :: let diff --git a/lib/arith.sail b/lib/arith.sail index f46663974..582b64e12 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -116,6 +116,11 @@ val print_int = pure "print_int" : (string, int) -> unit val prerr_int = pure "prerr_int" : (string, int) -> unit +/*! +We have special support for raising values to the power of two. Any Sail expression `2 ^ x` will be compiled to this builtin. +*/ +val pow2 = pure "pow2" : forall 'n. int('n) -> int(2 ^ 'n) + // ***** Integer shifts ***** /*! @@ -206,4 +211,10 @@ val abs_int_plain = pure { overload abs_int = {abs_int_plain} +val max_int = pure "max_int" : forall 'x 'y. + (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)} + +val min_int = pure "min_int" : forall 'x 'y. + (int('x), int('y)) -> {'z, ('x < 'y & 'z == 'x) | ('x >= 'y & 'z == 'y). int('z)} + $endif diff --git a/lib/concurrency_interface/common.sail b/lib/concurrency_interface/common.sail index 32a488403..15f67a8b3 100644 --- a/lib/concurrency_interface/common.sail +++ b/lib/concurrency_interface/common.sail @@ -67,8 +67,8 @@ $sail_internal -$target_set emulator_or_isla isla c ocaml interpreter -$target_set emulator c ocaml interpreter +$target_set emulator_or_isla isla c ocaml interpreter systemverilog +$target_set emulator c ocaml interpreter systemverilog $target_set prover lem coq $ifndef _CONCURRENCY_INTERFACE_COMMON diff --git a/lib/concurrency_interface/emulator_memory.sail b/lib/concurrency_interface/emulator_memory.sail index 74bca64b3..a5aaf96b8 100644 --- a/lib/concurrency_interface/emulator_memory.sail +++ b/lib/concurrency_interface/emulator_memory.sail @@ -83,6 +83,10 @@ $iftarget ocaml $define _EMULATOR_MEMORY_PRIMOPS $endif +$iftarget systemverilog +$define _EMULATOR_MEMORY_PRIMOPS +$endif + $ifdef INTERACTIVE $define _EMULATOR_MEMORY_PRIMOPS $endif diff --git a/lib/string.sail b/lib/string.sail index 43ec50d69..5bd245e52 100644 --- a/lib/string.sail +++ b/lib/string.sail @@ -96,4 +96,8 @@ val print_endline = pure "print_endline" : string -> unit val prerr_endline = pure "prerr_endline" : string -> unit +val print = pure "print" : string -> unit + +val prerr = pure "prerr" : string -> unit + $endif diff --git a/lib/sv/sail.sv b/lib/sv/sail.sv new file mode 100644 index 000000000..aee8103ff --- /dev/null +++ b/lib/sv/sail.sv @@ -0,0 +1,81 @@ +`ifndef SAIL_LIBRARY +`define SAIL_LIBRARY + +// 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; + +`ifdef SAIL_NOSTRINGS + +function automatic sail_unit sail_print_endline(sail_unit s); + return SAIL_UNIT; +endfunction // sail_print_endline + +function automatic sail_unit sail_prerr_endline(sail_unit s); + return SAIL_UNIT; +endfunction // sail_prerr_endline + +function automatic sail_unit sail_print(sail_unit s); + return SAIL_UNIT; +endfunction // sail_print + +function automatic sail_unit sail_prerr(sail_unit s); + return SAIL_UNIT; +endfunction // sail_prerr + +function automatic sail_unit sail_assert(bit b, sail_unit msg); + return SAIL_UNIT; +endfunction // sail_assert + +function automatic bit sail_eq_string(sail_unit s1, sail_unit s2); + return 0; +endfunction + +function automatic sail_unit sail_concat_str(sail_unit s1, sail_unit s2); + return SAIL_UNIT; +endfunction + +`else + +function automatic sail_unit sail_print_endline(string s); + $display(s); + return SAIL_UNIT; +endfunction // sail_print_endline + +function automatic sail_unit sail_prerr_endline(string s); + $display(s); + return SAIL_UNIT; +endfunction // sail_prerr_endline + +function automatic sail_unit sail_print(string s); + $write(s); + return SAIL_UNIT; +endfunction // sail_print + +function automatic sail_unit sail_prerr(string s); + $write(s); + return SAIL_UNIT; +endfunction // sail_prerr + +function automatic sail_unit sail_assert(bit b, string msg); + if (!b) begin + $display("%s", msg); + end; + return SAIL_UNIT; +endfunction // sail_assert + +function automatic bit sail_eq_string(string s1, string s2); + return s1 == s2; +endfunction + +function automatic string sail_concat_str(string s1, string s2); + return {s1, s2}; +endfunction + +`endif + +typedef enum logic [0:0] {SAIL_REAL} sail_real; + +`endif // `ifndef SAIL_LIBRARY diff --git a/lib/sv/sail_memory.sv b/lib/sv/sail_memory.sv new file mode 100644 index 000000000..743d06990 --- /dev/null +++ b/lib/sv/sail_memory.sv @@ -0,0 +1,67 @@ +`ifndef SAIL_MEMORY +`define SAIL_MEMORY + +logic [7:0] sail_memory [logic [63:0]]; + +bit sail_tag_memory [logic [63:0]]; + +function automatic sail_bits sail_emulator_read_mem(logic [63:0] addrsize, sail_bits addr, sail_int n); + logic [63:0] paddr; + logic [SAIL_BITS_WIDTH-1:0] buffer; + sail_int i; + + paddr = addr.bits[63:0]; + + for (i = n; i > 0; i = i - 1) begin + buffer = buffer << 8; + buffer[7:0] = sail_memory[paddr + (i[63:0] - 1)]; + end + + return '{n[SAIL_INDEX_WIDTH-1:0] * 8, buffer}; +endfunction + +function automatic sail_bits sail_emulator_read_mem_ifetch(logic [63:0] addrsize, sail_bits addr, sail_int n); + return sail_emulator_read_mem(addrsize, addr, n); +endfunction + +function automatic sail_bits sail_emulator_read_mem_exclusive(logic [63:0] addrsize, sail_bits addr, sail_int n); + return sail_emulator_read_mem(addrsize, addr, n); +endfunction + +function automatic bit sail_emulator_write_mem(logic [63:0] addrsize, sail_bits addr, sail_int n, sail_bits value); + logic [63:0] paddr; + logic [SAIL_BITS_WIDTH-1:0] buffer; + sail_int i; + + paddr = addr.bits[63:0]; + buffer = value.bits; + + for (i = 0; i < n; i = i + 1) begin + sail_memory[paddr + i[63:0]] = buffer[7:0]; + buffer = buffer >> 8; + end + + return 1'b1; +endfunction + +function automatic bit sail_emulator_write_mem_exclusive(logic [63:0] addrsize, sail_bits addr, sail_int n, sail_bits value); + return sail_emulator_write_mem(addrsize, addr, n, value); +endfunction + +function automatic bit sail_emulator_read_tag(logic [63:0] addrsize, sail_bits addr); + logic [63:0] paddr; + paddr = addr.bits[63:0]; + if (sail_tag_memory.exists(paddr) == 1) + return sail_tag_memory[paddr]; + else + return 1'b0; +endfunction + +function automatic sail_unit sail_emulator_write_tag(logic [63:0] addrsize, sail_bits addr, bit tag); + logic [63:0] paddr; + paddr = addr.bits[63:0]; + sail_tag_memory[paddr] = tag; + return SAIL_UNIT; +endfunction + +`endif diff --git a/sail.opam b/sail.opam index 5a10085b8..674772235 100644 --- a/sail.opam +++ b/sail.opam @@ -36,6 +36,7 @@ depends: [ "sail_ocaml_backend" {= version & post} "sail_c_backend" {= version & post} "sail_smt_backend" {= version & post} + "sail_sv_backend" {= version & post} "sail_lem_backend" {= version & post} "sail_coq_backend" {= version & post} "sail_latex_backend" {= version & post} diff --git a/sail_sv_backend.opam b/sail_sv_backend.opam new file mode 100644 index 000000000..1e965967d --- /dev/null +++ b/sail_sv_backend.opam @@ -0,0 +1,42 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.16" +synopsis: "Sail to Systemverilog translation" +maintainer: ["Sail Devs "] +authors: [ + "Alasdair Armstrong" + "Thomas Bauereiss" + "Brian Campbell" + "Shaked Flur" + "Jonathan French" + "Kathy Gray" + "Robert Norton" + "Christopher Pulte" + "Peter Sewell" + "Mark Wassell" +] +license: "BSD-2-Clause" +homepage: "https://github.com/rems-project/sail" +bug-reports: "https://github.com/rems-project/sail/issues" +depends: [ + "dune" {>= "3.0"} + "libsail" {= version} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/rems-project/sail.git" diff --git a/src/bin/callgraph_commands.ml b/src/bin/callgraph_commands.ml index 8690e1f63..e87fbfcf0 100644 --- a/src/bin/callgraph_commands.ml +++ b/src/bin/callgraph_commands.ml @@ -95,7 +95,7 @@ let dot_of_ast out_chan ast = let module G = Graph.Make (Node) in let module NodeSet = Set.Make (Node) in let g = graph_of_ast ast in - G.make_dot (node_color NodeSet.empty) edge_color node_string out_chan g + G.make_dot ~node_color:(node_color NodeSet.empty) ~edge_color ~string_of_node:node_string out_chan g let node_of_id env = let lets = Type_check.Env.get_toplevel_lets env in diff --git a/src/lib/graph.ml b/src/lib/graph.ml index 62f8fd3b3..8e7ee234e 100644 --- a/src/lib/graph.ml +++ b/src/lib/graph.ml @@ -114,7 +114,13 @@ module type S = sig components. *) val scc : ?original_order:node list -> graph -> node list list - val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit + val make_dot : + node_color:(node -> string) -> + edge_color:(node -> node -> string) -> + string_of_node:(node -> string) -> + out_channel -> + graph -> + unit end module Make (Ord : OrderedType) = struct @@ -285,7 +291,7 @@ module Make (Ord : OrderedType) = struct List.iter (fun v -> if not (Hashtbl.mem node_indices v) then visit_node v) nodes; List.rev !components - let make_dot node_color edge_color string_of_node out_chan graph = + let make_dot ~node_color ~edge_color ~string_of_node out_chan graph = Util.opt_colors := false; let to_string node = String.escaped (string_of_node node) in output_string out_chan "digraph DEPS {\n"; diff --git a/src/lib/graph.mli b/src/lib/graph.mli index 1f3913dec..2959ec0d2 100644 --- a/src/lib/graph.mli +++ b/src/lib/graph.mli @@ -116,7 +116,13 @@ module type S = sig components. *) val scc : ?original_order:node list -> graph -> node list list - val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit + val make_dot : + node_color:(node -> string) -> + edge_color:(node -> node -> string) -> + string_of_node:(node -> string) -> + out_channel -> + graph -> + unit end module Make (Ord : OrderedType) : diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 6323c272c..724bc476f 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -233,11 +233,11 @@ let rec mangle_string_of_ctyp ctx = function | CT_list ctyp -> "L" ^ mangle_string_of_ctyp ctx ctyp | CT_poly kid -> "P" ^ string_of_kid kid -module type Config = sig +module type CONFIG = sig val convert_typ : ctx -> typ -> ctyp val optimize_anf : ctx -> typ aexp -> typ aexp val unroll_loops : int option - val specialize_calls : bool + val make_call_precise : ctx -> id -> bool val ignore_64 : bool val struct_value : bool val tuple_value : bool @@ -270,7 +270,7 @@ let callgraph cdefs = ) IdGraph.empty cdefs -module Make (C : Config) = struct +module Make (C : CONFIG) = struct let ctyp_of_typ ctx typ = C.convert_typ ctx typ let rec chunkify n xs = match (Util.take n xs, Util.drop n xs) with xs, [] -> [xs] | xs, ys -> xs :: chunkify n ys @@ -498,7 +498,7 @@ module Make (C : Config) = struct let len = List.length avals in let direction = match ord with Ord_aux (Ord_inc, _) -> false | Ord_aux (Ord_dec, _) -> true in let elem_ctyp = ctyp_of_typ ctx typ in - let vector_ctyp = CT_vector elem_ctyp in + let vector_ctyp = CT_fvector (len, elem_ctyp) in let gs = ngensym () in let aval_set i aval = let setup, cval, cleanup = compile_aval l ctx aval in @@ -552,56 +552,6 @@ module Make (C : Config) = struct [iclear (CT_list ctyp) gs] ) - (* -let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = - let call () = - let setup = ref [] in - let cleanup = ref [] in - let cast_args = - List.map2 - (fun ctyp cval -> - let have_ctyp = cval_ctyp cval in - if is_polymorphic ctyp then - V_poly (cval, have_ctyp) - else if C.specialize_calls || ctyp_equal ctyp have_ctyp then - cval - else - let gs = ngensym () in - setup := iinit l ctyp gs cval :: !setup; - cleanup := iclear ctyp gs :: !cleanup; - V_id (gs, ctyp)) - arg_ctyps args - in - if C.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then - !setup @ [ifuncall l clexp id cast_args] @ !cleanup - else - let gs = ngensym () in - List.rev !setup - @ [idecl l ret_ctyp gs; - ifuncall l (CL_id (gs, ret_ctyp)) id cast_args; - icopy l clexp (V_id (gs, ret_ctyp)); - iclear ret_ctyp gs] - @ !cleanup - in - if not C.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then - let extern = Env.get_extern (fst id) ctx.tc_env "c" in - begin match extern, List.map cval_ctyp args, clexp_ctyp clexp with - | "slice", [CT_fbits _; CT_lint; _], CT_fbits (n, _) -> - let start = ngensym () in - [iinit l (CT_fint 64) start (List.nth args 1); - icopy l clexp (V_call (Slice n, [List.nth args 0; V_id (start, CT_fint 64)]))] - | "sail_unsigned", [CT_fbits _], CT_fint 64 -> - [icopy l clexp (V_call (Unsigned 64, [List.nth args 0]))] - | "sail_signed", [CT_fbits _], CT_fint 64 -> - [icopy l clexp (V_call (Signed 64, [List.nth args 0]))] - | "set_slice", [_; _; CT_fbits (n, _); CT_fint 64; CT_fbits (m, _)], CT_fbits (n', _) when n = n' -> - [icopy l clexp (V_call (Set_slice, [List.nth args 2; List.nth args 3; List.nth args 4]))] - | _, _, _ -> - call () - end - else call () - *) - let compile_funcall l ctx id args = let setup = ref [] in let cleanup = ref [] in @@ -740,14 +690,14 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = | CT_list ctyp -> let hd_pre, hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in let tl_pre, tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in - ( [ijump l (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_pre @ tl_pre, + ( [ijump l (V_call (List_is_empty, [cval])) case_label] @ hd_pre @ tl_pre, hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx ) | _ -> raise (Reporting.err_general l "Tried to pattern match cons on non list type") end - | AP_nil _ -> ([ijump l (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], [], ctx) + | AP_nil _ -> ([ijump l (V_call (Bnot, [V_call (List_is_empty, [cval])])) case_label], [], [], ctx) let unit_cval = V_lit (VL_unit, CT_unit) @@ -2007,7 +1957,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = Reporting.unreachable (id_loc id) __POS__ "Invalid cons call" end | None -> instr :: tail - | Some (param_ctyps, ret_ctyp) -> + | Some (param_ctyps, ret_ctyp) when C.make_call_precise ctx id -> if List.compare_lengths args param_ctyps <> 0 then Reporting.unreachable (id_loc id) __POS__ ("Function call found with incorrect arity: " ^ string_of_id id); @@ -2044,6 +1994,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = @ tail @ ret_cleanup @ cleanup ); ] + | Some _ -> instr :: tail end | instr -> instr :: tail in @@ -2061,9 +2012,9 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = in precise_calls [] cdefs - (** Once we specialize variants, there may be additional type - dependencies which could be in the wrong order. As such we need to - sort the type definitions in the list of cdefs. *) + (* Once we specialize variants, there may be additional type + dependencies which could be in the wrong order. As such we need + to sort the type definitions in the list of cdefs. *) let sort_ctype_defs reverse cdefs = (* Split the cdefs into type definitions and non type definitions *) let is_ctype_def = function CDEF_type _ -> true | _ -> false in @@ -2158,7 +2109,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = let cdefs, ctx = specialize_functions ctx cdefs in let cdefs = sort_ctype_defs true cdefs in let cdefs, ctx = specialize_variants ctx [] cdefs in - let cdefs = if C.specialize_calls then cdefs else make_calls_precise ctx cdefs in + let cdefs = make_calls_precise ctx cdefs in let cdefs = sort_ctype_defs false cdefs in (cdefs, ctx) end diff --git a/src/lib/jib_compile.mli b/src/lib/jib_compile.mli index e164fbe6a..258b4ce21 100644 --- a/src/lib/jib_compile.mli +++ b/src/lib/jib_compile.mli @@ -122,7 +122,7 @@ val initial_ctx : Env.t -> Effects.side_effect_info -> ctx Sail into Jib. We have to provide a conversion function from Sail types into Jib types, as well as a function that optimizes ANF expressions (which can just be the identity function) *) -module type Config = sig +module type CONFIG = sig val convert_typ : ctx -> typ -> ctyp val optimize_anf : ctx -> typ aexp -> typ aexp @@ -131,9 +131,10 @@ module type Config = sig generation. *) val unroll_loops : int option - (** If false, function arguments must match the function - type exactly. If true, they can be more specific. *) - val specialize_calls : bool + (** A call is precise if the function arguments match the function + type exactly. Leaving functions imprecise can allow later passes + to specialize implementations. *) + val make_call_precise : ctx -> id -> bool (** If false, will ensure that fixed size bitvectors are specifically less that 64-bits. If true this restriction will @@ -164,7 +165,7 @@ end val callgraph : cdef list -> IdGraph.graph -module Make (C : Config) : sig +module Make (C : CONFIG) : sig (** Compile a Sail definition into a Jib definition. The first two arguments are is the current definition number and the total number of definitions, and can be used to drive a progress bar diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index 3e6214a49..3781b6737 100644 --- a/src/lib/jib_optimize.ml +++ b/src/lib/jib_optimize.ml @@ -180,6 +180,37 @@ 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 + let rec create_value l = function + | CT_unit -> ([], V_lit (VL_unit, CT_unit)) + | CT_bool -> ([], V_lit (VL_bool false, CT_bool)) + | CT_bit -> ([], V_lit (VL_bit Sail2_values.B0, CT_bit)) + | CT_string -> ([], V_lit (VL_string "", CT_string)) + | CT_tup ctyps -> + let setup, values = + List.fold_right + (fun ctyp (setups, values) -> + let setup, value = create_value l ctyp in + (setup @ setups, value :: values) + ) + ctyps ([], []) + in + (setup, V_tuple (values, CT_tup ctyps)) + | 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 + let rec instrs_subst id subst = function | I_aux (I_decl (_, id'), _) :: _ as instrs when Name.compare id id' = 0 -> instrs | I_aux (I_init (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 -> @@ -564,9 +595,9 @@ let structure_control_flow_block instrs = in let iguard l guarded = function - | [] -> icomment "nop" + | [] -> [] | instrs -> ( - match guard_condition guarded with None -> iblock instrs | Some cond -> iif l cond instrs [] CT_unit + match guard_condition guarded with None -> instrs | Some cond -> [iif l cond instrs [] CT_unit] ) in @@ -574,18 +605,18 @@ let structure_control_flow_block instrs = | [] -> [] | (I_aux ((I_decl _ | I_init _), (_, l)) as instr) :: instrs -> let after_decl, rest = split_after_jump instrs in - instr :: iguard l guarded after_decl :: fix_block guarded rest + instr :: (iguard l guarded after_decl @ fix_block guarded rest) | I_aux (I_goto label, (_, l)) :: instrs -> let v = label_var label in let set_goto = iguard l guarded [icopy l (CL_id (v, CT_bool)) (V_lit (VL_bool true, CT_bool))] in let guarded = NameSet.add v guarded in let after_jump, rest = split_after_jump instrs in - set_goto :: iguard l guarded after_jump :: fix_block guarded rest + set_goto @ iguard l guarded after_jump @ fix_block guarded rest | I_aux (I_label label, (_, l)) :: instrs -> let v = label_var label in let guarded = NameSet.remove v guarded in let after_label, rest = split_after_jump instrs in - icomment label :: iguard l guarded after_label :: fix_block guarded rest + icomment label :: (iguard l guarded after_label @ fix_block guarded rest) | I_aux (I_jump (cond, label), (_, l)) :: instrs -> let v = label_var label in let set_goto = @@ -599,7 +630,7 @@ let structure_control_flow_block instrs = in let guarded = NameSet.add v guarded in let after_jump, rest = split_after_jump instrs in - set_goto :: iguard l guarded after_jump :: fix_block guarded rest + set_goto @ iguard l guarded after_jump @ fix_block guarded rest | instr :: instrs -> instr :: fix_block guarded instrs in diff --git a/src/lib/jib_optimize.mli b/src/lib/jib_optimize.mli index 7ace35e5e..d856813cb 100644 --- a/src/lib/jib_optimize.mli +++ b/src/lib/jib_optimize.mli @@ -84,6 +84,8 @@ val unique_per_function_ids : cdef list -> cdef list val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list +val remove_undefined : 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_util.ml b/src/lib/jib_util.ml index d5e8e57a9..89a022953 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -268,6 +268,7 @@ let string_of_op = function | Bor -> "@or" | List_hd -> "@hd" | List_tl -> "@tl" + | List_is_empty -> "@is_empty" | Eq -> "@eq" | Neq -> "@neq" | Bvnot -> "@bvnot" @@ -366,7 +367,6 @@ let string_of_value = function | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" | VL_real str -> str | VL_string str -> "\"" ^ str ^ "\"" - | VL_empty_list -> "NULL" | VL_enum element -> Util.zencode_string element | VL_ref r -> "&" ^ Util.zencode_string r | VL_undefined -> "undefined" @@ -393,6 +393,59 @@ let rec string_of_cval = function end | V_tuple (members, _) -> "(" ^ Util.string_of_list ", " string_of_cval members ^ ")" +let rec string_of_clexp = function + | CL_id (id, ctyp) -> string_of_name id + | CL_field (clexp, field) -> string_of_clexp clexp ^ "." ^ string_of_id field + | CL_addr clexp -> string_of_clexp clexp ^ "*" + | CL_tuple (clexp, n) -> string_of_clexp clexp ^ "." ^ string_of_int n + | CL_void -> "void" + | CL_rmw (id1, id2, ctyp) -> Printf.sprintf "rmw(%s, %s)" (string_of_name id1) (string_of_name id2) + +let rec doc_instr (I_aux (aux, _)) = + let open Printf in + let instr s = twice space ^^ string s in + match aux with + | I_decl (ctyp, id) -> ksprintf instr "%s : %s" (string_of_name id) (string_of_ctyp ctyp) + | I_reset (ctyp, id) -> ksprintf instr "reset %s : %s" (string_of_name id) (string_of_ctyp ctyp) + | I_init (ctyp, id, cval) -> + ksprintf instr "%s : %s = %s" (string_of_name id) (string_of_ctyp ctyp) (string_of_cval cval) + | I_reinit (ctyp, id, cval) -> + ksprintf instr "reinit %s : %s = %s" (string_of_name id) (string_of_ctyp ctyp) (string_of_cval cval) + | I_clear (ctyp, id) -> ksprintf instr "clear %s : %s" (string_of_name id) (string_of_ctyp ctyp) + | I_label label -> ksprintf string "%s:" label + | I_jump (cval, label) -> ksprintf instr "jump %s goto %s" (string_of_cval cval) label + | I_goto label -> ksprintf instr "goto %s" label + | I_exit cause -> ksprintf instr "exit %s" cause + | I_undefined ctyp -> ksprintf instr "arbitrary %s" (string_of_ctyp ctyp) + | I_end id -> ksprintf instr "end %s" (string_of_name id) + | I_raw str -> string str + | I_comment str -> twice space ^^ string "//" ^^ string str + | I_throw cval -> ksprintf instr "throw %s" (string_of_cval cval) + | I_return cval -> ksprintf instr "return %s" (string_of_cval cval) + | I_funcall (clexp, false, uid, args) -> + ksprintf instr "%s = %s(%s)" (string_of_clexp clexp) (string_of_uid uid) + (Util.string_of_list ", " string_of_cval args) + | I_funcall (clexp, true, uid, args) -> + ksprintf instr "%s = $%s(%s)" (string_of_clexp clexp) (string_of_uid uid) + (Util.string_of_list ", " string_of_cval args) + | I_copy (clexp, cval) -> ksprintf instr "%s = %s" (string_of_clexp clexp) (string_of_cval cval) + | I_block instrs -> + twice space ^^ char '{' + ^^ nest 2 (hardline ^^ separate_map hardline doc_instr instrs) + ^^ hardline ^^ twice space ^^ char '}' + | I_try_block instrs -> + twice space ^^ string "try {" + ^^ nest 2 (hardline ^^ separate_map hardline doc_instr instrs) + ^^ hardline ^^ twice space ^^ char '}' + | I_if (cond, then_instrs, else_instrs, _) -> + ksprintf instr "if %s {" (string_of_cval cond) + ^^ nest 2 (hardline ^^ separate_map hardline doc_instr then_instrs) + ^^ hardline ^^ twice space ^^ string "} else {" + ^^ nest 2 (hardline ^^ separate_map hardline doc_instr else_instrs) + ^^ hardline ^^ twice space ^^ char '}' + +let string_of_instr i = Pretty_print_sail.to_string (doc_instr i) + let rec map_ctyp f = function | ( CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_float _ | CT_rounding_mode | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly _ | CT_enum _ ) as ctyp -> @@ -532,7 +585,7 @@ let rec ctyp_suprema = function | CT_struct (id, ctors) -> CT_struct (id, ctors) | CT_variant (id, ctors) -> CT_variant (id, ctors) | CT_vector ctyp -> CT_vector (ctyp_suprema ctyp) - | CT_fvector (n, ctyp) -> CT_fvector (n, ctyp_suprema ctyp) + | CT_fvector (_, ctyp) -> CT_vector (ctyp_suprema ctyp) | CT_list ctyp -> CT_list (ctyp_suprema ctyp) | CT_ref ctyp -> CT_ref (ctyp_suprema ctyp) | CT_poly kid -> CT_poly kid @@ -917,6 +970,11 @@ let rec infer_call op vs = | CT_list ctyp -> CT_list ctyp | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid call to tl" end + | List_is_empty, [v] -> begin + match cval_ctyp v with + | CT_list ctyp -> CT_list ctyp + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid call to is_empty" + end | (Eq | Neq), _ -> CT_bool | Bvnot, [v] -> cval_ctyp v | Bvaccess, _ -> CT_bit diff --git a/src/lib/jib_util.mli b/src/lib/jib_util.mli index dd4703960..c174368c7 100644 --- a/src/lib/jib_util.mli +++ b/src/lib/jib_util.mli @@ -135,6 +135,8 @@ val string_of_ctyp : ctyp -> string val string_of_uid : id * ctyp list -> string val string_of_value : Value2.vl -> string val string_of_cval : cval -> string +val string_of_clexp : clexp -> string +val string_of_instr : instr -> string (** {1. Functions and modules for working with ctyps} *) diff --git a/src/lib/reporting.ml b/src/lib/reporting.ml index eb1b752c0..0537fc27a 100644 --- a/src/lib/reporting.ml +++ b/src/lib/reporting.ml @@ -314,3 +314,10 @@ let get_sail_dir default_sail_dir = ^ " does not exist. Make sure Sail is installed correctly, or try setting the SAIL_DIR environment variable" ) ) + +let system_checked ?loc:(l = Parse_ast.Unknown) cmd = + match Unix.system cmd with + | WEXITED 0 -> () + | WEXITED n -> raise (err_general l (Printf.sprintf "Command %s failed with exit code %d" cmd n)) + | WSTOPPED n -> raise (err_general l (Printf.sprintf "Command %s stopped by signal %d" cmd n)) + | WSIGNALED n -> raise (err_general l (Printf.sprintf "Command %s killed by signal %d" cmd n)) diff --git a/src/lib/reporting.mli b/src/lib/reporting.mli index 2b46a36e9..f020dec49 100644 --- a/src/lib/reporting.mli +++ b/src/lib/reporting.mli @@ -159,3 +159,6 @@ val simple_warn : string -> unit val suppress_warnings_for_file : string -> unit val get_sail_dir : string -> string + +(** Run a command using Unix.system, but raise a Reporting exception if the command fails or is stopped/killed by a signal *) +val system_checked : ?loc:Parse_ast.l -> string -> unit diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 4accc39c2..adac024d2 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -1802,13 +1802,13 @@ let pat_var (P_aux (paux, a)) = *) let rewrite_split_fun_ctor_pats fun_name effect_info env ast = let rewrite_fundef typquant (FD_aux (FD_function (r_o, t_o, clauses), ((l, _) as fdannot))) def_annot = - let rec_clauses, clauses = List.partition is_funcl_rec clauses in + (* let rec_clauses, clauses = List.partition is_funcl_rec clauses in *) let clauses, aux_funs = List.fold_left (fun (clauses, aux_funs) (FCL_aux (FCL_funcl (id, pexp), fannot) as clause) -> let pat, guard, exp, annot = destruct_pexp pexp in match pat with - | P_aux (P_app (ctor_id, args), pannot) -> + | P_aux (P_app (ctor_id, args), pannot) | P_aux (P_tuple [P_aux (P_app (ctor_id, args), pannot)], _) -> let ctor_typq, ctor_typ = Env.get_union_id ctor_id env in let args = match args with [P_aux (P_tuple args, _)] -> args | _ -> args in let argstup_typ = tuple_typ (List.map typ_of_pat args) in @@ -1846,7 +1846,7 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast = ) ([], Bindings.empty) clauses in - let add_aux_def id aux_funs defs = + let add_aux_def id aux_funs (valdefs, fundefs) = let funcls = List.map (fun (fcl, _, _) -> fcl) aux_funs in let env, quants, args_typ, ret_typ = match aux_funs with @@ -1882,12 +1882,13 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast = in let fundef = FD_aux (FD_function (r_o, t_o, funcls), fdannot) in let def_annot = mk_def_annot (gen_loc def_annot.loc) in - [DEF_aux (DEF_val val_spec, def_annot); DEF_aux (DEF_fundef fundef, def_annot)] @ defs + (DEF_aux (DEF_val val_spec, def_annot) :: valdefs, DEF_aux (DEF_fundef fundef, def_annot) :: fundefs) in - ( Bindings.fold add_aux_def aux_funs - [DEF_aux (DEF_fundef (FD_aux (FD_function (r_o, t_o, rec_clauses @ clauses), fdannot)), def_annot)], - List.map fst (Bindings.bindings aux_funs) - ) + let valdefs, fundefs = + Bindings.fold add_aux_def aux_funs + ([], [DEF_aux (DEF_fundef (FD_aux (FD_function (r_o, t_o, clauses), fdannot)), def_annot)]) + in + (valdefs @ fundefs, List.map fst (Bindings.bindings aux_funs)) in let typquant = List.fold_left @@ -1911,6 +1912,58 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast = ) ast.defs ([], effect_info) in + + (* If we have a call to execute(Clause(...)) we can directly + transform that to execute_Clause(...). This removes recursion + from when one execute clause is implemented in terms of another, + like RISC-V compressed instructions. *) + let optimize_split_call (f, args) = + match args with + | [E_aux (E_app (ctor_id, ctor_args), annot)] + when string_of_id f = fun_name && Env.is_union_constructor ctor_id (env_of_annot annot) -> begin + match ctor_args with + | [E_aux (E_tuple ctor_args, _)] -> E_app (prepend_id (fun_name ^ "_") ctor_id, ctor_args) + | [ctor_arg] -> E_app (prepend_id (fun_name ^ "_") ctor_id, [ctor_arg]) + | _ -> Reporting.unreachable (fst annot) __POS__ "Constructor with more than 1 argument found in split rewrite" + end + | _ -> E_app (f, args) + in + let optimize_exp = fold_exp { id_exp_alg with e_app = optimize_split_call } in + + let defs = + List.map + (fun def -> + match def with + | DEF_aux (DEF_fundef (FD_aux (FD_function (r_o, t_o, clauses), fdannot)), def_annot) -> + DEF_aux + ( DEF_fundef + (FD_aux + ( FD_function + ( r_o, + t_o, + List.map + (fun (FCL_aux (FCL_funcl (id, Pat_aux (pexp, pann)), fannot)) -> + match pexp with + | Pat_exp (pat, exp) -> + FCL_aux (FCL_funcl (id, Pat_aux (Pat_exp (pat, optimize_exp exp), pann)), fannot) + | Pat_when (pat, guard, exp) -> + FCL_aux + ( FCL_funcl + (id, Pat_aux (Pat_when (pat, optimize_exp guard, optimize_exp exp), pann)), + fannot + ) + ) + clauses + ), + fdannot + ) + ), + def_annot + ) + | _ -> def + ) + defs + in ({ ast with defs }, new_effect_info, env) let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) = Tu_aux (Tu_ty_id (rw_typ typ, id), annot) diff --git a/src/lib/smt_exp.ml b/src/lib/smt_exp.ml new file mode 100644 index 000000000..ed3cb2132 --- /dev/null +++ b/src/lib/smt_exp.ml @@ -0,0 +1,220 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Ast_util + +type smt_typ = + | Bitvec of int + | Bool + | String + | Real + | Datatype of string * (string * (string * smt_typ) list) list + | Array of smt_typ * smt_typ + +let mk_enum name elems = Datatype (name, List.map (fun elem -> (elem, [])) elems) + +let mk_record name fields = Datatype (name, [(name, fields)]) + +let mk_variant name ctors = Datatype (name, List.map (fun (ctor, ty) -> (ctor, [("un" ^ ctor, ty)])) ctors) + +type smt_array_info = Fixed of int + +type smt_exp = + | Bool_lit of bool + | Bitvec_lit of Sail2_values.bitU list + | Real_lit of string + | String_lit of string + | Var of Jib.name + | Enum of string + | Fn of string * smt_exp list + | Ite of smt_exp * smt_exp * smt_exp + | SignExtend of int * int * smt_exp + | ZeroExtend of int * int * smt_exp + | Extract of int * int * smt_exp + | Tester of string * smt_exp + | Unwrap of Ast.id * bool * smt_exp + | Field of Ast.id * Ast.id * smt_exp + | Store of smt_array_info * string * smt_exp * smt_exp * smt_exp + | Empty_list + | Hd of string * smt_exp + | Tl of string * smt_exp + +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)) + | SignExtend (len, n, exp) -> f (SignExtend (len, n, fold_smt_exp f exp)) + | ZeroExtend (len, n, exp) -> f (ZeroExtend (len, n, fold_smt_exp f exp)) + | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp)) + | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp)) + | Unwrap (ctor, b, exp) -> f (Unwrap (ctor, b, fold_smt_exp f exp)) + | Field (struct_id, field_id, exp) -> f (Field (struct_id, field_id, fold_smt_exp f exp)) + | Store (info, store_fn, arr, index, x) -> + f (Store (info, store_fn, fold_smt_exp f arr, fold_smt_exp f index, fold_smt_exp f x)) + | Hd (hd_op, xs) -> f (Hd (hd_op, fold_smt_exp f xs)) + | Tl (hd_op, xs) -> f (Tl (hd_op, fold_smt_exp f xs)) + | (Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Enum _ | Empty_list) as exp -> f exp + +let smt_conj = function [] -> Bool_lit true | [x] -> x | xs -> Fn ("and", xs) + +let smt_disj = function [] -> Bool_lit false | [x] -> x | xs -> Fn ("or", xs) + +let extract i j x = Extract (i, j, x) + +let bvnot x = Fn ("bvnot", [x]) +let bvand x y = Fn ("bvand", [x; y]) +let bvor x y = Fn ("bvor", [x; y]) +let bvneg x = Fn ("bvneg", [x]) +let bvadd x y = Fn ("bvadd", [x; y]) +let bvsub x y = Fn ("bvsub", [x; y]) +let bvmul x y = Fn ("bvmul", [x; y]) +let bvudiv x y = Fn ("bvudiv", [x; y]) +let bvurem x y = Fn ("bvurem", [x; y]) +let bvshl x y = Fn ("bvshl", [x; y]) +let bvlshr x y = Fn ("bvlshr", [x; y]) +let bvult x y = Fn ("bvult", [x; y]) + +let bvzero n = Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int n)) + +let bvones n = Bitvec_lit (Sail2_operators_bitlists.ones (Big_int.of_int n)) + +let bvone n = + if n > 0 then Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int (n - 1)) @ [Sail2_values.B1]) + else Bitvec_lit [] + +let rec simp exp = + let open Sail2_operators_bitlists in + match exp with + | Fn (f, args) -> + let args = List.map simp args in + begin + match (f, args) with + | "contents", [Fn ("Bits", [_; bv])] -> bv + | "len", [Fn ("Bits", [len; _])] -> len + | "concat", _ -> + let chunks, bv = + List.fold_left + (fun (chunks, current_literal) arg -> + match (current_literal, arg) with + | Some bv1, Bitvec_lit bv2 -> (chunks, Some (bv1 @ bv2)) + | None, Bitvec_lit bv -> (chunks, Some bv) + | Some bv, exp -> (exp :: Bitvec_lit bv :: chunks, None) + | None, exp -> (exp :: chunks, None) + ) + ([], None) args + in + begin + match (chunks, bv) with + | [], Some bv -> Bitvec_lit bv + | chunks, Some bv -> Fn ("concat", List.rev (Bitvec_lit bv :: chunks)) + | chunks, None -> Fn ("concat", List.rev chunks) + end + | "bvnot", [Bitvec_lit bv] -> Bitvec_lit (not_vec bv) + | "bvand", [Bitvec_lit lhs; Bitvec_lit rhs] -> Bitvec_lit (and_vec lhs rhs) + | "bvor", [Bitvec_lit lhs; Bitvec_lit rhs] -> Bitvec_lit (or_vec lhs rhs) + | "bvxor", [Bitvec_lit lhs; Bitvec_lit rhs] -> Bitvec_lit (xor_vec lhs rhs) + | "bvshl", [Bitvec_lit lhs; Bitvec_lit rhs] -> begin + match sint_maybe rhs with Some shift -> Bitvec_lit (shiftl lhs shift) | None -> Fn (f, args) + end + | "bvlshr", [Bitvec_lit lhs; Bitvec_lit rhs] -> begin + match sint_maybe rhs with Some shift -> Bitvec_lit (shiftr lhs shift) | None -> Fn (f, args) + end + | "bvashr", [Bitvec_lit lhs; Bitvec_lit rhs] -> begin + match sint_maybe rhs with Some shift -> Bitvec_lit (shiftr lhs shift) | None -> Fn (f, args) + end + | f, args -> Fn (f, args) + end + | ZeroExtend (to_len, from_len, arg) -> + let arg = simp arg in + begin + match arg with + | Bitvec_lit bv -> Bitvec_lit (zero_extend bv (Big_int.of_int to_len)) + | _ -> ZeroExtend (to_len, from_len, arg) + end + | SignExtend (to_len, from_len, arg) -> + let arg = simp arg in + begin + match arg with + | Bitvec_lit bv -> Bitvec_lit (sign_extend bv (Big_int.of_int to_len)) + | _ -> SignExtend (to_len, from_len, arg) + end + | Extract (n, m, arg) -> begin + match simp arg with + | Bitvec_lit bv -> Bitvec_lit (subrange_vec_dec bv (Big_int.of_int n) (Big_int.of_int m)) + | exp -> Extract (n, m, exp) + end + | Store (info, store_fn, arr, i, x) -> Store (info, store_fn, simp arr, simp i, simp x) + | exp -> exp + +type smt_def = + | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp + | Declare_fun of string * smt_typ list * smt_typ + | Declare_const of string * smt_typ + | Define_const of string * smt_typ * smt_exp + | Declare_datatypes of string * (string * (string * smt_typ) list) list + | Assert of smt_exp + +let declare_datatypes = function Datatype (name, ctors) -> Declare_datatypes (name, ctors) | _ -> assert false diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml new file mode 100644 index 000000000..b347882fa --- /dev/null +++ b/src/lib/smt_gen.ml @@ -0,0 +1,1232 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2023 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Ast_util +open Jib +open Jib_util +open Smt_exp + +let zencode_upper_id id = Util.zencode_upper_string (string_of_id id) +let zencode_id id = Util.zencode_string (string_of_id id) + +let zencode_uid (id, ctyps) = + match ctyps with + | [] -> Util.zencode_string (string_of_id id) + | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) + +(* [required_width n] is the required number of bits to losslessly + represent an integer n *) +let required_width n = + let rec required_width' n = + if Big_int.equal n Big_int.zero then 1 else 1 + required_width' (Big_int.shift_right n 1) + in + required_width' (Big_int.abs n) + +(* Generate SMT definitions in a writer monad that keeps tracks of any + overflow checks needed. *) + +type checks = { overflows : smt_exp list; strings_used : bool; reals_used : bool } + +let empty_checks = { overflows = []; strings_used = false; reals_used = false } + +let append_checks c1 c2 = + { + overflows = c1.overflows @ c2.overflows; + strings_used = c1.strings_used || c2.strings_used; + reals_used = c1.reals_used || c2.reals_used; + } + +type 'a check_writer_state = { value : 'a; checks : checks } + +type 'a check_writer = Parse_ast.l -> 'a check_writer_state + +let return x _ = { value = x; checks = empty_checks } + +let current_location l = { value = l; checks = empty_checks } + +let bind m f l = + let state = m l in + let state' = f state.value l in + { value = state'.value; checks = append_checks state.checks state'.checks } + +let fmap f m l = + let state = m l in + let value = f state.value in + { value; checks = state.checks } + +let ( let* ) = bind + +let ( let+ ) m f = fmap f m + +let rec mapM f = function + | [] -> return [] + | x :: xs -> + let* x = f x in + let* xs = mapM f xs in + return (x :: xs) + +let run m l = + let state = m l in + (state.value, state.checks) + +let overflow_check check (_ : Parse_ast.l) = { value = (); checks = { empty_checks with overflows = [check] } } + +let string_used (_ : Parse_ast.l) = { value = (); checks = { empty_checks with strings_used = true } } + +let real_used (_ : Parse_ast.l) = { value = (); checks = { empty_checks with reals_used = true } } + +(* [signed_size n m exp] takes a smt expression assumed to be a + integer (signed bitvector) of length m and forces it to be length n + by either sign extending it or truncating it as required *) +let signed_size ?(checked = true) ~into:n ~from:m smt = + if n = m then return smt + else if n > m then return (SignExtend (n, n - m, smt)) + else ( + let check = + (* If the top bit of the truncated number is one *) + Ite + ( Fn ("=", [Extract (n - 1, n - 1, smt); Bitvec_lit [Sail2_values.B1]]), + (* Then we have an overflow, unless all bits we truncated were also one *) + Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvones (m - n)])]), + (* Otherwise, all the top bits must be zero *) + Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvzero (m - n)])]) + ) + in + let* _ = if checked then overflow_check check else return () in + return (Extract (n - 1, 0, smt)) + ) + +(* [unsigned_size n m exp] is much like signed_size, but it assumes + that the bitvector is unsigned, so it either zero extends or + truncates as required. *) +let unsigned_size ?max_value ?(checked = true) ~into:n ~from:m smt = + if n = m then return smt + else if n > m then return (Fn ("concat", [bvzero (n - m); smt])) + else + (* Ensure we don't overwrite any high bits when truncating *) + let* _ = + if checked then overflow_check (Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvzero (m - n)])])) else return () + in + return (Extract (n - 1, 0, smt)) + +(* We often need to create a SMT bitvector of a length sz with integer + value x. [bvpint sz x] does this for positive integers, and [bvint sz x] + does this for all integers. It's quite awkward because we + don't have a very good way to get the binary representation of + either an OCaml integer or a big integer. *) +let bvpint ?(loc = Parse_ast.Unknown) sz x = + let open Sail2_values in + if Big_int.less_equal Big_int.zero x && Big_int.less_equal x (Big_int.of_int max_int) then ( + let x = Big_int.to_int x in + match Printf.sprintf "%X" x |> Util.string_to_list |> List.map nibble_of_char |> Util.option_all with + | Some nibbles -> + let bin = List.map (fun (a, b, c, d) -> [a; b; c; d]) nibbles |> List.concat in + let _, bin = Util.take_drop (function B0 -> true | _ -> false) bin in + let padding = List.init (sz - List.length bin) (fun _ -> B0) in + Bitvec_lit (padding @ bin) + | None -> assert false + ) + else if Big_int.greater x (Big_int.of_int max_int) then ( + let y = ref x in + let bin = ref [] in + while not (Big_int.equal !y Big_int.zero) do + let q, m = Big_int.quomod !y (Big_int.of_int 2) in + bin := (if Big_int.equal m Big_int.zero then B0 else B1) :: !bin; + y := q + done; + let padding_size = sz - List.length !bin in + if padding_size < 0 then + raise + (Reporting.err_general loc + (Printf.sprintf "Could not create a %d-bit integer with value %s.\nTry increasing the maximum integer size." + sz (Big_int.to_string x) + ) + ); + let padding = List.init padding_size (fun _ -> B0) in + Bitvec_lit (padding @ !bin) + ) + else Reporting.unreachable loc __POS__ "bvpint called on non-positive integer" + +let bvint sz x = + if Big_int.less x Big_int.zero then + Fn ("bvadd", [Fn ("bvnot", [bvpint sz (Big_int.abs x)]); bvpint sz (Big_int.of_int 1)]) + else bvpint sz x + +(* [required_width n] is the required number of bits to losslessly + represent an integer n *) +let required_width n = + let rec required_width' n = + if Big_int.equal n Big_int.zero then 1 else 1 + required_width' (Big_int.shift_right n 1) + in + required_width' (Big_int.abs n) + +module type CONFIG = sig + val max_unknown_integer_width : int + val max_unknown_bitvector_width : int + val union_ctyp_classify : ctyp -> bool +end + +module type PRIMOP_GEN = sig + val print_bits : Parse_ast.l -> ctyp -> string + val string_of_bits : Parse_ast.l -> ctyp -> string + val dec_str : Parse_ast.l -> ctyp -> string + val hex_str : Parse_ast.l -> ctyp -> string + val hex_str_upper : Parse_ast.l -> ctyp -> string + val count_leading_zeros : Parse_ast.l -> int -> string + val fvector_store : Parse_ast.l -> int -> ctyp -> string + val is_empty : Parse_ast.l -> ctyp -> string + val hd : Parse_ast.l -> ctyp -> string + val tl : Parse_ast.l -> ctyp -> string +end + +let builtin_type_error fn cvals ret_ctyp_opt = + let* l = current_location in + let args = Util.string_of_list ", " (fun cval -> string_of_ctyp (cval_ctyp cval)) cvals in + match ret_ctyp_opt with + | Some ret_ctyp -> + let message = Printf.sprintf "%s : (%s) -> %s" fn args (string_of_ctyp ret_ctyp) in + raise (Reporting.err_todo l message) + | None -> raise (Reporting.err_todo l (Printf.sprintf "%s : (%s)" fn args)) + +module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct + let lint_size = Config.max_unknown_integer_width + let lbits_size = Config.max_unknown_bitvector_width + let lbits_index = required_width (Big_int.of_int (lbits_size - 1)) + + let int_size = function + | CT_constant n -> required_width n + | CT_fint sz -> sz + | CT_lint -> lint_size + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Argument to int_size must be an integer type" + + let bv_size = function + | CT_fbits sz | CT_sbits sz -> sz + | CT_lbits -> lbits_size + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Argument to bv_size must be a bitvector type" + + let to_fbits ctyp bv = + match ctyp with + | CT_fbits n -> (n, bv) + | CT_lbits -> (lbits_size, Fn ("contents", [bv])) + | _ -> + Reporting.unreachable Parse_ast.Unknown __POS__ + (Printf.sprintf "Type %s must be a bitvector in to_fbits" (string_of_ctyp ctyp)) + + let literal vl ctyp = + let open Value2 in + match (vl, ctyp) with + | VL_bits bv, CT_fbits n -> unsigned_size ~into:n ~from:(List.length bv) (Bitvec_lit bv) + | VL_bool b, _ -> return (Bool_lit b) + | VL_int n, CT_constant m -> return (bvint (required_width n) n) + | VL_int n, CT_fint sz -> return (bvint sz n) + | VL_int n, CT_lint -> return (bvint Config.max_unknown_integer_width n) + | VL_bit b, CT_bit -> return (Bitvec_lit [b]) + | VL_unit, _ -> return (Enum "unit") + | VL_string str, _ -> + let* _ = string_used in + return (String_lit str) + | VL_real str, _ -> + let* _ = real_used in + return (if str.[0] = '-' then Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))]) else Real_lit str) + | VL_ref str, _ -> return (Fn ("reg_ref", [String_lit str])) + | _ -> + let* l = current_location in + Reporting.unreachable l __POS__ + ("Cannot translate literal to SMT: " ^ string_of_value vl ^ " : " ^ string_of_ctyp ctyp) + + let smt_cval_call op args = + match (op, args) with + | Bnot, [arg] -> Fn ("not", [arg]) + | Bor, [arg] -> arg + | Bor, args -> Fn ("or", args) + | Band, [arg] -> arg + | Band, args -> Fn ("and", args) + | Eq, args -> Fn ("=", args) + | Neq, args -> Fn ("not", [Fn ("=", args)]) + | Ilt, [lhs; rhs] -> Fn ("bvslt", [lhs; rhs]) + | Ilteq, [lhs; rhs] -> Fn ("bvsle", [lhs; rhs]) + | Igt, [lhs; rhs] -> Fn ("bvsgt", [lhs; rhs]) + | Igteq, [lhs; rhs] -> Fn ("bvsge", [lhs; rhs]) + | Iadd, args -> Fn ("bvadd", args) + | Isub, args -> Fn ("bvsub", args) + | Bvnot, args -> Fn ("bvnot", args) + | Bvor, args -> Fn ("bvor", args) + | Bvand, args -> Fn ("bvand", args) + | Bvxor, args -> Fn ("bvxor", args) + | Bvadd, args -> Fn ("bvadd", args) + | Bvsub, args -> Fn ("bvsub", args) + | Concat, args -> Fn ("concat", args) + | Zero_extend _, _ -> failwith "ZE" + | Sign_extend _, _ -> failwith "SE" + | Slice _, _ -> failwith "slice" + | Sslice _, _ -> failwith "sslice" + | Set_slice, _ -> failwith "set_slice" + | Replicate _, _ -> failwith "replicate" + | List_hd, [arg] -> Fn ("hd", [arg]) + | op, _ -> failwith (string_of_op op) + + let rec smt_cval cval = + match cval_ctyp cval with + | CT_constant n -> return (bvint (required_width n) n) + | _ -> ( + match cval with + | V_lit (vl, ctyp) -> literal vl ctyp + | V_id (id, _) -> return (Var id) + | V_call (List_hd, [arg]) -> + let* l = current_location in + let op = Primop_gen.hd l (cval_ctyp arg) in + let* arg = smt_cval arg in + return (Hd (op, arg)) + | V_call (List_tl, [arg]) -> + let* l = current_location in + let op = Primop_gen.tl l (cval_ctyp arg) in + let* arg = smt_cval arg in + return (Tl (op, arg)) + | V_call (List_is_empty, [arg]) -> + let* l = current_location in + let op = Primop_gen.is_empty l (cval_ctyp arg) in + let* arg = smt_cval arg in + return (Fn (op, [arg])) + | V_call (op, args) -> + let* args = mapM smt_cval args in + return (smt_cval_call op args) + | V_ctor_kind (union, ctor, _) -> + let* union = smt_cval union in + return (Fn ("not", [Tester (zencode_uid ctor, union)])) + | V_ctor_unwrap (union, (ctor, _), _) -> + let union_ctyp = cval_ctyp union in + let* union = smt_cval union in + return (Unwrap (ctor, Config.union_ctyp_classify union_ctyp, union)) + | V_field (record, field) -> begin + match cval_ctyp record with + | CT_struct (struct_id, _) -> + let* record = smt_cval record in + return (Field (struct_id, field, record)) + | _ -> failwith "Field for non-struct type" + end + | cval -> return (Var (Name (mk_id "UNKNOWN", -1))) (* failwith ("Unrecognised cval " ^ string_of_cval cval) *) + ) + + (* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval + which must be an integer type (either CT_fint, or CT_lint), and + produces a bitvector which is either zero extended or truncated to + exactly esz bits. *) + let bvzeint esz cval = + let sz = int_size (cval_ctyp cval) in + match cval with + | V_lit (VL_int n, _) -> return (bvint esz n) + | _ -> + let* smt = smt_cval cval in + return + ( if esz = sz then smt + else if esz > sz then Fn ("concat", [bvzero (esz - sz); smt]) + else Extract (esz - 1, 0, smt) + ) + + let builtin_arith fn big_int_fn padding v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | _, _, CT_constant c -> return (bvint (required_width c) c) + | CT_constant c1, CT_constant c2, _ -> return (bvint (int_size ret_ctyp) (big_int_fn c1 c2)) + | ctyp1, ctyp2, _ -> + (* To detect arithmetic overflow we can expand the input + bitvectors to some size determined by a padding function, + then check we don't lose precision when going back after + performing the operation. *) + let ret_sz = int_size ret_ctyp in + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let* padded_smt1 = signed_size ~into:(padding ret_sz) ~from:(int_size ctyp1) smt1 in + let* padded_smt2 = signed_size ~into:(padding ret_sz) ~from:(int_size ctyp2) smt2 in + signed_size ~into:ret_sz ~from:(padding ret_sz) (Fn (fn, [padded_smt1; padded_smt2])) + + let builtin_add_int = builtin_arith "bvadd" Big_int.add (fun x -> x + 1) + let builtin_sub_int = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1) + let builtin_mult_int = builtin_arith "bvmul" Big_int.mul (fun x -> x * 2) + + let builtin_neg_int v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | _, CT_constant c -> return (bvint (required_width c) c) + | CT_constant c, _ -> return (bvint (int_size ret_ctyp) (Big_int.negate c)) + | ctyp, _ -> + let open Sail2_values in + let* smt = bind (smt_cval v) (signed_size ~into:(int_size ret_ctyp) ~from:(int_size ctyp)) in + let* _ = overflow_check (Fn ("=", [smt; Bitvec_lit (B1 :: List.init (int_size ret_ctyp - 1) (fun _ -> B0))])) in + return (Fn ("bvneg", [smt])) + + let builtin_abs_int v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | _, CT_constant c -> return (bvint (required_width c) c) + | CT_constant c, _ -> return (bvint (int_size ret_ctyp) (Big_int.abs c)) + | ctyp, _ -> + let sz = int_size ctyp in + let* smt = smt_cval v in + let* resized_pos = signed_size ~into:(int_size ret_ctyp) ~from:sz smt in + let* resized_neg = signed_size ~into:(int_size ret_ctyp) ~from:sz (bvneg smt) in + return (Ite (Fn ("=", [Extract (sz - 1, sz - 1, smt); bvone 1]), resized_neg, resized_pos)) + + let builtin_choose_int compare op v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2) with + | CT_constant n, CT_constant m -> return (bvint (int_size ret_ctyp) (op n m)) + | ctyp1, ctyp2 -> + let ret_sz = int_size ret_ctyp in + let* smt1 = bind (smt_cval v1) (signed_size ~into:ret_sz ~from:(int_size ctyp1)) in + let* smt2 = bind (smt_cval v2) (signed_size ~into:ret_sz ~from:(int_size ctyp2)) in + return (Ite (Fn (compare, [smt1; smt2]), smt1, smt2)) + + let builtin_max_int = builtin_choose_int "bvsgt" max + let builtin_min_int = builtin_choose_int "bvslt" min + + let smt_conversion ~into:to_ctyp ~from:from_ctyp x = + match (from_ctyp, to_ctyp) with + | _, _ when ctyp_equal from_ctyp to_ctyp -> return x + | _, CT_constant c -> return (bvint (required_width c) c) + | CT_constant c, CT_fint sz -> return (bvint sz c) + | CT_constant c, CT_lint -> return (bvint lint_size c) + | CT_fint sz, CT_lint -> signed_size ~into:lint_size ~from:sz x + | CT_lint, CT_fint sz -> signed_size ~into:sz ~from:lint_size x + | CT_lint, CT_fbits n -> signed_size ~into:n ~from:lint_size x + | CT_lint, CT_lbits -> + let* x = signed_size ~into:lbits_size ~from:lint_size x in + return (Fn ("Bits", [bvint lbits_index (Big_int.of_int lint_size); x])) + | CT_fint n, CT_lbits -> + let* x = signed_size ~into:lbits_size ~from:n x in + return (Fn ("Bits", [bvint lbits_index (Big_int.of_int n); x])) + | CT_lbits, CT_fbits n -> unsigned_size ~into:n ~from:lbits_size (Fn ("contents", [x])) + | CT_fbits n, CT_fbits m -> unsigned_size ~into:m ~from:n x + | CT_fbits n, CT_lbits -> + let* x = unsigned_size ~into:lbits_size ~from:n x in + return (Fn ("Bits", [bvint lbits_index (Big_int.of_int n); x])) + | _, _ -> + let* l = current_location in + Reporting.unreachable l __POS__ + (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp)) + + let int_comparison fn big_int_fn v1 v2 = + let* sv1 = smt_cval v1 in + let* sv2 = smt_cval v2 in + match (cval_ctyp v1, cval_ctyp v2) with + | CT_constant c1, CT_constant c2 -> return (Bool_lit (big_int_fn c1 c2)) + | CT_lint, CT_lint -> return (Fn (fn, [sv1; sv2])) + | CT_fint sz1, CT_fint sz2 -> + return + ( if sz1 == sz2 then Fn (fn, [sv1; sv2]) + else if sz1 > sz2 then Fn (fn, [sv1; SignExtend (sz1, sz1 - sz2, sv2)]) + else Fn (fn, [SignExtend (sz2, sz2 - sz1, sv1); sv2]) + ) + | CT_constant c, CT_fint sz -> return (Fn (fn, [bvint sz c; sv2])) + | CT_fint sz, CT_constant c -> return (Fn (fn, [sv1; bvint sz c])) + | CT_constant c, CT_lint -> return (Fn (fn, [bvint lint_size c; sv2])) + | CT_lint, CT_constant c -> return (Fn (fn, [sv1; bvint lint_size c])) + | CT_fint sz, CT_lint when sz < lint_size -> return (Fn (fn, [SignExtend (lint_size, lint_size - sz, sv1); sv2])) + | CT_lint, CT_fint sz when sz < lint_size -> return (Fn (fn, [sv1; SignExtend (lint_size, lint_size - sz, sv2)])) + | _, _ -> builtin_type_error fn [v1; v2] None + + let builtin_eq_int = int_comparison "=" Big_int.equal + + let builtin_lt = int_comparison "bvslt" Big_int.less + let builtin_lteq = int_comparison "bvsle" Big_int.less_equal + let builtin_gt = int_comparison "bvsgt" Big_int.greater + let builtin_gteq = int_comparison "bvsge" Big_int.greater_equal + + let builtin_signed v ret_ctyp = + let* sv = smt_cval v in + match (cval_ctyp v, ret_ctyp) with + | CT_fbits n, CT_fint m when m >= n -> return (SignExtend (m, m - n, sv)) + | CT_fbits n, CT_lint -> return (SignExtend (lint_size, lint_size - n, sv)) + | CT_lbits, CT_lint -> + let contents = Fn ("contents", [sv]) in + let top_bit_shift = ZeroExtend (lbits_size, lbits_index, bvsub (Fn ("len", [sv])) (bvone lbits_index)) in + let top_bit = Extract (0, 0, bvlshr contents top_bit_shift) in + let is_signed = Fn ("=", [top_bit; bvone 1]) in + let* zero_extended = unsigned_size ~into:lint_size ~from:lbits_size contents in + let ones_mask = bvshl (bvones lint_size) (ZeroExtend (lint_size, lbits_index, Fn ("len", [sv]))) in + let ones_extended = bvor ones_mask zero_extended in + return (Ite (is_signed, ones_extended, zero_extended)) + | _, _ -> builtin_type_error "signed" [v] (Some ret_ctyp) + + let builtin_unsigned v ret_ctyp = + let* sv = smt_cval v in + match (cval_ctyp v, ret_ctyp) with + | CT_fbits n, CT_fint m when m > n -> return (Fn ("concat", [bvzero (m - n); sv])) + | CT_fbits n, CT_lint -> return (Fn ("concat", [bvzero (lint_size - n); sv])) + | CT_lbits, CT_lint -> signed_size ~into:lint_size ~from:lbits_size (Fn ("contents", [sv])) + | CT_lbits, CT_fint m -> signed_size ~into:m ~from:lbits_size (Fn ("contents", [sv])) + | _, _ -> builtin_type_error "unsigned" [v] (Some ret_ctyp) + + let bvmask len = + let all_ones = bvones lbits_size in + let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); len]) in + bvnot (bvshl all_ones shift) + + let builtin_shift shiftop vbits vshift ret_ctyp = + match cval_ctyp vbits with + | CT_fbits n -> + let* bv = smt_cval vbits in + let* shift = bvzeint n vshift in + return (Fn (shiftop, [bv; shift])) + | CT_lbits -> + let* bv = smt_cval vbits in + let* shift = bvzeint lbits_size vshift in + let shifted = + if shiftop = "bvashr" then ( + let mask = bvmask (Fn ("len", [bv])) in + bvand mask (Fn (shiftop, [bvor (bvnot mask) (Fn ("contents", [bv])); shift])) + ) + else Fn (shiftop, [Fn ("contents", [bv]); shift]) + in + return (Fn ("Bits", [Fn ("len", [bv]); shifted])) + | _ -> builtin_type_error shiftop [vbits; vshift] (Some ret_ctyp) + + let builtin_slice v1 v2 v3 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, ret_ctyp) with + | CT_lbits, CT_constant start, CT_constant len, CT_fbits _ -> + let top = Big_int.pred (Big_int.add start len) in + let* v1 = smt_cval v1 in + return (Extract (Big_int.to_int top, Big_int.to_int start, Fn ("contents", [v1]))) + | CT_fbits _, CT_constant start, CT_constant len, CT_fbits _ -> + let top = Big_int.pred (Big_int.add start len) in + let* v1 = smt_cval v1 in + return (Extract (Big_int.to_int top, Big_int.to_int start, v1)) + | CT_fbits _, CT_fint _, CT_constant len, CT_fbits _ -> + let* shifted = builtin_shift "bvlshr" v1 v2 (cval_ctyp v1) in + return (Extract (Big_int.to_int (Big_int.pred len), 0, shifted)) + | ctyp1, ctyp2, _, CT_lbits -> + let* smt1 = smt_cval v1 in + let sz, smt1 = to_fbits ctyp1 smt1 in + let* smt1 = unsigned_size ~into:lbits_size ~from:sz smt1 in + let* smt2 = bind (smt_cval v2) (signed_size ~into:lbits_size ~from:(int_size ctyp2)) in + let* smt3 = bvzeint lbits_index v3 in + return (Fn ("Bits", [smt3; Fn ("bvand", [Fn ("bvlshr", [smt1; smt2]); bvmask smt3])])) + | _ -> builtin_type_error "slice" [v1; v2; v3] (Some ret_ctyp) + + let builtin_zeros v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | _, CT_fbits n -> return (bvzero n) + | CT_constant c, CT_lbits -> return (Fn ("Bits", [bvint lbits_index c; bvzero lbits_size])) + | ctyp, CT_lbits when int_size ctyp >= lbits_index -> + let* v = smt_cval v in + return (Fn ("Bits", [extract (lbits_index - 1) 0 v; bvzero lbits_size])) + | _ -> builtin_type_error "zeros" [v] (Some ret_ctyp) + + let builtin_ones cval = function + | CT_fbits n -> return (bvones n) + | CT_lbits -> + let* v = smt_cval cval in + let len = extract (lbits_index - 1) 0 v in + return (Fn ("Bits", [len; Fn ("bvand", [bvmask len; bvones lbits_size])])) + | ret_ctyp -> builtin_type_error "ones" [cval] (Some ret_ctyp) + + let builtin_zero_extend vbits vlen ret_ctyp = + match (cval_ctyp vbits, cval_ctyp vlen, ret_ctyp) with + | CT_fbits n, _, CT_fbits m when n = m -> smt_cval vbits + | CT_fbits n, _, CT_fbits m -> + let* bv = smt_cval vbits in + return (Fn ("concat", [bvzero (m - n); bv])) + | CT_fbits n, CT_fint m, CT_lbits -> + let* bv = smt_cval vbits in + return (Fn ("concat", [bvzero (m - n); bv])) + | CT_lbits, _, CT_fbits m -> + let* bv = smt_cval vbits in + return (Extract (m - 1, 0, Fn ("contents", [bv]))) + (* + | CT_fbits n, CT_lbits -> + assert (lbits_size ctx >= n); + let vbits = + if lbits_size ctx = n then smt_cval ctx vbits + else if lbits_size ctx > n then Fn ("concat", [bvzero (lbits_size ctx - n); smt_cval ctx vbits]) + else assert false + in + Fn ("Bits", [bvzeint ctx ctx.lbits_index vlen; vbits]) + *) + | CT_lbits, CT_lint, CT_lbits -> + let* len = smt_cval vlen in + let* bv = smt_cval vbits in + return (Fn ("Bits", [extract (lbits_index - 1) 0 len; Fn ("contents", [bv])])) + | _ -> builtin_type_error "zero_extend" [vbits; vlen] (Some ret_ctyp) + + let builtin_sign_extend vbits vlen ret_ctyp = + let* bv = smt_cval vbits in + match (cval_ctyp vbits, cval_ctyp vlen, ret_ctyp) with + | CT_fbits n, _, CT_fbits m when n = m -> smt_cval vbits + | CT_fbits n, _, CT_fbits m -> + let top_bit_one = Fn ("=", [Extract (n - 1, n - 1, bv); bvone 1]) in + return (Ite (top_bit_one, Fn ("concat", [bvones (m - n); bv]), Fn ("concat", [bvzero (m - n); bv]))) + | CT_lbits, i_ctyp, CT_lbits -> + let* len = smt_cval vlen in + let contents = Fn ("contents", [bv]) in + let top_bit_shift = ZeroExtend (lbits_size, lbits_index, bvsub (Fn ("len", [bv])) (bvone lbits_index)) in + let top_bit = Extract (0, 0, bvlshr contents top_bit_shift) in + let is_signed = Fn ("=", [top_bit; bvone 1]) in + let* new_len = signed_size ~into:lbits_index ~from:(int_size i_ctyp) len in + let zero_extended = Fn ("Bits", [new_len; contents]) in + let ones_mask = bvshl (bvones lbits_size) (ZeroExtend (lbits_size, lbits_index, Fn ("len", [bv]))) in + let unused_mask = bvnot (bvshl (bvones lbits_size) (ZeroExtend (lbits_size, lbits_index, new_len))) in + let ones_extended = Fn ("Bits", [new_len; bvand unused_mask (bvor ones_mask contents)]) in + return (Ite (is_signed, ones_extended, zero_extended)) + | _ -> builtin_type_error "sign_extend" [vbits; vlen] (Some ret_ctyp) + + let builtin_replicate_bits vbits vtimes ret_ctyp = + match (cval_ctyp vbits, cval_ctyp vtimes, ret_ctyp) with + | CT_fbits n, _, CT_fbits m -> + let* bits = smt_cval vbits in + let times = m / n in + return (Fn ("concat", List.init times (fun _ -> bits))) + | CT_fbits n, vtimes_ctyp, CT_lbits -> + let max_times = (lbits_size / n) + 1 in + let* times = bind (smt_cval vtimes) (signed_size ~into:lbits_index ~from:(int_size vtimes_ctyp)) in + let len = bvmul (bvpint lbits_index (Big_int.of_int n)) times in + let* bits = smt_cval vbits in + let contents = Extract (lbits_size - 1, 0, Fn ("concat", List.init max_times (fun _ -> bits))) in + return (Fn ("Bits", [len; Fn ("bvand", [bvmask len; contents])])) + | CT_lbits, vtimes_ctyp, CT_lbits -> + let* bits = smt_cval vbits in + let* times = bind (smt_cval vtimes) (signed_size ~into:lbits_index ~from:(int_size vtimes_ctyp)) in + let new_len = bvmul (Fn ("len", [bits])) times in + (* This is extremely inefficient, but we don't have a good alternative if we find ourselves in this case. *) + let shifted = + List.init (lbits_size - 1) (fun n -> + let amount = + bvmul + (bvpint lbits_size (Big_int.of_int (n + 1))) + (ZeroExtend (lbits_size, lbits_index, Fn ("len", [bits]))) + in + bvshl (Fn ("contents", [bits])) amount + ) + in + let contents = List.fold_left bvor (Fn ("contents", [bits])) shifted in + return (Fn ("Bits", [new_len; Fn ("bvand", [bvmask new_len; contents])])) + | _ -> builtin_type_error "replicate_bits" [vbits; vtimes] (Some ret_ctyp) + + let builtin_not_bits v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | CT_lbits, CT_fbits n -> + let* bv = smt_cval v in + return (bvnot (Extract (n - 1, 0, Fn ("contents", [bv])))) + | CT_lbits, CT_lbits -> + let* bv = smt_cval v in + let len = Fn ("len", [bv]) in + return (Fn ("Bits", [len; Fn ("bvand", [bvmask len; bvnot (Fn ("contents", [bv]))])])) + | CT_fbits n, CT_fbits m when n = m -> + let* bv = smt_cval v in + return (bvnot bv) + | _, _ -> builtin_type_error "not_bits" [v] (Some ret_ctyp) + + let builtin_length v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | _, CT_constant len -> return (bvpint (int_size ret_ctyp) len) + | CT_fbits n, _ -> return (bvpint (int_size ret_ctyp) (Big_int.of_int n)) + | CT_lbits, _ -> + let* bv = smt_cval v in + unsigned_size ~into:(int_size ret_ctyp) ~from:lbits_index (Fn ("len", [bv])) + | _ -> builtin_type_error "length" [v] (Some ret_ctyp) + + let builtin_arith_bits op v1 v2 ret_ctyp = + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | CT_fbits n, CT_fbits m, CT_fbits o -> + (* The Sail type system should guarantee this *) + assert (n = m && m = o); + return (Fn (op, [smt1; smt2])) + | CT_lbits, CT_lbits, CT_lbits -> + return (Fn ("Bits", [Fn ("len", [smt1]); Fn (op, [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])) + | _ -> builtin_type_error ("arith_bits " ^ op) [v1; v2] (Some ret_ctyp) + + let builtin_arith_bits_int op v1 v2 ret_ctyp = + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | CT_fbits n, CT_constant c, CT_fbits o -> + assert (n = o); + return (Fn (op, [smt1; bvint o c])) + | CT_fbits n, CT_fint m, CT_fbits o -> + assert (n = o); + let* smt2 = signed_size ~into:o ~from:m smt2 in + return (Fn (op, [smt1; smt2])) + | CT_fbits n, CT_lint, CT_fbits o -> + assert (n = o); + let* smt2 = signed_size ~into:o ~from:lint_size smt2 in + return (Fn (op, [smt1; smt2])) + | CT_lbits, v2_ctyp, CT_lbits -> + let* smt2 = signed_size ~into:lbits_size ~from:(int_size v2_ctyp) smt2 in + return (Fn ("Bits", [Fn ("len", [smt1]); Fn (op, [Fn ("contents", [smt1]); smt2])])) + | _ -> builtin_type_error ("arith_bits_int " ^ op) [v1; v2] (Some ret_ctyp) + + let builtin_eq_bits v1 v2 = + match (cval_ctyp v1, cval_ctyp v2) with + | CT_fbits n, CT_fbits m -> + let o = max n m in + let* smt1 = bind (smt_cval v1) (unsigned_size ~into:o ~from:n) in + let* smt2 = bind (smt_cval v2) (unsigned_size ~into:o ~from:n) in + return (Fn ("=", [smt1; smt2])) + | CT_lbits, CT_lbits -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let len1 = Fn ("len", [smt1]) in + let contents1 = Fn ("contents", [smt1]) in + let len2 = Fn ("len", [smt2]) in + let contents2 = Fn ("contents", [smt2]) in + return + (Fn + ( "and", + [ + Fn ("=", [len1; len2]); + Fn ("=", [Fn ("bvand", [bvmask len1; contents1]); Fn ("bvand", [bvmask len2; contents2])]); + ] + ) + ) + | CT_lbits, CT_fbits n -> + let* smt1 = bind (smt_cval v1) (fun bv -> unsigned_size ~into:n ~from:lbits_size (Fn ("contents", [bv]))) in + let* smt2 = smt_cval v2 in + return (Fn ("=", [smt1; smt2])) + | CT_fbits n, CT_lbits -> + let* smt1 = smt_cval v1 in + let* smt2 = bind (smt_cval v2) (fun bv -> unsigned_size ~into:n ~from:lbits_size (Fn ("contents", [bv]))) in + return (Fn ("=", [smt1; smt2])) + | _ -> builtin_type_error "eq_bits" [v1; v2] None + + let builtin_neq_bits v1 v2 = + let* t = builtin_eq_bits v1 v2 in + return (Fn ("not", [t])) + + let builtin_append v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | CT_fbits n, CT_fbits m, CT_fbits o -> + assert (n + m = o); + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn ("concat", [smt1; smt2])) + | CT_fbits n, CT_lbits, CT_lbits -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let x = Fn ("concat", [bvzero (lbits_size - n); smt1]) in + let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); Fn ("len", [smt2])]) in + return + (Fn + ( "Bits", + [ + bvadd (bvint lbits_index (Big_int.of_int n)) (Fn ("len", [smt2])); + bvor (bvshl x shift) (Fn ("contents", [smt2])); + ] + ) + ) + | CT_lbits, CT_fbits n, CT_fbits m -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Extract (m - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))) + (* + | CT_lbits, CT_fbits n, CT_lbits -> + let smt1 = smt_cval ctx v1 in + let smt2 = smt_cval ctx v2 in + Fn + ( "Bits", + [ + bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt1])); + Extract (lbits_size ctx - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2])); + ] + ) + | CT_fbits n, CT_fbits m, CT_lbits -> + let smt1 = smt_cval ctx v1 in + let smt2 = smt_cval ctx v2 in + Fn + ( "Bits", + [ + bvint ctx.lbits_index (Big_int.of_int (n + m)); + unsigned_size ctx (lbits_size ctx) (n + m) (Fn ("concat", [smt1; smt2])); + ] + ) + *) + | CT_lbits, CT_lbits, CT_lbits -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let x = Fn ("contents", [smt1]) in + let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); Fn ("len", [smt2])]) in + return + (Fn ("Bits", [bvadd (Fn ("len", [smt1])) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))]) + ) + (* + | CT_lbits, CT_lbits, CT_fbits n -> + let smt1 = smt_cval ctx v1 in + let smt2 = smt_cval ctx v2 in + let x = Fn ("contents", [smt1]) in + let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in + unsigned_size ctx n (lbits_size ctx) (bvor (bvshl x shift) (Fn ("contents", [smt2]))) + *) + | _ -> builtin_type_error "append" [v1; v2] (Some ret_ctyp) + + let builtin_sail_truncate v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | v1_ctyp, CT_constant c, CT_fbits m -> + let* smt1 = smt_cval v1 in + let sz, bv = to_fbits v1_ctyp smt1 in + assert (Big_int.to_int c = m && m <= sz); + return (Extract (Big_int.to_int c - 1, 0, bv)) + | v1_ctyp, _, CT_lbits -> + let* smt1 = smt_cval v1 in + let sz, bv = to_fbits v1_ctyp smt1 in + let* smt1 = unsigned_size ~into:lbits_size ~from:sz bv in + let* smt2 = bvzeint lbits_index v2 in + return (Fn ("Bits", [smt2; Fn ("bvand", [bvmask smt2; smt1])])) + | _ -> builtin_type_error "sail_truncate" [v1; v2] (Some ret_ctyp) + + let builtin_sail_truncateLSB v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | v1_ctyp, CT_constant c, CT_fbits m -> + let* smt1 = smt_cval v1 in + let sz, bv = to_fbits v1_ctyp smt1 in + assert (Big_int.to_int c = m && m <= sz); + return (Extract (sz - 1, sz - Big_int.to_int c, bv)) + | CT_fbits sz, _, CT_lbits -> + let* smt1 = smt_cval v1 in + let* len = bvzeint lbits_index v2 in + let shift = bvsub (bvpint lbits_index (Big_int.of_int sz)) len in + let shifted = bvlshr smt1 (ZeroExtend (sz, lbits_index, shift)) in + let* shifted = unsigned_size ~checked:false ~into:lbits_size ~from:sz shifted in + return (Fn ("Bits", [len; shifted])) + | CT_lbits, _, CT_lbits -> + let* smt1 = smt_cval v1 in + let* len = bvzeint lbits_index v2 in + let shift = bvsub (Fn ("len", [smt1])) len in + let shifted = bvlshr (Fn ("contents", [smt1])) (ZeroExtend (lbits_size, lbits_index, shift)) in + return (Fn ("Bits", [len; shifted])) + | _ -> builtin_type_error "sail_truncateLSB" [v1; v2] (Some ret_ctyp) + + let builtin_bitwise fn v1 v2 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with + | CT_fbits n, CT_fbits m, CT_fbits o -> + assert (n = m && m = o); + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn (fn, [smt1; smt2])) + | CT_lbits, CT_lbits, CT_lbits -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn ("Bits", [Fn ("len", [smt1]); Fn (fn, [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])) + | _ -> builtin_type_error fn [v1; v2] (Some ret_ctyp) + + let fbits_mask mask_sz len = bvnot (bvshl (bvones mask_sz) len) + + let builtin_vector_access vec i ret_ctyp = + match (cval_ctyp vec, cval_ctyp i, ret_ctyp) with + | CT_fbits n, CT_constant i, CT_bit -> + let* bv = smt_cval vec in + return (Extract (Big_int.to_int i, Big_int.to_int i, bv)) + | CT_lbits, CT_constant i, CT_bit -> + let* bv = smt_cval vec in + return (Extract (Big_int.to_int i, Big_int.to_int i, Fn ("contents", [bv]))) + | ((CT_lbits | CT_fbits _) as bv_ctyp), i_ctyp, CT_bit -> + let* bv = smt_cval vec in + let sz, bv = to_fbits bv_ctyp bv in + let* i = smt_cval i in + (* checked:false should be fine here, as the Sail type system has already checked the bounds *) + let* shift = signed_size ~checked:false ~into:sz ~from:(int_size i_ctyp) i in + return (Extract (0, 0, Fn ("bvlshr", [bv; shift]))) + | CT_fvector (len, _), i_ctyp, _ -> + 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)) - 1) ~from:(int_size i_ctyp)) + in + return (Fn ("select", [vec; i])) + (* + | CT_vector _, CT_constant i, _ -> Fn ("select", [smt_cval ctx vec; bvint !vector_index i]) + | CT_vector _, index_ctyp, _ -> + Fn ("select", [smt_cval ctx vec; force_size ctx !vector_index (int_size ctx index_ctyp) (smt_cval ctx i)]) + *) + | _ -> builtin_type_error "vector_access" [vec; i] (Some ret_ctyp) + + let builtin_vector_subrange vec i j ret_ctyp = + match (cval_ctyp vec, cval_ctyp i, cval_ctyp j, ret_ctyp) with + | CT_fbits n, CT_constant i, CT_constant j, CT_fbits _ -> + let* vec = smt_cval vec in + return (Extract (Big_int.to_int i, Big_int.to_int j, vec)) + | CT_lbits, CT_constant i, CT_constant j, CT_fbits _ -> + let* vec = smt_cval vec in + return (Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [vec]))) + (* + | CT_fbits n, i_ctyp, CT_constant j, CT_lbits when Big_int.equal j Big_int.zero -> + let i' = signed_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in + let len = bvadd i' (bvint ctx.lbits_index (Big_int.of_int 1)) in + Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])]) + *) + | bv_ctyp, i_ctyp, j_ctyp, ret_ctyp -> + let* vec = smt_cval vec in + let sz, vec = to_fbits bv_ctyp vec in + let* i' = bind (smt_cval i) (signed_size ~into:sz ~from:(int_size i_ctyp)) in + let* j' = bind (smt_cval j) (signed_size ~into:sz ~from:(int_size j_ctyp)) in + let len = bvadd (bvadd i' (bvneg j')) (bvint sz (Big_int.of_int 1)) in + let extracted = bvand (bvlshr vec j') (fbits_mask sz len) in + smt_conversion ~into:ret_ctyp ~from:(CT_fbits sz) extracted + + let builtin_vector_update vec i x ret_ctyp = + match (cval_ctyp vec, cval_ctyp i, cval_ctyp x, ret_ctyp) with + | CT_fbits n, CT_constant i, CT_bit, CT_fbits m when n - 1 > Big_int.to_int i && Big_int.to_int i > 0 -> + assert (n = m); + let* bv = smt_cval vec in + let* x = smt_cval x in + let top = Extract (n - 1, Big_int.to_int i + 1, bv) in + let bot = Extract (Big_int.to_int i - 1, 0, bv) in + return (Fn ("concat", [top; Fn ("concat", [x; bot])])) + | CT_fbits n, CT_constant i, CT_bit, CT_fbits m when n - 1 = Big_int.to_int i && Big_int.to_int i > 0 -> + let* bv = smt_cval vec in + let* x = smt_cval x in + let bot = Extract (Big_int.to_int i - 1, 0, bv) in + return (Fn ("concat", [x; bot])) + | CT_fbits n, CT_constant i, CT_bit, CT_fbits m when n - 1 > Big_int.to_int i && Big_int.to_int i = 0 -> + let* bv = smt_cval vec in + let* x = smt_cval x in + let top = Extract (n - 1, 1, bv) in + return (Fn ("concat", [top; x])) + | CT_fbits n, CT_constant i, CT_bit, CT_fbits m when n - 1 = 0 && Big_int.to_int i = 0 -> smt_cval x + | CT_fbits n, i_ctyp, CT_bit, CT_fbits m -> + assert (n = m); + let* bv = smt_cval vec in + let* bit = smt_cval x in + (* Sail type system won't allow us to index out of range *) + let* shift = bind (smt_cval i) (unsigned_size ~checked:false ~into:n ~from:(int_size i_ctyp)) in + let mask = bvnot (bvshl (ZeroExtend (n, n - 1, bvone 1)) shift) in + let shifted_bit = bvshl (ZeroExtend (n, n - 1, bit)) shift in + return (bvor (bvand mask bv) shifted_bit) + | CT_lbits, i_ctyp, CT_bit, CT_lbits -> + let* bv = smt_cval vec in + let* bit = smt_cval x in + (* Sail type system won't allow us to index out of range *) + let* shift = bind (smt_cval i) (unsigned_size ~checked:false ~into:lbits_size ~from:(int_size i_ctyp)) in + let mask = bvnot (bvshl (ZeroExtend (lbits_size, lbits_size - 1, bvone 1)) shift) in + let shifted_bit = bvshl (ZeroExtend (lbits_size, lbits_size - 1, bit)) shift in + let contents = bvor (bvand mask (Fn ("contents", [bv]))) shifted_bit in + return (Fn ("Bits", [Fn ("len", [bv]); contents])) + | CT_fvector (len, ctyp), i_ctyp, _, CT_fvector (len_out, _) -> + assert (len = len_out); + let* l = current_location in + let store_fn = Primop_gen.fvector_store l len ctyp in + let* vec = smt_cval vec in + 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)) - 1) ~from:(int_size i_ctyp)) + in + return (Store (Fixed len, store_fn, vec, i, x)) + (* + | CT_vector _, CT_constant i, ctyp, CT_vector _ -> + Fn ("store", [smt_cval ctx vec; bvint !vector_index i; smt_cval ctx x]) + | CT_vector _, index_ctyp, _, CT_vector _ -> + Fn + ( "store", + [smt_cval ctx vec; force_size ctx !vector_index (int_size ctx index_ctyp) (smt_cval ctx i); smt_cval ctx x] + ) + *) + | _ -> builtin_type_error "vector_update" [vec; i; x] (Some ret_ctyp) + + let builtin_vector_update_subrange vec i j x ret_ctyp = + match (cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp) with + | CT_fbits n, CT_constant i, CT_constant j, CT_fbits sz, CT_fbits m + when n - 1 > Big_int.to_int i && Big_int.to_int j > 0 -> + assert (n = m); + let* vec = smt_cval vec in + let* x = smt_cval x in + let top = Extract (n - 1, Big_int.to_int i + 1, vec) in + let bot = Extract (Big_int.to_int j - 1, 0, vec) in + return (Fn ("concat", [top; Fn ("concat", [x; bot])])) + | CT_fbits n, CT_constant i, CT_constant j, CT_fbits sz, CT_fbits m + when n - 1 = Big_int.to_int i && Big_int.to_int j > 0 -> + assert (n = m); + let* vec = smt_cval vec in + let* x = smt_cval x in + let bot = Extract (Big_int.to_int j - 1, 0, vec) in + return (Fn ("concat", [x; bot])) + | CT_fbits n, CT_constant i, CT_constant j, CT_fbits sz, CT_fbits m + when n - 1 > Big_int.to_int i && Big_int.to_int j = 0 -> + assert (n = m); + let* vec = smt_cval vec in + let* x = smt_cval x in + let top = Extract (n - 1, Big_int.to_int i + 1, vec) in + return (Fn ("concat", [top; x])) + | CT_fbits n, CT_constant i, CT_constant j, CT_fbits sz, CT_fbits m + when n - 1 = Big_int.to_int i && Big_int.to_int j = 0 -> + smt_cval x + | CT_fbits n, ctyp_i, ctyp_j, ctyp_x, CT_fbits m -> + assert (n = m); + let* vec = smt_cval vec in + let* i' = bind (smt_cval i) (signed_size ~into:n ~from:(int_size ctyp_i)) in + let* j' = bind (smt_cval j) (signed_size ~into:n ~from:(int_size ctyp_j)) in + let* x' = bind (smt_cval x) (smt_conversion ~into:(CT_fbits n) ~from:ctyp_x) in + let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in + let mask = bvshl (fbits_mask n len) j' in + return (bvor (bvand vec (bvnot mask)) (bvand (bvshl x' j') mask)) + | bv_ctyp, ctyp_i, ctyp_j, ctyp_x, CT_lbits -> + let* sz, bv = fmap (to_fbits bv_ctyp) (smt_cval vec) in + let* i = bind (smt_cval i) (signed_size ~into:sz ~from:(int_size ctyp_i)) in + let* j = bind (smt_cval j) (signed_size ~into:sz ~from:(int_size ctyp_j)) in + let* x = bind (smt_cval x) (smt_conversion ~into:(CT_fbits sz) ~from:ctyp_x) in + let len = bvadd (bvadd i (bvneg j)) (bvpint sz (Big_int.of_int 1)) in + let mask = bvshl (fbits_mask sz len) j in + let contents = bvor (bvand bv (bvnot mask)) (bvand (bvshl x j) mask) in + let* index = signed_size ~into:lbits_index ~from:sz len in + return (Fn ("Bits", [index; contents])) + | _ -> builtin_type_error "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp) + + let builtin_get_slice_int v1 v2 v3 ret_ctyp = + match (cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, ret_ctyp) with + | CT_constant len, ctyp, CT_constant start, CT_fbits ret_sz -> + let len = Big_int.to_int len in + let start = Big_int.to_int start in + let in_sz = int_size ctyp in + let* smt = + if in_sz < len + start then bind (smt_cval v2) (signed_size ~into:(len + start) ~from:in_sz) else smt_cval v2 + in + return (Extract (start + len - 1, start, smt)) + | CT_lint, CT_lint, CT_constant start, CT_lbits when Big_int.equal start Big_int.zero -> + let* v1 = smt_cval v1 in + let len = Extract (lbits_index - 1, 0, v1) in + let* contents = bind (smt_cval v2) (unsigned_size ~into:lbits_size ~from:lint_size) in + return (Fn ("Bits", [len; bvand (bvmask len) contents])) + | ctyp1, ctyp2, ctyp3, ret_ctyp -> + let* smt1 = smt_cval v1 in + let* len = signed_size ~into:lbits_index ~from:(int_size ctyp1) smt1 in + let* smt2 = bind (smt_cval v2) (signed_size ~into:lbits_size ~from:(int_size ctyp2)) in + let* smt3 = bind (smt_cval v3) (signed_size ~into:lbits_size ~from:(int_size ctyp3)) in + let result = Fn ("Bits", [len; bvand (bvmask len) (bvlshr smt2 smt3)]) in + smt_conversion ~into:ret_ctyp ~from:CT_lbits result + + let builtin_pow2 v ret_ctyp = + match (cval_ctyp v, ret_ctyp) with + | CT_constant n, _ when Big_int.greater_equal n Big_int.zero -> + return (bvint (int_size ret_ctyp) (Big_int.pow_int_positive 2 (Big_int.to_int n))) + | CT_lint, CT_lint -> + let* v = smt_cval v in + (* TODO: Check we haven't shifted too far *) + return (bvshl (bvone lint_size) v) + | _ -> builtin_type_error "pow2" [v] (Some ret_ctyp) + + (* Technically, there's no bvclz in SMTLIB, but we can't generate + anything nice, so leave it in case a backend like SystemVerilog + can do better *) + let builtin_count_leading_zeros v ret_ctyp = + let* l = current_location in + match cval_ctyp v with + | CT_fbits sz -> + let bvclz = Primop_gen.count_leading_zeros l sz in + let* bv = smt_cval v in + unsigned_size ~max_value:sz ~into:(int_size ret_ctyp) ~from:sz (Fn (bvclz, [bv])) + | CT_lbits -> + let bvclz = Primop_gen.count_leading_zeros l lbits_size in + let* bv = smt_cval v in + let contents_clz = Fn (bvclz, [Fn ("contents", [bv])]) in + let* len = unsigned_size ~into:lbits_size ~from:lbits_index (Fn ("len", [bv])) in + let lz = bvsub contents_clz (bvsub (bvpint lbits_size (Big_int.of_int lbits_size)) len) in + unsigned_size ~max_value:lbits_size ~into:(int_size ret_ctyp) ~from:lbits_size lz + | _ -> builtin_type_error "count_leading_zeros" [v] (Some ret_ctyp) + + let arity_error = + let* l = current_location in + raise (Reporting.unreachable l __POS__ "Trying to generate primitive with incorrect number of arguments") + + let unary_primop f = Some (fun args ret_ctyp -> match args with [v] -> f v ret_ctyp | _ -> arity_error) + + let unary_primop_simple f = Some (fun args _ -> match args with [v] -> f v | _ -> arity_error) + + let binary_primop f = Some (fun args ret_ctyp -> match args with [v1; v2] -> f v1 v2 ret_ctyp | _ -> arity_error) + + let binary_primop_simple f = Some (fun args _ -> match args with [v1; v2] -> f v1 v2 | _ -> arity_error) + + let ternary_primop f = + Some (fun args ret_ctyp -> match args with [v1; v2; v3] -> f v1 v2 v3 ret_ctyp | _ -> arity_error) + + let builtin = function + | "eq_bit" -> + binary_primop_simple (fun v1 v2 -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn ("=", [smt1; smt2])) + ) + | "eq_bool" -> + binary_primop_simple (fun v1 v2 -> + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn ("=", [smt1; smt2])) + ) + | "eq_int" -> binary_primop_simple builtin_eq_int + | "not" -> + unary_primop_simple (fun v -> + let* v = smt_cval v in + return (Fn ("not", [v])) + ) + | "lt" -> binary_primop_simple builtin_lt + | "lteq" -> binary_primop_simple builtin_lteq + | "gt" -> binary_primop_simple builtin_gt + | "gteq" -> binary_primop_simple builtin_gteq + | "add_int" -> binary_primop builtin_add_int + | "sub_int" -> binary_primop builtin_sub_int + | "mult_int" -> binary_primop builtin_mult_int + | "neg_int" -> unary_primop builtin_neg_int + | "abs_int" -> unary_primop builtin_abs_int + | "max_int" -> binary_primop builtin_max_int + | "min_int" -> binary_primop builtin_min_int + | "pow2" -> unary_primop builtin_pow2 + | "zeros" -> unary_primop builtin_zeros + | "ones" -> unary_primop builtin_ones + | "zero_extend" -> binary_primop builtin_zero_extend + | "sign_extend" -> binary_primop builtin_sign_extend + | "sail_signed" -> unary_primop builtin_signed + | "sail_unsigned" -> unary_primop builtin_unsigned + | "slice" -> ternary_primop builtin_slice + | "add_bits" -> binary_primop (builtin_arith_bits "bvadd") + | "add_bits_int" -> binary_primop (builtin_arith_bits_int "bvadd") + | "sub_bits" -> binary_primop (builtin_arith_bits "bvsub") + | "sub_bits_int" -> binary_primop (builtin_arith_bits_int "bvsub") + | "append" -> binary_primop builtin_append + | "get_slice_int" -> ternary_primop builtin_get_slice_int + | "eq_bits" -> binary_primop_simple builtin_eq_bits + | "neq_bits" -> binary_primop_simple builtin_neq_bits + | "not_bits" -> unary_primop builtin_not_bits + | "sail_truncate" -> binary_primop builtin_sail_truncate + | "sail_truncateLSB" -> binary_primop builtin_sail_truncateLSB + | "shiftl" -> binary_primop (builtin_shift "bvshl") + | "shiftr" -> binary_primop (builtin_shift "bvlshr") + | "arith_shiftr" -> binary_primop (builtin_shift "bvashr") + | "and_bits" -> binary_primop (builtin_bitwise "bvand") + | "or_bits" -> binary_primop (builtin_bitwise "bvor") + | "xor_bits" -> binary_primop (builtin_bitwise "bvxor") + | "vector_access" -> binary_primop builtin_vector_access + | "vector_subrange" -> ternary_primop builtin_vector_subrange + | "vector_update" -> ternary_primop builtin_vector_update + | "vector_update_subrange" -> + Some + (fun args ret_ctyp -> + match args with [v1; v2; v3; v4] -> builtin_vector_update_subrange v1 v2 v3 v4 ret_ctyp | _ -> arity_error + ) + | "length" -> unary_primop builtin_length + | "replicate_bits" -> binary_primop builtin_replicate_bits + | "count_leading_zeros" -> unary_primop builtin_count_leading_zeros + | "print_bits" -> + binary_primop_simple (fun str bv -> + let* l = current_location in + let op = Primop_gen.print_bits l (cval_ctyp bv) in + let* str = smt_cval str in + let* bv = smt_cval bv in + return (Fn (op, [str; bv])) + ) + | "string_of_bits" -> + unary_primop_simple (fun bv -> + let* l = current_location in + let op = Primop_gen.string_of_bits l (cval_ctyp bv) in + let* bv = smt_cval bv in + return (Fn (op, [bv])) + ) + | "dec_str" -> + unary_primop_simple (fun bv -> + let* l = current_location in + let op = Primop_gen.dec_str l (cval_ctyp bv) in + let* bv = smt_cval bv in + return (Fn (op, [bv])) + ) + | "hex_str" -> + unary_primop_simple (fun bv -> + let* l = current_location in + let op = Primop_gen.hex_str l (cval_ctyp bv) in + let* bv = smt_cval bv in + return (Fn (op, [bv])) + ) + | "hex_str_upper" -> + unary_primop_simple (fun bv -> + let* l = current_location in + let op = Primop_gen.hex_str_upper l (cval_ctyp bv) in + let* bv = smt_cval bv in + return (Fn (op, [bv])) + ) + | "sail_assert" -> + binary_primop_simple (fun b msg -> + let* b = smt_cval b in + let* msg = smt_cval msg in + return (Fn ("sail_assert", [b; msg])) + ) + | "reg_deref" -> + unary_primop_simple (fun reg_ref -> + match cval_ctyp reg_ref with + | CT_ref ctyp -> + let* reg_ref = smt_cval reg_ref in + let op = "sail_reg_deref_" ^ Util.zencode_string (string_of_ctyp ctyp) in + return (Fn (op, [reg_ref])) + | _ -> + let* l = current_location in + Reporting.unreachable l __POS__ "reg_deref given non register reference" + ) + | "sail_cons" -> + binary_primop_simple (fun x xs -> + let* x = smt_cval x in + let* xs = smt_cval xs in + return (Fn ("cons", [x; xs])) + ) + | "eq_anything" -> + binary_primop_simple (fun a b -> + let* a = smt_cval a in + let* b = smt_cval b in + return (Fn ("=", [a; b])) + ) + | _ -> None +end diff --git a/src/lib/smt_gen.mli b/src/lib/smt_gen.mli new file mode 100644 index 000000000..daaf846f0 --- /dev/null +++ b/src/lib/smt_gen.mli @@ -0,0 +1,176 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2023 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +(** Compile Sail builtins to SMT bitvector expressions *) + +open Ast_util +open Jib + +(** The main limitiation when converting Sail into pure SMT bitvectors + is that Sail has arbitrary precision types, as well as types like + real and string that are not very SMT friendly. We can add dynamic + assertions that effectivly check at runtime that we never exceed + some upper bound on bitvector size, and log if we ever use + features like strings or real numbers. *) +type checks + +(** We generate primitives in a monad that accumulates any required + dynamic checks, and contains the location information for any + error messages. *) +type 'a check_writer + +(** The SMT generation monad contains the location of the expression + or definition we are generating SMT for *) +val current_location : Parse_ast.l check_writer + +val return : 'a -> 'a check_writer + +val bind : 'a check_writer -> ('a -> 'b check_writer) -> 'b check_writer + +val fmap : ('a -> 'b) -> 'a check_writer -> 'b check_writer + +val ( let* ) : 'a check_writer -> ('a -> 'b check_writer) -> 'b check_writer + +val ( let+ ) : 'a check_writer -> ('a -> 'b) -> 'b check_writer + +val mapM : ('a -> 'b check_writer) -> 'a list -> 'b list check_writer + +val run : 'a check_writer -> Parse_ast.l -> 'a * checks + +(** Convert a SMT bitvector expression of size [from] into a SMT + bitvector expression of size [into] with the same signed + value. When [into < from] inserts a dynamic check that the + original value is representable at the new length. *) +val signed_size : ?checked:bool -> into:int -> from:int -> Smt_exp.smt_exp -> Smt_exp.smt_exp check_writer + +(** Similar to [signed_size], except it assumes the bitvector is + representing an unsigned value. *) +val unsigned_size : + ?max_value:int -> ?checked:bool -> into:int -> from:int -> Smt_exp.smt_exp -> Smt_exp.smt_exp check_writer + +(** [bvint sz n] Create a (two's complement) SMT bitvector + representing a the number [n] in a bitvector of length + [sz]. Raises an error if this is not possible. *) +val bvint : int -> Big_int.num -> Smt_exp.smt_exp + +module type CONFIG = sig + (** Sail has arbitrary precision integers, but in order to generate + pure bitvectors we must constrain them to some upper bound. As + described above, we can insert dynamic checks to ensure this + constraint is never violated at runtime. *) + val max_unknown_integer_width : int + + (** If we have a Sail type [bits('n)], where ['n] is unconstrained, + then we cannot know how many bits to use to represent + it. Instead we use a bitvector of this length, plus a width + field. We will generate runtime checks to ensure this length is + sufficient. *) + val max_unknown_bitvector_width : int + + (** Some SystemVerilog implementations (e.g. Verilator), don't + support unpacked union types, which forces us to generate + different code for different unions depending on the types the + contain. This is abstracted into a classify function that the + instantiator of this module can supply. *) + val union_ctyp_classify : ctyp -> bool +end + +(** Some Sail primitives we can't directly convert to pure SMT + bitvectors, either because they don't exist in SMTLIB (like + count_leading_zeros), or they involve input/output. In these cases + we provide a module so the backend can generate the required + implementations for these primitives. *) +module type PRIMOP_GEN = sig + val print_bits : Parse_ast.l -> ctyp -> string + val string_of_bits : Parse_ast.l -> ctyp -> string + val dec_str : Parse_ast.l -> ctyp -> string + val hex_str : Parse_ast.l -> ctyp -> string + val hex_str_upper : Parse_ast.l -> ctyp -> string + val count_leading_zeros : Parse_ast.l -> int -> string + val fvector_store : Parse_ast.l -> int -> ctyp -> string + val is_empty : Parse_ast.l -> ctyp -> string + val hd : Parse_ast.l -> ctyp -> string + val tl : Parse_ast.l -> ctyp -> string +end + +module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) : sig + (** Convert a Jib IR cval into an SMT expression *) + val smt_cval : cval -> Smt_exp.smt_exp check_writer + + val int_size : ctyp -> int + + (** Create an SMT expression that converts an expression of the jib + type [from] into an SMT expression for the jib type [into]. Note + that this function assumes that the input is of the correct + type. *) + val smt_conversion : into:ctyp -> from:ctyp -> Smt_exp.smt_exp -> Smt_exp.smt_exp check_writer + + (** Compile a call to a Sail builtin function into an SMT expression + implementing that call. Returns None if that builtin is + unsupported by this module. *) + val builtin : string -> (cval list -> ctyp -> Smt_exp.smt_exp check_writer) option +end diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index c6fb7d2fc..6f9ee93b9 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1220,10 +1220,9 @@ end = struct end let get_union_id id env = - try - let bind = Bindings.find id env.union_ids in - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - with Not_found -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id) + match Bindings.find_opt id env.union_ids with + | Some bind -> List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + | None -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id) let rec valid_implicits env start = function | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var _, _)), _)]), l) :: rest -> diff --git a/src/lib/value2.lem b/src/lib/value2.lem index 8c17b1953..723603791 100644 --- a/src/lib/value2.lem +++ b/src/lib/value2.lem @@ -77,7 +77,6 @@ type vl = | VL_int of integer | VL_string of string | VL_real of string - | VL_empty_list | VL_enum of string | VL_ref of string | VL_undefined diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 9f45057a3..e7faf815b 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -186,7 +186,7 @@ let literal_to_fragment (L_aux (l_aux, _)) = module C_config (Opts : sig val branch_coverage : out_channel option -end) : Config = struct +end) : CONFIG = struct (** Convert a sail type into a C-type. This function can be quite slow, because it uses ctx.local_env and SMT to analyse the Sail types and attempts to fit them into the smallest possible C @@ -513,7 +513,7 @@ end) : Config = struct let optimize_anf ctx aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) let unroll_loops = None - let specialize_calls = false + let make_call_precise _ _ = true let ignore_64 = false let struct_value = false let tuple_value = false @@ -898,7 +898,6 @@ let sgen_value = function | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" | VL_real str -> str | VL_string str -> "\"" ^ str ^ "\"" - | VL_empty_list -> "NULL" | VL_enum element -> Util.zencode_string element | VL_ref r -> "&" ^ Util.zencode_string r | VL_undefined -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal" @@ -924,6 +923,7 @@ and sgen_call op cvals = | Bor, vs -> "(" ^ Util.string_of_list " || " sgen_cval vs ^ ")" | List_hd, [v] -> sprintf "(%s).hd" ("*" ^ sgen_cval v) | List_tl, [v] -> sprintf "(%s).tl" ("*" ^ sgen_cval v) + | List_is_empty, [v] -> sprintf "(%s == NULL)" (sgen_cval v) | Eq, [v1; v2] -> begin match cval_ctyp v1 with | CT_sbits _ -> sprintf "eq_sbits(%s, %s)" (sgen_cval v1) (sgen_cval v2) @@ -1083,7 +1083,8 @@ let rec codegen_conversion l clexp cval = if is_stack_ctyp ctyp_to then ksprintf string " %s = %s;" (sgen_clexp_pure l clexp) (sgen_cval cval) else ksprintf string " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp l clexp) (sgen_cval cval) | CT_ref _, _ -> codegen_conversion l (CL_addr clexp) cval - | CT_vector ctyp_elem_to, CT_vector ctyp_elem_from -> + | (CT_vector ctyp_elem_to | CT_fvector (_, ctyp_elem_to)), (CT_vector ctyp_elem_from | CT_fvector (_, ctyp_elem_from)) + -> let i = ngensym () in let from = ngensym () in let into = ngensym () in diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index b2fc83970..e1acf3997 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -209,7 +209,7 @@ let rec smt_ctyp ctx = function | CT_tup ctyps -> ctx.tuple_sizes := IntSet.add (List.length ctyps) !(ctx.tuple_sizes); Tuple (List.map (smt_ctyp ctx) ctyps) - | CT_vector ctyp -> Array (Bitvec !vector_index, smt_ctyp ctx ctyp) + | CT_vector ctyp | CT_fvector (_, ctyp) -> Array (Bitvec !vector_index, smt_ctyp ctx ctyp) | CT_string -> ctx.use_string := true; String @@ -223,7 +223,6 @@ let rec smt_ctyp ctx = function end | CT_list _ -> raise (Reporting.err_todo ctx.pragma_l "Lists not yet supported in SMT generation") | CT_float _ | CT_rounding_mode -> Reporting.unreachable ctx.pragma_l __POS__ "Floating point in SMT property" - | CT_fvector _ -> Reporting.unreachable ctx.pragma_l __POS__ "Found CT_fvector in SMT property" | CT_poly _ -> Reporting.unreachable ctx.pragma_l __POS__ "Found polymorphic type in SMT property" (* We often need to create a SMT bitvector of a length sz with integer @@ -311,6 +310,8 @@ let smt_conversion ctx from_ctyp to_ctyp x = | CT_fbits n, CT_fbits m -> unsigned_size ctx m n x | CT_fbits n, CT_lbits -> Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x]) + | CT_fvector _, CT_vector _ -> x + | CT_vector _, CT_fvector _ -> x | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp)) @@ -577,8 +578,8 @@ let builtin_eq_bits ctx v1 v2 = | CT_lbits, CT_lbits -> let len1 = Fn ("len", [smt_cval ctx v1]) in let contents1 = Fn ("contents", [smt_cval ctx v1]) in - let len2 = Fn ("len", [smt_cval ctx v1]) in - let contents2 = Fn ("contents", [smt_cval ctx v1]) in + let len2 = Fn ("len", [smt_cval ctx v2]) in + let contents2 = Fn ("contents", [smt_cval ctx v2]) in Fn ( "and", [ @@ -1368,7 +1369,7 @@ let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) module SMT_config (Opts : sig val unroll_limit : int -end) : Jib_compile.Config = struct +end) : Jib_compile.CONFIG = struct open Jib_compile (** Convert a sail type into a C-type. This function can be quite @@ -1546,7 +1547,7 @@ end) : Jib_compile.Config = struct let optimize_anf ctx aexp = aexp |> c_literals ctx |> fold_aexp (unroll_static_foreach ctx) - let specialize_calls = true + let make_call_precise _ _ = false let ignore_64 = true let unroll_loops = Some Opts.unroll_limit let struct_value = true diff --git a/src/sail_sv_backend/dune b/src/sail_sv_backend/dune new file mode 100644 index 000000000..c36d0d53e --- /dev/null +++ b/src/sail_sv_backend/dune @@ -0,0 +1,20 @@ +(env + (dev + (flags + (:standard -w -33 -w -27 -w -32 -w -26 -w -37))) + (release + (flags + (:standard -w -33 -w -27 -w -32 -w -26 -w -37)))) + +(executable + (name sail_plugin_sv) + (modes + (native plugin)) + (libraries libsail)) + +(install + (section + (site + (libsail plugins))) + (package sail_sv_backend) + (files sail_plugin_sv.cmxs)) diff --git a/src/sail_sv_backend/generate_primop.ml b/src/sail_sv_backend/generate_primop.ml new file mode 100644 index 000000000..cc68755fb --- /dev/null +++ b/src/sail_sv_backend/generate_primop.ml @@ -0,0 +1,505 @@ +(**************************************************************************) +(* Sail to verilog *) +(* *) +(* Copyright (c) 2023 *) +(* Alasdair Armstrong *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +module Big_int = Nat_big_num + +module StringSet = Set.Make (String) + +open Printf + +let required_width n = + let rec required_width' n = + if Big_int.equal n Big_int.zero then 1 else 1 + required_width' (Big_int.shift_right n 1) + in + required_width' (Big_int.abs n) + +let nf s = s +let pf fmt = sprintf fmt + +let generated_primops = ref (StringSet.empty, []) + +let register_primop name def = + let names, _ = !generated_primops in + if StringSet.mem name names then name + else ( + let source = def () in + let names, defs = !generated_primops in + generated_primops := (StringSet.add name names, source :: defs); + name + ) + +let get_generated_primops () = List.rev (snd !generated_primops) + +let sail_bits width = + let index_top = required_width (Big_int.of_int (width - 1)) - 1 in + [ + nf "typedef struct packed {"; + pf " logic [%d:0] size;" index_top; + pf " logic [%d:0] bits;" (width - 1); + nf "} sail_bits;"; + ""; + pf "localparam SAIL_BITS_WIDTH = %d;" width; + pf "localparam SAIL_INDEX_WIDTH = %d;" (index_top + 1); + ""; + pf "function automatic logic [%d:0] sail_bits_size(sail_bits bv); return bv.size; endfunction" index_top; + pf "function automatic logic [%d:0] sail_bits_value(sail_bits bv); return bv.bits; endfunction" (width - 1); + ] + +let sail_int width = [pf "typedef logic [%d:0] sail_int;" (width - 1)] + +let print_lbits width = + let zeros = String.make (width / 4) '0' in + let header = + [ + nf "function automatic sail_unit sail_print_bits(string prefix, sail_bits bv);"; + nf " string bstr;"; + nf " string zeros;"; + pf " zeros = \"%s\";" zeros; + ] + in + let body = + List.init (width - 1) (fun n -> + if (n + 1) mod 4 == 0 then + [ + pf " if (bv.size == %d) begin" (n + 1); + nf " bstr.hextoa(bv.bits);"; + pf " $display(\"%%s0x%%s%%s\", prefix, zeros.substr(0, %d - bstr.len()), bstr.toupper());" + (((n + 1) / 4) - 1); + nf " end"; + ] + else + [ + pf " if (bv.size == %d) begin" (n + 1); + pf " $display(\"%%s0b%%b\", prefix, bv.bits[%d:0]);" n; + nf " end"; + ] + ) + |> List.concat + in + let footer = "endfunction" in + header @ body @ [footer] + +let string_of_bits width = + let zeros = String.make (width - 1) '0' in + let header = + [ + nf "function automatic string sail_string_of_bits(sail_bits bv);"; + nf " string bstr;"; + nf " string zeros;"; + pf " zeros = \"%s\";" zeros; + ] + in + let body = + List.init (width - 1) (fun n -> + if (n + 1) mod 4 == 0 then + [ + pf " if (bv.size == %d) begin" (n + 1); + nf " bstr.hextoa(bv.bits);"; + pf " return {\"0x\", zeros.substr(0, %d - bstr.len()), bstr.toupper()};" (((n + 1) / 4) - 1); + nf " end"; + ] + else + [ + pf " if (bv.size == %d) begin" (n + 1); + nf " bstr.bintoa(bv.bits);"; + pf " return {\"0b\", zeros.substr(0, %d - bstr.len()), bstr};" n; + nf " end"; + ] + ) + |> List.concat + in + let footer = "endfunction" in + header @ body @ [footer] + +let print_lbits_stub width = + [ + nf "function automatic sail_unit sail_print_bits(sail_unit prefix, sail_bits bv);"; + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + +let string_of_bits_stub width = + [nf "function automatic sail_unit sail_string_of_bits(sail_bits bv);"; nf " return SAIL_UNIT;"; nf "endfunction"] + +let dec_str width = + [ + pf "function automatic string sail_dec_str(logic [%d:0] i);" (width - 1); + nf " string s;"; + nf " s.itoa(i);"; + nf " return s;"; + nf "endfunction"; + ] + +let dec_str_stub width = + [ + pf "function automatic sail_unit sail_dec_str(logic [%d:0] i);" (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + +let hex_str width = + [ + pf "function automatic string sail_hex_str(logic [%d:0] i);" (width - 1); + nf " string s;"; + nf " s.hextoa(i);"; + nf " return {\"0x\", s};"; + nf "endfunction"; + ] + +let hex_str_stub width = + [ + pf "function automatic sail_unit sail_hex_str(logic [%d:0] i);" (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + +let hex_str_upper width = + [ + pf "function automatic string sail_hex_str_upper(logic [%d:0] i);" (width - 1); + nf " string s;"; + nf " s.hextoa(i);"; + nf " return {\"0x\", s.toupper()};"; + nf "endfunction"; + ] + +let hex_str_upper_stub width = + [ + pf "function automatic sail_unit sail_hex_str_upper(logic [%d:0] i);" (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + +let print_int width = + [ + pf "function automatic sail_unit sail_print_int(string prefix, logic [%d:0] i);" (width - 1); + nf " $display(\"%s%0d\", prefix, signed'(i));"; + nf "endfunction"; + ] + +let print_int_stub width = + [ + pf "function automatic sail_unit sail_print_int(sail_unit prefix, logic [%d:0] i);" (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + +let get_cycle_count width = + [ + pf "function automatic logic [%d:0] sail_get_cycle_count(sail_unit u);" (width - 1); + nf " return sail_cycle_count_var;"; + nf "endfunction"; + ] + +let cycle_count () = + [ + "function automatic sail_unit sail_cycle_count(sail_unit u);"; + " sail_cycle_count_var = sail_cycle_count_var + 1;"; + " return SAIL_UNIT;"; + "endfunction"; + ] + +let output_primop buf lines = + List.iter + (fun line -> + Buffer.add_string buf line; + Buffer.add_char buf '\n' + ) + lines; + Buffer.add_char buf '\n' + +let common_primops bv_width int_width = + let buf = Buffer.create 4096 in + output_primop buf (sail_bits bv_width); + output_primop buf (sail_int int_width); + output_primop buf (print_lbits bv_width); + output_primop buf (string_of_bits bv_width); + output_primop buf (print_int int_width); + output_primop buf (dec_str int_width); + output_primop buf (hex_str int_width); + output_primop buf (hex_str_upper int_width); + Buffer.add_string buf (pf "logic [%d:0] sail_cycle_count_var;\n\n" (int_width - 1)); + output_primop buf (get_cycle_count int_width); + output_primop buf (cycle_count ()); + Buffer.contents buf + +let common_primops_stubs bv_width int_width = + let buf = Buffer.create 4096 in + output_primop buf (sail_bits bv_width); + output_primop buf (sail_int int_width); + output_primop buf (print_lbits_stub bv_width); + output_primop buf (string_of_bits_stub bv_width); + output_primop buf (print_int_stub int_width); + output_primop buf (dec_str_stub int_width); + output_primop buf (hex_str_stub int_width); + output_primop buf (hex_str_upper_stub int_width); + Buffer.add_string buf (pf "logic [%d:0] sail_cycle_count_var;\n\n" (int_width - 1)); + output_primop buf (get_cycle_count int_width); + output_primop buf (cycle_count ()); + Buffer.contents buf + +let print_fbits width = + let name = pf "sail_print_fixed_bits_%d" width in + register_primop name (fun () -> + let display = + if width mod 4 = 0 then ( + let zeros = String.make (width / 4) '0' in + [ + nf " string bstr;"; + nf " string zeros;"; + nf " bstr.hextoa(b);"; + pf " zeros = \"%s\";" zeros; + pf " $display(\"%%s0x%%s\", s, zeros.substr(0, %d - bstr.len()), bstr.toupper());" ((width / 4) - 1); + ] + ) + else [" $display(\"%s0b%b\", s, b);"] + in + [pf "function automatic sail_unit %s(string s, logic [%d:0] b);" name (width - 1)] + @ display + @ [" return SAIL_UNIT;"; "endfunction"] + ) + +let string_of_fbits width = + let name = pf "sail_string_of_bits_%d" width in + register_primop name (fun () -> + let header = [" string bstr;"; " string zeros;"] in + let display = + if width mod 4 = 0 then ( + let zeros = String.make (width / 4) '0' in + [ + nf " bstr.hextoa(b);"; + pf " zeros = \"%s\";" zeros; + pf " return {\"0x\", zeros.substr(0, %d - bstr.len()), bstr.toupper()};" ((width / 4) - 1); + ] + ) + else ( + let zeros = String.make (width - 1) '0' in + [ + nf " bstr.bintoa(b);"; + pf " zeros = \"%s\";" zeros; + pf " return {\"0b\", zeros.substr(0, %d - bstr.len()), bstr};" (width - 1); + ] + ) + in + [pf "function automatic string %s(logic [%d:0] b);" name (width - 1)] @ header @ display @ ["endfunction"] + ) + +let print_fbits_stub width = + let name = pf "sail_print_fixed_bits_%d" width in + register_primop name (fun () -> + [ + pf "function automatic sail_unit %s(sail_unit prefix, logic [%d:0] bv);" name (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + ) + +let string_of_fbits_stub width = + let name = pf "sail_string_of_bits_%d" width in + register_primop name (fun () -> + [ + pf "function automatic sail_unit %s(logic [%d:0] bv);" name (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + ) + +let dec_str_fint width = + let name = pf "sail_dec_str_%d" width in + register_primop name (fun () -> + [ + pf "function automatic string %s(logic [%d:0] i);" name (width - 1); + nf " string s;"; + nf " s.itoa(i);"; + nf " return s;"; + nf "endfunction"; + ] + ) + +let dec_str_fint_stub width = + let name = pf "sail_dec_str_%d" width in + register_primop name (fun () -> + [ + pf "function automatic sail_unit %s(logic [%d:0] i);" name (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + ) + +let hex_str_fint width = + let name = pf "sail_hex_str_%d" width in + register_primop name (fun () -> + [ + pf "function automatic string %s(logic [%d:0] i);" name (width - 1); + nf " string s;"; + nf " s.hextoa(i);"; + nf " return {\"0x\", s};"; + nf "endfunction"; + ] + ) + +let hex_str_fint_stub width = + let name = pf "sail_hex_str_%d" width in + register_primop name (fun () -> + [ + pf "function automatic sail_unit %s(logic [%d:0] i);" name (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + ) + +let hex_str_upper_fint width = + let name = pf "sail_hex_str_upper_%d" width in + register_primop name (fun () -> + [ + pf "function automatic string %s(logic [%d:0] i);" name (width - 1); + nf " string s;"; + nf " s.hextoa(i);"; + nf " return {\"0x\", s.toupper()};"; + nf "endfunction"; + ] + ) + +let hex_str_upper_fint_stub width = + let name = pf "sail_hex_str_upper_%d" width in + register_primop name (fun () -> + [ + pf "function automatic sail_unit %s(logic [%d:0] i);" name (width - 1); + nf " return SAIL_UNIT;"; + nf "endfunction"; + ] + ) + +let rec count_leading_zeros width = + let name = pf "sail_clz_%d" width in + register_primop name (fun () -> + if width == 1 then + [ + pf "function automatic logic [%d:0] %s(logic [%d:0] bv);" (width - 1) name (width - 1); + nf " return ~bv[0];"; + nf "endfunction"; + ] + else ( + let lower_width = width / 2 in + let upper_width = lower_width + (width mod 2) in + let upper = pf "bv[%d:%d]" (width - 1) (width - upper_width) in + let lower = pf "bv[%d:0]" (lower_width - 1) in + let clz_upper = count_leading_zeros upper_width in + let clz_lower = count_leading_zeros lower_width in + [ + pf "function automatic logic [%d:0] %s(logic [%d:0] bv);" (width - 1) name (width - 1); + pf " if (%s == 0) begin" upper; + pf " return %d'd%d + %d'(%s(%s));" width upper_width width clz_lower lower; + nf " end else begin"; + pf " return %d'(%s(%s));" width clz_upper upper; + nf " end;"; + nf "endfunction"; + ] + ) + ) + +let popcount width = + (* Cound maybe use $countones? *) + let name = pf "sail_popcount_%d" width in + register_primop name (fun () -> + let bits = List.init (width - 1) (fun n -> pf "%d'(bv[%d])" width (n + 1)) in + let sum = List.fold_left (fun sum bit -> pf "%s + %s" sum bit) (pf "%d'(bv[0])" width) bits in + [ + pf "function automatic logic [%d:0] %s(logic [%d:0] bv);" (width - 1) name (width - 1); + pf " return %s;" sum; + nf "endfunction"; + ] + ) + +let wrap_type (ty, ix_opt) str = match ix_opt with None -> ty ^ " " ^ str | Some ix -> ty ^ " " ^ str ^ " " ^ ix + +let array_type (ty, ix_opt) ix = match ix_opt with None -> (ty, Some ix) | Some inner_ix -> (ty, Some (inner_ix ^ ix)) + +let fvector_store len elem_ty key = + let name = pf "sail_array_store_%d_%s" len key in + register_primop name (fun () -> + let ret_ty_name = pf "ret_array_store_%d_%s" len key in + let outer_ix = pf "[%d:0]" (len - 1) in + let ix_ty = pf "logic [%d:0]" (required_width (Big_int.of_int (len - 1)) - 2) in + [ + pf "typedef %s%s;" (wrap_type elem_ty ret_ty_name) outer_ix; + ""; + pf "function automatic %s %s(%s, %s i, %s);" ret_ty_name name + (wrap_type (array_type elem_ty outer_ix) "arr") + ix_ty (wrap_type elem_ty "x"); + pf " %s r;" ret_ty_name; + nf " r = arr;"; + nf " r[i] = x;"; + nf " return r;"; + nf "endfunction"; + ] + ) + +let is_empty elem_ty key = + let name = pf "sail_is_empty_%s" key in + register_primop name (fun () -> + [ + pf "function automatic bit %s(%s[$]);" name (wrap_type elem_ty "xs"); + nf " return xs.size() == 0;"; + nf "endfunction"; + ] + ) + +let hd elem_ty key = + let name = pf "sail_hd_%s" key in + register_primop name (fun () -> + let ret_ty_name = pf "ret_hd_%s" key in + [ + pf "typedef %s;" (wrap_type elem_ty ret_ty_name); + ""; + pf "function automatic %s %s(%s[$]);" ret_ty_name name (wrap_type elem_ty "xs"); + pf " %s;" (wrap_type elem_ty "r"); + nf " r = xs[0];"; + nf " return r;"; + nf "endfunction"; + ] + ) + +let tl elem_ty key = + let name = pf "sail_tl_%s" key in + register_primop name (fun () -> + let ret_ty_name = pf "ret_tl_%s" key in + [ + pf "typedef %s[$];" (wrap_type elem_ty ret_ty_name); + ""; + pf "function automatic %s %s(%s[$]);" ret_ty_name name (wrap_type elem_ty "xs"); + pf " %s r;" ret_ty_name; + nf " r = xs;"; + nf " r.pop_front();"; + nf " return r;"; + nf "endfunction"; + ] + ) diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml new file mode 100644 index 000000000..bc438142d --- /dev/null +++ b/src/sail_sv_backend/jib_sv.ml @@ -0,0 +1,909 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* Louis-Emile Ploix *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Libsail + +open Ast_util +open Jib +open Jib_compile +open Jib_util +open PPrint +open Printf +open Smt_exp + +open Generate_primop + +module type CONFIG = sig + val max_unknown_integer_width : int + val max_unknown_bitvector_width : int + val line_directives : bool + val nostrings : bool + val nopacked : bool + val unreachable : string list + val comb : bool + val ignore : string list +end + +module Make (Config : CONFIG) = struct + let lbits_index_width = required_width (Big_int.of_int (Config.max_unknown_bitvector_width - 1)) + + let valid_sv_identifier_regexp : Str.regexp option ref = ref None + + let has_prefix prefix s = + if String.length s < String.length prefix then false else String.sub s 0 (String.length prefix) = prefix + + let has_bad_prefix s = has_prefix "sail_" s || has_prefix "t_" s || has_prefix "ret_" s + + let valid_sv_identifier s = + let regexp = + (* Cache the regexp to avoid compiling it every time *) + match !valid_sv_identifier_regexp with + | Some regexp -> regexp + | None -> + let regexp = Str.regexp "^[A-Za-z_][A-Za-z0-9_]*$" in + valid_sv_identifier_regexp := Some regexp; + regexp + in + Str.string_match regexp s 0 + + let sv_id_string id = + let s = string_of_id id in + if valid_sv_identifier s && (not (has_bad_prefix s)) && not (StringSet.mem s Keywords.sv_reserved_words) then s + else Util.zencode_string s + + let sv_id id = string (sv_id_string id) + + let sv_type_id_string id = "t_" ^ sv_id_string id + + let sv_type_id id = string (sv_type_id_string id) + + let rec is_packed = function + | CT_fbits _ | CT_unit | CT_bit | CT_bool | CT_fint _ | CT_lbits | CT_lint | CT_enum _ | CT_constant _ -> + not Config.nopacked + | CT_variant (_, ctors) -> List.for_all (fun (_, ctyp) -> is_packed ctyp) ctors + | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_packed ctyp) fields + | _ -> false + + let simple_type str = (str, None) + + let rec sv_ctyp = function + | CT_bool -> simple_type "bit" + | CT_bit -> simple_type "logic" + | 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 + ksprintf simple_type "struct packed { logic [7:0] size; %s bits; }" logic + | CT_lbits -> simple_type "sail_bits" + | CT_fint width -> ksprintf simple_type "logic [%d:0]" (width - 1) + | CT_lint -> ksprintf simple_type "logic [%d:0]" (Config.max_unknown_integer_width - 1) + | CT_string -> simple_type (if Config.nostrings then "sail_unit" else "string") + | CT_unit -> simple_type "sail_unit" + | CT_variant (id, _) | CT_struct (id, _) | CT_enum (id, _) -> simple_type (sv_type_id_string id) + | CT_constant c -> + let width = required_width c in + ksprintf simple_type "logic [%d:0]" (width - 1) + | CT_ref ctyp -> ksprintf simple_type "sail_reg_%s" (Util.zencode_string (string_of_ctyp ctyp)) + | CT_fvector (len, ctyp) -> + let outer_index = sprintf "[%d:0]" (len - 1) in + begin + match sv_ctyp ctyp with + | ty, Some inner_index -> (ty, Some (inner_index ^ outer_index)) + | ty, None -> (ty, Some outer_index) + end + | CT_list ctyp -> begin + match sv_ctyp ctyp with ty, Some inner_index -> (ty, Some (inner_index ^ "[$]")) | ty, None -> (ty, Some "[$]") + end + | CT_vector ctyp -> begin + match sv_ctyp ctyp with ty, Some inner_index -> (ty, Some (inner_index ^ "[]")) | ty, None -> (ty, Some "[]") + end + | CT_real -> simple_type "sail_real" + | CT_rounding_mode -> simple_type "sail_rounding_mode" + | CT_float width -> ksprintf simple_type "sail_float%d" width + | CT_tup _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Tuple type should not reach SV backend" + | CT_poly _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Polymorphic type should not reach SV backend" + + module Smt = + Smt_gen.Make + (struct + let max_unknown_integer_width = Config.max_unknown_integer_width + let max_unknown_bitvector_width = Config.max_unknown_bitvector_width + let union_ctyp_classify = is_packed + end) + (struct + let print_bits l = function + | CT_lbits -> "sail_print_bits" + | CT_fbits sz when Config.nostrings -> Generate_primop.print_fbits_stub sz + | CT_fbits sz -> Generate_primop.print_fbits sz + | _ -> Reporting.unreachable l __POS__ "print_bits" + + 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 + | _ -> Reporting.unreachable l __POS__ "string_of_bits" + + let dec_str l = function + | CT_lint -> "sail_dec_str" + | CT_fint sz when Config.nostrings -> Generate_primop.dec_str_fint_stub sz + | CT_fint sz -> Generate_primop.dec_str_fint sz + | _ -> Reporting.unreachable l __POS__ "dec_str" + + let hex_str l = function + | CT_lint -> "sail_hex_str" + | CT_fint sz when Config.nostrings -> Generate_primop.hex_str_fint_stub sz + | CT_fint sz -> Generate_primop.hex_str_fint sz + | _ -> Reporting.unreachable l __POS__ "hex_str" + + let hex_str_upper l = function + | CT_lint -> "sail_hex_str_upper" + | CT_fint sz when Config.nostrings -> Generate_primop.hex_str_upper_fint_stub sz + | CT_fint sz -> Generate_primop.hex_str_upper_fint sz + | _ -> Reporting.unreachable l __POS__ "hex_str_upper" + + let count_leading_zeros _l sz = Generate_primop.count_leading_zeros sz + + let fvector_store _l len ctyp = + Generate_primop.fvector_store len (sv_ctyp ctyp) (Util.zencode_string (string_of_ctyp ctyp)) + + let is_empty l = function + | CT_list ctyp -> Generate_primop.is_empty (sv_ctyp ctyp) (Util.zencode_string (string_of_ctyp ctyp)) + | _ -> Reporting.unreachable l __POS__ "is_empty" + + let hd l = function + | CT_list ctyp -> Generate_primop.hd (sv_ctyp ctyp) (Util.zencode_string (string_of_ctyp ctyp)) + | _ -> Reporting.unreachable l __POS__ "hd" + + let tl l = function + | CT_list ctyp -> Generate_primop.tl (sv_ctyp ctyp) (Util.zencode_string (string_of_ctyp ctyp)) + | _ -> Reporting.unreachable l __POS__ "tl" + end) + + let ( let* ) = Smt_gen.bind + let return = Smt_gen.return + let mapM = Smt_gen.mapM + + let sv_name = function + | Name (id, _) -> sv_id id + | Global (id, _) -> sv_id id + | Have_exception _ -> string "sail_have_exception" + | Current_exception _ -> string "sail_current_exception" + | Throw_location _ -> string "sail_throw_location" + | Return _ -> string "sail_return" + + let wrap_type ctyp doc = + match sv_ctyp ctyp with + | ty, None -> string ty ^^ space ^^ doc + | ty, Some index -> string ty ^^ space ^^ doc ^^ space ^^ string index + + (* + let sv_ctyp_dummy = function + | CT_bool -> string "0" + | CT_fbits width -> + ksprintf string "%d'b%s" width (String.make width 'X') + | CT_lbits -> + let index = ksprintf string "%d'b%s" lbits_index_width (String.make lbits_index_width 'X') in + let sz = Config.max_unknown_bitvector_width in + let contents = ksprintf string "%d'b%s" sz (String.make sz 'X') in + squote ^^ lbrace ^^ index ^^ comma ^^ space ^^ ksprintf string ^^ rbrace + | CT_bit -> string "1'bX" + | _ -> string "DEFAULT" + *) + + let sv_type_def = function + | CTD_enum (id, ids) -> + string "typedef" ^^ space ^^ string "enum" ^^ space + ^^ group (lbrace ^^ nest 4 (hardline ^^ separate_map (comma ^^ hardline) sv_id ids) ^^ hardline ^^ rbrace) + ^^ space ^^ sv_type_id id ^^ semi + | CTD_struct (id, fields) -> + let sv_field (id, ctyp) = wrap_type ctyp (sv_id id) in + let can_be_packed = List.for_all (fun (_, ctyp) -> is_packed ctyp) fields in + string "typedef" ^^ space ^^ string "struct" + ^^ (if can_be_packed then space ^^ string "packed" else empty) + ^^ space + ^^ group + (lbrace + ^^ nest 4 (hardline ^^ separate_map (semi ^^ hardline) sv_field fields) + ^^ semi ^^ hardline ^^ rbrace + ) + ^^ 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 (sv_id id) in + let tag_type = string ("sailtag_" ^ sv_id_string id) in + let value_type = string ("sailunion_" ^ sv_id_string id) in + let kind_enum = + separate space + [ + string "typedef"; + string "enum"; + group (lbrace ^^ nest 4 (hardline ^^ separate_map (comma ^^ hardline) kind_id ctors) ^^ hardline ^^ rbrace); + tag_type ^^ semi; + ] + in + (* At least verilator only allows unions for packed types (which + is roughly equivalent to types that can be represented as + finite bitvectors). *) + let can_be_packed = List.for_all (fun (_, ctyp) -> is_packed ctyp) ctors in + kind_enum ^^ twice hardline + ^^ + if can_be_packed then ( + let constructors = + List.map + (fun (ctor_id, ctyp) -> + separate space [string "function"; string "automatic"; sv_type_id id; sv_id ctor_id] + ^^ parens (wrap_type ctyp (char 'v')) + ^^ semi + ^^ nest 4 + (hardline ^^ sv_type_id id ^^ space ^^ char 'r' ^^ semi ^^ hardline + ^^ string ("sailunion_" ^ sv_id_string id) + ^^ space ^^ string "u" ^^ semi ^^ hardline + ^^ separate space + [ + string "r.tag"; + equals; + string_of_id ctor_id |> Util.zencode_string |> String.uppercase_ascii |> string; + ] + ^^ semi ^^ hardline + ^^ separate space [char 'u' ^^ dot ^^ sv_id ctor_id; equals; char 'v'] + ^^ semi ^^ hardline + ^^ separate space [string "r.value"; equals; char 'u'] + ^^ semi ^^ hardline ^^ string "return" ^^ space ^^ char 'r' ^^ semi + ) + ^^ hardline ^^ string "endfunction" + ) + ctors + in + separate space + [ + string "typedef"; + string "union"; + string "packed"; + group + (lbrace + ^^ nest 4 (hardline ^^ separate_map (semi ^^ hardline) sv_ctor ctors) + ^^ semi ^^ hardline ^^ rbrace + ); + value_type ^^ semi; + ] + ^^ twice hardline + ^^ separate space + [ + string "typedef"; + string "struct"; + string "packed"; + group + (lbrace + ^^ nest 4 + (hardline ^^ tag_type ^^ space ^^ string "tag" ^^ semi ^^ hardline ^^ value_type ^^ space + ^^ string "value" + ) + ^^ semi ^^ hardline ^^ rbrace + ); + sv_type_id id ^^ semi; + ] + ^^ twice hardline + ^^ separate (twice hardline) constructors + ^^ exception_boilerplate + ) + else ( + let constructors = + List.map + (fun (ctor_id, ctyp) -> + separate space [string "function"; string "automatic"; sv_type_id id; sv_id ctor_id] + ^^ parens (wrap_type ctyp (char 'v')) + ^^ semi + ^^ nest 4 + (hardline ^^ sv_type_id id ^^ space ^^ char 'r' ^^ semi ^^ hardline + ^^ separate space + [ + string "r.tag"; + equals; + string_of_id ctor_id |> Util.zencode_string |> String.uppercase_ascii |> string; + ] + ^^ semi ^^ hardline + ^^ separate space [char 'r' ^^ dot ^^ sv_id ctor_id; equals; char 'v'] + ^^ semi ^^ hardline ^^ string "return" ^^ space ^^ char 'r' ^^ semi + ) + ^^ hardline ^^ string "endfunction" + ) + ctors + in + separate space + [ + string "typedef"; + string "struct"; + group + (lbrace + ^^ nest 4 + (hardline ^^ tag_type ^^ space ^^ string "tag" ^^ semi ^^ hardline + ^^ separate_map (semi ^^ hardline) sv_ctor ctors + ) + ^^ semi ^^ hardline ^^ rbrace + ); + sv_type_id id ^^ semi; + ] + ^^ twice hardline + ^^ separate (twice hardline) constructors + ^^ exception_boilerplate + ) + + let sv_signed x = string "signed'" ^^ parens x + + let string_of_bitU = function Sail2_values.B0 -> "0" | Sail2_values.B1 -> "1" | Sail2_values.BU -> "X" + + let has_undefined_bit = List.exists (function Sail2_values.BU -> true | _ -> false) + + let rec hex_bitvector bits = + let open Sail2_values in + match bits with + | B0 :: B0 :: B0 :: B0 :: rest -> "0" ^ hex_bitvector rest + | B0 :: B0 :: B0 :: B1 :: rest -> "1" ^ hex_bitvector rest + | B0 :: B0 :: B1 :: B0 :: rest -> "2" ^ hex_bitvector rest + | B0 :: B0 :: B1 :: B1 :: rest -> "3" ^ hex_bitvector rest + | B0 :: B1 :: B0 :: B0 :: rest -> "4" ^ hex_bitvector rest + | B0 :: B1 :: B0 :: B1 :: rest -> "5" ^ hex_bitvector rest + | B0 :: B1 :: B1 :: B0 :: rest -> "6" ^ hex_bitvector rest + | B0 :: B1 :: B1 :: B1 :: rest -> "7" ^ hex_bitvector rest + | B1 :: B0 :: B0 :: B0 :: rest -> "8" ^ hex_bitvector rest + | B1 :: B0 :: B0 :: B1 :: rest -> "9" ^ hex_bitvector rest + | B1 :: B0 :: B1 :: B0 :: rest -> "A" ^ hex_bitvector rest + | B1 :: B0 :: B1 :: B1 :: rest -> "B" ^ hex_bitvector rest + | B1 :: B1 :: B0 :: B0 :: rest -> "C" ^ hex_bitvector rest + | B1 :: B1 :: B0 :: B1 :: rest -> "D" ^ hex_bitvector rest + | B1 :: B1 :: B1 :: B0 :: rest -> "E" ^ hex_bitvector rest + | B1 :: B1 :: B1 :: B1 :: rest -> "F" ^ hex_bitvector rest + | _ -> "" + + let rec tails = function + | Var v -> Some (0, v) + | Tl (_, arg) -> Option.map (fun (n, v) -> (n + 1, v)) (tails arg) + | _ -> None + + (* Convert a SMTLIB expression into SystemVerilog *) + let rec sv_smt ?(need_parens = false) = + let sv_smt_parens exp = sv_smt ~need_parens:true exp in + let opt_parens doc = if need_parens then parens doc else doc in + function + | 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) + else ksprintf string "%d'b%s" len (Util.string_of_list "" string_of_bitU bits) + | Bool_lit true -> string "1'h1" + | Bool_lit false -> string "1'h0" + | String_lit s -> if Config.nostrings then string "SAIL_UNIT" else ksprintf string "\"%s\"" s + | Enum "unit" -> string "SAIL_UNIT" + | Fn ("reg_ref", [String_lit r]) -> ksprintf string "SAIL_REG_%s" (Util.zencode_upper_string r) + | Fn ("Bits", [size; bv]) -> squote ^^ lbrace ^^ sv_smt size ^^ comma ^^ space ^^ sv_smt bv ^^ rbrace + | Fn ("concat", xs) -> lbrace ^^ separate_map (comma ^^ space) sv_smt xs ^^ rbrace + | Fn ("not", [Fn ("not", [x])]) -> sv_smt ~need_parens x + | Fn ("not", [Fn ("=", [x; y])]) -> opt_parens (separate space [sv_smt_parens x; string "!="; sv_smt_parens y]) + | Fn ("not", [x]) -> opt_parens (char '!' ^^ sv_smt_parens x) + | Fn ("=", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string "=="; sv_smt_parens y]) + | Fn ("and", xs) -> opt_parens (separate_map (space ^^ string "&&" ^^ space) sv_smt_parens xs) + | Fn ("or", xs) -> opt_parens (separate_map (space ^^ string "||" ^^ space) sv_smt_parens xs) + | Fn ("bvnot", [x]) -> opt_parens (char '~' ^^ sv_smt_parens x) + | Fn ("bvneg", [x]) -> opt_parens (char '-' ^^ sv_smt_parens x) + | Fn ("bvand", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '&'; sv_smt_parens y]) + | Fn ("bvnand", [x; y]) -> + opt_parens (char '~' ^^ parens (separate space [sv_smt_parens x; char '&'; sv_smt_parens y])) + | Fn ("bvor", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '|'; sv_smt_parens y]) + | Fn ("bvnor", [x; y]) -> + opt_parens (char '~' ^^ parens (separate space [sv_smt_parens x; char '|'; sv_smt_parens y])) + | Fn ("bvxor", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '^'; sv_smt_parens y]) + | Fn ("bvxnor", [x; y]) -> + opt_parens (char '~' ^^ parens (separate space [sv_smt_parens x; char '^'; sv_smt_parens y])) + | Fn ("bvadd", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '+'; sv_smt_parens y]) + | Fn ("bvsub", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '-'; sv_smt_parens y]) + | Fn ("bvmul", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '*'; sv_smt_parens y]) + | Fn ("bvult", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '<'; sv_smt_parens y]) + | Fn ("bvule", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string "<="; sv_smt_parens y]) + | Fn ("bvugt", [x; y]) -> opt_parens (separate space [sv_smt_parens x; char '>'; sv_smt_parens y]) + | Fn ("bvuge", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string ">="; sv_smt_parens y]) + | Fn ("bvslt", [x; y]) -> opt_parens (separate space [sv_signed (sv_smt x); char '<'; sv_signed (sv_smt y)]) + | Fn ("bvsle", [x; y]) -> opt_parens (separate space [sv_signed (sv_smt x); string "<="; sv_signed (sv_smt y)]) + | Fn ("bvsgt", [x; y]) -> opt_parens (separate space [sv_signed (sv_smt x); char '>'; sv_signed (sv_smt y)]) + | Fn ("bvsge", [x; y]) -> opt_parens (separate space [sv_signed (sv_smt x); string ">="; sv_signed (sv_smt y)]) + | Fn ("bvshl", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string "<<"; sv_signed (sv_smt y)]) + | Fn ("bvlshr", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string ">>"; sv_signed (sv_smt y)]) + | Fn ("bvashr", [x; y]) -> opt_parens (separate space [sv_smt_parens x; string ">>>"; sv_signed (sv_smt y)]) + | Fn ("select", [x; i]) -> sv_smt_parens x ^^ lbracket ^^ sv_smt i ^^ rbracket + | Fn ("contents", [Var v]) -> sv_name v ^^ dot ^^ string "bits" + | Fn ("contents", [x]) -> string "sail_bits_value" ^^ parens (sv_smt x) + | Fn ("len", [Var v]) -> sv_name v ^^ dot ^^ string "size" + | Fn ("len", [x]) -> string "sail_bits_size" ^^ parens (sv_smt x) + | Fn ("cons", [x; xs]) -> lbrace ^^ sv_smt x ^^ comma ^^ space ^^ sv_smt xs ^^ rbrace + | Fn (f, args) -> string f ^^ parens (separate_map (comma ^^ space) sv_smt args) + | Store (_, store_fn, arr, i, x) -> string store_fn ^^ parens (separate_map (comma ^^ space) sv_smt [arr; i; x]) + | SignExtend (len, _, x) -> ksprintf string "unsigned'(%d'(signed'({" len ^^ sv_smt x ^^ string "})))" + | ZeroExtend (len, _, x) -> ksprintf string "%d'({" len ^^ sv_smt x ^^ string "})" + | Extract (n, m, Bitvec_lit bits) -> + sv_smt (Bitvec_lit (Sail2_operators_bitlists.subrange_vec_dec bits (Big_int.of_int n) (Big_int.of_int m))) + | Extract (n, m, Var v) -> + if n = m then sv_name v ^^ lbracket ^^ string (string_of_int n) ^^ rbracket + else sv_name v ^^ lbracket ^^ string (string_of_int n) ^^ colon ^^ string (string_of_int m) ^^ rbracket + | Extract (n, m, x) -> + if n = m then braces (sv_smt x) ^^ lbracket ^^ string (string_of_int n) ^^ rbracket + else braces (sv_smt x) ^^ lbracket ^^ string (string_of_int n) ^^ colon ^^ string (string_of_int m) ^^ rbracket + | Var v -> sv_name v + | Tester (ctor, v) -> + opt_parens + (separate space [sv_smt v ^^ dot ^^ string "tag"; string "=="; string (ctor |> String.uppercase_ascii)]) + | Unwrap (ctor, packed, v) -> + if packed then sv_smt v ^^ dot ^^ string "value" ^^ dot ^^ sv_id ctor else sv_smt v ^^ dot ^^ sv_id ctor + | Field (_, field, v) -> sv_smt v ^^ dot ^^ sv_id field + | Ite (cond, then_exp, else_exp) -> + separate space [sv_smt_parens cond; char '?'; sv_smt_parens then_exp; char ':'; sv_smt_parens else_exp] + | Enum e -> failwith "Unknown enum" + | Empty_list -> string "{}" + | Hd (op, arg) -> begin + match tails arg with + | Some (index, v) -> sv_name v ^^ brackets (string (string_of_int index)) + | None -> string op ^^ parens (sv_smt arg) + end + | Tl (op, arg) -> string op ^^ parens (sv_smt arg) + | _ -> empty + + let sv_cval cval = + let* smt = Smt.smt_cval cval in + return (sv_smt smt) + + let rec sv_clexp = function + | CL_id (id, _) -> sv_name id + | CL_field (clexp, field) -> sv_clexp clexp ^^ dot ^^ sv_id field + | clexp -> string ("// CLEXP " ^ Jib_util.string_of_clexp clexp) + + let sv_update_fbits = function + | [bv; index; bit] -> begin + match (cval_ctyp bv, cval_ctyp index) with + | CT_fbits 1, _ -> Smt_gen.fmap sv_smt (Smt.smt_cval bit) + | CT_fbits sz, CT_constant c -> + let c = Big_int.to_int c in + let* bv_smt = Smt.smt_cval bv in + let bv_smt_1 = Extract (sz - 1, c + 1, bv_smt) in + let bv_smt_2 = Extract (c - 1, 0, bv_smt) in + let* bit_smt = Smt.smt_cval bit in + let smt = + if c = 0 then Fn ("concat", [bv_smt_1; bit_smt]) + else if c = sz - 1 then Fn ("concat", [bit_smt; bv_smt_2]) + else Fn ("concat", [bv_smt_1; bit_smt; bv_smt_2]) + in + return (sv_smt smt) + | _, _ -> failwith "update_fbits 1" + end + | _ -> failwith "update_fbits 2" + + let cval_for_ctyp = function + | CT_unit -> return (V_lit (VL_unit, CT_unit)) + | ctyp -> + let* l = Smt_gen.current_location in + Reporting.unreachable l __POS__ ("Cannot create undefined value of type " ^ string_of_ctyp ctyp) + + let sv_line_directive l = + match Reporting.simp_loc l with + | Some (p1, _) when Config.line_directives -> + ksprintf string "`line %d \"%s\" 0" p1.pos_lnum p1.pos_fname ^^ hardline + | _ -> empty + + let sv_assign clexp value = + match clexp with + | CL_addr (CL_id (id, CT_ref reg_ctyp)) -> + let encoded = Util.zencode_string (string_of_ctyp reg_ctyp) in + ksprintf string "sail_reg_assign_%s" encoded ^^ parens (sv_name id ^^ comma ^^ space ^^ value) ^^ semi + | _ -> sv_clexp clexp ^^ space ^^ equals ^^ space ^^ value ^^ semi + + let rec sv_instr ctx (I_aux (aux, (_, l))) = + let ld = sv_line_directive l in + match aux with + | I_comment str -> return (concat_map string ["/* "; str; " */"]) + | I_decl (ctyp, id) -> return (ld ^^ wrap_type ctyp (sv_name id) ^^ semi) + | I_init (ctyp, id, cval) -> + let* value = sv_cval cval in + return (ld ^^ separate space [wrap_type ctyp (sv_name id); equals; value] ^^ semi) + | I_return cval -> + let* value = sv_cval cval in + return (string "return" ^^ space ^^ value ^^ semi) + | I_end id -> return (string "return" ^^ space ^^ sv_name id ^^ semi) + | I_exit _ -> return (if Config.comb then string "sail_reached_unreachable = 1;" else string "$finish" ^^ semi) + | I_copy (clexp, cval) -> + let* value = + Smt_gen.bind (Smt.smt_cval cval) (Smt.smt_conversion ~into:(clexp_ctyp clexp) ~from:(cval_ctyp cval)) + in + return (sv_assign clexp (sv_smt value)) + | I_funcall (clexp, _, (id, _), args) -> + if ctx_is_extern id ctx then ( + let name = ctx_get_extern id ctx in + match Smt.builtin name with + | Some generator -> + let* value = Smt_gen.fmap Smt_exp.simp (generator args (clexp_ctyp clexp)) in + begin + (* We can optimize R = store(R, i x) into R[i] = x *) + match (clexp, value) with + | CL_id (v, _), Store (_, _, Var v', i, x) when Name.compare v v' = 0 -> + return + (ld + ^^ separate space [sv_clexp clexp ^^ lbracket ^^ sv_smt i ^^ rbracket; equals; sv_smt x] + ^^ semi + ) + | _, _ -> return (ld ^^ sv_assign clexp (sv_smt value)) + end + | None -> + let* args = mapM Smt.smt_cval args in + let value = Fn ("sail_" ^ name, args) in + return (ld ^^ sv_assign clexp (sv_smt value)) + ) + else if Id.compare id (mk_id "update_fbits") = 0 then + let* rhs = sv_update_fbits args in + return (ld ^^ sv_clexp clexp ^^ space ^^ equals ^^ space ^^ rhs ^^ semi) + else if Id.compare id (mk_id "internal_vector_init") = 0 then return empty + else if Id.compare id (mk_id "internal_vector_update") = 0 then ( + match args with + | [arr; i; x] -> begin + match cval_ctyp arr with + | CT_fvector (len, _) -> + 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)) + ) + in + let* x = Smt.smt_cval x in + return + (sv_clexp clexp ^^ lbracket ^^ sv_smt i ^^ rbracket ^^ space ^^ equals ^^ space ^^ sv_smt x ^^ semi) + | _ -> Reporting.unreachable l __POS__ "Invalid vector type for internal vector update" + end + | _ -> Reporting.unreachable l __POS__ "Invalid number of arguments to internal vector update" + ) + else + let* args = mapM sv_cval args in + let call = sv_id id ^^ parens (separate (comma ^^ space) args) in + return (ld ^^ sv_assign clexp call) + | I_if (cond, [], else_instrs, _) -> + let* cond = sv_cval (V_call (Bnot, [cond])) in + return + (string "if" ^^ space ^^ parens cond ^^ space ^^ string "begin" + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) else_instrs) + ^^ hardline ^^ string "end" ^^ semi + ) + | I_if (cond, then_instrs, [], _) -> + let* cond = sv_cval cond in + return + (string "if" ^^ space ^^ parens cond ^^ space ^^ string "begin" + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) then_instrs) + ^^ hardline ^^ string "end" ^^ semi + ) + | I_if (cond, then_instrs, else_instrs, _) -> + let* cond = sv_cval cond in + return + (string "if" ^^ space ^^ parens cond ^^ space ^^ string "begin" + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) then_instrs) + ^^ hardline ^^ string "end" ^^ space ^^ string "else" ^^ space ^^ string "begin" + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) else_instrs) + ^^ hardline ^^ string "end" ^^ semi + ) + | I_block instrs -> + return + (string "begin" + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) instrs) + ^^ hardline ^^ string "end" ^^ semi + ) + | I_raw s -> return (string s ^^ semi) + | I_undefined ctyp -> + Reporting.unreachable l __POS__ "Unreachable instruction should not reach SystemVerilog backend" + | I_jump _ | I_goto _ | I_label _ -> + Reporting.unreachable l __POS__ "Non-structured control flow should not reach SystemVerilog backend" + | I_throw _ | I_try_block _ -> + Reporting.unreachable l __POS__ "Exception handling should not reach SystemVerilog backend" + | I_clear _ | I_reset _ | I_reinit _ -> + Reporting.unreachable l __POS__ "Cleanup commands should not appear in SystemVerilog backend" + + and sv_checked_instr ctx (I_aux (_, (_, l)) as instr) = + let v, _ = Smt_gen.run (sv_instr ctx instr) l in + v + + let sv_fundef_with ctx f params param_ctyps ret_ctyp fun_body = + let sv_ret_ty, index_ty = sv_ctyp ret_ctyp in + let sv_ret_ty, typedef = + match index_ty with + | Some index -> + let encoded = Util.zencode_string (string_of_ctyp ret_ctyp) in + let new_ty = string ("t_" ^ f ^ "_" ^ encoded) in + (new_ty, separate space [string "typedef"; string sv_ret_ty; new_ty; string index] ^^ semi ^^ twice hardline) + | None -> (string sv_ret_ty, empty) + in + let param_docs = + try List.map2 (fun param ctyp -> wrap_type ctyp (sv_id param)) params param_ctyps + with Invalid_argument _ -> Reporting.unreachable Unknown __POS__ "Function arity mismatch" + in + typedef + ^^ separate space [string "function"; string "automatic"; sv_ret_ty; string f] + ^^ parens (separate (comma ^^ space) param_docs) + ^^ semi + ^^ nest 4 (hardline ^^ fun_body) + ^^ hardline ^^ string "endfunction" + + let sv_fundef ctx f params param_ctyps ret_ctyp body = + let fun_body = + if List.exists (fun unrf -> unrf = string_of_id f) Config.unreachable then string "sail_reached_unreachable = 1;" + else + wrap_type ret_ctyp (sv_name Jib_util.return) + ^^ semi ^^ hardline + ^^ separate_map hardline (sv_checked_instr ctx) body + in + sv_fundef_with ctx (sv_id_string f) params param_ctyps ret_ctyp fun_body + + let filter_clear = filter_instrs (function I_aux (I_clear _, _) -> false | _ -> true) + + let variable_decls_to_top instrs = + let decls, others = + List.fold_left + (fun (decls, others) instr -> + match instr with + | I_aux (I_decl (ctyp, id), (_, l)) -> (idecl l ctyp id :: decls, others) + | I_aux (I_init (ctyp, id, cval), (_, l)) -> + (idecl l ctyp id :: decls, icopy l (CL_id (id, ctyp)) cval :: others) + | other -> (decls, other :: others) + ) + ([], []) instrs + in + List.rev decls @ List.rev others + + 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 + ) + in + separate space [string "function"; string "automatic"; string "void"; string name] + ^^ string "()" ^^ semi + ^^ nest 4 (hardline ^^ separate_map hardline (sv_checked_instr ctx) setup) + ^^ hardline ^^ string "endfunction" ^^ twice hardline + + let collect_registers cdefs = + List.fold_left + (fun rmap cdef -> + match cdef with + | CDEF_register (id, ctyp, _) -> + CTMap.update ctyp (function Some ids -> Some (id :: ids) | None -> Some [id]) rmap + | _ -> rmap + ) + CTMap.empty cdefs + + let sv_register_references cdefs = + let rmap = collect_registers cdefs in + let reg_ref id = "SAIL_REG_" ^ Util.zencode_upper_string (string_of_id id) in + let reg_ref_enums = + List.map + (fun (ctyp, regs) -> + separate space [string "typedef"; string "enum"; lbrace] + ^^ nest 4 (hardline ^^ separate_map (comma ^^ hardline) (fun r -> string (reg_ref r)) regs) + ^^ hardline ^^ rbrace ^^ space + ^^ ksprintf string "sail_reg_%s" (Util.zencode_string (string_of_ctyp ctyp)) + ^^ semi + ) + (CTMap.bindings rmap) + |> separate (twice hardline) + in + let reg_ref_functions = + List.map + (fun (ctyp, regs) -> + let encoded = Util.zencode_string (string_of_ctyp ctyp) in + let sv_ty, index_ty = sv_ctyp ctyp in + let sv_ty, typedef = + match index_ty with + | Some index -> + let new_ty = string ("t_reg_deref_" ^ encoded) in + (new_ty, separate space [string "typedef"; string sv_ty; new_ty; string index] ^^ semi ^^ twice hardline) + | None -> (string sv_ty, empty) + in + typedef + ^^ separate space [string "function"; string "automatic"; sv_ty] + ^^ space + ^^ string ("sail_reg_deref_" ^ encoded) + ^^ parens (string ("sail_reg_" ^ encoded) ^^ space ^^ char 'r') + ^^ semi + ^^ nest 4 + (hardline + ^^ separate_map hardline + (fun reg -> + separate space + [ + string "if"; + parens (separate space [char 'r'; string "=="; string (reg_ref reg)]); + string "begin"; + ] + ^^ nest 4 (hardline ^^ string "return" ^^ space ^^ sv_id reg ^^ semi) + ^^ hardline ^^ string "end" ^^ semi + ) + regs + ) + ^^ hardline ^^ string "endfunction" ^^ twice hardline + ^^ separate space [string "function"; string "automatic"; string "void"] + ^^ space + ^^ string ("sail_reg_assign_" ^ encoded) + ^^ parens (separate space [string ("sail_reg_" ^ encoded); char 'r' ^^ comma; wrap_type ctyp (char 'v')]) + ^^ semi + ^^ nest 4 + (hardline + ^^ separate_map hardline + (fun reg -> + separate space + [ + string "if"; + parens (separate space [char 'r'; string "=="; string (reg_ref reg)]); + string "begin"; + ] + ^^ nest 4 (hardline ^^ sv_id reg ^^ space ^^ equals ^^ space ^^ char 'v' ^^ semi) + ^^ hardline ^^ string "end" ^^ semi + ) + regs + ) + ^^ hardline ^^ string "endfunction" + ) + (CTMap.bindings rmap) + |> separate (twice hardline) + in + (reg_ref_enums ^^ twice hardline, reg_ref_functions ^^ twice hardline) + + type cdef_doc = { outside_module : document; inside_module_prefix : document; inside_module : document } + + let empty_cdef_doc = { outside_module = empty; inside_module_prefix = empty; inside_module = empty } + + let sv_cdef ctx fn_ctyps setup_calls = function + | 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 + ( { empty_cdef_doc with inside_module_prefix = binding_doc; inside_module = sv_setup_function ctx name setup }, + fn_ctyps, + name :: setup_calls + ) + | CDEF_type td -> ({ empty_cdef_doc with outside_module = sv_type_def td ^^ twice hardline }, fn_ctyps, setup_calls) + | CDEF_val (f, _, param_ctyps, ret_ctyp) -> + (empty_cdef_doc, Bindings.add f (param_ctyps, ret_ctyp) fn_ctyps, setup_calls) + | CDEF_fundef (f, _, params, body) -> + if List.mem (string_of_id f) Config.ignore then (empty_cdef_doc, fn_ctyps, setup_calls) + else ( + let body = + Jib_optimize.( + body |> flatten_instrs |> remove_dead_code |> variable_decls_to_top |> structure_control_flow_block + |> remove_undefined |> filter_clear + ) + in + begin + match Bindings.find_opt f fn_ctyps with + | Some (param_ctyps, ret_ctyp) -> + ( { + empty_cdef_doc with + inside_module = sv_fundef ctx f params param_ctyps ret_ctyp body ^^ twice hardline; + }, + fn_ctyps, + setup_calls + ) + | None -> Reporting.unreachable (id_loc f) __POS__ ("No function type found for " ^ string_of_id f) + end + ) + | CDEF_let (n, bindings, setup) -> + let bindings_doc = + separate_map (semi ^^ hardline) (fun (id, ctyp) -> wrap_type ctyp (sv_id id)) bindings + ^^ semi ^^ twice hardline + in + let name = sprintf "sail_setup_let_%d" n in + ( { empty_cdef_doc with inside_module = bindings_doc ^^ sv_setup_function ctx name setup }, + fn_ctyps, + name :: setup_calls + ) + | _ -> (empty_cdef_doc, fn_ctyps, setup_calls) + + let main_args main fn_ctyps = + match main with + | Some (CDEF_fundef (f, _, params, body)) -> begin + match Bindings.find_opt f fn_ctyps with + | Some (param_ctyps, ret_ctyp) -> begin + let main_args = + List.map2 + (fun param param_ctyp -> match param_ctyp with CT_unit -> string "SAIL_UNIT" | _ -> sv_id param) + params param_ctyps + in + let non_unit = + List.filter_map + (fun x -> x) + (List.map2 + (fun param param_ctyp -> match param_ctyp with CT_unit -> None | _ -> Some (param, param_ctyp)) + params param_ctyps + ) + in + let module_main_in = + List.map + (fun (param, param_ctyp) -> string "input" ^^ space ^^ wrap_type param_ctyp (sv_id param)) + non_unit + in + match ret_ctyp with + | CT_unit -> (main_args, None, module_main_in) + | _ -> + ( main_args, + Some (string "main_result"), + (string "output" ^^ space ^^ wrap_type ret_ctyp (string "main_result")) :: module_main_in + ) + end + | None -> Reporting.unreachable (id_loc f) __POS__ ("No function type found for " ^ string_of_id f) + end + | _ -> ([], None, []) + + let make_call_precise ctx id = + if ctx_is_extern id ctx then ( + let name = ctx_get_extern id ctx in + Option.is_none (Smt.builtin name) + ) + else true +end diff --git a/src/sail_sv_backend/keywords.ml b/src/sail_sv_backend/keywords.ml new file mode 100644 index 000000000..e1242149f --- /dev/null +++ b/src/sail_sv_backend/keywords.ml @@ -0,0 +1,328 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* Louis-Emile Ploix *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Libsail + +open Generate_primop + +(** Systemverilog has a lot of keywords, this list is from the + SystemVerilog LRM 1800-2017, Table B.1. Fortunately, there are no + keywords begining with the letter z, so our z-encoding scheme + works to avoid any clashes. *) +let sv_reserved_words = + [ + "accept_on"; + "alias"; + "always"; + "always_comb"; + "always_ff"; + "always_latch"; + "and"; + "assert"; + "assign"; + "assume"; + "automatic"; + "before"; + "begin"; + "bind"; + "bins"; + "binsof"; + "bit"; + "break"; + "buf"; + "bufif0"; + "bufif1"; + "byte"; + "case"; + "casex"; + "casez"; + "cell"; + "chandle"; + "checker"; + "class"; + "clocking"; + "cmos"; + "config"; + "const"; + "constraint"; + "context"; + "continue"; + "cover"; + "covergroup"; + "coverpoint"; + "cross"; + "deassign"; + "default"; + "defparam"; + "design"; + "disable"; + "dist"; + "do"; + "edge"; + "else"; + "end"; + "endcase"; + "endchecker"; + "endclass"; + "endclocking"; + "endconfig"; + "endfunction"; + "endgenerate"; + "endgroup"; + "endinterface"; + "endmodule"; + "endpackage"; + "endprimitive"; + "endprogram"; + "endproperty"; + "endspecify"; + "endsequence"; + "endtable"; + "endtask"; + "enum"; + "event"; + "eventually"; + "expect"; + "export"; + "extends"; + "extern"; + "final"; + "first_match"; + "for"; + "force"; + "foreach"; + "forever"; + "fork"; + "forkjoin"; + "function"; + "generate"; + "genvar"; + "global"; + "highz0"; + "highz1"; + "if"; + "iff"; + "ifnone"; + "ignore_bins"; + "illegal_bins"; + "implements"; + "implies"; + "import"; + "incdir"; + "include"; + "initial"; + "inout"; + "input"; + "inside"; + "instance"; + "int"; + "integer"; + "interconnect"; + "interface"; + "intersect"; + "join"; + "join_any"; + "join_none"; + "large"; + "let"; + "liblist"; + "library"; + "local"; + "localparam"; + "logic"; + "longint"; + "macromodule"; + "matches"; + "medium"; + "modport"; + "module"; + "nand"; + "negedge"; + "nettype"; + "new"; + "nexttime"; + "nmos"; + "nor"; + "noshowcancelled"; + "not"; + "notif0"; + "notif1"; + "null"; + "or"; + "output"; + "package"; + "packed"; + "parameter"; + "pmos"; + "posedge"; + "primitive"; + "priority"; + "program"; + "property"; + "protected"; + "pull0"; + "pull1"; + "pulldown"; + "pullup"; + "pulsestyle_ondetect"; + "pulsestyle_onevent"; + "pure"; + "rand"; + "randc"; + "randcase"; + "randsequence"; + "rcmos"; + "real"; + "realtime"; + "ref"; + "reg"; + "reject_on"; + "release"; + "repeat"; + "restrict"; + "return"; + "rnmos"; + "rpmos"; + "rtran"; + "rtranif0"; + "rtranif1"; + "s_always"; + "s_eventually"; + "s_nexttime"; + "s_until"; + "s_until_with"; + "scalared"; + "sequence"; + "shortint"; + "shortreal"; + "showcancelled"; + "signed"; + "small"; + "soft"; + "solve"; + "specify"; + "specparam"; + "static"; + "string"; + "strong"; + "strong0"; + "strong1"; + "struct"; + "super"; + "supply0"; + "supply1"; + "sync_accept_on"; + "sync_reject_on"; + "table"; + "tagged"; + "task"; + "this"; + "throughout"; + "time"; + "timeprecision"; + "timeunit"; + "tran"; + "tranif0"; + "tranif1"; + "tri"; + "tri0"; + "tri1"; + "triand"; + "trior"; + "trireg"; + "type"; + "typedef"; + "union"; + "unique"; + "unique0"; + "unsigned"; + "until"; + "until_with"; + "untyped"; + "use"; + "uwire"; + "var"; + "vectored"; + "virtual"; + "void"; + "wait"; + "wait_order"; + "wand"; + "weak"; + "weak0"; + "weak1"; + "while"; + "wildcard"; + "wire"; + "with"; + "within"; + "wor"; + "xnor"; + "xor"; + ] + |> StringSet.of_list diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml new file mode 100644 index 000000000..16c3ad284 --- /dev/null +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -0,0 +1,602 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* Louis-Emile Ploix *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Libsail + +open Ast +open Ast_util +open Jib +open Jib_compile +open Jib_util +open Value2 +open PPrint +open Printf +open Smt_exp + +open Generate_primop + +module R = Jib_sv + +let opt_output_dir = ref None + +let opt_includes = ref [] + +type verilate_mode = Verilator_none | Verilator_compile | Verilator_run + +let opt_verilate = ref Verilator_none + +let opt_line_directives = ref false + +let opt_comb = ref false + +let opt_inregs = ref false +let opt_outregs = ref false + +let opt_max_unknown_integer_width = ref 128 +let opt_max_unknown_bitvector_width = ref 128 + +let opt_nostrings = ref false +let opt_nopacked = ref false +let opt_nomem = ref false + +let opt_unreachable = ref [] +let opt_fun2wires = ref [] + +let opt_int_specialize = ref None + +let verilog_options = + [ + ( "-sv_output_dir", + Arg.String (fun s -> opt_output_dir := Some s), + " set the output directory for generated SystemVerilog files" + ); + ( "-sv_include", + Arg.String (fun s -> opt_includes := s :: !opt_includes), + " add include directive to generated SystemVerilog file" + ); + ( "-sv_verilate", + Arg.String + (fun opt -> + if opt = "run" then opt_verilate := Verilator_run + else if opt = "compile" then opt_verilate := Verilator_compile + else + raise + (Reporting.err_general Parse_ast.Unknown + "Invalid argument for -sv_verilate option. Valid options are either 'run' or 'compile'." + ) + ), + " Invoke verilator on generated output" + ); + ("-sv_lines", Arg.Set opt_line_directives, " output `line directives"); + ("-sv_comb", Arg.Set opt_comb, " output an always_comb block instead of initial block"); + ("-sv_inregs", Arg.Set opt_inregs, " take register values from inputs"); + ("-sv_outregs", Arg.Set opt_outregs, " output register values"); + ( "-sv_int_size", + Arg.Int (fun i -> opt_max_unknown_integer_width := i), + " set the maximum width for unknown integers" + ); + ( "-sv_bits_size", + Arg.Int (fun i -> opt_max_unknown_bitvector_width := i), + " set the maximum width for bitvectors with unknown width" + ); + ("-sv_nostrings", Arg.Set opt_nostrings, " don't emit any strings, instead emit units"); + ("-sv_nopacked", Arg.Set opt_nopacked, " don't emit packed datastructures"); + ( "-sv_unreachable", + Arg.String (fun fn -> opt_unreachable := fn :: !opt_unreachable), + " Mark function as unreachable." + ); + ("-sv_nomem", Arg.Set opt_nomem, " don't emit a dynamic memory implementation"); + ( "-sv_fun2wires", + Arg.String (fun fn -> opt_fun2wires := fn :: !opt_fun2wires), + " Use input/output ports instead of emitting a function call" + ); + ( "-sv_specialize", + Arg.Int (fun i -> opt_int_specialize := Some i), + " Run n specialization passes on Sail Int-kinded type variables" + ); + ] + +let verilog_rewrites = + let open Rewrites in + [ + ("instantiate_outcomes", [String_arg "c"]); + ("realize_mappings", []); + ("toplevel_string_append", []); + ("pat_string_append", []); + ("mapping_patterns", []); + ("truncate_hex_literals", []); + ("mono_rewrites", [If_flag opt_mono_rewrites]); + ("recheck_defs", [If_flag opt_mono_rewrites]); + ("toplevel_nexps", [If_mono_arg]); + ("monomorphise", [String_arg "c"; If_mono_arg]); + ("atoms_to_singletons", [String_arg "c"; If_mono_arg]); + ("recheck_defs", [If_mono_arg]); + ("undefined", [Bool_arg false]); + ("vector_string_pats_to_bit_list", []); + ("remove_not_pats", []); + ("remove_vector_concat", []); + ("remove_bitvector_pats", []); + ("pattern_literals", [Literal_arg "all"]); + ("tuple_assignments", []); + ("vector_concat_assignments", []); + ("simple_struct_assignments", []); + ("split", [String_arg "execute"]); + ("exp_lift_assign", []); + ("merge_function_clauses", []); + ("recheck_defs", []); + ("constant_fold", [String_arg "c"]); + ] + +module type JIB_CONFIG = sig + val make_call_precise : Jib_compile.ctx -> id -> bool +end + +module Verilog_config (C : JIB_CONFIG) : Jib_compile.CONFIG = struct + open Type_check + open Jib_compile + + let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) + let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + + let rec convert_typ ctx typ = + let (Typ_aux (typ_aux, l) as typ) = Env.expand_synonyms ctx.local_env typ in + match typ_aux with + | Typ_id id when string_of_id id = "bit" -> CT_bit + | Typ_id id when string_of_id id = "bool" -> CT_bool + | Typ_id id when string_of_id id = "int" -> CT_lint + | 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 = "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 + | Typ_id id when string_of_id id = "float64" -> CT_float 64 + | Typ_id id when string_of_id id = "float128" -> CT_float 128 + | Typ_id id when string_of_id id = "float_rounding_mode" -> CT_rounding_mode + | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool + | Typ_app (id, args) when string_of_id id = "itself" -> convert_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l)) + | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" -> + begin + match destruct_range Env.empty typ with + | None -> assert false (* Checked if range type in guard *) + | Some (kids, constr, n, m) -> ( + let ctx = + { + ctx with + local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env; + } + in + match (nexp_simp n, nexp_simp m) with + | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.equal n m -> CT_constant n + | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> + CT_fint 64 + | n, m -> + if + prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) + && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) + then CT_fint 64 + else CT_lint + ) + end + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> CT_list (ctyp_suprema (convert_typ ctx typ)) + (* When converting a sail bitvector type into C, we have three options in order of efficiency: + - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits. + - If the length is less than 64, then use a small bits type, sbits. + - If the length may be larger than 64, use a large bits type lbits. *) + | Typ_app (id, [A_aux (A_nexp n, _)]) when string_of_id id = "bitvector" -> begin + match solve_unique ctx.local_env n with Some n -> CT_fbits (Big_int.to_int n) | _ -> CT_lbits + end + | Typ_app (id, [A_aux (A_nexp n, _); A_aux (A_typ typ, _)]) when string_of_id id = "vector" -> begin + match nexp_simp n with + | Nexp_aux (Nexp_constant c, _) -> CT_fvector (Big_int.to_int c, convert_typ ctx typ) + | _ -> CT_vector (convert_typ ctx typ) + end + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" -> CT_ref (convert_typ ctx typ) + | Typ_id id when Bindings.mem id ctx.records -> + CT_struct (id, Bindings.find id ctx.records |> snd |> Bindings.bindings) + | Typ_app (id, typ_args) when Bindings.mem id ctx.records -> + let typ_params, fields = Bindings.find id ctx.records in + let quants = + List.fold_left2 + (fun quants typ_param typ_arg -> + match typ_arg with + | A_aux (A_typ typ, _) -> KBindings.add typ_param (convert_typ ctx typ) quants + | _ -> Reporting.unreachable l __POS__ "Non-type argument for record here should be impossible" + ) + ctx.quants typ_params (List.filter is_typ_arg_typ typ_args) + in + let fix_ctyp ctyp = if is_polymorphic ctyp then ctyp_suprema (subst_poly quants ctyp) else ctyp in + CT_struct (id, Bindings.map fix_ctyp fields |> Bindings.bindings) + | Typ_id id when Bindings.mem id ctx.variants -> + CT_variant (id, Bindings.find id ctx.variants |> snd |> Bindings.bindings) + | Typ_app (id, typ_args) when Bindings.mem id ctx.variants -> + let typ_params, ctors = Bindings.find id ctx.variants in + let quants = + List.fold_left2 + (fun quants typ_param typ_arg -> + match typ_arg with + | A_aux (A_typ typ, _) -> KBindings.add typ_param (convert_typ ctx typ) quants + | _ -> Reporting.unreachable l __POS__ "Non-type argument for variant here should be impossible" + ) + ctx.quants typ_params (List.filter is_typ_arg_typ typ_args) + in + let fix_ctyp ctyp = if is_polymorphic ctyp then ctyp_suprema (subst_poly quants ctyp) else ctyp in + CT_variant (id, Bindings.map fix_ctyp ctors |> Bindings.bindings) + | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements) + | Typ_tuple typs -> CT_tup (List.map (convert_typ ctx) typs) + | Typ_exist _ -> begin + (* Use Type_check.destruct_exist when optimising with SMT, to + ensure that we don't cause any type variable clashes in + local_env, and that we can optimize the existential based + upon it's constraints. *) + match destruct_exist (Env.expand_synonyms ctx.local_env typ) with + | Some (kids, nc, typ) -> + let env = add_existential l kids nc ctx.local_env in + convert_typ { ctx with local_env = env } typ + | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!") + end + | Typ_var kid -> CT_poly kid + | _ -> Reporting.unreachable l __POS__ ("No C type for type " ^ string_of_typ typ) + + let optimize_anf _ aexp = aexp + + let unroll_loops = None + let specialize_calls = false + let make_call_precise = C.make_call_precise + let ignore_64 = true + let struct_value = false + let tuple_value = false + let track_throw = true + let branch_coverage = None + let use_real = false +end + +type function_footprint = { register_reads : IdSet.t; register_writes : IdSet.t } + +let rec instr_footprint (I_aux (aux, _)) = () + +and instrs_footprint instrs = () + +let register_types cdefs = + List.fold_left + (fun acc cdef -> match cdef with CDEF_register (id, ctyp, _) -> Bindings.add id ctyp acc | _ -> acc) + Bindings.empty cdefs + +let jib_of_ast make_call_precise env ast effect_info = + let open Jib_compile in + let module Jibc = Make (Verilog_config (struct + let make_call_precise = make_call_precise + end)) in + let env, effect_info = add_special_functions env effect_info in + let ctx = initial_ctx env effect_info in + Jibc.compile_ast ctx ast + +let wrap_module pre mod_name ins_outs doc = + pre ^^ hardline ^^ string "module" ^^ space ^^ string mod_name + ^^ parens (nest 4 (hardline ^^ separate (comma ^^ hardline) ins_outs) ^^ hardline) + ^^ semi + ^^ nest 4 (hardline ^^ doc) + ^^ hardline ^^ string "endmodule" ^^ hardline + +let verilator_cpp_wrapper name = + [ + sprintf "#include \"V%s.h\"" name; + "#include \"verilated.h\""; + "int main(int argc, char** argv) {"; + " VerilatedContext* contextp = new VerilatedContext;"; + " contextp->commandArgs(argc, argv);"; + sprintf " V%s* top = new V%s{contextp};" name name; + " while (!contextp->gotFinish()) { top -> eval(); }"; + " delete top;"; + " delete contextp;"; + " return 0;"; + "}"; + ] + +let make_genlib_file filename = + let common_primops = + if !opt_nostrings then + Generate_primop.common_primops_stubs !opt_max_unknown_bitvector_width !opt_max_unknown_integer_width + else Generate_primop.common_primops !opt_max_unknown_bitvector_width !opt_max_unknown_integer_width + in + let defs = Generate_primop.get_generated_primops () in + let ((out_chan, _, _, _) as file_info) = Util.open_output_with_check_unformatted !opt_output_dir filename in + output_string out_chan "`ifndef SAIL_LIBRARY_GENERATED\n"; + output_string out_chan "`define SAIL_LIBRARY_GENERATED\n\n"; + output_string out_chan common_primops; + List.iter + (fun def -> + List.iter + (fun line -> + output_string out_chan line; + output_char out_chan '\n' + ) + def; + output_char out_chan '\n' + ) + defs; + output_string out_chan "`endif\n"; + Util.close_output_with_check file_info + +let verilog_target _ default_sail_dir out_opt ast effect_info env = + let module SV = Jib_sv.Make (struct + let max_unknown_integer_width = !opt_max_unknown_integer_width + let max_unknown_bitvector_width = !opt_max_unknown_bitvector_width + let line_directives = !opt_line_directives + let nostrings = !opt_nostrings + let nopacked = !opt_nopacked + let unreachable = !opt_unreachable + let comb = !opt_comb + let ignore = !opt_fun2wires + end) in + let open SV in + let sail_dir = Reporting.get_sail_dir default_sail_dir in + let sail_sv_libdir = Filename.concat (Filename.concat sail_dir "lib") "sv" in + let out = match out_opt with None -> "out" | Some name -> name in + + let ast, env, effect_info = + let open Specialize in + match !opt_int_specialize with + | Some num_passes -> specialize_passes num_passes int_specialization env ast effect_info + | None -> (ast, env, effect_info) + in + + let cdefs, ctx = jib_of_ast SV.make_call_precise env ast effect_info in + let cdefs, ctx = Jib_optimize.remove_tuples cdefs ctx in + let registers = register_types cdefs in + + let include_doc = + (if !opt_nostrings then string "`define SAIL_NOSTRINGS" ^^ hardline else empty) + ^^ string "`include \"sail.sv\"" ^^ hardline + ^^ ksprintf string "`include \"sail_genlib_%s.sv\"" out + ^^ (if !opt_nomem then empty else hardline ^^ string "`include \"sail_memory.sv\"") + ^^ hardline + ^^ separate_map hardline (fun file -> ksprintf string "`include \"%s\"" file) !opt_includes + ^^ twice hardline + in + + let exception_vars = + string "bit sail_reached_unreachable;" ^^ hardline ^^ string "bit sail_have_exception;" ^^ hardline + ^^ (if !opt_nostrings then string "sail_unit" else string "string") + ^^ space ^^ string "sail_throw_location;" ^^ twice hardline + in + + let in_doc, out_doc, reg_doc, fn_ctyps, setup_calls = + List.fold_left + (fun (doc_in, doc_out, doc_reg, fn_ctyps, setup_calls) cdef -> + let cdef_doc, fn_ctyps, setup_calls = sv_cdef ctx fn_ctyps setup_calls cdef in + ( doc_in ^^ cdef_doc.inside_module, + doc_out ^^ cdef_doc.outside_module, + doc_reg ^^ cdef_doc.inside_module_prefix, + fn_ctyps, + setup_calls + ) + ) + (exception_vars, include_doc, empty, Bindings.empty, []) + cdefs + in + + let reg_ref_enums, reg_ref_functions = sv_register_references cdefs in + let out_doc = out_doc ^^ reg_ref_enums in + let in_doc = reg_doc ^^ reg_ref_functions ^^ in_doc in + + let mk_wire_fun nm = + let id = mk_id nm in + match Bindings.find_opt id fn_ctyps with + | None -> (empty, [], []) + | Some (arg_typs, ret_ty) -> + let arg_nms = List.mapi (fun i _ -> mk_id ("a" ^ string_of_int i)) arg_typs in + let real_name = if ctx_is_extern id ctx then "sail_" ^ ctx_get_extern id ctx else string_of_id id in + let invoke_flag = string (nm ^ "_sail_invoke") in + let result = string (nm ^ "_sail_invoke_ret") in + let arg_out i = string (nm ^ "_sail_invoke_arg_" ^ string_of_int i) in + let fun_body = + string "if (" ^^ invoke_flag + ^^ string ") sail_reached_unreachable = 1;" + ^^ hardline ^^ invoke_flag ^^ string " = 1;" ^^ hardline + ^^ (arg_nms + |> List.mapi (fun i arg -> arg_out i ^^ string " = " ^^ string (string_of_id arg) ^^ semi ^^ hardline) + |> separate empty + ) + ^^ string "return " ^^ result ^^ string ";" + in + ( sv_fundef_with ctx real_name arg_nms arg_typs ret_ty fun_body ^^ twice hardline, + separate space [string "output"; string "bit"; invoke_flag] + :: separate space [string "input"; string (fst (sv_ctyp ret_ty)); result] + :: List.mapi (fun i typ -> separate space [string "output"; string (fst (sv_ctyp typ)); arg_out i]) arg_typs, + [invoke_flag ^^ string " = 0;"] + ) + in + + let wire_funs, wire_fun_ports, wire_invoke_inits = + List.fold_right + (fun nm (code, ports, inits) -> + let new_code, new_ports, new_inits = mk_wire_fun nm in + (new_code ^^ code, new_ports @ ports, new_inits @ inits) + ) + !opt_fun2wires (empty, [], []) + in + + let setup_function = + string "function automatic void sail_setup();" + ^^ nest 4 + (hardline ^^ string "sail_reached_unreachable = 0;" ^^ hardline ^^ string "sail_have_exception = 0;" + ^^ hardline ^^ separate hardline wire_invoke_inits ^^ hardline + ^^ separate_map (semi ^^ hardline) (fun call -> string call ^^ string "()") (List.rev setup_calls) + ) + ^^ semi ^^ hardline ^^ string "endfunction" ^^ twice hardline + in + + let main_recv_inputs = + if !opt_inregs then + separate empty + (List.filter_map + (function + | CDEF_register (id, ctyp, _) -> + Some (SV.sv_id id ^^ space ^^ equals ^^ space ^^ sv_id id ^^ string "_in" ^^ semi ^^ hardline) + | _ -> None + ) + cdefs + ) + else empty + in + + let main_set_outputs = + if !opt_inregs then + separate empty + (List.filter_map + (function + | CDEF_register (id, ctyp, _) -> + Some (sv_id id ^^ string "_out" ^^ space ^^ equals ^^ space ^^ sv_id id ^^ semi ^^ hardline) + | _ -> None + ) + cdefs + ) + else empty + in + + let main = List.find_opt (function 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 = + hardline + ^^ (if Option.is_none main_result then string "sail_unit u;" ^^ hardline else empty) + ^^ string "sail_setup();" ^^ hardline ^^ string "$display(\"TEST START\");" ^^ hardline ^^ main_recv_inputs + ^^ Option.value main_result ~default:(string "u") + ^^ string " = main(" + ^^ separate (comma ^^ space) main_args + ^^ string ");" ^^ hardline ^^ main_set_outputs ^^ string "$display(\"TEST END\");" + in + + let invoke_main = + if not !opt_comb then + string "initial" ^^ space ^^ string "begin" ^^ nest 4 invoke_main_body ^^ hardline ^^ string "$finish;" + ^^ hardline ^^ string "end" + else string "always_comb" ^^ space ^^ string "begin" ^^ nest 4 invoke_main_body ^^ hardline ^^ string "end" + in + + let inputs = + if !opt_inregs then + List.filter_map + (function + | CDEF_register (id, ctyp, _) -> Some (string "input" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_in")) + | _ -> None + ) + cdefs + else [] + in + + let outputs = + if !opt_inregs then + List.filter_map + (function + | CDEF_register (id, ctyp, _) -> Some (string "output" ^^ space ^^ wrap_type ctyp (sv_id id ^^ string "_out")) + | _ -> None + ) + cdefs + else [] + in + + let sv_output = + Pretty_print_sail.to_string + (wrap_module out_doc ("sail_" ^ out) + (inputs @ outputs @ wire_fun_ports @ module_main_in_out) + (in_doc ^^ wire_funs ^^ setup_function ^^ invoke_main) + ) + in + make_genlib_file (sprintf "sail_genlib_%s.sv" out); + + let ((out_chan, _, _, _) as file_info) = Util.open_output_with_check_unformatted !opt_output_dir (out ^ ".sv") in + output_string out_chan sv_output; + Util.close_output_with_check file_info; + + begin + match !opt_verilate with + | Verilator_compile | Verilator_run -> + let ((out_chan, _, _, _) as file_info) = + Util.open_output_with_check_unformatted !opt_output_dir ("sim_" ^ out ^ ".cpp") + in + List.iter + (fun line -> + output_string out_chan line; + output_char out_chan '\n' + ) + (verilator_cpp_wrapper out); + Util.close_output_with_check file_info; + + Reporting.system_checked + (sprintf "verilator --cc --exe --build -j 0 -I%s sim_%s.cpp %s.sv" sail_sv_libdir out out); + begin + match !opt_verilate with Verilator_run -> Reporting.system_checked (sprintf "obj_dir/V%s" out) | _ -> () + end + | _ -> () + end + +let _ = + Target.register ~name:"systemverilog" ~flag:"sv" ~options:verilog_options ~rewrites:verilog_rewrites verilog_target diff --git a/test/builtins/clz.sail b/test/builtins/clz.sail index 5cf20068f..8ce59e897 100644 --- a/test/builtins/clz.sail +++ b/test/builtins/clz.sail @@ -1,5 +1,5 @@ default Order dec -$include +$include function main () : unit -> unit = { assert(count_leading_zeros(0x0) == 4); diff --git a/test/c/fvector_update.expect b/test/c/fvector_update.expect new file mode 100644 index 000000000..b287da3d9 --- /dev/null +++ b/test/c/fvector_update.expect @@ -0,0 +1,2 @@ +R[0] = 0xAB +vec[0] = 0xCD diff --git a/test/c/fvector_update.sail b/test/c/fvector_update.sail new file mode 100644 index 000000000..726dfb733 --- /dev/null +++ b/test/c/fvector_update.sail @@ -0,0 +1,13 @@ +default Order dec +$include + +register R : vector(8, dec, bits(8)) + +val main : unit -> unit + +function main() = { + R[0] = 0xAB; + let vec = [R with 0 = 0xCD]; + print_bits("R[0] = ", R[0]); + print_bits("vec[0] = ", vec[0]) +} \ No newline at end of file diff --git a/test/c/get_slice_int.expect b/test/c/get_slice_int.expect new file mode 100644 index 000000000..95ac40f2d --- /dev/null +++ b/test/c/get_slice_int.expect @@ -0,0 +1,6 @@ +3 3 0 = 0b011 +3 5 0 = 0b101 +3 5 0 = 0b101 +5 5 0 = 0b00101 +5 5 1 = 0b00010 +5 5 0 = 0b00101 diff --git a/test/c/get_slice_int.sail b/test/c/get_slice_int.sail new file mode 100644 index 000000000..ac19cf9d2 --- /dev/null +++ b/test/c/get_slice_int.sail @@ -0,0 +1,23 @@ +default Order dec +$include + +/* Use functions to hide the fact that these are really small constants, so they are forced to be represented as big ints */ + +val big_five : unit -> int + +function big_five() = 5 + +val big_zero : unit -> int + +function big_zero() = 0 + +val main : unit -> unit + +function main() = { + print_bits("3 3 0 = ", get_slice_int(3, 3, 0)); + print_bits("3 5 0 = ", get_slice_int(3, 5, 0)); + print_bits("3 5 0 = ", get_slice_int(3, big_five(), 0)); + print_bits("5 5 0 = ", get_slice_int(big_five(), big_five(), 0)); + print_bits("5 5 1 = ", get_slice_int(big_five(), 5, 1)); + print_bits("5 5 0 = ", get_slice_int(big_five(), big_five(), big_zero())); +} \ No newline at end of file diff --git a/test/c/list_scope2.sail b/test/c/list_scope2.sail index ceef63f92..82462e0dd 100644 --- a/test/c/list_scope2.sail +++ b/test/c/list_scope2.sail @@ -26,6 +26,6 @@ function main() = { print_endline(b); print_endline(c) }, - _ => (), - } + _ => print_endline("no match"), + } } diff --git a/test/c/pow2.expect b/test/c/pow2.expect new file mode 100644 index 000000000..ea7d2d23b --- /dev/null +++ b/test/c/pow2.expect @@ -0,0 +1,6 @@ +0 -> 1 +0 -> 1 +1 -> 2 +1 -> 2 +6 -> 64 +6 -> 64 diff --git a/test/c/pow2.sail b/test/c/pow2.sail new file mode 100644 index 000000000..fdce4d7c3 --- /dev/null +++ b/test/c/pow2.sail @@ -0,0 +1,25 @@ +default Order dec +$include + +val big0 : unit -> int + +function big0() = 0 + +val big1 : unit -> int + +function big1() = 1 + +val big6 : unit -> int + +function big6() = 6 + +val main : unit -> unit + +function main() = { + print_int("0 -> ", 2 ^ 0); + print_int("0 -> ", 2 ^ big0()); + print_int("1 -> ", 2 ^ 1); + print_int("1 -> ", 2 ^ big1()); + print_int("6 -> ", 2 ^ 6); + print_int("6 -> ", 2 ^ big6()); +} \ No newline at end of file diff --git a/test/c/primop.expect b/test/c/primop.expect new file mode 100644 index 000000000..d7e5e4999 --- /dev/null +++ b/test/c/primop.expect @@ -0,0 +1,2 @@ +4 +ok diff --git a/test/c/primop.sail b/test/c/primop.sail new file mode 100644 index 000000000..0843a3c84 --- /dev/null +++ b/test/c/primop.sail @@ -0,0 +1,28 @@ +default Order dec + +$include + +val big_four : unit -> int + +function big_four() = 4 + +val main : unit -> unit + +function main() = { + print_int("", abs_int(-4)); + assert(abs_int(-4) == 4); + assert(abs_int(4) == 4); + assert(abs_int(negate(4)) == 4); + assert(abs_int(-4) == big_four()); + assert(abs_int(big_four()) == big_four()); + assert(abs_int(negate(big_four())) == big_four()); + + assert(count_leading_zeros(0x0) == 4); + assert(count_leading_zeros(0x2) == 2); + + assert(max_int(2, 4) == 4); + assert(min_int(2, 4) == 2); + assert(min_int(-20, 20) == -20); + + print_endline("ok"); +} diff --git a/test/c/string_of_bits.sail b/test/c/string_of_bits.sail index fcaeb3e11..86a8bc7d5 100644 --- a/test/c/string_of_bits.sail +++ b/test/c/string_of_bits.sail @@ -22,4 +22,4 @@ function main(() : unit) -> unit = { let w = 0xFF; print_endline(x ++ y ++ BitStr(z) ++ " " ++ BitStr(w)) } -} \ No newline at end of file +} diff --git a/test/c/string_of_bits2.expect b/test/c/string_of_bits2.expect new file mode 100644 index 000000000..cca2dc4f7 --- /dev/null +++ b/test/c/string_of_bits2.expect @@ -0,0 +1,8 @@ +0b0 +0b1 +0b001 +0b00001 +0x1 +0x9 +0xAB +0x00AB diff --git a/test/c/string_of_bits2.sail b/test/c/string_of_bits2.sail new file mode 100644 index 000000000..4206ab2c4 --- /dev/null +++ b/test/c/string_of_bits2.sail @@ -0,0 +1,21 @@ +default Order dec + +$include +$include + +infixl 1 ++ + +overload operator ++ = {concat_str} + +val main : unit -> unit + +function main() = { + print(bits_str(0b0) ++ "\n"); + print(bits_str(0b1) ++ "\n"); + print(bits_str(0b001) ++ "\n"); + print(bits_str(0b00001) ++ "\n"); + print(bits_str(0b0001) ++ "\n"); + print(bits_str(0b1001) ++ "\n"); + print(bits_str(0xAB) ++ "\n"); + print(bits_str(0x00AB) ++ "\n") +} \ No newline at end of file diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail index 332b8aae1..ceb5a7b5c 100644 --- a/test/c/zero_length_bv.sail +++ b/test/c/zero_length_bv.sail @@ -11,4 +11,4 @@ function main((): unit) -> unit = { }; let x: vector(0, dec, string) = []; () -} \ No newline at end of file +} diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py index cba4001d6..542296af0 100755 --- a/test/smt/run_tests.py +++ b/test/smt/run_tests.py @@ -20,6 +20,7 @@ 'assembly_mapping_sat': { 'cvc4' }, # This test using unsupported CVC4 features 'arith_unsat': { 'z3', 'cvc4' }, 'arith_LFL_unsat' : { 'z3', 'cvc4' }, + 'revrev_endianness2_unsat' : { 'z3', 'cvc4' }, # There is some bug in this test } print("Sail is {}".format(sail)) diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py new file mode 100755 index 000000000..f2cfbacb5 --- /dev/null +++ b/test/sv/run_tests.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 + +import os +import re +import sys +import hashlib + +mydir = os.path.dirname(__file__) +os.chdir(mydir) +sys.path.insert(0, os.path.realpath('..')) + +from sailtest import * + +sail_dir = get_sail_dir() +sail = get_sail() + +skip_tests = { + 'all_even_vector_length', + 'assign_rename_bug', + 'bitvector', # This requires -sv_bits_size >= 200 + 'cheri128_hsb', + 'cheri_capreg', # behavior? + 'empty_list', # recursion + 'eq_struct', + 'flow_restrict', # contains very large integer literal + 'for_shadow', + 'foreach_none', + 'gvector', + 'inc_tests', + 'int64_vector_literal', + 'issue136', # recursion + 'large_bitvector', # This requires -sv_bits_size >= 204 + 'list_rec_functions1', # lists + 'list_rec_functions2', + 'list_torture', + 'loop_exception', + 'pointer_assign', + 'poly_mapping', # length + 'poly_mapping2', + 'read_write_ram', + 'real', + 'real_prop', # reals + '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', +} + +print("Sail is {}".format(sail)) +print("Sail dir is {}".format(sail_dir)) + +def test_sv(name, opts, skip_list): + banner('Testing {} with options:{}'.format(name, opts)) + results = Results(name) + for filenames in chunks(os.listdir('../c'), parallel()): + tests = {} + for filename in filenames: + basename = os.path.splitext(os.path.basename(filename))[0] + if basename in skip_list: + print_skip(filename) + continue + tests[filename] = os.fork() + if tests[filename] == 0: + if basename.startswith('fail'): + step('{} -no_warn -sv ../c/{} -o {} -sv_verilate compile{} > {}.out'.format(sail, filename, basename, opts, basename)) + else: + step('{} -no_warn -sv ../c/{} -o {} -sv_verilate run{} > {}.out'.format(sail, filename, basename, opts, basename)) + step('awk \'/TEST START/{{flag=1;next}}/TEST END/{{flag=0}}flag\' {}.out > {}.result'.format(basename, basename)) + step('diff ../c/{}.expect {}.result'.format(basename, basename)) + print_ok(filename) + sys.exit() + results.collect(tests) + return results.finish() + +xml = '\n' + +xml += test_sv('SystemVerilog', '', skip_tests) +xml += test_sv('SystemVerilog', ' -Oconstant_fold', skip_tests) +xml += test_sv('SystemVerilog', ' -sv_specialize 2', skip_tests) + +skip_tests.remove('bitvector') + +xml += test_sv('SystemVerilog', ' -sv_int_size 128 -sv_bits_size 256', skip_tests) + +xml += '\n' + +output = open('tests.xml', 'w') +output.write(xml) +output.close()