Further Sail->SV fixes (rems-project#586)

* Fix some Sail->SV tests with exceptions

* Update vector width and fix array assignment in Sail->SV

* More test fixes

lib/sv/sail_modules.sv

@@ -4,6 +4,9 @@
 // The Sail unit type.
 typedef enum logic [0:0] {SAIL_UNIT=0} sail_unit;
 
+// The Sail zero-width bitvector.
+typedef enum logic [0:0] {SAIL_ZWBV=0} sail_zwbv;
+
 module print
   (input string     in_str,
    input string     in_sail_stdout,

src/lib/jib_optimize.ml

@@ -185,8 +185,13 @@ let rec cval_map_id f = function
   | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_map_id f cval)) fields, ctyp)
   | V_tuple (members, ctyp) -> V_tuple (List.map (cval_map_id f) members, ctyp)
 
-let remove_undefined =
-  let gensym, _ = symbol_generator "gz" in
+module Remove_undefined = struct
+  open Jib
+  open Jib_util
+  open Jib_visitor
+
+  let gensym, _ = symbol_generator "gz"
+
   let rec create_value l = function
     | CT_unit -> ([], V_lit (VL_unit, CT_unit))
     | CT_bool -> ([], V_lit (VL_bool false, CT_bool))
@@ -205,16 +210,56 @@ let remove_undefined =
     | ctyp ->
         let gs = name (gensym ()) in
         ([idecl l ctyp gs], V_id (gs, ctyp))
