Source file evaluator.ml
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
open BinNums
open Utils0
open Type
open Sem_type
open Warray_
open Var0
open Varmap
open Low_memory
open Expr
open Psem_defs
open Values
open Sem_params
exception Eval_error of instr_info * Utils0.error
let pp_error fmt err =
Format.fprintf fmt "%s" @@
match err with
| ErrOob -> "out_of_bound"
| ErrAddrUndef -> "undefined address"
| ErrAddrInvalid -> "invalid address"
| ErrStack -> "stack error"
| ErrType -> "type error"
| ErrArith -> "arithmetic error"
| ErrSemUndef -> "undefined semantics"
let exn_exec (ii:instr_info) (r: 't exec) =
match r with
| Ok r -> r
| Error e -> raise (Eval_error(ii, e))
let of_val_z ii v : coq_Z =
Obj.magic (exn_exec ii (of_val Coq_sint v))
let of_val_b ii v : bool =
Obj.magic (exn_exec ii (of_val Coq_sbool v))
type 'asm stack =
| Sempty of instr_info * 'asm fundef
| Scall of
instr_info * 'asm fundef * lval list * Vm.t * 'asm instr list * 'asm stack
| Sfor of instr_info * var_i * coq_Z list * 'asm instr list * 'asm instr list * 'asm stack
type ('syscall_state, 'asm) state =
{ s_prog : 'asm prog;
s_cmd : 'asm instr list;
s_estate : 'syscall_state estate;
s_stk : 'asm stack;
}
exception Final of Memory.mem * values
let return ep spp s =
assert (s.s_cmd = []);
match s.s_stk with
| Sempty(ii, f) ->
let s2 = s.s_estate in
let m2 = s2.emem and vm2 = s2.evm in
let vres =
exn_exec ii (mapM (fun (x:var_i) -> get_var nosubword true vm2 x.v_var) f.f_res) in
let vres' = exn_exec ii (mapM2 ErrType truncate_val f.f_tyout vres) in
raise (Final(m2, vres'))
| Scall(ii,f,xs,vm1,c,stk) ->
let gd = s.s_prog.p_globs in
let {escs = scs2; emem = m2; evm = vm2} = s.s_estate in
let vres =
exn_exec ii (mapM (fun (x:var_i) -> get_var nosubword true vm2 x.v_var) f.f_res) in
let vres' = exn_exec ii (mapM2 ErrType truncate_val f.f_tyout vres) in
let s1 = exn_exec ii (write_lvals nosubword ep spp true gd {escs = scs2; emem = m2; evm = vm1 } xs vres') in
{ s with
s_cmd = c;
s_estate = s1;
s_stk = stk }
| Sfor(ii,i,ws,body,c,stk) ->
match ws with
| [] -> { s with s_cmd = c; s_stk = stk }
| w::ws ->
let s1 = exn_exec ii (write_var nosubword ep true i (Vint w) s.s_estate) in
{ s with s_cmd = body;
s_estate = s1;
s_stk = Sfor(ii, i, ws, body, c, stk) }
let small_step1 ep spp sip s =
match s.s_cmd with
| [] -> return ep spp s
| i :: c ->
let MkI(ii,ir) = i in
let gd = s.s_prog.p_globs in
let s1 = s.s_estate in
match ir with
| Cassgn(x,_,ty,e) ->
let v = exn_exec ii (sem_pexpr nosubword ep spp true gd s1 e) in
let v' = exn_exec ii (truncate_val ty v) in
let s2 = exn_exec ii (write_lval nosubword ep spp true gd x v' s1) in
{ s with s_cmd = c; s_estate = s2 }
| Copn(xs,_,op,es) ->
let s2 = exn_exec ii (sem_sopn nosubword ep spp sip._asmop gd op s1 xs es) in
{ s with s_cmd = c; s_estate = s2 }
| Csyscall(xs,o, es) ->
let ves = exn_exec ii (sem_pexprs nosubword ep spp true gd s1 es) in
let ((scs, m), vs) =
exn_exec ii (syscall_sem__ sip._sc_sem ep._pd s1.escs s1.emem o ves) in
let s2 = exn_exec ii (write_lvals nosubword ep spp true gd {escs = scs; emem = m; evm = s1.evm} xs vs) in
{ s with s_cmd = c; s_estate = s2 }
| Cif(e,c1,c2) ->
let b = of_val_b ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 e)) in
let c = (if b then c1 else c2) @ c in
{ s with s_cmd = c }
| Cfor (i,((d,lo),hi), body) ->
let vlo = of_val_z ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 lo)) in
let vhi = of_val_z ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 hi)) in
let rng = wrange d vlo vhi in
let s =
{s with s_cmd = []; s_stk = Sfor(ii, i, rng, body, c, s.s_stk) } in
return ep spp s
| Cwhile (_, c1, e, _, c2) ->
{ s with s_cmd = c1 @ MkI(ii, Cif(e, c2@[i],[])) :: c }
| Ccall(xs,fn,es) ->
let vargs' = exn_exec ii (sem_pexprs nosubword ep spp true gd s1 es) in
let f =
match get_fundef s.s_prog.p_funcs fn with
| Some f -> f
| None -> assert false in
let vargs = exn_exec ii (mapM2 ErrType truncate_val f.f_tyin vargs') in
let {escs; emem = m1; evm = vm1} = s1 in
let stk = Scall(ii,f, xs, vm1, c, s.s_stk) in
let sf =
exn_exec ii (write_vars nosubword ep true f.f_params vargs {escs; emem = m1; evm = Vm.init nosubword}) in
{s with s_cmd = f.f_body;
s_estate = sf;
s_stk = stk }
let rec small_step ep spp sip s =
small_step ep spp sip (small_step1 ep spp sip s)
let init_state ep scs0 p ii fn args m =
let f = BatOption.get (get_fundef p.p_funcs fn) in
let vargs = exn_exec ii (mapM2 ErrType truncate_val f.f_tyin args) in
let s_estate = { escs = scs0; emem = m; evm = Vm.init nosubword} in
let s_estate = exn_exec ii (write_vars nosubword ep true f.f_params vargs s_estate) in
{ s_prog = p; s_cmd = f.f_body; s_estate; s_stk = Sempty (ii, f) }
let exec ep spp sip scs0 p ii fn args m =
let s = init_state ep scs0 p ii fn args m in
try small_step ep spp sip s
with Final(m,vs) -> m, vs
let initial_memory reg_size rsp alloc =
let ptr_of_z z = Word0.wrepr reg_size (Conv.cz_of_z z) in
(Low_memory.Memory.coq_M reg_size).init
(List.map (fun (ptr, sz) -> (ptr_of_z ptr, Conv.cz_of_z sz)) alloc)
(ptr_of_z rsp)
let run (type reg regx xreg rflag cond asm_op extra_op)
(module A : Arch_full.Arch
with type reg = reg
and type regx = regx
and type xreg = xreg
and type rflag = rflag
and type cond = cond
and type asm_op = asm_op
and type extra_op = extra_op)
(p :
(reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op
Expr.uprog) ii fn args m =
let ep = Sem_params_of_arch_extra.ep_of_asm_e A.asm_e Syscall_ocaml.sc_sem in
let spp = Sem_params_of_arch_extra.spp_of_asm_e A.asm_e in
let sip =
Sem_params_of_arch_extra.sip_of_asm_e A.asm_e Syscall_ocaml.sc_sem
in
let scs0 = Syscall_ocaml.initial_state () in
exec ep spp sip scs0 p ii fn args m
let pp_undef fmt ty =
Format.fprintf fmt "undef<%a>" PrintCommon.pp_ty (Conv.ty_of_cty ty)
let pp_word fmt ws w =
let z = Word0.wunsigned ws w in
let z = Conv.z_of_cz z in
Printer.pp_print_X fmt z
let pp_val fmt v =
match v with
| Vbool b -> Format.fprintf fmt "%b" b
| Vint z -> Format.fprintf fmt "%a" Z.pp_print (Conv.z_of_cz z)
| Varr(p,t) ->
let ip = Conv.int_of_pos p in
let pp_res fmt = function
| Ok w -> pp_word fmt U8 w
| Error ErrAddrUndef -> pp_undef fmt (Coq_sword U8)
| Error _ -> assert false in
Format.fprintf fmt "@[[";
for i = 0 to ip-2 do
let i = Conv.cz_of_int i in
Format.fprintf fmt "%a;@ " pp_res (WArray.get p Aligned AAscale U8 t i);
done;
if 0 < ip then
pp_res fmt (WArray.get p Aligned AAscale U8 t (Conv.cz_of_int (ip-1)));
Format.fprintf fmt "]@]";
| Vword(ws, w) -> pp_word fmt ws w
| Vundef ty -> pp_undef fmt ty