Add a --warn-error flag

doc/Dockerfile

@@ -1,10 +1,10 @@
 FROM debian
 
-RUN apt-get update && apt-get install -y --no-install-recommends build-essential git ruby ruby-rubygems opam z3 rsync libgmp-dev pkg-config texlive-latex-base texlive-pictures poppler-utils
+RUN apt-get update && apt-get install -y --no-install-recommends build-essential git ruby ruby-dev ruby-rubygems opam z3 rsync libgmp-dev pkg-config texlive-latex-base texlive-pictures poppler-utils
 
 RUN gem install asciidoctor asciidoctor-pdf asciidoctor-bibtex asciidoctor-sail rouge
 
-RUN opam init -y --no-setup --compiler=5.1.0 --shell=sh --disable-sandboxing; eval "$(opam env)"; opam install -y obelisk
+RUN opam init -y --no-setup --compiler=5.5.0 --shell=sh --disable-sandboxing; eval "$(opam env)"; opam install -y obelisk
 
 WORKDIR /sail
 COPY . /sail

src/bin/sail.ml

@@ -49,11 +49,6 @@ open Libsail
 open Interactive.State
 open Sail_options
 
-type version = { major : int; minor : int; patch : int }
-
-(* Current version of Sail. Must be updated manually. *)
-let version = { major = 0; minor = 20; patch = 2 }
-
 let opt_new_cli = ref false
 let opt_free_arguments : string list ref = ref []
 let opt_file_out : string option ref = ref None
@@ -82,6 +77,7 @@ let opt_format_skip : string list ref = ref []
 let opt_format_debug : bool ref = ref false
 let opt_slice_instantiation_types : bool ref = ref false
 let opt_output_schema_file : string option ref = ref None
+let opt_warn_error : bool ref = ref false
 
 let is_bytecode = Sys.backend_type = Bytecode
 
@@ -100,7 +96,8 @@ let rec fix_options = function
             let explanation =
               Printf.sprintf "Old style command line flag %s used, use %s instead" flag canonical_flag
             in
-            Arg.Tuple [Arg.Unit (fun () -> Reporting.warn "Old style flag" Parse_ast.Unknown explanation); spec]
+            Arg.Tuple
+              [Arg.Unit (fun () -> Reporting.warn Version.v0_20_2 "Old style flag" Parse_ast.Unknown explanation); spec]
           )
           else spec
         in
@@ -183,28 +180,13 @@ let parse_instantiation inst =
   | _ -> raise (Reporting.err_general Parse_ast.Unknown "Failed to parse command-line instantiate flag")
 
 (* Version as a string, e.g. "1.2.3". *)
-let version_string = Printf.sprintf "%d.%d.%d" version.major version.minor version.patch
+let version_string = Version.to_string Version.current
 
 (* Full version string including Git branch & commit. *)
 let version_full =
   let open Manifest in
   Printf.sprintf "Sail %s (%s @ %s)" version_string branch commit
 
-(* Convert a string like "1.2.3" to a list [1; 2; 3] *)
-let parse_version dotted_version =
-  let open Util.Option_monad in
-  let* version = String.split_on_char '.' dotted_version |> List.map int_of_string_opt |> Util.option_all in
-  match version with
-  | [major; minor; patch] -> Some { major; minor; patch }
-  | [major; minor] -> Some { major; minor; patch = 0 }
-  | [major] -> Some { major; minor = 0; patch = 0 }
-  | _ -> None
-
-let version_check ~required =
-  required.major < version.major
-  || (required.major = version.major && required.minor < version.minor)
-  || (required.major = version.major && required.minor = version.minor && required.patch <= version.patch)
-
 let usage_msg = "Sail " ^ version_string ^ "\nusage: sail <options> <file1.sail> ... <fileN.sail>\n"
 
 let help options = raise (Arg.Help (Arg.usage_string options usage_msg))
@@ -291,6 +273,7 @@ let rec options =
       );
       ("-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings");
       ("-all_warnings", Arg.Set Reporting.opt_all_warnings, " print all warning messages");
+      ("-warn_error", Arg.Set opt_warn_error, " promote warnings to errors, if below the required version");
       ( "-strict_var",
         Arg.Tuple [Arg.Unit (fun () -> Preprocess.add_default_symbol "STRICT_VAR"); Arg.Set Type_check.opt_strict_var],
         " require var expressions for variable declarations"
@@ -444,7 +427,7 @@ let rec options =
       );
       ("-just_parse_project", Arg.Set opt_just_parse_project, "");
       ( "-infer_effects",
-        Arg.Unit (fun () -> Reporting.simple_warn "-infer_effects option is deprecated"),
+        Arg.Unit (fun () -> Reporting.simple_warn Version.v0_20_2 "-infer_effects option is deprecated"),
         " (deprecated) ignored for compatibility with older versions; effects are always inferred now"
       );
       ( "-undefined_gen",
@@ -657,7 +640,7 @@ let get_implicit_config_file override_file =
   let check_exists file =
     if Sys.file_exists file then Some file
     else (
-      Reporting.warn "" Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file);
+      Reporting.warn Version.v0_20_2 "" Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file);
       None
     )
   in
