Commit dd2f09b9 authored by MARCHE Claude's avatar MARCHE Claude

Why3 web interface: first draft

Can be tested using

bin/why3webserver.opt & firefox src/ide/index.html
parent 38ac7eb5
......@@ -736,6 +736,53 @@ install_local:: bin/why3ide
endif
###############
# WEBSERV
###############
WEBSERV_FILES = unix_scheduler wserver why3web
WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))
WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))
$(WEBSERVDEP): DEPFLAGS += -I src/ide
$(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide
# build targets
byte: bin/why3webserver.byte
opt: bin/why3webserver.opt
bin/why3webserver.opt: lib/why3/why3.cmxa $(WEBSERVCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3webserver.byte: lib/why3/why3.cma $(WEBSERVCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WEBSERVDEP)
endif
depend: $(WEBSERVDEP)
CLEANDIRS += src/ide
clean_old_install::
rm -f $(BINDIR)/why3webserver$(EXE)
install_no_local::
$(INSTALL) bin/why3webserver.@OCAMLBEST@ $(TOOLDIR)/why3webserver$(EXE)
install_local:: bin/why3webserver
###############
# Session
###############
......
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<title>Why3</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
</head>
<body id="body" style="background-color:#e0e0a0">
<h1>Test</h1>
<p>
<button id="b1" onClick="sendRequest('bouton1');">Button 1</button>
<button id="b2" onClick="sendRequest('bouton2');">Button 2</button>
<button id="b3" onclick="startNotificationHandler()">Start notification handler</button>
<button id="b4" onclick="stopNotificationHandler()">Stop notification handler</button>
</p>
<div id="answers" style="overflow:auto">
<p>Answer zone</p>
</div>
<script type="text/javascript" src="why3ide.js"></script>
</body>
</html>
function printAnswer (s) {
var node = document.createElement("P");
var textnode = document.createTextNode(s);
node.appendChild(textnode);
document.getElementById('answers').appendChild(node);
}
function readBody(xhr) {
var data;
if (!xhr.responseType || xhr.responseType === "text") {
data = xhr.responseText;
} else if (xhr.responseType === "document") {
data = xhr.responseXML;
} else {
data = xhr.response;
}
return data;
}
function getNotification () {
var req = new XMLHttpRequest();
req.open('GET', 'http://localhost:6789/getNotifications', true);
req.onreadystatechange = function (aEvt) {
if (req.readyState == XMLHttpRequest.DONE) {
if(req.status == 200)
printAnswer("" + readBody(req));
else
printAnswer("Erreur " + req.status);
}
};
req.send(null);
}
var notifHandler = null;
function startNotificationHandler() {
if (notifHandler == null) {
notifHandler = setInterval(getNotification,1000);
}
}
function stopNotificationHandler() {
if (notifHandler != null) {
clearInterval(notifHandler);
notifHandler = null;
}
}
function sendRequest(r) {
var req = new XMLHttpRequest();
req.open('GET', 'http://localhost:6789/request?value='+r, true);
req.overrideMimeType('text/json');
req.onreadystatechange = function (aEvt) {
if (req.readyState == XMLHttpRequest.DONE) {
if(req.status == 200)
printAnswer("" + readBody(req));
else
printAnswer("Erreur " + req.status);
}
};
req.send(null);
}
open Why3
module P = struct
let notify _ = ()
let get_requests () = []
end
module S = Itp_server.Make (Unix_scheduler.Unix_scheduler) (P)
open Format
let handle_script s args =
match s with
| "request" -> "{ \"request\": \"" ^ args ^ "\" }"
| "getNotifications" ->
let n = Random.int 4 in
"{ \"kind\": \"Random\", \"value\" = \"" ^ string_of_int n ^ "\" }"
| _ -> "bad request"
let plist fmt l =
List.iter (fun x -> fprintf fmt "'%s'@\n" x) l
let string_of_addr addr =
match addr with
| Unix.ADDR_UNIX s -> s
| Unix.ADDR_INET (ie,i) ->
(Unix.string_of_inet_addr ie)^":"^string_of_int(i)
let handler (addr,req) script cont fmt =
eprintf "addr : %s@." (string_of_addr addr);
eprintf "req: @[%a@]@." plist req;
eprintf "script: `%s'@." script;
eprintf "cont: `%s'@." cont;
let ans = handle_script script cont in
Wserver.http_header fmt "HTTP/1.0 200 OK";
fprintf fmt "Access-Control-Allow-Origin: *\n";
fprintf fmt "\n"; (* end of header *)
fprintf fmt "%s" ans;
fprintf fmt "@."
let () = Wserver.main_loop None 6789 handler
open Why3.Strings
open Format
let hexa_digit x =
if x >= 10 then Char.chr (Char.code 'A' + x - 10)
else Char.chr (Char.code '0' + x)
let hexa_val conf =
match conf with
'0'..'9' -> Char.code conf - Char.code '0'
| 'a'..'f' -> Char.code conf - Char.code 'a' + 10
| 'A'..'F' -> Char.code conf - Char.code 'A' + 10
| _ -> 0
let decode s =
let rec need_decode i =
if i < String.length s then
match s.[i] with
'%' | '+' -> true
| _ -> need_decode (succ i)
else false
in
let rec compute_len i i1 =
if i < String.length s then
let i =
match s.[i] with
'%' when i + 2 < String.length s -> i + 3
| _ -> succ i
in
compute_len i (succ i1)
else i1
in
let rec copy_decode_in s1 i i1 =
if i < String.length s then
let i =
match s.[i] with
'%' when i + 2 < String.length s ->
let v = hexa_val s.[i + 1] * 16 + hexa_val s.[i + 2] in
set s1 i1 (Char.chr v); i + 3
| '+' -> set s1 i1 ' '; succ i
| x -> set s1 i1 x; succ i
in
copy_decode_in s1 i (succ i1)
else s1
in
let rec strip_heading_and_trailing_spaces s =
if String.length s > 0 then
if s.[0] == ' ' then
strip_heading_and_trailing_spaces
(String.sub s 1 (String.length s - 1))
else if s.[String.length s - 1] == ' ' then
strip_heading_and_trailing_spaces
(String.sub s 0 (String.length s - 1))
else s
else s
in
if need_decode 0 then
let len = compute_len 0 0 in
let s1 = create len in
strip_heading_and_trailing_spaces (copy_decode_in s1 0 0)
else s
let special =
function
'\000'..'\031' | '\127'..'\255' | '<' | '>' | '\"' | '#' | '%' | '{' |
'}' | '|' | '\\' | '^' | '~' | '[' | ']' | '`' | ';' | '/' | '?' | ':' |
'@' | '=' | '&' ->
true
| _ -> false
let encode s =
let rec need_code i =
if i < String.length s then
match s.[i] with
' ' -> true
| x -> if special x then true else need_code (succ i)
else false
in
let rec compute_len i i1 =
if i < String.length s then
let i1 = if special s.[i] then i1 + 3 else succ i1 in
compute_len (succ i) i1
else i1
in
let rec copy_code_in s1 i i1 =
if i < String.length s then
let i1 =
match s.[i] with
' ' -> set s1 i1 '+'; succ i1
| c ->
if special c then
begin
set s1 i1 '%';
set s1 (i1 + 1) (hexa_digit (Char.code c / 16));
set s1 (i1 + 2) (hexa_digit (Char.code c mod 16));
i1 + 3
end
else begin set s1 i1 c; succ i1 end
in
copy_code_in s1 (succ i) i1
else s1
in
if need_code 0 then
let len = compute_len 0 0 in copy_code_in (create len) 0 0
else s
let nl = "\013\010"
let http_header fmt answer =
let answer = if answer = "" then "200 OK" else answer in
fprintf fmt "HTTP/1.0 %s%s" answer nl
let print_exc exc =
match exc with
Unix.Unix_error (err, fun_name, arg) ->
prerr_string "\"";
prerr_string fun_name;
prerr_string "\" failed";
if String.length arg > 0 then
begin prerr_string " on \""; prerr_string arg; prerr_string "\"" end;
prerr_string ": ";
prerr_endline (Unix.error_message err)
| Out_of_memory -> prerr_string "Out of memory\n"
| Match_failure (file, first_char, last_char) ->
prerr_string "Pattern matching failed, file ";
prerr_string file;
prerr_string ", chars ";
prerr_int first_char;
prerr_char '-';
prerr_int last_char;
prerr_char '\n'
| Assert_failure (file, first_char, last_char) ->
prerr_string "Assertion failed, file ";
prerr_string file;
prerr_string ", chars ";
prerr_int first_char;
prerr_char '-';
prerr_int last_char;
prerr_char '\n'
| x ->
prerr_string "Uncaught exception: ";
prerr_string (Obj.magic (Obj.field (Obj.field (Obj.repr x) 0) 0));
if Obj.size (Obj.repr x) > 1 then
begin
prerr_char '(';
for i = 1 to Obj.size (Obj.repr x) - 1 do
if i > 1 then prerr_string ", ";
let arg = Obj.field (Obj.repr x) i in
if not (Obj.is_block arg) then prerr_int (Obj.magic arg : int)
else if Obj.tag arg = 252 then
begin
prerr_char '\"';
prerr_string (Obj.magic arg : string);
prerr_char '\"'
end
else prerr_char '_'
done;
prerr_char ')'
end;
prerr_char '\n'
let print_err_exc exc = print_exc exc; flush stderr
let case_unsensitive_eq s1 s2 = lowercase s1 = lowercase s2
let rec extract_param name stop_char =
function
x :: l ->
if String.length x >= String.length name &&
case_unsensitive_eq (String.sub x 0 (String.length name)) name
then
let i =
let rec loop i =
if i = String.length x then i
else if x.[i] = stop_char then i
else loop (i + 1)
in
loop (String.length name)
in
String.sub x (String.length name) (i - String.length name)
else extract_param name stop_char l
| [] -> ""
let buff = ref (create 80)
let store len x =
if len >= String.length !buff then
buff := !buff ^ create (String.length !buff);
set !buff len x;
succ len
let get_buff len = String.sub !buff 0 len
let get_request strm =
let rec loop len (strm__ : _ Stream.t) =
match Stream.peek strm__ with
Some '\010' ->
Stream.junk strm__;
let s = strm__ in
if len == 0 then [] else let str = get_buff len in str :: loop 0 s
| Some '\013' -> Stream.junk strm__; loop len strm__
| Some c -> Stream.junk strm__; loop (store len c) strm__
| _ -> if len == 0 then [] else [get_buff len]
in
loop 0 strm
let get_request_and_content strm =
let request = get_request strm in
let content =
match extract_param "content-length: " ' ' request with
"" -> ""
| x ->
let str = create (int_of_string x) in
for i = 0 to String.length str - 1 do
set str i (
let (strm__ : _ Stream.t) = strm in
match Stream.peek strm__ with
Some x -> Stream.junk strm__; x
| _ -> ' ')
done;
str
in
request, content
let string_of_sockaddr =
function
Unix.ADDR_UNIX s -> s
| Unix.ADDR_INET (a, _) -> Unix.string_of_inet_addr a
let sockaddr_of_string s = Unix.ADDR_UNIX s
let treat_connection _tmout callback addr fd fmt =
let (request, contents__) =
let strm =
let c = " " in
Stream.from
(fun _ -> if Unix.read fd c 0 1 = 1 then Some c.[0] else None)
in
get_request_and_content strm
in
let (script_name, contents__) =
match extract_param "GET /" ' ' request with
"" -> extract_param "POST /" ' ' request, contents__
| str ->
try
let i = String.index str '?' in
String.sub str 0 i,
String.sub str (i + 1) (String.length str - i - 1)
with
Not_found -> str, ""
in
if script_name = "robots.txt" then
begin
http_header fmt "";
fprintf fmt "Content-type: text/plain%s%s" nl nl;
fprintf fmt "User-Agent: *%s" nl;
fprintf fmt "Disallow: /%s@." nl;
eprintf "Robot request@."
end
else
begin try callback (addr, request) script_name contents__ fmt with
| Unix.Unix_error (Unix.EPIPE, "write", _) -> ()
| exc -> print_err_exc exc
end
let accept_connection delay callback s =
let (a,_,_) = Unix.select [s] [] [] delay in
match a with
| [] ->
begin
Printf.eprintf "No connection. Compacting... ";
flush stderr;
Gc.compact ();
Printf.eprintf "Ok\n";
flush stderr
end
| [a] ->
assert (a == s);
let (t, addr) = Unix.accept s in
Unix.setsockopt t Unix.SO_KEEPALIVE true;
let cleanup () =
begin try Unix.shutdown t Unix.SHUTDOWN_SEND with
_ -> ()
end;
begin try Unix.shutdown t Unix.SHUTDOWN_RECEIVE with
_ -> ()
end;
try Unix.close t with
_ -> ()
in
let oc = Unix.out_channel_of_descr t in
treat_connection delay callback addr t (formatter_of_out_channel oc);
close_out oc;
cleanup ()
| _ -> assert false
(* the private list of functions to call on idle, sorted higher
priority first. *)
let idle_handler : (int * (unit -> bool)) list ref = ref []
(* [insert_idle_handler p f] inserts [f] as a new function to call
on idle, with priority [p] *)
let insert_idle_handler p f =
let rec aux l =
match l with
| [] -> [p,f]
| (p1,_) as hd :: rem ->
if p > p1 then (p,f) :: l else hd :: aux rem
in
idle_handler := aux !idle_handler
(* the private list of functions to call on timeout, sorted on
earliest trigger time first. *)
let timeout_handler : (float * float * (unit -> bool)) list ref = ref []
(* [insert_timeout_handler ms t f] inserts [f] as a new function to call
on timeout, with time step of [ms] and first call time as [t] *)
let insert_timeout_handler ms t f =
let rec aux l =
match l with
| [] -> [ms,t,f]
| (_,t1,_) as hd :: rem ->
if t < t1 then (ms,t,f) :: l else hd :: aux rem
in
timeout_handler := aux !timeout_handler
(* public function to register a task to run on idle *)
let idle ~(prio:int) f = insert_idle_handler prio f
(* public function to register a task to run on timeout *)
let timeout ~ms f =
assert (ms > 0);
let ms = float ms /. 1000.0 in
let time = Unix.gettimeofday () in
insert_timeout_handler ms (time +. ms) f
let main_loop addr_opt port g =
let addr =
match addr_opt with
Some addr ->
begin try Unix.inet_addr_of_string addr with
Failure _ -> (Unix.gethostbyname addr).Unix.h_addr_list.(0)
end
| None -> Unix.inet_addr_any
in
let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in
Unix.setsockopt s Unix.SO_REUSEADDR true;
Unix.bind s (Unix.ADDR_INET (addr, port));
Unix.listen s 4;
Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
let tm = Unix.localtime (Unix.time ()) in
Printf.eprintf "Ready %4d-%02d-%02d %02d:%02d port"
(1900 + tm.Unix.tm_year) (succ tm.Unix.tm_mon) tm.Unix.tm_mday
tm.Unix.tm_hour tm.Unix.tm_min;
Printf.eprintf " %d" port;
Printf.eprintf "...\n";
flush stderr;
while true do
(* attempt to run the first timeout handler *)
let time = Unix.gettimeofday () in
match !timeout_handler with
| (ms,t,f) :: rem when t <= time ->
timeout_handler := rem;
let b = f () in
let time = Unix.gettimeofday () in
if b then insert_timeout_handler ms (ms +. time) f
| _ ->
(* time is not yet passed *)
(* attempt to run the first idle handler *)
match !idle_handler with
| (p,f) :: rem ->
idle_handler := rem;
let b = f () in
if b then insert_idle_handler p f
| [] ->
(* no idle handler *)
(* check connection for a some delay *)
let delay =
match !timeout_handler with
| [] -> 0.125
(* 1/8 second by default *)
| (_,t,_) :: _ -> t -. time
(* or the time left until the next timeout otherwise *)
in
begin
try accept_connection delay g s
with
Unix.Unix_error (Unix.ECONNRESET, "accept", _) -> ()
| Unix.Unix_error ((Unix.EBADF | Unix.ENOTSOCK), "accept", _) as x ->
raise x
| exc -> print_err_exc exc
end;
flush stderr
done
val main_loop : string option -> int ->
(Unix.sockaddr * string list -> string -> string -> Format.formatter -> unit) -> unit
(** [main_loop addr port g] starts an elementary httpd server at port
[port] in the current machine. The variable [addr] is [Some
the-address-to-use] or [None] for any of the available addresses
of the present machine. The port number is any number greater than
1024 (to create a client < 1024, you must be root). At each
connection, the function [g] is called: [g (addr, request) scr
cont fmt] where [addr] is the client identification socket,
[request] the browser request, [scr] the script name (extracted
from [request]) and [cont] the stdin contents. [fmt] is the
formatter where the answer should be written. It must start by a
call to [http_header] below. *)
val timeout: ms:int -> (unit -> bool) -> unit
(** [timeout ~ms f] registers the function [f] as a function to be
called every [ms] milliseconds. The function is called repeatedly
until it returns false. the [ms] delay is not strictly guaranteed:
it is only a minimum delay between the end of the last call and
the beginning of the next call. Several functions can be
registered at the same time. *)
val idle: prio:int -> (unit -> bool) -> unit
(** [idle prio f] registers the function [f] as a function to be
called whenever there is nothing else to do. Several functions can
be registered at the same time. Several functions can be
registered at the same time. Functions registered with higher