[PATCH] D30489: [analyzer] catch out of bounds for VLA

[Daniel Marjamäki via Phabricator via cfe-commits]

danielmarjamaki updated this revision to Diff 94509.
danielmarjamaki added a comment.

This is just work in progress!!

With these changes Clang static analyzer will detect overflow in this sample code:

  void foo(int X) {
    char *Data = new char[X];
    Data[X] = 0; // <- error
    delete[] Data;
  }

I updated SimpleSValBuilder so evalEQ can calculate a SVal when both lhs and rhs are symbols. Source code that used to have problems:

  DefinedOrUnknownSVal extentMatchesSize = svalBuilder.evalEQ(
      State, Extent, SizeInBytes.castAs<DefinedOrUnknownSVal>());

Inputs: Extent is "extent_$3{SymRegion{conj_$1{char *}}}" and SizeInBytes is "reg_$0<int X>".

Before my quick fix the return SVal is "Unknown".
With my quick fix it will return a SVal "(extent_$3{SymRegion{conj_$1{char *}}}) == (reg_$0<int X>)".

I also made a simple fix for the ConstraintManager. If the state says X==Y then the ConstraintManager should be able to evaluate Y>=X. My evalUgly loops through the constraints and matches them manually.

Do you have some feedback? Do you think my SimpleSValBuilder approach is fine to commit if I polish it? It was just a quick hack so I guess it might make some tests fail etc.

About the ConstraintManager fix. Is it a good idea to handle simple SymSymExpr constraints? Or should this be handled by Z3 instead?


Repository:
  rL LLVM

https://reviews.llvm.org/D30489

Files:
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp


Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -547,6 +547,13 @@
       if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
         return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
 
+      if (!state->isTainted(rhs) && !state->isTainted(lhs)) {
+        const SymExpr *lhse = lhs.getAsSymExpr();
+        const SymExpr *rhse = rhs.getAsSymExpr();
+        return nonloc::SymbolVal(
+            SymMgr.getSymSymExpr(lhse, op, rhse, resultTy));
+      }
+
       // Give up -- this is not a symbolic expression we can handle.
       return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
     }
Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -53,6 +53,19 @@
 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
                                                    NonLoc Cond,
                                                    bool Assumption) {
+  if (1) {
+    Optional<nonloc::SymbolVal> SymVal = Cond.getAs<nonloc::SymbolVal>();
+    if (SymVal && SymVal->isExpression()) {
+      const SymExpr *SE = SymVal->getSymbol();
+      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+        if (SSE->getOpcode() == BO_GE) {
+          SymSymExpr SSE2(SSE->getRHS(), BO_EQ, SSE->getLHS(), SSE->getType());
+          if (State->getConstraintManager().uglyEval(&SSE2, State))
+            return Assumption ? State : nullptr;
+        }
+      }
+    }
+  }
 
   // We cannot reason about SymSymExprs, and can only reason about some
   // SymIntExprs.
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -287,6 +287,8 @@
   RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
       : RangedConstraintManager(SE, SVB) {}
 
+  virtual bool uglyEval(const SymSymExpr *SSE, ProgramStateRef state);
+
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
@@ -723,6 +725,25 @@
 // Pretty-printing.
 //===------------------------------------------------------------------------===/
 
+bool RangeConstraintManager::uglyEval(const SymSymExpr *SSE,
+                                      ProgramStateRef State) {
+  ConstraintRangeTy Ranges = State->get<ConstraintRange>();
+  for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
+       ++I) {
+    SymbolRef SR = I.getKey();
+    if (const SymSymExpr *SSE2 = dyn_cast<SymSymExpr>(SR)) {
+      if (SSE->getOpcode() != SSE2->getOpcode())
+        continue;
+      if (SSE->getLHS() != SSE2->getLHS())
+        continue;
+      if (SSE->getRHS() != SSE2->getRHS())
+        continue;
+      return true;
+    }
+  }
+  return false;
+}
+
 void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
                                    const char *nl, const char *sep) {
 
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -63,9 +63,12 @@
 public:
   ConstraintManager() : NotifyAssumeClients(true) {}
 
+  virtual bool uglyEval(const SymSymExpr *SSE, ProgramStateRef state) {
+    return false;
+  }
+
   virtual ~ConstraintManager();
-  virtual ProgramStateRef assume(ProgramStateRef state,
-                                 DefinedSVal Cond,
+  virtual ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
                                  bool Assumption) = 0;
 
   typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair;


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D30489.94509.patch
Type: text/x-patch
Size: 4251 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20170410/20c0108c/attachment-0001.bin>