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

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