src/clight/clightInterpret.ml

   1 module Mem = Driver.ClightMemory
   2 module Value = Driver.ClightMemory.Value
   3 module LocalEnv = Map.Make(String)
   4 type localEnv = Value.address LocalEnv.t
   5 type memory = Clight.fundef Mem.memory
   6
   7 open Clight
   8 open AST
   9
  10
  11 let error_prefix = "Clight 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   | Kstop
  27   | Kseq of statement*continuation
  28   | Kwhile of expr*statement*continuation
  29   | Kdowhile of expr*statement*continuation
  30   | Kfor2 of expr*statement*statement*continuation
  31   | Kfor3 of expr*statement*statement*continuation
  32   | Kswitch of continuation
  33   | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
  34
  35 type state =
  36   | State of cfunction*statement*continuation*localEnv*memory
  37   | Callstate of fundef*Value.t list*continuation*memory
  38   | Returnstate of Value.t*continuation*memory
  39
  40 let string_of_unop = function
  41   | Onotbool -> "!"
  42   | Onotint -> "~"
  43   | Oneg -> "-"
  44
  45 let string_of_binop = function
  46   | Oadd -> "+"
  47   | Osub -> "-"
  48   | Omul -> "*"
  49   | Odiv -> "/"
  50   | Omod -> "%"
  51   | Oand -> "&"
  52   | Oor  -> "|"
  53   | Oxor -> "^"
  54   | Oshl -> "<<"
  55   | Oshr -> ">>"
  56   | Oeq -> "=="
  57   | One -> "!="
  58   | Olt -> "<"
  59   | Ogt -> ">"
  60   | Ole -> "<="
  61   | Oge -> ">="
  62
  63 let string_of_signedness = function
  64   | Signed -> "signed"
  65   | Unsigned -> "unsigned"
  66
  67 let string_of_sized_int = function
  68   | I8 -> "char"
  69   | I16 -> "short"
  70   | I32 -> "int"
  71
  72 let rec string_of_ctype = function
  73   | Tvoid -> "void"
  74   | Tint (size, sign) ->
  75     (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
  76   | Tfloat _ -> error_float ()
  77   | Tpointer ty -> (string_of_ctype ty) ^ "*"
  78   | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
  79   | Tfunction _ -> assert false (* do not cast to a function type *)
  80   | Tstruct (id, _)
  81   | Tunion (id, _) -> id
  82   | Tcomp_ptr id -> id ^ "*"
  83
  84 let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
  85 and string_of_expr_descr = function
  86   | Econst_int i -> string_of_int i
  87   | Econst_float _ -> error_float ()
  88   | Evar x -> x
  89   | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
  90   | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
  91   | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
  92   | Ebinop (binop, e1, e2) ->
  93     "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
  94     "(" ^ (string_of_expr e2) ^ ")"
  95   | Ecast (ty, e) ->
  96     "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
  97   | Econdition (e1, e2, e3) ->
  98     "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
  99     ") : (" ^ (string_of_expr e3) ^ ")"
 100   | Eandbool (e1, e2) ->
 101     "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
 102   | Eorbool (e1, e2) ->
 103     "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
 104   | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
 105   | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
 106   | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
 107   | Ecall (f, arg, e) ->
 108     "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
 109
 110 let string_of_args args =
 111   "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
 112
 113 let rec string_of_statement = function
 114   | Sskip -> "skip"
 115   | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
 116   | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
 117   | Scall (Some e, f, args) ->
 118     (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
 119   | Ssequence _ -> "sequence"
 120   | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
 121   | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
 122   | Sdowhile _ -> "dowhile"
 123   | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
 124   | Sbreak -> "break"
 125   | Scontinue -> "continue"
 126   | Sreturn None -> "return"
 127   | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
 128   | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
 129   | Slabel (lbl, _) -> "label " ^ lbl
 130   | Sgoto lbl -> "goto " ^ lbl
 131   | Scost (lbl, _) -> "cost " ^ lbl
 132
 133 let string_of_local_env lenv =
 134   let f x addr s =
 135     s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
 136   LocalEnv.fold f lenv ""
 137
 138 let print_state = function
 139   | State (_, stmt, _, lenv, mem) ->
 140     Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
 141       (string_of_local_env lenv)
 142       (Mem.to_string mem)
 143       (string_of_statement stmt)
 144   | Callstate (_, args, _, mem) ->
 145     Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
 146       (Mem.to_string mem)
 147       (MiscPottier.string_of_list " " Value.to_string args)
 148   | Returnstate (v, _, mem) ->
 149     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
 150       (Mem.to_string mem)
 151       (Value.to_string v)
 152
 153
 154 (* Continuations and labels *)
 155
 156 let rec call_cont = function
 157   | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
 158   | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
 159   | k -> k
 160
 161 let rec seq_of_labeled_statement = function
 162   | LSdefault s -> s
 163   | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
 164
 165 let rec find_label1 lbl s k = match s with
 166    | Ssequence (s1,s2) ->
 167       (match find_label1 lbl s1 (Kseq (s2,k)) with
 168       | Some sk -> Some sk
 169       | None -> find_label1 lbl s2 k
 170       )
 171   | Sifthenelse (a,s1,s2) ->
 172       (match find_label1 lbl s1 k with
 173       | Some sk -> Some sk
 174       | None -> find_label1 lbl s2 k
 175       )
 176   | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
 177   | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
 178   | Sfor (a1,a2,a3,s1) ->
 179       (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
 180       | Some sk -> Some sk
 181       | None ->
 182           (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
 183           | Some sk -> Some sk
 184           | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
 185           ))
 186   | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
 187   | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
 188   | Scost (_,s') -> find_label1 lbl s' k
 189   | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
 190   | Scontinue | Sreturn _ | Sgoto _ -> None
 191
 192 and find_label_ls lbl sl k =  match sl with
 193   | LSdefault s -> find_label1 lbl s k
 194   | LScase (_,s,sl') ->
 195       (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
 196       | Some sk -> Some sk
 197       | None -> find_label_ls lbl sl' k
 198       )
 199
 200 let find_label lbl s k = match find_label1 lbl s k with
 201   | Some res -> res
 202   | _ -> assert false (* should be impossible *)
 203
 204 let rec select_switch i = function
 205   | LSdefault d -> LSdefault d
 206   | LScase (c,s,sl') when c=i-> LScase (c,s,sl')
 207   | LScase (_,_,sl') -> select_switch i sl'
 208
 209
 210 (* ctype functions *)
 211
 212 let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
 213
 214 let size_of_ctype = function
 215   | Tint (I8, _)  -> 1
 216   | Tint (I16, _) -> 2
 217   | Tint (I32, _) -> 4
 218   | Tfloat _ -> error_float ()
 219   | Tcomp_ptr _
 220   | Tpointer _
 221   | Tarray _
 222   | Tstruct _
 223   | Tunion _ -> Mem.ptr_size
 224   | _ -> assert false (* do not use on these arguments *)
 225
 226 let is_function_type = function
 227   | Tfunction _ -> true
 228   | _ -> false
 229
 230 let is_array_type = function
 231   | Tarray _ -> true
 232   | _ -> false
 233
 234 let is_complex_type = function
 235   | Tstruct _ | Tunion _ -> true
 236   | _ -> false
 237
 238 let is_big_type t = (is_array_type t) || (is_complex_type t)
 239
 240 let dest_type = function
 241   | Tpointer ty | Tarray (ty, _) -> ty
 242   | _ -> assert false (* do not use on these arguments *)
 243
 244
 245 (* Global and local environment management *)
 246
 247 let find_local x lenv =
 248   if LocalEnv.mem x lenv then LocalEnv.find x lenv
 249   else error ("Unknown local variable " ^ x ^ ".")
 250
 251 let find_global x mem =
 252   if Mem.mem_global mem x then Mem.find_global mem x
 253   else error ("Unknown global variable " ^ x ^ ".")
 254
 255 let find_symbol lenv mem x =
 256   if LocalEnv.mem x lenv then LocalEnv.find x lenv
 257   else
 258     if Mem.mem_global mem x then Mem.find_global mem x
 259     else error ("Unknown variable " ^ x ^ ".")
 260
 261 let find_fundef f mem =
 262   let addr = Mem.find_global mem f in
 263   Mem.find_fun_def mem addr
 264
 265
 266 (* Interpret *)
 267
 268 let byte_of_intsize = function
 269   | I8 -> 1
 270   | I16 -> 2
 271   | I32 -> 4
 272
 273 let choose_cast sign n m v =
 274   let f = match sign with
 275     | Signed -> Value.sign_ext
 276     | Unsigned -> Value.zero_ext in
 277   f v n m
 278
 279 let eval_cast = function
 280   (* Cast Integer *)
 281   | (v,Tint(isize,sign),Tint(isize',_)) ->
 282     choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
 283   | (v,_,_) -> v
 284
 285 let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
 286
 287 let eval_unop ret_ctype ((_, t) as e) op =
 288   let v = to_int32 e in
 289   let v = match op with
 290     | Onotbool -> Value.notbool v
 291     | Onotint -> Value.notint v
 292     | Oneg -> Value.negint v in
 293   eval_cast (v, t, ret_ctype)
 294
 295 let eval_add (v1,t1) (v2,t2) = match t1, t2 with
 296   | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
 297     let v = Value.mul (Value.of_int (sizeof ty)) v2 in
 298     Value.add v1 v
 299   | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
 300     let v = Value.mul (Value.of_int (sizeof ty)) v1 in
 301     Value.add v2 v
 302   | _ -> Value.add v1 v2
 303
 304 let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
 305   | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
 306     let v = Value.mul (Value.of_int (sizeof ty)) v2 in
 307     Value.sub v1 v
 308   | _ -> Value.sub v1 v2
 309
 310 let choose_sign op_signed op_unsigned v1 v2 t =
 311   let op = match t with
 312     | Tint (_, Signed) -> op_signed
 313     | Tint (_, Unsigned) -> op_unsigned
 314     | _ -> op_unsigned in
 315   op v1 v2
 316
 317 let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op =
 318   let v1 = to_int32 e1 in
 319   let v2 = to_int32 e2 in
 320   let e1 = (v1, t1) in
 321   let e2 = (v2, t2) in
 322   let v = match op with
 323     | Oadd -> eval_add e1 e2
 324     | Osub -> eval_sub e1 e2
 325     | Omul -> Value.mul v1 v2
 326     | Odiv -> choose_sign Value.div Value.divu v1 v2 t1
 327     | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1
 328     | Oand -> Value.and_op v1 v2
 329     | Oor -> Value.or_op v1 v2
 330     | Oxor -> Value.xor v1 v2
 331     | Oshl-> Value.shl v1 v2
 332     | Oshr-> Value.shr v1 v2
 333     | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1
 334     | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1
 335     | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1
 336     | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1
 337     | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1
 338     | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
 339   eval_cast (v, t1, ret_ctype)
 340
 341 let rec get_offset_struct v size id fields =
 342   let offsets = fst (Mem.concrete_offsets_size size) in
 343   let fields = List.combine (List.map fst fields) offsets in
 344   let off = Value.of_int (List.assoc id fields) in
 345   Value.add v off
 346
 347 let get_offset v id = function
 348   | Tstruct (_, fields) as t ->
 349     let size = ClightToCminor.sizeof_ctype t in
 350     get_offset_struct v size id fields
 351   | Tunion _ -> v
 352   | _ -> assert false (* do not use on these arguments *)
 353
 354 let is_true (v, _) = Value.is_true v
 355 let is_false (v, _) = Value.is_false v
 356
 357 let rec eval_expr localenv m (Expr (ee, tt)) =
 358   match ee with
 359     | Econst_int i ->
 360       let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
 361       ((v, tt),[])
 362     | Econst_float _ -> error_float ()
 363     | Evar id when is_function_type tt || is_big_type tt ->
 364       let v = value_of_address (find_symbol localenv m id) in
 365       ((v, tt), [])
 366     | Evar id ->
 367       let addr = find_symbol localenv m id in
 368       let v = Mem.load m (size_of_ctype tt) addr in
 369       ((v, tt), [])
 370     | Ederef e when is_function_type tt || is_big_type tt ->
 371       let ((v1,_),l1) = eval_expr localenv m e in
 372       ((v1,tt),l1)
 373     | Ederef e ->
 374       let ((v1,_),l1) = eval_expr localenv m e in
 375       let addr = address_of_value v1 in
 376       let v = Mem.load m (size_of_ctype tt) addr in
 377       ((v,tt),l1)
 378     | Eaddrof exp ->
 379       let ((addr,_),l) = eval_lvalue localenv m exp in
 380       ((value_of_address addr,tt),l)
 381     | Ebinop (op,exp1,exp2) ->
 382       let (v1,l1) = eval_expr localenv m exp1 in
 383       let (v2,l2) = eval_expr localenv m exp2 in
 384       ((eval_binop tt v1 v2 op,tt),l1@l2)
 385     | Eunop (op,exp) ->
 386       let (e1,l1) = eval_expr localenv m exp in
 387       ((eval_unop tt e1 op,tt),l1)
 388     | Econdition (e1,e2,e3) ->
 389       let (v1,l1) = eval_expr localenv m e1 in
 390       if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
 391       else
 392         if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
 393       else (v1,l1)
 394     | Eandbool (e1,e2) ->
 395       let (v1,l1) = eval_expr localenv m e1 in
 396       if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
 397       else (v1,l1)
 398     | Eorbool (e1,e2) ->
 399       let (v1,l1) = eval_expr localenv m e1 in
 400       if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
 401       else (v1,l1)
 402     | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
 403     | Efield (e1,id) ->
 404       let ((v1,t1),l1) = eval_expr localenv m e1 in
 405       let addr = address_of_value (get_offset v1 id t1) in
 406       ((Mem.load m (size_of_ctype tt) addr, tt), l1)
 407     | Ecost (lbl,e1) ->
 408       let (v1,l1) = eval_expr localenv m e1 in
 409       (v1,lbl::l1)
 410     | Ecall _ -> assert false (* only used by the annotation process *)
 411     | Ecast (cty,exp) ->
 412       let ((v,ty),l1) = eval_expr localenv m exp in
 413       ((eval_cast (v,ty,cty),tt),l1)
 414
 415 and eval_lvalue localenv m (Expr (e,t)) = match e with
 416   | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
 417   | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
 418   | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
 419   | Evar id -> ((find_symbol localenv m id,t),[])
 420   | Ederef ee ->
 421     let ((v,_),l1) = eval_expr localenv m ee in
 422     ((address_of_value v,t),l1)
 423   | Efield (ee,id) ->
 424     let ((v,tt),l1) = eval_expr localenv m ee in
 425     let v' = get_offset v id tt in
 426     ((address_of_value v', t), l1)
 427   | Ecost (lbl,ee) ->
 428     let (v,l) = eval_lvalue localenv m ee in
 429     (v,lbl::l)
 430   | Ecall _ -> assert false (* only used in the annotation process *)
 431
 432 let eval_exprlist lenv mem es =
 433   let f (vs, cost_lbls) e =
 434     let ((v, _), cost_lbls') = eval_expr lenv mem e in
 435     (vs @ [v], cost_lbls @ cost_lbls') in
 436   List.fold_left f ([], []) es
 437
 438
 439 let bind (mem, lenv) (x, ty) v =
 440   let (mem, addr) = Mem.alloc mem (sizeof ty) in
 441   let mem = Mem.store mem (sizeof ty) addr v in
 442   let lenv = LocalEnv.add x addr lenv in
 443   (mem, lenv)
 444
 445 let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
 446
 447 let init_fun_env mem params args vars =
 448   let lenv = LocalEnv.empty in
 449   let (mem, lenv) =
 450     try List.fold_left2 bind (mem, lenv) params args
 451     with Invalid_argument _ -> error "wrong size of arguments." in
 452   List.fold_left bind_var (mem, lenv) vars
 453
 454 let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
 455
 456
 457 let free_local_env mem lenv =
 458   let f _ addr mem = Mem.free mem addr in
 459   LocalEnv.fold f lenv mem
 460
 461 let condition v a_true a_false =
 462   if Value.is_false v then a_false
 463   else if Value.is_true v then a_true
 464   else error "undefined condition guard value."
 465
 466 let eval_stmt f k e m s = match s, k with
 467   | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
 468   | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
 469   | Sskip, Kdowhile(a,s,k) ->
 470     let ((v1, _),l1) = eval_expr e m a in
 471     let a_false = (State(f,Sskip,k,e,m),l1) in
 472     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
 473     condition v1 a_true a_false
 474   | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
 475   | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
 476   | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
 477   | Sskip, Kcall _ ->
 478     let m' = free_local_env m e in
 479     (Returnstate(Value.undef,k,m'),[])
 480   | Sassign(a1, a2), _ ->
 481     let ((v1,t1),l1) = (eval_lvalue e m a1) in
 482     let ((v2,t2),l2) = eval_expr e m a2 in
 483     (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
 484   | Scall(None,a,al), _ ->
 485     let ((v1,_),l1) = eval_expr e m a in
 486     let fd = Mem.find_fun_def m (address_of_value v1) in
 487     let (vargs,l2) = eval_exprlist e m al in
 488     (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
 489   | Scall(Some lhs,a,al), _ ->
 490     let ((v1,_),l1) = eval_expr e m a in
 491     let fd = Mem.find_fun_def m (address_of_value v1) in
 492     let (vargs,l2) = eval_exprlist e m al in
 493     let (vt3,l3) = eval_lvalue e m lhs in
 494     (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
 495   | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
 496   | Sifthenelse(a,s1,s2), _ ->
 497     let ((v1,_),l1) = eval_expr e m a in
 498     let a_true = (State(f,s1,k,e,m),l1) in
 499     let a_false = (State(f,s2,k,e,m),l1) in
 500     condition v1 a_true a_false
 501   | Swhile(a,s), _ ->
 502     let ((v1,_),l1) = eval_expr e m a in
 503     let a_false = (State(f,Sskip,k,e,m),l1) in
 504     let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
 505     condition v1 a_true a_false
 506   | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
 507   | Sfor(Sskip,a2,a3,s), _ ->
 508     let ((v1,_),l1) = eval_expr e m a2 in
 509     let a_false = (State(f,Sskip,k,e,m),l1) in
 510     let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
 511     condition v1 a_true a_false
 512   | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
 513   | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
 514   | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
 515   | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
 516   | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
 517   | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
 518   | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
 519   | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
 520   | Scontinue, Kdowhile(a,s,k) ->
 521     let ((v1,_),l1) = eval_expr e m a in
 522     let a_false = (State(f,Sskip,k,e,m),l1) in
 523     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
 524     condition v1 a_true a_false
 525   | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
 526   | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
 527   | Sreturn None, _ ->
 528     let m' = free_local_env m e in
 529     (Returnstate(Value.undef,(call_cont k),m'),[])
 530   | Sreturn (Some a), _ ->
 531     let ((v1,_),l1) = eval_expr e m a  in
 532     let m' = free_local_env m e in
 533     (Returnstate(v1,call_cont k,m'),l1)
 534   | Sswitch(a,sl), _ ->
 535     let ((v,_),l) = eval_expr e m a in
 536     let n = Value.to_int v in
 537     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
 538   | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
 539   | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
 540   | Sgoto lbl, _ ->
 541     let (s', k') = find_label lbl f.fn_body (call_cont k) in
 542     (State(f,s',k',e,m),[])
 543   | _ -> assert false (* should be impossible *)
 544
 545
 546 module InterpretExternal = Primitive.Interpret (Mem)
 547
 548 let interpret_external k mem f args =
 549   let (mem', v) = match InterpretExternal.t mem f args with
 550     | (mem', InterpretExternal.V vs) ->
 551       let v = if List.length vs = 0 then Value.undef else List.hd vs in
 552       (mem', v)
 553     | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
 554   Returnstate (v, k, mem')
 555
 556 let step_call args cont mem = function
 557   | Internal f ->
 558     let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
 559     State (f, f.fn_body, cont, e, mem')
 560   | External(id,targs,tres) when List.length targs = List.length args ->
 561     interpret_external cont mem id args
 562   | External(id,_,_) ->
 563     error ("wrong size of arguments when calling external " ^ id ^ ".")
 564
 565 let step = function
 566   | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
 567   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
 568   | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
 569   | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
 570     let m' = assign m v ty vv in
 571     (State(f,Sskip,k,e,m'),[])
 572   | _ -> error "state malformation."
 573
 574
 575 let data_of_init_data = function
 576   | Init_int8 i         -> Data_int8 i
 577   | Init_int16 i        -> Data_int16 i
 578   | Init_int32 i        -> Data_int32 i
 579   | Init_float32 f      -> error_float ()
 580   | Init_float64 f      -> error_float ()
 581   | Init_space i        -> error "bad global initialization style."
 582   | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
 583
 584 let datas_of_init_datas = function
 585   | [Init_space _] -> None
 586   | l -> Some (List.map data_of_init_data l)
 587
 588 let init_mem prog =
 589   let f_var mem ((x, init_datas), ty) =
 590     Mem.add_var mem x (ClightToCminor.sizeof_ctype ty)
 591       (datas_of_init_datas init_datas) in
 592   let mem = List.fold_left f_var Mem.empty prog.prog_vars in
 593   let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
 594   List.fold_left f_fun_def mem prog.prog_funct
 595
 596 let compute_result v =
 597   if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
 598   else IntValue.Int32.zero
 599
 600 let rec exec debug trace (state, l) =
 601   let cost_labels = l @ trace in
 602   let print_and_return_result res =
 603     if debug then Printf.printf "Result = %s\n%!"
 604       (IntValue.Int32.to_string res) ;
 605     (res, cost_labels) in
 606   if debug then print_state state ;
 607   match state with
 608     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
 609       print_and_return_result (compute_result v)
 610     | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
 611       print_and_return_result IntValue.Int32.zero
 612     | state -> exec debug cost_labels (step state)
 613
 614 let interpret debug prog =
 615   Printf.printf "*** Clight interpret ***\n%!" ;
 616   match prog.prog_main with
 617     | None -> (IntValue.Int32.zero, [])
 618     | Some main ->
 619       let mem = init_mem prog in
 620       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
 621       exec debug [] first_state