6 files changed, 62 insertions, 3 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e4f9388e..7cb01e5c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3286,11 +3286,14 @@ void Executor::executeAlloc(ExecutionState &state,
                             bool isLocal,
                             KInstruction *target,
                             bool zeroMemory,
-                            const ObjectState *reallocFrom) {
+                            const ObjectState *reallocFrom,
+                            size_t allocationAlignment) {
   size = toUnique(state, size);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) {
     const llvm::Value *allocSite = state.prevPC->inst;
-    size_t allocationAlignment = getAllocationAlignment(allocSite);
+    if (allocationAlignment == 0) {
+      allocationAlignment = getAllocationAlignment(allocSite);
+    }
     MemoryObject *mo =
         memory->allocate(CE->getZExtValue(), isLocal, /*isGlobal=*/false,
                          allocSite, allocationAlignment);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 180c9140..66a28ba8 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -301,12 +301,17 @@ private:
   /// done (realloc semantics). The initialized bytes will be the
   /// minimum of the size of the old and new objects, with remaining
   /// bytes initialized as specified by zeroMemory.
+  ///
+  /// \param allocationAlignment If non-zero, the given alignment is
+  /// used. Otherwise, the alignment is deduced via
+  /// Executor::getAllocationAlignment
   void executeAlloc(ExecutionState &state,
                     ref<Expr> size,
                     bool isLocal,
                     KInstruction *target,
                     bool zeroMemory=false,
-                    const ObjectState *reallocFrom=0);
+                    const ObjectState *reallocFrom=0,
+                    size_t allocationAlignment=0);
 
   /// Free the given address with checking for errors. If target is
   /// given it will be bound to 0 in the resulting states (this is a
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 8752c2c8..6f887a43 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -111,6 +111,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_warning_once", handleWarningOnce, false),
   add("klee_alias_function", handleAliasFunction, false),
   add("malloc", handleMalloc, true),
+  add("memalign", handleMemalign, true),
   add("realloc", handleRealloc, true),
 
   // operator delete[](void*)
@@ -427,6 +428,40 @@ void SpecialFunctionHandler::handleMalloc(ExecutionState &state,
   executor.executeAlloc(state, arguments[0], false, target);
 }
 
+void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
+                                            KInstruction *target,
+                                            std::vector<ref<Expr>> &arguments) {
+  if (arguments.size() != 2) {
+    executor.terminateStateOnError(state,
+      "Incorrect number of arguments to memalign(size_t alignment, size_t size)",
+      Executor::User);
+    return;
+  }
+
+  std::pair<ref<Expr>, ref<Expr>> alignmentRangeExpr =
+      executor.solver->getRange(state, arguments[0]);
+  ref<Expr> alignmentExpr = alignmentRangeExpr.first;
+  auto alignmentConstExpr = dyn_cast<ConstantExpr>(alignmentExpr);
+
+  if (!alignmentConstExpr) {
+    executor.terminateStateOnError(state,
+      "Could not determine size of symbolic alignment",
+      Executor::User);
+    return;
+  }
+
+  uint64_t alignment = alignmentConstExpr->getZExtValue();
+
+  // Warn, if the expression has more than one solution
+  if (alignmentRangeExpr.first != alignmentRangeExpr.second) {
+    klee_warning_once(
+        0, "Symbolic alignment for memalign. Choosing smallest alignment");
+  }
+
+  executor.executeAlloc(state, arguments[1], false, target, false, 0,
+                        alignment);
+}
+
 void SpecialFunctionHandler::handleAssume(ExecutionState &state,
                             KInstruction *target,
                             std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index f99a212f..fdb6b6de 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -119,6 +119,7 @@ namespace klee {
     HANDLER(handleIsSymbolic);
     HANDLER(handleMakeSymbolic);
     HANDLER(handleMalloc);
+    HANDLER(handleMemalign);
     HANDLER(handleMarkGlobal);
     HANDLER(handleOpenMerge);
     HANDLER(handleCloseMerge);
diff --git a/test/Feature/Memalign.c b/test/Feature/Memalign.c
new file mode 100644
index 00000000..e2ce8de0
--- /dev/null
+++ b/test/Feature/Memalign.c
@@ -0,0 +1,14 @@
+// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.log
+
+#include <stdlib.h>
+
+int main(int argc, char *argv[]) {
+  int *a = (int *)memalign(8, sizeof(int) * 5);
+  for (int i = 0; i < 5; ++i) {
+    a[i] = (i * 100) % 23;
+  }
+  free(a);
+  return 0;
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 50848bad..c7a19df6 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -721,6 +721,7 @@ static const char *modelledExternals[] = {
   "llvm.va_end",
   "malloc",
   "realloc",
+  "memalign",
   "_ZdaPv",
   "_ZdlPv",
   "_Znaj",