-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsymbolic_execution.v
222 lines (188 loc) · 7.96 KB
/
symbolic_execution.v
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
Require Import bbv.Word.
Require Import Nat.
Require Import Coq.NArith.NArith.
Require Import FORVES2.constants.
Import Constants.
Require Import FORVES2.program.
Import Program.
Require Import FORVES2.symbolic_state.
Import SymbolicState.
Require Import FORVES2.misc.
Import Misc.
Require Import FORVES2.stack_operation_instructions.
Import StackOpInstrs.
Require Import FORVES2.memory_ops_solvers.
Import MemoryOpsSolvers.
Require Import FORVES2.storage_ops_solvers.
Import StorageOpsSolvers.
Require Import FORVES2.constraints.
Import Constraints.
Require Import FORVES2.context.
Import Context.
Require Import List.
Import ListNotations.
Module SymbolicExecution.
Definition push_s (value : EVMWord) (ctx: ctx_t) :=
fun (sst : sstate) (ops: stack_op_instr_map) =>
let sstk := get_stack_sst sst in
match push (Val value) sstk with
| None => None
| Some sstk' => Some (set_stack_sst sst sstk')
end.
Definition metapush_s (cat value : N) :=
fun (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) =>
let sstk := get_stack_sst sst in
let sm : smap := get_smap_sst sst in
let v : smap_value := SymMETAPUSH cat value in
match add_to_smap sm v with
| pair key sm' =>
match push (FreshVar key) sstk with
| Some sstk' =>
let sst' := set_stack_sst sst sstk' in
let sst'' := set_smap_sst sst' sm' in
Some sst''
| None => None
end
end.
Definition pop_s (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sstk := get_stack_sst sst in
match pop sstk with
| None => None
| Some sstk' => Some (set_stack_sst sst sstk')
end.
Definition dup_s (k : nat) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sstk := get_stack_sst sst in
match dup k sstk with
| None => None
| Some sstk' => Some (set_stack_sst sst sstk')
end.
Definition swap_s (k : nat) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sstk := get_stack_sst sst in
match swap k sstk with
| None => None
| Some sstk' => Some (set_stack_sst sst sstk')
end.
Definition mload_s (mload_solver: mload_solver_type) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sm : smap := get_smap_sst sst in
let smem : smemory := get_memory_sst sst in
match get_stack_sst sst with
| soffset::sstk =>
(* let smv := SymMLOAD soffset smem in *)
let smv := mload_solver ctx soffset smem (get_smap_sst sst) ops in
match add_to_smap sm smv with
| pair key sm' =>
let sst' := set_stack_sst sst ((FreshVar key)::sstk) in
let sst'' := set_smap_sst sst' sm' in
Some sst''
end
| _ => None
end.
Definition sload_s (sload_solver: sload_solver_type) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sm : smap := get_smap_sst sst in
let sstrg : sstorage := get_storage_sst sst in
match get_stack_sst sst with
| skey::sstk =>
(* let smv := SymSLOAD skey sstrg in *)
let smv := sload_solver ctx skey sstrg (get_smap_sst sst) ops in
match add_to_smap sm smv with
| pair key sm' =>
let sst' := set_stack_sst sst ((FreshVar key)::sstk) in
let sst'' := set_smap_sst sst' sm' in
Some sst''
end
| _ => None
end.
Definition sha3_s (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
let sm : smap := get_smap_sst sst in
let smem : smemory := get_memory_sst sst in
match get_stack_sst sst with
| soffset::ssize::sstk =>
let sv := SymSHA3 soffset ssize smem in
match add_to_smap sm sv with
| pair key sm' =>
let sst' := set_stack_sst sst ((FreshVar key)::sstk) in
let sst'' := set_smap_sst sst' sm' in
Some sst''
end
| _ => None end.
Definition mstore8_s (smem_updater: smemory_updater_type) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
match get_stack_sst sst with
| soffset::svalue::sstk =>
let smem := get_memory_sst sst in
let smem' := smem_updater ctx (U_MSTORE8 sstack_val soffset svalue) smem (get_smap_sst sst) ops in
let sst' := set_memory_sst sst smem' in
(* let sst' := set_memory_sst sst ((U_MSTORE8 sstack_val soffset svalue)::smem) in *)
let sst'' := set_stack_sst sst' sstk in
Some sst''
| _ => None
end.
Definition mstore_s (smem_updater: smemory_updater_type) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
match get_stack_sst sst with
| soffset::svalue::sstk =>
let smem := get_memory_sst sst in
let smem' := smem_updater ctx (U_MSTORE sstack_val soffset svalue) smem (get_smap_sst sst) ops in
let sst' := set_memory_sst sst smem' in
(* let sst' := set_memory_sst sst ((U_MSTORE sstack_val soffset svalue)::smem) in *)
let sst'' := set_stack_sst sst' sstk in
Some sst''
| _ => None
end.
Definition sstore_s (sstrg_updater: sstorage_updater_type) (ctx: ctx_t) (sst : sstate) (ops: stack_op_instr_map) : option sstate :=
match get_stack_sst sst with
| skey::svalue::sstk =>
let sstrg := get_storage_sst sst in
let sstrg' := sstrg_updater ctx (U_SSTORE sstack_val skey svalue) sstrg (get_smap_sst sst) ops in
let sst' := set_storage_sst sst sstrg' in
(* let sst' := set_storage_sst sst ((U_SSTORE sstack_val key value)::sstrg) in *)
let sst'' := set_stack_sst sst' sstk in
Some sst''
| _ => None
end.
Definition exec_stack_op_intsr_s (label : stack_op_instr) (ctx: ctx_t) (sst : sstate) (ops : stack_op_instr_map) : option sstate :=
match (ops label) with
| OpImp nb_args _ _ _ =>
let sstk := get_stack_sst sst in
match firstn_e nb_args sstk, skipn_e nb_args sstk with
| Some s1,Some s2 =>
let sm : smap := get_smap_sst sst in
let v : smap_value := SymOp label s1 in
match add_to_smap sm v with
| pair key sm' =>
let sst' := set_stack_sst sst ((FreshVar key)::s2) in
let sst'' := set_smap_sst sst' sm' in
Some sst''
end
| _, _ => None
end
end.
Definition evm_exec_instr_s (smem_updater: smemory_updater_type) (sstrg_updater: sstorage_updater_type) (mload_solver: mload_solver_type) (sload_solver: sload_solver_type) (inst: instr) (ctx: ctx_t) (sst: sstate) (ops: stack_op_instr_map): option sstate :=
match inst with
| PUSH size w => (push_s (NToWord EVMWordSize w)) ctx sst ops
| METAPUSH cat v => (metapush_s cat v) ctx sst ops
| POP => pop_s ctx sst ops
| DUP pos => dup_s pos ctx sst ops
| SWAP pos => swap_s pos ctx sst ops
| MLOAD => mload_s mload_solver ctx sst ops
| MSTORE8 => mstore8_s smem_updater ctx sst ops
| MSTORE => mstore_s smem_updater ctx sst ops
| SLOAD => sload_s sload_solver ctx sst ops
| SSTORE => sstore_s sstrg_updater ctx sst ops
| SHA3 => sha3_s ctx sst ops
| KECCAK256 => sha3_s ctx sst ops
| OpInstr label => exec_stack_op_intsr_s label ctx sst ops
end.
Fixpoint evm_exec_block_s (smem_updater: smemory_updater_type) (sstrg_updater: sstorage_updater_type) (mload_solver: mload_solver_type) (sload_solver: sload_solver_type) (p : block) (ctx: ctx_t) (sst : sstate) (ops : stack_op_instr_map): option sstate :=
match p with
| [] => Some sst
| instr::instrs' =>
match (evm_exec_instr_s smem_updater sstrg_updater mload_solver sload_solver instr ctx sst ops) with
| None => None
| Some sst' => evm_exec_block_s smem_updater sstrg_updater mload_solver sload_solver instrs' ctx sst' ops
end
end.
(*
Definition evm_sym_exec (smem_updater: smemory_updater_type) (sstrg_updater: sstorage_updater_type) (mload_solver: mload_solver_type) (sload_solver: sload_solver_type) (p : block) (instk_height: nat) (ops : stack_op_instr_map): option sstate :=
let sst := gen_empty_sstate instk_height in
evm_exec_block_s smem_updater sstrg_updater mload_solver sload_solver p sst ops.
*)
End SymbolicExecution.