Skip to content

GitLab

Commit 0bd8a2b7 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Revert "Committing why3server code" 

This reverts commit 98f2682f.
parent c8fb4533
Show whitespace changes
Inline Side-by-side
Showing with 13 additions and 2303 deletions
Makefile.in
View file @ 0bd8a2b7
......@@ -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 = prove_client call_provers driver_ast driver_parser driver_lexer driver \
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
......@@ -236,10 +236,6 @@ 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
......@@ -250,11 +246,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 src/driver/vc_client.o
lib/why3/why3.cma: lib/why3/why3.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3.cmxa: lib/why3/why3.cmx src/driver/vc_client.o
lib/why3/why3.cmxa: lib/why3/why3.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
......@@ -559,7 +555,6 @@ 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)
......@@ -615,51 +610,6 @@ 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
##########
......
src/driver/call_provers.ml
View file @ 0bd8a2b7
......@@ -372,76 +372,3 @@ 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 ())
src/driver/call_provers.mli
View file @ 0bd8a2b7
......@@ -188,18 +188,3 @@ 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
src/driver/driver.ml
View file @ 0bd8a2b7
......@@ -257,6 +257,7 @@ 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
......@@ -322,8 +323,14 @@ let print_theory ?old drv fmt th =
let task = Task.use_export None th in
print_task ?old drv fmt task
let file_name_of_task ?old ?inplace drv task =
match old, inplace with
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
| Some fn, Some true -> fn
| _ ->
let pr = Task.task_goal task in
......@@ -332,15 +339,7 @@ let file_name_of_task ?old ?inplace 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
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;
in
let res =
call_on_buffer ~command ~limit
?inplace ?interactive ~filename ~printer_mapping drv buf in
......@@ -352,21 +351,6 @@ 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 =
......
src/driver/driver.mli
View file @ 0bd8a2b7
......@@ -70,12 +70,6 @@ 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 ->
......
src/driver/prove_client.ml deleted 100644 → 0
View file @ c8fb4533
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 ()))
src/driver/prove_client.mli deleted 100644 → 0
View file @ c8fb4533
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
src/driver/vc_client.c deleted 100644 → 0
View file @ c8fb4533
#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
src/tools/arraylist.c deleted 100644 → 0
View file @ c8fb4533
#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;
}
src/tools/arraylist.h deleted 100644 → 0
View file @ c8fb4533
#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);