From a802c6dfd600f81d6131c055685188e0ac08bb9e Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 17 Feb 2024 15:20:54 +0000 Subject: This commit fixes the concretization of arguments following an external call with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf. --- lib/Core/Executor.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 45209617..c869f49d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -184,9 +184,10 @@ cl::opt /*** External call policy options ***/ enum class ExternalCallPolicy { - None, // No external calls allowed - Concrete, // Only external calls with concrete arguments allowed - All, // All external calls allowed + None, // No external calls allowed + Concrete, // Only external calls with concrete arguments allowed + All, // All external calls allowed, symbolic arguments concretized + OverApprox, // All external calls allowed, symbolic inputs are not constrained by the call }; cl::opt ExternalCalls( @@ -203,7 +204,11 @@ cl::opt ExternalCalls( "allowed (default)"), clEnumValN(ExternalCallPolicy::All, "all", "All external function calls are allowed. This concretizes " - "any symbolic arguments in calls to external functions.")), + "any symbolic arguments in calls to external functions."), + clEnumValN(ExternalCallPolicy::OverApprox, "over-approx", + "All external function calls are allowed. This concretizes " + "any symbolic arguments in calls to external functions but" + "the concretization is ignored after the call (see docs).")), cl::init(ExternalCallPolicy::Concrete), cl::cat(ExtCallsCat)); @@ -4013,7 +4018,8 @@ void Executor::callExternalFunction(ExecutionState &state, unsigned wordIndex = 2; for (std::vector >::iterator ai = arguments.begin(), ae = arguments.end(); ai!=ae; ++ai) { - if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness + if (ExternalCalls == ExternalCallPolicy::All || + ExternalCalls == ExternalCallPolicy::OverApprox) { *ai = optimizer.optimizeExpr(*ai, true); ref cvalue = getValueFromSeeds(state, *ai); /* If no seed evaluation results in a constant, call the solver */ @@ -4022,7 +4028,11 @@ void Executor::callExternalFunction(ExecutionState &state, state.constraints, *ai, cvalue, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); } + cvalue->toMemory(&args[wordIndex]); + if (ExternalCalls == ExternalCallPolicy::All) + addConstraint(state, EqExpr::create(cvalue, *ai)); + ObjectPair op; // Checking to see if the argument is a pointer to something if (cvalue->getWidth() == Context::get().getPointerWidth() && -- cgit 1.4.1