From 91d185a174631337f1ecee8b57d3f600c3fb311c Mon Sep 17 00:00:00 2001 From: Marek Chalupa Date: Mon, 27 Jan 2020 15:50:01 +0100 Subject: readStringAtAddress: support pointer into objects The code assumed that the passed pointer points at the beginning of the object. Remove this assumption and support any (constant) pointer. The string is read util either the end of the object is hit (in which case a warning is issued as the string was not zero terminated) or until the terminating zero is found. --- lib/Core/SpecialFunctionHandler.cpp | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index dbc8f190..f1a11212 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -249,25 +249,33 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, Executor::TerminateReason::User); return ""; } - bool res __attribute__ ((unused)); - assert(executor.solver->mustBeTrue(state, - EqExpr::create(address, - op.first->getBaseExpr()), - res) && - res && - "XXX interior pointer unhandled"); + const MemoryObject *mo = op.first; const ObjectState *os = op.second; - std::ostringstream buf; + auto relativeOffset = mo->getOffsetExpr(address); + // the relativeOffset must be concrete as the address is concrete + size_t offset = cast(relativeOffset)->getZExtValue(); - unsigned i; - for (i = 0; i < mo->size - 1; i++) { + std::ostringstream buf; + char c = 0; + for (size_t i = offset; i < mo->size; ++i) { ref cur = os->read8(i); cur = executor.toUnique(state, cur); assert(isa(cur) && "hit symbolic char while reading concrete string"); - buf << static_cast(cast(cur)->getZExtValue(8)); + c = cast(cur)->getZExtValue(8); + if (c == '\0') { + // we read the whole string + break; + } + + buf << c; + } + + if (c != '\0') { + klee_warning_once(0, "String not terminated by \\0 passed to " + "one of the klee_ functions"); } return buf.str(); -- cgit 1.4.1