From 2cae55383a11fbcb3fcc1a8bac67949e2245d451 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 27 Feb 2024 16:05:19 +0000 Subject: Support external call concretisation policies for referenced objects Provide an additional argument to select the concretisation policy. Fix a bug where the concretisation of a shared memory object was visible across different states by retrieving a writable object state first. --- lib/Core/Executor.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e37045ee..1af88d88 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4020,12 +4020,16 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, state, a, "external call", ExternalCalls == ExternalCallPolicy::All); cvalue->toMemory(&args[wordIndex]); - ObjectPair op; - // Checking to see if the argument is a pointer to something - if (cvalue->getWidth() == Context::get().getPointerWidth() && - state.addressSpace.resolveOne(cvalue, op)) { - op.second->flushToConcreteStore(solver.get(), state); + // If the argument points to a valid and writable object, concretise it + // according to the selected policy + if (ObjectPair op; + cvalue->getWidth() == Context::get().getPointerWidth() && + state.addressSpace.resolveOne(cvalue, op) && !op.second->readOnly) { + auto *os = state.addressSpace.getWriteable(op.first, op.second); + os->flushToConcreteStore(*this, state, + ExternalCalls == ExternalCallPolicy::All); } + wordIndex += (cvalue->getWidth() + 63) / 64; } else { ref arg = toUnique(state, a); -- cgit 1.4.1