[analyzer] Handle pointer difference of ElementRegion and SymbolicRegion

[steakhal]

Summary

Currently, if the analyzer evaluates an expression like to - from, it only computes reasonable answer if both are representing ElementRegions.
This patch aims to extends the analyzer to be able to evaluate certain pointer arithmetic operations.

Formally, for all memory region X and for all NonLoc n, m:
Evaluate:

• Element{X,n} - Element{X,m} => n-m
• Element{X,n} - X => n
• X - Element{X,n} => -n
• Element{X,n} == X => true/falsedepending on n is zero or not.
• etc.

[steakhal]

Manually force request review, to start a discussion about this.

Although I managed to implement this in a way to pass the tests, but the logic became somewhat messy, that's why I stick to this dummy patch.
I'm gonna clean that up and update the diff, if you think that such handing of memregions are valid.
Sorry for the cfe-dev spam, I did not know that I can manually request review.

[xazax.hun]

I think adding code snippets that are affected by this patch would make it much easier to evaluate the changes and whether this is a good idea or not.

[NoQ]

I think the overall idea is correct.

Yup, the patch will need the new positive tests that started passing. If you can't demonstrate it with integration tests you should do unit tests because the contract you're trying to achieve is fairly clear and obviously correct and it makes sense to test it separately.

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1092

Symbolic regions aren't special. Any other parent region should work similarly.

1095–1096

You'll have to multiply by the size of a single element - it's an index, not an offset.

1103–1105

Yeah, sounds like we'll have to stick to UnknownVal for now when RightIndex is symbolic. You can easily compute unary minus for a concrete index though, and that'll probably be your most important case anyway.

[steakhal]

Thank you all for the comments.

In D84736#2179828, @NoQ wrote:

I think the overall idea is correct.

So I will keep going in this direction, you can expect the more complex version of this.
I plan to reuse this revision.

So we can formalize this logic like this:
for all MemReg, and Y: &Element{MemReg,Y,char} - &MemReg => Y

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1095–1096

Nice catch.

1103–1105

I managed to get around this by turning the unary minus into a binary substitution from zero (using ArrayIndexTy type).
Although I should have improved the SimpleSValBuilder::minus function to handle other svals besides concrete ints instead.

[steakhal]

Reworked ElementRegion handling.
Previously it handled only element regions in the form of: Element{X,n} OP Element{X,m}
Now supports Element{X,n} OP X and X OP Element{X,n} as well.
Still misses nested ElementRegions though like: Element{X,n} OP Element{Element{X,k},m}.

No tests yet.
Regression test vs unit test - which should I prefer?

[vsavchenko]

Great job, I'm on board with this change!

I think that our code is a bit under commented when it comes to the logic inside of functions, so I would really appreciate if we can add a good chunk of comments here!

Also, I believe integration tests would be pretty much straightforward with clang_analyzer_eval.

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1035–1038

I would prefer having a comment for this line with a very simple formula of the thing we are calculating. I think it can increase the readability of the code because when there is a call accepting a whole bunch of arguments it is never obvious and it always takes time to parse through.

1041

This comment is a bit deceiving IMO. It returns a concrete value even when HasSameMemRegions is false, but from the comment it seems like we evaluate the operator ONLY when HasSameMemRegions is true.

1068

I think it's better to add comments for each case describing what is the situation we handle here in a simplified form.
And for each return within the case - a short comment with the reason.

[steakhal]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1035–1038

Sure, I will add something like this:

// T buf[n];   Element{buf,2} --> 2 * sizeof(T)

1041

No, the comment is up to date.
This lambda handles both equality and inequality operators, and this is why its called EvaluateEqualityOperators.

EQResult will be true only if the two memory regions are the same and the index is zero.
The result of the inequality is just the negated version of the result of equality.

1068

I'm not sure if it's necessary.
I have already described these 3 cases at the beginning.
Quote:

// Handle: \forall MemRegion X, \forall NonLoc n, m:
//  - Element{X,n} OP Element{X,m}
//  - Element{X,n} OP X
//  -            X OP Element{X,n}
// We don't handle here nested ElementRegions like in the this expression:
// Element{Element{x,3,int [10]},5,int}  ==  Element{x,35,int}

