Skip to content

Commit 77ab728

Browse files
weirdsmileysteakhal
authored andcommitted
[analyzer][solver] Introduce reasoning for not equal to operator
With this patch, the solver can infer results for not equal (!=) operator over Ranges as well. This also fixes the issue of comparison between different types, by first converting the RangeSets to the resulting type, which then can be used for comparisons. Patch by Manas. Reviewed By: steakhal Differential Revision: https://reviews.llvm.org/D112621
1 parent f4c6d7b commit 77ab728

File tree

2 files changed

+193
-12
lines changed

2 files changed

+193
-12
lines changed

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

Lines changed: 44 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1333,18 +1333,7 @@ class SymbolicRangeInferrer
13331333
}
13341334

13351335
RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
1336-
RangeSet RHS, QualType T) {
1337-
switch (Op) {
1338-
case BO_Or:
1339-
return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
1340-
case BO_And:
1341-
return VisitBinaryOperator<BO_And>(LHS, RHS, T);
1342-
case BO_Rem:
1343-
return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
1344-
default:
1345-
return infer(T);
1346-
}
1347-
}
1336+
RangeSet RHS, QualType T);
13481337

13491338
//===----------------------------------------------------------------------===//
13501339
// Ranges and operators
@@ -1625,6 +1614,32 @@ class SymbolicRangeInferrer
16251614
// Range-based reasoning about symbolic operations
16261615
//===----------------------------------------------------------------------===//
16271616

1617+
template <>
1618+
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
1619+
RangeSet RHS,
1620+
QualType T) {
1621+
1622+
assert(!LHS.isEmpty() && !RHS.isEmpty() && "Both ranges should be non-empty");
1623+
1624+
if (LHS.getAPSIntType() == RHS.getAPSIntType()) {
1625+
if (intersect(RangeFactory, LHS, RHS).isEmpty())
1626+
return getTrueRange(T);
1627+
} else {
1628+
// Both RangeSets should be casted to bigger unsigned type.
1629+
APSIntType CastingType(std::max(LHS.getBitWidth(), RHS.getBitWidth()),
1630+
LHS.isUnsigned() || RHS.isUnsigned());
1631+
1632+
RangeSet CastedLHS = RangeFactory.castTo(LHS, CastingType);
1633+
RangeSet CastedRHS = RangeFactory.castTo(RHS, CastingType);
1634+
1635+
if (intersect(RangeFactory, CastedLHS, CastedRHS).isEmpty())
1636+
return getTrueRange(T);
1637+
}
1638+
1639+
// In all other cases, the resulting range cannot be deduced.
1640+
return infer(T);
1641+
}
1642+
16281643
template <>
16291644
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
16301645
QualType T) {
@@ -1785,6 +1800,23 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
17851800
return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
17861801
}
17871802

1803+
RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS,
1804+
BinaryOperator::Opcode Op,
1805+
RangeSet RHS, QualType T) {
1806+
switch (Op) {
1807+
case BO_NE:
1808+
return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
1809+
case BO_Or:
1810+
return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
1811+
case BO_And:
1812+
return VisitBinaryOperator<BO_And>(LHS, RHS, T);
1813+
case BO_Rem:
1814+
return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
1815+
default:
1816+
return infer(T);
1817+
}
1818+
}
1819+
17881820
//===----------------------------------------------------------------------===//
17891821
// Constraint manager implementation details
17901822
//===----------------------------------------------------------------------===//

