martong created this revision.
martong added reviewers: steakhal, NoQ, vsavchenko.
Herald added subscribers: ASDenysPetrov, gamesh411, dkrupp, donat.nagy, 
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, 
xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Currently, if we have a constraint on a binary operand and then we add
another constraint to any of the binop's sub-expression then the first
constraint is not considered by the engine:

  int foo() {
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK.
    if (y != 0)
      return 0;
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}} OK.
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} FAILS!
  }

Interestingly, if we constrain first y and then (x + y) then the
behaviour is what we'd normally expect:

  int foo() {
    if (y != 0)
      return 0;
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK.
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}} OK.
  }

The discrepancy stems from the underlying implementation of the engine:
In the latter case, the Environment of the current ExplodedNode has a
(x + y) -> [0, 0] binding. However, in the first case we have a [y] -> 0
binding in the current ExplodedNode, and when we build the SVal for the
(x + y) expression we simply build up the [x + 0] SVal, i.e. we never
try to find the constraint for (x + y).

In this patch, I add a StmtVisitor that builds up an SVal that
constitutes only from LValue SVals. This SVal then can be used to query
the constraint manager, this way we can find the desired constraint.

Alternative implementation could have been to traverse back in the
Exploded Graph to the Node where we can find the original binding of the
x + y expression. This seemed to be a far from ideal approach as we may
not know how far should we traverse back.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D102696

Files:
  clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
  clang/test/Analysis/find-binop-constraints.cpp

Index: clang/test/Analysis/find-binop-constraints.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/find-binop-constraints.cpp
@@ -0,0 +1,90 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+void clang_analyzer_eval(bool);
+
+int test_legacy_behavior(int x, int y) {
+  if (y != 0)
+    return 0;
+  if (x + y != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
+  return y / (x + y);              // expected-warning{{Division by zero}}
+}
+
+int test_rhs_further_constrained(int x, int y) {
+  if (x + y != 0)
+    return 0;
+  if (y != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_lhs_further_constrained(int x, int y) {
+  if (x + y != 0)
+    return 0;
+  if (x != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x == 0);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_lhs_and_rhs_further_constrained(int x, int y) {
+  if (x % y != 1)
+    return 0;
+  if (x != 1)
+    return 0;
+  if (y != 1)
+    return 0;
+  clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 1);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
+  switch (a) {
+  case 1: {
+    if (x + y + z != 0)
+      return 0;
+    if (z != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 2: {
+    if (x + y + z != 0)
+      return 0;
+    if (y != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 3: {
+    if (x + y + z != 0)
+      return 0;
+    if (x != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 4: {
+    if (x + y + z != 0)
+      return 0;
+    if (x + y != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}}
+    break;
+  }
+  }
+  return 0;
+}
Index: clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -10,8 +10,9 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "clang/AST/ExprCXX.h"
 #include "clang/AST/DeclCXX.h"
+#include "clang/AST/ExprCXX.h"
+#include "clang/AST/StmtVisitor.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 
@@ -37,10 +38,47 @@
   return Symbol;
 }
 
+// This class is responsible to build such an SVal for a BinOp expression where
+// all constituent SVals are representing an LValue expression. We use it to
+// query constraints that are attached directly to the BinOp.
+class LValueSValBuilder : public ConstStmtVisitor<LValueSValBuilder, SVal> {
+  QualType T;
+  const LocationContext *LCtx;
+  ProgramStateRef State;
+  SValBuilder &SvalBuilder;
+
+public:
+  LValueSValBuilder(QualType T, const LocationContext *LCtx,
+                    ProgramStateRef State, SValBuilder &SvalBuilder)
+      : T(T), LCtx(LCtx), State(State), SvalBuilder(SvalBuilder) {}
+
+  SVal VisitImplicitCastExpr(const ImplicitCastExpr *E) {
+    if (E->getCastKind() == CK_LValueToRValue) {
+      SVal LValue = State->getSVal(E->getSubExpr(), LCtx); // LValue.
+      if (Optional<Loc> LValueLoc = LValue.getAs<Loc>())
+        return State->getRawSVal(*LValueLoc, T);
+    }
+    return SVal();
+  }
+  SVal VisitBinaryOperator(const BinaryOperator *B) {
+    SVal L = Visit(B->getLHS());
+    SVal R = Visit(B->getRHS());
+    if (L.isUndef() || R.isUndef())
+      return SVal();
+    Optional<NonLoc> LNL = L.getAs<NonLoc>();
+    Optional<NonLoc> RNL = R.getAs<NonLoc>();
+    if (!LNL || !RNL)
+      return SVal();
+    SVal SymSym =
+        SvalBuilder.makeSymExprValNN(B->getOpcode(), *LNL, *RNL, B->getType());
+    return SymSym;
+  }
+  SVal VisitExpr(const Expr *E) { return SVal(); }
+};
+
 void ExprEngine::VisitBinaryOperator(const BinaryOperator* B,
                                      ExplodedNode *Pred,
                                      ExplodedNodeSet &Dst) {
-
   Expr *LHS = B->getLHS()->IgnoreParens();
   Expr *RHS = B->getRHS()->IgnoreParens();
 
@@ -95,9 +133,19 @@
       if (B->getOpcode() == BO_PtrMemD)
         state = createTemporaryRegionIfNeeded(state, LCtx, LHS);
 
-      // Process non-assignments except commas or short-circuited
-      // logical expressions (LAnd and LOr).
-      SVal Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
+      SVal Result;
+      // Query any constraint that may be directly attached to the BinOp.
+      SVal LValueSymExpr =
+          LValueSValBuilder(B->getType(), LCtx, state, svalBuilder).Visit(B);
+      const llvm::APSInt *KnownInt =
+          state->getStateManager().getConstraintManager().getSymVal(
+              state, LValueSymExpr.getAsSymbol());
+      if (KnownInt)
+        Result = svalBuilder.makeIntVal(*KnownInt);
+      // Fall-back to the constant folding mechanism.
+      if (Result.isUndef())
+        Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
+
       if (!Result.isUnknown()) {
         state = state->BindExpr(B, LCtx, Result);
       } else {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to