[Draft] Add assert timeout configuration option for Silicon backend#1013
[Draft] Add assert timeout configuration option for Silicon backend#1013jcp19 wants to merge 3 commits into
Conversation
Exposes Silicon's --assertTimeout option through Gobra's CLI, allowing users to set a per-assertion timeout in milliseconds. The option is Silicon-specific and guarded by validation to reject use with Carbon. https://claude.ai/code/session_01DNDg4ADj7NW35SQMt26uD2
The test defines an abstract ghost pure function `magic` (uninterpreted) and a method that assumes a quantifier whose trigger creates a matching loop. With a 1-second assert timeout set via inline config, Silicon correctly reports the assertion as failed instead of looping forever. https://claude.ai/code/session_01DNDg4ADj7NW35SQMt26uD2
|
Human here: I edited the PR description, I reviewed the code, and vouch for both. I find this option particularly useful in combination with a proposed change I discussed yesterday with Nick (@rayman2000) and Marco (@marcoeilers): to introduce a new type of error reason for proof obligations that time out. This is useful not only for humans debugging performance issues (e.g., understanding which precondition is taking forever to verify on a method-call) and to LLMs, as they would get more info on what the cause of verification error is on those cases. Ofc, we need to open a new PR to support that kind of error-reason if and when it is introduced in Viper. EDIT: if that error reason is eventually introduced in Viper, I think it is worth having a permissive (but finite) default value for the assert timeout in Gobra (10-15s). This would make Gobra more beginner friendly, as the new users would have a clear indication that something is not ideal about their queries |
jcp19
changed the title
|
Funnily enough, the added test does not terminate because the long verification times occur due to a push, not an assert. We could in principle configure the pushTimeout as well (silicon already supports this), but the SMT solver seems to ignore this parameter |
What happens on push? Is the SMT solver automatically figuring out whether there are any inconsistencies? |
3 participants
Summary
This PR adds support for configuring a timeout (in milliseconds) for assert operations performed by the Silicon backend. The timeout can be specified via the
--assertTimeoutcommand-line flag and is only applicable when using Silicon or ViperServer with Silicon as the backend.Key Changes
--assertTimeoutcommand-line option via Scallop configurationassertTimeoutthat takes the minimum value when both configs specify a timeout (most restrictive)EDIT: the test for this feature is currently failing. This failure seems to come from silicon itself (it is unclear if the assert timeout is being enforced). Please ignore the PR for now.