ROSE 0.11.145.192
NullSemantics.h
1#ifndef ROSE_BinaryAnalysis_InstructionSemantics_NullSemantics_H
2#define ROSE_BinaryAnalysis_InstructionSemantics_NullSemantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
5
6#include <Rose/BinaryAnalysis/BasicTypes.h>
7#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics.h>
8
9namespace Rose {
10namespace BinaryAnalysis { // documented elsewhere
11namespace InstructionSemantics { // documented elsewhere
12
13
18namespace NullSemantics {
19
21// Semantic values
23
26
29public:
32
34 using Ptr = SValuePtr;
35
37 // Real constructors.
38public:
39 ~SValue();
40
41protected:
42 explicit SValue(size_t nbits);
43
45 // Static allocating constructors
46public:
49
51 static SValuePtr instance(size_t nbits);
52
54 static SValuePtr instance(size_t nbits, uint64_t /*number*/);
55
57 static SValuePtr instance(const SValuePtr &other);
58
60 // Virtual constructors
61public:
62 virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const override;
63 virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const override;
64 virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const override;
65 virtual BaseSemantics::SValuePtr number_(size_t nBits, uint64_t number) const override;
66 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override;
69 const SmtSolverPtr&) const override;
70
72 // Dynamic pointer casting
73public:
76
78 // Implementations of functions inherited
79public:
80 virtual bool isBottom() const override;
81 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
82 virtual void hash(Combinatorics::Hasher&) const override;
83
85 // Override legacy members. These now are called by the camelCase names in the base class. Eventually we'll switch the
86 // camelCase names to be the virtual functions and get rid of the snake_case names, so be sure to specify "override" in
87 // your own code so you know when we make the switch.
88public:
89 // See isConcrete
90 virtual bool is_number() const override;
91
92 // See toUnsigned and toSigned
93 virtual uint64_t get_number() const override;
94
95 // See mayEqual
96 virtual bool may_equal(const BaseSemantics::SValuePtr&, const SmtSolverPtr& = SmtSolverPtr()) const override;
97
98 // See mustEqual
99 virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr& = SmtSolverPtr()) const override;
100};
101
102
104// Register state
106
108using RegisterStatePtr = boost::shared_ptr<class RegisterState>;
109
114public:
117
120
121public:
123
124protected:
125 RegisterState(const RegisterState &other);
127
128public:
131 const RegisterDictionaryPtr &regdict) const override;
132 virtual BaseSemantics::AddressSpacePtr clone() const override;
133 static RegisterStatePtr promote(const BaseSemantics::AddressSpacePtr &from);
134
136 BaseSemantics::RiscOperators *valOps) override;
137 virtual void clear() override;
138 virtual void zero() override;
147 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
148};
149
150
152// Memory state
154
156using MemoryStatePtr = boost::shared_ptr<class MemoryState>;
157
162public:
165
168
169public:
170 ~MemoryState();
171
172protected:
173 MemoryState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
174 MemoryState(const MemoryStatePtr &other);
175
176public:
177 static MemoryStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
178
179public:
181 const BaseSemantics::SValuePtr &valProtoval) const override;
182 virtual BaseSemantics::AddressSpacePtr clone() const override;
183
184public:
185 static MemoryStatePtr promote(const BaseSemantics::AddressSpacePtr&);
186
187public:
188 virtual void clear() override {}
189
191 const BaseSemantics::SValuePtr &dflt,
192 BaseSemantics::RiscOperators */*addrOps*/,
193 BaseSemantics::RiscOperators */*valOps*/) override;
194
195 virtual void writeMemory(const BaseSemantics::SValuePtr &/*addr*/, const BaseSemantics::SValuePtr &/*value*/,
196 BaseSemantics::RiscOperators */*addrOps*/, BaseSemantics::RiscOperators */*valOps*/) override;
197
199 BaseSemantics::RiscOperators */*addrOps*/,
200 BaseSemantics::RiscOperators */*valOps*/) override;
201
203 BaseSemantics::RiscOperators */*valOps*/) const override;
204
205 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
206
208 BaseSemantics::RiscOperators *valOps) override;
209};
210
211
213// Complete state
215
217using StatePtr = BaseSemantics::StatePtr;
218
219
221// RISC operators
223
225using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
226
229public:
232
235
237 // Real constructors
238protected:
240
241 explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);
242
244 // Static allocating constructors
245public:
247
251
254 const SmtSolverPtr &solver = SmtSolverPtr());
255
258
260 // Virtual constructors
261public:
263 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
264
266 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
267
269 // Risc operators inherited
270public:
272 const BaseSemantics::SValuePtr &b_) override;
273
275 const BaseSemantics::SValuePtr &b_) override;
276
278 const BaseSemantics::SValuePtr &b_) override;
279
281
283 size_t begin_bit, size_t end_bit) override;
284
286 const BaseSemantics::SValuePtr &b_) override;
287
289
291
293 const BaseSemantics::SValuePtr &sa_) override;
294
296 const BaseSemantics::SValuePtr &sa_) override;
297
299 const BaseSemantics::SValuePtr &sa_) override;
300
302 const BaseSemantics::SValuePtr &sa_) override;
303
305 const BaseSemantics::SValuePtr &sa_) override;
306
308
310 const BaseSemantics::SValuePtr &a_,
311 const BaseSemantics::SValuePtr &b_,
312 IteStatus&) override;
313
314 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
315
317 const BaseSemantics::SValuePtr &b_) override;
318
320 const BaseSemantics::SValuePtr &b_,
321 const BaseSemantics::SValuePtr &c_,
322 BaseSemantics::SValuePtr &carry_out/*out*/) override;
323
325
327 const BaseSemantics::SValuePtr &b_) override;
328
330 const BaseSemantics::SValuePtr &b_) override;
331
333 const BaseSemantics::SValuePtr &b_) override;
334
336 const BaseSemantics::SValuePtr &b_) override;
337
339 const BaseSemantics::SValuePtr &b_) override;
340
342 const BaseSemantics::SValuePtr &b_) override;
343
345 const BaseSemantics::SValuePtr &addr,
346 const BaseSemantics::SValuePtr &dflt,
347 const BaseSemantics::SValuePtr &cond) override;
348
350 const BaseSemantics::SValuePtr &addr,
351 const BaseSemantics::SValuePtr &dflt) override;
352
353 virtual void writeMemory(RegisterDescriptor segreg,
354 const BaseSemantics::SValuePtr &addr,
355 const BaseSemantics::SValuePtr &data,
356 const BaseSemantics::SValuePtr &cond) override;
357};
358
359} // namespace
360} // namespace
361} // namespace
362} // namespace
363
364#endif
365#endif
RegisterDictionaryPtr regdict
Registers that are able to be stored by this state.
Base class for most instruction semantics RISC operators.
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Base class for semantics machine states.
Definition State.h:42
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *, BaseSemantics::RiscOperators *) override
Read a value from memory without side effects.
virtual bool merge(const BaseSemantics::AddressSpacePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Merge address spaces for data flow analysis.
virtual BaseSemantics::AddressSpacePtr clone() const override
Deep-copy of this address space.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print an address space.
virtual void writeMemory(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &, BaseSemantics::RiscOperators *, BaseSemantics::RiscOperators *) override
Write a value to memory.
virtual void hash(Combinatorics::Hasher &, BaseSemantics::RiscOperators *, BaseSemantics::RiscOperators *) const override
Hash this address space.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *, BaseSemantics::RiscOperators *) override
Read a value from memory.
virtual void updateReadProperties(RegisterDescriptor) override
Update register properties after reading a register.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor, const BaseSemantics::SValuePtr &, BaseSemantics::RiscOperators *) override
Read a value from a register.
virtual void hash(Combinatorics::Hasher &, BaseSemantics::RiscOperators *, BaseSemantics::RiscOperators *) const override
Hash this address space.
virtual BaseSemantics::AddressSpacePtr clone() const override
Deep-copy of this address space.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print an address space.
virtual void zero() override
Set all registers to the zero.
virtual void clear() override
Removes stored values from the register state.
virtual void updateWriteProperties(RegisterDescriptor, BaseSemantics::InputOutputProperty) override
Update register properties after writing to a register.
virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor, const BaseSemantics::SValuePtr &, BaseSemantics::RiscOperators *) override
Read a register without side effects.
virtual bool merge(const BaseSemantics::AddressSpacePtr &, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Merge address spaces for data flow analysis.
virtual void writeRegister(RegisterDescriptor, const BaseSemantics::SValuePtr &, BaseSemantics::RiscOperators *) override
Write a value to a register.
virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval, const RegisterDictionaryPtr &regdict) const override
Virtual constructor.
NullSemantics operators always return a new undefined value.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with unsigned values.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the right.
virtual BaseSemantics::SValuePtr iteWithStatus(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, IteStatus &) override
If-then-else with status.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two unsigned values.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with signed values.
virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of least significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right arithmetically (with sign bit).
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override
One's complement.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the left.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise AND of two values.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Concatenates the bits of two values.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right logically (no sign bit).
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two signed values.
static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr &regdict)
Instantiate a new RiscOperators object and configures it to use semantic values and states that are d...
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Sign extends a value.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of most significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) override
Add two values of equal size and a carry bit.
static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Static allocating constructor.
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) override
Read memory without side effects.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
Extracts bits from a value.
static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Constructor.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise OR of two values.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiplies two signed values.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override
Two's complement.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted left.
virtual bool may_equal(const BaseSemantics::SValuePtr &, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
virtual bool is_number() const override
Virtual API.
virtual BaseSemantics::SValuePtr undefined_(size_t nBits) const override
Create a new undefined semantic value.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
virtual BaseSemantics::SValuePtr unspecified_(size_t nBits) const override
Create a new unspecified semantic value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
static SValuePtr instance(const SValuePtr &other)
Instantiate a new copy of an existing value.
virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override
Create a new value from an existing value, changing the width if new_width is non-zero.
static SValuePtr instance(size_t nbits, uint64_t)
Instantiate a new concrete value.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
static SValuePtr promote(const BaseSemantics::SValuePtr &)
Promote a base value to a NullSemantics value.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
virtual uint64_t get_number() const override
Virtual API.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
static SValuePtr instance()
Instantiate a new prototypical values.
virtual BaseSemantics::SValuePtr bottom_(size_t nBits) const override
Data-flow bottom value.
static SValuePtr instance(size_t nbits)
Instantiate a new undefined value.
virtual BaseSemantics::SValuePtr number_(size_t nBits, uint64_t number) const override
Create a new concrete semantic value.
Describes (part of) a physical CPU register.
Holds a value or nothing.
Definition Optional.h:56
Reference-counting intrusive smart pointer.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
boost::shared_ptr< AddressSpace > AddressSpacePtr
Shared-ownership pointer for AddressSpace objects.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.