[fix] Added ID's of states-owners for address symcretes. It is tempor…

…ary fix to let AddressManager work properly (as it maps address-expressions to concrete MemoryObjects from all states).

include/klee/Expr/SourceBuilder.h

@@ -14,11 +14,13 @@ class SourceBuilder {
   static ref<SymbolicSource>
   constant(const std::vector<ref<ConstantExpr>> &constantValues);
   static ref<SymbolicSource> symbolicSizeConstant(unsigned defaultValue);
-  static ref<SymbolicSource> symbolicSizeConstantAddress(unsigned defaultValue,
+  static ref<SymbolicSource> symbolicSizeConstantAddress(ID_t ownerTypeID,
+                                                         unsigned defaultValue,
                                                          unsigned version);
   static ref<SymbolicSource> makeSymbolic(const std::string &name,
                                           unsigned version);
-  static ref<SymbolicSource> lazyInitializationAddress(ref<Expr> pointer);
+  static ref<SymbolicSource> lazyInitializationAddress(ID_t ownerTypeID,
+                                                       ref<Expr> pointer);
   static ref<SymbolicSource> lazyInitializationSize(ref<Expr> pointer);
   static ref<SymbolicSource> lazyInitializationContent(ref<Expr> pointer);
   static ref<SymbolicSource> argument(const llvm::Argument &_allocSite,

include/klee/Expr/SymbolicSource.h

@@ -22,6 +22,8 @@ class Expr;
 class ConstantExpr;
 class KModule;
 
+typedef uint64_t ID_t;
+
 class SymbolicSource {
 protected:
   unsigned hashValue;
@@ -125,10 +127,13 @@ class SymbolicSizeConstantSource : public SymbolicSource {
 
 class SymbolicSizeConstantAddressSource : public SymbolicSource {
 public:
+  const ID_t ownerTypeID;
   const unsigned defaultValue;
   const unsigned version;
-  SymbolicSizeConstantAddressSource(unsigned _defaultValue, unsigned _version)
-      : defaultValue(_defaultValue), version(_version) {}
+  SymbolicSizeConstantAddressSource(ID_t ownerTypeID, unsigned _defaultValue,
+                                    unsigned _version)
+      : ownerTypeID(ownerTypeID), defaultValue(_defaultValue),
+        version(_version) {}
 
   Kind getKind() const override { return Kind::SymbolicSizeConstantAddress; }
   virtual std::string getName() const override {
@@ -150,6 +155,9 @@ class SymbolicSizeConstantAddressSource : public SymbolicSource {
     }
     const SymbolicSizeConstantAddressSource &ssb =
         static_cast<const SymbolicSizeConstantAddressSource &>(b);
+    if (ownerTypeID != ssb.ownerTypeID) {
+      return ownerTypeID < ssb.ownerTypeID ? -1 : 1;
+    }
     if (defaultValue != ssb.defaultValue) {
       return defaultValue < ssb.defaultValue ? -1 : 1;
     }
@@ -222,8 +230,9 @@ class LazyInitializationSource : public SymbolicSource {
 
 class LazyInitializationAddressSource : public LazyInitializationSource {
 public:
-  LazyInitializationAddressSource(ref<Expr> pointer)
-      : LazyInitializationSource(pointer) {}
+  const ID_t ownerStateID;
+  LazyInitializationAddressSource(ID_t ownerStateID, ref<Expr> pointer)
+      : LazyInitializationSource(pointer), ownerStateID(ownerStateID) {}
   Kind getKind() const override { return Kind::LazyInitializationAddress; }
   virtual std::string getName() const override {
     return "lazyInitializationAddress";
@@ -233,6 +242,16 @@ class LazyInitializationAddressSource : public LazyInitializationSource {
     return S->getKind() == Kind::LazyInitializationAddress;
   }
   static bool classof(const LazyInitializationAddressSource *) { return true; }
+
+  virtual int internalCompare(const SymbolicSource &b) const override {
+    if (const LazyInitializationAddressSource *liAddressSource =
+            dyn_cast<LazyInitializationAddressSource>(&b)) {
+      if (ownerStateID != liAddressSource->ownerStateID) {
+        return ownerStateID < liAddressSource->ownerStateID ? -1 : 1;
+      }
+    }
+    return LazyInitializationSource::internalCompare(b);
+  }
 };
 
 class LazyInitializationSizeSource : public LazyInitializationSource {

lib/Core/Executor.cpp

@@ -5389,9 +5389,10 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref<Expr> size,
   const Array *addressArray = makeArray(
       Expr::createPointer(pointerWidthInBits / CHAR_BIT),
       lazyInitializationSource
-          ? SourceBuilder::lazyInitializationAddress(lazyInitializationSource)
+          ? SourceBuilder::lazyInitializationAddress(state.getID(),
+                                                     lazyInitializationSource)
           : SourceBuilder::symbolicSizeConstantAddress(
-                0, updateNameVersion(state, "const_arr")));
+                state.getID(), 0, updateNameVersion(state, "const_arr")));
   ref<Expr> addressExpr =
       Expr::createTempRead(addressArray, pointerWidthInBits);
 

lib/Expr/Parser.cpp

@@ -540,7 +540,7 @@ SourceResult ParserImpl::ParseSymbolicSizeConstantAddressSource() {
   auto value = dyn_cast<ConstantExpr>(valueExpr);
   auto version = dyn_cast<ConstantExpr>(versionExpr);
   assert(value && version);
-  return SourceBuilder::symbolicSizeConstantAddress(value->getZExtValue(),
+  return SourceBuilder::symbolicSizeConstantAddress(0, value->getZExtValue(),
                                                     version->getZExtValue());
 }
 
@@ -560,7 +560,7 @@ SourceResult ParserImpl::ParseLazyInitializationContentSource() {
 
 SourceResult ParserImpl::ParseLazyInitializationAddressSource() {
   auto pointer = ParseExpr(TypeResult()).get();
-  return SourceBuilder::lazyInitializationAddress(pointer);
+  return SourceBuilder::lazyInitializationAddress(0, pointer);
 }
 
 SourceResult ParserImpl::ParseLazyInitializationSizeSource() {

lib/Expr/SourceBuilder.cpp

@@ -18,11 +18,10 @@ ref<SymbolicSource> SourceBuilder::symbolicSizeConstant(unsigned defaultValue) {
   return r;
 }
 
-ref<SymbolicSource>
-SourceBuilder::symbolicSizeConstantAddress(unsigned defaultValue,
-                                           unsigned version) {
-  ref<SymbolicSource> r(
-      new SymbolicSizeConstantAddressSource(defaultValue, version));
+ref<SymbolicSource> SourceBuilder::symbolicSizeConstantAddress(
+    ID_t ownerTypeID, unsigned defaultValue, unsigned version) {
+  ref<SymbolicSource> r(new SymbolicSizeConstantAddressSource(
+      ownerTypeID, defaultValue, version));
   r->computeHash();
   return r;
 }
@@ -35,8 +34,9 @@ ref<SymbolicSource> SourceBuilder::makeSymbolic(const std::string &name,
 }
 
 ref<SymbolicSource>
-SourceBuilder::lazyInitializationAddress(ref<Expr> pointer) {
-  ref<SymbolicSource> r(new LazyInitializationAddressSource(pointer));
+SourceBuilder::lazyInitializationAddress(ID_t ownerTypeID, ref<Expr> pointer) {
+  ref<SymbolicSource> r(
+      new LazyInitializationAddressSource(ownerTypeID, pointer));
   r->computeHash();
   return r;
 }

test/regression/2023-08-28-invalid-pointer-dereference.c

@@ -0,0 +1,22 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --use-sym-size-alloc --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+
+#pragma clang attribute push(__attribute__((optnone)), apply_to = function)
+
+int main() {
+  int length1 = klee_int("len");
+  int length2 = klee_int("len");
+  if (length1 < 1) {
+    length1 = 1;
+  }
+  if (length2 < 1) {
+    length2 = 1;
+  }
+  char *nondetString1 = (char *)__builtin_alloca(length1 * sizeof(char));
+  char *nondetString2 = (char *)__builtin_alloca(length2 * sizeof(char));
+  nondetString1[length1 - 1] = '\0';
+  // CHECK-NOT: memory error: out of bound pointer
+  nondetString2[length2 - 1] = '\0';
+}
+#pragma clang attribute pop