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

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

Update of D2.2 from Paris.

File size: 13.7 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  : CostLabel.t list }
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 compute_result st =
374  let v = get_reg I8051.dpl st in
375  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
376  else IntValue.Int8.zero
377
378let rec iter_small_step print_result lbls_offs st =
379(*
380    print_state lbls_offs st ;
381*)
382  match fetch_stmt lbls_offs st with
383    | LTL.St_return when Val.eq (return_pc st) Val.zero ->
384      let (res, cost_labels) as trace =
385        (compute_result st, List.rev st.trace) in
386      if print_result then
387        Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
388      trace
389    | stmt ->
390      let st' = interpret_stmt lbls_offs st stmt in
391      iter_small_step print_result lbls_offs st'
392
393
394let add_global_vars =
395  List.fold_left
396    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
397
398let add_fun_defs =
399  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
400
401let init_prog (st : state) (p : LTL.program) : state =
402  let mem = add_global_vars (add_fun_defs st.mem p.LTL.functs) p.LTL.vars in
403  change_mem st mem
404
405let init_renv st sp =
406  let f r st = add_reg r Val.undef st in
407  let st = I8051.RegisterSet.fold f I8051.registers st in
408  let vs = Val.break sp 2 in
409  let sph = List.nth vs 0 in
410  let spl = List.nth vs 1 in
411  let st = add_reg I8051.sph sph st in
412  let st = add_reg I8051.spl spl st in
413  st
414
415let init_sp st =
416  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
417  let (b, _) = Val.to_pointer sp in
418  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
419  let st = change_mem st mem in
420  (st, sp)
421
422let init_isp st =
423  let (mem, isp) = Mem.alloc st.mem int_ram_size in
424  let st = change_mem (change_isp st isp) mem in
425  let vs = Val.break Val.zero 2 in
426  let st = push st (List.nth vs 1) in
427  let st = push st (List.nth vs 0) in
428  st 
429
430let init_main_call lbls_offs st main =
431  let ptr = Mem.find_global st.mem main in
432  match Mem.find_fun_def st.mem ptr with
433    | LTL.F_int def ->
434      init_fun_call lbls_offs st ptr def
435    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
436
437
438(* Before interpreting, the environment is initialized:
439   - Build a bijection between the labels in the program and some values (taken
440     amongst the offsets).
441   - Add function definitions to the memory and reserve space for the globals.
442   - Allocate memory to emulate the external stack and initialize the external
443     stack pointer.
444   - Allocate memory to emulate the internal stack and initialize the internal
445     stack pointer.
446   - Initialiaze the physical register environment. All are set to 0, except for
447     the stack pointer registers that take the high and low bits of the external
448     stack pointer.
449   - Initialize a call to the main (set the current program counter to the
450     beginning of the function).
451   - Initialize the carry flag to 0. *)
452
453let interpret print_result p = match p.LTL.main with
454  | None -> (IntValue.Int8.zero, [])
455  | Some main ->
456    let lbls_offs = labels_offsets p in
457    let st = empty_state in
458    let st = init_prog st p in
459    let (st, sp) = init_sp st in
460    let st = init_isp st in
461    let st = init_renv st sp in
462    let st = init_main_call lbls_offs st main in
463    let st = change_carry st Val.zero in
464    iter_small_step print_result lbls_offs st
Note: See TracBrowser for help on using the repository browser.