1 module Mem = Driver.ClightMemory
2 module Value = Driver.ClightMemory.Value
3 module LocalEnv = Map.Make(String)
4 type localEnv = Value.address LocalEnv.t
5 type memory = Clight.fundef Mem.memory
11 let error_prefix = "Clight 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 | Kseq of statement*continuation
28 | Kwhile of expr*statement*continuation
29 | Kdowhile of expr*statement*continuation
30 | Kfor2 of expr*statement*statement*continuation
31 | Kfor3 of expr*statement*statement*continuation
32 | Kswitch of continuation
33 | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
36 | State of cfunction*statement*continuation*localEnv*memory
37 | Callstate of fundef*Value.t list*continuation*memory
38 | Returnstate of Value.t*continuation*memory
40 let string_of_unop = function
45 let string_of_binop = function
63 let string_of_signedness = function
65 | Unsigned -> "unsigned"
67 let string_of_sized_int = function
72 let rec string_of_ctype = function
74 | Tint (size, sign) ->
75 (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
76 | Tfloat _ -> error_float ()
77 | Tpointer ty -> (string_of_ctype ty) ^ "*"
78 | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
79 | Tfunction _ -> assert false (* do not cast to a function type *)
81 | Tunion (id, _) -> id
82 | Tcomp_ptr id -> id ^ "*"
84 let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
85 and string_of_expr_descr = function
86 | Econst_int i -> string_of_int i
87 | Econst_float _ -> error_float ()
89 | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
90 | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
91 | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
92 | Ebinop (binop, e1, e2) ->
93 "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
94 "(" ^ (string_of_expr e2) ^ ")"
96 "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
97 | Econdition (e1, e2, e3) ->
98 "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
99 ") : (" ^ (string_of_expr e3) ^ ")"
100 | Eandbool (e1, e2) ->
101 "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
102 | Eorbool (e1, e2) ->
103 "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
104 | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
105 | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
106 | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
107 | Ecall (f, arg, e) ->
108 "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
110 let string_of_args args =
111 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
113 let rec string_of_statement = function
115 | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
116 | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
117 | Scall (Some e, f, args) ->
118 (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
119 | Ssequence _ -> "sequence"
120 | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
121 | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
122 | Sdowhile _ -> "dowhile"
123 | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
125 | Scontinue -> "continue"
126 | Sreturn None -> "return"
127 | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
128 | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
129 | Slabel (lbl, _) -> "label " ^ lbl
130 | Sgoto lbl -> "goto " ^ lbl
131 | Scost (lbl, _) -> "cost " ^ lbl
133 let string_of_local_env lenv =
135 s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ " " in
136 LocalEnv.fold f lenv ""
138 let print_state = function
139 | State (_, stmt, _, lenv, mem) ->
140 Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
141 (string_of_local_env lenv)
143 (string_of_statement stmt)
144 | Callstate (_, args, _, mem) ->
145 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
147 (MiscPottier.string_of_list " " Value.to_string args)
148 | Returnstate (v, _, mem) ->
149 Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
154 (* Continuations and labels *)
156 let rec call_cont = function
157 | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
158 | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
161 let rec seq_of_labeled_statement = function
163 | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
165 let rec find_label1 lbl s k = match s with
166 | Ssequence (s1,s2) ->
167 (match find_label1 lbl s1 (Kseq (s2,k)) with
169 | None -> find_label1 lbl s2 k
171 | Sifthenelse (a,s1,s2) ->
172 (match find_label1 lbl s1 k with
174 | None -> find_label1 lbl s2 k
176 | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
177 | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
178 | Sfor (a1,a2,a3,s1) ->
179 (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
182 (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
184 | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
186 | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
187 | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
188 | Scost (_,s') -> find_label1 lbl s' k
189 | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
190 | Scontinue | Sreturn _ | Sgoto _ -> None
192 and find_label_ls lbl sl k = match sl with
193 | LSdefault s -> find_label1 lbl s k
194 | LScase (_,s,sl') ->
195 (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
197 | None -> find_label_ls lbl sl' k
200 let find_label lbl s k = match find_label1 lbl s k with
202 | _ -> assert false (* should be impossible *)
204 let rec select_switch i = function
205 | LSdefault d -> LSdefault d
206 | LScase (c,s,sl') when c=i-> LScase (c,s,sl')
207 | LScase (_,_,sl') -> select_switch i sl'
210 (* ctype functions *)
212 let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
214 let size_of_ctype = function
218 | Tfloat _ -> error_float ()
223 | Tunion _ -> Mem.ptr_size
224 | _ -> assert false (* do not use on these arguments *)
226 let is_function_type = function
227 | Tfunction _ -> true
230 let is_array_type = function
234 let is_complex_type = function
235 | Tstruct _ | Tunion _ -> true
238 let is_big_type t = (is_array_type t) || (is_complex_type t)
240 let dest_type = function
241 | Tpointer ty | Tarray (ty, _) -> ty
242 | _ -> assert false (* do not use on these arguments *)
245 (* Global and local environment management *)
247 let find_local x lenv =
248 if LocalEnv.mem x lenv then LocalEnv.find x lenv
249 else error ("Unknown local variable " ^ x ^ ".")
251 let find_global x mem =
252 if Mem.mem_global mem x then Mem.find_global mem x
253 else error ("Unknown global variable " ^ x ^ ".")
255 let find_symbol lenv mem x =
256 if LocalEnv.mem x lenv then LocalEnv.find x lenv
258 if Mem.mem_global mem x then Mem.find_global mem x
259 else error ("Unknown variable " ^ x ^ ".")
261 let find_fundef f mem =
262 let addr = Mem.find_global mem f in
263 Mem.find_fun_def mem addr
268 let byte_of_intsize = function
273 let choose_cast sign n m v =
274 let f = match sign with
275 | Signed -> Value.sign_ext
276 | Unsigned -> Value.zero_ext in
279 let eval_cast = function
281 | (v,Tint(isize,sign),Tint(isize',_)) ->
282 choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
285 let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
287 let eval_unop ret_ctype ((_, t) as e) op =
288 let v = to_int32 e in
289 let v = match op with
290 | Onotbool -> Value.notbool v
291 | Onotint -> Value.notint v
292 | Oneg -> Value.negint v in
293 eval_cast (v, t, ret_ctype)
295 let eval_add (v1,t1) (v2,t2) = match t1, t2 with
296 | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
297 let v = Value.mul (Value.of_int (sizeof ty)) v2 in
299 | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
300 let v = Value.mul (Value.of_int (sizeof ty)) v1 in
302 | _ -> Value.add v1 v2
304 let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
305 | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
306 let v = Value.mul (Value.of_int (sizeof ty)) v2 in
308 | _ -> Value.sub v1 v2
310 let choose_sign op_signed op_unsigned v1 v2 t =
311 let op = match t with
312 | Tint (_, Signed) -> op_signed
313 | Tint (_, Unsigned) -> op_unsigned
314 | _ -> op_unsigned in
317 let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op =
318 let v1 = to_int32 e1 in
319 let v2 = to_int32 e2 in
322 let v = match op with
323 | Oadd -> eval_add e1 e2
324 | Osub -> eval_sub e1 e2
325 | Omul -> Value.mul v1 v2
326 | Odiv -> choose_sign Value.div Value.divu v1 v2 t1
327 | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1
328 | Oand -> Value.and_op v1 v2
329 | Oor -> Value.or_op v1 v2
330 | Oxor -> Value.xor v1 v2
331 | Oshl-> Value.shl v1 v2
332 | Oshr-> Value.shr v1 v2
333 | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1
334 | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1
335 | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1
336 | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1
337 | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1
338 | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
339 eval_cast (v, t1, ret_ctype)
341 let rec get_offset_struct v size id fields =
342 let offsets = fst (Mem.concrete_offsets_size size) in
343 let fields = List.combine (List.map fst fields) offsets in
344 let off = Value.of_int (List.assoc id fields) in
347 let get_offset v id = function
348 | Tstruct (_, fields) as t ->
349 let size = ClightToCminor.sizeof_ctype t in
350 get_offset_struct v size id fields
352 | _ -> assert false (* do not use on these arguments *)
354 let is_true (v, _) = Value.is_true v
355 let is_false (v, _) = Value.is_false v
357 let rec eval_expr localenv m (Expr (ee, tt)) =
360 let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
362 | Econst_float _ -> error_float ()
363 | Evar id when is_function_type tt || is_big_type tt ->
364 let v = value_of_address (find_symbol localenv m id) in
367 let addr = find_symbol localenv m id in
368 let v = Mem.load m (size_of_ctype tt) addr in
370 | Ederef e when is_function_type tt || is_big_type tt ->
371 let ((v1,_),l1) = eval_expr localenv m e in
374 let ((v1,_),l1) = eval_expr localenv m e in
375 let addr = address_of_value v1 in
376 let v = Mem.load m (size_of_ctype tt) addr in
379 let ((addr,_),l) = eval_lvalue localenv m exp in
380 ((value_of_address addr,tt),l)
381 | Ebinop (op,exp1,exp2) ->
382 let (v1,l1) = eval_expr localenv m exp1 in
383 let (v2,l2) = eval_expr localenv m exp2 in
384 ((eval_binop tt v1 v2 op,tt),l1@l2)
386 let (e1,l1) = eval_expr localenv m exp in
387 ((eval_unop tt e1 op,tt),l1)
388 | Econdition (e1,e2,e3) ->
389 let (v1,l1) = eval_expr localenv m e1 in
390 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
392 if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
394 | Eandbool (e1,e2) ->
395 let (v1,l1) = eval_expr localenv m e1 in
396 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
399 let (v1,l1) = eval_expr localenv m e1 in
400 if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
402 | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
404 let ((v1,t1),l1) = eval_expr localenv m e1 in
405 let addr = address_of_value (get_offset v1 id t1) in
406 ((Mem.load m (size_of_ctype tt) addr, tt), l1)
408 let (v1,l1) = eval_expr localenv m e1 in
410 | Ecall _ -> assert false (* only used by the annotation process *)
412 let ((v,ty),l1) = eval_expr localenv m exp in
413 ((eval_cast (v,ty,cty),tt),l1)
415 and eval_lvalue localenv m (Expr (e,t)) = match e with
416 | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
417 | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_) | Eorbool (_,_)
418 | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
419 | Evar id -> ((find_symbol localenv m id,t),[])
421 let ((v,_),l1) = eval_expr localenv m ee in
422 ((address_of_value v,t),l1)
424 let ((v,tt),l1) = eval_expr localenv m ee in
425 let v' = get_offset v id tt in
426 ((address_of_value v', t), l1)
428 let (v,l) = eval_lvalue localenv m ee in
430 | Ecall _ -> assert false (* only used in the annotation process *)
432 let eval_exprlist lenv mem es =
433 let f (vs, cost_lbls) e =
434 let ((v, _), cost_lbls') = eval_expr lenv mem e in
435 (vs @ [v], cost_lbls @ cost_lbls') in
436 List.fold_left f ([], []) es
439 let bind (mem, lenv) (x, ty) v =
440 let (mem, addr) = Mem.alloc mem (sizeof ty) in
441 let mem = Mem.store mem (sizeof ty) addr v in
442 let lenv = LocalEnv.add x addr lenv in
445 let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
447 let init_fun_env mem params args vars =
448 let lenv = LocalEnv.empty in
450 try List.fold_left2 bind (mem, lenv) params args
451 with Invalid_argument _ -> error "wrong size of arguments." in
452 List.fold_left bind_var (mem, lenv) vars
454 let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
457 let free_local_env mem lenv =
458 let f _ addr mem = Mem.free mem addr in
459 LocalEnv.fold f lenv mem
461 let condition v a_true a_false =
462 if Value.is_false v then a_false
463 else if Value.is_true v then a_true
464 else error "undefined condition guard value."
466 let eval_stmt f k e m s = match s, k with
467 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
468 | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
469 | Sskip, Kdowhile(a,s,k) ->
470 let ((v1, _),l1) = eval_expr e m a in
471 let a_false = (State(f,Sskip,k,e,m),l1) in
472 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
473 condition v1 a_true a_false
474 | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
475 | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
476 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
478 let m' = free_local_env m e in
479 (Returnstate(Value.undef,k,m'),[])
480 | Sassign(a1, a2), _ ->
481 let ((v1,t1),l1) = (eval_lvalue e m a1) in
482 let ((v2,t2),l2) = eval_expr e m a2 in
483 (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
484 | Scall(None,a,al), _ ->
485 let ((v1,_),l1) = eval_expr e m a in
486 let fd = Mem.find_fun_def m (address_of_value v1) in
487 let (vargs,l2) = eval_exprlist e m al in
488 (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
489 | Scall(Some lhs,a,al), _ ->
490 let ((v1,_),l1) = eval_expr e m a in
491 let fd = Mem.find_fun_def m (address_of_value v1) in
492 let (vargs,l2) = eval_exprlist e m al in
493 let (vt3,l3) = eval_lvalue e m lhs in
494 (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
495 | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
496 | Sifthenelse(a,s1,s2), _ ->
497 let ((v1,_),l1) = eval_expr e m a in
498 let a_true = (State(f,s1,k,e,m),l1) in
499 let a_false = (State(f,s2,k,e,m),l1) in
500 condition v1 a_true a_false
502 let ((v1,_),l1) = eval_expr e m a in
503 let a_false = (State(f,Sskip,k,e,m),l1) in
504 let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
505 condition v1 a_true a_false
506 | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
507 | Sfor(Sskip,a2,a3,s), _ ->
508 let ((v1,_),l1) = eval_expr e m a2 in
509 let a_false = (State(f,Sskip,k,e,m),l1) in
510 let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
511 condition v1 a_true a_false
512 | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
513 | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
514 | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
515 | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
516 | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
517 | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
518 | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
519 | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
520 | Scontinue, Kdowhile(a,s,k) ->
521 let ((v1,_),l1) = eval_expr e m a in
522 let a_false = (State(f,Sskip,k,e,m),l1) in
523 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
524 condition v1 a_true a_false
525 | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
526 | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
528 let m' = free_local_env m e in
529 (Returnstate(Value.undef,(call_cont k),m'),[])
530 | Sreturn (Some a), _ ->
531 let ((v1,_),l1) = eval_expr e m a in
532 let m' = free_local_env m e in
533 (Returnstate(v1,call_cont k,m'),l1)
534 | Sswitch(a,sl), _ ->
535 let ((v,_),l) = eval_expr e m a in
536 let n = Value.to_int v in
537 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
538 | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
539 | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
541 let (s', k') = find_label lbl f.fn_body (call_cont k) in
542 (State(f,s',k',e,m),[])
543 | _ -> assert false (* should be impossible *)
546 module InterpretExternal = Primitive.Interpret (Mem)
548 let interpret_external k mem f args =
549 let (mem', v) = match InterpretExternal.t mem f args with
550 | (mem', InterpretExternal.V vs) ->
551 let v = if List.length vs = 0 then Value.undef else List.hd vs in
553 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
554 Returnstate (v, k, mem')
556 let step_call args cont mem = function
558 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
559 State (f, f.fn_body, cont, e, mem')
560 | External(id,targs,tres) when List.length targs = List.length args ->
561 interpret_external cont mem id args
562 | External(id,_,_) ->
563 error ("wrong size of arguments when calling external " ^ id ^ ".")
566 | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
567 | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
568 | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
569 | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
570 let m' = assign m v ty vv in
571 (State(f,Sskip,k,e,m'),[])
572 | _ -> error "state malformation."
575 let data_of_init_data = function
576 | Init_int8 i -> Data_int8 i
577 | Init_int16 i -> Data_int16 i
578 | Init_int32 i -> Data_int32 i
579 | Init_float32 f -> error_float ()
580 | Init_float64 f -> error_float ()
581 | Init_space i -> error "bad global initialization style."
582 | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
584 let datas_of_init_datas = function
585 | [Init_space _] -> None
586 | l -> Some (List.map data_of_init_data l)
589 let f_var mem ((x, init_datas), ty) =
590 Mem.add_var mem x (ClightToCminor.sizeof_ctype ty)
591 (datas_of_init_datas init_datas) in
592 let mem = List.fold_left f_var Mem.empty prog.prog_vars in
593 let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
594 List.fold_left f_fun_def mem prog.prog_funct
596 let compute_result v =
597 if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
598 else IntValue.Int32.zero
600 let rec exec debug trace (state, l) =
601 let cost_labels = l @ trace in
602 let print_and_return_result res =
603 if debug then Printf.printf "Result = %s\n%!"
604 (IntValue.Int32.to_string res) ;
605 (res, cost_labels) in
606 if debug then print_state state ;
608 | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
609 print_and_return_result (compute_result v)
610 | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
611 print_and_return_result IntValue.Int32.zero
612 | state -> exec debug cost_labels (step state)
614 let interpret debug prog =
615 Printf.printf "*** Clight interpret ***\n%!" ;
616 match prog.prog_main with
617 | None -> (IntValue.Int32.zero, [])
619 let mem = init_mem prog in
620 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
621 exec debug [] first_state