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

Last change on this file since 3673 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

File size: 22.6 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
6type indexing = CostLabel.const_indexing
7
8open Clight
9open AST
10
11
12let error_prefix = "Clight interpret"
13let error s = Error.global_error error_prefix s
14let warning s = Error.warning error_prefix s
15let error_float () = error "float not supported."
16
17
18(* Helpers *)
19
20let value_of_address = List.hd
21let address_of_value v = [v]
22
23
24(* State of execution *)
25
26type continuation =
27  | Kstop
28  | Kseq of statement*continuation
29  | Kwhile of int option*expr*statement*continuation
30  | Kdowhile of int option*expr*statement*continuation
31  | Kfor2 of int option*expr*statement*statement*continuation
32  | Kfor3 of int option*expr*statement*statement*continuation
33  | Kswitch of continuation
34  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
35
36type state =
37  | State of cfunction*statement*continuation*localEnv*memory*indexing list
38  | Callstate of fundef*Value.t list*continuation*memory*indexing list
39  | Returnstate of Value.t*continuation*memory*indexing list
40
41let string_of_unop = function
42  | Onotbool -> "!"
43  | Onotint -> "~"
44  | Oneg -> "-"
45
46let string_of_binop = function
47  | Oadd -> "+"
48  | Osub -> "-"
49  | Omul -> "*"
50  | Odiv -> "/"
51  | Omod -> "%"
52  | Oand -> "&"
53  | Oor  -> "|"
54  | Oxor -> "^"
55  | Oshl -> "<<"
56  | Oshr -> ">>"
57  | Oeq -> "=="
58  | One -> "!="
59  | Olt -> "<"
60  | Ogt -> ">"
61  | Ole -> "<="
62  | Oge -> ">="
63
64let string_of_signedness = function
65  | Signed -> "signed"
66  | Unsigned -> "unsigned"
67
68let string_of_sized_int = function
69  | I8 -> "char"
70  | I16 -> "short"
71  | I32 -> "int"
72
73let rec string_of_ctype = function
74  | Tvoid -> "void"
75  | Tint (size, sign) ->
76    (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
77  | Tfloat _ -> error_float ()
78  | Tpointer ty -> (string_of_ctype ty) ^ "*"
79  | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
80  | Tfunction _ -> assert false (* do not cast to a function type *)
81  | Tstruct (id, _)
82  | Tunion (id, _) -> id
83  | Tcomp_ptr id -> id ^ "*"
84
85let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
86and string_of_expr_descr = function
87  | Econst_int i -> string_of_int i
88  | Econst_float _ -> error_float ()
89  | Evar x -> x
90  | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
91  | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
92  | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
93  | Ebinop (binop, e1, e2) ->
94    "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
95    "(" ^ (string_of_expr e2) ^ ")"
96  | Ecast (ty, e) ->
97    "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
98  | Econdition (e1, e2, e3) ->
99    "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
100    ") : (" ^ (string_of_expr e3) ^ ")"
101  | Eandbool (e1, e2) ->
102    "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
103  | Eorbool (e1, e2) ->
104    "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
105  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
107  | Ecost (cost_lbl, e) -> 
108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
110  | Ecall (f, arg, e) ->
111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
112
113let string_of_args args =
114  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
115
116let string_of_loop_depth = function
117        | None -> ""
118        | Some d -> " at " ^ string_of_int d
119
120let rec string_of_statement = function
121  | Sskip -> "skip"
122  | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
123  | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
124  | Scall (Some e, f, args) ->
125    (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
126  | Ssequence _ -> "sequence"
127  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
128  | Swhile (i, e, _) ->
129                let d = string_of_loop_depth i in
130                "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")"
131  | Sdowhile (i, _, _) ->
132    let d = string_of_loop_depth i in
133    "dowhile" ^ d
134  | Sfor (i, s, _, _, _) ->
135                let d = string_of_loop_depth i in
136                "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)"
137  | Sbreak -> "break"
138  | Scontinue -> "continue"
139  | Sreturn None -> "return"
140  | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
141  | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
142  | Slabel (lbl, _) -> "label " ^ lbl
143  | Sgoto lbl -> "goto " ^ lbl
144  | Scost (lbl, _) ->
145    let lbl = CostLabel.string_of_cost_label lbl in
146                "cost " ^ lbl
147
148let string_of_local_env lenv =
149  let f x addr s =
150    s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
151  LocalEnv.fold f lenv ""
152
153let print_state state = match state with
154  | State (_, stmt, _, lenv, mem, c) ->
155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
156      (string_of_local_env lenv)
157      (Mem.to_string mem);
158    let i = CostLabel.curr_const_ind c in
159    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
160    Printf.printf "\nRegular state: %s\n\n%!"
161      (string_of_statement stmt)
162  | Callstate (_, args, _, mem, _) ->
163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
164      (Mem.to_string mem)
165      (MiscPottier.string_of_list " " Value.to_string args)
166  | Returnstate (v, _, mem, _) ->
167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
168      (Mem.to_string mem)
169      (Value.to_string v)
170
171
172(* Continuations and labels *)
173
174let rec call_cont = function
175  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
176  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
177  | k -> k
178
179let rec seq_of_labeled_statement = function
180  | LSdefault s -> s
181  | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
182
183let rec find_label1 lbl s k = match s with
184   | Ssequence (s1,s2) ->
185      (match find_label1 lbl s1 (Kseq (s2,k)) with
186      | Some sk -> Some sk
187      | None -> find_label1 lbl s2 k
188      )
189  | Sifthenelse (a,s1,s2) ->
190      (match find_label1 lbl s1 k with
191      | Some sk -> Some sk
192      | None -> find_label1 lbl s2 k
193      )
194  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
195  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
196  | Sfor (i,a1,a2,a3,s1) ->
197                (* doubt: should we search for labels in a1? *)
198      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
199      | Some sk -> Some sk
200      | None ->
201          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
202          | Some sk -> Some sk
203          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
204          ))
205  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
206  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
207  | Scost (_,s') -> find_label1 lbl s' k
208  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak 
209  | Scontinue | Sreturn _ | Sgoto _ -> None
210           
211and find_label_ls lbl sl k =  match sl with
212  | LSdefault s -> find_label1 lbl s k
213  | LScase (_,s,sl') ->
214      (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
215      | Some sk -> Some sk
216      | None -> find_label_ls lbl sl' k
217      )
218
219let find_label lbl s k = match find_label1 lbl s k with
220  | Some res -> res
221  | _ -> assert false (* should be impossible *)
222
223let rec select_switch i = function
224  | LSdefault d -> LSdefault d
225  | LScase (c,s,sl') when c=i-> LScase (c,s,sl') 
226  | LScase (_,_,sl') -> select_switch i sl'
227
228
229(* ctype functions *)
230
231let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
232
233let size_of_ctype = function
234  | Tint (I8, _)  -> 1
235  | Tint (I16, _) -> 2
236  | Tint (I32, _) -> 4
237  | Tfloat _ -> error_float ()
238  | Tcomp_ptr _
239  | Tpointer _
240  | Tarray _
241  | Tstruct _
242  | Tunion _ -> Mem.ptr_size
243  | _ -> assert false (* do not use on these arguments *)
244
245let is_function_type = function
246  | Tfunction _ -> true
247  | _ -> false
248
249let is_array_type = function
250  | Tarray _ -> true
251  | _ -> false
252
253let is_complex_type = function
254  | Tstruct _ | Tunion _ -> true
255  | _ -> false
256
257let is_big_type t = (is_array_type t) || (is_complex_type t)
258
259let dest_type = function
260  | Tpointer ty | Tarray (ty, _) -> ty
261  | _ -> assert false (* do not use on these arguments *)
262
263
264(* Global and local environment management *)
265
266let find_local x lenv =
267  if LocalEnv.mem x lenv then LocalEnv.find x lenv
268  else error ("Unknown local variable " ^ x ^ ".")
269
270let find_global x mem =
271  if Mem.mem_global mem x then Mem.find_global mem x
272  else error ("Unknown global variable " ^ x ^ ".")
273
274let find_symbol lenv mem x =
275  if LocalEnv.mem x lenv then LocalEnv.find x lenv
276  else
277    if Mem.mem_global mem x then Mem.find_global mem x
278    else error ("Unknown variable " ^ x ^ ".")
279
280let find_fundef f mem =
281  let addr = Mem.find_global mem f in
282  Mem.find_fun_def mem addr
283
284
285(* Interpret *)
286
287let byte_of_intsize = function
288  | I8 -> 1
289  | I16 -> 2
290  | I32 -> 4
291
292let choose_cast sign n m v =
293  let f = match sign with
294    | Signed -> Value.sign_ext
295    | Unsigned -> Value.zero_ext in
296  f v n m
297
298let eval_cast = function
299  (* Cast Integer *)
300  | (v,Tint(isize,sign),Tint(isize',_)) ->
301    choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
302  | (v,_,_) -> v
303
304let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
305
306let eval_unop ret_ctype ((_, t) as e) op =
307  let v = to_int32 e in
308  let v = match op with
309    | Onotbool -> Value.notbool v
310    | Onotint -> Value.notint v
311    | Oneg -> Value.negint v in
312  eval_cast (v, t, ret_ctype)
313
314let eval_add (v1,t1) (v2,t2) = match t1, t2 with
315  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
316    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
317    Value.add v1 v
318  | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
319    let v = Value.mul (Value.of_int (sizeof ty)) v1 in
320    Value.add v2 v
321  | _ -> Value.add v1 v2
322
323let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
324  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
325    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
326    Value.sub v1 v
327  | _ -> Value.sub v1 v2
328
329let choose_sign op_signed op_unsigned v1 v2 t =
330  let op = match t with
331    | Tint (_, Signed) -> op_signed
332    | Tint (_, Unsigned) -> op_unsigned
333    | _ -> op_unsigned in
334  op v1 v2
335
336let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op =
337  let v1 = to_int32 e1 in
338  let v2 = to_int32 e2 in
339  let e1 = (v1, t1) in
340  let e2 = (v2, t2) in
341  let v = match op with
342    | Oadd -> eval_add e1 e2
343    | Osub -> eval_sub e1 e2
344    | Omul -> Value.mul v1 v2
345    | Odiv -> choose_sign Value.div Value.divu v1 v2 t1
346    | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1
347    | Oand -> Value.and_op v1 v2
348    | Oor -> Value.or_op v1 v2
349    | Oxor -> Value.xor v1 v2
350    | Oshl-> Value.shl v1 v2
351    | Oshr-> Value.shr v1 v2
352    | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1
353    | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1
354    | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1
355    | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1
356    | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1
357    | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
358  eval_cast (v, t1, ret_ctype)
359
360let rec get_offset_struct v size id fields =
361  let offsets = fst (Mem.concrete_offsets_size size) in
362  let fields = List.combine (List.map fst fields) offsets in
363  let off = Value.of_int (List.assoc id fields) in
364  Value.add v off
365
366let get_offset v id = function
367  | Tstruct (_, fields) as t ->
368    let size = ClightToCminor.sizeof_ctype t in
369    get_offset_struct v size id fields
370  | Tunion _ -> v
371  | _ -> assert false (* do not use on these arguments *)
372
373let is_true (v, _) = Value.is_true v
374let is_false (v, _) = Value.is_false v
375
376let rec eval_expr localenv m c (Expr (ee, tt)) =
377  match ee with
378    | Econst_int i ->
379      let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
380      ((v, tt),[]) 
381    | Econst_float _ -> error_float ()
382    | Evar id when is_function_type tt || is_big_type tt ->
383      let v = value_of_address (find_symbol localenv m id) in
384      ((v, tt), [])
385    | Evar id ->
386      let addr = find_symbol localenv m id in
387      let v = Mem.load m (size_of_ctype tt) addr in
388      ((v, tt), [])
389    | Ederef e when is_function_type tt || is_big_type tt ->
390      let ((v1,_),l1) = eval_expr localenv m c e in
391      ((v1,tt),l1) 
392    | Ederef e ->
393      let ((v1,_),l1) = eval_expr localenv m c e in
394      let addr = address_of_value v1 in
395      let v = Mem.load m (size_of_ctype tt) addr in
396      ((v,tt),l1) 
397    | Eaddrof exp ->
398      let ((addr,_),l) = eval_lvalue localenv m c exp in
399      ((value_of_address addr,tt),l)
400    | Ebinop (op,exp1,exp2) -> 
401      let (v1,l1) = eval_expr localenv m c exp1 in
402      let (v2,l2) = eval_expr localenv m c exp2 in
403      ((eval_binop tt v1 v2 op,tt),l1@l2)
404    | Eunop (op,exp) -> 
405      let (e1,l1) = eval_expr localenv m c exp in
406      ((eval_unop tt e1 op,tt),l1)
407    | Econdition (e1,e2,e3) ->
408      let (v1,l1) = eval_expr localenv m c e1 in
409      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
410      else
411        if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3)
412      else (v1,l1)
413    | Eandbool (e1,e2) -> 
414      let (v1,l1) = eval_expr localenv m c e1 in
415      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
416      else (v1,l1)
417    | Eorbool (e1,e2) ->
418      let (v1,l1) = eval_expr localenv m c e1 in
419      if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
420      else (v1,l1)
421    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
422    | Efield (e1,id) -> 
423      let ((v1,t1),l1) = eval_expr localenv m c e1 in
424      let addr = address_of_value (get_offset v1 id t1) in
425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
426    | Ecost (lbl,e1) ->
427      (* applying current indexing on label *)
428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
429      let (v1,l1) = eval_expr localenv m c e1 in
430      (v1,lbl::l1)
431    | Ecall _ -> assert false (* only used by the annotation process *)
432    | Ecast (cty,exp) -> 
433      let ((v,ty),l1) = eval_expr localenv m c exp in
434      ((eval_cast (v,ty,cty),tt),l1)
435
436and eval_lvalue localenv m c (Expr (e,t)) = match e with
437  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 
438  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_) 
439  | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
440  | Evar id -> ((find_symbol localenv m id,t),[])
441  | Ederef ee ->
442    let ((v,_),l1) = eval_expr localenv m c ee in 
443    ((address_of_value v,t),l1)
444  | Efield (ee,id) ->
445    let ((v,tt),l1) = eval_expr localenv m c ee in 
446    let v' = get_offset v id tt in
447    ((address_of_value v', t), l1)
448  | Ecost (lbl,ee) ->
449    let (v,l) = eval_lvalue localenv m c ee in
450    (v,lbl::l)
451  | Ecall _ -> assert false (* only used in the annotation process *)
452
453let eval_exprlist lenv mem c es =
454  let f (vs, cost_lbls) e =
455    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
456    (vs @ [v], cost_lbls @ cost_lbls') in
457  List.fold_left f ([], []) es
458
459
460let bind (mem, lenv) (x, ty) v =
461  let (mem, addr) = Mem.alloc mem (sizeof ty) in
462  let mem = Mem.store mem (sizeof ty) addr v in
463  let lenv = LocalEnv.add x addr lenv in
464  (mem, lenv)
465
466let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
467
468let init_fun_env mem params args vars =
469  let lenv = LocalEnv.empty in
470  let (mem, lenv) =
471    try List.fold_left2 bind (mem, lenv) params args
472    with Invalid_argument _ -> error "wrong size of arguments." in
473  List.fold_left bind_var (mem, lenv) vars
474
475let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
476
477
478let free_local_env mem lenv =
479  let f _ addr mem = Mem.free mem addr in
480  LocalEnv.fold f lenv mem
481
482let condition v a_true a_false =
483  if Value.is_false v then a_false
484  else if Value.is_true v then a_true
485  else error "undefined condition guard value."
486
487let eval_stmt f k e m s c = match s, k with
488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
491    (* possibly continuing a loop *)
492    CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
493                                        will have no effect in the following. *) 
494    let ((v1,_),l1) = eval_expr e m c a in 
495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
496    let a_true = (State(f,s,k,e,m,c),l1) in
497    condition v1 a_true a_false
498  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
499    CostLabel.continue_loop_opt c i;
500    let ((v1,_),l1) = eval_expr e m c a2 in 
501    let a_false = (State(f,Sskip,k,e,m,c),l1) in
502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
503    condition v1 a_true a_false
504  | Sskip, Kfor2(i,a2,a3,s,k) ->
505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
507  | Sskip, Kcall _ -> 
508    let m' = free_local_env m e in
509    (Returnstate(Value.undef,k,m',c),[])
510  | Sassign(a1, a2), _ -> 
511    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
512    let ((v2,t2),l2) = eval_expr e m c a2 in
513    (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2)
514  | Scall(None,a,al), _ ->
515    let ((v1,_),l1) = eval_expr e m c a in 
516    let fd = Mem.find_fun_def m (address_of_value v1) in
517    let (vargs,l2) = eval_exprlist e m c al in
518    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
519  | Scall(Some lhs,a,al), _ ->
520    let ((v1,_),l1) = eval_expr e m c a in 
521    let fd = Mem.find_fun_def m (address_of_value v1) in
522    let (vargs,l2) = eval_exprlist e m c al in
523    let (vt3,l3) = eval_lvalue e m c lhs in
524    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
525  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
526  | Sifthenelse(a,s1,s2), _ -> 
527    let ((v1,_),l1) = eval_expr e m c a in 
528    let a_true = (State(f,s1,k,e,m,c),l1) in
529    let a_false = (State(f,s2,k,e,m,c),l1) in
530    condition v1 a_true a_false
531  | Swhile(i,a,s), _ ->
532    CostLabel.enter_loop_opt c i;
533    let ((v1,_),l1) = eval_expr e m c a in 
534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
535    let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in
536    condition v1 a_true a_false
537  | Sdowhile(i,a,s), _ ->
538    CostLabel.enter_loop_opt c i;
539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
540  | Sfor(i,Sskip,a2,a3,s), _ ->
541    CostLabel.enter_loop_opt c i;
542    let ((v1,_),l1) = eval_expr e m c a2 in 
543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
544    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
545    condition v1 a_true a_false
546  | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[])
547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
550  | Scontinue, Kseq(_,k)
551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
552  | Sreturn None, _ -> 
553    let m' = free_local_env m e in
554    (Returnstate(Value.undef,(call_cont k),m',c),[])
555  | Sreturn (Some a), _ -> 
556    let ((v1,_),l1) = eval_expr e m c a  in
557    let m' = free_local_env m e in
558    (Returnstate(v1,call_cont k,m',c),l1)
559  | Sswitch(a,sl), _ -> 
560    let ((v,_),l) = eval_expr e m c a in
561    let n = Value.to_int v in
562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
564  | Scost(lbl,s), _ ->
565    (* applying current indexing on label *)
566    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
567    (State(f,s,k,e,m,c),[lbl])
568  | Sgoto lbl, _ ->
569    (* if we exit an indexed loop, we don't care. It should not be possible to *)
570    (* enter an indexed loop that is not the current one, so we do nothing *)
571    (* to loop indexes *)
572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
573    (State(f,s',k',e,m,c),[])
574  | _ -> assert false (* should be impossible *)
575
576
577module InterpretExternal = Primitive.Interpret (Mem)
578
579let interpret_external k mem c f args =
580  let (mem', v) = match InterpretExternal.t mem f args with
581    | (mem', InterpretExternal.V vs) ->
582      let v = if List.length vs = 0 then Value.undef else List.hd vs in
583      (mem', v)
584    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
585  Returnstate (v, k, mem',c)
586
587let step_call args cont mem c = function
588  | Internal f -> 
589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
590    (* initializing loop indices *)
591    let c = CostLabel.new_const_ind c in
592    State (f, f.fn_body, cont, e, mem', c)
593  | External(id,targs,tres) when List.length targs = List.length args -> 
594    interpret_external cont mem c id args
595  | External(id,_,_) -> 
596    error ("wrong size of arguments when calling external " ^ id ^ ".")
597
598let step = function
599  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
601  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
602    let c = CostLabel.forget_const_ind c in
603    (State(f,Sskip,k,e,m,c),[])
604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) -> 
605    let c = CostLabel.forget_const_ind c in
606    let m' = assign m v ty vv in
607    (State(f,Sskip,k,e,m',c),[])
608  | _ -> error "state malformation."
609
610
611let data_of_init_data = function
612  | Init_int8 i         -> Data_int8 i
613  | Init_int16 i        -> Data_int16 i
614  | Init_int32 i        -> Data_int32 i
615  | Init_float32 f      -> error_float ()
616  | Init_float64 f      -> error_float ()
617  | Init_space i        -> error "bad global initialization style."
618  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
619
620let datas_of_init_datas = function
621  | [Init_space _] -> None
622  | l -> Some (List.map data_of_init_data l)
623
624let init_mem prog =
625  let f_var mem ((x, init_datas), ty) =
626    Mem.add_var mem x (ClightToCminor.sizeof_ctype ty)
627      (datas_of_init_datas init_datas) in
628  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
629  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
630  List.fold_left f_fun_def mem prog.prog_funct
631
632let compute_result v =
633  if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
634  else IntValue.Int32.zero
635
636let rec exec debug trace (state, l) =
637  let cost_labels = l @ trace in
638  let print_and_return_result res =
639    if debug then Printf.printf "Result = %s\n%!"
640      (IntValue.Int32.to_string res) ;
641    (res, List.rev cost_labels) in
642  if debug then print_state state ;
643  match state with
644    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
645      print_and_return_result (compute_result v)
646    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
647      print_and_return_result IntValue.Int32.zero
648    | state -> exec debug cost_labels (step state)
649
650let interpret debug prog =
651  Printf.printf "*** Clight interpret ***\n%!" ;
652  match prog.prog_main with
653    | None -> (IntValue.Int32.zero, [])
654    | Some main ->
655      let mem = init_mem prog in
656      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
657      exec debug [] first_state
Note: See TracBrowser for help on using the repository browser.