-
Notifications
You must be signed in to change notification settings - Fork 79
Forward dataflow analysis for collecting comparison facts #657
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
…into collect-facts
@dtarditi I believe this PR is ready for a review of this stage. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great start! I have a number of suggestions for the code.
lib/Sema/SemaBounds.cpp
Outdated
// - Expr1 <= Expr2 | ||
// - Expr2 > Expr1 | ||
// - Expr2 >= Expr1 | ||
void ExtractComparisons(const Stmt *St, ComparisonSet &ISet) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can St be an Expression? I'd like you to use the Expr::ignoreParens() method to ignore parenthesis, so that this is more general.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure.
lib/Sema/SemaBounds.cpp
Outdated
// This function looks recursively for comparisons in statement `S`. | ||
// Then, it records them as elements of type Comparison in `ISet`. | ||
// Each Comparison is a pair in form of (Expr1, Expr2) where both | ||
// Expr1 and Expr2 are of type Expr*. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The comment is confusing. It should just say that for each expression, Expr1 <= Expr2 holds.
lib/Sema/SemaBounds.cpp
Outdated
@@ -3285,6 +3288,318 @@ namespace { | |||
}; | |||
} | |||
|
|||
namespace { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the code for this analysis should be broken out into separate files: a .h file for the class declaration and cpp for the class implementation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
lib/Sema/SemaBounds.cpp
Outdated
@@ -1491,6 +1492,8 @@ Expr *Sema::MakeAssignmentImplicitCastExplicit(Expr *E) { | |||
|
|||
namespace { | |||
class CheckBoundsDeclarations { | |||
public: | |||
typedef llvm::SmallPtrSet<const Stmt *, 16> StmtSet; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Instead of hard-wiring 16 into the code, can we use a constant expression?
lib/Sema/SemaBounds.cpp
Outdated
} | ||
|
||
// This function fills `ComparisonFacts` with pairs (Expr1, Expr2) where | ||
// Expr1 < Expr2, Expr1 <= Expr2, Expr2 > Expr1, or Expr2 >= Expr1. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this comment is confusing. The invariant is that Expr1 <= Expr2.
lib/Sema/SemaBounds.cpp
Outdated
} | ||
|
||
// Given a set of Comparisons `InputSet`, this function negates them | ||
// by swaping the element of pairs, and records them in `OutputSet`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Typo: swaping->swapping.
test/CheckedC/dump-dataflow-facts.c
Outdated
@@ -0,0 +1,213 @@ | |||
// Tests for dumping of datafow analysis for collecting facts | |||
// | |||
// RUN: %clang_cc1 -DDEBUG_DATAFLOW -fcheckedc-extension %s 2>&1 | FileCheck %s |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You need to add a compiler flag. After the analysis, you'd check the compiler flag and dump the results accordingly. You can look at the recent commit by @mgrang to see how to do this.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done. The new flag is -fdump-extracted-comparison-facts.
test/CheckedC/dump-dataflow-facts.c
Outdated
b = c; | ||
} | ||
|
||
// CHECK: { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should include block number information. Otherwise this will be very difficult to debug in the future.
Could you add more test cases for more complicated expressions?
lib/Sema/SemaBounds.cpp
Outdated
WorkList.push(GetByCFGBlock(*I)); | ||
} | ||
|
||
//if(DEBUG_DATAFLOW) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This needs to be moved out to a separate routine. The dumps should be controlled by a compiler flag.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
lib/Sema/SemaBounds.cpp
Outdated
return false; | ||
} | ||
|
||
// This function looks recursively for comparisons in statement `S`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the proper invariant is this: this function computes a list of comparisons E1 <= E2 that will be true if the expression S evaluates to true. Clearly if S is simple direct comparison expression E3 op E4, a comparison can be created if op is one of LE, LT, GE, GT, or EQ. If S has the form A && B, comparisons can be created for A and B.
Could you add a TODO for handling logical negation the (!
) operator?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
We also need to conservative in the set of comparisons that we collect with respect to pointers and calls.
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hi Pardis,
I've left some comments in the PR for your consideration.
Thank you,
Sunny
lib/Sema/SemaBounds.cpp
Outdated
@@ -1520,6 +1521,8 @@ Expr *Sema::MakeAssignmentImplicitCastExplicit(Expr *E) { | |||
|
|||
namespace { | |||
class CheckBoundsDeclarations { | |||
public: | |||
typedef llvm::SmallPtrSet<const Stmt *, 16> StmtSet; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: "using" is the preferred syntax over C-style typedef :) Similar suggestion for other places where you've used a typedef.
lib/Sema/SemaBounds.cpp
Outdated
ComparisonSet Kill, GenThen, GenElse; | ||
|
||
public: | ||
ElevatedCFGBlock(const CFGBlock *Block) : Block(Block) {} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: ElevatedCFGBlock(const CFGBlock *Block) : Block(Block) {} -> Can we use a different variable name than the data member?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@sunnychatterjee I followed a similar naming convention that appears in the existing constructors in this file. Should I change it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@ppashakhanloo You don't have to change this if it appears in the existing convention. Personally, I don't prefer this style since you have to qualify member access with a "this" in such cases.
lib/Sema/SemaBounds.cpp
Outdated
|
||
class ElevatedCFGBlock { | ||
private: | ||
const CFGBlock *Block; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we add default initializations for the data members? For example:
private:
const CFGBlock *Block = nullptr;
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similarly, for other data members.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@sunnychatterjee ElevatedCFGBlock has one constructor with const CFGBlock *Block
as input. And there is no default constructor for it. I am not sure why we need to add default initializations for the data members here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@ppashakhanloo For a single data member like in your example, it's fine. I usually follow the rule to always initialize data members of the object: http://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines#Res-always.
This way, we avoid errors when constructors sometimes don't initialize all the data members of a class.
lib/Sema/SemaBounds.cpp
Outdated
public: | ||
ElevatedCFGBlock(const CFGBlock *Block) : Block(Block) {} | ||
|
||
friend class AvailableFactsAnalysis; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
friend class AvailableFactsAnalysis; --> Is there a way to avoid the "friend"? For example, we can have public methods to access the data members of "ElevatedCFGBlock".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@sunnychatterjee I used friend
since AvailableFactsAnalysis
should be the only class that manipulates an object of ElevatedCFGBlock
. (I thought of it as an Iterator class.)
If I make public methods to access the data members of it, I think I share more than necessary with the world outside AvailableFactsAnalysis
. Is there a better way to achieve this goal?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@ppashakhanloo Thanks for the explanation. I try to avoid "friend" wherever possible since it tends to break encapsulation. However, there are exceptions to this like iterators as you mention. Given that the two classes are so close to each other (nested), let's leave them as is.
lib/Sema/SemaBounds.cpp
Outdated
if (Block->getBlockID() > MaxBlockID) | ||
MaxBlockID = Block->getBlockID(); | ||
|
||
BlockIDs.resize(MaxBlockID + 1, 0); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we clear BlockIDs before calling resize?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
lib/Sema/SemaBounds.cpp
Outdated
WorkList.push(GetByCFGBlock(*I)); | ||
} | ||
|
||
//if(DEBUG_DATAFLOW) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You meant to remove the comment here right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I added a compiler flag for debugging purposes and removed this comment.
lib/Sema/SemaBounds.cpp
Outdated
return Blocks[BlockIDs[B->getBlockID()]]; | ||
} | ||
|
||
// Given two sets S1 and S2, the return value is S1 \ S2. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: You meant: S1 - S2, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@sunnychatterjee I will change this comment to S1 - S2
for more clarity. I meant \
which is the set difference operator.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@ppashakhanloo This was a clarifying question. Feel free keep the set difference operator.
lib/Sema/SemaBounds.cpp
Outdated
if (const Expr *E = dyn_cast<Expr>(St)) | ||
AllExprs.insert(E); | ||
for (auto I = St->child_begin(); I != St->child_end(); ++I) | ||
CollectExpressions(*I, AllExprs); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can use range-for loop here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done!
lib/Sema/SemaBounds.cpp
Outdated
CollectDefinedVars(*I, DefinedVars); | ||
} | ||
|
||
//#if DEBUG_DATAFLOW |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You meant to remove the comment for DEBUG_DATAFLOW, right? I'd expect the pattern to look like this in the production code. Alternatively, you can use some debug flags to enable this.
#DEBUG_DATAFLOW 0 // Set this to 1 for debugging
#if DEBUG_DATAFLOW
...
#endif // DEBUG_DATAFLOW
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I removed this comment and added a new compiler flag which is only used when testing the functionality of this part of the code.
lib/Sema/SemaBounds.cpp
Outdated
@@ -3394,8 +3726,11 @@ void Sema::CheckFunctionBodyBoundsDecls(FunctionDecl *FD, Stmt *Body) { | |||
ComputeBoundsDependencies(Tracker, FD, Body); | |||
std::unique_ptr<CFG> Cfg = CFG::buildCFG(nullptr, Body, &getASTContext(), CFG::BuildOptions()); | |||
CheckBoundsDeclarations Checker(*this, Body, Cfg.get(), FD->getBoundsExpr()); | |||
if (Cfg != nullptr) | |||
AvailableFactsAnalysis Collector(*this, Cfg.get()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Move this inside the if-block below.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The tests for assignments via pointers or dereferences via pointers need to be corrected.
The operators are defined in clang/include/clang/AST/OperationKinds.def. The *'
, '->and
[]` operators all produce lvalues. In the clang AST, memory is read by using an LValueToRvalue Cast. Memory is modified in the lvalue appearing as the left-hand side of an assignment or as the subexpression of increment or decrement operator.
@@ -169,7 +169,6 @@ CODEGENOPT(CoverageMapping , 1, 0) ///< Generate coverage mapping regions to | |||
///< enable code coverage analysis. | |||
CODEGENOPT(DumpCoverageMapping , 1, 0) ///< Dump the generated coverage mapping | |||
///< regions. | |||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It appears a newline was deleted here. Could you add it back?
include/clang/Driver/Options.td
Outdated
@@ -2625,6 +2625,9 @@ def : Flag<["-"], "integrated-as">, Alias<fintegrated_as>, Flags<[DriverOption]> | |||
def : Flag<["-"], "no-integrated-as">, Alias<fno_integrated_as>, | |||
Flags<[CC1Option, DriverOption]>; | |||
|
|||
def fdump_extracted_comparison_facts : Flag<["-"], "fdump-extracted-comparison-facts">, Group<f_Group>, Flags<[CC1Option]>, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you move this next to the other Checked C flags? The flags beging at def fcheckedc_extension.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
|
||
bool AvailableFactsAnalysis::ContainsFunctionCall(const Expr *E) { | ||
if (const DeclRefExpr *DRE = dyn_cast<DeclRefExpr>(E)) | ||
if (const FunctionDecl *FD = dyn_cast<FunctionDecl>(DRE->getDecl())) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This isn't the right check for whether an expression contains a call expression. You should for CallExpr, not the presence of a function call.
@dtarditi I addressed your comments and added more tests. The code is ready for review. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have some additional suggestions for the code. I think you can simplify the code by using the existing function Sema::CheckIsNonModifying also. You'll want to pass an argument so that CheckIsNonModifying doesn't report an error if it s find a modifying expression.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
return true; | ||
} | ||
if (const CallExpr *CE = dyn_cast<CallExpr>(E)) { | ||
for (int ArgIndex = 0; ArgIndex < CE->getNumArgs(); ArgIndex++) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any call expression must be considered as possibly doing a pointer assignment. We should not consider the types of the arguments passed to the function call. It's possible that a pointer could be accessible to a function via a global variable or through a structure type.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
return false; | ||
} | ||
|
||
// This function return true if an expression is volatile, and false otherwise. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Typo: return->returns
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
// - If the child of `E` is `e`, then `f(e)` must be true. `f(e)` is defined in | ||
// a separate function `IsPointerDerefLValue`. | ||
// Otherwise, the function returns false; | ||
bool AvailableFactsAnalysis::IsPointerDeref(const Expr *E) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You need to check whether E contains a pointer dereference. That means you need to check the children recursively also. I think you should rename this function.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
return false; | ||
} | ||
|
||
bool AvailableFactsAnalysis::IsPointerAssignment(const Expr *E) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You need to check whether E contains a pointer assignment. You need to recursively check the children too. I think you should rename this function.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
CollectExpressions(I.first, Exprs); | ||
CollectExpressions(I.second, Exprs); | ||
for (auto InnerExpr : Exprs) | ||
if (const DeclRefExpr *DRE = dyn_cast<DeclRefExpr>(InnerExpr)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A variable v produces an lvalue. For the variable to be used, the lvalue must be the used by an LValueToRValue cast expression.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for explaining this. Fixed.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
// - `E` has the form `E1 && E2`: ExtractComparisons in E1 and E2 and add them to `ISet`. | ||
// TODO: handle the case where logical negation operator (!) is used. | ||
void AvailableFactsAnalysis::ExtractComparisons(const Expr *E, ComparisonSet &ISet) { | ||
if (IsVolatile(E) || ContainsCallExpr(E)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can use the function Sema::CheckIsNonModifying instead.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
// - `E` has the form `E1 || E2`: ExtractNegatedComparisons in E1 and E2 and add | ||
// them to `ISet`. | ||
void AvailableFactsAnalysis::ExtractNegatedComparisons(const Expr *E, ComparisonSet &ISet) { | ||
if (IsVolatile(E) || ContainsCallExpr(E)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can use the function Sema::CheckIsNonModifying instead.
lib/Sema/AvailableFactsAnalysis.cpp
Outdated
|
||
// This function return true if an expression is volatile, and false otherwise. | ||
// An expression is volatile if there is at least one volatile variable in it. | ||
bool AvailableFactsAnalysis::IsVolatile(const Expr *E) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is overly conservative: it would flag an expression that used &v, where v is a volatile variable, as being volatile. I suggest that you use the existing function CheckIsNonModifying in the functions that are calling this instead.
// We assume a variable is defined if it appears in the lhs of an assignment: | ||
// 1. increment or decrement operator (a++) | ||
// 2. assignment operator (a += 1, a = 2) | ||
void AvailableFactsAnalysis::CollectDefinedVars(const Stmt *St, std::set<const VarDecl *> &DefinedVars) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This function could miss some definitions of variables. In the unary operator case, the expression being incremented/decremented could be parenthesized. In both cases, the LValueBitCast could also be parenthesized. I think you need a loop that ignores parentheses and lvalue bit casts until nothing changes. This should be factored into a separate function.
lib/Sema/SemaBounds.cpp
Outdated
return false; | ||
|
||
bool EqualWithoutFacts = EqualValue(Ctx, VariablePart1, VariablePart2, EquivExprs); | ||
bool LEWithFacts = FactExists(Ctx, VariablePart1, VariablePart2, EquivExprs, Facts); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The logic would be clearer to return true if EqualWithoutFact is true, and similarly return true if LEWtihFacts is true. Then return false otherwise.
@dtarditi Thanks for your comments. I addressed all of them. |
…into collect-facts
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good! Thank you.
There is one change in a comment that I'd like you to make. I don't need to re-review it before you complete the PR.
lib/Sema/SemaBounds.cpp
Outdated
@@ -2151,6 +2156,62 @@ namespace { | |||
return true; | |||
} | |||
|
|||
// This function is an extension of EqualExtended. It looks into the provided `Facts` | |||
// in order to prove `Base1 + Offset1 <= Offset2 + Offset2`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There's typo here: Offset2 is used twice.
Could you add a TODO comment: we are ignoring the possibility of overflow in the addition.
The most important changes: - Clean up the multi-decl detection and rewriting code, and unify the code paths for global variables, fields, and local variables. - Automatically generate names for unnamed inline structs if they need to be rewritten, and remove 3C's previous workarounds that tried to avoid needing to rewrite multi-decls with unnamed inline structs that 3C couldn't handle correctly. - Inside a struct, when rewriting a field multi-decl that contains an inline struct, correctly detect the presence of the inline struct to avoid losing it completely, and additionally move it to the top level to avoid a compiler warning. - Add support for typedef multi-decls on par with variable and field multi-decls. See correctcomputation#657 for more details.
This pull request adds a forward dataflow analysis for collecting facts in every function for each CFG block.
I have added some new tests under test/CheckedC/dump_dataflow_facts.c.
Some comments still need to be added.The main function that runs the analysis is AvailableFactsAnalysis::Analyze() which implements the iterative worklist algorithm. This function must be called before checking the bounds declarations.
For each CFG block B, the following sets are computed:
For using the collected facts, the following functions can be used:
Representation of the comparison facts: