trywhy3.ml 11.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12
(* simple helpers *)
13

14
let get_opt o = Js.Opt.get o (fun () -> assert false)
15

16
let log s = Firebug.console ## log (Js.string s)
17

18

19
(* module for generating HTML elements *)
20

MARCHE Claude's avatar
MARCHE Claude committed
21 22
module Html = struct

23
let d = Dom_html.document
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26

let node x = (x : #Dom.node Js.t :> Dom.node Js.t)

MARCHE Claude's avatar
MARCHE Claude committed
27
let of_string s = node (d##createTextNode (Js.string s))
MARCHE Claude's avatar
MARCHE Claude committed
28

29 30 31 32 33 34 35
let img i =
  let x = Dom_html.createImg d in
  x##src <- Js.string i;
  x##height <- 12;
  (* X##align <- Js.string "bottom"; *)
  node x

36 37 38 39
let img_accept () = img "accept32.png"
let img_help () = img "help32.png"
let img_bug () = img "bug32.png"

MARCHE Claude's avatar
MARCHE Claude committed
40 41 42 43
let par nl =
  let x = d##createElement (Js.string "p") in
  List.iter (Dom.appendChild x) nl;
  node x
MARCHE Claude's avatar
MARCHE Claude committed
44

MARCHE Claude's avatar
MARCHE Claude committed
45 46 47 48 49 50 51 52 53 54 55
let ul nl =
  let x = d##createElement (Js.string "ul") in
  List.iter
    (fun n ->
      let y =  d##createElement (Js.string "li") in
      List.iter (Dom.appendChild y) n;
      Dom.appendChild x (node y))
    nl;
  node x

end
MARCHE Claude's avatar
MARCHE Claude committed
56

57

58
(* Interface to Why3 and Alt-Ergo *)
MARCHE Claude's avatar
MARCHE Claude committed
59

60
let why3_conf_file = "/trywhy3.conf"
61

MARCHE Claude's avatar
MARCHE Claude committed
62
open Why3
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
open Format

(* 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

93 94 95 96 97 98 99 100 101 102 103 104
module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
module FE = Frontend.Make (SAT)

let print_status fmt _d status steps =
  match status with
  | FE.Unsat _dep ->
    fprintf fmt "Proved (%Ld steps)" steps
  | FE.Inconsistent -> ()
    (* fprintf fmt "Inconsistent assumption" *)
  | FE.Unknown _t | FE.Sat _t ->
      fprintf fmt "Unknown (%Ld steps)@." steps

105 106 107 108 109 110 111 112
type prover_answer = Valid | Unknown of string | Error of string

let report_status report _d status _steps =
  match status with
  | FE.Unsat _dep -> report Valid
  | FE.Inconsistent -> ()
  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")

113 114 115 116
let run_alt_ergo_on_task t =
  (* printing the task in a string *)
  Driver.print_task alt_ergo_driver str_formatter t;
  let text = flush_str_formatter () in
117
  let lb = Lexing.from_string text in
118 119 120 121 122 123
(* from Alt-Ergo, src/main/frontend.ml *)
  let a = Why_parser.file Why_lexer.token lb in
  Parsing.clear_parser ();
  let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
  match Why_typing.split_goals ltd with
  | [d] ->
124
    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
125
    SAT.reset_steps ();
126 127 128 129 130 131 132 133 134 135 136
    let stat = ref (Error "no answer from Alt-Ergo") in
    let f s = stat := s in
    begin
      try
        let _x = Queue.fold (FE.process_decl (report_status f))
          (SAT.empty (), true, Explanation.empty) d
        in
        !stat
      with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
    end
  | _ -> Error "zero or more than 1 goal to solve"
137 138

let split_trans = Trans.lookup_transform_l "split_goal_wp" env
MARCHE Claude's avatar
MARCHE Claude committed
139

140 141 142 143 144
let why3_prove theories =
  let theories =
    Stdlib.Mstr.fold
      (fun thname th acc ->
        let tasks = Task.split_theory th None None in
145
        let tasks = List.rev_map
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
          (fun t ->
            let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
            let expl = match expl with
              | Some s -> s
              | None -> id.Ident.id_string
            in
            let tl = Trans.apply split_trans t in
            let tasks =
              List.map
                (fun task ->
                  let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
                  let expl = match expl with
                    | Some s -> s
                    | None -> id.Ident.id_string
                  in
                  let result = run_alt_ergo_on_task task in
162
                  let img,res = match result with
163 164 165
                    | Valid -> Html.img_accept, expl
                    | Unknown s -> Html.img_help, expl ^ " (" ^ s ^ ")"
                    | Error s -> Html.img_bug, expl ^ " (" ^ s ^ ")"
166
                  in
167
                  [img (); Html.of_string (" " ^ res)])
168 169 170 171 172
                tl
            in
            [Html.of_string expl; Html.ul tasks])
          tasks
        in
173 174 175 176
        let loc =
          Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
        in
        (loc,[ Html.of_string thname; Html.ul tasks]) :: acc)
177 178
      theories []
  in
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
  let s =
    List.sort
      (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
      theories
  in
  Html.ul (List.rev_map snd s)

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"
224 225 226 227 228 229

let why3_execute (modules,_theories) =
  let mods =
    Stdlib.Mstr.fold
      (fun _k m acc ->
        let th = m.Mlw_module.mod_theory in
230 231 232 233 234
        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
235 236 237 238 239 240
          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,[Html.of_string (modname ^ ".main() returns " ^ result)])
          :: acc
241
        with Not_found -> acc)
242 243
      modules []
  in
MARCHE Claude's avatar
MARCHE Claude committed
244 245 246 247 248 249 250 251 252
  match mods with
  | [] -> Html.par [Html.of_string "No main function found"]
  | _ ->
    let s =
      List.sort
        (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
        mods
    in
    Html.ul (List.rev_map snd s)
253

254

255
(* Connecting Why3 calls to the interface *)
256 257 258

let temp_file_name = "/input.mlw"

MARCHE Claude's avatar
MARCHE Claude committed
259
let () = Sys_js.register_file ~name:temp_file_name ~content:""
260

261
let run_why3 f lang global text =
262 263 264
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
265 266
  try
    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
267 268
    let theories = Env.read_file lang env temp_file_name in
    f theories
269 270 271
  with
  | Loc.Located(loc,e') ->
    let (_,l,b,e) = Loc.get loc in
272 273
    ignore (Js.Unsafe.meth_call global "highlightError"
	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
274 275 276 277 278 279 280 281 282 283 284
    Html.par
      [Html.of_string
          (Pp.sprintf
             "error line %d, columns %d-%d: %a" l b e
             Exn_printer.exn_printer e')]
  | e ->
    Html.par
      [Html.of_string
          (Pp.sprintf
             "unexpected exception: %a (%s)" Exn_printer.exn_printer e
             (Printexc.to_string e))]
285

MARCHE Claude's avatar
MARCHE Claude committed
286
let add_why3_cmd buttonname f input_lang =
287 288 289 290
  let handler = Dom.handler
    (fun _ev ->
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
291 292
      let lang = "en"
(*
MARCHE Claude's avatar
MARCHE Claude committed
293 294 295
        Js.to_string
          (Js.Unsafe.meth_call editor "getAttribute"
             [| Js.Unsafe.inject (Js.string "lang") |])
296
*)
MARCHE Claude's avatar
MARCHE Claude committed
297
      in
298
      let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
MARCHE Claude's avatar
MARCHE Claude committed
299 300 301
      log ("Why3 is running, lang = " ^ lang);
      let answer = run_why3 f input_lang global code in
      log "Why3 answer given";
302 303 304
      let console =
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
      in
MARCHE Claude's avatar
MARCHE Claude committed
305
      (* remove the previous answer if any *)
306 307 308
      Js.Opt.iter (console##lastChild) (Dom.removeChild console);
      (* put the new answer *)
      Dom.appendChild console answer;
MARCHE Claude's avatar
MARCHE Claude committed
309
      (* give the focus back to the editor *)
310
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
311
      Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
312
  in
313
  let button =
314
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
315 316
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
317

318 319 320 321
let () =
  add_why3_cmd "prove" why3_prove Env.base_language;
  add_why3_cmd "run" why3_execute Mlw_module.mlw_language

322

323
(* Predefined examples *)
324

325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
let add_file_example buttonname file =
  let handler = Dom.handler
    (fun _ev ->
      let text = Sysutil.file_contents file in
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
      Js.Unsafe.set global (Js.string "loadedBuffer") (Js.string text);
      let loaded = Filename.basename file in
      Js.Unsafe.set global (Js.string "loadedFilename") (Js.string loaded);
      ignore (Js.Unsafe.meth_call global "replaceWithLoaded" [| |]);
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
      Js._false)
  in
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
  in
  button ## onclick <- handler

let () =
  add_file_example "drinkers" "/drinkers.why";
345 346
(*  add_file_example "simplearith" "/simplearith.why";*)
  add_file_example "bin_mult" "/bin_mult.mlw";
347
  add_file_example "fact" "/fact.mlw";
348 349
  add_file_example "isqrt" "/isqrt.mlw";
  Options.set_steps_bound 100
350

MARCHE Claude's avatar
MARCHE Claude committed
351 352 353 354 355 356

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
End:
*)