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

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

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 12.5 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      trace  : CostLabel.t list }
34
35
36(* Helpers *)
37
38let change_pc st pc = { st with pc = pc }
39let change_isp st isp = { st with isp = isp }
40let change_exit st exit = { st with exit = exit }
41let change_carry st carry = { st with carry = carry }
42let change_renv st renv = { st with renv = renv }
43let change_mem st mem = { st with mem = mem }
44let change_trace st trace = { st with trace = trace }
45let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
46
47let empty_state =
48  { pc     = Val.null ;
49    isp    = Val.null ;
50    exit   = Val.null ;
51    carry  = Val.undef ;
52    renv   = I8051.RegisterMap.empty ;
53    mem    = Mem.empty ;
54    trace  = [] }
55
56
57(* Each label of each function is associated a pointer. The base of this pointer
58   is the base of the function in memory. Inside a function, offsets are
59   bijectively associated to labels. *)
60
61module Labels_Offsets = Bijection.Make (Label) (Val.Offset)
62
63let labels_offsets_internal int_fun =
64  let f lbl _ (lbls_offs, i) =
65    (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in
66  Label.Map.fold f int_fun.LTL.f_graph
67
68(* [labels_offsets p] builds a bijection between the labels found in the
69   functions of [p] and some offsets. *)
70
71let labels_offsets p =
72  let f (lbls_offs, i) (_, def) = match def with
73    | LTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i)
74    | _ -> (lbls_offs, i) in
75  fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.LTL.functs)
76
77let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
78  | LTL.F_int def -> def
79  | _ -> error "Trying to fetch the definition of an external function."
80
81let fetch_stmt lbls_offs st =
82  let msg =
83    Printf.sprintf "%s does not point to a statement."
84      (Val.string_of_address st.pc) in
85  if Val.is_mem_address st.pc then
86    let off = Val.offset_of_address st.pc in
87    let def = fun_def_of_ptr st.mem st.pc in
88    let lbl = Labels_Offsets.find2 off lbls_offs in
89    Label.Map.find lbl def.LTL.f_graph
90  else error msg
91
92let entry_pc lbls_offs ptr def =
93  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
94
95let init_fun_call lbls_offs st ptr def =
96  let pc = entry_pc lbls_offs ptr def in
97  change_pc st pc
98
99let next_pc lbls_offs st lbl =
100  let off = Labels_Offsets.find1 lbl lbls_offs in
101  change_pc st (Val.change_address_offset st.pc off)
102
103let framesize st =
104  if Val.is_mem_address st.pc then
105    let def = fun_def_of_ptr st.mem st.pc in
106    def.LTL.f_stacksize
107  else error "Trying to load the stack size of an external function."
108
109let add_reg r v st =
110  let renv = I8051.RegisterMap.add r v st.renv in
111  change_renv st renv
112
113let get_reg r st =
114  if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
115  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
116
117let push st v =
118  let mem = Mem.store st.mem chunk st.isp v in
119  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
120  change_mem (change_isp st isp) mem
121
122let pop st =
123  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
124  let st = change_isp st isp in
125  let v = Mem.load st.mem chunk st.isp in
126  (st, v)
127
128let save_ra lbls_offs st lbl =
129  let ra =
130    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
131  let st = push st (List.nth ra 0) in
132  let st = push st (List.nth ra 1) in
133  st
134
135let label_of_pointer lbls_offs ptr =
136(*
137  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
138*)
139  let off = Val.offset_of_address ptr in
140  Labels_Offsets.find2 off lbls_offs
141
142let pointer_of_label lbls_offs ptr lbl =
143  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
144
145let return_pc st =
146  let (st, pch) = pop st in
147  let (st, pcl) = pop st in
148  (st, [pcl ; pch])
149
150let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
151
152
153(* State pretty-printing *)
154
155let current_label lbls_offs st =
156  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
157
158let print_renv renv =
159  let f r v =
160    if not (Val.eq v Val.undef) then
161    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
162  I8051.RegisterMap.iter f renv
163
164let print_state lbls_offs st =
165  Printf.printf "PC: %s (%s)\n%!"
166    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
167  Printf.printf "SP: %s\n%!"
168    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
169  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
170  print_renv st.renv ;
171  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
172  Mem.print st.mem ;
173  Printf.printf "\n%!"
174
175
176module InterpretExternal = Primitive.Interpret (Mem)
177
178let interpret_external mem f args = match InterpretExternal.t mem f args with
179  | (mem', InterpretExternal.V vs) -> (mem', vs)
180  | (mem', InterpretExternal.A addr) -> (mem', addr)
181
182let fetch_external_args f st =
183  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
184  let params = MiscPottier.prefix size I8051.parameters in
185  List.map (fun r -> get_reg r st) params
186
187let set_result st vs =
188  let f st (r, v) = add_reg r v st in
189  List.fold_left f st (MiscPottier.combine I8051.rets vs)
190
191let interpret_external_call st f next_pc =
192  let args = fetch_external_args f st in
193  let (mem, vs) = interpret_external st.mem f args in
194  let st = change_mem st mem in
195  let st = set_result st vs in
196  change_pc st next_pc
197
198let interpret_call lbls_offs st ptr ra =
199  match Mem.find_fun_def st.mem ptr with
200    | LTL.F_int def ->
201      let st = save_ra lbls_offs st ra in
202      init_fun_call lbls_offs st ptr def
203    | LTL.F_ext def ->
204      let next_pc = 
205        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
206      interpret_external_call st def.AST.ef_tag next_pc
207
208let interpret_return lbls_offs st =
209  let (st, pc) = return_pc st in
210  change_pc st pc
211
212
213(* Interpret statements. *)
214
215let interpret_stmt lbls_offs st stmt =
216  let next_pc = next_pc lbls_offs in
217  match stmt with
218
219    | LTL.St_skip lbl ->
220      next_pc st lbl
221
222    | LTL.St_comment (s, lbl) ->
223(*
224      Printf.printf "*** %s ***\n\n%!" s ;
225*)
226      next_pc st lbl
227
228    | LTL.St_cost (cost_lbl, lbl) ->
229      let st = add_trace st cost_lbl in
230      next_pc st lbl
231
232    | LTL.St_int (r, i, lbl) ->
233      let st = add_reg r (Val.of_int i) st in
234      next_pc st lbl
235
236    | LTL.St_pop lbl ->
237      let (st, v) = pop st in
238      let st = add_reg I8051.a v st in
239      next_pc st lbl
240
241    | LTL.St_push lbl ->
242      let v = get_reg I8051.a st in
243      let st = push st v in
244      next_pc st lbl
245
246    | LTL.St_addr (x, lbl) ->
247      let vs = Mem.find_global st.mem x in
248      let st = add_reg I8051.dpl (List.nth vs 0) st in
249      let st = add_reg I8051.dph (List.nth vs 1) st in
250      next_pc st lbl
251
252    | LTL.St_from_acc (destr, lbl) ->
253      let st = add_reg destr (get_reg (I8051.a) st) st in
254      next_pc st lbl
255
256    | LTL.St_to_acc (srcr, lbl) ->
257      let st = add_reg I8051.a (get_reg srcr st) st in
258      next_pc st lbl
259
260    | LTL.St_opaccs (opaccs, lbl) ->
261      let (a, b) =
262        Eval.opaccs opaccs
263          (get_reg I8051.a st)
264          (get_reg I8051.b st) in
265      let st = add_reg I8051.a a st in
266      let st = add_reg I8051.b b st in
267      next_pc st lbl
268
269    | LTL.St_op1 (op1, lbl) ->
270      let v = Eval.op1 op1 (get_reg I8051.a st) in
271      let st = add_reg I8051.a v st in
272      next_pc st lbl
273
274    | LTL.St_op2 (op2, srcr, lbl) ->
275      let (v, carry) =
276        Eval.op2 st.carry op2
277          (get_reg I8051.a st)
278          (get_reg srcr st) in
279      let st = change_carry st carry in
280      let st = add_reg I8051.a v st in
281      next_pc st lbl
282
283    | LTL.St_clear_carry lbl ->
284      let st = change_carry st Val.zero in
285      next_pc st lbl
286
287    | LTL.St_set_carry lbl ->
288      let st = change_carry st (Val.of_int 1) in
289      next_pc st lbl
290
291    | LTL.St_load lbl ->
292      let addr = dptr st in
293      let v = Mem.load st.mem chunk addr in
294      let st = add_reg I8051.a v st in
295      next_pc st lbl
296
297    | LTL.St_store lbl ->
298      let addr = dptr st in
299      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
300      let st = change_mem st mem in
301      next_pc st lbl
302
303    | LTL.St_call_id (f, lbl) ->
304      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
305
306    | LTL.St_call_ptr (f1, f2, lbl) ->
307      let addr = List.map (fun r -> get_reg r st) [f1 ; f2] in
308      interpret_call lbls_offs st addr lbl
309
310    | LTL.St_condacc (lbl_true, lbl_false) ->
311      let v = get_reg I8051.a st in
312      let lbl =
313        if Val.is_true v then lbl_true
314        else
315          if Val.is_false v then lbl_false
316          else error "Undecidable branchment." in
317      next_pc st lbl
318
319    | LTL.St_return ->
320      interpret_return lbls_offs st
321
322
323let compute_result st =
324  let vs = List.map (fun r -> get_reg r st) I8051.rets in
325  let f res v = res && (Val.is_int v) in
326  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
327  if is_int vs then
328    let chunks =
329      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
330    IntValue.Int32.merge chunks
331  else IntValue.Int32.zero
332
333let rec iter_small_step debug lbls_offs st =
334  let print_and_return_result (res, cost_labels) =
335    if debug then Printf.printf "Result = %s\n%!"
336      (IntValue.Int32.to_string res) ;
337    (res, cost_labels) in
338  if debug then print_state lbls_offs st ;
339  match fetch_stmt lbls_offs st with
340    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
341      print_and_return_result (compute_result st, List.rev st.trace)
342    | stmt ->
343      let st' = interpret_stmt lbls_offs st stmt in
344      iter_small_step debug lbls_offs st'
345
346
347let add_global_vars =
348  List.fold_left
349    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
350
351let add_fun_defs =
352  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
353
354let init_prog (st : state) (p : LTL.program) : state =
355  let mem = add_global_vars (add_fun_defs st.mem p.LTL.functs) p.LTL.vars in
356  change_mem st mem
357
358let init_sp st =
359  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
360  let sp =
361    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
362  let st = change_mem st mem in
363  (st, sp)
364
365let init_isp st =
366  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
367  let st = change_mem (change_isp st isp) mem in
368  let (mem, exit) = Mem.alloc st.mem 1 in
369  let st = change_exit st exit in
370  let st = push st (List.nth exit 0) in
371  let st = push st (List.nth exit 1) in
372  st 
373
374let init_renv st sp =
375  let f r st = add_reg r Val.undef st in
376  let st = I8051.RegisterSet.fold f I8051.registers st in
377  let spl = List.nth sp 0 in
378  let sph = List.nth sp 1 in
379  let st = add_reg I8051.spl spl st in
380  let st = add_reg I8051.sph sph st in
381  st
382
383let init_main_call lbls_offs st main =
384  let ptr = Mem.find_global st.mem main in
385  match Mem.find_fun_def st.mem ptr with
386    | LTL.F_int def ->
387      init_fun_call lbls_offs st ptr def
388    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
389
390
391(* Before interpreting, the environment is initialized:
392   - Build a bijection between the labels in the program and some values (taken
393     amongst the offsets).
394   - Add function definitions to the memory and reserve space for the globals.
395   - Allocate memory to emulate the external stack and initialize the external
396     stack pointer.
397   - Allocate memory to emulate the internal stack and initialize the internal
398     stack pointer.
399   - Initialiaze the physical register environment. All are set to 0, except for
400     the stack pointer registers that take the high and low bits of the external
401     stack pointer.
402   - Initialize a call to the main (set the current program counter to the
403     beginning of the function).
404   - Initialize the carry flag to 0. *)
405
406let interpret debug p =
407  Printf.printf "*** LTL interpret ***\n%!" ;
408  match p.LTL.main with
409    | None -> (IntValue.Int8.zero, [])
410    | Some main ->
411      let lbls_offs = labels_offsets p in
412      let st = empty_state in
413      let st = init_prog st p in
414      let (st, sp) = init_sp st in
415      let st = init_isp st in
416      let st = init_renv st sp in
417      let st = init_main_call lbls_offs st main in
418      let st = change_carry st Val.zero in
419      iter_small_step debug lbls_offs st
Note: See TracBrowser for help on using the repository browser.