[sim642]

This is on top of #1849.

It's enough to self-validate the transition invariants generated with #1849. Also it validates the sv-witnesses example from https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/blob/main/examples/terminating-program-example.witness-2.1.yml (added as test).

TODO

• Parse invariant expressions with \at(...). This is done quite hackily to not require CIL extensions: \at(x, AnyPrev) is replaced with __any_x_AnyPrev__, which is at least valid C syntax.
• Map __any_x_AnyPrev__ variables to suitable internal varinfos.
• Actually evaluate expressions with those in them.
• Profit?

[michael-schwarz]

I'm worried this may not be sound for path-sensitivity:

int c = 0;
int x = 0;
int mode = 0;

while (c < 20) {
    c++;
    mode = !mode;
    x = mode ? c - 100 : c;
}

assume that I am partitioning by mode. x_prev < x will be validated within each partition and then joined. However it is not true overall. So I think one might have to join before evaluating here?

Maybe the same applies for generation too?

[michael-schwarz]

Also, maybe we need to check whether the termination was proven (which goes beyond showing that the transition invariant holds, e.g., because of recursion) before answering true?

[sim642]

Also, maybe we need to check whether the termination was proven (which goes beyond showing that the transition invariant holds, e.g., because of recursion) before answering true?

That happens in a general way for all properties and invariants at

analyzer/src/witness/witness.ml

Lines 252 to 258 in aafcc37

	match yaml_validate_result with
	| Some (Stdlib.Error _ as result)
	| Some (Ok (Svcomp.Result.False _ | Unknown) as result) ->
	result
	| Some (Ok True)
	| None ->
	write entrystates

where write falls back to the verification verdict if validation was fine.

[sim642]

So I think one might have to join before evaluating here?

Maybe the same applies for generation too?

Indeed, I found a similar issue with loop unrolling. The simple joining that was just optimized in #2293 doesn't help with either:

• Unrolled loop iterations have a different node, so the joining needs to also happen across unrollings. We have the data for it, but I don't know if we ever used it for joining like that.
• And from the outside, I don't think we can even force to join all the paths of a Spec.D: PathSensitivity2 will just keep different paths separate internally anyway. And paths_as_set won't help: it will split into multiple Spec.D-s but joining those will again keep the separate paths. I recall some version of the effects implementation having a special function to join paths.

This isn't a problem for normal invariant evaluation, but it is for transition invariants because the transition could exactly go from one path/unrolling to another, not necessarily stay in the same one (especially with unrollings). And unless we know better, we'd have to cover transitions from every one to every other one (at a location):

• This should be doable if we actually force join everything into one. Of course it's less precise but that's not the main priority currently.
• I thought about it for a while and I think we could also try joining all pairs (including with itself), but that's more expensive and requires a bit of extra trickery in EvalTransitionInt to still identify the same unrolling (by all loop counters being same/constant). And it'd also have to apply to all pairs of paths.