why3session_lib.ml 8.97 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   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 Why3
13

14 15 16
module S = Session
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 64 65

let read_env_spec () =
  (** Configuration *)
  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 75 76
  let env = Env.create_env loadpath in
  env,config,read_simple_spec ()


let read_update_session ~allow_obsolete env config fname =
  let project_dir = Session.get_project_dir fname in
77
  let session,use_shapes = Session.read_session project_dir in
78 79 80 81
  let ctxt = {
    S.allow_obsolete_goals = allow_obsolete;
    S.release_tasks = false;
    S.use_shapes_for_pairing_sub_goals = use_shapes;
82
    (* S.theory_is_fully_up_to_date = false; *)
83 84
    S.keygen = fun ?parent:_ _ -> ();
  }
85
  in
MARCHE Claude's avatar
MARCHE Claude committed
86
  Session.update_session ~ctxt session env config
87 88 89

(** filter *)
type filter_prover =
90 91
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
92 93 94 95

let filter_prover = Stack.create ()

let read_opt_prover s =
96
  try
97
    let l = Strings.rev_split ',' s in
98 99 100 101 102 103 104 105 106 107
    match l with
    | [altern;version;name] when List.for_all (fun s -> s.[0] <> '^') l ->
      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 ^")
108 109 110 111


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

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
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)

127 128
let opt_status = ref []

129 130 131
let filter_spec =
  ["--filter-prover", Arg.String add_filter_prover,
   " [name,version[,alternative]|id] \
132
the proof containing this prover are selected";
François Bobot's avatar
François Bobot committed
133
   "--filter-obsolete", opt_three opt_filter_obsolete,
134 135 136 137 138 139 140
   " 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)";
141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
   "--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",
   Arg.String (fun s -> opt_status := Call_provers.Unknown s::!opt_status),
   " 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";
156
]
157

158 159 160 161 162 163
type filters =
    { provers : C.Sprover.t; (* if empty : every provers *)
      obsolete : filter_three;
      archived : filter_three;
      verified : filter_three;
      verified_goal : filter_three;
164
      status : Call_provers.prover_answer list; (* if empty : any answer *)
165
    }
166

167 168 169 170 171
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)

172
let prover_of_filter_prover whyconf = function
173 174 175 176
  | Prover p        -> p
  | FilterProver fp ->
    (C.filter_one_prover whyconf fp).C.prover

177 178 179 180 181 182

let read_filter_spec whyconf : filters * bool =
  let should_exit = ref false in
  let s = ref C.Sprover.empty in
  let iter p =
    try
183 184
      s := C.Sprover.union (provers_of_filter_prover whyconf p) !s
    with C.ProverNotFound (_,fp) ->
185
      Format.eprintf
186 187 188
        "The prover %a is not found in the configuration file %s@."
        Whyconf.print_filter_prover fp
        (Whyconf.get_conf_file whyconf);
189 190
      should_exit := true in
  Stack.iter iter filter_prover;
191 192 193 194 195
  {provers = !s;
   obsolete = !opt_filter_obsolete;
   archived = !opt_filter_archived;
   verified = !opt_filter_verified;
   verified_goal = !opt_filter_verified_goal;
196
   status = !opt_status;
197 198
  },!should_exit

199
let iter_proof_attempt_by_filter iter filters f session =
200 201 202 203 204 205 206
  (** provers *)
  let iter_provers a =
    if C.Sprover.mem a.S.proof_prover filters.provers then f a in
  let f = if C.Sprover.is_empty filters.provers then f else iter_provers in
  (** three value *)
  let three_value f v p =
    let iter_obsolete a =
207 208 209
      match v, p a with
        | FT_No, false -> f a
        | FT_Yes, true -> f a
210 211 212 213 214 215 216 217
        | _ -> () (** FT_All treated after *) in
    if v = FT_All then f else iter_obsolete in
  (** obsolete *)
  let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
  (** archived *)
  let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
  (** verified_goal *)
  let f = three_value f filters.verified_goal
218
    (fun a -> Opt.inhabited a.S.proof_parent.S.goal_verified) in
219
  (** verified *)
220 221
  let f = three_value f filters.verified 
    (fun p -> Opt.inhabited (S.proof_verified p)) in
222 223 224 225 226 227 228 229 230 231 232
  (** status *)
  let f = if filters.status = [] then f else
      (fun a -> match a.S.proof_state with
      | S.Done pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
      | _ -> ()) in
  iter f session

let theory_iter_proof_attempt_by_filter filters f th =
  iter_proof_attempt_by_filter S.theory_iter_proof_attempt filters f th
let session_iter_proof_attempt_by_filter filters f s =
  iter_proof_attempt_by_filter S.session_iter_proof_attempt filters f s
233 234

let set_filter_verified_goal t = opt_filter_verified_goal := t
235 236 237 238 239 240

let opt_force_obsolete = ref false

let force_obsolete_spec =
  ["-F", Arg.Set opt_force_obsolete,
   " transform obsolete session"]
241 242 243 244 245 246 247 248 249 250 251



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

252
let ask_yn_nonblock ~callback =
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
  let b = Buffer.create 3 in
  let s = String.create 1 in
  Format.printf "(y/n)@.";
  fun () ->
    match Unix.select [Unix.stdin] [] [] 0. with
    | [],_,_ -> true
    | _ ->
      if Unix.read Unix.stdin s 1 0 = 0 then
        begin (** EndOfFile*) callback false; false end
      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