ROSE 0.11.145.147
SValue.h
1#ifndef ROSE_BinaryAnalysis_InstructionSemantics_BaseSemantics_SValue_H
2#define ROSE_BinaryAnalysis_InstructionSemantics_BaseSemantics_SValue_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
5
6#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
7#include <Rose/BinaryAnalysis/SmtSolver.h>
8#include <Combinatorics.h> // rose
9
10#include <boost/serialization/access.hpp>
11#include <boost/serialization/export.hpp>
12#include <boost/serialization/nvp.hpp>
13#include <Sawyer/SharedPointer.h>
14
15namespace Rose {
16namespace BinaryAnalysis {
17namespace InstructionSemantics {
18namespace BaseSemantics {
19
21// Semantic Values
23
24// This is leftover for compatibility with an older API. The old API had code like this:
25// User::SValue user_svalue = BaseSemantics::dynamic_pointer_cast<User::SValue>(base_svalue);
26// Which can be replaced now with
27// User::SValue user_svalue = base_svalue.dynamicCast<User::SValue>();
28template<class To, class From>
29Sawyer::SharedPointer<To> dynamic_pointer_cast(const Sawyer::SharedPointer<From> &from) {
30 return from.template dynamicCast<To>();
31}
32
48public:
50 using Ptr = SValuePtr;
51
52protected:
53 size_t width;
56 // Serialization
57#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
58private:
59 friend class boost::serialization::access;
60
61 template<class S>
62 void serialize(S &s, const unsigned /*version*/) {
63 s & BOOST_SERIALIZATION_NVP(width);
64 }
65#endif
66
68 // Normal, protected, C++ constructors
69protected:
70 SValue(): width(0) {} // needed for serialization
71 explicit SValue(size_t nbits): width(nbits) {} // hot
72 SValue(const SValue &other): Sawyer::SharedObject(other), width(other.width) {}
73
74public:
75 virtual ~SValue() {}
76
78 // Allocating static constructor. None are needed--this class is abstract.
79
81 // Allocating virtual constructors. undefined_() needs underscores, so we do so consistently for all
82 // these allocating virtual c'tors. However, we use copy() rather than copy_() because this one is fundamentally
83 // different: the object (this) is use for more than just selecting which virtual method to invoke.
84 //
85 // The naming scheme we use here is a bit different than for most other objects for historical reasons. Most other classes
86 // use "create" and "clone" as the virtual constructor names, but SValue uses names ending in undercore, and "copy". The
87 // other difference (at least in this base class) is that we don't define any real constructors or static allocating
88 // constructors (usually named "instance")--it's because this is an abstract class.
89public:
95 virtual SValuePtr undefined_(size_t nbits) const = 0; // hot
96
105 virtual SValuePtr unspecified_(size_t nbits) const = 0;
106
112 virtual SValuePtr bottom_(size_t nBits) const = 0;
113
117 virtual SValuePtr number_(size_t nbits, uint64_t number) const = 0; // hot
118
122 virtual SValuePtr boolean_(bool value) const { return number_(1, value?1:0); }
123
127 virtual SValuePtr copy(size_t new_width=0) const = 0;
128
156 createOptionalMerge(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const = 0;
157
164 SValuePtr createMerged(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const /*final*/ {
165 return createOptionalMerge(other, merger, solver).orElse(copy());
166 }
167
169 // Dynamic pointer casts. No-ops since this is the base class
170public:
171 static SValuePtr promote(const SValuePtr &x) {
172 ASSERT_not_null(x);
173 return x;
174 }
175
177 // The rest of the API...
178public:
184 size_t nBits() const /*final*/;
185
191 virtual bool isBottom() const = 0;
192
200 bool isConcrete() const /*final*/;
201
208 Sawyer::Optional<uint64_t> toUnsigned() const /*final*/;
209
216 Sawyer::Optional<int64_t> toSigned() const /*final*/;
217
223 bool mustEqual(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const /*final*/;
224
230 bool mayEqual(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const /*final*/;
231
235 bool isTrue() const /*final*/;
236
240 bool isFalse() const /*final*/;
241
252 std::string comment() const /*final*/;
253 void comment(const std::string&) const /*final*/; // const is intentional (see documentation)
259 virtual void hash(Combinatorics::Hasher&) const = 0;
260
264 void print(std::ostream&) const;
265 virtual void print(std::ostream&, Formatter&) const = 0;
272 std::string toString() const;
273
276 SValuePtr obj;
277 Formatter &fmt;
278 public:
279 WithFormatter(const SValuePtr &svalue, Formatter &fmt): obj(svalue), fmt(fmt) {}
280 void print(std::ostream &stream) const { obj->print(stream, fmt); }
281 };
282
292 WithFormatter operator+(const std::string &linePrefix);
296 // This is the virtual interface that uses names that are not consistent with most of the rest of binary analysis. Calling
297 // these directly is deprecated and we may make them protected at some time. [Robb Matzke 2021-03-18].
299public: // for backward compatibility for now, but assume protected
301 virtual bool is_number() const = 0;
302
304 virtual uint64_t get_number() const = 0;
305
309 virtual size_t get_width() const { return width; }
310 virtual void set_width(size_t nbits) { width = nbits; }
314 virtual bool must_equal(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const = 0;
315
317 virtual bool may_equal(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const = 0;
318
324 virtual std::string get_comment() const { return ""; }
325 virtual void set_comment(const std::string&) const {} // const is intended; cf. doxygen comment
327};
328
329std::ostream& operator<<(std::ostream&, const SValue&);
330std::ostream& operator<<(std::ostream&, const SValue::WithFormatter&);
331
332} // namespace
333} // namespace
334} // namespace
335} // namespace
336
338
339#endif
340#endif
WithFormatter with_format(Formatter &fmt)
Used for printing values with formatting.
Definition SValue.h:290
Sawyer::Optional< uint64_t > toUnsigned() const
Converts a concrete value to a native unsigned integer.
void print(std::ostream &) const
Print a value to a stream using default format.
virtual Sawyer::Optional< SValuePtr > createOptionalMerge(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const =0
Possibly create a new value by merging two existing values.
virtual bool must_equal(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
Virtual API.
virtual void set_width(size_t nbits)
Virtual API.
Definition SValue.h:310
virtual void set_comment(const std::string &) const
Some subclasses support the ability to add comments to values.
Definition SValue.h:325
virtual bool may_equal(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
Virtual API.
virtual SValuePtr number_(size_t nbits, uint64_t number) const =0
Create a new concrete semantic value.
WithFormatter operator+(const std::string &linePrefix)
Used for printing values with formatting.
std::string toString() const
Render this symbolic expression as a string.
virtual SValuePtr boolean_(bool value) const
Create a new, Boolean value.
Definition SValue.h:122
virtual SValuePtr undefined_(size_t nbits) const =0
Create a new undefined semantic value.
virtual bool isBottom() const =0
Determines whether a value is a data-flow bottom.
virtual SValuePtr unspecified_(size_t nbits) const =0
Create a new unspecified semantic value.
bool mayEqual(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
Tests two values for possible equality.
virtual std::string get_comment() const
Some subclasses support the ability to add comments to values.
Definition SValue.h:324
bool isFalse() const
Returns true if concrete zero.
bool isTrue() const
Returns true if concrete non-zero.
SValuePtr createMerged(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const
Create a new value by merging two existing values.
Definition SValue.h:164
virtual SValuePtr copy(size_t new_width=0) const =0
Create a new value from an existing value, changing the width if new_width is non-zero.
bool mustEqual(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
Tests two values for equality.
Sawyer::Optional< int64_t > toSigned() const
Converts a concrete value to a native signed integer.
bool isConcrete() const
Determines if the value is a concrete number.
virtual SValuePtr bottom_(size_t nBits) const =0
Data-flow bottom value.
WithFormatter operator+(Formatter &fmt)
Used for printing values with formatting.
Definition SValue.h:291
Holds a value or nothing.
Definition Optional.h:56
Creates SharedPointer from this.
Base class for reference counted objects.
SharedObject()
Default constructor.
Reference-counting intrusive smart pointer.
Small object support.
Definition SmallObject.h:19
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.
Sawyer support library.