Commit 2d310952 authored by Sylvain Dailler's avatar Sylvain Dailler

Merge cherrypicked commits from Adacore and new_ide

This reduces the differences between why3server of Adacore (which is known
to be working on Windows) and why3server of Why3.

Recovered src/driver/prove_client.ml whose version from Adacore is not
suitable on Why3 side.
parents 30ed0224 9f61968f
......@@ -160,6 +160,8 @@ fi
fi
AC_PROG_CC
# Add compatibility for C99
AC_PROG_CC_STDC
AC_PROG_MKDIR_P
AC_PROG_INSTALL
......
......@@ -109,11 +109,20 @@ let connect_internal () =
Filename.temp_file "why3server" "sock"
in
let exec = Filename.concat Config.libdir "why3server" in
let pid = Unix.create_process exec
let pid =
(* use this version for debugging the C code
Unix.create_process "valgrind"
[|"/usr/bin/valgrind";exec; "--socket"; socket_name;
"--single-client";
"-j"; string_of_int !max_running_provers|]
Unix.stdin Unix.stdout Unix.stderr
*)
Unix.create_process exec
[|exec; "--socket"; socket_name;
"--single-client";
"-j"; string_of_int !max_running_provers|]
Unix.stdin Unix.stdout Unix.stderr in
Unix.stdin Unix.stdout Unix.stderr
in
Unix.chdir cwd;
(* sleep before connecting, or the server will not be ready yet *)
let rec try_connect n d =
......
This is a VC server for Why3. It implements the following functionalities:
* wait for connections on a unix domain socket (unix) or named pipe
(windows) for clients
* clients can send requests for a process to spawn, including
timeout/memory limit
* server will send back a filename containing the output of the process,
as well as the time taken and the exit code
timeout/memory limit. To process is not spawned immediately but put
in a queue od processes to be spawned. Process are spawned in
parallel up to some maximal number.
* when a process is spawned, server sends a message to the client of the form 'S;id' to inform it that process 'id' has started.
* when the process is terminated, either normally or by a ressource
limit reached, server sends back a detailed message containing the
output of the process, as well as the time taken and the exit code
* clients can also request to change the maximal number of process
that can run in parallel
* clients can also request to interrupt a process, killing it if it
already runs
Command line options
====================
......@@ -20,8 +35,11 @@ A client request is a single line which looks like this:
commandkind;payload
Where commandkind is a simple string and payload is a semicolon-separated
list. There are currently three possible commands. The first command looks
like this:
list. There are currently four possible commands.
1 Running a process
The first command looks like this:
run;id;timeout;memlimit;cmd;arg1;arg2;...;argn
......@@ -59,6 +77,8 @@ Their meaning is the following:
file - the path to a file which contains the stdout and stderr of the
executed program
2 Running a process on sdtin
The second command is very similar:
runstdin;id;timeout;memlimit;cmd;arg1;arg2;...;argn;filename
......@@ -68,6 +88,8 @@ difference that an extra filename is given as the last argument to the
command. This filename is not passed to the command as a commandline argument,
instead it is "piped" into the stdin of the command.
3 Changing the maximal number of processes run in parallel
The third commmand is like this:
parallel;num
......@@ -77,6 +99,14 @@ When this command is received, the server will allow to run up to 'num'
processes in parallel from now on. Later 'parallel' commands can increase or
decrease this number. There is no server answer to this command.
4 Interrupt a process
interrupt;id
will stop the process of the given id, killing it if it was already running
== notes ==
There are two separate implementations on linux and windows, but both are
very similar in structure and share some code (but should share much more).
They are both essentially a single-threaded event loop, where the possible
......
......@@ -33,8 +33,7 @@ bool list_is_empty(plist l) {
}
int list_lookup_index(plist l, int key) {
int i;
for (i = 0; i < l->len; i++) {
for (int i = 0; i < l->len; i++) {
if (l->key[i] == key) {
return i;
}
......
......@@ -24,7 +24,7 @@ typedef struct {
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
// simpler to have two separate arrays for that
// return a list of initial capacity <capacity>
plist init_list(int capacity);
......
......@@ -16,7 +16,8 @@
#include "options.h"
int parallel = 1;
char* basename = NULL;
/* global data doesn't need null initialization, so none provided here */
char* socketname;
bool logging = false;
bool single_client = false;
......@@ -65,7 +66,7 @@ void parse_options(int argc, char **argv) {
break;
case 's':
basename = optarg;
socketname = optarg;
break;
case '?':
......@@ -77,12 +78,11 @@ void parse_options(int argc, char **argv) {
}
}
if (optind < argc) {
printf("extra arguments, stopping\n");
printf("extra arguments, stopping [opt_index=%d,argc=%d]\n",optind,argc);
exit(1);
}
if (basename == NULL) {
if (socketname == NULL) {
printf("need to specify a socket name using --socket\n");
exit(1);
}
}
......@@ -14,9 +14,13 @@
#include <stdbool.h>
// how many processes are allowed to run in parallel
extern int parallel;
extern char* basename;
// the name of the socket (path)
extern char* socketname;
// enable or disable logging
extern bool logging;
// start in single client mode
extern bool single_client;
//parse command line options and set the variables <basename> and <parallel>
......
......@@ -29,8 +29,7 @@ int copy_up_to_semicolon(char* buf, int begin, int len, char** result);
int count_semicolons(char* buf, int len) {
int cnt = 0;
int i = 0;
for (i = 0; i < len; i++) {
for (int i = 0; i < len; i++) {
if (buf[i] == ';') {
cnt++;
}
......@@ -57,7 +56,6 @@ int copy_up_to_semicolon(char* buf, int begin, int len, char** result) {
prequest parse_request(char* str_req, int len, int key) {
int numargs, semic, parallel_arg;
int i = 0;
int pos = 0;
prequest req;
char* tmp;
......@@ -70,8 +68,8 @@ prequest parse_request(char* str_req, int len, int key) {
if (semic == 0) {
return NULL;
}
// might be a 'parallel' command
if (semic == 1) {
// might be a 'parallel' or a 'interrupt' command
pos = copy_up_to_semicolon (str_req, pos, len, &tmp);
if (strncmp(tmp, "parallel", pos) == 0) {
free(tmp);
......@@ -81,6 +79,14 @@ prequest parse_request(char* str_req, int len, int key) {
parallel = parallel_arg;
}
}
else if (strncmp(tmp, "interrupt", pos) == 0) {
free(tmp);
req = (prequest) malloc(sizeof(request));
req->key = key;
req->req_type = REQ_INTERRUPT;
pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
return req;
}
free(tmp);
return NULL;
}
......@@ -101,6 +107,7 @@ prequest parse_request(char* str_req, int len, int key) {
free(tmp);
req = (prequest) malloc(sizeof(request));
req->key = key;
req->req_type = REQ_RUN;
req->numargs = numargs;
req->usestdin = runstdin;
pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
......@@ -112,17 +119,16 @@ prequest parse_request(char* str_req, int len, int key) {
free(tmp);
pos = copy_up_to_semicolon(str_req, pos, len, &(req->cmd));
req->args = (char**)malloc(sizeof(char*) * (numargs));
for (i = 0; i < numargs; i++) {
for (int i = 0; i < numargs; i++) {
pos = copy_up_to_semicolon(str_req, pos, len, &(req->args[i]));
}
return req;
}
void print_request(prequest r) {
int i;
if (r) {
printf("%s %d %d %s", r->id, r->timeout, r->memlimit, r->cmd);
for (i = 0; i < r->numargs; i++) {
for (int i = 0; i < r->numargs; i++) {
printf(" %s", r->args[i]);
}
} else {
......@@ -131,9 +137,8 @@ void print_request(prequest r) {
}
void free_request(prequest r) {
int i;
free(r->cmd);
for (i = 0;i < r->numargs; i++) {
for (int i = 0;i < r->numargs; i++) {
free(r->args[i]);
}
free(r->args);
......
......@@ -14,8 +14,11 @@
#include <stdbool.h>
typedef enum { REQ_RUN, REQ_INTERRUPT } request_type;
typedef struct {
int key;
request_type req_type;
char* id;
int timeout;
int memlimit;
......
......@@ -23,6 +23,7 @@
#include <stdio.h>
#include <errno.h>
#include <fcntl.h>
#include <libgen.h>
#include <poll.h>
#include <stddef.h>
#include <stdlib.h>
......@@ -65,6 +66,7 @@ struct pollfd* poll_list;
int poll_num = 0;
int poll_len = 0;
// global pointers are initialized with NULL by C semantics
plist processes;
plist clients;
char *current_dir;
......@@ -75,12 +77,11 @@ static int cpipe[2];
void shutdown_with_msg(char* msg);
void shutdown_with_msg(char* msg) {
int i;
if (server_sock != -1) {
close(server_sock);
}
if (clients != NULL) {
for (i = 0; i < list_length(clients); i++) {
for (int i = 0; i < list_length(clients); i++) {
close(((pclient) clients->data[i])->fd);
}
}
......@@ -102,8 +103,7 @@ void add_to_poll_list(int sock, short events) {
}
struct pollfd* poll_list_lookup(int fd) {
int i;
for (i = 0; i < poll_num; i++) {
for (int i = 0; i < poll_num; i++) {
if (poll_list[i].fd == fd) {
return poll_list+i;
}
......@@ -206,23 +206,47 @@ size_t unix_path_max() {
return sizeof(struct sockaddr_un) - offsetof(struct sockaddr_un, sun_path);
}
void server_init_listening(char* basename, int parallel) {
void server_init_listening(char* socketname, int parallel) {
struct sockaddr_un addr;
int res;
init_logging();
int cur_dir;
char *socketname_copy1, *socketname_copy2, *dirn, *filen;
// Initialize current_dir pointer. Do that here because we switch the
// directory temporarily below.
current_dir = get_cur_dir();
// Before opening the socket, we switch to the dir of the socket. This
// workaround is needed because Unix sockets only support relatively short
// paths (~100 chars depending on the system). We also open a file
// descriptor to the current dir so that we can switch back afterwards.
socketname_copy1 = strdup(socketname);
socketname_copy2 = strdup(socketname);
dirn = dirname(socketname_copy1);
filen = basename(socketname_copy2);
cur_dir = open(".", O_RDONLY);
if (cur_dir == -1) {
shutdown_with_msg("error when opening current directory");
}
res = chdir(dirn);
if (res == -1) {
shutdown_with_msg("error when switching to socket directory");
}
init_logging();
queue = init_queue(100);
clients = init_list(parallel);
addr.sun_family = AF_UNIX;
poll_len = 2 + parallel;
poll_list = (struct pollfd*) malloc(sizeof(struct pollfd) * poll_len);
poll_num = 0;
if (strlen(basename) + 1 > unix_path_max()) {
shutdown_with_msg("basename too long");
if (strlen(filen) + 1 > unix_path_max()) {
shutdown_with_msg("basename of filename too long");
}
memcpy(addr.sun_path, basename, strlen(basename) + 1);
memcpy(addr.sun_path, filen, strlen(filen) + 1);
server_sock = socket(AF_UNIX, SOCK_STREAM, 0);
res = unlink(basename);
res = unlink(filen);
// we delete the file if present
if (res == -1 && errno != ENOENT) {
shutdown_with_msg("error deleting socket");
......@@ -235,6 +259,16 @@ void server_init_listening(char* basename, int parallel) {
if (res == -1) {
shutdown_with_msg("error listening on socket");
}
res = fchdir(cur_dir);
if (res == -1) {
shutdown_with_msg("error when switching back to current directory");
}
res = close(cur_dir);
if (res == -1) {
shutdown_with_msg("error closing descriptor to current dir");
}
free(socketname_copy1);
free(socketname_copy2);
add_to_poll_list(server_sock, POLLIN);
processes = init_list(parallel);
setup_child_pipe();
......@@ -257,7 +291,6 @@ pid_t create_process(char* cmd,
int timelimit,
int memlimit) {
struct rlimit res;
int i;
char** unix_argv;
int count = argc;
// in the case of usestdin, the last argument is in fact not passed to
......@@ -268,7 +301,7 @@ pid_t create_process(char* cmd,
unix_argv = (char**)malloc(sizeof(char*) * (count + 2));
unix_argv[0] = cmd;
unix_argv[count + 1] = NULL;
for (i = 0; i < count; i++) {
for (int i = 0; i < count; i++) {
unix_argv[i + 1] = argv[i];
}
......@@ -436,6 +469,8 @@ void handle_child_events() {
}
}
/*@ requires r != NULL && r->req_type == REQ_RUN;
@*/
void run_request (prequest r) {
char* outfile;
int out_descr;
......@@ -467,6 +502,20 @@ void run_request (prequest r) {
send_started_msg_to_client(client, r->id);
}
void remove_from_queue(pqueue p, char *id) {
// inefficient, but what else?
pqueue tmp = init_queue(p->capacity);
while (!queue_is_empty(p)) {
prequest r = queue_pop(p);
if (strcmp(r->id,id)) queue_push(tmp, r);
}
while (!queue_is_empty(tmp)) {
prequest r = queue_pop(tmp);
queue_push(p, r);
}
free_queue(tmp);
}
void handle_msg(pclient client, int key) {
prequest r;
char* buf;
......@@ -486,11 +535,22 @@ void handle_msg(pclient client, int key) {
break;
r = parse_request(buf + old, cur - old, key);
if (r) {
if (list_length(processes) < parallel) {
run_request(r);
switch (r->req_type) {
case REQ_RUN:
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
queue_push(queue, (void*) r);
}
break;
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
remove_from_queue(queue, r->id);
// kill all processes whose id is r->id;
// TODO kill_processes(processes, r->id);
free_request(r);
} else {
queue_push(queue, (void*) r);
break;
}
}
//skip newline
......@@ -503,7 +563,7 @@ void handle_msg(pclient client, int key) {
}
void shutdown_server() {
unlink(basename);
unlink(socketname);
shutdown_with_msg("last client disconnected");
}
......@@ -544,13 +604,12 @@ void schedule_new_jobs() {
}
int main(int argc, char **argv) {
int i;
char ch;
int res;
struct pollfd* cur;
pclient client;
parse_options(argc, argv);
server_init_listening(basename, parallel);
server_init_listening(socketname, parallel);
while (1) {
schedule_new_jobs();
while ((res = poll(poll_list, poll_num, -1)) == -1 && errno == EINTR)
......@@ -558,7 +617,7 @@ int main(int argc, char **argv) {
if (res == -1) {
shutdown_with_msg("call to poll failed");
}
for (i = 0; i < poll_num; i++) {
for (int i = 0; i < poll_num; i++) {
cur = (struct pollfd*) poll_list + i;
if (cur->revents == 0) {
continue;
......
......@@ -20,11 +20,11 @@
#include <ntstatus.h>
#include <windows.h>
#include <libgen.h>
#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
#include <tchar.h>
#include <assert.h>
#include "queue.h"
#include "request.h"
#include "options.h"
......@@ -39,6 +39,7 @@
#define READOP 0
#define WRITEOP 1
// constants to distinguish between events from sockets and processes
#define SOCKET 0
#define PROCESS 1
......@@ -69,10 +70,16 @@ typedef struct {
char* outfile;
} t_proc, *pproc;
pserver server_socket = NULL;
int server_key = 0;
plist clients = NULL;
plist processes = NULL;
// AFAIU, there is no connection queue or something like that, so we need to
// create several socket instances to be able to process several clients that
// would connect almost at the same time. The two variables below will be
// allocated to arrays of equal length, holding the socket handle and the
// "key" (used for IO Completion Port) for each socket instance.
pserver* server_socket;
int* server_key;
plist clients;
plist processes;
char current_dir[MAX_PATH];
int gen_key = 1;
......@@ -95,28 +102,29 @@ int key_of_ms_key(ULONG_PTR ms) {
void init();
char* socket_name = NULL;
char* pipe_name;
HANDLE completion_port = NULL;
HANDLE completion_port;
void shutdown_with_msg(char* msg);
void shutdown_with_msg(char* msg) {
pproc proc;
int i;
if (completion_port != NULL) {
CloseHandle (completion_port);
}
if (server_socket != NULL) {
CloseHandle (server_socket->handle);
for (int i = 0; i < parallel; i++) {
if (server_socket[i] != NULL) {
CloseHandle (server_socket[i]->handle);
}
}
if (clients != NULL) {
for (i = 0; i < list_length(clients); i++) {
for (int i = 0; i < list_length(clients); i++) {
CloseHandle(((pclient) clients->data[i])->handle);
}
}
if (processes != NULL) {
for (i = 0; i < list_length(processes); i++) {
for (int i = 0; i < list_length(processes); i++) {
proc = processes->data[i];
CloseHandle(proc->handle);
CloseHandle(proc->job);
......@@ -169,12 +177,14 @@ void try_write(pclient client) {
}
}
void create_server_socket () {
// create a server socket and store it in the ith component of the
// server_socket array
void create_server_socket (int socket_num) {
pserver server;
int key = keygen();
server = (pserver) malloc(sizeof(t_server));
server->handle = CreateNamedPipe(
socket_name,
pipe_name,
PIPE_ACCESS_DUPLEX |
FILE_FLAG_OVERLAPPED, // non-blocking IO
PIPE_TYPE_MESSAGE | // message-type pipe
......@@ -191,8 +201,8 @@ void create_server_socket () {
add_to_completion_port(server->handle, to_ms_key(key, SOCKET));
ZeroMemory(&server->connect, sizeof(OVERLAPPED));
server->connect.hEvent = CreateEvent(NULL, FALSE, TRUE, NULL);
server_socket = server;
server_key = key;
server_socket[socket_num] = server;
server_key[socket_num] = key;
if (!ConnectNamedPipe(server->handle, (LPOVERLAPPED) &server->connect)) {
DWORD err = GetLastError();
if (err == ERROR_IO_PENDING) {
......@@ -292,18 +302,16 @@ void run_request (prequest r) {
/* Now take care of the arguments */
{
int k;
for (k = 0; k < argcount; k++)
for (int k = 0; k < argcount; k++)
{
char *ca = r->args[k]; /* current arg */
int ca_index; /* index of the current character in ca */
int need_quote = 1; /* set to 1 if quotes are needed */
/* Should we quote the string ? */
if (strlen(ca) > 0)
need_quote = 0;
for (ca_index = 0; ca_index < strlen(ca); ca_index++)
for (int ca_index = 0; ca_index < strlen(ca); ca_index++)
{
if (ca[ca_index] == ' ' || ca[ca_index] == '"')
{
......@@ -322,7 +330,7 @@ void run_request (prequest r) {
/* Open the double quoted string */
cmd[cl_index] = '"'; cl_index++;
for (ca_index = 0; ca_index < strlen(ca); ca_index++)
for (int ca_index = 0; ca_index < strlen(ca); ca_index++)
{
/* We have a double in the argument. It should be escaped
......@@ -333,8 +341,7 @@ void run_request (prequest r) {
They should be quoted. */
if (ca_index > 0 && ca[ca_index - 1] == '\\')
{
int j;
for (j = ca_index - 1; j >= 0 && ca[j] == '\\' ;j--)
for (int j = ca_index - 1; j >= 0 && ca[j] == '\\' ;j--)
{
cmd[cl_index] = '\\'; cl_index++;
}
......@@ -352,8 +359,7 @@ void run_request (prequest r) {
They should be quoted. */
if (ca[ca_index] == '\\' && ca_index + 1 == strlen(ca))
{
int j;
for (j = ca_index; j >= 0 && ca[j] == '\\' ;j--)
for (int j = ca_index; j >= 0 && ca[j] == '\\' ;j--)
{
cmd[cl_index] = '\\'; cl_index++;
}
......@@ -454,11 +460,19 @@ void handle_msg(pclient client, int key) {
//the read buffer also contains the newline, skip it
r = parse_request(client->readbuf->data, client->readbuf->len - 1, key);
if (r) {
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
switch (r->req_type) {
case REQ_RUN:
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
queue_push(queue, (void*) r);
}
break;
case REQ_INTERRUPT:
// TODO: remove r from the queue if still there, or kill the process r->id;
free_request(r);
break;
}
}
}
......@@ -473,15 +487,18 @@ void do_read(pclient client) {
(LPOVERLAPPED) &client->read);
}
void accept_client(int key) {
// the server socket with [key] and whose handle is stored in the [socket_num]
// component of the server_socket array, has received a client request. Handle
// it and create a new server socket instance for this socket number
void accept_client(int key, int socket_num) {
pclient client = (pclient) malloc(sizeof(t_client));
client->handle = server_socket->handle;
client->handle = server_socket[socket_num]->handle;
client->readbuf = init_readbuf(BUFSIZE);
client->writebuf = init_writebuf(16);
init_connect_data(&(client->read), READOP);
init_connect_data(&(client->write), WRITEOP);
free(server_socket);
create_server_socket();
free(server_socket[socket_num]);
create_server_socket(socket_num);
list_append(clients, key, (void*)client);
do_read(client);
}
......@@ -618,18 +635,40 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
}
void init() {
// The socketname variable may contain a full path, but on Windows,
// pipe sockets live in a special address space. We throw away the
// path info and just use the basename of the socketname variable.
char* socketname_copy, *my_pipe_name;
GetCurrentDirectory(MAX_PATH, current_dir);
socketname_copy = strdup(socketname);
my_pipe_name = basename(socketname_copy);
// on windows, named pipes live in a special address space
socket_name = (char*) malloc(sizeof(char) * (strlen(basename) + 10));
strcpy(socket_name, TEXT("\\\\.\\pipe\\"));
strcat(socket_name, basename);
pipe_name = (char*) malloc(sizeof(char) * (strlen(my_pipe_name) + 10));
strcpy(pipe_name, TEXT("\\\\.\\pipe\\"));
strcat(pipe_name, my_pipe_name);
queue = init_queue(100);
clients = init_list(16);
processes = init_list(16);
server_socket = (pserver*) malloc(parallel * sizeof(pserver));
server_key = (int*) malloc(parallel * sizeof(int));
init_logging();
create_server_socket();
for (int i = 0; i < parallel; i++) {
create_server_socket(i);
}
free(socketname_copy);
}
// If the key in argument corresponds to a server socket, return the server
// socket number, else return -1.
int get_server_num (int key) {
for (int i=0; i < parallel; i++) {
if (server_key[i] == key)
return i;
}
return -1;
}
int main(int argc, char **argv) {
......@@ -637,6 +676,7 @@ int main(int argc, char **argv) {
ULONG_PTR mskey;
int key;
int kind;
int server_num;
LPOVERLAPPED ov;
p_conn_data conn;
BOOL res;
......@@ -660,13 +700,14 @@ int main(int argc, char **argv) {
}
key = key_of_ms_key(mskey);
kind = kind_of_ms_key(mskey);
server_num = get_server_num(key);
switch (kind) {
case SOCKET:
if (key == server_key) {
if (server_num != -1) {
if (!res && GetLastError () != ERROR_PIPE_CONNECTED) {
shutdown_with_msg("error connecting client");
} else {