[fix] Model objects for ctype_* functions for 32-bit executables. Handle ConstantPointer instead of ConstantExpr where it is required. Removed propagating of operations in SelectExpr (caused division on 0 for *Div operations).

[fix] Model return value of ctype_* functions as pointers.

[fix] Allow to resolve SelectExpr of ConsantExprs on all memory objects in address space.

[fix] DebugInfo may not point to any address.

[fix] Do not optimize SelectExpr for *Div operations, terminate state on call to raise function.

[refactor] Logic for writing in CType objects put in lambdas.

[test] Added tests for propagating select through division, calling to raise and for resolve of symbolic pointer represeneted as a select by a symbolic condition.

[refactor] addCType* functions moved to private methods for better readability, optimization on sifting up selects during construction of expressions moved to seperate method also for better readability.

Author: S1eGa

lib/Core/AddressSpace.cpp

@@ -13,6 +13,7 @@
 #include "Memory.h"
 #include "TimingSolver.h"
 
+#include "klee/Expr/ArrayExprVisitor.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Module/KType.h"
 #include "klee/Statistics/TimerStatIncrementer.h"
@@ -199,6 +200,24 @@ class ResolvePredicate {
         timestamp = moBasePair.first->timestamp;
       }
     }
+    // This is hack to deal with the poineters, which are represented as
+    // select expressions from constant pointers with symbolic condition.
+    // in such case we allow to resolve in all objects in the address space,
+    // but should forbid lazy initilization.
+    if (isa<SelectExpr>(base)) {
+      std::vector<ref<Expr>> alternatives;
+      ArrayExprHelper::collectAlternatives(cast<SelectExpr>(*base),
+                                           alternatives);
+      if (std::find_if_not(alternatives.begin(), alternatives.end(),
+                           [](ref<Expr> expr) {
+                             return isa<ConstantExpr>(expr);
+                           }) == alternatives.end()) {
+        skipNotSymbolicObjects = false;
+        skipNotLazyInitialized = false;
+        skipLocal = false;
+        skipGlobal = false;
+      }
+    }
   }
 
   bool operator()(const MemoryObject *mo, const ObjectState *os) const {

lib/Core/Executor.cpp

@@ -55,6 +55,10 @@ DISABLE_WARNING_POP
 #include <unordered_map>
 #include <vector>
 
+#ifdef HAVE_CTYPE_EXTERNALS
+#include <ctype.h>
+#endif
+
 struct KTest;
 
 namespace llvm {
@@ -129,6 +133,12 @@ class Executor : public Interpreter {
 private:
   int *errno_addr;
 
+#ifdef HAVE_CTYPE_EXTERNALS
+  decltype(__ctype_b_loc()) c_type_b_loc_addr;
+  decltype(__ctype_tolower_loc()) c_type_tolower_addr;
+  decltype(__ctype_toupper_loc()) c_type_toupper_addr;
+#endif
+
   size_t maxNewWriteableOSSize = 0;
   size_t maxNewStateStackSize = 0;
 
@@ -267,8 +277,21 @@ class Executor : public Interpreter {
 
   // Given a concrete object in our [klee's] address space, add it to
   // objects checked code can reference.
-  MemoryObject *addExternalObject(ExecutionState &state, void *addr, KType *,
-                                  unsigned size, bool isReadOnly);
+  ObjectPair addExternalObject(ExecutionState &state, const void *addr, KType *,
+                               unsigned size, bool isReadOnly);
+  ObjectPair addExternalObjectAsNonStatic(ExecutionState &state, KType *,
+                                          unsigned size, bool isReadOnly);
+
+#ifdef HAVE_CTYPE_EXTERNALS
+  template <typename F>
+  decltype(auto) addCTypeFixedObject(ExecutionState &state, int addressSpaceNum,
+                                     llvm::Module &m, F objectProvider);
+
+  template <typename F>
+  decltype(auto) addCTypeModelledObject(ExecutionState &state,
+                                        int addressSpaceNum, llvm::Module &m,
+                                        F objectProvider);
+#endif
 
   void initializeGlobalAlias(const llvm::Constant *c, ExecutionState &state);
   void initializeGlobalObject(ExecutionState &state, ObjectState *os,
@@ -442,8 +465,8 @@ class Executor : public Interpreter {
   StatePair forkInternal(ExecutionState &current, ref<Expr> condition,
                          BranchType reason);
 
-  // If the MaxStatic*Pct limits have been reached, concretize the condition and
-  // return it. Otherwise, return the unmodified condition.
+  // If the MaxStatic*Pct limits have been reached, concretize the condition
+  // and return it. Otherwise, return the unmodified condition.
   ref<Expr> maxStaticPctChecks(ExecutionState &current, ref<Expr> condition);
 
   /// Add the given (boolean) condition as a constraint on state. This
@@ -587,8 +610,8 @@ class Executor : public Interpreter {
                              unsigned size = 0,
                              const MemoryObject *mo = nullptr) const;
 
-  // Determines the \param lastInstruction of the \param state which is not KLEE
-  // internal and returns its KInstruction
+  // Determines the \param lastInstruction of the \param state which is not
+  // KLEE internal and returns its KInstruction
   const KInstruction *
   getLastNonKleeInternalInstruction(const ExecutionState &state) const;
 
@@ -697,7 +720,8 @@ class Executor : public Interpreter {
   void doImpliedValueConcretization(ExecutionState &state, ref<Expr> e,
                                     ref<ConstantExpr> value);
 
-  /// check memory usage and terminate states when over threshold of -max-memory
+  /// check memory usage and terminate states when over threshold of
+  /// -max-memory
   /// + 100MB \return true if below threshold, false otherwise (states were
   /// terminated)
   bool checkMemoryUsage();

lib/Core/Executor.h

@@ -191,6 +191,11 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
     add("klee_rintf", handleRint, true),
 #if defined(__x86_64__) || defined(__i386__)
     add("klee_rintl", handleRint, true),
+#if defined(HAVE_CTYPE_EXTERNALS)
+    add("__ctype_b_loc", handleCTypeBLoc, true),
+    add("__ctype_tolower_loc", handleCTypeToLowerLoc, true),
+    add("__ctype_toupper_loc", handleCTypeToUpperLoc, true),
+#endif
 #endif
 #undef addDNR
 #undef add
@@ -1214,3 +1219,34 @@ void SpecialFunctionHandler::handleFAbs(ExecutionState &state,
   ref<Expr> result = FAbsExpr::create(arguments[0]);
   executor.bindLocal(target, state, result);
 }
+
+#ifdef HAVE_CTYPE_EXTERNALS
+
+void SpecialFunctionHandler::handleCTypeBLoc(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  ref<ConstantExpr> pointerValue = Expr::createPointer(
+      reinterpret_cast<uint64_t>(executor.c_type_b_loc_addr));
+  ref<Expr> result = ConstantPointerExpr::create(pointerValue, pointerValue);
+  executor.bindLocal(target, state, result);
+}
+
+void SpecialFunctionHandler::handleCTypeToLowerLoc(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  ref<ConstantExpr> pointerValue = Expr::createPointer(
+      reinterpret_cast<uint64_t>(executor.c_type_tolower_addr));
+  ref<Expr> result = ConstantPointerExpr::create(pointerValue, pointerValue);
+  executor.bindLocal(target, state, result);
+}
+
+void SpecialFunctionHandler::handleCTypeToUpperLoc(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  ref<ConstantExpr> pointerValue = Expr::createPointer(
+      reinterpret_cast<uint64_t>(executor.c_type_toupper_addr));
+  ref<Expr> result = ConstantPointerExpr::create(pointerValue, pointerValue);
+  executor.bindLocal(target, state, result);
+}
+
+#endif

lib/Core/SpecialFunctionHandler.cpp

@@ -181,6 +181,11 @@ class SpecialFunctionHandler {
   HANDLER(handleNonnullArg);
   HANDLER(handleNullabilityArg);
   HANDLER(handlePointerOverflow);
+#ifdef HAVE_CTYPE_EXTERNALS
+  HANDLER(handleCTypeBLoc);
+  HANDLER(handleCTypeToLowerLoc);
+  HANDLER(handleCTypeToUpperLoc);
+#endif
 #undef HANDLER
 };
 } // namespace klee

lib/Core/SpecialFunctionHandler.h

@@ -2329,20 +2329,45 @@ static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   }
 }
 
+template <typename T> static bool isDiv() {
+  return T::kind == Expr::Kind::SDiv || T::kind == Expr::Kind::UDiv ||
+         T::kind == Expr::Kind::FDiv;
+}
+
+/// Heuristic.
+/// Attempts to sift up select expression during creation.
+template <typename T>
+static ref<Expr> tryCreateWithSiftUpSelectExpr(const ref<Expr> &l,
+                                               const ref<Expr> &r,
+                                               bool skipInnerSelect = false) {
+  if (isDiv<T>()) {
+    return nullptr;
+  }
+
+  if (ref<SelectExpr> sel = dyn_cast<SelectExpr>(l)) {
+    if (isa<ConstantExpr>(sel->trueExpr) &&
+        (!skipInnerSelect || !isa<SelectExpr>(r))) {
+      return SelectExpr::create(sel->cond, T::create(sel->trueExpr, r),
+                                T::create(sel->falseExpr, r));
+    }
+  }
+  if (ref<SelectExpr> ser = dyn_cast<SelectExpr>(r)) {
+    if (isa<ConstantExpr>(ser->trueExpr) &&
+        (!skipInnerSelect || !isa<SelectExpr>(l))) {
+      return SelectExpr::create(ser->cond, T::create(l, ser->trueExpr),
+                                T::create(l, ser->falseExpr));
+    }
+  }
+
+  return nullptr;
+}
+
 #define BCREATE_R(_e_op, _op, partialL, partialR, pointerL, pointerR)          \
   ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {           \
     assert(l->getWidth() == r->getWidth() && "type mismatch");                 \
-    if (SelectExpr *sel = dyn_cast<SelectExpr>(l)) {                           \
-      if (isa<ConstantExpr>(sel->trueExpr)) {                                  \
-        return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r),  \
-                                  _e_op::create(sel->falseExpr, r));           \
-      }                                                                        \
-    }                                                                          \
-    if (SelectExpr *ser = dyn_cast<SelectExpr>(r)) {                           \
-      if (isa<ConstantExpr>(ser->trueExpr)) {                                  \
-        return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr),  \
-                                  _e_op::create(l, ser->falseExpr));           \
-      }                                                                        \
+    if (auto withSiftUpSelectExpr =                                            \
+            tryCreateWithSiftUpSelectExpr<_e_op>(l, r)) {                      \
+      return withSiftUpSelectExpr;                                             \
     }                                                                          \
     if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) {                          \
       if (PointerExpr *pr = dyn_cast<PointerExpr>(r))                          \
@@ -2364,17 +2389,9 @@ static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 #define BCREATE_R_C(_e_op, _op, partialL, partialR, pointerL, pointerR)        \
   ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {           \
     assert(l->getWidth() == r->getWidth() && "type mismatch");                 \
-    if (SelectExpr *sel = dyn_cast<SelectExpr>(l)) {                           \
-      if (isa<ConstantExpr>(sel->trueExpr)) {                                  \
-        return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r),  \
-                                  _e_op::create(sel->falseExpr, r));           \
-      }                                                                        \
-    }                                                                          \
-    if (SelectExpr *ser = dyn_cast<SelectExpr>(r)) {                           \
-      if (isa<ConstantExpr>(ser->trueExpr)) {                                  \
-        return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr),  \
-                                  _e_op::create(l, ser->falseExpr));           \
-      }                                                                        \
+    if (auto withSiftUpSelectExpr =                                            \
+            tryCreateWithSiftUpSelectExpr<_e_op>(l, r)) {                      \
+      return withSiftUpSelectExpr;                                             \
     }                                                                          \
     if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) {                          \
       if (PointerExpr *pr = dyn_cast<PointerExpr>(r))                          \
@@ -2409,17 +2426,9 @@ static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 #define BCREATE(_e_op, _op)                                                    \
   ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {           \
     assert(l->getWidth() == r->getWidth() && "type mismatch");                 \
-    if (SelectExpr *sel = dyn_cast<SelectExpr>(l)) {                           \
-      if (isa<ConstantExpr>(sel->trueExpr)) {                                  \
-        return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r),  \
-                                  _e_op::create(sel->falseExpr, r));           \
-      }                                                                        \
-    }                                                                          \
-    if (SelectExpr *ser = dyn_cast<SelectExpr>(r)) {                           \
-      if (isa<ConstantExpr>(ser->trueExpr)) {                                  \
-        return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr),  \
-                                  _e_op::create(l, ser->falseExpr));           \
-      }                                                                        \
+    if (auto withSiftUpSelectExpr =                                            \
+            tryCreateWithSiftUpSelectExpr<_e_op>(l, r)) {                      \
+      return withSiftUpSelectExpr;                                             \
     }                                                                          \
     if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) {                          \
       if (PointerExpr *pr = dyn_cast<PointerExpr>(r))                          \
@@ -2457,17 +2466,9 @@ BCREATE(AShrExpr, AShr)
 #define CMPCREATE(_e_op, _op)                                                  \
   ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {           \
     assert(l->getWidth() == r->getWidth() && "type mismatch");                 \
-    if (SelectExpr *sel = dyn_cast<SelectExpr>(l)) {                           \
-      if (isa<ConstantExpr>(sel->trueExpr) && !isa<SelectExpr>(r)) {           \
-        return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r),  \
-                                  _e_op::create(sel->falseExpr, r));           \
-      }                                                                        \
-    }                                                                          \
-    if (SelectExpr *ser = dyn_cast<SelectExpr>(r)) {                           \
-      if (isa<ConstantExpr>(ser->trueExpr) && !isa<SelectExpr>(l)) {           \
-        return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr),  \
-                                  _e_op::create(l, ser->falseExpr));           \
-      }                                                                        \
+    if (auto withSiftUpSelectExpr =                                            \
+            tryCreateWithSiftUpSelectExpr<_e_op>(l, r, true)) {                \
+      return withSiftUpSelectExpr;                                             \
     }                                                                          \
     if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) {                          \
       if (PointerExpr *pr = dyn_cast<PointerExpr>(r))                          \
@@ -2485,17 +2486,9 @@ BCREATE(AShrExpr, AShr)
 #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR)           \
   ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {           \
     assert(l->getWidth() == r->getWidth() && "type mismatch");                 \
-    if (SelectExpr *sel = dyn_cast<SelectExpr>(l)) {                           \
-      if (isa<ConstantExpr>(sel->trueExpr) && !isa<SelectExpr>(r)) {           \
-        return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r),  \
-                                  _e_op::create(sel->falseExpr, r));           \
-      }                                                                        \
-    }                                                                          \
-    if (SelectExpr *ser = dyn_cast<SelectExpr>(r)) {                           \
-      if (isa<ConstantExpr>(ser->trueExpr) && !isa<SelectExpr>(l)) {           \
-        return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr),  \
-                                  _e_op::create(l, ser->falseExpr));           \
-      }                                                                        \
+    if (auto withSiftUpSelectExpr =                                            \
+            tryCreateWithSiftUpSelectExpr<_e_op>(l, r, true)) {                \
+      return withSiftUpSelectExpr;                                             \
     }                                                                          \
     if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) {                          \
       if (PointerExpr *pr = dyn_cast<PointerExpr>(r))                          \

lib/Expr/Expr.cpp

@@ -35,7 +35,7 @@ bool LocalVarDeclarationFinderPass::runOnFunction(llvm::Function &function) {
               llvm::dyn_cast<const llvm::DbgDeclareInst>(&instruction)) {
         llvm::Value *source = debugDeclareInstruction->getAddress();
         if (llvm::Instruction *sourceInstruction =
-                llvm::dyn_cast<llvm::Instruction>(source)) {
+                llvm::dyn_cast_or_null<llvm::Instruction>(source)) {
           sourceInstruction->setDebugLoc(
               debugDeclareInstruction->getDebugLoc());
           anyChanged = true;

lib/Module/LocalVarDeclarationFinderPass.cpp

@@ -0,0 +1,17 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --mock-policy=all --external-calls=all %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <signal.h>
+
+int main() {
+  int n;
+  klee_make_symbolic(&n, sizeof(n), "n");
+
+  if (n) {
+    // CHECK: Call to "raise" is unmodelled
+    raise(5);
+  }
+  // CHECK: KLEE: done: completed paths = 1
+}

test/regression/2024-07-08-call-to-raise.c

@@ -0,0 +1,15 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  int n, m;
+  klee_make_symbolic(&n, sizeof(n), "n");
+  klee_make_symbolic(&m, sizeof(m), "m");
+
+  int z = (n ? 1 : 0) / (m ? 1 : 0);
+  (void)z;
+}
+// CHECK: KLEE: done

test/regression/2024-07-08-division-in-select.c

@@ -0,0 +1,27 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --skip-not-lazy-initialized --skip-local --skip-global %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <assert.h>
+
+int main() {
+  int x = 0;
+  int y = 1;
+
+  int cond;
+  klee_make_symbolic(&cond, sizeof(cond), "cond");
+
+  int *z = cond ? &x : &y;
+  // CHECK-NOT: memory error: out of bound pointer
+  *z = 10;
+
+  // CHECK-NOT: ASSERTION FAIL
+  if (x == 10) {
+    assert(y == 1);
+  } else {
+    assert(x == 0);
+    assert(y == 10);
+  }
+  // CHECK: KLEE: done: completed paths = 2
+}