2 // Created by ssunny on 7/1/16.
5 #ifndef DYNINST_SYMEVALSEMANTICS_H
6 #define DYNINST_SYMEVALSEMANTICS_H
8 #include "external/rose/armv8InstructionEnum.h"
9 #include "BaseSemantics2.h"
10 #include "../../h/SymEval.h"
13 namespace BinaryAnalysis {
14 namespace InstructionSemantics2 {
15 namespace SymEvalSemantics {
17 /***************************************************************************************************/
19 /***************************************************************************************************/
21 typedef Sawyer::SharedPointer<class SValue> SValuePtr;
23 class SValue : public BaseSemantics::SValue {
25 Dyninst::AST::Ptr expr;
27 SValue(Dyninst::Absloc r, Dyninst::Address addr): BaseSemantics::SValue(64) {
28 expr = Dyninst::DataflowAPI::VariableAST::create(Variable(Dyninst::AbsRegion(r), addr));
31 SValue(size_t nbits, uint64_t num): BaseSemantics::SValue(nbits) {
32 expr = Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(num, nbits));
35 SValue(Dyninst::AST::Ptr expr): BaseSemantics::SValue(64) {
40 static SValuePtr instance(Dyninst::Absloc r, Dyninst::Address addr) {
41 return SValuePtr(new SValue(r, addr));
44 static SValuePtr instance(size_t nbits, uint64_t num) {
45 return SValuePtr(new SValue(nbits, num));
48 static SValuePtr instance(Dyninst::AST::Ptr expr) {
49 return SValuePtr(new SValue(expr));
53 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const {
54 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
57 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const {
58 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
62 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const {
63 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(true)));
66 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t num) const {
67 return SValuePtr(new SValue(nbits, num));
70 virtual BaseSemantics::SValuePtr boolean_(bool value) const {
71 return SValuePtr(new SValue(Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(value?1:0, 1))));
74 virtual BaseSemantics::SValuePtr copy(size_t new_width = 0) const {
75 SValuePtr retval(new SValue(this->get_expression()));
76 if (new_width!=0 && new_width!=retval->get_width())
77 retval->set_width(new_width);
81 virtual Sawyer::Optional<BaseSemantics::SValuePtr>
82 createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const;
85 static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
86 SValuePtr retval = v.dynamicCast<SValue>();
87 ASSERT_not_null(retval);
92 virtual Dyninst::AST::Ptr get_expression() {
96 virtual bool isBottom() const {
97 return expr->getID() == Dyninst::DataflowAPI::V_BottomAST;
100 virtual bool is_number() const {
101 return expr->getID() == Dyninst::DataflowAPI::V_ConstantAST;
104 virtual uint64_t get_number() const {
105 assert(expr->getID() == Dyninst::DataflowAPI::V_ConstantAST);
106 Dyninst::DataflowAPI::Constant constant = expr->val();
107 ASSERT_not_null(constant);
111 virtual void print(std::ostream &, BaseSemantics::Formatter &) const { }
116 /***************************************************************************************************/
118 /***************************************************************************************************/
120 typedef boost::shared_ptr<class RegisterStateARM64> RegisterStateARM64Ptr;
122 class RegisterStateARM64 : public BaseSemantics::RegisterState {
124 RegisterStateARM64(const BaseSemantics::SValuePtr &protoval,
125 const RegisterDictionary *regdict) : RegisterState(protoval, regdict) { }
128 static RegisterStateARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
129 const RegisterDictionary *regdict) {
130 return RegisterStateARM64Ptr(new RegisterStateARM64(protoval, regdict));
133 virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval,
134 const RegisterDictionary *regdict) const {
135 return instance(protoval, regdict);
138 virtual BaseSemantics::RegisterStatePtr clone() const {
139 ASSERT_not_implemented("RegisterState::clone() should not be called with Dyninst's SymEval policy");
142 static RegisterStateARM64Ptr promote(const BaseSemantics::RegisterStatePtr &from) {
143 RegisterStateARM64Ptr retval = boost::dynamic_pointer_cast<RegisterStateARM64>(from);
144 ASSERT_not_null(retval);
149 virtual void clear() {
150 ASSERT_not_implemented("RegisterState::clear() should not be called with Dyninst's SymEval policy");
153 virtual void zero() {
154 ASSERT_not_implemented("RegisterState::zero() should not be called with Dyninst's SymEval policy");
157 virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
158 virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
160 virtual void print(std::ostream &, BaseSemantics::Formatter &) const {}
162 virtual bool merge(const RegisterDescriptor &other, BaseSemantics::RiscOperators *ops) {
166 void writeRegister(const RegisterDescriptor ®, const BaseSematics::SValuePtr &value,
167 Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
170 Dyninst::AST::Ptr wrap(Dyninst::Absloc r) {
171 return Dyninst::DataflowAPI::VariableAST::create(Dyninst::DataflowAPI::Variable(Dyninst::AbsRegion(r), addr));
174 Dyninst::Absloc convert(ARMv8GeneralPurposeRegister r, unsigned int size);
178 /***************************************************************************************************/
180 /***************************************************************************************************/
182 typedef boost::shared_ptr<class MemoryStateARM64> MemoryStateARM64Ptr;
184 class MemoryStateARM64 : public BaseSemantics::MemoryState {
186 MemoryStateARM64(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval):
187 BaseSemantics::MemoryState(addrProtoval, valProtoval) { }
190 static MemoryStateARM64Ptr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
191 return MemoryStateARM64Ptr(new MemoryStateARM64(addrProtoval, valProtoval));
194 virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const {
195 return instance(addrProtoval, valProtoval);
198 static MemoryStateARM64Ptr promote(const BaseSemantics::MemoryStatePtr &from) {
199 MemoryStateARM64Ptr retval = boost::dynamic_pointer_cast<MemoryStateARM64>(from);
200 ASSERT_not_null(retval);
205 virtual BaseSemantics::MemoryStatePtr clone() const {
206 ASSERT_not_implemented("MemoryState::clone() should not be called with Dyninst's SymEval policy");
209 virtual void clear() {
210 ASSERT_not_implemented("MemoryState::clear() should not be called with Dyninst's SymEval policy");
213 virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) {
218 virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
219 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
221 virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
222 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
224 void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSematics::SValuePtr &value,
225 Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
229 /***************************************************************************************************/
231 /***************************************************************************************************/
233 typedef boost::shared_ptr<class StateARM64> StateARM64Ptr;
235 class StateARM64 : public BaseSemantics::State {
237 StateARM64(Dyninst::DataflowAPI::Result_t &r,
239 Dyninst::Architecture ac,
240 Dyninst::InstructionAPI::Instruction::Ptr insn_,
241 const BaseSemantics::RegisterStatePtr ®isters,
242 const BaseSemantics::MemoryStatePtr &memory): BaseSemantics::State(registers, memory) {
243 for (Dyninst::DataflowAPI::Result_t::iterator iter = r.begin();
244 iter != r.end(); ++iter) {
245 Dyninst::Assignment::Ptr a = iter->first;
246 // For a different instruction...
247 if (a->addr() != addr)
249 Dyninst::AbsRegion &o = a->out();
251 if (o.containsOfType(Dyninst::Absloc::Register)) {
252 // We're assuming this is a single register...
253 //std::cerr << "Marking register " << a << std::endl;
254 aaMap[o.absloc()] = a;
257 // Use sufficiently-unique (Heap,0) Absloc
258 // to represent a definition to a memory absloc
259 aaMap[Absloc(0)] = a;
265 static StateARM64Ptr instance(Dyninst::DataflowAPI::Result_t &r,
267 Dyninst::Architecture ac,
268 Dyninst::InstructionAPI::Instruction::Ptr insn_,
269 const BaseSemantics::RegisterStatePtr ®isters,
270 const BaseSemantics::MemoryStatePtr &memory) {
271 return StateARM64Ptr(new StateARM64(r, a, ac, insn_, registers, memory));
274 virtual BaseSemantics::StatePtr create(Dyninst::DataflowAPI::Result_t &r,
276 Dyninst::Architecture ac,
277 Dyninst::InstructionAPI::Instruction::Ptr insn_,
278 const BaseSemantics::RegisterStatePtr ®isters,
279 const BaseSemantics::MemoryStatePtr &memory) const {
280 return instance(r, a, ac, insn_, registers, memory);
283 static StateARM64Ptr promote(const BaseSemantics::StatePtr &from) {
284 StateARM64Ptr retval = boost::dynamic_pointer_cast<StateARM64>(from);
285 ASSERT_not_null(retval);
290 virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
291 virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps,
292 BaseSemantics::RiscOperators *valOps);
295 Dyninst::DataflowAPI::Result_t &res;
296 Dyninst::Architecture arch;
297 Dyninst::Address addr;
298 Dyninst::InstructionAPI::Instruction::Ptr insn;
300 std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> aaMap;
304 /***************************************************************************************************/
306 /***************************************************************************************************/
307 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
309 /** RISC operators for use by the Symbolic Semantics Domain of Dyninst.
312 class RiscOperators : public BaseSemantics::RiscOperators {
314 RiscOperators(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver = NULL)
315 : BaseSemantics::RiscOperators(protoval, solver) {
316 (void)SValue::promote(protoval);
319 RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL)
320 : BaseSemantics::RiscOperators(state, solver) {
321 (void)SValue::promote(state->protoval());
325 static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval,
326 SMTSolver *solver = NULL) {
327 return RiscOperatorsPtr(new RiscOperators(protoval, solver));
330 static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL) {
331 return RiscOperatorsPtr(new RiscOperators(state, solver));
335 virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
336 SMTSolver *solver = NULL) {
337 return instance(protoval, solver);
340 virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
341 SMTSolver *solver = NULL) {
342 return instance(state, solver);
346 /** Run-time promotion of a base RiscOperators pointer to symbolic operators. This is a checked conversion--it
347 * will fail if @p x does not point to a SymbolicSemantics::RiscOperators object. */
348 static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
349 RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
350 ASSERT_not_null(retval);
355 virtual BaseSemantics::SValuePtr boolean_(bool b) {
356 SValuePtr retVal = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
360 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) {
361 SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
366 virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
367 const BaseSemantics::SValuePtr &b_);
368 virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
369 const BaseSemantics::SValuePtr &b_);
370 virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
371 const BaseSemantics::SValuePtr &b_);
372 virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_);
373 virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
374 size_t begin, size_t end);
375 virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
376 const BaseSemantics::SValuePtr &a_,
377 const BaseSemantics::SValuePtr &b_);
378 virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
379 const BaseSemantics::SValuePtr &b_);
380 virtual BaseSemantics::SValuePtr leastSignificantBit(const BaseSemantics::SValuePtr &a_);
381 virtual BaseSemantics::SValuePtr mostSignificantBit(const BaseSemantics::SValuePtr &a_);
382 virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
383 const BaseSemantics::SValuePtr &b_);
384 virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
385 const BaseSemantics::SValuePtr &b_);
386 virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
387 const BaseSemantics::SValuePtr &b_);
388 virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
389 const BaseSemantics::SValuePtr &b_);
390 virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
391 const BaseSemantics::SValuePtr &b_);
392 virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_);
393 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_,
394 size_t newwidth = 0);
395 virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
396 const BaseSemantics::SValuePtr &b_);
397 virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
398 const BaseSemantics::SValuePtr &b_,
399 const BaseSemantics::SValuePtr &c_,
400 BaseSemantics::SValuePtr &carry_out);
401 virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_);
402 virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
403 const BaseSemantics::SValuePtr &b_);
404 virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
405 const BaseSemantics::SValuePtr &b_);
406 virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
407 const BaseSemantics::SValuePtr &b_);
408 virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
409 const BaseSemantics::SValuePtr &b_);
410 virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
411 const BaseSemantics::SValuePtr &b_);
412 virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
413 const BaseSemantics::SValuePtr &b_);
416 virtual BaseSemantics::SValuePtr readMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt,
417 const BaseSemantics::SValuePtr &cond);
418 virtual void writeMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data,
419 const BaseSemantics::SValuePtr &cond);
422 Dyninst::AST::Ptr getUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
425 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a);
428 Dyninst::AST::Ptr getBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
432 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b);
435 Dyninst::AST::Ptr getTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
440 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b, c);
443 SValuePtr createUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_) {
444 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
445 Dyninst::AST::Ptr ast = getUnaryAST(op, a);
449 SValuePtr createBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) {
450 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
451 Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
452 Dyninst::AST::Ptr ast = getBinaryAST(op, a, b);
453 return SValue::instance(ast);
456 SValuePtr createTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_,
457 const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, size_t s = 0) {
458 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
459 Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
460 Dyninst::AST::Ptr c = SValue::promote(c_)->get_expression();
461 Dyninst::AST::Ptr ast = getTernaryAST(op, a, b, c, s);
462 return SValue::instance(ast);
471 #endif //DYNINST_SYMEVALSEMANTICS_H