diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2021-06-07 16:26:12 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2024-02-29 19:57:08 +0000 |
commit | a4d9762a31402c5e5298ef22870a7e25124a7af2 (patch) | |
tree | f322ab797ef8d06a266b9f8b277fb87719108652 /lib | |
parent | 279be1d2748f9694c27423cc650deb46638736ad (diff) | |
download | klee-a4d9762a31402c5e5298ef22870a7e25124a7af2.tar.gz |
Correctly update symbolic variables that have been changed externally
Before, external changes to symbolic variables have not been propagated back to their internal representation. Do a byte-by-byte comparison and update object state if required.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/AddressSpace.cpp | 34 |
1 files changed, 27 insertions, 7 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index ab3bbb8c..bb77f0fc 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -336,13 +336,33 @@ bool AddressSpace::copyInConcretes() { bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os, uint64_t src_address) { auto address = reinterpret_cast<std::uint8_t*>(src_address); - if (memcmp(address, os->concreteStore, mo->size) != 0) { - if (os->readOnly) { - return false; - } else { - ObjectState *wos = getWriteable(mo, os); - memcpy(wos->concreteStore, address, mo->size); - } + + // Don't do anything if the underlying representation has not been changed + // externally. + if (std::memcmp(address, os->concreteStore, mo->size) == 0) + return true; + + // External object representation has been changed + + // Return `false` if the object is marked as read-only + if (os->readOnly) + return false; + + ObjectState *wos = getWriteable(mo, os); + // Check if the object is fully concrete object. If so, use the fast + // path and `memcpy` the new values from the external object to the internal + // representation + if (!wos->unflushedMask) { + std::memcpy(wos->concreteStore, address, mo->size); + return true; + } + + // The object is partially symbolic, it needs to be updated byte-by-byte + // via object state's `write` function + for (size_t i = 0, ie = mo->size; i < ie; ++i) { + u_int8_t external_byte_value = *(address + i); + if (external_byte_value != wos->concreteStore[i]) + wos->write8(i, external_byte_value); } return true; } |