4 module Mem = Driver.CminorMemory
6 module LocalEnv = Map.Make(String)
7 type local_env = Val.t LocalEnv.t
8 type memory = Cminor.function_def Mem.memory
11 let error_prefix = "Cminor interpret"
12 let error s = Error.global_error error_prefix s
13 let warning s = Error.warning error_prefix s
14 let error_float () = error "float not supported."
19 let value_of_address = List.hd
20 let address_of_value v = [v]
23 (* State of execution *)
27 | Ct_cont of statement*continuation
28 | Ct_endblock of continuation
30 ident option*internal_function*Val.address*local_env*continuation
34 internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
35 | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
36 | State_return of Val.t*continuation*(function_def Mem.memory)
38 let string_of_local_env lenv =
39 let f x v s = s ^ x ^ " = " ^ (Val.to_string v) ^ " " in
40 LocalEnv.fold f lenv ""
42 let string_of_expr = CminorPrinter.print_expression
44 let string_of_args args =
45 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
47 let rec string_of_statement = function
49 | St_assign (x, e) -> x ^ " = " ^ (string_of_expr e)
50 | St_store (q, e1, e2) ->
51 Printf.sprintf "%s[%s] = %s"
52 (Memory.string_of_quantity q) (string_of_expr e1) (string_of_expr e2)
53 | St_call (None, f, args, _)
54 | St_tailcall (f, args, _) -> (string_of_expr f) ^ (string_of_args args)
55 | St_call (Some x, f, args, _) ->
56 x ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
57 | St_seq _ -> "sequence"
58 | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
60 | St_block _ -> "block"
61 | St_exit n -> "exit " ^ (string_of_int n)
62 | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
63 | St_return None -> "return"
64 | St_return (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
65 | St_label (lbl, _) -> "label " ^ lbl
66 | St_goto lbl -> "goto " ^ lbl
67 | St_cost (lbl, _) -> "cost " ^ lbl
69 let print_state = function
70 | State_regular (_, stmt, _, sp, lenv, mem) ->
71 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
72 (string_of_local_env lenv)
74 (Val.to_string (value_of_address sp))
75 (string_of_statement stmt)
76 | State_call (_, args, _, mem) ->
77 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
79 (MiscPottier.string_of_list " " Val.to_string args)
80 | State_return (v, _, mem) ->
81 Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
86 (* Global and local environment management *)
88 let init_local_env args params vars =
89 let f_param lenv (x, _) v = LocalEnv.add x v lenv in
90 let f_var lenv (x, _) = LocalEnv.add x Val.undef lenv in
91 let lenv = List.fold_left2 f_param LocalEnv.empty params args in
92 List.fold_left f_var lenv vars
94 let find_fundef f mem =
95 let addr = Mem.find_global mem f in
96 Mem.find_fun_def mem addr
99 (* Expression evaluation *)
101 module Eval_op (M : Memory.S) = struct
103 let concrete_stacksize = M.concrete_size
105 let ext_fun_of_sign = function
106 | AST.Signed -> M.Value.sign_ext
107 | AST.Unsigned -> M.Value.zero_ext
109 let cast_to_std t v = match t with
110 | AST.Sig_int (size, sign) -> (ext_fun_of_sign sign) v size M.int_size
111 | AST.Sig_float _ -> error_float ()
112 | AST.Sig_offset | AST.Sig_ptr -> v
114 let cast_from_std t v = match t with
115 | AST.Sig_int (size, _) -> (ext_fun_of_sign AST.Unsigned) v M.int_size size
116 | AST.Sig_float _ -> error_float ()
117 | AST.Sig_offset | AST.Sig_ptr -> v
119 let cst mem sp t = function
120 | Cst_int i -> cast_to_std t (M.Value.of_int i)
121 | Cst_float _ -> error_float ()
122 | Cst_addrsymbol id when M.mem_global mem id ->
123 value_of_address (M.find_global mem id)
124 | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
125 | Cst_stack -> value_of_address sp
126 | Cst_offset off -> M.Value.of_int (M.concrete_offset off)
127 | Cst_sizeof t' -> cast_to_std t (M.Value.of_int (M.concrete_size t'))
129 let fun_of_op1 = function
130 | Op_cast ((from_size, from_sign), to_size) ->
131 (fun v -> (ext_fun_of_sign from_sign) v from_size to_size)
132 | Op_negint -> M.Value.negint
133 | Op_notbool -> M.Value.notbool
134 | Op_notint -> M.Value.negint
135 | Op_id -> (fun v -> v)
138 error "conversion between integers and pointers not supported yet."
140 let op1 ret_type t op v =
141 cast_from_std ret_type ((fun_of_op1 op) (cast_to_std t v))
143 let fun_of_op2 = function
144 | Op_add | Op_addp -> M.Value.add
145 | Op_sub | Op_subp | Op_subpp -> M.Value.sub
146 | Op_mul -> M.Value.mul
147 | Op_div -> M.Value.div
148 | Op_divu -> M.Value.divu
149 | Op_mod -> M.Value.modulo
150 | Op_modu -> M.Value.modulou
151 | Op_and -> M.Value.and_op
152 | Op_or -> M.Value.or_op
153 | Op_xor -> M.Value.xor
154 | Op_shl -> M.Value.shl
155 | Op_shr -> M.Value.shr
156 | Op_shru -> M.Value.shru
157 | Op_cmp Cmp_eq | Op_cmpp Cmp_eq -> M.Value.cmp_eq
158 | Op_cmp Cmp_ne | Op_cmpp Cmp_ne -> M.Value.cmp_ne
159 | Op_cmp Cmp_gt | Op_cmpp Cmp_gt -> M.Value.cmp_gt
160 | Op_cmp Cmp_ge | Op_cmpp Cmp_ge -> M.Value.cmp_ge
161 | Op_cmp Cmp_lt | Op_cmpp Cmp_lt -> M.Value.cmp_lt
162 | Op_cmp Cmp_le | Op_cmpp Cmp_le -> M.Value.cmp_le
163 | Op_cmpu Cmp_eq -> M.Value.cmp_eq_u
164 | Op_cmpu Cmp_ne -> M.Value.cmp_ne_u
165 | Op_cmpu Cmp_gt -> M.Value.cmp_gt_u
166 | Op_cmpu Cmp_ge -> M.Value.cmp_ge_u
167 | Op_cmpu Cmp_lt -> M.Value.cmp_lt_u
168 | Op_cmpu Cmp_le -> M.Value.cmp_le_u
170 let op2 ret_type t1 t2 op2 v1 v2 =
171 let v1 = cast_to_std t1 v1 in
172 let v2 = cast_to_std t2 v2 in
173 cast_from_std ret_type ((fun_of_op2 op2) v1 v2)
176 module Eval = Eval_op (Mem)
178 let concrete_stacksize = Eval.concrete_stacksize
179 let eval_constant = Eval.cst
180 let eval_unop = Eval.op1
181 let eval_binop = Eval.op2
183 let type_of_expr (Cminor.Expr (_, t)) = t
185 let rec eval_expression stack local_env memory (Cminor.Expr (ed, t)) =
187 | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
188 | Id x -> error ("unknown local variable " ^ x ^ ".")
189 | Cst(c) -> (eval_constant memory stack t c,[])
191 let (v,l) = eval_expression stack local_env memory arg in
192 (eval_unop t (type_of_expr arg) op v,l)
193 | Op2(op, arg1, arg2) ->
194 let (v1,l1) = eval_expression stack local_env memory arg1 in
195 let (v2,l2) = eval_expression stack local_env memory arg2 in
196 (eval_binop t (type_of_expr arg1) (type_of_expr arg2) op v1 v2,l1@l2)
198 let (v,l) = eval_expression stack local_env memory a in
199 (Mem.loadq memory q (address_of_value v),l)
201 let (v1,l1) = eval_expression stack local_env memory a1 in
202 if Val.is_true v1 then
203 let (v2,l2) = eval_expression stack local_env memory a2 in
206 if Val.is_false v1 then
207 let (v3,l3) = eval_expression stack local_env memory a3 in
209 else error "undefined conditional value."
211 let (v,l) = eval_expression stack local_env memory e in
214 let eval_exprlist sp lenv mem es =
215 let f (vs, cost_lbls) e =
216 let (v, cost_lbls') = eval_expression sp lenv mem e in
217 (vs @ [v], cost_lbls @ cost_lbls') in
218 List.fold_left f ([], []) es
220 (* State transition *)
222 let rec callcont = function
224 | Ct_cont(_,k) -> callcont k
225 | Ct_endblock(k) -> callcont k
226 | Ct_returnto(a,b,c,d,e) -> Ct_returnto(a,b,c,d,e)
228 let findlabel lbl st k =
229 let rec fdlbl k = function
231 | St_assign(_,_) -> None
232 | St_store(_,_,_) -> None
233 | St_call(_,_,_,_) -> None
234 | St_tailcall(_,_,_) -> None
236 (match fdlbl (Ct_cont(s2,k)) s1 with
240 | St_ifthenelse(_,s1,s2) ->
241 (match fdlbl k s1 with
245 | St_loop(s) -> fdlbl (Ct_cont(St_loop(s),k)) s
246 | St_block(s) -> fdlbl (Ct_endblock(k)) s
248 | St_switch(_,_,_) -> None
249 | St_return(_) -> None
250 | St_label(l,s) when l = lbl -> Some((s,k))
252 | St_cost (_,s) | St_label (_,s) -> fdlbl k s
253 in match fdlbl k st with
254 None -> assert false (*Wrong label*)
258 let call_state sigma e m f params cont =
259 let (addr,l1) = eval_expression sigma e m f in
260 let fun_def = Mem.find_fun_def m (address_of_value addr) in
261 let (args,l2) = eval_exprlist sigma e m params in
262 (State_call(fun_def,args,cont,m),l1@l2)
264 let eval_stmt f k sigma e m s = match s, k with
265 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
266 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
267 | St_skip, (Ct_returnto _ as k) ->
268 (State_return (Val.undef,k,Mem.free m sigma),[])
270 (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
271 | St_assign(x,exp),_ ->
272 let (v,l) = eval_expression sigma e m exp in
273 let e = LocalEnv.add x v e in
274 (State_regular(f, St_skip, k, sigma, e, m),l)
275 | St_store(q,a1,a2),_ ->
276 let (v1,l1) = eval_expression sigma e m a1 in
277 let (v2,l2) = eval_expression sigma e m a2 in
278 let m = Mem.storeq m q (address_of_value v1) v2 in
279 (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
280 | St_call(xopt,f',params,_),_ ->
281 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
282 | St_tailcall(f',params,_),_ ->
283 call_state sigma e m f' params (callcont k)
284 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
285 | St_ifthenelse(exp,s1,s2),_ ->
286 let (v,l) = eval_expression sigma e m exp in
288 if Val.is_true v then s1
290 if Val.is_false v then s2
291 else error "undefined conditional value." in
292 (State_regular(f,next_stmt,k,sigma,e,m),l)
293 | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
294 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
295 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
296 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
297 | St_exit(n),Ct_endblock(k) ->
298 (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
299 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
301 let (s2,k2) = findlabel lbl f.f_body (callcont k) in
302 (State_regular(f,s2,k2,sigma,e,m),[])
303 | St_switch(exp,lst,def),_ ->
304 let (v,l) = eval_expression sigma e m exp in
307 let i = Val.to_int v in
309 if List.mem_assoc i lst then List.assoc i lst
311 (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
312 with _ -> error "int value too big."
313 else error "undefined switch value."
314 | St_return(None),_ ->
315 (State_return (Val.undef,callcont k,Mem.free m sigma),[])
316 | St_return(Some(a)),_ ->
317 let (v,l) = eval_expression sigma e m a in
318 (State_return (v,callcont k,Mem.free m sigma),l)
319 | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
320 | _ -> error "state malformation."
323 module InterpretExternal = Primitive.Interpret (Mem)
325 let interpret_external k mem f args =
326 let (mem', v) = match InterpretExternal.t mem f args with
327 | (mem', InterpretExternal.V vs) ->
328 let v = if List.length vs = 0 then Val.undef else List.hd vs in
330 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
331 State_return (v, k, mem')
333 let step_call vargs k m = function
335 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
336 let lenv = init_local_env vargs f.f_params f.f_vars in
337 State_regular(f,f.f_body,k,sp,lenv,m)
338 | F_ext f -> interpret_external k m f.ef_tag vargs
341 | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
342 | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
343 | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
344 (State_regular(f,St_skip,k,sigma,e,m),[])
345 | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
346 let e = LocalEnv.add x v e in
347 (State_regular(f,St_skip,k,sigma,e,m),[])
348 | _ -> error "state malformation."
352 let f_var mem (x, size, init_datas) = Mem.add_var mem x size init_datas in
353 let mem = List.fold_left f_var Mem.empty prog.vars in
354 let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
355 List.fold_left f_fun_def mem prog.functs
357 let compute_result v =
358 if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
359 else IntValue.Int32.zero
361 let rec exec debug trace (state, l) =
362 let cost_labels = l @ trace in
363 let print_and_return_result res =
364 if debug then Printf.printf "Result = %s\n%!"
365 (IntValue.Int32.to_string res) ;
366 (res, cost_labels) in
367 if debug then print_state state ;
369 | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
370 print_and_return_result (compute_result v)
371 | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
372 print_and_return_result IntValue.Int32.zero
373 | state -> exec debug cost_labels (step state)
375 let interpret debug prog =
376 Printf.printf "*** Cminor interpret ***\n%!" ;
378 | None -> (IntValue.Int32.zero, [])
380 let mem = init_mem prog in
381 let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
382 exec debug [] first_state