clang/test/Analysis/constant-folding.c

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,3 +281,152 @@ void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
281281
clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
282282
}
283283
}
284+
285+
void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
286+
int s1, int s2, int s3, unsigned char uch,
287+
signed char sch, short ssh, unsigned short ush) {
288+
289+
// Checks for overflowing values
290+
if (u1 > INT_MAX && u1 <= UINT_MAX / 2 + 4 && u1 != UINT_MAX / 2 + 2 &&
291+
u1 != UINT_MAX / 2 + 3 && s1 >= INT_MIN + 1 && s1 <= INT_MIN + 2) {
292+
// u1: [INT_MAX+1, INT_MAX+1]U[INT_MAX+4, INT_MAX+4],
293+
// s1: [INT_MIN+1, INT_MIN+2]
294+
clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
295+
}
296+
297+
if (u1 >= INT_MIN && u1 <= INT_MIN + 2 &&
298+
s1 > INT_MIN + 2 && s1 < INT_MIN + 4) {
299+
// u1: [INT_MAX+1, INT_MAX+1]U[INT_MAX+4, INT_MAX+4],
300+
// s1: [INT_MIN+3, INT_MIN+3]
301+
clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
302+
}
303+
304+
if (s1 < 0 && s1 > -4 && u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
305+
// s1: [-3, -1], u1: [UINT_MAX - 3, UINT_MAX - 2]
306+
clang_analyzer_eval(u1 != s1); // expected-warning{{UNKNOWN}}
307+
}
308+
309+
if (s1 < 1 && s1 > -6 && s1 != -4 && s1 != -3 &&
310+
u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
311+
// s1: [-5, -5]U[-2, 0], u1: [UINT_MAX - 3, UINT_MAX - 2]
312+
clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
313+
}
314+
315+
if (s1 < 1 && s1 > -7 && s1 != -4 && s1 != -3 &&
316+
u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
317+
// s1: [-6, -5]U[-2, 0], u1: [UINT_MAX - 3, UINT_MAX - 2]
318+
clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
319+
}
320+
321+
if (s1 > 4 && u1 < 4) {
322+
// s1: [4, INT_MAX], u1: [0, 3]
323+
clang_analyzer_eval(s1 != u1); // expected-warning{{TRUE}}
324+
}
325+
326+
// Check when RHS is in between two Ranges in LHS
327+
if (((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) &&
328+
u2 >= 5 && u2 <= 6) {
329+
// u1: [1, 2]U[8, 9], u2: [5, 6]
330+
clang_analyzer_eval(u1 != u2); // expected-warning{{TRUE}}
331+
}
332+
333+
// Checks for concrete value with same type
334+
if (u1 > 1 && u1 < 3 && u2 > 1 && u2 < 3) {
335+
// u1: [2, 2], u2: [2, 2]
336+
clang_analyzer_eval(u1 != u2); // expected-warning{{FALSE}}
337+
}
338+
339+
// Check for concrete value with different types
340+
if (u1 > 4 && u1 < 6 && s1 > 4 && s1 < 6) {
341+
// u1: [5, 5], s1: [5, 5]
342+
clang_analyzer_eval(u1 != s1); // expected-warning{{FALSE}}
343+
}
344+
345+
// Checks when ranges are not overlapping
346+
if (u1 <= 10 && u2 >= 20) {
347+
// u1: [0,10], u2: [20,UINT_MAX]
348+
clang_analyzer_eval(u1 != u2); // expected-warning{{TRUE}}
349+
}
350+
351+
if (s1 <= INT_MIN + 10 && s2 >= INT_MAX - 10) {
352+
// s1: [INT_MIN,INT_MIN + 10], s2: [INT_MAX - 10,INT_MAX]
353+
clang_analyzer_eval(s1 != s2); // expected-warning{{TRUE}}
354+
}
355+
356+
// Checks when ranges are completely overlapping and have more than one point
357+
if (u1 >= 20 && u1 <= 50 && u2 >= 20 && u2 <= 50) {
358+
// u1: [20,50], u2: [20,50]
359+
clang_analyzer_eval(u1 != u2); // expected-warning{{UNKNOWN}}
360+
}
361+
362+
if (s1 >= -20 && s1 <= 20 && s2 >= -20 && s2 <= 20) {
363+
// s1: [-20,20], s2: [-20,20]
364+
clang_analyzer_eval(s1 != s2); // expected-warning{{UNKNOWN}}
365+
}
366+
367+
// Checks when ranges are partially overlapping
368+
if (u1 >= 100 && u1 <= 200 && u2 >= 150 && u2 <= 300) {
369+
// u1: [100,200], u2: [150,300]
370+
clang_analyzer_eval(u1 != u2); // expected-warning{{UNKNOWN}}
371+
}
372+
373+
if (s1 >= -80 && s1 <= -50 && s2 >= -100 && s2 <= -75) {
374+
// s1: [-80,-50], s2: [-100,-75]
375+
clang_analyzer_eval(s1 != s2); // expected-warning{{UNKNOWN}}
376+
}
377+
378+
// Checks for ranges which are subset of one-another
379+
if (u1 >= 500 && u1 <= 1000 && u2 >= 750 && u2 <= 1000) {
380+
// u1: [500,1000], u2: [750,1000]
381+
clang_analyzer_eval(u1 != u2); // expected-warning{{UNKNOWN}}
382+
}
383+
384+
if (s1 >= -1000 && s1 <= -500 && s2 >= -750 && s2 <= -500) {
385+
// s1: [-1000,-500], s2: [-750, -500]
386+
clang_analyzer_eval(s1 != s2); // expected-warning{{UNKNOWN}}
387+
}
388+
389+
// Checks for comparison between different types
390+
// Using different variables as previous constraints may interfere in the
391+
// reasoning.
392+
if (u3 <= 255 && s3 < 0) {
393+
// u3: [0, 255], s3: [INT_MIN, -1]
394+
clang_analyzer_eval(u3 != s3); // expected-warning{{TRUE}}
395+
}
396+
397+
// Checks for char-uchar types
398+
if (uch >= 1 && sch <= 1) {
399+
// uch: [1, UCHAR_MAX], sch: [SCHAR_MIN, 1]
400+
clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
401+
}
402+
403+
// FIXME: Casting smaller signed types to unsigned one may leave us with
404+
// overlapping values, falsely indicating UNKNOWN, where it is possible to
405+
// assert TRUE.
406+
if (uch > 1 && sch < 1) {
407+
// uch: [2, UCHAR_MAX], sch: [SCHAR_MIN, 0]
408+
clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
409+
}
410+
411+
if (uch <= 1 && uch >= 1 && sch <= 1 && sch >= 1) {
412+
// uch: [1, 1], sch: [1, 1]
413+
clang_analyzer_eval(uch != sch); // expected-warning{{FALSE}}
414+
}
415+
416+
// Checks for short-ushort types
417+
if (ush >= 1 && ssh <= 1) {
418+
// ush: [1, USHRT_MAX], ssh: [SHRT_MIN, 1]
419+
clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
420+
}
421+
422+
// FIXME: Casting leave us with overlapping values. Should be TRUE.
423+
if (ush > 1 && ssh < 1) {
424+
// ush: [2, USHRT_MAX], ssh: [SHRT_MIN, 0]
425+
clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
426+
}
427+
428+
if (ush <= 1 && ush >= 1 && ssh <= 1 && ssh >= 1) {
429+
// ush: [1, 1], ssh: [1, 1]
430+
clang_analyzer_eval(ush != ssh); // expected-warning{{FALSE}}
431+
}
432+
}

0 commit comments

Comments
 (0)