source: Deliverables/D2.3/8051/src/LTL/LTLInterpret.ml @ 453

Last change on this file since 453 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 13.1 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(* External RAM size *)
15let ext_ram_size = 1000
16(* Internal RAM size *)
17let int_ram_size = 100
18
19
20let change_offset v off =
21  if Val.is_pointer v then
22    let (b, _) = Val.to_pointer v in
23    Val.of_pointer (b, off)
24  else error ((Val.to_string v) ^ " is not a pointer.")
25
26
27(* Memory *)
28
29type memory = LTL.function_def Mem.memory
30
31(* Hardware registers environments. They associate a value to the each hardware
32   register. *)
33
34type hdw_reg_env = Val.t I8051.RegisterMap.t
35
36(* Execution states. *)
37
38type state =
39    { pc     : Val.t ;
40      isp    : Val.t ;
41      carry  : Val.t ;
42      renv   : hdw_reg_env ;
43      mem    : memory ;
44      trace  : AST.trace }
45
46
47(* Helpers *)
48
49let change_pc st pc = { st with pc = pc }
50let change_isp st isp = { st with isp = isp }
51let change_carry st carry = { st with carry = carry }
52let change_renv st renv = { st with renv = renv }
53let change_mem st mem = { st with mem = mem }
54let change_trace st trace = { st with trace = trace }
55
56let empty_state =
57  { pc     = Val.undef ;
58    isp    = Val.undef ;
59    carry  = Val.undef ;
60    renv   = I8051.RegisterMap.empty ;
61    mem    = Mem.empty ;
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 = 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." (Val.to_string st.pc) in
92  let error () = error msg in
93  if Val.is_pointer st.pc then
94    let (_, off) = Val.to_pointer 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 ()
99
100let entry_pc lbls_offs ptr def =
101  change_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  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 (change_offset st.pc off)
110
111let framesize st =
112  if Val.is_pointer 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.store2 st.mem chunk st.isp v in
127  let isp = Val.succ st.isp in
128  change_mem (change_isp st isp) mem
129
130let pop st =
131  let isp = Val.pred st.isp in
132  let st = change_isp st isp in
133  let v = Mem.load2 st.mem chunk st.isp in
134  (st, v)
135
136let save_ra lbls_offs st lbl =
137  let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
138  let vs = Val.break ra 2 in
139  let st = push st (List.nth vs 1) in
140  let st = push st (List.nth vs 0) 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.to_pointer ptr in
148  Labels_Offsets.find2 off lbls_offs
149
150let pointer_of_label lbls_offs ptr lbl =
151  let (b, _) = Val.to_pointer ptr in
152  let off = Labels_Offsets.find1 lbl lbls_offs in
153  Val.of_pointer (b, off)
154
155let return_pc st =
156  let (st, pch) = pop st in
157  let (st, pcl) = pop st in
158  Val.merge [pch ; pcl]
159
160
161(*
162let get_int () =
163  try Val.of_int (int_of_string (read_line ()))
164  with Failure "int_of_string" -> error "Failed to scan an integer."
165let get_float () =
166  try Val.of_float (float_of_string (read_line ()))
167  with Failure "float_of_string" -> error "Failed to scan a float."
168
169let interpret_external
170    (mem  : memory)
171    (def  : AST.external_function)
172    (args : Val.t list) :
173    memory * Val.t list =
174  match def.AST.ef_tag, args with
175    | s, _ when s = Primitive.scan_int ->
176      (mem, [get_int ()])
177    | "scan_float", _ ->
178      (mem, [get_float ()])
179    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
180      Printf.printf "%d" (Val.to_int v) ;
181      (mem, [Val.zero])
182    | "print_float", v :: _ when Val.is_float v ->
183      Printf.printf "%f" (Val.to_float v) ;
184      (mem, [Val.zero])
185    | "print_ptr", v :: _ when Val.is_pointer v ->
186      let (b, off) = Val.to_pointer v in
187      Printf.printf "block: %s, offset: %s"
188        (Val.Block.to_string b) (Val.Offset.to_string off) ;
189      (mem, [Val.zero])
190    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
191      Printf.printf "%d\n" (Val.to_int v) ;
192      (mem, [Val.zero])
193    | "print_floatln", v :: _ when Val.is_float v ->
194      Printf.printf "%f" (Val.to_float v) ;
195      (mem, [Val.zero])
196    | "print_ptrln", v :: _ when Val.is_pointer v ->
197      let (b, off) = Val.to_pointer v in
198      Printf.printf "block: %s, offset: %s\n"
199        (Val.Block.to_string b) (Val.Offset.to_string off) ;
200      (mem, [Val.zero])
201    | s, v :: _ when s = Primitive.alloc ->
202      let (mem, ptr) = Mem.alloc mem v in
203      let vs = Val.break ptr 2 in
204      (mem, vs)
205    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
206      (mem, [Val.modulo v1 v2])
207
208    (* The other cases are either a type error (only integers and pointers
209       may not be differenciated during type checking) or an unknown
210       function. *)
211    | "print_int", _ | "print_intln", _ ->
212      error "Illegal cast from pointer to integer."
213    | "print_ptr", _ | "print_ptrln", _ ->
214      error "Illegal cast from integer to pointer."
215    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
216*)
217
218
219let interpret_call lbls_offs st f ra =
220  let ptr = Mem.find_global st.mem f in
221  match Mem.find_fun_def st.mem ptr with
222    | LTL.F_int def ->
223(*
224      Printf.printf "Pushing return address in IRAM: %s = %s\n%!"
225        ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;
226*)
227      let st = save_ra lbls_offs st ra in
228      init_fun_call lbls_offs st ptr def
229    | LTL.F_ext def -> assert false (* TODO *)
230
231let interpret_return lbls_offs st =
232  let pc = return_pc st in
233(*
234  Printf.printf "Returning to %s = %s\n%!"
235    (Val.to_string pc) (label_of_pointer lbls_offs pc) ;
236*)
237  change_pc st pc
238
239
240(* Interpret statements. *)
241
242let interpret_stmt lbls_offs st stmt =
243  let next_pc = next_pc lbls_offs in
244  match stmt with
245
246    | LTL.St_skip lbl ->
247      next_pc st lbl
248
249    | LTL.St_comment (s, lbl) ->
250(*
251      Printf.printf "*** %s ***\n\n%!" s ;
252*)
253      next_pc st lbl
254
255    | LTL.St_cost (cost_lbl, lbl) ->
256      let st = change_trace st (cost_lbl :: st.trace) in
257      next_pc st lbl
258
259    | LTL.St_int (r, i, lbl) ->
260      let st = add_reg r (Val.of_int i) st in
261      next_pc st lbl
262
263    | LTL.St_pop lbl ->
264      let (st, v) = pop st in
265      let st = add_reg I8051.a v st in
266      next_pc st lbl
267
268    | LTL.St_push lbl ->
269      let v = get_reg I8051.a st in
270      let st = push st v in
271      next_pc st lbl
272
273    | LTL.St_addr (x, lbl) ->
274      let v = Mem.find_global st.mem x in
275      let vs = Val.break v 2 in
276      let st = add_reg I8051.dph (List.nth vs 0) st in
277      let st = add_reg I8051.dpl (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 v =
290        Eval.opaccs opaccs
291          (get_reg I8051.a st)
292          (get_reg I8051.b st) in
293      let st = add_reg I8051.a v st in
294      next_pc st lbl
295
296    | LTL.St_op1 (op1, lbl) ->
297      let v = Eval.op1 op1 (get_reg I8051.a st) in
298      let st = add_reg I8051.a v st in
299      next_pc st lbl
300
301    | LTL.St_op2 (op2, srcr, lbl) ->
302      let (v, carry) =
303        Eval.op2 st.carry op2
304          (get_reg I8051.a st)
305          (get_reg srcr st) in
306      let st = change_carry st carry in
307      let st = add_reg I8051.a v st in
308      next_pc st lbl
309
310    | LTL.St_clear_carry lbl ->
311      let st = change_carry st Val.zero in
312      next_pc st lbl
313
314    | LTL.St_load lbl ->
315      let addr =
316        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
317      let v = Mem.load2 st.mem chunk addr in
318      let st = add_reg I8051.a v st in
319      next_pc st lbl
320
321    | LTL.St_store lbl ->
322      let addr =
323        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
324      let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
325      let st = change_mem st mem in
326      next_pc st lbl
327
328    | LTL.St_call_id (f, lbl) ->
329      interpret_call lbls_offs st f 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 current_label lbls_offs st =
345  let (_, off) = Val.to_pointer st.pc in
346  Labels_Offsets.find2 off lbls_offs
347
348let print_renv renv =
349  let f r v =
350    if not (Val.eq v Val.undef) then
351    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
352  I8051.RegisterMap.iter f renv
353
354let print_state lbls_offs st =
355  Printf.printf "PC: %s (%s)\n%!"
356    (Val.to_string st.pc) (current_label lbls_offs st) ;
357  Printf.printf "SP: %s\n%!"
358    (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
359  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
360  print_renv st.renv ;
361  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
362  Mem.print st.mem ;
363  Printf.printf "\n%!"
364
365let rec iter_small_step lbls_offs st =
366(*
367    print_state lbls_offs st ;
368*)
369  match fetch_stmt lbls_offs st with
370    | LTL.St_return when Val.eq (return_pc st) Val.zero ->
371(*
372      print_state lbls_offs st ;
373*)
374      List.rev st.trace
375    | stmt ->
376      let st' = interpret_stmt lbls_offs st stmt in
377      iter_small_step lbls_offs st'
378
379
380let add_global_vars =
381  List.fold_left
382    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
383
384let add_fun_defs =
385  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
386
387let init_prog (st : state) (p : LTL.program) : state =
388  let mem = add_global_vars (add_fun_defs st.mem p.LTL.functs) p.LTL.vars in
389  change_mem st mem
390
391let init_renv st sp =
392  let f r st = add_reg r Val.undef st in
393  let st = I8051.RegisterSet.fold f I8051.registers st in
394  let vs = Val.break sp 2 in
395  let sph = List.nth vs 0 in
396  let spl = List.nth vs 1 in
397  let st = add_reg I8051.sph sph st in
398  let st = add_reg I8051.spl spl st in
399  st
400
401let init_sp st =
402  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
403  let (b, _) = Val.to_pointer sp in
404  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
405  let st = change_mem st mem in
406  (st, sp)
407
408let init_isp st =
409  let (mem, isp) = Mem.alloc st.mem int_ram_size in
410  let st = change_mem (change_isp st isp) mem in
411  let vs = Val.break Val.zero 2 in
412  let st = push st (List.nth vs 1) in
413  let st = push st (List.nth vs 0) in
414  st 
415
416let init_main_call lbls_offs st main =
417  let ptr = Mem.find_global st.mem main in
418  match Mem.find_fun_def st.mem ptr with
419    | LTL.F_int def ->
420      init_fun_call lbls_offs st ptr def
421    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
422
423
424(* Before interpreting, the environment is initialized:
425   - Build a bijection between the labels in the program and some values (taken
426     amongst the offsets).
427   - Add function definitions to the memory and reserve space for the globals.
428   - Allocate memory to emulate the external stack and initialize the external
429     stack pointer.
430   - Allocate memory to emulate the internal stack and initialize the internal
431     stack pointer.
432   - Initialiaze the physical register environment. All are set to 0, except for
433     the stack pointer registers that take the high and low bits of the external
434     stack pointer.
435   - Initialize a call to the main (set the current program counter to the
436     beginning of the function).
437   - Initialize the carry flag to 0. *)
438
439let interpret p = match p.LTL.main with
440  | None -> []
441  | Some main ->
442    let lbls_offs = labels_offsets p in
443    let st = empty_state in
444    let st = init_prog st p in
445    let (st, sp) = init_sp st in
446    let st = init_isp st in
447    let st = init_renv st sp in
448    let st = init_main_call lbls_offs st main in
449    let st = change_carry st Val.zero in
450    iter_small_step lbls_offs st
Note: See TracBrowser for help on using the repository browser.