From cb5e898561f9b8769d8838bc1bdca17a6f4f5d20 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Thu, 30 Nov 2023 20:35:55 +0000
Subject: Modify getValueFromSeeds() to include more functionality and simplify
 its callers

---
 lib/Core/Executor.cpp | 30 ++++++++++++------------------
 lib/Core/Executor.h   |  3 +--
 2 files changed, 13 insertions(+), 20 deletions(-)

(limited to 'lib')

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 73f994ce..49df9790 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1321,11 +1321,8 @@ Executor::toConstant(ExecutionState &state,
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
     return CE;
 
-  ref<Expr> value;
-  if (auto found = seedMap.find(&state); found != seedMap.end())
-    value = getValueFromSeeds(found->second, e);
   /* If no seed evaluation results in a constant, call the solver */
-  ref<ConstantExpr> cvalue = llvm::dyn_cast_or_null<ConstantExpr>(value);
+  ref<ConstantExpr> cvalue = getValueFromSeeds(state, e);
   if (!cvalue) {
     [[maybe_unused]] bool success =
         solver->getValue(state.constraints, e, cvalue, state.queryMetaData);
@@ -1348,9 +1345,13 @@ Executor::toConstant(ExecutionState &state,
   return cvalue;
 }
 
-ref<klee::Expr>
-Executor::getValueFromSeeds(std::vector<SeedInfo> &seeds, ref<Expr> e) {
-  assert(!seeds.empty());
+ref<klee::ConstantExpr> Executor::getValueFromSeeds(ExecutionState &state,
+                                                    ref<Expr> e) {
+  auto found = seedMap.find(&state);
+  if (found == seedMap.end())
+    return nullptr;
+
+  auto seeds = found->second;
   for (auto const &seed : seeds) {
     auto value = seed.assignment.evaluate(e);
     if (isa<ConstantExpr>(value))
@@ -3958,12 +3959,9 @@ void Executor::callExternalFunction(ExecutionState &state,
        ae = arguments.end(); ai!=ae; ++ai) {
     if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
       *ai = optimizer.optimizeExpr(*ai, true);
-      ref<ConstantExpr> cvalue;
-      ref<Expr> value = nullptr;
-      if (auto found = seedMap.find(&state); found != seedMap.end())
-        value = getValueFromSeeds(found->second, *ai);
+      ref<ConstantExpr> cvalue = getValueFromSeeds(state, *ai);
       /* If no seed evaluation results in a constant, call the solver */
-      if (!value || !(cvalue = dyn_cast<ConstantExpr>(value))) {
+      if (!cvalue) {
         [[maybe_unused]] bool success = solver->getValue(
             state.constraints, *ai, cvalue, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
@@ -4196,13 +4194,9 @@ void Executor::executeAlloc(ExecutionState &state,
 
     size = optimizer.optimizeExpr(size, true);
 
-    ref<ConstantExpr> example;
     // Check if in seed mode, then try to replicate size from a seed
-    ref<Expr> value = nullptr;
-    if (auto found = seedMap.find(&state); found != seedMap.end())
-      value = getValueFromSeeds(found->second, size);
-    /* If no seed evaluation results in a constant, call the solver */
-    if (!value || !(example = dyn_cast<ConstantExpr>(value))) {
+    ref<ConstantExpr> example = getValueFromSeeds(state, size);
+    if (!example) {
       bool success = solver->getValue(state.constraints, size, example,
                                       state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index bf773fa5..d19758d4 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -400,8 +400,7 @@ private:
   /// first one that results in a constant, if such a seed exist.  Otherwise,
   /// return the non-constant evaluation of the expression under one of the
   /// seeds.
-  ref<klee::Expr> getValueFromSeeds(std::vector<SeedInfo> &seeds,
-                                            ref<Expr> e);
+  ref<klee::ConstantExpr> getValueFromSeeds(ExecutionState &state, ref<Expr> e);
 
   /// Bind a constant value for e to the given target. NOTE: This
   /// function may fork state if the state has multiple seeds.
-- 
cgit 1.4.1