Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (10 years ago)
Author:
ayache
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r619 r740  
    44module Mem = Driver.CminorMemory
    55module Value = Mem.Value
    6 module Valtbl = Hashtbl.Make(Value)
    7 
    8 
    9 let 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 
    15 type local_env = (ident,Value.t) Hashtbl.t
     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 *)
    1624
    1725type continuation =
     
    2028  | Ct_endblock of continuation
    2129  | Ct_returnto of
    22       ident option*internal_function*Value.t*local_env*continuation
     30      ident option*internal_function*Value.address*local_env*continuation
    2331
    2432type state =
    2533    State_regular of
    26       internal_function*statement*continuation*Value.t*local_env*(function_def Mem.memory)
     34      internal_function*statement*continuation*Value.address*local_env*(function_def Mem.memory)
    2735  | State_call of function_def*Value.t list*continuation*(function_def Mem.memory)
    2836  | State_return of Value.t*continuation*(function_def Mem.memory)
    2937
    30 (* Local environment abstraction *)
    31 
    32 let get_local_value e id =
    33   try Hashtbl.find e id
    34   with Not_found -> assert false (*Wrong ident*)
    35 
    36 let set_local_value e id v = Hashtbl.add e id v
    37 
    38 (* Create_local_env :
    39 * constructs the local environement from effective parameters. *)
    40 let 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 
    56 let 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 
    62 let 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 *)
    85 let symbol g id = let (id_b,b_fd) = g in
    86 try Hashtbl.find id_b id
    87 with Not_found -> assert false
    88 
    89 (* Funct : returns the definition of the function located in block b *)
    90 let funct g b = let (id_b,b_fd) = g in
    91 try Valtbl.find b_fd b
    92 with Not_found -> assert false
    93 
     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
    9497
    9598
    9699(* Expression evaluation *)
    97100
    98 let 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 
    104 let 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 
    123 let 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.modulou 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 
    163 let 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,[])
     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,[])
    166172  | Op1(op,arg) ->
    167       let (v,l) = eval_expression global_env stack local_env memory arg in
    168       (eval_unop v op,l)
     173    let (v,l) = eval_expression stack local_env memory arg in
     174    (eval_unop op v,l)
    169175  | 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    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)
    176182  | 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*)
     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."
    185192  | Exp_cost(lbl,e) ->
    186       let (v,l) = eval_expression global_env stack local_env memory e in
    187         (v,l@[lbl])
     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
    188201
    189202(* State transition *)
     
    224237    | Some(v) -> v
    225238
    226 (*FIXME To move in AST*)
    227 let 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 
    241 let 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 
    265 let 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 
    287 let 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
     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
    353300      (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 
    369 let 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 
    391 let 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))
     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
    406336
    407337let compute_result v =
     
    409339  else IntValue.Int8.zero
    410340
    411 let interpret debug prog = match prog.main with
    412   | None -> (IntValue.Int8.zero, [])
    413   | Some main ->
    414       let (m,global_env) = initmem_cminor prog in
    415       let first_state = (State_call (
    416                            funct global_env (symbol global_env main),
    417                            [], Ct_stop,m),[]) in
    418       let rec exec l = function
    419         | (State_return(v,Ct_stop,m),lbl) ->
    420 (*
    421             if debug then (
    422               print_string ("Result: "^(Value.to_string v));
    423               print_string ("\nMemory dump: \n");
    424               Mem.print m
    425             );
    426 *)
    427           let (res, cost_labels) as trace = (compute_result v, lbl@l) in
    428           if debug then
    429             Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ;
    430           trace
    431         | (State_regular(_,St_skip,Ct_stop,_,_,m),lbl) ->
    432 (*
    433             if debug then (
    434               print_string ("Result: (implicit return)\n");
    435               print_string ("\nMemory dump: \n");
    436               Mem.print m
    437             );
    438 *)
    439           let (res, cost_labels) as trace = (IntValue.Int8.zero, lbl@l) in
    440           if debug then
    441             Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ;
    442           trace
    443         | (state,lbl) ->
    444 (*
    445             if debug then print_string ((string_of_state state)^"\n");
    446 *)
    447             exec (lbl@l) (state_transition state global_env)
    448       in
    449 (*
    450       if debug then print_string ">------------------- Interpret Cminor -------------------<\n";
    451 *)
    452       (exec [] first_state)
     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 TracChangeset for help on using the changeset viewer.