source: Deliverables/D2.2/8051/src/clight/clightInterpret.ml @ 818

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

File size: 21.0 KB
Line 
1module Mem = Driver.ClightMemory
2module Value = Driver.ClightMemory.Value
3module LocalEnv = Map.Make(String)
4type localEnv = Value.address LocalEnv.t
5type memory = Clight.fundef Mem.memory
6
7open Clight
8open AST
9
10
11let error_prefix = "Clight interpret"
12let error s = Error.global_error error_prefix s
13let warning s = Error.warning error_prefix s
14let error_float () = error "float not supported."
15
16
17(* Helpers *)
18
19let value_of_address = List.hd
20let address_of_value v = [v]
21
22
23(* State of execution *)
24
25type continuation =
26  | Kstop
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
34
35type state =
36  | State of cfunction*statement*continuation*localEnv*memory
37  | Callstate of fundef*Value.t list*continuation*memory
38  | Returnstate of Value.t*continuation*memory
39
40let string_of_unop = function
41  | Onotbool -> "!"
42  | Onotint -> "~"
43  | Oneg -> "-"
44
45let string_of_binop = function
46  | Oadd -> "+"
47  | Osub -> "-"
48  | Omul -> "*"
49  | Odiv -> "/"
50  | Omod -> "%"
51  | Oand -> "&"
52  | Oor  -> "|"
53  | Oxor -> "^"
54  | Oshl -> "<<"
55  | Oshr -> ">>"
56  | Oeq -> "=="
57  | One -> "!="
58  | Olt -> "<"
59  | Ogt -> ">"
60  | Ole -> "<="
61  | Oge -> ">="
62
63let string_of_signedness = function
64  | Signed -> "signed"
65  | Unsigned -> "unsigned"
66
67let string_of_sized_int = function
68  | I8 -> "char"
69  | I16 -> "short"
70  | I32 -> "int"
71
72let rec string_of_ctype = function
73  | Tvoid -> "void"
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 *)
80  | Tstruct (id, _)
81  | Tunion (id, _) -> id
82  | Tcomp_ptr id -> id ^ "*"
83
84let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
85and string_of_expr_descr = function
86  | Econst_int i -> string_of_int i
87  | Econst_float _ -> error_float ()
88  | Evar x -> x
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) ^ ")"
95  | Ecast (ty, e) ->
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) ^ ")"
109
110let string_of_args args =
111  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
112
113let rec string_of_statement = function
114  | Sskip -> "skip"
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) ^ "; ...)"
124  | Sbreak -> "break"
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
132
133let string_of_local_env lenv =
134  let f x addr s =
135    s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
136  LocalEnv.fold f lenv ""
137
138let 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)
142      (Mem.to_string mem)
143      (string_of_statement stmt)
144  | Callstate (_, args, _, mem) ->
145    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
146      (Mem.to_string mem)
147      (MiscPottier.string_of_list " " Value.to_string args)
148  | Returnstate (v, _, mem) ->
149    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
150      (Mem.to_string mem)
151      (Value.to_string v)
152
153
154(* Continuations and labels *)
155
156let rec call_cont = function
157  | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
158  | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
159  | k -> k
160
161let rec seq_of_labeled_statement = function
162  | LSdefault s -> s
163  | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
164
165let rec find_label1 lbl s k = match s with
166   | Ssequence (s1,s2) ->
167      (match find_label1 lbl s1 (Kseq (s2,k)) with
168      | Some sk -> Some sk
169      | None -> find_label1 lbl s2 k
170      )
171  | Sifthenelse (a,s1,s2) ->
172      (match find_label1 lbl s1 k with
173      | Some sk -> Some sk
174      | None -> find_label1 lbl s2 k
175      )
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
180      | Some sk -> Some sk
181      | None ->
182          (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
183          | Some sk -> Some sk
184          | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
185          ))
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
191           
192and 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
196      | Some sk -> Some sk
197      | None -> find_label_ls lbl sl' k
198      )
199
200let find_label lbl s k = match find_label1 lbl s k with
201  | Some res -> res
202  | _ -> assert false (* should be impossible *)
203
204let 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'
208
209
210(* ctype functions *)
211
212let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
213
214let size_of_ctype = function
215  | Tint (I8, _)  -> 1
216  | Tint (I16, _) -> 2
217  | Tint (I32, _) -> 4
218  | Tfloat _ -> error_float ()
219  | Tcomp_ptr _
220  | Tpointer _
221  | Tarray _
222  | Tstruct _
223  | Tunion _ -> Mem.ptr_size
224  | _ -> assert false (* do not use on these arguments *)
225
226let is_function_type = function
227  | Tfunction _ -> true
228  | _ -> false
229
230let is_array_type = function
231  | Tarray _ -> true
232  | _ -> false
233
234let is_complex_type = function
235  | Tstruct _ | Tunion _ -> true
236  | _ -> false
237
238let is_big_type t = (is_array_type t) || (is_complex_type t)
239
240let dest_type = function
241  | Tpointer ty | Tarray (ty, _) -> ty
242  | _ -> assert false (* do not use on these arguments *)
243
244
245(* Global and local environment management *)
246
247let find_local x lenv =
248  if LocalEnv.mem x lenv then LocalEnv.find x lenv
249  else error ("Unknown local variable " ^ x ^ ".")
250
251let find_global x mem =
252  if Mem.mem_global mem x then Mem.find_global mem x
253  else error ("Unknown global variable " ^ x ^ ".")
254
255let find_symbol lenv mem x =
256  if LocalEnv.mem x lenv then LocalEnv.find x lenv
257  else
258    if Mem.mem_global mem x then Mem.find_global mem x
259    else error ("Unknown variable " ^ x ^ ".")
260
261let find_fundef f mem =
262  let addr = Mem.find_global mem f in
263  Mem.find_fun_def mem addr
264
265
266(* Interpret *)
267
268let byte_of_intsize = function
269  | I8 -> 1
270  | I16 -> 2
271  | I32 -> 4
272
273let choose_cast sign n m v =
274  let f = match sign with
275    | Signed -> Value.sign_ext
276    | Unsigned -> Value.zero_ext in
277  f v n m
278
279let eval_cast = function
280  (* Cast Integer *)
281  | (v,Tint(isize,sign),Tint(isize',_)) ->
282    choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
283  | (v,_,_) -> v
284
285let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
286
287let 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)
294
295let 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
298    Value.add v1 v
299  | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
300    let v = Value.mul (Value.of_int (sizeof ty)) v1 in
301    Value.add v2 v
302  | _ -> Value.add v1 v2
303
304let 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
307    Value.sub v1 v
308  | _ -> Value.sub v1 v2
309
310let 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
315  op v1 v2
316
317let 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
320  let e1 = (v1, t1) in
321  let e2 = (v2, t2) 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)
340
341let 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
345  Value.add v off
346
347let 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
351  | Tunion _ -> v
352  | _ -> assert false (* do not use on these arguments *)
353
354let is_true (v, _) = Value.is_true v
355let is_false (v, _) = Value.is_false v
356
357let rec eval_expr localenv m (Expr (ee, tt)) =
358  match ee with
359    | Econst_int i ->
360      let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
361      ((v, tt),[]) 
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
365      ((v, tt), [])
366    | Evar id ->
367      let addr = find_symbol localenv m id in
368      let v = Mem.load m (size_of_ctype tt) addr in
369      ((v, tt), [])
370    | Ederef e when is_function_type tt || is_big_type tt ->
371      let ((v1,_),l1) = eval_expr localenv m e in
372      ((v1,tt),l1) 
373    | Ederef e ->
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
377      ((v,tt),l1) 
378    | Eaddrof exp ->
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)
385    | Eunop (op,exp) -> 
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)
391      else
392        if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
393      else (v1,l1)
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)
397      else (v1,l1)
398    | Eorbool (e1,e2) ->
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)
401      else (v1,l1)
402    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
403    | Efield (e1,id) -> 
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)
407    | Ecost (lbl,e1) ->
408      let (v1,l1) = eval_expr localenv m e1 in
409      (v1,lbl::l1)
410    | Ecall _ -> assert false (* only used by the annotation process *)
411    | Ecast (cty,exp) -> 
412      let ((v,ty),l1) = eval_expr localenv m exp in
413      ((eval_cast (v,ty,cty),tt),l1)
414
415and 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),[])
420  | Ederef ee ->
421    let ((v,_),l1) = eval_expr localenv m ee in 
422    ((address_of_value v,t),l1)
423  | Efield (ee,id) ->
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)
427  | Ecost (lbl,ee) ->
428    let (v,l) = eval_lvalue localenv m ee in
429    (v,lbl::l)
430  | Ecall _ -> assert false (* only used in the annotation process *)
431
432let 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
437
438
439let 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
443  (mem, lenv)
444
445let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
446
447let init_fun_env mem params args vars =
448  let lenv = LocalEnv.empty in
449  let (mem, lenv) =
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
453
454let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
455
456
457let free_local_env mem lenv =
458  let f _ addr mem = Mem.free mem addr in
459  LocalEnv.fold f lenv mem
460
461let 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."
465
466let 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),[])
477  | Sskip, Kcall _ -> 
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
501  | Swhile(a,s), _ ->
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),[])
527  | Sreturn None, _ -> 
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])
540  | Sgoto 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 *)
544
545
546module InterpretExternal = Primitive.Interpret (Mem)
547
548let 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
552      (mem', v)
553    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
554  Returnstate (v, k, mem')
555
556let step_call args cont mem = function
557  | Internal f -> 
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 ^ ".")
564
565let step = function
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."
573
574
575let 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 *)
583
584let datas_of_init_datas = function
585  | [Init_space _] -> None
586  | l -> Some (List.map data_of_init_data l)
587
588let init_mem prog =
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
595
596let compute_result v =
597  if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
598  else IntValue.Int32.zero
599
600let 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 ;
607  match state with
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)
613
614let interpret debug prog =
615  Printf.printf "*** Clight interpret ***\n%!" ;
616  match prog.prog_main with
617    | None -> (IntValue.Int32.zero, [])
618    | Some main ->
619      let mem = init_mem prog in
620      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
621      exec debug [] first_state
Note: See TracBrowser for help on using the repository browser.