Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (9 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/ERTL/ERTLInterpret.ml

    r619 r740  
    1212module Eval = I8051.Eval (Val)
    1313
    14 (* External RAM size *)
    15 let ext_ram_size = 1000
    16 (* Internal RAM size *)
    17 let int_ram_size = 100
    18 
    19 
    20 let change_offset v off =
    21   if Val.is_pointer v then
    22     let (b, _) = Val.to_pointer v in
    23     Val.of_pointer (b, off)
    24   else error ((Val.to_string v) ^ " is not a pointer.")
    25 
    2614
    2715(* Memory *)
     
    4937type state =
    5038    { st_frs : stack_frame list ;
    51       pc     : Val.t ;
    52       isp    : Val.t ;
     39      pc     : Val.address ;
     40      isp    : Val.address ;
     41      exit   : Val.address ;
    5342      lenv   : local_env ;
    5443      carry  : Val.t ;
     
    6655let change_pc st pc = { st with pc = pc }
    6756let change_isp st isp = { st with isp = isp }
     57let change_exit st exit = { st with exit = exit }
    6858let change_lenv st lenv = { st with lenv = lenv }
    6959let change_carry st carry = { st with carry = carry }
     
    7161let change_mem st mem = { st with mem = mem }
    7262let change_trace st trace = { st with trace = trace }
     63let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    7364
    7465let empty_state =
    7566  { st_frs = [] ;
    76     pc     = Val.undef ;
    77     isp    = Val.undef ;
     67    pc     = Val.null ;
     68    isp    = Val.null ;
     69    exit   = Val.null ;
    7870    lenv   = Register.Map.empty ;
    7971    carry  = Val.undef ;
     
    8375
    8476
    85 (* Each label of each function is associated a pointer. The base of this pointer
    86    is the base of the function in memory. Inside a function, offsets are
     77(* Each label of each function is associated an address. The base of this
     78   address is the base of the function in memory. Inside a function, offsets are
    8779   bijectively associated to labels. *)
    8880
     
    9587
    9688(* [labels_offsets p] builds a bijection between the labels found in the
    97    functions of [p] and some offsets. *)
     89   functions of [p] and some memory addresses. *)
    9890
    9991let labels_offsets p =
     
    109101let fetch_stmt lbls_offs st =
    110102  let msg =
    111     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
    112   let error () = error msg in
    113   if Val.is_pointer st.pc then
    114     let (_, off) = Val.to_pointer st.pc in
     103    Printf.sprintf "%s does not point to a statement."
     104      (Val.string_of_address st.pc) in
     105  if Val.is_mem_address st.pc then
     106    let off = Val.offset_of_address st.pc in
    115107    let def = fun_def_of_ptr st.mem st.pc in
    116108    let lbl = Labels_Offsets.find2 off lbls_offs in
    117109    Label.Map.find lbl def.ERTL.f_graph
    118   else error ()
     110  else error msg
    119111
    120112let entry_pc lbls_offs ptr def =
    121   change_offset ptr (Labels_Offsets.find1 def.ERTL.f_entry lbls_offs)
     113  let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in
     114  Val.change_address_offset ptr off
    122115
    123116let init_fun_call lbls_offs st ptr def =
     
    129122let next_pc lbls_offs st lbl =
    130123  let off = Labels_Offsets.find1 lbl lbls_offs in
    131   change_pc st (change_offset st.pc off)
     124  change_pc st (Val.change_address_offset st.pc off)
    132125
    133126let framesize st =
    134   if Val.is_pointer st.pc then
     127  if Val.is_mem_address st.pc then
    135128    let def = fun_def_of_ptr st.mem st.pc in
    136129    def.ERTL.f_stacksize
     
    156149
    157150let push st v =
    158   let mem = Mem.store2 st.mem chunk st.isp v in
    159   let isp = Val.succ st.isp in
     151  let mem = Mem.store st.mem chunk st.isp v in
     152  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
    160153  change_mem (change_isp st isp) mem
    161154
    162155let pop st =
    163   let isp = Val.pred st.isp in
     156  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
    164157  let st = change_isp st isp in
    165   let v = Mem.load2 st.mem chunk st.isp in
     158  let v = Mem.load st.mem chunk st.isp in
    166159  (st, v)
    167160
     161let get_ra st =
     162  let (st, pch) = pop st in
     163  let (st, pcl) = pop st in
     164  [pcl ; pch]
     165
    168166let save_ra lbls_offs st lbl =
    169   let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
    170   let vs = Val.break ra 2 in
    171   let st = push st (List.nth vs 1) in
    172   let st = push st (List.nth vs 0) in
     167  let ra =
     168    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
     169  let st = push st (List.nth ra 0) in
     170  let st = push st (List.nth ra 1) in
    173171  st
    174172
    175 let save_frame st =
    176   add_st_frs st st.lenv
     173let save_frame st = add_st_frs st st.lenv
    177174
    178175let label_of_pointer lbls_offs ptr =
     
    180177  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
    181178*)
    182   let (_, off) = Val.to_pointer ptr in
     179  let off = Val.offset_of_address ptr in
    183180  Labels_Offsets.find2 off lbls_offs
    184181
    185182let pointer_of_label lbls_offs ptr lbl =
    186   let (b, _) = Val.to_pointer ptr in
    187   let off = Labels_Offsets.find1 lbl lbls_offs in
    188   Val.of_pointer (b, off)
     183  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
    189184
    190185let get_sp st =
    191   let sph = get_reg (Hdw I8051.sph) st in
    192   let spl = get_reg (Hdw I8051.spl) st in
    193   Val.merge [sph ; spl]
    194 
    195 let set_sp v st =
    196   let vs = Val.break v 2 in
    197   let sph = List.nth vs 0 in
    198   let spl = List.nth vs 1 in
     186  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
     187
     188let set_sp vs st =
     189  let spl = List.nth vs 0 in
     190  let sph = List.nth vs 1 in
     191  let st = add_reg (Hdw I8051.spl) spl st in
    199192  let st = add_reg (Hdw I8051.sph) sph st in
    200   let st = add_reg (Hdw I8051.spl) spl st in
    201193  st
    202194
    203195
    204 (*
    205 let get_int () =
    206   try Val.of_int (int_of_string (read_line ()))
    207   with Failure "int_of_string" -> error "Failed to scan an integer."
    208 let get_float () =
    209   try Val.of_float (float_of_string (read_line ()))
    210   with Failure "float_of_string" -> error "Failed to scan a float."
    211 
    212 let interpret_external
    213     (mem  : memory)
    214     (def  : AST.external_function)
    215     (args : Val.t list) :
    216     memory * Val.t list =
    217   match def.AST.ef_tag, args with
    218     | s, _ when s = Primitive.scan_int ->
    219       (mem, [get_int ()])
    220     | "scan_float", _ ->
    221       (mem, [get_float ()])
    222     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    223       Printf.printf "%d" (Val.to_int v) ;
    224       (mem, [Val.zero])
    225     | "print_float", v :: _ when Val.is_float v ->
    226       Printf.printf "%f" (Val.to_float v) ;
    227       (mem, [Val.zero])
    228     | "print_ptr", v :: _ when Val.is_pointer v ->
    229       let (b, off) = Val.to_pointer v in
    230       Printf.printf "block: %s, offset: %s"
    231         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    232       (mem, [Val.zero])
    233     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    234       Printf.printf "%d\n" (Val.to_int v) ;
    235       (mem, [Val.zero])
    236     | "print_floatln", v :: _ when Val.is_float v ->
    237       Printf.printf "%f" (Val.to_float v) ;
    238       (mem, [Val.zero])
    239     | "print_ptrln", v :: _ when Val.is_pointer v ->
    240       let (b, off) = Val.to_pointer v in
    241       Printf.printf "block: %s, offset: %s\n"
    242         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    243       (mem, [Val.zero])
    244     | s, v :: _ when s = Primitive.alloc ->
    245       let (mem, ptr) = Mem.alloc mem v in
    246       let vs = Val.break ptr 2 in
    247       (mem, vs)
    248     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    249       (mem, [Val.modulo v1 v2])
    250 
    251     (* The other cases are either a type error (only integers and pointers
    252        may not be differenciated during type checking) or an unknown
    253        function. *)
    254     | "print_int", _ | "print_intln", _ ->
    255       error "Illegal cast from pointer to integer."
    256     | "print_ptr", _ | "print_ptrln", _ ->
    257       error "Illegal cast from integer to pointer."
    258     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
    259 *)
    260 
     196module InterpretExternal = Primitive.Interpret (Mem)
     197
     198let interpret_external mem f args = match InterpretExternal.t mem f args with
     199  | (mem', InterpretExternal.V v) -> (mem', [v])
     200  | (mem', InterpretExternal.A addr) -> (mem', addr)
     201
     202let fetch_external_args st =
     203  (* TODO: this is bad when parameters are the empty list. *)
     204  [get_reg (Hdw (List.hd I8051.parameters)) st]
     205
     206let set_result st = function
     207  | [] -> assert false (* should be impossible: at least one value returned *)
     208  | [v] -> add_reg (Hdw I8051.dpl) v st
     209  | v1 :: v2 :: _ ->
     210    let st = add_reg (Hdw I8051.dpl) v1 st in
     211    add_reg (Hdw I8051.dph) v2 st
     212
     213let interpret_external_call st f next_pc =
     214  let args = fetch_external_args st in
     215  let (mem, vs) = interpret_external st.mem f args in
     216  let st = change_mem st mem in
     217  let st = set_result st vs in
     218  change_pc st next_pc
    261219
    262220let interpret_call lbls_offs st f ra =
     
    264222  match Mem.find_fun_def st.mem ptr with
    265223    | ERTL.F_int def ->
    266 (*
    267       Printf.printf "Pushing return address in IRAM: %s = %s\n%!"
    268         ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;
    269 *)
    270224      let st = save_ra lbls_offs st ra in
    271225      let st = save_frame st in
    272226      init_fun_call lbls_offs st ptr def
    273     | ERTL.F_ext def -> assert false (* TODO *)
     227    | ERTL.F_ext def ->
     228      let next_pc =
     229        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
     230      interpret_external_call st def.AST.ef_tag next_pc
    274231
    275232let interpret_return lbls_offs st =
     
    277234  let (st, pch) = pop st in
    278235  let (st, pcl) = pop st in
    279   let pc = Val.merge [pch ; pcl] in
    280 (*
    281   Printf.printf "Returning to %s = %s\n%!"
    282     (Val.to_string pc) (label_of_pointer lbls_offs pc) ;
    283 *)
     236  let pc = [pcl ; pch] in
    284237  change_pc st pc
    285238
     
    301254
    302255    | ERTL.St_cost (cost_lbl, lbl) ->
    303       let st = change_trace st (cost_lbl :: st.trace) in
     256      let st = add_trace st cost_lbl in
    304257      next_pc st lbl
    305258
     
    319272      let size = framesize st in
    320273      let sp = get_sp st in
    321       let new_sp = Val.sub sp (Val.of_int size) in
     274      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
    322275      let st = set_sp new_sp st in
    323276      next_pc st lbl
     
    326279      let size = framesize st in
    327280      let sp = get_sp st in
    328       let new_sp = Val.add sp (Val.of_int size) in
     281      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
    329282      let st = set_sp new_sp st in
    330283      next_pc st lbl
     
    346299
    347300    | ERTL.St_addrH (r, x, lbl) ->
    348       let v = Mem.find_global st.mem x in
    349       let vs = Val.break v 2 in
     301      let vs = Mem.find_global st.mem x in
     302      let st = add_reg (Psd r) (List.nth vs 1) st in
     303      next_pc st lbl
     304
     305    | ERTL.St_addrL (r, x, lbl) ->
     306      let vs = Mem.find_global st.mem x in
    350307      let st = add_reg (Psd r) (List.nth vs 0) st in
    351       next_pc st lbl
    352 
    353     | ERTL.St_addrL (r, x, lbl) ->
    354       let v = Mem.find_global st.mem x in
    355       let vs = Val.break v 2 in
    356       let st = add_reg (Psd r) (List.nth vs 1) st in
    357308      next_pc st lbl
    358309
     
    392343
    393344    | ERTL.St_load (destr, addr1, addr2, lbl) ->
    394       let addr =
    395         Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in
    396       let v = Mem.load2 st.mem chunk addr in
     345      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     346      let v = Mem.load st.mem chunk addr in
    397347      let st = add_reg (Psd destr) v st in
    398348      next_pc st lbl
    399349
    400350    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
    401       let addr =
    402         Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in
    403       let mem = Mem.store2 st.mem chunk addr (get_reg (Psd srcr) st) in
     351      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     352      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
    404353      let st = change_mem st mem in
    405354      next_pc st lbl
     
    421370
    422371
    423 let fetch_result renv ret_regs = match ret_regs with
    424   | [] -> Val.undef
    425   | [_] -> I8051.RegisterMap.find I8051.dpl renv
    426   | _ -> Val.merge [I8051.RegisterMap.find I8051.dph renv ;
    427                     I8051.RegisterMap.find I8051.dpl renv]
    428 
    429 
    430372let print_lenv lenv =
    431373  let f r v =
     
    441383
    442384let current_label lbls_offs st =
    443   let (_, off) = Val.to_pointer st.pc in
    444   Labels_Offsets.find2 off lbls_offs
     385  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
    445386
    446387let print_state lbls_offs st =
    447388  Printf.printf "PC: %s (%s)\n%!"
    448     (Val.to_string st.pc) (current_label lbls_offs st) ;
    449   Printf.printf "SP: %s\n%!"
    450     (Val.to_string (Val.merge [get_reg (Hdw I8051.sph) st ;
    451                                get_reg (Hdw I8051.spl) st])) ;
    452   Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
     389    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
     390  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
     391  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
    453392  print_lenv st.lenv ;
    454393  print_renv st.renv ;
     
    458397let compute_result st ret_regs =
    459398  try
    460     let v = get_reg (Psd (MiscPottier.last ret_regs)) st in
     399    let v = get_reg (Psd (List.hd ret_regs)) st in
    461400    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
    462401    else IntValue.Int8.zero
    463402  with Not_found -> IntValue.Int8.zero
    464403
    465 let rec iter_small_step print_result lbls_offs st =
     404let rec iter_small_step debug lbls_offs st =
     405  if debug then print_state lbls_offs st ;
    466406  match fetch_stmt lbls_offs st with
    467     | ERTL.St_return ret_regs when st.st_frs = [] ->
    468       let (res, cost_labels) as trace =
    469         (compute_result st ret_regs, List.rev st.trace) in
    470       if print_result then
    471         Printf.printf "ERTL: %s\n%!" (IntValue.Int8.to_string res) ;
    472       trace
     407    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
     408      (compute_result st ret_regs, List.rev st.trace)
    473409    | stmt ->
    474     (*
    475       print_state lbls_offs st ;
    476     *)
    477410      let st' = interpret_stmt lbls_offs st stmt in
    478       iter_small_step print_result lbls_offs st'
     411      iter_small_step debug lbls_offs st'
    479412
    480413
     
    490423  change_mem st mem
    491424
     425let init_sp st =
     426  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
     427  let sp =
     428    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
     429  let st = change_mem st mem in
     430  (st, sp)
     431
     432let init_isp st =
     433  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
     434  let st = change_mem (change_isp st isp) mem in
     435  let (mem, exit) = Mem.alloc st.mem 1 in
     436  let st = change_exit st exit in
     437  let st = push st (List.nth exit 0) in
     438  let st = push st (List.nth exit 1) in
     439  st 
     440
    492441let init_renv st sp =
    493442  let f r renv = I8051.RegisterMap.add r Val.undef renv in
    494443  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
    495   let vs = Val.break sp 2 in
    496   let sph = List.nth vs 0 in
    497   let spl = List.nth vs 1 in
     444  let spl = List.nth sp 0 in
     445  let sph = List.nth sp 1 in
    498446  let renv = I8051.RegisterMap.add I8051.sph sph renv in
    499447  let renv = I8051.RegisterMap.add I8051.spl spl renv in
    500448  change_renv st renv
    501 
    502 let init_sp st =
    503   let (mem, sp) = Mem.alloc st.mem ext_ram_size in
    504   let (b, _) = Val.to_pointer sp in
    505   let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
    506   let st = change_mem st mem in
    507   (st, sp)
    508 
    509 let init_isp st =
    510   let (mem, isp) = Mem.alloc st.mem int_ram_size in
    511   let st = change_mem (change_isp st isp) mem in
    512   let st = push st Val.zero in
    513   let st = push st Val.zero in
    514   st 
    515449
    516450let init_main_call lbls_offs st main =
     
    537471   - Initialize the carry flag to 0. *)
    538472
    539 let interpret print_result p = match p.ERTL.main with
    540   | None -> (IntValue.Int8.zero (* TODO *), [])
    541   | Some main ->
    542     let lbls_offs = labels_offsets p in
    543     let st = empty_state in
    544     let st = init_prog st p in
    545     let (st, sp) = init_sp st in
    546     let st = init_isp st in
    547     let st = init_renv st sp in
    548     let st = init_main_call lbls_offs st main in
    549     let st = change_carry st Val.zero in
    550     iter_small_step print_result lbls_offs st
     473let interpret debug p =
     474  if debug then Printf.printf "*** ERTL ***\n\n%!" ;
     475  match p.ERTL.main with
     476    | None -> (IntValue.Int8.zero, [])
     477    | Some main ->
     478      let lbls_offs = labels_offsets p in
     479      let st = empty_state in
     480      let st = init_prog st p in
     481      let (st, sp) = init_sp st in
     482      let st = init_isp st in
     483      let st = init_renv st sp in
     484      let st = init_main_call lbls_offs st main in
     485      let st = change_carry st Val.zero in
     486      iter_small_step debug lbls_offs st
Note: See TracChangeset for help on using the changeset viewer.