exit status: return 'unknown' exit code (0) on timeout

[amosr]

Hi Daniel,

We've noticed a strange behaviour where, if Kind2 times out, the exit code is 20 (safe). For some reason this only seems to happen when modular is true. We're worried about this because we're just checking the error codes, and this could hide some real issues.

I've tried to fix it by modifying status_of_exn in kind2Flow.ml so that it always returns "unknown" if the exception is a timeout.

If you want to reproduce, I used this example locally:

kind2 timeout.lus --timeout 1 --modular true ; echo exit code $?

On this (synthetic) timeout.lus which takes a while to verify or disprove:

node lastn(x: bool; const n: int)
returns (out: bool)
var
	count: int;
	prev:  int;
let
	prev = 0 -> pre count;
	count = if x then (if prev = n then n else prev + 1) else 0;
	out = count = n;
tel

node real_thing(a : int)
returns (o : int)
(*@contract
  assume a > 0;
  guarantee lastn(a > 1, 1000) => o >= 1000000000;
*)
let
  o = if lastn(a > 1, 1) then a * (0 -> pre o) + 1 else 0;
tel

on master I get the exit code 20 (safe):

-----------------------------------------------------------------------------------------------------
Summary of properties:
-----------------------------------------------------------------------------------------------------
guarantee[l17c2][1]: true up to 24 steps
=====================================================================================================

<Timeout> Wallclock timeout.

exit code 20

I couldn't figure out how to write an automated test for this one because it requires the timeout. It also seems a bit fragile in case Kind2 solves it before the timeout. What do you think?

Thanks,
Amos

[daniel-larraz]

Hi Amos,

Thank you very much for reporting this bug, and sorry for any inconvenience this may have caused to you.

I developed a more general fix that addresses the underlying problem. You can find it in pull request #690.

Thanks!
Daniel

[amosr]

Thanks Daniel!