When both CHC and BMC engines are used, the type of state variable
changes when trusted mode for external calls is used. This is because in
CHC engine, trusted mode means we pack more information into the
symbolic state. In BMC this type is always simple.
However, if BMC is run after CHC, in the current code state variables
are reset (and their declaration dumped into SMT-LIB script) before BMC
resets the type of the state variable.
The proposed solution is to simply reset the variable type before the
first variable of this type is created.
if a struct has a member that is a function pointer with `external`
attribute, and such a member is called, it is currently incorrectly
treated as a public getter in SMTEncoder.
The proposed fix is to make SMTEncoder::publicGetter more strict in
deciding whether an expression is a public getter.
The added condition, that the access happens on a state variable, is
exactly what is checked later with an assertion that is currently
failing.
Previously, we did not remember trusted external calls for later phase
when we compute possible verification targets for each function.
This led to false negative in cases where verification target can be
violated, but not by calling a public function directly, but only when
it is called as an external function from other function.
The added test cases witnesses this behaviour. The underflow in
`dec` cannot happen in any other way except what the `dec` is called
from `f`.
The same problem did not occur when the functions are called internally,
because for such cases, we have already been remembering these calls in
the callgraph in the CHC engine.
Without path condition, verification targets created inside ternary
operator ignore the condition of the operator inside the branches.
This led to false positives.
Further updates:
- Function calls should consider the conditions under which they are
called, otherwise the analysis may report false positives.
The fix proposed here is to add the current path condition to the edge
that propagates error from a function call.
- Increment error index after function call
This is necessary for the analysis of the ternary operator to work
correctly. No information should leak from a function call inside a
ternary operator in the first branch to the second branch, including
whether or not an error would have occured in the first branch.
However, for the execution that continues after the function call,
we still need to ensure that under the current path condition
the error has not occurred in that function call.
It would be better to isolate the analysis of the branches to separate
clauses, but I do not see an easy way for that now. In this way, even
though the function call in first branch is included in the clause of
the second branch, no information leaks.
- Additonal test for ternary operator
This tests the behaviour of SMTChecker on ternary operator with function
calls inside both branches. Specifically, it tests that SMTChecker
successfully detects a violation of a verification target in the second
branch when the same target is present also in the first branch, but
there it cannot be triggered because of the operator's condition.
is to, in a future commit, replace such occurences of
isByteArrayOrString() which are required to return True only for Bytes
type with a new isByteArray() function.
