why3session_lib.ml 11 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12

open Why3
13

14
module S = Session_itp
15 16
module C = Whyconf

17 18 19
let verbose = Debug.register_info_flag "verbose"
    ~desc:"Increase verbosity."

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
type spec_list = (Arg.key * Arg.spec * Arg.doc) list

type cmd =
    {
      cmd_spec : spec_list;
      cmd_desc : string;
      cmd_name : string;
      cmd_run  : unit -> unit;
    }

let files = Queue.create ()
let iter_files f = Queue.iter f files
let anon_fun (f:string) = Queue.add f files

let read_simple_spec () =
35 36
  Debug.Args.set_flags_selected ();
  Debug.Args.option_list ()
37 38 39

let opt_config = ref None
let opt_loadpath = ref []
40
let opt_extra = ref []
41

42
let common_options = [
43
  "-C", Arg.String (fun s -> opt_config := Some s),
44
      "<file> read configuration from <file>";
45
  "--config", Arg.String (fun s -> opt_config := Some s),
MARCHE Claude's avatar
MARCHE Claude committed
46
      "<file> same as -C";
47
  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
48
      "<file> read additional configuration from <file>";
49
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
50
      "<dir> add <dir> to the library search path";
51
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
MARCHE Claude's avatar
MARCHE Claude committed
52
      "<dir> same as -L";
53
  Debug.Args.desc_shortcut "verbose" "--verbose" "increase verbosity";
54 55 56
  Debug.Args.desc_debug_list;
  Debug.Args.desc_debug_all;
  Debug.Args.desc_debug;
57 58
]

59
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
60
let env_spec = common_options
61
*)
62 63

let read_env_spec () =
64
  (* Configuration *)
65
  let config = Whyconf.read_config !opt_config in
66
  let config = List.fold_left Whyconf.merge_config config !opt_extra in
67 68 69
  let main = Whyconf.get_main config in
  Whyconf.load_plugins main;
  let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
MARCHE Claude's avatar
MARCHE Claude committed
70
    @ List.rev !opt_loadpath in
71 72 73
  let env = Env.create_env loadpath in
  env,config,read_simple_spec ()

74
let read_session fname =
75 76 77
  let q = Queue.create () in
  Queue.push fname q;
  let project_dir = Server_utils.get_session_dir ~allow_mkdir:false q in
78 79 80 81
  S.load_session project_dir

let read_update_session ~allow_obsolete env config fname =
  let session,use_shapes = read_session fname in
82
(*
83 84 85 86
  let ctxt = S.mk_update_context
    ~allow_obsolete_goals:allow_obsolete
    ~use_shapes_for_pairing_sub_goals:use_shapes
    (fun ?parent:_ () -> ())
87
  in
88
  S.update_session ~ctxt session env config
89
 *)
90
  let cont = Controller_itp.create_controller config env session in
91 92 93
  let found_obs, some_merge_miss =
    try
      Controller_itp.reload_files cont ~use_shapes;
94
      true, false (* TODO: take allow_obsolete, return values *)
95 96 97 98 99
    with
    | e ->
       Format.eprintf "%a@." Exn_printer.exn_printer e;
       exit 1
  in
100
  if (found_obs || some_merge_miss) && not allow_obsolete then raise Exit;
101
  cont, found_obs, some_merge_miss
102 103 104

(** filter *)
type filter_prover =
105 106
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
107 108 109 110

let filter_prover = Stack.create ()

let read_opt_prover s =
111
  try
112
    let l = Strings.rev_split ',' s in
113
    match l with
114
    (* A prover specified uniquely *)
115 116
    | [altern;version;name]
      when List.for_all (fun s -> s = "" || s.[0] <> '^') l ->
117 118 119 120 121 122 123 124
      Prover {Whyconf.prover_name = name;
              prover_version = version;
              prover_altern = altern}
    | _ -> FilterProver (Whyconf.parse_filter_prover s)
  with Whyconf.ParseFilterProver _ ->
    raise (Arg.Bad
             "--filter-prover name[,version[,alternative]|,,alternative] \
                regexp must start with ^")
125 126 127 128


let add_filter_prover s = Stack.push (read_opt_prover s) filter_prover

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
type filter_three = | FT_Yes | FT_No | FT_All

