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
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
to reflect the new license.
We understand that people may be surprised that we're moving the header
entirely to discuss the new license. We checked this carefully with the
Foundation's lawyer and we believe this is the correct approach.
Essentially, all code in the project is now made available by the LLVM
project under our new license, so you will see that the license headers
include that license only. Some of our contributors have contributed
code under our old license, and accordingly, we have retained a copy of
our old license notice in the top-level files in each project and
repository.
llvm-svn: 351636
Summary: SimpleConstraintManager is difficult to use, and makes assumptions about capabilities of the constraint manager. This patch refactors out those portions into a new RangedConstraintManager, and also fixes some issues with camel case, formatting, and confusing naming.
Reviewers: zaks.anna, dcoughlin
Subscribers: mgorny, xazax.hun, NoQ, rgov, cfe-commits
Differential Revision: https://reviews.llvm.org/D26061
llvm-svn: 296242
Summary: It breaks the build for the ASTMatchers
Subscribers: klimek, cfe-commits
Differential Revision: http://reviews.llvm.org/D13893
llvm-svn: 250827
Previously, every call to a ConstraintManager's isNull would do a full
assumeDual to test feasibility. Now, ConstraintManagers can override
checkNull if they have a cheaper way to do the same thing.
RangeConstraintManager can do this in less than half the work.
<rdar://problem/12608209>
llvm-svn: 167138
with at least one subtle bug in MacOSXKeyChainAPIChecker where the
calling the method was a substitute for assuming a symbolic value
was null (which is not the case).
We still keep ConstraintManager::getSymVal(), but we use that as
an optimization in SValBuilder and ProgramState::getSVal() to
constant-fold SVals. This is only if the ConstraintManager can
provide us with that information, which is no longer a requirement.
As part of this, introduce a default implementation of
ConstraintManager::getSymVal() which returns null.
For Checkers, introduce ConstraintManager::isNull(), which queries
the state to see if the symbolic value is constrained to be a null
value. It does this without assuming it has been implicitly constant
folded.
llvm-svn: 163428
