Class declarations for SymEvalSemantics
[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 "BaseSemantics2.h"
9 #include "../../h/SymEval.h"
10
11 namespace rose {
12     namespace BinaryAnalysis {
13         namespace InstructionSemantics2 {
14             namespace SymEvalSemantics {
15
16                 /***************************************************************************************************/
17                 /*                                              SValue                                             */
18                 /***************************************************************************************************/
19                 typedef Sawyer::SharedPointer<class SValue> SValuePtr;
20
21                 class SValue : public BaseSemantics::SValue {
22                 protected:
23                     Dyninst::AST::Ptr expr;
24
25                     SValue(Dyninst::Absloc r, Dyninst::ParseAPI::Address addr): BaseSemantics::SValue(0) {
26                         //FIXME
27                     }
28
29                     SValue(size_t nbits, uint64_t num): BaseSemantics::SValue(nbits) {
30                         expr = Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(num, nbits));
31                     }
32
33                     //FIXME
34                     SValue(Dyninst::AST::Ptr expr): BaseSemantics::SValue(0) {
35                         this->expr = expr;
36                     }
37
38                 public:
39                     virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const {
40                         return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(false)));
41                     }
42
43                     virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const {
44                         //FIXME
45                     }
46
47                     //TODO
48                     virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const {
49                         return SValuePtr(new SValue(Dyninst::DataflowAPI::BottomAST::create(true)));
50                     }
51
52                     virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t num) const {
53                         return SValuePtr(new SValue(nbits, num));
54                     }
55
56                     virtual BaseSemantics::SValuePtr boolean_(bool value) const {
57                         return SValuePtr(new SValue(Dyninst::DataflowAPI::ConstantAST::create(Dyninst::DataflowAPI::Constant(value?1:0, 1))));
58                     }
59
60                     virtual BaseSemantics::SValuePtr copy(size_t new_width = 0) const {
61                         SValuePtr retval(new SValue(*this));
62                         if (new_width!=0 && new_width!=retval->get_width())
63                             retval->set_width(new_width);
64                         return retval;
65                     }
66
67                     virtual Sawyer::Optional<BaseSemantics::SValuePtr>
68                             createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&, SMTSolver*) const;
69
70                 public:
71                     static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
72                         SValuePtr retval = v.dynamicCast<SValue>();
73                         ASSERT_not_null(retval);
74                         return retval;
75                     }
76
77                 public:
78                     //TODO
79                     virtual bool isBottom() const {
80                         return expr->getID() == Dyninst::DataflowAPI::V_BottomAST;
81                     }
82
83                     virtual bool is_number() const {
84                         return expr->getID() == Dyninst::DataflowAPI::V_ConstantAST;
85                     }
86
87                     virtual uint64_t get_number() const {
88                         assert(expr->getID() == Dyninst::DataflowAPI::V_ConstantAST);
89                         Dyninst::DataflowAPI::Constant constant = expr->val();
90                         ASSERT_not_null(constant);
91                         return constant.val;
92                     }
93
94                     virtual void print(std::ostream &, BaseSemantics::Formatter &) const {
95                         //TODO
96                     }
97
98                 };
99
100
101                 class RegisterState : public BaseSemantics::RegisterState {
102
103                 };
104
105
106                 class MemoryState : public BaseSemantics::MemoryState {
107
108                 };
109
110
111                 /***************************************************************************************************/
112                 /*                                          RiscOperators                                          */
113                 /***************************************************************************************************/
114                 typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
115
116                 /** RISC operators for use by the Symbolic Semantics Domain of Dyninst.
117                  *
118                  */
119                 class RiscOperators : public BaseSemantics::RiscOperators {
120                 protected:
121                     explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, SMTSolver *solver = NULL)
122                             : BaseSemantics::RiscOperators(protoval, solver) {
123                         //SValue::promote(protoval);
124                     }
125
126                     explicit RiscOperators(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL)
127                             : BaseSemantics::RiscOperators(state, solver) {
128                         //SValue::promote(state->protoval());
129                     }
130
131                 public:
132                     static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SMTSolver *solver = NULL) {
133                         //init SValue
134                         //init RegisterState
135                         //init MemoryState
136                         //init State
137                         //return new RiscOperatorsPtr(new RiscOperators(state, solver));
138                     }
139
140                     static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval,
141                                                      SMTSolver *solver = NULL) {
142                         return RiscOperatorsPtr(new RiscOperators(protoval, solver));
143                     }
144
145                     static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, SMTSolver *solver = NULL) {
146                         return RiscOperatorsPtr(new RiscOperators(state, solver));
147                     }
148
149                 public:
150                     virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
151                                                                    SMTSolver *solver = NULL) {
152                         return instance(protoval, solver);
153                     }
154
155                     virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
156                                                                    SMTSolver *solver = NULL) {
157                         return instance(state, solver);
158                     }
159
160                 public:
161                     /** Run-time promotion of a base RiscOperators pointer to symbolic operators. This is a checked conversion--it
162                     *  will fail if @p x does not point to a SymbolicSemantics::RiscOperators object. */
163                     static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
164                         RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperatorsPtr>(x);
165                         ASSERT_not_null(retval);
166
167                         return retval;
168                     }
169
170                 public:
171                     virtual BaseSemantics::SValuePtr boolean_(bool b) {
172                         SValuePtr retVal = SValue::promote(BaseSemantics::RiscOperators::boolean_(b));
173                         return retval;
174                     }
175
176                     virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) {
177                         SValuePtr retval = SValue::promote(BaseSemantics::RiscOperators::number_(nbits, value));
178                         return retval;
179                     }
180
181                 public:
182                     virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
183                                                           const BaseSemantics::SValuePtr &b_);
184                     virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
185                                                           const BaseSemantics::SValuePtr &b_);
186                     virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
187                                                           const BaseSemantics::SValuePtr &b_);
188                     virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_);
189                     virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
190                                                              size_t begin, size_t end);
191                     virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
192                                                          const BaseSemantics::SValuePtr &a_,
193                                                          const BaseSemantics::SValuePtr &b_);
194
195                     virtual BaseSemantics::SValuePtr readRegister(const RegisterDescriptor &reg,
196                                                                   const BaseSemantics::SValuePtr &dflt);
197                     virtual void writeRegister(const RegisterDescriptor &reg, const BaseSemantics::SValuePtr &a_);
198                 };
199             }
200         }
201     }
202 }
203
204 #endif //DYNINST_SYMEVALSEMANTICS_H