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

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 12.7 KB
Line 
1open AST
2open Cminor
3
4module Mem = Driver.CminorMemory
5module Value = Mem.Value
6module LocalEnv = Map.Make(String)
7type local_env = Value.t LocalEnv.t
8type memory = Cminor.function_def Mem.memory
9
10
11let error_prefix = "Cminor interpret"
12let error s = Error.global_error error_prefix s
13let warning s = Error.warning error_prefix s
14let error_float () = error "float not supported."
15
16
17(* Helpers *)
18
19let value_of_address = List.hd
20let address_of_value v = [v]
21
22
23(* State of execution *)
24
25type continuation = 
26    Ct_stop
27  | Ct_cont of statement*continuation
28  | Ct_endblock of continuation
29  | Ct_returnto of
30      ident option*internal_function*Value.address*local_env*continuation
31
32type state = 
33    State_regular of
34      internal_function*statement*continuation*Value.address*local_env*(function_def Mem.memory)
35  | State_call of function_def*Value.t list*continuation*(function_def Mem.memory)
36  | State_return of Value.t*continuation*(function_def Mem.memory)
37
38let string_of_local_env lenv =
39  let f x v s = s ^ x ^ " = " ^ (Value.to_string v) ^ "  " in
40  LocalEnv.fold f lenv ""
41
42let string_of_expr = CminorPrinter.print_expression
43
44let string_of_args args =
45  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
46
47let rec string_of_statement = function
48  | St_skip -> "skip"
49  | St_assign (x, e) -> x ^ " = " ^ (string_of_expr e)
50  | St_store (q, e1, e2) ->
51    Printf.sprintf "%s[%s] = %s"
52      (Memory.string_of_quantity q) (string_of_expr e1) (string_of_expr e2)
53  | St_call (None, f, args, _)
54  | St_tailcall (f, args, _) -> (string_of_expr f) ^ (string_of_args args)
55  | St_call (Some x, f, args, _) ->
56    x ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
57  | St_seq _ -> "sequence"
58  | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
59  | St_loop _ -> "loop"
60  | St_block _ -> "block"
61  | St_exit n -> "exit " ^ (string_of_int n)
62  | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
63  | St_return None -> "return"
64  | St_return (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
65  | St_label (lbl, _) -> "label " ^ lbl
66  | St_goto lbl -> "goto " ^ lbl
67  | St_cost (lbl, _) -> "cost " ^ lbl
68
69let print_state = function
70  | State_regular (_, stmt, _, sp, lenv, mem) ->
71    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
72      (string_of_local_env lenv)
73      (Mem.to_string mem)
74      (Value.to_string (value_of_address sp))
75      (string_of_statement stmt)
76  | State_call (_, args, _, mem) ->
77    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
78      (Mem.to_string mem)
79      (MiscPottier.string_of_list " " Value.to_string args)
80  | State_return (v, _, mem) ->
81    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
82      (Mem.to_string mem)
83      (Value.to_string v)
84
85
86(* Global and local environment management *)
87
88let init_local_env args params vars =
89  let f_param lenv x v = LocalEnv.add x v lenv in
90  let f_var lenv x = LocalEnv.add x Value.undef lenv in
91  let lenv = List.fold_left2 f_param LocalEnv.empty params args in
92  List.fold_left f_var lenv vars
93
94let find_fundef f mem =
95  let addr = Mem.find_global mem f in
96  Mem.find_fun_def mem addr
97
98
99(* Expression evaluation *)
100
101let eval_constant stack m = function
102  | Cst_int i -> Value.of_int i
103  | Cst_float _ -> error_float ()
104  | Cst_addrsymbol id when Mem.mem_global m id ->
105    value_of_address (Mem.find_global m id)
106  | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
107  | Cst_stackoffset o -> Value.add (value_of_address stack) (Value.of_int o)
108
109let eval_unop = function 
110  | Op_negf
111  | Op_absf
112  | Op_singleoffloat
113  | Op_intoffloat
114  | Op_intuoffloat
115  | Op_floatofint
116  | Op_floatofintu -> error_float ()
117  | Op_cast8unsigned    -> Value.cast8unsigned
118  | Op_cast8signed      -> Value.cast8signed
119  | Op_cast16unsigned   -> Value.cast16unsigned
120  | Op_cast16signed     -> Value.cast16signed
121  | Op_negint           -> Value.negint
122  | Op_notbool          -> Value.notbool
123  | Op_notint           -> Value.notint
124  | Op_id               -> (fun v -> v)
125  | Op_ptrofint         -> assert false (*Not supported yet*)
126  | Op_intofptr         -> assert false (*Not supported yet*)
127
128let eval_binop = function
129  | Op_add
130  | Op_addp             -> Value.add
131  | Op_sub
132  | Op_subp             -> Value.sub
133  | Op_mul              -> Value.mul
134  | Op_div              -> Value.div
135  | Op_divu             -> Value.divu
136  | Op_mod              -> Value.modulo
137  | Op_modu             -> Value.modulou
138  | Op_and              -> Value.and_op
139  | Op_or               -> Value.or_op
140  | Op_xor              -> Value.xor
141  | Op_shl              -> Value.shl
142  | Op_shr              -> Value.shr
143  | Op_shru             -> Value.shru
144  | Op_addf
145  | Op_subf
146  | Op_mulf
147  | Op_divf
148  | Op_cmpf _           -> error_float ()
149  | Op_cmp(Cmp_eq)
150  | Op_cmpp(Cmp_eq)     -> Value.cmp_eq
151  | Op_cmp(Cmp_ne)
152  | Op_cmpp(Cmp_ne)     -> Value.cmp_ne
153  | Op_cmp(Cmp_gt)
154  | Op_cmpp(Cmp_gt)     -> Value.cmp_gt
155  | Op_cmp(Cmp_ge)
156  | Op_cmpp(Cmp_ge)     -> Value.cmp_ge
157  | Op_cmp(Cmp_lt)
158  | Op_cmpp(Cmp_lt)     -> Value.cmp_lt
159  | Op_cmp(Cmp_le)
160  | Op_cmpp(Cmp_le)     -> Value.cmp_le
161  | Op_cmpu(Cmp_eq)     -> Value.cmp_eq_u
162  | Op_cmpu(Cmp_ne)     -> Value.cmp_ne_u
163  | Op_cmpu(Cmp_gt)     -> Value.cmp_gt_u
164  | Op_cmpu(Cmp_ge)     -> Value.cmp_ge_u
165  | Op_cmpu(Cmp_lt)     -> Value.cmp_lt_u
166  | Op_cmpu(Cmp_le)     -> Value.cmp_le_u
167
168let rec eval_expression stack local_env memory = function
169  | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
170  | Id x -> error ("unknown local variable " ^ x ^ ".")
171  | Cst(c) -> (eval_constant stack memory c,[])
172  | Op1(op,arg) -> 
173    let (v,l) = eval_expression stack local_env memory arg in
174    (eval_unop op v,l)
175  | Op2(op,arg1,arg2) -> 
176    let (v1,l1) = eval_expression stack local_env memory arg1 in
177    let (v2,l2) = eval_expression stack local_env memory arg2 in
178    (eval_binop op v1 v2,l1@l2) 
179  | Mem(q,a) -> 
180    let (v,l) = eval_expression stack local_env memory a in 
181    (Mem.loadq memory q (address_of_value v),l)
182  | Cond(a1,a2,a3) ->
183    let (v1,l1) = eval_expression stack local_env memory a1 in
184    if Value.is_true v1 then
185      let (v2,l2) = eval_expression stack local_env memory a2 in
186      (v2,l1@l2)
187    else
188      if Value.is_false v1 then
189        let (v3,l3) = eval_expression stack local_env memory a3 in
190        (v3,l1@l3)
191      else error "undefined conditional value."
192  | Exp_cost(lbl,e) -> 
193    let (v,l) = eval_expression stack local_env memory e in
194    (v,l@[lbl])
195
196let eval_exprlist sp lenv mem es =
197  let f (vs, cost_lbls) e =
198    let (v, cost_lbls') = eval_expression sp lenv mem e in
199    (vs @ [v], cost_lbls @ cost_lbls') in
200  List.fold_left f ([], []) es
201
202(* State transition *)
203
204let rec callcont = function
205    Ct_stop                     -> Ct_stop
206  | Ct_cont(_,k)                -> callcont k
207  | Ct_endblock(k)              -> callcont k
208  | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
209
210let findlabel lbl st k = 
211  let rec fdlbl k = function
212    St_skip                     -> None
213  | St_assign(_,_)              -> None
214  | St_store(_,_,_)             -> None
215  | St_call(_,_,_,_)            -> None
216  | St_tailcall(_,_,_)          -> None 
217  | St_seq(s1,s2)               -> 
218      (match fdlbl (Ct_cont(s2,k)) s1 with
219           None -> fdlbl k s2
220         | Some(v) -> Some(v)
221      )
222  | St_ifthenelse(_,s1,s2)      ->
223      (match fdlbl k s1 with
224           None -> fdlbl k s2
225         | Some(v) -> Some(v)
226      )
227  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
228  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
229  | St_exit(_)                  -> None
230  | St_switch(_,_,_)            -> None
231  | St_return(_)                -> None
232  | St_label(l,s)               -> if l=lbl then Some((s,k)) else None 
233  | St_goto(_)                  -> None
234  | St_cost (_,s)               -> fdlbl k s
235  in match fdlbl k st with
236      None -> assert false (*Wrong label*)
237    | Some(v) -> v
238
239
240let call_state sigma e m f params cont =
241  let (addr,l1) = eval_expression sigma e m f in
242  let fun_def = Mem.find_fun_def m (address_of_value addr) in
243  let (args,l2) = eval_exprlist sigma e m params in
244  (State_call(fun_def,args,cont,m),l1@l2)
245
246let eval_stmt f k sigma e m s = match s, k with
247  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
248  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
249  | St_skip, (Ct_returnto _ as k) ->
250    (State_return (Value.undef,k,Mem.free m sigma),[])
251  | St_skip,Ct_stop -> 
252    (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
253  | St_assign(x,exp),_ -> 
254    let (v,l) = eval_expression sigma e m exp in
255    let e = LocalEnv.add x v e in
256    (State_regular(f, St_skip, k, sigma, e, m),l)
257  | St_store(q,a1,a2),_ ->
258    let (v1,l1) = eval_expression sigma e m a1 in
259    let (v2,l2) = eval_expression sigma e m a2 in
260    let m = Mem.storeq m q (address_of_value v1) v2 in
261    (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
262  | St_call(xopt,f',params,_),_ ->
263    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
264  | St_tailcall(f',params,_),_ -> 
265    call_state sigma e m f' params (callcont k)
266  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
267  | St_ifthenelse(exp,s1,s2),_ ->
268    let (v,l) = eval_expression sigma e m exp in
269    let next_stmt =
270      if Value.is_true v then s1
271      else
272        if Value.is_false v then s2
273        else error "undefined conditional value." in
274      (State_regular(f,next_stmt,k,sigma,e,m),l)
275  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
276  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
277  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
278  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
279  | St_exit(n),Ct_endblock(k) ->
280    (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
281  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
282  | St_goto(lbl),_ -> 
283    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
284    (State_regular(f,s2,k2,sigma,e,m),[])
285  | St_switch(exp,lst,def),_ ->
286    let (v,l) = eval_expression sigma e m exp in
287    if Value.is_int v then
288      try
289        let i = Value.to_int v in
290        let nb_exit =
291          if List.mem_assoc i lst then List.assoc i lst
292          else def in
293        (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
294      with _ -> error "int value too big."
295    else error "undefined switch value."
296  | St_return(None),_ ->
297    (State_return (Value.undef,callcont k,Mem.free m sigma),[])
298  | St_return(Some(a)),_ ->
299      let (v,l) = eval_expression sigma e m a in
300      (State_return (v,callcont k,Mem.free m sigma),l)
301  | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
302  | _ -> error "state malformation."
303
304
305module InterpretExternal = Primitive.Interpret (Mem)
306
307let interpret_external k mem f args =
308  let (mem', v) = match InterpretExternal.t mem f args with
309    | (mem', InterpretExternal.V v) -> (mem', v)
310    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
311  State_return (v, k, mem')
312
313let step_call vargs k m = function
314  | F_int f ->
315    let (m, sp) = Mem.alloc m f.f_stacksize in
316    let lenv = init_local_env vargs f.f_params f.f_vars in
317    State_regular(f,f.f_body,k,sp,lenv,m)
318  | F_ext f -> interpret_external k m f.ef_tag vargs
319
320let step = function
321  | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
322  | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
323  | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
324    (State_regular(f,St_skip,k,sigma,e,m),[])
325  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
326    let e = LocalEnv.add x v e in
327    (State_regular(f,St_skip,k,sigma,e,m),[])
328  | _ -> error "state malformation."
329
330
331let init_mem prog =
332  let f_var mem (x, init_datas) = Mem.add_var mem x init_datas in
333  let mem = List.fold_left f_var Mem.empty prog.vars in
334  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
335  List.fold_left f_fun_def mem prog.functs
336
337let compute_result v =
338  if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
339  else IntValue.Int8.zero
340
341let rec exec debug trace (state, l) =
342  let cost_labels = l @ trace in
343  let print_and_return_result res =
344    if debug then Printf.printf "Result = %s\n%!"
345      (IntValue.Int8.to_string res) ;
346    (res, cost_labels) in
347  if debug then print_state state ;
348  match state with
349    | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
350      print_and_return_result (compute_result v)
351    | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
352      print_and_return_result IntValue.Int8.zero
353    | state -> exec debug cost_labels (step state)
354
355let interpret debug prog =
356  if debug then Printf.printf "*** Cminor ***\n\n%!" ;
357  match prog.main with
358    | None -> (IntValue.Int8.zero, [])
359    | Some main ->
360      let mem = init_mem prog in
361      let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
362      exec debug [] first_state
Note: See TracBrowser for help on using the repository browser.