ROSE 0.11.145.263
SymbolicSemantics.h
1#ifndef ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
2#define ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
5#include <Rose/BinaryAnalysis/BasicTypes.h>
6
7#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/Formatter.h>
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryCellList.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryCellMap.h>
10#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryState.h>
11#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/Merger.h>
12#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/RegisterStateGeneric.h>
13#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/RiscOperators.h>
14#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/State.h>
15#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/SValue.h>
16#include <Rose/BinaryAnalysis/SymbolicExpression.h>
17
18#include <Cxx_GrammarSerialization.h>
19
20#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
21#include <boost/serialization/access.hpp>
22#include <boost/serialization/base_object.hpp>
23#include <boost/serialization/export.hpp>
24#include <boost/serialization/set.hpp>
25#endif
26
27#include <inttypes.h>
28#include <map>
29#include <vector>
30
31namespace Rose {
32namespace BinaryAnalysis {
33namespace InstructionSemantics {
34
53namespace SymbolicSemantics {
54
61using InsnSet = std::set<SgAsmInstruction*>;
62
64// Boolean flags
66
68namespace AllowSideEffects {
69 enum Flag {NO, YES};
70}
71
72
74// Merging symbolic values
76
79
82 size_t setSizeLimit_ = 1;
83protected:
84 Merger();
85
86public:
88 typedef MergerPtr Ptr;
89
91 static Ptr instance();
92
94 static Ptr instance(size_t);
95
107 size_t setSizeLimit() const { return setSizeLimit_; }
108 void setSizeLimit(size_t n) { setSizeLimit_ = n; }
110};
111
112
113
115// Semantic values
117
120
123public:
124 SymbolicExpression::Formatter expr_formatter;
125};
126
196public:
199
201 using Ptr = SValuePtr;
202
203protected:
206
209 InsnSet defs;
210
212 // Serialization
213#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
214private:
215 friend class boost::serialization::access;
216
217 template<class S>
218 void serialize(S &s, const unsigned /*version*/) {
219 roseAstSerializationRegistration(s); // "defs" has SgAsmInstruction ASTs
220 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
221 s & BOOST_SERIALIZATION_NVP(expr);
222 s & BOOST_SERIALIZATION_NVP(defs);
223 }
224#endif
225
227 // Real constructors
228protected:
229 SValue(); // needed for serialization
230 explicit SValue(size_t nbits);
231 SValue(size_t nbits, uint64_t number);
233
235 // Static allocating constructors
236public:
239
241 static SValuePtr instance_bottom(size_t nbits);
242
244 static SValuePtr instance_undefined(size_t nbits);
245
247 static SValuePtr instance_unspecified(size_t nbits);
248
250 static SValuePtr instance_integer(size_t nbits, uint64_t value);
251
254
256 // Virtual allocating constructors
257public:
258 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override;
259 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override;
260 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override;
261 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override;
262 virtual BaseSemantics::SValuePtr boolean_(bool value) const override;
263 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override;
264
267 const SmtSolverPtr&) const override;
268
270 // Dynamic pointer casts
271public:
274
276 // Override virtual methods...
277public:
278 virtual bool isBottom() const override;
279
280 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
281
282 virtual void hash(Combinatorics::Hasher&) const override;
283
284protected: // when implementing use these names; but when calling, use the camelCase names
285 virtual bool may_equal(const BaseSemantics::SValuePtr &other,
286 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
287 virtual bool must_equal(const BaseSemantics::SValuePtr &other,
288 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
289
290 // It's not possible to change the size of a symbolic expression in place. That would require that we recursively change
291 // the size of the SymbolicExpression, which might be shared with many unrelated values whose size we don't want to affect.
292 virtual void set_width(size_t nbits) override;
293 virtual bool is_number() const override;
294 virtual uint64_t get_number() const override;
295 virtual std::string get_comment() const override;
296 virtual void set_comment(const std::string&) const override;
297
299 // Additional methods first declared in this class...
300public:
308 virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const;
309
316 virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3);
317 virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2);
318 virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1);
319 virtual void defined_by(SgAsmInstruction *insn);
325 virtual const ExprPtr& get_expression() const;
326
329 virtual void set_expression(const ExprPtr &new_expr);
330 virtual void set_expression(const SValuePtr &source);
347 virtual const InsnSet& get_defining_instructions() const;
348
354 virtual size_t add_defining_instructions(const InsnSet &to_add);
355 virtual size_t add_defining_instructions(const SValuePtr &source);
364 virtual void set_defining_instructions(const InsnSet &new_defs);
365 virtual void set_defining_instructions(const SValuePtr &source);
368};
369
370
372// Register state
374
376typedef BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;
377
378
380// List-based Memory state
382
384typedef boost::shared_ptr<class MemoryListState> MemoryListStatePtr;
385
403public:
406
409
412 public:
414 protected:
415 CellCompressor() {}
416 public:
417 virtual ~CellCompressor() {}
418
420 virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
422 const BaseSemantics::CellList &cells) = 0;
423 };
424
439 public:
440 static Ptr instance();
441 virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
443 const BaseSemantics::CellList &cells) override;
444 };
445
448 public:
449 static Ptr instance();
450 virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
452 const BaseSemantics::CellList &cells) override;
453 };
454
459 CellCompressor::Ptr mccarthy_;
460 CellCompressor::Ptr simple_;
461 protected:
463 public:
464 static Ptr instance();
465 virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
467 const BaseSemantics::CellList &cells) override;
468 };
469
474 public:
475 static Ptr instance();
476 virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
478 const BaseSemantics::CellList &cells) override;
479 };
480
481private:
482 CellCompressor::Ptr cellCompressor_; // Callback when a memory read aliases multiple memory cells.
483
485 // Serialization
486#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
487private:
488 friend class boost::serialization::access;
489
490 template<class S>
491 void serialize(S &s, const unsigned /*version*/) {
492 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
493 }
494#endif
495
496
498 // Real constructors
499protected:
500 MemoryListState(); // for serialization
501 explicit MemoryListState(const BaseSemantics::MemoryCellPtr &protocell);
502 MemoryListState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
503 MemoryListState(const MemoryListState &other);
504
506 // Static allocating constructors
507public:
510
513 static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
514
517
519 // Virtual constructors
520public:
524 const BaseSemantics::SValuePtr &valProtoval) const override;
525
527 virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override;
528
530 virtual BaseSemantics::AddressSpacePtr clone() const override;
531
533 // Dynamic pointer casts
534public:
538
540 // Methods we inherited
541public:
547 BaseSemantics::RiscOperators *valOps) override;
548
554 BaseSemantics::RiscOperators *valOps) override;
555
559 virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
561
562protected:
563 BaseSemantics::SValuePtr readOrPeekMemory(const BaseSemantics::SValuePtr &address,
564 const BaseSemantics::SValuePtr &dflt,
567 AllowSideEffects::Flag allowSideEffects);
568
570 // Methods first declared in this class
571public:
581 // Deprecated [Robb Matzke 2021-12-15]
582 CellCompressor::Ptr get_cell_compressor() const ROSE_DEPRECATED("use cellCompressor");
583 void set_cell_compressor(const CellCompressor::Ptr&) ROSE_DEPRECATED("use cellCompressor");
584};
585
586
588// Map-based Memory state
590
592typedef boost::shared_ptr<class MemoryMapState> MemoryMapStatePtr;
593
611class MemoryMapState: public BaseSemantics::MemoryCellMap {
612public:
615
618
620 // Serialization
621#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
622private:
623 friend class boost::serialization::access;
624
625 template<class S>
626 void serialize(S &s, const unsigned /*version*/) {
627 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
628 }
629#endif
630
632 // Real constructors
633protected:
634 MemoryMapState(); // for serialization
635
636 explicit MemoryMapState(const BaseSemantics::MemoryCellPtr &protocell);
637
638 MemoryMapState(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
639
641 // Static allocating constructors
642public:
645
648 static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval);
649
652
654 // Virtual constructors
655public:
659 const BaseSemantics::SValuePtr &valProtoval) const override;
660
663
665 virtual BaseSemantics::AddressSpacePtr clone() const override;
666
668 // Dynamic pointer casts
669public:
673
675 // Methods we override from the super class (documented in the super class)
676public:
677 virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const override;
678};
679
680
681
683// Default memory state
685
686// List-base memory was the type originally used by this domain. We must keep it that way because some analysis, including 3rd
687// party, assumes that the state is list-based. New analysis can use the map-based state by instantiating it when the symbolic
688// risc operators are constructed.
690typedef MemoryListStatePtr MemoryStatePtr;
691
693// Complete state
695
697typedef BaseSemantics::StatePtr StatePtr;
698
699
701// RISC operators
703
710
717
719typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
720
741public:
744
747
748protected:
749 bool omit_cur_insn; // if true, do not include cur_insn as a definer
750 DefinersMode computingDefiners_; // whether to track definers (instruction VAs) of SValues
751 WritersMode computingMemoryWriters_; // whether to track writers (instruction VAs) to memory.
752 WritersMode computingRegisterWriters_; // whether to track writers (instruction VAs) to registers.
753 uint64_t trimThreshold_; // max size of expressions (zero means no maximimum)
754 bool reinterpretMemoryReads_; // cast data to unsigned integer when reading from memory
755 bool reinterpretRegisterReads_; // cast data to unsigned integer when reading from registers
756 size_t nTrimmed_ = 0; // number of expressions trimmed down to a new variable
757
758
760 // Serialization
761#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
762private:
763 friend class boost::serialization::access;
764
765 template<class S>
766 void serialize(S &s, const unsigned /*version*/) {
767 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
768 s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
769 s & BOOST_SERIALIZATION_NVP(computingDefiners_);
770 s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
771 s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
772 s & BOOST_SERIALIZATION_NVP(trimThreshold_);
773 }
774#endif
775
777 // Real constructors
778protected:
779 RiscOperators(); // for serialization
780
781 explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver);
782
783 explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver);
784
786 // Static allocating constructors
787public:
789
793
797 const SmtSolverPtr &solver = SmtSolverPtr());
798
802
804 // Virtual constructors
805public:
807 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
808
810 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
811
813 // Dynamic pointer casts
814public:
818
820 // Inherited methods for constructing values.
821public:
822 virtual BaseSemantics::SValuePtr boolean_(bool b) override;
823 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override;
824
826 // New methods for constructing values, so we don't have to write so many SValue::promote calls in the RiscOperators
827 // implementations.
828 SValuePtr svalueExpr(const ExprPtr &expr, const InsnSet &defs=InsnSet());
829
830protected:
831 SValuePtr svalueUndefined(size_t nbits);
832 SValuePtr svalueBottom(size_t nbits);
833 SValuePtr svalueUnspecified(size_t nbits);
834 SValuePtr svalueNumber(size_t nbits, uint64_t value);
835 SValuePtr svalueBoolean(bool b);
836
838 // Configuration properties
839public:
840
858 void computingDefiners(DefinersMode m) { computingDefiners_ = m; }
859 DefinersMode computingDefiners() const { return computingDefiners_; }
880 void computingMemoryWriters(WritersMode m) { computingMemoryWriters_ = m; }
881 WritersMode computingMemoryWriters() const { return computingMemoryWriters_; }
905 void computingRegisterWriters(WritersMode m) { computingRegisterWriters_ = m; }
906 WritersMode computingRegisterWriters() const { return computingRegisterWriters_; }
909 // Used internally to control whether cur_insn should be omitted from the list of definers.
910 bool getset_omit_cur_insn(bool b) { bool retval = omit_cur_insn; omit_cur_insn=b; return retval; }
911
918 void trimThreshold(uint64_t n) { trimThreshold_ = n; }
919 uint64_t trimThreshold() const { return trimThreshold_; }
928 size_t nTrimmed() const { return nTrimmed_; }
929 void nTrimmed(size_t n) { nTrimmed_ = n; }
939 bool reinterpretMemoryReads() const { return reinterpretMemoryReads_; }
940 void reinterpretMemoryReads(bool b) { reinterpretMemoryReads_ = b; }
941 bool reinterpretRegisterReads() const { return reinterpretRegisterReads_; }
942 void reinterpretRegisterReads(bool b) { reinterpretRegisterReads_ = b; }
946 // Methods first defined at this level of the class hierarchy
947public:
1009 virtual void substitute(const SValuePtr &from, const SValuePtr &to);
1010
1016
1022
1027
1029 // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
1030public:
1031 virtual void interrupt(int majr, int minr) override;
1033 const BaseSemantics::SValuePtr &b_) override;
1035 const BaseSemantics::SValuePtr &b_) override;
1037 const BaseSemantics::SValuePtr &b_) override;
1040 size_t begin_bit, size_t end_bit) override;
1042 const BaseSemantics::SValuePtr &b_) override;
1046 const BaseSemantics::SValuePtr &sa_) override;
1048 const BaseSemantics::SValuePtr &sa_) override;
1050 const BaseSemantics::SValuePtr &sa_) override;
1052 const BaseSemantics::SValuePtr &sa_) override;
1054 const BaseSemantics::SValuePtr &sa_) override;
1057 const BaseSemantics::SValuePtr &a_,
1058 const BaseSemantics::SValuePtr &b_,
1059 IteStatus&) override;
1060 virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1061 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
1063 const BaseSemantics::SValuePtr &b_) override;
1065 const BaseSemantics::SValuePtr &b_,
1066 const BaseSemantics::SValuePtr &c_,
1067 BaseSemantics::SValuePtr &carry_out/*out*/) override;
1070 const BaseSemantics::SValuePtr &b_) override;
1072 const BaseSemantics::SValuePtr &b_) override;
1074 const BaseSemantics::SValuePtr &b_) override;
1076 const BaseSemantics::SValuePtr &b_) override;
1078 const BaseSemantics::SValuePtr &b_) override;
1080 const BaseSemantics::SValuePtr &b_) override;
1082 SgAsmFloatType *retType) override;
1085 const BaseSemantics::SValuePtr &dflt) override;
1087 const BaseSemantics::SValuePtr &dflt) override;
1088 virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) override;
1090 const BaseSemantics::SValuePtr &addr,
1091 const BaseSemantics::SValuePtr &dflt,
1092 const BaseSemantics::SValuePtr &cond) override;
1094 const BaseSemantics::SValuePtr &addr,
1095 const BaseSemantics::SValuePtr &dflt) override;
1096 virtual void writeMemory(RegisterDescriptor segreg,
1097 const BaseSemantics::SValuePtr &addr,
1098 const BaseSemantics::SValuePtr &data,
1099 const BaseSemantics::SValuePtr &cond) override;
1100
1101public:
1102 BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg,
1103 const BaseSemantics::SValuePtr &addr,
1104 const BaseSemantics::SValuePtr &dflt,
1105 AllowSideEffects::Flag);
1106};
1107
1108} // namespace
1109} // namespace
1110} // namespace
1111} // namespace
1112
1113#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
1118#endif
1119
1120#endif
1121#endif
Base class for most instruction semantics RISC operators.
Base class for semantics machine states.
Definition State.h:45
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells)=0
Compress the cells into a single value.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
static MemoryListStatePtr instance(const MemoryListStatePtr &other)
Instantiates a new deep copy of an existing state.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory with no side effects.
static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
static MemoryListStatePtr promote(const BaseSemantics::AddressSpacePtr &)
Recasts a base pointer to a symbolic memory state.
CellCompressor::Ptr cellCompressor() const
Callback for handling a memory read whose address matches more than one memory cell.
void cellCompressor(const CellCompressor::Ptr &)
Callback for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::AddressSpacePtr clone() const override
Virtual copy constructor.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
virtual BaseSemantics::AddressSpacePtr clone() const override
Virtual copy constructor.
static MemoryMapStatePtr promote(const BaseSemantics::AddressSpacePtr &)
Recasts a base pointer to a symbolic memory state.
static MemoryMapStatePtr instance(const MemoryMapStatePtr &other)
Instantiates a new deep copy of an existing state.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
virtual CellKey generateCellKey(const BaseSemantics::SValuePtr &addr_) const override
Generate a cell lookup key.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
Defines RISC operators for the SymbolicSemantics domain.
static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
void computingDefiners(DefinersMode m)
Property: Track which instructions define a semantic value.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with unsigned values.
static SgAsmFloatType * sgIsIeee754(SgAsmType *)
Tests whether a SgAsmType is an IEEE-754 floating-point type.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
size_t nTrimmed() const
Property: Number of symbolic expressions trimmed.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with signed values.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override
One's complement.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two signed values.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Sign extends a value.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the right.
virtual BaseSemantics::SValuePtr boolean_(bool b) override
Returns a Boolean value.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Reads a value from a register.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Obtain a register value without side effects.
WritersMode computingRegisterWriters() const
Property: Track latest writer to each register.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right logically (no sign bit).
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) override
Read memory without side effects.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the left.
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 number_(size_t nbits, uint64_t value) override
Returns a number of the specified bit width.
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 shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right arithmetically (with sign bit).
virtual BaseSemantics::SValuePtr filterResult(const BaseSemantics::SValuePtr &)
Filters results from RISC operators.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators pointer to symbolic operators.
void nTrimmed(size_t n)
Property: Number of symbolic expressions trimmed.
void computingRegisterWriters(WritersMode m)
Property: Track latest writer to each register.
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a_) override
Writes a value to a register.
virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType, SgAsmFloatType *retType) override
Convert from one floating-point type to another.
virtual void interrupt(int majr, int minr) override
Unconditionally raise an interrupt.
static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
void trimThreshold(uint64_t n)
Property: Maximum size of expressions.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two unsigned values.
virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr &, SgAsmType *) override
Reinterpret an expression as a different type.
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 equalToZero(const BaseSemantics::SValuePtr &a_) override
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr iteWithStatus(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, IteStatus &) override
If-then-else with status.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
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 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.
virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits.
WritersMode computingMemoryWriters() const
Property: Track which instructions write to each memory location.
virtual void substitute(const SValuePtr &from, const SValuePtr &to)
Substitute all occurrences of from with to in the current state.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Adds two integers of equal size.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override
Two'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 concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Concatenates the bits of two values.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted left.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
Extracts bits from a value.
uint64_t trimThreshold() const
Property: Maximum size of expressions.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise AND of two values.
static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiplies two signed values.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise OR of two values.
virtual SymbolicExpression::Type sgTypeToSymbolicType(SgAsmType *)
Convert a SgAsmType to a symbolic type.
Type of values manipulated by the SymbolicSemantics domain.
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
virtual size_t add_defining_instructions(const InsnSet &to_add)
Adds definitions to the list of defining instructions.
static SValuePtr instance()
Instantiate a new prototypical value.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
Adds instructions to the list of defining instructions.
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_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
virtual void set_expression(const ExprPtr &new_expr)
Changes the expression stored in the value.
static SValuePtr promote(const BaseSemantics::SValuePtr &)
Promote a base value to a SymbolicSemantics value.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value)
Instantiate a new symbolic value.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3)
Adds instructions to the list of defining instructions.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
virtual size_t add_defining_instructions(const SValuePtr &source)
Adds definitions to the list of defining instructions.
virtual void set_defining_instructions(SgAsmInstruction *insn)
Set defining instructions.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
virtual void set_width(size_t nbits) override
Virtual API.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
virtual std::string get_comment() const override
Some subclasses support the ability to add comments to values.
virtual void set_comment(const std::string &) const override
Some subclasses support the ability to add comments to values.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
virtual size_t add_defining_instructions(SgAsmInstruction *insn)
Adds definitions to the list of defining instructions.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
virtual uint64_t get_number() const override
Virtual API.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
virtual void set_expression(const SValuePtr &source)
Changes the expression stored in the value.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
Describes (part of) a physical CPU register.
Controls formatting of expression trees when printing.
Interior node of an expression tree for instruction semantics.
Leaf node of an expression tree for instruction semantics.
Base class for symbolic expression nodes.
Holds a value or nothing.
Definition Optional.h:56
Base class for reference counted objects.
Reference-counting intrusive smart pointer.
Floating point types.
Base class for machine instructions.
Base class for binary types.
Base classes for instruction semantics.
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.
std::list< MemoryCellPtr > CellList
List of memory cells.
Definition MemoryCell.h:280
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
boost::shared_ptr< AddressSpace > AddressSpacePtr
Shared-ownership pointer for AddressSpace objects.
WritersMode
How to update the list of writers stored at each abstract location.
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
DefinersMode
How to update the list of definers stored in each semantic value.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
Sawyer::SharedPointer< Interior > InteriorPtr
Reference counting pointer.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Sawyer::SharedPointer< Leaf > LeafPtr
Reference counting pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.