source: Deliverables/D2.3/8051/src/cminor/cminorInterpret.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: 16.0 KB
Line 
1open AST
2open Cminor
3
4module Mem = Driver.CminorMemory
5module Value = Mem.Value
6module Valtbl = Hashtbl.Make(Value)
7
8
9let print_hashtbl h name =
10  print_string ("Hashtbl "^name^":\n"); 
11  Hashtbl.iter (fun a _ -> print_string (" - "^a^"\n") ) h
12
13(* Type definition *)
14
15type local_env = (ident,Value.t) Hashtbl.t
16
17type continuation = 
18    Ct_stop
19  | Ct_cont of statement*continuation
20  | Ct_endblock of continuation
21  | Ct_returnto of
22      ident option*internal_function*Value.t*local_env*continuation
23
24type state = 
25    State_regular of
26      internal_function*statement*continuation*Value.t*local_env*(function_def Mem.memory)
27  | State_call of function_def*Value.t list*continuation*(function_def Mem.memory)
28  | State_return of Value.t*continuation*(function_def Mem.memory)
29
30(* Local environment abstraction *)
31
32let get_local_value e id = 
33  try Hashtbl.find e id
34  with Not_found -> assert false (*Wrong ident*)
35
36let set_local_value e id v = Hashtbl.add e id v
37
38(* Create_local_env :
39* constructs the local environement from effective parameters. *)
40let create_local_env arg params vars = 
41  let h = Hashtbl.create 11 in
42  if List.length params = List.length arg then
43    (
44      for i=1 to (List.length params) do
45        Hashtbl.add h (List.nth params (i-1)) (List.nth arg (i-1))
46      done;
47      for i=1 to (List.length vars) do
48        Hashtbl.add h (List.nth vars (i-1)) Value.undef
49      done;
50      h
51    )
52  else assert false (*Wrong number of parameters*)
53
54(* Pretty Printing and debug *)
55
56let string_of_cont = function
57    Ct_stop -> "stop"
58  | Ct_cont(s1,_) -> (CminorPrinter.string_of_statement s1)^"::cont"
59  | Ct_endblock(_) -> "endblock"
60  | Ct_returnto(_,_,_,_,_) -> "returnto"
61
62let string_of_state = function
63    State_regular(_,s,c,_,_,_) -> 
64      "State_regular { "
65      ^(CminorPrinter.string_of_statement s)^" - "^(string_of_cont c)^" }"
66  | State_call(F_ext(e),v,c,_) -> 
67      "State_call { extern "
68      ^e.ef_tag
69      ^"("
70      ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v))
71      ^") - "
72      ^(string_of_cont c)^" }"
73  | State_call(F_int(i),v,c,_) ->
74      "State_call { function("
75      ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v))
76      ^") - "
77      ^(string_of_cont c)^" }"
78  | State_return(v,c,_) -> 
79      "State_return { "^(Value.to_string v)^" - "^(string_of_cont c)^" }"
80
81(* Global environment abstraction *)
82
83(* Symbol : returns the block corresponding to the identifier
84* id in the global environement g *)
85let symbol g id = let (id_b,b_fd) = g in
86try Hashtbl.find id_b id
87with Not_found -> assert false
88
89(* Funct : returns the definition of the function located in block b *)
90let funct g b = let (id_b,b_fd) = g in
91try Valtbl.find b_fd b
92with Not_found -> assert false
93
94
95
96(* Expression evaluation *)
97
98let eval_constant global_env stack = function
99    Cst_int i           -> Value.of_int i
100  | Cst_float _         -> assert false
101  | Cst_addrsymbol id   -> symbol global_env id
102  | Cst_stackoffset o   -> stack
103
104let eval_unop arg = function 
105    Op_cast8unsigned    -> Value.cast8unsigned arg
106  | Op_cast8signed      -> Value.cast8signed arg
107  | Op_cast16unsigned   -> Value.cast16unsigned arg
108  | Op_cast16signed     -> Value.cast16signed arg
109  | Op_negint           -> Value.negint arg
110  | Op_notbool          -> Value.notbool arg
111  | Op_notint           -> Value.notint arg
112  | Op_negf             -> assert false (*Not supported*)
113  | Op_absf             -> assert false (*Not supported*)
114  | Op_singleoffloat    -> assert false (*Not supported*)
115  | Op_intoffloat       -> assert false (*Not supported*) 
116  | Op_intuoffloat      -> assert false (*Not supported*) 
117  | Op_floatofint       -> assert false (*Not supported*) 
118  | Op_floatofintu      -> assert false (*Not supported*) 
119  | Op_id               -> arg
120  | Op_ptrofint         -> assert false (*FIXME check semantics*)
121  | Op_intofptr         -> assert false (*FIXME check semantics*)
122
123let eval_binop arg1 arg2 = function
124    Op_add              -> Value.add arg1 arg2
125  | Op_sub              -> Value.sub arg1 arg2
126  | Op_mul              -> Value.mul arg1 arg2
127  | Op_div              -> Value.div arg1 arg2
128  | Op_divu             -> Value.divu arg1 arg2
129  | Op_mod              -> Value.modulo arg1 arg2
130  | Op_modu             -> Value.modu arg1 arg2
131  | Op_and              -> Value.and_op arg1 arg2
132  | Op_or               -> Value.or_op arg1 arg2
133  | Op_xor              -> Value.xor arg1 arg2
134  | Op_shl              -> Value.shl arg1 arg2
135  | Op_shr              -> Value.shr arg1 arg2
136  | Op_shru             -> Value.shru arg1 arg2
137  | Op_addf             -> assert false (*Not supported*)
138  | Op_subf             -> assert false (*Not supported*)
139  | Op_mulf             -> assert false (*Not supported*)
140  | Op_divf             -> assert false (*Not supported*)
141  | Op_cmp(Cmp_eq)      -> Value.cmp_eq arg1 arg2
142  | Op_cmp(Cmp_ne)      -> Value.cmp_ne arg1 arg2
143  | Op_cmp(Cmp_gt)      -> Value.cmp_gt arg1 arg2
144  | Op_cmp(Cmp_ge)      -> Value.cmp_ge arg1 arg2
145  | Op_cmp(Cmp_lt)      -> Value.cmp_lt arg1 arg2
146  | Op_cmp(Cmp_le)      -> Value.cmp_le arg1 arg2
147  | Op_cmpu(Cmp_eq)     -> Value.cmp_eq_u arg1 arg2
148  | Op_cmpu(Cmp_ne)     -> Value.cmp_ne_u arg1 arg2
149  | Op_cmpu(Cmp_gt)     -> Value.cmp_gt_u arg1 arg2
150  | Op_cmpu(Cmp_ge)     -> Value.cmp_ge_u arg1 arg2
151  | Op_cmpu(Cmp_lt)     -> Value.cmp_lt_u arg1 arg2
152  | Op_cmpu(Cmp_le)     -> Value.cmp_le_u arg1 arg2
153  | Op_cmpf(_)          -> assert false (*Not supported*)
154  | Op_addp             -> Value.add arg1 arg2
155  | Op_subp             -> Value.sub arg1 arg2
156  | Op_cmpp(Cmp_eq)      -> Value.cmp_eq arg1 arg2
157  | Op_cmpp(Cmp_ne)      -> Value.cmp_ne arg1 arg2
158  | Op_cmpp(Cmp_gt)      -> Value.cmp_gt arg1 arg2
159  | Op_cmpp(Cmp_ge)      -> Value.cmp_ge arg1 arg2
160  | Op_cmpp(Cmp_lt)      -> Value.cmp_lt arg1 arg2
161  | Op_cmpp(Cmp_le)      -> Value.cmp_le arg1 arg2
162
163let rec eval_expression global_env stack local_env memory = function
164    Id(str) -> (get_local_value local_env str,[])
165  | Cst(c) -> (eval_constant global_env stack c,[])
166  | Op1(op,arg) -> 
167      let (v,l) = eval_expression global_env stack local_env memory arg in
168      (eval_unop v op,l)
169  | Op2(op,arg1,arg2) -> 
170      let (v1,l1) = eval_expression global_env stack local_env memory arg1
171      and (v2,l2) = eval_expression global_env stack local_env memory arg2 in
172        (eval_binop v1 v2 op,l1@l2) 
173  | Mem(k,a) -> 
174      let (v,l) = (eval_expression global_env stack local_env memory a) in 
175        (Mem.load memory k v,l)
176  | Cond(a1,a2,a3) ->
177      let (v1,l1) = eval_expression global_env stack local_env memory a1 in
178        if Value.is_true v1 then
179          let (v2,l2) = eval_expression global_env stack local_env memory a2 in
180            (v2,l1@l2)
181        else if Value.is_false v1 then
182          let (v2,l2) = eval_expression global_env stack local_env memory a3 in
183            (v2,l1@l2)
184        else assert false (*A boolean value is expected*)
185  | Exp_cost(lbl,e) -> 
186      let (v,l) = eval_expression global_env stack local_env memory e in
187        (v,l@[lbl])
188
189(* State transition *)
190
191let rec callcont = function
192    Ct_stop                     -> Ct_stop
193  | Ct_cont(_,k)                -> callcont k
194  | Ct_endblock(k)              -> callcont k
195  | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
196
197let findlabel lbl st k = 
198  let rec fdlbl k = function
199    St_skip                     -> None
200  | St_assign(_,_)              -> None
201  | St_store(_,_,_)             -> None
202  | St_call(_,_,_,_)            -> None
203  | St_tailcall(_,_,_)          -> None 
204  | St_seq(s1,s2)               -> 
205      (match fdlbl (Ct_cont(s2,k)) s1 with
206           None -> fdlbl k s2
207         | Some(v) -> Some(v)
208      )
209  | St_ifthenelse(_,s1,s2)      ->
210      (match fdlbl k s1 with
211           None -> fdlbl k s2
212         | Some(v) -> Some(v)
213      )
214  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
215  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
216  | St_exit(_)                  -> None
217  | St_switch(_,_,_)            -> None
218  | St_return(_)                -> None
219  | St_label(l,s)               -> if l=lbl then Some((s,k)) else None 
220  | St_goto(_)                  -> None
221  | St_cost (_,s)               -> fdlbl k s
222  in match fdlbl k st with
223      None -> assert false (*Wrong label*)
224    | Some(v) -> v
225
226let call_state global_env sigma e m a1 params sgn cont = 
227  let (f,l) = eval_expression global_env sigma e m a1 in
228    match funct global_env f with
229      | F_int(fi) when fi.f_sig = sgn ->
230          let tmp = List.map (eval_expression global_env sigma e m) params in
231            (State_call(F_int(fi),(List.map fst tmp),cont,m),
232             l@(List.flatten (List.map snd tmp)))
233      | F_ext(fe) when fe.ef_sig = sgn ->
234          let tmp = List.map (eval_expression global_env sigma e m) params in
235            (State_call(F_ext(fe), (List.map fst tmp) ,cont,m),
236             l@(List.flatten (List.map snd tmp)))
237      | _ -> assert false (*Signatures mismatche*)
238
239
240let interpret_external f v k m =
241  try match f.ef_tag with
242    | "scan_int" ->
243        let res = Value.of_int (int_of_string (read_line ())) in
244          State_return (res, k, m)
245    | "print_int" ->
246        Printf.printf "%d" (Value.to_int (List.hd v)) ;
247        State_return (Value.zero, k, m)
248    | "print_intln" ->
249        Printf.printf "%d\n" (Value.to_int (List.hd v)) ;
250        State_return (Value.zero, k, m)
251    | "alloc" -> let (m',vv) = Mem.alloc m (Value.to_int (List.hd v)) in 
252        State_return (vv, k, m')
253    | _ -> assert false (*Unknown external function*)
254  with Failure _ -> assert false (*Wrong number of arguments*)
255
256let state_transition state global_env = match state with
257
258    (* Transition semantics for Cminor, part 1: statements *)
259
260    State_regular(f,St_skip,Ct_cont(s,k),sigma,e,m) ->
261      (State_regular(f, s, k, sigma, e, m),[])
262  | State_regular(f,St_skip,Ct_endblock(k),sigma,e,m) -> 
263      (State_regular(f, St_skip, k, sigma, e, m),[])
264  | State_regular(f,St_assign(str,exp),k,sigma,e,m) -> 
265      let (v,l) = eval_expression global_env sigma e m exp in
266        set_local_value e str v;
267        (State_regular(f, St_skip, k, sigma, e, m),l)
268  | State_regular(f,St_store(q,a1,a2),k,sigma,e,m) ->
269      let (v1,l1) = eval_expression global_env sigma e m a1 in
270      let (v2,l2) = eval_expression global_env sigma e m a2 in
271        (State_regular(f, St_skip, k, sigma, e, Mem.store m q v1 v2),l1@l2)
272  | State_regular(f,St_seq(s1,s2),k,sigma,e,m) -> 
273      (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
274  | State_regular(f,St_ifthenelse(exp,s1,s2),k,sigma,e,m) ->
275      let (v,l) = eval_expression global_env sigma e m exp in
276        if Value.is_true v then (State_regular(f,s1,k,sigma,e,m),l)
277        else if Value.is_false v then (State_regular(f,s2,k,sigma,e,m),l)
278        else assert false (*boolean value expected*)
279  | State_regular(f,St_loop(s),k,sigma,e,m) -> 
280      (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
281  | State_regular(f,St_block(s),k,sigma,e,m) -> 
282      (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
283  | State_regular(f,St_exit(n),Ct_cont(s,k),sigma,e,m) -> 
284      (State_regular(f,(St_exit n),k,sigma,e,m),[])
285  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when n=0 -> 
286      (State_regular(f,St_skip,k,sigma,e,m),[])
287  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when (n>0) ->
288      (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
289  | State_regular(f,St_switch(exp,lst,def),k,sigma,e,m) ->
290      let (v,l) = eval_expression global_env sigma e m exp in
291        (try (State_regular 
292                (f, St_exit (List.assoc (Value.to_int v) lst),k, sigma, e, m),l)
293         with Not_found -> 
294           (State_regular (f, St_exit def, k, sigma, e, m),l) )
295  | State_regular(f,St_label(_,s),k,sigma,e,m) -> 
296      (State_regular(f,s,k,sigma,e,m),[])
297  | State_regular(f,St_cost(lbl,s),k,sigma,e,m) -> 
298      (State_regular(f,s,k,sigma,e,m),[lbl])
299  | State_regular(f,St_goto(lbl),k,sigma,e,m) -> 
300      let (s2,k2) = findlabel lbl f.f_body (callcont k)
301      in (State_regular(f,s2,k2,sigma,e,m),[])
302
303  (* Transition semantics for Cminor, part 2:
304  * functions, initial states, final states *)
305
306  | State_regular(f,St_call(id,a1,params,sgn),k,sigma,e,m) -> 
307      call_state global_env sigma e m a1 params sgn (Ct_returnto(id,f,sigma,e,k))
308  | State_regular(f,St_tailcall(a1,params,sgn),k,sigma,e,m) -> 
309      call_state global_env sigma e m a1 params sgn (callcont k)
310  | State_regular(f,St_skip,Ct_returnto(p1,p2,p3,p4,p5),sigma,e,m) 
311      when f.f_sig.res = Type_void -> 
312      (State_return (Value.undef,Ct_returnto(p1,p2,p3,p4,p5),Mem.free m sigma),[])
313  | State_regular(f,St_skip,Ct_stop,sigma,e,m) when f.f_sig.res = Type_void -> 
314      (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
315  | State_regular(f,St_return(_),k,sigma,e,m)  when f.f_sig.res = Type_void ->
316      (State_return (Value.undef,callcont k,Mem.free m sigma),[])
317  | State_regular(f,St_return(Some(a)),k,sigma,e,m) 
318      when f.f_sig.res != Type_void ->
319      let (v,l) = eval_expression global_env sigma e m a in
320      (State_return (v,callcont k,Mem.free m sigma),l)
321  | State_call(F_int(f),v,k,m) -> 
322      let (m2,ptr) = Mem.alloc m f.f_stacksize in
323        (State_regular(f,f.f_body,k,ptr,(create_local_env v f.f_params f.f_vars),m2),[])
324  | State_call(F_ext(f),v,k,m) ->
325      (interpret_external f v k m,[])
326  | State_return(v,Ct_returnto(id,f,sigma,e,k),m) -> 
327      ( match id with
328            Some(i) -> 
329              (State_regular(f,St_skip,k,sigma,(set_local_value e i v;e),m),[])
330          | None -> (State_regular(f,St_skip,k,sigma,e,m),[])
331      )
332  | _ -> assert false 
333
334let alloc_datas m (_,lst) = 
335  let rec sizeof = function
336    | [] -> 0
337    | (Data_reserve n)::l -> n + (sizeof l)
338    | (Data_int8 _)::l -> 1 + (sizeof l)
339    | (Data_int16 _)::l -> 2 + (sizeof l)
340    | (Data_int32 _)::l -> 4 + (sizeof l)
341    | (Data_float32 _)::l | (Data_float64 _)::l -> assert false (*Not supported*)
342  in let store_data (m,ptr) = function (*FIXME signed ?*)
343    | Data_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
344                       ,Value.add ptr (Value.of_int 1))
345    | Data_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
346                       ,Value.add ptr (Value.of_int 2))
347    | Data_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
348                       ,Value.add ptr (Value.of_int 4))
349    | Data_float32 _ -> assert false (*Not supported*)
350    | Data_float64 _ -> assert false (*Not supported*)
351    | Data_reserve n -> (m,Value.add ptr (Value.of_int n))
352  in let (m2,ptr) = (Mem.alloc m (sizeof lst))
353  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
354
355
356let initmem_cminor prog =
357  let alloc_funct i (g,f) (id,fct) = 
358    Hashtbl.add g id (Value.of_int (-i-1));
359    Valtbl.add f (Value.of_int (-i-1)) fct;
360    (g,f)
361  and alloc_var (m,g) v =
362    let (m',ptr) = alloc_datas m v in 
363      Hashtbl.add g (fst v) ptr;
364      (m',g) 
365  in let (m,g) = 
366    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.vars
367  in let (g2,f) = 
368    MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.functs
369  in 
370    (m,(g2,f))
371
372 (*
373
374  let id_to_b = Hashtbl.create 1 and b_to_fd = Hashtbl.create 11 in
375  let alloc_var m (id,data) =
376    let (m2,ptr) = alloc_datas m data in
377      Hashtbl.add id_to_b id ptr;m2
378  and add_funct i f =
379    let b = Value.of_int (i+1) in
380      Hashtbl.add id_to_b (fst f) b;
381      Hashtbl.add b_to_fd b (snd f)
382  in
383    MiscPottier.iteri add_funct prog.functs;
384    (List.fold_left alloc_var Mem.empty prog.vars,(id_to_b,b_to_fd))
385  *)
386
387let interpret debug prog = match prog.main with
388  | None -> []
389  | Some main ->
390      let (m,global_env) = initmem_cminor prog in
391      let first_state = (State_call (
392                           funct global_env (symbol global_env main),
393                           [], Ct_stop,m),[]) in
394      let rec exec l = function
395        | (State_return(v,Ct_stop,m),lbl) -> 
396            if debug then (
397              print_string ("Result: "^(Value.to_string v));
398              print_string ("\nMemory dump: \n");
399              Mem.print m
400            );
401            lbl@l
402        | (state,lbl) -> 
403            if debug then print_string ((string_of_state state)^"\n");
404            exec (lbl@l) (state_transition state global_env)
405      in 
406      if debug then print_string ">------------------- Interpret Cminor -------------------<\n";
407      (exec [] first_state)
Note: See TracBrowser for help on using the repository browser.