source: Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml @ 1568

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