let opt_filter_archived = ref FT_No
let opt_filter_obsolete = ref FT_All
let opt_filter_verified_goal = ref FT_All
let opt_filter_verified = ref FT_All

let add_filter_three r = function
  | "no" -> r := FT_No
  | "yes" -> r := FT_Yes
  | "all" -> r := FT_All
  | _ -> assert false

let opt_three r = Arg.Symbol (["yes";"no";"all"], add_filter_three r)

144 145
let opt_status = ref []

146 147 148
let filter_spec =
  ["--filter-prover", Arg.String add_filter_prover,
   " [name,version[,alternative]|id] \
149
the proof containing this prover are selected";
François Bobot's avatar
François Bobot committed
150
   "--filter-obsolete", opt_three opt_filter_obsolete,
151 152 153 154 155 156 157
   " no: only non-obsolete, yes: only obsolete (default all)";
   "--filter-archived", opt_three opt_filter_archived,
   " no: only unarchived, yes: only archived (default no)";
   "--filter-verified-goal", opt_three opt_filter_verified_goal,
   " no: only parent goal not verified, yes: only verified (default all)";
   "--filter-verified", opt_three opt_filter_verified,
   " no: only not verified, yes: only verified (default all)";
158 159 160 161 162 163 164 165 166 167
   "--filter-highfailure",
   Arg.Unit (fun () -> opt_status := Call_provers.HighFailure::!opt_status),
   " filter the call that fail in an unexpeted way";
   "--filter-valid",
   Arg.Unit (fun () -> opt_status := Call_provers.Valid::!opt_status),
   " filter the valid goals (can be obsolete)";
   "--filter-invalid",
   Arg.Unit (fun () -> opt_status := Call_provers.Invalid::!opt_status),
   " filter the invalid goals";
   "--filter-unknown",
168
   Arg.String (fun s -> opt_status := Call_provers.Unknown (s, None)::!opt_status),
169 170 171 172
   " filter when the prover reports it can't determine if the task is valid";
   "--filter-failure",
   Arg.String (fun s -> opt_status := Call_provers.Failure s::!opt_status),
   " filter when the prover reports a failure";
173
]
174

175 176 177 178 179 180
type filters =
    { provers : C.Sprover.t; (* if empty : every provers *)
      obsolete : filter_three;
      archived : filter_three;
      verified : filter_three;
      verified_goal : filter_three;
181
      status : Call_provers.prover_answer list; (* if empty : any answer *)
182
    }
183

184 185 186 187 188
let provers_of_filter_prover whyconf = function
  | Prover p        -> C.Sprover.singleton p
  | FilterProver fp ->
    C.Mprover.map (Util.const ()) (C.filter_provers whyconf fp)

189
let prover_of_filter_prover whyconf = function
190 191 192 193
  | Prover p        -> p
  | FilterProver fp ->
    (C.filter_one_prover whyconf fp).C.prover

194 195 196 197 198 199

let read_filter_spec whyconf : filters * bool =
  let should_exit = ref false in
  let s = ref C.Sprover.empty in
  let iter p =
    try
200 201
      s := C.Sprover.union (provers_of_filter_prover whyconf p) !s
    with C.ProverNotFound (_,fp) ->
202
      Format.eprintf
203 204 205
        "The prover %a is not found in the configuration file %s@."
        Whyconf.print_filter_prover fp
        (Whyconf.get_conf_file whyconf);
206 207
      should_exit := true in
  Stack.iter iter filter_prover;
208 209 210 211 212
  {provers = !s;
   obsolete = !opt_filter_obsolete;
   archived = !opt_filter_archived;
   verified = !opt_filter_verified;
   verified_goal = !opt_filter_verified_goal;
213
   status = !opt_status;
214 215
  },!should_exit

216
let iter_proof_attempt_by_filter ses iter filters f =
217
  (* provers *)
218
  let iter_provers a =
219
    if C.Sprover.mem a.S.prover filters.provers then f a in
220
  let f = if C.Sprover.is_empty filters.provers then f else iter_provers in
221
  (* three value *)
222 223
  let three_value f v p =
    let iter_obsolete a =
224 225 226
      match v, p a with
        | FT_No, false -> f a
        | FT_Yes, true -> f a
