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

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

fighting with a bug of the translation from RTL to ERTL

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