Skip to content

[analyzer][clang-tidy][NFC] Clean up eagerly-assume handling #112209

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

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion clang-tools-extra/clang-tidy/ClangTidy.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,6 @@ ClangTidyASTConsumerFactory::createASTConsumer(
if (!AnalyzerOptions.CheckersAndPackages.empty()) {
setStaticAnalyzerCheckerOpts(Context.getOptions(), AnalyzerOptions);
AnalyzerOptions.AnalysisDiagOpt = PD_NONE;
AnalyzerOptions.eagerlyAssumeBinOpBifurcation = true;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a functionality loss from Tidy's perspective? AFAIK, there is no way to set CSA analyser engine options when invoked through Tidy.

Copy link
Contributor

@5chmidti 5chmidti Oct 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Clang-Tidy can set CSA options, I recently added support for it for --verify-config in #109523, where I had checked which syntax it has, and if the syntax worked beforehand.

E.g.: clang-analyzer-optin.cplusplus.UninitializedObject:Pedantic: true

Copy link
Contributor Author

@NagyDonat NagyDonat Oct 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, this is not functionality loss from Tidy's perspective, because this data member is dead, its value doesn't influence anything. The eagerly-assume feature is controlled by a different data member AnalyzerOptions.ShouldEagerlyAssume (which is true by default).

std::unique_ptr<ento::AnalysisASTConsumer> AnalysisConsumer =
ento::CreateAnalysisConsumer(Compiler);
AnalysisConsumer->AddDiagnosticConsumer(
Expand Down
13 changes: 6 additions & 7 deletions clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
Original file line number Diff line number Diff line change
Expand Up @@ -299,13 +299,12 @@ ANALYZER_OPTION(

ANALYZER_OPTION(
bool, ShouldEagerlyAssume, "eagerly-assume",
"Whether we should eagerly assume evaluations of conditionals, thus, "
"bifurcating the path. This indicates how the engine should handle "
"expressions such as: 'x = (y != 0)'. When this 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.",
"If this is enabled (the default behavior), when the analyzer encounters "
"a comparison operator or logical negation, it immediately splits the "
"state to separate the case when the expression is true and the case when "
"it's false. 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.",
Comment on lines +306 to +307
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know this part of the change is only because of formatting, but here we are saying that "the downside [of eagerly bifurcating the path] is that it eagerly bifurcates paths", which has a very low information value.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fair point, but I think it's still useful to highlight that bifurcating paths is a downside, not a helpful effect.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My problem is that it does not explain well why it is a downside, considering we have a strong claim "increases analysis precision" in the other sentence.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"the downside [of eagerly bifurcating the path] is that it eagerly bifurcates paths"

I think in this case it's more like "the downside [of eagerly assuming the value of a bool expression] is that it eagerly bifurcates paths"

My problem is that it does not explain well why it is a downside

I think in this case the why is that "it eagerly bifurcates paths".

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think in this case it's more like "the downside [of eagerly assuming the value of a bool expression] is that it eagerly bifurcates paths"

I do not think there is a significant difference here, because the help text, as it stands now, immediately tries to explain what a "bifurcation" is (which one may or may not understand that this is actually the definition of that term) by saying "splits the state to separate […] true and […] false".

So we say that turning this option on will cause bifurcation…

I think in this case the why is that "it eagerly bifurcates paths".

…and then go on and say that the bifurcation (which is the only immediate effect of turning this option on) is a downside.

That still does not explain to me why this would be a problem, and what trade-offs I am making when the benefit is the increased precision. Will it cause more CPU use? Will it make the analysis run longer? Or, conversely, will it actually make it run shorter? There is this claim about a behavioural change with no mentions of the actual observeable difference.

And, remember, these documentation tidbits exist for the user, as it is dumped with the --help flags and similar. Users will not know the intimacies of the analyser's implementation!

true)

ANALYZER_OPTION(
Expand Down
8 changes: 3 additions & 5 deletions clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
Original file line number Diff line number Diff line change
Expand Up @@ -229,8 +229,6 @@ class AnalyzerOptions : public RefCountedBase<AnalyzerOptions> {
unsigned AnalyzerDisplayProgress : 1;
unsigned AnalyzerNoteAnalysisEntryPoints : 1;

unsigned eagerlyAssumeBinOpBifurcation : 1;

unsigned TrimGraph : 1;
unsigned visualizeExplodedGraphWithGraphViz : 1;
unsigned UnoptimizedCFG : 1;
Expand Down Expand Up @@ -293,9 +291,9 @@ class AnalyzerOptions : public RefCountedBase<AnalyzerOptions> {
ShowConfigOptionsList(false),
ShouldEmitErrorsOnInvalidConfigValue(false), AnalyzeAll(false),
AnalyzerDisplayProgress(false), AnalyzerNoteAnalysisEntryPoints(false),
eagerlyAssumeBinOpBifurcation(false), TrimGraph(false),
visualizeExplodedGraphWithGraphViz(false), UnoptimizedCFG(false),
PrintStats(false), NoRetryExhausted(false), AnalyzerWerror(false) {}
TrimGraph(false), visualizeExplodedGraphWithGraphViz(false),
UnoptimizedCFG(false), PrintStats(false), NoRetryExhausted(false),
AnalyzerWerror(false) {}

/// Interprets an option's string value as a boolean. The "true" string is
/// interpreted as true and the "false" string is interpreted as false.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -583,14 +583,13 @@ class ExprEngine {
ExplodedNode *Pred,
ExplodedNodeSet &Dst);

/// 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 evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
const Expr *Ex);
/// evalEagerlyAssumeBifurcation - Given the nodes in 'Src', eagerly assume
/// concrete boolean values for 'Ex', storing the resulting nodes in 'Dst'.
void evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst, ExplodedNodeSet &Src,
const Expr *Ex);

static std::pair<const ProgramPointTag *, const ProgramPointTag *>
geteagerlyAssumeBinOpBifurcationTags();
getEagerlyAssumeBifurcationTags();

ProgramStateRef handleLValueBitCast(ProgramStateRef state, const Expr *Ex,
const LocationContext *LCtx, QualType T,
Expand Down
2 changes: 1 addition & 1 deletion clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2695,7 +2695,7 @@ ConditionBRVisitor::VisitNodeImpl(const ExplodedNode *N,
PathSensitiveBugReport &BR) {
ProgramPoint ProgPoint = N->getLocation();
const std::pair<const ProgramPointTag *, const ProgramPointTag *> &Tags =
ExprEngine::geteagerlyAssumeBinOpBifurcationTags();
ExprEngine::getEagerlyAssumeBifurcationTags();

// If an assumption was made on a branch, it should be caught
// here by looking at the state transition.
Expand Down
41 changes: 18 additions & 23 deletions clang/lib/StaticAnalyzer/Core/ExprEngine.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2129,7 +2129,7 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
(B->isRelationalOp() || B->isEqualityOp())) {
ExplodedNodeSet Tmp;
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Tmp);
evalEagerlyAssumeBinOpBifurcation(Dst, Tmp, cast<Expr>(S));
evalEagerlyAssumeBifurcation(Dst, Tmp, cast<Expr>(S));
}
else
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
Expand Down Expand Up @@ -2402,7 +2402,7 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
if (AMgr.options.ShouldEagerlyAssume && (U->getOpcode() == UO_LNot)) {
ExplodedNodeSet Tmp;
VisitUnaryOperator(U, Pred, Tmp);
evalEagerlyAssumeBinOpBifurcation(Dst, Tmp, U);
evalEagerlyAssumeBifurcation(Dst, Tmp, U);
}
else
VisitUnaryOperator(U, Pred, Dst);
Expand Down Expand Up @@ -3742,23 +3742,20 @@ void ExprEngine::evalLocation(ExplodedNodeSet &Dst,
BldrTop.addNodes(Tmp);
}

std::pair<const ProgramPointTag *, const ProgramPointTag*>
ExprEngine::geteagerlyAssumeBinOpBifurcationTags() {
static SimpleProgramPointTag
eagerlyAssumeBinOpBifurcationTrue(TagProviderName,
"Eagerly Assume True"),
eagerlyAssumeBinOpBifurcationFalse(TagProviderName,
"Eagerly Assume False");
return std::make_pair(&eagerlyAssumeBinOpBifurcationTrue,
&eagerlyAssumeBinOpBifurcationFalse);
std::pair<const ProgramPointTag *, const ProgramPointTag *>
ExprEngine::getEagerlyAssumeBifurcationTags() {
static SimpleProgramPointTag TrueTag(TagProviderName, "Eagerly Assume True"),
FalseTag(TagProviderName, "Eagerly Assume False");

return std::make_pair(&TrueTag, &FalseTag);
}

void ExprEngine::evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst,
ExplodedNodeSet &Src,
const Expr *Ex) {
void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
ExplodedNodeSet &Src,
const Expr *Ex) {
StmtNodeBuilder Bldr(Src, Dst, *currBldrCtx);

for (const auto Pred : Src) {
for (ExplodedNode *Pred : Src) {
// Test if the previous node was as the same expression. This can happen
// when the expression fails to evaluate to anything meaningful and
// (as an optimization) we don't generate a node.
Expand All @@ -3767,28 +3764,26 @@ void ExprEngine::evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst,
continue;
}

ProgramStateRef state = Pred->getState();
SVal V = state->getSVal(Ex, Pred->getLocationContext());
ProgramStateRef State = Pred->getState();
SVal V = State->getSVal(Ex, Pred->getLocationContext());
std::optional<nonloc::SymbolVal> SEV = V.getAs<nonloc::SymbolVal>();
if (SEV && SEV->isExpression()) {
const std::pair<const ProgramPointTag *, const ProgramPointTag*> &tags =
geteagerlyAssumeBinOpBifurcationTags();
const auto &[TrueTag, FalseTag] = getEagerlyAssumeBifurcationTags();

ProgramStateRef StateTrue, StateFalse;
std::tie(StateTrue, StateFalse) = state->assume(*SEV);
auto [StateTrue, StateFalse] = State->assume(*SEV);

// First assume that the condition is true.
if (StateTrue) {
SVal Val = svalBuilder.makeIntVal(1U, Ex->getType());
StateTrue = StateTrue->BindExpr(Ex, Pred->getLocationContext(), Val);
Bldr.generateNode(Ex, Pred, StateTrue, tags.first);
Bldr.generateNode(Ex, Pred, StateTrue, TrueTag);
}

// Next, assume that the condition is false.
if (StateFalse) {
SVal Val = svalBuilder.makeIntVal(0U, Ex->getType());
StateFalse = StateFalse->BindExpr(Ex, Pred->getLocationContext(), Val);
Bldr.generateNode(Ex, Pred, StateFalse, tags.second);
Bldr.generateNode(Ex, Pred, StateFalse, FalseTag);
}
}
}
Expand Down
Loading