Definitions of the register state, memory state and value type for SymEval semantics...
[dyninst.git] / dataflowAPI / rose / semantics / SymEvalSemantics.h
1 //
2 // Created by ssunny on 7/1/16.
3 //
4
5 #ifndef DYNINST_SYMEVALSEMANTICS_H
6 #define DYNINST_SYMEVALSEMANTICS_H
7
8 #include "external/rose/armv8InstructionEnum.h"
9 #include "BaseSemantics2.h"
10 #include "../../h/SymEval.h"
11
12 namespace rose {
13     namespace BinaryAnalysis {
14         namespace InstructionSemantics2 {
15             namespace SymEvalSemantics {
16
17                 /***************************************************************************************************/
18                 /*                                              SValue                                             */
19                 /***************************************************************************************************/
20                 typedef Sawyer::SharedPointer<class SValue> SValuePtr;
21
22                 class SValue : public BaseSemantics::SValue {
23                 protected:
24                     Dyninst::AST::Ptr expr;
25
26                     SValue(Dyninst::Absloc r, Dyninst::Address addr): BaseSemantics::SValue(64) {
27                         expr = Dyninst::DataflowAPI::VariableAST::create(Variable(Dyninst::AbsRegion(r), addr));
28                     }
29
30                     SValue(size_t nbits, uint64_t num): BaseSemantics::SValue(nbits) {
31                         expr = Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(num, nbits));
32                     }
33
34                     SValue(Dyninst::AST::Ptr expr): BaseSemantics::SValue(64) {
35                         this->expr = expr;
36                     }
37
38                 public:
39                     static SValuePtr instance(Dyninst::Absloc r, Dyninst::Address addr) {
40                         return SValuePtr(new SValue(r, addr));
41                     }
42
43                     static SValuePtr instance(size_t nbits, uint64_t num) {
44                         return SValuePtr(new SValue(nbits, num));
45                     }
46
47                     static SValuePtr instance(Dyninst::AST::Ptr expr) {
48                         return SValuePtr(new SValue(expr));
49                     }
50
51                 public:
52                     virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const {
53                         return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
54                     }
55
56                     virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const {
57                         return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
58                     }
59
60                     //TODO
61                     virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const {
62                         return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(true)));
63                     }
64
65                     virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t num) const {
66                         return SValuePtr(new SValue(nbits, num));
67                     }
68
69                     virtual BaseSemantics::SValuePtr boolean_(bool value) const {
70                         return SValuePtr(new SValue(Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(value?1:0, 1))));
71                     }
72
73                     virtual BaseSemantics::SValuePtr copy(size_t new_width = 0) const {
74                         SValuePtr retval(new SValue(this->get_expression()));
75                         if (new_width!=0 && new_width!=retval->get_width())
76                             retval->set_width(new_width);
77                         return retval;
78                     }
79
80                     virtual Sawyer::Optional<BaseSemantics::SValuePtr>
81                             createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const;
82
83                 public:
84                     static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
85                         SValuePtr retval = v.dynamicCast<SValue>();
86                         ASSERT_not_null(retval);
87                         return retval;
88                     }
89
90                 public:
91                     virtual Dyninst::AST::Ptr get_expression() {
92                         return expr;
93                     }
94
95                     virtual bool isBottom() const {
96                         return expr->getID() == Dyninst::DataflowAPI::V_BottomAST;
97                     }
98
99                     virtual bool is_number() const {
100                         return expr->getID() == Dyninst::DataflowAPI::V_ConstantAST;
101                     }
102
103                     virtual uint64_t get_number() const {
104                         assert(expr->getID() == Dyninst::DataflowAPI::V_ConstantAST);
105                         Dyninst::DataflowAPI::Constant constant = expr->val();
106                         ASSERT_not_null(constant);
107                         return constant.val;
108                     }
109
110                     virtual void print(std::ostream &, BaseSemantics::Formatter &) const { }
111
112                 };
113
114
115                 /***************************************************************************************************/
116                 /*                                          Register State                                         */
117                 /***************************************************************************************************/
118
119                 typedef boost::shared_ptr<class RegisterStateARM64> RegisterStateARM64Ptr;
120
121                 class RegisterStateARM64 : public BaseSemantics::RegisterState {
122                 public:
123                     RegisterStateARM64(const BaseSemantics::SValuePtr &protoval,
124                                        const RegisterDictionary *regdict) : RegisterState(protoval, regdict) { }
125
126                 public:
127                     static RegisterStateARM64Ptr instance(const BaseSemantics::SValuePtr &protoval,
128                                                           const RegisterDictionary *regdict) {
129                         return RegisterStateARM64Ptr(new RegisterStateARM64(protoval, regdict));
130                     }
131
132                     virtual BaseSemantics::RegisterStatePtr create(const BaseSemantics::SValuePtr &protoval,
133                                                                    const RegisterDictionary *regdict) const {
134                         return instance(protoval, regdict);
135                     }
136
137                     virtual BaseSemantics::RegisterStatePtr clone() const {
138                         ASSERT_not_implemented("RegisterState::clone() should not be called with Dyninst's SymEval policy");
139                     }
140
141                     static RegisterStateARM64Ptr promote(const BaseSemantics::RegisterStatePtr &from) {
142                         RegisterStateARM64Ptr retval = boost::dynamic_pointer_cast<RegisterStateARM64>(from);
143                         ASSERT_not_null(retval);
144                         return retval;
145                     }
146
147                 public:
148                     virtual void clear() {
149                         ASSERT_not_implemented("RegisterState::clear() should not be called with Dyninst's SymEval policy");
150                     }
151
152                     virtual void zero() {
153                         ASSERT_not_implemented("RegisterState::zero() should not be called with Dyninst's SymEval policy");
154                     }
155
156                     virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor &reg, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *ops);
157                     virtual void writeRegister(const RegisterDescriptor &reg, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
158
159                     virtual void print(std::ostream &, BaseSemantics::Formatter &) const {}
160
161                     virtual bool merge(const RegisterDescriptor &other, BaseSemantics::RiscOperators *ops) {
162                         return true;
163                     }
164
165                     void writeRegister(const RegisterDescriptor &reg, const BaseSematics::SValuePtr &value,
166                                        Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
167
168                 private:
169                     Dyninst::AST::Ptr wrap(Dyninst::Absloc r) {
170                         return Dyninst::DataflowAPI::VariableAST::create(Dyninst::DataflowAPI::Variable(Dyninst::AbsRegion(r), addr));
171                     }
172
173                     Dyninst::Absloc convert(ARMv8GeneralPurposeRegister r, unsigned int size);
174                 };
175
176
177                 /***************************************************************************************************/
178                 /*                                           Memory State                                          */
179                 /***************************************************************************************************/
180
181                 typedef boost::shared_ptr<class MemoryStateARM64> MemoryStateARM64Ptr;
182
183                 class MemoryStateARM64 : public BaseSemantics::MemoryState {
184                 protected:
185                     MemoryStateARM64(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval):
186                             BaseSemantics::MemoryState(addrProtoval, valProtoval) { }
187
188                 public:
189                     static MemoryStateARM64Ptr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) {
190                         return MemoryStateARM64Ptr(new MemoryStateARM64(addrProtoval, valProtoval));
191                     }
192
193                     virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const {
194                         return instance(addrProtoval, valProtoval);
195                     }
196
197                     static MemoryStateARM64Ptr promote(const BaseSemantics::MemoryStatePtr &from) {
198                         MemoryStateARM64Ptr retval = boost::dynamic_pointer_cast<MemoryStateARM64>(from);
199                         ASSERT_not_null(retval);
200                         return retval;
201                     }
202
203                 public:
204                     virtual BaseSemantics::MemoryStatePtr clone() const {
205                         ASSERT_not_implemented("MemoryState::clone() should not be called with Dyninst's SymEval policy");
206                     }
207
208                     virtual void clear() {
209                         ASSERT_not_implemented("MemoryState::clear() should not be called with Dyninst's SymEval policy");
210                     }
211
212                     virtual bool merge(const BaseSemantics::MemoryStatePtr &other, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) {
213                         return true;
214                     }
215
216                 public:
217                     virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &address, const BaseSemantics::SValuePtr &dflt,
218                                                                 BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
219
220                     virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value,
221                                              BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps);
222
223                     void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSematics::SValuePtr &value,
224                                        Dyninst::DataflowAPI::Result_t &res, std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> &aaMap);
225                 };
226
227
228                 /***************************************************************************************************/
229                 /*                                                State                                            */
230                 /***************************************************************************************************/
231
232                 typedef boost::shared_ptr<class StateARM64> StateARM64Ptr;
233
234                 class StateARM64 : public BaseSemantics::State {
235                 public:
236                     StateARM64(Dyninst::DataflowAPI::Result_t &r,
237                                Dyninst::Address a,
238                                Dyninst::Architecture ac,
239                                Dyninst::InstructionAPI::Instruction::Ptr insn_,
240                                const BaseSemantics::RegisterStatePtr &registers,
241                                const BaseSemantics::MemoryStatePtr &memory): BaseSemantics::State(registers, memory) {
242                         for (Dyninst::DataflowAPI::Result_t::iterator iter = r.begin();
243                              iter != r.end(); ++iter) {
244                             Dyninst::Assignment::Ptr a = iter->first;
245                             // For a different instruction...
246                             if (a->addr() != addr)
247                                 continue;
248                             Dyninst::AbsRegion &o = a->out();
249
250                             if (o.containsOfType(Dyninst::Absloc::Register)) {
251                                 // We're assuming this is a single register...
252                                 //std::cerr << "Marking register " << a << std::endl;
253                                 aaMap[o.absloc()] = a;
254                             }
255                             else {
256                                 // Use sufficiently-unique (Heap,0) Absloc
257                                 // to represent a definition to a memory absloc
258                                 aaMap[Absloc(0)] = a;
259                             }
260                         }
261                     }
262
263                 public:
264                     static StateARM64Ptr instance(Dyninst::DataflowAPI::Result_t &r,
265                                                   Dyninst::Address a,
266                                                   Dyninst::Architecture ac,
267                                                   Dyninst::InstructionAPI::Instruction::Ptr insn_,
268                                                   const BaseSemantics::RegisterStatePtr &registers,
269                                                   const BaseSemantics::MemoryStatePtr &memory) {
270                         return StateARM64Ptr(new StateARM64(r, a, ac, insn_, registers, memory));
271                     }
272
273                     virtual BaseSemantics::StatePtr create(Dyninst::DataflowAPI::Result_t &r,
274                                                  Dyninst::Address a,
275                                                  Dyninst::Architecture ac,
276                                                  Dyninst::InstructionAPI::Instruction::Ptr insn_,
277                                                  const BaseSemantics::RegisterStatePtr &registers,
278                                                  const BaseSemantics::MemoryStatePtr &memory) const {
279                         return instance(r, a, ac, insn_, registers, memory);
280                     }
281
282                     static StateARM64Ptr promote(const BaseSemantics::StatePtr &from) {
283                         StateARM64Ptr retval = boost::dynamic_pointer_cast<StateARM64>(from);
284                         ASSERT_not_null(retval);
285                         return retval;
286                     }
287
288                 public:
289                     virtual void writeRegister(const RegisterDescriptor &reg, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *ops);
290                     virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps,
291                                              BaseSemantics::RiscOperators *valOps);
292
293                 protected:
294                     Dyninst::DataflowAPI::Result_t &res;
295                     Dyninst::Architecture arch;
296                     Dyninst::Address addr;
297                     Dyninst::InstructionAPI::Instruction::Ptr insn;
298
299                     std::map<Dyninst::Absloc, Dyninst::Assignment::Ptr> aaMap;
300                 };
301
302
303                 /***************************************************************************************************/
304                 /*                                          RiscOperators                                          */
305                 /***************************************************************************************************/
306                 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
307
308                 /** RISC operators for use by the Symbolic Semantics Domain of Dyninst.
309                  *
310                  */
311                 class RiscOperators : public BaseSemantics::RiscOperators {
312                 protected:
313                     RiscOperators(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver = NULL)
314                             : BaseSemantics::RiscOperators(protoval, solver) {
315                         (void)SValue::promote(protoval);
316                     }
317
318                     RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL)
319                             : BaseSemantics::RiscOperators(state, solver) {
320                         (void)SValue::promote(state->protoval());
321                     }
322
323                 public:
324                     static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval,
325                                                      SMTSolver *solver = NULL) {
326                         return RiscOperatorsPtr(new RiscOperators(protoval, solver));
327                     }
328
329                     static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL) {
330                         return RiscOperatorsPtr(new RiscOperators(state, solver));
331                     }
332
333                 public:
334                     virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
335                                                                    SMTSolver *solver = NULL) {
336                         return instance(protoval, solver);
337                     }
338
339                     virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
340                                                                    SMTSolver *solver = NULL) {
341                         return instance(state, solver);
342                     }
343
344                 public:
345                     /** Run-time promotion of a base RiscOperators pointer to symbolic operators. This is a checked conversion--it
346                     *  will fail if @p x does not point to a SymbolicSemantics::RiscOperators object. */
347                     static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
348                         RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
349                         ASSERT_not_null(retval);
350                         return retval;
351                     }
352
353                 public:
354                     virtual BaseSemantics::SValuePtr boolean_(bool b) {
355                         SValuePtr retVal = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
356                         return retval;
357                     }
358
359                     virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) {
360                         SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
361                         return retval;
362                     }
363
364                 public:
365                     virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
366                                                           const BaseSemantics::SValuePtr &b_);
367                     virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
368                                                           const BaseSemantics::SValuePtr &b_);
369                     virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
370                                                           const BaseSemantics::SValuePtr &b_);
371                     virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_);
372                     virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
373                                                              size_t begin, size_t end);
374                     virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
375                                                          const BaseSemantics::SValuePtr &a_,
376                                                          const BaseSemantics::SValuePtr &b_);
377
378                     virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor &reg,
379                                                                   const BaseSemantics::SValuePtr &dflt);
380                     virtual void writeRegister(const RegisterDescriptor &reg, const BaseSemantics::SValuePtr &a_);
381                 };
382             }
383         }
384     }
385 }
386
387 #endif //DYNINST_SYMEVALSEMANTICS_H