[analyzer] Enable support for symbolic extension/truncation

[mikhail.ramalho]

Summary

Generate symbolic extension and truncation constraints where supported by the underlying constraint manager, currently limited to Z3. Also fix integer type bug with Z3ConstraintManager, and support comparison of APSInt with different types in SimpleConstraintManager.

[rgov]

Are all the changes here related to the extension/truncation support, for instance the changes to test/Analysis/malloc.c? Can you move misc. cleanup changes to another review?

[ddcc]

When I was testing this patch, it was on top of both D28952 and D28953. For malloc.c, the change on line 1708 from int to size_t is necessary to prevent a false positive warning at line 1710. The other three type changes in that file don't affect the testcase output, but I probably made the changes at the same time. Do you want those other three pulled out separately?

In general, I think all the changes are related to the commit, or were other instances of a testcase related fix in the same file.

[NoQ]

In D28955#652443, @ddcc wrote:

When I was testing this patch, it was on top of both D28952 and D28953. For malloc.c, the change on line 1708 from int to size_t is necessary to prevent a false positive warning at line 1710.

We should have expected-warning on 64-bit targets (where size_t easily overflows int) and no-warning on 32-bit targets (where they are of the same size and the fix for the original issue https://llvm.org/bugs/show_bug.cgi?id=16558 applies). I think we should have two run-lines for this test, with two concrete targets specified; it'd be great to actually have other tests in this file undergo such trial.

[ddcc]

We should have expected-warning on 64-bit targets (where size_t easily overflows int) and no-warning on 32-bit targets (where they are of the same size and the fix for the original issue https://llvm.org/bugs/show_bug.cgi?id=16558 applies). I think we should have two run-lines for this test, with two concrete targets specified; it'd be great to actually have other tests in this file undergo such trial.

To clarify, you're asking for something like the following, instead of changing from int to size_t?

diff --git a/test/Analysis/malloc.c b/test/Analysis/malloc.c
index 42deb9f..80e4184 100644
--- a/test/Analysis/malloc.c
+++ b/test/Analysis/malloc.c
@@ -1,4 +1,5 @@
-// RUN: %clang_cc1 %z3_cc1 -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s
+// RUN: %clang_cc1 %z3_cc1 -triple i386-unknown-linux -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s
+// RUN: %clang_cc1 %z3_cc1 -triple x86_64-unknown-linux -Dx86_64 -analyze -analyzer-checker=core,alpha.deadcode.UnreachableCode,alpha.core.CastSize,unix.Malloc,debug.ExprInspection -analyzer-store=region -verify %s

 #include "Inputs/system-header-simulator.h"

@@ -1705,9 +1706,13 @@ void *smallocNoWarn(size_t size) {
 }

 char *dupstrNoWarn(const char *s) {
-  const size_t len = strlen(s);
+  const int len = strlen(s);
   char *p = (char*) smallocNoWarn(len + 1);
-  strcpy(p, s); // no-warning
+#ifdef x86_64
+  strcpy(p, s); // expected-warning{{String copy function overflows destination buffer}}
+#else
+  strcpy(p, s); // no warning
+#endif
   return p;
 }

[ddcc]

Rebase

[ddcc]

Rebase

[ddcc]

@dcoughlin : ping

[dcoughlin]

@ddcc : When I run this I get a bunch of assertion failures. Does this depend on https://reviews.llvm.org/D28953? (Which was reverted) Is it subsumed by https://reviews.llvm.org/D35450?

Is this blocking on a review of another patch on our end?

[ddcc]

Rebase, factor out floating-point changes, fix Z3 type bug, support general APSInt comparison

[ddcc]

@dcoughlin No, all three patches are separate. I have been testing them with each applied incrementally onto the previous, in the order trunk, D35450, D28954, then D28955 (this). But since these are a lot of dependencies, I've refactored this patch to apply directly on top of D35450, though the floating-point specific changes will need to be merged into D28954. Also, I think D28954 is waiting for review.

[ddcc]

@NoQ Does the proposal in https://reviews.llvm.org/D28955#652465 satisfy your concern?

[NoQ]

@mikhail.ramalho brought this up in pr41809 so let's revisit this.

Like, the patch looks great, the idea looks great, but i'd like to make super duper sure that the behavior without Z3 remains the same, because we are in no position to give up on the no-Z3 mode yet.

test/Analysis/PR3991.m

63 ↗

(On Diff #113619)

This looks like a regression to me. Even though BoolAssignment is an alpha checker, it's definitely one of the good ones, which i want to enable by default sooner rather than later, so can we try not to regress it too much?

test/Analysis/std-c-library-functions.c

149 ↗

(On Diff #113619)

Why did this have to change? I don't remember all the details of how these functions work, but as far as i remember the only character that is printable but not graphical is the space character (32) which converts between int and char just fine.

[ddcc]

I don't have the time to rebase and retest this currently, so it might be better for someone else to take over this patch. Unfortunately, it's been long enough that I don't remember the details of these changes.

[NoQ]

@ddcc, sure, np!

[mikhail.ramalho]

I can give some help here, but my time is quite limited as well :/

Let me at least rebase against master.

[mikhail.ramalho]

Two changes:

• Moved the BoolAssignmentChecker changes to separate revision (D73062).
• Rebased on top of master.

There are a few cases failing, some because clang is trying to match some strings printed by the ranged constraint manager and there is at least 1 segfault.

[NoQ]

Thanks for picking this up!~

Hmm, why did the change in MallocChecker tests disappear?

clang is trying to match some strings printed by the ranged constraint manager

Are these state dump tests / exploded-graph-rewriter tests? We'll need to ignore/silence them in Z3 mode.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

#endif
   /// Convenience method to query the state to see if a symbol is null or
   /// not null, or if neither assumption can be made.
   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 
     return checkNull(State, Sym);
   }
 
+  /// canReasonAboutSymbolicExtTrunc - Not all ConstraintManagers can reason
+  ///  symbolic extension and truncation. Used this to ask directly when
+  ///  building SVals.
+  virtual bool canReasonAboutSymbolicExtTrunc() const = 0;
+
 protected:
   /// A flag to indicate that clients should be notified of assumptions.
   /// By default this is the case, but sometimes this needs to be restricted
   /// to avoid infinite recursions within the ConstraintManager.
   ///
   /// Note that this flag allows the ConstraintManager to be re-entrant,
   /// but not thread-safe.
   bool NotifyAssumeClients = true;

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
     }
 
     llvm_unreachable("Unsupported expression to reason about!");
   }
 
+  bool canReasonAboutSymbolicExtTrunc() const override {
+    return Solver->isExtTruncSupported();
+  }
+
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
                                      const llvm::SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

SValBuilder(llvm::BumpPtrAllocator &alloc, ASTContext &context,
               ProgramStateManager &stateMgr)
       : Context(context), BasicVals(context, alloc),
         SymMgr(context, BasicVals, alloc), MemMgr(context, alloc),
         StateMgr(stateMgr), ArrayIndexTy(context.LongLongTy),
         ArrayIndexWidth(context.getTypeSize(ArrayIndexTy)) {}
 
   virtual ~SValBuilder() = default;
 
-  bool haveSameType(const SymExpr *Sym1, const SymExpr *Sym2) {
-    return haveSameType(Sym1->getType(), Sym2->getType());
-  }
-
   bool haveSameType(QualType Ty1, QualType Ty2) {
-    // FIXME: Remove the second disjunct when we support symbolic
-    // truncation/extension.
-    return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
-            (Ty1->isIntegralOrEnumerationType() &&
-             Ty2->isIntegralOrEnumerationType()));
+    return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2));
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);
 
   // Handles casts of type CK_IntegralCast.
   SVal evalIntegralCast(ProgramStateRef state, SVal val, QualType castTy,
                         QualType originalType);
 

