Commit 883af7f6 authored by Johannes Kanig's avatar Johannes Kanig

P909-002 allow for large exit codes

Sometimes the windows syscall GetExitCodeProcess returns a large result,
larger than the ocaml [int] type. This is expected and not an error. For
example the constant STATUS_QUOTA_EXCEEDED, which is 0xC0000044, may be
a valid exit code. Such large values trip up the [int_of_string] parsing
in the client.

This patch implements the following solution to this problem:
* the server doesn't care and sends the large value;
* (the server now recognizes this value, though, to set the timeout flag
  more often)
* the client uses an Int64 value to parse that big constant;
* when converting to the internal Unix.process_status type, we simply
  convert to [int], because such large values don't have any special
  meaning for Why3 anyway.

* call_provers.ml
(parse_prover_run): now directly take the exit status as argument, and
convert it to int;
(handle_answer): don't wrap argument to parse_prover_run into unix type
* prove_client.ml
(read_answer): read Int64 type now
* server-win.c
(handle_child_event): set timeout boolean also when exitcode is equal to
   constant STATUS_QUOTA_EXCEEDED

Change-Id: I1163a6f1adf1bdbfe1f53269ce0ae57dc8bd0287
parent 81090d89
......@@ -193,19 +193,16 @@ let debug_print_model model =
let model_str = Model_parser.model_to_string model in
Debug.dprintf debug "Call_provers: %s@." model_str
let parse_prover_run res_parser time out ret limit ~printer_mapping =
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
grep out res_parser.prp_regexps
| Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
grep out res_parser.prp_regexps
| Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n res_parser.prp_exitcodes
with Not_found -> grep out res_parser.prp_regexps)
in
let parse_prover_run res_parser time out exitcode limit ~printer_mapping =
Debug.dprintf debug "Call_provers: exited with status %Ld@." exitcode;
(* the following conversion is incorrect (but does not fail) on 32bit, but if
the incoming exitcode was really outside the bounds of [int], its exact
value is meaningless for Why3 anyway (e.g. some windows status codes). If
it becomes meaningful, we might want to change the conversion here *)
let int_exitcode = Int64.to_int exitcode in
let ans =
try List.assoc int_exitcode res_parser.prp_exitcodes
with Not_found -> grep out res_parser.prp_regexps in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
......@@ -254,7 +251,7 @@ let parse_prover_run res_parser time out ret limit ~printer_mapping =
Debug.dprintf debug "Call_provers: model:@.";
debug_print_model model;
{ pr_answer = ans;
pr_status = ret;
pr_status = Unix.WEXITED int_exitcode;
pr_output = out;
pr_time = time;
pr_steps = steps;
......@@ -341,7 +338,7 @@ let handle_answer answer =
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 ret = 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
......
......@@ -171,7 +171,7 @@ type final_answer = {
time : float;
timeout : bool;
out_file : string;
exit_code : int;
exit_code : int64;
}
type answer =
......@@ -188,7 +188,7 @@ let read_answer s =
Finished { id = int_of_string id;
out_file = Strings.join ";" rest;
time = float_of_string time_s;
exit_code = int_of_string exit_s;
exit_code = Int64.of_string exit_s;
timeout = (timeout_s = "1"); }
| "S" :: [id] ->
Started (int_of_string id)
......
......@@ -33,7 +33,7 @@ type final_answer = {
time : float;
timeout : bool;
out_file : string;
exit_code : int;
exit_code : int64;
}
type answer =
......
......@@ -18,6 +18,7 @@
#ifdef _WIN32
#include <ntstatus.h>
#include <windows.h>
#include <stdio.h>
#include <stdlib.h>
......@@ -565,6 +566,7 @@ void schedule_new_jobs() {
void handle_child_event(pproc child, pclient client, int proc_key, DWORD event) {
DWORD exitcode;
bool timeout;
FILETIME ft_start, ft_stop, ft_system, ft_user;
ULARGE_INTEGER ull_system, ull_user;
double cpu_time;
......@@ -596,11 +598,12 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
ull_user.HighPart = ft_user.dwHighDateTime;
cpu_time =
((ull_system.QuadPart + ull_user.QuadPart + 0.0) / 10000000.);
timeout = (exitcode == 1816) || (exitcode == STATUS_QUOTA_EXCEEDED);
send_msg_to_client(client,
child->id,
exitcode,
cpu_time,
(exitcode == 1816),
timeout,
child->outfile);
free_process(child);
break;
......
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