If you still insist, I will defenately add more comments though.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1035–1038

Yeah, something like this would be good. I would prefer more explicit version of it simply because Stmt; Smth can be a bit confusing for notation.

1041

If both have the same and the index has a concrete value, we can evaluate equality operators.

In this setting, I assume that we talk about "if and only if", and in any case other than "both have the same and the index has a concrete value" we can't evaluate equality operators.
Also, I didn't say that it is necessarily incorrect, I said that it is deceiving because if it confused me, it can confuse other people as well.

I would prefer something more like this:

// For a situation, a OP b + index, where OP is equality operator, 
// we can infer the result for known `index` values.
// We are able to do this because ...

1068

In that comment, you don't say anything about OP and how we handle those.

Also I want to add that you probably want to add an arbitrary MemRegion Y as well because you handle not only cases when MemRegions are same.

[steakhal]

• Refined documentation comments as noted.
• Added tests.
• Removed the complicated ByteOffsetOfElement lambda.
• Rename revision.

---

Before this patch, only these reported Unknown instead of the currently expected value.
Besides that all tests passed as-is on master:

clang_analyzer_dump_int(p - p0);       // expected-warning {{0 S32b}}
clang_analyzer_dump_int(p - p1);       // expected-warning {{-1 S32b}}
clang_analyzer_dump_int(p - pn);       // expected-warning-re {{0 - (reg_${{[0-9]+}}<int n>)}}
clang_analyzer_dump_int((p + 1) - p);  // expected-warning {{1 S32b}}

// Swapped operands:
clang_analyzer_dump_int(p0 - p);       // expected-warning {{0 S32b}}
clang_analyzer_dump_int(p1 - p);       // expected-warning {{1 S32b}}
clang_analyzer_dump_int(pn - p);       // expected-warning-re {{reg_${{[0-9]+}}<int n>}}
clang_analyzer_dump_int(p - (p + 1));  // expected-warning {{-1 S32b}}

---

Further notes:
Element{X, n, Ty1} and Element{X, m, Ty2} should compare equal if and only if the n * sizeof(Ty1) equals to n * sizeof(Ty2).
However, previously it did not take the size of the types into account (there is the corresponding FIXIT).
I'm not fixing this either for now.

The analyzer returns Unknown for this call:
clang_analyzer_dump_int((p + 1) - q);
However, IMO it should hold the expression 'p+1+q' instead - regardless of p alias (or not) the same memory region of p
There is a FIXME in the testcode for this.

[steakhal]

clang/test/Analysis/pointer-arithmetic.c

88

The suggested expression should be p+1-q.

100

The suggested expression should be q-p+1.

[steakhal]

clang/test/Analysis/pointer-arithmetic.c

88

xD more like (p+1)-q

100

q-(p+1)

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

if (LeftBase != RightBase &&
         return UnknownVal();
       case BO_EQ:
         return makeTruthVal(false, resultTy);
       case BO_NE:
         return makeTruthVal(true, resultTy);
       }
     }
 
