Changeset 740 for Deliverables/D2.2


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.

Location:
Deliverables/D2.2/8051/src
Files:
50 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

    r631 r740  
    19861986
    19871987let interpret print_result p =
     1988  if print_result then Printf.printf "8051: %!" ;
    19881989  if p.ASM.has_main then
    19891990    let st = load_program p in
     
    19931994    let res = result st in
    19941995    if print_result then
    1995       Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ;
     1996      Printf.printf "%s\n%!" (IntValue.Int8.to_string res) ;
    19961997    (res, List.rev !trace)
    19971998  else (IntValue.Int8.zero, [])
  • Deliverables/D2.2/8051/src/ASM/I8051.ml

    r619 r740  
    183183
    184184let reg_addr r = `DIRECT (BitVectors.vect_of_int r `Eight)
     185
     186(* External RAM size *)
     187let ext_ram_size = MiscPottier.pow 2 16
     188(* Internal RAM size *)
     189let int_ram_size = MiscPottier.pow 2 8
  • Deliverables/D2.2/8051/src/ASM/I8051.mli

    r486 r740  
    6060
    6161val reg_addr : register -> [> ASM.direct]
     62
     63val ext_ram_size : int
     64val int_ram_size : int
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r486 r740  
    121121
    122122  (* Load from external memory. Parameters are the destination register, the
    123      address registers, and the label of the next statement. *)
     123     address registers (low bytes first), and the label of the next
     124     statement. *)
    124125  | St_load of Register.t * Register.t * Register.t * Label.t
    125126
    126   (* Store to external memory. Parameters are the address registers, the source
    127      register, and the label of the next statement. *)
     127  (* Store to external memory. Parameters are the address registers (low bytes
     128     first), the source register, and the label of the next statement. *)
    128129  | St_store of Register.t * Register.t * Register.t * Label.t
    129130
  • 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
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r486 r740  
    259259        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    260260        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     261        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     262        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    261263        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    262         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    263         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    264264        LTL.St_skip l
    265265
     
    270270        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    271271        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     272        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     273        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    272274        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    273         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    274         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    275275        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
    276276        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
  • Deliverables/D2.2/8051/src/LIN/LINInterpret.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 *)
     
    2917type memory = LIN.function_def Mem.memory
    3018
    31 (* Hardware registers environments. They associate a value to the each hardware
     19(* Hardware registers environments. They associate a value to each hardware
    3220   register. *)
    3321
     
    3725
    3826type state =
    39     { pc     : Val.t ;
    40       isp    : Val.t ;
     27    { pc     : Val.address ;
     28      isp    : Val.address ;
     29      exit   : Val.address ;
    4130      carry  : Val.t ;
    4231      renv   : hdw_reg_env ;
     
    4938let change_pc st pc = { st with pc = pc }
    5039let change_isp st isp = { st with isp = isp }
     40let change_exit st exit = { st with exit = exit }
    5141let change_carry st carry = { st with carry = carry }
    5242let change_renv st renv = { st with renv = renv }
    5343let change_mem st mem = { st with mem = mem }
    5444let change_trace st trace = { st with trace = trace }
     45let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    5546
    5647let empty_state =
    57   { pc     = Val.undef ;
    58     isp    = Val.undef ;
     48  { pc     = Val.null ;
     49    isp    = Val.null ;
     50    exit   = Val.null ;
    5951    carry  = Val.undef ;
    6052    renv   = I8051.RegisterMap.empty ;
     
    7163let fetch_stmt st =
    7264  let msg =
    73     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
    74   let error () = error msg in
    75   if Val.is_pointer st.pc then
    76     let (_, off) = Val.to_pointer st.pc in
     65    Printf.sprintf "%s does not point to a statement."
     66      (Val.string_of_address st.pc) in
     67  if Val.is_mem_address st.pc then
     68    let off = Val.offset_of_address st.pc in
    7769    let def = int_fun_of_ptr st.mem st.pc in
    7870    List.nth def (Val.Offset.to_int off)
    79   else error ()
     71  else error msg
    8072
    8173let init_fun_call st ptr =
    82   change_pc st (change_offset ptr Val.Offset.zero)
     74  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    8375
    8476let next_pc st =
    85   change_pc st (Val.succ st.pc)
     77  change_pc st (Val.add_address st.pc Val.Offset.one)
    8678
    8779let add_reg r v st =
     
    9486
    9587let push st v =
    96   let mem = Mem.store2 st.mem chunk st.isp v in
    97   let isp = Val.succ st.isp in
     88  let mem = Mem.store st.mem chunk st.isp v in
     89  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
    9890  change_mem (change_isp st isp) mem
    9991
    10092let pop st =
    101   let isp = Val.pred st.isp in
     93  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
    10294  let st = change_isp st isp in
    103   let v = Mem.load2 st.mem chunk st.isp in
     95  let v = Mem.load st.mem chunk st.isp in
    10496  (st, v)
    10597
    10698let save_ra st =
    107   let ra = Val.succ st.pc in
    108   let vs = Val.break ra 2 in
    109   let st = push st (List.nth vs 1) in
    110   let st = push st (List.nth vs 0) in
     99  let ra = Val.add_address st.pc Val.Offset.one in
     100  let st = push st (List.nth ra 0) in
     101  let st = push st (List.nth ra 1) in
    111102  st
    112103
     
    122113  let code = current_int_fun st in
    123114  let off = find_label lbl code in
    124   change_offset st.pc (Val.Offset.of_int off)
     115  Val.change_address_offset st.pc (Val.Offset.of_int off)
    125116
    126117let goto st lbl =
     
    130121  let (st, pch) = pop st in
    131122  let (st, pcl) = pop st in
    132   Val.merge [pch ; pcl]
    133 
    134 
    135 (*
    136 let get_int () =
    137   try Val.of_int (int_of_string (read_line ()))
    138   with Failure "int_of_string" -> error "Failed to scan an integer."
    139 let get_float () =
    140   try Val.of_float (float_of_string (read_line ()))
    141   with Failure "float_of_string" -> error "Failed to scan a float."
    142 
    143 let interpret_external
    144     (mem  : memory)
    145     (def  : AST.external_function)
    146     (args : Val.t list) :
    147     memory * Val.t list =
    148   match def.AST.ef_tag, args with
    149     | s, _ when s = Primitive.scan_int ->
    150       (mem, [get_int ()])
    151     | "scan_float", _ ->
    152       (mem, [get_float ()])
    153     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    154       Printf.printf "%d" (Val.to_int v) ;
    155       (mem, [Val.zero])
    156     | "print_float", v :: _ when Val.is_float v ->
    157       Printf.printf "%f" (Val.to_float v) ;
    158       (mem, [Val.zero])
    159     | "print_ptr", v :: _ when Val.is_pointer v ->
    160       let (b, off) = Val.to_pointer v in
    161       Printf.printf "block: %s, offset: %s"
    162         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    163       (mem, [Val.zero])
    164     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    165       Printf.printf "%d\n" (Val.to_int v) ;
    166       (mem, [Val.zero])
    167     | "print_floatln", v :: _ when Val.is_float v ->
    168       Printf.printf "%f" (Val.to_float v) ;
    169       (mem, [Val.zero])
    170     | "print_ptrln", v :: _ when Val.is_pointer v ->
    171       let (b, off) = Val.to_pointer v in
    172       Printf.printf "block: %s, offset: %s\n"
    173         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    174       (mem, [Val.zero])
    175     | s, v :: _ when s = Primitive.alloc ->
    176       let (mem, ptr) = Mem.alloc mem v in
    177       let vs = Val.break ptr 2 in
    178       (mem, vs)
    179     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    180       (mem, [Val.modulo v1 v2])
    181 
    182     (* The other cases are either a type error (only integers and pointers
    183        may not be differenciated during type checking) or an unknown
    184        function. *)
    185     | "print_int", _ | "print_intln", _ ->
    186       error "Illegal cast from pointer to integer."
    187     | "print_ptr", _ | "print_ptrln", _ ->
    188       error "Illegal cast from integer to pointer."
    189     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
    190 *)
    191 
     123  (st, [pcl ; pch])
     124
     125let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
     126
     127
     128(* State pretty-printing *)
     129
     130let print_renv renv =
     131  let f r v =
     132    if not (Val.eq v Val.undef) then
     133    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
     134  I8051.RegisterMap.iter f renv
     135
     136let print_state st =
     137  Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
     138  Printf.printf "SP: %s\n%!"
     139    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
     140  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
     141  print_renv st.renv ;
     142  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
     143  Mem.print st.mem ;
     144  Printf.printf "\n%!"
     145
     146
     147module InterpretExternal = Primitive.Interpret (Mem)
     148
     149let interpret_external mem f args = match InterpretExternal.t mem f args with
     150  | (mem', InterpretExternal.V v) -> (mem', [v])
     151  | (mem', InterpretExternal.A addr) -> (mem', addr)
     152
     153let fetch_external_args st =
     154  (* TODO: this is bad when parameters are the empty list. *)
     155  [get_reg (List.hd I8051.parameters) st]
     156
     157let set_result st = function
     158  | [] -> assert false (* should be impossible: at least one value returned *)
     159  | [v] -> add_reg I8051.dpl v st
     160  | v1 :: v2 :: _ ->
     161    let st = add_reg I8051.dpl v1 st in
     162    add_reg I8051.dph v2 st
     163
     164let interpret_external_call st f =
     165  let args = fetch_external_args st in
     166  let (mem, vs) = interpret_external st.mem f args in
     167  let st = change_mem st mem in
     168  set_result st vs
    192169
    193170let interpret_call st f =
     
    197174      let st = save_ra st in
    198175      init_fun_call st ptr
    199     | LIN.F_ext def -> assert false (* TODO *)
     176    | LIN.F_ext def ->
     177      let st = next_pc st in
     178      interpret_external_call st def.AST.ef_tag
    200179
    201180let interpret_return st =
    202   let pc = return_pc st in
     181  let (st, pc) = return_pc st in
    203182  change_pc st pc
    204183
     
    219198
    220199    | LIN.St_cost cost_lbl ->
    221       let st = change_trace st (cost_lbl :: st.trace) in
     200      let st = add_trace st cost_lbl in
    222201      next_pc st
    223202
     
    237216
    238217    | LIN.St_addr x ->
    239       let v = Mem.find_global st.mem x in
    240       let vs = Val.break v 2 in
    241       let st = add_reg I8051.dph (List.nth vs 0) st in
    242       let st = add_reg I8051.dpl (List.nth vs 1) st in
     218      let vs = Mem.find_global st.mem x in
     219      let st = add_reg I8051.dpl (List.nth vs 0) st in
     220      let st = add_reg I8051.dph (List.nth vs 1) st in
    243221      next_pc st
    244222
     
    278256
    279257    | LIN.St_load ->
    280       let addr =
    281         Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
    282       let v = Mem.load2 st.mem chunk addr in
     258      let addr = dptr st in
     259      let v = Mem.load st.mem chunk addr in
    283260      let st = add_reg I8051.a v st in
    284261      next_pc st
    285262
    286263    | LIN.St_store ->
    287       let addr =
    288         Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
    289       let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
     264      let addr = dptr st in
     265      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
    290266      let st = change_mem st mem in
    291267      next_pc st
     
    305281
    306282
    307 let print_renv renv =
    308   let f r v =
    309     if not (Val.eq v Val.undef) then
    310     Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
    311   I8051.RegisterMap.iter f renv
    312 
    313 let print_state st =
    314   Printf.printf "PC: %s\n%!" (Val.to_string st.pc) ;
    315   Printf.printf "SP: %s\n%!"
    316     (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
    317   Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
    318   print_renv st.renv ;
    319   Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
    320   Mem.print st.mem ;
    321   Printf.printf "\n%!"
    322 
    323283let compute_result st =
    324284  let v = get_reg I8051.dpl st in
     
    326286  else IntValue.Int8.zero
    327287
    328 let rec iter_small_step print_result st =
    329 (*
    330   (* <DEBUG> *)
    331   print_state st ;
    332   (* </DEBUG> *)
    333 *)
     288let rec iter_small_step debug st =
     289  if debug then print_state st ;
    334290  match fetch_stmt st with
    335     | LIN.St_return when Val.eq (return_pc st) Val.zero ->
    336       let (res, cost_labels) as trace =
    337         (compute_result st, List.rev st.trace) in
    338       if print_result then
    339         Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ;
    340       trace
     291    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
     292      (compute_result st, List.rev st.trace)
    341293    | stmt ->
    342294      let st' = interpret_stmt st stmt in
    343       iter_small_step print_result st'
     295      iter_small_step debug st'
    344296
    345297
     
    355307  change_mem st mem
    356308
     309let init_sp st =
     310  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
     311  let sp =
     312    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
     313  let st = change_mem st mem in
     314  (st, sp)
     315
     316let init_isp st =
     317  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
     318  let st = change_mem (change_isp st isp) mem in
     319  let (mem, exit) = Mem.alloc st.mem 1 in
     320  let st = change_exit st exit in
     321  let st = push st (List.nth exit 0) in
     322  let st = push st (List.nth exit 1) in
     323  st 
     324
    357325let init_renv st sp =
    358326  let f r st = add_reg r Val.undef st in
    359327  let st = I8051.RegisterSet.fold f I8051.registers st in
    360   let vs = Val.break sp 2 in
    361   let sph = List.nth vs 0 in
    362   let spl = List.nth vs 1 in
     328  let spl = List.nth sp 0 in
     329  let sph = List.nth sp 1 in
     330  let st = add_reg I8051.spl spl st in
    363331  let st = add_reg I8051.sph sph st in
    364   let st = add_reg I8051.spl spl st in
    365332  st
    366 
    367 let init_sp st =
    368   let (mem, sp) = Mem.alloc st.mem ext_ram_size in
    369   let (b, _) = Val.to_pointer sp in
    370   let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
    371   let st = change_mem st mem in
    372   (st, sp)
    373 
    374 let init_isp st =
    375   let (mem, isp) = Mem.alloc st.mem int_ram_size in
    376   let st = change_mem (change_isp st isp) mem in
    377   let vs = Val.break Val.zero 2 in
    378   let st = push st (List.nth vs 1) in
    379   let st = push st (List.nth vs 0) in
    380   st 
    381333
    382334let init_main_call st main =
     
    401353   - Initialize the carry flag to 0. *)
    402354
    403 let interpret print_result p = match p.LIN.main with
    404   | None -> (IntValue.Int8.zero, [])
    405   | Some main ->
    406     let st = empty_state in
    407     let st = init_prog st p in
    408     let (st, sp) = init_sp st in
    409     let st = init_isp st in
    410     let st = init_renv st sp in
    411     let st = init_main_call st main in
    412     let st = change_carry st Val.zero in
    413     iter_small_step print_result st
     355let interpret debug p =
     356  if debug then Printf.printf "*** LIN ***\n\n%!" ;
     357  match p.LIN.main with
     358    | None -> (IntValue.Int8.zero, [])
     359    | Some main ->
     360      let st = empty_state in
     361      let st = init_prog st p in
     362      let (st, sp) = init_sp st in
     363      let st = init_isp st in
     364      let st = init_renv st sp in
     365      let st = init_main_call st main in
     366      let st = change_carry st Val.zero in
     367      iter_small_step debug st
  • 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
  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r486 r740  
    1818
    1919  (* Assign the address of a symbol to registers. Parameters are the destination
    20      registers, the symbol and the label of the next statement. *)
     20     registers (low bytes first), the symbol and the label of the next
     21     statement. *)
    2122  | St_addr of Register.t * Register.t * AST.ident * Label.t
    2223
    2324  (* Assign the stack pointer to registers. Parameters are the destination
    24      registers, and the label of the next statement. *)
     25     registers (low bytes first), and the label of the next statement. *)
    2526  | St_stackaddr of Register.t * Register.t * Label.t
    2627
     
    5152
    5253  (* Load from external memory. Parameters are the destination register, the
    53      address registers, and the label of the next statement. *)
     54     address registers (low bytes first), and the label of the next
     55     statement. *)
    5456  | St_load of Register.t * Register.t * Register.t * Label.t
    5557
    56   (* Store to external memory. Parameters are the address registers, the source
    57      register, and the label of the next statement. *)
     58  (* Store to external memory. Parameters are the address registers (low bytes
     59     first), the source register, and the label of the next statement. *)
    5860  | St_store of Register.t * Register.t * Register.t * Label.t
    5961
     
    6466
    6567  (* Call to a function given its address. Parameters are the registers holding
    66      the address of the function, the arguments of the function, the destination
    67      registers, and the label of the next statement. *)
     68     the address of the function (low bytes first), the arguments of the
     69     function, the destination registers, and the label of the next
     70     statement. *)
    6871  | St_call_ptr of Register.t * Register.t * Register.t list * registers *
    69                    Label.t
     72      Label.t
    7073
    7174  (* Tail call to a function given its name. Parameters are the name of the
     
    7477
    7578  (* Tail call to a function given its address. Parameters are the registers
    76      holding the address of the function, and the arguments of the function. *)
     79     holding the address of the function (low bytes first), and the arguments of
     80     the function. *)
    7781  | St_tailcall_ptr of Register.t * Register.t * Register.t list
    7882
     
    8488  (* Return the value of some registers. Their may be no register in case of
    8589     procedures, one register when returning an integer, or two registers when
    86      returning an address. *)
     90     returning an address (low bytes first). *)
    8791  | St_return of registers
    8892
     
    9498      f_runiverse : Register.universe ;
    9599      f_sig       : AST.signature ;
    96       f_result    : Register.t list ;
     100      f_result    : Register.t list (* low byte first *) ;
    97101      f_params    : Register.t list ;
    98102      f_locals    : Register.Set.t ;
  • 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
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r624 r740  
    110110  let (def, tmpr) = fresh_reg def in
    111111  adds_graph
    112     [ERTL.St_framesize (addr2, start_lbl) ;
     112    [ERTL.St_framesize (addr1, start_lbl) ;
    113113     ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ;
    114      ERTL.St_op2 (I8051.Sub, addr2, addr2, tmpr, start_lbl) ;
     114     ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ;
    115115     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    116      ERTL.St_op2 (I8051.Add, addr2, addr2, tmpr, start_lbl) ;
    117      ERTL.St_int (addr1, 0, start_lbl) ;
     116     ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ;
     117     ERTL.St_int (addr2, 0, start_lbl) ;
    118118     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    119      ERTL.St_op2 (I8051.Addc, addr1, addr1, tmpr, start_lbl) ;
     119     ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ;
    120120     ERTL.St_load (destr, addr1, addr2, start_lbl)]
    121121    start_lbl dest_lbl def
     
    137137  (get_params_hdw hdw_params) @ (get_params_stack stack_params)
    138138
    139 let add_prologue params srah sral sregs def =
     139let add_prologue params sral srah sregs def =
    140140  let start_lbl = def.ERTL.f_entry in
    141141  let tmp_lbl = fresh_label def in
     
    174174      let (def, r_tmp) = fresh_reg def in
    175175      adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ;
    176                   ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl) ;
    177                   ERTL.St_set_hdw (I8051.st0, r, start_lbl)]
     176                  ERTL.St_set_hdw (I8051.st0, r, start_lbl) ;
     177                  ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl)]
    178178        start_lbl dest_lbl def]
    179179  | r1 :: r2 :: _ ->
    180180    [(fun start_lbl ->
    181       adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl) ;
    182                   ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
    183 
    184 let add_epilogue ret_regs srah sral sregs def =
     181      adds_graph [ERTL.St_set_hdw (I8051.st0, r1, start_lbl) ;
     182                  ERTL.St_set_hdw (I8051.st1, r2, start_lbl)] start_lbl)]
     183
     184let add_epilogue ret_regs sral srah sregs def =
    185185  let start_lbl = def.ERTL.f_exit in
    186186  let tmp_lbl = fresh_label def in
     
    204204       (* assign the result to actual return registers *)
    205205       [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @
    206        [adds_graph [ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ;
    207                     ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ;
     206       [adds_graph [ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ;
     207                    ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ;
    208208                    ERTL.St_comment ("End Epilogue", start_lbl)]])
    209209      start_lbl tmp_lbl def in
     
    221221  (* Allocate registers to hold the return address. *)
    222222  let (def, sra) = fresh_regs def 2 in
    223   let srah = List.nth sra 0 in
    224   let sral = List.nth sra 1 in
     223  let sral = List.nth sra 0 in
     224  let srah = List.nth sra 1 in
    225225  (* Allocate registers to save callee-saved registers. *)
    226226  let (def, sregs) = allocate_regs I8051.callee_saved def in
    227227  (* Add a prologue and a epilogue. *)
    228   let def = add_prologue params srah sral sregs def in
    229   let def = add_epilogue ret_regs srah sral sregs def in
     228  let def = add_prologue params sral srah sregs def in
     229  let def = add_epilogue ret_regs sral srah sregs def in
    230230  def
    231231
     
    246246     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    247247     ERTL.St_clear_carry start_lbl ;
     248     ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
     249     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
     250     ERTL.St_int (addr2, 0, start_lbl) ;
    248251     ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ;
    249      ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    250      ERTL.St_int (addr1, 0, start_lbl) ;
    251      ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
    252252     ERTL.St_store (addr1, addr2, srcr, start_lbl)]
    253253    start_lbl dest_lbl def
     
    284284  | r1 :: r2 :: _ ->
    285285    adds_graph
    286       [ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ;
    287        ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
    288        ERTL.St_get_hdw (r1, I8051.st1, start_lbl) ;
    289        ERTL.St_get_hdw (r2, I8051.st0, start_lbl)]
     286      [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
     287       ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ;
     288       ERTL.St_get_hdw (r1, I8051.st0, start_lbl) ;
     289       ERTL.St_get_hdw (r2, I8051.st1, start_lbl)]
    290290      start_lbl
    291291
     
    319319  | RTL.St_addr (r1, r2, x, lbl') ->
    320320    adds_graph
    321       [ERTL.St_addrH (r1, x, lbl) ; ERTL.St_addrL (r2, x, lbl) ;]
     321      [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;]
    322322      lbl lbl' def
    323323
    324324  | RTL.St_stackaddr (r1, r2, lbl') ->
    325325    adds_graph
    326       [ERTL.St_get_hdw (r1, I8051.sph, lbl) ;
    327        ERTL.St_get_hdw (r2, I8051.spl, lbl)]
     326      [ERTL.St_get_hdw (r1, I8051.spl, lbl) ;
     327       ERTL.St_get_hdw (r2, I8051.sph, lbl)]
    328328      lbl lbl' def
    329329
  • Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

    r486 r740  
    99   RTLabs is the last language of the frontend. It is intended to
    1010   ease retargetting. *)
    11 
    12 
    13 (* From the RTLabs point of view, a pseudo-register can represent a physical
    14    location or a pointer. When instruction selection is over, a pseudo-register
    15    represents a physical location. Thus, some operations --- those on pointers
    16    --- may involve several pseudo-registers when a pointer value is more than
    17    one physical location (which is the case of the 8051). *)
    18 
    19 type registers = Register.t list
    2011
    2112
     
    5243  | St_cost of CostLabel.t * Label.t
    5344
    54   (* Assign a constant to registers. Parameters are the destination registers,
     45  (* Assign a constant to registers. Parameters are the destination register,
    5546     the constant and the label of the next statement. *)
    56   | St_cst of registers * AST.cst * Label.t
     47  | St_cst of Register.t * AST.cst * Label.t
    5748
    5849  (* Application of an unary operation. Parameters are the operation, the
    59      destination registers, the argument registers and the label of the next
     50     destination register, the argument register and the label of the next
    6051     statement. *)
    61   | St_op1 of AST.op1 * registers * registers * Label.t
     52  | St_op1 of AST.op1 * Register.t * Register.t * Label.t
    6253
    6354  (* Application of a binary operation. Parameters are the operation, the
    64      destination register, the argument registers and the label of the next
     55     destination register, the two argument registers and the label of the next
    6556     statement. *)
    66   | St_op2 of AST.op2 * registers * registers * registers * Label.t
     57  | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
    6758
    68   (* Memory load. Parameters are the size and type of what to load,
    69      the addressing mode and its arguments, the destination register
    70      and the label of the next statement. *)
    71   | St_load of Memory.memory_q * addressing * registers list *
    72                registers * Label.t
     59  (* Memory load. Parameters are the size in bytes of what to load, the
     60     addressing mode and its arguments, the destination register and the label
     61     of the next statement. *)
     62  | St_load of Memory.quantity * addressing * Register.t list * Register.t *
     63               Label.t
    7364
    74   (* Memory store. Parameters are the size and type of what to store,
    75      the addressing mode and its arguments, the source register
    76      and the label of the next statement. *)
    77   | St_store of Memory.memory_q * addressing * registers list *
    78                 registers * Label.t
     65  (* Memory store. Parameters are the size in bytes of what to store, the
     66     addressing mode and its arguments, the source register and the label of the
     67     next statement. *)
     68  | St_store of Memory.quantity * addressing * Register.t list * Register.t *
     69                Label.t
    7970
    8071  (* Call to a function given its name. Parameters are the name of the
    8172     function, the arguments of the function, the destination
    82      registers, the signature of the function and the label of the next
     73     register, the signature of the function and the label of the next
    8374     statement. *)
    84   | St_call_id of AST.ident * registers list * registers *
     75  | St_call_id of AST.ident * Register.t list * Register.t *
    8576                  AST.signature * Label.t
    8677
    87   (* Call to a function given its address. Parameters are registers
     78  (* Call to a function given its address. Parameters are the register
    8879     holding the address of the function, the arguments of the
    89      function, the destination registers, the signature of the function
     80     function, the destination register, the signature of the function
    9081     and the label of the next statement. This statement with an
    9182     [St_op] before can represent a [St_call_id]. However, we
    9283     differenciate the two to allow translation to a formalism with no
    9384     function pointer. *)
    94   | St_call_ptr of registers * registers list * registers *
     85  | St_call_ptr of Register.t * Register.t list * Register.t *
    9586                   AST.signature * Label.t
    9687
    97   (* Tail call to a function given its name. Parameters are the name
    98      of the function, the arguments of the function, the destination
    99      register, the signature of the function and the label of the next
    100      statement. *)
    101   | St_tailcall_id of AST.ident * registers list * AST.signature
     88  (* Tail call to a function given its name. Parameters are the name of the
     89     function, the arguments of the function, the signature of the function and
     90     the label of the next statement. *)
     91  | St_tailcall_id of AST.ident * Register.t list * AST.signature
    10292
    103   (* Tail call to a function given its address. Parameters are a
    104      register holding the address of the function, the arguments of
    105      the function, the destination register, the signature of the
    106      function and the label of the next statement. Same remark as for
    107      the [St_call_ptr]. *)
    108   | St_tailcall_ptr of registers * registers list * AST.signature
     93  (* Tail call to a function given its address. Parameters are a register
     94     holding the address of the function, the arguments of the function, the
     95     signature of the function and the label of the next statement. Same remark
     96     as for the [St_call_ptr]. *)
     97  | St_tailcall_ptr of Register.t * Register.t list * AST.signature
    10998
    11099  (* Constant branch. Parameters are the constant, the label to go to when the
     
    117106     true (not 0), and the label to go to when the operation on the
    118107     argument evaluates to false (0). *)
    119   | St_cond1 of AST.op1 * registers * Label.t * Label.t
     108  | St_cond1 of AST.op1 * Register.t * Label.t * Label.t
    120109
    121110  (* Binary branch. Parameters are the operation, its arguments, the
     
    123112     true (not 0), and the label to go to when the operation on the
    124113     arguments evaluates to false (0). *)
    125   | St_cond2 of AST.op2 * registers * registers * Label.t * Label.t
     114  | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t
    126115
    127116  (* Jump statement. Parameters are a register and a list of
    128117     labels. The execution will go to the [n]th label of the list of
    129118     labels, where [n] is the natural value held in the register. *)
    130   | St_jumptable of registers * Label.t list
     119  | St_jumptable of Register.t * Label.t list
    131120
    132121  (* Return statement. *)
    133   | St_return of registers
     122  | St_return of Register.t
    134123
    135124
     
    140129      f_runiverse : Register.universe ;
    141130      f_sig       : AST.signature ;
    142       f_result    : registers ;
    143       f_params    : registers list ;
    144       f_locals    : registers list ;
     131      f_result    : Register.t ;
     132      f_params    : Register.t list ;
     133      f_locals    : Register.t list ;
     134      f_ptrs      : Register.t list ;
    145135      f_stacksize : int ;
    146136      f_graph     : graph ;
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r619 r740  
    99module Mem = Driver.RTLabsMemory
    1010module Val = Mem.Value
     11
     12let error_float () = error "float not supported"
    1113
    1214
     
    2527
    2628type stack_frame =
    27     { ret_regs : Register.t list ;
     29    { ret_reg  : Register.t ;
    2830      graph    : RTLabs.graph ;
    29       sp       : Val.t ;
     31      sp       : Val.address ;
    3032      pc       : Label.t ;
    3133      lenv     : local_env }
     
    3739
    3840type state =
    39   | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) *
     41  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
    4042             Label.t * local_env * memory * CostLabel.t list
    4143  | CallState of stack_frame list * RTLabs.function_def *
     
    4446                   memory * CostLabel.t list
    4547
     48let string_of_local_env lenv =
     49  let f x v s =
     50    s ^
     51      (if Val.eq v Val.undef then ""
     52       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
     53  Register.Map.fold f lenv ""
     54
     55let string_of_args args =
     56  let f s v = s ^ " " ^ (Val.to_string v) in
     57  List.fold_left f "" args
     58
     59let print_state = function
     60  | State (_, _, sp, lbl, lenv, mem, _) ->
     61    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     62      (Val.string_of_address sp)
     63      (string_of_local_env lenv)
     64      (Mem.to_string mem)
     65      lbl
     66  | CallState (_, _, args, mem, _) ->
     67    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
     68      (Mem.to_string mem)
     69      (string_of_args args)
     70  | ReturnState (_, v, mem, _) ->
     71    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
     72      (Mem.to_string mem)
     73      (Val.to_string v)
     74
    4675
    4776let find_function mem f =
    48   let v = Mem.find_global mem f in
    49   Mem.find_fun_def mem v
     77  let addr = Mem.find_global mem f in
     78  Mem.find_fun_def mem addr
    5079
    5180let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
     
    5483let get_arg_values lenv args = List.map (get_local_value lenv) args
    5584
    56 let get_local_valuel (lenv : local_env) (rl : Register.t list) : Val.t =
    57   let vl = List.map (get_local_value lenv) rl in
    58   Val.merge vl
    59 let get_arg_valuesl lenv argsl = List.map (get_local_valuel lenv) argsl
    60 
    61 (* An address is represented by two pseudo-registers (because in 8051, addresses
    62    are coded on two bytes). Thus, assignments may involve several
    63    registers. When we want to assign a single value to several registers, we
    64    break the value into as many parts as there are registers, and then we update
    65    each register with a part of the value. *)
    66 
    67 let adds rs v lenv = match rs with
    68   | [] -> lenv
    69   | _ ->
    70     let vs = Val.break v (List.length rs) in
    71     let f lenv r v = Register.Map.add r v lenv in
    72     List.fold_left2 f lenv rs vs
     85let adds rs vs lenv =
     86  let f lenv r v = Register.Map.add r v lenv in
     87  List.fold_left2 f lenv rs vs
     88
     89let value_of_address = List.hd
     90let address_of_value v = [v]
    7391
    7492
    7593let eval_addressing
    7694    (mem  : memory)
    77     (sp   : Val.t)
     95    (sp   : Val.address)
    7896    (mode : RTLabs.addressing)
    7997    (args : Val.t list) :
    80     Val.t = match mode, args with
    81 
    82       | RTLabs.Aindexed off, addr :: _ when Val.is_pointer addr ->
    83         Val.add addr (Val.of_int off)
    84 
    85       | RTLabs.Aindexed2, addr :: shift :: _
    86         when Val.is_pointer addr && Val.is_int shift ->
    87         Val.add addr shift
    88 
    89       | RTLabs.Aindexed2, shift :: addr :: _
    90         when Val.is_pointer addr && Val.is_int shift ->
    91         Val.add addr shift
     98    Val.address = match mode, args with
     99
     100      | RTLabs.Aindexed off, v :: _ ->
     101        address_of_value (Val.add v (Val.of_int off))
     102
     103      | RTLabs.Aindexed2, v1 :: v2 :: _ ->
     104        address_of_value (Val.add v1 v2)
    92105
    93106      | RTLabs.Aglobal (id, off), _ ->
    94         Val.add (Mem.find_global mem id) (Val.of_int off)
     107        Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off)
    95108
    96109      | RTLabs.Abased (id, off), v :: _ ->
    97         let addr = Val.add (Mem.find_global mem id) (Val.of_int off) in
    98         Val.add addr v
     110        let addr =
     111          Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) in
     112        address_of_value (Val.add (value_of_address addr) v)
    99113
    100114      | RTLabs.Ainstack off, _ ->
    101         Val.add sp (Val.of_int off)
     115        Val.add_address sp (Val.Offset.of_int off)
    102116
    103117      | _, _ -> error "Bad addressing mode."
     
    106120let eval_cst mem sp = function
    107121  | AST.Cst_int i -> Val.of_int i
    108   | AST.Cst_float f -> Val.of_float f
    109   | AST.Cst_addrsymbol id -> Mem.find_global mem id
    110   | AST.Cst_stackoffset shift -> Val.add sp (Val.of_int shift)
     122  | AST.Cst_float f -> error_float ()
     123  | AST.Cst_addrsymbol id -> value_of_address (Mem.find_global mem id)
     124  | AST.Cst_stackoffset shift ->
     125    value_of_address (Val.add_address sp (Val.Offset.of_int shift))
    111126
    112127let eval_op1 = function
     
    118133  | AST.Op_notbool -> Val.notbool
    119134  | AST.Op_notint -> Val.notint
    120   | AST.Op_negf -> Val.negf
    121   | AST.Op_absf -> Val.absf
    122   | AST.Op_singleoffloat -> Val.singleoffloat
    123   | AST.Op_intoffloat -> Val.intoffloat
    124   | AST.Op_intuoffloat -> Val.intuoffloat
    125   | AST.Op_floatofint -> Val.floatofint
    126   | AST.Op_floatofintu -> Val.floatofintu
     135  | AST.Op_negf
     136  | AST.Op_absf
     137  | AST.Op_singleoffloat
     138  | AST.Op_intoffloat
     139  | AST.Op_intuoffloat
     140  | AST.Op_floatofint
     141  | AST.Op_floatofintu -> error_float ()
    127142  | AST.Op_id -> (fun (v : Val.t) -> v)
    128   | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO? *)
     143  | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *)
    129144
    130145let rec eval_op2 = function
     
    142157  | AST.Op_shr -> Val.shr
    143158  | AST.Op_shru -> Val.shru
    144   | AST.Op_addf -> Val.addf
    145   | AST.Op_subf -> Val.subf
    146   | AST.Op_mulf -> Val.mulf
    147   | AST.Op_divf -> Val.divf
    148159  | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
    149160  | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
     
    158169  | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
    159170  | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
    160   | AST.Op_cmpf AST.Cmp_eq -> Val.cmp_eq_f
    161   | AST.Op_cmpf AST.Cmp_ne -> Val.cmp_ne_f
    162   | AST.Op_cmpf AST.Cmp_lt -> Val.cmp_lt_f
    163   | AST.Op_cmpf AST.Cmp_le -> Val.cmp_le_f
    164   | AST.Op_cmpf AST.Cmp_gt -> Val.cmp_gt_f
    165   | AST.Op_cmpf AST.Cmp_ge -> Val.cmp_ge_f
    166171  | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp)
     172  | AST.Op_addf
     173  | AST.Op_subf
     174  | AST.Op_mulf
     175  | AST.Op_divf
     176  | AST.Op_cmpf _ -> error_float ()
    167177
    168178(* Assign a value to some destinations registers. *)
    169179
    170 let assign_state cs c sp lbl lenv mem t destrs v =
    171   let lenv = adds destrs v lenv in
    172   State (cs, c, sp, lbl, lenv, mem, t)
     180let assign_state sfrs graph sp lbl lenv mem trace destr v =
     181  let lenv = Register.Map.add destr v lenv in
     182  State (sfrs, graph, sp, lbl, lenv, mem, trace)
    173183
    174184(* Branch on a value. *)
    175185
    176 let branch_state cs c sp lbl_true lbl_false lenv mem t v =
     186let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
    177187  let next_lbl =
    178188    if Val.is_true v then lbl_true
     
    180190      if Val.is_false v then lbl_false
    181191      else error "Undefined conditional value." in
    182   State (cs, c, sp, next_lbl, lenv, mem, t)
     192  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    183193
    184194
     
    186196
    187197let interpret_statement
    188     (cs   : stack_frame list)
    189     (c    : RTLabs.graph)
    190     (sp   : Val.t)
    191     (lenv : local_env)
    192     (mem  : memory)
    193     (stmt : RTLabs.statement)
    194     (t    : CostLabel.t list) :
     198    (sfrs  : stack_frame list)
     199    (graph : RTLabs.graph)
     200    (sp    : Val.address)
     201    (lenv  : local_env)
     202    (mem   : memory)
     203    (stmt  : RTLabs.statement)
     204    (trace : CostLabel.t list) :
    195205    state = match stmt with
    196206
    197       | RTLabs.St_skip lbl -> State (cs, c, sp, lbl, lenv, mem, t)
     207      | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace)
    198208
    199209      | RTLabs.St_cost (cost_lbl, lbl) ->
    200         State (cs, c, sp, lbl, lenv, mem, cost_lbl :: t)
    201 
    202       | RTLabs.St_cst (destrs, cst, lbl) ->
     210        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
     211
     212      | RTLabs.St_cst (destr, cst, lbl) ->
    203213        let v = eval_cst mem sp cst in
    204         assign_state cs c sp lbl lenv mem t destrs v
    205 
    206       | RTLabs.St_op1 (op1, destrs, srcrs, lbl) ->
    207         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
    208         assign_state cs c sp lbl lenv mem t destrs v
    209 
    210       | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl) ->
     214        assign_state sfrs graph sp lbl lenv mem trace destr v
     215
     216      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
     217        let v = eval_op1 op1 (get_local_value lenv srcr) in
     218        assign_state sfrs graph sp lbl lenv mem trace destr v
     219
     220      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    211221        let v =
    212222          eval_op2 op2
    213             (get_local_valuel lenv srcrs1)
    214             (get_local_valuel lenv srcrs2) in
    215         assign_state cs c sp lbl lenv mem t destrs v
    216 
    217       | RTLabs.St_load (chunk, mode, args, destrs, lbl) ->
    218         let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
    219         let v = Mem.load mem chunk addr in
    220         assign_state cs c sp lbl lenv mem t destrs v
    221 
    222       | RTLabs.St_store (chunk, mode, args, srcrs, lbl) ->
    223         let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
    224         let mem = Mem.store mem chunk addr (get_local_valuel lenv srcrs) in
    225         State (cs, c, sp, lbl, lenv, mem, t)
     223            (get_local_value lenv srcr1)
     224            (get_local_value lenv srcr2) in
     225        assign_state sfrs graph sp lbl lenv mem trace destr v
     226
     227      | RTLabs.St_load (q, mode, args, destr, lbl) ->
     228        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
     229        let v = Mem.loadq mem q addr in
     230        assign_state sfrs graph sp lbl lenv mem trace destr v
     231
     232      | RTLabs.St_store (q, mode, args, srcr, lbl) ->
     233        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
     234        let v = get_local_value lenv srcr in
     235        let mem = Mem.storeq mem q addr v in
     236        State (sfrs, graph, sp, lbl, lenv, mem, trace)
    226237
    227238      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
    228239        let f_def = find_function mem f in
    229         let args = get_arg_valuesl lenv args in
     240        let args = get_arg_values lenv args in
    230241        (* Save the stack frame. *)
    231242        let sf =
    232           { ret_regs = destr ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
     243          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    233244        in
    234         CallState (sf :: cs, f_def, args, mem, t)
    235 
    236       | RTLabs.St_call_ptr (rs, args, destrs, sg, lbl) ->
    237         let addr = get_local_valuel lenv rs in
    238         let f_def = Mem.find_fun_def mem addr in
    239         let args = get_arg_valuesl lenv args in
     245        CallState (sf :: sfrs, f_def, args, mem, trace)
     246
     247      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
     248        let addr = get_local_value lenv r in
     249        let f_def = Mem.find_fun_def mem (address_of_value addr) in
     250        let args = get_arg_values lenv args in
    240251        (* Save the stack frame. *)
    241252        let sf =
    242           { ret_regs = destrs ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
     253          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    243254        in
    244         CallState (sf :: cs, f_def, args, mem, t)
     255        CallState (sf :: sfrs, f_def, args, mem, trace)
    245256
    246257      | RTLabs.St_tailcall_id (f, args, sg) ->
    247258        let f_def = find_function mem f in
    248         let args = get_arg_valuesl lenv args in
     259        let args = get_arg_values lenv args in
    249260        (* No need to save the stack frame. But free the stack. *)
    250261        let mem = Mem.free mem sp in
    251         CallState (cs, f_def, args, mem, t)
    252 
    253       | RTLabs.St_tailcall_ptr (rs, args, sg) ->
    254         let addr = get_local_valuel lenv rs in
    255         let f_def = Mem.find_fun_def mem addr in
    256         let args = get_arg_valuesl lenv args in
     262        CallState (sfrs, f_def, args, mem, trace)
     263
     264      | RTLabs.St_tailcall_ptr (r, args, sg) ->
     265        let addr = get_local_value lenv r in
     266        let f_def = Mem.find_fun_def mem (address_of_value addr) in
     267        let args = get_arg_values lenv args in
    257268        (* No need to save the stack frame. But free the stack. *)
    258269        let mem = Mem.free mem sp in
    259         CallState (cs, f_def, args, mem, t)
     270        CallState (sfrs, f_def, args, mem, trace)
    260271
    261272      | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    262273        let v = eval_cst mem sp cst in
    263         branch_state cs c sp lbl_true lbl_false lenv mem t v
    264 
    265       | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
    266         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
    267         branch_state cs c sp lbl_true lbl_false lenv mem t v
    268 
    269       | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
     274        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     275
     276      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
     277        let v = eval_op1 op1 (get_local_value lenv srcr) in
     278        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     279
     280      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
    270281        let v =
    271282          eval_op2 op2
    272             (get_local_valuel lenv srcrs1)
    273             (get_local_valuel lenv srcrs2) in
    274         branch_state cs c sp lbl_true lbl_false lenv mem t v
    275 
    276       | RTLabs.St_jumptable (r, table) -> assert false (* TODO *)
     283            (get_local_value lenv srcr1)
     284            (get_local_value lenv srcr2) in
     285        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     286
     287      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
    277288      (*
    278289        let i = match get_local_value lenv r with
     
    282293        (try
    283294        let next_lbl = List.nth table i in
    284         State (cs, c, sp, next_lbl, lenv, mem, t)
     295        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    285296        with
    286297        | Failure "nth" | Invalid_argument "List.nth" ->
     
    288299      *)
    289300
    290       | RTLabs.St_return rs ->
    291         let v = get_local_valuel lenv rs in
     301      | RTLabs.St_return r ->
     302        let v = get_local_value lenv r in
    292303        let mem = Mem.free mem sp in
    293         ReturnState (cs, v, mem, t)
    294 
    295 
    296 let get_int () =
    297   try Val.of_int (int_of_string (read_line ()))
    298   with Failure "int_of_string" -> error "Failed to scan an integer."
    299 let get_float () =
    300   try Val.of_float (float_of_string (read_line ()))
    301   with Failure "float_of_string" -> error "Failed to scan a float."
    302 
    303 let interpret_external
    304     (mem  : memory)
    305     (def  : AST.external_function)
    306     (args : Val.t list) :
    307     memory * Val.t =
    308   match def.AST.ef_tag, args with
    309     | s, _ when s = Primitive.scan_int ->
    310       (mem, get_int ())
    311     | "scan_float", _ ->
    312       (mem, get_float ())
    313     | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
    314       Printf.printf "%d" (Val.to_int v) ;
    315       (mem, Val.zero)
    316     | "print_float", v :: _ when Val.is_float v ->
    317       Printf.printf "%f" (Val.to_float v) ;
    318       (mem, Val.zero)
    319     | "print_ptr", v :: _ when Val.is_pointer v ->
    320       let (b, off) = Val.to_pointer v in
    321       Printf.printf "block: %s, offset: %s"
    322         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    323       (mem, Val.zero)
    324     | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
    325       Printf.printf "%d\n" (Val.to_int v) ;
    326       (mem, Val.zero)
    327     | "print_floatln", v :: _ when Val.is_float v ->
    328       Printf.printf "%f" (Val.to_float v) ;
    329       (mem, Val.zero)
    330     | "print_ptrln", v :: _ when Val.is_pointer v ->
    331       let (b, off) = Val.to_pointer v in
    332       Printf.printf "block: %s, offset: %s\n"
    333         (Val.Block.to_string b) (Val.Offset.to_string off) ;
    334       (mem, Val.zero)
    335     | s, v :: _ when s = Primitive.alloc ->
    336       let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
    337       (mem, ptr)
    338     | s, v1 :: v2 :: _ when s = Primitive.modulo ->
    339       (mem, Val.modulo v1 v2)
    340 
    341     (* The other cases are either a type error (only integers and pointers
    342        may not be differenciated during type checking) or an unknown
    343        function. *)
    344     | "print_int", _ | "print_intln", _ ->
    345       error "Illegal cast from pointer to integer."
    346     | "print_ptr", _ | "print_ptrln", _ ->
    347       error "Illegal cast from integer to pointer."
    348     | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
    349 
     304        ReturnState (sfrs, v, mem, trace)
     305
     306
     307module InterpretExternal = Primitive.Interpret (Mem)
     308
     309let interpret_external mem f args = match InterpretExternal.t mem f args with
     310  | (mem', InterpretExternal.V v) -> (mem', v)
     311  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
    350312
    351313let init_locals
    352     (locals : Register.t list list)
    353     (params : Register.t list list)
     314    (locals : Register.t list)
     315    (params : Register.t list)
    354316    (args   : Val.t list) :
    355317    local_env =
    356   let f lenv rs = adds rs Val.undef lenv in
     318  let f lenv r = Register.Map.add r Val.undef lenv in
    357319  let lenv = List.fold_left f Register.Map.empty locals in
    358   let f lenv rs v = adds rs v lenv in
     320  let f lenv r v = Register.Map.add r v lenv in
    359321  List.fold_left2 f lenv params args
    360322
    361323let state_after_call
    362     (cs    : stack_frame list)
     324    (sfrs  : stack_frame list)
    363325    (f_def : RTLabs.function_def)
    364326    (args  : Val.t list)
    365327    (mem   : memory)
    366     (t    : CostLabel.t list) :
     328    (trace : CostLabel.t list) :
    367329    state =
    368330  match f_def with
    369331    | RTLabs.F_int def ->
    370332      let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
    371       State (cs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
     333      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
    372334             init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
    373              mem', t)
     335             mem', trace)
    374336    | RTLabs.F_ext def ->
    375       let (mem', v) = interpret_external mem def args in
    376       ReturnState (cs, v, mem', t)
     337      let (mem', v) = interpret_external mem def.AST.ef_tag args in
     338      ReturnState (sfrs, v, mem', trace)
    377339
    378340
    379341let state_after_return
    380342    (sf      : stack_frame)
    381     (cs      : stack_frame list)
     343    (sfrs    : stack_frame list)
    382344    (ret_val : Val.t)
    383345    (mem     : memory)
    384     (t       : CostLabel.t list) :
     346    (trace   : CostLabel.t list) :
    385347    state =
    386   let lenv = adds sf.ret_regs ret_val sf.lenv in
    387   State (cs, sf.graph, sf.sp, sf.pc, lenv, mem, t)
     348  let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in
     349  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
    388350
    389351
    390352let small_step (st : state) : state = match st with
    391   | State (cs, graph, sp, pc, lenv, mem, t) ->
     353  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
    392354    let stmt = Label.Map.find pc graph in
    393     interpret_statement cs graph sp lenv mem stmt t
    394   | CallState (cs, f_def, args, mem, t) ->
    395     state_after_call cs f_def args mem t
    396   | ReturnState ([], ret_val, mem, t) ->
     355    interpret_statement sfrs graph sp lenv mem stmt trace
     356  | CallState (sfrs, f_def, args, mem, trace) ->
     357    state_after_call sfrs f_def args mem trace
     358  | ReturnState ([], ret_val, mem, trace) ->
    397359    assert false (* End of execution; handled in iter_small_step. *)
    398   | ReturnState (sf :: cs, ret_val, mem, t) ->
    399     state_after_return sf cs ret_val mem t
     360  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
     361    state_after_return sf sfrs ret_val mem trace
    400362
    401363
     
    404366  else IntValue.Int8.zero
    405367
    406 let rec iter_small_step print_result st = match small_step st with
    407 (*
    408   (* <DEBUG> *)
    409   | ReturnState ([], v, mem, t) ->
    410     Mem.print mem ;
    411     Printf.printf "Return: %s\n%!" (Val.to_string v) ;
    412     List.rev t
    413   | CallState (_, _, _, mem, _)
    414   | ReturnState (_, _, mem, _)
    415   | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st'
    416   (* </DEBUG> *)
    417 *)
    418   | ReturnState ([], v, mem, t) ->
    419     let (res, cost_labels) as trace = (compute_result v, List.rev t) in
    420     if print_result then
    421       Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ;
    422     trace
    423   | st' -> iter_small_step print_result st'
     368let rec iter_small_step debug st =
     369  if debug then print_state st ;
     370  match small_step st with
     371    | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace)
     372    | st' -> iter_small_step debug st'
    424373
    425374
     
    441390(* Interpret the program only if it has a main. *)
    442391
    443 let interpret print_result p = match p.RTLabs.main with
    444   | None -> (IntValue.Int8.zero, [])
    445   | Some main ->
    446     let mem = init_mem p in
    447     let main_def = find_function mem main in
    448     let st = CallState ([], main_def, [], mem, []) in
    449     iter_small_step print_result st
     392let interpret debug p =
     393  if debug then Printf.printf "*** RTLabs ***\n\n%!" ;
     394  match p.RTLabs.main with
     395    | None -> (IntValue.Int8.zero, [])
     396    | Some main ->
     397      let mem = init_mem p in
     398      let main_def = find_function mem main in
     399      let st = CallState ([], main_def, [], mem, []) in
     400      iter_small_step debug st
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r486 r740  
    1212
    1313
    14 let print_reg_list rl =
    15   Printf.sprintf "[%s]" (MiscPottier.string_of_list " ; " Register.print rl)
     14let print_reg = Register.print
    1615
    1716let rec print_args args =
    18   Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg_list args)
    19 
    20 let print_result rl = print_reg_list rl
    21 
    22 let print_params rl =
    23   Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg_list rl)
    24 
    25 let print_locals rl =
    26   Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg_list rl)
    27 
    28 
    29 let print_memory_q = Memory.string_of_memory_q
     17  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
     18
     19let print_result r = print_reg r
     20
     21let print_params r =
     22  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r)
     23
     24let print_locals r =
     25  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r)
    3026
    3127
     
    5955  | AST.Op_floatofint -> "floatofint"
    6056  | AST.Op_floatofintu -> "floatofintu"
    61   | AST.Op_id -> "mov"
     57  | AST.Op_id -> "id"
    6258  | AST.Op_ptrofint -> "ptrofint"
    6359  | AST.Op_intofptr -> "intofptr"
     
    107103  | RTLabs.St_cost (cost_lbl, lbl) ->
    108104      Printf.sprintf "emit %s --> %s" cost_lbl lbl
    109   | RTLabs.St_cst (dests, cst, lbl) ->
     105  | RTLabs.St_cst (destr, cst, lbl) ->
    110106      Printf.sprintf "imm %s, %s --> %s"
    111         (print_reg_list dests)
     107        (print_reg destr)
    112108        (print_cst cst)
    113109        lbl
    114   | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
     110  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    115111      Printf.sprintf "%s %s, %s --> %s"
    116112        (print_op1 op1)
    117         (print_reg_list dests)
    118         (print_reg_list srcs)
    119         lbl
    120   | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
     113        (print_reg destr)
     114        (print_reg srcr)
     115        lbl
     116  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    121117      Printf.sprintf "%s %s, %s, %s --> %s"
    122118        (print_op2 op2)
    123         (print_reg_list dests)
    124         (print_reg_list srcs1)
    125         (print_reg_list srcs2)
    126         lbl
    127   | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
     119        (print_reg destr)
     120        (print_reg srcr1)
     121        (print_reg srcr2)
     122        lbl
     123  | RTLabs.St_load (q, mode, args, destr, lbl) ->
    128124      Printf.sprintf "load %s, %s, %s, %s --> %s"
    129         (print_memory_q chunk)
     125        (Memory.string_of_quantity q)
    130126        (print_addressing mode)
    131127        (print_args args)
    132         (print_reg_list dests)
    133         lbl
    134   | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
     128        (print_reg destr)
     129        lbl
     130  | RTLabs.St_store (q, mode, args, srcr, lbl) ->
    135131      Printf.sprintf "store %s, %s, %s, %s --> %s"
    136         (print_memory_q chunk)
     132        (Memory.string_of_quantity q)
    137133        (print_addressing mode)
    138134        (print_args args)
    139         (print_reg_list srcs)
     135        (print_reg srcr)
    140136        lbl
    141137  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
     
    143139        f
    144140        (print_params args)
    145         (print_reg_list res)
     141        (print_reg res)
    146142        (Primitive.print_sig sg)
    147143        lbl
    148144  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    149145      Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
    150         (print_reg_list f)
    151         (print_params args)
    152         (print_reg_list res)
     146        (print_reg f)
     147        (print_params args)
     148        (print_reg res)
    153149        (Primitive.print_sig sg)
    154150        lbl
     
    160156  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    161157      Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
    162         (print_reg_list f)
     158        (print_reg f)
    163159        (print_params args)
    164160        (Primitive.print_sig sg)
     
    168164        lbl_true
    169165        lbl_false
    170   | RTLabs.St_cond1 (op1, srcs, lbl_true, lbl_false) ->
     166  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
    171167      Printf.sprintf "%s %s --> %s, %s"
    172168        (print_op1 op1)
    173         (print_reg_list srcs)
     169        (print_reg srcr)
    174170        lbl_true
    175171        lbl_false
    176   | RTLabs.St_cond2 (op2, srcs1, srcs2, lbl_true, lbl_false) ->
     172  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
    177173      Printf.sprintf "%s %s, %s --> %s, %s"
    178174        (print_op2 op2)
    179         (print_reg_list srcs1)
    180         (print_reg_list srcs2)
     175        (print_reg srcr1)
     176        (print_reg srcr2)
    181177        lbl_true
    182178        lbl_false
    183   | RTLabs.St_jumptable (rs, tbl) ->
     179  | RTLabs.St_jumptable (r, tbl) ->
    184180      Printf.sprintf "j_tbl %s --> %s"
    185         (print_reg_list rs)
     181        (print_reg r)
    186182        (print_table tbl)
    187   | RTLabs.St_return rs -> Printf.sprintf "return %s" (print_reg_list rs)
     183  | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r)
    188184
    189185
     
    201197
    202198  Printf.sprintf
    203     "%s\"%s\"%s: %s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
     199    "%s\"%s\"%s: %s\n%slocals: %s\n%spointers: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
    204200    (n_spaces n)
    205201    f
     
    208204    (n_spaces (n+2))
    209205    (print_locals def.RTLabs.f_locals)
     206    (n_spaces (n+2))
     207    (print_locals def.RTLabs.f_ptrs)
    210208    (n_spaces (n+2))
    211209    (print_result def.RTLabs.f_result)
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

    r486 r740  
    22(** This module provides a function to print [RTLabs] programs. *)
    33
     4val print_statement : RTLabs.statement -> string
     5
    46val print_program : RTLabs.program -> string
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r486 r740  
    2828    (def, r :: res)
    2929
    30 let rtl_args regs_list = List.flatten regs_list
    31 
    3230let addr_regs regs = match regs with
    3331  | r1 :: r2 :: _ -> (r1, r2)
    3432  | _ -> error "Function pointer is not an address."
     33
     34
     35(* Local environments associate one (in case of an integer) or two (in case of a
     36   pointer) RTL pseudo-registers to one RTLabs pseudo-register. *)
     37
     38type reg_type =
     39  | Int of Register.t
     40  | Ptr of Register.t * Register.t
     41
     42type local_env = reg_type Register.Map.t
     43
     44let initialize_local_env runiverse ptrs registers =
     45  let f lenv r =
     46    let rt =
     47      if List.mem r ptrs then Ptr (r, Register.fresh runiverse)
     48      else Int r in
     49    Register.Map.add r rt lenv in
     50  List.fold_left f Register.Map.empty registers
     51
     52let filter_and_to_list_local_env lenv registers =
     53  let f l r =
     54    l @ (match Register.Map.find r lenv with
     55      | Int r -> [r]
     56      | Ptr (r1, r2) -> [r1 ; r2]) in
     57  List.fold_left f [] registers
     58
     59let list_of_reg_type = function
     60  | Int r -> [r]
     61  | Ptr (r1, r2) -> [r1 ; r2]
     62
     63let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv)
     64
     65let find_and_list_args args lenv =
     66  List.map (fun r -> find_and_list r lenv) args
     67
     68let find_and_addr r lenv = match find_and_list r lenv with
     69  | r1 :: r2 :: _ -> (r1, r2)
     70  | _ -> assert false (* do not use on these arguments *)
     71
     72let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv)
     73   
    3574
    3675
     
    112151      [RTL.St_stackaddr (r1, r2, start_lbl) ;
    113152       RTL.St_int (tmpr, off, start_lbl) ;
    114        RTL.St_op2 (I8051.Add, r2, r2, tmpr, start_lbl) ;
     153       RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ;
    115154       RTL.St_int (tmpr, 0, start_lbl) ;
    116        RTL.St_op2 (I8051.Addc, r1, r1, tmpr, start_lbl)]
     155       RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)]
    117156      start_lbl dest_lbl def
    118157
     
    128167    | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _
    129168    | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ ->
    130       def
     169      translate_move destrs srcrs start_lbl dest_lbl def
    131170
    132171    | AST.Op_negint, [destr], [srcr] ->
     
    146185    | AST.Op_ptrofint, [destr1 ; destr2], [srcr] ->
    147186      adds_graph
    148         [RTL.St_move (destr2, srcr, dest_lbl) ;
    149          RTL.St_int (destr1, 0, start_lbl)]
    150         start_lbl dest_lbl def
    151 
    152     | AST.Op_intofptr, [destr], [_ ; srcr] ->
     187        [RTL.St_move (destr1, srcr, dest_lbl) ;
     188         RTL.St_int (destr2, 0, start_lbl)]
     189        start_lbl dest_lbl def
     190
     191    | AST.Op_intofptr, [destr], [srcr ; _] ->
    153192      add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
    154193
     
    230269      error_float ()
    231270
    232     | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
     271    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
     272    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
    233273      let (def, tmpr1) = fresh_reg def in
    234274      let (def, tmpr2) = fresh_reg def in
    235275      adds_graph
    236         [RTL.St_op2 (I8051.Add, tmpr2, srcr12, srcr2, start_lbl) ;
    237          RTL.St_int (tmpr1, 0, start_lbl) ;
    238          RTL.St_op2 (I8051.Addc, destr1, tmpr1, srcr11, start_lbl) ;
    239          RTL.St_move (destr2, tmpr2, start_lbl)]
    240         start_lbl dest_lbl def
    241 
    242     | AST.Op_subp, [destr], [_ ; srcr1], [_ ; srcr2] ->
     276        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
     277         RTL.St_int (tmpr2, 0, start_lbl) ;
     278         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
     279         RTL.St_move (destr1, tmpr1, start_lbl)]
     280        start_lbl dest_lbl def
     281
     282    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
    243283      let (def, tmpr1) = fresh_reg def in
    244284      let (def, tmpr2) = fresh_reg def in
     
    251291
    252292    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
    253       let (def, tmpr1) = fresh_reg def in
    254       let (def, tmpr2) = fresh_reg def in
    255       let (def, tmpr3) = fresh_reg def in
    256293      adds_graph
    257294        [RTL.St_clear_carry start_lbl ;
    258          RTL.St_op2 (I8051.Sub, destr2, srcr12, srcr2, start_lbl) ;
    259          RTL.St_int (destr1, 0, start_lbl) ;
    260          RTL.St_op2 (I8051.Sub, destr1, srcr11, destr1, start_lbl)]
     295         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
     296         RTL.St_int (destr2, 0, start_lbl) ;
     297         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
    261298        start_lbl dest_lbl def
    262299
     
    282319
    283320    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
    284       translate_op2 (AST.Op_cmp AST.Cmp_lt)
     321      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
    285322        destrs srcrs2 srcrs1 start_lbl dest_lbl def
    286323
     
    322359      let (def, tmpr2) = fresh_reg def in
    323360      add_translates
    324         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr11] [srcr21] ;
    325          translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr11] [srcr21] ;
    326          translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr12] [srcr22] ;
     361        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
     362         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
     363         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
    327364         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
    328365         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
     
    366403
    367404  | AST.Cst_addrsymbol x ->
    368     let (def, rs) = fresh_regs def 2 in
    369     let r1 = List.nth rs 0 in
    370     let r2 = List.nth rs 1 in
     405    let (def, r1) = fresh_reg def in
     406    let (def, r2) = fresh_reg def in
    371407    let lbl = fresh_label def in
    372408    let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in
     
    417453    | AST.Op_id, _ -> assert false (* wrong number of arguments *)
    418454
    419     | _, _ ->
     455    | _, srcrs ->
    420456      let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in
    421457      let lbl = fresh_label def in
     
    443479  | AST.Op_addp -> 2
    444480  | AST.Op_subp ->
    445     if n = 1 (* sub between pointer and integer *) then 2
    446     else (* sub between two pointers *) 1
     481    if n = 4 (* sub between two pointers, result is an integer *) then 1
     482    else (* sub between a pointer and an integer, result is a pointer *) 2
    447483  | AST.Op_addf
    448484  | AST.Op_subf
     
    463499
    464500    | _, _, _ ->
    465       let n = List.length srcrs2 in
     501      let n = (List.length srcrs1) + (List.length srcrs2) in
    466502      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
    467503      let lbl = fresh_label def in
     
    513549
    514550
    515 let translate_load chunk mode args destrs start_lbl dest_lbl def =
    516   match chunk, destrs with
    517 
    518     | Memory.MQ_pointer, [destr1 ; destr2] ->
     551let translate_load q mode args destrs start_lbl dest_lbl def =
     552  match q, destrs with
     553
     554    | Memory.QInt 1, [destr] ->
     555      let (def, addr1) = fresh_reg def in
     556      let (def, addr2) = fresh_reg def in
     557      add_translates
     558        [addressing_pointer mode args addr1 addr2 ;
     559         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
     560        start_lbl dest_lbl def
     561
     562    | Memory.QPtr, [destr1 ; destr2] ->
    519563      let (def, addr1) = fresh_reg def in
    520564      let (def, addr2) = fresh_reg def in
     
    523567      add_translates
    524568        [addressing_pointer mode args addr1 addr2 ;
    525          adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl) ;
     569         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
    526570                     RTL.St_int (tmpr, 1, start_lbl)] ;
    527571         translate_op2 AST.Op_addp addr addr [tmpr] ;
    528          adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl)]]
    529         start_lbl dest_lbl def
    530 
    531     | Memory.MQ_int8signed, [destr]
    532     | Memory.MQ_int8unsigned, [destr] ->
     572         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
     573        start_lbl dest_lbl def
     574
     575    | _ -> error "Size error in load."
     576
     577
     578let translate_store q mode args srcrs start_lbl dest_lbl def =
     579  match q, srcrs with
     580
     581    | Memory.QInt 1, [srcr] ->
    533582      let (def, addr1) = fresh_reg def in
    534583      let (def, addr2) = fresh_reg def in
    535584      add_translates
    536585        [addressing_pointer mode args addr1 addr2 ;
    537          adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
    538         start_lbl dest_lbl def
    539 
    540     | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
    541     | Memory.MQ_int32, _ ->
    542       error_int ()
    543 
    544     | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
    545       error_float ()
    546 
    547     | _ -> assert false (* wrong number of argument *)
    548 
    549 
    550 let translate_store chunk mode args srcrs start_lbl dest_lbl def =
    551   match chunk, srcrs with
    552 
    553     | Memory.MQ_pointer, [srcr1 ; srcr2] ->
     586         adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
     587        start_lbl dest_lbl def
     588
     589    | Memory.QPtr, [srcr1 ; srcr2] ->
    554590      let (def, addr1) = fresh_reg def in
    555591      let (def, addr2) = fresh_reg def in
     
    558594      add_translates
    559595        [addressing_pointer mode args addr1 addr2 ;
    560          adds_graph [RTL.St_store (addr1, addr2, srcr2, start_lbl) ;
     596         adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ;
    561597                     RTL.St_int (tmpr, 1, start_lbl)] ;
    562598         translate_op2 AST.Op_addp addr addr [tmpr] ;
    563          adds_graph [RTL.St_store (addr1, addr2, srcr1, dest_lbl)]]
    564         start_lbl dest_lbl def
    565 
    566     | Memory.MQ_int8signed, [srcr]
    567     | Memory.MQ_int8unsigned, [srcr] ->
    568       let (def, addr1) = fresh_reg def in
    569       let (def, addr2) = fresh_reg def in
    570       add_translates
    571         [addressing_pointer mode args addr1 addr2 ;
    572          adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
    573         start_lbl dest_lbl def
    574 
    575     | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
    576     | Memory.MQ_int32, _ ->
    577       error_int ()
    578 
    579     | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
    580       error_float ()
    581 
    582     | _ -> assert false (* wrong number of argument *)
    583 
    584 
    585 let translate_stmt lbl stmt def = match stmt with
     599         adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]]
     600        start_lbl dest_lbl def
     601
     602    | _ -> error "Size error in store."
     603
     604
     605let translate_stmt lenv lbl stmt def = match stmt with
    586606
    587607  | RTLabs.St_skip lbl' ->
     
    591611    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
    592612
    593   | RTLabs.St_cst (destrs, cst, lbl') ->
    594     translate_cst cst destrs lbl lbl' def
    595 
    596   | RTLabs.St_op1 (op1, destrs, srcrs, lbl') ->
    597     translate_op1 op1 destrs srcrs lbl lbl' def
    598 
    599   | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl') ->
    600     translate_op2 op2 destrs srcrs1 srcrs2 lbl lbl' def
    601 
    602   | RTLabs.St_load (chunk, mode, args, destrs, lbl') ->
    603     translate_load chunk mode args destrs lbl lbl' def
    604 
    605   | RTLabs.St_store (chunk, mode, args, srcrs, lbl') ->
    606     translate_store chunk mode args srcrs lbl lbl' def
    607 
    608   | RTLabs.St_call_id (f, args, retrs, _, lbl') ->
    609     add_graph lbl (RTL.St_call_id (f, rtl_args args, retrs, lbl')) def
    610 
    611   | RTLabs.St_call_ptr (f, args, retrs, _, lbl') ->
    612     let (f1, f2) = addr_regs f in
     613  | RTLabs.St_cst (destr, cst, lbl') ->
     614    translate_cst cst (find_and_list destr lenv) lbl lbl' def
     615
     616  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
     617    translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv)
     618      lbl lbl' def
     619
     620  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     621    translate_op2 op2 (find_and_list destr lenv)
     622      (find_and_list srcr1 lenv) (find_and_list srcr2 lenv) lbl lbl' def
     623
     624  | RTLabs.St_load (q, mode, args, destr, lbl') ->
     625    translate_load q mode (find_and_list_args args lenv)
     626      (find_and_list destr lenv) lbl lbl' def
     627
     628  | RTLabs.St_store (q, mode, args, srcr, lbl') ->
     629    translate_store q mode (find_and_list_args args lenv)
     630      (find_and_list srcr lenv) lbl lbl' def
     631
     632  | RTLabs.St_call_id (f, args, retr, _, lbl') ->
     633    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
     634                                   find_and_list retr lenv, lbl')) def
     635
     636  | RTLabs.St_call_ptr (f, args, retr, _, lbl') ->
     637    let (f1, f2) = find_and_addr f lenv in
    613638    add_graph lbl
    614       (RTL.St_call_ptr (f1, f2, rtl_args args, retrs, lbl')) def
     639      (RTL.St_call_ptr
     640         (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def
    615641
    616642  | RTLabs.St_tailcall_id (f, args, _) ->
    617     add_graph lbl (RTL.St_tailcall_id (f, rtl_args args)) def
     643    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
    618644
    619645  | RTLabs.St_tailcall_ptr (f, args, _) ->
    620     let (f1, f2) = addr_regs f in
    621     add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args)) def
     646    let (f1, f2) = find_and_addr f lenv in
     647    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
    622648
    623649  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    624650    translate_condcst cst lbl lbl_true lbl_false def
    625651
    626   | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
    627     translate_cond1 op1 srcrs lbl lbl_true lbl_false def
    628 
    629   | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
    630     translate_cond2 op2 srcrs1 srcrs2 lbl lbl_true lbl_false def
     652  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
     653    translate_cond1 op1 (find_and_list srcr lenv)
     654      lbl lbl_true lbl_false def
     655
     656  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
     657    translate_cond2 op2 (find_and_list srcr1 lenv)
     658      (find_and_list srcr2 lenv) lbl lbl_true lbl_false def
    631659
    632660  | RTLabs.St_jumptable _ ->
    633661    error "Jump tables not supported yet."
    634662
    635   | RTLabs.St_return regs ->
    636     add_graph lbl (RTL.St_return regs) def
     663  | RTLabs.St_return r ->
     664    add_graph lbl (RTL.St_return (find_and_list r lenv)) def
    637665
    638666
    639667let translate_internal def =
    640   let set_of_list_list l =
    641     let l = List.flatten l in
    642     List.fold_left (fun res x -> Register.Set.add x res) Register.Set.empty l
    643   in
     668  let runiverse = def.RTLabs.f_runiverse in
     669  let lenv =
     670    initialize_local_env runiverse def.RTLabs.f_ptrs
     671      (def.RTLabs.f_params @ def.RTLabs.f_locals) in
     672  let result = find_and_list def.RTLabs.f_result lenv in
     673  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
     674  let params = filter_and_to_list_local_env lenv def.RTLabs.f_params in
     675  let locals = filter_and_to_list_local_env lenv def.RTLabs.f_locals in
     676  let locals = set_of_list locals in
    644677  let res =
    645678    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
    646       RTL.f_runiverse = def.RTLabs.f_runiverse ;
     679      RTL.f_runiverse = runiverse ;
    647680      RTL.f_sig       = def.RTLabs.f_sig ;
    648       RTL.f_result    = def.RTLabs.f_result ;
    649       RTL.f_params    = List.flatten def.RTLabs.f_params ;
    650       RTL.f_locals    = set_of_list_list def.RTLabs.f_locals ;
     681      RTL.f_result    = result ;
     682      RTL.f_params    = params ;
     683      RTL.f_locals    = locals ;
    651684      RTL.f_stacksize = def.RTLabs.f_stacksize ;
    652685      RTL.f_graph     = Label.Map.empty ;
    653686      RTL.f_entry     = def.RTLabs.f_entry ;
    654687      RTL.f_exit      = def.RTLabs.f_exit } in
    655   Label.Map.fold translate_stmt def.RTLabs.f_graph res
     688  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
    656689
    657690
  • Deliverables/D2.2/8051/src/acc.ml

    r640 r740  
    2929    | None -> (false, filename)
    3030    | Some filename' -> (true, filename') in
    31   let save = Languages.save exact_output output_filename in
     31  let save ?(suffix="") ast =
     32    Languages.save exact_output output_filename suffix ast
     33  in
    3234  let target_asts =
    3335    (** If debugging is enabled, the compilation function returns all
     
    3739  in
    3840  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    39     save final_ast;
    40     (if Options.annotation_requested () then
    41        let (annotated_input_ast, cost_id, cost_incr) =
    42          Languages.annotate input_ast final_ast in
    43        save annotated_input_ast;
    44        Languages.save_cost output_filename cost_id cost_incr);
    45     (if Options.is_debug_enabled () then
    46       List.iter save intermediate_asts);
    47     if Options.interpretation_requested () || Options.is_debug_enabled () then
    48       begin
    49         let asts = input_ast :: target_asts in
    50         let print_result = Options.is_print_result_enabled () in
    51         let label_traces = List.map (Languages.interpret print_result) asts in
    52         Printf.eprintf "Checking execution traces...%!";
    53         Checker.same_traces (List.combine asts label_traces);
    54         Printf.eprintf "OK.\n%!";
    55       end
     41  save final_ast;
     42  if Options.annotation_requested () then
     43    begin
     44      let (annotated_input_ast, cost_id, cost_incr) =
     45        Languages.annotate input_ast final_ast in (
     46          save ~suffix:"-annotated" annotated_input_ast;
     47          Languages.save_cost output_filename cost_id cost_incr);
     48    end;
     49                                             
     50  if Options.is_debug_enabled () then
     51    List.iter save intermediate_asts;
     52
     53  if Options.interpretation_requested () || Options.is_debug_enabled () then
     54    begin
     55      let asts = input_ast :: target_asts in
     56      let label_traces = List.map (Languages.interpret false) asts in
     57      Printf.eprintf "Checking execution traces...%!";
     58      Checker.same_traces (List.combine asts label_traces);
     59      Printf.eprintf "OK.\n%!";
     60    end
    5661
    5762let _ =
  • Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

    r619 r740  
    203203
    204204let translate p =
     205  (* TODO: restore below *)
     206(*
    205207  let (p, unop_assoc, binop_assoc) = Runtime.add p in
    206208  let p = ClightCasts.simplify p in
     
    212214  (* TODO: do the translation *)
    213215  p
     216*)
     217  ClightCasts.simplify p
  • Deliverables/D2.2/8051/src/clight/clightCasts.ml

    r624 r740  
    33
    44    Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
    5     will be transformed into [x + y]. *)
     5    will be transformed into [x + y]. Primitive operations are thus supposed to
     6    be polymorphic, but working only on homogene types. *)
    67
    78let f_ctype ctype _ = ctype
    89
     10(*
    911let f_expr = ClightFold.expr_fill_subs
    1012
     
    6567                  (Clight.Expr (_,
    6668                                Clight.Tint (Clight.I8, signedness2)) as e1)),
    67                _)),
     69               _)),sub_ctypes_res sub_exprs_res
    6870         _) :: _ when signedness1 = signedness2 ->
    6971      Clight.Ebinop (binop,
     
    7274                     e1)
    7375    | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res
     76*)
    7477
    75 let f_statement = ClightFold.statement_fill_subs
     78let simplify_exp ctype_opt e = e (* TODO *)
     79
     80let f_expr e _ _ = e
     81
     82let f_expr_descr e _ _ =  e
     83
     84let f_statement stmt _ sub_stmts_res =
     85  let sub_exprs = match stmt with
     86    | _ -> assert false in
     87  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
    7688
    7789let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
     
    8597  (id, fundef')
    8698
    87 let simplify p =
     99let simplify p = p
     100(* (* TODO: below *)
    88101  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
     102*)
  • Deliverables/D2.2/8051/src/clight/clightCasts.mli

    r619 r740  
    33
    44    Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
    5     will be transformed into [x + y]. *)
     5    will be transformed into [x + y]. Primitive operations are thus supposed to
     6    be polymorphic, but working only on homogene types. *)
    67
    78val simplify : Clight.program -> Clight.program
  • Deliverables/D2.2/8051/src/clight/clightFold.mli

    r619 r740  
    77val ctype : (Clight.ctype -> 'a list -> 'a) -> Clight.ctype -> 'a
    88
    9 val expr : (Clight.expr_descr -> 'a list -> 'b list -> 'c) ->
    10            (Clight.ctype -> 'a list -> 'a) ->
    11            (Clight.expr -> 'c list -> 'a list -> 'b) ->
    12            Clight.expr ->
    13            'b
     9val expr_fill_subs :
     10  Clight.expr -> Clight.ctype list -> Clight.expr_descr list ->
     11  Clight.expr
    1412
    15 val expr_descr : (Clight.ctype -> 'a list -> 'a) ->
    16                  (Clight.expr -> 'b list -> 'a list -> 'c) ->
    17                  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
    18                  Clight.expr_descr ->
    19                  'b
     13val expr :
     14  (Clight.ctype -> 'a list -> 'a) ->
     15  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     16  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     17  Clight.expr ->
     18  'c
    2019
    21 (*
    22 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the
    23    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    24    [f_stmt]'s third argument is the list of [statement_left]'s results
    25    on [stmt]'s sub-statements. The results are computed from left to right
    26    following their appearance order in the [Cminor.statement] type. *)
     20val expr_descr_fill_subs :
     21  Clight.expr_descr -> Clight.ctype list -> Clight.expr list ->
     22  Clight.expr_descr
    2723
    28 val statement_left : (Cminor.expression -> 'a list -> 'a) ->
    29                      (Cminor.statement -> 'a list -> 'b list -> 'b) ->
    30                      Cminor.statement ->
    31                      'b
    32 *)
     24val expr_descr :
     25  (Clight.ctype -> 'a list -> 'a) ->
     26  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     27  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     28  Clight.expr_descr ->
     29  'b
     30
     31val statement_fill_subs :
     32  Clight.statement -> Clight.expr list -> Clight.statement list ->
     33  Clight.statement
     34
     35val statement :
     36  (Clight.ctype -> 'a list -> 'a) ->
     37  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     38  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     39  (Clight.statement -> 'c list -> 'd list -> 'd) ->
     40  Clight.statement ->
     41  'd
  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r630 r740  
    11module Mem = Driver.ClightMemory
    22module Value = Driver.ClightMemory.Value
    3 module Valtbl = Hashtbl.Make(Value)
     3module LocalEnv = Map.Make(String)
     4type localEnv = Value.address LocalEnv.t
     5type memory = Clight.fundef Mem.memory
    46
    57open Clight
    68open AST
    79
    8 let warning msg = print_string ("Warning: "^msg^" (clightInterpret.ml)\n")
    9 
    10 type localEnv = (ident,Value.t) Hashtbl.t
     10
     11let error_prefix = "Clight 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 *)
    1124
    1225type continuation =
     
    1831  | Kfor3 of expr*statement*statement*continuation
    1932  | Kswitch of continuation
    20   | Kcall of (Value.t*ctype) option*cfunction*localEnv*continuation
     33  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    2134
    2235type state =
    23   | State of cfunction*statement*continuation*localEnv*(fundef Mem.memory)
    24   | Callstate of fundef*Value.t list*continuation*(fundef Mem.memory)
    25   | Returnstate of Value.t*continuation*(fundef Mem.memory)
    26 
    27 (* ctype functions *)
    28 
    29 let rec sizeof = function
    30   | Tvoid               -> 0
    31   | Tint (I8,_)         -> 1
    32   | Tint (I16,_)        -> 2
    33   | Tint (I32,_)        -> 4
    34   | Tfloat _            -> assert false (* Not supported *)
    35   | Tpointer _          -> Mem.ptr_size
    36   | Tarray (t,s)        -> s*(sizeof t)                   
    37   | Tfunction (_,_)     -> assert false (* Not supported *)
    38   | Tstruct (_,lst)     ->
    39       List.fold_left
    40         (fun n (_,ty) -> (fun a b -> a+b) n (sizeof ty)) 0 lst
    41   | Tunion (_,lst)      ->
    42       List.fold_left
    43         (fun n (_,ty)   ->
    44            let sz = (sizeof ty) in (if n>sz then n else sz)
    45         ) 0 lst
    46   | Tcomp_ptr _         -> Mem.ptr_size
    47 
    48 let rec mq_of_ty = function
    49   | Tvoid               -> assert false
    50   | Tint (I8,Signed)    -> Memory.MQ_int8signed
    51   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
    52   | Tint (I16,Signed)   -> Memory.MQ_int16signed
    53   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
    54   (*FIXME MQ_int32 : signed or unsigned ?*)
    55   | Tint (I32,Signed)   -> Memory.MQ_int32
    56   | Tint (I32,Unsigned) -> Memory.MQ_int32
    57   | Tfloat _            -> assert false (* Not supported *)
    58   | Tpointer _          -> Mem.mq_of_ptr
    59   | Tarray (c,s)        -> Mem.mq_of_ptr
    60   | Tfunction (_,_)     -> assert false (* Not supported *)
    61   | Tstruct (_,_)       -> Mem.mq_of_ptr
    62   | Tunion (_,_)        -> Mem.mq_of_ptr
    63   | Tcomp_ptr _         -> Mem.mq_of_ptr
    64 
    65 (* Pretty printing for Clight states *)
    66 
    67 let string_s = function
    68   | Sskip                               -> "skip"
    69   | Sassign (Expr (Evar id,_),_)        -> "assign "^id
    70   | Sassign (_,_)                       -> "assign"
    71   | Scall (_,_,_)                       -> "call"
    72   | Ssequence (_,_)                     -> "seq"
    73   | Sifthenelse (_,_,_)                 -> "ifthenelse"
    74   | Swhile (_,_)                        -> "while"
    75   | Sdowhile (_,_)                      -> "dowhile"
    76   | Sfor (_,_,_,_)                      -> "for"
    77   | Sbreak                              -> "break"
    78   | Scontinue                           -> "continue"
    79   | Sreturn _                           -> "return"
    80   | Sswitch (_,_)                       -> "switch"
    81   | Slabel (_,_)                        -> "label"
    82   | Sgoto _                             -> "goto"
    83   | Scost (_,_)                         -> "cost"
    84 
    85 let string_f = function
    86   | Internal _          -> "func"
    87   | External (id,_,_)   -> id
    88 
    89 let string_c = function
    90   | Kstop               -> "stop"
    91   | Kseq (_,_)          -> "seq"
    92   | Kwhile (_,_,_)      -> "while"
    93   | Kdowhile (_,_,_)    -> "dowhile"
    94   | Kfor2 (_,_,_,_)     -> "for2"
    95   | Kfor3 (_,_,_,_)     -> "for3"
    96   | Kswitch _           -> "switch"
    97   | Kcall (_,_,_,_)     -> "call"
    98 
    99 let string_of_state = function
    100   | State (_,s,c,_,_) -> "Regular("^(string_s s)^","^(string_c c)^")"
    101   | Callstate (f,_,c,_) -> "Call("^(string_f f)^","^(string_c c)^")"
    102   | Returnstate (v,c,_) ->
    103       "Return("^(Value.to_string v)^","^(string_c c)^")"
    104 
    105 (* Global and local environment management *)
    106 
    107 let find_funct_id g id =
    108   try Valtbl.find (snd g) (Hashtbl.find (fst g) id)
    109   with Not_found -> assert false
    110 
    111 let find_funct g v =
    112   try Valtbl.find (snd g) (fst v)
    113   with Not_found -> assert false
    114 
    115 let find_symbol globalenv localenv id =
    116   try Hashtbl.find localenv id
    117   with Not_found -> (
    118     try Hashtbl.find (fst globalenv) id
    119     with Not_found ->
    120      Printf.eprintf "Error: cannot find symbol %s\n" id;
    121       assert false
    122   )
     36  | State of cfunction*statement*continuation*localEnv*memory
     37  | Callstate of fundef*Value.t list*continuation*memory
     38  | Returnstate of Value.t*continuation*memory
     39
     40let string_of_unop = function
     41  | Onotbool -> "!"
     42  | Onotint -> "~"
     43  | Oneg -> "-"
     44
     45let string_of_binop = function
     46  | Oadd -> "+"
     47  | Osub -> "-"
     48  | Omul -> "*"
     49  | Odiv -> "/"
     50  | Omod -> "%"
     51  | Oand -> "&"
     52  | Oor  -> "|"
     53  | Oxor -> "^"
     54  | Oshl -> "<<"
     55  | Oshr -> ">>"
     56  | Oeq -> "=="
     57  | One -> "!="
     58  | Olt -> "<"
     59  | Ogt -> ">"
     60  | Ole -> "<="
     61  | Oge -> ">="
     62
     63let string_of_signedness = function
     64  | Signed -> "signed"
     65  | Unsigned -> "unsigned"
     66
     67let string_of_sized_int = function
     68  | I8 -> "char"
     69  | I16 -> "short"
     70  | I32 -> "int"
     71
     72let rec string_of_ctype = function
     73  | Tvoid -> "void"
     74  | Tint (size, sign) ->
     75    (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
     76  | Tfloat _ -> error_float ()
     77  | Tpointer ty -> (string_of_ctype ty) ^ "*"
     78  | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
     79  | Tfunction _ -> assert false (* do not cast to a function type *)
     80  | Tstruct (id, _)
     81  | Tunion (id, _) -> id
     82  | Tcomp_ptr id -> id ^ "*"
     83
     84let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
     85and string_of_expr_descr = function
     86  | Econst_int i -> string_of_int i
     87  | Econst_float _ -> error_float ()
     88  | Evar x -> x
     89  | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
     90  | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
     91  | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
     92  | Ebinop (binop, e1, e2) ->
     93    "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
     94    "(" ^ (string_of_expr e2) ^ ")"
     95  | Ecast (ty, e) ->
     96    "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
     97  | Econdition (e1, e2, e3) ->
     98    "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
     99    ") : (" ^ (string_of_expr e3) ^ ")"
     100  | Eandbool (e1, e2) ->
     101    "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
     102  | Eorbool (e1, e2) ->
     103    "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
     104  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
     105  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
     106  | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     107  | Ecall (f, arg, e) ->
     108    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
     109
     110let string_of_args args =
     111  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
     112
     113let rec string_of_statement = function
     114  | Sskip -> "skip"
     115  | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
     116  | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
     117  | Scall (Some e, f, args) ->
     118    (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
     119  | Ssequence _ -> "sequence"
     120  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
     121  | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
     122  | Sdowhile _ -> "dowhile"
     123  | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
     124  | Sbreak -> "break"
     125  | Scontinue -> "continue"
     126  | Sreturn None -> "return"
     127  | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
     128  | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
     129  | Slabel (lbl, _) -> "label " ^ lbl
     130  | Sgoto lbl -> "goto " ^ lbl
     131  | Scost (lbl, _) -> "cost " ^ lbl
     132
     133let string_of_local_env lenv =
     134  let f x addr s =
     135    s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
     136  LocalEnv.fold f lenv ""
     137
     138let print_state = function
     139  | State (_, stmt, _, lenv, mem) ->
     140    Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     141      (string_of_local_env lenv)
     142      (Mem.to_string mem)
     143      (string_of_statement stmt)
     144  | Callstate (_, args, _, mem) ->
     145    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
     146      (Mem.to_string mem)
     147      (MiscPottier.string_of_list " " Value.to_string args)
     148  | Returnstate (v, _, mem) ->
     149    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
     150      (Mem.to_string mem)
     151      (Value.to_string v)
     152
    123153
    124154(* Continuations and labels *)
    125155
    126156let rec call_cont = function
    127   | Kseq (_,k)          -> call_cont k
    128   | Kwhile (_,_,k)      -> call_cont k
    129   | Kdowhile (_,_,k)    -> call_cont k
    130   | Kfor2 (_,_,_,k)     -> call_cont k
    131   | Kfor3 (_,_,_,k)     -> call_cont k
    132   | Kswitch k           -> call_cont k
    133   | k                   -> k
    134 
    135 let is_call_cont = function
    136   | Kstop | Kcall (_,_,_,_) -> true
    137   | _ -> false
     157  | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
     158  | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     159  | k -> k
    138160
    139161let rec seq_of_labeled_statement = function
    140162  | LSdefault s -> s
    141163  | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
     164
     165let rec find_label1 lbl s k = match s with
     166   | Ssequence (s1,s2) ->
     167      (match find_label1 lbl s1 (Kseq (s2,k)) with
     168      | Some sk -> Some sk
     169      | None -> find_label1 lbl s2 k
     170      )
     171  | Sifthenelse (a,s1,s2) ->
     172      (match find_label1 lbl s1 k with
     173      | Some sk -> Some sk
     174      | None -> find_label1 lbl s2 k
     175      )
     176  | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
     177  | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
     178  | Sfor (a1,a2,a3,s1) ->
     179      (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
     180      | Some sk -> Some sk
     181      | None ->
     182          (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     183          | Some sk -> Some sk
     184          | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     185          ))
     186  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
     187  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
     188  | Scost (_,s') -> find_label1 lbl s' k
     189  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
     190  | Scontinue | Sreturn _ | Sgoto _ -> None
     191           
     192and find_label_ls lbl sl k =  match sl with
     193  | LSdefault s -> find_label1 lbl s k
     194  | LScase (_,s,sl') ->
     195      (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
     196      | Some sk -> Some sk
     197      | None -> find_label_ls lbl sl' k
     198      )
     199
     200let find_label lbl s k = match find_label1 lbl s k with
     201  | Some res -> res
     202  | _ -> assert false (* should be impossible *)
    142203
    143204let rec select_switch i = function
     
    146207  | LScase (_,_,sl') -> select_switch i sl'
    147208
    148 let rec find_label lbl s k = match s with
    149    | Ssequence (s1,s2) ->
    150       (match find_label lbl s1 (Kseq (s2,k)) with
    151       | Some sk -> Some sk
    152       | None -> find_label lbl s2 k
    153       )
    154   | Sifthenelse (a,s1,s2) ->
    155       (match find_label lbl s1 k with
    156       | Some sk -> Some sk
    157       | None -> find_label lbl s2 k
    158       )
    159   | Swhile (a,s1) -> find_label lbl s1 (Kwhile(a,s1,k))
    160   | Sdowhile (a,s1) -> find_label lbl s1 (Kdowhile(a,s1,k))
    161   | Sfor (a1,a2,a3,s1) ->
    162       (match find_label lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
    163       | Some sk -> Some sk
    164       | None ->
    165           (match find_label lbl s1 (Kfor2(a2,a3,s1,k)) with
    166           | Some sk -> Some sk
    167           | None -> find_label lbl a3 (Kfor3(a2,a3,s1,k))
    168           ))
    169   | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
    170   | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label lbl s' k
    171   | Scost (_,s') -> find_label lbl s' k
    172   | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
    173   | Scontinue | Sreturn _ | Sgoto _ -> None
    174            
    175 and find_label_ls lbl sl k =  match sl with
    176   | LSdefault s -> find_label lbl s k
    177   | LScase (_,s,sl') ->
    178       (match find_label lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
    179       | Some sk -> Some sk
    180       | None -> find_label_ls lbl sl' k
    181       )
     209
     210(* ctype functions *)
     211
     212let rec sizeof = function
     213  | Tint (I8, _)  -> 1
     214  | Tint (I16, _) -> 2
     215  | Tint (I32, _) -> 4
     216  | Tfloat _ -> error_float ()
     217  | Tcomp_ptr _ -> Mem.ptr_size
     218  | Tpointer _ -> Mem.ptr_size
     219  | Tarray (ty, n) -> n * (sizeof ty)
     220  | Tstruct (_, fields) ->
     221    let sizes = List.map sizeof (List.map snd fields) in
     222    snd (Mem.align 0 sizes)
     223  | Tunion (_, fields) ->
     224    MiscPottier.max_list (List.map sizeof (List.map snd fields))
     225  | _ -> assert false (* do not use on these arguments *)
     226
     227let size_of_ctype = function
     228  | Tint (I8, _)  -> 1
     229  | Tint (I16, _) -> 2
     230  | Tint (I32, _) -> 4
     231  | Tfloat _ -> error_float ()
     232  | Tcomp_ptr _
     233  | Tpointer _
     234  | Tarray _
     235  | Tstruct _
     236  | Tunion _ -> Mem.ptr_size
     237  | _ -> assert false (* do not use on these arguments *)
     238
     239let is_function_type = function
     240  | Tfunction _ -> true
     241  | _ -> false
     242
     243let is_array_type = function
     244  | Tarray _ -> true
     245  | _ -> false
     246
     247let is_complex_type = function
     248  | Tstruct _ | Tunion _ -> true
     249  | _ -> false
     250
     251let is_big_type t = (is_array_type t) || (is_complex_type t)
     252
     253let dest_type = function
     254  | Tpointer ty | Tarray (ty, _) -> ty
     255  | _ -> assert false (* do not use on these arguments *)
     256
     257
     258(* Global and local environment management *)
     259
     260let find_local x lenv =
     261  if LocalEnv.mem x lenv then LocalEnv.find x lenv
     262  else error ("Unknown local variable " ^ x ^ ".")
     263
     264let find_global x mem =
     265  if Mem.mem_global mem x then Mem.find_global mem x
     266  else error ("Unknown global variable " ^ x ^ ".")
     267
     268let find_symbol lenv mem x =
     269  if LocalEnv.mem x lenv then LocalEnv.find x lenv
     270  else
     271    if Mem.mem_global mem x then Mem.find_global mem x
     272    else error ("Unknown variable " ^ x ^ ".")
     273
     274let find_fundef f mem =
     275  let addr = Mem.find_global mem f in
     276  Mem.find_fun_def mem addr
     277
    182278
    183279(* Interpret *)
    184280
    185 let is_int_type = function
    186   | Tint (_,_)    -> true
    187   | _ -> false
    188 let is_float_type = function
    189   | Tfloat _  -> true
    190   | _ -> false
    191 let is_pointer_type = function
    192   | Tpointer _ | Tarray (_,_) | Tstruct (_,_)
    193   | Tunion (_,_) | Tcomp_ptr _ -> true
    194   | _ -> false
    195 
    196 let eval_cast = function
    197   (* no cast *)
    198   | (e,a,b) when a=b                            -> e
     281let int_of_intsize = function
     282  | I8 -> 8
     283  | I16 -> 16
     284  | I32 -> 32
     285
     286let choose_cast signedness n m v =
     287  let f = match signedness with
     288    | Signed -> Value.sign_ext
     289    | Unsigned -> Value.zero_ext in
     290  f v n m
     291
     292let eval_cast = function
    199293  (* Cast Integer *)
    200   | (v,_,Tint(I8,Signed))                       -> Value.cast8signed v
    201   | (v,_,Tint(I8,Unsigned))                     -> Value.cast8unsigned v
    202   | (v,_,Tint(I16,Signed))                      -> Value.cast16signed v
    203   | (v,_,Tint(I16,Unsigned))                    -> Value.cast16unsigned v
    204   | (v,_,Tint(I32,Signed)) when Value.is_int v  -> v
    205   | (v,_,Tint(I32,Unsigned)) when Value.is_int v-> v (*FIXME*)
    206   (* Cast float*)
    207   | (v,_,Tfloat _)                              -> assert false(*Not supported*)
    208   (* Cast pointeur *)
    209   | (v,Tarray(_,_),Tpointer _)                  -> v
    210   | (v,Tpointer _,Tarray(_,_))                  -> v
    211   | (v,Tpointer _,Tpointer _)                   -> v
    212   | (v,Tarray (_,_),Tarray(_,_))                -> v
    213   | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
    214   | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
    215   | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
    216   | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
    217   (* error *)
    218   | (e,_,_)                                     ->
    219       warning "eval_cast";e (*Value.undef*)
    220 
    221 let eval_unop (v,t) = function 
    222   | Onotbool when is_int_type t -> Value.notbool v
    223   | Onotint when is_int_type t  -> Value.notint v
    224   | Oneg when is_int_type t     -> Value.negint v
    225   | Oneg when is_float_type t   -> assert false (*Not supported*)
    226   | _                           -> assert false (*Type error*)
    227 
    228 let get_subtype = function
    229   | Tarray(t,_) -> t
    230   | Tpointer t -> t
    231   | _ -> assert false (*Misuse of get_subtype*)
    232 
    233 let eval_add = function
    234   (*Integer*)
    235   | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 
    236       let v = Value.add v1 v2 in
    237         (match t1 with
    238            | Tint(I8,Signed)    -> Value.cast8signed v
    239            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    240            | Tint(I16,Signed)   -> Value.cast16signed v
    241            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    242            | Tint(I32,Signed)   -> v
    243            | Tint(I32,Unsigned) -> v (*FIXME*)
    244            | _                  -> assert false (*Prevented by is_int_type*))
    245   (*Float*)
    246   | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
    247       assert false (*Not supported*)
    248   (*Pointer*)
    249   | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    250       Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    251   | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
    252       Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    253   (*Error*)
    254   | _ -> assert false (*Type error*)
    255 
    256 let eval_sub = function
    257   (*Integer*)
    258   | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 ->
    259       let v = Value.sub v1 v2 in
    260         (match t1 with
    261            | Tint(I8,Signed)    -> Value.cast8signed v
    262            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    263            | Tint(I16,Signed)   -> Value.cast16signed v
    264            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    265            | Tint(I32,Signed)   -> v
    266            | Tint(I32,Unsigned) -> v (*FIXME*)
    267            | _                  -> assert false (*Prevented by is_int_type*))
    268   (*Float*)
    269   | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
    270       assert false (*Not supported*)
    271   (*Pointer*)
    272   | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    273       Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    274   (*Error*)
    275   | _ -> assert false (*Type error*)
    276 
    277 let eval_mul = function
    278   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
    279       let v = Value.mul v1 v2 in
    280         (match t1 with
    281            | Tint(I8,Signed)    -> Value.cast8signed v
    282            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    283            | Tint(I16,Signed)   -> Value.cast16signed v
    284            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    285            | Tint(I32,Signed)   -> v
    286            | Tint(I32,Unsigned) -> v (*FIXME*)
    287            | _                  -> assert false (*Prevented by is_int_type*))   
    288   | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
    289       assert false (*Not supported*)
    290   | _ -> assert false (*Type error*)
    291 
    292 let eval_mod = function
    293   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
    294       Value.modulo v1 v2
    295   | _ -> assert false (*Type error*)
    296 
    297 let eval_div = function
    298   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2
    299   | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
    300       assert false (*Not supported*)
    301   | _ -> assert false (*Type error*)
    302 
    303 let eval_and = function
    304   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2
    305   | _ -> assert false (*Type error*)
    306 
    307 let eval_or = function
    308   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2
    309   | _ -> assert false (*Type error*)
    310 
    311 let eval_xor = function
    312   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2
    313   | _ -> assert false (*Type error*)
    314 
    315 let eval_shl = function         
    316   | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shl v1 v2
    317   | _ -> assert false (*Type error*)
    318 
    319 let eval_shr = function         
    320   | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shr v1 v2
    321   | _ -> assert false (*Type error*)
    322 
    323 let eval_eq = function
    324   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2
    325   | _ -> assert false (*Type error*)
    326            
    327 let eval_ne = function
    328   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2
    329   | _ -> assert false (*Type error*)
    330 
    331 let eval_lt = function
    332   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2
    333   | _ -> assert false (*Type error*)
    334 
    335 let eval_gt = function
    336   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2
    337   | _ -> assert false (*Type error*)
    338 
    339 let eval_le = function
    340   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2
    341   | _ -> assert false (*Type error*)
    342 
    343 let eval_ge = function
    344   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2
    345   | _ -> assert false (*Type error*)
    346 
    347 let eval_binop e1 e2 = function
    348   | Oadd -> eval_add (e1,e2)
    349   | Osub -> eval_sub (e1,e2)
    350   | Omul -> eval_mul (e1,e2)
    351   | Odiv -> eval_div (e1,e2)
    352   | Omod -> eval_mod (e1,e2)
    353   | Oand -> eval_and (e1,e2)
    354   | Oor -> eval_or (e1,e2)
    355   | Oxor-> eval_xor (e1,e2)
    356   | Oshl-> eval_shl (e1,e2)
    357   | Oshr-> eval_shr (e1,e2)
    358   | Oeq -> eval_eq (e1,e2)
    359   | One -> eval_ne (e1,e2)
    360   | Olt -> eval_lt (e1,e2)
    361   | Ogt -> eval_gt (e1,e2)
    362   | Ole -> eval_le (e1,e2)
    363   | Oge -> eval_ge (e1,e2)
    364 
    365 let rec get_offset_struct v id = function
    366   | [] -> assert false (*Wrong id*)
    367   | (fi,_)::_ when fi=id -> v
    368   | (_,ty)::ll -> get_offset_struct
    369                     (Value.add v (Value.of_int (sizeof ty))) id ll
    370 
    371 let is_true (v,_) = Value.is_true v
    372 
    373 let is_false (v,_) = Value.is_false v
    374 
    375 let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in
     294  | (v,Tint(isize,signedness),Tint(isize',_)) ->
     295    choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v
     296  | (v,_,_) -> v
     297
     298let eval_unop = function 
     299  | Onotbool -> Value.notbool
     300  | Onotint -> Value.notint
     301  | Oneg -> Value.negint
     302
     303let eval_add (v1,t1) (v2,t2) = match t1, t2 with
     304  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
     305    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
     306    Value.add v1 v
     307  | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
     308    let v = Value.mul (Value.of_int (sizeof ty)) v1 in
     309    Value.add v2 v
     310  | _ -> Value.add v1 v2
     311
     312let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
     313  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
     314    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
     315    Value.sub v1 v
     316  | _ -> Value.sub v1 v2
     317
     318let choose_signedness op_signed op_unsigned v1 v2 t =
     319  let op = match t with
     320    | Tint (_, Signed) -> op_signed
     321    | Tint (_, Unsigned) -> op_unsigned
     322    | _ -> op_unsigned in
     323  op v1 v2
     324
     325let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op =
     326  let v = match op with
     327    | Oadd -> eval_add e1 e2
     328    | Osub -> eval_sub e1 e2
     329    | Omul -> Value.mul v1 v2
     330    | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1
     331    | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1
     332    | Oand -> Value.and_op v1 v2
     333    | Oor -> Value.or_op v1 v2
     334    | Oxor -> Value.xor v1 v2
     335    | Oshl-> Value.shl v1 v2
     336    | Oshr-> Value.shr v1 v2
     337    | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1
     338    | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1
     339    | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1
     340    | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1
     341    | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1
     342    | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
     343  eval_cast (v, t1, ret_ctype)
     344
     345let rec get_offset_struct v id fields =
     346  let sizes = List.map (fun (_, ty) -> sizeof ty) fields in
     347  let (offsets, _) = Mem.align 0 sizes in
     348  let rec select = function
     349    | (x, _) :: _, off :: _ when x = id -> off
     350    | _ :: fields, _ :: offsets -> select (fields, offsets)
     351    | _ -> assert false (* should be impossible *) in
     352  let off = Value.of_int (select (fields, offsets)) in
     353  Value.add v off
     354
     355let get_offset v id = function
     356  | Tstruct (_, fields) -> get_offset_struct v id fields
     357  | Tunion _ -> v
     358  | _ -> assert false (* do not use on these arguments *)
     359
     360let is_true (v, _) = Value.is_true v
     361let is_false (v, _) = Value.is_false v
     362
     363let rec eval_expr localenv m (Expr (ee, tt)) =
    376364  match ee with
    377     | Econst_int i ->
    378         let v = (match tt with
    379                    | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i)
    380                    | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i)
    381                    | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i)
    382                    | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i)
    383                    | Tint(I32,Signed) -> Value.of_int i
    384                    | Tint(I32,Unsigned) -> Value.of_int i (*FIXME*)
    385                    | _ -> assert false (*Type error*))
    386       in ((v,tt),[])
    387     | Econst_float _ -> assert false (*Not supported *)
    388     | Evar id   ->
    389         (match tt with
    390            | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[])
    391            | _ ->
    392                ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[])
    393         )
    394     | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in
    395         ((Mem.load m (mq_of_ty tt) v1,tt),l1)
    396     | Eaddrof exp -> eval_lvalue globalenv localenv m exp
     365    | Econst_int i ->
     366      let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
     367      ((v, tt),[])
     368    | Econst_float _ -> error_float ()
     369    | Evar id when is_function_type tt || is_big_type tt ->
     370      let v = value_of_address (find_symbol localenv m id) in
     371      ((v, tt), [])
     372    | Evar id ->
     373      let addr = find_symbol localenv m id in
     374      let v = Mem.load m (size_of_ctype tt) addr in
     375      ((v, tt), [])
     376    | Ederef e when is_function_type tt || is_big_type tt ->
     377      let ((v1,_),l1) = eval_expr localenv m e in
     378      ((v1,tt),l1)
     379    | Ederef e ->
     380      let ((v1,_),l1) = eval_expr localenv m e in
     381      let addr = address_of_value v1 in
     382      let v = Mem.load m (size_of_ctype tt) addr in
     383      ((v,tt),l1)
     384    | Eaddrof exp ->
     385      let ((addr,_),l) = eval_lvalue localenv m exp in
     386      ((value_of_address addr,tt),l)
     387    | Ebinop (op,exp1,exp2) -> 
     388      let (v1,l1) = eval_expr localenv m exp1 in
     389      let (v2,l2) = eval_expr localenv m exp2 in
     390      ((eval_binop tt v1 v2 op,tt),l1@l2)
    397391    | Eunop (op,exp) ->
    398         let (v1,l1) = eval_expr globalenv localenv m exp in
    399           ((eval_unop v1 op,tt),l1)
    400     | Ebinop (op,exp1,exp2) -> 
    401         let (v1,l1) = eval_expr globalenv localenv m exp1
    402         and (v2,l2) = eval_expr globalenv localenv m exp2 in
    403           ((eval_binop v1 v2 op,tt),l1@l2)
    404     | Ecast (cty,exp) ->
    405         let ((v,ty),l1) = eval_expr globalenv localenv m exp in
    406           ((eval_cast (v,ty,cty),tt),l1)
     392      let ((v1,_),l1) = eval_expr localenv m exp in
     393      ((eval_unop op v1,tt),l1)
    407394    | Econdition (e1,e2,e3) ->
    408         let (v1,l1) = eval_expr globalenv localenv m e1 in
    409           if is_true v1 then
    410             let (v2,l2) = eval_expr globalenv localenv m e2 in
    411               (v2,l1@l2)
    412           else if is_false v1 then
    413             let (v2,l2) = eval_expr globalenv localenv m e3 in
    414               (v2,l1@l2)
    415           else ((Value.undef,tt),l1)
     395      let (v1,l1) = eval_expr localenv m e1 in
     396      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     397      else
     398        if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
     399      else (v1,l1)
    416400    | Eandbool (e1,e2) ->
    417         let (v1,l1) = eval_expr globalenv localenv m e1 in
    418           if is_true v1 then (
    419             let (v2,l2) = eval_expr globalenv localenv m e2 in
    420               if is_true v2 then
    421                 ((Value.val_true,tt),l1@l2)
    422               else (
    423                 if is_false v2 then ((Value.val_false,tt),l1@l2)
    424                 else ((Value.undef,tt),l1@l2)
    425               )) else (
    426                 if is_false v1 then ((Value.val_false,tt),l1)
    427                 else ((Value.undef,tt),l1))
     401      let (v1,l1) = eval_expr localenv m e1 in
     402      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     403      else (v1,l1)
    428404    | Eorbool (e1,e2) ->
    429         let (v1,l1) = eval_expr globalenv localenv m e1 in
    430           if is_false v1 then (
    431             let (v2,l2) = eval_expr globalenv localenv m e2 in
    432               if is_true v2 then ((Value.val_true,tt),l1@l2)
    433               else (
    434                 if is_false v2 then ((Value.val_false,tt),l1@l2)
    435                 else ((Value.undef,tt),l1@l2)
    436           )) else (
    437             if is_true v1 then ((Value.val_true,tt),l1)
    438             else ((Value.undef,tt),l1))
     405      let (v1,l1) = eval_expr localenv m e1 in
     406      if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     407      else (v1,l1)
    439408    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    440409    | Efield (e1,id) ->
    441         let (v1,l1) = eval_expr globalenv localenv m e1 in
    442         (match v1 with
    443            | (v,Tstruct(_,lst)) when List.mem (id,tt) lst ->
    444                ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1)
    445            | (v,Tunion(_,lst)) when List.mem (id,tt) lst ->
    446                ((Mem.load m (mq_of_ty tt) v,tt),l1)
    447            | _ -> ((Value.undef,tt),l1)
    448         )
    449     | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in
    450         (v1,lbl::l1)
    451     | Ecall _ -> assert false (*For annotations only*)
    452 
    453 and eval_lvalue globalenv localenv m expr =
    454   let Expr (e,t) = expr in match e with
    455     | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    456     | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
    457     | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
    458     | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in
    459         (match v1 with
    460            | (v,Tstruct(_,lst)) when List.mem (id,t) lst ->
    461                ((get_offset_struct v id lst,t),l1)
    462            | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1)
    463            | _ -> ((Value.undef,t),l1)
    464         )
    465     | Evar id -> ((find_symbol globalenv localenv id,t),[])
    466     | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in
    467         ((v,t),l1)
    468     | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in
    469         (v,lbl::l)
    470     | Ecall _ -> assert false (*For annotation only*)
    471 
    472 let eval_exprlist globalenv localenv m l =
    473   let rec eval_exprlist_rec vl ll = function
    474     | [] -> (vl,ll)
    475     | e::lst ->
    476         let (vl0,ll0) = eval_exprlist_rec vl ll lst
    477         and ((v,_),t) = eval_expr globalenv localenv m e in
    478         (v::vl0,t@ll0)
    479   in eval_exprlist_rec [] [] l
    480 
    481 let is_struct = function
    482   | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
    483   | _ -> false
    484 
    485 let bind_parameters m param_l arg_l var_l =
    486  let bind (m,e) (id,ty) arg =
    487    if is_struct ty then (
    488      assert (arg=Value.undef); (*a parameter can't be a struct/union/array*)
    489      let (m2,ptr2) = Mem.alloc m (sizeof ty)
    490      in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size)
    491      in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2
    492      in (m4, (Hashtbl.add e id ptr3;e) ))
    493    else
    494      let (m2,ptr) = Mem.alloc m (sizeof ty) in
    495      let m3 = Mem.store m2 (mq_of_ty ty) ptr arg
    496      in (m3, (Hashtbl.add e id ptr;e) )
    497  in
    498    List.fold_left
    499      (fun a b -> bind a b Value.undef)
    500      (try List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l
    501      with (Invalid_argument _) -> assert false)
    502      var_l
    503 
    504 let assign m v ty ptr = Mem.store m (mq_of_ty ty) ptr v
    505 
    506 
    507 let type_of_fundef = function
    508   | Internal f -> Tfunction (List.map snd f.fn_params,f.fn_return)
    509   | External (_,p,t) -> Tfunction (p,t)
    510 
    511 let rec free_list m = function
    512   | [] -> m
    513   | v::l -> free_list (Mem.free m v) l
    514 
    515 let blocks_of_env e =
    516   let l = ref [] in
    517     Hashtbl.iter (fun _ b -> l:=b::(!l)) e;!l
    518 
    519 let typeof e = let Expr (_,t) = e in t
    520 
    521 let interpret_external vargs k m = function
    522     | "scan_int" ->
    523           Returnstate (Value.of_int (int_of_string (read_line ())), k, m)
    524     | "print_int" when List.length vargs = 1 ->
    525         Printf.printf "%d" (Value.to_int (List.hd vargs)) ;
    526         Returnstate (Value.zero, k, m)
    527     | "print_intln" when List.length vargs = 1 ->
    528         Printf.printf "%d\n" (Value.to_int (List.hd vargs)) ;
    529         Returnstate (Value.zero, k, m)
    530     | "malloc" | "alloc" when List.length vargs = 1 ->
    531         let (m',vv) = Mem.alloc m (Value.to_int (List.hd vargs)) in
    532           Returnstate (vv, k, m')
    533    | "exit"  when List.length vargs = 1 -> Returnstate(List.hd vargs,Kstop,m)
    534    | s -> Printf.eprintf "Error: unknown external function: %s\n" s;
    535           assert false (*Unknown external function*)
    536 
    537 let next_step globalenv = function
    538     | State(f,Sassign(a1,a2),k,e,m) ->
    539         let ((v1,t1),l1) = (eval_lvalue globalenv e m a1)
    540         and ((v2,t2),l2) = eval_expr globalenv e m a2
    541         in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
    542     | State(f,Scall(None,a,al),k,e,m) ->
    543         let (v1,l1) = eval_expr globalenv e m a in
    544         let fd = find_funct globalenv v1
    545         and (vargs,l2) = (eval_exprlist globalenv e m al) in
    546           if type_of_fundef fd = typeof a
    547           then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
    548           else assert false (*Signature mismatches*)
    549   | State(f,Scall(Some lhs,a,al),k,e,m) ->
    550       let (v1,l1) = eval_expr globalenv e m a in
    551       let fd = find_funct globalenv v1
    552       and (vargs,l2) = (eval_exprlist globalenv e m al)
    553       and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in
    554         if type_of_fundef fd = typeof a then
    555           (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3)
    556         else assert false (*Signature mismatches*)
    557   | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[])
    558   | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[])
    559   | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[])
    560   | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[])
    561   | State(f,Sifthenelse(a,s1,s2),k,e,m) ->
    562       let (v1,l1) = eval_expr globalenv e m a in
    563         if is_true v1 then (State(f,s1,k,e,m),l1)
    564         else if is_false v1 then (State(f,s2,k,e,m),l1)
    565         else assert false (*Wrong condition guard*)
    566   | State(f,Swhile(a,s),k,e,m) ->
    567       let (v1,l1) = eval_expr globalenv e m a in
    568         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    569         else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1)
    570         else assert false (*Wrong condition guard*)
    571   | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
    572   | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
    573   | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    574   | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    575   | State(f,Sskip,Kdowhile(a,s,k),e,m) ->
    576       let (v1,l1) = eval_expr globalenv e m a in
    577         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    578         else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
    579         else assert false (*Wrong condition guard*)
    580   | State(f,Scontinue,Kdowhile(a,s,k),e,m) ->
    581       let (v1,l1) = eval_expr globalenv e m a in
    582         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    583         else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
    584         else assert false (*Wrong condition guard*)
    585   | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    586   | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip ->
    587       (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
    588   | State(f,Sfor(Sskip,a2,a3,s),k,e,m) ->
    589       let (v1,l1) = eval_expr globalenv e m a2 in
    590       if is_false v1 then (State(f,Sskip,k,e,m),l1)
    591       else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1)
    592       else assert false (*Wrong condition guard*)
    593   | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    594   | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) ->
    595       (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    596   | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    597   | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) ->
    598       (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    599   | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid ->
    600       let m' = free_list m (blocks_of_env e) in
    601         (Returnstate(Value.undef,(call_cont k),m'),[])
    602   | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid ->
    603       let (v1,l1) = eval_expr globalenv e m a
    604       and m' = free_list m (blocks_of_env e) in
    605         (Returnstate(fst v1,call_cont k,m'),l1)
    606   | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k ->
    607       let m' = free_list m (blocks_of_env e) in
    608         (Returnstate(Value.undef,k,m'),[])
    609   | State(f,Sswitch(a,sl),k,e,m) ->
    610       let (n,l) = (match eval_expr globalenv e m a with
    611                      | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll)
    612                      | _ -> assert false (*Wrong switch index*)
    613       ) in
    614         (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
    615   | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
    616   | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
    617   | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[])
    618   | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[])
    619   | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl])
    620   | State(f,Sgoto lbl,k,e,m) ->
    621       (match find_label lbl f.fn_body (call_cont k) with
    622          | Some (s',k') -> (State(f,s',k',e,m),[])
    623          | None -> assert false (*Label does not exist*))
    624   | Callstate(Internal f,vargs,k,m) ->
    625       let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in
    626         (State(f,f.fn_body,k,e,m'),[])
    627   | Callstate(External(id,targs,tres),vargs,k,m)
    628       when List.length targs = List.length vargs ->
    629       (interpret_external vargs k m id,[])
     410      let ((v1,t1),l1) = eval_expr localenv m e1 in
     411      let addr = address_of_value (get_offset v1 id t1) in
     412      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
     413    | Ecost (lbl,e1) ->
     414      let (v1,l1) = eval_expr localenv m e1 in
     415      (v1,lbl::l1)
     416    | Ecall _ -> assert false (* only used by the annotation process *)
     417    | Ecast (cty,exp) ->
     418      let ((v,ty),l1) = eval_expr localenv m exp in
     419      ((eval_cast (v,ty,cty),tt),l1)
     420
     421and eval_lvalue localenv m (Expr (e,t)) = match e with
     422  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
     423  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
     424  | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
     425  | Evar id -> ((find_symbol localenv m id,t),[])
     426  | Ederef ee ->
     427    let ((v,_),l1) = eval_expr localenv m ee in
     428    ((address_of_value v,t),l1)
     429  | Efield (ee,id) ->
     430    let ((v,tt),l1) = eval_expr localenv m ee in
     431    let v' = get_offset v id tt in
     432    ((address_of_value v', t), l1)
     433  | Ecost (lbl,ee) ->
     434    let (v,l) = eval_lvalue localenv m ee in
     435    (v,lbl::l)
     436  | Ecall _ -> assert false (* only used in the annotation process *)
     437
     438let eval_exprlist lenv mem es =
     439  let f (vs, cost_lbls) e =
     440    let ((v, _), cost_lbls') = eval_expr lenv mem e in
     441    (vs @ [v], cost_lbls @ cost_lbls') in
     442  List.fold_left f ([], []) es
     443
     444
     445let bind (mem, lenv) (x, ty) v =
     446  let (mem, addr) = Mem.alloc mem (sizeof ty) in
     447  let mem = Mem.store mem (sizeof ty) addr v in
     448  let lenv = LocalEnv.add x addr lenv in
     449  (mem, lenv)
     450
     451let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
     452
     453let init_fun_env mem params args vars =
     454  let lenv = LocalEnv.empty in
     455  let (mem, lenv) =
     456    try List.fold_left2 bind (mem, lenv) params args
     457    with Invalid_argument _ -> error "wrong size of arguments." in
     458  List.fold_left bind_var (mem, lenv) vars
     459
     460let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
     461
     462
     463let free_local_env mem lenv =
     464  let f _ addr mem = Mem.free mem addr in
     465  LocalEnv.fold f lenv mem
     466
     467let condition v a_true a_false =
     468  if Value.is_false v then a_false
     469  else if Value.is_true v then a_true
     470  else error "undefined condition guard value."
     471
     472let eval_stmt f k e m s = match s, k with
     473  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
     474  | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
     475  | Sskip, Kdowhile(a,s,k) ->
     476    let ((v1, _),l1) = eval_expr e m a in
     477    let a_false = (State(f,Sskip,k,e,m),l1) in
     478    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     479    condition v1 a_true a_false
     480  | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
     481  | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
     482  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
     483  | Sskip, Kcall _ ->
     484    let m' = free_local_env m e in
     485    (Returnstate(Value.undef,k,m'),[])
     486  | Sassign(a1, a2), _ ->
     487    let ((v1,t1),l1) = (eval_lvalue e m a1) in
     488    let ((v2,t2),l2) = eval_expr e m a2 in
     489    (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
     490  | Scall(None,a,al), _ ->
     491    let ((v1,_),l1) = eval_expr e m a in
     492    let fd = Mem.find_fun_def m (address_of_value v1) in
     493    let (vargs,l2) = eval_exprlist e m al in
     494    (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
     495  | Scall(Some lhs,a,al), _ ->
     496    let ((v1,_),l1) = eval_expr e m a in
     497    let fd = Mem.find_fun_def m (address_of_value v1) in
     498    let (vargs,l2) = eval_exprlist e m al in
     499    let (vt3,l3) = eval_lvalue e m lhs in
     500    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
     501  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
     502  | Sifthenelse(a,s1,s2), _ ->
     503    let ((v1,_),l1) = eval_expr e m a in
     504    let a_true = (State(f,s1,k,e,m),l1) in
     505    let a_false = (State(f,s2,k,e,m),l1) in
     506    condition v1 a_true a_false
     507  | Swhile(a,s), _ ->
     508    let ((v1,_),l1) = eval_expr e m a in
     509    let a_false = (State(f,Sskip,k,e,m),l1) in
     510    let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
     511    condition v1 a_true a_false
     512  | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
     513  | Sfor(Sskip,a2,a3,s), _ ->
     514    let ((v1,_),l1) = eval_expr e m a2 in
     515    let a_false = (State(f,Sskip,k,e,m),l1) in
     516    let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     517    condition v1 a_true a_false
     518  | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
     519  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
     520  | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
     521  | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
     522  | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
     523  | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
     524  | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
     525  | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
     526  | Scontinue, Kdowhile(a,s,k) ->
     527    let ((v1,_),l1) = eval_expr e m a in
     528    let a_false = (State(f,Sskip,k,e,m),l1) in
     529    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     530    condition v1 a_true a_false
     531  | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
     532  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
     533  | Sreturn None, _ ->
     534    let m' = free_local_env m e in
     535    (Returnstate(Value.undef,(call_cont k),m'),[])
     536  | Sreturn (Some a), _ ->
     537    let ((v1,_),l1) = eval_expr e m a  in
     538    let m' = free_local_env m e in
     539    (Returnstate(v1,call_cont k,m'),l1)
     540  | Sswitch(a,sl), _ ->
     541    let ((v,_),l) = eval_expr e m a in
     542    let n = Value.to_int v in
     543    (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
     544  | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
     545  | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
     546  | Sgoto lbl, _ ->
     547    let (s', k') = find_label lbl f.fn_body (call_cont k) in
     548    (State(f,s',k',e,m),[])
     549  | _ -> assert false (* should be impossible *)
     550
     551
     552module InterpretExternal = Primitive.Interpret (Mem)
     553
     554let interpret_external k mem f args =
     555  let (mem', v) = match InterpretExternal.t mem f args with
     556    | (mem', InterpretExternal.V v) -> (mem', v)
     557    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
     558  Returnstate (v, k, mem')
     559
     560let step_call args cont mem = function
     561  | Internal f ->
     562    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
     563    State (f, f.fn_body, cont, e, mem')
     564  | External(id,targs,tres) when List.length targs = List.length args ->
     565    interpret_external cont mem id args
     566  | External(id,_,_) ->
     567    error ("wrong size of arguments when calling external " ^ id ^ ".")
     568
     569let step = function
     570  | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
     571  | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    630572  | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
    631573  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
    632       let m' = assign m v ty vv in
    633         (State(f,Sskip,k,e,m'),[])
    634   | st ->
    635       Printf.eprintf "Error: no transition for %s\n" (string_of_state st);
    636       assert false
    637 
    638 let init_to_data = function
     574    let m' = assign m v ty vv in
     575    (State(f,Sskip,k,e,m'),[])
     576  | _ -> error "state malformation."
     577
     578
     579let data_of_init_data = function
    639580  | Init_int8 i         -> Data_int8 i
    640581  | Init_int16 i        -> Data_int16 i
    641582  | Init_int32 i        -> Data_int32 i
    642   | Init_float32 f      -> assert false (* Not supported *)
    643   | Init_float64 f      -> assert false (* Not supported *)
     583  | Init_float32 f      -> error_float ()
     584  | Init_float64 f      -> error_float ()
    644585  | Init_space i        -> Data_reserve i
    645   | Init_addrof (_,_)   -> assert false (*TODO*)
    646 
    647 let alloc_datas m ((_,lst),ty) =
    648   let store_data (m,ptr) = function (*FIXME signed or unsigned ?*)
    649     | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
    650                        ,Value.add ptr (Value.of_int 1))
    651     | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
    652                        ,Value.add ptr (Value.of_int 2))
    653     | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
    654                        ,Value.add ptr (Value.of_int 4))
    655     | Init_float32 _ -> assert false (*Not supported*)
    656     | Init_float64 _ -> assert false (*Not supported*)
    657     | Init_space n -> (m,Value.add ptr (Value.of_int n))
    658     | Init_addrof (_,_) -> assert false (*TODO*)
    659   in let (m2,ptr) = (Mem.alloc m (sizeof ty))
    660   in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
    661 
    662 let initmem_clight prog =
    663   let alloc_funct i (g,f) (id,fct) =
    664     Hashtbl.add g id (Value.of_int (-i-1));
    665     Valtbl.add f (Value.of_int (-i-1)) fct;
    666     (g,f)
    667   and alloc_var (m,g) v =
    668     let (m',ptr) = alloc_datas m v in
    669       if is_struct (snd v) then
    670         let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in
    671         let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
    672         Hashtbl.add g (fst (fst v)) ptr2;(m3,g)
    673       else
    674         ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
    675   in let (m,g) =
    676     List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
    677   in let (g2,f) =
    678     MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct
    679   in
    680     (m,(g2,f))
     586  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
     587
     588let init_mem prog =
     589  let f_var mem ((x, init_datas), ty) =
     590    Mem.add_var mem x (List.map data_of_init_data init_datas) in
     591  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
     592  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
     593  List.fold_left f_fun_def mem prog.prog_funct
    681594
    682595let compute_result v =
     
    684597  else IntValue.Int8.zero
    685598
    686 let interpret debug prog = match prog.prog_main with
    687   | None -> (IntValue.Int8.zero, [])
    688   | Some main ->
    689       let (m,g) = initmem_clight prog in
    690       let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in
    691       let rec exec trace = function
    692         | (Returnstate(v,Kstop,m),l) ->
    693 (*
    694             if debug then (
    695               print_string ("Result: "^(Value.to_string v));
    696               print_string ("\nMemory dump: \n");
    697               Mem.print m
    698             );
    699 *)
    700           let (res, cost_labels) as trace = (compute_result v, l@trace) in
    701           if debug then
    702             Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
    703           trace
    704         | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*)
    705 (*
    706             if debug then (
    707               print_string ("Result: (implicit return)");
    708               print_string ("\nMemory dump: \n");
    709               Mem.print m
    710             );
    711 *)
    712           let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in
    713           if debug then
    714             Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
    715           trace
    716         | (state,l) ->
    717 (*
    718             if debug then print_string ((string_of_state state)^"\n");
    719 *)
    720             exec (l@trace) (next_step g state)
    721       in
    722 (*
    723       if debug then print_string "> --- Interpret Clight --- <\n";
    724 *)
    725       exec [] first_state
     599let rec exec debug trace (state, l) =
     600  let cost_labels = l @ trace in
     601  let print_and_return_result res =
     602    if debug then Printf.printf "Result = %s\n%!"
     603      (IntValue.Int8.to_string res) ;
     604    (res, cost_labels) in
     605  if debug then print_state state ;
     606  match state with
     607    | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     608      print_and_return_result (compute_result v)
     609    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     610      print_and_return_result IntValue.Int8.zero
     611    | state -> exec debug cost_labels (step state)
     612
     613let interpret debug prog =
     614  if debug then Printf.printf "*** Clight ***\n\n%!" ;
     615  match prog.prog_main with
     616    | None -> (IntValue.Int8.zero, [])
     617    | Some main ->
     618      let mem = init_mem prog in
     619      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     620      exec debug [] first_state
  • Deliverables/D2.2/8051/src/clight/clightInterpret.mli

    r486 r740  
    33    can also print debug informations.  *)
    44
     5(** [interpret debug p] returns the trace of execution of program [p]. *)
     6
    57val interpret: bool -> Clight.program -> AST.trace
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r486 r740  
    11let process file =
    2   let tmp_file = Filename.temp_file "cparser" ".i"
     2  let tmp_file1 = Filename.temp_file "cparser1" ".c"
     3  and tmp_file2 = Filename.temp_file "cparser2" ".i"
    34  and prepro_opts = [] in
     5
     6  (* Add CerCo's primitives *)
     7  let _ =
     8    try
     9      let oc = open_out tmp_file1 in
     10      output_string oc Primitive.prototypes ;
     11      close_out oc
     12    with Sys_error _ -> failwith "Error adding primitive prototypes." in
     13  let rc = Sys.command
     14    (Printf.sprintf "cat %s >> %s"
     15       (Filename.quote file) (Filename.quote tmp_file1)) in
     16  if rc <> 0 then (
     17    Misc.SysExt.safe_remove tmp_file1;
     18    failwith "Error adding primitive prototypes."
     19  );
    420
    521  (* Preprocessing *)
     
    824    (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
    925       (String.concat " " (List.map Filename.quote prepro_opts))
    10        (Filename.quote file) (Filename.quote tmp_file)) in
     26       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    1127  if rc <> 0 then (
    12     Misc.SysExt.safe_remove tmp_file; failwith "Error calling gcc."
     28    Misc.SysExt.safe_remove tmp_file1;
     29    Misc.SysExt.safe_remove tmp_file2;
     30    failwith "Error calling gcc."
    1331  );
    1432
    1533  (* C to Cil *)
    16   let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file in
    17   Misc.SysExt.safe_remove tmp_file;
     34  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
     35  Misc.SysExt.safe_remove tmp_file1;
     36  Misc.SysExt.safe_remove tmp_file2;
    1837  match r with
    1938    | None -> failwith "Error during C parsing."
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r624 r740  
    22open Cminor
    33open Clight
     4
     5
     6let error_prefix = "Cminor to RTLabs"
     7let error = Error.global_error error_prefix
     8let error_float () = error "float not supported."
     9
    410
    511(*For internal use*)
     
    1420let ptr_size = Driver.CminorMemory.ptr_size
    1521let alignment = Driver.CminorMemory.alignment
    16 let ptr_mq = Memory.MQ_pointer
    1722
    1823let fresh_tmp variables =
     
    3641  | _           -> Sig_int
    3742
    38 let rec mq_of_ty = function
     43let rec size_of_ty = function
    3944  | Tvoid               -> assert false
    4045  | Tfloat _            -> assert false (*Not supported*)
    4146  | Tfunction (_,_)     -> assert false (*Not supported*)
    42   | Tint (I8,Signed)    -> Memory.MQ_int8signed
    43   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
    44   | Tint (I16,Signed)   -> Memory.MQ_int16signed
    45   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
     47  | Tint (I8,Signed)    -> 1
     48  | Tint (I8,Unsigned)  -> 1
     49  | Tint (I16,Signed)   -> 2
     50  | Tint (I16,Unsigned) -> 2
    4651  (*FIXME MQ_int32 : signed or unsigned ? *)
    47   | Tint (I32,Signed)   -> Memory.MQ_int32
    48   | Tint (I32,Unsigned) ->  Memory.MQ_int32
     52  | Tint (I32,Signed)   -> 4
     53  | Tint (I32,Unsigned) -> 4
    4954  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    50   | Tcomp_ptr _         -> ptr_mq
     55  | Tcomp_ptr _         -> ptr_size
     56
     57let size_of_intsize = function
     58  | I8 -> 1
     59  | I16 -> 2
     60  | I32 -> 4
     61
     62let quantity_of_ty = function
     63  | Tvoid               -> assert false (* do not use on this argument *)
     64  | Tint (size,_)       -> Memory.QInt (size_of_intsize size)
     65  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
     66  | Tfunction (_,_)
     67  | Tcomp_ptr _         -> Memory.QPtr
     68  | Tfloat _            -> error_float ()
    5169
    5270let init_to_data l = List.map (
     
    103121      Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    104122  | (Tint(_,_),Tpointer t)      ->
    105       Op2 (Op_addp,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
     123      Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))))
    106124  | (Tarray (t,_),Tint(_,_))    ->
    107125      Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
     
    115133  | (Tpointer t,Tint(_,_))      ->
    116134      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    117   | (Tint(_,_),Tpointer t)      ->
    118       Op2 (Op_subp,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
    119135  | (Tarray (t,_),Tint(_,_))    ->
    120136      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    121   | (Tint(_,_),Tarray(t,_))     ->
    122       Op2 (Op_subp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    123137  | _                           -> assert false (*Type error*)
    124138
     
    129143
    130144let translate_div e1 e2 = function
    131 (*
    132145  | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_div,e1,e2)
    133 *)
    134   (* TODO: temporary hack! *)
    135   | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_divu,e1,e2)
    136146  | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2)
    137147  | (Tfloat _,Tfloat _)                 -> assert false (*Not supported*)
     
    157167
    158168let make_cast e = function
    159   | (Tint(_,_),Tint(I8,Signed)) when int_size>8     -> Op1 (Op_cast8signed,e)
    160   | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8   -> Op1 (Op_cast8unsigned,e)
    161   | (Tint(_,_),Tint(I16,Signed)) when int_size>16   -> Op1 (Op_cast16signed,e)
    162   | (Tint(_,_),Tint(I16,Unsigned)) when int_size>16 -> Op1 (Op_cast16unsigned,e)
     169  | (Tint(I8,Signed),Tint(_,_))    -> Op1 (Op_cast8signed,e)
     170  | (Tint(I8,Unsigned),Tint(_,_))  -> Op1 (Op_cast8unsigned,e)
     171  | (Tint(I16,Signed),Tint(_,_))   -> Op1 (Op_cast16signed,e)
     172  | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e)
    163173  | _ -> e
    164174
     
    191201           | (Local,_)          -> Id id
    192202           | (Stack o,ty) when is_struct ty     -> Cst (Cst_stackoffset o)
    193            | (Stack o,_)        -> Mem (mq_of_ty c,Cst (Cst_stackoffset o))
     203           | (Stack o,_)        ->
     204             Mem (quantity_of_ty c,Cst (Cst_stackoffset o))
    194205           | (Param,_)          -> Id id
    195206           | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id)
    196            | (Global,_)         -> Mem (mq_of_ty c,Cst (Cst_addrsymbol id))
     207           | (Global,_)         ->
     208             Mem (quantity_of_ty c,Cst (Cst_addrsymbol id))
    197209        ) with Not_found -> assert false)
    198210    | Ederef e when is_ptr_to_struct (get_type e) ->
    199211        translate_expr variables e
    200     | Ederef e          -> Mem (mq_of_ty c,translate_expr variables e)
     212    | Ederef e          -> Mem (quantity_of_ty c,translate_expr variables e)
    201213    | Eaddrof se        ->  (
    202214        match se with
     
    248260           | Tstruct(_,lst) ->
    249261               (try
    250                   Mem (mq_of_ty (List.assoc id lst)
     262                  Mem (quantity_of_ty (List.assoc id lst)
    251263                       ,Op2(Op_add
    252264                            ,translate_expr variables e
     
    258270           | Tunion(_,lst) ->
    259271               (try
    260                   Mem (mq_of_ty (List.assoc id lst), translate_expr variables e)
     272                  Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e)
    261273                with Not_found -> assert false (*field does not exists*)
    262274               )
     
    270282      (try (match Hashtbl.find variables v with
    271283         | (Local,_)            -> St_assign (v,translate_expr variables e)
    272          | (Stack o,_)          -> St_store (mq_of_ty t
     284         | (Stack o,_)          -> St_store (quantity_of_ty t
    273285                                             ,Cst (Cst_stackoffset o)
    274286                                             ,translate_expr variables e)
    275287         | (Param,_)            -> St_assign (v,translate_expr variables e)
    276          | (Global,_)           -> St_store (mq_of_ty t
     288         | (Global,_)           -> St_store (quantity_of_ty t
    277289                                             ,Cst (Cst_addrsymbol v)
    278290                                             ,translate_expr variables e)
    279291      ) with Not_found -> assert false)
    280   | Expr (Ederef ee,t)          -> St_store (mq_of_ty t
     292  | Expr (Ederef ee,t)          -> St_store (quantity_of_ty t
    281293                                             ,translate_expr variables ee
    282294                                             ,translate_expr variables e)
     
    284296      (match ee with
    285297         | Expr (_,Tstruct(_,lst)) ->
    286              St_store (mq_of_ty t
     298             St_store (quantity_of_ty t
    287299                       ,Op2(Op_add,translate_expr variables ee
    288300                            ,Cst(Cst_int (get_offset_struct 0 id lst )))
    289301                       ,translate_expr variables e)
    290          | Expr (_,Tunion(_,_)) -> St_store (mq_of_ty t
     302         | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t
    291303                                             ,translate_expr variables ee
    292304                                             ,translate_expr variables e)
     
    319331                         St_seq (
    320332                           st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    321                            ,St_store (mq_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
     333                           ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
    322334                         )
    323335                   | (Global,_) ->
     
    325337                         St_seq (
    326338                           st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    327                            ,St_store (mq_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
     339                           ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
    328340                         )
    329341                ) with Not_found -> assert false )
     
    526538
    527539let translate p =
    528   (* TODO: Clight32 to Clight8 transformation *)
    529 (*
    530540  let p = Clight32ToClight8.translate p in
    531 *)
    532   (* <DEBUG> *)
    533 (*
    534   Printf.printf "%s\n%!" (ClightPrinter.print_program p) ;
    535 *)
    536   (* </DEBUG> *)
    537541  let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
    538542  let p =
     
    540544     Cminor.functs = List.map (translate_funct globals ) p.prog_funct;
    541545     Cminor.main = p.prog_main } in
     546  (* TODO: find a better solution to get the pointers in the result. *)
    542547  CminorPointers.fill p
  • 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 sig