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

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

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