Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 6c7c5d2c authored by Andrei Paskevich's avatar Andrei Paskevich

use Call_provers.prover_answer in why3ide and why3bench

parent 7036132a
......@@ -91,13 +91,8 @@ module BenchUtil =
struct
let print_proof_status fmt = function
| Db.Valid -> fprintf fmt "Valid"
| Db.Invalid -> fprintf fmt "Invalid"
| Db.Timeout -> fprintf fmt "Timeout"
| Db.Unknown -> fprintf fmt "Unknown"
| Db.Failure -> fprintf fmt "Failure"
| Db.HighFailure -> fprintf fmt "HighFailure"
| Db.Undone -> fprintf fmt "Undone"
| Db.Done a -> Call_provers.print_prover_answer fmt a
| Db.Undone -> fprintf fmt "Undone"
open Worker
......@@ -220,15 +215,7 @@ struct
let tl = apply_transl (task,db_goal) tr in
List.fold_left (apply_transll trl) acc tl
let proof_status_to_db_result pr =
match pr with
| {pr_answer = Valid} -> (Db.Valid,pr.pr_time)
| {pr_answer = Invalid} -> (Db.Invalid,pr.pr_time)
| {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
| {pr_answer = Failure _} -> (Db.Failure,pr.pr_time)
| {pr_answer = HighFailure} -> (Db.HighFailure,pr.pr_time)
| {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
let proof_status_to_db_result pr = (Db.Done pr.pr_answer, pr.pr_time)
end
......@@ -268,8 +255,9 @@ let call callback tool prob =
Debug.dprintf debug "Database has (%a,%f) for the goal@."
BenchUtil.print_proof_status proof_status time;
begin
if proof_status = Db.Valid ||
(proof_status = Db.Timeout && time > (float tool.ttime -. 0.1))
if proof_status = Db.Done Call_provers.Valid ||
(proof_status = Db.Done Call_provers.Timeout &&
time > (float tool.ttime -. 0.1))
then
callback pval i task (Cached (proof_status,time))
else
......@@ -438,23 +426,28 @@ let empty_tool_res =
match r with
| Done (answer,time) ->
begin match answer with
| Db.Valid -> {tr with valid = add_nb_avg tr.valid time}
| Db.Timeout -> {tr with timeout = add_nb_avg tr.timeout time}
| Db.Invalid -> {tr with invalid = add_nb_avg tr.invalid time}
| Db.Undone | Db.Unknown _ ->
{tr with unknown = add_nb_avg tr.unknown time}
| Db.Failure _ |Db.HighFailure ->
{tr with failure = add_nb_avg tr.failure time}
| Db.Done Call_provers.Valid ->
{tr with valid = add_nb_avg tr.valid time}
| Db.Done Call_provers.Timeout ->
{tr with timeout = add_nb_avg tr.timeout time}
| Db.Done Call_provers.Invalid ->
{tr with invalid = add_nb_avg tr.invalid time}
| Db.Undone | Db.Done (Call_provers.Unknown _) ->
{tr with unknown = add_nb_avg tr.unknown time}
| Db.Done (Call_provers.Failure _)
| Db.Done Call_provers.HighFailure ->
{tr with failure = add_nb_avg tr.failure time}
end
| InternalFailure _ ->
{tr with failure = add_nb_avg tr.failure 0.} in
{tr with failure = add_nb_avg tr.failure 0.} in
List.fold_left fold empty_tool_res l
let extract_time = function Done (_,t) -> t
| InternalFailure _ -> assert false
let filter_timeline l =
let l = List.filter (function {result = Done (Db.Valid,_)} -> true
let l = List.filter (function
| {result = Done (Db.Done Call_provers.Valid,_)} -> true
| _ -> false) l in
let compare_valid x y =
let c = compare (extract_time x.result)
......
......@@ -416,8 +416,8 @@ let () =
begin begin match res with
| B.Runned B.Done (ans,_) -> incr nb_done;
begin match ans with
| Db.Valid -> incr nb_valid
| _ -> () end
| Db.Done Call_provers.Valid -> incr nb_valid
| _ -> () end
| B.Runned B.InternalFailure _ -> incr nb_done; incr nb_failure
| B.Cached (_,_) -> incr nb_cached
end;
......
......@@ -216,13 +216,8 @@ module Htransf = Hashtbl.Make
type proof_status =
| Undone (** external proof attempt no done yet *)
| Valid (** external proof attempt succeeded *)
| Invalid (** external proof attempt found a counter-example *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| Failure (** external prover call failed *)
| HighFailure (** external prover call failed *)
| Undone (** external proof attempt not done yet *)
| Done of Call_provers.prover_answer (** external proof attempt done *)
type proof_attempt = int64
(*
......@@ -473,17 +468,23 @@ let transf_from_name n =
with Not_found -> TransfId.add db n
let status_array = [| Undone; Valid; Timeout; Unknown; Failure;
Invalid; HighFailure |]
let status_array = [|
Undone;
Done Call_provers.Valid;
Done Call_provers.Timeout;
Done (Call_provers.Unknown "");
Done (Call_provers.Failure "");
Done Call_provers.Invalid;
Done Call_provers.HighFailure; |]
let int64_from_status = function
| Undone -> 0L
| Valid -> 1L
| Invalid -> 5L
| Timeout -> 2L
| Unknown -> 3L
| Failure -> 4L
| HighFailure -> 6L
| Undone -> 0L
| Done Call_provers.Valid -> 1L
| Done Call_provers.Timeout -> 2L
| Done (Call_provers.Unknown _) -> 3L
| Done (Call_provers.Failure _) -> 4L
| Done Call_provers.Invalid -> 5L
| Done Call_provers.HighFailure -> 6L
let status_from_int64 i =
......
......@@ -54,13 +54,8 @@ type transf
(** status of an external proof attempt *)
type proof_status =
| Undone (** external proof attempt no done yet *)
| Valid (** external proof attempt succeeded *)
| Invalid (** external proof attempt found a counter-example *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| Failure (** external prover call failed *)
| HighFailure (** external prover call failed *)
| Undone (** external proof attempt not done yet *)
| Done of Call_provers.prover_answer (** external proof attempt done *)
(** parent of a goal: either a theory (for "toplevel" goals)
or a transformation (for "subgoals") *)
......
......@@ -231,13 +231,7 @@ module Model = struct
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Valid (** external proof attempt succeeded *)
| Invalid (** external proof attempt found a counter-example *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| Failure (** external prover call failed *)
| HighFailure (** external prover call failed *)
| Done of Call_provers.prover_answer (** external proof attempt done *)
type proof_attempt =
{ prover : prover_data;
......@@ -540,18 +534,18 @@ module Helpers = struct
match obsolete,result with
| _, Scheduled -> !image_scheduled
| _, Running -> !image_running
| false, Valid -> !image_valid
| false, Invalid -> !image_unknown (** TODO change *)
| false, Timeout -> !image_timeout
| false, Unknown -> !image_unknown
| false, Failure -> !image_failure
| false, HighFailure -> !image_failure
| true, Valid -> !image_valid_obs
| true, Invalid -> !image_unknown (** TODO change *)
| true, Timeout -> !image_timeout_obs
| true, Unknown -> !image_unknown_obs
| true, Failure -> !image_failure_obs
| true, HighFailure -> !image_failure_obs
| false, Done Call_provers.Valid -> !image_valid
| false, Done Call_provers.Invalid -> !image_unknown (** TODO change *)
| false, Done Call_provers.Timeout -> !image_timeout
| false, Done (Call_provers.Unknown _) -> !image_unknown
| false, Done (Call_provers.Failure _) -> !image_failure
| false, Done Call_provers.HighFailure -> !image_failure
| true, Done Call_provers.Valid -> !image_valid_obs
| true, Done Call_provers.Invalid -> !image_unknown_obs (** TODO change *)
| true, Done Call_provers.Timeout -> !image_timeout_obs
| true, Done (Call_provers.Unknown _) -> !image_unknown_obs
| true, Done (Call_provers.Failure _) -> !image_failure_obs
| true, Done Call_provers.HighFailure -> !image_failure_obs
let set_row_status b row =
if b then
......@@ -587,7 +581,8 @@ module Helpers = struct
let rec check_goal_proved g =
let b1 = Hashtbl.fold
(fun _ a acc -> acc || a.status = Valid) g.external_proofs false
(fun _ a acc -> acc || a.status = Done Call_provers.Valid)
g.external_proofs false
in
let b = Hashtbl.fold
(fun _ t acc -> acc || t.transf_proved) g.transformations b1
......@@ -858,15 +853,11 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Model.HighFailure
| Db.Valid ->
| Db.Undone -> Model.Done Call_provers.HighFailure
| Db.Done Call_provers.Valid ->
if not obsolete then proved := true;
Model.Valid
| Db.Invalid -> Model.Invalid
| Db.Unknown -> Model.Unknown
| Db.Timeout -> Model.Timeout
| Db.Failure -> Model.Failure
| Db.HighFailure -> Model.HighFailure
Model.Done Call_provers.Valid
| Db.Done a -> Model.Done a
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete ~edit goal p a s t
......@@ -1084,15 +1075,9 @@ let callback_of_callback callback = function
| Scheduler.Scheduled -> callback Model.Scheduled 0. ""
| Scheduler.Running -> callback Model.Running 0. ""
| Scheduler.InternalFailure _ ->
callback Model.HighFailure 0. "Prover call failed"
callback (Model.Done Call_provers.HighFailure) 0. "Prover call failed"
| Scheduler.Done r ->
let res = match r.Call_provers.pr_answer with
| Call_provers.Valid -> Model.Valid
| Call_provers.Timeout -> Model.Timeout
| Call_provers.Unknown _ -> Model.Unknown
| Call_provers.Invalid -> Model.Invalid
| Call_provers.Failure _ -> Model.Failure
| Call_provers.HighFailure -> Model.HighFailure in
let res = Model.Done r.Call_provers.pr_answer in
callback res r.Call_provers.pr_time r.Call_provers.pr_output
(* q is a queue of proof attempt where to put the new one *)
......@@ -1101,16 +1086,11 @@ let redo_external_proof q g a =
let callback result time output =
a.Model.output <- output;
Helpers.set_proof_status ~obsolete:false a result time ;
if result = Model.Valid
if result = Model.Done Call_provers.Valid
then Helpers.set_proved ~propagate:true a.Model.proof_goal;
let db_res = match result with
| Model.Scheduled | Model.Running -> Db.Undone
| Model.Valid -> Db.Valid
| Model.Invalid -> Db.Invalid
| Model.Unknown -> Db.Unknown
| Model.Timeout -> Db.Timeout
| Model.HighFailure -> Db.HighFailure
| Model.Failure -> Db.Failure
| Model.Done a -> Db.Done a
in
Db.set_status a.Model.proof_db db_res time
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment