source: Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml @ 1345

Last change on this file since 1345 was 1345, checked in by tranquil, 8 years ago

work on ERTL and LTL completed

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