Bounded-like checker for LTS

[kris7t]

This patch adds a bounded-like model checker that can work with LTS. This allows use to use BMC for models that can't be converted to MonolithicExpr directly, or when such conversion introduces a large overhead. Another benefit is testing new features (e.g., XCFA labels) that are only implemented in the LTS and TransFunc level, without having to provide a corresponding MonolithicExpr implementation.

• Adds BoundedLtsChecker, a checker that expands and LTS and an Analysis like an Abstractor, but applies a BMC-like procedure to call an SMT solver after every expanded transition and finally deliver a safe/unsafe/unknown verdict.
• In theory, the bounded-like checker could be used with any Analysis and Prec. Such a configuration would use the specified level of abstraction to enumerate transitions without passing the full path condition to the SMT solver before checking the full path condition like a BMC. However, we currently only use the unit abstraction, meaning that fireability is entirely determined by full path condition checking.
• Adds UnitXcfaAnalysis, anAnalysis that uses the unit abstraction for XCFA. This analysis is not suitable for CEGAR, as it cannot be refined, but it lets BoundedLtsChecker handle the full path condition.

[leventeBajczi]

Thanks for the PR! Besides a version bump, could you please also do the following so that this could be used from the CLI?

1. Create a new entry here:

   theta/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt

   Lines 66 to 68 in c7e1c3e

   	enum class Backend {
   	CEGAR,
   	BOUNDED,

2. Add an entry here, with possible configuration options (create your own / reuse cegar / use null if no further input option is possible):

   theta/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

   Lines 202 to 227 in c7e1c3e

   	when (backend) {
   	Backend.CEGAR -> CegarConfig() as T
   	Backend.BMC ->
   	BoundedConfig(
   	indConfig = InductionConfig(disable = true),
   	itpConfig = InterpolationConfig(disable = true),
   	)
   	as T
   	Backend.KIND -> BoundedConfig(itpConfig = InterpolationConfig(disable = true)) as T
   	Backend.IMC ->
   	BoundedConfig(
   	bmcConfig = BMCConfig(disable = true),
   	indConfig = InductionConfig(disable = true),
   	)
   	as T
   	Backend.KINDIMC -> BoundedConfig() as T
   	Backend.BOUNDED -> BoundedConfig() as T
   	Backend.CHC -> HornConfig() as T
   	Backend.OC -> OcConfig() as T
   	Backend.LAZY -> null
   	Backend.PORTFOLIO -> PortfolioConfig() as T
   	Backend.MDD -> MddConfig() as T
   	Backend.LASSO_VALIDATION -> LassoValidationConfig() as T
   	Backend.NONE -> null
   	Backend.IC3 -> Ic3Config() as T
   	}

3. Create a checker if that backend was specified (should probably be similar to cegar checker):

   theta/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt

   Line 48 in c7e1c3e

   Backend.CEGAR -> getCegarChecker(xcfa, mcm, config, logger)

4. Optionally extend these few lines to check if a safety proof is bounded, and return unknown if needed:

   theta/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt

   Line 264 in c7e1c3e

   result.isSafe && xcfa?.unsafeUnrollUsed ?: false -> {

This way it could be integrated easily into other parts of Theta, e.g., portfolios. Also, it would be easy to run a sanity check with SV-COMP tasks to see if anything was missed.

[kris7t]

@leventeBajczi

2. Add an entry here, with possible configuration options (create your own / reuse cegar / use null if no further input option is possible):

So this is the point where users should configure the BMC bound?

4. Optionally extend these few lines to check if a safety proof is bounded, and return unknown if needed:

I'm not sure this is needed, the checker already returns UNSAFE unless the whole state space has been explored with the provided bound. Or does unsafeUnrollUsed do something even more unsafe?

Also, it would be easy to run a sanity check with SV-COMP tasks to see if anything was missed.

This is a good idea, although I'm not sure what bound to set for SV-COMP. The current exploration strategy is depth-first to take advantage of push/pop, so merely running until the time is exhausted (with increasing bounds) isn't really feasible.

We could possibly make the exploration breath-first (and sacrifice push/pop), but I'm not sure whether that's really useful just to support SV-COMP. At any rate, the programs where we currently want to use this (examples from ongoing paper) are loop-free, so either setup works.

21.0% Coverage on New Code (required ≥ 60%)

So I reckon I should put a test for BoundedLtsChecker in :theta-analysis, as coverage information doesn't get picked up :theta-xcfa-analysis, right?

[leventeBajczi]

So this is the point where users should configure the BMC bound?

Yes, exactly. Alternatively, you could leave it always unbounded, and use the --force-unroll flag from the input options to create an unrolled tree-like XCFA

I'm not sure this is needed, the checker already returns UNSAFE unless the whole state space has been explored with the provided bound. Or does unsafeUnrollUsed do something even more unsafe?

Great! I missed that.

This is a good idea, although I'm not sure what bound to set for SV-COMP. The current exploration strategy is depth-first to take advantage of push/pop, so merely running until the time is exhausted (with increasing bounds) isn't really feasible.

For SV-COMP, a loop unroll bound of 3-10 is usually enough. If the bound is a bound on edges, then let's triple that number (given LBE, I think that's at least somewhat correct).

So I reckon I should put a test for BoundedLtsChecker in :theta-analysis, as coverage information doesn't get picked up :theta-xcfa-analysis, right?

Yep, that's right. But lately we've been ignoring the sonar quality gate where there are tests but Sonar does not pick them up, so don't invest too much time there (alternatively, if you had some ideas how to collect the test data such that it would pick up coverage inter-subproject, we would really appreciate it)

[kris7t]

@leventeBajczi I added some support for calling this checker into xcfa-cli. Based on @csanadtelbisz 's suggestion, it's available under the name PATH_ENUMERATION. It should be possible to combine it with COI and SPOR, but not AAPOR or DPOR.

You can also set an abstract domain other than UNIT. In this case, only those paths will be enumerate that are allowed by the abstract domain to reduce SMT solver calls. This likely only makes sense is calculating the next abstract state is cheaper that checking the whole path condition (deterministic programs with EXPL perhaps?). Another interesting use-case would be to use zone abstraction for timed systems, but a zone domain that handles thread start/end remains to be implemented.

How could we test this on SV-COMP? I don't expect it to be very useful, but maybe there are some interesting cases it can cover with SPOR.

[sonarqubecloud]

Quality Gate failed

Failed conditions
18.5% Coverage on New Code (required ≥ 60%)

See analysis details on SonarQube Cloud

[csanadtelbisz]

How could we test this on SV-COMP? I don't expect it to be very useful, but maybe there are some interesting cases it can cover with SPOR.

I send you a config file in private.

[csanadtelbisz]

4. Optionally extend these few lines to check if a safety proof is bounded, and return unknown if needed:

I'm not sure this is needed, the checker already returns UNSAFE unless the whole state space has been explored with the provided bound. Or does unsafeUnrollUsed do something even more unsafe?

I think Levi misinterpreted your comment. Other bounded analyses in Theta behave in a way that they return SAFE if no error is found within bound (or UNKNOWN). However, the unsafeUnrollUsed flag should be set whenever the whole state space was (probably) not explored. For example, see LoopUnrollPass when it uses force unroll mode. The final result processor will know that the result is unknown if the analysis returned SAFE but the flag is set. (But we can easily bypass this postprocessing using the --accept-unreliable-safe cli option if we want to compare with other bounded tools outputting SAFE for bounded proofs.)

For example, the consistency checker produces the following behavior (and log) for a task with an infinite loop after exploring the behavior up to certain iterations and finding no bugs:

OC checker result: (SafetyResult Safe)
Incomplete loop unroll used: safe result is unreliable.
(SafetyResult Unknown)
hu.bme.mit.theta.common.exception.NotSolvableException: Task is not solvable with this configuration!

[kris7t]

Ah, sorry, I meant the checker returns UNKNOWN unless the whole state space has been explored with the provided bound. So basically

• If the error location is reached within the bound, the output is UNSAFE
• If states reached after max-bound edges have any outgoing actions, the output is UNKNOWN
• Otherwise, the output is SAFE
  • Post-processing due to force-unroll will change this UNKNOWN

So the output is SAFE iff no force-unroll is used and all states of the system has been explored. Is this logic correct, or should I change it to be more in line with other bounded checkers?

[csanadtelbisz]

This is perfect, thank you.

[kris7t]

@leventeBajczi After running on SV-COMP, there are some false Safe (e.g., pthread/singleton.yml) and false Unsafe (e.g., pthread/stack-1.yml) results on parallel programs with pointers, some something's amiss with my PtrState handling.