Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

session.ml 89.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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.                           *)
(*                                                                  *)
(********************************************************************)
François Bobot's avatar
François Bobot committed
11

12
open Stdlib
François Bobot's avatar
François Bobot committed
13 14 15 16 17 18
open Ty
open Ident
open Decl
open Term
open Theory
open Task
François Bobot's avatar
François Bobot committed
19

20 21 22 23
module Mprover = Whyconf.Mprover
module Sprover = Whyconf.Sprover
module PHprover = Whyconf.Hprover
module C = Whyconf
24
module Tc = Termcode
25

26
let debug = Debug.register_info_flag "session"
Andrei Paskevich's avatar
Andrei Paskevich committed
27 28
  ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
         creation,@ reading@ and@ writing."
François Bobot's avatar
François Bobot committed
29 30 31

(** {2 Type definitions} *)

32
module PHstr = Hstr
François Bobot's avatar
François Bobot committed
33

34 35 36 37
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
François Bobot's avatar
François Bobot committed
38 39 40 41 42 43
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

type task_option = Task.task option
44
type 'a hide = 'a option
François Bobot's avatar
François Bobot committed
45

46 47 48 49
type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
François Bobot's avatar
François Bobot committed
50 51
  }

52 53 54 55 56 57 58
let print_ident_path fmt ip =
  Format.fprintf fmt "%a.%s.%a"
    (Pp.print_list Pp.dot Pp.string) ip.ip_library
    ip.ip_theory
    (Pp.print_list Pp.dot Pp.string) ip.ip_qualid

let compare_ident_path x y =
59
  let c = Lists.compare String.compare x.ip_library y.ip_library in
François Bobot's avatar
François Bobot committed
60
  if c <> 0 then -c else (* in order to be bottom up *)
61
  let c = String.compare x.ip_theory y.ip_theory in
François Bobot's avatar
François Bobot committed
62
  if c <> 0 then c else
63
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
64
  c
François Bobot's avatar
François Bobot committed
65 66

module Pos = struct
67 68
  type t = ident_path
  let compare = compare_ident_path
François Bobot's avatar
François Bobot committed
69 70 71 72
  let equal x y = (x : t) = y
  let hash x = Hashtbl.hash (x : t)
end

73 74 75
module Mpos = Extmap.Make(Pos)
module Spos = Extset.MakeOfMap(Mpos)
module Hpos = Exthtbl.Make(Pos)
François Bobot's avatar
François Bobot committed
76 77 78

type meta_args = meta_arg list

79
module Mmeta_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
80 81 82 83 84 85 86 87 88 89 90 91
  type t = meta_args

  let meta_arg_id = function
    | MAty _  -> 0
    | MAts _  -> 1
    | MAls _  -> 2
    | MApr _  -> 3
    | MAstr _ -> 4
    | MAint _ -> 5

  let compare_meta_arg x y =
    match x,y with
92
    (* These hash are in fact tag *)
François Bobot's avatar
François Bobot committed
93 94 95 96 97 98 99 100
    | MAty  x, MAty  y -> compare (ty_hash x) (ty_hash y)
    | MAts  x, MAts  y -> compare (ts_hash x) (ts_hash y)
    | MAls  x, MAls  y -> compare (ls_hash x) (ls_hash y)
    | MApr  x, MApr  y -> compare (pr_hash x) (pr_hash y)
    | MAstr x, MAstr y -> String.compare x y
    | MAint x, MAint y -> compare x y
    | _ -> compare (meta_arg_id x) (meta_arg_id y)

101
  let compare = Lists.compare compare_meta_arg
François Bobot's avatar
François Bobot committed
102
end)
103 104

module Smeta_args = Extset.MakeOfMap(Mmeta_args)
François Bobot's avatar
François Bobot committed
105

Andrei Paskevich's avatar
Andrei Paskevich committed
106 107
type metas_args = Smeta_args.t Mstr.t

108
module Mmetas_args = Extmap.Make(struct
François Bobot's avatar
François Bobot committed
109 110 111 112 113
  type t = metas_args
  let compare = Mstr.compare Smeta_args.compare
end)

type idpos = {
114 115 116
  idpos_ts : ident_path Mts.t;
  idpos_ls : ident_path Mls.t;
  idpos_pr : ident_path Mpr.t;
François Bobot's avatar
François Bobot committed
117 118 119 120 121 122 123 124 125
}

let empty_idpos =
  {
    idpos_ts = Mts.empty;
    idpos_ls = Mls.empty;
    idpos_pr = Mpr.empty;
  }

