From e851cb6d0cbe7c209db78ff62bb8ded128ccc8c5 Mon Sep 17 00:00:00 2001
From: Sergey Morozov <morozov.serg901@gmail.com>
Date: Thu, 12 Oct 2023 18:10:19 +0400
Subject: [PATCH] [fix] Fixed inner types for unnamed structs.

---
 lib/Core/TypeManager.cpp                     | 20 ++++-
 test/regression/2023-10-12-inner-types-fix.c | 89 ++++++++++++++++++++
 2 files changed, 105 insertions(+), 4 deletions(-)
 create mode 100644 test/regression/2023-10-12-inner-types-fix.c

diff --git a/lib/Core/TypeManager.cpp b/lib/Core/TypeManager.cpp
index 0ba8f8ffb1..c053d449fa 100644
--- a/lib/Core/TypeManager.cpp
+++ b/lib/Core/TypeManager.cpp
@@ -37,6 +37,12 @@ KType *TypeManager::getWrappedType(llvm::Type *type) {
   if (typesMap.count(type) == 0) {
     types.emplace_back(new KType(type, this));
     typesMap.emplace(type, types.back().get());
+    if (type && type->isPointerTy()) {
+      getWrappedType(type->getPointerElementType());
+    }
+    if (type && type->isArrayTy()) {
+      getWrappedType(type->getArrayElementType());
+    }
   }
   return typesMap[type];
 }
@@ -61,15 +67,21 @@ void TypeManager::initTypesFromStructs() {
    * and pull types to top.
    */
 
-  std::vector<llvm::StructType *> collectedStructTypes =
-      parent->module->getIdentifiedStructTypes();
-  for (auto &structType : collectedStructTypes) {
+  for (auto &structType : parent->module->getIdentifiedStructTypes()) {
     getWrappedType(structType);
   }
 
+  std::unordered_set<llvm::StructType *> collectedStructTypes;
+  for (const auto &it : typesMap) {
+    if (llvm::StructType *itStruct =
+            llvm::dyn_cast<llvm::StructType>(it.first)) {
+      collectedStructTypes.insert(itStruct);
+    }
+  }
+
   for (auto &typesToOffsets : typesMap) {
     if (llvm::isa<llvm::StructType>(typesToOffsets.first)) {
-      collectedStructTypes.emplace_back(
+      collectedStructTypes.insert(
           llvm::cast<llvm::StructType>(typesToOffsets.first));
     }
   }
diff --git a/test/regression/2023-10-12-inner-types-fix.c b/test/regression/2023-10-12-inner-types-fix.c
new file mode 100644
index 0000000000..2484dc6a1f
--- /dev/null
+++ b/test/regression/2023-10-12-inner-types-fix.c
@@ -0,0 +1,89 @@
+// RUN: %clang  -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --entry-point=klee_entry --skip-not-lazy-initialized --min-number-elements-li=1 %t1.bc 2>&1
+// RUN: %ktest-tool %t.klee-out/test000003.ktest | FileCheck %s
+
+#include "klee/klee.h"
+
+struct StructWithPointer {
+  int x;
+  int *y;
+};
+
+struct StructWithDoublePointer {
+  int x;
+  int **y;
+};
+
+struct StructWithArrayOfPointer {
+  int x;
+  int *y[2];
+};
+
+struct StructWithStructWithPointer {
+  struct StructWithPointer swp;
+  struct StructWithDoublePointer *swdp;
+};
+
+struct StructManyPointers {
+  int a;
+  int *b;
+  int **c;
+  int ***d;
+};
+
+struct StructComplex {
+  int x;
+  int *y;
+  int **z;
+  struct StructWithPointer *swp;
+  struct StructWithDoublePointer **swdp;
+  struct StructManyPointers smp;
+};
+
+int sumStructWithPointer(struct StructWithPointer par) {
+  return par.x + *par.y;
+}
+
+int sumStructWithPointerAsPointer(struct StructWithPointer *par) {
+  return par->x + *par->y;
+}
+
+int sumStructWithDoublePointer(struct StructWithDoublePointer par) {
+  return par.x + **par.y;
+}
+
+int sumStructWithArrayOfPointer(struct StructWithArrayOfPointer par) {
+  return par.x + *(par.y[0]) + *(par.y[1]);
+}
+
+int sumStructWithStructWithPointer(struct StructWithStructWithPointer par) {
+  int sswp = sumStructWithPointer(par.swp);
+  int sswdp = sumStructWithDoublePointer(*par.swdp);
+  return sswp + sswdp;
+}
+
+int sumStructManyPointers(struct StructManyPointers par) {
+  return par.a + *par.b + **par.c + ***par.d;
+}
+
+int sumStructComplex(struct StructComplex par) {
+  int sswp = sumStructWithPointer(*par.swp);
+  int sswdp = sumStructWithDoublePointer(**par.swdp);
+  int ssmp = sumStructManyPointers(par.smp);
+  return par.x + *par.y + **par.z + sswp + sswdp + ssmp;
+}
+
+// CHECK: object 2: pointers: [(8, 3, 0)]
+int klee_entry(int utbot_argc, char **utbot_argv, char **utbot_envp) {
+  struct StructComplex par;
+  klee_make_symbolic(&par, sizeof(par), "par");
+  klee_prefer_cex(&par, par.x >= -10 & par.x <= 10);
+  klee_prefer_cex(&par, par.smp.a >= -10 & par.smp.a <= 10);
+  ////////////////////////////////////////////
+  int utbot_result;
+  klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
+  int utbot_tmp = sumStructComplex(par);
+  klee_assume(utbot_tmp == utbot_result);
+  return 0;
+}
\ No newline at end of file