ROSE 0.11.145.276
Semantics.h
1#ifndef ROSE_BinaryAnalysis_Partitioner2_Semantics_H
2#define ROSE_BinaryAnalysis_Partitioner2_Semantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
5
6#include <Rose/As.h>
7#include <Rose/BinaryAnalysis/MemoryMap.h>
8#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryCellMap.h>
10#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
11#include <Rose/BinaryAnalysis/SymbolicExpression.h>
12
13#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
14#include <boost/serialization/access.hpp>
15#endif
16
17namespace Rose {
18namespace BinaryAnalysis {
19namespace Partitioner2 {
20
27namespace Semantics {
28
31
34
37
40
43
46
48// Memory State
50
57template<class Super = InstructionSemantics::SymbolicSemantics::MemoryListState> // or MemoryMapState
58class MemoryState: public Super {
59public:
61 using Ptr = boost::shared_ptr<MemoryState>;
62
63private:
64 MemoryMapPtr map_;
65 std::vector<SValuePtr> addressesRead_;
66 bool enabled_;
67
68#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
69private:
70 friend class boost::serialization::access;
71 template<class S> void serialize(S&, unsigned version);
72#endif
73
74protected:
75 MemoryState() // for serialization
76 : enabled_(true) {}
77
79 : Super(protocell), enabled_(true) {}
80
81 MemoryState(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval,
83 : Super(addrProtoval, valProtoval), enabled_(true) {}
84
85public:
88 return Ptr(new MemoryState(protocell));
89 }
90
94 return Ptr(new MemoryState(addrProtoval, valProtoval));
95 }
96
98 static Ptr instance(const Ptr &other) {
99 return Ptr(new MemoryState(*other));
100 }
101
102public:
106 const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval) const override {
107 return instance(addrProtoval, valProtoval);
108 }
109
113 return instance(protocell);
114 }
115
118 clone() const override {
119 return Ptr(new MemoryState(*this));
120 }
121
122public:
125 static Ptr
127 Ptr retval = as<MemoryState>(x);
128 assert(x!=NULL);
129 return retval;
130 }
131
132public:
139 bool enabled() const { return enabled_; }
140 void enabled(bool b) { enabled_ = b; }
150 MemoryMapPtr memoryMap() const { return map_; }
151 void memoryMap(const MemoryMapPtr &map) { map_ = map; }
157 const std::vector<SValuePtr>& addressesRead() const { return addressesRead_; }
158 std::vector<SValuePtr>& addressesRead() { return addressesRead_; }
161public:
167
168 virtual void
173
179
180private:
182 readOrPeekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
186 bool withSideEffects);
187
188public:
189 void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&) const override;
190};
191
194
197
199using MemoryListStatePtr = boost::shared_ptr<MemoryListState>;
200
202using MemoryMapStatePtr = boost::shared_ptr<MemoryMapState>;
203
205// RISC Operators
207
209using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
210
216public:
218 using Ptr = RiscOperatorsPtr;
219
220private:
221 static const size_t TRIM_THRESHOLD_DFLT = 100;
222
224 // Serialization
225#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
226private:
227 friend class boost::serialization::access;
228 template<class S> void serialize(S&, unsigned version);
229#endif
230
232 // Real constructors
233protected:
234 RiscOperators(); // for serialization
235
237
239
240public:
242
244 // Static allocating constructors
245public:
269 // Virtual constructors
270public:
273 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
274
277 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
278
280 // Dynamic pointer casts
281public:
285
287 // Override methods from base class.
288public:
289 virtual void startInstruction(SgAsmInstruction*) override;
290};
291
293// Memory State
295
296template<class Super>
302 return readOrPeekMemory(addr, dflt, addrOps, valOps, true/*with side effects*/);
303}
304
305template<class Super>
311 return readOrPeekMemory(addr, dflt, addrOps, valOps, false/*no side effects*/);
312}
313
314template<class Super>
320 bool withSideEffects) {
321 using namespace InstructionSemantics;
322 ASSERT_require2(8==dflt->nBits(), "multi-byte reads should have been handled above this call");
323
324 if (!enabled_)
325 return dflt->copy();
326
327 addressesRead_.push_back(SValue::promote(addr));
328
329 // Symbolic memory takes precedence over concrete memory when the address is concrete. I.e., reading from concrete address
330 // 0x1234 the first time will return the value stored in concrete memory, say 0 and not make any modifications to the symbolic
331 // state. If the value 1 is then written to 0x1234 it will be written to the symbolic state, not the concrete state (because
332 // changing the concrete state is probably a global side effect unless the entire memory map has been copied). Subsequent reads
333 // from 0x1234 should return the 1 that we wrote, not the 0 that's stored in the concrete memory.
334 BaseSemantics::SValuePtr symbolicDefault = dflt;
335 if (map_ && addr->toUnsigned()) {
336 Address va = *addr->toUnsigned();
337 bool isModifiable = map_->at(va).require(MemoryMap::WRITABLE).exists();
338 bool isInitialized = map_->at(va).require(MemoryMap::INITIALIZED).exists();
339
340 // Read the byte from concrete memory if possible.
341 SymbolicExpression::Ptr valueRead;
342 if (!isModifiable || isInitialized) {
343 uint8_t byte;
344 if (1 == map_->at(va).limit(1).read(&byte).size())
345 valueRead = SymbolicExpression::makeIntegerConstant(8, byte);
346 }
347
348 // If concrete memory is mutable, then we don't really know the value for sure.
349 if (isModifiable) {
350 const auto indeterminate = SymbolicExpression::makeIntegerVariable(8);
351 if (valueRead) {
352 valueRead = SymbolicExpression::makeSet(valueRead, indeterminate, valOps->solver());
353 } else {
354 valueRead = indeterminate;
355 }
356 }
357
358 // Make the value that we read from concrete memory the default for reading from symbolic memory.
359 if (valueRead) {
360 auto val = SymbolicSemantics::SValue::promote(valOps->undefined_(8));
361 val->set_expression(valueRead);
362 symbolicDefault = val;
363 }
364
365 // Does symbolic memory define this address?
366 const bool isPresentSymbolically = [this, &addr]() {
367 struct CellFinder: BaseSemantics::MemoryCell::Visitor {
368 BaseSemantics::SValue::Ptr needle;
369 bool found = false;
370
371 explicit CellFinder(const BaseSemantics::SValue::Ptr &addr)
372 : needle(addr) {
373 ASSERT_not_null(addr);
374 }
375
376 void operator()(BaseSemantics::MemoryCell::Ptr &haystack) override {
377 ASSERT_not_null(haystack);
378 if (haystack->address()->mustEqual(needle))
379 found = true;
380 }
381 } cellFinder(addr);
382 this->traverse(cellFinder);
383 return cellFinder.found;
384 }();
385
386 // Perhaps there is no need to update the symbolic memory.
387 if (!isPresentSymbolically && isInitialized && !isModifiable)
388 return symbolicDefault;
389
390 // But if we do have to update the symbolic memory, do so in a way that makes it look like the value was always there.
391 if (!isPresentSymbolically) {
392 SgAsmInstruction *addrInsn = addrOps->currentInstruction(); // order is important because addrOps and valOps
393 SgAsmInstruction *valInsn = valOps->currentInstruction(); // might be the same object. Read both of them
394 addrOps->currentInstruction(nullptr); // before clearing either of them.
395 valOps->currentInstruction(nullptr);
396 Super::writeMemory(addr, symbolicDefault, addrOps, valOps);
397 addrOps->currentInstruction(addrInsn);
398 valOps->currentInstruction(valInsn);
399 }
400 }
401
402 // Read from symbolic memory
403 if (withSideEffects) {
404 return Super::readMemory(addr, symbolicDefault, addrOps, valOps);
405 } else {
406 return Super::peekMemory(addr, symbolicDefault, addrOps, valOps);
407 }
408}
409
410template<class Super>
411void
416 if (!enabled_)
417 return;
418 Super::writeMemory(addr, value, addrOps, valOps);
419}
420
421template<class Super>
422void
424 namespace BS = InstructionSemantics::BaseSemantics;
425
426 out <<fmt.get_line_prefix() <<"concrete memory:\n";
427 if (map_) {
428 map_->dump(out, fmt.get_line_prefix() + " ");
429 } else {
430 out <<fmt.get_line_prefix() <<"no memory map\n";
431 }
432
433 const bool isEmpty = as<const BS::MemoryCellState>(this) ?
434 as<const BS::MemoryCellState>(this)->allCells().empty() :
435 false;
436
437 if (as<const BS::MemoryCellMap>(this)) {
438 out <<fmt.get_line_prefix() <<"symbolic memory (map-based):\n";
439 } else {
440 out <<fmt.get_line_prefix() <<"symbolic memory (list-based):\n";
441 }
442 BS::Indent indent(fmt);
443 if (isEmpty) {
444 out <<fmt.get_line_prefix() <<"empty\n";
445 } else {
446 Super::print(out, fmt);
447 }
448}
449
450} // namespace
451} // namespace
452} // namespace
453} // namespace
454
455#endif
456#endif
std::string get_line_prefix() const
The string to print at the start of each line.
Definition Formatter.h:60
Base class for most instruction semantics RISC operators.
virtual SValuePtr undefined_(size_t nbits)
Returns a new undefined value.
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
virtual SgAsmInstruction * currentInstruction() const
Property: Current instruction.
Sawyer::Optional< uint64_t > toUnsigned() const
Converts a concrete value to a native unsigned integer.
Base class for semantics machine states.
Definition State.h:45
Defines RISC operators for the SymbolicSemantics domain.
Type of values manipulated by the SymbolicSemantics domain.
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 promote(const BaseSemantics::SValuePtr &)
Promote a base value to a SymbolicSemantics value.
std::vector< SValuePtr > & addressesRead()
Property: concrete virtual addresses that were read.
Definition Semantics.h:158
const std::vector< SValuePtr > & addressesRead() const
Property: concrete virtual addresses that were read.
Definition Semantics.h:157
virtual void writeMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &value, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
Definition Semantics.h:412
void print(std::ostream &, InstructionSemantics::BaseSemantics::Formatter &) const override
Print an address space.
Definition Semantics.h:423
boost::shared_ptr< MemoryState > Ptr
Shared-ownership pointer to a Semantics::MemoryState.
Definition Semantics.h:61
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr create(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval, const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
Definition Semantics.h:105
static Ptr instance(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
Definition Semantics.h:87
void memoryMap(const MemoryMapPtr &map)
The memory map for the specimen.
Definition Semantics.h:151
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr create(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
Definition Semantics.h:112
MemoryMapPtr memoryMap() const
The memory map for the specimen.
Definition Semantics.h:150
virtual InstructionSemantics::BaseSemantics::AddressSpacePtr clone() const override
Virtual copy constructor.
Definition Semantics.h:118
static Ptr instance(const Ptr &other)
Instantiates a new deep copy of an existing state.
Definition Semantics.h:98
virtual InstructionSemantics::BaseSemantics::SValuePtr readMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &dflt, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
Definition Semantics.h:298
static Ptr promote(const InstructionSemantics::BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
Definition Semantics.h:126
static Ptr instance(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval, const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
Definition Semantics.h:92
virtual InstructionSemantics::BaseSemantics::SValuePtr peekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &dflt, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Read a byte from memory with no side effects.
Definition Semantics.h:307
static RiscOperatorsPtr promote(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators pointer to our operators.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr &, const SmtSolverPtr &)
Instantiate a new RiscOperators with specified state.
static RiscOperatorsPtr instance(const RegisterDictionaryPtr &, const SmtSolverPtr &, SemanticMemoryParadigm memoryParadigm=LIST_BASED_MEMORY)
Instantiate a new RiscOperators object and configure it using default values.
virtual void startInstruction(SgAsmInstruction *) override
Called at the beginning of every instruction.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &)
Instantiate a new RiscOperators object with specified prototypical values.
static RiscOperatorsPtr instance(const RegisterDictionaryPtr &)
Instantiate a new RiscOperators object and configure it using default values.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr &)
Instantiate a new RiscOperators with specified state.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics::BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval)
Instantiate a new RiscOperators object with specified prototypical values.
Reference-counting intrusive smart pointer.
Base class for machine instructions.
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< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
boost::shared_ptr< AddressSpace > AddressSpacePtr
Shared-ownership pointer for AddressSpace objects.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
InstructionSemantics::BaseSemantics::RegisterStateGenericPtr RegisterStatePtr
Reference counting pointer to register state.
Definition Semantics.h:39
InstructionSemantics::BaseSemantics::StatePtr StatePtr
Reference counting pointer to total state.
Definition Semantics.h:45
boost::shared_ptr< MemoryListState > MemoryListStatePtr
Shared-ownership pointer to a MemoryListState.
Definition Semantics.h:199
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to the RISC operators object.
Definition Semantics.h:209
boost::shared_ptr< MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to a MemoryMapState.
Definition Semantics.h:202
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::uint64_t Address
Address.
Definition Address.h:11
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.
ROSE_DLL_API bool isInitialized()
Checks whether the library has been initialized.