Since `raw_string_ostream` doesn't own the string buffer, it is
desirable (in terms of memory safety) for users to directly reference
the string buffer rather than use `raw_string_ostream::str()`.
Work towards TODO comment to remove `raw_string_ostream::str()`.
Previously the function `RangeConstraintManager::printValue()` crashed
when it encountered an empty rangeset (because `RangeSet::getBitwidth()`
and `RangeSet::isUnsigned()` assert that the rangeset is not empty).
This commit adds a special case that avoids this behavior.
As `printValue()` is only used by the checker debug.ExprInspection (and
during manual debugging), the impacts of this commit are very limited.
---------
Co-authored-by: Balazs Benics <benicsbalazs@gmail.com>
This commit extends the class `SValBuilder` with the methods
`getMinValue()` and `getMaxValue()` to that work like
`SValBuilder::getKnownValue()` but return the minimal/maximal possible
value the `SVal` is not perfectly constrained.
This extension of the ConstraintManager API is discussed at:
https://discourse.llvm.org/t/expose-the-inferred-range-information-in-warning-messages/75192
As a simple proof-of-concept application of this new API, this commit
extends a message from `core.BitwiseShift` with some range information
that reports the assumptions of the analyzer.
My main motivation for adding these methods is that I'll also want to
use them in `ArrayBoundCheckerV2` to make the error messages less
awkward, but I'm starting with this simpler and less important usecase
because I want to avoid merge conflicts with my other commit
https://github.com/llvm/llvm-project/pull/72107 which is currently under
review.
The testcase `too_large_right_operand_compound()` shows a situation
where querying the range information does not work (and the extra
information is not added to the error message). This also affects the
debug utility `clang_analyzer_value()`, so the problem isn't in the
fresh code. I'll do some investigations to resolve this, but I think
that this commit is a step forward even with this limitation.
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
This patch fixes certain cases where solver was not able to infer
disequality due to overlapping of values in rangeset. This case was
casting from lower signed type to bigger unsigned type.
Reviewed By: steakhal
Differential Revision: https://reviews.llvm.org/D140086
With this patch, the solver can infer results for not equal (!=) operator
over Ranges as well. This also fixes the issue of comparison between
different types, by first converting the RangeSets to the resulting type,
which then can be used for comparisons.
Patch by Manas.
Reviewed By: steakhal
Differential Revision: https://reviews.llvm.org/D112621
This patch mechanically replaces None with std::nullopt where the
compiler would warn if None were deprecated. The intent is to reduce
the amount of manual work required in migrating from Optional to
std::optional.
This is part of an effort to migrate from llvm::Optional to
std::optional:
https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getvalue-getvalueor/63716
Summary: Introduce a new function 'clang_analyzer_value'. It emits a report that in turn prints a RangeSet or APSInt associated with SVal. If there is no associated value, prints "n/a".
Summary: Sorted some handler-functions into more appropriate visitor functions of the SymbolicRangeInferrer.
- Spread `getRangeForNegatedSub` body over several visitor functions: `VisitSymExpr`, `VisitSymIntExpr`, `VisitSymSymExpr`.
- Moved `getRangeForComparisonSymbol` from `infer` to `VisitSymSymExpr`.
Differential Revision: https://reviews.llvm.org/D129678
Depends on D124758. That patch introduced serious regression in the run-time in
some special cases. This fixes that.
Differential Revision: https://reviews.llvm.org/D126406
Fixes https://github.com/llvm/llvm-project/issues/55546
The assertion mentioned in the issue is triggered because an
inconsistency is formed in the Sym->Class and Class->Sym relations. A
simpler but similar inconsistency is demonstrated here:
https://reviews.llvm.org/D114887 .
Previously in `removeMember`, we didn't remove the old symbol's
Sym->Class relation. Back then, we explained it with the following two
bullet points:
> 1) This way constraints for the old symbol can still be found via it's
> equivalence class that it used to be the member of.
> 2) Performance and resource reasons. We can spare one removal and thus one
> additional tree in the forest of `ClassMap`.
This patch do remove the old symbol's Sym->Class relation in order to
keep the Sym->Class relation consistent with the Class->Sym relations.
Point 2) above has negligible performance impact, empirical measurements
do not show any noticeable difference in the run-time. Point 1) above
seems to be a not well justified statement. This is because we cannot
create a new symbol that would be equal to the old symbol after the
simplification had happened. The reason for this is that the SValBuilder
uses the available constant constraints for each sub-symbol.
Differential Revision: https://reviews.llvm.org/D126281
Summary: Handle casts for ranges working similarly to APSIntType::apply function but for the whole range set. Support promotions, truncations and conversions.
Example:
promotion: char [0, 42] -> short [0, 42] -> int [0, 42] -> llong [0, 42]
truncation: llong [4295033088, 4295033130] -> int [65792, 65834] -> short [256, 298] -> char [0, 42]
conversion: char [-42, 42] -> uint [0, 42]U[4294967254, 4294967295] -> short[-42, 42]
Differential Revision: https://reviews.llvm.org/D103094
Summary: Handle intersected and adjacent ranges uniting them into a single one.
Example:
intersection [0, 10] U [5, 20] = [0, 20]
adjacency [0, 10] U [11, 20] = [0, 20]
Differential Revision: https://reviews.llvm.org/D99797
This reverts commit f02c5f3478318075d1a469203900e452ba651421 and
addresses the issue mentioned in D114619 differently.
Repeating the issue here:
Currently, during symbol simplification we remove the original member
symbol from the equivalence class (`ClassMembers` trait). However, we
keep the reverse link (`ClassMap` trait), in order to be able the query
the related constraints even for the old member. This asymmetry can lead
to a problem when we merge equivalence classes:
```
ClassA: [a, b] // ClassMembers trait,
a->a, b->a // ClassMap trait, a is the representative symbol
```
Now let,s delete `a`:
```
ClassA: [b]
a->a, b->a
```
Let's merge ClassA into the trivial class `c`:
```
ClassA: [c, b]
c->c, b->c, a->a
```
Now, after the merge operation, `c` and `a` are actually in different
equivalence classes, which is inconsistent.
This issue manifests in a test case (added in D103317):
```
void recurring_symbol(int b) {
if (b * b != b)
if ((b * b) * b * b != (b * b) * b)
if (b * b == 1)
}
```
Before the simplification we have these equivalence classes:
```
trivial EQ1: [b * b != b]
trivial EQ2: [(b * b) * b * b != (b * b) * b]
```
During the simplification with `b * b == 1`, EQ1 is merged with `1 != b`
`EQ1: [b * b != b, 1 != b]` and we remove the complex symbol, so
`EQ1: [1 != b]`
Then we start to simplify the only symbol in EQ2:
`(b * b) * b * b != (b * b) * b --> 1 * b * b != 1 * b --> b * b != b`
But `b * b != b` is such a symbol that had been removed previously from
EQ1, thus we reach the above mentioned inconsistency.
This patch addresses the issue by making it impossible to synthesise a
symbol that had been simplified before. We achieve this by simplifying
the given symbol to the absolute simplest form.
Differential Revision: https://reviews.llvm.org/D114887
Currently, during symbol simplification we remove the original member symbol
from the equivalence class (`ClassMembers` trait). However, we keep the
reverse link (`ClassMap` trait), in order to be able the query the
related constraints even for the old member. This asymmetry can lead to
a problem when we merge equivalence classes:
```
ClassA: [a, b] // ClassMembers trait,
a->a, b->a // ClassMap trait, a is the representative symbol
```
Now lets delete `a`:
```
ClassA: [b]
a->a, b->a
```
Let's merge the trivial class `c` into ClassA:
```
ClassA: [c, b]
c->c, b->c, a->a
```
Now after the merge operation, `c` and `a` are actually in different
equivalence classes, which is inconsistent.
One solution to this problem is to simply avoid removing the original
member and this is what this patch does.
Other options I have considered:
1) Always merge the trivial class into the non-trivial class. This might
work most of the time, however, will fail if we have to merge two
non-trivial classes (in that case we no longer can track equivalences
precisely).
2) In `removeMember`, update the reverse link as well. This would cease
the inconsistency, but we'd loose precision since we could not query
the constraints for the removed member.
Differential Revision: https://reviews.llvm.org/D114619
We no longer need a reference to RangedConstraintManager, we call top
level `State->assume` functions.
Differential Revision: https://reviews.llvm.org/D113261
D103314 introduced symbol simplification when a new constant constraint is
added. Currently, we simplify existing equivalence classes by iterating over
all existing members of them and trying to simplify each member symbol with
simplifySVal.
At the end of such a simplification round we may end up introducing a
new constant constraint. Example:
```
if (a + b + c != d)
return;
if (c + b != 0)
return;
// Simplification starts here.
if (b != 0)
return;
```
The `c == 0` constraint is the result of the first simplification iteration.
However, we could do another round of simplification to reach the conclusion
that `a == d`. Generally, we could do as many new iterations until we reach a
fixpoint.
We can reach to a fixpoint by recursively calling `State->assume` on the
newly simplified symbol. By calling `State->assume` we re-ignite the
whole assume machinery (along e.g with adjustment handling).
Why should we do this? By reaching a fixpoint in simplification we are capable
of discovering infeasible states at the moment of the introduction of the
**first** constant constraint.
Let's modify the previous example just a bit, and consider what happens without
the fixpoint iteration.
```
if (a + b + c != d)
return;
if (c + b != 0)
return;
// Adding a new constraint.
if (a == d)
return;
// This brings in a contradiction.
if (b != 0)
return;
clang_analyzer_warnIfReached(); // This produces a warning.
// The path is already infeasible...
if (c == 0) // ...but we realize that only when we evaluate `c == 0`.
return;
```
What happens currently, without the fixpoint iteration? As the inline comments
suggest, without the fixpoint iteration we are doomed to realize that we are on
an infeasible path only after we are already walking on that. With fixpoint
iteration we can detect that before stepping on that. With fixpoint iteration,
the `clang_analyzer_warnIfReached` does not warn in the above example b/c
during the evaluation of `b == 0` we realize the contradiction. The engine and
the checkers do rely on that either `assume(Cond)` or `assume(!Cond)` should be
feasible. This is in fact assured by the so called expensive checks
(LLVM_ENABLE_EXPENSIVE_CHECKS). The StdLibraryFuncionsChecker is notably one of
the checkers that has a very similar assertion.
Before this patch, we simply added the simplified symbol to the equivalence
class. In this patch, after we have added the simplified symbol, we remove the
old (more complex) symbol from the members of the equivalence class
(`ClassMembers`). Removing the old symbol is beneficial because during the next
iteration of the simplification we don't have to consider again the old symbol.
Contrary to how we handle `ClassMembers`, we don't remove the old Sym->Class
relation from the `ClassMap`. This is important for two reasons: The
constraints of the old symbol can still be found via it's equivalence class
that it used to be the member of (1). We can spare one removal and thus one
additional tree in the forest of `ClassMap` (2).
Performance and complexity: Let us assume that in a State we have N non-trivial
equivalence classes and that all constraints and disequality info is related to
non-trivial classes. In the worst case, we can simplify only one symbol of one
class in each iteration. The number of symbols in one class cannot grow b/c we
replace the old symbol with the simplified one. Also, the number of the
equivalence classes can decrease only, b/c the algorithm does a merge operation
optionally. We need N iterations in this case to reach the fixpoint. Thus, the
steps needed to be done in the worst case is proportional to `N*N`. Empirical
results (attached) show that there is some hardly noticeable run-time and peak
memory discrepancy compared to the baseline. In my opinion, these differences
could be the result of measurement error.
This worst case scenario can be extended to that cases when we have trivial
classes in the constraints and in the disequality map are transforming to such
a State where there are only non-trivial classes, b/c the algorithm does merge
operations. A merge operation on two trivial classes results in one non-trivial
class.
Differential Revision: https://reviews.llvm.org/D106823
We can reuse the "adjustment" handling logic in the higher level
of the solver by calling `State->assume`.
Differential Revision: https://reviews.llvm.org/D112296
Initiate the reorganization of the equality information during symbol
simplification. E.g., if we bump into `c + 1 == 0` during simplification
then we'd like to express that `c == -1`. It makes sense to do this only
with `SymIntExpr`s.
Reviewed By: steakhal
Differential Revision: https://reviews.llvm.org/D111642
Prior to this, the solver was only able to verify whether two symbols
are equal/unequal, only when constants were involved. This patch allows
the solver to work over ranges as well.
Reviewed By: steakhal, martong
Differential Revision: https://reviews.llvm.org/D106102
Patch by: @manas (Manas Gupta)
Summary:
`a % b != 0` implies that `a != 0` for any `a` and `b`. This patch
extends the ConstraintAssignor to do just that. In fact, we could do
something similar with division and in case of multiplications we could
have some other inferences, but I'd like to keep these for future
patches.
Fixes https://bugs.llvm.org/show_bug.cgi?id=51940
Reviewers: noq, vsavchenko, steakhal, szelethus, asdenyspetrov
Subscribers:
Differential Revision: https://reviews.llvm.org/D110357
In this patch we store a reference to `RangedConstraintManager` in the
`ConstraintAssignor`. This way it is possible to call back and reuse some
functions of it. This patch is exclusively needed for its child patches,
it is not intended to be a standalone patch.
Differential Revision: https://reviews.llvm.org/D111640
In this patch we simply move the definition of RangeConstraintManager before
the definition of ConstraintAssignor. This patch is exclusively needed for it's
child patch, so in the child the diff would be clean and the review would be
easier.
Differential Revision: https://reviews.llvm.org/D110387
The solver's symbol simplification mechanism was not able to handle cases
when a symbol is simplified to a concrete integer. This patch adds the
capability.
E.g., in the attached lit test case, the original symbol is `c + 1` and
it has a `[0, 0]` range associated with it. Then, a new condition `c == 0`
is assumed, so a new range constraint `[0, 0]` comes in for `c` and
simplification kicks in. `c + 1` becomes `0 + 1`, but the associated
range is `[0, 0]`, so now we are able to realize the contradiction.
Differential Revision: https://reviews.llvm.org/D110913
There is an error in the implementation of the logic of reaching the `Unknonw` tristate in CmpOpTable.
```
void cmp_op_table_unknownX2(int x, int y, int z) {
if (x >= y) {
// x >= y [1, 1]
if (x + z < y)
return;
// x + z < y [0, 0]
if (z != 0)
return;
// x < y [0, 0]
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
}
}
```
We miss the `FALSE` warning because the false branch is infeasible.
We have to exploit simplification to discover the bug. If we had `x < y`
as the second condition then the analyzer would return the parent state
on the false path and the new constraint would not be part of the State.
But adding `z` to the condition makes both paths feasible.
The root cause of the bug is that we reach the `Unknown` tristate
twice, but in both occasions we reach the same `Op` that is `>=` in the
test case. So, we reached `>=` twice, but we never reached `!=`, thus
querying the `Unknonw2x` column with `getCmpOpStateForUnknownX2` is
wrong.
The solution is to ensure that we reached both **different** `Op`s once.
Differential Revision: https://reviews.llvm.org/D110910
Stop using APInt constructors and methods that were soft-deprecated in
D109483. This fixes all the uses I found in clang.
Differential Revision: https://reviews.llvm.org/D110808
This change is an extension to D103967 where I added dump methods for
(dis)equality classes of the State. There, the (dis)equality classes and their
contents are dumped in an ordered fashion, they are ordered based on their
string representation. This is very useful once we start to use FileCheck to
test the State dump in certain tests.
Differential Revision: https://reviews.llvm.org/D106642
https://bugs.llvm.org/show_bug.cgi?id=51109
When we merged two classes, `*this` became an obsolete representation of
the new `State`. This is b/c the member relations had changed during the
previous merge of another member of the same class in a way that `*this`
had no longer any members. (`mergeImpl` might keep the member relations
to `Other` and could dissolve `*this`.)
Differential Revision: https://reviews.llvm.org/D106285
../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
Differential Revision: https://reviews.llvm.org/D106063
