From 4e99f8f1c7a336d83168ceb07b576a63b838cb2e Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Wed, 8 Nov 2023 16:26:37 +0000
Subject: Refactored some code related to seeding.

---
 lib/Core/Executor.cpp | 29 ++++++++++++++---------------
 lib/Core/SeedInfo.cpp | 23 +++++++++--------------
 2 files changed, 23 insertions(+), 29 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');
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 55f4ed48..ddc40b26 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -74,27 +74,22 @@ void SeedInfo::patchSeed(const ExecutionState &state,
   std::set< std::pair<const Array*, unsigned> > directReads;
   std::vector< ref<ReadExpr> > reads;
   findReads(condition, false, reads);
-  for (std::vector< ref<ReadExpr> >::iterator it = reads.begin(), 
-         ie = reads.end(); it != ie; ++it) {
-    ReadExpr *re = it->get();
+  for (auto const &re : reads) {
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
       directReads.insert(std::make_pair(re->updates.root, 
                                         (unsigned) CE->getZExtValue(32)));
     }
   }
-  
-  for (std::set< std::pair<const Array*, unsigned> >::iterator
-         it = directReads.begin(), ie = directReads.end(); it != ie; ++it) {
-    const Array *array = it->first;
-    unsigned i = it->second;
+
+  for (auto const &[array, i] : directReads) {
     ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                       ConstantExpr::alloc(i, Expr::Int32));
     
-    // If not in bindings then this can't be a violation?
-    Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
-    if (it2 != assignment.bindings.end()) {
+    // If not in bindings, then this can't be a violation?
+    auto a = assignment.bindings.find(array);
+    if (a != assignment.bindings.end()) {
       ref<Expr> isSeed = EqExpr::create(read, 
-                                        ConstantExpr::alloc(it2->second[i], 
+                                        ConstantExpr::alloc(a->second[i],
                                                             Expr::Int8));
       bool res;
       bool success =
@@ -107,9 +102,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
             solver->getValue(required, read, value, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
-        it2->second[i] = value->getZExtValue(8);
+        a->second[i] = value->getZExtValue(8);
         cm.addConstraint(EqExpr::create(
-            read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
+            read, ConstantExpr::alloc(a->second[i], Expr::Int8)));
       } else {
         cm.addConstraint(isSeed);
       }
-- 
cgit 1.4.1