martong added a comment.
> OK, we definitely need to know about performance.
Couldn't agree more. I am in the middle of a performance measurement that I do
with csa-testbench (on
memchached,tmux,curl,twin,redis,vim,openssl,sqlite,ffmpeg,postgresql,tinyxml2,libwebm,xerces,bitcoin,protobuf).
Hopefully I can give you some results soon.
> Plus, I'm still curious about the crash. I didn't get how simplification
> helped/caused that crash.
So, the crash was actually an assertion failure in StdLibraryFunctionsChecker,
which came when I made a test analysis run on the twin project. The assertion
was here:
if (FailureSt && !SuccessSt) {
if (ExplodedNode *N = C.generateErrorNode(NewState))
reportBug(Call, N, Constraint.get(), Summary, C);
break;
} else {
// We will apply the constraint even if we cannot reason about the
// argument. This means both SuccessSt and FailureSt can be true. If we
// weren't applying the constraint that would mean that symbolic
// execution continues on a code whose behaviour is undefined.
assert(SuccessSt); //
<----------------------------------------------------------------- This fired
!!!
NewState = SuccessSt;
}
With multiple creduce iterations below is a minimal example with
StdLibraryFunctionsChecker. That crashed when we applied the `BufferSize`
constraint of `fread`.
typedef int FILE;
long b;
unsigned long fread(void *__restrict, unsigned long, unsigned long,
FILE *__restrict);
void foo();
void c(int *a, int e0) {
int e1 = e0 - b;
b == 2;
foo();
int e2 = e1 - b;
if (e2 > 0 && b == e1) {
(void)a; (void)e1; (void)c;
fread(a, sizeof(char), e1, c);
}
}
Turned out, the checker had the assertion because before applying the arg
constraint and its negated counterpart, the state was already infeasible. (But
the analyzer recognized this only when it added the new assumptions when
checking the applicability of the arg constraint.)
Thus, I could remove `fread` and the Checker from the problem set and could
create the test case that synthesizes the unfeasible state.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D103314/new/
https://reviews.llvm.org/D103314
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
