diff --git a/src/lib/jib_ssa.ml b/src/lib/jib_ssa.ml index 8b71543ce..b78b195ce 100644 --- a/src/lib/jib_ssa.ml +++ b/src/lib/jib_ssa.ml @@ -892,4 +892,4 @@ let ssa ?globals ?debug_prefix instrs = place_phi_functions cfg df; rename_variables (Option.value ~default:NameSet.empty globals) cfg start children; place_pi_functions ~start ~finish ~post_idom ~post_df cfg; - (start, cfg) + (start, finish, cfg) diff --git a/src/lib/jib_ssa.mli b/src/lib/jib_ssa.mli index 5f50eb276..797d8303e 100644 --- a/src/lib/jib_ssa.mli +++ b/src/lib/jib_ssa.mli @@ -131,7 +131,8 @@ end val phi_dependencies : (ssa_elem list * cf_node) array_graph -> NameGraph.graph * int NameMap.t (** Convert a list of instructions into SSA form *) -val ssa : ?globals:NameSet.t -> ?debug_prefix:string -> Jib.instr list -> int * (ssa_elem list * cf_node) array_graph +val ssa : + ?globals:NameSet.t -> ?debug_prefix:string -> Jib.instr list -> int * int * (ssa_elem list * cf_node) array_graph (** Output the control-flow graph in graphviz format for debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 1378f5809..a36e7db42 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -709,7 +709,7 @@ module Make (Config : CONFIG) = struct let stack = Stack.create () in let open Jib_ssa in - let start, cfg = ssa ?debug_prefix:(Option.map (fun _ -> name) debug_attr) instrs in + let start, _, cfg = ssa ?debug_prefix:(Option.map (fun _ -> name) debug_attr) instrs in let visit_order = try topsort cfg with Not_a_DAG n -> diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 36466eb44..5c7792dbc 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -1438,6 +1438,13 @@ module Make (Config : CONFIG) = struct attribute_data_bool skip_graph ) + let never_returns end_node cfg = + let open Jib_ssa in + let _, preds, _ = Option.get (get_vertex cfg end_node) in + IntSet.for_all + (fun pred -> match get_vertex cfg pred with Some ((_, CF_block (_, T_exit _)), _, _) -> true | _ -> false) + preds + let svir_module debug_attr spec_info ctx f params param_ctyps ret_ctyp body = prerr_endline Util.(string_of_id f |> red |> clear); let footprint = Bindings.find f spec_info.footprints in @@ -1455,12 +1462,14 @@ module Make (Config : CONFIG) = struct (List.map (fun (I_aux (_, (_, l)) as instr) -> string_of_instr instr ^ " " ^ Reporting.short_loc_to_string l) body); let open Jib_ssa in - let start, cfg = + let _, end_node, cfg = ssa ~globals:spec_info.global_lets ?debug_prefix:(Option.map (fun _ -> string_of_id f) debug_attr) (visit_instrs (new thread_registers ctx spec_info) body) in + if never_returns end_node cfg then prerr_endline "NEVER RETURNS"; + if Option.is_some debug_attr && not (debug_attr_skip_graph debug_attr) then dump_graph (string_of_id f) cfg; let visit_order = @@ -1565,8 +1574,10 @@ module Make (Config : CONFIG) = struct | name -> name in + let get_final_name name = match NameMap.find_opt name final_names with Some n -> n | None -> name in + let output_ports : sv_module_port list = - [{ name = NameMap.find Jib_util.return final_names; external_name = "sail_return"; typ = ret_ctyp }] + [{ name = get_final_name Jib_util.return; external_name = "sail_return"; typ = ret_ctyp }] @ List.map (fun id -> { @@ -1578,9 +1589,9 @@ module Make (Config : CONFIG) = struct (IdSet.elements footprint.all_writes) @ ( if footprint.throws then [ - { name = NameMap.find (Have_exception (-1)) final_names; external_name = "have_exception"; typ = CT_bool }; + { name = get_final_name (Have_exception (-1)); external_name = "have_exception"; typ = CT_bool }; { - name = NameMap.find (Current_exception (-1)) final_names; + name = get_final_name (Current_exception (-1)); external_name = "current_exception"; typ = spec_info.exception_ctyp; }; @@ -2005,10 +2016,6 @@ module Make (Config : CONFIG) = struct let debug_attr = get_def_attribute "jib_debug" def_annot in if List.mem (string_of_id f) Config.ignore then ([], fn_ctyps) else ( - if Option.is_some debug_attr then ( - prerr_endline Util.("Pre-SV IR for " ^ string_of_id f ^ ":" |> yellow |> bold |> clear); - List.iter (fun instr -> prerr_endline (string_of_instr instr)) body - ); let body = Jib_optimize.( body |> remove_undefined |> remove_functions_to_references |> flatten_instrs |> remove_dead_code diff --git a/test/c/short_circuit.sail b/test/c/short_circuit.sail index 8289efa66..3ad83566a 100644 --- a/test/c/short_circuit.sail +++ b/test/c/short_circuit.sail @@ -19,4 +19,4 @@ function main () = { } else { print("ok"); } -} \ No newline at end of file +} diff --git a/test/sailtest.py b/test/sailtest.py index 5f0fa155e..08b076d3e 100644 --- a/test/sailtest.py +++ b/test/sailtest.py @@ -3,6 +3,19 @@ import sys import subprocess import datetime +import argparse + +parser = argparse.ArgumentParser("run_tests.py") +parser.add_argument("--hide-errors", help="Hide error information.", action='store_true') +parser.add_argument("--compact", help="Compact output.", action='store_true') +args = parser.parse_args() + +def is_compact(): + return args.compact + +def compact_char(code, char): + print('{}{}{}'.format(code, char, color.END), end='') + sys.stdout.flush() class color: NOTICE = '\033[94m' @@ -33,10 +46,16 @@ def get_sail_dir(): sys.exit(1) def print_ok(name): - print('{} {}{}{}'.format('{} '.format(name).ljust(40, '.'), color.PASS, 'ok', color.END)) + if is_compact(): + compact_char(color.PASS, '.') + else: + print('{} {}{}{}'.format('{} '.format(name).ljust(40, '.'), color.PASS, 'ok', color.END)) def print_skip(name): - print('{} {}{}{}'.format('{} '.format(name).ljust(40, '.'), color.WARNING, 'skip', color.END)) + if is_compact(): + compact_char(color.WARNING, 's') + else: + print('{} {}{}{}'.format('{} '.format(name).ljust(40, '.'), color.WARNING, 'skip', color.END)) def get_sail(): try: @@ -68,11 +87,15 @@ def step(string, expected_status=0): out, err = p.communicate() status = p.wait() if status != expected_status: - print("{}Failed{}: {}".format(color.FAIL, color.END, string)) - print('{}stdout{}:'.format(color.NOTICE, color.END)) - print(out.decode('utf-8')) - print('{}stderr{}:'.format(color.NOTICE, color.END)) - print(err.decode('utf-8')) + if is_compact(): + compact_char(color.FAIL, 'X') + else: + print("{}Failed{}: {}".format(color.FAIL, color.END, string)) + if not args.hide_errors: + print('{}stdout{}:'.format(color.NOTICE, color.END)) + print(out.decode('utf-8')) + print('{}stderr{}:'.format(color.NOTICE, color.END)) + print(err.decode('utf-8')) sys.exit(1) def banner(string): @@ -120,6 +143,8 @@ def collect(self, tests): def finish(self): xfail_msg = f' ({self.xfails} expected failures)' if self.xfails else '' + if is_compact(): + print() print('{}{} passes and {} failures{}{}'.format(color.NOTICE, self.passes, self.failures, xfail_msg, color.END)) time = datetime.datetime.utcnow() diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py index d36926662..66e4b0f96 100755 --- a/test/sv/run_tests.py +++ b/test/sv/run_tests.py @@ -47,6 +47,14 @@ 'warl_undef', 'xlen_val', # Calls external C function 'spc_mappings', + 'list_test', # lists + 'list_scope', # lists + 'list_scope2', # lists + 'list_scope3', # lists + 'list_cons_cons', # lists + 'lib_hex_bits', # bitvector parsing + 'lib_hex_bits_signed', # bitvector parsing + 'lib_valid_hex_bits', # bitvector parsing } print("Sail is {}".format(sail))