Patch by Oscar Dustmann fixing a buffer overflow when long names are

used: "patch for STPBuilder.cpp that allows for arbitrary length
symbol names while still limiting the unique string to 32 bytes."



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157820 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 5 insertions, 1 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index b5dddad1..b1289f8d 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -405,7 +405,11 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
     // STP uniques arrays by name, so we make sure the name is unique by
     // including the address.
     char buf[32];
-    sprintf(buf, "%s_%p", root->name.c_str(), (void*) root);
+    unsigned const addrlen = sprintf(buf, "_%p", (void*)root) + 1; // +1 for null-termination
+    unsigned const space = (root->name.length() > 32 - addrlen)?(32 - addrlen):root->name.length();
+    memmove(buf + space, buf, addrlen); // moving the address part to the end
+    memcpy(buf, root->name.c_str(), space); // filling out the name part
+    
     root->stpInitialArray = buildArray(buf, 32, 8);
 
     if (root->isConstantArray()) {