Commit 98f2682f authored by Johannes Kanig's avatar Johannes Kanig

Committing why3server code

For the moment, new API functions are introduced. If existing API
functions are called, the why3server is not used.
parent 281da180
......@@ -160,7 +160,7 @@ LIB_UTIL = config bigInt util opt lists strings \
LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
......@@ -236,6 +236,10 @@ src/session/compress.ml: config.status src/session/compress_none.ml
cp src/session/compress_none.ml $@
endif
src/driver/vc_client.o: src/driver/vc_client.c
ocamlopt -c $^
mv $(CURDIR)/vc_client.o $@
# hide deprecated warnings for strings
src/util/strings.cmo:: WARNINGS:=$(WARNINGS)-3
......@@ -246,11 +250,11 @@ src/util/strings.cmx:: WARNINGS:=$(WARNINGS)-3
byte: lib/why3/why3.cma
opt: lib/why3/why3.cmxa
lib/why3/why3.cma: lib/why3/why3.cmo
lib/why3/why3.cma: lib/why3/why3.cmo src/driver/vc_client.o
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3.cmxa: lib/why3/why3.cmx
lib/why3/why3.cmxa: lib/why3/why3.cmx src/driver/vc_client.o
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
......@@ -555,6 +559,7 @@ clean_old_install::
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3server$(EXE) $(BINDIR)/why3$(EXE)
cp -f bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE)
cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
......@@ -610,6 +615,51 @@ clean::
%.type: %.mlw bin/why3ide.opt
bin/why3.opt --type-only $*.mlw
##############
# Why3server #
##############
SERVER_MODULES:= logging arraylist options queue readbuf request writebuf server_main
SERVER_C:= $(addprefix src/tools/, $(addsuffix .c, $(SERVER_MODULES)))
SERVER_H:= $(addprefix src/tools/, $(addsuffix .h, $(SERVER_MODULES)))
SERVER_O:= $(addprefix src/tools/, $(addsuffix .o, $(SERVER_MODULES)))
opt: bin/why3server$(EXE)
bin/why3server$(EXE): $(SERVER_O)
gcc -o $@ $^
%.o: %.c %.h
gcc -c -Wall -g -o $@ $<
%.o: %.c
gcc -c -Wall -g -o $@ $<
src/tools/main.o:: src/tools/server-unix.c src/tools/server-win.c
install_no_local::
cp -f bin/why3server$(EXE) $(BINDIR)/why3server$(EXE)
clean::
rm -f $(SERVER_O)
install_spark2014:
mkdir -p $(BINDIR)
mkdir -p $(DATADIR)/why3
mkdir -p $(DATADIR)/why3/theories
mkdir -p $(DATADIR)/why3/drivers
mkdir -p $(DATADIR)/why3/modules
mkdir -p $(DATADIR)/why3/libs
cp -f theories/*.why $(DATADIR)/why3/theories
cp -f modules/*.mlw $(DATADIR)/why3/modules
cp -f drivers/*.drv drivers/*.gen drivers/*.aux $(DATADIR)/why3/drivers
cp -f share/why3session.dtd $(DATADIR)/why3
cp -f bin/why3server$(EXE) $(BINDIR)/why3server$(EXE)
cp -f bin/gnatwhy3.@OCAMLBEST@ $(BINDIR)/gnatwhy3$(EXE)
cp -f bin/why3realize.@OCAMLBEST@ $(BINDIR)/why3realize$(EXE)
cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
cp -f share/provers-detection-data.conf $(DATADIR)/why3/
cp -rf lib/coq $(DATADIR)/why3/libs
##########
# gallery
##########
......
......@@ -372,3 +372,76 @@ let wait_on_call pc =
let post_wait_call pc ret = pc.call ret
let prover_call_pid pc = pc.pid
let set_socket_name =
Prove_client.set_socket_name
type server_id = int
let gen_id =
let x = ref 0 in
fun () ->
incr x;
!x
type save_data =
{ vc_file : string;
is_temporary : bool;
limit : resource_limit;
res_parser : prover_result_parser;
printer_mapping : Printer.printer_mapping;
}
let regexs : (int, save_data) Hashtbl.t = Hashtbl.create 17
let prove_file_server ~res_parser ~command ~limit
~printer_mapping ?(inplace=false) ?(interactive=false) file =
let id = gen_id () in
let cmd, _, _ = actualcommand command ~use_why3cpulimit:false limit interactive file in
let saved_data =
{ vc_file = file;
is_temporary = not inplace;
limit = limit;
res_parser = res_parser;
printer_mapping = printer_mapping } in
Hashtbl.add regexs id saved_data;
let timelimit = get_time limit in
let memlimit = get_mem limit in
Prove_client.send_request ~id ~timelimit ~memlimit ~cmd;
id
let read_and_delete_file fn =
let cin = open_in fn in
let buf = Buffer.create 1024 in
try
while true do
Buffer.add_string buf (input_line cin);
Buffer.add_char buf '\n'
done;
assert false
with End_of_file ->
begin
close_in cin;
Sys.remove fn;
Buffer.contents buf
end
let handle_answer answer =
let id = answer.Prove_client.id in
let save = Hashtbl.find regexs id in
Hashtbl.remove regexs id;
if save.is_temporary then
Sys.remove save.vc_file;
let out = read_and_delete_file answer.Prove_client.out_file in
let ret = Unix.WEXITED answer.Prove_client.exit_code in
let printer_mapping = save.printer_mapping in
let ans =
parse_prover_run save.res_parser
answer.Prove_client.time
out ret answer.Prove_client.timeout save.limit
~printer_mapping
in
id, ans
let wait_for_server_result () =
List.map handle_answer (Prove_client.read_answers ())
......@@ -188,3 +188,18 @@ val post_wait_call : prover_call -> Unix.process_status -> post_prover_call
val prover_call_pid : prover_call -> int
(** Return the pid of the prover *)
val set_socket_name : string -> unit
type server_id = int
val prove_file_server :
res_parser : prover_result_parser ->
command : string ->
limit : resource_limit ->
printer_mapping : Printer.printer_mapping ->
?inplace : bool ->
?interactive : bool ->
string -> server_id
val wait_for_server_result : unit -> (server_id * prover_result) list
......@@ -257,7 +257,6 @@ let call_on_buffer ~command ~limit
~command ~limit ~res_parser:drv.drv_res_parser
~filename ~printer_mapping ?inplace ?interactive buffer
(** print'n'prove *)
exception NoPrinter
......@@ -323,14 +322,8 @@ let print_theory ?old drv fmt th =
let task = Task.use_export None th in
print_task ?old drv fmt task
let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let old_channel = Opt.map open_in old in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
pp_print_flush fmt ();
Opt.iter close_in old_channel;
let filename = match old, inplace with
let file_name_of_task ?old ?inplace drv task =
match old, inplace with
| Some fn, Some true -> fn
| _ ->
let pr = Task.task_goal task in
......@@ -339,7 +332,15 @@ let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
| None -> "" in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
get_filename drv fn "T" pr.pr_name.id_string
in
let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let old_channel = Opt.map open_in old in
let filename = file_name_of_task ?old ?inplace drv task in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
pp_print_flush fmt ();
Opt.iter close_in old_channel;
let res =
call_on_buffer ~command ~limit
?inplace ?interactive ~filename ~printer_mapping drv buf in
......@@ -351,6 +352,21 @@ let prove_task ~command ~limit ?(cntexample=false) ?old
let task = prepare_task ~cntexample drv task in
prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task
let prove_task_server command ~limit ~cntexample ?old ?inplace drv task =
let task = prepare_task ~cntexample drv task in
let fn = file_name_of_task ?old ?inplace drv task in
let res_parser = drv.drv_res_parser in
let printer_mapping = get_default_printer_mapping in
match inplace with
| Some true ->
prove_file_server ~command ~res_parser ~limit ~printer_mapping ?inplace fn
| _ -> let fn, outc = Filename.open_temp_file "why_" ("_" ^ fn) in
let fmt = Format.formatter_of_out_channel outc in
let printer_mapping = print_task_prepared ?old:None drv fmt task in
close_out outc;
prove_file_server ~command ~res_parser ~limit ~printer_mapping fn
(* exception report *)
let string_of_qualid thl idl =
......
......@@ -70,6 +70,12 @@ val print_task_prepared :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> Printer.printer_mapping
val prove_task_server : string ->
limit : Call_provers.resource_limit ->
cntexample:bool ->
?old:string -> ?inplace:bool -> driver -> Task.task ->
Call_provers.server_id
val prove_task_prepared :
command : string ->
limit : Call_provers.resource_limit ->
......
external client_connect : string -> unit = "c_client_connect"
external client_disconnect : unit -> unit = "c_client_disconnect"
external send_request_string : string -> unit = "c_send_request_string"
external read_from_client : unit -> string = "c_read_from_client"
type answer =
{
id : int;
exit_code : int;
time : float;
timeout : bool;
out_file : string;
}
let socket_name : string ref = ref ""
let set_socket_name s =
socket_name := s
let buf : Buffer.t = Buffer.create 1024
let connect () =
Buffer.clear buf;
client_connect !socket_name
let disconnect () =
client_disconnect ()
let send_request ~id ~timelimit ~memlimit ~cmd =
let buf = Buffer.create 128 in
Buffer.add_string buf (string_of_int id);
Buffer.add_char buf ';';
Buffer.add_string buf (string_of_int timelimit);
Buffer.add_char buf ';';
Buffer.add_string buf (string_of_int memlimit);
List.iter (fun x ->
Buffer.add_char buf ';';
Buffer.add_string buf x)
cmd;
Buffer.add_char buf '\n';
let s = Buffer.contents buf in
send_request_string s
let rec read_lines () =
let s = read_from_client () in
if String.contains s '\n' then begin
let s = Buffer.contents buf ^ s in
Buffer.clear buf;
let l = Strings.rev_split '\n' s in
match l with
| [] -> assert false
| [x] -> [x]
| (x::xs) as l ->
if x = "" then List.rev xs else
if x.[String.length x - 1] = '\n' then List.rev l
else begin
Buffer.add_string buf x;
List.rev xs
end
end else begin
Buffer.add_string buf s;
read_lines ()
end
let bool_of_timeout_string s =
if s = "1" then true else false
let read_answer s =
let l = Strings.split ';' s in
match l with
| id :: exit_s :: time_s :: timeout_s :: ( (_ :: _) as rest) ->
(* same trick we use in other parsing code. The file name may contain
';'. Luckily, the file name comes last, so we still split on ';', and
put the pieces back together afterwards *)
let out_file = Strings.join ";" rest in
{ id = int_of_string id;
out_file = out_file;
time = float_of_string time_s;
exit_code = int_of_string exit_s;
timeout = bool_of_timeout_string timeout_s;
}
|_ ->
assert false
let read_answers () =
List.map read_answer (List.filter (fun x -> x <> "") (read_lines ()))
val set_socket_name : string -> unit
val connect : unit -> unit
val send_request :
id:int ->
timelimit:int ->
memlimit:int ->
cmd:string list->
unit
type answer =
{
id : int;
exit_code : int;
time : float;
timeout : bool;
out_file : string;
}
val read_answers : unit -> answer list
val disconnect : unit -> unit
#ifdef _WIN32
# include <windows.h>
#else
# include <sys/socket.h>
# include <sys/types.h>
# include <sys/un.h>
# include <unistd.h>
# include <errno.h>
#endif
#include <caml/mlvalues.h>
#include <caml/alloc.h>
#include <caml/memory.h>
#include <assert.h>
#include <stdio.h>
#ifdef _WIN32
HANDLE pipe;
CAMLprim value c_client_connect(value v) {
CAMLparam1(v);
char *basename;
char *socket_name;
unsigned namelen;
basename = String_val(v);
namelen = caml_string_length(v);
socket_name = (char*) malloc(sizeof(char) * (namelen + 10));
strcpy(socket_name, TEXT("\\\\.\\pipe\\"));
strcat(socket_name, basename);
pipe = CreateFile(
socket_name, // pipe name
GENERIC_READ | // read and write access
GENERIC_WRITE,
0, // no sharing
NULL, // default security attributes
OPEN_EXISTING, // opens existing pipe
0, // default attributes
NULL);
CAMLreturn(Val_unit);
}
CAMLprim value c_client_disconnect(value unit) {
CAMLparam1(unit);
CloseHandle(pipe);
CAMLreturn(Val_unit);
}
CAMLprim value c_send_request_string(value v) {
CAMLparam1(v);
char *msg;
int to_write, pointer;
DWORD written;
BOOL res;
msg = String_val(v);
to_write = caml_string_length(v);
pointer = 0;
while (pointer < to_write) {
res = WriteFile(
pipe, // pipe handle
msg+pointer, // message
to_write-pointer, // message length
&written, // bytes written
NULL);
pointer += written;
}
CAMLreturn(Val_unit);
}
CAMLprim value c_read_from_client(value unit) {
CAMLparam1(unit);
DWORD read;
char buf[1024];
CAMLlocal1( ml_data );
ReadFile(pipe, buf, 1024, &read, NULL);
ml_data = caml_alloc_string(read);
memcpy(String_val(ml_data), buf, read);
CAMLreturn(ml_data);
}
#else
int client_sock;
CAMLprim value c_client_connect(value v) {
CAMLparam1(v);
struct sockaddr_un addr;
int res;
unsigned namelen = caml_string_length(v);
addr.sun_family = AF_UNIX;
memcpy(addr.sun_path, String_val(v), namelen + 1);
client_sock = socket(AF_UNIX, SOCK_STREAM, 0);
res = connect(client_sock, (struct sockaddr*) &addr, sizeof(struct sockaddr_un));
if (res == -1) {
printf("connection failed : %d\n", errno);
exit(1);
}
CAMLreturn(Val_unit);
}
CAMLprim value c_client_disconnect(value unit) {
CAMLparam1(unit);
close(client_sock);
CAMLreturn(Val_unit);
}
CAMLprim value c_send_request_string(value v) {
CAMLparam1(v);
char *msg;
ssize_t to_write, pointer;
ssize_t res;
msg = String_val(v);
to_write = caml_string_length(v);
pointer = 0;
while (pointer < to_write) {
res = write(client_sock, msg + pointer, to_write - pointer);
if (res == -1) {
break;
}
pointer += res;
}
CAMLreturn(Val_unit);
}
CAMLprim value c_read_from_client(value unit) {
CAMLparam1(unit);
ssize_t have_read;
char buf[1024];
CAMLlocal1( ml_data );
have_read = read(client_sock, buf, 1024);
ml_data = caml_alloc_string(have_read);
memcpy(String_val(ml_data), buf, have_read);
CAMLreturn(ml_data);
}
#endif
#include <assert.h>
#include <stdlib.h>
#include "arraylist.h"
#define INVALID_INDEX (-1)
int list_lookup_index(plist l, int key);
void list_resize(plist l);
plist init_list(int capacity) {
plist result;
result = (plist) malloc (sizeof(t_list));
result->capacity = capacity;
result->len = 0;
result->key = (int*) malloc(sizeof(int) * capacity);
result->data = (void**) malloc(sizeof(void*) * capacity);
return result;
}
bool list_is_empty(plist l) {
return (l->len == 0);
}
int list_lookup_index(plist l, int key) {
int i;
for (i = 0; i < l->len; i++) {
if (l->key[i] == key) {
return i;
}
}
return INVALID_INDEX;
}
void* list_lookup(plist l, int key) {
int i = list_lookup_index(l, key);
if (i == INVALID_INDEX) {
return NULL;
} else {
return l->data[i];
}
}
void list_remove(plist l, int key) {
int i = list_lookup_index(l, key);
if (i != INVALID_INDEX) {
assert (!list_is_empty(l));
l->len--;
l->key[i] = l->key[l->len];
l->data[i] = l->data[l->len];
}
}
void free_list(plist l) {
assert (list_is_empty(l));
free(l->data);
free(l->key);
free(l);
}
void list_resize(plist l) {
int newcap = l->capacity * 2;
l->capacity = newcap;
l->key = (int*) realloc(l->key, sizeof(int) * newcap);
l->data = (void**) realloc(l->data, sizeof(void*) * newcap);
}
void list_append(plist l, int key, void* elt) {
if (l->len == l->capacity) {
list_resize(l);
}
l->key[l->len] = key;
l->data[l->len] = elt;
l->len++;
}
int list_length(plist l) {
return l->len;
}
#ifndef ARRAYLIST_H
#define ARRAYLIST_H
#include <stdbool.h>
// A simple list implementation based on a resizable array. The list has a
// field "key" which allows to lookup certain members by this key.
typedef struct {
int* key; // the key data, as an array
void** data; // the actual list data, as an array
int len; // the number of elements in the list
int capacity; // the capacity of the arrays key and data
} t_list, *plist;
// The idea is that each element in the list is a tuple (key, data), but it is
// simpler to hahve two separate arrays for that
// return a list of initial capacity <capacity>
plist init_list(int capacity);
// add a new element <elt> to the list <l>, with <key>. The array will
// automatically grow if more space is needed.
void list_append(plist l, int key, void* elt);
// return true if the list is empty, false otherwise
bool list_is_empty(plist l);
// return the number of elements in the list
int list_length(plist l);
// remove the element in the list whose key is equal to <key>. If no such data
// exists, do nothing.
void list_remove(plist l, int key);
// Return the data whose key is equal to <key>. Return NULL if no such data
// exists.
void* list_lookup(plist l, int key);
// free storage associated with the list. The list must be empty when freeing
// it.
void free_list(plist l);
#endif
#include <stdio.h>
#include <stdlib.h>
#include "logging.h"
FILE* logfile;
void init_logging() {
logfile = fopen("why3server.log", "w");
}
void log_msg(char* s) {
fprintf (logfile, "%s\n", s);
}
void logging_shutdown(char* s) {
log_msg(s);
fclose(logfile);
exit(1);
}
#ifndef LOGGING_H
#define LOGGING_H
void init_logging();
void log_msg(char* s);
void logging_shutdown(char* s);
#endif
#include <getopt.h>
#include <stdio.h>
#include <stdlib.h>
#include <errno.h>
#include "options.h"
int parallel = 1;
char* basename = NULL;
void parse_options(int argc, char **argv) {
static struct option long_options[] = {
/* These options set a flag. */
{"socket", required_argument, 0, 's'},
{0, 0, 0, 0}
};
while (1) {
int option_index = 0;
char c = 0;
c = getopt_long (argc, argv, "j:s:",
long_options, &option_index);
/* Detect the end of the options. */
if (c == -1) break;
switch (c) {
case 0:
/* The case where a long option has been detected for --socket should
be handled like the short option, as a NULL value was given for the
corresponding flag in long_options. */
exit (1);
case 'j':
errno = 0;
parallel = strtol(optarg, NULL, 10);
if (errno == EINVAL) {
printf("-j requires a number\n");
exit(1);
}
if (parallel <= 0 ) {
printf("-j requires a positive number\n");
exit(1);
}
break;
case 's':
basename = optarg;
break;
case '?':
/* getopt_long already printed an error message. */
exit (1);
default:
exit (1);
}
}
if (optind < argc) {
printf("extra arguments, stopping\n");
exit(1);
}
if (basename == NULL) {
printf("need to specify a socket name using --socket\n");
exit(1);