126
(* dead code
François Bobot's avatar
François Bobot committed
127 128 129 130 131 132 133 134 135
let posid_of_idpos idpos =
  let posid = Mpos.empty in
  let posid = Mts.fold (fun ts pos ->
    Mpos.add pos (MAts ts)) idpos.idpos_ts posid  in
  let posid = Mls.fold (fun ls pos ->
    Mpos.add pos (MAls ls)) idpos.idpos_ls posid  in
  let posid = Mpr.fold (fun pr pos ->
    Mpos.add pos (MApr pr)) idpos.idpos_pr posid  in
  posid
136
*)
François Bobot's avatar
François Bobot committed
137

MARCHE Claude's avatar
MARCHE Claude committed
138 139
type expl = string option

François Bobot's avatar
François Bobot committed
140
type 'a goal =
141 142
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
MARCHE Claude's avatar
MARCHE Claude committed
143
    goal_expl : expl;
144
    goal_parent : 'a goal_parent;
145
    mutable goal_checksum : Tc.checksum option;
146
    mutable goal_shape : Tc.shape;
147
    mutable goal_verified : float option;
148
    mutable goal_task: task_option;
149 150 151
    mutable goal_expanded : bool;
    goal_external_proofs : 'a proof_attempt PHprover.t;
    goal_transformations : 'a transf PHstr.t;
François Bobot's avatar
François Bobot committed
152
    mutable goal_metas : 'a metas Mmetas_args.t;
153
  }
François Bobot's avatar
François Bobot committed
154 155

and 'a proof_attempt =
156 157 158 159
  { proof_key : 'a;
    mutable proof_prover : Whyconf.prover;
    proof_parent : 'a goal;
    mutable proof_state : proof_attempt_status;
160
    mutable proof_limit : Call_provers.resource_limit;
161 162 163 164
    mutable proof_obsolete : bool;
    mutable proof_archived : bool;
    mutable proof_edited_as : string option;
  }
François Bobot's avatar
François Bobot committed
165 166 167 168

and 'a goal_parent =
  | Parent_theory of 'a theory
  | Parent_transf of 'a transf
François Bobot's avatar
François Bobot committed
169 170 171 172 173 174 175
  | Parent_metas  of 'a metas

and 'a metas =
  { mutable metas_key : 'a;
    metas_added : metas_args;
    metas_idpos : idpos;
    metas_parent : 'a goal;
176
    mutable metas_verified : float option;
François Bobot's avatar
François Bobot committed
177 178 179 180
    mutable metas_goal : 'a goal;
    (** Not mutated after the creation *)
    mutable metas_expanded : bool;
  }
François Bobot's avatar
François Bobot committed
181 182 183 184 185 186

and 'a transf =
    { mutable transf_key : 'a;
      transf_name : string;
      (** Why3 tranformation name *)
      transf_parent : 'a goal;
187
      mutable transf_verified : float option;
François Bobot's avatar
François Bobot committed
188 189 190
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation of the session *)
      mutable transf_expanded : bool;
191
      mutable transf_detached : 'a detached option;
François Bobot's avatar
François Bobot committed
192 193
    }

194 195 196
and 'a detached =
    { detached_goals: 'a goal list; }

François Bobot's avatar
François Bobot committed
197 198 199 200
and 'a theory =
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
201
      mutable theory_checksum : Termcode.checksum option;
François Bobot's avatar
François Bobot committed
202
      mutable theory_goals : 'a goal list;
203
      mutable theory_verified : float option;
François Bobot's avatar
François Bobot committed
204
      mutable theory_expanded : bool;
205
      mutable theory_task : Theory.theory hide;
206
      mutable theory_detached : 'a detached option;
François Bobot's avatar
François Bobot committed
207 208 209 210 211
    }

and 'a file =
    { mutable file_key : 'a;
      file_name : string;
212
      file_format : string option;
François Bobot's avatar
François Bobot committed
213 214 215
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
216
      mutable file_verified : float option;
François Bobot's avatar
François Bobot committed
217
      mutable file_expanded : bool;
218
      mutable file_for_recovery : Theory.theory Mstr.t hide;
François Bobot's avatar
François Bobot committed
219 220 221 222
    }

and 'a session =
    { session_files : 'a file PHstr.t;
MARCHE Claude's avatar
MARCHE Claude committed
223
      mutable session_shape_version : int;
224
      session_prover_ids : int PHprover.t;
François Bobot's avatar
François Bobot committed
225 226 227 228 229 230 231
      session_dir   : string; (** Absolute path *)
    }

type loaded_prover =
    { prover_config : Whyconf.config_prover;
      prover_driver : Driver.driver}

232
type loaded_provers = loaded_prover option PHprover.t
François Bobot's avatar
François Bobot committed
233 234 235

