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.1 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
      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 =
202
        match get_info_opt id with
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
        | 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

227 228 229 230 231
      in
      loop id st []

    let rec clean_task id =
      try
232
        let info = get_info id in
233 234 235 236 237 238 239 240 241 242
        List.iter clean_task info.subtasks;
        Hashtbl.remove task_table id
      with
        Not_found -> ()

  end



(* External API *)
243 244


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


Kim Nguyễn's avatar
Kim Nguyễn committed
258
let why3_split id =
259
  let open Task in
260
  let t = get_info id in
261 262
  match t.subtasks with
    [] ->
263 264 265 266 267
    begin
      match Trans.apply split_trans (get_task t.task), t.task with
	[], _ -> ()
      | [ child ], `Task(orig) when Why3.Task.task_equal child orig -> ()
      | subtasks, _ ->
268 269
          t.subtasks <- List.map (fun t -> register_task id t) subtasks;
          List.iter why3_prove t.subtasks
270
    end
271
  | _ -> ()
Kim Nguyễn's avatar
Kim Nguyễn committed
272

273

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

275
let why3_clean id =
276
  let open Task in
277
  try
278
    let t = get_info id in
279 280
    List.iter clean_task t.subtasks;
    t.subtasks <- [];
281 282
    let l = set_status id `Unknown in
    List.iter W.send l
283 284
  with
    Not_found -> ()
285

286 287 288 289
let why3_prove_all () =
  Hashtbl.iter
    (fun _ info ->
     match info.Task.task with
290
       `Theory _ -> List.iter (fun i -> why3_prove i) info.Task.subtasks
291 292
     | _ -> ()) Task.task_table

293

294
let why3_parse_theories theories =
295
  let theories =
296
    Wstdlib.Mstr.fold
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
      (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
312

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


Guillaume Melquiond's avatar
Guillaume Melquiond committed
345
let () = Sys_js.create_file ~name:temp_file_name ~content:""
346 347 348 349 350 351 352 353

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
354
    W.send (Warning !Task.warnings);
355 356 357 358
    f theories
  with
  | Loc.Located(loc,e') ->
     let _, l, b, e = Loc.get loc in
359
     W.send (ErrorLoc ((l-1,b, l-1, e),
360 361 362 363
		     Pp.sprintf
		       "error line %d, columns %d-%d: %a" l b e
		       Exn_printer.exn_printer e'))
  | e ->
364 365 366
     W.send (Error (Pp.sprintf
		      "unexpected exception: %a (%s)" Exn_printer.exn_printer e
		      (Printexc.to_string e)))
367 368 369


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