From ff2e8223fcc489c170d2985775e90b74e55ef0d8 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Mon, 2 Sep 2024 08:18:43 +0900 Subject: [PATCH 1/3] rename reason to check_kind --- src/gnat/gnat_expl.ml | 59 ++++++++++++++++++------------------ src/gnat/gnat_expl.mli | 36 +++++++++++----------- src/gnat/gnat_objectives.ml | 10 +++--- src/gnat/gnat_objectives.mli | 2 +- src/gnat/gnat_report.ml | 6 ++-- src/gnat/gnat_report.mli | 4 +-- 6 files changed, 60 insertions(+), 57 deletions(-) diff --git a/src/gnat/gnat_expl.ml b/src/gnat/gnat_expl.ml index 1ececadbe..57872734b 100644 --- a/src/gnat/gnat_expl.ml +++ b/src/gnat/gnat_expl.ml @@ -1,7 +1,7 @@ open Why3 open Term -type reason = +type check_kind = (* VC_RTE_Kind - run-time checks *) | VC_Division_Check | VC_Index_Check @@ -67,7 +67,7 @@ type reason = | VC_Unreachable_Branch | VC_Dead_Code -let is_warning_reason r = +let is_warning_kind r = match r with (* VC_RTE_Kind - run-time checks *) | VC_Division_Check @@ -141,7 +141,7 @@ type subp_entity = Gnat_loc.loc type id = int type check = { id : id; - reason : reason; + check_kind : check_kind; sloc : Gnat_loc.loc; shape : string; already_proved : bool @@ -168,20 +168,20 @@ type limit_mode = let check_compare a b = let c = Stdlib.compare a.id b.id in if c <> 0 then c - else Stdlib.compare a.reason b.reason + else Stdlib.compare a.check_kind b.check_kind let check_equal a b = - Stdlib.(=) a.id b.id && Stdlib.(=) a.reason b.reason + Stdlib.(=) a.id b.id && Stdlib.(=) a.check_kind b.check_kind -let check_hash e = Hashcons.combine (Hashtbl.hash e.id) (Hashtbl.hash e.reason) +let check_hash e = Hashcons.combine (Hashtbl.hash e.id) (Hashtbl.hash e.check_kind) -let mk_check ?shape:shape reason id sloc ap = - { reason = reason; id = id ; sloc = sloc ; already_proved = ap; +let mk_check ?shape:shape check_kind id sloc ap = + { check_kind = check_kind; id = id ; sloc = sloc ; already_proved = ap; shape = match shape with None -> "" | Some s -> s } let get_loc c = c.sloc -let get_reason c = c.reason -let reason_from_string s = +let get_check_kind c = c.check_kind +let check_kind_from_string s = match s with (* VC_RTE_Kind - run-time checks *) | "VC_DIVISION_CHECK" -> VC_Division_Check @@ -250,11 +250,11 @@ let reason_from_string s = | "VC_UNREACHABLE_BRANCH" -> VC_Unreachable_Branch | "VC_DEAD_CODE" -> VC_Dead_Code | _ -> - let s = Format.sprintf "unknown VC reason: %s@." s in + let s = Format.sprintf "unknown VC kind: %s@." s in Gnat_util.abort_with_message ~internal:true s -let reason_to_ada reason = - match reason with +let check_kind_to_ada kind = + match kind with (* VC_RTE_Kind - run-time checks *) | VC_Division_Check -> "VC_DIVISION_CHECK" | VC_Index_Check -> "VC_INDEX_CHECK" @@ -322,8 +322,8 @@ let reason_to_ada reason = | VC_Unreachable_Branch -> "VC_UNREACHABLE_BRANCH" | VC_Dead_Code -> "VC_DEAD_CODE" -let reason_to_string reason = - match reason with +let check_kind_to_string kind = + match kind with (* VC_RTE_Kind - run-time checks *) | VC_Division_Check -> "division_check" | VC_Index_Check -> "index_check" @@ -390,7 +390,7 @@ let reason_to_string reason = | VC_Dead_Code -> "dead_code" type gp_label = - | Gp_Check of int * reason * Gnat_loc.loc + | Gp_Check of int * check_kind * Gnat_loc.loc | Gp_Pretty_Ada of int | Gp_Shape of string | Gp_Already_Proved @@ -398,9 +398,9 @@ type gp_label = let parse_check_string s l = match l with - | id::reason_string::sloc_rest -> + | id::check_kind_string::sloc_rest -> begin try - Gp_Check (int_of_string id, reason_from_string reason_string, Gnat_loc.parse_loc sloc_rest) + Gp_Check (int_of_string id, check_kind_from_string check_kind_string, Gnat_loc.parse_loc sloc_rest) with e when Debug.test_flag Debug.stack_trace -> raise e | Failure _ -> let s = @@ -447,7 +447,7 @@ let read_label s = type my_expl = { mutable check_id : int option; - mutable check_reason : reason option; + mutable check_kind : check_kind option; mutable extra_node : int option; mutable check_sloc : Gnat_loc.loc option; mutable shape : string option; @@ -459,13 +459,14 @@ type my_expl = let default_expl = { check_id = None; - check_reason = None; + check_kind = None; check_sloc = None; extra_node = None; shape = None; already_proved = false; inline = None; } + let read_vc_labels acc s = (* This function takes a set of labels and extracts a "node_info" from that set. We start with an empty record; We fill it up by iterating over all @@ -475,8 +476,8 @@ let read_vc_labels acc s = (fun x -> let s = x.Ident.attr_string in match read_label s with - | Some Gp_Check (id, reason, sloc) -> - b.check_reason <- Some reason; + | Some Gp_Check (id, kind, sloc) -> + b.check_kind <- Some kind; b.check_id <- Some id; b.check_sloc <- Some sloc; | Some Gp_Pretty_Ada node -> @@ -493,14 +494,14 @@ let read_vc_labels acc s = ) s; (* We potentially need to rectify in the case of loop invariants: We need to check whether the VC is for initialization or preservation *) - if b.check_reason = Some VC_Loop_Invariant then begin + if b.check_kind = Some VC_Loop_Invariant then begin Ident.Sattr.iter (fun x -> let s = x.Ident.attr_string in if Strings.has_prefix "expl:" s then if s = "expl:loop invariant init" then - b.check_reason <- Some VC_Loop_Invariant_Init + b.check_kind <- Some VC_Loop_Invariant_Init else - b.check_reason <- Some VC_Loop_Invariant_Preserv) s + b.check_kind <- Some VC_Loop_Invariant_Preserv) s end; b @@ -508,11 +509,11 @@ let read_vc_labels acc s = let extract_check b = match b with | { check_id = Some id ; - check_reason = Some reason; + check_kind = Some check_kind; check_sloc = Some sloc; shape = shape; already_proved = ap; } -> - Some (mk_check ?shape reason id sloc ap) + Some (mk_check ?shape check_kind id sloc ap) | _ -> None (* Copied from Termcode and modified to use an accumulator. Traverse the @@ -550,7 +551,7 @@ let to_filename fmt check = let file, line, col = Gnat_loc.explode x in Format.fprintf fmt "%s_%d_%d_" file line col; ) check.sloc; - Format.fprintf fmt "%s" (reason_to_string check.reason) + Format.fprintf fmt "%s" (check_kind_to_string check.check_kind) let parse_line_spec s = try @@ -565,7 +566,7 @@ let parse_line_spec s = | [fn;line;col;check] -> let line = int_of_string line in let col = int_of_string col in - let check = reason_from_string check in + let check = check_kind_from_string check in let loc = Gnat_loc.mk_loc fn line col None in Limit_Check (mk_check check 0 loc false) | _ -> diff --git a/src/gnat/gnat_expl.mli b/src/gnat/gnat_expl.mli index 3617f3ec0..df88c2ab8 100644 --- a/src/gnat/gnat_expl.mli +++ b/src/gnat/gnat_expl.mli @@ -5,7 +5,7 @@ open Why3 type id = int -type reason = +type check_kind = (* VC_RTE_Kind - run-time checks *) | VC_Division_Check | VC_Index_Check @@ -71,20 +71,22 @@ type reason = | VC_Unreachable_Branch | VC_Dead_Code -val is_warning_reason : reason -> bool +val is_warning_kind : check_kind -> bool (* returns whether a VC is generated to issue possibly a warning *) type check = { id : id; - reason : reason; + check_kind : check_kind; sloc : Gnat_loc.loc; shape : string; already_proved : bool } -(* A check is equal to a check ID as provided by gnat2why, as well as a reason. - We need the reason because in the case of a loop invariant, there is a - single check id, but in fact two checks (initialization and preservation). - A check can be proved already (e.g. by CodePeer). +(* A check is equal to a check ID as provided by gnat2why, as well as a check kind. + We need the check kind even though gnat2why already knows it, because in the + case of a loop invariant, there is a single check id (VC_Loop_Invariant), + but in fact two checks (VC_Loop_Invariant_Init and + VC_Loop_Invariant_Preserv). A check can be proved already (e.g. by + CodePeer). *) type extra_info = @@ -108,7 +110,7 @@ type subp_entity = Gnat_loc.loc (* the type of labels that are used by gnatprove and recognized by gnatwhy3 *) type gp_label = - | Gp_Check of int * reason * Gnat_loc.loc + | Gp_Check of int * check_kind * Gnat_loc.loc (* used to indicate the ID, VC Kind and sloc of a VC *) | Gp_Pretty_Ada of int (* label "GP_Pretty_Ada" used to give an Ada source node for some @@ -130,22 +132,22 @@ val read_label : string -> gp_label option val check_compare : check -> check -> int val get_loc : check -> Gnat_loc.loc -val get_reason : check -> reason +val get_check_kind : check -> check_kind -(* Conversion functions between a reason string and the OCaml type are +(* Conversion functions between a check_kind string and the OCaml type are used only for debugging. The actual message tag is set by gnat2why directly. *) -val reason_from_string : string -> reason -(* parse a reason string from Ada into the OCaml type *) -val reason_to_ada : reason -> string -(* print a reason from the OCaml type into the Ada representation *) +val check_kind_from_string : string -> check_kind +(* parse a check string from Ada into the OCaml type *) +val check_kind_to_ada : check_kind -> string +(* print a check from the OCaml type into the Ada representation *) val to_filename : Format.formatter -> check -> unit (* print a representation of a check that could serve as a filename *) -val mk_check : ?shape:string -> reason -> id -> Gnat_loc.loc -> bool -> check -(* [mk_expl reason id sloc already_proved] - reason - the kind of check for this VC +val mk_check : ?shape:string -> check_kind -> id -> Gnat_loc.loc -> bool -> check +(* [mk_expl check id sloc already_proved] + check - the kind of check for this VC id - the id of the VC sloc - the sloc of the VC already_proved - if the VC needs proof or not diff --git a/src/gnat/gnat_objectives.ml b/src/gnat/gnat_objectives.ml index 2db437b6c..af1e864fa 100644 --- a/src/gnat/gnat_objectives.ml +++ b/src/gnat/gnat_objectives.ml @@ -214,7 +214,7 @@ let add_to_objective ~toplevel ex go = | Gnat_expl.Limit_Line l -> Gnat_loc.equal_line l (Gnat_expl.get_loc check) | Gnat_expl.Limit_Check c -> - (c.Gnat_expl.reason = Gnat_expl.get_reason check) + (c.Gnat_expl.check_kind = Gnat_expl.get_check_kind check) && (Gnat_loc.equal_orig_loc c.Gnat_expl.sloc (Gnat_expl.get_loc check)) ) Gnat_config.limit_lines in @@ -479,7 +479,7 @@ let has_been_tried_by s (g: goal_id) (prover: Whyconf.prover) = try let paid = Whyconf.Hprover.find proof_attempt_set prover in let pa = Session_itp.get_proof_attempt_node s paid in - let warn = Gnat_expl.is_warning_reason (Gnat_expl.get_reason (get_objective g)) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind (get_objective g)) in (* only count non-obsolete proof attempts with identical options *) (not pa.Session_itp.proof_obsolete && @@ -609,7 +609,7 @@ let register_result c goal result : 'a * 'b = (* The prover run was scheduled just to get counterexample *) obj, Not_Proved else - let warn = Gnat_expl.is_warning_reason (Gnat_expl.get_reason obj) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind obj) in if not warn then begin (* We first remove the goal from the list of goals to be tried. It may be * put back later, see below *) @@ -991,7 +991,7 @@ let run_goal ?proof_script_filename ?limit ~callback c prover g = end else let check = get_objective g in - let warn = Gnat_expl.is_warning_reason (Gnat_expl.get_reason check) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind check) in let limit = match limit with | None -> Gnat_config.limit ~prover ~warning:warn @@ -1021,7 +1021,7 @@ let schedule_goal ~callback c g = immediately. *) let check = get_objective g in let s = c.Controller_itp.controller_session in - let warn = Gnat_expl.is_warning_reason (Gnat_expl.get_reason check) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind check) in if Gnat_config.parallel > 1 then begin let provers = if warn then [Option.get (Gnat_config.prover_warn)] else Gnat_config.provers diff --git a/src/gnat/gnat_objectives.mli b/src/gnat/gnat_objectives.mli index 00655f157..1961ed4ba 100644 --- a/src/gnat/gnat_objectives.mli +++ b/src/gnat/gnat_objectives.mli @@ -2,7 +2,7 @@ better part of scheduling of VCs. An objective is something to be proved in Ada, say, a range check. An - objective is defined by an explanation (reason + Ada location). + objective is defined by an explanation (check kind + Ada location). A goal is a VC that will be sent to Alt-Ergo. In general, there will be many goals for each objective. Each goal has a trace (list of locations). diff --git a/src/gnat/gnat_report.ml b/src/gnat/gnat_report.ml index 7aa8249db..4ddb19091 100644 --- a/src/gnat/gnat_report.ml +++ b/src/gnat/gnat_report.ml @@ -90,12 +90,12 @@ let get_cntexmp_models = let t = Ident.Sattr.fold Term.t_attr_add ctx.Pinterp_core.attrs t in let check = match Gnat_expl.search_labels t with - | Some Gnat_expl.{check={id; reason; sloc}} -> + | Some Gnat_expl.{check={id; check_kind; sloc}} -> let file, line, col = Gnat_loc.explode (Gnat_loc.orig_loc sloc) in Record [ "id", Int id; - "vc_kind", String (Gnat_expl.reason_to_ada reason); + "vc_kind", String (Gnat_expl.check_kind_to_ada check_kind); "sloc", Record [ "file", String file; "line", Int line; @@ -165,7 +165,7 @@ let get_msg (check, m) = Record ( List.concat [ [ "id", Int check.Gnat_expl.id ; - "reason", String (Gnat_expl.reason_to_ada check.Gnat_expl.reason) ; + "check_kind", String (Gnat_expl.check_kind_to_ada check.Gnat_expl.check_kind) ; "result", Bool m.result ; "check_tree", m.check_tree ; "extra_info", get_extra_info m.extra_info diff --git a/src/gnat/gnat_report.mli b/src/gnat/gnat_report.mli index 337e76c27..f03af8e68 100644 --- a/src/gnat/gnat_report.mli +++ b/src/gnat/gnat_report.mli @@ -28,7 +28,7 @@ open Why3 that occured during execution of gnatwhy3. result = { "id" : int, - "reason" : string, + "check_kind" : string, "result" : bool, "extra_info" : extra_info, "vc_file" : string, @@ -37,7 +37,7 @@ open Why3 "cntexmp" : cntexmp_rec } - The field "id" contains the id of the VC. The field "reason" identifies the + The field "id" contains the id of the VC. The field "check_kind" identifies the kind of the VC, such as "overflow_check" etc. The field "result" tells if the VC has been proved or not. The field "extra_info" specifies more precisely the part of the VC (see below). The fields "vc_file" and From 2478f2ce881a394eb8f22fcd69668868cd08e137 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Mon, 2 Sep 2024 09:13:20 +0900 Subject: [PATCH 2/3] rename objective to check --- src/gnat/gnat_main.ml | 36 +++---- src/gnat/gnat_objectives.ml | 196 +++++++++++++++++------------------ src/gnat/gnat_objectives.mli | 87 ++++++++-------- 3 files changed, 156 insertions(+), 163 deletions(-) diff --git a/src/gnat/gnat_main.ml b/src/gnat/gnat_main.ml index 9c164f54f..1867f3be6 100644 --- a/src/gnat/gnat_main.ml +++ b/src/gnat/gnat_main.ml @@ -7,14 +7,14 @@ - it generates a summary of what was proved and not proved in JSON format and outputs this JSON format to stdout (for gnat2why to read). - See gnat_objectives.mli for the notion of objective and goal. + See gnat_objectives.mli for the notion of check and goal. See gnat_report.mli for the JSON format gnat_main can be seen as the "driver" for gnatwhy3. Much of the functionality is elsewhere. Specifically, this file does: - - compute the objective that belongs to a goal/VC + - compute the check that belongs to a goal/VC - drive the scheduling of VCs, and handling of results - output the messages *) @@ -69,7 +69,7 @@ let register_goal cont goal_id = if c.Gnat_expl.check.Gnat_expl.already_proved then Gnat_objectives.set_not_interesting goal_id else - Gnat_objectives.add_to_objective c goal_id + Gnat_objectives.add_to_check c goal_id end let rec handle_vc_result c goal result = @@ -78,16 +78,16 @@ let rec handle_vc_result c goal result = result a boolean, true if the prover has proved the VC prover_result the actual proof result, to extract statistics *) - let obj, status = C.register_result c goal result in + let check, status = C.register_result c goal result in match status with | Gnat_objectives.Proved -> () | Gnat_objectives.Not_Proved -> () | Gnat_objectives.Work_Left -> - List.iter (create_manual_or_schedule c obj) (Gnat_objectives.next obj) + List.iter (create_manual_or_schedule c check) (Gnat_objectives.next check) | Gnat_objectives.Counter_Example -> (* In this case, counterexample prover and VC will be never None *) let prover_ce = (Option.get Gnat_config.prover_ce) in - match Gnat_objectives.ce_goal obj with + match Gnat_objectives.ce_goal check with | None -> assert false | Some g -> C.schedule_goal_with_prover c ~callback:(interpret_result c) g prover_ce @@ -149,12 +149,12 @@ and schedule_goal (c: Controller_itp.controller) (g : Session_itp.proofNodeID) = and actually_schedule_goal c g = C.schedule_goal ~callback:(interpret_result c) c g -let handle_obj c obj = - if Gnat_objectives.objective_status obj <> Gnat_objectives.Proved then begin - match Gnat_objectives.next obj with +let handle_obj c check = + if Gnat_objectives.check_status check <> Gnat_objectives.Proved then begin + match Gnat_objectives.next check with | [] -> () | l -> - List.iter (create_manual_or_schedule c obj) l + List.iter (create_manual_or_schedule c check) l end let all_split_subp c subp = @@ -197,15 +197,15 @@ let maybe_giant_step_rac ctr parent models = (Gnat_counterexamples.post_clean#model m, Some res)) ) models) -let report_messages c obj = +let report_messages c check = let s = c.Controller_itp.controller_session in let result = - if C.session_proved_status c obj then - let (stats, stat_checker) = C.Save_VCs.extract_stats c obj in + if C.session_proved_status c check then + let (stats, stat_checker) = C.Save_VCs.extract_stats c check in Gnat_report.Proved (stats, stat_checker) else let models = - let ce_pa = C.session_find_ce_pa c obj in + let ce_pa = C.session_find_ce_pa c check in match ce_pa with | None -> [] | Some pa -> @@ -217,13 +217,13 @@ let report_messages c obj = let models = List.filter not_step_limit pr.Call_provers.pr_models in maybe_giant_step_rac c ce_pan.Session_itp.parent models in - let unproved_pa = C.session_find_unproved_pa c obj in + let unproved_pa = C.session_find_unproved_pa c check in let manual_info = Opt.bind unproved_pa (Gnat_manual.manual_proof_info s) in let unproved_goal = (* In some cases (replay) no proofattempt proves the goal but we still want a task to be able to extract the expl from it. *) match unproved_pa with - | None -> C.session_find_unproved_goal c obj + | None -> C.session_find_unproved_goal c check | Some pa -> Some (Session_itp.get_proof_attempt_parent s pa) in let extra_info = @@ -246,7 +246,7 @@ let report_messages c obj = else { Gnat_expl.pretty_node = None; inlined = None } in Gnat_report.Not_Proved (extra_info, models, manual_info) in - Gnat_report.register obj (C.Save_VCs.check_to_json s obj) result + Gnat_report.register check (C.Save_VCs.check_to_json s check) result (* Escaping all debug printings *) let escape_buffer = Buffer.create 42 @@ -296,7 +296,7 @@ let save_session_and_exit c signum = (* This is the main code. We read the file into the session if not already done, we apply the split_goal transformation when needed, and we schedule - the first VC of all objectives. When done, we save the session. + the first VC of all check. When done, we save the session. *) let _ = diff --git a/src/gnat/gnat_objectives.ml b/src/gnat/gnat_objectives.ml index af1e864fa..d1797a941 100644 --- a/src/gnat/gnat_objectives.ml +++ b/src/gnat/gnat_objectives.ml @@ -9,10 +9,6 @@ type subp = { subp_goal : goal_id } correctness formula for a subp). We use a different type to avoid confusion with regular goals. *) -type objective = Gnat_expl.check -(* an objective is identified by its explanation, which contains the source - location and the kind of the check *) - type status = | Proved | Not_Proved @@ -154,23 +150,23 @@ struct with Found k -> k end -type objective_rec = +type check_rec = { to_be_scheduled : GoalSet.t; (* when a goal is scheduled, it is removed from this set *) to_be_proved : GoalSet.t; (* when a goal is proved (or unproved), it is removed from this set *) toplevel : GoalSet.t; (* the set of top-level goals, that is not obtained by transformation. - * They are "entry points" of the objective into the Why3 session *) + * They are "entry points" of the check into the Why3 session *) mutable not_proved : bool; - (* when a goal is not proved, the objective is marked "not proved" by + (* when a goal is not proved, the check is marked "not proved" by * setting this boolean to "true" *) mutable counter_example : goal_id option; (* when a goal is not proved, store the counterexample VC in this field *) } -(* an objective consists of to be scheduled and to be proved goals *) +(* a check consists of to be scheduled and to be proved goals *) -let empty_objective () = +let empty_check () = { to_be_scheduled = GoalSet.empty (); to_be_proved = GoalSet.empty (); toplevel = GoalSet.empty (); @@ -179,14 +175,14 @@ let empty_objective () = } (* The state of the module consists of these mutable structures *) -let explmap : objective_rec Gnat_expl.HCheck.t = Gnat_expl.HCheck.create 17 -(* maps proof objectives to goals *) +let explmap : check_rec Gnat_expl.HCheck.t = Gnat_expl.HCheck.create 17 +(* maps proof checks to goals *) let goalmap : Gnat_expl.vc_info GoalMap.t = GoalMap.create 17 -(* maps goals to their objectives *) +(* maps goals to their checks *) let total_nb_goals : int ref = ref 0 -let nb_objectives : int ref = ref 0 +let nb_checks : int ref = ref 0 let not_interesting : GoalSet.t = GoalSet.empty () @@ -195,19 +191,19 @@ let clear () = GoalMap.clear goalmap; GoalSet.reset not_interesting; total_nb_goals := 0; - nb_objectives := 0 + nb_checks := 0 let find e = try Gnat_expl.HCheck.find explmap e with Not_found -> - let r = empty_objective () in + let r = empty_check () in Gnat_expl.HCheck.add explmap e r; - incr nb_objectives; + incr nb_checks; r -let add_to_objective ~toplevel ex go = +let add_to_check ~toplevel ex go = let check = ex.Gnat_expl.check in - (* add a goal to an objective. + (* add a goal to a check. * A goal can be "top-level", that is a direct goal coming from WP, or not * top-level, that is obtained by transformation. *) let filter_line = Gnat_config.limit_lines = [] || List.exists (function @@ -227,19 +223,19 @@ let add_to_objective ~toplevel ex go = if filter_line && filter_region then begin incr total_nb_goals; GoalMap.add goalmap go ex; - let obj = find check in - GoalSet.add obj.to_be_scheduled go; - GoalSet.add obj.to_be_proved go; - if toplevel then GoalSet.add obj.toplevel go; + let cr = find check in + GoalSet.add cr.to_be_scheduled go; + GoalSet.add cr.to_be_proved go; + if toplevel then GoalSet.add cr.toplevel go; end let get_vc_info goal = GoalMap.find goalmap goal -let get_objective goal = (get_vc_info goal).Gnat_expl.check +let get_check_of_goal goal = (get_vc_info goal).Gnat_expl.check let get_extra_info goal = (get_vc_info goal).Gnat_expl.extra_info let add_clone derive goal = - let obj = get_vc_info derive in - add_to_objective ~toplevel:false obj goal + let check = get_vc_info derive in + add_to_check ~toplevel:false check goal let trivial_prover = { Whyconf.prover_name = "Trivial"; @@ -268,21 +264,21 @@ let add_trivial_proof s goal_id = Session_itp.update_goal_node (fun _ -> ()) s goal_id -let add_to_objective = add_to_objective ~toplevel:true -(* we mask the add_to_objective function here and fix it's toplevel argument to +let add_to_check = add_to_check ~toplevel:true +(* we mask the add_to_check function here and fix it's toplevel argument to "true", so that outside calls always set toplevel to true *) let set_not_interesting x = GoalSet.add not_interesting x let is_not_interesting x = GoalSet.mem not_interesting x let is_interesting x = not (is_not_interesting x) -let next objective = +let next check = (* this lookup should always succeed, otherwise it would mean we have a corrupt database *) - let obj_rec = Gnat_expl.HCheck.find explmap objective in + let check_rec = Gnat_expl.HCheck.find explmap check in try - let goal = GoalSet.choose obj_rec.to_be_scheduled in - GoalSet.remove obj_rec.to_be_scheduled goal; + let goal = GoalSet.choose check_rec.to_be_scheduled in + GoalSet.remove check_rec.to_be_scheduled goal; [goal] with Not_found -> [] @@ -459,19 +455,19 @@ let init_cont () = (Pp.print_list Pp.space Exn_printer.exn_printer) l) end -let objective_status obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in - if obj_rec.counter_example <> None then Counter_Example - else if GoalSet.is_empty obj_rec.to_be_proved then - if obj_rec.not_proved then Not_Proved else Proved - else if GoalSet.is_empty obj_rec.to_be_scheduled then +let check_status check = + let check_rec = Gnat_expl.HCheck.find explmap check in + if check_rec.counter_example <> None then Counter_Example + else if GoalSet.is_empty check_rec.to_be_proved then + if check_rec.not_proved then Not_Proved else Proved + else if GoalSet.is_empty check_rec.to_be_scheduled then Not_Proved else Work_Left -let ce_goal obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in - obj_rec.counter_example +let ce_goal check = + let check_rec = Gnat_expl.HCheck.find explmap check in + check_rec.counter_example let has_been_tried_by s (g: goal_id) (prover: Whyconf.prover) = (* Check whether the goal has been tried already *) @@ -479,7 +475,7 @@ let has_been_tried_by s (g: goal_id) (prover: Whyconf.prover) = try let paid = Whyconf.Hprover.find proof_attempt_set prover in let pa = Session_itp.get_proof_attempt_node s paid in - let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind (get_objective g)) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind (get_check_of_goal g)) in (* only count non-obsolete proof attempts with identical options *) (not pa.Session_itp.proof_obsolete && @@ -512,19 +508,19 @@ let iter_leaf_goals s subp f = iter_leafs s subp.subp_goal f let iter f = - let obj = Gnat_expl.HCheck.fold (fun k _ acc -> k :: acc) explmap [] in - List.iter f obj + let check = Gnat_expl.HCheck.fold (fun k _ acc -> k :: acc) explmap [] in + List.iter f check -let unproved_vc_continue obj obj_rec = +let unproved_vc_continue check check_rec = (* This function checks whether proof should continue even though we have an unproved VC. This function raises Exit when: * lazy mode is on (default) * no more VCs left - otherwise it returns obj, Work_Left *) - obj_rec.not_proved <- true; + otherwise it returns check, Work_Left *) + check_rec.not_proved <- true; if Gnat_config.lazy_ then raise Exit; - if GoalSet.is_empty obj_rec.to_be_proved then raise Exit; - obj, Work_Left + if GoalSet.is_empty check_rec.to_be_proved then raise Exit; + check, Work_Left (* This function only gets the subgoals of the gnat_split transformation. It is part of a code that should not be used when other transformations (manual @@ -603,71 +599,71 @@ let add_ce_goal c goal = with Not_found -> goal let register_result c goal result : 'a * 'b = - let obj = get_objective goal in - let obj_rec = Gnat_expl.HCheck.find explmap obj in - if obj_rec.counter_example <> None then + let check = get_check_of_goal goal in + let check_rec = Gnat_expl.HCheck.find explmap check in + if check_rec.counter_example <> None then (* The prover run was scheduled just to get counterexample *) - obj, Not_Proved + check, Not_Proved else - let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind obj) in + let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind check) in if not warn then begin (* We first remove the goal from the list of goals to be tried. It may be * put back later, see below *) - GoalSet.remove obj_rec.to_be_proved goal; + GoalSet.remove check_rec.to_be_proved goal; if result then (* goal has been proved, we only need to store that info *) - if not (GoalSet.is_empty obj_rec.to_be_proved) then - obj, Work_Left + if not (GoalSet.is_empty check_rec.to_be_proved) then + check, Work_Left else - if obj_rec.not_proved then - obj, Not_Proved - else obj, Proved + if check_rec.not_proved then + check, Not_Proved + else check, Proved else begin try (* the goal was not proved. *) (* We first check whether another prover may apply *) if Gnat_config.parallel = 1 && Gnat_config.manual_prover = None && not (all_provers_tried c.Controller_itp.controller_session goal) then begin (* put the goal back to be scheduled and proved *) - GoalSet.add obj_rec.to_be_scheduled goal; - GoalSet.add obj_rec.to_be_proved goal; - obj, Work_Left + GoalSet.add check_rec.to_be_scheduled goal; + GoalSet.add check_rec.to_be_proved goal; + check, Work_Left end else begin (* This particular goal has been tried with all provers. But maybe we can split/apply transformations. *) if is_full_split_goal c.Controller_itp.controller_session goal then - unproved_vc_continue obj obj_rec + unproved_vc_continue check check_rec else let new_goals = further_split c goal; subsubgoals c.Controller_itp.controller_session goal in - if new_goals = [] then unproved_vc_continue obj obj_rec + if new_goals = [] then unproved_vc_continue check check_rec else begin (* if we are here, it means we have simplified the goal. We add the new goals to the set of goals to be proved/scheduled. *) List.iter (add_clone goal) new_goals; - obj, Work_Left + check, Work_Left end end with Exit -> - (* if we cannot simplify, the objective has been disproved *) - GoalSet.reset obj_rec.to_be_scheduled; + (* if we cannot simplify, the check has been disproved *) + GoalSet.reset check_rec.to_be_scheduled; if Gnat_config.counterexamples then begin (* The goal will be scheduled to get a counterexample *) - obj_rec.not_proved <- true; + check_rec.not_proved <- true; let ce_goal = add_ce_goal c goal in - obj_rec.counter_example <- Some ce_goal; + check_rec.counter_example <- Some ce_goal; GoalMap.add goalmap ce_goal (get_vc_info goal); (* The goal will be scheduled manually in Gnat_main.handle_result - so it is not put to the obj_rec.to_be_scheduled *) - obj, Counter_Example + so it is not put to the check_rec.to_be_scheduled *) + check, Counter_Example end else - obj, Not_Proved + check, Not_Proved end end else - obj, (if result then Proved else Not_Proved) + check, (if result then Proved else Not_Proved) let iter_main_goals s fu = (* Main goals are at the following point in the theory: @@ -858,13 +854,13 @@ module Save_VCs = struct (Session_itp.get_transformations ses goal); with Exit -> () - let extract_stats c (obj : objective) = + let extract_stats c (check : Gnat_expl.check) = (* Hold the stats for provers *) let stats = Whyconf.Hprover.create 5 in (* stat_checker = number of goal proved by a transformation *) let stat_checkers = ref 0 in - let obj_rec = Gnat_expl.HCheck.find explmap obj in - GoalSet.iter (extract_stat_goal c stats stat_checkers) obj_rec.toplevel; + let check_rec = Gnat_expl.HCheck.find explmap check in + GoalSet.iter (extract_stat_goal c stats stat_checkers) check_rec.toplevel; (stats, !stat_checkers) let count_map : (int ref) Gnat_expl.HCheck.t = Gnat_expl.HCheck.create 17 @@ -892,7 +888,7 @@ module Save_VCs = struct Pp.sprintf "%a%s%s" Gnat_expl.to_filename check count_str ext let save_vc c goal (prover: Whyconf.prover) = - let check = get_objective goal in + let check = get_check_of_goal goal in let driver = snd (Whyconf.Hprover.find c.Controller_itp.controller_provers prover) in (* Reusing a filename to get several prover files with the same name is @@ -907,10 +903,10 @@ module Save_VCs = struct More precisely a session forest, because we start with a list of goals for a given check. See gnat_report.mli for the JSON structure that we use here. *) - let rec check_to_json session obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in + let rec check_to_json session check = + let check_rec = Gnat_expl.HCheck.find explmap check in let l = ref [] in - GoalSet.iter (fun x -> l := goal_to_json session x :: !l) obj_rec.toplevel; + GoalSet.iter (fun x -> l := goal_to_json session x :: !l) check_rec.toplevel; Json_base.List !l and goal_to_json session g = Json_base.Record [ @@ -973,7 +969,7 @@ let run_goal ?proof_script_filename ?limit ~callback c prover g = begin match old_file with | None -> - let check = get_objective g in + let check = get_check_of_goal g in let new_file = Sysutil.system_independent_path_of_file (Gnat_manual.create_prover_file c g check prover) in let _paid, _file, _ores = C.prepare_edition c ~file:new_file @@ -990,7 +986,7 @@ let run_goal ?proof_script_filename ?limit ~callback c prover g = ~limit:Call_provers.empty_limit ~callback ~notification end else - let check = get_objective g in + let check = get_check_of_goal g in let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind check) in let limit = match limit with @@ -1019,7 +1015,7 @@ let schedule_goal_with_prover ~callback c g p = let schedule_goal ~callback c g = (* actually schedule the goal, ie call the prover. This function returns immediately. *) - let check = get_objective g in + let check = get_check_of_goal g in let s = c.Controller_itp.controller_session in let warn = Gnat_expl.is_warning_kind (Gnat_expl.get_check_kind check) in if Gnat_config.parallel > 1 then begin @@ -1061,7 +1057,7 @@ let all_split_leaf_goals () = iter_leafs g (fun goal -> let is_registered = - try ignore (get_objective goal); true + try ignore (get_check_of_goal goal); true with Not_found -> false in if is_registered then if is_full_split_goal goal then begin Save_VCs.save_vc goal end @@ -1091,10 +1087,10 @@ let is_valid_not_ce session g = transformations_list in (b || b') -let session_proved_status c obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in +let session_proved_status c check = + let check_rec = Gnat_expl.HCheck.find explmap check in let session = c.Controller_itp.controller_session in - GoalSet.for_all (fun x -> is_valid_not_ce session x) obj_rec.toplevel + GoalSet.for_all (fun x -> is_valid_not_ce session x) check_rec.toplevel let finished_but_not_valid_or_unedited pa = (* return true if the proof attempt in argument has terminated, but did not @@ -1138,8 +1134,8 @@ let select_appropriate_proof_attempt pa = finished_but_not_valid_or_unedited pa && List.exists (fun p -> p = pa.Session_itp.prover) Gnat_config.provers -let session_find_unproved_pa c obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in +let session_find_unproved_pa c check = + let check_rec = Gnat_expl.HCheck.find explmap check in let session = c.Controller_itp.controller_session in let traversal_function () g = match g with @@ -1158,15 +1154,15 @@ let session_find_unproved_pa c obj = Session_itp.fold_all_any session traversal_function () (Session_itp.APn g) in try - GoalSet.iter iter_on_sub_goal obj_rec.toplevel; + GoalSet.iter iter_on_sub_goal check_rec.toplevel; None with PA_Found p -> Some p -let session_find_ce_pa c obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in +let session_find_ce_pa c check = + let check_rec = Gnat_expl.HCheck.find explmap check in let session = c.Controller_itp.controller_session in - match obj_rec.counter_example with + match check_rec.counter_example with | None -> None | Some g -> @@ -1183,9 +1179,9 @@ let is_ce_goal s g = | Some tr when tr = ce_transform -> true | _ -> false -let session_find_unproved_goal c obj = +let session_find_unproved_goal c check = - let obj_rec = Gnat_expl.HCheck.find explmap obj in + let check_rec = Gnat_expl.HCheck.find explmap check in let session = c.Controller_itp.controller_session in let traversal_function () g = match g with @@ -1199,7 +1195,7 @@ let session_find_unproved_goal c obj = Session_itp.fold_all_any session traversal_function () (Session_itp.APn g) in try - GoalSet.iter iter_on_sub_goal obj_rec.toplevel; + GoalSet.iter iter_on_sub_goal check_rec.toplevel; None with Found_goal_id p -> Some p @@ -1286,12 +1282,12 @@ and replay_goal c goal = ~notification:(fun _ -> ())) prover -let replay_obj session obj = - let obj_rec = Gnat_expl.HCheck.find explmap obj in - GoalSet.iter (replay_goal session) obj_rec.toplevel +let replay_check session check = + let check_rec = Gnat_expl.HCheck.find explmap check in + GoalSet.iter (replay_goal session) check_rec.toplevel let replay session = - iter (replay_obj session) + iter (replay_check session) (* This register an observer that can monitor the number of provers waiting/scheduled/running *) diff --git a/src/gnat/gnat_objectives.mli b/src/gnat/gnat_objectives.mli index 1961ed4ba..acbb096b9 100644 --- a/src/gnat/gnat_objectives.mli +++ b/src/gnat/gnat_objectives.mli @@ -1,65 +1,62 @@ -(* This module is the Database for objectives and goals. It also deals with the +(* This module is the Database for checks and goals. It also deals with the better part of scheduling of VCs. - An objective is something to be proved in Ada, say, a range check. An - objective is defined by an explanation (check kind + Ada location). + A check is something to be proved in Ada, say, a range check. A + check is defined by an explanation (check kind + Ada location). This is the + Gnat_expl.check type. A goal is a VC that will be sent to Alt-Ergo. In general, there will be many - goals for each objective. Each goal has a trace (list of locations). + goals for each check. Each goal has a trace (list of locations). This module has the following functionality: - - It answers queries to get the goals of an objective and the - objective of a goal. + - It answers queries to get the goals of a check and the + check of a goal. - It supports scheduling by providing a "next" function that will by - little chunks return all goals associated to an objective. + little chunks return all goals associated to a check. - It allows registering prover results and keeps track of the status of - an objective. + a check. - It defines the scheduler and initializes it, and all the goals, correctly. *) open Why3 -type objective = Gnat_expl.check -(* an objective is identified by its check, which contains the check id and the - kind of the check *) - type status = | Proved | Not_Proved | Work_Left | Counter_Example -(* These are the possible statuses of an objective. - [Proved] means that all goals of that objectives are proved. - [Not_Proved] means that a proof attempt for a goal of the objective that +(* These are the possible statuses of a check. + [Proved] means that all goals of that check are proved. + [Not_Proved] means that a proof attempt for a goal of the check that cannot (or should not) be further simplified has failed. In both cases, there is no more work to do, and we can issue a message to the user. - [Work_Left] means that we don't know yet whether the objective is proved or + [Work_Left] means that we don't know yet whether the check is proved or not, this means that all subgoals were proved up to now or if unproved could be further simplified, but there is some work left. - [Counter_Example] means that the objective cannot be proved and the + [Counter_Example] means that the check cannot be proved and the counterexample should be generated. *) type subp -(* An object of type "subp" represents all objectives for a given Ada +(* An object of type "subp" represents all checks for a given Ada subprogram. *) -(* various possibilities to add objectives and goals to the database, and the +(* various possibilities to add checks and goals to the database, and the "interesting" bit *) type goal_id = Session_itp.proofNodeID (* This is the type of identifier of goal. They can be queried from the session through Session_itp functions *) -val add_to_objective : Gnat_expl.vc_info -> goal_id -> unit -(* register the goal with the given objective. If this is the - first time we register a goal for given objective, the objective is - registered as well. Only do the registering if the objective is to de +val add_to_check : Gnat_expl.vc_info -> goal_id -> unit +(* register the goal with the given check. If this is the + first time we register a goal for given check, the check is + registered as well. Only do the registering if the check is to be discharged (ie, if the --limit-subp / --limit-line directives apply). *) val set_not_interesting : goal_id -> unit @@ -71,22 +68,22 @@ val is_interesting : goal_id -> bool val add_trivial_proof : Session_itp.session -> goal_id -> unit -val get_objective : goal_id -> objective -(* get the objective associated with a goal_id *) +val get_check_of_goal : goal_id -> Gnat_expl.check +(* get the check associated with a goal_id *) val get_extra_info : goal_id -> Gnat_expl.extra_info (* Scheduling and proof *) -val next : objective -> goal_id list -(* For an objective, successive calls of [next] will return all goal_ids - associated to the objective, by chunks of size Gnat_config.parallel. [] is - returned if no goal_ids are left. One can add new goal_ids to an objective at any +val next : Gnat_expl.check -> goal_id list +(* For a check, successive calls of [next] will return all goal_ids + associated to the check, by chunks of size Gnat_config.parallel. [] is + returned if no goal_ids are left. One can add new goal_ids to a check at any time. *) (* Auxiliary functions *) -val iter : (objective -> unit) -> unit -(* iterate over all objectives *) +val iter : (Gnat_expl.check -> unit) -> unit +(* iterate over all registered checks *) val iter_leaf_goals : Session_itp.session -> subp -> @@ -98,10 +95,10 @@ val all_provers_tried : Session_itp.session -> goal_id -> bool (* check whether an existing valid proof attempt exists for the goal_id, for all requested provers *) -val objective_status : objective -> status -(* query the status of the objective *) +val check_status : Gnat_expl.check -> status +(* query the status of the check *) -val ce_goal : objective -> goal_id option +val ce_goal : Gnat_expl.check -> goal_id option val init_cont : unit -> Controller_itp.controller (* Makes a new controller with session *) @@ -127,9 +124,9 @@ end module Make (S: Controller_itp.Scheduler) : sig -val register_result : Controller_itp.controller -> goal_id -> bool -> objective * status +val register_result : Controller_itp.controller -> goal_id -> bool -> Gnat_expl.check * status (* Register the result of a prover for a given goal_id, and return the updated - * status of the objective, as well as the objective itself *) + * status of the check, as well as the check itself *) val schedule_goal : callback:(Session_itp.proofAttemptID -> Controller_itp.proof_attempt_status -> unit) -> @@ -162,14 +159,14 @@ module Save_VCs : sig (* Provide saving of VCs, traces *) val extract_stats : - Controller_itp.controller -> objective -> Gnat_report.stats * int + Controller_itp.controller -> Gnat_expl.check -> Gnat_report.stats * int (* The second field of the return tuple is the number of goal proved by a transformation that is not trivial_true (Checker prover). *) val vc_file : goal_id -> string (* get the file name for a given goal *) - val check_to_json : Session_itp.session -> objective -> Json_base.json + val check_to_json : Session_itp.session -> Gnat_expl.check -> Json_base.json end val all_split_leaf_goals : unit -> unit @@ -181,8 +178,8 @@ val goal_has_splits : Session_itp.session -> goal_id -> bool val is_ce_goal : Session_itp.session -> Session_itp.proofNodeID -> bool val is_valid_not_ce: Session_itp.session -> Session_itp.proofNodeID -> bool -val session_proved_status : Controller_itp.controller -> objective -> bool -(* check the proof status of an objective by looking at the verified/not +val session_proved_status : Controller_itp.controller -> Gnat_expl.check -> bool +(* check the proof status of an check by looking at the verified/not verified status of its VCs in the session *) val remove_all_valid_ce_attempt: Session_itp.session -> unit @@ -191,17 +188,17 @@ val remove_all_valid_ce_attempt: Session_itp.session -> unit or try greater timeout ? *) val session_find_unproved_pa : - Controller_itp.controller -> objective -> Session_itp.proofAttemptID option + Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofAttemptID option (* find the first unproved (not obsolete) proof attempt in a session which is - * in subforest of objective. *) + * in subforest of check. *) val session_find_ce_pa : - Controller_itp.controller -> objective -> Session_itp.proofAttemptID option + Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofAttemptID option (* Find the proof attempt related to the counter example, if any *) val session_find_unproved_goal : - Controller_itp.controller -> objective -> Session_itp.proofNodeID option -(* find the first unproved goal in a session (in subforest of objective) *) + Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofNodeID option +(* find the first unproved goal in a session (in subforest of check) *) val replay : Controller_itp.controller -> unit From 9e0bec8310a2a14539bf791160e58683abd33f75 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Mon, 2 Sep 2024 09:25:26 +0900 Subject: [PATCH 3/3] rename gnat_objectives to gnat_checks --- Makefile.in | 2 +- .../{gnat_objectives.ml => gnat_checks.ml} | 0 .../{gnat_objectives.mli => gnat_checks.mli} | 0 src/gnat/gnat_main.ml | 46 +++++++++---------- 4 files changed, 24 insertions(+), 24 deletions(-) rename src/gnat/{gnat_objectives.ml => gnat_checks.ml} (100%) rename src/gnat/{gnat_objectives.mli => gnat_checks.mli} (100%) diff --git a/Makefile.in b/Makefile.in index 6b5b7eb56..e1c2d0f7c 100644 --- a/Makefile.in +++ b/Makefile.in @@ -753,7 +753,7 @@ clean:: ############ GNATWHY3_FILES := gnat_util gnat_loc gnat_expl gnat_counterexamples gnat_config\ - gnat_scheduler gnat_manual gnat_report gnat_objectives gnat_main + gnat_scheduler gnat_manual gnat_report gnat_checks gnat_main GNATWHY3MODULES := $(addprefix src/gnat/, $(GNATWHY3_FILES)) GNATWHY3DEP = $(addsuffix .dep, $(GNATWHY3MODULES)) diff --git a/src/gnat/gnat_objectives.ml b/src/gnat/gnat_checks.ml similarity index 100% rename from src/gnat/gnat_objectives.ml rename to src/gnat/gnat_checks.ml diff --git a/src/gnat/gnat_objectives.mli b/src/gnat/gnat_checks.mli similarity index 100% rename from src/gnat/gnat_objectives.mli rename to src/gnat/gnat_checks.mli diff --git a/src/gnat/gnat_main.ml b/src/gnat/gnat_main.ml index 1867f3be6..e386fe604 100644 --- a/src/gnat/gnat_main.ml +++ b/src/gnat/gnat_main.ml @@ -22,7 +22,7 @@ open Why3 open Gnat_scheduler -module C = Gnat_objectives.Make (Gnat_scheduler) +module C = Gnat_checks.Make (Gnat_scheduler) let warn_gnat_rac_not_done = Loc.register_warning "gnat_rac_not_done" "Warn if RAC could not be completed" @@ -53,10 +53,10 @@ let register_goal cont goal_id = let task = Session_itp.get_task s goal_id in let fml = Task.task_goal_fmla task in let is_trivial = is_trivial fml in - if is_trivial then Gnat_objectives.add_trivial_proof s goal_id; + if is_trivial then Gnat_checks.add_trivial_proof s goal_id; match is_trivial, Gnat_expl.search_labels fml with | true, None -> - Gnat_objectives.set_not_interesting goal_id + Gnat_checks.set_not_interesting goal_id | false, None -> let base_msg = "Task has no tracability label" in let msg = @@ -67,9 +67,9 @@ let register_goal cont goal_id = | _, Some c -> begin if c.Gnat_expl.check.Gnat_expl.already_proved then - Gnat_objectives.set_not_interesting goal_id + Gnat_checks.set_not_interesting goal_id else - Gnat_objectives.add_to_check c goal_id + Gnat_checks.add_to_check c goal_id end let rec handle_vc_result c goal result = @@ -80,14 +80,14 @@ let rec handle_vc_result c goal result = *) let check, status = C.register_result c goal result in match status with - | Gnat_objectives.Proved -> () - | Gnat_objectives.Not_Proved -> () - | Gnat_objectives.Work_Left -> - List.iter (create_manual_or_schedule c check) (Gnat_objectives.next check) - | Gnat_objectives.Counter_Example -> + | Gnat_checks.Proved -> () + | Gnat_checks.Not_Proved -> () + | Gnat_checks.Work_Left -> + List.iter (create_manual_or_schedule c check) (Gnat_checks.next check) + | Gnat_checks.Counter_Example -> (* In this case, counterexample prover and VC will be never None *) let prover_ce = (Option.get Gnat_config.prover_ce) in - match Gnat_objectives.ce_goal check with + match Gnat_checks.ce_goal check with | None -> assert false | Some g -> C.schedule_goal_with_prover c ~callback:(interpret_result c) g prover_ce @@ -138,7 +138,7 @@ and schedule_goal (c: Controller_itp.controller) (g : Session_itp.proofNodeID) = if Session_itp.pn_proved c.Controller_itp.controller_session g then begin handle_vc_result c g true (* Maybe there was a previous proof attempt with identical parameters *) - end else if Gnat_objectives.all_provers_tried c.Controller_itp.controller_session g then begin + end else if Gnat_checks.all_provers_tried c.Controller_itp.controller_session g then begin (* the proof attempt was necessarily false *) handle_vc_result c g false end else begin @@ -150,8 +150,8 @@ and actually_schedule_goal c g = C.schedule_goal ~callback:(interpret_result c) c g let handle_obj c check = - if Gnat_objectives.check_status check <> Gnat_objectives.Proved then begin - match Gnat_objectives.next check with + if Gnat_checks.check_status check <> Gnat_checks.Proved then begin + match Gnat_checks.next check with | [] -> () | l -> List.iter (create_manual_or_schedule c check) l @@ -160,9 +160,9 @@ let handle_obj c check = let all_split_subp c subp = let s = c.Controller_itp.controller_session in C.init_subp_vcs c subp; - Gnat_objectives.iter_leaf_goals s subp (register_goal c); + Gnat_checks.iter_leaf_goals s subp (register_goal c); C.all_split_leaf_goals (); - Gnat_objectives.clear () + Gnat_checks.clear () let maybe_giant_step_rac ctr parent models = if not Gnat_config.giant_step_rac then @@ -235,13 +235,13 @@ let report_messages c check = properly registered. In that case, we attempt to find a parent goal that is registered. *) try - Gnat_objectives.get_extra_info g + Gnat_checks.get_extra_info g with Not_found -> if C.is_ce_goal s g then match Session_itp.get_proof_parent s g with | Session_itp.Theory _ -> default | Session_itp.Trans t -> - try Gnat_objectives.get_extra_info (Session_itp.get_trans_parent s t) + try Gnat_checks.get_extra_info (Session_itp.get_trans_parent s t) with Not_found -> default else { Gnat_expl.pretty_node = None; inlined = None } in @@ -258,7 +258,7 @@ let ending c () = Debug.Stats.record_timing "gnatwhy3.run_vcs" (fun () -> C.remove_all_valid_ce_attempt c.Controller_itp.controller_session); Debug.Stats.record_timing "gnatwhy3.save_session" (fun () -> C.save_session c); - Gnat_objectives.iter (report_messages c); + Gnat_checks.iter (report_messages c); let s = Buffer.contents escape_buffer in if s <> "" then Gnat_report.add_warning s; @@ -278,7 +278,7 @@ let ending c () = let normal_handle_one_subp c subp = C.init_subp_vcs c subp; let s = c.Controller_itp.controller_session in - Gnat_objectives.iter_leaf_goals s subp (register_goal c) + Gnat_checks.iter_leaf_goals s subp (register_goal c) (* save session on interrupt initiated by the user *) let save_session_and_exit c signum = @@ -315,7 +315,7 @@ let _ = Loc.set_warning_hook (fun ?loc:_ line -> Format.fprintf fmt "%s@." line) with Not_found -> () ); try - let c = Debug.Stats.record_timing "gnatwhy3.init" Gnat_objectives.init_cont in + let c = Debug.Stats.record_timing "gnatwhy3.init" Gnat_checks.init_cont in (* This has to be done after initialization of controller. Otherwise we don't have session. *) Sys.set_signal Sys.sigint (Sys.Signal_handle (save_session_and_exit c)); @@ -327,10 +327,10 @@ let _ = (fun () -> C.iter_subps c (normal_handle_one_subp c)); if Gnat_config.replay then begin C.replay c (*; - Gnat_objectives.do_scheduled_jobs (fun _ _ -> ());*) + Gnat_checks.do_scheduled_jobs (fun _ _ -> ());*) end else begin Debug.Stats.record_timing "gnatwhy3.schedule_vcs" - (fun () -> Gnat_objectives.iter (handle_obj c)); + (fun () -> Gnat_checks.iter (handle_obj c)); end; | Gnat_config.All_Split -> C.iter_subps c (all_split_subp c)