src/LTL/LTLInterpret.ml

   1
   2 (** This module provides an interpreter for the LTL language. *)
   3
   4
   5 let error_prefix = "LTL interpret"
   6 let error s = Error.global_error error_prefix s
   7
   8
   9 module Mem = Driver.LTLMemory
  10 module Val = Mem.Value
  11 let chunk = Driver.LTLMemory.int_size
  12 module Eval = I8051.Eval (Val)
  13
  14
  15 (* Memory *)
  16
  17 type memory = LTL.function_def Mem.memory
  18
  19 (* Hardware registers environments. They associate a value to the each hardware
  20    register. *)
  21
  22 type hdw_reg_env = Val.t I8051.RegisterMap.t
  23
  24 (* Execution states. *)
  25
  26 type state =
  27     { pc     : Val.address ;
  28       isp    : Val.address ;
  29       exit   : Val.address ;
  30       carry  : Val.t ;
  31       renv   : hdw_reg_env ;
  32       mem    : memory ;
  33       trace  : CostLabel.t list }
  34
  35
  36 (* Helpers *)
  37
  38 let change_pc st pc = { st with pc = pc }
  39 let change_isp st isp = { st with isp = isp }
  40 let change_exit st exit = { st with exit = exit }
  41 let change_carry st carry = { st with carry = carry }
  42 let change_renv st renv = { st with renv = renv }
  43 let change_mem st mem = { st with mem = mem }
  44 let change_trace st trace = { st with trace = trace }
  45 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
  46
  47 let empty_state =
  48   { pc     = Val.null ;
  49     isp    = Val.null ;
  50     exit   = Val.null ;
  51     carry  = Val.undef ;
  52     renv   = I8051.RegisterMap.empty ;
  53     mem    = Mem.empty ;
  54     trace  = [] }
  55
  56
  57 (* Each label of each function is associated a pointer. The base of this pointer
  58    is the base of the function in memory. Inside a function, offsets are
  59    bijectively associated to labels. *)
  60
  61 module Labels_Offsets = Bijection.Make (Label) (Val.Offset)
  62
  63 let labels_offsets_internal int_fun =
  64   let f lbl _ (lbls_offs, i) =
  65     (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in
  66   Label.Map.fold f int_fun.LTL.f_graph
  67
  68 (* [labels_offsets p] builds a bijection between the labels found in the
  69    functions of [p] and some offsets. *)
  70
  71 let labels_offsets p =
  72   let f (lbls_offs, i) (_, def) = match def with
  73     | LTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i)
  74     | _ -> (lbls_offs, i) in
  75   fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.LTL.functs)
  76
  77 let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
  78   | LTL.F_int def -> def
  79   | _ -> error "Trying to fetch the definition of an external function."
  80
  81 let fetch_stmt lbls_offs st =
  82   let msg =
  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
  87     let def = fun_def_of_ptr st.mem st.pc in
  88     let lbl = Labels_Offsets.find2 off lbls_offs in
  89     Label.Map.find lbl def.LTL.f_graph
  90   else error msg
  91
  92 let entry_pc lbls_offs ptr def =
  93   Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
  94
  95 let init_fun_call lbls_offs st ptr def =
  96   let pc = entry_pc lbls_offs ptr def in
  97   change_pc st pc
  98
  99 let next_pc lbls_offs st lbl =
 100   let off = Labels_Offsets.find1 lbl lbls_offs in
 101   change_pc st (Val.change_address_offset st.pc off)
 102
 103 let framesize st =
 104   if Val.is_mem_address st.pc then
 105     let def = fun_def_of_ptr st.mem st.pc in
 106     def.LTL.f_stacksize
 107   else error "Trying to load the stack size of an external function."
 108
 109 let add_reg r v st =
 110   let renv = I8051.RegisterMap.add r v st.renv in
 111   change_renv st renv
 112
 113 let get_reg r st =
 114   if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
 115   else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
 116
 117 let push st v =
 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
 120   change_mem (change_isp st isp) mem
 121
 122 let pop st =
 123   let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
 124   let st = change_isp st isp in
 125   let v = Mem.load st.mem chunk st.isp in
 126   (st, v)
 127
 128 let save_ra lbls_offs st lbl =
 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
 133   st
 134
 135 let label_of_pointer lbls_offs ptr =
 136 (*
 137   Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
 138 *)
 139   let off = Val.offset_of_address ptr in
 140   Labels_Offsets.find2 off lbls_offs
 141
 142 let pointer_of_label lbls_offs ptr lbl =
 143   Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
 144
 145 let return_pc st =
 146   let (st, pch) = pop st in
 147   let (st, pcl) = pop st in
 148   (st, [pcl ; pch])
 149
 150 let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
 151
 152
 153 (* State pretty-printing *)
 154
 155 let current_label lbls_offs st =
 156   Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
 157
 158 let 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
 164 let 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
 176 module InterpretExternal = Primitive.Interpret (Mem)
 177
 178 let interpret_external mem f args = match InterpretExternal.t mem f args with
 179   | (mem', InterpretExternal.V vs) -> (mem', vs)
 180   | (mem', InterpretExternal.A addr) -> (mem', addr)
 181
 182 let fetch_external_args f st =
 183   let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
 184   let params = MiscPottier.prefix size I8051.parameters in
 185   List.map (fun r -> get_reg r st) params
 186
 187 let set_result st vs =
 188   let f st (r, v) = add_reg r v st in
 189   List.fold_left f st (MiscPottier.combine I8051.rets vs)
 190
 191 let interpret_external_call st f next_pc =
 192   let args = fetch_external_args f st in
 193   let (mem, vs) = interpret_external st.mem f args in
 194   let st = change_mem st mem in
 195   let st = set_result st vs in
 196   change_pc st next_pc
 197
 198 let interpret_call lbls_offs st ptr ra =
 199   match Mem.find_fun_def st.mem ptr with
 200     | LTL.F_int def ->
 201       let st = save_ra lbls_offs st ra in
 202       init_fun_call lbls_offs st ptr def
 203     | LTL.F_ext def ->
 204       let next_pc =
 205         Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
 206       interpret_external_call st def.AST.ef_tag next_pc
 207
 208 let interpret_return lbls_offs st =
 209   let (st, pc) = return_pc st in
 210   change_pc st pc
 211
 212
 213 (* Interpret statements. *)
 214
 215 let interpret_stmt lbls_offs st stmt =
 216   let next_pc = next_pc lbls_offs in
 217   match stmt with
 218
 219     | LTL.St_skip lbl ->
 220       next_pc st lbl
 221
 222     | LTL.St_comment (s, lbl) ->
 223 (*
 224       Printf.printf "*** %s ***\n\n%!" s ;
 225 *)
 226       next_pc st lbl
 227
 228     | LTL.St_cost (cost_lbl, lbl) ->
 229       let st = add_trace st cost_lbl in
 230       next_pc st lbl
 231
 232     | LTL.St_int (r, i, lbl) ->
 233       let st = add_reg r (Val.of_int i) st in
 234       next_pc st lbl
 235
 236     | LTL.St_pop lbl ->
 237       let (st, v) = pop st in
 238       let st = add_reg I8051.a v st in
 239       next_pc st lbl
 240
 241     | LTL.St_push lbl ->
 242       let v = get_reg I8051.a st in
 243       let st = push st v in
 244       next_pc st lbl
 245
 246     | LTL.St_addr (x, lbl) ->
 247       let vs = Mem.find_global st.mem x in
 248       let st = add_reg I8051.dpl (List.nth vs 0) st in
 249       let st = add_reg I8051.dph (List.nth vs 1) st in
 250       next_pc st lbl
 251
 252     | LTL.St_from_acc (destr, lbl) ->
 253       let st = add_reg destr (get_reg (I8051.a) st) st in
 254       next_pc st lbl
 255
 256     | LTL.St_to_acc (srcr, lbl) ->
 257       let st = add_reg I8051.a (get_reg srcr st) st in
 258       next_pc st lbl
 259
 260     | LTL.St_opaccs (opaccs, lbl) ->
 261       let (a, b) =
 262         Eval.opaccs opaccs
 263           (get_reg I8051.a st)
 264           (get_reg I8051.b st) in
 265       let st = add_reg I8051.a a st in
 266       let st = add_reg I8051.b b st in
 267       next_pc st lbl
 268
 269     | LTL.St_op1 (op1, lbl) ->
 270       let v = Eval.op1 op1 (get_reg I8051.a st) in
 271       let st = add_reg I8051.a v st in
 272       next_pc st lbl
 273
 274     | LTL.St_op2 (op2, srcr, lbl) ->
 275       let (v, carry) =
 276         Eval.op2 st.carry op2
 277           (get_reg I8051.a st)
 278           (get_reg srcr st) in
 279       let st = change_carry st carry in
 280       let st = add_reg I8051.a v st in
 281       next_pc st lbl
 282
 283     | LTL.St_clear_carry lbl ->
 284       let st = change_carry st Val.zero in
 285       next_pc st lbl
 286
 287     | LTL.St_set_carry lbl ->
 288       let st = change_carry st (Val.of_int 1) in
 289       next_pc st lbl
 290
 291     | LTL.St_load lbl ->
 292       let addr = dptr st in
 293       let v = Mem.load st.mem chunk addr in
 294       let st = add_reg I8051.a v st in
 295       next_pc st lbl
 296
 297     | LTL.St_store lbl ->
 298       let addr = dptr st in
 299       let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
 300       let st = change_mem st mem in
 301       next_pc st lbl
 302
 303     | LTL.St_call_id (f, lbl) ->
 304       interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
 305
 306     | LTL.St_call_ptr lbl ->
 307       interpret_call lbls_offs st (dptr st) lbl
 308
 309     | LTL.St_condacc (lbl_true, lbl_false) ->
 310       let v = get_reg I8051.a st in
 311       let lbl =
 312         if Val.is_true v then lbl_true
 313         else
 314           if Val.is_false v then lbl_false
 315           else error "Undecidable branchment." in
 316       next_pc st lbl
 317
 318     | LTL.St_return ->
 319       interpret_return lbls_offs st
 320
 321
 322 let compute_result st =
 323   let vs = List.map (fun r -> get_reg r st) I8051.rets in
 324   let f res v = res && (Val.is_int v) in
 325   let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
 326   if is_int vs then
 327     let chunks =
 328       List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
 329     IntValue.Int32.merge chunks
 330   else IntValue.Int32.zero
 331
 332 let rec iter_small_step debug lbls_offs st =
 333   let print_and_return_result (res, cost_labels) =
 334     if debug then Printf.printf "Result = %s\n%!"
 335       (IntValue.Int32.to_string res) ;
 336     (res, cost_labels) in
 337   if debug then print_state lbls_offs st ;
 338   match fetch_stmt lbls_offs st with
 339     | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
 340       print_and_return_result (compute_result st, List.rev st.trace)
 341     | stmt ->
 342       let st' = interpret_stmt lbls_offs st stmt in
 343       iter_small_step debug lbls_offs st'
 344
 345
 346 let add_global_vars =
 347   List.fold_left
 348     (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
 349
 350 let add_fun_defs =
 351   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
 352
 353 let init_prog (st : state) (p : LTL.program) : state =
 354   let mem = add_global_vars (add_fun_defs st.mem p.LTL.functs) p.LTL.vars in
 355   change_mem st mem
 356
 357 let init_sp st =
 358   let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
 359   let sp =
 360     Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
 361   let st = change_mem st mem in
 362   (st, sp)
 363
 364 let init_isp st =
 365   let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
 366   let st = change_mem (change_isp st isp) mem in
 367   let (mem, exit) = Mem.alloc st.mem 1 in
 368   let st = change_exit st exit in
 369   let st = push st (List.nth exit 0) in
 370   let st = push st (List.nth exit 1) in
 371   st
 372
 373 let init_renv st sp =
 374   let f r st = add_reg r Val.undef st in
 375   let st = I8051.RegisterSet.fold f I8051.registers st in
 376   let spl = List.nth sp 0 in
 377   let sph = List.nth sp 1 in
 378   let st = add_reg I8051.spl spl st in
 379   let st = add_reg I8051.sph sph st in
 380   st
 381
 382 let init_main_call lbls_offs st main =
 383   let ptr = Mem.find_global st.mem main in
 384   match Mem.find_fun_def st.mem ptr with
 385     | LTL.F_int def ->
 386       init_fun_call lbls_offs st ptr def
 387     | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
 388
 389
 390 (* Before interpreting, the environment is initialized:
 391    - Build a bijection between the labels in the program and some values (taken
 392      amongst the offsets).
 393    - Add function definitions to the memory and reserve space for the globals.
 394    - Allocate memory to emulate the external stack and initialize the external
 395      stack pointer.
 396    - Allocate memory to emulate the internal stack and initialize the internal
 397      stack pointer.
 398    - Initialiaze the physical register environment. All are set to 0, except for
 399      the stack pointer registers that take the high and low bits of the external
 400      stack pointer.
 401    - Initialize a call to the main (set the current program counter to the
 402      beginning of the function).
 403    - Initialize the carry flag to 0. *)
 404
 405 let interpret debug p =
 406   Printf.printf "*** LTL interpret ***\n%!" ;
 407   match p.LTL.main with
 408     | None -> (IntValue.Int8.zero, [])
 409     | Some main ->
 410       let lbls_offs = labels_offsets p in
 411       let st = empty_state in
 412       let st = init_prog st p in
 413       let (st, sp) = init_sp st in
 414       let st = init_isp st in
 415       let st = init_renv st sp in
 416       let st = init_main_call lbls_offs st main in
 417       let st = change_carry st Val.zero in
 418       iter_small_step debug lbls_offs st