[PATCH] D103314: [Analyzer][solver] Simplify existing constraints when a new constraint is added

[Gabor Marton via Phabricator via cfe-commits]

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