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

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

Deliverable D2.2

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