Commit 8f610390 authored by Johannes Kanig's avatar Johannes Kanig Committed by Sylvain Dailler

Q213-024 why3server allows to take long path as socket

Unix sockets have the restriction that the path to the socket must be
quite short (100 chars give or take depending on exact OS). We can
workaround this limitation by chdir'ing to the dirname of the socket
first. We need to do that in the client and server parts of the code,
but only for Unix (windows doesn't use Unix sockets obviously).

Right now this code is not strictly needed in gnatprove, because we
don't pass a path, only a filename as the socket. But this will change
later.

* prove_client.ml
(client_connect): save curdir, change to dirname, connect to basename,
  then go back to curdir
* options.c
rename socketname because it would clash with basename from libgen.h
* server-unix.c
rename of basename to socketname
(server_init_listening): save curdir, change to dirname, connect to
  basename, then go back to curdir
* server-win.c
rename of basename to socketname

Change-Id: Ib69587dfa136f6ced753c983bc37203c37acb936
(cherry picked from commit e6c15eb26d6077e814ab8c72deb92fc86e43600a)
parent 7904985c
......@@ -24,10 +24,16 @@ let client_connect ~fail socket_name =
if Sys.os_type = "Win32" then
let name = "\\\\.\\pipe\\" ^ socket_name in
Unix.openfile name [Unix.O_RDWR] 0
else
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX socket_name);
sock
else begin
let curdir = Sys.getcwd () in
let dir = Filename.dirname socket_name in
let fn = Filename.basename socket_name in
Sys.chdir dir;
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX fn);
Sys.chdir curdir;
sock
end
in
socket := Some sock
with
......
......@@ -16,7 +16,7 @@
#include "options.h"
int parallel = 1;
char* basename = NULL;
char* socketname = NULL;
bool logging = false;
bool single_client = false;
......@@ -65,7 +65,7 @@ void parse_options(int argc, char **argv) {
break;
case 's':
basename = optarg;
socketname = optarg;
break;
case '?':
......@@ -80,7 +80,7 @@ void parse_options(int argc, char **argv) {
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);
}
......
......@@ -17,7 +17,7 @@
// how many processes are allowed to run in parallel
extern int parallel;
// the name of the socket (path)
extern char* basename;
extern char* socketname;
// enable or disable logging
extern bool logging;
// start in single client mode
......
......@@ -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>
......@@ -204,23 +205,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");
......@@ -233,6 +258,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();
......@@ -527,7 +562,7 @@ void handle_msg(pclient client, int key) {
}
void shutdown_server() {
unlink(basename);
unlink(socketname);
shutdown_with_msg("last client disconnected");
}
......@@ -573,7 +608,7 @@ int main(int argc, char **argv) {
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)
......
......@@ -637,9 +637,9 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
void init() {
GetCurrentDirectory(MAX_PATH, current_dir);
// on windows, named pipes live in a special address space
socket_name = (char*) malloc(sizeof(char) * (strlen(basename) + 10));
socket_name = (char*) malloc(sizeof(char) * (strlen(socketname) + 10));
strcpy(socket_name, TEXT("\\\\.\\pipe\\"));
strcat(socket_name, basename);
strcat(socket_name, socketname);
queue = init_queue(100);
clients = init_list(16);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment