@@ -64,7 +64,8 @@ using SR = SatisfiabilityResult;
64
64
// FIXME: These AST matchers should also be exported via the
65
65
// NullPointerAnalysisModel class, for tests
66
66
auto ptrWithBinding (llvm::StringRef VarName = kVar ) {
67
- return expr (hasType (isAnyPointer ())).bind (VarName);
67
+ return traverse (TK_IgnoreUnlessSpelledInSource,
68
+ expr (hasType (isAnyPointer ())).bind (VarName));
68
69
}
69
70
70
71
auto derefMatcher () {
@@ -81,8 +82,8 @@ auto castExprMatcher() {
81
82
.bind (kCond );
82
83
}
83
84
84
- auto nullptrMatcher () {
85
- return castExpr (hasCastKind (CK_NullToPointer)).bind (kVar );
85
+ auto nullptrMatcher (llvm::StringRef VarName = kVar ) {
86
+ return castExpr (hasCastKind (CK_NullToPointer)).bind (VarName );
86
87
}
87
88
88
89
auto addressofMatcher () {
@@ -99,6 +100,19 @@ auto assignMatcher() {
99
100
hasRHS (expr ().bind (kValue )));
100
101
}
101
102
103
+ auto nullCheckExprMatcher () {
104
+ return binaryOperator (hasAnyOperatorName (" ==" , " !=" ),
105
+ hasOperands (ptrWithBinding (), nullptrMatcher (kValue )));
106
+ }
107
+
108
+ // FIXME: When TK_IgnoreUnlessSpelledInSource is removed from ptrWithBinding(),
109
+ // this matcher should be merged with nullCheckExprMatcher().
110
+ auto equalExprMatcher () {
111
+ return binaryOperator (hasAnyOperatorName (" ==" , " !=" ),
112
+ hasOperands (ptrWithBinding (kVar ),
113
+ ptrWithBinding (kValue )));
114
+ }
115
+
102
116
auto anyPointerMatcher () { return expr (hasType (isAnyPointer ())).bind (kVar ); }
103
117
104
118
// Only computes simple comparisons against the literals True and False in the
@@ -217,34 +231,72 @@ void matchDereferenceExpr(const Stmt *stmt,
217
231
Env.assume (Env.arena ().makeNot (getVal (kIsNull , *RootValue).formula ()));
218
232
}
219
233
220
- void matchCastExpr (const CastExpr *cond, const MatchFinder::MatchResult &Result,
221
- NullPointerAnalysisModel::TransferArgs &Data) {
222
- auto [IsNonnullBranch, Env] = Data;
223
-
234
+ void matchNullCheckExpr (const Expr *NullCheck,
235
+ const MatchFinder::MatchResult &Result,
236
+ Environment &Env) {
224
237
const auto *Var = Result.Nodes .getNodeAs <Expr>(kVar );
225
238
assert (Var != nullptr );
226
239
227
- Value *RootValue = getValue (*Var, Env);
228
-
229
- Value *NewRootValue = Env.createValue (Var->getType ());
240
+ // (bool)p or (p != nullptr)
241
+ bool IsNonnullOp = true ;
242
+ if (auto *BinOp = dyn_cast<BinaryOperator>(NullCheck);
243
+ BinOp->getOpcode () == BO_EQ) {
244
+ IsNonnullOp = false ;
245
+ }
230
246
231
- setGLValue (*Var, *NewRootValue , Env);
247
+ Value *RootValue = getValue (*Var , Env);
232
248
233
249
Arena &A = Env.arena ();
234
250
BoolValue &IsNonnull = getVal (kIsNonnull , *RootValue);
235
251
BoolValue &IsNull = getVal (kIsNull , *RootValue);
252
+ BoolValue *CondValue = cast_or_null<BoolValue>(Env.getValue (*NullCheck));
253
+ if (!CondValue) {
254
+ CondValue = &A.makeAtomValue ();
255
+ Env.setValue (*NullCheck, *CondValue);
256
+ }
257
+ const Formula &CondFormula = IsNonnullOp ? CondValue->formula ()
258
+ : A.makeNot (CondValue->formula ());
259
+
260
+ Env.assume (A.makeImplies (CondFormula, A.makeNot (IsNull.formula ())));
261
+ Env.assume (A.makeImplies (A.makeNot (CondFormula),
262
+ A.makeNot (IsNonnull.formula ())));
263
+ }
264
+
265
+ void matchEqualExpr (const BinaryOperator *EqualExpr,
266
+ const MatchFinder::MatchResult &Result,
267
+ Environment &Env) {
268
+ bool IsNotEqualsOp = EqualExpr->getOpcode () == BO_NE;
269
+
270
+ const auto *LHSVar = Result.Nodes .getNodeAs <Expr>(kVar );
271
+ assert (LHSVar != nullptr );
236
272
237
- if (IsNonnullBranch) {
238
- Env.assume (A.makeNot (IsNull.formula ()));
239
- NewRootValue->setProperty (kIsNull , Env.getBoolLiteralValue (false ));
273
+ const auto *RHSVar = Result.Nodes .getNodeAs <Expr>(kValue );
274
+ assert (RHSVar != nullptr );
240
275
241
- NewRootValue-> setProperty ( kIsNonnull , IsNonnull );
242
- } else {
243
- NewRootValue-> setProperty ( kIsNull , IsNull );
276
+ Arena &A = Env. arena ( );
277
+ Value *LHSValue = getValue (*LHSVar, Env);
278
+ Value *RHSValue = getValue (*RHSVar, Env );
244
279
245
- Env.assume (A.makeNot (IsNonnull.formula ()));
246
- NewRootValue->setProperty (kIsNonnull , Env.getBoolLiteralValue (false ));
280
+ BoolValue *CondValue = cast_or_null<BoolValue>(Env.getValue (*EqualExpr));
281
+ if (!CondValue) {
282
+ CondValue = &A.makeAtomValue ();
283
+ Env.setValue (*EqualExpr, *CondValue);
247
284
}
285
+
286
+ const Formula &CondFormula = IsNotEqualsOp ? A.makeNot (CondValue->formula ())
287
+ : CondValue->formula ();
288
+
289
+ // If the pointers are equal, the nullability properties are the same.
290
+ Env.assume (A.makeImplies (CondFormula,
291
+ A.makeAnd (A.makeEquals (getVal (kIsNull , *LHSValue).formula (),
292
+ getVal (kIsNull , *RHSValue).formula ()),
293
+ A.makeEquals (getVal (kIsNonnull , *LHSValue).formula (),
294
+ getVal (kIsNonnull , *RHSValue).formula ()))));
295
+
296
+ // If the pointers are not equal, at most one of the pointers is null.
297
+ Env.assume (A.makeImplies (A.makeNot (CondFormula),
298
+ A.makeNot (A.makeAnd (getVal (kIsNull , *LHSValue).formula (),
299
+ getVal (kIsNull , *RHSValue).formula ()))));
248
300
}
249
301
250
302
void matchNullptrExpr (const Expr *expr, const MatchFinder::MatchResult &Result,
@@ -255,24 +307,31 @@ void matchNullptrExpr(const Expr *expr, const MatchFinder::MatchResult &Result,
255
307
Value *RootValue = Env.getValue (*PrVar);
256
308
if (!RootValue) {
257
309
RootValue = Env.createValue (PrVar->getType ());
310
+ Env.setValue (*PrVar, *RootValue);
258
311
}
259
312
260
313
RootValue->setProperty (kIsNull , Env.getBoolLiteralValue (true ));
261
314
RootValue->setProperty (kIsNonnull , Env.getBoolLiteralValue (false ));
262
- Env.setValue (*PrVar, *RootValue);
263
315
}
264
316
265
317
void matchAddressofExpr (const Expr *expr,
266
318
const MatchFinder::MatchResult &Result,
267
319
Environment &Env) {
268
- const auto *PrVar = Result.Nodes .getNodeAs <Expr>(kVar );
269
- assert (PrVar != nullptr );
320
+ const auto *Var = Result.Nodes .getNodeAs <Expr>(kVar );
321
+ assert (Var != nullptr );
322
+
323
+ Value *RootValue = Env.getValue (*Var);
324
+ if (!RootValue) {
325
+ RootValue = Env.createValue (Var->getType ());
270
326
271
- Value *RootValue = Env.createValue (PrVar->getType ());
327
+ if (!RootValue)
328
+ return ;
329
+
330
+ setUnknownValue (*Var, *RootValue, Env);
331
+ }
272
332
273
333
RootValue->setProperty (kIsNull , Env.getBoolLiteralValue (false ));
274
334
RootValue->setProperty (kIsNonnull , Env.getBoolLiteralValue (true ));
275
- Env.setValue (*PrVar, *RootValue);
276
335
}
277
336
278
337
void matchAnyPointerExpr (const Expr *fncall,
@@ -336,9 +395,9 @@ diagnoseAssignLocation(const Expr *Assign,
336
395
}
337
396
338
397
NullCheckAfterDereferenceDiagnoser::ResultType
339
- diagnoseCastExpr (const CastExpr *Stmt, const MatchFinder::MatchResult &Result ,
340
- const NullCheckAfterDereferenceDiagnoser::DiagnoseArgs &Data) {
341
-
398
+ diagnoseNullCheckExpr (const Expr *NullCheck ,
399
+ const MatchFinder::MatchResult &Result,
400
+ const NullCheckAfterDereferenceDiagnoser::DiagnoseArgs &Data) {
342
401
auto [ValToDerefLoc, WarningLocToVal, Env] = Data;
343
402
344
403
const auto *Var = Result.Nodes .getNodeAs <Expr>(kVar );
@@ -352,6 +411,7 @@ diagnoseCastExpr(const CastExpr *Stmt, const MatchFinder::MatchResult &Result,
352
411
bool IsNonnull = Env.allows (getVal (kIsNonnull , *RootValue).formula ());
353
412
354
413
if (!IsNull && IsNonnull) {
414
+ // FIXME: Separate function
355
415
bool Inserted =
356
416
WarningLocToVal.try_emplace (Var->getBeginLoc (), RootValue).second ;
357
417
assert (Inserted && " multiple warnings at the same source location" );
@@ -370,16 +430,44 @@ diagnoseCastExpr(const CastExpr *Stmt, const MatchFinder::MatchResult &Result,
370
430
}
371
431
}
372
432
373
- // If no matches are found, the cast itself signals a special location
433
+ // If no matches are found, the null-check itself signals a special location
374
434
auto [It, Inserted] = ValToDerefLoc.try_emplace (RootValue, nullptr );
375
435
376
436
if (Inserted)
377
- It->second = Stmt ;
437
+ It->second = NullCheck ;
378
438
}
379
439
380
440
return {};
381
441
}
382
442
443
+ NullCheckAfterDereferenceDiagnoser::ResultType
444
+ diagnoseEqualExpr (const Expr *PtrCheck, const MatchFinder::MatchResult &Result,
445
+ NullCheckAfterDereferenceDiagnoser::DiagnoseArgs &Data) {
446
+ auto [ValToDerefLoc, WarningLocToVal, Env] = Data;
447
+
448
+ const auto *LHSVar = Result.Nodes .getNodeAs <Expr>(kVar );
449
+ assert (LHSVar != nullptr );
450
+ const auto *RHSVar = Result.Nodes .getNodeAs <Expr>(kValue );
451
+ assert (RHSVar != nullptr );
452
+
453
+ Arena &A = Env.arena ();
454
+ std::vector<SourceLocation> NullVarLocations;
455
+
456
+ if (Value *LHSValue = Env.getValue (*LHSVar);
457
+ Env.proves (A.makeNot (getVal (kIsNonnull , *LHSValue).formula ()))) {
458
+ WarningLocToVal.try_emplace (LHSVar->getBeginLoc (), LHSValue);
459
+ NullVarLocations.push_back (LHSVar->getBeginLoc ());
460
+ }
461
+
462
+ if (Value *RHSValue = Env.getValue (*RHSVar);
463
+ Env.proves (A.makeNot (getVal (kIsNonnull , *RHSValue).formula ()))) {
464
+ WarningLocToVal.try_emplace (RHSVar->getBeginLoc (), RHSValue);
465
+ NullVarLocations.push_back (RHSVar->getBeginLoc ());
466
+ }
467
+
468
+ return {NullVarLocations, {}};
469
+ }
470
+
383
471
auto buildTransferMatchSwitch () {
384
472
return CFGMatchSwitchBuilder<Environment>()
385
473
.CaseOfCFGStmt <Stmt>(derefMatcher (), matchDereferenceExpr)
@@ -388,12 +476,16 @@ auto buildTransferMatchSwitch() {
388
476
.CaseOfCFGStmt <Expr>(addressofMatcher (), matchAddressofExpr)
389
477
.CaseOfCFGStmt <Expr>(functionCallMatcher (), matchAnyPointerExpr)
390
478
.CaseOfCFGStmt <Expr>(anyPointerMatcher (), matchAnyPointerExpr)
479
+ .CaseOfCFGStmt <Expr>(castExprMatcher (), matchNullCheckExpr)
480
+ .CaseOfCFGStmt <Expr>(nullCheckExprMatcher (), matchNullCheckExpr)
481
+ .CaseOfCFGStmt <BinaryOperator>(equalExprMatcher (), matchEqualExpr)
391
482
.Build ();
392
483
}
393
484
394
485
auto buildBranchTransferMatchSwitch () {
395
486
return ASTMatchSwitchBuilder<Stmt, NullPointerAnalysisModel::TransferArgs>()
396
- .CaseOf <CastExpr>(castExprMatcher (), matchCastExpr)
487
+ // .CaseOf<CastExpr>(castExprMatcher(), matchNullCheckExpr)
488
+ // .CaseOf<BinaryOperator>(equalExprMatcher(), matchEqualExpr)
397
489
.Build ();
398
490
}
399
491
@@ -403,7 +495,9 @@ auto buildDiagnoseMatchSwitch() {
403
495
.CaseOfCFGStmt <Expr>(derefMatcher (), diagnoseDerefLocation)
404
496
.CaseOfCFGStmt <Expr>(arrowMatcher (), diagnoseDerefLocation)
405
497
.CaseOfCFGStmt <Expr>(assignMatcher (), diagnoseAssignLocation)
406
- .CaseOfCFGStmt <CastExpr>(castExprMatcher (), diagnoseCastExpr)
498
+ .CaseOfCFGStmt <Expr>(castExprMatcher (), diagnoseNullCheckExpr)
499
+ .CaseOfCFGStmt <Expr>(nullCheckExprMatcher (), diagnoseNullCheckExpr)
500
+ .CaseOfCFGStmt <Expr>(equalExprMatcher (), diagnoseEqualExpr)
407
501
.Build ();
408
502
}
409
503
0 commit comments