Commit ec36a6ec authored by Johannes Kanig's avatar Johannes Kanig

Recommitting why3 server code because merge removed it

parent a69c569a
......@@ -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,13 +236,10 @@ src/session/compress.ml: config.status src/session/compress_none.ml
cp src/session/compress_none.ml $@
endif
<<<<<<< HEAD
src/driver/vc_client.o: src/driver/vc_client.c
gcc -O -mms-bitfields -Wall -Wno-unused -c -I$(OCAMLLIB) -fPIC $^
mv $(CURDIR)/vc_client.o $@
=======
>>>>>>> lri-master
# hide deprecated warnings for strings
src/util/strings.cmo:: WARNINGS:=$(WARNINGS)-3
......@@ -253,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 $@ $^
......@@ -562,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)
......@@ -617,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) {