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(Dyninst::DataflowAPI::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 //TODO possibly set width differently for register types
36 SValue(Dyninst::AST::Ptr expr): BaseSemantics::SValue(64) {
41 static SValuePtr instance(Dyninst::Absloc r, Dyninst::Address addr) {
42 return SValuePtr(new SValue(r, addr));
45 static SValuePtr instance(size_t nbits, uint64_t num) {
46 return SValuePtr(new SValue(nbits, num));
49 static SValuePtr instance(Dyninst::AST::Ptr expr) {
50 return SValuePtr(new SValue(expr));
54 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const {
55 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
58 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const {
59 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
63 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const {
64 return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(true)));
67 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t num) const {
68 return SValuePtr(new SValue(nbits, num));
71 virtual BaseSemantics::SValuePtr boolean_(bool value) const {
72 return SValuePtr(new SValue(1, value?1:0));
75 virtual BaseSemantics::SValuePtr copy(size_t new_width = 0) const {
76 SValuePtr retval(new SValue(get_expression()));
77 if (new_width!=0 && new_width!=retval->get_width())
78 retval->set_width(new_width);
82 virtual Sawyer::Optional<BaseSemantics::SValuePtr>
83 createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const {
84 ASSERT_not_implemented("SValue::createOptionalMerge not implemented for use in dyninst");
88 static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
89 SValuePtr retval = v.dynamicCast<SValue>();
90 ASSERT_not_null(retval);
95 virtual Dyninst::AST::Ptr get_expression() const {
99 virtual bool isBottom() const {
100 return expr->getID() == Dyninst::AST::V_BottomAST;
103 virtual bool is_number() const {
104 return expr->getID() == Dyninst::AST::V_ConstantAST;
107 virtual uint64_t get_number() const {
108 assert(expr->getID() == Dyninst::AST::V_ConstantAST);
110 Dyninst::DataflowAPI::Constant constant = boost::dynamic_pointer_cast<Dyninst::DataflowAPI::ConstantAST>(expr)->val();
114 virtual void print(std::ostream &, BaseSemantics::Formatter &) const { }
119 /***************************************************************************************************/
121 /***************************************************************************************************/
123 typedef boost::shared_ptr<class RegisterStateARM64> RegisterStateARM64Ptr;
125 class RegisterStateARM64 : public BaseSemantics::RegisterState {
127 RegisterStateARM64(const BaseSemantics::SValuePtr &protoval,
128 const RegisterDictionary *regdict) : RegisterState(protoval, regdict) { }
131 static RegisterStateARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
132 const RegisterDictionary *regdict) {
133 return RegisterStateARM64Ptr(new RegisterStateARM64(protoval, regdict));
136 virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval,
137 const RegisterDictionary *regdict) const {
138 return instance(protoval, regdict);
141 virtual BaseSemantics::RegisterStatePtr clone() const {
142 ASSERT_not_implemented("RegisterState::clone() should not be called with Dyninst's SymEval policy");
145 static RegisterStateARM64Ptr promote(const BaseSemantics::RegisterStatePtr &from) {
146 RegisterStateARM64Ptr retval = boost::dynamic_pointer_cast<RegisterStateARM64>(from);
147 ASSERT_not_null(retval);
152 virtual void clear() {
153 ASSERT_not_implemented("RegisterState::clear() should not be called with Dyninst's SymEval policy");
156 virtual void zero() {
157 ASSERT_not_implemented("RegisterState::zero() should not be called with Dyninst's SymEval policy");
160 virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
161 virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
163 virtual void print(std::ostream &, BaseSemantics::Formatter &) const {}
165 virtual bool merge(const BaseSemantics::RegisterStatePtr &other, BaseSemantics::RiscOperators *ops) {
169 BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, Dyninst::Address addr);
170 void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value,
171 Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
174 Dyninst::AST::Ptr wrap(Dyninst::Absloc r, Dyninst::Address addr) {
175 return Dyninst::DataflowAPI::VariableAST::create(Dyninst::DataflowAPI::Variable(Dyninst::AbsRegion(r), addr));
178 Dyninst::Absloc convert(const RegisterDescriptor ®);
182 /***************************************************************************************************/
184 /***************************************************************************************************/
186 typedef boost::shared_ptr<class MemoryStateARM64> MemoryStateARM64Ptr;
188 class MemoryStateARM64 : public BaseSemantics::MemoryState {
190 MemoryStateARM64(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval):
191 BaseSemantics::MemoryState(addrProtoval, valProtoval) { }
194 static MemoryStateARM64Ptr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
195 return MemoryStateARM64Ptr(new MemoryStateARM64(addrProtoval, valProtoval));
198 virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const {
199 return instance(addrProtoval, valProtoval);
202 static MemoryStateARM64Ptr promote(const BaseSemantics::MemoryStatePtr &from) {
203 MemoryStateARM64Ptr retval = boost::dynamic_pointer_cast<MemoryStateARM64>(from);
204 ASSERT_not_null(retval);
209 virtual BaseSemantics::MemoryStatePtr clone() const {
210 ASSERT_not_implemented("MemoryState::clone() should not be called with Dyninst's SymEval policy");
213 virtual void clear() {
214 ASSERT_not_implemented("MemoryState::clear() should not be called with Dyninst's SymEval policy");
217 virtual void print(std::ostream&, BaseSemantics::Formatter&) const {
221 virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) {
226 virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
227 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
229 BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, size_t readSize);
231 virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
232 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
234 void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
235 Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap, size_t writeSize);
239 /***************************************************************************************************/
241 /***************************************************************************************************/
243 typedef boost::shared_ptr<class StateARM64> StateARM64Ptr;
245 class StateARM64 : public BaseSemantics::State {
247 StateARM64(Dyninst::DataflowAPI::Result_t &r,
249 Dyninst::Architecture ac,
250 Dyninst::InstructionAPI::Instruction::Ptr insn_,
251 const BaseSemantics::RegisterStatePtr ®isters,
252 const BaseSemantics::MemoryStatePtr &memory): BaseSemantics::State(registers, memory), res(r), addr(a), arch(ac), insn(insn_) {
253 for (Dyninst::DataflowAPI::Result_t::iterator iter = r.begin();
254 iter != r.end(); ++iter) {
255 Dyninst::Assignment::Ptr a = iter->first;
256 // For a different instruction...
257 if (a->addr() != addr)
259 Dyninst::AbsRegion &o = a->out();
261 if (o.containsOfType(Dyninst::Absloc::Register)) {
262 // We're assuming this is a single register...
263 //std::cerr << "Marking register " << a << std::endl;
264 aaMap[o.absloc()] = a;
267 // Use sufficiently-unique (Heap,0) Absloc
268 // to represent a definition to a memory absloc
269 aaMap[Dyninst::Absloc(0)] = a;
275 static StateARM64Ptr instance(Dyninst::DataflowAPI::Result_t &r,
277 Dyninst::Architecture ac,
278 Dyninst::InstructionAPI::Instruction::Ptr insn_,
279 const BaseSemantics::RegisterStatePtr ®isters,
280 const BaseSemantics::MemoryStatePtr &memory) {
281 return StateARM64Ptr(new StateARM64(r, a, ac, insn_, registers, memory));
284 virtual BaseSemantics::StatePtr create(Dyninst::DataflowAPI::Result_t &r,
286 Dyninst::Architecture ac,
287 Dyninst::InstructionAPI::Instruction::Ptr insn_,
288 const BaseSemantics::RegisterStatePtr ®isters,
289 const BaseSemantics::MemoryStatePtr &memory) const {
290 return instance(r, a, ac, insn_, registers, memory);
293 static StateARM64Ptr promote(const BaseSemantics::StatePtr &from) {
294 StateARM64Ptr retval = boost::dynamic_pointer_cast<StateARM64>(from);
295 ASSERT_not_null(retval);
300 virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
301 virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
302 virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
303 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, size_t readSize = 0);
304 virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps,
305 BaseSemantics::RiscOperators *valOps, size_t writeSize = 0);
308 Dyninst::DataflowAPI::Result_t &res;
309 Dyninst::Architecture arch;
310 Dyninst::Address addr;
311 Dyninst::InstructionAPI::Instruction::Ptr insn;
313 std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> aaMap;
317 /***************************************************************************************************/
319 /***************************************************************************************************/
320 typedef boost::shared_ptr<class RiscOperatorsARM64> RiscOperatorsARM64Ptr;
322 /** RISC operators for use by the Symbolic Semantics Domain of Dyninst.
325 class RiscOperatorsARM64 : public BaseSemantics::RiscOperators {
327 RiscOperatorsARM64(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver = NULL)
328 : BaseSemantics::RiscOperators(protoval, solver) {
329 (void)SValue::promote(protoval);
332 RiscOperatorsARM64(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL)
333 : BaseSemantics::RiscOperators(state, solver) {
334 (void)SValue::promote(state->protoval());
338 static RiscOperatorsARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
339 SMTSolver *solver = NULL) {
340 return RiscOperatorsARM64Ptr(new RiscOperatorsARM64(protoval, solver));
343 static RiscOperatorsARM64Ptr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL) {
344 return RiscOperatorsARM64Ptr(new RiscOperatorsARM64(state, solver));
348 virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
349 SMTSolver *solver = NULL) const {
350 return instance(protoval, solver);
353 virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
354 SMTSolver *solver = NULL) const {
355 return instance(state, solver);
359 /** Run-time promotion of a base RiscOperators pointer to symbolic operators. This is a checked conversion--it
360 * will fail if @p x does not point to a SymbolicSemantics::RiscOperators object. */
361 static RiscOperatorsARM64Ptr promote(const BaseSemantics::RiscOperatorsPtr &x) {
362 RiscOperatorsARM64Ptr retval = boost::dynamic_pointer_cast<RiscOperatorsARM64>(x);
363 ASSERT_not_null(retval);
368 virtual BaseSemantics::SValuePtr boolean_(bool b) {
369 SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
373 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) {
374 SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
379 virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
380 const BaseSemantics::SValuePtr &b_);
381 virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
382 const BaseSemantics::SValuePtr &b_);
383 virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
384 const BaseSemantics::SValuePtr &b_);
385 virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_);
386 virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
387 uint64_t begin, uint64_t end);
388 virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
389 const BaseSemantics::SValuePtr &a_,
390 const BaseSemantics::SValuePtr &b_);
391 virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
392 const BaseSemantics::SValuePtr &b_);
393 virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_);
394 virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_);
395 virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
396 const BaseSemantics::SValuePtr &b_);
397 virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
398 const BaseSemantics::SValuePtr &b_);
399 virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
400 const BaseSemantics::SValuePtr &b_);
401 virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
402 const BaseSemantics::SValuePtr &b_);
403 virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
404 const BaseSemantics::SValuePtr &b_);
405 virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_);
406 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_,
407 uint64_t newwidth = 0);
408 virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
409 const BaseSemantics::SValuePtr &b_);
410 virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
411 const BaseSemantics::SValuePtr &b_,
412 const BaseSemantics::SValuePtr &c_,
413 BaseSemantics::SValuePtr &carry_out);
414 virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_);
415 virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
416 const BaseSemantics::SValuePtr &b_);
417 virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
418 const BaseSemantics::SValuePtr &b_);
419 virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
420 const BaseSemantics::SValuePtr &b_);
421 virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
422 const BaseSemantics::SValuePtr &b_);
423 virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
424 const BaseSemantics::SValuePtr &b_);
425 virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
426 const BaseSemantics::SValuePtr &b_);
429 virtual BaseSemantics::SValuePtr readMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt,
430 const BaseSemantics::SValuePtr &cond);
431 virtual void writeMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data,
432 const BaseSemantics::SValuePtr &cond);
435 Dyninst::AST::Ptr getUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
438 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a);
441 Dyninst::AST::Ptr getBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
445 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b);
448 Dyninst::AST::Ptr getTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
453 return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b, c);
456 SValuePtr createUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_) {
457 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
458 Dyninst::AST::Ptr ast = getUnaryAST(op, a);
459 return SValue::instance(ast);
462 SValuePtr createBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) {
463 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
464 Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
465 Dyninst::AST::Ptr ast = getBinaryAST(op, a, b);
466 return SValue::instance(ast);
469 SValuePtr createTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_,
470 const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, size_t s = 0) {
471 Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
472 Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
473 Dyninst::AST::Ptr c = SValue::promote(c_)->get_expression();
474 Dyninst::AST::Ptr ast = getTernaryAST(op, a, b, c, s);
475 return SValue::instance(ast);
484 #endif //DYNINST_SYMEVALSEMANTICS_H