MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

call_provers.ml 15.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Format
13
open Model_parser
14

15
16
17
18
let debug = Debug.register_info_flag "call_prover"
  ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
         and@ keep@ temporary@ files."

19
20
let keep_vcs = Debug.register_info_flag "keep_vcs" ~desc:"Keep@ intermediate@ prover@ files."

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
type reason_unknown =
  | Resourceout
  | Other

type prover_answer =
  | Valid
  | Invalid
  | Timeout
  | OutOfMemory
  | StepLimitExceeded
  | Unknown of (string * reason_unknown option)
  | Failure of string
  | HighFailure

type prover_result = {
  pr_answer : prover_answer;
  pr_status : Unix.process_status;
  pr_output : string;
  pr_time   : float;
  pr_steps  : int;		(* -1 if unknown *)
  pr_model  : model;
}

44
45
46
47
48
type resource_limit = {
  limit_time  : int;
  limit_mem   : int;
  limit_steps : int;
}
49

50
let empty_limit = { limit_time = 0 ; limit_mem = 0; limit_steps = 0 }
51

52
53
54
55
56
57
let limit_max =
  let single_limit_max a b = if a = 0 || b = 0 then 0 else max a b in
  fun a b ->
    { limit_time = single_limit_max a.limit_time b.limit_time;
      limit_steps = single_limit_max a.limit_steps b.limit_steps;
      limit_mem = single_limit_max a.limit_mem b.limit_mem; }
58

59
60
61
62
63
64
type timeunit =
  | Hour
  | Min
  | Sec
  | Msec

65
66
67
type timeregexp = {
  re    : Str.regexp;
  group : timeunit array; (* i-th corresponds to the group i+1 *)
68
69
}

70
type stepregexp = {
71
  steps_re        : Str.regexp;
72
73
  steps_group_num : int;
  (* the number of matched group which corresponds to the number of steps *)
74
75
}

76
let timeregexp s =
77
78
79
80
81
82
83
84
85
86
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let nb = ref 0 in
  let l = ref [] in
  let add_unit x = l := (!nb,x) :: !l; incr nb; "\\([0-9]+.?[0-9]*\\)" in
  let replace s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "h" -> add_unit Hour
    | "m" -> add_unit Min
    | "s" -> add_unit Sec
    | "i" -> add_unit Msec
87
88
    | x -> failwith ("unknown time format specifier: %%" ^
            x ^ " (should be either %%h, %%m, %%s or %%i")
89
90
91
92
  in
  let s = Str.global_substitute cmd_regexp replace s in
  let group = Array.make !nb Hour in
  List.iter (fun (i,u) -> group.(i) <- u) !l;
93
  { re = Str.regexp s; group = group }
94
95
96
97

let rec grep_time out = function
  | [] -> None
  | re :: l ->
98
99
100
101
102
103
104
105
106
107
108
109
      begin try
        ignore (Str.search_forward re.re out 0);
        let t = ref 0. in
        Array.iteri (fun i u ->
          let v = Str.matched_group (succ i) out in
          match u with
          | Hour -> t := !t +. float_of_string v *. 3600.
          | Min  -> t := !t +. float_of_string v *. 60.
          | Sec  -> t := !t +. float_of_string v
          | Msec -> t := !t +. float_of_string v /. 1000.) re.group;
        Some !t
      with _ -> grep_time out l end
110

111
let stepregexp s_re s_group_num =
112
113
114
115
116
  {steps_re = (Str.regexp s_re); steps_group_num = s_group_num}

let rec grep_steps out = function
  | [] -> None
  | re :: l ->
117
118
119
120
121
      begin try
        ignore (Str.search_forward re.steps_re out 0);
        let v = Str.matched_group (re.steps_group_num) out in
        Some(int_of_string v)
      with _ -> grep_steps out l end
122

123
124
let grep_reason_unknown out =
  try
125
    (* TODO: this is SMTLIB specific, should be done in drivers instead *)
126
127
    let re = Str.regexp "^(:reason-unknown \\([^)]*\\)" in
    ignore (Str.search_forward re out 0);
128
    match (Str.matched_group 1 out) with
129
130
131
132
    | "resourceout" -> Resourceout
    | _ -> Other
  with Not_found ->
    Other
133

134
135
136
type prover_result_parser = {
  prp_regexps     : (Str.regexp * prover_answer) list;
  prp_timeregexps : timeregexp list;
137
  prp_stepregexps : stepregexp list;
138
  prp_exitcodes   : (int * prover_answer) list;
139
  prp_model_parser : Model_parser.model_parser;
140
141
}

