Additional tests for Sail->SV

Add some options to the Sail test script to add more compact output

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)

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

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 ->

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

test/c/short_circuit.sail

@@ -19,4 +19,4 @@ function main () = {
   } else {
     print("ok");
   }
-}
+}

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()

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))