Skip to content

[NFC][Static Analyzer] Rename and discuss about NotNullConstraint & NotNullBufferConstraint #131374

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.

Sign up for GitHub

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
ziqingluo-90 merged 3 commits into from
Mar 25, 2025
Merged

[NFC][Static Analyzer] Rename and discuss about NotNullConstraint & NotNullBufferConstraint #131374

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fdc265e
[NFC][Static Analyzer] Rename `NotNullConstraint` & `NotNullBufferCon…
ziqingluo-90 Mar 14, 2025
93a9728
Change the assertion message to indicate that some cases are not impl…
ziqingluo-90 Mar 24, 2025
b1bb00f
fix format
ziqingluo-90 Mar 24, 2025
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
38 changes: 19 additions & 19 deletions clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,13 +367,13 @@ class StdLibraryFunctionsChecker
};

/// Check null or non-null-ness of an argument that is of pointer type.
class NotNullConstraint : public ValueConstraint {
class NullnessConstraint : public ValueConstraint {
using ValueConstraint::ValueConstraint;
// This variable has a role when we negate the constraint.
bool CannotBeNull = true;

public:
NotNullConstraint(ArgNo ArgN, bool CannotBeNull = true)
NullnessConstraint(ArgNo ArgN, bool CannotBeNull = true)
: ValueConstraint(ArgN), CannotBeNull(CannotBeNull) {}

ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
Expand All @@ -389,9 +389,9 @@ class StdLibraryFunctionsChecker
llvm::raw_ostream &Out) const override;

ValueConstraintPtr negate() const override {
NotNullConstraint Tmp(*this);
NullnessConstraint Tmp(*this);
Tmp.CannotBeNull = !this->CannotBeNull;
return std::make_shared<NotNullConstraint>(Tmp);
return std::make_shared<NullnessConstraint>(Tmp);
}

protected:
Expand All @@ -407,17 +407,17 @@ class StdLibraryFunctionsChecker
/// The argument is meant to be a buffer that has a size constraint, and it
/// is allowed to have a NULL value if the size is 0. The size can depend on
/// 1 or 2 additional arguments, if one of these is 0 the buffer is allowed to
/// be NULL. This is useful for functions like `fread` which have this special
/// property.
class NotNullBufferConstraint : public ValueConstraint {
/// be NULL. Otherwise, the buffer pointer must be non-null. This is useful
/// for functions like `fread` which have this special property.
class BufferNullnessConstraint : public ValueConstraint {
using ValueConstraint::ValueConstraint;
ArgNo SizeArg1N;
std::optional<ArgNo> SizeArg2N;
// This variable has a role when we negate the constraint.
bool CannotBeNull = true;

public:
NotNullBufferConstraint(ArgNo ArgN, ArgNo SizeArg1N,
BufferNullnessConstraint(ArgNo ArgN, ArgNo SizeArg1N,
std::optional<ArgNo> SizeArg2N,
bool CannotBeNull = true)
: ValueConstraint(ArgN), SizeArg1N(SizeArg1N), SizeArg2N(SizeArg2N),
Expand All @@ -436,9 +436,9 @@ class StdLibraryFunctionsChecker
llvm::raw_ostream &Out) const override;

ValueConstraintPtr negate() const override {
NotNullBufferConstraint Tmp(*this);
BufferNullnessConstraint Tmp(*this);
Tmp.CannotBeNull = !this->CannotBeNull;
Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 14, 2025

Choose a reason for hiding this comment

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

The negation of the constraint does not fully match my expectation: this constraint is saying size == 0 || buf != 0. So the negation is suppose to be size != 0 && buf == 0. The implementation looks more like size == 0 || buf == 0 to me.

In general, how is the negation of a constraint used? I imagine that sometimes the engine needs to split the path by assuming 'C' and '!C' for a constraint 'C'? If the negation can be used as an assumption for a path, we should be serious about its correctness. Additionally, describe and describeArgumentValue need to report differently depending on whether the constraint is negated or not.

Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 19, 2025

Choose a reason for hiding this comment

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

The negation of a constraint C is only used to determine if the constraint holds at a state. It checks that applying C results in a feasible state and applying !C results in a infeasible one.

The current negation implementation of NotNullBufferConstraint is kind of "weaker" than what it suppose to be. (Formally, the "weaker than" relation doesn't exist between them.) In other words, applying !C may not result in an infeasible state when it is suppose to happen. Consequently, the checker can miss the chance of determining a constraint holds at a state. But I suspect this is some rare corner case.

My conclusion is to make no change but some comments about this. @balazske

Copy link
Collaborator

@balazske balazske Mar 20, 2025

Choose a reason for hiding this comment

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

The purpose is to ignore the constraint of the buffer if size == 0 is true. If size is 0 the buffer can be a null or non-null pointer, so the constraint has no effect.

Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 20, 2025

Choose a reason for hiding this comment

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

Oh, I somehow thought the checker passes a pre-condition C only when State->assume(C) && !State->assume(!C)) but the reality is it reports a violation only when State->assume(!C) && !State->assume(C).

Yes, you are right. This is fine.

return std::make_shared<NotNullBufferConstraint>(Tmp);
return std::make_shared<BufferNullnessConstraint>(Tmp);
}

protected:
Expand Down Expand Up @@ -1151,7 +1151,7 @@ ProgramStateRef StdLibraryFunctionsChecker::ComparisonConstraint::apply(
return State;
}

ProgramStateRef StdLibraryFunctionsChecker::NotNullConstraint::apply(
ProgramStateRef StdLibraryFunctionsChecker::NullnessConstraint::apply(
ProgramStateRef State, const CallEvent &Call, const Summary &Summary,
CheckerContext &C) const {
SVal V = getArgSVal(Call, getArgNo());
Expand All @@ -1165,7 +1165,7 @@ ProgramStateRef StdLibraryFunctionsChecker::NotNullConstraint::apply(
return State->assume(L, CannotBeNull);
}

void StdLibraryFunctionsChecker::NotNullConstraint::describe(
void StdLibraryFunctionsChecker::NullnessConstraint::describe(
DescriptionKind DK, const CallEvent &Call, ProgramStateRef State,
const Summary &Summary, llvm::raw_ostream &Out) const {
assert(CannotBeNull &&
Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 14, 2025

Choose a reason for hiding this comment

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

The flag CannotBeNull controls whether this constraint is checking for null or non-null. But why describe function asserts CannotBeNull and below describeArgumentValue function asserts !CannotBeNull?

My understanding is that describe and describeArgumentValue are used to explain assumptions made by the checker to users during error reporting. I suppose both can be called in either case.

Copy link
Collaborator

@balazske balazske Mar 17, 2025

Choose a reason for hiding this comment

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

Did you check the comments of describe and describeArgumentValue (at class ValueConstraint)? If these are not exact they could be improved. I think that describe is used at reporting failed preconditions of functions when only non-null is the "usual" case, and describeArgumentValue is used when an execution path is displayed. Probably the assert is there to have a "summary case" description instead to explain the situation better. (But I should check it in more detail.)

Copy link
Collaborator

@balazske balazske Mar 18, 2025

Choose a reason for hiding this comment

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

Currently the NotNullConstraint is used in two ways:

  • Argument preconditions where only a non-null condition is used. When describe is called here the CannotBeNull should be true. The describeArgumentValue is called on the negated version of it when CannotBeNull is false.
  • Return value conditions at "cases" where it can be null or non-null. Here always a custom description text is used and describe or describeArgumentValue is not called.

Purpose of the assertion seems to be only to make a simplification (not implement describe in the null and describeArgumentValue in the non-null case). The assertion could be extended with something like getArgNo() != Ret && (verify the first use case above).

Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 19, 2025

Choose a reason for hiding this comment

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

@balazske Thanks for pointing out the places I should look at. I've learned more about them.

Regarding the NotNullConstraint class, it represents two mutually exclusive constraints NotNull and IsNull. And then, yes, NotNull is only used in pre-conditions on arguments and IsNull is only used in post-condition cases. The two functions describe and describeArgumentValue are only called when pre-conditions are violated, meaning that they are never called on IsNull. In addition, describeArgumentValue is always called on the negation of the violated pre-condition to describe the violating argument. This specific usage ensures that the checker never runs into violations of those assertions within describe and describeArgumentValue. In other words, nothing broken at this point.

However, the assertions and the implementations of describe and describeArgumentValue do not fully align with their documents IMO. The document of describe is general and accurate---

 /// Give a description that explains the constraint to the user. Used when
 /// a bug is reported or when the constraint is applied and displayed as a
 /// note.

This suggests that describe should be callable on any constraint to produce a summary. NotNull and IsNull are both constraints. So are their negations. But in practice, calling describe on IsNull will violate the assertion.

I believe the document of describeArgumentValue is not so accurate. It says

/// .... This function should be called only when the current constraint is satisfied by the argument. ...

But in practice, this function is called when reporting pre-condition violations, i.e., the constraint is not satisfied by the argument. Additionally, describeArgumentValue should be callable for any constraint as well.

In conclusion, I suggest we make no changes except for the name of NotNullConstraint, as nothing is currently broken. The NotNullConstraint class is essentially the common implementation of the two constraints NotNull and IsNull, so I think the name should reflect that. Assertions in describe and describeArgumentValue will notify developers immediately when their implementations really need to be corrected. I would like to add some comments there to note my findings if they sound right to you.

Copy link
Collaborator

@balazske balazske Mar 20, 2025

Choose a reason for hiding this comment

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

The describeArgumentValue should be really called only with a ProgramState where the current constraint is true. The purpose is to generate a description of the actual value and probably use the program state for this. It is exactly used on the negated version of a failed constraint in reportBug.

Copy link
Contributor Author

@ziqingluo-90 ziqingluo-90 Mar 20, 2025

Choose a reason for hiding this comment

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

ah, I see. It's called on the negation of the violated constraint!

Then the only remaining question I have is that do you think describe and describeArgumentValue should be allowed to be called on any constraint? For example, we cannot call describe on the IsNull constraint currently. But since IsNull is used in making assumptions on post-conditions, I imagine one may be interested in adding a description note to a state/node explaining where the assumption comes from. As far as I know, users sometimes struggle to understand where assumptions are made that eventually lead a path to an error. So I'd like to leave some comments there for a future developer who might attempt to call describe on IsNull. @balazske

Copy link
Collaborator

@balazske balazske Mar 21, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Technically it is not an error to use the describe functions on any constraint, the assertion indicates only a not implemented (and not used) case. We can remove the assertion and print out a text like "(describe not implemented yet)" as description.

Expand All @@ -1176,15 +1176,15 @@ void StdLibraryFunctionsChecker::NotNullConstraint::describe(
Out << "is not NULL";
}

bool StdLibraryFunctionsChecker::NotNullConstraint::describeArgumentValue(
bool StdLibraryFunctionsChecker::NullnessConstraint::describeArgumentValue(
const CallEvent &Call, ProgramStateRef State, const Summary &Summary,
llvm::raw_ostream &Out) const {
assert(!CannotBeNull && "This function is used when the value is NULL");
Out << "is NULL";
return true;
}

ProgramStateRef StdLibraryFunctionsChecker::NotNullBufferConstraint::apply(
ProgramStateRef StdLibraryFunctionsChecker::BufferNullnessConstraint::apply(
ProgramStateRef State, const CallEvent &Call, const Summary &Summary,
CheckerContext &C) const {
SVal V = getArgSVal(Call, getArgNo());
Expand Down Expand Up @@ -1213,7 +1213,7 @@ ProgramStateRef StdLibraryFunctionsChecker::NotNullBufferConstraint::apply(
return State->assume(L, CannotBeNull);
}

void StdLibraryFunctionsChecker::NotNullBufferConstraint::describe(
void StdLibraryFunctionsChecker::BufferNullnessConstraint::describe(
DescriptionKind DK, const CallEvent &Call, ProgramStateRef State,
const Summary &Summary, llvm::raw_ostream &Out) const {
assert(CannotBeNull &&
Expand All @@ -1224,7 +1224,7 @@ void StdLibraryFunctionsChecker::NotNullBufferConstraint::describe(
Out << "is not NULL";
}

bool StdLibraryFunctionsChecker::NotNullBufferConstraint::describeArgumentValue(
bool StdLibraryFunctionsChecker::BufferNullnessConstraint::describeArgumentValue(
const CallEvent &Call, ProgramStateRef State, const Summary &Summary,
llvm::raw_ostream &Out) const {
assert(!CannotBeNull && "This function is used when the value is NULL");
Expand Down Expand Up @@ -1792,14 +1792,14 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
};
auto LessThanOrEq = BO_LE;
auto NotNull = [&](ArgNo ArgN) {
return std::make_shared<NotNullConstraint>(ArgN);
return std::make_shared<NullnessConstraint>(ArgN);
};
auto IsNull = [&](ArgNo ArgN) {
return std::make_shared<NotNullConstraint>(ArgN, false);
return std::make_shared<NullnessConstraint>(ArgN, false);
};
auto NotNullBuffer = [&](ArgNo ArgN, ArgNo SizeArg1N,
std::optional<ArgNo> SizeArg2N = std::nullopt) {
return std::make_shared<NotNullBufferConstraint>(ArgN, SizeArg1N,
return std::make_shared<BufferNullnessConstraint>(ArgN, SizeArg1N,
SizeArg2N);
};

Expand Down
Loading