clang/lib/StaticAnalyzer/Core/ProgramState.cpp

SVal ProgramState::getSVal(Loc location, QualType T) const {
   // If 'V' is a symbolic value that is *perfectly* constrained to
   // be a constant value, use that value instead to lessen the burden
   // on later analysis stages (so we have less symbolic values to reason
   // about).
   // We only go into this branch if we can convert the APSInt value we have
   // to the type of T, which is not always the case (e.g. for void).
   if (!T.isNull() && (T->isIntegralOrEnumerationType() || Loc::isLocType(T))) {
     if (SymbolRef sym = V.getAsSymbol()) {
-      if (const llvm::APSInt *Int = getStateManager()
-                                    .getConstraintManager()
-                                    .getSymVal(this, sym)) {
+      ConstraintManager &CM = getStateManager().getConstraintManager();
+
+      if (const llvm::APSInt *Int = CM.getSymVal(this, sym)) {
         // FIXME: Because we don't correctly model (yet) sign-extension
         // and truncation of symbolic values, we need to convert
-        // the integer value to the correct signedness and bitwidth.
+        // the integer value to the correct signedness and
         //
         // This shows up in the following:
         //
         //   char foo();
         //   unsigned x = foo();
         //   if (x == 54)
         //     ...
         //
         //  The symbolic value stored to 'x' is actually the conjured
         //  symbol for the call to foo(); the type of that symbol is 'char',
         //  not unsigned.
-        const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int);
+        if (!CM.canReasonAboutSymbolicExtTrunc())
+          Int = &getBasicVals().Convert(T, *Int);
 
         if (V.getAs<Loc>())
-          return loc::ConcreteInt(NewV);
+          return loc::ConcreteInt(*Int);
         else
-          return nonloc::ConcreteInt(NewV);
+          return nonloc::ConcreteInt(*Int);
       }
     }
   }
 
   return V;
 }
 
 ProgramStateRef ProgramState::BindExpr(const Stmt *S,

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

public:
 
   bool haveEqualConstraints(ProgramStateRef S1,
                             ProgramStateRef S2) const override {
     return S1->get<ConstraintRange>() == S2->get<ConstraintRange>();
   }
 
   bool canReasonAbout(SVal X) const override;
 
+  bool canReasonAboutSymbolicExtTrunc() const override;
+
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
 
   ProgramStateRef removeDeadBindings(ProgramStateRef State,
                                      SymbolReaper &SymReaper) override;
 
if (SymVal && SymVal->isExpression()) {
     }
 
     return false;
   }
 
   return true;
 }
 
