about summary refs log tree commit diff homepage
path: root/lib/Core/SpecialFunctionHandler.cpp
diff options
context:
space:
mode:
authorLukas Wölfer <lukas.woelfer@rwth-aachen.de>2018-08-27 00:51:03 +0200
committerMartinNowack <martin.nowack@gmail.com>2018-11-23 22:34:13 +0000
commit0283175fdda6bf4dbd9343b53987d0aee01ce9fc (patch)
tree53725b53080f718d22a8aa5d8661e63283c3084d /lib/Core/SpecialFunctionHandler.cpp
parent92b49c62b796e4c2544fc2415d9817068aed6eae (diff)
downloadklee-0283175fdda6bf4dbd9343b53987d0aee01ce9fc.tar.gz
Implemented memalign with alignment
Diffstat (limited to 'lib/Core/SpecialFunctionHandler.cpp')
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp35
1 files changed, 35 insertions, 0 deletions
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) {