src/cminor/cminorInterpret.ml

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