142
let print_unknown_reason fmt = function
143
144
145
  | Some Resourceout -> fprintf fmt "resource limit reached"
  | Some Other -> fprintf fmt "other"
  | None -> fprintf fmt "none"
146

147
148
149
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
150
  | Timeout -> fprintf fmt "Timeout"
151
  | OutOfMemory -> fprintf fmt "Ouf Of Memory"
152
  | StepLimitExceeded -> fprintf fmt "Step limit exceeded"
153
  | Unknown ("", r) -> fprintf fmt "Unknown (%a)" print_unknown_reason r
154
  | Failure "" -> fprintf fmt "Failure"
155
  | Unknown (s, r) -> fprintf fmt "Unknown %a(%s)" print_unknown_reason r s
156
  | Failure s -> fprintf fmt "Failure (%s)" s
157
158
  | HighFailure -> fprintf fmt "HighFailure"

159
160
161
162
163
let print_prover_status fmt = function
  | Unix.WSTOPPED n -> fprintf fmt "stopped by signal %d" n
  | Unix.WSIGNALED n -> fprintf fmt "killed by signal %d" n
  | Unix.WEXITED n -> fprintf fmt "exited with status %d" n

164
let print_steps fmt s =
165
  if s >= 0 then fprintf fmt ", %d steps" s
166

167
168
169
let print_prover_result fmt {pr_answer = ans; pr_status = status;
                             pr_output = out; pr_time   = t;
                             pr_steps  = s;   pr_model  = m} =
170
  fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
171
  if not (Model_parser.is_model_empty m) then begin
172
    fprintf fmt "\nCounter-example model:";
173
    Model_parser.print_model fmt m
174
  end;
175
176
177
  if ans == HighFailure then
    fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
      print_prover_status status out
178

179
let rec grep out l = match l with
180
  | [] ->
181
182
      HighFailure
  | (re,pa) :: l ->
183
184
185
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
186
        | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
187
        | Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
188
189
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
190
      with Not_found -> grep out l end
191

192
let backup_file f = f ^ ".save"
193

194
let debug_print_model model =
195
196
197
  let model_str = Model_parser.model_to_string model in
  Debug.dprintf debug "Call_provers: %s@." model_str

198
199
200
201
202
203
204
205
206
207
let parse_prover_run res_parser time out exitcode limit ~printer_mapping =
  Debug.dprintf debug "Call_provers: exited with status %Ld@." exitcode;
  (* the following conversion is incorrect (but does not fail) on 32bit, but if
     the incoming exitcode was really outside the bounds of [int], its exact
     value is meaningless for Why3 anyway (e.g. some windows status codes). If
     it becomes meaningful, we might want to change the conversion here *)
  let int_exitcode = Int64.to_int exitcode in
  let ans =
    try List.assoc int_exitcode res_parser.prp_exitcodes
    with Not_found -> grep out res_parser.prp_regexps in
208
  Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
209
  let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
210
  let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
211
  (* add info for unknown if possible. FIXME: this is too SMTLIB specific *)
212
  let ans = match ans with
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
    | Unknown (s, _) ->
       let reason_unknown = grep_reason_unknown out in
       Unknown (s, Some reason_unknown)
    | _ -> ans
  in
  (* Highfailures close to time limit are assumed to be timeouts *)
  let tlimit = float limit.limit_time in
  let ans, time =
    match ans with
    | HighFailure when tlimit > 0.0 && time >= 0.9 *. tlimit ->
       Debug.dprintf
	 debug
	 "[Call_provers.parse_prover_run] highfailure after %f >= 0.9 timelimit -> set to Timeout@." time;
       Timeout, tlimit
    | _ -> ans,time
  in
  (* attempt to fix early timeouts / resp. unknown answers after timelimit *)
  (* does not work well. Let's give the answer and time without change instead, and let
     Session_scheduler.fuzzy_proof_time do the job instead
  Debug.dprintf
    debug
    "[Call_provers.parse_prover_run] fixing timeout versus unknown answers (time=%f, tlimit=%f)@."
    time tlimit;
  let ans,time =
    match ans with
    | Unknown _ when tlimit > 0.0 && time >= 0.99 *. tlimit ->
       Debug.dprintf
	 debug
	 "[Call_provers.parse_prover_run] unknown answer after %f >= 0.99 timelimit -> set to Timeout@." time;
       Timeout, tlimit
    | Timeout when time < tlimit ->
       Debug.dprintf
	 debug
	 "[Call_provers.parse_prover_run] timeout answer after %f <= timelimit -> set to Unknown@." time;
       Unknown("early timeout",Some Resourceout), time
    | _ -> ans, time
  in
   ***)
  (* get counterexample if any *)
252
  let model = res_parser.prp_model_parser out printer_mapping in
