Merge branch 'feature/wp/fct-timeout' into 'master'

WP function timeout

See merge request frama-c/frama-c!3625

src/plugins/wp/Changelog

@@ -24,6 +24,8 @@
 Plugin WP <next-release>
 ########################
 
+- WP          [2022-02-28] New option -wp-fct-timeout, used to customize the
+                           provers timeout per function
 - WP          [2022-02-02] New option -wp-smoke-dead-local-init, smoke tests on
                            local variables initialization
 - WP          [2022-01-25] Removed deprecated "native:coq" prover

src/plugins/wp/ProverTask.ml

@@ -132,17 +132,6 @@ let location file line = {
   Lexing.pos_cnum = 0 ;
 }
 
-let timeout ~smoke = function
-  | None ->
-    if smoke
-    then Wp_parameters.SmokeTimeout.get ()
-    else Wp_parameters.Timeout.get ()
-  | Some t -> t
-
-let stepout = function
-  | None -> Wp_parameters.Steps.get ()
-  | Some t -> t
-
 let pp_file ~message ~file =
   if Sys.file_exists file then
     Log.print_on_output

src/plugins/wp/ProverTask.mli

@@ -54,8 +54,6 @@ val p_until_space : string (** No space group pattern "\\([^ \t\n]*\\)" *)
 
 val location : string -> int -> Lexing.position
 
-val timeout : smoke:bool -> int option -> int
-val stepout : int option -> int
 type logs = [ `OUT | `ERR | `BOTH ]
 
 class virtual command : string ->

src/plugins/wp/VCS.ml

@@ -164,11 +164,14 @@ let current () = {
 
 let default = { valid = false ; timeout = None ; stepout = None }
 
-let get_timeout ~smoke = function
+let get_timeout ?kf ~smoke = function
   | { timeout = None } ->
     if smoke
     then Wp_parameters.SmokeTimeout.get ()
-    else Wp_parameters.Timeout.get ()
+    else begin match Option.map Wp_parameters.FctTimeout.find kf with
+      | exception Not_found | None -> Wp_parameters.Timeout.get ()
+      | Some timeout -> timeout
+    end
   | { timeout = Some t } -> t
 
 let get_stepout = function

src/plugins/wp/VCS.mli

@@ -69,7 +69,9 @@ type config = {
 val current : unit -> config (** Current parameters *)
 val default : config (** all None *)
 
-val get_timeout : smoke:bool -> config -> int (** 0 means no-timeout *)
+val get_timeout : ?kf:Kernel_function.t -> smoke:bool -> config -> int
+(** 0 means no-timeout *)
+
 val get_stepout : config -> int (** 0 means no-stepout *)
 
 (** {2 Results} *)

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -1304,6 +1304,9 @@ See \texttt{-wp-interactive <mode>} option for details.
   on proved goals when available (default is: \texttt{no}).
 \item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
   to the decision prover (defaults to 10 seconds).
+\item[\tt -wp-fct-timeout <f1:t1,f2:t2,...>] customize the timeout for each
+  specified function (\texttt{t1} for \texttt{f1}, \texttt{t2} for \texttt{f2},
+  etc).
 \item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
   (see \verb+-wp-smoke-tests+, defaults to 5 seconds).
 \item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking

src/plugins/wp/prover.ml

@@ -35,8 +35,12 @@ let dispatch ?(config=VCS.default) mode prover wpo =
     | Qed | Tactical -> Task.return VCS.no_result
     | Why3 prover ->
       let smoke = Wpo.is_smoke_test wpo in
+      let kf = match Wpo.get_scope wpo with
+        | Global -> None
+        | Kf kf -> Some kf
+      in
       ProverWhy3.prove
-        ~timeout:(VCS.get_timeout ~smoke config)
+        ~timeout:(VCS.get_timeout ?kf ~smoke config)
         ~steplimit:(VCS.get_stepout config)
         ~mode ~prover wpo
   end

src/plugins/wp/wp_parameters.ml

@@ -797,6 +797,29 @@ module Timeout =
         "Set the timeout (in seconds) for provers (default: %d)." default
   end)
 
+let () = Parameter_customize.set_group wp_prover
+module FctTimeout =
+  Kernel_function_map
+    (struct
+      include Datatype.Int
+      type key = Cil_types.kernel_function
+      let of_string ~key:_ ~prev:_ s =
+        Option.map
+          (fun s ->
+             try int_of_string s
+             with Failure _ ->
+               raise (Cannot_build ("'" ^ s ^ "' is not an integer")))
+          s
+      let to_string ~key:_ = Option.map string_of_int
+    end)
+    (struct
+      let option_name = "-wp-fct-timeout"
+      let arg_name = "f1:t1,...,fn:tn"
+      let help = "Customize the WP timeout (in secondes) for each specified \
+                  function (t1 seconds for f1, t2 for f2, etc)."
+      let default = Kernel_function.Map.empty
+    end)
+
 let () = Parameter_customize.set_group wp_prover
 module SmokeTimeout =
   Int(struct

src/plugins/wp/wp_parameters.mli

@@ -121,6 +121,10 @@ module CacheDir: Parameter_sig.String
 module CachePrint: Parameter_sig.Bool
 module Drivers: Parameter_sig.String_list
 module Timeout: Parameter_sig.Int
+module FctTimeout:
+  Parameter_sig.Map
+  with type key = Cil_types.kernel_function
+   and type value = int
 module SmokeTimeout: Parameter_sig.Int
 module InteractiveTimeout: Parameter_sig.Int
 module TimeExtra: Parameter_sig.Int