type 'a env_session =
    { env : Env.env;
236
      mutable whyconf : Whyconf.config;
François Bobot's avatar
François Bobot committed
237
      loaded_provers : loaded_provers;
238
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
François Bobot's avatar
François Bobot committed
239 240
      session : 'a session}

241
let update_env_session_config e c = e.whyconf <- c
François Bobot's avatar
François Bobot committed
242 243 244 245 246 247 248 249 250 251

(*************************)
(**       Iterators      *)
(*************************)
type 'a any =
  | File of 'a file
  | Theory of 'a theory
  | Goal of 'a goal
  | Proof_attempt of 'a proof_attempt
  | Transf of 'a transf
François Bobot's avatar
François Bobot committed
252
  | Metas of 'a metas
François Bobot's avatar
François Bobot committed
253 254 255

let rec goal_iter_proof_attempt f g =
  PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
256 257
  PHstr.iter (fun _ t -> transf_iter_proof_attempt f t) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> metas_iter_proof_attempt f t) g.goal_metas;
François Bobot's avatar
François Bobot committed
258 259 260 261

and transf_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.transf_goals

François Bobot's avatar
François Bobot committed
262 263 264
and metas_iter_proof_attempt f t =
  goal_iter_proof_attempt f t.metas_goal

François Bobot's avatar
François Bobot committed
265 266 267
let theory_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.theory_goals

François Bobot's avatar
François Bobot committed
268 269 270
let metas_iter_proof_attempt f m =
  goal_iter_proof_attempt f m.metas_goal

François Bobot's avatar
François Bobot committed
271 272 273 274 275 276
let file_iter_proof_attempt f t =
  List.iter (theory_iter_proof_attempt f) t.file_theories

let session_iter_proof_attempt f s =
  PHstr.iter (fun _ file -> file_iter_proof_attempt f file) s.session_files

277
let iter_proof_attempt f = function
François Bobot's avatar
François Bobot committed
278 279 280 281 282
    | Goal g -> goal_iter_proof_attempt f g
    | Theory th -> theory_iter_proof_attempt f th
    | File file -> file_iter_proof_attempt f file
    | Proof_attempt a -> f a
    | Transf tr -> transf_iter_proof_attempt f tr
François Bobot's avatar
François Bobot committed
283
    | Metas m -> metas_iter_proof_attempt f m
François Bobot's avatar
François Bobot committed
284 285

let rec goal_iter_leaf_goal ~unproved_only f g =
286
  if not (Opt.inhabited g.goal_verified && unproved_only) then
François Bobot's avatar
François Bobot committed
287 288 289 290 291 292 293
    let r = ref true in
    PHstr.iter
      (fun _ t -> r := false;
        List.iter (goal_iter_leaf_goal ~unproved_only f) t.transf_goals)
      g.goal_transformations;
    if !r then f g

294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
let rec fold_all_sub_goals_of_goal f acc g =
  let acc =
    PHstr.fold
      (fun _ tr acc ->
       List.fold_left (fold_all_sub_goals_of_goal f) acc tr.transf_goals)
      g.goal_transformations acc
  in
  let acc =
    Mmetas_args.fold
      (fun _ m acc ->
       fold_all_sub_goals_of_goal f acc m.metas_goal)
      g.goal_metas acc
  in
  f acc g

let fold_all_sub_goals_of_theory f acc th =
  List.fold_left (fold_all_sub_goals_of_goal f) acc th.theory_goals


François Bobot's avatar
François Bobot committed
313
(** iterators not reccursive *)
François Bobot's avatar
François Bobot committed
314
let iter_goal fp ft fm g =
François Bobot's avatar
François Bobot committed
315
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
316 317
  PHstr.iter (fun _ t -> ft t) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> fm t) g.goal_metas
François Bobot's avatar
François Bobot committed
318 319 320 321

let iter_transf f t =
  List.iter (fun g -> f g) t.transf_goals

François Bobot's avatar
François Bobot committed
322 323
let iter_metas f t = f t.metas_goal

324 325 326
let iter_theory f t =
  List.iter f t.theory_goals

327 328 329 330
let iter_file f fi = List.iter f fi.file_theories

let iter_session f s = PHstr.iter (fun _ th -> f th) s.session_files

François Bobot's avatar
François Bobot committed
331
let goal_iter f g =
332 333
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
François Bobot's avatar
François Bobot committed
334 335 336
  PHstr.iter (fun _ t -> f (Transf t)) g.goal_transformations;
  Mmetas_args.iter (fun _ t -> f (Metas t)) g.goal_metas

François Bobot's avatar
François Bobot committed
337 338 339 340

