trywhy3: preliminary version with web workers

contributed by Kim Nguyen <kn@lri.fr>

.gitignore

@@ -278,14 +278,19 @@ pvsbin/
 /modules/mach/int/
 
 # Try Why3
-/src/trywhy3/trywhy3.js
 /src/trywhy3/trywhy3.byte
+/src/trywhy3/trywhy3.js
+/src/trywhy3/alt_ergo_worker.byte
+/src/trywhy3/alt_ergo_worker.js
+/src/trywhy3/why3_worker.byte
+/src/trywhy3/why3_worker.js
 /src/trywhy3/index.en.html
 /src/trywhy3/index.fr.html
 /src/trywhy3/index.html
-/src/trywhy3/ace-builds
+/src/trywhy3/ace-builds/
 /src/trywhy3/*.png
 /src/trywhy3/alt-ergo-1.00-private-2015-01-29
+/src/trywhy3/fontawesome/
 
 # jessie3
 /src/jessie/config.log

Makefile.in

@@ -1504,10 +1504,10 @@ ALTERGOMODS=util/numsNumbers util/numbers \
 	instances/matching \
 	sat/sat_solvers \
 	main/frontend
+ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
+TRYWHY3CMO=lib/why3/why3.cma 
 
-TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
-
-trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
+trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
 
 %.fr.html: %.prehtml
 	yamlpp -l fr $< -o $@
@@ -1516,19 +1516,38 @@ trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.h
 	yamlpp -l en $< -o $@
 
 src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
-	js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
-		--file=try_alt_ergo.drv:/ \
+	js_of_ocaml --extern-fs -I . -I src/trywhy3 \
 		--file=drinkers.why:/ \
 		--file=simplearith.why:/ \
 		--file=bin_mult.mlw:/ \
 		--file=fact.mlw:/ \
 		--file=isqrt.mlw:/ \
-		`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
 		+weak.js +nat.js $^
 
-src/trywhy3/trywhy3.byte: $(TRYWHY3CMO) src/trywhy3/trywhy3.cmo
+src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
+	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
+
+
+src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
+	js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
+		--file=try_alt_ergo.drv:/ \
+		`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+	+weak.js +nat.js $^
+
+src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
+	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
+
+
+src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
+	js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $^
+
+src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
 	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
 
+src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo
+src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo
+src/trywhy3/trywhy3.cmo: src/trywhy3/worker_proto.cmo
+
 src/trywhy3/%.cmo: src/trywhy3/%.ml
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
@@ -1536,7 +1555,11 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
 clean::
-	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte
+	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
+	 src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
+         src/trywhy3/alt_ergo_worker.js src/trywhy3/alt_ergo_worker.byte src/trywhy3/alt_ergo_worker.cm* \
+         src/trywhy3/worker_proto.cm*	\
+	 src/trywhy3/index.en.html src/trywhy3/index.fr.html
 
 CLEANDIRS += src/trywhy3
 

src/trywhy3/README

@@ -7,6 +7,12 @@ Instructions to build TryWhy3
 
      git clone https://github.com/ajaxorg/ace-builds.git
 
+  ** copy the fontawesome webfont locally :
+     mkdir fontawesome
+     cd fontawesome
+     wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome.css
+     wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome-webfont.woff
+
   ** install Alt-Ergo
 
      - get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in

src/trywhy3/alt_ergo_worker.ml

+open Format
+open Worker_proto
+
+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
+
+
+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")
+
+let run_alt_ergo_on_task text =
+  let lb = Lexing.from_string text in
+(* 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] ->
+    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
+    SAT.reset_steps ();
+    let stat = ref (Invalid "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
+  | _ -> Invalid "zero or more than 1 goal to solve"
+
+
+
+
+let () =
+  Options.set_steps_bound 100;
+  Worker.set_onmessage (fun msg ->
+			let (id, text) = unmarshal msg in
+			let result = run_alt_ergo_on_task text in
+			Worker.post_message (marshal (id,result)))

src/trywhy3/index.prehtml

@@ -40,6 +40,7 @@
       </div>
     </div>
     <!-- the main page -->
+    <div id="header">
       <div align="right">
         <#fr><a href="index.en.html">English version</a></#fr>
         <#en><a href="index.fr.html">Version fran&ccedil;aise</a></#en>
@@ -72,6 +73,7 @@
           <#fr>utilis&eacute; pour produire cette page</#fr>
       </ul>
     </p>
+    </div>
     <div class="menu-bar">
       <ul>
 	<li><a href="#"><#en>File</#en><#fr>Fichier</#fr></a>
@@ -132,6 +134,10 @@
 	    <li><a href="#" id="prove">
                 <#en>Prove</#en>
                 <#fr>Prouver</#fr>
+            </a></li>
+	    	    <li><a href="#" id="stop">
+                <#en>Stop Alt-ergo</#en>
+                <#fr>Arrêter Alt-ergo</#fr>
             </a></li>
 	  </ul>
 	</li>

src/trywhy3/style.css

+@import url(fontawesome/fontawesome.css);
+
+/* fontawesome */
+[class*="fontawesome-"]:before {
+    font-family: 'FontAwesome', sans-serif;
+}
+
+
 body {
     padding:0;
     margin:0;
@@ -132,20 +140,20 @@ body {
 
 #console ul {
     list-style-type: none;
-    padding: 8px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em; */
 }
 
 #console ul ul {
     list-style-type: disc;
-    padding: 8px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em;*/
 }
 
 #console ul ul ul {
     list-style-type: none;
