From 935803fef71a87ea697fe6bb0f4355b211f9f95c Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 17 Jan 2022 15:33:51 +0100
Subject: [PATCH] [eacsl] Add phase information to error messages
---
src/plugins/e-acsl/E_ACSL.mli | 8 +-
src/plugins/e-acsl/src/libraries/error.ml | 158 ++++++++++++++-------
src/plugins/e-acsl/src/libraries/error.mli | 130 ++++++++++-------
3 files changed, 197 insertions(+), 99 deletions(-)
diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 1b68985666f..d6d9aa98332 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -24,9 +24,13 @@
open Cil_types
+module Options: sig
+ type category
+end
+
module Error: sig
- exception Typing_error of string
- exception Not_yet of string
+ exception Typing_error of Options.category option * string
+ exception Not_yet of Options.category option * string
end
module Translate_terms: sig
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index fb6b3ad8709..1f48938294e 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -22,14 +22,39 @@
open Error_types
-exception Typing_error of string
-let untypable s = raise (Typing_error s)
+module Exn_impl = struct
+ exception Typing_error of Options.category option * string
+ exception Not_yet of Options.category option * string
+ exception Not_memoized of Options.category option
+end
-exception Not_yet of string
-let not_yet s = raise (Not_yet s)
+module type Exn = module type of Exn_impl
-exception Not_memoized
-let not_memoized () = raise Not_memoized
+module type S = sig
+ include Exn
+ val make_untypable: string -> exn
+ val make_not_yet: string -> exn
+ val make_not_memoized: unit -> exn
+ val untypable: string -> 'a
+ val not_yet: string -> 'a
+ val not_memoized: unit -> 'a
+ val print_not_yet: string -> unit
+ val handle: ('a -> 'a) -> 'a -> 'a
+ val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+ val nb_untypable: unit -> int
+ val nb_not_yet: unit -> int
+ val retrieve_preprocessing:
+ string ->
+ ('a -> 'b or_error) ->
+ 'a ->
+ (Format.formatter -> 'a -> unit) ->
+ 'b
+ val pp_or_error:
+ (Format.formatter -> 'a -> unit) ->
+ Format.formatter ->
+ 'a or_error ->
+ unit
+end
module Nb_typing =
State_builder.Ref
@@ -40,8 +65,6 @@ module Nb_typing =
let dependencies = [ Ast.self ]
end)
-let nb_untypable = Nb_typing.get
-
module Nb_not_yet =
State_builder.Ref
(Datatype.Int)
@@ -51,46 +74,85 @@ module Nb_not_yet =
let dependencies = [ Ast.self ]
end)
-let nb_not_yet = Nb_not_yet.get
-
-let print_not_yet msg =
- let msg =
- Format.sprintf "@[E-ACSL construct@ `%s'@ is not yet supported.@]" msg
- in
- Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
- Nb_not_yet.set (Nb_not_yet.get () + 1)
-
-let generic_handle f res x =
- try
- f x
- with
- | Typing_error s ->
- let msg = Format.sprintf "@[invalid E-ACSL construct@ `%s'.@]" s in
- Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
- Nb_typing.set (Nb_typing.get () + 1);
- res
- | Not_yet s ->
- print_not_yet s;
- res
-
-let handle f x = generic_handle f x x
-
-let retrieve_preprocessing analyse_name getter parameter pp =
- try
- match getter parameter with
- | Res res -> res
- | Err exn -> raise exn
- with Not_memoized ->
- Options.fatal
- "%s was not performed on construct %a"
- analyse_name
- pp
- parameter
-
-let pp_or_error pp fmt a_or_error =
- match a_or_error with
- | Res a -> Format.fprintf fmt "@[%a@]" pp a
- | Err err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+module Make_with_opt(P: sig val phase:Options.category option end): S = struct
+ include Exn_impl
+
+ let make_untypable msg = Typing_error (P.phase, msg)
+ let make_not_yet msg = Not_yet (P.phase, msg)
+ let make_not_memoized () = Not_memoized P.phase
+
+ let untypable msg = raise (make_untypable msg)
+ let not_yet msg = raise (make_not_yet msg)
+ let not_memoized () = raise (make_not_memoized ())
+
+ let nb_untypable = Nb_typing.get
+ let nb_not_yet = Nb_not_yet.get
+
+ let pp_phase fmt phase =
+ match phase with
+ | Some phase ->
+ if Options.verbose_atleast 2 then
+ Format.fprintf fmt "@[@ in phase `%a'@]" Options.pp_category phase
+ | None -> ()
+
+ let do_print_not_yet phase msg =
+ let msg =
+ Format.asprintf
+ "@[E-ACSL construct@ `%s'@ is not yet supported%a.@]"
+ msg
+ pp_phase phase
+ in
+ Options.warning
+ ~once:true ~current:true
+ "@[%s@ Ignoring annotation.@]" msg;
+ Nb_not_yet.set (Nb_not_yet.get () + 1)
+
+ let print_not_yet msg =
+ do_print_not_yet P.phase msg
+
+ let generic_handle f res x =
+ try
+ f x
+ with
+ | Typing_error (phase, s) ->
+ let msg =
+ Format.asprintf "@[invalid E-ACSL construct@ `%s'%a.@]"
+ s
+ pp_phase phase
+ in
+ Options.warning
+ ~once:true ~current:true
+ "@[%s@ Ignoring annotation.@]" msg;
+ Nb_typing.set (Nb_typing.get () + 1);
+ res
+ | Not_yet (phase, s) ->
+ do_print_not_yet phase s;
+ res
+
+ let handle f x = generic_handle f x x
+
+ let retrieve_preprocessing analyse_name getter parameter pp =
+ try
+ match getter parameter with
+ | Res res -> res
+ | Err exn -> raise exn
+ with Not_memoized phase ->
+ Options.fatal
+ "@[%s was not performed on construct %a%a@]"
+ analyse_name
+ pp parameter
+ pp_phase phase
+
+ let pp_or_error pp fmt a_or_error =
+ match a_or_error with
+ | Res a -> Format.fprintf fmt "@[%a@]" pp a
+ | Err err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+end
+
+module Make(P: sig val phase:Options.category end): S =
+ Make_with_opt(struct let phase = Some P.phase end)
+
+include Make_with_opt(struct let phase = None end)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 60e8dd1f339..656adfcaa33 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -23,57 +23,89 @@
(** Handling errors. *)
open Error_types
-exception Typing_error of string
-exception Not_yet of string
-exception Not_memoized
-
-val untypable: string -> 'a
-(** Type error built from the given argument. *)
-
-val not_yet: string -> 'a
-(** Not_yet_implemented error built from the given argument. *)
-
-val not_memoized : unit -> 'a
-(** @raise Not_memoized when asking the preprocessed form of something that
- was not preprocessed *)
-
-val handle: ('a -> 'a) -> 'a -> 'a
-(** Run the closure with the given argument and handle potential errors.
- Return the provide argument in case of errors. *)
-
-val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
-(** Run the closure with the given argument and handle potential errors.
- Return the additional argument in case of errors. *)
-
-val nb_untypable: unit -> int
-(** Number of untypable annotations. *)
-
-val nb_not_yet: unit -> int
-(** Number of not-yet-supported annotations. *)
-
-val print_not_yet: string -> unit
-(** Print the "not yet" message without raising an exception. *)
-
-val retrieve_preprocessing:
- string ->
- ('a -> 'b or_error) ->
- 'a ->
- (Format.formatter -> 'a -> unit) ->
- 'b
-(** Retrieve the result of a preprocessing phase, which possibly failed.
- The [string] argument and the formatter are used to display a message in
- case the preprocessing phase did not compute the required result. *)
-
-val pp_or_error:
- (Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a or_error ->
- unit
-(** [pp_or_error pp] where [pp] is a formatter for ['a] returns a formatter for
- ['a or_error]. *)
+(** Internal module holding the exception of [Error].
+
+ The module is included into [S] later and should not be used directly.
+ However we need to have a separate module for the exception so that every
+ exception built by [Make] is the exact same type. *)
+module type Exn = sig
+ exception Typing_error of Options.category option * string
+ (** Typing error where the first element is the phase where the error occured
+ and the second element is the error message. *)
+
+ exception Not_yet of Options.category option * string
+ (** "Not yet supported" error where the first element is the phase where the
+ error occured and the second element is the error message. *)
+
+ exception Not_memoized of Options.category option
+ (** "Not memoized" error with the phase where the error occured. *)
+end
+
+module type S = sig
+ include Exn
+
+ val make_untypable: string -> exn
+ (** Make a [Typing_error] exception with the given message. *)
+
+ val make_not_yet: string -> exn
+ (** Make a [Not_yet] exception with the given message. *)
+
+ val make_not_memoized: unit -> exn
+ (** Make a [Not_memoized] exception with the given message. *)
+
+ val untypable: string -> 'a
+ (** @raise Typing_error with the given message. *)
+
+ val not_yet: string -> 'a
+ (** @raise Not_yet with the given message. *)
+
+ val not_memoized: unit -> 'a
+ (** @raise Not_memoized *)
+
+ val print_not_yet: string -> unit
+ (** Print the "not yet supported" message without raising an exception. *)
+
+ val handle: ('a -> 'a) -> 'a -> 'a
+ (** Run the closure with the given argument and handle potential errors.
+ Return the provide argument in case of errors. *)
+
+ val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+ (** Run the closure with the given argument and handle potential errors.
+ Return the additional argument in case of errors. *)
+
+ val nb_untypable: unit -> int
+ (** Number of untypable annotations. *)
+
+ val nb_not_yet: unit -> int
+ (** Number of not-yet-supported annotations. *)
+
+ val retrieve_preprocessing:
+ string ->
+ ('a -> 'b or_error) ->
+ 'a ->
+ (Format.formatter -> 'a -> unit) ->
+ 'b
+ (** Retrieve the result of a preprocessing phase, which possibly failed.
+ The [string] argument and the formatter are used to display a message in
+ case the preprocessing phase did not compute the required result. *)
+
+ val pp_or_error:
+ (Format.formatter -> 'a -> unit) ->
+ Format.formatter ->
+ 'a or_error ->
+ unit
+ (** [pp_or_error pp] where [pp] is a formatter for ['a] returns a formatter for
+ ['a or_error]. *)
+end
+
+(** Functor to build an [Error] module for a given [phase]. *)
+module Make(P: sig val phase:Options.category end): S
+
+(** The [Error] module implements [Error.S] with no phase. *)
+include S
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
--
GitLab