why3_worker.ml 11.2 KB
Newer Older
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  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)


(* Interface to Why3 and Alt-Ergo *)

let why3_conf_file = "/trywhy3.conf"

open Why3
open Format
open Worker_proto

21 22


23 24
let () = log_time ("Initialising why3 worker: start ")

25 26 27
(* Name of the pseudo file *)

let temp_file_name = "/trywhy3_input.mlw"
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49

(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
  if Whyconf.Mprover.is_empty provers then begin
    eprintf "Prover Alt-Ergo not installed or not configured@.";
    exit 0
  end else snd (Whyconf.Mprover.choose provers)

(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)

let alt_ergo_driver : Driver.driver =
  try
    Printexc.record_backtrace true;
50
    Whyconf.load_driver main env alt_ergo.Whyconf.driver []
51 52 53 54 55 56 57 58
  with e ->
    let s = Printexc.get_backtrace () in
    eprintf "Failed to load driver for alt-ergo: %a@.%s@."
      Exn_printer.exn_printer e s;
  exit 1

let () = log_time ("Initialising why3 worker: end ")

59
let split_trans = Trans.lookup_transform_l "split_vc" env
60

61
(* CF gmain.ml ligne 568 et suivante *)
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
module W =
  struct
    let send msg =
      ignore (Worker.post_message (marshal msg))

    let set_onmessage f =
      Worker.set_onmessage (fun data -> f (unmarshal data))
  end

(* Task Management *)
module Why3Task = Task (* prevent shadowing *)

module Task =
  struct
    type task_info =
      { task : [ `Theory of Theory.theory | `Task of Task.task ];
	parent_id : id;
	mutable status : status;
	mutable subtasks : id list;
81
	loc : why3_loc list;
82
	expl : string;
83
        pretty : string;
84 85 86 87 88
      }

    let task_table : (id, task_info) Hashtbl.t = Hashtbl.create 17

    let clear_table () = Hashtbl.clear task_table
89 90 91 92 93 94
    let get_info id = Hashtbl.find task_table id
    let get_info_opt id =
      try
        Some (get_info id)
      with
        Not_found -> None
95

96
    let get_parent_id id = (get_info id).parent_id
97

98 99 100 101
    let mk_loc (f, a,b,c) =
      if f = temp_file_name then
        Some (a,b,c)
      else None
102 103 104 105 106 107


    let warnings = ref []
    let clear_warnings () = warnings := []
    let () =
      Warning.set_hook (fun ?(loc=(Loc.user_position "" 1 0 0)) msg ->
MARCHE Claude's avatar
MARCHE Claude committed
108
                        let _, a,b,_ = Loc.get loc in
109 110 111
                        warnings := ((a-1,b), msg) :: !warnings)


112
    let premise_kind = function
113
      | { Term. t_node = Term.Tnot _; t_loc = None } -> "why3-loc-neg-premise"
114 115
      | _ -> "why3-loc-premise"

116 117 118
    let collect_locs t =
      (* from why 3 ide *)
      let locs = ref [] in
119
      let rec get_locs kind f =
120 121 122 123
        Opt.iter (fun loc ->
            match mk_loc (Loc.get loc) with
              None -> ()
            | Some l -> locs := (kind, l) :: !locs) f.Term.t_loc;
124
        Term.t_fold (fun () t -> get_locs kind t ) () f
125 126 127 128
      in
      let rec get_t_locs f =
        match f.Term.t_node with
        | Term.Tbinop (Term.Timplies,f1,f2) ->
129
           get_locs (premise_kind f1) f1;
130 131 132
           get_t_locs f2
        | Term.Tlet (t,fb) ->
           let _,f1 = Term.t_open_bound fb in
133
           get_locs (premise_kind t) t;
134 135 136 137 138
           get_t_locs f1
        | Term.Tquant (Term.Tforall,fq) ->
           let _,_,f1 = Term.t_open_quant fq in
           get_t_locs f1
        | _ ->
139
           get_locs "why3-loc-goal" f
140 141 142 143 144 145 146
      in
      match t with
      | Some { Task.task_decl =
                 { Theory.td_node =
                     Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
         get_t_locs f; !locs
      |  _ -> []
147 148

    let task_to_string t =
149
      Format.asprintf "%a" (Driver.print_task alt_ergo_driver) t
150 151 152 153 154

    let gen_id =
      let c = ref 0 in
      fun () -> incr c; "id" ^ (string_of_int !c)

155 156 157
    let task_text t =
      Pp.string_of Pretty.print_task t

158 159 160
    let register_task parent_id task =
      let id = gen_id () in
      let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
161 162
      let id_loc = match vid.Ident.id_loc with
          None -> []
163 164 165 166
        | Some l -> begin match mk_loc (Loc.get l) with
              Some l -> [ ("why3-loc-goal", l) ]
            | None -> []
          end
167
      in
168 169 170 171 172
      let task_info =
        { task = `Task(task);
	  parent_id = parent_id;
	  status = `New;
	  subtasks = [];
173
	  loc = id_loc @  (collect_locs task);
174
	  expl = expl;
175
          pretty = task_text task;
176
        }
177 178 179 180 181 182 183 184 185 186 187 188 189
      in
      Hashtbl.add task_table id task_info;
      id

    let register_theory th_name th =
      let th_id = gen_id () in
      let tasks = Why3Task.split_theory th None None in
      let task_ids = List.fold_left (fun acc t ->
				     let tid = register_task th_id t in
				     tid:: acc) [] tasks in
      Hashtbl.add task_table th_id  { task = `Theory(th);
				      parent_id = "theory-list";
				      status = `New;
190
				      subtasks = List.rev task_ids;
191
				      loc = [];
192 193 194
				      expl = th_name;
                                      pretty = "";
                                    };
195 196 197 198 199 200 201 202 203
      th_id

    let get_task = function `Task t -> t
                          | `Theory _ -> log ("called get_task on a theory !"); assert false

    let set_status id st =
      let rec loop id st acc =
        match
          try
204
            Some (get_info id)
205 206
          with Not_found -> None
        with
207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
        | Some info when info.status <> st ->
	   info.status <- st;
           let acc = (UpdateStatus (st, id)) :: acc in
           begin
             match get_info_opt info.parent_id with
               None -> acc
             | Some par_info ->
	        let has_new, has_unknown =
	          List.fold_left
	            (fun (an, au) id ->
	             let info = Hashtbl.find task_table id in
	             (an || info.status = `New), (au || info.status = `Unknown))
	            (false, false) par_info.subtasks
	        in
	        let par_status = if has_new then `New else if
			           has_unknown then `Unknown
			         else `Valid
	        in
	        if par_info.status <> par_status then
	          loop info.parent_id par_status acc
                else acc
           end
        | _ -> acc

231 232 233 234 235
      in
      loop id st []

    let rec clean_task id =
      try
236
        let info = get_info id in
237 238 239 240 241 242 243 244 245 246
        List.iter clean_task info.subtasks;
        Hashtbl.remove task_table id
      with
        Not_found -> ()

  end



(* External API *)
247 248


249
let rec why3_prove ?(steps= ~-1) id =
250
  let open Task in
251
  let t = get_info id in
252 253
  match t.subtasks with
    [] ->  t.status <- `Unknown;
254
	  let task = get_task t.task in
255
	  let msg = Task (id, t.parent_id, t.expl, task_to_string task, t.loc, t.pretty, steps) in
256 257 258
	  W.send msg;
	  let l = set_status id `New in
          List.iter W.send l
259
  | l -> List.iter (why3_prove ~steps) l
260 261


Kim Nguyễn's avatar
Kim Nguyễn committed
262
let why3_split id =
263
  let open Task in
264
  let t = get_info id in
265 266
  match t.subtasks with
    [] ->
267 268 269 270 271 272 273 274 275 276
    begin
      match Trans.apply split_trans (get_task t.task), t.task with
	[], _ -> ()
      | [ child ], `Task(orig) when Why3.Task.task_equal child orig -> ()
      | subtasks, _ ->
	 t.subtasks <- List.fold_left (fun acc t ->
				       let tid = register_task id t in
				       why3_prove tid;
				       tid :: acc) [] subtasks
    end
277
  | _ -> ()
Kim Nguyễn's avatar
Kim Nguyễn committed
278

279

Kim Nguyễn's avatar
Kim Nguyễn committed
280

281
let why3_clean id =
282
  let open Task in
283
  try
284
    let t = get_info id in
285 286
    List.iter clean_task t.subtasks;
    t.subtasks <- [];
287 288
    let l = set_status id `Unknown in
    List.iter W.send l
289 290
  with
    Not_found -> ()
291

292 293 294 295
let why3_prove_all () =
  Hashtbl.iter
    (fun _ info ->
     match info.Task.task with
296
       `Theory _ -> List.iter (fun i -> why3_prove i) info.Task.subtasks
297 298
     | _ -> ()) Task.task_table

299

300
let why3_parse_theories theories =
301
  let theories =
302
    Wstdlib.Mstr.fold
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
      (fun thname th acc ->
       let loc =
         Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
       in
       (loc, (thname, th)) :: acc) theories []
  in
  let theories = List.sort  (fun (l1,_) (l2,_) -> Loc.compare l1 l2) theories in
  List.iter
    (fun (_, (th_name, th)) ->
     let th_id = Task.register_theory th_name th in
     W.send (Theory(th_id, th_name));
     let subs = (Task.get_info th_id).Task.subtasks in
     W.send (UpdateStatus( (if subs == [] then `Valid else `New) , th_id));
     List.iter (fun i -> why3_prove i) subs
    ) theories
318

Guillaume Melquiond's avatar
Guillaume Melquiond committed
319
let why3_execute modules =
320 321
  let result =
    let mods =
322
      Wstdlib.Mstr.fold
323
	(fun _k m acc ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
324
         let th = m.Pmodule.mod_theory in
325 326
         let modname = th.Theory.th_name.Ident.id_string in
         try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
327
           let rs = Pmodule.ns_find_rs m.Pmodule.mod_export ["main"]
328
           in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
329
           let result = Pp.sprintf "%a" (Pinterp.eval_global_symbol env m) rs in
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
           let loc =
             Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
           in
           (loc, modname ^ ".main() returns " ^ result)
           :: acc
         with Not_found -> acc)
	modules []
    in
    match mods with
    | [] -> Error "No main function found"
    | _ ->
       let s =
	 List.sort
           (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
           mods
       in
       (Result (List.rev_map snd s) )
  in
348
  W.send result
349 350


Guillaume Melquiond's avatar
Guillaume Melquiond committed
351
let () = Sys_js.create_file ~name:temp_file_name ~content:""
352 353 354 355 356 357 358 359

let why3_run f lang code =
  try
    let ch = open_out temp_file_name in
    output_string ch code;
    close_out ch;

    let theories = Env.read_file lang env temp_file_name in
360
    W.send (Warning !Task.warnings);
361 362 363 364
    f theories
  with
  | Loc.Located(loc,e') ->
     let _, l, b, e = Loc.get loc in
365
     W.send (ErrorLoc ((l-1,b, l-1, e),
366 367 368 369
		     Pp.sprintf
		       "error line %d, columns %d-%d: %a" l b e
		       Exn_printer.exn_printer e'))
  | e ->
370 371 372
     W.send (Error (Pp.sprintf
		      "unexpected exception: %a (%s)" Exn_printer.exn_printer e
		      (Printexc.to_string e)))
373 374 375


let () =
376
  W.set_onmessage
377
    (fun msg ->
378 379 380 381 382 383 384
     let () =
       match msg with
       | Transform (`Split, id) -> why3_split id
       | Transform (`Prove(steps), id) -> why3_prove ~steps id
       | Transform (`Clean, id) -> why3_clean id
       | ProveAll -> why3_prove_all ()
       | ParseBuffer code ->
385
          Task.clear_warnings ();
386 387 388
          Task.clear_table ();
          why3_run why3_parse_theories Env.base_language code
       | ExecuteBuffer code ->
389
          Task.clear_warnings ();
390
	  Task.clear_table ();
Guillaume Melquiond's avatar
Guillaume Melquiond committed
391
	  why3_run why3_execute Pmodule.mlw_language code
392 393 394
       | SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
     in
     W.send Idle
395 396 397
    )
(*
Local Variables:
398
compile-command: "unset LANG; make -C ../.. trywhy3"
399 400
End:
*)