-
Notifications
You must be signed in to change notification settings - Fork 149
/
SymEvalSemantics.h
484 lines (395 loc) · 28.2 KB
/
SymEvalSemantics.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
//
// Created by ssunny on 7/1/16.
//
#ifndef DYNINST_SYMEVALSEMANTICS_H
#define DYNINST_SYMEVALSEMANTICS_H
#include "external/rose/armv8InstructionEnum.h"
#include "BaseSemantics2.h"
#include "../../h/SymEval.h"
namespace rose {
namespace BinaryAnalysis {
namespace InstructionSemantics2 {
namespace SymEvalSemantics {
/***************************************************************************************************/
/* SValue */
/***************************************************************************************************/
typedef Sawyer::SharedPointer<class SValue> SValuePtr;
class SValue : public BaseSemantics::SValue {
protected:
Dyninst::AST::Ptr expr;
SValue(Dyninst::Absloc r, Dyninst::Address addr): BaseSemantics::SValue(64) {
expr = Dyninst::DataflowAPI::VariableAST::create(Dyninst::DataflowAPI::Variable(Dyninst::AbsRegion(r), addr));
}
SValue(size_t nbits, uint64_t num): BaseSemantics::SValue(nbits) {
expr = Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(num, nbits));
}
//TODO possibly set width differently for register types
SValue(Dyninst::AST::Ptr expr): BaseSemantics::SValue(64) {
this->expr = expr;
}
public:
static SValuePtr instance(Dyninst::Absloc r, Dyninst::Address addr) {
return SValuePtr(new SValue(r, addr));
}
static SValuePtr instance(size_t nbits, uint64_t num) {
return SValuePtr(new SValue(nbits, num));
}
static SValuePtr instance(Dyninst::AST::Ptr expr) {
return SValuePtr(new SValue(expr));
}
public:
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const {
return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
}
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const {
return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
}
//TODO
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const {
return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(true)));
}
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t num) const {
return SValuePtr(new SValue(nbits, num));
}
virtual BaseSemantics::SValuePtr boolean_(bool value) const {
return SValuePtr(new SValue(1, value?1:0));
}
virtual BaseSemantics::SValuePtr copy(size_t new_width = 0) const {
SValuePtr retval(new SValue(get_expression()));
if (new_width!=0 && new_width!=retval->get_width())
retval->set_width(new_width);
return retval;
}
virtual Sawyer::Optional<BaseSemantics::SValuePtr>
createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const {
ASSERT_not_implemented("SValue::createOptionalMerge not implemented for use in dyninst");
}
public:
static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
SValuePtr retval = v.dynamicCast<SValue>();
ASSERT_not_null(retval);
return retval;
}
public:
virtual Dyninst::AST::Ptr get_expression() const {
return expr;
}
virtual bool isBottom() const {
return expr->getID() == Dyninst::AST::V_BottomAST;
}
virtual bool is_number() const {
return expr->getID() == Dyninst::AST::V_ConstantAST;
}
virtual uint64_t get_number() const {
assert(expr->getID() == Dyninst::AST::V_ConstantAST);
//TODO
Dyninst::DataflowAPI::Constant constant = boost::dynamic_pointer_cast<Dyninst::DataflowAPI::ConstantAST>(expr)->val();
return constant.val;
}
virtual void print(std::ostream &, BaseSemantics::Formatter &) const { }
};
/***************************************************************************************************/
/* Register State */
/***************************************************************************************************/
typedef boost::shared_ptr<class RegisterStateARM64> RegisterStateARM64Ptr;
class RegisterStateARM64 : public BaseSemantics::RegisterState {
public:
RegisterStateARM64(const BaseSemantics::SValuePtr &protoval,
const RegisterDictionary *regdict) : RegisterState(protoval, regdict) { }
public:
static RegisterStateARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
const RegisterDictionary *regdict) {
return RegisterStateARM64Ptr(new RegisterStateARM64(protoval, regdict));
}
virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval,
const RegisterDictionary *regdict) const {
return instance(protoval, regdict);
}
virtual BaseSemantics::RegisterStatePtr clone() const {
ASSERT_not_implemented("RegisterState::clone() should not be called with Dyninst's SymEval policy");
}
static RegisterStateARM64Ptr promote(const BaseSemantics::RegisterStatePtr &from) {
RegisterStateARM64Ptr retval = boost::dynamic_pointer_cast<RegisterStateARM64>(from);
ASSERT_not_null(retval);
return retval;
}
public:
virtual void clear() {
ASSERT_not_implemented("RegisterState::clear() should not be called with Dyninst's SymEval policy");
}
virtual void zero() {
ASSERT_not_implemented("RegisterState::zero() should not be called with Dyninst's SymEval policy");
}
virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
virtual void print(std::ostream &, BaseSemantics::Formatter &) const {}
virtual bool merge(const BaseSemantics::RegisterStatePtr &other, BaseSemantics::RiscOperators *ops) {
return true;
}
BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, Dyninst::Address addr);
void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value,
Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
private:
Dyninst::AST::Ptr wrap(Dyninst::Absloc r, Dyninst::Address addr) {
return Dyninst::DataflowAPI::VariableAST::create(Dyninst::DataflowAPI::Variable(Dyninst::AbsRegion(r), addr));
}
Dyninst::Absloc convert(const RegisterDescriptor ®);
};
/***************************************************************************************************/
/* Memory State */
/***************************************************************************************************/
typedef boost::shared_ptr<class MemoryStateARM64> MemoryStateARM64Ptr;
class MemoryStateARM64 : public BaseSemantics::MemoryState {
protected:
MemoryStateARM64(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval):
BaseSemantics::MemoryState(addrProtoval, valProtoval) { }
public:
static MemoryStateARM64Ptr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
return MemoryStateARM64Ptr(new MemoryStateARM64(addrProtoval, valProtoval));
}
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const {
return instance(addrProtoval, valProtoval);
}
static MemoryStateARM64Ptr promote(const BaseSemantics::MemoryStatePtr &from) {
MemoryStateARM64Ptr retval = boost::dynamic_pointer_cast<MemoryStateARM64>(from);
ASSERT_not_null(retval);
return retval;
}
public:
virtual BaseSemantics::MemoryStatePtr clone() const {
ASSERT_not_implemented("MemoryState::clone() should not be called with Dyninst's SymEval policy");
}
virtual void clear() {
ASSERT_not_implemented("MemoryState::clear() should not be called with Dyninst's SymEval policy");
}
virtual void print(std::ostream&, BaseSemantics::Formatter&) const {
//
}
virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) {
return true;
}
public:
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, size_t readSize);
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap, size_t writeSize);
};
/***************************************************************************************************/
/* State */
/***************************************************************************************************/
typedef boost::shared_ptr<class StateARM64> StateARM64Ptr;
class StateARM64 : public BaseSemantics::State {
public:
StateARM64(Dyninst::DataflowAPI::Result_t &r,
Dyninst::Address a,
Dyninst::Architecture ac,
Dyninst::InstructionAPI::Instruction::Ptr insn_,
const BaseSemantics::RegisterStatePtr ®isters,
const BaseSemantics::MemoryStatePtr &memory): BaseSemantics::State(registers, memory), res(r), addr(a), arch(ac), insn(insn_) {
for (Dyninst::DataflowAPI::Result_t::iterator iter = r.begin();
iter != r.end(); ++iter) {
Dyninst::Assignment::Ptr a = iter->first;
// For a different instruction...
if (a->addr() != addr)
continue;
Dyninst::AbsRegion &o = a->out();
if (o.containsOfType(Dyninst::Absloc::Register)) {
// We're assuming this is a single register...
//std::cerr << "Marking register " << a << std::endl;
aaMap[o.absloc()] = a;
}
else {
// Use sufficiently-unique (Heap,0) Absloc
// to represent a definition to a memory absloc
aaMap[Dyninst::Absloc(0)] = a;
}
}
}
public:
static StateARM64Ptr instance(Dyninst::DataflowAPI::Result_t &r,
Dyninst::Address a,
Dyninst::Architecture ac,
Dyninst::InstructionAPI::Instruction::Ptr insn_,
const BaseSemantics::RegisterStatePtr ®isters,
const BaseSemantics::MemoryStatePtr &memory) {
return StateARM64Ptr(new StateARM64(r, a, ac, insn_, registers, memory));
}
virtual BaseSemantics::StatePtr create(Dyninst::DataflowAPI::Result_t &r,
Dyninst::Address a,
Dyninst::Architecture ac,
Dyninst::InstructionAPI::Instruction::Ptr insn_,
const BaseSemantics::RegisterStatePtr ®isters,
const BaseSemantics::MemoryStatePtr &memory) const {
return instance(r, a, ac, insn_, registers, memory);
}
static StateARM64Ptr promote(const BaseSemantics::StatePtr &from) {
StateARM64Ptr retval = boost::dynamic_pointer_cast<StateARM64>(from);
ASSERT_not_null(retval);
return retval;
}
public:
virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
virtual void writeRegister(const RegisterDescriptor ®, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, size_t readSize = 0);
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps,
BaseSemantics::RiscOperators *valOps, size_t writeSize = 0);
protected:
Dyninst::DataflowAPI::Result_t &res;
Dyninst::Architecture arch;
Dyninst::Address addr;
Dyninst::InstructionAPI::Instruction::Ptr insn;
std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> aaMap;
};
/***************************************************************************************************/
/* RiscOperators */
/***************************************************************************************************/
typedef boost::shared_ptr<class RiscOperatorsARM64> RiscOperatorsARM64Ptr;
/** RISC operators for use by the Symbolic Semantics Domain of Dyninst.
*
*/
class RiscOperatorsARM64 : public BaseSemantics::RiscOperators {
protected:
RiscOperatorsARM64(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver = NULL)
: BaseSemantics::RiscOperators(protoval, solver) {
(void)SValue::promote(protoval);
}
RiscOperatorsARM64(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL)
: BaseSemantics::RiscOperators(state, solver) {
(void)SValue::promote(state->protoval());
}
public:
static RiscOperatorsARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
SMTSolver *solver = NULL) {
return RiscOperatorsARM64Ptr(new RiscOperatorsARM64(protoval, solver));
}
static RiscOperatorsARM64Ptr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL) {
return RiscOperatorsARM64Ptr(new RiscOperatorsARM64(state, solver));
}
public:
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
SMTSolver *solver = NULL) const {
return instance(protoval, solver);
}
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
SMTSolver *solver = NULL) const {
return instance(state, solver);
}
public:
/** Run-time promotion of a base RiscOperators pointer to symbolic operators. This is a checked conversion--it
* will fail if @p x does not point to a SymbolicSemantics::RiscOperators object. */
static RiscOperatorsARM64Ptr promote(const BaseSemantics::RiscOperatorsPtr &x) {
RiscOperatorsARM64Ptr retval = boost::dynamic_pointer_cast<RiscOperatorsARM64>(x);
ASSERT_not_null(retval);
return retval;
}
public:
virtual BaseSemantics::SValuePtr boolean_(bool b) {
SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
return retval;
}
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) {
SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
return retval;
}
public:
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_);
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
size_t begin, size_t end);
virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_);
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_);
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_);
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_,
size_t newwidth = 0);
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_,
const BaseSemantics::SValuePtr &c_,
BaseSemantics::SValuePtr &carry_out);
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_);
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_);
public:
virtual BaseSemantics::SValuePtr readMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt,
const BaseSemantics::SValuePtr &cond);
virtual void writeMemory(const RegisterDescriptor &segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data,
const BaseSemantics::SValuePtr &cond);
private:
Dyninst::AST::Ptr getUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
Dyninst::AST::Ptr a,
size_t s = 0) {
return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a);
}
Dyninst::AST::Ptr getBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
Dyninst::AST::Ptr a,
Dyninst::AST::Ptr b,
size_t s = 0) {
return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b);
}
Dyninst::AST::Ptr getTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op,
Dyninst::AST::Ptr a,
Dyninst::AST::Ptr b,
Dyninst::AST::Ptr c,
size_t s = 0) {
return Dyninst::DataflowAPI::RoseAST::create(Dyninst::DataflowAPI::ROSEOperation(op, s), a, b, c);
}
SValuePtr createUnaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_) {
Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
Dyninst::AST::Ptr ast = getUnaryAST(op, a);
return SValue::instance(ast);
}
SValuePtr createBinaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) {
Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
Dyninst::AST::Ptr ast = getBinaryAST(op, a, b);
return SValue::instance(ast);
}
SValuePtr createTernaryAST(Dyninst::DataflowAPI::ROSEOperation::Op op, const BaseSemantics::SValuePtr &a_,
const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, size_t s = 0) {
Dyninst::AST::Ptr a = SValue::promote(a_)->get_expression();
Dyninst::AST::Ptr b = SValue::promote(b_)->get_expression();
Dyninst::AST::Ptr c = SValue::promote(c_)->get_expression();
Dyninst::AST::Ptr ast = getTernaryAST(op, a, b, c, s);
return SValue::instance(ast);
}
};
}
}
}
}
#endif //DYNINST_SYMEVALSEMANTICS_H