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/LTL/LTLInterpret.ml

    r619 r740  
    1010module Val = Mem.Value
    1111let chunk = Driver.LTLMemory.int_size
    12 (*
    13 let load mem = Mem.load2 st.mem chunk st.isp
    14 *)
    1512module Eval = I8051.Eval (Val)
    16 
    17 (* External RAM size *)
    18 let ext_ram_size = 1000
    19 (* Internal RAM size *)
    20 let int_ram_size = 100
    21 
    22 
    23 let change_offset v off =
    24   if Val.is_pointer v then
    25     let (b, _) = Val.to_pointer v in
    26     Val.of_pointer (b, off)
    27   else error ((Val.to_string v) ^ " is not a pointer.")
    2813
    2914
     
    4025
    4126type state =
    42     { pc     : Val.t ;
    43       isp    : Val.t ;
     27    { pc     : Val.address ;
     28      isp    : Val.address ;
     29      exit   : Val.address ;
    4430      carry  : Val.t ;
    4531      renv   : hdw_reg_env ;
     
    5238let change_pc st pc = { st with pc = pc }
    5339let change_isp st isp = { st with isp = isp }
     40let change_exit st exit = { st with exit = exit }
    5441let change_carry st carry = { st with carry = carry }
    5542let change_renv st renv = { st with renv = renv }
    5643let change_mem st mem = { st with mem = mem }
    5744let change_trace st trace = { st with trace = trace }
     45let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    5846
    5947let empty_state =
    60   { pc     = Val.undef ;
    61     isp    = Val.undef ;
     48  { pc     = Val.null ;
     49    isp    = Val.null ;
     50    exit   = Val.null ;
    6251    carry  = Val.undef ;
    6352    renv   = I8051.RegisterMap.empty ;
     
    9281let fetch_stmt lbls_offs st =
    9382  let msg =
    94     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
    95   let error () = error msg in
    96   if Val.is_pointer st.pc then
    97     let (_, off) = Val.to_pointer st.pc in
     83    Printf.sprintf "%s does not point to a statement."
     84      (Val.string_of_address st.pc) in
     85  if Val.is_mem_address st.pc then
     86    let off = Val.offset_of_address st.pc in
    9887    let def = fun_def_of_ptr st.mem st.pc in
    9988    let lbl = Labels_Offsets.find2 off lbls_offs in
    10089    Label.Map.find lbl def.LTL.f_graph
    101   else error ()
     90  else error msg
    10291
    10392let entry_pc lbls_offs ptr def =
    104   change_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
     93  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
    10594
    10695let init_fun_call lbls_offs st ptr def =
     
    11099let next_pc lbls_offs st lbl =
    111100  let off = Labels_Offsets.find1 lbl lbls_offs in
    112   change_pc st (change_offset st.pc off)
     101  change_pc st (Val.change_address_offset st.pc off)
    113102
    114103let framesize st =
    115   if Val.is_pointer st.pc then
     104  if Val.is_mem_address st.pc then
    116105    let def = fun_def_of_ptr st.mem st.pc in
    117106    def.LTL.f_stacksize
     
    127116
    128117let push st v =
    129   let mem = Mem.store2 st.mem chunk st.isp v in
    130   let isp = Val.succ st.isp in
     118  let mem = Mem.store st.mem chunk st.isp v in
     119  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
    131120  change_mem (change_isp st isp) mem
    132121
    133122let pop st =
    134   let isp = Val.pred st.isp in
     123  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
    135124  let st = change_isp st isp in
    136   let v = Mem.load2 st.mem chunk st.isp in
     125  let v = Mem.load st.mem chunk st.isp in
    137126  (st, v)
    138127
    139128let save_ra lbls_offs st lbl =
    140   let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
    141   let vs = Val.break ra 2 in
    142   let st = push st (List.nth vs 1) in
    143   let st = push st (List.nth vs 0) in
     129  let ra =
     130    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
     131  let st = push st (List.nth ra 0) in
     132  let st = push st (List.nth ra 1) in
    144133  st
    145134
     
    148137  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
    149138*)
    150   let (_, off) = Val.to_pointer ptr in
     139  let off = Val.offset_of_address ptr in
    151140  Labels_Offsets.find2 off lbls_offs
    152141
    153142let pointer_of_label lbls_offs ptr lbl =
    154   let (b, _) = Val.to_pointer ptr in
    155   let off = Labels_Offsets.find1 lbl lbls_offs in
    156   Val.of_pointer (b, off)
     143  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
    157144
    158145let return_pc st =
    159146  let (st, pch) = pop st in
    160147  let (st, pcl) = pop st in
    161   Val.merge [pch ; pcl]
    162 
    163 
    164 (*
    165 let get_int () =
    166   try Val.of_int (int_of_string (read_line ()))
    167   with Failure "int_of_string" -> error "Failed to scan an integer."
    168 let get_float () =
    169   try Val.of_float (float_of_string (read_line ()))
    170   with Failure "float_of_string" -> error "Failed to scan a float."
    171 
    172 let interpret_external
    173     (mem  : memory)
    174     (def  : AST.external_function)
    175     (args : Val.t list) :
    176     memory * Val.t list =
    177   match def.AST.ef_tag, args with
    178     | s, _ when s = Primitive.scan_int ->
    179       (mem, [get_int ()])
    180     | "scan_float", _ ->
    181       (mem, [get_float ()])
    182     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    183       Printf.printf "%d" (Val.to_int v) ;
    184       (mem, [Val.zero])
    185     | "print_float", v :: _ when Val.is_float v ->
    186       Printf.printf "%f" (Val.to_float v) ;
    187       (mem, [Val.zero])
    188     | "print_ptr", v :: _ when Val.is_pointer v ->
    189       let (b, off) = Val.to_pointer v in
    190       Printf.printf "block: %s, offset: %s"
    191         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    192       (mem, [Val.zero])
    193     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    194       Printf.printf "%d\n" (Val.to_int v) ;
    195       (mem, [Val.zero])
    196     | "print_floatln", v :: _ when Val.is_float v ->
    197       Printf.printf "%f" (Val.to_float v) ;
    198       (mem, [Val.zero])
    199     | "print_ptrln", v :: _ when Val.is_pointer v ->
    200       let (b, off) = Val.to_pointer v in
    201       Printf.printf "block: %s, offset: %s\n"
    202         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    203       (mem, [Val.zero])
    204     | s, v :: _ when s = Primitive.alloc ->
    205       let (mem, ptr) = Mem.alloc mem v in
    206       let vs = Val.break ptr 2 in
    207       (mem, vs)
    208     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    209       (mem, [Val.modulo v1 v2])
    210 
    211     (* The other cases are either a type error (only integers and pointers
    212        may not be differenciated during type checking) or an unknown
    213        function. *)
    214     | "print_int", _ | "print_intln", _ ->
    215       error "Illegal cast from pointer to integer."
    216     | "print_ptr", _ | "print_ptrln", _ ->
    217       error "Illegal cast from integer to pointer."
    218     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
    219 *)
    220 
     148  (st, [pcl ; pch])
     149
     150let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
     151
     152
     153(* State pretty-printing *)
     154
     155let current_label lbls_offs st =
     156  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
     157
     158let print_renv renv =
     159  let f r v =
     160    if not (Val.eq v Val.undef) then
     161    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
     162  I8051.RegisterMap.iter f renv
     163
     164let print_state lbls_offs st =
     165  Printf.printf "PC: %s (%s)\n%!"
     166    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
     167  Printf.printf "SP: %s\n%!"
     168    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
     169  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
     170  print_renv st.renv ;
     171  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
     172  Mem.print st.mem ;
     173  Printf.printf "\n%!"
     174
     175
     176module InterpretExternal = Primitive.Interpret (Mem)
     177
     178let interpret_external mem f args = match InterpretExternal.t mem f args with
     179  | (mem', InterpretExternal.V v) -> (mem', [v])
     180  | (mem', InterpretExternal.A addr) -> (mem', addr)
     181
     182let fetch_external_args st =
     183  (* TODO: this is bad when parameters are the empty list. *)
     184  [get_reg (List.hd I8051.parameters) st]
     185
     186let set_result st = function
     187  | [] -> assert false (* should be impossible: at least one value returned *)
     188  | [v] -> add_reg I8051.dpl v st
     189  | v1 :: v2 :: _ ->
     190    let st = add_reg I8051.dpl v1 st in
     191    add_reg I8051.dph v2 st
     192
     193let interpret_external_call st f next_pc =
     194  let args = fetch_external_args st in
     195  let (mem, vs) = interpret_external st.mem f args in
     196  let st = change_mem st mem in
     197  let st = set_result st vs in
     198  change_pc st next_pc
    221199
    222200let interpret_call lbls_offs st f ra =
     
    224202  match Mem.find_fun_def st.mem ptr with
    225203    | LTL.F_int def ->
    226 (*
    227       Printf.printf "Pushing return address in IRAM: %s = %s\n%!"
    228         ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;
    229 *)
    230204      let st = save_ra lbls_offs st ra in
    231205      init_fun_call lbls_offs st ptr def
    232     | LTL.F_ext def -> assert false (* TODO *)
     206    | LTL.F_ext def ->
     207      let next_pc =
     208        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
     209      interpret_external_call st def.AST.ef_tag next_pc
    233210
    234211let interpret_return lbls_offs st =
    235   let pc = return_pc st in
    236 (*
    237   Printf.printf "Returning to %s = %s\n%!"
    238     (Val.to_string pc) (label_of_pointer lbls_offs pc) ;
    239 *)
     212  let (st, pc) = return_pc st in
    240213  change_pc st pc
    241214
     
    257230
    258231    | LTL.St_cost (cost_lbl, lbl) ->
    259       let st = change_trace st (cost_lbl :: st.trace) in
     232      let st = add_trace st cost_lbl in
    260233      next_pc st lbl
    261234
     
    275248
    276249    | LTL.St_addr (x, lbl) ->
    277       let v = Mem.find_global st.mem x in
    278       let vs = Val.break v 2 in
    279       let st = add_reg I8051.dph (List.nth vs 0) st in
    280       let st = add_reg I8051.dpl (List.nth vs 1) st in
     250      let vs = Mem.find_global st.mem x in
     251      let st = add_reg I8051.dpl (List.nth vs 0) st in
     252      let st = add_reg I8051.dph (List.nth vs 1) st in
    281253      next_pc st lbl
    282254
     
    316288
    317289    | LTL.St_load lbl ->
    318       let addr =
    319         Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
    320       let v = Mem.load2 st.mem chunk addr in
     290      let addr = dptr st in
     291      let v = Mem.load st.mem chunk addr in
    321292      let st = add_reg I8051.a v st in
    322293      next_pc st lbl
    323294
    324295    | LTL.St_store lbl ->
    325       let addr =
    326         Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
    327       let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
     296      let addr = dptr st in
     297      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
    328298      let st = change_mem st mem in
    329299      next_pc st lbl
     
    345315
    346316
    347 let current_label lbls_offs st =
    348   let (_, off) = Val.to_pointer st.pc in
    349   Labels_Offsets.find2 off lbls_offs
    350 
    351 let print_renv renv =
    352   let f r v =
    353     if not (Val.eq v Val.undef) then
    354     Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
    355   I8051.RegisterMap.iter f renv
    356 
    357 let print_state lbls_offs st =
    358   Printf.printf "PC: %s (%s)\n%!"
    359     (Val.to_string st.pc) (current_label lbls_offs st) ;
    360   Printf.printf "SP: %s\n%!"
    361     (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
    362   Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
    363   print_renv st.renv ;
    364   Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
    365   Mem.print st.mem ;
    366   Printf.printf "\n%!"
    367 
    368 let print_result st =
    369   let string_of_reg r = Val.to_string (get_reg r st) in
    370   Printf.printf "DPH: %s - DPL: %s\n%!"
    371     (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
    372 
    373317let compute_result st =
    374318  let v = get_reg I8051.dpl st in
     
    376320  else IntValue.Int8.zero
    377321
    378 let rec iter_small_step print_result lbls_offs st =
    379 (*
    380     print_state lbls_offs st ;
    381 *)
     322let rec iter_small_step debug lbls_offs st =
     323  if debug then print_state lbls_offs st ;
    382324  match fetch_stmt lbls_offs st with
    383     | LTL.St_return when Val.eq (return_pc st) Val.zero ->
    384       let (res, cost_labels) as trace =
    385         (compute_result st, List.rev st.trace) in
    386       if print_result then
    387         Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
    388       trace
     325    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
     326      (compute_result st, List.rev st.trace)
    389327    | stmt ->
    390328      let st' = interpret_stmt lbls_offs st stmt in
    391       iter_small_step print_result lbls_offs st'
     329      iter_small_step debug lbls_offs st'
    392330
    393331
     
    403341  change_mem st mem
    404342
     343let init_sp st =
     344  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
     345  let sp =
     346    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
     347  let st = change_mem st mem in
     348  (st, sp)
     349
     350let init_isp st =
     351  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
     352  let st = change_mem (change_isp st isp) mem in
     353  let (mem, exit) = Mem.alloc st.mem 1 in
     354  let st = change_exit st exit in
     355  let st = push st (List.nth exit 0) in
     356  let st = push st (List.nth exit 1) in
     357  st 
     358
    405359let init_renv st sp =
    406360  let f r st = add_reg r Val.undef st in
    407361  let st = I8051.RegisterSet.fold f I8051.registers st in
    408   let vs = Val.break sp 2 in
    409   let sph = List.nth vs 0 in
    410   let spl = List.nth vs 1 in
     362  let spl = List.nth sp 0 in
     363  let sph = List.nth sp 1 in
     364  let st = add_reg I8051.spl spl st in
    411365  let st = add_reg I8051.sph sph st in
    412   let st = add_reg I8051.spl spl st in
    413366  st
    414 
    415 let init_sp st =
    416   let (mem, sp) = Mem.alloc st.mem ext_ram_size in
    417   let (b, _) = Val.to_pointer sp in
    418   let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
    419   let st = change_mem st mem in
    420   (st, sp)
    421 
    422 let init_isp st =
    423   let (mem, isp) = Mem.alloc st.mem int_ram_size in
    424   let st = change_mem (change_isp st isp) mem in
    425   let vs = Val.break Val.zero 2 in
    426   let st = push st (List.nth vs 1) in
    427   let st = push st (List.nth vs 0) in
    428   st 
    429367
    430368let init_main_call lbls_offs st main =
     
    451389   - Initialize the carry flag to 0. *)
    452390
    453 let interpret print_result p = match p.LTL.main with
    454   | None -> (IntValue.Int8.zero, [])
    455   | Some main ->
    456     let lbls_offs = labels_offsets p in
    457     let st = empty_state in
    458     let st = init_prog st p in
    459     let (st, sp) = init_sp st in
    460     let st = init_isp st in
    461     let st = init_renv st sp in
    462     let st = init_main_call lbls_offs st main in
    463     let st = change_carry st Val.zero in
    464     iter_small_step print_result lbls_offs st
     391let interpret debug p =
     392  if debug then Printf.printf "*** LTL ***\n\n%!" ;
     393  match p.LTL.main with
     394    | None -> (IntValue.Int8.zero, [])
     395    | Some main ->
     396      let lbls_offs = labels_offsets p in
     397      let st = empty_state in
     398      let st = init_prog st p in
     399      let (st, sp) = init_sp st in
     400      let st = init_isp st in
     401      let st = init_renv st sp in
     402      let st = init_main_call lbls_offs st main in
     403      let st = change_carry st Val.zero in
     404      iter_small_step debug lbls_offs st
Note: See TracChangeset for help on using the changeset viewer.