-  in
-  let rewrite_instr = function
-    | I_aux (I_undefined ctyp, (_, l)) ->
-        let setup, value = create_value l ctyp in
-        begin
-          match setup with [] -> ireturn value | _ -> iblock (setup @ [ireturn value])
-        end
-    | instr -> instr
-  in
-  map_instr_list rewrite_instr
+
+  class visitor : jib_visitor =
+    object
+      inherit empty_jib_visitor
+
+      method! vctyp _ = SkipChildren
+      method! vcval _ = SkipChildren
+
+      method! vinstr =
+        function
+        | I_aux (I_undefined ctyp, (_, l)) ->
+            let setup, value = create_value l ctyp in
+            ChangeTo (iblock (setup @ [icopy l (CL_id (return, ctyp)) value; iend l]))
+        | _ -> DoChildren
+    end
+end
+
+let remove_undefined = Jib_visitor.visit_instrs (new Remove_undefined.visitor)
+
+module Remove_functions_to_references = struct
+  open Jib
+  open Jib_util
+  open Jib_visitor
+
+  let gensym, _ = symbol_generator "gref"
+
+  class visitor : jib_visitor =
+    object
+      inherit empty_jib_visitor
+
+      method! vctyp _ = SkipChildren
+      method! vcval _ = SkipChildren
+
+      method! vinstr =
+        function
+        | I_aux (I_funcall (CR_one (CL_addr (CL_id (id, CT_ref reg_ctyp))), ext, f, args), (n, l)) ->
+            let gs = name (gensym ()) in
+            ChangeTo
+              (iblock
+                 [
+                   idecl l reg_ctyp gs;
+                   I_aux (I_funcall (CR_one (CL_id (gs, reg_ctyp)), ext, f, args), (n, l));
+                   icopy l (CL_addr (CL_id (id, CT_ref reg_ctyp))) (V_id (gs, reg_ctyp));
+                 ]
+              )
+        | _ -> DoChildren
+    end
+end
+
+let remove_functions_to_references = Jib_visitor.visit_instrs (new Remove_functions_to_references.visitor)
 
 let rec instrs_subst id subst = function
   | I_aux (I_decl (_, id'), _) :: _ as instrs when Name.compare id id' = 0 -> instrs

src/lib/jib_optimize.mli

@@ -86,6 +86,8 @@ val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list
 
 val remove_undefined : instr list -> instr list
 
+val remove_functions_to_references : instr list -> instr list
+
 val remove_clear : instr list -> instr list
 
 (** Remove gotos immediately followed by the label it jumps to *)

src/lib/jib_ssa.ml

@@ -532,7 +532,7 @@ let phi_dependencies cfg =
   done;
   (!deps, !decl_nodes)
 
-let rename_variables graph root children =
+let rename_variables globals graph root children =
   let counts = ref NameMap.empty in
   let stacks = ref NameMap.empty in
 
@@ -554,8 +554,11 @@ let rename_variables graph root children =
 
   let rec fold_cval = function
     | V_id (id, ctyp) ->
-        let i = top_stack id in
-        V_id (ssa_name i id, ctyp)
+        if NameSet.mem id globals then V_id (id, ctyp)
+        else (
+          let i = top_stack id in
+          V_id (ssa_name i id, ctyp)
+        )
     | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
@@ -862,8 +865,16 @@ let make_dominators_dot out_chan idom graph =
   output_string out_chan "}\n";
   Util.opt_colors := true
 
-let ssa ?debug_prefix instrs =
+let ssa ?globals ?debug_prefix instrs =
   let start, finish, cfg = control_flow_graph instrs in
+  begin
+    match debug_prefix with
+    | Some prefix ->
+        let out_chan = open_out (prefix ^ "_cfg.gv") in
+        make_dot out_chan cfg;
+        close_out out_chan
+    | None -> ()
+  end;
   let idom = immediate_dominators cfg start in
   let post_idom = immediate_dominators ~post:true cfg finish in
   begin
@@ -879,6 +890,6 @@ let ssa ?debug_prefix instrs =
   let df = dominance_frontiers cfg start idom children in
   let post_df = dominance_frontiers ~post:true cfg finish post_idom post_children in
   place_phi_functions cfg df;
-  rename_variables cfg start children;
+  rename_variables (Option.value ~default:NameSet.empty globals) cfg start children;
   place_pi_functions ~start ~finish ~post_idom ~post_df cfg;
   (start, cfg)

src/lib/jib_ssa.mli

@@ -131,7 +131,7 @@ end
 val phi_dependencies : (ssa_elem list * cf_node) array_graph -> NameGraph.graph * int NameMap.t
 
 (** Convert a list of instructions into SSA form *)
-val ssa : ?debug_prefix:string -> Jib.instr list -> int * (ssa_elem list * cf_node) array_graph
+val ssa : ?globals:NameSet.t -> ?debug_prefix:string -> Jib.instr list -> int * (ssa_elem list * cf_node) array_graph
 
 (** Output the control-flow graph in graphviz format for
    debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png

src/lib/jib_util.ml

@@ -1091,6 +1091,13 @@ let ctype_def_ctyps = function
   | CTD_struct (_, fields) -> List.map snd fields
   | CTD_variant (_, ctors) -> List.map snd ctors
 
+let ctype_def_id = function CTD_enum (id, _) -> id | CTD_struct (id, _) -> id | CTD_variant (id, _) -> id
+
+let ctype_def_to_ctyp = function
+  | CTD_enum (id, ids) -> CT_enum (id, ids)
+  | CTD_struct (id, fields) -> CT_struct (id, fields)
+  | CTD_variant (id, ctors) -> CT_variant (id, ctors)
+
 let cdef_ctyps (CDEF_aux (aux, _)) =
   match aux with
   | CDEF_register (_, ctyp, instrs) -> CTSet.add ctyp (instrs_ctyps instrs)

src/lib/jib_util.mli

@@ -191,6 +191,12 @@ val cdef_ctyps : cdef -> CTSet.t
 
 val cdef_ctyps_has : (ctyp -> bool) -> cdef -> bool
 
+(** {2 Type definitions} *)
+
+val ctype_def_id : ctype_def -> id
+
+val ctype_def_to_ctyp : ctype_def -> ctyp
+
 (** {1 Functions for mapping over and extracting information from instructions, values, and definitions} *)
 
 val instr_ids : instr -> NameSet.t

src/lib/smt_exp.ml

@@ -108,6 +108,8 @@ type smt_exp =
   | Hd of string * smt_exp
   | Tl of string * smt_exp
 
+let var_id id = Var (Name (id, -1))
+
 let rec fold_smt_exp f = function
   | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args))
   | Ite (cond, t, e) -> f (Ite (fold_smt_exp f cond, fold_smt_exp f t, fold_smt_exp f e))
@@ -164,9 +166,13 @@ let simp_or xs =
   | [x] -> x
   | _ -> if List.exists (function Bool_lit true -> true | _ -> false) xs then Bool_lit true else Fn ("or", xs)
 
+let simp_eq x y =
+  match (x, y) with Bool_lit x, Bool_lit y -> Some (x = y) | Bitvec_lit x, Bitvec_lit y -> Some (x = y) | _ -> None
+
 let simp_fn f args =
   let open Sail2_operators_bitlists in
   match (f, args) with
+  | "=", [x; y] -> begin match simp_eq x y with Some b -> Bool_lit b | None -> Fn (f, args) end
   | "not", [Fn ("not", [exp])] -> exp
   | "not", [Bool_lit b] -> Bool_lit (not b)
   | "contents", [Fn ("Bits", [_; bv])] -> bv
@@ -233,8 +239,13 @@ let rec simp vars exp =
       | exp -> Extract (n, m, exp)
     end
   | Store (info, store_fn, arr, i, x) -> Store (info, store_fn, simp vars arr, simp vars i, simp vars x)
-  | Ite (Fn ("not", [cond]), then_exp, else_exp) -> simp vars (Ite (cond, else_exp, then_exp))
-  | Ite (cond, then_exp, else_exp) -> Ite (simp vars cond, simp vars then_exp, simp vars else_exp)
+  | Ite (cond, then_exp, else_exp) -> begin
+      match Ite (simp vars cond, simp vars then_exp, simp vars else_exp) with
+      | Ite (Bool_lit true, then_exp, _) -> then_exp
+      | Ite (Bool_lit false, _, else_exp) -> else_exp
+      | Ite (Fn ("not", [cond]), then_exp, else_exp) -> Ite (cond, else_exp, then_exp)
+      | exp -> exp
+    end
   | Tester (ctor, exp) -> Tester (ctor, simp vars exp)
   | Unwrap (ctor, b, exp) -> Unwrap (ctor, b, simp vars exp)
   | Field (struct_id, field_id, exp) -> Field (struct_id, field_id, simp vars exp)

src/lib/smt_gen.ml

@@ -919,7 +919,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         let* vec = smt_cval vec in
         let* i =
           bind (smt_cval i)
-            (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp))
+            (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp))
         in
         return (Fn ("select", [vec; i]))
         (*
@@ -998,7 +998,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         let* x = smt_cval x in
         let* i =
           bind (smt_cval i)
-            (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp))
+            (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp))
         in
         return (Store (Fixed len, store_fn, vec, i, x))
     (*

src/sail_smt_backend/jib_smt.ml

@@ -320,7 +320,7 @@ module Make (Config : CONFIG) = struct
         return (mk_variant (zencode_upper_id id) ctors)
     | CT_fvector (n, ctyp) ->
         let* ctyp = smt_ctyp ctyp in
-        return (Array (Bitvec (required_width (Big_int.of_int (n - 1))), ctyp))
+        return (Array (Bitvec (required_width (Big_int.of_int (n - 1)) - 1), ctyp))
     | CT_vector ctyp ->
         let* ctyp = smt_ctyp ctyp in
         return (Array (Bitvec vector_index_width, ctyp))
@@ -571,10 +571,10 @@ module Make (Config : CONFIG) = struct
         else if extern && string_of_id function_id = "internal_vector_update" then begin
           match args with
           | [vec; i; x] ->
-              let sz = required_width (Big_int.of_int (Smt.generic_vector_length (cval_ctyp vec) - 1)) in
+              let sz = required_width (Big_int.of_int (Smt.generic_vector_length (cval_ctyp vec) - 1)) - 1 in
               let* vec = Smt.smt_cval vec in
               let* i =
-                Smt_gen.bind (Smt.smt_cval i) (Smt_gen.signed_size ~into:sz ~from:(Smt.int_size (cval_ctyp i)))
+                Smt_gen.bind (Smt.smt_cval i) (Smt_gen.unsigned_size ~into:sz ~from:(Smt.int_size (cval_ctyp i)))
               in
               let* x = Smt.smt_cval x in
               singleton (define_const id ret_ctyp (Fn ("store", [vec; i; x])))
@@ -841,14 +841,15 @@ module Make (Config : CONFIG) = struct
             List.iter (fun include_file -> output_string out_chan (Util.read_whole_file include_file)) smt_includes;
 
             let queue = Queue_optimizer.optimize stack in
+
+            (* let queue = Queue.of_seq (List.to_seq (List.rev (List.of_seq (Stack.to_seq stack)))) in *)
             Queue.iter
               (fun def ->
                 output_string out_chan (string_of_smt_def def);
                 output_string out_chan "\n"
               )
               queue;
 
-            (* (Queue.of_seq (List.to_seq (List.rev (List.of_seq (Stack.to_seq stack))))); *)
             output_string out_chan "(check-sat)\n";
             if prop_type = "counterexample" then output_string out_chan "(get-model)\n";
 

src/sail_sv_backend/generate_primop2.ml

@@ -74,6 +74,8 @@ module type S = sig
 
   val get_generated_library_defs : unit -> sv_def list
 
+  val string_of_fbits : int -> string
+
   val hex_str : unit -> string
 
   val dec_str : unit -> string
@@ -244,6 +246,38 @@ module Make
           }
     )
 
