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

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