[all-commits] [llvm/llvm-project] c4fa05: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: c4fa05f5f7783efa380c200d96cc1f756fa88c6c
      https://github.com/llvm/llvm-project/commit/c4fa05f5f7783efa380c200d96cc1f756fa88c6c
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-10 (Tue, 10 May 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
    M clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/ProgramState.cpp
    A clang/test/Analysis/infeasible-sink.c

  Log Message:
  -----------
  [analyzer] Indicate if a parent state is infeasible

In some cases a parent State is already infeasible, but we recognize
this only if an additonal constraint is added. This patch is the first
of a series to address this issue. In this patch `assumeDual` is changed
to clone the parent State but with an `Infeasible` flag set, and this
infeasible-parent is returned both for the true and false case. Then
when we add a new transition in the exploded graph and the destination
is marked as infeasible, the node will be a sink node.

Related bug:
https://github.com/llvm/llvm-project/issues/50883
Actually, this patch does not solve that bug in the solver, rather with
this patch we can handle the general parent-infeasible cases.

Next step would be to change the State API and require all checkers to
use the `assume*Dual` API and deprecate the simple `assume` calls.

Hopefully, the next patch will introduce `assumeInBoundDual` and will
solve the CRASH we have here:
https://github.com/llvm/llvm-project/issues/54272

Differential Revision: https://reviews.llvm.org/D124674


  Commit: 1c1c1e25f94fd1bb10fdbfe96dc14ffc655db5df
      https://github.com/llvm/llvm-project/commit/1c1c1e25f94fd1bb10fdbfe96dc14ffc655db5df
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-10 (Tue, 10 May 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
    A clang/test/Analysis/infeasible-crash.c

  Log Message:
  -----------
  [analyzer] Implement assume in terms of assumeDual

Summary:
By evaluating both children states, now we are capable of discovering
infeasible parent states. In this patch, `assume` is implemented in the terms
of `assumeDuali`. This might be suboptimal (e.g. where there are adjacent
assume(true) and assume(false) calls, next patches addresses that). This patch
fixes a real CRASH.
Fixes https://github.com/llvm/llvm-project/issues/54272

Differential Revision:
https://reviews.llvm.org/D124758


  Commit: 34ac048aef298270d82e5430727ffd00f15c63d5
      https://github.com/llvm/llvm-project/commit/34ac048aef298270d82e5430727ffd00f15c63d5
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-10 (Tue, 10 May 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
    M clang/lib/StaticAnalyzer/Checkers/ArrayBoundChecker.cpp
    M clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
    M clang/lib/StaticAnalyzer/Checkers/ObjCContainersChecker.cpp
    M clang/lib/StaticAnalyzer/Checkers/ReturnPointerRangeChecker.cpp
    M clang/lib/StaticAnalyzer/Checkers/UndefResultChecker.cpp
    M clang/lib/StaticAnalyzer/Core/ProgramState.cpp

  Log Message:
  -----------
  [analyzer] Replace adjacent assumeInBound calls to assumeInBoundDual

This is to minimize superfluous assume calls.

Depends on D124758

Differential Revision: https://reviews.llvm.org/D124761


Compare: https://github.com/llvm/llvm-project/compare/3d888b0491f8...34ac048aef29