summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--editors/sail-mode.el3
-rw-r--r--src/constant_fold.ml7
-rw-r--r--src/jib/anf.ml4
-rw-r--r--src/jib/jib_smt.ml2
-rw-r--r--src/latex.ml4
-rw-r--r--src/monomorphise.ml6
-rw-r--r--src/optimize.ml2
-rw-r--r--src/pattern_completeness.ml18
-rw-r--r--src/process_file.ml14
-rw-r--r--src/reporting.ml23
-rw-r--r--src/reporting.mli20
-rw-r--r--src/sail.ml12
-rw-r--r--src/type_check.ml12
-rw-r--r--src/util.ml20
-rw-r--r--src/util.mli9
15 files changed, 93 insertions, 63 deletions
diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index a0d98429..e800b05f 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -45,7 +45,8 @@
(defconst sail2-special
'("_prove" "_not_prove" "create" "kill" "convert" "undefined"
- "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex" "$property" "$counterexample"))
+ "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize"
+ "$latex" "$property" "$counterexample" "$suppress_warnings"))
(defconst sail2-font-lock-keywords
`((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face)
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 4c26b641..abedcf35 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -201,9 +201,10 @@ let rw_exp ok not_ok istate =
try (ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)) with
| Type_error (env, l, err) ->
(* A type error here would be unexpected, so don't ignore it! *)
- Util.warn ("Type error when folding constants in "
- ^ string_of_exp (E_aux (e_aux, annot))
- ^ "\n" ^ Type_error.string_of_type_error err);
+ Reporting.warn "" l
+ ("Type error when folding constants in "
+ ^ string_of_exp (E_aux (e_aux, annot))
+ ^ "\n" ^ Type_error.string_of_type_error err);
not_ok ();
E_aux (e_aux, annot)
end
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index bd4813ed..fdb4f941 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -556,8 +556,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
| E_block [] ->
- Util.warn (Reporting.loc_to_string l
- ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)");
+ Reporting.warn "" 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 ->
let exps, last = split_block l exps in
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 0d6f42fe..74e56ef6 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -329,7 +329,7 @@ let add_pathcond_event ctx ev =
let overflow_check ctx smt =
if not !opt_ignore_overflow then (
- Util.warn "Adding overflow check in generated SMT";
+ Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
add_event ctx Overflow smt
)
diff --git a/src/latex.ml b/src/latex.ml
index aa786b83..9f5979c1 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -342,7 +342,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
close_out chan;
let command = sprintf "\\%s%s%s" !opt_prefix (category_name cat) (latex_id id) in
if StringSet.mem command state.commands then
- (Util.warn ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
+ (Reporting.warn "" l ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
else
begin
state.commands <- StringSet.add command state.commands;
@@ -417,7 +417,7 @@ let process_pragma l command =
Some (ksprintf string "\\newcommand{\\%s}{%s}" name body)
| _ ->
- Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l));
+ Reporting.warn "Bad latex pragma at" l "";
None
let tdef_id = function
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 1e52d708..145d9046 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3686,10 +3686,10 @@ type options = {
}
let recheck defs =
- let w = !Util.opt_warnings in
- let () = Util.opt_warnings := false in
+ let w = !Reporting.opt_warnings in
+ let () = Reporting.opt_warnings := false in
let r = Type_error.check (Type_check.Env.no_casts Type_check.initial_env) defs in
- let () = Util.opt_warnings := w in
+ let () = Reporting.opt_warnings := w in
r
let mono_rewrites = MonoRewrites.mono_rewrite
diff --git a/src/optimize.ml b/src/optimize.ml
index a372abf4..1fc2fbe8 100644
--- a/src/optimize.ml
+++ b/src/optimize.ml
@@ -87,7 +87,7 @@ let recheck (Defs defs) =
!specs @ !bodies @ find_optimizations defs
| _ ->
- Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma);
+ Reporting.warn "Unrecognised optimize pragma at" p_l "";
def1 :: def2 :: find_optimizations defs
end
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 79fc93ee..3e26502d 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -106,7 +106,7 @@ let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) =
| Unbound -> GP_wild
| Local (Immutable, _) -> GP_wild
| Register _ | Local (Mutable, _) ->
- Util.warn ("Matching on register or mutable variable at " ^ Reporting.loc_to_string l); GP_wild
+ Reporting.warn "Matching on register or mutable variable at " l ""; GP_wild
| Enum _ -> GP_app (Bindings.singleton id GP_wild)
end
| P_var (pat, _) -> generalize ctx pat
@@ -164,7 +164,7 @@ let join_bits bits1 bits2 =
(* The join_lit function takes two patterns and produces a pattern
that matches both literals *)
-let rec join_lit (L_aux (l_aux1, _) as lit1) (L_aux (l_aux2, _) as lit2) =
+let rec join_lit (L_aux (l_aux1, l) as lit1) (L_aux (l_aux2, _) as lit2) =
match l_aux1, l_aux2 with
(* The only literal with type unit is the unit literal *)
| L_unit, _ -> GP_lit lit1
@@ -207,7 +207,7 @@ let rec join_lit (L_aux (l_aux1, _) as lit1) (L_aux (l_aux2, _) as lit2) =
Printf.sprintf "Have two differently typed pattern literals %s and %s matching the same thing"
(string_of_lit lit1) (string_of_lit lit2)
in
- Util.warn message;
+ Reporting.warn "" l message;
GP_wild
let rec join ctx gpat1 gpat2 =
@@ -270,7 +270,7 @@ let combine ctx gpat (l, pat) =
(* This warning liable to false positives as join returns a
pattern that overapproximates what can match, so we only
report when the second match is a constructor. *)
- Util.warn (Printf.sprintf "Possible redundant pattern match at %s\n" (Reporting.loc_to_string l));
+ Reporting.warn "Possible redundant pattern match at" l "";
GP_wild
| _, gpat' -> join ctx gpat gpat'
@@ -288,15 +288,11 @@ let shrink_loc = function
let check l ctx cases =
match cases_to_pats cases with
- | [] -> Util.warn (Printf.sprintf "No non-guarded patterns at %s\n" (Reporting.loc_to_string (shrink_loc l)))
+ | [] -> Reporting.warn "No non-guarded patterns at" (shrink_loc l) ""
| (_, pat) :: pats ->
let top_pat = List.fold_left (combine ctx) (generalize ctx pat) pats in
if is_wild top_pat then
()
else
- let message =
- Printf.sprintf "Possible incomplete pattern match at %s\n\nMost general matched pattern is %s\n"
- (Reporting.loc_to_string (shrink_loc l))
- (string_of_gpat top_pat |> Util.cyan |> Util.clear)
- in
- Util.warn message
+ Reporting.warn "Possible incomplete pattern match at" (shrink_loc l)
+ (Printf.sprintf "Most general matched pattern is %s" (string_of_gpat top_pat |> Util.cyan |> Util.clear))
diff --git a/src/process_file.ml b/src/process_file.ml
index ae79d5c3..7221ec25 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -144,6 +144,7 @@ let all_pragmas =
"latex";
"property";
"counterexample";
+ "suppress_warnings";
]
let rec preprocess opts = function
@@ -179,7 +180,7 @@ let rec preprocess opts = function
| Parse_ast.DEF_pragma ("include", file, l) :: defs ->
let len = String.length file in
if len = 0 then
- (Util.warn "Skipping bad $include. No file argument."; preprocess opts defs)
+ (Reporting.warn "" l "Skipping bad $include. No file argument."; preprocess opts defs)
else if file.[0] = '"' && file.[len - 1] = '"' then
let relative = match l with
| Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname))
@@ -206,11 +207,18 @@ let rec preprocess opts = function
include_defs @ preprocess opts defs
else
let help = "Make sure the filename is surrounded by quotes or angle brackets" in
- (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
+ (Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
+
+ | Parse_ast.DEF_pragma ("suppress_warnings", _, l) :: defs ->
+ begin match Reporting.simp_loc l with
+ | None -> () (* This shouldn't happen, but if it does just continue *)
+ | Some (p, _) -> Reporting.suppress_warnings_for_file p.pos_fname
+ end;
+ preprocess opts defs
| Parse_ast.DEF_pragma (p, arg, l) :: defs ->
if not (StringSet.mem p all_pragmas) then
- Util.warn (Reporting.loc_to_string l ^ "Unrecognised directive: " ^ p);
+ Reporting.warn "" l ("Unrecognised directive: " ^ p);
Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs
| (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs ->
diff --git a/src/reporting.ml b/src/reporting.ml
index 9387ee6b..e81fbae8 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -95,6 +95,8 @@
(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
(**************************************************************************)
+let opt_warnings = ref true
+
type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
let print_err_internal p_l m1 m2 =
@@ -164,3 +166,24 @@ let unreachable l pos msg =
let print_error e =
let (m1, pos_l, m2) = dest_err e in
print_err_internal pos_l m1 m2
+
+(* Warnings *)
+
+module StringSet = Set.Make(String)
+
+let ignored_files = ref StringSet.empty
+
+let suppress_warnings_for_file f =
+ ignored_files := StringSet.add f !ignored_files
+
+let warn str1 l str2 =
+ if !opt_warnings then
+ match simp_loc l with
+ | None ->
+ prerr_endline (Util.("Warning" |> yellow |> clear) ^ ": " ^ str1 ^ "\n" ^ str2)
+ | Some (p1, p2) when not (StringSet.mem p1.pos_fname !ignored_files) ->
+ prerr_endline (Util.("Warning" |> yellow |> clear) ^ ": "
+ ^ str1 ^ (if str1 <> "" then " " else "") ^ loc_to_string l ^ str2)
+ | Some _ -> ()
+ else
+ ()
diff --git a/src/reporting.mli b/src/reporting.mli
index 28f2a799..0bdff5ca 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -50,16 +50,18 @@
(** Basic error reporting
- [Reporting] contains functions to report errors and warnings.
+ [Reporting] contains functions to report errors and warnings.
It contains functions to print locations ([Parse_ast.l] and [Ast.l]) and lexing positions.
The main functionality is reporting errors. This is done by raising a
- [Fatal_error] exception. This is caught internally and reported via [report_error].
+ [Fatal_error] exception. This is caught internally and reported via [report_error].
There are several predefined types of errors which all cause different error
- messages. If none of these fit, [Err_general] can be used.
+ messages. If none of these fit, [Err_general] can be used.
*)
+val opt_warnings : bool ref
+
(** {2 Auxiliary Functions } *)
(** [loc_to_string] includes code from file if code optional argument is true (default) *)
@@ -70,7 +72,7 @@ val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
(** [short_loc_to_string] prints the location as a single line in a simple format *)
val short_loc_to_string : Parse_ast.l -> string
-
+
(** [print_err fatal print_loc_source l head mes] prints an error / warning message to
std-err. It starts with printing location information stored in [l]
It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
@@ -113,7 +115,15 @@ val err_typ : Parse_ast.l -> string -> exn
(** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
val err_syntax_loc : Parse_ast.l -> string -> exn
-
+
val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
val print_error : error -> unit
+
+(** Print a warning message. The first string is printed before the
+ location, the second after. *)
+val warn : string -> Parse_ast.l -> string -> unit
+
+(** Will suppress all warnings for a given file. Used by
+ $suppress_warnings directive in process_file.ml *)
+val suppress_warnings_for_file : string -> unit
diff --git a/src/sail.ml b/src/sail.ml
index c4991fe5..19a87f6a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -87,7 +87,7 @@ let options = Arg.align ([
Arg.Set Interactive.opt_emacs_mode,
" run sail interactively as an emacs mode child process");
( "-no_warn",
- Arg.Clear Util.opt_warnings,
+ Arg.Clear Reporting.opt_warnings,
" do not print warnings");
( "-tofrominterp",
set_target "tofrominterp",
@@ -458,7 +458,7 @@ let target name out_name ast type_envs =
ast_c, type_envs
in
let close, output_chan = match !opt_file_out with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
- Util.opt_warnings := true;
+ Reporting.opt_warnings := true;
C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
flush output_chan;
if close then close_out output_chan else ()
@@ -471,7 +471,7 @@ let target name out_name ast type_envs =
| Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir.sail"))
| None -> false, stdout
in
- Util.opt_warnings := true;
+ Reporting.opt_warnings := true;
let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
(* let cdefs = List.map Jib_optimize.flatten_cdef cdefs in *)
let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
@@ -490,7 +490,7 @@ let target name out_name ast type_envs =
| Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
| None -> fun str -> str ^ ".smt2"
in
- Util.opt_warnings := true;
+ Reporting.opt_warnings := true;
Jib_smt.generate_smt props name_file type_envs ast_smt;
| Some "lem" ->
@@ -500,7 +500,7 @@ let target name out_name ast type_envs =
output "" (Coq_out (!opt_libs_coq)) [(out_name, type_envs, ast)]
| Some "latex" ->
- Util.opt_warnings := true;
+ Reporting.opt_warnings := true;
let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
begin
try
@@ -524,7 +524,7 @@ let main () =
else
begin
let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
- Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
+ Reporting.opt_warnings := false; (* Don't show warnings during re-writing for now *)
begin match !opt_process_elf, !opt_file_out with
| Some elf, Some out ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 2be68ade..77263b4a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3090,9 +3090,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
(* If the identifier we're matching on is also a constructor of
a union, that's probably a mistake, so warn about it. *)
if Env.is_union_constructor v env then
- Util.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at %s\n"
- (string_of_id v)
- (Reporting.loc_to_string l))
+ Reporting.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at"
+ (string_of_id v))
+ l ""
else ();
match Env.lookup_id v env with
| Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
@@ -4014,9 +4014,9 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
(* If the identifier we're matching on is also a constructor of
a union, that's probably a mistake, so warn about it. *)
if Env.is_union_constructor v env then
- Util.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at %s\n"
- (string_of_id v)
- (Reporting.loc_to_string l))
+ Reporting.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at"
+ (string_of_id v))
+ l ""
else ();
match Env.lookup_id v env with
| Local (Immutable, _) | Unbound -> annot_mpat (MP_id v) typ, Env.add_local v (Immutable, typ) env, []
diff --git a/src/util.ml b/src/util.ml
index 6a2fb9bb..2745631c 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -94,7 +94,6 @@
(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
(**************************************************************************)
-let opt_warnings = ref true
let opt_colors = ref true
let opt_verbosity = ref 0
@@ -110,7 +109,7 @@ let rec butlast = function
module Duplicate(S : Set.S) = struct
-type dups =
+type dups =
| No_dups of S.t
| Has_dups of S.elt
@@ -129,7 +128,7 @@ end
let remove_duplicates l =
let l' = List.sort Pervasives.compare l in
let rec aux acc l = match (acc, l) with
- (_, []) -> List.rev acc
+ (_, []) -> List.rev acc
| ([], x :: xs) -> aux [x] xs
| (y::ys, x :: xs) -> if (x = y) then aux (y::ys) xs else aux (x::y::ys) xs
in
@@ -138,7 +137,7 @@ let remove_duplicates l =
let remove_dups compare eq l =
let l' = List.sort compare l in
let rec aux acc l = match (acc, l) with
- (_, []) -> List.rev acc
+ (_, []) -> List.rev acc
| ([], x :: xs) -> aux [x] xs
| (y::ys, x :: xs) -> if (eq x y) then aux (y::ys) xs else aux (x::y::ys) xs
in
@@ -159,7 +158,7 @@ let rec assoc_compare_opt cmp k l =
| [] -> None
| (k',v)::l -> if cmp k k' = 0 then Some v else assoc_compare_opt cmp k l
-let rec compare_list f l1 l2 =
+let rec compare_list f l1 l2 =
match (l1,l2) with
| ([],[]) -> 0
| (_,[]) -> 1
@@ -199,7 +198,7 @@ let rec map_filter (f : 'a -> 'b option) (l : 'a list) : 'b list =
match l with [] -> []
| x :: xs ->
let xs' = map_filter f xs in
- match (f x) with None -> xs'
+ match (f x) with None -> xs'
| Some x' -> x' :: xs'
let list_index p l =
@@ -317,13 +316,13 @@ let string_to_list s =
else aux (i-1) (s.[i] :: acc)
in aux (String.length s - 1) []
-module IntSet = Set.Make(
+module IntSet = Set.Make(
struct
let compare = Pervasives.compare
type t = int
end )
-module IntIntSet = Set.Make(
+module IntIntSet = Set.Make(
struct
let compare = Pervasives.compare
type t = int * int
@@ -456,11 +455,6 @@ let file_encode_string str =
let md5 = Digest.to_hex (Digest.string zstr) in
String.lowercase_ascii zstr ^ String.lowercase_ascii md5
-let warn str =
- if !opt_warnings then
- prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)
- else ()
-
let log_line str line msg =
"\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg
diff --git a/src/util.mli b/src/util.mli
index ddc5347f..9c57e360 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -50,13 +50,12 @@
(** Various non Sail specific utility functions *)
-(* Last element of a list *)
-val last : 'a list -> 'a
-
-val opt_warnings : bool ref
val opt_colors : bool ref
val opt_verbosity : int ref
+(* Last element of a list *)
+val last : 'a list -> 'a
+
val butlast : 'a list -> 'a list
(** Mixed useful things *)
@@ -270,5 +269,3 @@ val log_line : string -> int -> string -> string
val header : string -> int -> string
val progress : string -> string -> int -> int -> unit
-
-val warn : string -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:35:55 +0000