From 8a0f1af7500e10dadd97300f242424917d2e9902 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 1 Apr 2019 14:08:43 +0100 Subject: Use constraint sets and separate metadata for timing solver invocation Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints) --- lib/Core/ExecutionState.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'lib/Core/ExecutionState.h') diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 397b2364..03cad916 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -17,6 +17,7 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Module/KInstIterator.h" +#include "klee/Solver/Solver.h" #include "klee/System/Time.h" #include @@ -96,8 +97,8 @@ public: /// Statistics and information - /// @brief Costs for all queries issued for this state, in seconds - mutable time::Span queryCost; + /// @brief Metadata utilized and collected by solvers for this state + mutable SolverQueryMetaData queryMetaData; /// @brief History of complete path: represents branches taken to /// reach/create this state (both concrete and symbolic) -- cgit 1.4.1