[NFC][Static Analyzer] Rename and discuss about NotNullConstraint & NotNullBufferConstraint
#131374
Conversation
…straint` NotNullConstraint is used to check both null and non-null of a pointer. So the name, which was created originally for just checking non-nullness, becomes less suitable. The same reason applies to `NotNullBufferConstraint`.
ziqingluo-90
requested review from
NagyDonat,
Szelethus,
Xazax-hun,
balazske,
haoNoQ and
steakhal
llvmbot
added
clang
|
@llvm/pr-subscribers-clang @llvm/pr-subscribers-clang-static-analyzer-1 Author: Ziqing Luo (ziqingluo-90) ChangesNotNullConstraint is used to check both null and non-null of a pointer. So the name, which was created originally for just checking non-nullness, becomes less suitable. Other than the names, I have some concerns noted in comments below. I'd like to discuss them with Static Analyzer folks! Full diff: https://github.com/llvm/llvm-project/pull/131374.diff 1 Files Affected:
diff --git a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
index fef19b4547555..3542b7c8aaf30 100644
--- a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -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,
@@ -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:
@@ -407,9 +407,9 @@ 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;
@@ -417,7 +417,7 @@ class StdLibraryFunctionsChecker
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),
@@ -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;
- return std::make_shared<NotNullBufferConstraint>(Tmp);
+ return std::make_shared<BufferNullnessConstraint>(Tmp);
}
protected:
@@ -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());
@@ -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 &&
@@ -1176,7 +1176,7 @@ 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");
@@ -1184,7 +1184,7 @@ bool StdLibraryFunctionsChecker::NotNullConstraint::describeArgumentValue(
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());
@@ -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 &&
@@ -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");
@@ -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);
};
|
| void StdLibraryFunctionsChecker::NullnessConstraint::describe( | ||
| DescriptionKind DK, const CallEvent &Call, ProgramStateRef State, | ||
| const Summary &Summary, llvm::raw_ostream &Out) const { | ||
| assert(CannotBeNull && |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.)
There was a problem hiding this comment.
Currently the NotNullConstraint is used in two ways:
- Argument preconditions where only a non-null condition is used. When
describeis called here theCannotBeNullshould be true. ThedescribeArgumentValueis called on the negated version of it whenCannotBeNullis false. - Return value conditions at "cases" where it can be null or non-null. Here always a custom description text is used and
describeordescribeArgumentValueis 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).
There was a problem hiding this comment.
@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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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.
| ValueConstraintPtr negate() const override { | ||
| NotNullBufferConstraint Tmp(*this); | ||
| BufferNullnessConstraint Tmp(*this); | ||
| Tmp.CannotBeNull = !this->CannotBeNull; |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
|
✅ With the latest revision this PR passed the C/C++ code formatter. |
|
I like what you present here. I also share your concerns and your proposed resolutions. |
Hi @steakhal. As nothing is being broken so far, I suggest making no changes but adding comments about what could be wrong and how to fix them in case fix becomes necessary. |
I wanted to suggest. Thank you. |
balazske
left a comment
balazske
left a comment
There was a problem hiding this comment.
Rename looks good. According to the format check code should be reformatted. Do not forget to remove the "discuss" part from the commit title.
|
@balazske Thank you for the discussion and explanation. I now have a better understanding of this checker. |
…emented instread of should not happen
4 participants
NotNullConstraint is used to check both null and non-null of a pointer. So the name, which was created originally for just checking non-nullness, becomes less suitable.
The same reason applies to
NotNullBufferConstraint.Other than the names, I have some concerns noted in comments below. I'd like to discuss them with Static Analyzer folks!