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/RTL/RTLInterpret.ml

    r619 r740  
    3030      graph    : RTL.graph ;
    3131      pc       : Label.t ;
    32       sp       : Val.t ;
     32      sp       : Val.address ;
    3333      lenv     : local_env ;
    3434      carry    : Val.t }
     
    4040
    4141type state =
    42   | State of stack_frame list * RTL.graph * Label.t * Val.t (* sp *) *
     42  | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
    4343             local_env * Val.t (* carry *) * memory * CostLabel.t list
    4444  | CallState of stack_frame list * RTL.function_def *
     
    4747                   memory * CostLabel.t list
    4848
     49let string_of_local_env lenv =
     50  let f x v s =
     51    s ^
     52      (if Val.eq v Val.undef then ""
     53       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
     54  Register.Map.fold f lenv ""
     55
     56let string_of_args args =
     57  let f s v = s ^ " " ^ (Val.to_string v) in
     58  List.fold_left f "" args
     59
     60let print_state = function
     61  | State (_, _, lbl, sp, lenv, carry, mem, _) ->
     62    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     63      (Val.string_of_address sp)
     64      (Val.to_string carry)
     65      (string_of_local_env lenv)
     66      (Mem.to_string mem)
     67      lbl
     68  | CallState (_, _, args, mem, _) ->
     69    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
     70      (Mem.to_string mem)
     71      (string_of_args args)
     72  | ReturnState (_, vs, mem, _) ->
     73    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
     74      (Mem.to_string mem)
     75      (string_of_args vs)
     76
    4977
    5078let find_function mem f =
    51   let v = Mem.find_global mem f in
    52   Mem.find_fun_def mem v
     79  let addr = Mem.find_global mem f in
     80  Mem.find_fun_def mem addr
    5381
    5482let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
     
    5886
    5987let get_local_addr lenv f1 f2 =
    60   Val.merge (List.map (get_local_value lenv) [f1 ; f2])
    61 
    62 (* An address is represented by two pseudo-registers (because in 8051, addresses
    63    are coded on two bytes). Thus, assignments may involve several
    64    registers. When we want to assign a single value to several registers, we
    65    break the value into as many parts as there are registers, and then we update
    66    each register with a part of the value. *)
    67 
    68 let adds rs v lenv = match rs with
    69   | [] -> lenv
    70   | _ ->
    71     let vs = Val.break v (List.length rs) in
    72     let f lenv r v = Register.Map.add r v lenv in
    73     List.fold_left2 f lenv rs vs
     88  List.map (get_local_value lenv) [f1 ; f2]
     89
     90
     91let adds rs vs lenv =
     92  let f lenv r v = Register.Map.add r v lenv in
     93  List.fold_left2 f lenv rs vs
    7494
    7595
    7696(* Assign a value to some destinations registers. *)
    7797
    78 let assign_state cs c lbl sp lenv carry mem t destrs v =
    79   let lenv = adds destrs v lenv in
    80   State (cs, c, lbl, sp, lenv, carry, mem, t)
     98let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
     99  let lenv = adds destrs vs lenv in
     100  State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
    81101
    82102(* Branch on a value. *)
    83103
    84 let branch_state cs c lbl_true lbl_false sp lenv carry mem t v =
     104let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
    85105  let next_lbl =
    86106    if Val.is_true v then lbl_true
     
    88108      if Val.is_false v then lbl_false
    89109      else error "Undefined conditional value." in
    90   State (cs, c, next_lbl, sp, lenv, carry, mem, t)
     110  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
    91111
    92112
     
    94114
    95115let interpret_statement
    96     (cs    : stack_frame list)
    97     (c    : RTL.graph)
    98     (sp    : Val.t)
     116    (sfrs  : stack_frame list)
     117    (graph : RTL.graph)
     118    (sp    : Val.address)
    99119    (lenv  : local_env)
    100120    (carry : Val.t)
    101121    (mem   : memory)
    102122    (stmt  : RTL.statement)
    103     (t    : CostLabel.t list) :
     123    (trace : CostLabel.t list) :
    104124    state = match stmt with
    105125
    106126      | RTL.St_skip lbl ->
    107         State (cs, c, lbl, sp, lenv, carry, mem, t)
     127        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
    108128
    109129      | RTL.St_cost (cost_lbl, lbl) ->
    110         State (cs, c, lbl, sp, lenv, carry, mem, cost_lbl :: t)
     130        State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
    111131
    112132      | RTL.St_addr (r1, r2, x, lbl) ->
    113         assign_state cs c lbl sp lenv carry mem t [r1 ; r2]
     133        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
    114134          (Mem.find_global mem x)
    115135
    116136      | RTL.St_stackaddr (r1, r2, lbl) ->
    117         assign_state cs c lbl sp lenv carry mem t [r1 ; r2] sp
     137        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
    118138
    119139      | RTL.St_int (r, i, lbl) ->
    120         assign_state cs c lbl sp lenv carry mem t [r] (Val.of_int i)
     140        assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
    121141
    122142      | RTL.St_move (destr, srcr, lbl) ->
    123         assign_state cs c lbl sp lenv carry mem t [destr]
    124           (get_local_value lenv srcr)
     143        assign_state sfrs graph lbl sp lenv carry mem trace [destr]
     144          [get_local_value lenv srcr]
    125145
    126146      | RTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
     
    129149            (get_local_value lenv srcr1)
    130150            (get_local_value lenv srcr2) in
    131         assign_state cs c lbl sp lenv carry mem t [destr] v
     151        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
    132152
    133153      | RTL.St_op1 (op1, destr, srcr, lbl) ->
    134154        let v = Eval.op1 op1 (get_local_value lenv srcr) in
    135         assign_state cs c lbl sp lenv carry mem t [destr] v
     155        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
    136156
    137157      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
     
    140160            (get_local_value lenv srcr1)
    141161            (get_local_value lenv srcr2) in
    142         assign_state cs c lbl sp lenv carry mem t [destr] v
     162        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
    143163
    144164      | RTL.St_clear_carry lbl ->
    145         State (cs, c, lbl, sp, lenv, Val.zero, mem, t)
     165        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
    146166
    147167      | RTL.St_load (destr, addr1, addr2, lbl) ->
    148         let dph = get_local_value lenv addr1 in
    149         let dpl = get_local_value lenv addr2 in
    150         let addr = Val.merge [dph ; dpl] in
    151         let v = Mem.load2 mem chunk addr in
    152         assign_state cs c lbl sp lenv carry mem t [destr] v
     168        let addr = get_local_addr lenv addr1 addr2 in
     169        let v = Mem.load mem chunk addr in
     170        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
    153171
    154172      | RTL.St_store (addr1, addr2, srcr, lbl) ->
    155         let dph = get_local_value lenv addr1 in
    156         let dpl = get_local_value lenv addr2 in
    157         let addr = Val.merge [dph ; dpl] in
    158         let mem = Mem.store2 mem chunk addr (get_local_value lenv srcr) in
    159         State (cs, c, lbl, sp, lenv, carry, mem, t)
     173        let addr = get_local_addr lenv addr1 addr2 in
     174        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
     175        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
    160176
    161177      | RTL.St_call_id (f, args, ret_regs, lbl) ->
     
    163179        let args = get_arg_values lenv args in
    164180        let sf =
    165           { ret_regs = ret_regs ; graph = c ; pc = lbl ;
     181          { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
    166182            sp = sp ; lenv = lenv ; carry = carry }
    167183        in
    168         CallState (sf :: cs, f_def, args, mem, t)
     184        CallState (sf :: sfrs, f_def, args, mem, trace)
    169185
    170186      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
     
    172188        let f_def = Mem.find_fun_def mem addr in
    173189        let args = get_arg_values lenv args in
    174         let sf = { ret_regs = ret_regs ; graph = c ; pc = lbl ;
     190        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
    175191                   sp = sp ; lenv = lenv ; carry = carry } in
    176         CallState (sf :: cs, f_def, args, mem, t)
     192        CallState (sf :: sfrs, f_def, args, mem, trace)
    177193
    178194      | RTL.St_tailcall_id (f, args) ->
     
    180196        let args = get_arg_values lenv args in
    181197        let mem = Mem.free mem sp in
    182         CallState (cs, f_def, args, mem, t)
     198        CallState (sfrs, f_def, args, mem, trace)
    183199
    184200      | RTL.St_tailcall_ptr (f1, f2, args) ->
     
    187203        let args = get_arg_values lenv args in
    188204        let mem = Mem.free mem sp in
    189         CallState (cs, f_def, args, mem, t)
     205        CallState (sfrs, f_def, args, mem, trace)
    190206
    191207      | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
    192208        let v = get_local_value lenv srcr in
    193         branch_state cs c lbl_true lbl_false sp lenv carry mem t v
     209        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
    194210
    195211      | RTL.St_return rl ->
    196212        let vl = List.map (get_local_value lenv) rl in
    197213        let mem = Mem.free mem sp in
    198         ReturnState (cs, vl, mem, t)
    199 
    200 
    201 let get_int () =
    202   try Val.of_int (int_of_string (read_line ()))
    203   with Failure "int_of_string" -> error "Failed to scan an integer."
    204 let get_float () =
    205   try Val.of_float (float_of_string (read_line ()))
    206   with Failure "float_of_string" -> error "Failed to scan a float."
    207 
    208 let interpret_external
    209     (mem  : memory)
    210     (def  : AST.external_function)
    211     (args : Val.t list) :
    212     memory * Val.t list =
    213   match def.AST.ef_tag, args with
    214     | s, _ when s = Primitive.scan_int ->
    215       (mem, [get_int ()])
    216     | "scan_float", _ ->
    217       (mem, [get_float ()])
    218     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    219       Printf.printf "%d" (Val.to_int v) ;
    220       (mem, [Val.zero])
    221     | "print_float", v :: _ when Val.is_float v ->
    222       Printf.printf "%f" (Val.to_float v) ;
    223       (mem, [Val.zero])
    224     | "print_ptr", v :: _ when Val.is_pointer v ->
    225       let (b, off) = Val.to_pointer v in
    226       Printf.printf "block: %s, offset: %s"
    227         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    228       (mem, [Val.zero])
    229     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    230       Printf.printf "%d\n" (Val.to_int v) ;
    231       (mem, [Val.zero])
    232     | "print_floatln", v :: _ when Val.is_float v ->
    233       Printf.printf "%f" (Val.to_float v) ;
    234       (mem, [Val.zero])
    235     | "print_ptrln", v :: _ when Val.is_pointer v ->
    236       let (b, off) = Val.to_pointer v in
    237       Printf.printf "block: %s, offset: %s\n"
    238         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    239       (mem, [Val.zero])
    240     | s, v :: _ when s = Primitive.alloc ->
    241       let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
    242       let vs = Val.break ptr 2 in
    243       (mem, vs)
    244     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    245       (mem, [Val.modulo v1 v2])
    246 
    247     (* The other cases are either a type error (only integers and pointers
    248        may not be differenciated during type checking) or an unknown
    249        function. *)
    250     | "print_int", _ | "print_intln", _ ->
    251       error "Illegal cast from pointer to integer."
    252     | "print_ptr", _ | "print_ptrln", _ ->
    253       error "Illegal cast from integer to pointer."
    254     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
     214        ReturnState (sfrs, vl, mem, trace)
     215
     216
     217module InterpretExternal = Primitive.Interpret (Mem)
     218
     219let interpret_external mem f args = match InterpretExternal.t mem f args with
     220  | (mem', InterpretExternal.V v) -> (mem', [v])
     221  | (mem', InterpretExternal.A addr) -> (mem', addr)
    255222
    256223let init_locals
     
    265232
    266233let state_after_call
    267     (cs    : stack_frame list)
     234    (sfrs  : stack_frame list)
    268235    (f_def : RTL.function_def)
    269236    (args  : Val.t list)
    270237    (mem   : memory)
    271     (t    : CostLabel.t list) :
     238    (trace : CostLabel.t list) :
    272239    state =
    273240  match f_def with
    274241    | RTL.F_int def ->
    275242      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    276       State (cs, def.RTL.f_graph, def.RTL.f_entry, sp,
     243      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    277244             init_locals def.RTL.f_locals def.RTL.f_params args,
    278              Val.undef, mem', t)
     245             Val.undef, mem', trace)
    279246    | RTL.F_ext def ->
    280       let (mem', vs) = interpret_external mem def args in
    281       ReturnState (cs, vs, mem', t)
     247      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
     248      ReturnState (sfrs, vs, mem', trace)
    282249
    283250let state_after_return
    284251    (sf       : stack_frame)
    285     (cs       : stack_frame list)
     252    (sfrs     : stack_frame list)
    286253    (ret_vals : Val.t list)
    287254    (mem      : memory)
    288     (t        : CostLabel.t list) :
     255    (trace    : CostLabel.t list) :
    289256    state =
    290257  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    291258  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
    292   State (cs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, t)
     259  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
    293260
    294261
    295262let small_step (st : state) : state = match st with
    296   | State (cs, graph, pc, sp, lenv, carry, mem, t) ->
     263  | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
    297264    let stmt = Label.Map.find pc graph in
    298     interpret_statement cs graph sp lenv carry mem stmt t
    299   | CallState (cs, f_def, args, mem, t) ->
    300     state_after_call cs f_def args mem t
    301   | ReturnState ([], ret_vals, mem, t) ->
     265    interpret_statement sfrs graph sp lenv carry mem stmt trace
     266  | CallState (sfrs, f_def, args, mem, trace) ->
     267    state_after_call sfrs f_def args mem trace
     268  | ReturnState ([], ret_vals, mem, trace) ->
    302269    assert false (* End of execution; handled in iter_small_step. *)
    303   | ReturnState (sf :: cs, ret_vals, mem, t) ->
    304     state_after_return sf cs ret_vals mem t
    305 
    306 
    307 let print_args = MiscPottier.string_of_list ", " Val.to_string
    308 let print_ret_vals = MiscPottier.string_of_list ", " Val.to_string
    309 let print_lenv =
    310   Register.Map.iter (fun r v -> Printf.printf "%s = %s\n%!"
    311     (Register.print r) (Val.to_string v))
     270  | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
     271    state_after_return sf sfrs ret_vals mem trace
     272
    312273
    313274let compute_result vs =
    314275  try
    315     let v = MiscPottier.last vs in
     276    let v = List.hd vs in
    316277    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    317278    else IntValue.Int8.zero
    318279  with Not_found -> IntValue.Int8.zero
    319280
    320 let rec iter_small_step print_result st = match small_step st with
    321 (*
    322   (* <DEBUG> *)
    323   | ReturnState ([], vs, mem, t) ->
    324     Mem.print mem ;
    325     Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
    326     List.rev t
    327   | CallState (_, _, args, mem, _) as st' ->
    328     Printf.printf "Call state: %s\n%!" (print_args args) ;
    329     Mem.print mem ;
    330     iter_small_step st'
    331   | ReturnState (_, ret_vals, mem, _) as st' ->
    332     Printf.printf "Return state: %s\n%!" (print_ret_vals ret_vals) ;
    333     Mem.print mem ;
    334     iter_small_step st'
    335   | State (_, _, pc, sp, lenv, carry, mem, _) as st' ->
    336     Printf.printf "State: PC = %s ; SP = %s\n%!" pc (Val.to_string sp) ;
    337     Mem.print mem ;
    338     print_lenv lenv ;
    339     Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ;
    340     iter_small_step st'
    341   (* </DEBUG> *)
    342 *)
    343   | ReturnState ([], vs, mem, t) ->
    344     let (res, cost_labels) as trace = (compute_result vs, List.rev t) in
    345     if print_result then
    346       Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ;
    347     trace
    348   | st' -> iter_small_step print_result st'
     281let rec iter_small_step debug st =
     282  if debug then print_state st ;
     283  match small_step st with
     284    | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace)
     285    | st' -> iter_small_step debug st'
    349286
    350287
     
    357294
    358295
    359 (* The memory is initialized by load the code into it, and by reserving space
     296(* The memory is initialized by loading the code into it, and by reserving space
    360297   for the global variables. *)
    361298
     
    366303(* Interpret the program only if it has a main. *)
    367304
    368 let interpret print_result p = match p.RTL.main with
    369   | None -> (IntValue.Int8.zero, [])
    370   | Some main ->
    371     let mem = init_mem p in
    372     let main_def = find_function mem main in
    373     let st = CallState ([], main_def, [], mem, []) in
    374     iter_small_step print_result st
     305let interpret debug p =
     306  if debug then Printf.printf "*** RTL ***\n\n%!" ;
     307  match p.RTL.main with
     308    | None -> (IntValue.Int8.zero, [])
     309    | Some main ->
     310      let mem = init_mem p in
     311      let main_def = find_function mem main in
     312      let st = CallState ([], main_def, [], mem, []) in
     313      iter_small_step debug st
Note: See TracChangeset for help on using the changeset viewer.