@@ -709,14 +692,15 @@ let main () =
   ( match !opt_require_version with
   | Some required_version ->
       let required_version_parsed =
-        match parse_version required_version with
+        match Version.parse required_version with
         | Some v -> v
         | None -> raise (Reporting.err_general Unknown ("Couldn't parse required version '" ^ required_version ^ "'"))
       in
-      if not (version_check ~required:required_version_parsed) then (
+      if not (Version.check ~required:required_version_parsed ()) then (
         Printf.eprintf "Sail version %s is older than requested version %s" version_string required_version;
         exit 1
-      )
+      );
+      if !opt_warn_error then Reporting.opt_warn_error := Some required_version_parsed
   | None -> ()
   );
 

src/lib/anf.ml

@@ -743,7 +743,7 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
   | E_undef -> mk_aexp (AE_val (AV_undef (typ_of exp)))
   | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
   | E_block [] ->
-      Reporting.warn "" l
+      Reporting.warn Version.v0_20_2 "" l
         "Translating empty block (possibly assigning to an uninitialized variable at the end of a block?)";
       mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp))
   | E_block exps ->

src/lib/config.ml

@@ -528,7 +528,8 @@ let fix_length ~at:l ~len bitlist =
   match Primops.zero_extend (V_bitvector bitlist) (V_int (Big_int.of_int len)) with
   | Some (V_bitvector bitlist) -> bitlist
   | _ ->
-      Reporting.warn ~force_show:true "Configuration" l "Forced to truncate configuration bitvector literal";
+      Reporting.warn ~force_show:true Version.v0_20_2 "Configuration" l
+        "Forced to truncate configuration bitvector literal";
       let d = len - List.length bitlist in
       Util.drop (abs d) bitlist
 

src/lib/constant_fold.ml

@@ -186,7 +186,7 @@ let rw_exp fixed target ok not_ok istate =
           Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)
         with Type_error.Type_error (l, err) ->
           (* A type error here would be unexpected, so don't ignore it! *)
-          Reporting.warn "" l
+          Reporting.warn Version.v0_20_2 "" l
             ("Type error when folding constants in "
             ^ string_of_exp (E_aux (e_aux, annot))
             ^ "\n"

src/lib/constraint.ml

@@ -293,7 +293,7 @@ let load_digests_err path =
         let solution = input_binary_int in_chan in
         known_uniques := DigestMap.add digest (Some solution) !known_uniques
     | _ ->
-        Reporting.warn "" Parse_ast.Unknown "SMT cache file 'sail_smt_cache' is invalid";
+        Reporting.warn Version.v0_20_2 "" Parse_ast.Unknown "SMT cache file 'sail_smt_cache' is invalid";
         known_problems := DigestMap.empty;
         known_uniques := DigestMap.empty;
         (* Exit the loop as if we reached the end of the file *)

src/lib/format_sail.ml

@@ -425,7 +425,7 @@ let known_key k =
 let int_option k = function
   | `Int n -> Some n
   | json ->
-      Reporting.simple_warn
+      Reporting.simple_warn Version.v0_20_2
         (Printf.sprintf "Argument for key %s must be an integer, got %s instead. Using default value." k
            (Yojson.Safe.to_string json)
         );
@@ -434,7 +434,7 @@ let int_option k = function
 let bool_option k = function
   | `Bool n -> Some n
   | json ->
-      Reporting.simple_warn
+      Reporting.simple_warn Version.v0_20_2
         (Printf.sprintf "Argument for key %s must be a boolean, got %s instead. Using default value." k
            (Yojson.Safe.to_string json)
         );
@@ -444,7 +444,7 @@ let float_option k = function
   | `Int n -> Some (float_of_int n)
   | `Float n -> Some n
   | json ->
-      Reporting.simple_warn
+      Reporting.simple_warn Version.v0_20_2
         (Printf.sprintf "Argument for key %s must be a number, got %s instead. Using default value." k
            (Yojson.Safe.to_string json)
         );
@@ -454,10 +454,11 @@ let enum_option f k = function
   | `String s ->
       let res = f s in
       if Option.is_none res then
-        Reporting.simple_warn (Printf.sprintf "Argument for key %s was not a recognized setting. Using default value." k);
+        Reporting.simple_warn Version.v0_20_2
+          (Printf.sprintf "Argument for key %s was not a recognized setting. Using default value." k);
       res
   | json ->
-      Reporting.simple_warn
+      Reporting.simple_warn Version.v0_20_2
         (Printf.sprintf "Argument for key %s must be a string, got %s instead. Using default value." k
            (Yojson.Safe.to_string json)
         );
@@ -470,7 +471,7 @@ let config_from_json (json : Yojson.Safe.t) =
   match json with
   | `Assoc keys ->
       ( match List.find_opt (fun (k, _) -> not (known_key k)) keys with
-      | Some (k, _) -> Reporting.simple_warn (Printf.sprintf "Unknown key %s in formatting config" k)
+      | Some (k, _) -> Reporting.simple_warn Version.v0_20_2 (Printf.sprintf "Unknown key %s in formatting config" k)
       | None -> ()
       );
       {

src/lib/initial_check.ml

@@ -1073,7 +1073,8 @@ module ConvertType = struct
     | P.QI_id kopt ->
         let (kopts, constrs, ctx), attr = to_ast_kopts kenv ctx kopt in
         ( match attr with
-        | Some "constant" -> Reporting.warn "Deprecated" l "constant type variable attribute no longer used"
+        | Some "constant" ->
+            Reporting.warn Version.v0_20_2 "Deprecated" l "constant type variable attribute no longer used"
         | Some attr -> raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr))
         | None -> ()
         );
@@ -1217,7 +1218,7 @@ let parse_hex_lit ?warn_inconsistent_case str =
               match warn_inconsistent_case with
               | None -> ()
               | Some l ->
-                  Reporting.warn "Inconsistent hexadecimal casing" l
+                  Reporting.warn Version.v0_20_2 "Inconsistent hexadecimal casing" l
                     "This hexadecimal bitvector literal contains both lowercase and uppercase digits."
             )
       )
