ROSE 0.11.145.250
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/BasicTypes.h>
7#include <Combinatorics.h> // ROSE
8
9#include <Sawyer/SharedObject.h>
10#include <Sawyer/SmallObject.h>
11
12#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
13#include <boost/serialization/access.hpp>
14#include <boost/serialization/export.hpp>
15#include <boost/serialization/nvp.hpp>
16#endif
17
18namespace Rose {
19namespace BinaryAnalysis {
20namespace InstructionSemantics {
21namespace BaseSemantics {
22
24// Semantic Values
26
42public:
44 using Ptr = SValuePtr;
45
46protected:
47 size_t width;
50 // Serialization
51#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
52private:
53 friend class boost::serialization::access;
54
55 template<class S>
56 void serialize(S &s, const unsigned /*version*/) {
57 s & BOOST_SERIALIZATION_NVP(width);
58 }
59#endif
60
62 // Normal, protected, C++ constructors
63protected:
64 SValue(); // needed for serialization
65 explicit SValue(size_t nbits); // hot
66 SValue(const SValue&);
67 SValue& operator=(const SValue&);
68
69public:
70 virtual ~SValue();
71
73 // Allocating static constructor. None are needed--this class is abstract.
74
76 // Allocating virtual constructors. undefined_() needs underscores, so we do so consistently for all
77 // these allocating virtual c'tors. However, we use copy() rather than copy_() because this one is fundamentally
78 // different: the object (this) is use for more than just selecting which virtual method to invoke.
79 //
80 // The naming scheme we use here is a bit different than for most other objects for historical reasons. Most other classes
81 // use "create" and "clone" as the virtual constructor names, but SValue uses names ending in undercore, and "copy". The
82 // other difference (at least in this base class) is that we don't define any real constructors or static allocating
83 // constructors (usually named "instance")--it's because this is an abstract class.
84public:
90 virtual SValuePtr undefined_(size_t nbits) const = 0; // hot
91
100 virtual SValuePtr unspecified_(size_t nbits) const = 0;
101
107 virtual SValuePtr bottom_(size_t nBits) const = 0;
108
112 virtual SValuePtr number_(size_t nbits, uint64_t number) const = 0; // hot
113
117 virtual SValuePtr boolean_(bool value) const { return number_(1, value?1:0); }
118
122 virtual SValuePtr copy(size_t new_width=0) const = 0;
123
151 createOptionalMerge(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const = 0;
152
159 SValuePtr createMerged(const SValuePtr &other, const MergerPtr&, const SmtSolverPtr&) const /*final*/;
160
162 // Dynamic pointer casts. No-ops since this is the base class
163public:
164 static SValuePtr promote(const SValuePtr&);
165
167 // The rest of the API...
168public:
174 size_t nBits() const /*final*/;
175
181 virtual bool isBottom() const = 0;
182
190 bool isConcrete() const /*final*/;
191
198 Sawyer::Optional<uint64_t> toUnsigned() const /*final*/;
199
206 Sawyer::Optional<int64_t> toSigned() const /*final*/;
207
213 bool mustEqual(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const /*final*/;
214
220 bool mayEqual(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const /*final*/;
221
225 bool isTrue() const /*final*/;
226
230 bool isFalse() const /*final*/;
231
242 std::string comment() const /*final*/;
243 void comment(const std::string&) const /*final*/; // const is intentional (see documentation)
249 virtual void hash(Combinatorics::Hasher&) const = 0;
250
254 void print(std::ostream&) const;
255 virtual void print(std::ostream&, Formatter&) const = 0;
262 std::string toString() const;
263
266 SValuePtr obj;
267 Formatter &fmt;
268 public:
270 void print(std::ostream&) const;
271 };
272
282 WithFormatter operator+(const std::string &linePrefix);
286 // This is the virtual interface that uses names that are not consistent with most of the rest of binary analysis. Calling
287 // these directly is deprecated and we may make them protected at some time. [Robb Matzke 2021-03-18].
289public: // for backward compatibility for now, but assume protected
291 virtual bool is_number() const = 0;
292
294 virtual uint64_t get_number() const = 0;
295
299 virtual size_t get_width() const { return width; }
300 virtual void set_width(size_t nbits) { width = nbits; }
304 virtual bool must_equal(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const = 0;
305
307 virtual bool may_equal(const SValuePtr &other, const SmtSolverPtr &solver = SmtSolverPtr()) const = 0;
308
314 virtual std::string get_comment() const;
315 virtual void set_comment(const std::string&) const; // const is intended; cf. doxygen comment
317};
318
319std::ostream& operator<<(std::ostream&, const SValue&);
320std::ostream& operator<<(std::ostream&, const SValue::WithFormatter&);
321
322} // namespace
323} // namespace
324} // namespace
325} // namespace
326
327#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
329#endif
330
331#endif
332#endif
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:300
virtual void set_comment(const std::string &) const
Some subclasses support the ability to add comments to values.
WithFormatter with_format(Formatter &)
Used for printing values with formatting.
SValuePtr createMerged(const SValuePtr &other, const MergerPtr &, const SmtSolverPtr &) const
Create a new value by merging two existing values.
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+(Formatter &)
Used for printing values with formatting.
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:117
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.
bool isFalse() const
Returns true if concrete zero.
bool isTrue() const
Returns true if concrete non-zero.
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.
Holds a value or nothing.
Definition Optional.h:56
Creates SharedPointer from this.
Base class for reference counted objects.
Small object support.
Definition SmallObject.h:19
Base classes for instruction semantics.
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.