Fix timeout

[Stevendeo]

Timeouts were disabled for satml_frontend (check #946). The issue was that the timeout may kill the calculation while the environment is being updated, which leaves it in a state where some invariants have been broken, and the model_gen_on_timeout attemps to generate a model from an unsound environment.

This PR forces the model_gen_on_timeout to return I_dont_know whatever the exception raised by its calculation.

[bclement-ocp]

I didn't think about this while we discussed it in #946 but: beyond exceptions, we are also dealing with error messages. For instance the error in #946 is printed using Printer.print_err and that would happen even if we catch the exceptions :(

[Stevendeo]

Good point; error messages could still be printed as long as they are in smtlib2 format (prefixed with ';'), this would allow us to have feedback on failed assertions and still properly return unknown

[Stevendeo]

I am realizing that now we properly handle timeouts, we no longer catch Util.Timeout on the binary side. The only reason we do is because Timeout catching was disabled, but now the new tests cardinal.models.timeout_dolmen.smt2 and cs-soundness.models.timeout.smt2 do not pass as errors, but as unknown with error code 0.
Do you think I should remove the timeout handler from the binary as well in this PR?

[bclement-ocp]

Error messages are on the diagnostics channel so they should not need to be prefixed with ;. That said, do we really want to risk displaying such humongous error messages as the one in #946 to users in what we want to look like normal operating circumstances? This really looks like a bug, and if people are using this feature and hitting the condition — we will probably get bug reports.

(Not even mentioning that one of the main issues with #946 is that this fills up the logs database when we run benchmarks — although now that I think about it we don't use --timelimit-interpretation when running benchmarks so that should not be an issue here)

I see 3 options:

1. Keep the PR as is, users risk seeing awful error messages but we cross our fingers that it won't happen too often;
2. Keep the PR as is, but temporarily disable the diagnostics channel during model_gen_on_timeout
3. Only keep the part of the PR that uses the infrastructure you wrote for --steps-bound also for the timeouts, but keep model_gen_on_timeout disabled for satML (this is my preferred option, especially given that Why3 does not use this feature)

[bclement-ocp]

I am realizing that now we properly handle timeouts, we no longer catch Util.Timeout on the binary side. The only reason we do is because Timeout catching was disabled, but now the new tests cardinal.models.timeout_dolmen.smt2 and cs-soundness.models.timeout.smt2 do not pass as errors, but as unknown with error code 0. Do you think I should remove the timeout handler from the binary as well in this PR?

Ah dang. Does this mean that the binary keeps processing additional statements after a timeout? If so, that is an issue, the binary should terminate as quick as possible after a timeout. Well, that's the contract that we had for the --timelimit option until now, at least, unless --timelimit-per-goal is enabled. So maybe what we should do is only catch the timeouts in the frontend if --timelimit-per-goal is enabled, and let the binary catch it otherwise. I think this would be the closest to the behavior of released versions, which is what users would expect. Would that make sense?

[Stevendeo]

I am in favor for option 3 actually. @Halbaroth any opinion on the matter?

Does this mean that the binary keeps processing additional statements after a timeout?

I am not sure that is the case. What happens now is that exit_on_timeout is dead code, because the timeout treatment is exclusively handled on the library side. We could keep it just in case we forgot a case and the frontend somehow lets a Timeout escape though.

[Stevendeo]

We discussed it and he agrees with option 3

[bclement-ocp]

I am not sure that is the case. What happens now is that exit_on_timeout is dead code, because the timeout treatment is exclusively handled on the library side. We could keep it just in case we forgot a case and the frontend somehow lets a Timeout escape though.

Not sure I undestand — if exit_as_timeout is not called, who is stopping the binary from processing further statements? Isn't the Dolmen pipe going to keep going until the end of the file (and potentially start another check-sat with no timeout)?

[Stevendeo]

Not sure I undestand — if exit_as_timeout is not called, who is stopping the binary from processing further statements? Isn't the Dolmen pipe going to keep going until the end of the file (and potentially start another check-sat with no timeout)?

Oh ok I see your point; I think it keeps processing commands but everytime the command requires to call for the SAT, it fails because it reaches the timeout.

[bclement-ocp]

Yeah, then that's not good — the contract is that --timelimit is a limit on the time Alt-Ergo takes to process the whole file (unless --timelimit-per-goal is specified, then this is a limit for each check-sat), so the binary needs to stop ASAP. If my mental model is right, the Frontend would also currently allow a second check-sat call that would be processed with no timeout after a first one has finished with a timeout (I may be wrong on that, but would be an issue).

I think that what is currently implemented in the PR is the proper behavior for --timelimit-per-goal, but we still need to keep the behavior when --timelimit-per-goal is not enabled, hence my suggestion to only catch timeouts in the frontend if --timelimit-per-goal is enabled (and let the binary catch it and call exit_as_timeout otherwise).

[Stevendeo]

If my mental model is right, the Frontend would also currently allow a second check-sat call that would be processed with no timeout after a first one has finished with a timeout (I may be wrong on that, but would be an issue).

Your mental model is actually right ^^'

[Stevendeo]

Okay, now the hook on status checks if timeout is the status has been reached and exits

[bclement-ocp]

Okay, now the hook on status checks if timeout is the status has been reached and exits

That looks like a good way to do it.

We could keep it just in case we forgot a case and the frontend somehow lets a Timeout escape though.

I agree with this — let's keep the exception handlers for now. We'll clean that up when we move processing directly into the solving loop.

[bclement-ocp]

Suggested change

	| Timeout _ -> exit_as_timeout ()
	| Timeout _ when not Options.get_timelimit_per_goal () -> exit_as_timeout ()

[Stevendeo]

How to tell which timeout has been triggered?

[bclement-ocp]

What do you mean? There is only one timeout -- the --timelimit-per-goal option changes the meaning of that timeout from "per solver instance" to "per SAT query" (in which case we need to continue processing).

[Stevendeo]

Oh okay, I thought there were two kinds of timeout my bad!

[bclement-ocp]

Can't blame you, there should be IMO (see also the discussion in #946), but yeah currently we only have the one.

[bclement-ocp]

I believe that this PR removes the only piece of code that sets model_gen_phase to true, so the field should be removed.

[Stevendeo]

I agree with this — let's keep the exception handlers for now. We'll clean that up when we move processing directly into the solving loop.

Actually, it is necessary to keep them in the case the timeout is triggered between calls of the sat solver. The chance of this happening is extremely low, but it might happen.

[bclement-ocp]

Just a thought: wondering if we should call Frontend.print_status at all when we call exit_as_timeout, since it leads to slightly weird output:

unknown
(error "timeout")

Maybe just (error "timeout") (or even timeout as we used to do; it is not a standard SMT-LIB response, but it is used by Z3 and hence parsed by many tools, including Why3 — and since we don't support unknown-reason with the "hard" timeout that would be easier for them to get the information out).

[Stevendeo]

I am in favor of either the current solution (unknown + error) or the timeout only, but I have a preference for the first one because it matches the standard

[bclement-ocp]

My understanding is that the current behavior is actually not standard-compliant because we give two responses to a (check-sat) command where the standard only expects (at most; success can be skipped) one response per command.

(In any case, this is unrelated to this PR)

[Stevendeo]

Error handling is quite generic in the smtlib reference:

An expression of the form (error e) should be returned for any kind of error situation 
(wrong command syntax, incorrect parameters, erroneous execution, and so on).

[bclement-ocp]

I understand this as being a particular case of:

Generally, once a solver completes its processing in response to a command, it should print to its regular output channel a 〈general_response〉

But it doesn't really matter; tools can process either output anyway (I had a glance at Why3's code for the SMT variant of Alt-Ergo and it looks like they currently don't parse timeouts at all there, so eh).