@@ -2622,7 +2623,7 @@ let generate_enum_number_conversions defs =
 
             let already_defined name =
               let original_id = IdSet.find name vs_ids in
-              Reporting.warn
+              Reporting.warn Version.v0_20_2
                 (Printf.sprintf "Cannot generate %s for enum" (string_of_id name))
                 (Hint ("Function with the same name defined here", id_loc original_id, def_annot.loc))
                 (Printf.sprintf

src/lib/lint.ml

@@ -113,7 +113,7 @@ let warn_unmodified_variables (type a) (ast : (a, 'b) ast) : unit =
     let unmodified = IdSet.diff lexp exp in
     IdSet.iter
       (fun id ->
-        Reporting.warn "Unnecessary mutability" (id_loc id)
+        Reporting.warn Version.v0_20_2 "Unnecessary mutability" (id_loc id)
           "This variable is mutable, but it is never modified. It could be declared as immutable using 'let'."
       )
       unmodified;
@@ -142,7 +142,7 @@ let warn_unused_variables (ast : Type_check.typed_ast) : unit =
     IdSet.iter
       (fun id ->
         if not (ignore_variable id) then
-          Reporting.warn "Unused variable" (id_loc id) "This variable is defined but never used."
+          Reporting.warn Version.v0_20_2 "Unused variable" (id_loc id) "This variable is defined but never used."
       )
       unused;
     IdSet.diff used pat

src/lib/parse_ast_diff.ml

@@ -562,13 +562,15 @@ let rec diff_mapcl (MCL_aux (lhs, l)) (MCL_aux (rhs, _)) =
       | _ -> Some l
     )
   | MCL_forwards_deprecated _ ->
-      Reporting.warn "Deprecated" l "Cannot check AST equivalence here, as a deprecated construct was found.";
+      Reporting.warn Version.v0_20_2 "Deprecated" l
+        "Cannot check AST equivalence here, as a deprecated construct was found.";
       None
   | MCL_forwards pexp1 -> (
       match rhs with
       | MCL_forwards pexp2 -> diff_pexp pexp1 pexp2
       | MCL_forwards_deprecated _ ->
-          Reporting.warn "Deprecated" l "Cannot check AST equivalence here, as a deprecated construct was found.";
+          Reporting.warn Version.v0_20_2 "Deprecated" l
+            "Cannot check AST equivalence here, as a deprecated construct was found.";
           None
       | _ -> Some l
     )

src/lib/parser.mly

@@ -182,24 +182,24 @@ let pragma_left_spaces pragma p s =
   !n
 
 let effect_deprecated l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "Explicit effect annotations are deprecated. They are no longer used and can be removed."
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l "Explicit effect annotations are deprecated. They are no longer used and can be removed."
 
 let cast_deprecated l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "Cast annotations are deprecated. They will be removed in a future version of the language."
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l "Cast annotations are deprecated. They will be removed in a future version of the language."
 
 let old_bitfield_deprecated ?(bitfield = "<bitfield>") l field =
   let replace = if field = "bits" then Printf.sprintf "%s.bits" bitfield else Printf.sprintf "%s[%s]" bitfield field in
-  Reporting.warn ~once_from:__POS__ "Deprecated" l
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l
     ("Old bitfield syntax, use '" ^ replace ^ "' instead")
 
 let warn_extern_effect l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either pure or impure"
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l "All external bindings should be marked as either pure or impure"
 
 let forwards_mapcl_deprecated l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "Single direction mapping clause should be prefixed by a direction, either forwards or backwards"
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l "Single direction mapping clause should be prefixed by a direction, either forwards or backwards"
 
 let set_syntax_deprecated l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}."
+  Reporting.warn ~once_from:__POS__ Version.v0_20_2 "Deprecated" l "Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}."
 
 %}
 

