Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
eaa8926a
Commit
eaa8926a
authored
Jul 01, 2016
by
sylvain dailler
Browse files
Adding support for started message from server
parent
6f1a4308
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/driver/call_provers.ml
View file @
eaa8926a
...
...
@@ -296,19 +296,23 @@ let read_and_delete_file fn =
out
let
handle_answer
answer
=
let
id
=
answer
.
Prove_client
.
id
in
let
save
=
Hashtbl
.
find
saved_data
id
in
Hashtbl
.
remove
saved_data
id
;
if
Debug
.
test_noflag
debug
then
begin
Sys
.
remove
save
.
vc_file
;
if
save
.
inplace
then
Sys
.
rename
(
backup_file
save
.
vc_file
)
save
.
vc_file
end
;
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
save
.
limit
~
printer_mapping
in
id
,
ans
match
answer
with
|
Prove_client
.
Finished
answer
->
let
id
=
answer
.
Prove_client
.
id
in
let
save
=
Hashtbl
.
find
saved_data
id
in
Hashtbl
.
remove
saved_data
id
;
if
Debug
.
test_noflag
debug
then
begin
Sys
.
remove
save
.
vc_file
;
if
save
.
inplace
then
Sys
.
rename
(
backup_file
save
.
vc_file
)
save
.
vc_file
end
;
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
save
.
limit
~
printer_mapping
in
id
,
Some
ans
|
Prove_client
.
Started
id
->
id
,
None
let
wait_for_server_result
~
blocking
=
List
.
map
handle_answer
(
Prove_client
.
read_answers
~
blocking
)
...
...
@@ -345,7 +349,11 @@ type prover_update =
let
result_buffer
:
(
server_id
,
prover_update
)
Hashtbl
.
t
=
Hashtbl
.
create
17
let
get_new_results
~
blocking
=
(* TODO: handle ProverStarted events *)
List
.
iter
(
fun
(
id
,
r
)
->
Hashtbl
.
add
result_buffer
id
(
ProverFinished
r
))
List
.
iter
(
fun
(
id
,
r
)
->
let
x
=
match
r
with
|
Some
r
->
ProverFinished
r
|
None
->
ProverStarted
in
Hashtbl
.
add
result_buffer
id
x
)
(
wait_for_server_result
~
blocking
)
let
query_result_buffer
id
=
...
...
@@ -375,7 +383,7 @@ let rec wait_on_call = function
|
ServerCall
id
as
pc
->
begin
match
query_result_buffer
id
with
|
ProverFinished
r
->
r
|
_
->
|
_
->
get_new_results
~
blocking
:
true
;
wait_on_call
pc
end
...
...
src/driver/prove_client.ml
View file @
eaa8926a
...
...
@@ -166,7 +166,7 @@ let rec read_lines blocking =
read_lines
blocking
end
type
answer
=
{
type
final_
answer
=
{
id
:
int
;
time
:
float
;
timeout
:
bool
;
...
...
@@ -174,16 +174,22 @@ type answer = {
exit_code
:
int
;
}
type
answer
=
|
Started
of
int
|
Finished
of
final_answer
let
read_answer
s
=
match
Strings
.
split
'
;
'
s
with
|
id
::
exit_s
::
time_s
::
timeout_s
::
(
(
_
::
_
)
as
rest
)
->
|
"F"
::
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 *)
{
id
=
int_of_string
id
;
Finished
{
id
=
int_of_string
id
;
out_file
=
Strings
.
join
";"
rest
;
time
=
float_of_string
time_s
;
exit_code
=
int_of_string
exit_s
;
timeout
=
(
timeout_s
=
"1"
);
}
|
"S"
::
[
id
]
->
Started
(
int_of_string
id
)
|
_
->
raise
(
InvalidAnswer
s
)
...
...
src/driver/prove_client.mli
View file @
eaa8926a
...
...
@@ -28,7 +28,7 @@ val send_request :
cmd
:
string
list
->
unit
type
answer
=
{
type
final_
answer
=
{
id
:
int
;
time
:
float
;
timeout
:
bool
;
...
...
@@ -36,6 +36,10 @@ type answer = {
exit_code
:
int
;
}
type
answer
=
|
Started
of
int
|
Finished
of
final_answer
val
read_answers
:
blocking
:
bool
->
answer
list
val
set_max_running_provers
:
int
->
unit
src/server/server-unix.c
View file @
eaa8926a
...
...
@@ -341,6 +341,26 @@ void write_to_client(pclient client, struct pollfd* entry) {
}
}
void
send_started_msg_to_client
(
pclient
client
,
char
*
id
)
{
char
*
msgbuf
;
size_t
len
=
0
;
int
used
;
//len of id + S + semicolon + \n + \0
len
+=
strlen
(
id
)
+
4
;
msgbuf
=
(
char
*
)
malloc
(
sizeof
(
char
)
*
len
);
if
(
msgbuf
==
NULL
)
{
shutdown_with_msg
(
"error when allocating client msg"
);
}
used
=
snprintf
(
msgbuf
,
len
,
"S;%s
\n
"
,
id
);
if
(
used
!=
len
-
1
)
{
shutdown_with_msg
(
"message for client too long"
);
}
queue_write
(
client
,
msgbuf
);
}
void
send_msg_to_client
(
pclient
client
,
char
*
id
,
int
exitcode
,
...
...
@@ -350,8 +370,8 @@ void send_msg_to_client(pclient client,
char
*
msgbuf
;
size_t
len
=
0
;
int
used
;
//len of id + semicolon
len
+=
strlen
(
id
)
+
1
;
//len of id +
F + 2
semicolon
len
+=
strlen
(
id
)
+
3
;
// we assume a length of at most 9 for both exitcode and time, plus one for
// the timeout boolean, plus three semicolons, makes 23 chars
len
+=
23
;
...
...
@@ -361,7 +381,7 @@ void send_msg_to_client(pclient client,
if
(
msgbuf
==
NULL
)
{
shutdown_with_msg
(
"error when allocating client msg"
);
}
used
=
snprintf
(
msgbuf
,
len
,
"%s;%d;%.2f;%d;%s
\n
"
,
used
=
snprintf
(
msgbuf
,
len
,
"
F;
%s;%d;%.2f;%d;%s
\n
"
,
id
,
exitcode
,
cpu_time
,
(
timeout
?
1
:
0
),
outfile
);
if
(
used
>=
len
)
{
shutdown_with_msg
(
"message for client too long"
);
...
...
@@ -444,6 +464,7 @@ void run_request (prequest r) {
proc
->
id
=
id
;
proc
->
outfile
=
outfile
;
list_append
(
processes
,
id
,
(
void
*
)
proc
);
send_started_msg_to_client
(
client
,
r
->
id
);
}
void
handle_msg
(
pclient
client
,
int
key
)
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment