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

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