src/lib/pattern_completeness.ml

@@ -275,7 +275,7 @@ module Make (C : Config) = struct
     let preserved = get_preserved_patterns cinfo in
     let wildcards = get_wildcard_patterns cinfo in
     let rec go wild (P_aux (aux, (l, (t, n))) as full_pat) =
-      if IntSet.mem n preserved then Reporting.warn "Required literal" l preserved_explanation;
+      if IntSet.mem n preserved then Reporting.warn Version.v0_20_2 "Required literal" l preserved_explanation;
       let wild = wild || List.exists (fun wildcard -> wildcard = n) wildcards in
       let t = ref t in
       let aux =
@@ -378,7 +378,7 @@ module Make (C : Config) = struct
                 | P_wild | P_id _ -> (mask ^ "0", bits ^ "0")
                 | P_typ (_, P_aux (pat, _)) -> go pat
                 | _ ->
-                    Reporting.warn "Unexpected pattern" l "";
+                    Reporting.warn Version.v0_20_2 "Unexpected pattern" l "";
                     (mask ^ "0", bits ^ "0")
               in
               go pat
@@ -1005,7 +1005,7 @@ module Make (C : Config) = struct
       (* The type-checker can prune some case armms early, if it determines the pattern would introduce a
          false/impossible flow typing constraint. If this happens we can get an empty list here. *)
       | have_guard, have_mapping, [] ->
-          Reporting.warn "Incomplete pattern match statement at" (shrink_loc keyword l)
+          Reporting.warn Version.v0_20_2 "Incomplete pattern match statement at" (shrink_loc keyword l)
             ("No expression of type "
             ^ Util.(string_of_typ head_exp_typ |> yellow |> clear)
             ^ " can be matched"
@@ -1023,7 +1023,7 @@ module Make (C : Config) = struct
           in
           match matrix_is_complete l ctx matrix with
           | Incomplete (unmatched :: _) ->
-              Reporting.warn "Incomplete pattern match statement at" (shrink_loc keyword l)
+              Reporting.warn Version.v0_20_2 "Incomplete pattern match statement at" (shrink_loc keyword l)
                 ("The following expression is unmatched"
                 ^ guard_info ~terminator:": " ~have_guard ~have_mapping
                 ^ Util.(string_of_exp unmatched |> yellow |> clear)
@@ -1036,17 +1036,18 @@ module Make (C : Config) = struct
               List.iter
                 (fun (idx, _) ->
                   if IntSet.mem idx.num cinfo.redundant then
-                    Reporting.warn "Redundant case" idx.loc "This match case is never used"
+                    Reporting.warn Version.v0_20_2 "Redundant case" idx.loc "This match case is never used"
                 )
                 (rows_to_list matrix);
               let result = update_cases l wildcarded_pats cases in
               if remove_redundant then Some (filter_out cinfo.redundant result) else Some result
           | Completeness_unknown -> None
         )
     with
-    (* For now, if any error occurs just report the pattern match is incomplete *)
-    | _ ->
-      None
+    (* For now, if any error occurs just report the pattern match is incomplete. The only exception is if we want
+       warnings to be fatal, so re-raise those. *)
+    | Reporting.Fatal_error (Err_warning _) as exn -> raise exn
+    | _ -> None
 
   let is_complete_funcls_wildcarded ?(keyword = "match") ?(remove_redundant = false) l ctx funcls head_exp_typ =
     let destruct_funcl (FCL_aux (FCL_funcl (id, pexp), annot)) = ((id, annot), pexp) in