let transf_iter f t =
  List.iter (fun g -> f (Goal g)) t.transf_goals

François Bobot's avatar
François Bobot committed
341 342 343
let metas_iter f t =
  f (Goal t.metas_goal)

François Bobot's avatar
François Bobot committed
344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
let theory_iter f t =
  List.iter (fun g -> f (Goal g)) t.theory_goals

let file_iter f t =
  List.iter (fun th -> f (Theory th)) t.file_theories

let session_iter f s =
  PHstr.iter (fun _ file -> f (File file)) s.session_files

let iter f = function
    | Goal g -> goal_iter f g
    | Theory th -> theory_iter f th
    | File file -> file_iter f file
    | Proof_attempt _ -> ()
    | Transf tr -> transf_iter f tr
François Bobot's avatar
François Bobot committed
359
    | Metas m -> metas_iter f m
François Bobot's avatar
François Bobot committed
360 361 362 363 364 365 366 367 368

(** Print session *)


module PTreeT = struct
  type 'a t = | Any of 'a any | Session of 'a session
  let decomp = function
    | Any t ->
      let s = match t with
369
        | File f ->
370
          if Opt.inhabited f.file_verified
371 372 373
          then f.file_name
          else f.file_name^"?"
        | Theory th ->
374
          if Opt.inhabited th.theory_verified
375 376
          then th.theory_name.Ident.id_string
          else th.theory_name.Ident.id_string^"?"
François Bobot's avatar
François Bobot committed
377
        | Goal g ->
378
          if Opt.inhabited g.goal_verified
379 380
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
381
        | Proof_attempt pr ->
382
          Pp.sprintf_wnl "%a%s%s%s%s"
383
            Whyconf.print_prover pr.proof_prover
384 385 386 387
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
388 389 390
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
391
        | Transf tr ->
392
          if Opt.inhabited tr.transf_verified
393
          then tr.transf_name
François Bobot's avatar
François Bobot committed
394 395
          else tr.transf_name^"?"
        | Metas metas ->
396
          if Opt.inhabited metas.metas_verified
François Bobot's avatar
François Bobot committed
397 398 399
          then "metas..."
          else "metas..."^"?"
      in
François Bobot's avatar
François Bobot committed
400 401 402 403 404 405
      let l = ref [] in
      iter (fun a -> l := (Any a)::!l) t;
      s,!l
    | Session s ->
      let l = ref [] in
      session_iter (fun a -> l := (Any a)::!l) s;
406 407 408
      (* Previously "" was `Filename.basename s.session_dir` but
         the tree depend on the filename given in input and not the content
         which is not easy for diffing
409 410
      *)
      "",!l
François Bobot's avatar
François Bobot committed
411 412 413 414 415 416 417 418 419 420 421

end

module PTree = Print_tree.PMake(PTreeT)

let print_any fmt any = PTree.print fmt (PTreeT.Any any)

let print_session fmt s = PTree.print fmt (PTreeT.Session s)

(** 2 Create a session *)

MARCHE Claude's avatar
MARCHE Claude committed
422 423 424 425 426 427 428
let empty_session ?shape_version dir =
  let shape_version = match shape_version with
    | Some v -> v
    | None -> Termcode.current_shape_version
  in
  { session_files = PHstr.create 3;
    session_shape_version = shape_version;
429
    session_prover_ids = PHprover.create 7;
MARCHE Claude's avatar
MARCHE Claude committed
430 431 432 433
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
François Bobot's avatar
François Bobot committed
434 435
  if not (Sys.file_exists project_dir) then
    begin
436
      Debug.dprintf debug
François Bobot's avatar
François Bobot committed
437 438 439 440
        "[Info] '%s' does not exists. Creating directory of that name \
 for the project@." project_dir;
      Unix.mkdir project_dir 0o777
    end;
MARCHE Claude's avatar
MARCHE Claude committed
441
  empty_session ?shape_version project_dir
François Bobot's avatar
François Bobot committed
442 443


444
(* dead code
François Bobot's avatar
François Bobot committed
445 446 447 448 449 450 451
let load_env_session ?(includes=[]) session conf_path_opt =
  let config = Whyconf.read_config conf_path_opt in
  let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) @ includes in
  let env = Env.create_env loadpath in
  { session = session;
    env = env;
    whyconf = config;
452
    loaded_provers = PHprover.create 5;
François Bobot's avatar
François Bobot committed
453
  }
454
*)
François Bobot's avatar
François Bobot committed
455 456 457 458 459

(************************)
(* session accessor     *)
(************************)