-    padding: 0px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em; */
 }
 
 #editor {
@@ -198,3 +206,17 @@ body {
 #confirm-dialog .btn {
     width:40%;
 }
+
+#header {
+    height: 30vh;
+
+}
+.menu-bar {
+    height: 5vh;
+}
+#editor-panel {
+    height: 65vh;
+}
+#console {
+    overflow: auto;
+}
\ No newline at end of file

src/trywhy3/why3_worker.ml

+(********************************************************************)
+(*                                                                  *)
+(*  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 ")
+
+
+
+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 =
+  Worker.post_message (marshal msg)
+
+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
+     let tasks = Task.split_theory th None None in
+     List.iter
+       (fun task ->
+	let (id,expl,_) = Termcode.goal_expl_task ~root:true task in
+        let task_name = match expl with
+          | Some s -> s
+          | None -> id.Ident.id_string
+        in
+	let task_id = gen_id () in
+	List.iter
+	  (fun vc ->
+	   let vc_id = gen_id () in
+	   let id, expl, _ = Termcode.goal_expl_task ~root:false vc in
+	   let expl = match expl with
+             | Some s -> s
+             | None -> id.Ident.id_string
+           in
+	   let msg = Tasks ((th_id, th_name),
+			    (task_id, task_name),
+			    (vc_id, expl, task_to_string vc))
+	   in
+	   send msg)
+	  (Trans.apply split_trans task)
+       ) (List.rev tasks)
+    ) 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 () =
+  
+  Worker.set_onmessage
+    (fun ev ->
+
+     log_time ("Entering why3 worker ");
+     let ev = unmarshal ev in
+     log_time ("After unmarshal ");
+     match ev with
+       Init -> ()
+     | ParseBuffer code ->
+       why3_run why3_parse_theories Env.base_language code
+     | ExecuteBuffer code ->
+	why3_run why3_execute Mlw_module.mlw_language code
+    )
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
+End:
+*)

src/trywhy3/worker_proto.ml

+type command =  ParseBuffer of string
+              | ExecuteBuffer of string
+              | Init
+
+
+type output = Error of string (* msg *)
+             | ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
+             | Tasks of ((string * string) (* Theory (id, name) *)
+                       * (string * string) (* Task (id, name *)
+                       * (string * string * string)) (* VC (id, expl, code ) *)
+             | Result of string list
+
+type prover_answer = Valid | Unknown of string | Invalid of string
+
+let marshal a =
+  Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))
+
+let unmarshal a =
+  Marshal.from_string (Scanf.unescaped (Js.to_string a)) 0
+
+
+
+let log s = ignore (Firebug.console ## log (Js.string s))
+let log_time s =
+  let date = jsnew Js.date_now () in
+  let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
+  log (date_str ^ " : " ^ s)