253
  Debug.dprintf debug "Call_provers: model:@.";
254
  debug_print_model model;
255
  { pr_answer = ans;
256
    pr_status = Unix.WEXITED int_exitcode;
257
    pr_output = out;
258
259
    pr_time   = time;
    pr_steps  = steps;
260
    pr_model  = model;
261
  }
262

263
let actualcommand command limit file =
264
265
  let stime = string_of_int limit.limit_time in
  let smem = string_of_int limit.limit_mem in
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  let arglist = Cmdline.cmdline_split command in
267
  let use_stdin = ref true in
268
  let on_timelimit = ref false in
269
  let cmd_regexp = Str.regexp "%\\(.\\)" in
270
  let replace s = match Str.matched_group 1 s with
271
    | "%" -> "%"
272
    | "f" -> use_stdin := false; file
273
    | "t" -> on_timelimit := true; stime
274
    | "m" -> smem
275
276
277
    (* FIXME: libdir and datadir can be changed in the configuration file
       Should we pass them as additional arguments? Or would it be better
       to prepare the command line in a separate function? *)
278
    | "l" -> Config.libdir
279
    | "d" -> Config.datadir
280
    | "S" -> string_of_int limit.limit_steps
281
    | _ -> failwith "unknown specifier, use %%, %f, %t, %m, %l, %d or %S"
282
  in
283
284
285
286
  let args =
    List.map (Str.global_substitute cmd_regexp replace) arglist
  in
  args, !use_stdin, !on_timelimit
Johannes Kanig's avatar
Johannes Kanig committed
287

288
let actualcommand ~cleanup ~inplace command limit file =
289
290
291
292
293
294
295
  try
    let (cmd, _,_) as x =
      actualcommand command limit file
    in
    Debug.dprintf debug "@[<hv 2>Call_provers: actual command is:@ @[%a@]@]@."
                  (Pp.print_list Pp.space pp_print_string) cmd;
    x
296
  with e ->
297
298
299
300
    Debug.dprintf
      debug
      "@[<hv 2>Call_provers: failed to build an actual corresponding to@ %s@]@."
      command;
301
302
303
304
305
    if cleanup then Sys.remove file;
    if inplace then Sys.rename (backup_file file) file;
    raise e

let adapt_limits limit on_timelimit =
306
307
308
309
310
311
  if limit.limit_time = empty_limit.limit_time then limit
  else
    { limit with limit_time =
      (* for steps limit use 2 * t + 1 time *)
      if limit.limit_steps <> empty_limit.limit_steps
      then (2 * limit.limit_time + 1)
312
313
      (* if prover implements time limit, use 16t + 1 *)
      else if on_timelimit then 16 * limit.limit_time + 1
314
315
      (* otherwise use t *)
      else limit.limit_time }
316

317
type server_id = int
318

319
320
321
322
323
324
let gen_id =
  let x = ref 0 in
  fun () ->
    incr x;
    !x

325
326
327
328
329
330
331
type save_data = {
  vc_file    : string;
  inplace    : bool;
  limit      : resource_limit;
  res_parser : prover_result_parser;
  printer_mapping : Printer.printer_mapping;
}
332

333
let saved_data : (int, save_data) Hashtbl.t = Hashtbl.create 17
334
335
336

let read_and_delete_file fn =
  let cin = open_in fn in
337
338
339
340
  let out = Sysutil.channel_contents cin in
  close_in cin;
  if Debug.test_noflag debug then Sys.remove fn;
  out
341
342

let handle_answer answer =
343
344
345
346
347
  match answer with
  | Prove_client.Finished answer ->
      let id = answer.Prove_client.id in
      let save = Hashtbl.find saved_data id in
      Hashtbl.remove saved_data id;
348
349
350
      if Debug.test_noflag debug && Debug.test_noflag keep_vcs then begin
        Sys.remove save.vc_file;
        if save.inplace then Sys.rename (backup_file save.vc_file) save.vc_file
351
352
      end;
      let out = read_and_delete_file answer.Prove_client.out_file in
353
      let ret = answer.Prove_client.exit_code in
354
355
      let printer_mapping = save.printer_mapping in
      let ans = parse_prover_run save.res_parser
356
          answer.Prove_client.time out ret save.limit ~printer_mapping in
357
358
359
      id, Some ans
  | Prove_client.Started id ->
      id, None
360

361
362
363
let wait_for_server_result ~blocking =
  List.map handle_answer (Prove_client.read_answers ~blocking)

364
365
type prover_call =
  | ServerCall of server_id
Andrei Paskevich's avatar
Andrei Paskevich committed
366
  | EditorCall of int
367
368