+bool RangeConstraintManager::canReasonAboutSymbolicExtTrunc() const {
+  return false;
+}
+
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
                                                     SymbolRef Sym) {
   const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
 
   // If we don't have any information about this symbol, it's underconstrained.
   if (!Ranges)
     return ConditionTruthVal();
 

clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
   case nonloc::SymbolValKind: {
     if (SymbolRef Sym = Value.getAsSymbol())
       return assumeSymInclusiveRange(State, Sym, From, To, InRange);
     return State;
   } // end switch
 
   case nonloc::ConcreteIntKind: {
     const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
-    bool IsInRange = IntVal >= From && IntVal <= To;
+    bool IsInRange = llvm::APSInt::compareValues(IntVal, From) != -1 &&
+                     llvm::APSInt::compareValues(IntVal, To) != 1;
     bool isFeasible = (IsInRange == InRange);
     return isFeasible ? State : nullptr;
   }
   } // end switch
 }
 
 } // end of namespace ento
 
 } // end of namespace clang

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

 
 SVal SimpleSValBuilder::dispatchCast(SVal Val, QualType CastTy) {
   assert(Val.getAs<Loc>() || Val.getAs<NonLoc>());
   return Val.getAs<Loc>() ? evalCastFromLoc(Val.castAs<Loc>(), CastTy)
                            : evalCastFromNonLoc(Val.castAs<NonLoc>(), CastTy);
 }
 
 SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) {
+  ConstraintManager &CM = getStateManager().getConstraintManager();
+
   bool isLocType = Loc::isLocType(castTy);
   if (val.getAs<nonloc::PointerToMember>())
     return val;
 
   if (Optional<nonloc::LocAsInteger> LI = val.getAs<nonloc::LocAsInteger>()) {
     if (isLocType)
       return LI->getLoc();
+
     // FIXME: Correctly support promotions/truncations.
-    unsigned castSize = Context.getIntWidth(castTy);
-    if (castSize == LI->getNumBits())
+    unsigned castSize = Context.getTypeSize(castTy);
+    if (!CM.canReasonAboutSymbolicExtTrunc() && castSize == LI->getNumBits())
       return val;
+
     return makeLocAsInteger(LI->getLoc(), castSize);
   }
 
   if (const SymExpr *se = val.getAsSymbolicExpression()) {
     QualType T = Context.getCanonicalType(se->getType());
-    // If types are the same or both are integers, ignore the cast.
+    // If types are the same, ignore the cast.
+    if (haveSameType(T, castTy))
+      return val;
+
+    // If types are both integers, ignore the cast.
     // FIXME: Remove this hack when we support symbolic truncation/extension.
     // HACK: If both castTy and T are integers, ignore the cast.  This is
     // not a permanent solution.  Eventually we want to precisely handle
     // extension/truncation of symbolic integers.  This prevents us from losing
     // precision when we assign 'x = y' and 'y' is symbolic and x and y are
     // different integer types.
-   if (haveSameType(T, castTy))
+    if (!CM.canReasonAboutSymbolicExtTrunc() &&
+        (T->isIntegralOrEnumerationType() &&
+        castTy->isIntegralOrEnumerationType()))
       return val;
 
-    if (!isLocType)
-      return makeNonLoc(se, T, castTy);
+    if (isLocType)
       return UnknownVal();
+
+    return makeNonLoc(se, T, castTy);
   }
 
   // If value is a non-integer constant, produce unknown.
   if (!val.getAs<nonloc::ConcreteInt>())
     return UnknownVal();
 
   // Handle casts to a boolean type.
   if (castTy->isBooleanType()) {

clang/lib/StaticAnalyzer/Core/Store.cpp

SVal StoreManager::getLValueElement(QualType elementType, NonLoc Offset,
   if (!Offset.getAs<nonloc::ConcreteInt>()) {
     if (isa<ElementRegion>(BaseRegion->StripCasts()))
       return UnknownVal();
 
     return loc::MemRegionVal(MRMgr.getElementRegion(
         elementType, Offset, cast<SubRegion>(ElemR->getSuperRegion()), Ctx));
   }
 
-  const llvm::APSInt& OffI = Offset.castAs<nonloc::ConcreteInt>().getValue();
+  // FIXME: This isn't quite correct, but avoids casting the Offset symbol
+  llvm::APSInt OffI = APSIntType(BaseIdxI).convert(
+      Offset.castAs<nonloc::ConcreteInt>().getValue());
   assert(BaseIdxI.isSigned());
 
   // Compute the new index.
   nonloc::ConcreteInt NewIdx(svalBuilder.getBasicValueFactory().getValue(BaseIdxI +
                                                                     OffI));
 
   // Construct the new ElementRegion.
   const SubRegion *ArrayR = cast<SubRegion>(ElemR->getSuperRegion());

llvm/include/llvm/Support/SMTAPI.h

public:
   virtual void pop(unsigned NumStates = 1) = 0;
 
   /// Reset the solver and remove all constraints.
   virtual void reset() = 0;
 
   /// Checks if the solver supports floating-points.
   virtual bool isFPSupported() = 0;
 
+  /// Checks if the solver supports extension/truncation.
+  virtual bool isExtTruncSupported() = 0;
+
   virtual void print(raw_ostream &OS) const = 0;
 };
 
 /// Shared pointer for SMTSolvers.
 using SMTSolverRef = std::shared_ptr<SMTSolver>;
 
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
 } // namespace llvm
 
 #endif

llvm/lib/Support/Z3Solver.cpp

public:
 
   void pop(unsigned NumStates = 1) override {
     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
     return Z3_solver_pop(Context.Context, Solver, NumStates);
   }
 
   bool isFPSupported() override { return true; }
 
+  bool isExtTruncSupported() override { return true; }
+
   /// Reset the solver and remove all constraints.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
 }; // end class Z3Solver