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.

Location:
Deliverables/D2.2/8051/src/cminor
Files:
9 edited

Legend:

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

    r486 r740  
    1010  | Op1 of AST.op1 * expression
    1111  | Op2 of AST.op2 * expression * expression
    12   | Mem of Memory.memory_q * expression          (* Memory read *)
     12  | Mem of Memory.quantity * expression          (* Memory read *)
    1313  | Cond of expression * expression * expression (* Ternary expression *)
    1414  | Exp_cost of CostLabel.t * expression         (* Labelled expression *)
     
    1717  | St_skip
    1818  | St_assign of AST.ident * expression
    19   | St_store of Memory.memory_q * expression * expression
     19  | St_store of Memory.quantity * expression * expression
    2020
    2121  (* Function call. Parameters are an optional variable to store the
  • Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

    r640 r740  
    2020let increment cost_id incr =
    2121  let cost = Cminor.Cst (AST.Cst_addrsymbol cost_id) in
    22   let load = Cminor.Mem (Memory.MQ_int32, cost) in
     22  let load = Cminor.Mem (Memory.QInt 4, cost) in
    2323  let incr = Cminor.Op2 (AST.Op_add, load, Cminor.Cst (AST.Cst_int incr)) in
    24   Cminor.St_store (Memory.MQ_int32, cost, incr)
     24  Cminor.St_store (Memory.QInt 4, cost, incr)
    2525
    2626
  • 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
  • Deliverables/D2.2/8051/src/cminor/cminorLexer.mll

    r486 r740  
    8181  | "intoffloat"    { INTOFFLOAT }
    8282  | "intuoffloat"    { INTUOFFLOAT }
     83  | "ptr" { PTR }
    8384  | "{"    { LBRACE }
    8485(*  | "{{"    { LBRACELBRACE } *)
  • Deliverables/D2.2/8051/src/cminor/cminorParser.mly

    r486 r740  
    11/* Adapted from Leroy's CompCert */
     2/* TODO: check coherence with CminorPrinter */
    23
    34/* tokens ALLOC, DOLLAR, IN, LET, p_let were unused and have been removed */
     
    5758    | ROp1 of op1 * rexpr
    5859    | ROp2 of op2 * rexpr * rexpr
    59     | RMem of memory_q * rexpr
     60    | RMem of Memory.quantity * rexpr
    6061    | RCond of rexpr * rexpr * rexpr
    6162    | RCall of rexpr * rexpr list * signature
     
    121122            prepend_seq !convert_accu (St_assign (id, c))
    122123
    123   (* [mkstore chunk e1 e2] creates the AST statement associated to the Cminor
     124  (* [mkstore size e1 e2] creates the AST statement associated to the Cminor
    124125     instruction
    125        chunk[e1] = e2;
     126       size[e1] = e2;
    126127     where [e1] and [e2] are expressions with possible function calls *)
    127   let mkstore chunk e1 e2 =
     128  let mkstore size e1 e2 =
    128129    convert_accu := [];
    129130    let c1 = convert_rexpr e1 in
    130131    let c2 = convert_rexpr e2 in
    131       prepend_seq !convert_accu (St_store (chunk, c1, c2))
     132      prepend_seq !convert_accu (St_store (size, c1, c2))
    132133
    133134  (* [mkifthenelse e s1 s2] creates the AST statement associated to the Cminor
     
    318319%token VOID
    319320%token GOTO BLOCK
     321%token PTR
    320322
    321323/* Unused */
     
    384386  | LBRACKET INTLIT RBRACKET       { AST.Data_reserve $2 }
    385387;
     388
     389quantity:
     390    INTLIT { Memory.QInt $1 }
     391  | PTR    { Memory.QPtr }
    386392
    387393init_data_list:
     
    462468    expr SEMICOLON                         { mkeval $1 }
    463469  | IDENT EQUAL expr SEMICOLON             { mkassign $1 $3 }
    464   | memory_q LBRACKET expr RBRACKET EQUAL expr SEMICOLON
     470  | quantity LBRACKET expr RBRACKET EQUAL expr SEMICOLON
    465471      { mkstore $1 $3 $6 }
    466472  | IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 }
     
    565571  | expr GREATERF expr                  { ROp2 (Op_cmpf Cmp_gt, $1, $3) }
    566572  | expr GREATEREQUALF expr             { ROp2 (Op_cmpf Cmp_ge, $1, $3) }
    567   | memory_q LBRACKET expr RBRACKET     { RMem ($1, $3) }
     573  | quantity LBRACKET expr RBRACKET       { RMem ($1, $3) }
    568574  | expr AMPERSANDAMPERSAND expr        { RCond ($1, $3, RCst (Cst_int 0)) }
    569575  | expr BARBAR expr                    { RCond ($1, RCst (Cst_int 1), $3) }
     
    584590;
    585591
    586 memory_q:
    587     INT8S   { MQ_int8signed }
    588   | INT8U   { MQ_int8unsigned }
    589   | INT16S  { MQ_int16signed }
    590   | INT16U  { MQ_int16unsigned }
    591   | INT32   { MQ_int32 }
    592   | INT     { MQ_int32 }
    593   | FLOAT32 { MQ_float32 }
    594   | FLOAT64 { MQ_float64 }
    595   | FLOAT   { MQ_float64 }
    596 ;
    597 
    598592type_:
    599593    INT   { Sig_int }
  • Deliverables/D2.2/8051/src/cminor/cminorPointers.ml

    r486 r740  
    44
    55
    6 (** [is_pointer ptrs e] returns true iff the expression [e] represents an
     6(** [is_pointer ptrs e] returns true only if the expression [e] represents an
    77    address when considering that the variables in the set [ptrs] are
    88    pointers. *)
     
    1515  | Cminor.Op1 (AST.Op_ptrofint, _) -> true
    1616  | Cminor.Op2 (AST.Op_addp, _, _) | Cminor.Op2 (AST.Op_subp, _, _) -> true
    17   | Cminor.Mem (Memory.MQ_pointer, _) -> true
    1817  | Cminor.Cond (_, e2, e3) -> (is_pointer ptrs e2) || (is_pointer ptrs e3)
    1918  | Cminor.Exp_cost (_, e) -> is_pointer ptrs e
     
    109108    statement, if any. [ptrs] is a set of already known pointer variables.  *)
    110109
    111 let statement_pointers type_ret stmt ptrs =
     110let statement_pointers ret_type stmt ptrs =
    112111  CminorFold.statement_left (fun _ _ -> StringTools.Set.empty)
    113     (f_statement_pointers type_ret ptrs) stmt
     112    (f_statement_pointers ret_type ptrs) stmt
     113
     114
     115(** [init_pointer def] returns the local variables or parameters of a function
     116    that can be deduced as pointers from the signature and the declarations of
     117    the function. *)
     118
     119let init_pointers def =
     120  let ptrs = StringTools.Set.empty in
     121  (* Adding the parameter pointers. *)
     122  let f ptrs x = function
     123    | AST.Sig_ptr -> StringTools.Set.add x ptrs
     124    | _ -> ptrs in
     125  let ptrs =
     126    List.fold_left2 f ptrs def.Cminor.f_params def.Cminor.f_sig.AST.args in
     127  (* Adding the local pointers. *)
     128  let f ptrs x =
     129    if List.mem x def.Cminor.f_ptrs then StringTools.Set.add x ptrs
     130    else
     131      if StringTools.Set.mem x ptrs then
     132        (* Case where a parameter with the same name is a pointer. Thus, for the
     133           moment, it is in [ptrs]. But only the local can be seen inside the
     134           function and it is not a pointer, so we have to remove it. *)
     135        StringTools.Set.remove x ptrs
     136      else ptrs in
     137  List.fold_left f ptrs def.Cminor.f_vars
    114138
    115139
     
    126150  (* The pointers of a function are found by iterating one step of collecting
    127151     the pointers until a fixpoint is reached. *)
     152  let ptrs = init_pointers def in
    128153  let ptrs =
    129154    fixpoint
    130       (statement_pointers def.Cminor.f_sig.AST.res def.Cminor.f_body)
    131       StringTools.Set.empty in
     155      (statement_pointers def.Cminor.f_sig.AST.res def.Cminor.f_body) ptrs in
    132156  let ptrs = StringTools.Set.fold (fun x l -> x :: l) ptrs [] in
    133157  { def with Cminor.f_ptrs = ptrs }
  • Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml

    r486 r740  
    108108        (print_op2 op2)
    109109        (add_parenthesis e2)
    110   | Cminor.Mem (chunk, e) ->
    111       Printf.sprintf "%s[%s]" (Memory.string_of_memory_q chunk) (print_expression e)
     110  | Cminor.Mem (q, e) ->
     111      Printf.sprintf "%s[%s]" (Memory.string_of_quantity q) (print_expression e)
    112112  | Cminor.Cond (e1, e2, e3) ->
    113113      Printf.sprintf "%s ? %s : %s"
     
    131131
    132132
    133 let print_locals n vars =
    134   let rec aux = function
    135     | [] -> ""
    136     | [id] -> id
    137     | id :: vars -> id ^ ", " ^ (aux vars)
    138   in
    139   match vars with
    140     | [] -> ""
    141     | _ -> Printf.sprintf "%svar %s;\n\n" (n_spaces n) (aux vars)
     133let print_locals vars =
     134  (MiscPottier.string_of_list ", " (fun x -> x) vars ^
     135   (if vars = [] then "" else ";"))
    142136
    143137
     
    153147  | Cminor.St_assign (id, e) ->
    154148      Printf.sprintf "%s%s = %s;\n" (n_spaces n) id (print_expression e)
    155   | Cminor.St_store (chunk, e1, e2) ->
     149  | Cminor.St_store (q, e1, e2) ->
    156150      Printf.sprintf "%s%s[%s] = %s;\n"
    157151        (n_spaces n)
    158         (Memory.string_of_memory_q chunk)
     152        (Memory.string_of_quantity q)
    159153        (print_expression e1)
    160154        (print_expression e2)
     
    220214
    221215let print_internal f_name f_def =
    222   Printf.sprintf "\"%s\" (%s) : %s {\n\n  stack %d;\n\n%s%s\n}\n\n\n"
     216  Printf.sprintf "\"%s\" (%s) : %s {\n\n  stack %d;\n\n  vars: %s\n  pointers: %s\n\n%s}\n\n\n"
    223217    f_name
    224218    (print_args (List.map (fun id -> Cminor.Id id) f_def.Cminor.f_params))
    225219    (print_sig f_def.Cminor.f_sig)
    226220    f_def.Cminor.f_stacksize
    227     (print_locals 2 f_def.Cminor.f_vars)
     221    (print_locals f_def.Cminor.f_vars)
     222    (print_locals f_def.Cminor.f_ptrs)
    228223    (print_body 2 f_def.Cminor.f_body)
    229224
  • Deliverables/D2.2/8051/src/cminor/cminorPrinter.mli

    r486 r740  
    55val print_expression : Cminor.expression -> string
    66
     7val print_body : int (* indentation *) -> Cminor.statement -> string
     8
    79val string_of_statement : Cminor.statement -> string
    810
  • Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

    r486 r740  
    77let error_prefix = "Cminor to RTLabs"
    88let error = Error.global_error error_prefix
     9let error_float () = error "float not supported."
    910
    1011
    1112(* Helper functions *)
    1213
    13 let ptr_nb_ints = Driver.TargetArch.ptr_size / Driver.TargetArch.int_size
    14 
    15 let rec freshs runiverse n =
    16   if n = 0 then []
    17   else (Register.fresh runiverse) :: (freshs runiverse (n-1))
    18 
    19 let int_size_of_type = function
    20   | AST.Type_void -> 0
    21   | AST.Type_ret AST.Sig_int -> 1
    22   | AST.Type_ret AST.Sig_ptr -> ptr_nb_ints
    23   | AST.Type_ret AST.Sig_float -> error "floats not handled."
    24 
    25 let fresh_type runiverse ty = freshs runiverse (int_size_of_type ty)
    26 
    27 let fresh_result runiverse def = fresh_type runiverse def.Cminor.f_sig.AST.res
    28 
    29 let type_of_local def x =
    30   if List.mem x def.Cminor.f_ptrs then AST.Type_ret AST.Sig_ptr
    31   else
    32     if List.mem x def.Cminor.f_vars then AST.Type_ret AST.Sig_int
    33     else
    34       let n = MiscPottier.index_of x def.Cminor.f_params in
    35       AST.Type_ret (List.nth def.Cminor.f_sig.AST.args n)
    36 
    37 let type_of_cst = function
    38   | AST.Cst_int _ -> AST.Sig_int
    39   | AST.Cst_float _ -> error "floats not handled."
    40   | AST.Cst_addrsymbol _ | AST.Cst_stackoffset _ -> AST.Sig_ptr
    41 
    42 let type_of_op1 = function
     14let is_pointer_op1 = function
    4315  | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned
    4416  | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint
    45   | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr ->
    46       AST.Sig_int
     17  | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr
    4718  | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint
    4819  | AST.Op_floatofintu ->
    49       AST.Sig_float
     20      false
    5021  | AST.Op_ptrofint ->
    51       AST.Sig_ptr
     22      true
    5223  | AST.Op_id ->
    53       assert false (* Dependent on argument. Treated in type_of_expr *)
    54 
    55 let type_of_op2 = function
     24      assert false (* Dependent on argument. Treated in type_of_expr. *)
     25
     26let is_pointer_op2 = function
    5627  | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod
    5728  | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr
    58   | AST.Op_shru ->
    59       AST.Sig_int
    60   | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf ->
    61       AST.Sig_float
     29  | AST.Op_shru
     30  | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf
    6231  | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ ->
    63       AST.Sig_int
     32      false
    6433  | AST.Op_addp | AST.Op_subp ->
    65       AST.Sig_ptr
    66 
    67 let rec type_of_expr def = function
    68   | Cminor.Id x -> type_of_local def x
    69   | Cminor.Cst cst -> AST.Type_ret (type_of_cst cst)
    70   | Cminor.Op1 (AST.Op_id, e) -> type_of_expr def e
    71   | Cminor.Op1 (op1, _) -> AST.Type_ret (type_of_op1 op1)
    72   | Cminor.Op2 (op2, _, _) -> AST.Type_ret (type_of_op2 op2)
    73   | Cminor.Mem (mq, _) -> AST.Type_ret (Memory.type_of_memory_q mq)
    74   | Cminor.Cond _ -> AST.Type_ret AST.Sig_int
    75   | Cminor.Exp_cost (_, e) -> type_of_expr def e
    76 
    77 let fresh_local runiverse def x =
    78   fresh_type runiverse (type_of_local def x)
    79 
    80 let allocate (rtlabs_fun : RTLabs.internal_function) (n : int)
    81     : RTLabs.internal_function * Register.t list =
    82   let rs = freshs rtlabs_fun.RTLabs.f_runiverse n in
     34      true
     35
     36let rec is_pointer ptrs = function
     37  | Cminor.Id x -> List.mem x ptrs
     38  | Cminor.Cst (AST.Cst_int _)
     39  | Cminor.Cst (AST.Cst_float _) -> false
     40  | Cminor.Cst (AST.Cst_addrsymbol _)
     41  | Cminor.Cst (AST.Cst_stackoffset _) -> true
     42  | Cminor.Op1 (AST.Op_id, e) -> is_pointer ptrs e
     43  | Cminor.Op1 (op1, _) -> is_pointer_op1 op1
     44  | Cminor.Op2 (op2, _, _) -> is_pointer_op2 op2
     45  | Cminor.Mem (q, _) -> q = Memory.QPtr
     46  | Cminor.Cond _ -> false
     47  | Cminor.Exp_cost (_, e) -> is_pointer ptrs e
     48
     49let allocate (rtlabs_fun : RTLabs.internal_function) (is_pointer : bool)
     50    : RTLabs.internal_function * Register.t =
     51  let r = Register.fresh rtlabs_fun.RTLabs.f_runiverse in
    8352  let rtlabs_fun =
    84     { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [rs] } in
    85   (rtlabs_fun, rs)
     53    { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [r] } in
     54  let rtlabs_fun =
     55    if is_pointer then
     56      { rtlabs_fun with RTLabs.f_ptrs = rtlabs_fun.RTLabs.f_ptrs @ [r] }
     57    else rtlabs_fun in
     58  (rtlabs_fun, r)
    8659
    8760let allocate_expr
    88     (def        : Cminor.internal_function)
     61    (ptrs       : AST.ident list)
    8962    (rtlabs_fun : RTLabs.internal_function)
    9063    (e          : Cminor.expression)
    91     : (RTLabs.internal_function * Register.t list) =
    92   allocate rtlabs_fun (int_size_of_type (type_of_expr def e))
    93 
    94 type local_env = Register.t list StringTools.Map.t
    95 
    96 let find_local (lenv : local_env) (x : AST.ident) : Register.t list =
     64    : (RTLabs.internal_function * Register.t) =
     65  allocate rtlabs_fun (is_pointer ptrs e)
     66
     67type local_env = Register.t StringTools.Map.t
     68
     69let find_local (lenv : local_env) (x : AST.ident) : Register.t =
    9770  if StringTools.Map.mem x lenv then StringTools.Map.find x lenv
    9871  else error ("Unknown local \"" ^ x ^ "\".")
    9972
    100 let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t list =
     73let find_olocal
     74    (rtlabs_fun : RTLabs.internal_function)
     75    (lenv       : local_env)
     76    (ox         : AST.ident option)
     77    : RTLabs.internal_function * Register.t =
    10178  match ox with
    102     | None -> []
    103     | Some x -> find_local lenv x
     79    | None -> allocate rtlabs_fun false
     80    | Some x -> (rtlabs_fun, find_local lenv x)
    10481
    10582let choose_destination
    106     (def        : Cminor.internal_function)
     83    (ptrs       : AST.ident list)
    10784    (rtlabs_fun : RTLabs.internal_function)
    10885    (lenv       : local_env)
    10986    (e          : Cminor.expression)
    110     : RTLabs.internal_function * Register.t list =
     87    : RTLabs.internal_function * Register.t =
    11188  match e with
    11289    | Cminor.Id x -> (rtlabs_fun, find_local lenv x)
    113     | _ -> allocate_expr def rtlabs_fun e
     90    | _ -> allocate_expr ptrs rtlabs_fun e
    11491
    11592let choose_destinations
    116     (def        : Cminor.internal_function)
     93    (ptrs       : AST.ident list)
    11794    (rtlabs_fun : RTLabs.internal_function)
    11895    (lenv       : local_env)
    11996    (args       : Cminor.expression list)
    120     : RTLabs.internal_function * Register.t list list =
     97    : RTLabs.internal_function * Register.t list =
    12198  let f (rtlabs_fun, regs) e =
    122     let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    123     (rtlabs_fun, regs @ [rs]) in
     99    let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     100    (rtlabs_fun, regs @ [r]) in
    124101  List.fold_left f (rtlabs_fun, []) args
    125102
     
    178155(* Translating conditions
    179156
    180    The Cminor definition [def] is used for typing purposes (differencing from
    181    integers and pointers). [rtlabs_fun] is the function being
    182    constructed. [lenv] is the environment associating a pseudo-register to the
    183    variables of the program being translated. *)
     157   [ptrs] is used for typing purposes (differencing from integers and
     158   pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
     159   environment associating a pseudo-register to the variables of the program
     160   being translated. *)
    184161
    185162let rec translate_branch
    186     (def        : Cminor.internal_function)
     163    (ptrs       : AST.ident list)
    187164    (rtlabs_fun : RTLabs.internal_function)
    188165    (lenv       : local_env)
     
    194171
    195172    | Cminor.Id x ->
    196         let stmt =
    197           RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
    198         generate rtlabs_fun stmt
     173      let stmt =
     174        RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
     175      generate rtlabs_fun stmt
    199176
    200177    | Cminor.Cst cst ->
    201         generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))
     178      generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))
    202179
    203180    | Cminor.Op1 (op1, e) ->
    204         let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    205         let stmt = RTLabs.St_cond1 (op1, rs, lbl_true, lbl_false) in
    206         let rtlabs_fun = generate rtlabs_fun stmt in
    207         translate_expr def rtlabs_fun lenv rs e
     181      let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     182      let stmt = RTLabs.St_cond1 (op1, r, lbl_true, lbl_false) in
     183      let rtlabs_fun = generate rtlabs_fun stmt in
     184      translate_expr ptrs rtlabs_fun lenv r e
    208185
    209186    | Cminor.Op2 (op2, e1, e2) ->
    210         let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
    211         let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
    212         let stmt = RTLabs.St_cond2 (op2, rs1, rs2, lbl_true, lbl_false) in
    213         let rtlabs_fun = generate rtlabs_fun stmt in
    214         translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]
     187      let (rtlabs_fun, r1) = choose_destination ptrs rtlabs_fun lenv e1 in
     188      let (rtlabs_fun, r2) = choose_destination ptrs rtlabs_fun lenv e2 in
     189      let stmt = RTLabs.St_cond2 (op2, r1, r2, lbl_true, lbl_false) in
     190      let rtlabs_fun = generate rtlabs_fun stmt in
     191      translate_exprs ptrs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
    215192
    216193    | _ ->
    217         let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    218         let stmt = RTLabs.St_cond1 (AST.Op_id, rs, lbl_true, lbl_false) in
    219         let rtlabs_fun = generate rtlabs_fun stmt in
    220         translate_expr def rtlabs_fun lenv rs e
     194      let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     195      let stmt = RTLabs.St_cond1 (AST.Op_id, r, lbl_true, lbl_false) in
     196      let rtlabs_fun = generate rtlabs_fun stmt in
     197      translate_expr ptrs rtlabs_fun lenv r e
    221198
    222199(* Translating expressions
    223200
    224    The Cminor definition [def] is used for typing purposes (differencing from
    225    integers and pointers). [rtlabs_fun] is the function being
    226    constructed. [lenv] is the environment associating a pseudo-register to the
    227    variables of the program being translated. [destrs] are the destination
    228    registers. There may be more than one in the case of pointers, and when the
    229    size of addresses is bigger than a machine word. *)
     201   [ptrs] is used for typing purposes (differencing from integers and
     202   pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
     203   environment associating a pseudo-register to the variables of the program
     204   being translated. [destr] is the destination register. *)
    230205
    231206and translate_expr
    232     (def        : Cminor.internal_function)
    233     (rtlabs_fun : RTLabs.internal_function)
    234     (lenv       : local_env)
    235     (destrs     : Register.t list)
     207    (ptrs       : AST.ident list)
     208    (rtlabs_fun : RTLabs.internal_function)
     209    (lenv       : local_env)
     210    (destr      : Register.t)
    236211    (e          : Cminor.expression)
    237212    : RTLabs.internal_function =
     
    239214
    240215    | Cminor.Id x ->
    241       let xrs = find_local lenv x in
    242       let rec eq_reg_list rl1 rl2 = match rl1, rl2 with
    243         | [], [] -> true
    244         | r1 :: rl1, r2 :: rl2 ->
    245           (Register.equal r1 r2) && (eq_reg_list rl1 rl2)
    246         | _ -> false in
    247       (* If the destinations and sources are the same, just do nothing. *)
    248       if eq_reg_list destrs xrs then rtlabs_fun
     216      let xr = find_local lenv x in
     217      (* If the destination and source are the same, just do nothing. *)
     218      if Register.equal destr xr then rtlabs_fun
    249219      else
    250220        let old_entry = rtlabs_fun.RTLabs.f_entry in
    251         let stmt = RTLabs.St_op1 (AST.Op_id, destrs, xrs, old_entry) in
     221        let stmt = RTLabs.St_op1 (AST.Op_id, destr, xr, old_entry) in
    252222        generate rtlabs_fun stmt
    253223
    254224    | Cminor.Cst cst ->
    255225      let old_entry = rtlabs_fun.RTLabs.f_entry in
    256       let stmt = RTLabs.St_cst (destrs, cst, old_entry) in
     226      let stmt = RTLabs.St_cst (destr, cst, old_entry) in
    257227      generate rtlabs_fun stmt
    258228
    259229    | Cminor.Op1 (op1, e) ->
    260       let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    261       let old_entry = rtlabs_fun.RTLabs.f_entry in
    262       let stmt = RTLabs.St_op1 (op1, destrs, rs, old_entry) in
    263       let rtlabs_fun = generate rtlabs_fun stmt in
    264       translate_expr def rtlabs_fun lenv rs e
     230      let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     231      let old_entry = rtlabs_fun.RTLabs.f_entry in
     232      let stmt = RTLabs.St_op1 (op1, destr, r, old_entry) in
     233      let rtlabs_fun = generate rtlabs_fun stmt in
     234      translate_expr ptrs rtlabs_fun lenv r e
    265235
    266236    | Cminor.Op2 (op2, e1, e2) ->
    267       let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
    268       let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
    269       let old_entry = rtlabs_fun.RTLabs.f_entry in
    270       let stmt = RTLabs.St_op2 (op2, destrs, rs1, rs2, old_entry) in
    271       let rtlabs_fun = generate rtlabs_fun stmt in
    272       translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]
     237      let (rtlabs_fun, r1) = choose_destination ptrs rtlabs_fun lenv e1 in
     238      let (rtlabs_fun, r2) = choose_destination ptrs rtlabs_fun lenv e2 in
     239      let old_entry = rtlabs_fun.RTLabs.f_entry in
     240      let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
     241      let rtlabs_fun = generate rtlabs_fun stmt in
     242      translate_exprs ptrs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
    273243
    274244    | Cminor.Mem (chunk, e) ->
    275245      let (mode, args) = addressing e in
    276       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
    277       let old_entry = rtlabs_fun.RTLabs.f_entry in
    278       let stmt = RTLabs.St_load (chunk, mode, regs, destrs, old_entry) in
    279       let rtlabs_fun = generate rtlabs_fun stmt in
    280       translate_exprs def rtlabs_fun lenv regs args
     246      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     247      let old_entry = rtlabs_fun.RTLabs.f_entry in
     248      let stmt = RTLabs.St_load (chunk, mode, regs, destr, old_entry) in
     249      let rtlabs_fun = generate rtlabs_fun stmt in
     250      translate_exprs ptrs rtlabs_fun lenv regs args
    281251
    282252    | Cminor.Cond (e1, e2, e3) ->
    283253      let old_entry = rtlabs_fun.RTLabs.f_entry in
    284       let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
    285       let (rtlabs_fun, rs3) = choose_destination def rtlabs_fun lenv e3 in
    286       let rtlabs_fun = translate_expr def rtlabs_fun lenv rs3 e3 in
     254      let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e3 in
    287255      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    288256      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    289       let rtlabs_fun = translate_expr def rtlabs_fun lenv rs2 e2 in
     257      let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e2 in
    290258      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    291       translate_branch def rtlabs_fun lenv e1 lbl_true lbl_false
     259      translate_branch ptrs rtlabs_fun lenv e1 lbl_true lbl_false
    292260
    293261    | Cminor.Exp_cost (lbl, e) ->
    294       let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    295       let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e in
     262      let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e in
    296263      let old_entry = rtlabs_fun.RTLabs.f_entry in
    297264      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
    298265
    299266and translate_exprs
    300     (def        : Cminor.internal_function)
    301     (rtlabs_fun : RTLabs.internal_function)
    302     (lenv       : local_env)
    303     (regs       : Register.t list list)
     267    (ptrs       : AST.ident list)
     268    (rtlabs_fun : RTLabs.internal_function)
     269    (lenv       : local_env)
     270    (regs       : Register.t list)
    304271    (args       : Cminor.expression list)
    305272    : RTLabs.internal_function =
    306   let f destrs e rtlabs_fun = translate_expr def rtlabs_fun lenv destrs e in
     273  let f destr e rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e in
    307274  List.fold_right2 f regs args rtlabs_fun
    308275
     
    343310(* Translating statements
    344311
    345    The Cminor definition [def] is used for typing purposes (differencing from
    346    integers and pointers). [rtlabs_fun] is the function being
    347    constructed. [lenv] is the environment associating a pseudo-register to the
    348    variables of the program being translated. [exists] is the list of label to
    349    exit to. The leftmost label in the list is used to exit the closest block. *)
     312   [ptrs] is used for typing purposes (differencing from integers and
     313   pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
     314   environment associating a pseudo-register to each variable of the function
     315   being translated. [exists] is the list of label to exit to. The leftmost
     316   label in the list is used to exit the closest block. *)
    350317
    351318let rec translate_stmt
    352     (def        : Cminor.internal_function)
     319    (ptrs       : AST.ident list)
    353320    (rtlabs_fun : RTLabs.internal_function)
    354321    (lenv       : local_env)
     
    361328
    362329    | Cminor.St_assign (x, e) ->
    363       translate_expr def rtlabs_fun lenv (find_local lenv x) e
     330      translate_expr ptrs rtlabs_fun lenv (find_local lenv x) e
    364331
    365332    | Cminor.St_store (chunk, e1, e2) ->
    366333      let (mode, args) = addressing e1 in
    367       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
    368       let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e2 in
    369       let old_entry = rtlabs_fun.RTLabs.f_entry in
    370       let stmt = RTLabs.St_store (chunk, mode, regs, rs, old_entry) in
    371       let rtlabs_fun = generate rtlabs_fun stmt in
    372       let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e2 in
    373       translate_exprs def rtlabs_fun lenv regs args
     334      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     335      let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e2 in
     336      let old_entry = rtlabs_fun.RTLabs.f_entry in
     337      let stmt = RTLabs.St_store (chunk, mode, regs, r, old_entry) in
     338      let rtlabs_fun = generate rtlabs_fun stmt in
     339      let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv r e2 in
     340      translate_exprs ptrs rtlabs_fun lenv regs args
    374341
    375342    | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
    376       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
    377       let retrs = find_olocal lenv oret in
    378       let old_entry = rtlabs_fun.RTLabs.f_entry in
    379       let stmt = RTLabs.St_call_id (f, regs, retrs, sg, old_entry) in
    380       let rtlabs_fun = generate rtlabs_fun stmt in
    381       translate_exprs def rtlabs_fun lenv regs args
     343      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     344      let (rtlabs_fun, retr) = find_olocal rtlabs_fun lenv oret in
     345      let old_entry = rtlabs_fun.RTLabs.f_entry in
     346      let stmt = RTLabs.St_call_id (f, regs, retr, sg, old_entry) in
     347      let rtlabs_fun = generate rtlabs_fun stmt in
     348      translate_exprs ptrs rtlabs_fun lenv regs args
    382349
    383350    | Cminor.St_call (oret, f, args, sg) ->
    384       let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
    385       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
    386       let retrs = find_olocal lenv oret in
    387       let old_entry = rtlabs_fun.RTLabs.f_entry in
    388       let stmt = RTLabs.St_call_ptr (frs, regs, retrs, sg, old_entry) in
    389       let rtlabs_fun = generate rtlabs_fun stmt in
    390       let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
    391       translate_expr def rtlabs_fun lenv frs f
     351      let (rtlabs_fun, fr) = choose_destination ptrs rtlabs_fun lenv f in
     352      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     353      let (rtlabs_fun, retr) = find_olocal rtlabs_fun lenv oret in
     354      let old_entry = rtlabs_fun.RTLabs.f_entry in
     355      let stmt = RTLabs.St_call_ptr (fr, regs, retr, sg, old_entry) in
     356      let rtlabs_fun = generate rtlabs_fun stmt in
     357      let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in
     358      translate_expr ptrs rtlabs_fun lenv fr f
    392359
    393360    | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
    394       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
     361      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
    395362      let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
    396363      let rtlabs_fun = generate rtlabs_fun stmt in
    397       translate_exprs def rtlabs_fun lenv regs args
     364      translate_exprs ptrs rtlabs_fun lenv regs args
    398365
    399366    | Cminor.St_tailcall (f, args, sg) ->
    400       let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
    401       let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
    402       let stmt = RTLabs.St_tailcall_ptr (frs, regs, sg) in
    403       let rtlabs_fun = generate rtlabs_fun stmt in
    404       let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
    405       translate_expr def rtlabs_fun lenv frs f
     367      let (rtlabs_fun, fr) = choose_destination ptrs rtlabs_fun lenv f in
     368      let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     369      let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in
     370      let rtlabs_fun = generate rtlabs_fun stmt in
     371      let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in
     372      translate_expr ptrs rtlabs_fun lenv fr f
    406373
    407374    | Cminor.St_seq (s1, s2) ->
    408       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
    409       translate_stmt def rtlabs_fun lenv exits s1
     375      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s2 in
     376      translate_stmt ptrs rtlabs_fun lenv exits s1
    410377
    411378    | Cminor.St_ifthenelse (e, s1, s2) ->
    412379      let old_entry = rtlabs_fun.RTLabs.f_entry in
    413       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
     380      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s2 in
    414381      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    415382      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    416       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s1 in
     383      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s1 in
    417384      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    418       translate_branch def rtlabs_fun lenv e lbl_true lbl_false
     385      translate_branch ptrs rtlabs_fun lenv e lbl_true lbl_false
    419386
    420387    | Cminor.St_loop s ->
    421388      let loop_start = fresh_label rtlabs_fun in
    422389      let rtlabs_fun = change_entry rtlabs_fun loop_start in
    423       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
     390      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
    424391      let old_entry = rtlabs_fun.RTLabs.f_entry in
    425392      add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)
     
    427394    | Cminor.St_block s ->
    428395      let old_entry = rtlabs_fun.RTLabs.f_entry in
    429       translate_stmt def rtlabs_fun lenv (old_entry :: exits) s
     396      translate_stmt ptrs rtlabs_fun lenv (old_entry :: exits) s
    430397
    431398    | Cminor.St_exit n ->
     
    436403      (match eopt, rtlabs_fun.RTLabs.f_result with
    437404        | None, _ -> rtlabs_fun
    438         | Some e, retrs -> translate_expr def rtlabs_fun lenv retrs e)
     405        | Some e, retr -> translate_expr ptrs rtlabs_fun lenv retr e)
    439406
    440407    | Cminor.St_switch (e, cases, dfl) ->
    441408      let stmt = transform_switch e cases dfl in
    442       translate_stmt def rtlabs_fun lenv exits stmt
     409      translate_stmt ptrs rtlabs_fun lenv exits stmt
    443410
    444411    | Cminor.St_label (lbl, s) ->
    445       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
     412      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
    446413      let old_entry = rtlabs_fun.RTLabs.f_entry in
    447414      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
    448415
    449416    | Cminor.St_cost (lbl, s) ->
    450       let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
     417      let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
    451418      let old_entry = rtlabs_fun.RTLabs.f_entry in
    452419      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
     
    482449  (* Local environment *)
    483450  let add_local lenv x =
    484     let rs = fresh_local runiverse f_def x in
    485     StringTools.Map.add x rs lenv in
     451    StringTools.Map.add x (Register.fresh runiverse) lenv in
    486452  let lenv = StringTools.Map.empty in
    487453  let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
     
    498464  let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in
    499465
     466 (* Pointer registers *)
     467  let ptrs = extract f_def.Cminor.f_ptrs in
     468
    500469  (* Exit label of the graph *)
    501470  let exit = Label.Gen.fresh luniverse in
    502471
    503   (* [retrs] are the registers that holds the return value of the body, if
    504      any. *)
    505   let retrs = fresh_result runiverse f_def in
    506 
    507   let locals = locals @ [retrs] in
     472  (* [retr] is the register that holds the return value of the body, if any. *)
     473  let retr = Register.fresh runiverse in
     474
     475  let locals = locals @ [retr] in
    508476
    509477  (* The control flow graph: for now, it is only a return instruction at the
    510478     end. *)
    511   let graph = Label.Map.add exit (RTLabs.St_return retrs) Label.Map.empty in
     479  let graph = Label.Map.add exit (RTLabs.St_return retr) Label.Map.empty in
    512480
    513481  let rtlabs_fun =
     
    515483      RTLabs.f_runiverse = runiverse ;
    516484      RTLabs.f_sig       = f_def.Cminor.f_sig ;
    517       RTLabs.f_result    = retrs ;
     485      RTLabs.f_result    = retr ;
    518486      RTLabs.f_params    = params ;
    519487      RTLabs.f_locals    = locals ;
     488      RTLabs.f_ptrs      = ptrs ;
    520489      RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
    521490      RTLabs.f_graph     = graph ;
     
    524493
    525494  (* Complete the graph *)
    526   translate_stmt f_def rtlabs_fun lenv [] f_def.Cminor.f_body
     495  translate_stmt f_def.Cminor.f_ptrs rtlabs_fun lenv [] f_def.Cminor.f_body
    527496
    528497
     
    537506(* Initialization of globals *)
    538507
     508let quantity_of_data data =
     509  let i = match data with
     510    | AST.Data_int8 _ -> 1
     511    | AST.Data_int16 _ -> 2
     512    | AST.Data_int32 _ -> 4
     513    | _ -> assert false (* do not use on these arguments *) in
     514  Memory.QInt i
     515
    539516let assign_data x stmt (data, off) =
    540517  let e = Cminor.Op2 (AST.Op_add,
    541518                      Cminor.Cst (AST.Cst_addrsymbol x),
    542519                      Cminor.Cst (AST.Cst_int off)) in
    543   let chunk () = Memory.mq_of_data data in
    544520  let stmt' = match data with
    545521    | AST.Data_reserve _ -> Cminor.St_skip
    546522    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
    547         Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_int i))
    548     | AST.Data_float32 f | AST.Data_float64 f ->
    549         Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_float f)) in
     523        Cminor.St_store (quantity_of_data data, e, Cminor.Cst (AST.Cst_int i))
     524    | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
    550525  Cminor.St_seq (stmt, stmt')
    551526
Note: See TracChangeset for help on using the changeset viewer.