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 8.4 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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

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


(* 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;
    Driver.load_driver env alt_ergo.Whyconf.driver []
  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 ")


Kim Nguyễn's avatar
Kim Nguyễn committed
55
let task_table = Hashtbl.create 17
56 57 58 59 60 61 62 63 64 65 66 67 68

let split_trans = Trans.lookup_transform_l "split_goal_wp" env

let task_to_string t =
  ignore (flush_str_formatter ());
  Driver.print_task alt_ergo_driver str_formatter t;
  flush_str_formatter ()

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

let send msg =
Kim Nguyễn's avatar
Kim Nguyễn committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
  ignore (Worker.post_message (marshal msg))


let get_loc l =
  match l with
    Some (l) ->
    let _, l, c1, c2 = Loc.get l in
    Some (l, c1, l, c2)
  | _ -> None


let send_task parent_id task =
  let id = gen_id () in
  let () = Hashtbl.add task_table id (`Task (task), parent_id, `New, []) in
  let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
  let expl = match expl with
    | Some s -> s
    | None -> vid.Ident.id_string
  in
  let msg = Task (id, parent_id, expl, task_to_string task, [ (* TODO *) ]) in
  send msg;
  send (UpdateStatus(`New, id));
  id
let get_task = function `Task t -> t
                      | `Theory _ -> log ("called get_task on a theory !"); assert false

let why3_split id =
  try
    let task, parent_id,_,subtasks =  Hashtbl.find task_table id in
    match subtasks with
      [] ->
      let subtasks = Trans.apply split_trans (get_task task) in
      send (UpdateStatus(`New, id));
      let sub_ids = List.fold_left (fun acc t -> (send_task id t)::acc) [] subtasks in
      Hashtbl.replace task_table id (task,parent_id, `New, sub_ids)
    | _ -> ()
  with
    Not_found -> log ("No task with id " ^ id)

let set_status st id =
  try
    let task, parent_id, _, subs = Hashtbl.find task_table id in
    Hashtbl.replace task_table id (task, parent_id, st, subs);
    let _,_,_, depends = Hashtbl.find task_table parent_id  in
    send (UpdateStatus (st, id));
    if
      List.for_all (fun cid -> try
                            match Hashtbl.find task_table cid with
                              (_, _, `Valid, _) -> true
                            | _ -> false
                          with Not_found -> false) depends
    then
      send (UpdateStatus (`Valid, parent_id))
  with
    Not_found -> log ("No task with id " ^ id)


126 127 128 129 130 131 132 133 134 135 136 137 138 139

let why3_parse_theories theories =
  let theories =
    Stdlib.Mstr.fold
      (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 = gen_id () in
Kim Nguyễn's avatar
Kim Nguyễn committed
140 141
     let () = send (Theory(th_id, th_name)) in
     send (UpdateStatus(`New, th_id));
142
     let tasks = Task.split_theory th None None in
Kim Nguyễn's avatar
Kim Nguyễn committed
143 144
     let task_ids = List.fold_left (fun acc t ->  (send_task th_id t):: acc) [] tasks in
     Hashtbl.add task_table th_id (`Theory(th), "theory-list", `New, task_ids)
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
    ) theories

let execute_symbol m fmt ps =
  match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
  | None ->
     fprintf fmt "function '%s' has no definition"
	     ps.Mlw_expr.ps_name.Ident.id_string
  | Some d ->
    let lam = d.Mlw_expr.fun_lambda in
    match lam.Mlw_expr.l_args with
    | [pvs] when
        Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
      begin
        let spec = lam.Mlw_expr.l_spec in
        let eff = spec.Mlw_ty.c_effect in
        let writes = eff.Mlw_ty.eff_writes in
        let body = lam.Mlw_expr.l_expr in
        try
          let res, _final_env =
            Mlw_interp.eval_global_expr env m.Mlw_module.mod_known
              m.Mlw_module.mod_theory.Theory.th_known writes body
          in
          match res with
          | Mlw_interp.Normal v -> Mlw_interp.print_value fmt v
          | Mlw_interp.Excep(x,v) ->
            fprintf fmt "exception %s(%a)"
              x.Mlw_ty.xs_name.Ident.id_string Mlw_interp.print_value v
          | Mlw_interp.Irred e ->
            fprintf fmt "cannot execute expression@ @[%a@]"
              Mlw_pretty.print_expr e
          | Mlw_interp.Fun _ ->
            fprintf fmt "result is a function"
        with e ->
          fprintf fmt
            "failure during execution of function: %a (%s)"
            Exn_printer.exn_printer e
            (Printexc.to_string e)
    end
  | _ ->
    fprintf fmt "Only functions with one unit argument can be executed"

let why3_execute (modules,_theories) =
  let result =
    let mods =
      Stdlib.Mstr.fold
	(fun _k m acc ->
         let th = m.Mlw_module.mod_theory in
         let modname = th.Theory.th_name.Ident.id_string in
         try
           let ps =
             Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
           in
           let result = Pp.sprintf "%a" (execute_symbol m) ps in
           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
  send result

let temp_file_name = "/input.mlw"

let () = Sys_js.register_file ~name:temp_file_name ~content:""

let why3_run f lang code =
  try
    log_time "Why3 worker : start writing file";
    let ch = open_out temp_file_name in
    output_string ch code;
    close_out ch;
    log_time "Why3 worker : stop writing file";

    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
    log_time "Why3 worker : start parsing file";

    let theories = Env.read_file lang env temp_file_name in
    log_time "Why3 worker : stop parsing file";
    f theories
  with
  | Loc.Located(loc,e') ->
     let _, l, b, e = Loc.get loc in
     send (ErrorLoc ((l-1,b, l-1, e),
		     Pp.sprintf
		       "error line %d, columns %d-%d: %a" l b e
		       Exn_printer.exn_printer e'))
  | e ->
     send (Error (Pp.sprintf
		    "unexpected exception: %a (%s)" Exn_printer.exn_printer e
		    (Printexc.to_string e)))


let () =
Kim Nguyễn's avatar
Kim Nguyễn committed
250

251 252 253 254 255 256 257
  Worker.set_onmessage
    (fun ev ->

     log_time ("Entering why3 worker ");
     let ev = unmarshal ev in
     log_time ("After unmarshal ");
     match ev with
Kim Nguyễn's avatar
Kim Nguyễn committed
258 259
     | Transform (`Split, id) ->
        why3_split id
260
     | ParseBuffer code ->
Kim Nguyễn's avatar
Kim Nguyễn committed
261 262
        Hashtbl.clear task_table;
        why3_run why3_parse_theories Env.base_language code
263 264
     | ExecuteBuffer code ->
	why3_run why3_execute Mlw_module.mlw_language code
Kim Nguyễn's avatar
Kim Nguyễn committed
265
     | SetStatus (st, id) -> set_status st id
266 267 268 269 270 271
    )
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
End:
*)