-    // Handle special cases for when both regions are element regions.
+    // We simplify the binary expressions of the following forms, by evaluating
+    // the operator.
+    // \forall MemRegion X, \forall NonLoc n, m:
+    //  - Element{X,n} OP Element{X,m}
+    //  - Element{X,n} OP X
+    //  -            X OP Element{X,n}
+    // Where the OP is an equality or subtraction operator. Eg:
+    //   - Element{X,n} - Element{X,m} => n-m
+    //   - Element{X,0} == X           => true
+    //   - Element{X,1} == X           => false
+    // We don't simplify the nested ElementRegions here, such as:
+    // Element{Element{x,3,int [10]},5,int}  ==  Element{x,35,int}
+    {
+      // For a situation, where `a` and `b` are memory regions, and `OP` is an
+      // equality operator, we can infer the result for known `Index` values. We
+      // are able to do this because:
+      //  - If we check for equality:
+      //    The answer is `true` if and only if both regions are the same and
+      //    the `Index` is zero (so the ElementRegion refers to the same item),
+      //    `false` otherwise.
+      //  - If we check for inequality:
+      //    The answer is `true` if and only if either the regions are different
+      //    or the `Index` is known to be non-zero.
+      const auto EvaluateEqualityOperators =
+          [this, state, op, resultTy](NonLoc Index,
+                                      bool HasSameMemRegions) -> SVal {
+        assert(BinaryOperator::isEqualityOp(op));
+        const llvm::APSInt *Int = getKnownValue(state, Index);
+        if (!Int)
+          return UnknownVal();
+
+        const bool EQResult = HasSameMemRegions && *Int == 0;
+        return makeTruthVal(op == BO_EQ ? EQResult : !EQResult, resultTy);
+      };
+
       const ElementRegion *RightER = dyn_cast<ElementRegion>(RightMR);
       const ElementRegion *LeftER = dyn_cast<ElementRegion>(LeftMR);
       if (RightER && LeftER) {
-      // Next, see if the two ERs have the same super-region and matching types.
+        // Next, see if the two ERs have the same super-region and matching
+        // types.
         // FIXME: This should do something useful even if the types don't match,
         // though if both indexes are constant the RegionRawOffset path will
         // give the correct answer.
         if (LeftER->getSuperRegion() == RightER->getSuperRegion() &&
             LeftER->getElementType() == RightER->getElementType()) {
-        // Get the left index and cast it to the correct type.
-        // If the index is unknown or undefined, bail out here.
-        SVal LeftIndexVal = LeftER->getIndex();
-        Optional<NonLoc> LeftIndex = LeftIndexVal.getAs<NonLoc>();
-        if (!LeftIndex)
-          return UnknownVal();
-        LeftIndexVal = evalCastFromNonLoc(*LeftIndex, ArrayIndexTy);
-        LeftIndex = LeftIndexVal.getAs<NonLoc>();
-        if (!LeftIndex)
-          return UnknownVal();
-
-        // Do the same for the right index.
-        SVal RightIndexVal = RightER->getIndex();
-        Optional<NonLoc> RightIndex = RightIndexVal.getAs<NonLoc>();
-        if (!RightIndex)
-          return UnknownVal();
-        RightIndexVal = evalCastFromNonLoc(*RightIndex, ArrayIndexTy);
-        RightIndex = RightIndexVal.getAs<NonLoc>();
-        if (!RightIndex)
-          return UnknownVal();
-
-        // Actually perform the operation.
-        // evalBinOpNN expects the two indexes to already be the right type.
-        return evalBinOpNN(state, op, *LeftIndex, *RightIndex, resultTy);
+          return evalBinOpNN(state, op, LeftER->getIndex(), RightER->getIndex(),
+                             resultTy);
+        }
+      } else if (LeftER && !RightER) {
+        NonLoc LeftIndex = LeftER->getIndex();
+        const bool HasSameMemRegions = LeftER->getSuperRegion() == RightMR;
+
+        if (BinaryOperator::isEqualityOp(op))
+          return EvaluateEqualityOperators(LeftIndex, HasSameMemRegions);
+
+        if (op == BO_Sub && HasSameMemRegions)
+          return LeftIndex;
+        return UnknownVal();
+      } else if (!LeftER && RightER) {
+        NonLoc RightIndex = RightER->getIndex();
+        const bool HasSameMemRegions = LeftMR == RightER->getSuperRegion();
+
+        if (BinaryOperator::isEqualityOp(op))
+          return EvaluateEqualityOperators(RightIndex, HasSameMemRegions);
+
+        // FIXME: Consider refactoring evalMinus function to accept the State
+        // as well, and use it here.
+        if (op == BO_Sub && HasSameMemRegions)
+          return evalBinOpNN(state, BO_Sub, makeZeroArrayIndex(), RightIndex,
+                             ArrayIndexTy);
+        return UnknownVal();
       }
     }
 
     // Special handling of the FieldRegions, even with symbolic offsets.
     const FieldRegion *RightFR = dyn_cast<FieldRegion>(RightMR);
     const FieldRegion *LeftFR = dyn_cast<FieldRegion>(LeftMR);
     if (RightFR && LeftFR) {
       SVal R = evalBinOpFieldRegionFieldRegion(LeftFR, RightFR, op, resultTy,
                                                *this);
       if (!R.isUnknown())
         return R;
     }
 
     // Compare the regions using the raw offsets.
     RegionOffset LeftOffset = LeftMR->getAsOffset();
     RegionOffset RightOffset = RightMR->getAsOffset();
 
     if (LeftOffset.getRegion() != nullptr &&
         LeftOffset.getRegion() == RightOffset.getRegion() &&
         !LeftOffset.hasSymbolicOffset() && !RightOffset.hasSymbolicOffset()) {
       int64_t left = LeftOffset.getOffset();
       int64_t right = RightOffset.getOffset();
 

clang/test/Analysis/pointer-arithmetic.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false -verify %s
+
+void clang_analyzer_eval(int);
+void clang_analyzer_dump_ptr(int *);
+void clang_analyzer_dump_int(int);
 
 int test1() {
   int *p = (int *)sizeof(int);
   p -= 1;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
 int test2() {

 
 int test4() {
   // This is a special case where pointer arithmetic is not calculated to
   // preserve useful warnings on dereferences of null pointers.
   int *p = 0;
   p += 1;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
+
+void simplify_symregion_and_elementregion_pointer_arithmetic_and_comparison(int *p, int n, int m, int *q) {
+  // 'q' is SymReg{q}
+  // 'p' is SymReg{p}
+  int *p1 = p + 1;  // Element{p,1}
+  int *p0 = p1 - 1; // Element{p,0}
+  int *pn = p + n;  // Element{p,n}
+  int *pm = p + m;  // Element{p,m}
+
+  clang_analyzer_dump_ptr(q);
+  clang_analyzer_dump_ptr(p);
+  clang_analyzer_dump_ptr(p0);
+  clang_analyzer_dump_ptr(p1);
+  clang_analyzer_dump_ptr(pn);
+  clang_analyzer_dump_ptr(pm);
+  // expected-warning-re@-6 {{&SymRegion{reg_${{[0-9]+}}<int * q>}}}
+  // expected-warning-re@-6 {{&SymRegion{reg_${{[0-9]+}}<int * p>}}}
+  // expected-warning-re@-6 {{&Element{SymRegion{reg_${{[0-9]+}}<int * p>},0 S64b,int}}}}
+  // expected-warning-re@-6 {{&Element{SymRegion{reg_${{[0-9]+}}<int * p>},1 S64b,int}}}
+  // expected-warning-re@-6 {{&Element{SymRegion{reg_${{[0-9]+}}<int * p>},reg_${{[0-9]+}}<int n>,int}}}
+  // expected-warning-re@-6 {{&Element{SymRegion{reg_${{[0-9]+}}<int * p>},reg_${{[0-9]+}}<int m>,int}}}
+
+  // Test the equality operator:
+  clang_analyzer_eval(p == p0);  // expected-warning {{TRUE}}
+  clang_analyzer_eval(p == p1);  // expected-warning {{FALSE}}
+  clang_analyzer_eval(p1 == pn); // expected-warning {{UNKNOWN}}
+  clang_analyzer_eval(pn == pm); // expected-warning {{UNKNOWN}}
+
+  // Reverse operands:
+  clang_analyzer_eval(p0 == p);  // expected-warning {{TRUE}}
+  clang_analyzer_eval(p1 == p);  // expected-warning {{FALSE}}
+  clang_analyzer_eval(pn == p1); // expected-warning {{UNKNOWN}}
+  clang_analyzer_eval(pm == pn); // expected-warning {{UNKNOWN}}
+
+  // Test the inequality operator:
+  clang_analyzer_eval(p != p0);  // expected-warning {{FALSE}}
+  clang_analyzer_eval(p != p1);  // expected-warning {{TRUE}}
+  clang_analyzer_eval(p1 != pn); // expected-warning {{UNKNOWN}}
+  clang_analyzer_eval(pn != pm); // expected-warning {{UNKNOWN}}
+
+  // Reverse operands:
+  clang_analyzer_eval(p0 != p);  // expected-warning {{FALSE}}
+  clang_analyzer_eval(p1 != p);  // expected-warning {{TRUE}}
+  clang_analyzer_eval(pn != p1); // expected-warning {{UNKNOWN}}
+  clang_analyzer_eval(pm != pn); // expected-warning {{UNKNOWN}}
+
+  // Test the subtraction operator:
+  clang_analyzer_dump_int(p - q);        // expected-warning-re {{(reg_${{[0-9]+}}<int * p>) - (reg_${{[0-9]+}}<int * q>)}}
+  clang_analyzer_dump_int(p - p);        // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int(p - p0);       // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int(p - p1);       // expected-warning {{-1 S32b}}
+  clang_analyzer_dump_int(p - pn);       // expected-warning-re {{0 - (reg_${{[0-9]+}}<int n>)}}
+  clang_analyzer_dump_int((p + 1) - q);  // expected-warning {{Unknown}} // FIXME: Might point to the same region, we should hold the expression 'p+1+q' instead.
+  clang_analyzer_dump_int((p + 1) - p);  // expected-warning {{1 S32b}}
+  clang_analyzer_dump_int((p + 1) - p0); // expected-warning {{1 S32b}}
+  clang_analyzer_dump_int((p + 1) - p1); // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int((p + 1) - pn); // expected-warning-re {{1 - (reg_${{[0-9]+}}<int n>)}}
+
+  // Reverse operands:
+  clang_analyzer_dump_int(q - p);        // expected-warning-re {{(reg_${{[0-9]+}}<int * q>) - (reg_${{[0-9]+}}<int * p>)}}
+  clang_analyzer_dump_int(p - p);        // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int(p0 - p);       // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int(p1 - p);       // expected-warning {{1 S32b}}
+  clang_analyzer_dump_int(pn - p);       // expected-warning-re {{reg_${{[0-9]+}}<int n>}}
+  clang_analyzer_dump_int(q - (p + 1));  // expected-warning {{Unknown}} // FIXME: Might point to the same region, we should hold the expression 'p+1+q' instead.
+  clang_analyzer_dump_int(p - (p + 1));  // expected-warning {{-1 S32b}}
+  clang_analyzer_dump_int(p0 - (p + 1)); // expected-warning {{-1 S32b}}
+  clang_analyzer_dump_int(p1 - (p + 1)); // expected-warning {{0 S32b}}
+  clang_analyzer_dump_int(pn - (p + 1)); // expected-warning-re {{(reg_${{[0-9]+}}<int n>) - 1}}
+}
+
+void clang_analyzer_dump_ptrarray(int (*p)[10]);
+void test_arrays(int (*p)[10]) {
+  int(*pp)[10] = p + 2;
+  clang_analyzer_dump_ptrarray(p);  // expected-warning-re {{&SymRegion{reg_${{[0-9]+}}<int (*)[10] p>}}}
+  clang_analyzer_dump_ptrarray(pp); // expected-warning-re {{&Element{SymRegion{reg_${{[0-9]+}}<int (*)[10] p>},2 S64b,int [10]}}}
+
+  // Assuming a casual x86 architecture:
+  int *q = (int *)p;
+  int *qq = q + 10 * 2;
+  clang_analyzer_dump_ptr(q);              // expected-warning-re {{&Element{SymRegion{reg_${{[0-9]+}}<int (*)[10] p>},0 S64b,int}}}
+  clang_analyzer_dump_ptr(qq);             // expected-warning-re {{&Element{SymRegion{reg_${{[0-9]+}}<int (*)[10] p>},20 S64b,int}}}
+  clang_analyzer_dump_ptrarray(pp);        // expected-warning-re {{&Element{SymRegion{reg_${{[0-9]+}}<int (*)[10] p>},2 S64b,int [10]}}}
+  clang_analyzer_dump_int(qq - (int *)pp); // expected-warning {{0 S32b}}
+}