why3session_lib.ml 9.81 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
74
  let env = Env.create_env loadpath in
  env,config,read_simple_spec ()

let read_update_session ~allow_obsolete env config 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
  let session,use_shapes = S.load_session project_dir in
(*
80
81
82
83
  let ctxt = S.mk_update_context
    ~allow_obsolete_goals:allow_obsolete
    ~use_shapes_for_pairing_sub_goals:use_shapes
    (fun ?parent:_ () -> ())
84
  in
85
  S.update_session ~ctxt session env config
86
 *)
87
  let cont = Controller_itp.create_controller config env session in
88
89
90
  let found_obs, some_merge_miss =
    try
      Controller_itp.reload_files cont ~use_shapes;
91
      true, false (* TODO: take allow_obsolete, return values *)
92
93
94
95
96
    with
    | e ->
       Format.eprintf "%a@." Exn_printer.exn_printer e;
       exit 1
  in
97
  cont, found_obs, some_merge_miss
98
99
100

(** filter *)
type filter_prover =
101
102
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
103
104
105
106

let filter_prover = Stack.create ()

let read_opt_prover s =
107
  try
108
    let l = Strings.rev_split ',' s in
109
    match l with
110
    (* A prover specified uniquely *)
111
112
    | [altern;version;name]
      when List.for_all (fun s -> s = "" || s.[0] <> '^') l ->
113
114
115
116
117
118
119
120
      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 ^")
121
122
123
124


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

125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
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)

140
141
let opt_status = ref []

142
143
144
let filter_spec =
  ["--filter-prover", Arg.String add_filter_prover,
   " [name,version[,alternative]|id] \
145
the proof containing this prover are selected";
François Bobot's avatar
François Bobot committed
146
   "--filter-obsolete", opt_three opt_filter_obsolete,
147
148
149
150
151
152
153
   " 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)";
154
155
156
157
158
159
160
161
162
163
   "--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",
164
   Arg.String (fun s -> opt_status := Call_provers.Unknown (s, None)::!opt_status),
165
166
167
168
   " 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";
169
]
170

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

180
181
182
183
184
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)

185
let prover_of_filter_prover whyconf = function
186
187
188
189
  | Prover p        -> p
  | FilterProver fp ->
    (C.filter_one_prover whyconf fp).C.prover

190
191
192
193
194
195

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

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

let theory_iter_proof_attempt_by_filter cont filters f th =
  iter_proof_attempt_by_filter
    cont
    (fun f s -> S.theory_iter_proof_attempt s f)
    filters f th

let session_iter_proof_attempt_by_filter cont filters f s =
  iter_proof_attempt_by_filter
    cont
    (fun f _s ->
     S.session_iter_proof_attempt (fun _ x -> f x))
    filters f s
257

258
259

let set_filter_verified_goal t = opt_filter_verified_goal := t
260
261
262
263
264
265

let opt_force_obsolete = ref false

let force_obsolete_spec =
  ["-F", Arg.Set opt_force_obsolete,
   " transform obsolete session"]
266
267
268
269
270
271
272
273
274
275
276



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

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


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