Age | Commit message (Collapse) | Author |
|
(1) libAnalysis is a generic analysis library that can be used by
Sema. It defines the CFG, basic dataflow analysis primitives, and
inexpensive flow-sensitive analyses (e.g. LiveVariables).
(2) libChecker contains the guts of the static analyzer, incuding the
path-sensitive analysis engine and domain-specific checks.
Now any clients that want to use the frontend to build their own tools
don't need to link in the entire static analyzer.
This change exposes various obvious cleanups that can be made to the
layout of files and headers in libChecker. More changes pending. :)
This change also exposed a layering violation between AnalysisContext
and MemRegion. BlockInvocationContext shouldn't explicitly know about
BlockDataRegions. For now I've removed the BlockDataRegion* from
BlockInvocationContext (removing context-sensitivity; although this
wasn't used yet). We need to have a better way to extend
BlockInvocationContext (and any LocationContext) to add
context-sensitivty.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@94406 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
GRStateManager. Having these references was an abstraction violation,
as they really should only be known about GRExprEngine.
This change required adding a new 'ProcessAssume' callback in
GRSubEngine. GRExprEngine implements this callback by calling
'EvalAssume' on all registered Checker objects as well as the
registered GRTransferFunc object.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@92549 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@90028 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@81346 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@74136 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@73735 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Remove the 'isFeasible' flag from all uses of 'Assume'.
- Remove the 'Assume' methods from GRStateManager. Now the only way to
create a new GRState with an assumption is to use the new 'assume' methods
in GRState.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@73731 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@73648 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
ConstraintManager:
- constify getSymVal()
BasicConstraintManager:
- Pull out logic that would be common to ConstraintManagers of a similar nature
and put them in a parent class called 'SimpleConstraintManager'.
RangeConstraintManager:
- Added a new prototype ConstraintManager to track ranges of variables! This
ConstraintManager keeps tracks of ranges of concrete integers that a symbolic
integer may have.
AnalysisConsumer:
- Add driver option to use RangeConstraintManager with GRExprEngine-based
analyses.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@64558 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
do the symblic regions associated with them and we need them to be typed.
Current SymbolicRegion::getRValueType() method is very restricting. It may be
modified when we are more clear about what could be the types of symblic
regions.
BasicConstraintManager::Assume() is changed due to that now SymblicRegion is a
subclass of SubRegion.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@63844 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@63363 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@63249 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
'ConstEq'. This avoids collisions in the GDM.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@63002 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
their associated APIs. We no longer need separate SymbolData objects
for fields, variables, etc. Instead, we now associated symbols with
the "rvalue" of a MemRegion (i.e., the value stored at that region).
Now we only have two kinds of SymbolData objects: SymbolRegionRValue
and SymbolConjured.
This cleanup also makes the distinction between a SymbolicRegion and a
symbolic value that is a location much clearer. A SymbolicRegion
represents a chunk of symbolic memory, while a symbolic location is
just a "pointer" with different possible values. Without any specific
knowledge, a symbolic location resolves (i.e., via a dereference) to a
SymbolicRegion. In the future, when we do better alias reasoning, a
symbolic location can become an alias for another location, thus
merging the constraints on the referred SymbolicRegion with the other
region.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@62769 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
called "SymbolReaper". Right now it just consolidates the two and cleans up some client code, but shortly it will be used to enable "lazy computation" of live symbols for use with RegionStore.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@62722 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Fix regression reported in <rdar://problem/6452745>. After a null check, null references to resources should not have a retain count. This regression was caused by removing the call to "GRTransferFuncs::EvalAssume" in BasicConstraintManager.
- Added a test case to test this behavior.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@61155 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
the representation of symbolic values.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60575 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Fix nonsensical logic in AssumeSymGE. When comparing 'sym >= constant' and the
constant is the maximum integer value, add the constraint that 'sym ==
constant' when the path is deemed feasible. All other cases are feasible.
- Improve AssumeSymGT. When comparing 'sym > constant' and constant is the
maximum integer value we know the path is infeasible.
- Add test case for this enhancement to AssumeSymGT.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60490 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Fix nonsensical logic in AssumeSymLE. When comparing 'sym <= constant' and the
constant is the minimum integer value, add the constraint that 'sym ==
constant' when the path is deemed feasible. All other cases are feasible.
- Improve AssumeSymLT to address <rdar://problem/6407949>. When comparing
'sym < constant' and constant is the minimum integer value we know the
path is infeasible.
- Add test case for <rdar://problem/6407949>.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60489 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60151 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60146 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
There might be other, similar bugs lurking there.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@59974 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
ConcreteInt index for now.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@59869 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
migrating the output in analyzer to llvm::raw_ostream.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@58965 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
the Store.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@58182 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
regions and symbolic regions. When assuming whether or not a location is non-null, walk up the region hierarchy until we hit a symbolic region (and test it for null). This may not be the end all solution, as the notion of what a "symbolic region" is really belongs in the specific subclass of StoreManager.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@57730 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
RVal => SVal
LVal => Loc
NonLVal => NonLoc
lval => loc
nonlval => nonloc
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@57671 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
regions.
Remove GRExprEngine::getLVal and RValues::MakeVal.
Enhance StoreManager "GetLValue" methods to dispatch for specific kinds of lvalue queries, as opposed to interogating the expression tree (GRExprEngine already does this).
Added FIXMEs. In particular, we no longer "assume" that a base pointer in a field/array access is null (this logic was removed). Perhaps we should do this when fetching the lvalue for fields and array elements?
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@57657 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
the patch consists of deltas due to API changes.
This patch overhauls the "memory region" abstraction that was prototyped (but never really used) as part of the Store.h. This patch adds MemRegion.h and MemRegion.cpp, which defines the class MemRegion and its subclasses. This classes serve to define an abstract representation of memory, with regions being layered on other regions to to capture the relationships between fields and variables, variables and the address space they are allocated in, and so on.
The main motivation of this patch is that key parts of the analyzer assumed that all value bindings were to VarDecls. In the future this won't be the case, and this patch removes lval::DeclVal and replaces it with lval::MemRegionVal. Now all pieces of the analyzer must reason about abstract memory blocks instead of just variables.
There should be no functionality change from this patch, but it opens the door for significant improvements to the analyzer such as field-sensitivity and object-sensitivity, both which were on hold until the memory abstraction got generalized.
The memory region abstraction also allows type-information to literally be affixed to a memory region. This will allow the some now redundant logic to be removed from the retain/release checker.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@57042 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
For checking if a symbol >= value, we need to check if symbol == value || symbol
> value. When checking symbol > value and we know that symbol != value, the path
is infeasible only if value == maximum integer.
For checking if a symbol <= value, we need to check if symbol == value || symbol
< value. When checking symbol < value and we know that symbol != value, the path
is infeasible only if value == minimum integer.
Updated test case exercising this logic: we only prune paths if the values are
unsigned.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@56354 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@56334 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
if we know that 'len != 0' and know that 'i == 0' then we know that
'i < len' must evaluate to true and cannot evaluate to false
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@56260 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55559 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55537 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55536 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55412 91177308-0d34-0410-b5e6-96231b3b80d8
|