source: Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml @ 486

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

Deliverable D2.2

File size: 17.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 (*Not supported*)
121  | Op_intofptr         -> assert false (*Not supported*)
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
226(*FIXME To move in AST*)
227let string_of_sig sign = 
228  let rec tmp = function 
229    | [] -> ""
230    | Sig_int::l -> "int "^(tmp l) 
231    | Sig_float::l -> "float "^(tmp l)
232    | Sig_ptr::l -> "ptr "^(tmp l)
233  in 
234    match sign.res with
235      | Type_void -> (tmp sign.args)^" -> void"
236      | Type_ret Sig_int ->(tmp sign.args)^" -> int"
237      | Type_ret Sig_float ->(tmp sign.args)^" -> float"
238      | Type_ret Sig_ptr ->(tmp sign.args)^" -> ptr"
239
240
241let call_state global_env sigma e m a1 params sgn cont = 
242  let (f,l) = eval_expression global_env sigma e m a1 in
243    match funct global_env f with
244      | F_int(fi) ->
245          if fi.f_sig = sgn then (
246            let tmp = List.map (eval_expression global_env sigma e m) params in
247              (State_call(F_int(fi),(List.map fst tmp),cont,m),
248               l@(List.flatten (List.map snd tmp)))
249          ) else (
250            Printf.eprintf "Error: signature (%s) different from (%s) \n" 
251              (string_of_sig fi.f_sig)
252              (string_of_sig sgn);
253            assert false) (*Signatures mismatche*)
254      | F_ext(fe) ->
255          if fe.ef_sig = sgn then (
256          let tmp = List.map (eval_expression global_env sigma e m) params in
257            (State_call(F_ext(fe), (List.map fst tmp) ,cont,m),
258             l@(List.flatten (List.map snd tmp)))
259           ) else ( 
260             Printf.eprintf "Error: signature (%s) different from (%s) \n" 
261               (string_of_sig fe.ef_sig)
262               (string_of_sig sgn);
263             assert false) (*Signatures mismatche*)           
264
265let interpret_external f v k m =
266  try match f.ef_tag with
267    | "scan_int" ->
268        let res = Value.of_int (int_of_string (read_line ())) in
269          State_return (res, k, m)
270    | "print_int" ->
271        Printf.printf "%d" (Value.to_int (List.hd v)) ;
272        State_return (Value.zero, k, m)
273    | "print_intln" ->
274        Printf.printf "%d\n" (Value.to_int (List.hd v)) ;
275        State_return (Value.zero, k, m)
276    | "alloc" | "malloc" -> 
277        let (m',vv) = Mem.alloc m (Value.to_int (List.hd v)) in 
278          State_return (vv, k, m')
279    | "exit"  -> 
280        State_return (List.hd v,Ct_stop,m)
281    | s -> 
282        Printf.eprintf "Error: unknown external function: %s\n" s;
283        assert false (*Unknown external function*)
284  with 
285      Failure _ -> assert false (*Wrong number of arguments*)
286
287let state_transition state global_env = match state with
288
289    (* Transition semantics for Cminor, part 1: statements *)
290
291    State_regular(f,St_skip,Ct_cont(s,k),sigma,e,m) ->
292      (State_regular(f, s, k, sigma, e, m),[])
293  | State_regular(f,St_skip,Ct_endblock(k),sigma,e,m) -> 
294      (State_regular(f, St_skip, k, sigma, e, m),[])
295  | State_regular(f,St_assign(str,exp),k,sigma,e,m) -> 
296      let (v,l) = eval_expression global_env sigma e m exp in
297        set_local_value e str v;
298        (State_regular(f, St_skip, k, sigma, e, m),l)
299  | State_regular(f,St_store(q,a1,a2),k,sigma,e,m) ->
300      let (v1,l1) = eval_expression global_env sigma e m a1 in
301      let (v2,l2) = eval_expression global_env sigma e m a2 in
302        (State_regular(f, St_skip, k, sigma, e, Mem.store m q v1 v2),l1@l2)
303  | State_regular(f,St_seq(s1,s2),k,sigma,e,m) -> 
304      (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
305  | State_regular(f,St_ifthenelse(exp,s1,s2),k,sigma,e,m) ->
306      let (v,l) = eval_expression global_env sigma e m exp in
307        if Value.is_true v then (State_regular(f,s1,k,sigma,e,m),l)
308        else if Value.is_false v then (State_regular(f,s2,k,sigma,e,m),l)
309        else (
310          Printf.eprintf "Error: %s is not a boolean.\n" (Value.to_string v);
311          assert false (*boolean value expected*))
312  | State_regular(f,St_loop(s),k,sigma,e,m) -> 
313      (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
314  | State_regular(f,St_block(s),k,sigma,e,m) -> 
315      (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
316  | State_regular(f,St_exit(n),Ct_cont(s,k),sigma,e,m) -> 
317      (State_regular(f,(St_exit n),k,sigma,e,m),[])
318  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when n=0 -> 
319      (State_regular(f,St_skip,k,sigma,e,m),[])
320  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when (n>0) ->
321      (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
322  | State_regular(f,St_switch(exp,lst,def),k,sigma,e,m) ->
323      let (v,l) = eval_expression global_env sigma e m exp in
324        (try (State_regular 
325                (f, St_exit (List.assoc (Value.to_int v) lst),k, sigma, e, m),l)
326         with Not_found -> 
327           (State_regular (f, St_exit def, k, sigma, e, m),l) )
328  | State_regular(f,St_label(_,s),k,sigma,e,m) -> 
329      (State_regular(f,s,k,sigma,e,m),[])
330  | State_regular(f,St_cost(lbl,s),k,sigma,e,m) -> 
331      (State_regular(f,s,k,sigma,e,m),[lbl])
332  | State_regular(f,St_goto(lbl),k,sigma,e,m) -> 
333      let (s2,k2) = findlabel lbl f.f_body (callcont k)
334      in (State_regular(f,s2,k2,sigma,e,m),[])
335
336  (* Transition semantics for Cminor, part 2:
337  * functions, initial states, final states *)
338
339  | State_regular(f,St_call(id,a1,params,sgn),k,sigma,e,m) -> 
340      call_state global_env sigma e m a1 params sgn (Ct_returnto(id,f,sigma,e,k))
341  | State_regular(f,St_tailcall(a1,params,sgn),k,sigma,e,m) -> 
342      call_state global_env sigma e m a1 params sgn (callcont k)
343  | State_regular(f,St_skip,Ct_returnto(p1,p2,p3,p4,p5),sigma,e,m) 
344      when f.f_sig.res = Type_void -> 
345      (State_return (Value.undef,Ct_returnto(p1,p2,p3,p4,p5),Mem.free m sigma),[])
346  | State_regular(f,St_skip,Ct_stop,sigma,e,m) when f.f_sig.res = Type_void -> 
347      (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
348  | State_regular(f,St_return(_),k,sigma,e,m)  when f.f_sig.res = Type_void ->
349      (State_return (Value.undef,callcont k,Mem.free m sigma),[])
350  | State_regular(f,St_return(Some(a)),k,sigma,e,m) 
351      when f.f_sig.res != Type_void ->
352      let (v,l) = eval_expression global_env sigma e m a in
353      (State_return (v,callcont k,Mem.free m sigma),l)
354  | State_call(F_int(f),v,k,m) -> 
355      let (m2,ptr) = Mem.alloc m f.f_stacksize in
356        (State_regular(f,f.f_body,k,ptr,(create_local_env v f.f_params f.f_vars),m2),[])
357  | State_call(F_ext(f),v,k,m) ->
358      (interpret_external f v k m,[])
359  | State_return(v,Ct_returnto(id,f,sigma,e,k),m) -> 
360      ( match id with
361            Some(i) -> 
362              (State_regular(f,St_skip,k,sigma,(set_local_value e i v;e),m),[])
363          | None -> (State_regular(f,St_skip,k,sigma,e,m),[])
364      )
365  | st -> 
366      Printf.eprintf "Error: no transition for %s\n" (string_of_state st);
367      assert false 
368
369let alloc_datas m (_,lst) = 
370  let rec sizeof = function
371    | [] -> 0
372    | (Data_reserve n)::l -> n + (sizeof l)
373    | (Data_int8 _)::l -> 1 + (sizeof l)
374    | (Data_int16 _)::l -> 2 + (sizeof l)
375    | (Data_int32 _)::l -> 4 + (sizeof l)
376    | (Data_float32 _)::l | (Data_float64 _)::l -> assert false (*Not supported*)
377  in let store_data (m,ptr) = function (*FIXME signed or unsigned ?*)
378    | Data_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
379                       ,Value.add ptr (Value.of_int 1))
380    | Data_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
381                       ,Value.add ptr (Value.of_int 2))
382    | Data_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
383                       ,Value.add ptr (Value.of_int 4))
384    | Data_float32 _ -> assert false (*Not supported*)
385    | Data_float64 _ -> assert false (*Not supported*)
386    | Data_reserve n -> (m,Value.add ptr (Value.of_int n))
387  in let (m2,ptr) = (Mem.alloc m (sizeof lst))
388  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
389
390
391let initmem_cminor prog =
392  let alloc_funct i (g,f) (id,fct) = 
393    Hashtbl.add g id (Value.of_int (-i-1));
394    Valtbl.add f (Value.of_int (-i-1)) fct;
395    (g,f)
396  and alloc_var (m,g) v =
397    let (m',ptr) = alloc_datas m v in 
398      Hashtbl.add g (fst v) ptr;
399      (m',g) 
400  in let (m,g) = 
401    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.vars
402  in let (g2,f) = 
403    MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.functs
404  in 
405    (m,(g2,f))
406
407let interpret debug prog = match prog.main with
408  | None -> []
409  | Some main ->
410      let (m,global_env) = initmem_cminor prog in
411      let first_state = (State_call (
412                           funct global_env (symbol global_env main),
413                           [], Ct_stop,m),[]) in
414      let rec exec l = function
415        | (State_return(v,Ct_stop,m),lbl) -> 
416            if debug then (
417              print_string ("Result: "^(Value.to_string v));
418              print_string ("\nMemory dump: \n");
419              Mem.print m
420            );
421            lbl@l
422        | (State_regular(_,St_skip,Ct_stop,_,_,m),lbl) ->
423            if debug then (
424              print_string ("Result: (implicit return)\n");
425              print_string ("\nMemory dump: \n");
426              Mem.print m
427            );
428            lbl@l
429        | (state,lbl) -> 
430            if debug then print_string ((string_of_state state)^"\n");
431            exec (lbl@l) (state_transition state global_env)
432      in 
433      if debug then print_string ">------------------- Interpret Cminor -------------------<\n";
434      (exec [] first_state)
Note: See TracBrowser for help on using the repository browser.