steakhal added a comment.
In D88019#2303078 <https://reviews.llvm.org/D88019#2303078>, @martong wrote:
> I like the second approach, i.e. to have a debug checker. But I don't see,
> how would this checker validate all constraints at the moment when they are
> added to the State.
`ProgramStateRef evalAssume(ProgramStateRef State, SVal Cond, bool Assumption)`
checker callback is called **after** any assume call.
So, we would have a `State` which has all? the constraints stored in the
appropriate GDM. I'm not sure if we should aggregate all the constraints till
this node - like we do for refutation. I think, in this case, we should just
make sure that the **current** state does not have any contradiction.
---
Here is my proof-of-concept:
I've dumped the state and args of evalAssume for the repro example, pretending
that we don't reach a code-path on the infeasable path to crash:
void avoidInfeasibleConstraintforGT(int a, int b) {
int c = b - a;
if (c <= 0)
return;
if (a != b) {
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
return;
}
clang_analyzer_warnIfReached(); // eh, we will reach this..., #1
// These are commented out, to pretend that we don't find out that we are
on an infeasable path...
// a == b
// if (c < 0)
// ;
}
We reach the `#1` line, but more importantly, we will have the following state
dumps:
evalAssume: assuming Cond: (reg_$1<int a>) != (reg_$0<int b>) to be true in
state:
"program_state": {
"constraints": [
{ "symbol": "(reg_$0<int b>) - (reg_$1<int a>)", "range": "{ [1,
2147483647] }" },
{ "symbol": "(reg_$1<int a>) != (reg_$0<int b>)", "range": "{
[-2147483648, -1], [1, 2147483647] }" }
]
}
evalAssume: assuming Cond: (reg_$1<int a>) != (reg_$0<int b>) to be false in
state:
"program_state": {
"constraints": [
{ "symbol": "(reg_$0<int b>) - (reg_$1<int a>)", "range": "{ [1,
2147483647] }" },
{ "symbol": "(reg_$1<int a>) != (reg_$0<int b>)", "range": "{ [0, 0] }" }
]
}
As you can see, the **latter** is the //infeasable// path, and if we have had
serialized the constraints and let the Z3 check it, we would have gotten that
it's unfeasable.
At this point the checker can dump any useful data for debugging, and crash the
analyzer to let us know that something really bad happened.
> [...] And that might be too slow, it would have the same speed as using z3
> instead of the range based solver.
Yes, it will probably freaking slow, but at least we have something.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D88019/new/
https://reviews.llvm.org/D88019
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
