source: Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.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: 15.7 KB
Line 
1
2(** This module provides an interpreter for the ERTL language. *)
3
4
5let error_prefix = "ERTL interpret"
6let error s = Error.global_error error_prefix s
7
8
9module Mem = Driver.ERTLMemory
10module Val = Mem.Value
11let chunk = Driver.ERTLMemory.int_size
12module Eval = I8051.Eval (Val)
13
14
15(* Memory *)
16
17type memory = ERTL.function_def Mem.memory
18
19(* Local environments. They associate a value to the pseudo-registers of the
20   function being executed. *)
21
22type local_env = Val.t Register.Map.t
23
24(* Hardware registers environments. They associate a value to each hardware
25   register. *)
26
27type hdw_reg_env = Val.t I8051.RegisterMap.t
28
29(* Call frames. The execution state has a call stack, each element of the stack
30   being composed of the local environment to resume the execution of the
31   caller. *)
32
33type stack_frame = local_env
34
35(* Execution states. *)
36
37type state =
38    { st_frs : stack_frame list ;
39      pc     : Val.address ;
40      isp    : Val.address ;
41      exit   : Val.address ;
42      lenv   : local_env ;
43      carry  : Val.t ;
44      renv   : hdw_reg_env ;
45      mem    : memory ;
46      trace  : CostLabel.t list }
47
48
49(* Helpers *)
50
51let add_st_frs st frame = { st with st_frs = frame :: st.st_frs }
52let pop_st_frs st = match st.st_frs with
53  | [] -> error "Empty stack frames."
54  | lenv :: st_frs -> { st with st_frs = st_frs ; lenv = lenv }
55let change_pc st pc = { st with pc = pc }
56let change_isp st isp = { st with isp = isp }
57let change_exit st exit = { st with exit = exit }
58let change_lenv st lenv = { st with lenv = lenv }
59let change_carry st carry = { st with carry = carry }
60let change_renv st renv = { st with renv = renv }
61let change_mem st mem = { st with mem = mem }
62let change_trace st trace = { st with trace = trace }
63let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
64
65let empty_state =
66  { st_frs = [] ;
67    pc     = Val.null ;
68    isp    = Val.null ;
69    exit   = Val.null ;
70    lenv   = Register.Map.empty ;
71    carry  = Val.undef ;
72    renv   = I8051.RegisterMap.empty ;
73    mem    = Mem.empty ;
74    trace  = [] }
75
76
77(* Each label of each function is associated an address. The base of this
78   address is the base of the function in memory. Inside a function, offsets are
79   bijectively associated to labels. *)
80
81module Labels_Offsets = Bijection.Make (Label) (Val.Offset)
82
83let labels_offsets_internal int_fun =
84  let f lbl _ (lbls_offs, i) =
85    (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in
86  Label.Map.fold f int_fun.ERTL.f_graph
87
88(* [labels_offsets p] builds a bijection between the labels found in the
89   functions of [p] and some memory addresses. *)
90
91let labels_offsets p =
92  let f (lbls_offs, i) (_, def) = match def with
93    | ERTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i)
94    | _ -> (lbls_offs, i) in
95  fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.ERTL.functs)
96
97let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
98  | ERTL.F_int def -> def
99  | _ -> error "Trying to fetch the definition of an external function."
100
101let fetch_stmt lbls_offs st =
102  let msg =
103    Printf.sprintf "%s does not point to a statement."
104      (Val.string_of_address st.pc) in
105  if Val.is_mem_address st.pc then
106    let off = Val.offset_of_address st.pc in
107    let def = fun_def_of_ptr st.mem st.pc in
108    let lbl = Labels_Offsets.find2 off lbls_offs in
109    Label.Map.find lbl def.ERTL.f_graph
110  else error msg
111
112let entry_pc lbls_offs ptr def =
113  let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in
114  Val.change_address_offset ptr off
115
116let init_fun_call lbls_offs st ptr def =
117  let f r lenv = Register.Map.add r Val.undef lenv in
118  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
119  let pc = entry_pc lbls_offs ptr def in
120  change_lenv (change_pc st pc) lenv
121
122let next_pc lbls_offs st lbl =
123  let off = Labels_Offsets.find1 lbl lbls_offs in
124  change_pc st (Val.change_address_offset st.pc off)
125
126let framesize st =
127  if Val.is_mem_address st.pc then
128    let def = fun_def_of_ptr st.mem st.pc in
129    def.ERTL.f_stacksize
130  else error "No function at the given address."
131
132type register = Hdw of I8051.register | Psd of Register.t
133
134let add_reg r v st = match r with
135  | Hdw r ->
136    let renv = I8051.RegisterMap.add r v st.renv in
137    change_renv st renv
138  | Psd r ->
139    let lenv = Register.Map.add r v st.lenv in
140    change_lenv st lenv
141
142let get_reg r st = match r with
143  | Hdw r ->
144    if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
145    else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
146  | Psd r ->
147    if Register.Map.mem r st.lenv then Register.Map.find r st.lenv
148    else error ("Unknown local register " ^ (Register.print r) ^ ".")
149
150let push st v =
151  let mem = Mem.store st.mem chunk st.isp v in
152  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
153  change_mem (change_isp st isp) mem
154
155let pop st =
156  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
157  let st = change_isp st isp in
158  let v = Mem.load st.mem chunk st.isp in
159  (st, v)
160
161let get_ra st =
162  let (st, pch) = pop st in
163  let (st, pcl) = pop st in
164  [pcl ; pch]
165
166let save_ra lbls_offs st lbl =
167  let ra =
168    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
169  let st = push st (List.nth ra 0) in
170  let st = push st (List.nth ra 1) in
171  st
172
173let save_frame st = add_st_frs st st.lenv
174
175let label_of_pointer lbls_offs ptr =
176(*
177  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
178*)
179  let off = Val.offset_of_address ptr in
180  Labels_Offsets.find2 off lbls_offs
181
182let pointer_of_label lbls_offs ptr lbl =
183  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
184
185let get_sp st =
186  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
187
188let set_sp vs st =
189  let spl = List.nth vs 0 in
190  let sph = List.nth vs 1 in
191  let st = add_reg (Hdw I8051.spl) spl st in
192  let st = add_reg (Hdw I8051.sph) sph st in
193  st
194
195let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
196
197
198module InterpretExternal = Primitive.Interpret (Mem)
199
200let interpret_external mem f args = match InterpretExternal.t mem f args with
201  | (mem', InterpretExternal.V vs) -> (mem', vs)
202  | (mem', InterpretExternal.A addr) -> (mem', addr)
203
204let fetch_external_args f st =
205  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
206  let params = MiscPottier.prefix size I8051.parameters in
207  List.map (fun r -> get_reg (Hdw r) st) params
208
209let set_result st vs =
210  let f st (r, v) = add_reg (Hdw r) v st in
211  List.fold_left f st (MiscPottier.combine I8051.rets vs)
212
213let interpret_external_call st f next_pc =
214  let args = fetch_external_args f st in
215  let (mem, vs) = interpret_external st.mem f args in
216  let st = change_mem st mem in
217  let st = set_result st vs in
218  change_pc st next_pc
219
220let interpret_call lbls_offs st ptr ra =
221  (* let ptr = Mem.find_global st.mem f in *)
222  match Mem.find_fun_def st.mem ptr with
223    | ERTL.F_int def ->
224      let st = save_ra lbls_offs st ra in
225      let st = save_frame st in
226      init_fun_call lbls_offs st ptr def
227    | ERTL.F_ext def ->
228      let next_pc = 
229        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
230      interpret_external_call st def.AST.ef_tag next_pc
231
232let interpret_return lbls_offs st =
233  let st = pop_st_frs st in
234  let (st, pch) = pop st in
235  let (st, pcl) = pop st in
236  let pc = [pcl ; pch] in
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    | ERTL.St_skip lbl ->
247      next_pc st lbl
248
249    | ERTL.St_comment (s, lbl) ->
250(*
251      Printf.printf "*** %s ***\n\n%!" s ;
252*)
253      next_pc st lbl
254
255    | ERTL.St_cost (cost_lbl, lbl) ->
256      let st = add_trace st cost_lbl in
257      next_pc st lbl
258
259    | ERTL.St_get_hdw (destr, srcr, lbl) ->
260      let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in
261      next_pc st lbl
262
263    | ERTL.St_set_hdw (destr, srcr, lbl) ->
264      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
265      next_pc st lbl
266
267    | ERTL.St_hdw_to_hdw (destr, srcr, lbl) ->
268      let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in
269      next_pc st lbl
270
271    | ERTL.St_newframe lbl ->
272      let size = framesize st in
273      let sp = get_sp st in
274      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
275      let st = set_sp new_sp st in
276      next_pc st lbl
277
278    | ERTL.St_delframe lbl ->
279      let size = framesize st in
280      let sp = get_sp st in
281      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
282      let st = set_sp new_sp st in
283      next_pc st lbl
284
285    | ERTL.St_framesize (destr, lbl) ->
286      let size = framesize st in
287      let st = add_reg (Psd destr) (Val.of_int size) st in
288      next_pc st lbl
289
290    | ERTL.St_pop (destr, lbl) ->
291      let (st, v) = pop st in
292      let st = add_reg (Psd destr) v st in
293      next_pc st lbl
294
295    | ERTL.St_push (srcr, lbl) ->
296      let v = get_reg (Psd srcr) st in
297      let st = push st v in
298      next_pc st lbl
299
300    | ERTL.St_addrH (r, x, lbl) ->
301      let vs = Mem.find_global st.mem x in
302      let st = add_reg (Psd r) (List.nth vs 1) st in
303      next_pc st lbl
304
305    | ERTL.St_addrL (r, x, lbl) ->
306      let vs = Mem.find_global st.mem x in
307      let st = add_reg (Psd r) (List.nth vs 0) st in
308      next_pc st lbl
309
310    | ERTL.St_int (r, i, lbl) ->
311      let st = add_reg (Psd r) (Val.of_int i) st in
312      next_pc st lbl
313
314    | ERTL.St_move (destr, srcr, lbl) ->
315      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
316      next_pc st lbl
317
318    | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) ->
319      let (v, _) =
320        Eval.opaccs opaccs
321          (get_reg (Psd srcr1) st)
322          (get_reg (Psd srcr2) st) in
323      let st = add_reg (Psd destr) v st in
324      next_pc st lbl
325
326    | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
327      let (_, v) =
328        Eval.opaccs opaccs
329          (get_reg (Psd srcr1) st)
330          (get_reg (Psd srcr2) st) in
331      let st = add_reg (Psd destr) v st in
332      next_pc st lbl
333
334    | ERTL.St_op1 (op1, destr, srcr, lbl) ->
335      let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
336      let st = add_reg (Psd destr) v st in
337      next_pc st lbl
338
339    | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
340      let (v, carry) =
341        Eval.op2 st.carry op2
342          (get_reg (Psd srcr1) st)
343          (get_reg (Psd srcr2) st) in
344      let st = change_carry st carry in
345      let st = add_reg (Psd destr) v st in
346      next_pc st lbl
347
348    | ERTL.St_clear_carry lbl ->
349      let st = change_carry st Val.zero in
350      next_pc st lbl
351
352    | ERTL.St_set_carry lbl ->
353      let st = change_carry st (Val.of_int 1) in
354      next_pc st lbl
355
356    | ERTL.St_load (destr, addr1, addr2, lbl) ->
357      let addr = make_addr st addr1 addr2 in
358      let v = Mem.load st.mem chunk addr in
359      let st = add_reg (Psd destr) v st in
360      next_pc st lbl
361
362    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
363      let addr = make_addr st addr1 addr2 in
364      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
365      let st = change_mem st mem in
366      next_pc st lbl
367
368    | ERTL.St_call_id (f, _, lbl) ->
369      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
370
371    | ERTL.St_call_ptr (f1, f2, _, lbl) ->
372      interpret_call lbls_offs st (make_addr st f1 f2) lbl
373
374    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
375      let v = get_reg (Psd srcr) st in
376      let lbl =
377        if Val.is_true v then lbl_true
378        else
379          if Val.is_false v then lbl_false
380          else error "Undecidable branchment." in
381      next_pc st lbl
382
383    | ERTL.St_return _ ->
384      interpret_return lbls_offs st
385
386
387let print_lenv lenv =
388  let f r v =
389    if not (Val.eq v Val.undef) then
390      Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
391  Register.Map.iter f lenv
392
393let print_renv renv =
394  let f r v =
395    if not (Val.eq v Val.undef) then
396    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
397  I8051.RegisterMap.iter f renv
398
399let current_label lbls_offs st =
400  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
401
402let print_state lbls_offs st =
403  Printf.printf "PC: %s (%s)\n%!"
404    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
405  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
406  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
407  Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
408  print_lenv st.lenv ;
409  print_renv st.renv ;
410  Mem.print st.mem ;
411  Printf.printf "\n%!"
412
413let compute_result st ret_regs =
414  let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
415  let f res v = res && (Val.is_int v) in
416  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
417  if is_int vs then
418    let chunks =
419      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
420    IntValue.Int32.merge chunks
421  else IntValue.Int32.zero
422
423let rec iter_small_step debug lbls_offs st =
424  let print_and_return_result (res, cost_labels) =
425    if debug then Printf.printf "Result = %s\n%!"
426      (IntValue.Int32.to_string res) ;
427    (res, cost_labels) in
428  if debug then print_state lbls_offs st ;
429  match fetch_stmt lbls_offs st with
430    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
431      print_and_return_result (compute_result st ret_regs, List.rev st.trace)
432    | stmt ->
433      let st' = interpret_stmt lbls_offs st stmt in
434      iter_small_step debug lbls_offs st'
435
436
437let add_global_vars =
438  List.fold_left
439    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
440
441let add_fun_defs =
442  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
443
444let init_prog (st : state) (p : ERTL.program) : state =
445  let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
446  change_mem st mem
447
448let init_sp st =
449  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
450  let sp =
451    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
452  let st = change_mem st mem in
453  (st, sp)
454
455let init_isp st =
456  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
457  let st = change_mem (change_isp st isp) mem in
458  let (mem, exit) = Mem.alloc st.mem 1 in
459  let st = change_exit st exit in
460  let st = push st (List.nth exit 0) in
461  let st = push st (List.nth exit 1) in
462  st 
463
464let init_renv st sp =
465  let f r renv = I8051.RegisterMap.add r Val.undef renv in
466  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
467  let spl = List.nth sp 0 in
468  let sph = List.nth sp 1 in
469  let renv = I8051.RegisterMap.add I8051.sph sph renv in
470  let renv = I8051.RegisterMap.add I8051.spl spl renv in
471  change_renv st renv
472
473let init_main_call lbls_offs st main =
474  let ptr = Mem.find_global st.mem main in
475  match Mem.find_fun_def st.mem ptr with
476    | ERTL.F_int def ->
477      init_fun_call lbls_offs st ptr def
478    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
479
480
481(* Before interpreting, the environment is initialized:
482   - Build a bijection between the labels in the program and some values (taken
483     amongst the offsets).
484   - Add function definitions to the memory and reserve space for the globals.
485   - Allocate memory to emulate the external stack and initialize the external
486     stack pointer.
487   - Allocate memory to emulate the internal stack and initialize the internal
488     stack pointer.
489   - Initialiaze the physical register environment. All are set to 0, except for
490     the stack pointer registers that take the high and low bits of the external
491     stack pointer.
492   - Initialize a call to the main (set the current program counter to the
493     beginning of the function).
494   - Initialize the carry flag to 0. *)
495
496let interpret debug p =
497  Printf.printf "*** ERTL interpret ***\n%!" ;
498  match p.ERTL.main with
499    | None -> (IntValue.Int32.zero, [])
500    | Some main ->
501      let lbls_offs = labels_offsets p in
502      let st = empty_state in
503      let st = init_prog st p in
504      let (st, sp) = init_sp st in
505      let st = init_isp st in
506      let st = init_renv st sp in
507      let st = init_main_call lbls_offs st main in
508      let st = change_carry st Val.zero in
509      iter_small_step debug lbls_offs st
Note: See TracBrowser for help on using the repository browser.