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

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

Update of D2.2 from Paris.

File size: 28.1 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.mul v2 (Value.of_int (sizeof (get_subtype t1))))
251  | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
252      Value.add v1 (Value.mul v2 (Value.of_int (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.mul v2 (Value.of_int (sizeof (get_subtype t1))))
274  (*Error*)
275  | _ -> assert false (*Type error*)
276
277let eval_mul = function
278  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 
279      let v = Value.mul v1 v2 in 
280        (match t1 with
281           | Tint(I8,Signed)    -> Value.cast8signed v
282           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
283           | Tint(I16,Signed)   -> Value.cast16signed v
284           | Tint(I16,Unsigned) -> Value.cast16unsigned v
285           | Tint(I32,Signed)   -> v
286           | Tint(I32,Unsigned) -> v (*FIXME*)
287           | _                  -> assert false (*Prevented by is_int_type*))   
288  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 
289      assert false (*Not supported*)
290  | _ -> assert false (*Type error*)
291
292let eval_mod = function
293  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 
294      Value.modulo v1 v2
295  | _ -> assert false (*Type error*)
296
297let eval_div = function
298  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2
299  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 
300      assert false (*Not supported*)
301  | _ -> assert false (*Type error*)
302
303let eval_and = function
304  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2
305  | _ -> assert false (*Type error*)
306
307let eval_or = function
308  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2
309  | _ -> assert false (*Type error*)
310
311let eval_xor = function
312  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2
313  | _ -> assert false (*Type error*)
314
315let eval_shl = function         
316  | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shl v1 v2
317  | _ -> assert false (*Type error*)
318
319let eval_shr = function         
320  | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shr v1 v2
321  | _ -> assert false (*Type error*)
322
323let eval_eq = function
324  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2
325  | _ -> assert false (*Type error*)
326           
327let eval_ne = function
328  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2
329  | _ -> assert false (*Type error*)
330
331let eval_lt = function
332  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2
333  | _ -> assert false (*Type error*)
334
335let eval_gt = function
336  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2
337  | _ -> assert false (*Type error*)
338
339let eval_le = function
340  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2
341  | _ -> assert false (*Type error*)
342
343let eval_ge = function
344  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2
345  | _ -> assert false (*Type error*)
346
347let eval_binop e1 e2 = function
348  | Oadd -> eval_add (e1,e2)
349  | Osub -> eval_sub (e1,e2)
350  | Omul -> eval_mul (e1,e2)
351  | Odiv -> eval_div (e1,e2)
352  | Omod -> eval_mod (e1,e2)
353  | Oand -> eval_and (e1,e2)
354  | Oor -> eval_or (e1,e2)
355  | Oxor-> eval_xor (e1,e2)
356  | Oshl-> eval_shl (e1,e2)
357  | Oshr-> eval_shr (e1,e2)
358  | Oeq -> eval_eq (e1,e2)
359  | One -> eval_ne (e1,e2)
360  | Olt -> eval_lt (e1,e2)
361  | Ogt -> eval_gt (e1,e2)
362  | Ole -> eval_le (e1,e2)
363  | Oge -> eval_ge (e1,e2)
364
365let rec get_offset_struct v id = function
366  | [] -> assert false (*Wrong id*)
367  | (fi,_)::_ when fi=id -> v
368  | (_,ty)::ll -> get_offset_struct
369                    (Value.add v (Value.of_int (sizeof ty))) id ll
370
371let is_true (v,_) = Value.is_true v
372
373let is_false (v,_) = Value.is_false v
374
375let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in
376  match ee with
377    | Econst_int i -> 
378        let v = (match tt with
379                   | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i)
380                   | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i)
381                   | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i)
382                   | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i)
383                   | Tint(I32,Signed) -> Value.of_int i
384                   | Tint(I32,Unsigned) -> Value.of_int i (*FIXME*) 
385                   | _ -> assert false (*Type error*))
386      in ((v,tt),[]) 
387    | Econst_float _ -> assert false (*Not supported *)
388    | Evar id   -> 
389        (match tt with 
390           | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[])
391           | _ -> 
392               ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[]) 
393        )
394    | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in 
395        ((Mem.load m (mq_of_ty tt) v1,tt),l1) 
396    | Eaddrof exp -> eval_lvalue globalenv localenv m exp
397    | Eunop (op,exp) -> 
398        let (v1,l1) = eval_expr globalenv localenv m exp in
399          ((eval_unop v1 op,tt),l1)
400    | Ebinop (op,exp1,exp2) -> 
401        let (v1,l1) = eval_expr globalenv localenv m exp1
402        and (v2,l2) = eval_expr globalenv localenv m exp2 in
403          ((eval_binop v1 v2 op,tt),l1@l2)
404    | Ecast (cty,exp) -> 
405        let ((v,ty),l1) = eval_expr globalenv localenv m exp in
406          ((eval_cast (v,ty,cty),tt),l1)
407    | Econdition (e1,e2,e3) ->
408        let (v1,l1) = eval_expr globalenv localenv m e1 in
409          if is_true v1 then
410            let (v2,l2) = eval_expr globalenv localenv m e2 in
411              (v2,l1@l2)
412          else if is_false v1 then
413            let (v2,l2) = eval_expr globalenv localenv m e3 in
414              (v2,l1@l2)
415          else ((Value.undef,tt),l1)
416    | Eandbool (e1,e2) -> 
417        let (v1,l1) = eval_expr globalenv localenv m e1 in
418          if is_true v1 then (
419            let (v2,l2) = eval_expr globalenv localenv m e2 in
420              if is_true v2 then 
421                ((Value.val_true,tt),l1@l2)
422              else (
423                if is_false v2 then ((Value.val_false,tt),l1@l2)
424                else ((Value.undef,tt),l1@l2)
425              )) else (
426                if is_false v1 then ((Value.val_false,tt),l1)
427                else ((Value.undef,tt),l1))
428    | Eorbool (e1,e2) ->
429        let (v1,l1) = eval_expr globalenv localenv m e1 in
430          if is_false v1 then (
431            let (v2,l2) = eval_expr globalenv localenv m e2 in
432              if is_true v2 then ((Value.val_true,tt),l1@l2)
433              else ( 
434                if is_false v2 then ((Value.val_false,tt),l1@l2)
435                else ((Value.undef,tt),l1@l2)
436          )) else ( 
437            if is_true v1 then ((Value.val_true,tt),l1)
438            else ((Value.undef,tt),l1))
439    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
440    | Efield (e1,id) -> 
441        let (v1,l1) = eval_expr globalenv localenv m e1 in
442        (match v1 with
443           | (v,Tstruct(_,lst)) when List.mem (id,tt) lst -> 
444               ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1)
445           | (v,Tunion(_,lst)) when List.mem (id,tt) lst -> 
446               ((Mem.load m (mq_of_ty tt) v,tt),l1)
447           | _ -> ((Value.undef,tt),l1)
448        )
449    | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in
450        (v1,lbl::l1)
451    | Ecall _ -> assert false (*For annotations only*)
452
453and eval_lvalue globalenv localenv m expr = 
454  let Expr (e,t) = expr in match e with
455    | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 
456    | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_) 
457    | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
458    | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in 
459        (match v1 with 
460           | (v,Tstruct(_,lst)) when List.mem (id,t) lst -> 
461               ((get_offset_struct v id lst,t),l1) 
462           | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1)
463           | _ -> ((Value.undef,t),l1)
464        )
465    | Evar id -> ((find_symbol globalenv localenv id,t),[])
466    | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in 
467        ((v,t),l1)
468    | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in
469        (v,lbl::l)
470    | Ecall _ -> assert false (*For annotation only*)
471
472let eval_exprlist globalenv localenv m l =
473  let rec eval_exprlist_rec vl ll = function
474    | [] -> (vl,ll)
475    | e::lst -> 
476        let (vl0,ll0) = eval_exprlist_rec vl ll lst
477        and ((v,_),t) = eval_expr globalenv localenv m e in 
478        (v::vl0,t@ll0)
479  in eval_exprlist_rec [] [] l
480
481let is_struct = function
482  | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
483  | _ -> false
484
485let bind_parameters m param_l arg_l var_l = 
486 let bind (m,e) (id,ty) arg = 
487   if is_struct ty then (
488     assert (arg=Value.undef); (*a parameter can't be a struct/union/array*)
489     let (m2,ptr2) = Mem.alloc m (sizeof ty)
490     in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size)
491     in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2
492     in (m4, (Hashtbl.add e id ptr3;e) ))
493   else 
494     let (m2,ptr) = Mem.alloc m (sizeof ty) in
495     let m3 = Mem.store m2 (mq_of_ty ty) ptr arg
496     in (m3, (Hashtbl.add e id ptr;e) )
497 in 
498   List.fold_left
499     (fun a b -> bind a b Value.undef) 
500     (try List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l
501     with (Invalid_argument _) -> assert false)
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    | "malloc" | "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   | "exit"  when List.length vargs = 1 -> Returnstate(List.hd vargs,Kstop,m)
534   | s -> Printf.eprintf "Error: unknown external function: %s\n" s;
535          assert false (*Unknown external function*)
536
537let next_step globalenv = function
538    | State(f,Sassign(a1,a2),k,e,m) -> 
539        let ((v1,t1),l1) = (eval_lvalue globalenv e m a1)
540        and ((v2,t2),l2) = eval_expr globalenv e m a2
541        in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
542    | State(f,Scall(None,a,al),k,e,m) ->
543        let (v1,l1) = eval_expr globalenv e m a in 
544        let fd = find_funct globalenv v1
545        and (vargs,l2) = (eval_exprlist globalenv e m al) in
546          if type_of_fundef fd = typeof a
547          then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
548          else assert false (*Signature mismatches*)
549  | State(f,Scall(Some lhs,a,al),k,e,m) ->
550      let (v1,l1) = eval_expr globalenv e m a in 
551      let fd = find_funct globalenv v1
552      and (vargs,l2) = (eval_exprlist globalenv e m al)
553      and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in
554        if type_of_fundef fd = typeof a then 
555          (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3)
556        else assert false (*Signature mismatches*) 
557  | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[])
558  | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[])
559  | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[])
560  | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[])
561  | State(f,Sifthenelse(a,s1,s2),k,e,m) -> 
562      let (v1,l1) = eval_expr globalenv e m a in 
563        if is_true v1 then (State(f,s1,k,e,m),l1)
564        else if is_false v1 then (State(f,s2,k,e,m),l1)
565        else assert false (*Wrong condition guard*)
566  | State(f,Swhile(a,s),k,e,m) ->
567      let (v1,l1) = eval_expr globalenv e m a in 
568        if is_false v1 then (State(f,Sskip,k,e,m),l1)
569        else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1)
570        else assert false (*Wrong condition guard*)
571  | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
572  | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
573  | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
574  | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[])
575  | State(f,Sskip,Kdowhile(a,s,k),e,m) ->
576      let (v1,l1) = eval_expr globalenv e m a in 
577        if is_false v1 then (State(f,Sskip,k,e,m),l1)
578        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
579        else assert false (*Wrong condition guard*)
580  | State(f,Scontinue,Kdowhile(a,s,k),e,m) ->
581      let (v1,l1) = eval_expr globalenv e m a in 
582        if is_false v1 then (State(f,Sskip,k,e,m),l1)
583        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
584        else assert false (*Wrong condition guard*)
585  | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
586  | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip ->
587      (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
588  | State(f,Sfor(Sskip,a2,a3,s),k,e,m) ->
589      let (v1,l1) = eval_expr globalenv e m a2 in 
590      if is_false v1 then (State(f,Sskip,k,e,m),l1)
591      else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1)
592      else assert false (*Wrong condition guard*)
593  | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
594  | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) ->
595      (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
596  | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
597  | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) ->
598      (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
599  | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid -> 
600      let m' = free_list m (blocks_of_env e) in
601        (Returnstate(Value.undef,(call_cont k),m'),[])
602  | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid -> 
603      let (v1,l1) = eval_expr globalenv e m a
604      and m' = free_list m (blocks_of_env e) in
605        (Returnstate(fst v1,call_cont k,m'),l1)
606  | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k -> 
607      let m' = free_list m (blocks_of_env e) in
608        (Returnstate(Value.undef,k,m'),[])
609  | State(f,Sswitch(a,sl),k,e,m) -> 
610      let (n,l) = (match eval_expr globalenv e m a with 
611                     | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll)
612                     | _ -> assert false (*Wrong switch index*)
613      ) in 
614        (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
615  | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
616  | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
617  | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[])
618  | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[])
619  | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl])
620  | State(f,Sgoto lbl,k,e,m) -> 
621      (match find_label lbl f.fn_body (call_cont k) with 
622         | Some (s',k') -> (State(f,s',k',e,m),[])
623         | None -> assert false (*Label does not exist*))
624  | Callstate(Internal f,vargs,k,m) -> 
625      let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in
626        (State(f,f.fn_body,k,e,m'),[])
627  | Callstate(External(id,targs,tres),vargs,k,m) 
628      when List.length targs = List.length vargs -> 
629      (interpret_external vargs k m id,[])
630  | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
631  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) -> 
632      let m' = assign m v ty vv in
633        (State(f,Sskip,k,e,m'),[])
634  | st -> 
635      Printf.eprintf "Error: no transition for %s\n" (string_of_state st); 
636      assert false 
637
638let init_to_data = function
639  | Init_int8 i         -> Data_int8 i
640  | Init_int16 i        -> Data_int16 i
641  | Init_int32 i        -> Data_int32 i
642  | Init_float32 f      -> assert false (* Not supported *)
643  | Init_float64 f      -> assert false (* Not supported *)
644  | Init_space i        -> Data_reserve i
645  | Init_addrof (_,_)   -> assert false (*TODO*)
646
647let alloc_datas m ((_,lst),ty) = 
648  let store_data (m,ptr) = function (*FIXME signed or unsigned ?*)
649    | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
650                       ,Value.add ptr (Value.of_int 1))
651    | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
652                       ,Value.add ptr (Value.of_int 2))
653    | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
654                       ,Value.add ptr (Value.of_int 4))
655    | Init_float32 _ -> assert false (*Not supported*)
656    | Init_float64 _ -> assert false (*Not supported*)
657    | Init_space n -> (m,Value.add ptr (Value.of_int n))
658    | Init_addrof (_,_) -> assert false (*TODO*) 
659  in let (m2,ptr) = (Mem.alloc m (sizeof ty))
660  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
661
662let initmem_clight prog =
663  let alloc_funct i (g,f) (id,fct) = 
664    Hashtbl.add g id (Value.of_int (-i-1));
665    Valtbl.add f (Value.of_int (-i-1)) fct;
666    (g,f)
667  and alloc_var (m,g) v =
668    let (m',ptr) = alloc_datas m v in
669      if is_struct (snd v) then
670        let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in 
671        let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
672        Hashtbl.add g (fst (fst v)) ptr2;(m3,g) 
673      else 
674        ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
675  in let (m,g) = 
676    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
677  in let (g2,f) = 
678    MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct
679  in 
680    (m,(g2,f))
681
682let compute_result v =
683  if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
684  else IntValue.Int8.zero
685
686let interpret debug prog = match prog.prog_main with
687  | None -> (IntValue.Int8.zero, [])
688  | Some main ->
689      let (m,g) = initmem_clight prog in
690      let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in
691      let rec exec trace = function
692        | (Returnstate(v,Kstop,m),l) -> 
693(*
694            if debug then (
695              print_string ("Result: "^(Value.to_string v));
696              print_string ("\nMemory dump: \n");
697              Mem.print m
698            );
699*)
700          let (res, cost_labels) as trace = (compute_result v, l@trace) in
701          if debug then
702            Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
703          trace
704        | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*)
705(*
706            if debug then (
707              print_string ("Result: (implicit return)");
708              print_string ("\nMemory dump: \n");
709              Mem.print m
710            );
711*)
712          let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in
713          if debug then
714            Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
715          trace
716        | (state,l) ->
717(*
718            if debug then print_string ((string_of_state state)^"\n");
719*)
720            exec (l@trace) (next_step g state)
721      in 
722(*
723      if debug then print_string "> --- Interpret Clight --- <\n";
724*)
725      exec [] first_state
Note: See TracBrowser for help on using the repository browser.