about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-11-08 16:26:37 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-30 17:30:11 +0000
commit4e99f8f1c7a336d83168ceb07b576a63b838cb2e (patch)
tree604f5c17531c55df8fae6861e56a14b9e52ce458 /lib/Core/Executor.cpp
parent9d5bbe8a309c5760166febf7edfc3b790d77ab7e (diff)
downloadklee-4e99f8f1c7a336d83168ceb07b576a63b838cb2e.tar.gz
Refactored some code related to seeding.
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp29
1 files changed, 14 insertions, 15 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bc9e31f7..89072490 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4568,13 +4568,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     bindObjectInState(state, mo, false, array);
     state.addSymbolic(mo, array);
     
-    std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
-      seedMap.find(&state);
-    if (it!=seedMap.end()) { // In seed mode we need to add this as a
-                             // binding.
-      for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
-             siie = it->second.end(); siit != siie; ++siit) {
-        SeedInfo &si = *siit;
+    auto found = seedMap.find(&state);
+    if (found != seedMap.end()) {
+      // In seed mode we need to add this as binding
+
+      for (SeedInfo &si : found->second) {
         KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
 
         if (!obj) {
@@ -4582,26 +4580,27 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
             std::vector<unsigned char> &values = si.assignment.bindings[array];
             values = std::vector<unsigned char>(mo->size, '\0');
           } else if (!AllowSeedExtension) {
-            terminateStateOnUserError(state, "ran out of inputs during seeding");
+            terminateStateOnUserError(state,
+                                      "ran out of inputs during seeding");
             break;
           }
         } else {
-          if (obj->numBytes != mo->size &&
-              ((!(AllowSeedExtension || ZeroSeedExtension)
-                && obj->numBytes < mo->size) ||
-               (!AllowSeedTruncation && obj->numBytes > mo->size))) {
-	    std::stringstream msg;
+          /* The condition below implies obj->numBytes != mo->size */
+          if ((obj->numBytes < mo->size && !(AllowSeedExtension || ZeroSeedExtension)) ||
+              (obj->numBytes > mo->size && !AllowSeedTruncation)) {
+            std::stringstream msg;
 	    msg << "replace size mismatch: "
 		<< mo->name << "[" << mo->size << "]"
 		<< " vs " << obj->name << "[" << obj->numBytes << "]"
 		<< " in test\n";
-
             terminateStateOnUserError(state, msg.str());
             break;
           } else {
+            /* Either sizes are equal or seed extension/trucation is allowed */
             std::vector<unsigned char> &values = si.assignment.bindings[array];
-            values.insert(values.begin(), obj->bytes, 
+            values.insert(values.begin(), obj->bytes,
                           obj->bytes + std::min(obj->numBytes, mo->size));
+
             if (ZeroSeedExtension) {
               for (unsigned i=obj->numBytes; i<mo->size; ++i)
                 values.push_back('\0');