460
(* dead code
François Bobot's avatar
François Bobot committed
461 462 463 464 465 466 467 468
let get_session_file file = file.file_parent

let get_session_theory th = get_session_file th.theory_parent

let rec get_session_goal goal =
  match goal.goal_parent with
    | Parent_transf trans -> get_session_trans trans
    | Parent_theory th    -> get_session_theory th
François Bobot's avatar
François Bobot committed
469
    | Parent_metas  metas -> get_session_metas metas
François Bobot's avatar
François Bobot committed
470

471

François Bobot's avatar
François Bobot committed
472 473
and get_session_trans transf = get_session_goal transf.transf_parent

François Bobot's avatar
François Bobot committed
474 475
and get_session_metas metas = get_session_goal metas.metas_parent

François Bobot's avatar
François Bobot committed
476
let get_session_proof_attempt pa = get_session_goal pa.proof_parent
477
*)
François Bobot's avatar
François Bobot committed
478

479
let get_used_provers session =
François Bobot's avatar
François Bobot committed
480
  let sprover = ref Sprover.empty in
481
   session_iter_proof_attempt
François Bobot's avatar
François Bobot committed
482
    (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
483
     session;
François Bobot's avatar
François Bobot committed
484 485
  !sprover

486 487 488 489 490 491
let get_used_provers_with_stats session =
  let prover_table = PHprover.create 5 in
  session_iter_proof_attempt
    (fun pa ->
      (* record mostly used pa.proof_timelimit pa.proof_memlimit *)
      let prover = pa.proof_prover in
492
      let timelimits,steplimits,memlimits =
493 494
        try PHprover.find prover_table prover
        with Not_found ->
495
          let x = (Hashtbl.create 5,Hashtbl.create 5,Hashtbl.create 5) in
496 497 498
          PHprover.add prover_table prover x;
          x
      in
499 500 501 502 503 504 505
      let lim_time = Call_provers.get_time pa.proof_limit in
      let lim_mem = Call_provers.get_mem pa.proof_limit in
      let lim_steps = Call_provers.get_steps pa.proof_limit in
      let tf = try Hashtbl.find timelimits lim_time with Not_found -> 0 in
      let sf = try Hashtbl.find steplimits lim_steps with Not_found -> 0 in
      let mf = try Hashtbl.find memlimits lim_mem with Not_found -> 0 in
      Hashtbl.replace timelimits lim_time (tf+1);
Andrei Paskevich's avatar
Andrei Paskevich committed
506 507
      Hashtbl.replace steplimits lim_steps (sf+1);
      Hashtbl.replace memlimits lim_mem (mf+1))
508 509 510
    session;
  prover_table

François Bobot's avatar
François Bobot committed
511 512
exception NoTask

513
let goal_task g = Opt.get_exn NoTask g.goal_task
François Bobot's avatar
François Bobot committed
514 515
let goal_task_option g = g.goal_task

516
let goal_expl g =
MARCHE Claude's avatar
MARCHE Claude committed
517 518
  match g.goal_expl with
  | Some s -> s
519
  | None ->
MARCHE Claude's avatar
MARCHE Claude committed
520 521 522
    try let _,_,l = restore_path g.goal_name in
        String.concat "." l
    with Not_found -> g.goal_name.Ident.id_string
François Bobot's avatar
François Bobot committed
523 524 525 526 527 528 529

(************************)
(* saving state on disk *)
(************************)
open Format

let db_filename = "why3session.xml"
530
let shape_filename = "why3shapes"
531
let compressed_shape_filename = "why3shapes.gz"
532
let session_dir_for_save = ref "."
François Bobot's avatar
François Bobot committed
533

534
let save_string = Pp.html_string
MARCHE Claude's avatar
MARCHE Claude committed
535

536 537 538
let opt pr lab fmt = function
  | None -> ()
  | Some s -> fprintf fmt "@ %s=\"%a\"" lab pr s
MARCHE Claude's avatar
MARCHE Claude committed
539

François Bobot's avatar
François Bobot committed
540
let save_result fmt r =
541 542 543
  let steps = if  r.Call_provers.pr_steps >= 0 then
		Some  r.Call_provers.pr_steps
	      else
544 545 546
		None
  in
  fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"%a/>"
François Bobot's avatar
François Bobot committed
547 548 549 550 551 552
    (match r.Call_provers.pr_answer with
       | Call_provers.Valid -> "valid"
       | Call_provers.Failure _ -> "failure"
       | Call_provers.Unknown _ -> "unknown"
       | Call_provers.HighFailure -> "highfailure"
       | Call_provers.Timeout -> "timeout"
553
       | Call_provers.OutOfMemory -> "outofmemory"
554
       | Call_provers.StepLimitExceeded -> "steplimitexceeded"
François Bobot's avatar
François Bobot committed
555 556
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time
557
    (opt pp_print_int "steps") steps
François Bobot's avatar
François Bobot committed
558 559 560

let save_status fmt s =
  match s with
561
    | Unedited ->
562
        fprintf fmt "<unedited/>"
563
    | Scheduled | Running | Interrupted | JustEdited ->
564
        fprintf fmt "<undone/>"
François Bobot's avatar
François Bobot committed
565
    | InternalFailure msg ->
566
        fprintf fmt "<internalfailure@ reason=\"%a\"/>"
MARCHE Claude's avatar
MARCHE Claude committed
567
          save_string (Printexc.to_string msg)
François Bobot's avatar
François Bobot committed
568 569 570
    | Done r -> save_result fmt r


571 572 573
let save_bool_def name def fmt b =
  if b <> def then fprintf fmt "@ %s=\"%b\"" name b

574 575 576
let save_int_def name def fmt n =
  if n <> def then fprintf fmt "@ %s=\"%d\"" name n

577
let opt_string = opt save_string
François Bobot's avatar
François Bobot committed
578

579
let save_proof_attempt fmt ((id,tl,sl,ml),a) =
François Bobot's avatar
François Bobot committed
580
  fprintf fmt
581
    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a%a>"
582
    id
583 584 585
    (save_int_def "timelimit" tl) (Call_provers.get_time a.proof_limit)
    (save_int_def "steplimit" sl) (Call_provers.get_steps a.proof_limit)
    (save_int_def "memlimit" ml) (Call_provers.get_mem a.proof_limit)
586
    (opt_string "edited") a.proof_edited_as
587 588
    (save_bool_def "obsolete" false) a.proof_obsolete
    (save_bool_def "archived" false) a.proof_archived;
François Bobot's avatar
François Bobot committed
589
  save_status fmt a.proof_state;
590
  fprintf fmt "</proof>@]"
François Bobot's avatar
François Bobot committed
591 592

let save_ident fmt id =
MARCHE Claude's avatar
MARCHE Claude committed
593 594 595 596 597 598 599
  let n=
    try
      let (_,_,l) = Theory.restore_path id in
      String.concat "." l
    with Not_found -> id.Ident.id_string
  in
  fprintf fmt "name=\"%a\"" save_string n
MARCHE Claude's avatar
details  
MARCHE Claude committed
600

601 602
module Compr = Compress.Compress_z

603
type save_ctxt = {
604
  prover_ids : int PHprover.t;
605
  provers : (int * int * int * int) Mprover.t;
606
  ch_shapes : Compr.out_channel;
607 608
}

609 610 611
let save_checksum fmt s =
  fprintf fmt "%s" (Tc.string_of_checksum s)

612
let rec save_goal ctxt fmt g =
613 614
  let shape = Tc.string_of_shape g.goal_shape in
  assert (shape <> "");
François Bobot's avatar
François Bobot committed
615
  fprintf fmt
616
    "@\n@[<v 0>@[<h><goal@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
617
    save_ident g.goal_name
618
    (opt_string "expl") g.goal_expl
619
    (save_bool_def "expanded" false) g.goal_expanded;
620 621 622 623 624 625
  let sum =
    match g.goal_checksum with
    | None -> assert false
    | Some s -> Tc.string_of_checksum s
  in
  Compr.output_string ctxt.ch_shapes sum;
626 627 628
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
629
(*
630
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
631
*)
632
  let l = PHprover.fold
633
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
634
    g.goal_external_proofs [] in
635
  let l = List.sort (fun ((i1,_,_,_),_) ((i2,_,_,_),_) -> compare i1 i2) l in
636 637 638
  List.iter (save_proof_attempt fmt) l;
  let l = PHstr.fold (fun _ t acc -> t :: acc) g.goal_transformations [] in
  let l = List.sort (fun t1 t2 -> compare t1.transf_name t2.transf_name) l in
639 640
  List.iter (save_trans ctxt fmt) l;
  Mmetas_args.iter (save_metas ctxt fmt) g.goal_metas;
François Bobot's avatar
François Bobot committed
641 642
  fprintf fmt "@]@\n</goal>"

643
and save_trans ctxt fmt t =
644
  fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a>@]"
645
    save_string t.transf_name
646
    (save_bool_def "expanded" false) t.transf_expanded;
647
  List.iter (save_goal ctxt fmt) t.transf_goals;
François Bobot's avatar
François Bobot committed
648 649
  fprintf fmt "@]@\n</transf>"

650
and save_metas ctxt fmt _ m =
651
  fprintf fmt "@\n@[<hov 1><metas%a>"
652
    (save_bool_def "expanded" false) m.metas_expanded;
François Bobot's avatar
François Bobot committed
653
  let save_pos fmt pos =
Andrei Paskevich's avatar
Andrei Paskevich committed
654
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
655
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
656
      pos.ip_library;
657
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
658 659
      pos.ip_qualid;
  in
François Bobot's avatar
François Bobot committed
660
  let save_ts_pos fmt ts pos =
661
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
662
    id=\"%i\"@ %a@]@\n</ts_pos>"
François Bobot's avatar
François Bobot committed
663 664 665
      save_string ts.ts_name.id_string (List.length ts.ts_args)
      (ts_hash ts) save_pos pos in
  let save_ls_pos fmt ls pos =
666
    (* TODO: add the signature? *)
667
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
François Bobot's avatar
François Bobot committed
668
      save_string ls.ls_name.id_string
669
      (ls_hash ls) save_pos pos
François Bobot's avatar
François Bobot committed
670 671
  in
  let save_pr_pos fmt pr pos =
672
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
François Bobot's avatar
François Bobot committed
673
      save_string pr.pr_name.id_string
674
      (pr_hash pr) save_pos pos
François Bobot's avatar
François Bobot committed
675 676 677 678 679 680
  in
  Mts.iter (save_ts_pos fmt) m.metas_idpos.idpos_ts;
  Mls.iter (save_ls_pos fmt) m.metas_idpos.idpos_ls;
  Mpr.iter (save_pr_pos fmt) m.metas_idpos.idpos_pr;
  Mstr.iter (fun s smeta_args ->
    Smeta_args.iter (save_meta_args fmt s) smeta_args) m.metas_added;
681
  save_goal ctxt fmt m.metas_goal;
François Bobot's avatar
François Bobot committed
682 683 684
  fprintf fmt "@]@\n</metas>"

and save_meta_args fmt s l =
685
  fprintf fmt "@\n@[<hov 1><meta@ name=\"%a\">" save_string s;
François Bobot's avatar
François Bobot committed
686
  let save_meta_arg fmt = function
687
    | MAty ty -> fprintf fmt "@\n@[<hov 1><meta_arg_ty/>";
François Bobot's avatar
François Bobot committed
688 689 690
      save_ty fmt ty;
      fprintf fmt "@]@\n</meta_arg_ty>"
    | MAts ts ->
691
      fprintf fmt "@\n@[<hov 1><meta_arg_ts@ id=\"%i\"/>@]" (ts_hash ts)
François Bobot's avatar
François Bobot committed
692
    | MAls ls ->
693
      fprintf fmt "@\n@[<hov 1><meta_arg_ls@ id=\"%i\"/>@]" (ls_hash ls)
François Bobot's avatar
François Bobot committed
694
    | MApr pr ->
695
      fprintf fmt "@\n@[<hov 1><meta_arg_pr@ id=\"%i\"/>@]" (pr_hash pr)
François Bobot's avatar
François Bobot committed
696
    | MAstr s ->
697
      fprintf fmt "@\n@[<hov 1><meta_arg_str@ val=\"%s\"/>@]" s
François Bobot's avatar
François Bobot committed
698
    | MAint i ->
699
      fprintf fmt "@\n@[<hov 1><meta_arg_int@ val=\"%i\"/>@]" i
François Bobot's avatar
François Bobot committed
700 701
  in
  List.iter (save_meta_arg fmt) l;
702
  fprintf fmt "@]@\n</meta>"
François Bobot's avatar
François Bobot committed
703 704 705 706

and save_ty fmt ty =
  match ty.ty_node with
  | Tyvar tv ->
707
    fprintf fmt "@\n@[<hov 1><ty_var@ id=\"%i\"/>@]" (tv_hash tv)
François Bobot's avatar
François Bobot committed
708
  | Tyapp (ts,l) ->
709
    fprintf fmt "@\n@[<hov 1><ty_app@ id=\"%i\"/>" (ts_hash ts);
François Bobot's avatar
François Bobot committed
710 711 712
    List.iter (save_ty fmt) l;
    fprintf fmt "@]@\n</ty_app>"

713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728
module CombinedTheoryChecksum = struct

 let b = Buffer.create 1024

 let f () g =
    match g.goal_checksum with
    | None -> assert false
    | Some c -> Buffer.add_string b (Tc.string_of_checksum c)

 let compute th =
   let () = fold_all_sub_goals_of_theory f () th in
   let c = Tc.buffer_checksum b in
   Buffer.clear b; c

end

729
let save_theory ctxt fmt t =
730 731
  let c = CombinedTheoryChecksum.compute t in
  t.theory_checksum <- Some c;
François Bobot's avatar
François Bobot committed
732
  fprintf fmt
733
    "@\n@[<v 1>@[<h><theory@ %a%a%a>@]"
François Bobot's avatar
François Bobot committed
734
    save_ident t.theory_name
735
    (opt save_checksum "sum") t.theory_checksum
736
    (save_bool_def "expanded" false) t.theory_expanded;
737
  List.iter (save_goal ctxt fmt) t.theory_goals;
François Bobot's avatar
François Bobot committed
738 739
  fprintf fmt "@]@\n</theory>"

740
let save_file ctxt fmt _ f =
741
  fprintf fmt
742
    "@\n@[<v 0>@[<h><file@ name=\"%a\"%a%a>@]"
743
    save_string f.file_name (opt_string "format")
744
    f.file_format (save_bool_def "expanded" false) f.file_expanded;
745
  List.iter (save_theory ctxt fmt) f.file_theories;
François Bobot's avatar
François Bobot committed
746 747
  fprintf fmt "@]@\n</file>"

748
let get_prover_to_save prover_ids p (timelimits,steplimits,memlimits) provers =
749 750 751 752 753 754
  let mostfrequent_timelimit,_ =
    Hashtbl.fold
      (fun t f ((_,f') as t') -> if f > f' then (t,f) else t')
      timelimits
      (0,0)
  in
755 756 757 758 759 760
  let mostfrequent_steplimit,_ =
    Hashtbl.fold
      (fun s f ((_,f') as s') -> if f > f' then (s,f) else s')
      steplimits
      (0,0)
  in
761 762 763 764 765 766
  let mostfrequent_memlimit,_ =
    Hashtbl.fold
      (fun m f ((_,f') as m') -> if f > f' then (m,f) else m')
      memlimits
      (0,0)
  in
767 768
  let id =
    try
769
      PHprover.find prover_ids p
770 771 772
    with Not_found ->
      (* we need to find an unused prover id *)
      let occurs = Hashtbl.create 7 in
773
      PHprover.iter (fun _ n -> Hashtbl.add occurs n ()) prover_ids;
774
      let id = ref 0 in
775 776
      try
        while true do
777 778 779
          try
            let _ = Hashtbl.find occurs !id in incr id
          with Not_found -> raise Exit
780
        done;
781
        assert false
782
      with Exit ->
783
        PHprover.add prover_ids p !id;
784 785
        !id
  in
786
  Mprover.add p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) provers
787 788


789
let save_prover fmt id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) =
790 791 792
  let steplimit =
    if mostfrequent_steplimit < 0 then None else Some mostfrequent_steplimit
  in
793
  fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
794
               version=\"%a\"%a@ timelimit=\"%d\"%a@ memlimit=\"%d\"/>@]"
MARCHE Claude's avatar
MARCHE Claude committed
795
    id save_string p.C.prover_name save_string p.C.prover_version
796 797
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
798
    p.C.prover_altern
799 800 801
    mostfrequent_timelimit
    (opt pp_print_int "steplimit") steplimit
    mostfrequent_memlimit
François Bobot's avatar
François Bobot committed
802

803
let save fname shfname _config session =
François Bobot's avatar
François Bobot committed
804
  let ch = open_out fname in
805
  let chsh = Compr.open_out shfname in
François Bobot's avatar
François Bobot committed
806 807
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
808
  fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
809 810 811
  (*
    let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
    fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
812
    save_string rel_file session.session_shape_version;
813
  *)
814
  fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
815
    session.session_shape_version;
816
  Tc.reset_dict ();
817
  let prover_ids = session.session_prover_ids in
818
  let provers =
819 820
    PHprover.fold (get_prover_to_save prover_ids)
      (get_used_provers_with_stats session) Mprover.empty
821
  in
822 823
  let provers_to_save =
    Mprover.fold
824 825
      (fun p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc ->
        Mint.add id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc)
826 827 828 829 830
      provers Mint.empty
  in
  Mint.iter (save_prover fmt) provers_to_save;
  let ctxt = { prover_ids = prover_ids; provers = provers; ch_shapes = chsh } in
  PHstr.iter (save_file ctxt fmt) session.session_files;
François Bobot's avatar
François Bobot committed
831 832
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
833
  close_out ch;
834
  Compr.close_out chsh
François Bobot's avatar
François Bobot committed
835

MARCHE Claude's avatar
MARCHE Claude committed
836
let save_session config session =
François Bobot's avatar
François Bobot committed
837 838
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
839 840
  let fs = Filename.concat session.session_dir shape_filename in
  Sysutil.backup_file fs;
841 842
  let fz = Filename.concat session.session_dir compressed_shape_filename in
  Sysutil.backup_file fz;