+  let string_of_fbits width =
+    let function_name = pf "sail_string_of_bits_%d" width in
+    register_library_def function_name (fun () ->
+        let b = primop_name "b" in
+        let bstr = primop_name "bstr" in
+        let zeros = primop_name "zeros" in
+        let vars = [SVS_var (bstr, CT_string, None); SVS_var (zeros, CT_string, None)] in
+        let body =
+          if width mod 4 = 0 then
+            [
+              svs_raw "bstr.hextoa(b)" ~inputs:[b] ~outputs:[bstr];
+              svs_raw (pf "zeros = \"%s\"" (String.make (width / 4) '0')) ~outputs:[zeros];
+              svs_raw
+                (pf "return {\"0x\", zeros.substr(0, %d - bstr.len()), bstr.toupper()}" ((width / 4) - 1))
+                ~inputs:[zeros; bstr];
+            ]
+          else
+            [
+              svs_raw "bstr.bintoa(b)" ~inputs:[b] ~outputs:[bstr];
+              svs_raw (pf "zeros = \"%s\"" (String.make width '0')) ~outputs:[zeros];
+              svs_raw (pf "return {\"0b\", zeros.substr(0, %d - bstr.len()), bstr}" (width - 1)) ~inputs:[zeros; bstr];
+            ]
+        in
+        SVD_fundef
+          {
+            function_name = SVN_string function_name;
+            return_type = Some CT_string;
+            params = [(mk_id "b", CT_fbits width)];
+            body = mk_statement (SVS_block (List.map mk_statement (vars @ body)));
+          }
+    )
+
   let print_int () =
     let name = "sail_print_int" in
     register_library_def name (fun () ->