forked from OSchip/llvm-project
Rename AnalyzerOptions 'EagerlyAssume' to 'eagerlyAssumeBinOpBifurcation'.
llvm-svn: 162930
This commit is contained in:
parent
8756c4a1a9
commit
6f5131f149
|
@ -109,14 +109,13 @@ public:
|
|||
/// \brief The flag regulates if we should eagerly assume evaluations of
|
||||
/// conditionals, thus, bifurcating the path.
|
||||
///
|
||||
/// EagerlyAssume - A flag indicating how the engine should handle
|
||||
/// expressions such as: 'x = (y != 0)'. When this flag is true then
|
||||
/// the subexpression 'y != 0' will be eagerly assumed to be true or false,
|
||||
/// thus evaluating it to the integers 0 or 1 respectively. The upside
|
||||
/// is that this can increase analysis precision until we have a better way
|
||||
/// to lazily evaluate such logic. The downside is that it eagerly
|
||||
/// bifurcates paths.
|
||||
unsigned EagerlyAssume : 1;
|
||||
/// This flag indicates how the engine should handle expressions such as: 'x =
|
||||
/// (y != 0)'. When this flag is true then the subexpression 'y != 0' will be
|
||||
/// eagerly assumed to be true or false, thus evaluating it to the integers 0
|
||||
/// or 1 respectively. The upside is that this can increase analysis
|
||||
/// precision until we have a better way to lazily evaluate such logic. The
|
||||
/// downside is that it eagerly bifurcates paths.
|
||||
unsigned eagerlyAssumeBinOpBifurcation : 1;
|
||||
|
||||
unsigned TrimGraph : 1;
|
||||
unsigned VisualizeEGDot : 1;
|
||||
|
@ -150,7 +149,7 @@ public:
|
|||
AnalyzeAll = 0;
|
||||
AnalyzerDisplayProgress = 0;
|
||||
AnalyzeNestedBlocks = 0;
|
||||
EagerlyAssume = 0;
|
||||
eagerlyAssumeBinOpBifurcation = 0;
|
||||
TrimGraph = 0;
|
||||
VisualizeEGDot = 0;
|
||||
VisualizeEGUbi = 0;
|
||||
|
|
|
@ -396,14 +396,14 @@ public:
|
|||
ExplodedNode *Pred,
|
||||
ExplodedNodeSet &Dst);
|
||||
|
||||
/// evalEagerlyAssume - Given the nodes in 'Src', eagerly assume symbolic
|
||||
/// evalEagerlyAssumeBinOpBifurcation - Given the nodes in 'Src', eagerly assume symbolic
|
||||
/// expressions of the form 'x != 0' and generate new nodes (stored in Dst)
|
||||
/// with those assumptions.
|
||||
void evalEagerlyAssume(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
|
||||
void evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
|
||||
const Expr *Ex);
|
||||
|
||||
std::pair<const ProgramPointTag *, const ProgramPointTag*>
|
||||
getEagerlyAssumeTags();
|
||||
geteagerlyAssumeBinOpBifurcationTags();
|
||||
|
||||
SVal evalMinus(SVal X) {
|
||||
return X.isValid() ? svalBuilder.evalMinus(cast<NonLoc>(X)) : X;
|
||||
|
|
|
@ -159,7 +159,7 @@ static void AnalyzerOptsToArgs(const AnalyzerOptions &Opts, ToArgsList &Res) {
|
|||
Res.push_back("-analyzer-display-progress");
|
||||
if (Opts.AnalyzeNestedBlocks)
|
||||
Res.push_back("-analyzer-opt-analyze-nested-blocks");
|
||||
if (Opts.EagerlyAssume)
|
||||
if (Opts.eagerlyAssumeBinOpBifurcation)
|
||||
Res.push_back("-analyzer-eagerly-assume");
|
||||
if (Opts.TrimGraph)
|
||||
Res.push_back("-trim-egraph");
|
||||
|
@ -1123,7 +1123,7 @@ static bool ParseAnalyzerArgs(AnalyzerOptions &Opts, ArgList &Args,
|
|||
Opts.AnalyzerDisplayProgress = Args.hasArg(OPT_analyzer_display_progress);
|
||||
Opts.AnalyzeNestedBlocks =
|
||||
Args.hasArg(OPT_analyzer_opt_analyze_nested_blocks);
|
||||
Opts.EagerlyAssume = Args.hasArg(OPT_analyzer_eagerly_assume);
|
||||
Opts.eagerlyAssumeBinOpBifurcation = Args.hasArg(OPT_analyzer_eagerly_assume);
|
||||
Opts.AnalyzeSpecificFunction = Args.getLastArgValue(OPT_analyze_function);
|
||||
Opts.UnoptimizedCFG = Args.hasArg(OPT_analysis_UnoptimizedCFG);
|
||||
Opts.CFGAddImplicitDtors = Args.hasArg(OPT_analysis_CFGAddImplicitDtors);
|
||||
|
|
|
@ -646,7 +646,7 @@ PathDiagnosticPiece *ConditionBRVisitor::VisitNodeImpl(const ExplodedNode *N,
|
|||
// violation.
|
||||
const std::pair<const ProgramPointTag *, const ProgramPointTag *> &tags =
|
||||
cast<GRBugReporter>(BRC.getBugReporter()).
|
||||
getEngine().getEagerlyAssumeTags();
|
||||
getEngine().geteagerlyAssumeBinOpBifurcationTags();
|
||||
|
||||
const ProgramPointTag *tag = PS->getTag();
|
||||
if (tag == tags.first)
|
||||
|
|
|
@ -704,11 +704,11 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
|
|||
|
||||
Bldr.takeNodes(Pred);
|
||||
|
||||
if (AMgr.options.EagerlyAssume &&
|
||||
if (AMgr.options.eagerlyAssumeBinOpBifurcation &&
|
||||
(B->isRelationalOp() || B->isEqualityOp())) {
|
||||
ExplodedNodeSet Tmp;
|
||||
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Tmp);
|
||||
evalEagerlyAssume(Dst, Tmp, cast<Expr>(S));
|
||||
evalEagerlyAssumeBinOpBifurcation(Dst, Tmp, cast<Expr>(S));
|
||||
}
|
||||
else
|
||||
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
|
||||
|
@ -924,10 +924,10 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
|
|||
case Stmt::UnaryOperatorClass: {
|
||||
Bldr.takeNodes(Pred);
|
||||
const UnaryOperator *U = cast<UnaryOperator>(S);
|
||||
if (AMgr.options.EagerlyAssume && (U->getOpcode() == UO_LNot)) {
|
||||
if (AMgr.options.eagerlyAssumeBinOpBifurcation && (U->getOpcode() == UO_LNot)) {
|
||||
ExplodedNodeSet Tmp;
|
||||
VisitUnaryOperator(U, Pred, Tmp);
|
||||
evalEagerlyAssume(Dst, Tmp, U);
|
||||
evalEagerlyAssumeBinOpBifurcation(Dst, Tmp, U);
|
||||
}
|
||||
else
|
||||
VisitUnaryOperator(U, Pred, Dst);
|
||||
|
@ -1736,15 +1736,17 @@ void ExprEngine::evalLocation(ExplodedNodeSet &Dst,
|
|||
}
|
||||
|
||||
std::pair<const ProgramPointTag *, const ProgramPointTag*>
|
||||
ExprEngine::getEagerlyAssumeTags() {
|
||||
ExprEngine::geteagerlyAssumeBinOpBifurcationTags() {
|
||||
static SimpleProgramPointTag
|
||||
EagerlyAssumeTrue("ExprEngine : Eagerly Assume True"),
|
||||
EagerlyAssumeFalse("ExprEngine : Eagerly Assume False");
|
||||
return std::make_pair(&EagerlyAssumeTrue, &EagerlyAssumeFalse);
|
||||
eagerlyAssumeBinOpBifurcationTrue("ExprEngine : Eagerly Assume True"),
|
||||
eagerlyAssumeBinOpBifurcationFalse("ExprEngine : Eagerly Assume False");
|
||||
return std::make_pair(&eagerlyAssumeBinOpBifurcationTrue,
|
||||
&eagerlyAssumeBinOpBifurcationFalse);
|
||||
}
|
||||
|
||||
void ExprEngine::evalEagerlyAssume(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
|
||||
const Expr *Ex) {
|
||||
void ExprEngine::evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst,
|
||||
ExplodedNodeSet &Src,
|
||||
const Expr *Ex) {
|
||||
StmtNodeBuilder Bldr(Src, Dst, *currBldrCtx);
|
||||
|
||||
for (ExplodedNodeSet::iterator I=Src.begin(), E=Src.end(); I!=E; ++I) {
|
||||
|
@ -1762,7 +1764,7 @@ void ExprEngine::evalEagerlyAssume(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
|
|||
nonloc::SymbolVal *SEV = dyn_cast<nonloc::SymbolVal>(&V);
|
||||
if (SEV && SEV->isExpression()) {
|
||||
const std::pair<const ProgramPointTag *, const ProgramPointTag*> &tags =
|
||||
getEagerlyAssumeTags();
|
||||
geteagerlyAssumeBinOpBifurcationTags();
|
||||
|
||||
// First assume that the condition is true.
|
||||
if (ProgramStateRef StateTrue = state->assume(*SEV, true)) {
|
||||
|
|
Loading…
Reference in New Issue