Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

why3_worker.ml 11.3 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 149

    let task_to_string t =
      ignore (flush_str_formatter ());
MARCHE Claude's avatar
MARCHE Claude committed
150
      Driver.print_task alt_ergo_driver str_formatter t;
151 152 153 154 155 156
      flush_str_formatter ()

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

157 158 159
    let task_text t =
      Pp.string_of Pretty.print_task t

160 161 162
    let register_task parent_id task =
      let id = gen_id () in
      let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
163 164
      let id_loc = match vid.Ident.id_loc with
          None -> []
165 166 167 168
        | Some l -> begin match mk_loc (Loc.get l) with
              Some l -> [ ("why3-loc-goal", l) ]
            | None -> []
          end
169
      in
170 171 172 173 174
      let task_info =
        { task = `Task(task);
	  parent_id = parent_id;
	  status = `New;
	  subtasks = [];
175
	  loc = id_loc @  (collect_locs task);
176
	  expl = expl;
177
          pretty = task_text task;
178
        }
179 180 181 182 183 184 185 186 187 188 189 190 191 192
      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;
				      subtasks = task_ids;
193
				      loc = [];
194 195 196
				      expl = th_name;
                                      pretty = "";
                                    };
197 198 199 200 201 202 203 204 205
      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
206
            Some (get_info id)
207 208
          with Not_found -> None
        with
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
        | 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

233 234 235 236 237
      in
      loop id st []

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

  end



(* External API *)
249 250


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


Kim Nguyễn's avatar
Kim Nguyễn committed
264
let why3_split id =
265
  let open Task in
266
  let t = get_info id in
267 268
  match t.subtasks with
    [] ->
269 270 271 272 273 274 275 276 277 278
    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
279
  | _ -> ()
Kim Nguyễn's avatar
Kim Nguyễn committed
280

281

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

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

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

301

302
let why3_parse_theories theories =
303
  let theories =
304
    Wstdlib.Mstr.fold
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
      (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
320

Guillaume Melquiond's avatar
Guillaume Melquiond committed
321
let why3_execute modules =
322 323
  let result =
    let mods =
324
      Wstdlib.Mstr.fold
325
	(fun _k m acc ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
326
         let th = m.Pmodule.mod_theory in
327 328
         let modname = th.Theory.th_name.Ident.id_string in
         try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
329
           let rs = Pmodule.ns_find_rs m.Pmodule.mod_export ["main"]
330
           in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
331
           let result = Pp.sprintf "%a" (Pinterp.eval_global_symbol env m) rs in
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
           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
350
  W.send result
351 352


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

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


let () =
378
  W.set_onmessage
379
    (fun msg ->
380 381 382 383 384 385 386
     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 ->
387
          Task.clear_warnings ();
388 389 390
          Task.clear_table ();
          why3_run why3_parse_theories Env.base_language code
       | ExecuteBuffer code ->
391
          Task.clear_warnings ();
392
	  Task.clear_table ();
Guillaume Melquiond's avatar
Guillaume Melquiond committed
393
	  why3_run why3_execute Pmodule.mlw_language code
394 395 396
       | SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
     in
     W.send Idle
397 398 399
    )
(*
Local Variables:
400
compile-command: "unset LANG; make -C ../.. trywhy3"
401 402
End:
*)