From 7a640c68ba7517b4a64f2cd684e91bd3de804580 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Thu, 22 Feb 2024 22:37:34 +0000
Subject: Extend toConstant() to take an additional boolean argument that
 decides whether the expression is concretised.  Also changed a C string
 argument to std::string.

---
 lib/Core/Executor.cpp | 15 ++++++---------
 lib/Core/Executor.h   | 11 ++++++-----
 2 files changed, 12 insertions(+), 14 deletions(-)

(limited to 'lib/Core')

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c869f49d..d12af171 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1316,13 +1316,9 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
   return result;
 }
 
-
-/* Concretize the given expression, and return a possible constant value. 
-   'reason' is just a documentation string stating the reason for concretization. */
-ref<klee::ConstantExpr> 
-Executor::toConstant(ExecutionState &state, 
-                     ref<Expr> e,
-                     const char *reason) {
+ref<klee::ConstantExpr> Executor::toConstant(ExecutionState &state, ref<Expr> e,
+                                             const std::string &reason,
+                                             bool concretize) {
   e = ConstraintManager::simplifyExpr(state.constraints, e);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
     return CE;
@@ -1344,9 +1340,10 @@ Executor::toConstant(ExecutionState &state,
   if (ExternalCallWarnings == ExtCallWarnings::All)
     klee_warning("%s", os.str().c_str());
   else
-    klee_warning_once(reason, "%s", os.str().c_str());
+    klee_warning_once(reason.c_str(), "%s", os.str().c_str());
 
-  addConstraint(state, EqExpr::create(e, cvalue));
+  if (concretize)
+    addConstraint(state, EqExpr::create(e, cvalue));
 
   return cvalue;
 }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index d19758d4..7be056a1 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -387,14 +387,15 @@ private:
   /// value). Otherwise return the original expression.
   ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e);
 
-  /// Return a constant value for the given expression, forcing it to
-  /// be constant in the given state by adding a constraint if
+  /// Return a constant value for the given expression.  If \param concretize is
+  /// true, the expression is forced to be a constant by adding a constraint if
   /// necessary. Note that this function breaks completeness and
   /// should generally be avoided.
   ///
-  /// \param purpose An identify string to printed in case of concretization.
-  ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e, 
-                                     const char *purpose);
+  /// \param reason A documentation string stating the reason for concretization
+  ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e,
+                                     const std::string &reason,
+                                     bool concretize = true);
 
   /// Evaluate the given expression under each seed, and return the
   /// first one that results in a constant, if such a seed exist.  Otherwise,
-- 
cgit 1.4.1