Use call as location for error node corresponding to requires

[schuessf]

Currently, the error nodes in the CFG that correspond to a requires use the location of the requires itself instead of the call (this behaviour was changed in bb54f4c). Therefore, the results whether a requires for a call holds (as produced by e.g., trace abstraction) also contain the location (as a line number) of the function declaration. This behaviour is particullarly problematic when checking for memsafety of C programs. There, we add a requires to an auxiliary read function (that has the line number -1 for that reason) and therefore we get results like this: CounterExampleResult [Line: -1]: pointer dereference may fail.

This PR changes the behaviour again, such that the location of the call is used to identify the error location from a requires. To do so, the method CfgBuilder::addErrorNode receives the BoogieASTNode for the location and the specification to label the error node separately.

The change was applied to RCFGBuilder and IcfgBuilder.

[danieldietsch]

What happens if a function with a requires is called from multiple locations, i.e., a function with more than one call?

[schuessf]

What happens if a function with a requires is called from multiple locations, i.e., a function with more than one call?

For each call different error nodes are already constructed, this was not changed in this PR, they just have the "wrong" location at the declaration of the function to be called. You can see it in this log from the SV-COMP for memsafety:

  - CounterExampleResult [Line: -1]: pointer dereference may fail
    pointer dereference may fail
We found a FailurePath: 
[...]
[L584]              pat[i]
  - UnprovableResult [Line: -1]: Unable to prove that pointer dereference always succeeds
    Unable to prove that pointer dereference always succeeds
    [...]

There are multiple pointer dereferences in the C program and you can see from the counterexample that we found that the dereference in line 584 might fail, but any result (CounterExampleResult and all the UnprovableResults) just contain line -1 (i.e., the location of the auxiliary function).

[danieldietsch]

I was thinking about the case where a program has an ACSL requires and a call violates that. How is this error reported now?

[schuessf]

Okay, consider this program

//@ requires x >= 0;
int f(int x) {
  return x - 1;
}

int main() {
  f(0);
  f(-1);
}

Currently, there are two results:
UnprovableResult [Line: 1]: Unable to prove that procedure precondition always holds for the call f(0) and

CounterExampleResult [Line: 1]: procedure precondition can be violated
procedure precondition can be violated
We found a FailurePath: 
[L7]  CALL  f(0)
      VAL   [\at(x, Pre)=0]
[L1]        //@ requires (x >= 0);
      VAL   [\at(x, Pre)=0]
[L3]        return x - 1;
      VAL   [\at(x, Pre)=0, \result=-1]
[L7]  RET   f(0)
[L1]        //@ requires (x >= 0);

for f(-1)

Both of these results contain the line 1 of the requires, with this PR the locations of the results would change to line 7 and 8.

[danieldietsch]

Ok, is this the current state? What would it look like with this PR?

I would think we want to have both, the requires and the call, and if the requires does not have a valid line then we drop it.
For the example, I would expect either a positive result for the first call and a counterexample for the second, or only the counterexample for the second, but certainly not an UJnprovableResult -- this is also somewhat weird.

And the second result looks strange anyways: why is there Call, Requires, Return, Requires? I would expect Call, Requires, Return, Call, Requires. Why is the second call different?

[schuessf]

Ok, is this the current state? What would it look like with this PR?

So far, this PR only changes the location of the error nodes that are only used in the result.
The output of the counterexample uses the location of the edges that remain unchanged.
But I checked again: For this example the locations of the results did not change to line 7 and 8, but to line -1, as we try to merge the locations for the requires and the call. I have to investigate the reason for that....

I would think we want to have both, the requires and the call, and if the requires does not have a valid line then we drop it. For the example, I would expect either a positive result for the first call and a counterexample for the second, or only the counterexample for the second, but certainly not an UJnprovableResult -- this is also somewhat weird.

We get a counterexample for the second call, even though the call f(-1) is somehow not contained in the counterexample.
We get a UnprovableResult for the first call f(0), as we don't even check it because we find the counterexample first. We already discussed in the past, whether we always need an UnprovableResult or whether it should be renamed.

And the second result looks strange anyways: why is there Call, Requires, Return, Requires? I would expect Call, Requires, Return, Call, Requires. Why is the second call different?

🤷‍♂️

[danieldietsch]

:)

I thought we had a NotCheckedResult or something like that,