227
        | _ -> () (* FT_All treated after *) in
228
    if v = FT_All then f else iter_obsolete in
229
  (* obsolete *)
230
  let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
231
  (* archived *)
232
(*
233
  let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
234
 *)
235
  (* verified_goal *)
236
  let f = three_value f filters.verified_goal
237
    (fun a -> S.pn_proved ses a.S.parent) in
238
  (* verified *)
239
  let f = three_value f filters.verified
Sylvain Dailler's avatar
Sylvain Dailler committed
240
    (fun p -> match p.S.proof_state with Some pr when pr.Call_provers.pr_answer = Call_provers.Valid ->
241
                                      true | _ -> false) in
242
  (* status *)
243 244
  let f = if filters.status = [] then f else
      (fun a -> match a.S.proof_state with
245
      | Some pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
246
      | _ -> ()) in
247
  iter f ses
248

249
let theory_iter_proof_attempt_by_filter s filters f th =
250
  iter_proof_attempt_by_filter
251
    s
252 253 254
    (fun f s -> S.theory_iter_proof_attempt s f)
    filters f th

255
let session_iter_proof_attempt_by_filter s filters f =
256
  iter_proof_attempt_by_filter
257
    s
258 259 260
    (fun f _s ->
     S.session_iter_proof_attempt (fun _ x -> f x))
    filters f s
261

262 263

let set_filter_verified_goal t = opt_filter_verified_goal := t
264 265 266 267 268 269

let opt_force_obsolete = ref false

let force_obsolete_spec =
  ["-F", Arg.Set opt_force_obsolete,
   " transform obsolete session"]
270 271 272 273 274 275 276 277 278 279 280



let rec ask_yn () =
  Format.printf "(y/n)@.";
  let answer = read_line () in
  match answer with
    | "y" -> true
    | "n" -> false
    | _ -> ask_yn ()

281
let ask_yn_nonblock ~callback =
282
  let b = Buffer.create 3 in
283
  let s = Strings.create 1 in
284 285 286 287 288 289
  Format.printf "(y/n)@.";
  fun () ->
    match Unix.select [Unix.stdin] [] [] 0. with
    | [],_,_ -> true
    | _ ->
      if Unix.read Unix.stdin s 1 0 = 0 then
290
        begin (* EndOfFile *) callback false; false end
291 292 293 294 295 296 297 298 299 300 301 302
      else begin
        if s.[0] <> '\n'
        then (Buffer.add_char b s.[0]; true)
        else
          match Buffer.contents b with
          | "y" -> callback true; false
          | "n" | "" -> callback false; false
          | _ ->
            Format.printf "(y/N)@.";
            Buffer.clear b;
            true
      end
303 304


MARCHE Claude's avatar
MARCHE Claude committed
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
let get_used_provers_goal session g =
  let sprover = ref Whyconf.Sprover.empty in
  Session_itp.goal_iter_proof_attempt session
    (fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
    g;
  !sprover

let get_used_provers_theory session th =
  let sprover = ref Whyconf.Sprover.empty in
  Session_itp.theory_iter_proof_attempt session
    (fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
    th;
  !sprover

let get_used_provers_file session f =
  let sprover = ref Whyconf.Sprover.empty in
  Session_itp.file_iter_proof_attempt session
    (fun pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
    f;
  !sprover

326 327 328 329 330 331
let get_used_provers session =
  let sprover = ref Whyconf.Sprover.empty in
  Session_itp.session_iter_proof_attempt
    (fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
     session;
  !sprover
MARCHE Claude's avatar
MARCHE Claude committed
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348


let rec transf_depth s tr =
  List.fold_left
    (fun depth g -> max depth (goal_depth s g)) 0 (Session_itp.get_sub_tasks s tr)
and goal_depth s g =
  List.fold_left
    (fun depth tr -> max depth (1 + transf_depth s tr))
    1 (Session_itp.get_transformations s g)

let theory_depth s t =
  List.fold_left
    (fun depth g -> max depth (goal_depth s g)) 0 (Session_itp.theory_goals t)

let file_depth s f =
  List.fold_left (fun depth t -> max depth (theory_depth s t)) 0
    (Session_itp.file_theories f)