source: Deliverables/D2.3/8051/src/clight/clightInterpret.ml @ 453

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

Import of the Paris's sources.

File size: 27.3 KB
Line 
1module Mem = Driver.ClightMemory
2module Value = Driver.ClightMemory.Value
3module Valtbl = Hashtbl.Make(Value)
4
5open Clight
6open AST
7
8let warning msg = print_string ("Warning: "^msg^" (clightInterpret.ml)\n")
9
10type localEnv = (ident,Value.t) Hashtbl.t
11
12type continuation =
13  | Kstop
14  | Kseq of statement*continuation
15  | Kwhile of expr*statement*continuation
16  | Kdowhile of expr*statement*continuation
17  | Kfor2 of expr*statement*statement*continuation
18  | Kfor3 of expr*statement*statement*continuation
19  | Kswitch of continuation
20  | Kcall of (Value.t*ctype) option*cfunction*localEnv*continuation
21
22type state =
23  | State of cfunction*statement*continuation*localEnv*(fundef Mem.memory)
24  | Callstate of fundef*Value.t list*continuation*(fundef Mem.memory)
25  | Returnstate of Value.t*continuation*(fundef Mem.memory)
26
27(* ctype functions *)
28
29let rec sizeof = function
30  | Tvoid               -> 0
31  | Tint (I8,_)         -> 1
32  | Tint (I16,_)        -> 2
33  | Tint (I32,_)        -> 4
34  | Tfloat _            -> assert false (* Not supported *)
35  | Tpointer _          -> Mem.ptr_size
36  | Tarray (t,s)        -> s*(sizeof t)                   
37  | Tfunction (_,_)     -> assert false (* Not supported *) 
38  | Tstruct (_,lst)     -> 
39      List.fold_left
40        (fun n (_,ty) -> (fun a b -> a+b) n (sizeof ty)) 0 lst
41  | Tunion (_,lst)      -> 
42      List.fold_left
43        (fun n (_,ty)   -> 
44           let sz = (sizeof ty) in (if n>sz then n else sz)
45        ) 0 lst
46  | Tcomp_ptr _         -> Mem.ptr_size
47
48let rec mq_of_ty = function
49  | Tvoid               -> assert false
50  | Tint (I8,Signed)    -> Memory.MQ_int8signed 
51  | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
52  | Tint (I16,Signed)   -> Memory.MQ_int16signed
53  | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
54  | Tint (I32,Signed)   -> Memory.MQ_int32
55  | Tint (I32,Unsigned) -> assert false (* Not supported *)
56  | Tfloat _            -> assert false (* Not supported *)
57  | Tpointer _          -> Mem.mq_of_ptr
58  | Tarray (c,s)        -> Mem.mq_of_ptr
59  | Tfunction (_,_)     -> assert false (* Not supported *)
60  | Tstruct (_,_)       -> Mem.mq_of_ptr
61  | Tunion (_,_)        -> Mem.mq_of_ptr
62  | Tcomp_ptr _         -> Mem.mq_of_ptr
63
64(* Pretty printing for Clight states *)
65
66let string_s = function 
67  | Sskip                               -> "skip"
68  | Sassign (Expr (Evar id,_),_)        -> "assign "^id
69  | Sassign (_,_)                       -> "assign"
70  | Scall (_,_,_)                       -> "call"
71  | Ssequence (_,_)                     -> "seq"
72  | Sifthenelse (_,_,_)                 -> "ifthenelse"
73  | Swhile (_,_)                        -> "while"
74  | Sdowhile (_,_)                      -> "dowhile"
75  | Sfor (_,_,_,_)                      -> "for"
76  | Sbreak                              -> "break"
77  | Scontinue                           -> "continue"
78  | Sreturn _                           -> "return"
79  | Sswitch (_,_)                       -> "switch"
80  | Slabel (_,_)                        -> "label"
81  | Sgoto _                             -> "goto"
82  | Scost (_,_)                         -> "cost"
83
84let string_f = function
85  | Internal _          -> "func"
86  | External (id,_,_)   -> id
87
88let string_c = function
89  | Kstop               -> "stop"
90  | Kseq (_,_)          -> "seq"
91  | Kwhile (_,_,_)      -> "while"
92  | Kdowhile (_,_,_)    -> "dowhile"
93  | Kfor2 (_,_,_,_)     -> "for2"
94  | Kfor3 (_,_,_,_)     -> "for3"
95  | Kswitch _           -> "switch"
96  | Kcall (_,_,_,_)     -> "call"
97
98let string_of_state = function
99  | State (_,s,c,_,_) -> "Regular("^(string_s s)^","^(string_c c)^")"
100  | Callstate (f,_,c,_) -> "Call("^(string_f f)^","^(string_c c)^")"
101  | Returnstate (v,c,_) -> 
102      "Return("^(Value.to_string v)^","^(string_c c)^")"
103
104(* Global and local environment management *)
105
106let find_funct_id g id = 
107  try Valtbl.find (snd g) (Hashtbl.find (fst g) id)
108  with Not_found -> assert false
109
110let find_funct g v = 
111  try Valtbl.find (snd g) (fst v) 
112  with Not_found -> assert false
113
114let find_symbol globalenv localenv id =
115  try Hashtbl.find localenv id
116  with Not_found -> (
117    try Hashtbl.find (fst globalenv) id
118    with Not_found -> assert false
119  )
120
121(* Continuations and labels *)
122
123let rec call_cont = function
124  | Kseq (_,k)          -> call_cont k
125  | Kwhile (_,_,k)      -> call_cont k
126  | Kdowhile (_,_,k)    -> call_cont k
127  | Kfor2 (_,_,_,k)     -> call_cont k
128  | Kfor3 (_,_,_,k)     -> call_cont k
129  | Kswitch k           -> call_cont k
130  | k                   -> k
131
132let is_call_cont = function
133  | Kstop | Kcall (_,_,_,_) -> true
134  | _ -> false
135
136let rec seq_of_labeled_statement = function
137  | LSdefault s -> s
138  | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
139
140let rec select_switch i = function
141  | LSdefault d -> LSdefault d
142  | LScase (c,s,sl') when c=i-> LScase (c,s,sl') 
143  | LScase (_,_,sl') -> select_switch i sl'
144
145let rec find_label lbl s k = match s with
146   | Ssequence (s1,s2) ->
147      (match find_label lbl s1 (Kseq (s2,k)) with
148      | Some sk -> Some sk
149      | None -> find_label lbl s2 k
150      )
151  | Sifthenelse (a,s1,s2) ->
152      (match find_label lbl s1 k with
153      | Some sk -> Some sk
154      | None -> find_label lbl s2 k
155      )
156  | Swhile (a,s1) -> find_label lbl s1 (Kwhile(a,s1,k))
157  | Sdowhile (a,s1) -> find_label lbl s1 (Kdowhile(a,s1,k))
158  | Sfor (a1,a2,a3,s1) ->
159      (match find_label lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
160      | Some sk -> Some sk
161      | None ->
162          (match find_label lbl s1 (Kfor2(a2,a3,s1,k)) with
163          | Some sk -> Some sk
164          | None -> find_label lbl a3 (Kfor3(a2,a3,s1,k))
165          ))
166  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
167  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label lbl s' k
168  | Scost (_,s') -> find_label lbl s' k
169  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak 
170  | Scontinue | Sreturn _ | Sgoto _ -> None
171           
172and find_label_ls lbl sl k =  match sl with
173  | LSdefault s -> find_label lbl s k
174  | LScase (_,s,sl') ->
175      (match find_label lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
176      | Some sk -> Some sk
177      | None -> find_label_ls lbl sl' k
178      )
179
180(* Interpret *)
181
182let is_int_type = function
183  | Tint (_,_)    -> true
184  | _ -> false
185let is_float_type = function
186  | Tfloat _  -> true
187  | _ -> false
188let is_pointer_type = function
189  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) 
190  | Tunion (_,_) | Tcomp_ptr _ -> true
191  | _ -> false 
192
193let eval_cast = function 
194  (* no cast *)
195  | (e,a,b) when a=b                            -> e
196  (* Cast Integer *)
197  | (v,_,Tint(I8,Signed))                       -> Value.cast8signed v
198  | (v,_,Tint(I8,Unsigned))                     -> Value.cast8unsigned v
199  | (v,_,Tint(I16,Signed))                      -> Value.cast16signed v
200  | (v,_,Tint(I16,Unsigned))                    -> Value.cast16unsigned v
201  | (v,_,Tint(I32,Signed)) when Value.is_int v  -> v
202  | (v,_,Tint(I32,Unsigned))                    -> assert false(*Not supported*)
203  (* Cast float*)
204  | (v,_,Tfloat _)                              -> assert false(*Not supported*)
205  (* Cast pointeur *)
206  | (v,Tarray(_,_),Tpointer _)                  -> v
207  | (v,Tpointer _,Tarray(_,_))                  -> v
208  | (v,Tpointer _,Tpointer _)                   -> v
209  | (v,Tarray (_,_),Tarray(_,_))                -> v
210  (*Struct and pointer to struct FIXME: is it correct ?*)
211  | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v
212  | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v
213  (*Union and pointer to union FIXME: is it correct ?*)
214  | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v
215  | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v
216  (* error *)
217  | (e,_,_)                                     -> 
218      warning "eval_cast";Value.undef
219
220let eval_unop (v,t) = function 
221  | Onotbool when is_int_type t -> Value.notbool v
222  | Onotint when is_int_type t  -> Value.notint v
223  | Oneg when is_int_type t     -> Value.negint v
224  | Oneg when is_float_type t   -> assert false (*Not supported*)
225  | _                           -> assert false (*Type error*)
226
227let get_subtype = function
228  | Tarray(t,_) -> t
229  | Tpointer t -> t
230  | _ -> assert false (*Misuse of get_subtype*)
231
232let eval_add = function
233  (*Integer*)
234  | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 
235      let v = Value.add v1 v2 in 
236        (match t1 with
237           | Tint(I8,Signed)    -> Value.cast8signed v
238           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
239           | Tint(I16,Signed)   -> Value.cast16signed v
240           | Tint(I16,Unsigned) -> Value.cast16unsigned v
241           | Tint(I32,Signed)   -> v
242           | Tint(I32,Unsigned) -> assert false (*Not supported*)
243           | _                  -> assert false (*Prevented by is_int_type*))
244  (*Float*)
245  | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 -> 
246      assert false (*Not supported*)
247  (*Pointer*)
248  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
249      Value.add v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
250  | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
251      Value.add v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
252  (*Error*)
253  | _ -> assert false (*Type error*) 
254
255let eval_sub = function
256  (*Integer*)
257  | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 
258      let v = Value.sub v1 v2 in
259        (match t1 with
260           | Tint(I8,Signed)    -> Value.cast8signed v
261           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
262           | Tint(I16,Signed)   -> Value.cast16signed v
263           | Tint(I16,Unsigned) -> Value.cast16unsigned v
264           | Tint(I32,Signed)   -> v
265           | Tint(I32,Unsigned) -> assert false (*Not supported*)
266           | _                  -> assert false (*Prevented by is_int_type*))
267  (*Float*)
268  | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
269      assert false (*Not supported*)
270  (*Pointer*)
271  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
272      Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
273  | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
274      Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
275  (*Error*)
276  | _ -> assert false (*Type error*)
277
278let eval_mul = function
279  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 
280      let v = Value.mul v1 v2 in 
281        (match t1 with
282           | Tint(I8,Signed)    -> Value.cast8signed v
283           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
284           | Tint(I16,Signed)   -> Value.cast16signed v
285           | Tint(I16,Unsigned) -> Value.cast16unsigned v
286           | Tint(I32,Signed)   -> v
287           | Tint(I32,Unsigned) -> assert false (*Not supported*)
288           | _                  -> assert false (*Prevented by is_int_type*))   
289  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 
290      assert false (*Not supported*)
291  | _ -> assert false (*Type error*)
292
293let eval_mod = function
294  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 
295      Value.modulo v1 v2
296  | _ -> assert false (*Type error*)
297
298let eval_div = function
299  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2
300  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 
301      assert false (*Not supported*)
302  | _ -> assert false (*Type error*)
303
304let eval_and = function
305  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2
306  | _ -> assert false (*Type error*)
307
308let eval_or = function
309  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2
310  | _ -> assert false (*Type error*)
311
312let eval_xor = function
313  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2
314  | _ -> assert false (*Type error*)
315
316let eval_shl = function         
317  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.shl v1 v2
318  | _ -> assert false (*Type error*)
319
320let eval_shr = function         
321  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.shr v1 v2
322  | _ -> assert false (*Type error*)
323
324let eval_eq = function
325  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2
326  | _ -> assert false (*Type error*)
327           
328let eval_ne = function
329  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2
330  | _ -> assert false (*Type error*)
331
332let eval_lt = function
333  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2
334  | _ -> assert false (*Type error*)
335
336let eval_gt = function
337  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2
338  | _ -> assert false (*Type error*)
339
340let eval_le = function
341  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2
342  | _ -> assert false (*Type error*)
343
344let eval_ge = function
345  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2
346  | _ -> assert false (*Type error*)
347
348let eval_binop e1 e2 = function
349  | Oadd -> eval_add (e1,e2)
350  | Osub -> eval_sub (e1,e2)
351  | Omul -> eval_mul (e1,e2)
352  | Odiv -> eval_div (e1,e2)
353  | Omod -> eval_mod (e1,e2)
354  | Oand -> eval_and (e1,e2)
355  | Oor -> eval_or (e1,e2)
356  | Oxor-> eval_xor (e1,e2)
357  | Oshl-> eval_shl (e1,e2)
358  | Oshr-> eval_shr (e1,e2)
359  | Oeq -> eval_eq (e1,e2)
360  | One -> eval_ne (e1,e2)
361  | Olt -> eval_lt (e1,e2)
362  | Ogt -> eval_gt (e1,e2)
363  | Ole -> eval_le (e1,e2)
364  | Oge -> eval_ge (e1,e2)
365
366let rec get_offset_struct v id = function
367  | [] -> assert false (*Wrong id*)
368  | (fi,_)::_ when fi=id -> v
369  | (_,ty)::ll -> get_offset_struct
370                    (Value.add v (Value.of_int (sizeof ty))) id ll
371
372let is_true (v,_) = Value.is_true v
373
374let is_false (v,_) = Value.is_false v
375
376let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in
377  match ee with
378    | Econst_int i -> 
379        let v = (match tt with
380                   | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i)
381                   | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i)
382                   | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i)
383                   | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i)
384                   | Tint(I32,Signed) -> Value.of_int i
385                   | Tint(I32,Unsigned) -> assert false (*Not supported*) 
386                   | _ -> assert false (*Type error*))
387      in ((v,tt),[]) 
388    | Econst_float _ -> assert false (*Not supported *)
389    | Evar id   -> 
390        (match tt with 
391           | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[])
392           | _ -> 
393               ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[]) 
394        )
395    | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in 
396        ((Mem.load m (mq_of_ty tt) v1,tt),l1) 
397    | Eaddrof exp -> eval_lvalue globalenv localenv m exp
398    | Eunop (op,exp) -> 
399        let (v1,l1) = eval_expr globalenv localenv m exp in
400          ((eval_unop v1 op,tt),l1)
401    | Ebinop (op,exp1,exp2) -> 
402        let (v1,l1) = eval_expr globalenv localenv m exp1
403        and (v2,l2) = eval_expr globalenv localenv m exp2 in
404          ((eval_binop v1 v2 op,tt),l1@l2)
405    | Ecast (cty,exp) -> 
406        let ((v,ty),l1) = eval_expr globalenv localenv m exp in
407          ((eval_cast (v,ty,cty),tt),l1)
408    | Econdition (e1,e2,e3) ->
409        let (v1,l1) = eval_expr globalenv localenv m e1 in
410          if is_true v1 then
411            let (v2,l2) = eval_expr globalenv localenv m e2 in
412              (v2,l1@l2)
413          else if is_false v1 then
414            let (v2,l2) = eval_expr globalenv localenv m e3 in
415              (v2,l1@l2)
416          else ((Value.undef,tt),l1)
417    | Eandbool (e1,e2) -> 
418        let (v1,l1) = eval_expr globalenv localenv m e1 in
419          if is_true v1 then (
420            let (v2,l2) = eval_expr globalenv localenv m e2 in
421              if is_true v2 then 
422                ((Value.val_true,tt),l1@l2)
423              else (
424                if is_false v2 then ((Value.val_false,tt),l1@l2)
425                else ((Value.undef,tt),l1@l2)
426              )) else (
427                if is_false v1 then ((Value.val_false,tt),l1)
428                else ((Value.undef,tt),l1))
429    | Eorbool (e1,e2) ->
430        let (v1,l1) = eval_expr globalenv localenv m e1 in
431          if is_false v1 then (
432            let (v2,l2) = eval_expr globalenv localenv m e2 in
433              if is_true v2 then ((Value.val_true,tt),l1@l2)
434              else ( 
435                if is_false v2 then ((Value.val_false,tt),l1@l2)
436                else ((Value.undef,tt),l1@l2)
437          )) else ( 
438            if is_true v1 then ((Value.val_true,tt),l1)
439            else ((Value.undef,tt),l1))
440    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
441    | Efield (e1,id) -> 
442        let (v1,l1) = eval_expr globalenv localenv m e1 in
443        (match v1 with
444           | (v,Tstruct(_,lst)) when List.mem (id,tt) lst -> 
445               ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1)
446           | (v,Tunion(_,lst)) when List.mem (id,tt) lst -> 
447               ((Mem.load m (mq_of_ty tt) v,tt),l1)
448           | _ -> ((Value.undef,tt),l1)
449        )
450    | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in
451        (v1,lbl::l1)
452    | Ecall _ -> assert false (*For annotations only*)
453
454and eval_lvalue globalenv localenv m expr = 
455  let Expr (e,t) = expr in match e with
456    | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 
457    | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_) 
458    | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
459    | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in 
460        (match v1 with 
461           | (v,Tstruct(_,lst)) when List.mem (id,t) lst -> 
462               ((get_offset_struct v id lst,t),l1) 
463           | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1)
464           | _ -> ((Value.undef,t),l1)
465        )
466    | Evar id -> ((find_symbol globalenv localenv id,t),[])
467    | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in 
468        ((v,t),l1)
469    | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in
470        (v,lbl::l)
471    | Ecall _ -> assert false (*For annotation only*)
472
473let eval_exprlist globalenv localenv m l =
474  let rec eval_exprlist_rec vl ll = function
475    | [] -> (vl,ll)
476    | e::lst -> 
477        let (vl0,ll0) = eval_exprlist_rec vl ll lst
478        and ((v,_),t) = eval_expr globalenv localenv m e in 
479        (v::vl0,t@ll0)
480  in eval_exprlist_rec [] [] l
481
482let is_struct = function
483  | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
484  | _ -> false
485
486let bind_parameters m param_l arg_l var_l = 
487 let bind (m,e) (id,ty) arg = 
488   if is_struct ty then (
489     assert (arg=Value.undef); (*a parameter can't be a struct/union/array*)
490     let (m2,ptr2) = Mem.alloc m (sizeof ty)
491     in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size)
492     in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2
493     in (m4, (Hashtbl.add e id ptr3;e) ))
494   else 
495     let (m2,ptr) = Mem.alloc m (sizeof ty) in
496     let m3 = Mem.store m2 (mq_of_ty ty) ptr arg
497     in (m3, (Hashtbl.add e id ptr;e) )
498 in 
499   List.fold_left
500     (fun a b -> bind a b Value.undef) 
501     (List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l)
502     var_l
503
504let assign m v ty ptr = Mem.store m (mq_of_ty ty) ptr v
505
506
507let type_of_fundef = function
508  | Internal f -> Tfunction (List.map snd f.fn_params,f.fn_return)
509  | External (_,p,t) -> Tfunction (p,t)
510
511let rec free_list m = function
512  | [] -> m
513  | v::l -> free_list (Mem.free m v) l
514
515let blocks_of_env e =
516  let l = ref [] in
517    Hashtbl.iter (fun _ b -> l:=b::(!l)) e;!l
518
519let typeof e = let Expr (_,t) = e in t
520
521let interpret_external vargs k m = function
522    | "scan_int" ->
523          Returnstate (Value.of_int (int_of_string (read_line ())), k, m)
524    | "print_int" when List.length vargs = 1 ->
525        Printf.printf "%d" (Value.to_int (List.hd vargs)) ;
526        Returnstate (Value.zero, k, m)
527    | "print_intln" when List.length vargs = 1 ->
528        Printf.printf "%d\n" (Value.to_int (List.hd vargs)) ;
529        Returnstate (Value.zero, k, m)
530    | "alloc" when List.length vargs = 1 -> 
531        let (m',vv) = Mem.alloc m (Value.to_int (List.hd vargs)) in 
532          Returnstate (vv, k, m')
533    | _ -> assert false (*Unknown external function*)
534
535let next_step globalenv = function
536    | State(f,Sassign(a1,a2),k,e,m) -> 
537        let ((v1,t1),l1) = (eval_lvalue globalenv e m a1)
538        and ((v2,t2),l2) = eval_expr globalenv e m a2
539        in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
540    | State(f,Scall(None,a,al),k,e,m) ->
541        let (v1,l1) = eval_expr globalenv e m a in 
542        let fd = find_funct globalenv v1
543        and (vargs,l2) = (eval_exprlist globalenv e m al) in
544          if type_of_fundef fd = typeof a
545          then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
546          else assert false (*Signature mismatches*)
547  | State(f,Scall(Some lhs,a,al),k,e,m) ->
548      let (v1,l1) = eval_expr globalenv e m a in 
549      let fd = find_funct globalenv v1
550      and (vargs,l2) = (eval_exprlist globalenv e m al)
551      and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in
552        if type_of_fundef fd = typeof a then 
553          (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3)
554        else assert false (*Signature mismatches*) 
555  | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[])
556  | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[])
557  | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[])
558  | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[])
559  | State(f,Sifthenelse(a,s1,s2),k,e,m) -> 
560      let (v1,l1) = eval_expr globalenv e m a in 
561        if is_true v1 then (State(f,s1,k,e,m),l1)
562        else if is_false v1 then (State(f,s2,k,e,m),l1)
563        else assert false (*Wrong condition guard*)
564  | State(f,Swhile(a,s),k,e,m) ->
565      let (v1,l1) = eval_expr globalenv e m a in 
566        if is_false v1 then (State(f,Sskip,k,e,m),l1)
567        else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1)
568        else assert false (*Wrong condition guard*)
569  | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
570  | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
571  | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
572  | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[])
573  | State(f,Sskip,Kdowhile(a,s,k),e,m) ->
574      let (v1,l1) = eval_expr globalenv e m a in 
575        if is_false v1 then (State(f,Sskip,k,e,m),l1)
576        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
577        else assert false (*Wrong condition guard*)
578  | State(f,Scontinue,Kdowhile(a,s,k),e,m) ->
579      let (v1,l1) = eval_expr globalenv e m a in 
580        if is_false v1 then (State(f,Sskip,k,e,m),l1)
581        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
582        else assert false (*Wrong condition guard*)
583  | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
584  | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip ->
585      (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
586  | State(f,Sfor(Sskip,a2,a3,s),k,e,m) ->
587      let (v1,l1) = eval_expr globalenv e m a2 in 
588      if is_false v1 then (State(f,Sskip,k,e,m),l1)
589      else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1)
590      else assert false (*Wrong condition guard*)
591  | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
592  | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) ->
593      (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
594  | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
595  | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) ->
596      (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
597  | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid -> 
598      let m' = free_list m (blocks_of_env e) in
599        (Returnstate(Value.undef,(call_cont k),m'),[])
600  | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid -> 
601      let (v1,l1) = eval_expr globalenv e m a
602      and m' = free_list m (blocks_of_env e) in
603        (Returnstate(fst v1,call_cont k,m'),l1)
604  | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k -> 
605      let m' = free_list m (blocks_of_env e) in
606        (Returnstate(Value.undef,k,m'),[])
607  | State(f,Sswitch(a,sl),k,e,m) -> 
608      let (n,l) = (match eval_expr globalenv e m a with 
609                     | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll) 
610                     | _ -> assert false (*Wrong switch index*)
611      ) in 
612        (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
613  | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
614  | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
615  | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[])
616  | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[])
617  | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl])
618  | State(f,Sgoto lbl,k,e,m) -> 
619      (match find_label lbl f.fn_body (call_cont k) with 
620         | Some (s',k') -> (State(f,s',k',e,m),[])
621         | None -> assert false (*Label does not exist*))
622  | Callstate(Internal f,vargs,k,m) -> 
623      let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in
624        (State(f,f.fn_body,k,e,m'),[])
625  | Callstate(External(id,targs,tres),vargs,k,m) 
626      when List.length targs = List.length vargs -> 
627      (interpret_external vargs k m id,[])
628  | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
629  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) -> 
630      let m' = assign m v ty vv in
631        (State(f,Sskip,k,e,m'),[])
632  | _ -> assert false
633
634let init_to_data = function
635  | Init_int8 i         -> Data_int8 i
636  | Init_int16 i        -> Data_int16 i
637  | Init_int32 i        -> Data_int32 i
638  | Init_float32 f      -> assert false (* Not supported *)
639  | Init_float64 f      -> assert false (* Not supported *)
640  | Init_space i        -> Data_reserve i
641  | Init_addrof (_,_)   -> assert false (*FIXME what is this ?*)
642
643let alloc_datas m ((_,lst),ty) = 
644  let store_data (m,ptr) = function (*FIXME signed ?*)
645    | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
646                       ,Value.add ptr (Value.of_int 1))
647    | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
648                       ,Value.add ptr (Value.of_int 2))
649    | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
650                       ,Value.add ptr (Value.of_int 4))
651    | Init_float32 _ -> assert false (*Not supported*)
652    | Init_float64 _ -> assert false (*Not supported*)
653    | Init_space n -> (m,Value.add ptr (Value.of_int n))
654    | Init_addrof (_,_) -> assert false (*FIXME what is this ?*) 
655  in let (m2,ptr) = (Mem.alloc m (sizeof ty))
656  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
657
658let initmem_clight prog =
659  let alloc_funct i (g,f) (id,fct) = 
660    Hashtbl.add g id (Value.of_int (-i-1));
661    Valtbl.add f (Value.of_int (-i-1)) fct;
662    (g,f)
663  and alloc_var (m,g) v =
664    let (m',ptr) = alloc_datas m v in
665      if is_struct (snd v) then
666        let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in 
667        let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
668        Hashtbl.add g (fst (fst v)) ptr2;(m3,g) 
669      else 
670        ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
671  in let (m,g) = 
672    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
673  in let (g2,f) = 
674    MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct
675  in 
676    (m,(g2,f))
677
678let interpret debug prog = match prog.prog_main with
679  | None -> []
680  | Some main ->
681      let (m,g) = initmem_clight prog in
682      let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in
683      let rec exec trace = function
684        | (Returnstate(v,Kstop,m),l) -> 
685            if debug then (
686              print_string ("Result: "^(Value.to_string v));
687              print_string ("\nMemory dump: \n");
688              Mem.print m
689            );
690            l@trace
691        | (state,l) ->
692            if debug then print_string ((string_of_state state)^"\n");
693            exec (l@trace) (next_step g state)
694      in 
695      if debug then print_string "> --- Interpret Clight --- <\n";
696      exec [] first_state
Note: See TracBrowser for help on using the repository browser.