[analyzer] StdLibraryFunctionsChecker: fix bug with arg constraints

Summary:
Previously we induced a state split if there were multiple argument
constraints given for a function. This was because we called
`addTransition` inside the for loop.
The fix is to is to store the state and apply the next argument
constraint on that. And once the loop is finished we call `addTransition`.

Reviewers: NoQ, Szelethus, baloghadamsoftware

Subscribers: whisperity, xazax.hun, szepet, rnkovacs, a.sidorin, mikhail.ramalho, donat.nagy, dkrupp, gamesh411, C

Tags: #clang

Differential Revision: https://reviews.llvm.org/D76790
This commit is contained in:
Gabor Marton 2020-04-02 16:59:02 +02:00
parent da8eda1ab1
commit 1525232e27
3 changed files with 78 additions and 9 deletions

View File

@ -1422,6 +1422,12 @@ def DebugIteratorModeling : Checker<"DebugIteratorModeling">,
Dependencies<[DebugContainerModeling, IteratorModeling]>,
Documentation<NotDocumented>;
def StdCLibraryFunctionsTesterChecker : Checker<"StdCLibraryFunctionsTester">,
HelpText<"Add test functions to the summary map, so testing of individual "
"summary constituents becomes possible.">,
Dependencies<[StdCLibraryFunctionsChecker]>,
Documentation<NotDocumented>;
} // end "debug"

View File

@ -306,7 +306,11 @@ public:
void checkPostCall(const CallEvent &Call, CheckerContext &C) const;
bool evalCall(const CallEvent &Call, CheckerContext &C) const;
enum CheckKind { CK_StdCLibraryFunctionArgsChecker, CK_NumCheckKinds };
enum CheckKind {
CK_StdCLibraryFunctionArgsChecker,
CK_StdCLibraryFunctionsTesterChecker,
CK_NumCheckKinds
};
DefaultBool ChecksEnabled[CK_NumCheckKinds];
CheckerNameRef CheckNames[CK_NumCheckKinds];
@ -455,23 +459,26 @@ void StdLibraryFunctionsChecker::checkPreCall(const CallEvent &Call,
const Summary &Summary = *FoundSummary;
ProgramStateRef State = C.getState();
ProgramStateRef NewState = State;
for (const ValueConstraintPtr& VC : Summary.ArgConstraints) {
ProgramStateRef SuccessSt = VC->apply(State, Call, Summary);
ProgramStateRef FailureSt = VC->negate()->apply(State, Call, Summary);
ProgramStateRef SuccessSt = VC->apply(NewState, Call, Summary);
ProgramStateRef FailureSt = VC->negate()->apply(NewState, Call, Summary);
// The argument constraint is not satisfied.
if (FailureSt && !SuccessSt) {
if (ExplodedNode *N = C.generateErrorNode(State))
if (ExplodedNode *N = C.generateErrorNode(NewState))
reportBug(Call, N, C);
break;
} else {
// Apply the constraint even if we cannot reason about the argument. This
// means both SuccessSt and FailureSt can be true. If we weren't applying
// the constraint that would mean that symbolic execution continues on a
// code whose behaviour is undefined.
// We will apply the constraint even if we cannot reason about the
// argument. This means both SuccessSt and FailureSt can be true. If we
// weren't applying the constraint that would mean that symbolic
// execution continues on a code whose behaviour is undefined.
assert(SuccessSt);
C.addTransition(SuccessSt);
NewState = SuccessSt;
}
}
if (NewState && NewState != State)
C.addTransition(NewState);
}
void StdLibraryFunctionsChecker::checkPostCall(const CallEvent &Call,
@ -936,6 +943,32 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
{"getdelim", Summaries{Getline(IntTy, IntMax), Getline(LongTy, LongMax),
Getline(LongLongTy, LongLongMax)}},
};
// Functions for testing.
if (ChecksEnabled[CK_StdCLibraryFunctionsTesterChecker]) {
llvm::StringMap<Summaries> TestFunctionSummaryMap = {
{"__two_constrained_args",
Summaries{
Summary(ArgTypes{IntTy, IntTy}, RetType{IntTy}, EvalCallAsPure)
.ArgConstraint(
ArgumentCondition(0U, WithinRange, SingleValue(1)))
.ArgConstraint(
ArgumentCondition(1U, WithinRange, SingleValue(1)))}},
{"__arg_constrained_twice",
Summaries{Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
.ArgConstraint(
ArgumentCondition(0U, OutOfRange, SingleValue(1)))
.ArgConstraint(
ArgumentCondition(0U, OutOfRange, SingleValue(2)))}},
};
for (auto &E : TestFunctionSummaryMap) {
auto InsertRes =
FunctionSummaryMap.insert({std::string(E.getKey()), E.getValue()});
assert(InsertRes.second &&
"Test functions must not clash with modeled functions");
(void)InsertRes;
}
}
}
void ento::registerStdCLibraryFunctionsChecker(CheckerManager &mgr) {
@ -958,3 +991,4 @@ bool ento::shouldRegisterStdCLibraryFunctionsChecker(const CheckerManager &mgr)
bool ento::shouldRegister##name(const CheckerManager &mgr) { return true; }
REGISTER_CHECKER(StdCLibraryFunctionArgsChecker)
REGISTER_CHECKER(StdCLibraryFunctionsTesterChecker)

View File

@ -3,6 +3,7 @@
// RUN: -analyzer-checker=core \
// RUN: -analyzer-checker=apiModeling.StdCLibraryFunctions \
// RUN: -analyzer-checker=apiModeling.StdCLibraryFunctionArgs \
// RUN: -analyzer-checker=debug.StdCLibraryFunctionsTester \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -triple x86_64-unknown-linux-gnu \
// RUN: -verify=report
@ -12,6 +13,7 @@
// RUN: -analyzer-checker=core \
// RUN: -analyzer-checker=apiModeling.StdCLibraryFunctions \
// RUN: -analyzer-checker=apiModeling.StdCLibraryFunctionArgs \
// RUN: -analyzer-checker=debug.StdCLibraryFunctionsTester \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -triple x86_64-unknown-linux-gnu \
// RUN: -analyzer-output=text \
@ -85,3 +87,30 @@ void test_notnull_symbolic2(FILE *fp, int *buf) {
// bugpath-warning{{Function argument constraint is not satisfied}} \
// bugpath-note{{Function argument constraint is not satisfied}}
}
int __two_constrained_args(int, int);
void test_constraints_on_multiple_args(int x, int y) {
// State split should not happen here. I.e. x == 1 should not be evaluated
// FALSE.
__two_constrained_args(x, y);
clang_analyzer_eval(x == 1); // \
// report-warning{{TRUE}} \
// bugpath-warning{{TRUE}} \
// bugpath-note{{TRUE}}
clang_analyzer_eval(y == 1); // \
// report-warning{{TRUE}} \
// bugpath-warning{{TRUE}} \
// bugpath-note{{TRUE}}
}
int __arg_constrained_twice(int);
void test_multiple_constraints_on_same_arg(int x) {
__arg_constrained_twice(x);
// Check that both constraints are applied and only one branch is there.
clang_analyzer_eval(x < 1 || x > 2); // \
// report-warning{{TRUE}} \
// bugpath-warning{{TRUE}} \
// bugpath-note{{TRUE}} \
// bugpath-note{{Assuming 'x' is < 1}} \
// bugpath-note{{Left side of '||' is true}}
}