@@ -106,8 +106,8 @@ RNG theRNG;
106106}
107107
108108Executor::Executor (InterpreterHandler *ih, LLVMContext &context)
109- : kmodule(0 ), interpreterHandler(ih), searcher(0 ), externalDispatcher(new ExternalDispatcher(context) ),
110- statsTracker( 0 ), specialFunctionHandler(0 ) {
109+ : kmodule(0 ), interpreterHandler(ih), searcher(0 ), externalDispatcher(new ExternalDispatcher()), statsTracker( 0 ),
110+ specialFunctionHandler(0 ) {
111111
112112 memory = new MemoryManager ();
113113}
@@ -1707,6 +1707,10 @@ static const char *okExternalsList[] = {"printf", "fprintf", "puts", "getpid"};
17071707static std::set<std::string> okExternals (okExternalsList,
17081708 okExternalsList + (sizeof (okExternalsList) / sizeof (okExternalsList[0 ])));
17091709
1710+ extern " C" {
1711+ typedef uint64_t (*external_fcn_t )(...);
1712+ }
1713+
17101714void Executor::callExternalFunction (ExecutionState &state, KInstruction *target, Function *function,
17111715 std::vector<ref<Expr>> &arguments) {
17121716 // check if specialFunctionHandler wants it
@@ -1719,16 +1723,14 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
17191723 return ;
17201724 }
17211725
1722- // normal external function handling path
1723- uint64_t *args = (uint64_t *) alloca (sizeof (*args) * (arguments.size () + 1 ));
1724- memset (args, 0 , sizeof (*args) * (arguments.size () + 1 ));
1726+ ExternalDispatcher::Arguments cas;
17251727
17261728 unsigned i = 1 ;
17271729 for (std::vector<ref<Expr>>::iterator ai = arguments.begin (), ae = arguments.end (); ai != ae; ++ai, ++i) {
17281730 ref<Expr> arg = state.toUnique (*ai);
17291731 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(arg)) {
17301732 // XXX kick toMemory functions from here
1731- CE ->toMemory (( void *) &args[i] );
1733+ cas. push_back ( CE ->getZExtValue () );
17321734 } else {
17331735 // Fork all possible concrete solutions
17341736 klee::ref<klee::ConstantExpr> concreteArg;
@@ -1754,7 +1756,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
17541756
17551757 sp.first ->pc = savedPc;
17561758
1757- concreteArg->toMemory (( void *) &args[i] );
1759+ cas. push_back ( concreteArg->getZExtValue () );
17581760 }
17591761 }
17601762
@@ -1771,18 +1773,47 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
17711773 klee_warning_external (function, " %s" , os.str ().c_str ());
17721774 }
17731775
1774- bool success = externalDispatcher->executeCall (function, target->inst , args);
1775- if (!success) {
1776+ uint64_t result;
1777+ external_fcn_t targetFunction = (external_fcn_t ) externalDispatcher->resolveSymbol (function->getName ());
1778+ if (!targetFunction) {
17761779 std::stringstream ss;
1777- ss << " failed external call: " << function->getName ().str ();
1780+ ss << " Could not find address of external function " << function->getName ().str ();
1781+ terminateState (state, ss.str ());
1782+ return ;
1783+ }
1784+
1785+ std::stringstream ss;
1786+ if (!externalDispatcher->call (targetFunction, cas, &result, ss)) {
1787+ ss << " : " << function->getName ().str ();
17781788 terminateState (state, ss.str ());
17791789 return ;
17801790 }
17811791
17821792 Type *resultType = target->inst ->getType ();
1793+
17831794 if (resultType != Type::getVoidTy (function->getContext ())) {
1784- ref<Expr> e = ConstantExpr::fromMemory ((void *) args, getWidthForLLVMType (resultType));
1785- state.bindLocal (target, e);
1795+ ref<Expr> resultExpr;
1796+ auto resultWidth = getWidthForLLVMType (resultType);
1797+ switch (resultWidth) {
1798+ case Expr::Bool:
1799+ resultExpr = ConstantExpr::create (result & 1 , resultWidth);
1800+ case Expr::Int8:
1801+ resultExpr = ConstantExpr::create ((uint8_t ) result, resultWidth);
1802+ break ;
1803+ case Expr::Int16:
1804+ resultExpr = ConstantExpr::create ((uint16_t ) result, resultWidth);
1805+ break ;
1806+ case Expr::Int32:
1807+ resultExpr = ConstantExpr::create ((uint32_t ) result, resultWidth);
1808+ break ;
1809+ case Expr::Int64:
1810+ resultExpr = ConstantExpr::create ((uint64_t ) result, resultWidth);
1811+ break ;
1812+ default :
1813+ abort ();
1814+ }
1815+
1816+ state.bindLocal (target, resultExpr);
17861817 }
17871818}
17881819
0 commit comments