let call_on_file ~command ~limit ~res_parser ~printer_mapping
Andrei Paskevich's avatar
Andrei Paskevich committed
369
                 ?(inplace=false) fin =
370
  let id = gen_id () in
371
  let cmd, use_stdin, on_timelimit =
372
    actualcommand ~cleanup:true ~inplace command limit fin in
373
374
375
376
377
378
  let save = {
    vc_file    = fin;
    inplace    = inplace;
    limit      = limit;
    res_parser = res_parser;
    printer_mapping = printer_mapping } in
379
  Hashtbl.add saved_data id save;
380
  let limit = adapt_limits limit on_timelimit in
381
  let use_stdin = if use_stdin then Some fin else None in
382
383
384
385
386
  Debug.dprintf
    debug
    "Request sent to prove_client:@ timelimit=%d@ memlimit=%d@ cmd=@[[%a]@]@."
    limit.limit_time limit.limit_mem
    (Pp.print_list Pp.comma Pp.string) cmd;
387
388
389
390
  Prove_client.send_request ~use_stdin ~id
                            ~timelimit:limit.limit_time
                            ~memlimit:limit.limit_mem
                            ~cmd;
391
  ServerCall id
392

Andrei Paskevich's avatar
Andrei Paskevich committed
393
394
type prover_update =
  | NoUpdates
395
396
  | ProverInterrupted
  | InternalFailure of exn
Andrei Paskevich's avatar
Andrei Paskevich committed
397
398
399
400
401
  | ProverStarted
  | ProverFinished of prover_result

let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17

402
let fetch_new_results ~blocking = (* TODO: handle ProverStarted events *)
403
404
405
406
407
  List.iter (fun (id, r) ->
    let x = match r with
    | Some r -> ProverFinished r
    | None -> ProverStarted in
    Hashtbl.add result_buffer id x)
408
409
    (wait_for_server_result ~blocking)

410
411
let get_new_results ~blocking =
  fetch_new_results ~blocking;
412
  let q = ref [] in
413
414
415
416
  Hashtbl.iter (fun key element ->
    if element = ProverStarted && blocking then
      ()
    else
417
      q := (ServerCall key, element) :: !q) result_buffer;
418
  Hashtbl.clear result_buffer;
419
  !q
420

Andrei Paskevich's avatar
Andrei Paskevich committed
421
422
423
424
425
426
let query_result_buffer id =
  try let r = Hashtbl.find result_buffer id in
      Hashtbl.remove result_buffer id; r
  with Not_found -> NoUpdates

let editor_result ret = {
427
  pr_answer = Unknown ("", None);
Andrei Paskevich's avatar
Andrei Paskevich committed
428
429
430
431
432
433
434
  pr_status = ret;
  pr_output = "";
  pr_time   = 0.0;
  pr_steps  = 0;
  pr_model  = Model_parser.default_model;
}

435
436
let query_call = function
  | ServerCall id ->
437
      fetch_new_results ~blocking:false;
Andrei Paskevich's avatar
Andrei Paskevich committed
438
439
      query_result_buffer id
  | EditorCall pid ->
440
      let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
Andrei Paskevich's avatar
Andrei Paskevich committed
441
442
      if pid = 0 then NoUpdates else
      ProverFinished (editor_result ret)
443

444
445
let rec wait_on_call = function
  | ServerCall id as pc ->
Andrei Paskevich's avatar
Andrei Paskevich committed
446
447
      begin match query_result_buffer id with
        | ProverFinished r -> r
448
        | _ ->
449
            fetch_new_results ~blocking:true;
Andrei Paskevich's avatar
Andrei Paskevich committed
450
            wait_on_call pc
451
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
454
  | EditorCall pid ->
      let _, ret = Unix.waitpid [] pid in
      editor_result ret
455
456

let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
457
                   ~gen_new_file ?(inplace=false) buffer =
458
  let fin,cin =
459
460
461
462
463
464
465
466
467
468
    if gen_new_file then
      Filename.open_temp_file "why_" ("_" ^ filename)
    else
      begin
        let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
        if inplace then
          Sys.rename filename (backup_file filename);
        filename, open_out filename
      end
  in
469
  Buffer.output_buffer cin buffer; close_out cin;
470
471
472
473
474
475
476
  call_on_file ~command ~limit ~res_parser ~printer_mapping ~inplace fin

let call_editor ~command fin =
  let command, use_stdin, _ =
    actualcommand ~cleanup:false ~inplace:false command empty_limit fin in
  let exec = List.hd command in
  let argarray = Array.of_list command in
Andrei Paskevich's avatar
Andrei Paskevich committed
477
478
479
480
481
  let fd_in =
    if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
  let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
  if use_stdin then Unix.close fd_in;
  EditorCall pid