afcf70aa6d
One might think that by merging the equivalence classes (eqclasses) of `Sym1` and `Sym2` symbols we would end up with a `State` in which the eqclass of `Sym1` and `Sym2` should now be the same. Surprisingly, it's not //always// true. Such an example triggered the assertion enforcing this _unjustified_ invariant in https://github.com/llvm/llvm-project/issues/58677. ```lang=C++ unsigned a, b; #define assert(cond) if (!(cond)) return void f(unsigned c) { /*(1)*/ assert(c == b); /*(2)*/ assert((c | a) != a); /*(3)*/ assert(a); // a = 0 => c | 0 != 0 => c != 0 => b != 0 } ``` I believe, that this assertion hold for reasonable cases - where both `MemberSym` and `SimplifiedMemberSym` refer to live symbols. It can only fail if `SimplifiedMemberSym` refers to an already dead symbol. See the reasoning at the very end. In this context, I don't know any way of determining if a symbol is alive/dead, so I cannot refine the assertion in that way. So, I'm proposing to drop this unjustified assertion. --- Let me elaborate on why I think the assertion is wrong in its current shape. Here is a quick reminder about equivalence classes in CSA. We have 4 mappings: 1) `ClassMap`: map, associating `Symbols` with an `EquivalenceClass`. 2) `ClassMembers`: map, associating `EquivalenceClasses` with its members - basically an enumeration of the `Symbols` which are known to be equal. 3) `ConstraintRange`: map, associating `EquivalenceClasses` with the range constraint which should hold for all the members of the eqclass. 4) `DisequalityMap`: I'm omitting this, as it's irrelevant for our purposes now. Whenever we encounter/assume that two `SymbolRefs` are equal, we update the `ClassMap` so that now both `SymbolRefs` are referring to the same eqclass. This operation is known as `merge` or `union`. Each eqclass is uniquely identified by the `representative` symbol, but it could have been just a unique number or anything else - the point is that an eqclass is identified by something unique. Initially, all Symbols form - by itself - a trivial eqclass, as there are no other Symbols to which it is assumed to be equal. A trivial eqclass has //notionally// exactly one member, the representative symbol. I'm emphasizing that //notionally// because for such cases we don't store an entry in the `ClassMap` nor in the `ClassMembers` map, because it could be deduced. By `merging` two eqclasses, we essentially do what you would think it does. An important thing to highlight is that the representative symbol of the resulting eqclass will be the same as one of the two eqclasses. This operation should be commutative, so that `merge(eq1,eq2)` and `merge(eq2,eq1)` should result in the same eqclass - except for the representative symbol, which is just a unique identifier of the class, a name if you will. Using the representative symbol of `eq1` or `eq2` should have no visible effect on the analysis overall. When merging `eq1` into `eq2`, we take each of the `ClassMembers` of `eq1` and add them to the `ClassMembers` of `eq2` while we also redirect all the `Symbol` members of `eq1` to map to the `eq2` eqclass in the `ClassMap`. This way all members of `eq1` will refer to the correct eqclass. After these, `eq1` key is unreachable in the `ClassMembers`, hence we can drop it. --- Let's get back to the example. Note that when I refer to symbols `a`, `b`, `c`, I'm referring to the `SymbolRegionValue{VarRegion{.}}` - the value of that variable. After `(1)`, we will have a constraint `c == b : [1,1]` and an eqclass `c,b` with the `c` representative symbol. After `(2)`, we will have an additional constraint `c|b != a : [1,1]` with the same eqclass. We will also have disequality info about that `c|a` is disequal to `a` - and the other way around. However, after the full-expression, `c` will become dead. This kicks in the garbage collection, which transforms the state into this: - We no longer have any constraints, because only `a` is alive, for which we don't have any constraints. - We have a single (non-trivial) eqclass with a single element `b` and representative symbol `c`. (Dead symbols can be representative symbols.) - We have the same disequality info as before. At `(3)` within the false branch, `a` get perfectly constrained to zero. This kicks in the simplification, so we try to substitute (simplify) the variable in each SymExpr-tree. In our case, it means that the `c|a != a : [1,1]` constraint gets re-evaluated as `c|0 != 0 : [1,1]`, which is `c != 0 : [1,1]`. Under the hood, it means that we will call `merge(c|a, c)`. where `c` is the result of `simplifyToSVal(State, MemberSym).getAsSymbol()` inside `EquivalenceClass::simplify()`. Note that the result of `simplifyToSVal()` was a dead symbol. We shouldn't have acquired an already dead symbol. AFAIK, this is the only way we can get one at this point. Since `c` is dead, we no longer have a mapping in `ClassMap` for it; hence when we try to `find()` the eqclass of `c`, it will report that it's a trivial eqclass with the representative symbol `c`. After `merge(c|a, c)`, we will have a single (non-trivial) eqclass of `b, c|a` with the representative symbol `c|a` - because we merged the eqclass of `c` into the eqclass of `c|a`. This means that `find(c|a)` will result in the eqclass with the representative symbol `c|a`. So, we ended up having different eqclasses for `find(c|a)` and `find(c)` after `merge(c|a, c)`, firing the assertion. I believe, that this assertion hold for reasonable cases - where both `MemberSym` and `SimplifiedMemberSym` refer to live symbols. `MemberSym` should be live in all cases here, because it is from `ClassMembers` which is pruned in `removeDeadBindings()` so these must be alive. In this context, I don't know any way of determining if a symbol is alive/dead, so I cannot refine the assertion in that way. So, I'm proposing to drop this unjustified assertion. I'd like to thank @martong for helping me to conclude the investigation. It was really difficult to track down. PS: I mentioned that `merge(eq1, eq2)` should be commutative. We actually exploit this for merging the smaller eqclass into the bigger one within `EquivalenceClass::merge()`. Yea, for some reason, if you swap the operands, 3 tests break (only failures, no crashes) aside from the test which checks the state dumps. But I believe, that is a different bug and orthogonal to this one. I just wanted to mention that. - `Analysis/solver-sym-simplification-adjustment.c` - `Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp` - `Analysis/symbol-simplification-reassume.cpp` Fixes #58677 Reviewed By: vabridgers Differential Revision: https://reviews.llvm.org/D138037
//===----------------------------------------------------------------------===//
// Clang Static Analyzer
//===----------------------------------------------------------------------===//
= Library Structure =
The analyzer library has two layers: a (low-level) static analysis
engine (ExprEngine.cpp and friends), and some static checkers
(*Checker.cpp). The latter are built on top of the former via the
Checker and CheckerVisitor interfaces (Checker.h and
CheckerVisitor.h). The Checker interface is designed to be minimal
and simple for checker writers, and attempts to isolate them from much
of the gore of the internal analysis engine.
= How It Works =
The analyzer is inspired by several foundational research papers ([1],
[2]). (FIXME: kremenek to add more links)
In a nutshell, the analyzer is basically a source code simulator that
traces out possible paths of execution. The state of the program
(values of variables and expressions) is encapsulated by the state
(ProgramState). A location in the program is called a program point
(ProgramPoint), and the combination of state and program point is a
node in an exploded graph (ExplodedGraph). The term "exploded" comes
from exploding the control-flow edges in the control-flow graph (CFG).
Conceptually the analyzer does a reachability analysis through the
ExplodedGraph. We start at a root node, which has the entry program
point and initial state, and then simulate transitions by analyzing
individual expressions. The analysis of an expression can cause the
state to change, resulting in a new node in the ExplodedGraph with an
updated program point and an updated state. A bug is found by hitting
a node that satisfies some "bug condition" (basically a violation of a
checking invariant).
The analyzer traces out multiple paths by reasoning about branches and
then bifurcating the state: on the true branch the conditions of the
branch are assumed to be true and on the false branch the conditions
of the branch are assumed to be false. Such "assumptions" create
constraints on the values of the program, and those constraints are
recorded in the ProgramState object (and are manipulated by the
ConstraintManager). If assuming the conditions of a branch would
cause the constraints to be unsatisfiable, the branch is considered
infeasible and that path is not taken. This is how we get
path-sensitivity. We reduce exponential blow-up by caching nodes. If
a new node with the same state and program point as an existing node
would get generated, the path "caches out" and we simply reuse the
existing node. Thus the ExplodedGraph is not a DAG; it can contain
cycles as paths loop back onto each other and cache out.
ProgramState and ExplodedNodes are basically immutable once created. Once
one creates a ProgramState, you need to create a new one to get a new
ProgramState. This immutability is key since the ExplodedGraph represents
the behavior of the analyzed program from the entry point. To
represent these efficiently, we use functional data structures (e.g.,
ImmutableMaps) which share data between instances.
Finally, individual Checkers work by also manipulating the analysis
state. The analyzer engine talks to them via a visitor interface.
For example, the PreVisitCallExpr() method is called by ExprEngine
to tell the Checker that we are about to analyze a CallExpr, and the
checker is asked to check for any preconditions that might not be
satisfied. The checker can do nothing, or it can generate a new
ProgramState and ExplodedNode which contains updated checker state. If it
finds a bug, it can tell the BugReporter object about the bug,
providing it an ExplodedNode which is the last node in the path that
triggered the problem.
= Notes about C++ =
Since now constructors are seen before the variable that is constructed
in the CFG, we create a temporary object as the destination region that
is constructed into. See ExprEngine::VisitCXXConstructExpr().
In ExprEngine::processCallExit(), we always bind the object region to the
evaluated CXXConstructExpr. Then in VisitDeclStmt(), we compute the
corresponding lazy compound value if the variable is not a reference, and
bind the variable region to the lazy compound value. If the variable
is a reference, just use the object region as the initializer value.
Before entering a C++ method (or ctor/dtor), the 'this' region is bound
to the object region. In ctors, we synthesize 'this' region with
CXXRecordDecl*, which means we do not use type qualifiers. In methods, we
synthesize 'this' region with CXXMethodDecl*, which has getThisType()
taking type qualifiers into account. It does not matter we use qualified
'this' region in one method and unqualified 'this' region in another
method, because we only need to ensure the 'this' region is consistent
when we synthesize it and create it directly from CXXThisExpr in a single
method call.
= Working on the Analyzer =
If you are interested in bringing up support for C++ expressions, the
best place to look is the visitation logic in ExprEngine, which
handles the simulation of individual expressions. There are plenty of
examples there of how other expressions are handled.
If you are interested in writing checkers, look at the Checker and
CheckerVisitor interfaces (Checker.h and CheckerVisitor.h). Also look
at the files named *Checker.cpp for examples on how you can implement
these interfaces.
= Debugging the Analyzer =
There are some useful command-line options for debugging. For example:
$ clang -cc1 -help | grep analyze
-analyze-function <value>
-analyzer-display-progress
-analyzer-viz-egraph-graphviz
...
The first allows you to specify only analyzing a specific function.
The second prints to the console what function is being analyzed. The
third generates a graphviz dot file of the ExplodedGraph. This is
extremely useful when debugging the analyzer and viewing the
simulation results.
Of course, viewing the CFG (Control-Flow Graph) is also useful:
$ clang -cc1 -help | grep cfg
-cfg-add-implicit-dtors Add C++ implicit destructors to CFGs for all analyses
-cfg-add-initializers Add C++ initializers to CFGs for all analyses
-cfg-dump Display Control-Flow Graphs
-cfg-view View Control-Flow Graphs using GraphViz
-unoptimized-cfg Generate unoptimized CFGs for all analyses
-cfg-dump dumps a textual representation of the CFG to the console,
and -cfg-view creates a GraphViz representation.
= References =
[1] Precise interprocedural dataflow analysis via graph reachability,
T Reps, S Horwitz, and M Sagiv, POPL '95,
http://portal.acm.org/citation.cfm?id=199462
[2] A memory model for static analysis of C programs, Z Xu, T
Kremenek, and J Zhang, http://lcs.ios.ac.cn/~xzx/memmodel.pdf