source: Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml @ 1334

Last change on this file since 1334 was 1334, checked in by tranquil, 8 years ago

work on Cminor completed

File size: 14.7 KB
Line 
1open AST
2open Cminor
3
4module Mem = Driver.CminorMemory
5module Val = Mem.Value
6module LocalEnv = Map.Make(String)
7type local_env = Val.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 indexing = CostLabel.const_indexing
26
27type continuation = 
28    Ct_stop
29  | Ct_cont of statement*continuation
30        | Ct_ind_inc of CostLabel.index*continuation
31  | Ct_endblock of continuation
32  | Ct_returnto of
33      ident option*internal_function*Val.address*local_env*indexing*continuation
34
35type state = 
36    State_regular of
37      internal_function*statement*continuation*Val.address*local_env*
38                         (function_def Mem.memory)*indexing
39  | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
40  | State_return of Val.t*continuation*(function_def Mem.memory)
41
42let string_of_local_env lenv =
43  let f x v s = s ^ x ^ " = " ^ (Val.to_string v) ^ "  " in
44  LocalEnv.fold f lenv ""
45
46let string_of_expr = CminorPrinter.print_expression
47
48let string_of_args args =
49  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
50
51let rec string_of_statement = function
52  | St_skip -> "skip"
53  | St_assign (x, e) -> x ^ " = " ^ (string_of_expr e)
54  | St_store (q, e1, e2) ->
55    Printf.sprintf "%s[%s] = %s"
56      (Memory.string_of_quantity q) (string_of_expr e1) (string_of_expr e2)
57  | St_call (None, f, args, _)
58  | St_tailcall (f, args, _) -> (string_of_expr f) ^ (string_of_args args)
59  | St_call (Some x, f, args, _) ->
60    x ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
61  | St_seq _ -> "sequence"
62  | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
63  | St_loop _ -> "loop"
64  | St_block _ -> "block"
65  | St_exit n -> "exit " ^ (string_of_int n)
66  | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
67  | St_return None -> "return"
68  | St_return (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
69  | St_label (lbl, _) -> "label " ^ lbl
70  | St_goto lbl -> "goto " ^ lbl
71  | St_cost (lbl, _) ->
72                let lbl = CostLabel.string_of_cost_label lbl in
73                "cost " ^ lbl
74        | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0"
75        | St_ind_inc (_, i) -> "post-increment " ^ string_of_int i
76
77let print_state = function
78  | State_regular (_, stmt, _, sp, lenv, mem, i) ->
79    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:"
80      (string_of_local_env lenv)
81      (Mem.to_string mem)
82      (Val.to_string (value_of_address sp));
83                        Array.iter (fun a -> Printf.printf "%d, " a) i;
84                        Printf.printf "\nRegular state: %s\n\n%!"
85      (string_of_statement stmt)
86  | State_call (_, args, _, mem) ->
87    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
88      (Mem.to_string mem)
89      (MiscPottier.string_of_list " " Val.to_string args)
90  | State_return (v, _, mem) ->
91    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
92      (Mem.to_string mem)
93      (Val.to_string v)
94
95
96(* Global and local environment management *)
97
98let init_local_env args params vars =
99  let f_param lenv (x, _) v = LocalEnv.add x v lenv in
100  let f_var lenv (x, _) = LocalEnv.add x Val.undef lenv in
101  let lenv = List.fold_left2 f_param LocalEnv.empty params args in
102  List.fold_left f_var lenv vars
103
104let find_fundef f mem =
105  let addr = Mem.find_global mem f in
106  Mem.find_fun_def mem addr
107
108
109(* Expression evaluation *)
110
111module Eval_op (M : Memory.S) = struct
112
113  let concrete_stacksize = M.concrete_size
114
115  let ext_fun_of_sign = function
116    | AST.Signed -> M.Value.sign_ext
117    | AST.Unsigned -> M.Value.zero_ext
118
119  let cast_to_std t v = match t with
120    | AST.Sig_int (size, sign) -> (ext_fun_of_sign sign) v size M.int_size
121    | AST.Sig_float _ -> error_float ()
122    | AST.Sig_offset | AST.Sig_ptr -> v
123
124  let cast_from_std t v = match t with
125    | AST.Sig_int (size, _) -> (ext_fun_of_sign AST.Unsigned) v M.int_size size
126    | AST.Sig_float _ -> error_float ()
127    | AST.Sig_offset | AST.Sig_ptr -> v
128
129  let cst mem sp t = function
130    | Cst_int i -> cast_to_std t (M.Value.of_int i)
131    | Cst_float _ -> error_float ()
132    | Cst_addrsymbol id when M.mem_global mem id ->
133      value_of_address (M.find_global mem id)
134    | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
135    | Cst_stack -> value_of_address sp
136    | Cst_offset off -> M.Value.of_int (M.concrete_offset off)
137    | Cst_sizeof t' -> cast_to_std t (M.Value.of_int (M.concrete_size t'))
138
139  let fun_of_op1 = function
140    | Op_cast ((from_size, from_sign), to_size) ->
141      (fun v -> (ext_fun_of_sign from_sign) v from_size to_size)
142    | Op_negint -> M.Value.negint
143    | Op_notbool -> M.Value.notbool
144    | Op_notint -> M.Value.negint
145    | Op_id -> (fun v -> v)
146    | Op_ptrofint
147    | Op_intofptr ->
148      error "conversion between integers and pointers not supported yet."
149
150  let op1 ret_type t op v =
151    cast_from_std ret_type ((fun_of_op1 op) (cast_to_std t v))
152
153  let fun_of_op2 = function
154    | Op_add | Op_addp -> M.Value.add
155    | Op_sub | Op_subp | Op_subpp -> M.Value.sub
156    | Op_mul -> M.Value.mul
157    | Op_div -> M.Value.div
158    | Op_divu -> M.Value.divu
159    | Op_mod -> M.Value.modulo
160    | Op_modu -> M.Value.modulou
161    | Op_and -> M.Value.and_op
162    | Op_or -> M.Value.or_op
163    | Op_xor -> M.Value.xor
164    | Op_shl -> M.Value.shl
165    | Op_shr -> M.Value.shr
166    | Op_shru -> M.Value.shru
167    | Op_cmp Cmp_eq | Op_cmpp Cmp_eq -> M.Value.cmp_eq
168    | Op_cmp Cmp_ne | Op_cmpp Cmp_ne -> M.Value.cmp_ne
169    | Op_cmp Cmp_gt | Op_cmpp Cmp_gt -> M.Value.cmp_gt
170    | Op_cmp Cmp_ge | Op_cmpp Cmp_ge -> M.Value.cmp_ge
171    | Op_cmp Cmp_lt | Op_cmpp Cmp_lt -> M.Value.cmp_lt
172    | Op_cmp Cmp_le | Op_cmpp Cmp_le -> M.Value.cmp_le
173    | Op_cmpu Cmp_eq -> M.Value.cmp_eq_u
174    | Op_cmpu Cmp_ne -> M.Value.cmp_ne_u
175    | Op_cmpu Cmp_gt -> M.Value.cmp_gt_u
176    | Op_cmpu Cmp_ge -> M.Value.cmp_ge_u
177    | Op_cmpu Cmp_lt -> M.Value.cmp_lt_u
178    | Op_cmpu Cmp_le -> M.Value.cmp_le_u
179
180  let op2 ret_type t1 t2 op2 v1 v2 =
181    let v1 = cast_to_std t1 v1 in
182    let v2 = cast_to_std t2 v2 in
183    cast_from_std ret_type ((fun_of_op2 op2) v1 v2)
184end
185
186module Eval = Eval_op (Mem)
187
188let concrete_stacksize = Eval.concrete_stacksize
189let eval_constant = Eval.cst
190let eval_unop = Eval.op1
191let eval_binop = Eval.op2
192
193let type_of_expr (Cminor.Expr (_, t)) = t
194
195let rec eval_expression stack local_env memory (Cminor.Expr (ed, t)) =
196  match ed with
197    | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
198    | Id x -> error ("unknown local variable " ^ x ^ ".")
199    | Cst(c) -> (eval_constant memory stack t c,[])
200    | Op1(op,arg) -> 
201      let (v,l) = eval_expression stack local_env memory arg in
202      (eval_unop t (type_of_expr arg) op v,l)
203    | Op2(op, arg1, arg2) -> 
204      let (v1,l1) = eval_expression stack local_env memory arg1 in
205      let (v2,l2) = eval_expression stack local_env memory arg2 in
206      (eval_binop t (type_of_expr arg1) (type_of_expr arg2) op v1 v2,l1@l2) 
207    | Mem(q,a) -> 
208      let (v,l) = eval_expression stack local_env memory a in 
209      (Mem.loadq memory q (address_of_value v),l)
210    | Cond(a1,a2,a3) ->
211      let (v1,l1) = eval_expression stack local_env memory a1 in
212      if Val.is_true v1 then
213        let (v2,l2) = eval_expression stack local_env memory a2 in
214        (v2,l1@l2)
215      else
216        if Val.is_false v1 then
217          let (v3,l3) = eval_expression stack local_env memory a3 in
218          (v3,l1@l3)
219        else error "undefined conditional value."
220    | Exp_cost(lbl,e) -> 
221      let (v,l) = eval_expression stack local_env memory e in
222      (v,l@[lbl])
223
224let eval_exprlist sp lenv mem es =
225  let f (vs, cost_lbls) e =
226    let (v, cost_lbls') = eval_expression sp lenv mem e in
227    (vs @ [v], cost_lbls @ cost_lbls') in
228  List.fold_left f ([], []) es
229
230(* State transition *)
231
232let rec callcont = function
233  | Ct_cont(_,k) | Ct_endblock k | Ct_ind_inc(_,k) -> callcont k
234        | (Ct_stop | Ct_returnto _) as k -> k
235
236let findlabel lbl st k = 
237  let rec fdlbl k = function
238    St_skip                     -> None
239  | St_assign(_,_)              -> None
240  | St_store(_,_,_)             -> None
241  | St_call(_,_,_,_)            -> None
242  | St_tailcall(_,_,_)          -> None 
243  | St_seq(s1,s2)               -> 
244      (match fdlbl (Ct_cont(s2,k)) s1 with
245           None -> fdlbl k s2
246         | Some(v) -> Some(v)
247      )
248  | St_ifthenelse(_,s1,s2)      ->
249      (match fdlbl k s1 with
250           None -> fdlbl k s2
251         | Some(v) -> Some(v)
252      )
253  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
254  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
255  | St_exit(_)                  -> None
256  | St_switch(_,_,_)            -> None
257  | St_return(_)                -> None
258  | St_label(l,s)               -> if l=lbl then Some((s,k)) else None 
259  | St_goto(_)                  -> None
260  | St_cost (_,s) | St_ind_0(_,s) | St_ind_inc(s,_) -> fdlbl k s
261  in match fdlbl k st with
262      None -> assert false (*Wrong label*)
263    | Some(v) -> v
264
265
266let call_state sigma e m f params cont =
267  let (addr,l1) = eval_expression sigma e m f in
268  let fun_def = Mem.find_fun_def m (address_of_value addr) in
269  let (args,l2) = eval_exprlist sigma e m params in
270  (State_call(fun_def,args,cont,m),l1@l2)
271
272let eval_stmt f k sigma e m i s = match s, k with
273  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
274  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[])
275  | St_skip, (Ct_returnto _ as k) ->
276    (State_return (Val.undef,k,Mem.free m sigma),[])
277  | St_skip,Ct_ind_inc(ind,k) ->
278                CostLabel.continue_loop (Some ind) i;
279                (State_regular(f, s, k, sigma, e, m, i),[]) 
280  | St_skip,Ct_stop -> 
281    (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
282  | St_assign(x,exp),_ -> 
283    let (v,l) = eval_expression sigma e m exp in
284    let e = LocalEnv.add x v e in
285    (State_regular(f, St_skip, k, sigma, e, m, i),l)
286  | St_store(q,a1,a2),_ ->
287    let (v1,l1) = eval_expression sigma e m a1 in
288    let (v2,l2) = eval_expression sigma e m a2 in
289    let m = Mem.storeq m q (address_of_value v1) v2 in
290    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
291  | St_call(xopt,f',params,_),_ ->
292    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k))
293  | St_tailcall(f',params,_),_ -> 
294    call_state sigma e m f' params (callcont k)
295  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
296  | St_ifthenelse(exp,s1,s2),_ ->
297    let (v,l) = eval_expression sigma e m exp in
298    let next_stmt =
299      if Val.is_true v then s1
300      else
301        if Val.is_false v then s2
302        else error "undefined conditional value." in
303      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
304  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
305  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
306  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
307  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
308  | St_exit(n),Ct_endblock(k) ->
309    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[])
310  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
311  | St_goto(lbl),_ -> 
312    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
313    (State_regular(f,s2,k2,sigma,e,m,i),[])
314  | St_switch(exp,lst,def),_ ->
315    let (v,l) = eval_expression sigma e m exp in
316    if Val.is_int v then
317      try
318        let v = Val.to_int v in
319        let nb_exit =
320          if List.mem_assoc v lst then List.assoc v lst
321          else def in
322        (State_regular(f, St_exit nb_exit,k, sigma, e, m, i),l)
323      with _ -> error "int value too big."
324    else error "undefined switch value."
325  | St_return(None),_ ->
326    (State_return (Val.undef,callcont k,Mem.free m sigma),[])
327  | St_return(Some(a)),_ ->
328      let (v,l) = eval_expression sigma e m a in
329      (State_return (v,callcont k,Mem.free m sigma),l)
330  | St_cost(lbl,s),_ ->
331    (* applying current indexing on label *)
332    let lbl = CostLabel.apply_const_indexing i lbl in
333                (State_regular(f,s,k,sigma,e,m,i),[lbl])
334        | St_ind_0(ind,s),_ ->
335                CostLabel.enter_loop (Some ind) i;
336                (State_regular(f,s,k,sigma,e,m,i), [])
337        | St_ind_inc(s,ind),_ ->
338    (State_regular(f,s,Ct_ind_inc(ind,k),sigma,e,m,i), [])
339  | _ -> error "state malformation."
340
341
342module InterpretExternal = Primitive.Interpret (Mem)
343
344let interpret_external k mem f args =
345  let (mem', v) = match InterpretExternal.t mem f args with
346    | (mem', InterpretExternal.V vs) ->
347      let v = if List.length vs = 0 then Val.undef else List.hd vs in
348      (mem', v)
349    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
350  State_return (v, k, mem')
351
352let max_loop_index =
353  let f_expr _ _ = () in
354  let f_stmt stmt _ sub_stmts_res =
355        let curr_max = List.fold_left max 0 sub_stmts_res in
356        match stmt with
357          | Cminor.St_ind_0 (x, _) | Cminor.St_ind_inc (_, x) ->
358                                                 max (x+1) curr_max
359          | _ -> curr_max in
360  CminorFold.statement f_expr f_stmt
361
362let step_call vargs k m = function
363  | F_int f ->
364    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
365    let lenv = init_local_env vargs f.f_params f.f_vars in
366                let i = Array.make (max_loop_index f.f_body) 0 in 
367    State_regular(f,f.f_body,k,sp,lenv,m,i)
368  | F_ext f -> interpret_external k m f.ef_tag vargs
369
370let step = function
371  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
372  | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
373  | State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) ->
374    (State_regular(f,St_skip,k,sigma,e,m,i),[])
375  | State_return(v,Ct_returnto(Some x,f,sigma,e,i,k),m) ->
376    let e = LocalEnv.add x v e in
377    (State_regular(f,St_skip,k,sigma,e,m,i),[])
378  | _ -> error "state malformation."
379
380
381let init_mem prog =
382  let f_var mem (x, size, init_datas) = Mem.add_var mem x size init_datas in
383  let mem = List.fold_left f_var Mem.empty prog.vars in
384  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
385  List.fold_left f_fun_def mem prog.functs
386
387let compute_result v =
388  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
389  else IntValue.Int32.zero
390
391let rec exec debug trace (state, l) =
392  let cost_labels = l @ trace in
393  let print_and_return_result res =
394    if debug then Printf.printf "Result = %s\n%!"
395      (IntValue.Int32.to_string res) ;
396    (res, cost_labels) in
397  if debug then print_state state ;
398  match state with
399    | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
400      print_and_return_result (compute_result v)
401    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
402      print_and_return_result IntValue.Int32.zero
403    | state -> exec debug cost_labels (step state)
404
405let interpret debug prog =
406  Printf.printf "*** Cminor interpret ***\n%!" ;
407  match prog.main with
408    | None -> (IntValue.Int32.zero, [])
409    | Some main ->
410      let mem = init_mem prog in
411      let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
412      exec debug [] first_state
Note: See TracBrowser for help on using the repository browser.