Assorted bug fixes (#1637)

* Fix an outdated comment

* Fix an issue where --c-no-mangle could cause name clashes

Fix issues with recent Verilator versions.

- The --sv-padding option is removed. It is now always on, as this
  behaviour is technically required by the SystemVerilog spec and
  Verilator now enforces this.

- Verilator is now stricter about hextoa, bintoa, and itoa.
  Use $sformatf directly.

Add a regression test for 1555

Author: Alasdair

src/lib/constant_fold.ml

@@ -157,7 +157,7 @@ let rec run frame =
   | Interpreter.Effect_request _ -> assert false (* effectful, raise exception to abort constant folding *)
 
 (** This rewriting pass looks for function applications (E_app) expressions where every argument is a literal. It passes
-    these expressions to the OCaml interpreter in interpreter.ml, and reconstructs the values returned back into
+    these expressions to the Rocq-derived interpreter in interpreter.ml, and reconstructs the values returned back into
     expressions which are then re-typechecked and re-inserted back into the AST.
 
     We don't use the effect system to decide if expressions are safe to evaluate, because this ignores I/O, and would

src/sail_c_backend/c_backend.ml

@@ -989,7 +989,8 @@ module Codegen (Config : CODEGEN_CONFIG) = struct
   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_sail_prefix s = has_prefix "sail_" s || has_prefix "Sail_" s || has_prefix "SAIL_" s
+  let has_bad_prefix s =
+    has_prefix "sail_" s || has_prefix "Sail_" s || has_prefix "SAIL_" s || has_prefix "undefined_" s
 
   (* Prefix to function name in definitions. *)
   let class_impl_prefix () = if Config.cpp then Config.cpp_class_name ^ "::" else ""
@@ -1013,7 +1014,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct
             && (not (Util.StringSet.mem s Keywords.c_reserved_words))
             && (not (Util.StringSet.mem s Keywords.c_used_words))
             && (not (Util.StringSet.mem s Config.reserved_words))
-            && (not (has_sail_prefix s))
+            && (not (has_bad_prefix s))
             && not (c_int_type_name s)
           in
           (not Config.no_mangle) || valid_name s

src/sail_sv_backend/generate_primop2.ml

@@ -157,43 +157,27 @@ module Make
             (* If the width is a multiple of four, format as hexadecimal.
              We take care to ensure the formatting is identical to other
              Sail backends. *)
-            let zeros = Jib_util.name (mk_id "zeros") in
             let bstr = Jib_util.name (mk_id "bstr") in
             if width mod 4 = 0 then (
               let zeros_init = String.make (width / 4) '0' in
               [
-                SVS_var (zeros, CT_string, None);
                 SVS_var (bstr, CT_string, None);
-                svs_raw "bstr.hextoa(b)" ~inputs:[b] ~outputs:[bstr];
-                svs_raw (sprintf "zeros = \"%s\"" zeros_init) ~outputs:[zeros];
-                svs_raw
-                  (sprintf
-                     "out_str = {in_str, s, $sformatf(\"0x%%s\", zeros.substr(0, %d - bstr.len()), bstr.toupper()), \
-                      \"\\n\"}"
-                     ((width / 4) - 1)
-                  )
-                  ~inputs:[in_str; s; zeros; bstr] ~outputs:[out_str];
+                svs_raw "bstr = $sformatf(\"%h\", b)" ~inputs:[b] ~outputs:[bstr];
+                svs_raw "out_str = {in_str, s, \"0x\", bstr.toupper(), \"\\n\"}" ~inputs:[in_str; s; bstr]
+                  ~outputs:[out_str];
                 SVS_assign (SVP_id Jib_util.return, Unit);
               ]
               |> List.map mk_statement
             )
-            else (
-              let zeros_init = String.make width '0' in
+            else
               [
-                SVS_var (zeros, CT_string, None);
                 SVS_var (bstr, CT_string, None);
-                svs_raw "bstr.bintoa(b)" ~inputs:[b] ~outputs:[bstr];
-                svs_raw (sprintf "zeros = \"%s\"" zeros_init) ~outputs:[zeros];
-                svs_raw
-                  (sprintf
-                     "out_str = {in_str, s, $sformatf(\"0b%%s\", zeros.substr(0, %d - bstr.len())), bstr, \"\\n\"}"
-                     (width - 1)
-                  )
-                  ~inputs:[in_str; s; bstr; zeros] ~outputs:[out_str];
+                svs_raw "bstr = $sformatf(\"%b\", b)" ~inputs:[b] ~outputs:[bstr];
+                svs_raw "out_str = {in_str, s, \"0b\", bstr.toupper(), \"\\n\"}" ~inputs:[in_str; s; bstr]
+                  ~outputs:[out_str];
                 SVS_assign (SVP_id Jib_util.return, Unit);
               ]
               |> List.map mk_statement
-            )
           )
         in
         SVD_module
@@ -231,8 +215,8 @@ module Make
                         (List.map mk_statement
                            [
                              svs_raw (sprintf "zeros = \"%s\"" (String.make width '0')) ~outputs:[zeros];
-                             svs_raw (sprintf "hexstr.hextoa(b.sb_bits)") ~inputs:[b] ~outputs:[hexstr];
-                             svs_raw (sprintf "binstr.bintoa(b.sb_bits)") ~inputs:[b] ~outputs:[binstr];
+                             svs_raw (sprintf "hexstr.hextoa(int'(b.sb_bits))") ~inputs:[b] ~outputs:[hexstr];
+                             svs_raw (sprintf "binstr.bintoa(int'(b.sb_bits))") ~inputs:[b] ~outputs:[binstr];
                              svs_raw
                                (sprintf "%s = {in_str, s}" (string_of_name ~zencode:false (tempstr 0)))
                                ~inputs:[in_str; s]
@@ -306,15 +290,15 @@ module Make
           if Config.no_strings then [svs_raw "return SAIL_UNIT"]
           else if width mod 4 = 0 then
             [
-              svs_raw "bstr.hextoa(b)" ~inputs:[b] ~outputs:[bstr];
+              svs_raw "bstr.hextoa(int'(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 "bstr.bintoa(int'(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];
             ]
@@ -374,7 +358,7 @@ module Make
                             SVS_var (n, CT_bool, None);
                             SVS_var (p, CT_string, None);
                             svs_raw "is_negative = signed'(i) < 0" ~inputs:[i] ~outputs:[n];
-                            svs_raw "s.hextoa(is_negative ? (-i) : i)" ~inputs:[i; n] ~outputs:[s];
+                            svs_raw "s = $sformatf(\"%0h\", is_negative ? (-i) : i)" ~inputs:[i; n] ~outputs:[s];
                             svs_raw "prefix = is_negative ? \"-0x\" : \"0x\"" ~inputs:[n] ~outputs:[p];
                             SVS_return (Fn ("str.++", [Var p; Var s]));
                           ]
@@ -407,7 +391,7 @@ module Make
                             SVS_var (n, CT_bool, None);
                             SVS_var (p, CT_string, None);
                             svs_raw "is_negative = signed'(i) < 0" ~inputs:[i] ~outputs:[n];
-                            svs_raw "s.hextoa(is_negative ? (-i) : i)" ~inputs:[i; n] ~outputs:[s];
+                            svs_raw "s = $sformatf(\"%0h\", is_negative ? (-i) : i)" ~inputs:[i; n] ~outputs:[s];
                             svs_raw "s = s.toupper()" ~inputs:[s] ~outputs:[s];
                             svs_raw "prefix = is_negative ? \"-0x\" : \"0x\"" ~inputs:[n] ~outputs:[p];
                             SVS_return (Fn ("str.++", [Var p; Var s]));
@@ -436,7 +420,7 @@ module Make
                        (List.map mk_statement
                           [
                             SVS_var (s, CT_string, None);
-                            svs_raw "s.itoa(i)" ~inputs:[i] ~outputs:[s];
+                            svs_raw "s = $sformatf(\"%0d\", i)" ~inputs:[i] ~outputs:[s];
                             SVS_return (Var s);
                           ]
                        )

src/sail_sv_backend/jib_sv.ml

@@ -103,7 +103,6 @@ module type CONFIG = sig
   val no_packed : bool
   val no_assertions : bool
   val never_pack_unions : bool
-  val union_padding : bool
   val no_unions : bool
   val unreachable : string list
   val no_write_flush : bool
@@ -184,14 +183,19 @@ module Make (Config : CONFIG) = struct
   let rec bit_width ctx = function
     | CT_unit | CT_bool -> Some 1
     | CT_fbits len -> Some len
-    | CT_lbits -> Some Config.max_unknown_bitvector_width
+    | CT_lbits ->
+        let w = Config.max_unknown_bitvector_width in
+        Some (required_width (Big_int.of_int (w - 1)) + 1 + w)
     | CT_enum enum_id ->
         let members = Jib_compile.enum_members Parse_ast.Unknown ctx enum_id in
         Some (required_width (Big_int.of_int (IdSet.cardinal members - 1)))
     | CT_constant c -> Some (required_width c)
     | CT_variant _ as ctyp ->
+        let open Util.Option_monad in
         let ctors = Jib_compile.variant_constructor_bindings Parse_ast.Unknown ctx ctyp |> snd |> Bindings.bindings in
-        List.map (fun (_, ctyp) -> bit_width ctx ctyp) ctors |> Util.option_all |> Option.map (List.fold_left max 1)
+        let* ctor_widths = List.map (fun (_, ctyp) -> bit_width ctx ctyp) ctors |> Util.option_all in
+        let max_width = List.fold_left max 1 ctor_widths in
+        Some (max_width + required_width (Big_int.of_int (List.length ctors - 1)))
     | CT_struct _ as ctyp ->
         let fields = Jib_compile.struct_field_bindings Parse_ast.Unknown ctx ctyp |> snd |> Bindings.bindings in
         List.map (fun (_, ctyp) -> bit_width ctx ctyp) fields |> Util.option_all |> Option.map (List.fold_left ( + ) 0)
@@ -319,7 +323,9 @@ module Make (Config : CONFIG) = struct
         Reporting.unreachable (id_loc id) __POS__ "Abstract types not supported for SystemVerilog target"
     | CTD_abbrev _ -> empty
     | CTD_enum (id, ids) ->
-        string "typedef" ^^ space ^^ string "enum" ^^ space
+        let width = required_width (Big_int.of_int (List.length ids - 1)) in
+        let width_doc = lbracket ^^ string (string_of_int (width - 1)) ^^ colon ^^ char '0' ^^ rbracket in
+        string "typedef" ^^ space ^^ string "enum" ^^ space ^^ width_doc ^^ space
         ^^ group (lbrace ^^ nest 4 (hardline ^^ separate_map (comma ^^ hardline) pp_id ids) ^^ hardline ^^ rbrace)
         ^^ space ^^ sv_type_id id ^^ semi
     | CTD_struct (id, _, fields) ->
@@ -339,11 +345,13 @@ module Make (Config : CONFIG) = struct
         let sv_ctor (id, ctyp) = wrap_type ctyp (pp_id id) in
         let tag_type = string ("sailtag_" ^ pp_id_string id) in
         let value_type = string ("sailunion_" ^ pp_id_string id) in
+        let tag_width = required_width (Big_int.of_int (List.length ctors - 1)) in
         let kind_enum =
           separate space
             [
               string "typedef";
               string "enum";
+              lbracket ^^ string (string_of_int (tag_width - 1)) ^^ colon ^^ char '0' ^^ rbracket;
               group (lbrace ^^ nest 4 (hardline ^^ separate_map (comma ^^ hardline) kind_id ctors) ^^ hardline ^^ rbrace);
               tag_type ^^ semi;
             ]
@@ -393,84 +401,54 @@ module Make (Config : CONFIG) = struct
               ctors
           in
           let constructors =
-            if Config.union_padding then
-              List.map
-                (fun (_, (ctor_id, ctyp, padding_type, required_padding)) ->
-                  separate space [string "function"; string "automatic"; sv_type_id id; pp_id ctor_id]
-                  ^^ parens (wrap_type ctyp (char 'v'))
-                  ^^ semi
-                  ^^ nest 4
-                       (hardline ^^ sv_type_id id ^^ space ^^ char 'r' ^^ semi ^^ hardline
-                       ^^ string ("sailunion_" ^ pp_id_string id)
-                       ^^ space ^^ char 'u' ^^ semi ^^ hardline ^^ padding_type ^^ space ^^ char 'p' ^^ 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 'p' ^^ dot ^^ pp_id ctor_id; equals; char 'v']
-                       ^^ semi ^^ hardline
-                       ^^ ( if required_padding > 0 then
-                              separate space
-                                [
-                                  char 'p' ^^ dot ^^ string "padding";
-                                  equals;
-                                  ksprintf string "%d'b%s" required_padding (String.make required_padding '0');
-                                ]
-                              ^^ semi ^^ hardline
-                            else empty
-                          )
-                       ^^ separate space [char 'u' ^^ dot ^^ pp_id ctor_id; equals; char 'p']
-                       ^^ semi ^^ hardline
-                       ^^ separate space [string "r.value"; equals; char 'u']
-                       ^^ semi ^^ hardline ^^ string "return" ^^ space ^^ char 'r' ^^ semi
-                       )
-                  ^^ hardline ^^ string "endfunction"
-                )
-                padding_structs
-            else
-              List.map
-                (fun (ctor_id, ctyp) ->
-                  separate space [string "function"; string "automatic"; sv_type_id id; pp_id ctor_id]
-                  ^^ parens (wrap_type ctyp (char 'v'))
-                  ^^ semi
-                  ^^ nest 4
-                       (hardline ^^ sv_type_id id ^^ space ^^ char 'r' ^^ semi ^^ hardline
-                       ^^ string ("sailunion_" ^ pp_id_string id)
-                       ^^ space ^^ char '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 ^^ pp_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
+            List.map
+              (fun (_, (ctor_id, ctyp, padding_type, required_padding)) ->
+                separate space [string "function"; string "automatic"; sv_type_id id; pp_id ctor_id]
+                ^^ parens (wrap_type ctyp (char 'v'))
+                ^^ semi
+                ^^ nest 4
+                     (hardline ^^ sv_type_id id ^^ space ^^ char 'r' ^^ semi ^^ hardline
+                     ^^ string ("sailunion_" ^ pp_id_string id)
+                     ^^ space ^^ char 'u' ^^ semi ^^ hardline ^^ padding_type ^^ space ^^ char 'p' ^^ 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 'p' ^^ dot ^^ pp_id ctor_id; equals; char 'v']
+                     ^^ semi ^^ hardline
+                     ^^ ( if required_padding > 0 then
+                            separate space
+                              [
+                                char 'p' ^^ dot ^^ string "padding";
+                                equals;
+                                ksprintf string "%d'b%s" required_padding (String.make required_padding '0');
+                              ]
+                            ^^ semi ^^ hardline
+                          else empty
+                        )
+                     ^^ separate space [char 'u' ^^ dot ^^ pp_id ctor_id; equals; char 'p']
+                     ^^ semi ^^ hardline
+                     ^^ separate space [string "r.value"; equals; char 'u']
+                     ^^ semi ^^ hardline ^^ string "return" ^^ space ^^ char 'r' ^^ semi
+                     )
+                ^^ hardline ^^ string "endfunction"
+              )
+              padding_structs
           in
           let sv_padded_ctor (_, (ctor_id, _, padding_type, _)) = padding_type ^^ space ^^ pp_id ctor_id in
-          (if Config.union_padding then separate_map (twice hardline) fst padding_structs ^^ twice hardline else empty)
+          separate_map (twice hardline) fst padding_structs
+          ^^ twice hardline
           ^^ separate space
                [
                  string "typedef";
                  (if Config.no_unions then string "struct" else string "union");
                  string "packed";
                  group
                    (lbrace
-                   ^^ nest 4
-                        (hardline
-                        ^^
-                        if Config.union_padding then separate_map (semi ^^ hardline) sv_padded_ctor padding_structs
-                        else separate_map (semi ^^ hardline) sv_ctor ctors
-                        )
+                   ^^ nest 4 (hardline ^^ separate_map (semi ^^ hardline) sv_padded_ctor padding_structs)
                    ^^ semi ^^ hardline ^^ rbrace
                    );
                  value_type ^^ semi;
@@ -666,7 +644,7 @@ module Make (Config : CONFIG) = struct
              [pp_smt v ^^ dot ^^ string "tag"; string "=="; string (ctor |> zencode_id |> String.uppercase_ascii)]
           )
     | Unwrap (ctor, packed, v) ->
-        let packed_ctor = if Config.union_padding then pp_id ctor ^^ dot ^^ pp_id ctor else pp_id ctor in
+        let packed_ctor = pp_id ctor ^^ dot ^^ pp_id ctor in
         if packed then pp_smt v ^^ dot ^^ string "value" ^^ dot ^^ packed_ctor else pp_smt v ^^ dot ^^ pp_id ctor
     | Field (_, field, v) -> pp_smt v ^^ dot ^^ pp_id field
     | Ite (cond, then_exp, else_exp) ->

src/sail_sv_backend/jib_sv.mli

@@ -78,7 +78,6 @@ module type CONFIG = sig
   val no_assertions : bool
 
   val never_pack_unions : bool
-  val union_padding : bool
   val no_unions : bool
   val unreachable : string list
   val no_write_flush : bool

src/sail_sv_backend/sail_plugin_sv.ml

@@ -101,7 +101,6 @@ let opt_no_strings = ref false
 let opt_no_packed = ref false
 let opt_no_assertions = ref false
 let opt_never_pack_unions = ref false
-let opt_padding = ref false
 let opt_no_unions = ref false
 let opt_nomem = ref false
 let opt_no_assert_fatal = ref false
@@ -198,7 +197,6 @@ let verilog_options =
     (Flag.create ~prefix:["sv"] "no_packed", Arg.Set opt_no_packed, "don't emit packed datastructures");
     (Flag.create ~prefix:["sv"] "no_assertions", Arg.Set opt_no_assertions, "ignore all Sail asserts");
     (Flag.create ~prefix:["sv"] "never_pack_unions", Arg.Set opt_never_pack_unions, "never emit a packed union");
-    (Flag.create ~prefix:["sv"] "padding", Arg.Set opt_padding, "add padding on packed unions");
     ( Flag.create ~prefix:["sv"] ~arg:"functionname" "unreachable",
       Arg.String (fun fn -> opt_unreachable := fn :: !opt_unreachable),
       "Mark function as unreachable."
@@ -486,7 +484,6 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } =
     let no_packed = !opt_no_packed
     let no_assertions = !opt_no_assertions
     let never_pack_unions = !opt_never_pack_unions
-    let union_padding = !opt_padding
     let no_unions = !opt_no_unions
     let unreachable = !opt_unreachable
     let comb = !opt_comb

test/c/issue1555.expect

@@ -0,0 +1 @@
+Is B