Added constaints for pointers: for alignment and size of underlying o…

…bjects. Fixed type creation for C++ types, fixed tests for types and added for alignment.

include/klee/Module/KType.h

@@ -36,6 +36,16 @@ class KType {
    */
   TypeManager *parent;
 
+  /**
+   * Alignment in bytes for this type.
+   */
+  size_t alignment = 1;
+
+  /**
+   * Size of type.
+   */
+  size_t typeStoreSize = 0;
+
   /**
    * Innner types. Maps type to their offsets in current
    * type. Should contain type itself and
@@ -73,6 +83,23 @@ class KType {
    */
   llvm::Type *getRawType() const;
 
+  /**
+   * Getter for the size.
+   */
+  size_t getSize() const;
+
+  /**
+   * Getter for the alignment.
+   */
+  size_t getAlignment() const;
+
+  /**
+   * Return alignment requirements for that object and
+   * it subobjects. If no such restrictions can be applied
+   * returns ref to null expression.
+   */
+  virtual ref<Expr> getContentRestrictions(ref<Expr>) const;
+
   TypeSystemKind getTypeSystemKind() const;
 
   virtual void print(llvm::raw_ostream &) const;

lib/Core/CXXTypeSystem/CXXTypeManager.cpp

@@ -44,7 +44,8 @@ KType *CXXTypeManager::getWrappedType(llvm::Type *type) {
       /* Vector types are considered as their elements type */
       llvm::Type *unwrappedRawType = type;
       if (unwrappedRawType->isVectorTy()) {
-        unwrappedRawType = llvm::cast<llvm::VectorType>(unwrappedRawType)->getElementType();
+        unwrappedRawType =
+            llvm::cast<llvm::VectorType>(unwrappedRawType)->getElementType();
       }
 
       switch (unwrappedRawType->getTypeID()) {
@@ -54,6 +55,10 @@ KType *CXXTypeManager::getWrappedType(llvm::Type *type) {
       case (llvm::Type::IntegerTyID):
         kt = new cxxtypes::KCXXIntegerType(unwrappedRawType, this);
         break;
+      case (llvm::Type::PPC_FP128TyID):
+      case (llvm::Type::FP128TyID):
+      case (llvm::Type::X86_FP80TyID):
+      case (llvm::Type::DoubleTyID):
       case (llvm::Type::FloatTyID):
         kt = new cxxtypes::KCXXFloatingPointType(unwrappedRawType, this);
         break;
@@ -172,6 +177,38 @@ void CXXTypeManager::onFinishInitModule() {
   }
 }
 
+/**
+ * Util method to create constraints for pointers
+ * for complex structures that can have many types located
+ * by different offsets.
+ */
+static ref<Expr> getComplexPointerRestrictions(
+    ref<Expr> object,
+    const std::vector<std::pair<size_t, KType *>> &offsetsToTypes) {
+  ref<Expr> resultCondition;
+  for (auto &offsetToTypePair : offsetsToTypes) {
+    size_t offset = offsetToTypePair.first;
+    KType *extractedType = offsetToTypePair.second;
+
+    ref<Expr> extractedOffset = ExtractExpr::create(
+        object, offset * CHAR_BIT, extractedType->getSize() * CHAR_BIT);
+    ref<Expr> innerAlignmentRequirement =
+        llvm::cast<cxxtypes::KCXXType>(extractedType)
+            ->getPointersRestrictions(extractedOffset);
+    if (innerAlignmentRequirement.isNull()) {
+      continue;
+    }
+
+    if (resultCondition.isNull()) {
+      resultCondition = innerAlignmentRequirement;
+    } else {
+      resultCondition =
+          AndExpr::create(resultCondition, innerAlignmentRequirement);
+    }
+  }
+  return resultCondition;
+}
+
 /* C++ KType base class */
 cxxtypes::KCXXType::KCXXType(llvm::Type *type, TypeManager *parent)
     : KType(type, parent) {
@@ -193,6 +230,19 @@ bool cxxtypes::KCXXType::isAccessableFrom(KType *accessingType) const {
   assert(false && "Attempted to compare raw llvm type with C++ type!");
 }
 
+ref<Expr> cxxtypes::KCXXType::getContentRestrictions(ref<Expr> object) const {
+  if (type == nullptr) {
+    return nullptr;
+  }
+  llvm::Type *elementType = type->getPointerElementType();
+  return llvm::cast<cxxtypes::KCXXType>(parent->getWrappedType(elementType))
+      ->getPointersRestrictions(object);
+}
+
+ref<Expr> cxxtypes::KCXXType::getPointersRestrictions(ref<Expr>) const {
+  return nullptr;
+}
+
 bool cxxtypes::KCXXType::isAccessingFromChar(KCXXType *accessingType) {
   /* Special case for unknown type */
   if (accessingType->getRawType() == nullptr) {
@@ -231,6 +281,19 @@ cxxtypes::KCXXCompositeType::KCXXCompositeType(KType *type, TypeManager *parent,
   insertedTypes.emplace(type);
 }
 
+ref<Expr>
+cxxtypes::KCXXCompositeType::getPointersRestrictions(ref<Expr> object) const {
+  if (containsSymbolic) {
+    return nullptr;
+  }
+  std::vector<std::pair<size_t, KType *>> offsetToTypes;
+  for (auto &offsetToTypePair : typesLocations) {
+    offsetToTypes.emplace_back(offsetToTypePair.first,
+                               offsetToTypePair.second.first);
+  }
+  return getComplexPointerRestrictions(object, offsetToTypes);
+}
+
 void cxxtypes::KCXXCompositeType::handleMemoryAccess(KType *type,
                                                      ref<Expr> offset,
                                                      ref<Expr> size,
@@ -411,6 +474,21 @@ cxxtypes::KCXXStructType::KCXXStructType(llvm::Type *type, TypeManager *parent)
   }
 }
 
+ref<Expr>
+cxxtypes::KCXXStructType::getPointersRestrictions(ref<Expr> object) const {
+  std::vector<std::pair<size_t, KType *>> offsetsToTypes;
+  for (auto &innerTypeToOffsets : innerTypes) {
+    KType *innerType = innerTypeToOffsets.first;
+    if (!llvm::isa<KCXXPointerType>(innerType)) {
+      continue;
+    }
+    for (auto &offset : innerTypeToOffsets.second) {
+      offsetsToTypes.emplace_back(offset, innerType);
+    }
+  }
+  return getComplexPointerRestrictions(object, offsetsToTypes);
+}
+
 bool cxxtypes::KCXXStructType::isAccessableFrom(KCXXType *accessingType) const {
   /* FIXME: this is a temporary hack for vtables in C++. Ideally, we
    * should demangle global variables to get additional info, at least
@@ -460,6 +538,15 @@ cxxtypes::KCXXArrayType::KCXXArrayType(llvm::Type *type, TypeManager *parent)
   arrayElementsCount = rawArrayType->getArrayNumElements();
 }
 
+ref<Expr>
+cxxtypes::KCXXArrayType::getPointersRestrictions(ref<Expr> object) const {
+  std::vector<std::pair<size_t, KType *>> offsetsToTypes;
+  for (unsigned idx = 0; idx < arrayElementsCount; ++idx) {
+    offsetsToTypes.emplace_back(idx * elementType->getSize(), elementType);
+  }
+  return getComplexPointerRestrictions(object, offsetsToTypes);
+}
+
 bool cxxtypes::KCXXArrayType::isAccessableFrom(KCXXType *accessingType) const {
   if (llvm::isa<KCXXArrayType>(accessingType)) {
     return innerIsAccessableFrom(llvm::cast<KCXXArrayType>(accessingType));
@@ -575,6 +662,26 @@ bool cxxtypes::KCXXPointerType::innerIsAccessableFrom(
   return accessingType->getRawType() == nullptr;
 }
 
+ref<Expr>
+cxxtypes::KCXXPointerType::getPointersRestrictions(ref<Expr> object) const {
+  /**
+   * We assume that alignment is always a power of 2 and has
+   * a bit representation as 00...010...00. By subtracting 1
+   * we are getting 00...011...1. Then we apply this mask to
+   * address and require, that bitwise AND should give 0 (i.e.
+   * non of the last bits is 1).
+   */
+  ref<Expr> appliedAlignmentMask = AndExpr::create(
+      Expr::createPointer(elementType->getAlignment() - 1), object);
+
+  ref<Expr> sizeExpr = Expr::createPointer(elementType->getSize() - 1);
+
+  ref<Expr> objectUpperBound = AddExpr::create(object, sizeExpr);
+
+  return AndExpr::create(Expr::createIsZero(appliedAlignmentMask),
+                         UgeExpr::create(objectUpperBound, sizeExpr));
+}
+
 bool cxxtypes::KCXXPointerType::innerIsAccessableFrom(
     KCXXPointerType *accessingType) const {
   return elementType->isAccessableFrom(accessingType->elementType);

lib/Core/CXXTypeSystem/CXXTypeManager.h

@@ -91,6 +91,9 @@ class KCXXType : public KType {
   virtual bool isAccessableFrom(KType *) const final override;
   virtual bool isAccessableFrom(KCXXType *) const;
 
+  virtual ref<Expr> getContentRestrictions(ref<Expr>) const override;
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const;
+
   CXXTypeKind getTypeKind() const;
 
   static bool classof(const KType *);
@@ -115,6 +118,7 @@ class KCXXCompositeType : public KCXXType {
   KCXXCompositeType(KType *, TypeManager *, ref<Expr>);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual void handleMemoryAccess(KType *, ref<Expr>, ref<Expr> size,
                                   bool isWrite) override;
   virtual bool isAccessableFrom(KCXXType *) const override;
@@ -137,6 +141,7 @@ class KCXXStructType : public KCXXType {
   KCXXStructType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
 
   static bool classof(const KType *);
@@ -224,6 +229,7 @@ class KCXXArrayType : public KCXXType {
   KCXXArrayType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
 
   static bool classof(const KType *);
@@ -245,7 +251,9 @@ class KCXXPointerType : public KCXXType {
   KCXXPointerType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
+
   bool isPointerToChar() const;
   bool isPointerToFunction() const;
 

lib/Core/Executor.cpp

@@ -159,6 +159,12 @@ cl::opt<bool>
             cl::desc("Turns on restrictions based on types compatibility for "
                      "symbolic pointers (default=false)"),
             cl::init(false));
+
+cl::opt<bool>
+    AlignSymbolicPointers("align-symbolic-pointers",
+                          cl::desc("Makes symbolic pointers aligned according"
+                                   "to the used type system (default=true)"),
+                          cl::init(true));
 } // namespace klee
 
 namespace {
@@ -5002,7 +5008,19 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     if (!unbound)
       break;
   }
-
+
+
+  if (unbound) {
+    StatePair branches =
+        fork(*unbound, Expr::createIsZero(base), true, BranchType::MemOp);
+    ExecutionState *bound = branches.first;
+    if (bound) {
+      terminateStateOnError(*bound, "memory error: null pointer exception",
+                            StateTerminationType::Ptr);
+    }
+    unbound = branches.second;
+  }
+
   // XXX should we distinguish out of bounds and overlapped cases?
   if (unbound) {
     if (incomplete) {
@@ -5122,7 +5140,15 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     const Array *array = makeArray(state, mo->size, name);
     const_cast<Array*>(array)->binding = mo;
     const_cast<MemoryObject *>(mo)->isKleeMakeSymbolic = true;
-    bindObjectInState(state, mo, type, isLocal, array);
+    ObjectState *os = bindObjectInState(state, mo, type, isLocal, array);
+
+    if (AlignSymbolicPointers) {
+      if (ref<Expr> alignmentRestrictions =
+              type->getContentRestrictions(os->read(0, os->size * CHAR_BIT))) {
+        addConstraint(state, alignmentRestrictions);
+      }
+    }
+
     state.addSymbolic(mo, array);
 
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 

lib/Core/TypeManager.cpp

@@ -92,7 +92,7 @@ void TypeManager::initTypesFromStructs() {
     dfs(structType);
   }
 
-  for (auto structType : sortedStructTypesGraph) {  
+  for (auto structType : sortedStructTypesGraph) {
     if (structType->isOpaque()) {
       continue;
     }
@@ -160,6 +160,16 @@ void TypeManager::initTypesFromInstructions() {
   }
 }
 
+void TypeManager::initTypeInfo() {
+  for (auto &type : types) {
+    llvm::Type *rawType = type->getRawType();
+    if (rawType && rawType->isSized()) {
+      type->alignment = parent->targetData->getABITypeAlignment(rawType);
+      type->typeStoreSize = parent->targetData->getTypeStoreSize(rawType);
+    }
+  }
+}
+
 void TypeManager::onFinishInitModule() {}
 
 /**
@@ -174,5 +184,6 @@ void TypeManager::initModule() {
   initTypesFromGlobals();
   initTypesFromInstructions();
   initTypesFromStructs();
+  initTypeInfo();
   onFinishInitModule();
 }

lib/Core/TypeManager.h

@@ -30,6 +30,7 @@ class TypeManager {
   void initTypesFromGlobals();
   void initTypesFromStructs();
   void initTypesFromInstructions();
+  void initTypeInfo();
 
 protected:
   KModule *parent;

lib/Module/KType.cpp

@@ -24,12 +24,16 @@ bool KType::isAccessableFrom(KType *accessingType) const { return true; }
 
 llvm::Type *KType::getRawType() const { return type; }
 
-TypeSystemKind KType::getTypeSystemKind() const {
-  return typeSystemKind;
-}
+TypeSystemKind KType::getTypeSystemKind() const { return typeSystemKind; }
 
 void KType::handleMemoryAccess(KType *, ref<Expr>, ref<Expr>, bool isWrite) {}
 
+size_t KType::getSize() const { return typeStoreSize; }
+
+size_t KType::getAlignment() const { return alignment; }
+
+ref<Expr> KType::getContentRestrictions(ref<Expr>) const { return nullptr; }
+
 void KType::print(llvm::raw_ostream &os) const {
   if (type == nullptr) {
     os << "nullptr";

test/Feature/NullPointerDereferenceCheck.c

@@ -0,0 +1,12 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  int *ptr;
+  klee_make_symbolic(&ptr, sizeof(ptr), "ptr");
+  // CHECK: NullPointerDereferenceCheck.c:[[@LINE+1]]: memory error: null pointer exception
+  *ptr = 10;
+}