src/trywhy3/why3_worker.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2022 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12
  13 (* Interface to Why3 *)
  14
  15 let why3_conf_file = "/trywhy3.conf"
  16
  17 open Why3
  18 open Format
  19 open Worker_proto
  20 open Bindings
  21
  22 module Sys_js = Js_of_ocaml.Sys_js
  23 module Worker = Js_of_ocaml.Worker
  24
  25 let () = log_time ("Initialising why3 worker: start ")
  26
  27 (* Name of the pseudo file *)
  28
  29 let temp_file_name = "/trywhy3_input.mlw"
  30
  31 (* reads the config file *)
  32 let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
  33 (* the [main] section of the config file *)
  34 let main : Whyconf.main = Whyconf.get_main config
  35 (* all the provers detected, from the config file *)
  36 let provers : Whyconf.config_prover Whyconf.Mprover.t =
  37   Whyconf.get_provers config
  38
  39 (* One prover named Alt-Ergo in the config file *)
  40 let alt_ergo : Whyconf.config_prover =
  41   if Whyconf.Mprover.is_empty provers then begin
  42     eprintf "Prover Alt-Ergo not installed or not configured@.";
  43     exit 0
  44   end else snd (Whyconf.Mprover.choose provers)
  45
  46 (* builds the environment from the [loadpath] *)
  47 let env : Env.env = Env.create_env (Whyconf.loadpath main)
  48
  49 let alt_ergo_driver : Driver.driver =
  50   try
  51     Printexc.record_backtrace true;
  52     Whyconf.load_driver main env alt_ergo
  53   with e ->
  54     let s = Printexc.get_backtrace () in
  55     eprintf "Failed to load driver for alt-ergo: %a@.%s@."
  56       Exn_printer.exn_printer e s;
  57   exit 1
  58
  59 let () = log_time ("Initialising why3 worker: end ")
  60
  61 let split_trans = Trans.lookup_transform_l "split_vc" env
  62
  63 (* CF gmain.ml ligne 568 et suivante *)
  64 module W =
  65   struct
  66     let send msg =
  67       ignore (Worker.post_message (marshal msg))
  68
  69     let set_onmessage f =
  70       Worker.set_onmessage (fun data -> f (unmarshal data))
  71   end
  72
  73 (* Task Management *)
  74 module Why3Task = Task (* prevent shadowing *)
  75
  76 module Task =
  77   struct
  78     type task_kind = Theory of Theory.theory | Task of Task.task
  79
  80     type task_info = {
  81         task : task_kind;
  82         parent_id : id;
  83         mutable status : status;
  84         mutable subtasks : id list;
  85         loc : why3_loc list;
  86         expl : string;
  87         pretty : string;
  88       }
  89
  90     let task_table : (id, task_info) Hashtbl.t = Hashtbl.create 17
  91
  92     let clear_table () = Hashtbl.clear task_table
  93     let get_info id = Hashtbl.find task_table id
  94     let get_info_opt id =
  95       try
  96         Some (get_info id)
  97       with
  98         Not_found -> None
  99
 100     let mk_loc (f, a,b,c) =
 101       if f = temp_file_name then
 102         Some (a,b,c)
 103       else None
 104
 105
 106     let warnings = ref []
 107     let clear_warnings () = warnings := []
 108     let () =
 109       Warning.set_hook (fun ?(loc=(Loc.user_position "" 1 0 0)) msg ->
 110                         let _, a,b,_ = Loc.get loc in
 111                         warnings := ((a-1,b), msg) :: !warnings)
 112
 113
 114     let premise_kind = function
 115       | { Term. t_node = Term.Tnot _; t_loc = None } -> "why3-loc-neg-premise"
 116       | _ -> "why3-loc-premise"
 117
 118     let collect_locs t =
 119       (* from why 3 ide *)
 120       let locs = ref [] in
 121       let rec get_locs kind f =
 122         Opt.iter (fun loc ->
 123             match mk_loc (Loc.get loc) with
 124               None -> ()
 125             | Some l -> locs := (kind, l) :: !locs) f.Term.t_loc;
 126         Term.t_fold (fun () t -> get_locs kind t ) () f
 127       in
 128       let rec get_t_locs f =
 129         match f.Term.t_node with
 130         | Term.Tbinop (Term.Timplies,f1,f2) ->
 131            get_locs (premise_kind f1) f1;
 132            get_t_locs f2
 133         | Term.Tlet (t,fb) ->
 134            let _,f1 = Term.t_open_bound fb in
 135            get_locs (premise_kind t) t;
 136            get_t_locs f1
 137         | Term.Tquant (Term.Tforall,fq) ->
 138            let _,_,f1 = Term.t_open_quant fq in
 139            get_t_locs f1
 140         | _ ->
 141            get_locs "why3-loc-goal" f
 142       in
 143       match t with
 144       | Some { Task.task_decl =
 145                  { Theory.td_node =
 146                      Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
 147          get_t_locs f; !locs
 148       |  _ -> []
 149
 150     let task_to_string t =
 151       Format.asprintf "%a" (Driver.print_task alt_ergo_driver) t
 152
 153     let gen_id =
 154       let c = ref 0 in
 155       fun () -> incr c; !c
 156
 157     let task_text t =
 158       Pp.string_of Pretty.print_task t
 159
 160     let register_task parent_id task =
 161       let id = gen_id () in
 162       let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
 163       let id_loc = match vid.Ident.id_loc with
 164           None -> []
 165         | Some l -> begin match mk_loc (Loc.get l) with
 166               Some l -> [ ("why3-loc-goal", l) ]
 167             | None -> []
 168           end
 169       in
 170       let task_info =
 171         { task = Task task;
 172           parent_id = parent_id;
 173           status = StNew;
 174           subtasks = [];
 175           loc = id_loc @  (collect_locs task);
 176           expl = expl;
 177           pretty = task_text task;
 178         }
 179       in
 180       Hashtbl.add task_table id task_info;
 181       id
 182
 183     let register_theory th_name th =
 184       let th_id = gen_id () in
 185       let tasks = Why3Task.split_theory th None None in
 186       let task_ids = List.fold_left (fun acc t ->
 187                                      let tid = register_task th_id t in
 188                                      tid:: acc) [] tasks in
 189       Hashtbl.add task_table th_id  {
 190           task = Theory th;
 191           parent_id = 0;
 192           status = StNew;
 193           subtasks = List.rev task_ids;
 194           loc = [];
 195           expl = th_name;
 196           pretty = "";
 197         };
 198       th_id
 199
 200     let get_task = function
 201       | Task t -> t
 202       | Theory _ -> log ("called get_task on a theory !"); assert false
 203
 204     let set_status id st =
 205       let rec loop id st acc =
 206         match get_info_opt id with
 207         | Some info when info.status <> st ->
 208            info.status <- st;
 209            let acc = (UpdateStatus (st, id)) :: acc in
 210            begin
 211              match get_info_opt info.parent_id with
 212                None -> acc
 213              | Some par_info ->
 214                 let has_new, has_unknown =
 215                   List.fold_left
 216                     (fun (an, au) id ->
 217                      let info = Hashtbl.find task_table id in
 218                      (an || info.status = StNew), (au || info.status = StUnknown))
 219                     (false, false) par_info.subtasks
 220                 in
 221                 let par_status =
 222                   if has_new then StNew
 223                   else if has_unknown then StUnknown
 224                   else StValid
 225                 in
 226                 if par_info.status <> par_status then
 227                   loop info.parent_id par_status acc
 228                 else acc
 229            end
 230         | _ -> acc
 231
 232       in
 233       loop id st []
 234
 235     let rec clean_task id =
 236       try
 237         let info = get_info id in
 238         List.iter clean_task info.subtasks;
 239         Hashtbl.remove task_table id
 240       with
 241         Not_found -> ()
 242
 243   end
 244
 245
 246
 247 (* External API *)
 248
 249
 250 let rec why3_prove ?(steps= ~-1) id =
 251   let open Task in
 252   let t = get_info id in
 253   match t.subtasks with
 254   | [] ->
 255       t.status <- StUnknown;
 256       let task = get_task t.task in
 257       let msg = Worker_proto.Task (id, t.parent_id, t.expl, task_to_string task, t.loc, t.pretty, steps) in
 258       W.send msg;
 259       let l = set_status id StNew in
 260       List.iter W.send l
 261   | l -> List.iter (why3_prove ~steps) l
 262
 263
 264
 265 let rec why3_split t orig id steps unfold =
 266   let open Task in
 267   match Trans.apply split_trans orig with
 268     | [] -> ()
 269     | [ child ] when Why3.Task.task_equal child orig ->
 270         if unfold then why3_split t (Trans.apply Inlining.goal orig) id steps false
 271     | subtasks ->
 272         t.subtasks <- List.map (fun t -> register_task id t) subtasks;
 273         List.iter (fun i -> why3_prove i ~steps) t.subtasks
 274
 275 let why3_split steps id =
 276   let open Task in
 277   let t = get_info id in
 278   match t.subtasks with
 279   | [] -> why3_split t (get_task t.task) id steps true
 280   | _ -> ()
 281
 282
 283
 284 let why3_clean id =
 285   let open Task in
 286   try
 287     let t = get_info id in
 288     List.iter clean_task t.subtasks;
 289     t.subtasks <- [];
 290     let l = set_status id StUnknown in
 291     List.iter W.send l
 292   with
 293     Not_found -> ()
 294
 295 let why3_parse_theories steps theories =
 296   let theories =
 297     Wstdlib.Mstr.fold
 298       (fun thname th acc ->
 299        let loc =
 300          Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
 301        in
 302        (loc, (thname, th)) :: acc) theories []
 303   in
 304   let theories = List.sort  (fun (l1,_) (l2,_) -> Loc.compare l1 l2) theories in
 305   List.iter
 306     (fun (_, (th_name, th)) ->
 307      let th_id = Task.register_theory th_name th in
 308      W.send (Theory(th_id, th_name));
 309      let subs = (Task.get_info th_id).Task.subtasks in
 310      W.send (UpdateStatus( (if subs == [] then StValid else StNew) , th_id));
 311      List.iter (fun i -> why3_prove i ~steps) subs
 312     ) theories
 313
 314 let why3_execute_one m rs =
 315   let open Expr in
 316   let e_unit = e_exec (c_app (rs_tuple 0) [] [] (Ity.ity_tuple [])) in
 317   let (let_defn,pv) = let_var (Ident.id_fresh "o") e_unit in
 318   let e_rs_unit = e_exec (c_app rs [pv] [] rs.rs_cty.Ity.cty_result) in
 319   let expr = e_let let_defn e_rs_unit in
 320   let output = Buffer.create 17 in
 321   Sys_js.set_channel_flusher stdout (fun v -> Buffer.add_string output v);
 322   let {Theory.th_name = th} = m.Pmodule.mod_theory in
 323   let mod_name = th.Ident.id_string in
 324   let result =
 325     try
 326       let ctx = Pinterp.mk_ctx (Pinterp.mk_empty_env env m)
 327           ~do_rac:false ~giant_steps:false () in
 328       let res = Pinterp.exec_global_fundef ctx [] None expr in
 329       Format.print_flush ();
 330       asprintf "@[<v>%s.main produces@,%a@,output:@,%s@]"
 331         mod_name (Pinterp.report_eval_result expr) res
 332         (Buffer.contents output)
 333     with Pinterp_core.Incomplete r ->
 334       asprintf "%s.main cannot compute (%s)" mod_name r in
 335   let mod_loc = Opt.get_def Loc.dummy_position th.Ident.id_loc in
 336   (mod_loc, result)
 337
 338 let why3_execute modules =
 339   let mods =
 340     Wstdlib.Mstr.fold (fun _ m acc ->
 341         match Pmodule.ns_find_rs m.Pmodule.mod_export ["main"] with
 342         | rs -> why3_execute_one m rs :: acc
 343         | exception Not_found -> acc)
 344       modules [] in
 345   let result =
 346     if mods = [] then
 347       Error "No main function found"
 348     else
 349       let s = List.sort (fun (l1,_) (l2,_) -> Loc.compare l2 l1) mods in
 350       Result (List.rev_map snd s) in
 351   W.send result
 352
 353
 354 let () = Sys_js.create_file ~name:temp_file_name ~content:""
 355
 356 let why3_run f format lang code =
 357   try
 358     let ch = open_out temp_file_name in
 359     output_string ch code;
 360     close_out ch;
 361
 362     let (theories, _) = Env.read_file ~format lang env temp_file_name in
 363     W.send (Warning !Task.warnings);
 364     f theories
 365   with
 366   | Loc.Located(loc,e') ->
 367      let _, l, b, e = Loc.get loc in
 368      W.send (ErrorLoc ((l-1,b, l-1, e),
 369                      Pp.sprintf
 370                        "error line %d, columns %d-%d: %a" l b e
 371                        Exn_printer.exn_printer e'))
 372   | e ->
 373      W.send (Error (Pp.sprintf
 374                       "unexpected exception: %a (%s)" Exn_printer.exn_printer e
 375                       (Printexc.to_string e)))
 376
 377 let handle_message = function
 378   | Transform (Split steps, id) -> why3_split steps id
 379   | Transform (Prove steps, id) -> why3_prove ~steps id
 380   | Transform (Clean, id) -> why3_clean id
 381   | ParseBuffer (format, code, steps) ->
 382       Task.clear_warnings ();
 383       Task.clear_table ();
 384       why3_run (why3_parse_theories steps) format Env.base_language code
 385   | ExecuteBuffer (format, code) ->
 386       Task.clear_warnings ();
 387       Task.clear_table ();
 388       why3_run why3_execute format Pmodule.mlw_language code
 389   | SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
 390   | GetFormats ->
 391       let formats = Env.list_formats Env.base_language in
 392       let formats = List.map (fun (name, ext, _) -> (name, ext)) formats in
 393       W.send (Formats formats)
 394
 395
 396 let () =
 397   W.set_onmessage (fun msg ->
 398       handle_message msg;
 399       W.send Idle
 400     )
 401 (*
 402 Local Variables:
 403 compile-command: "unset LANG; make -C ../.. trywhy3"
 404 End:
 405 *)