source: Deliverables/D2.2/8051/src/LIN/LINInterpret.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: 10.6 KB
Line 
1
2(** This module provides an interpreter for the LIN language. *)
3
4
5let error_prefix = "LIN interpret"
6let error s = Error.global_error error_prefix s
7
8
9module Mem = Driver.LINMemory
10module Val = Mem.Value
11let chunk = Driver.LINMemory.int_size
12module Eval = I8051.Eval (Val)
13
14
15(* Memory *)
16
17type memory = LIN.function_def Mem.memory
18
19(* Hardware registers environments. They associate a value to 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
57let int_fun_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
58  | LIN.F_int def -> def
59  | _ -> error "Trying to fetch the definition of an external function."
60
61let current_int_fun st = int_fun_of_ptr st.mem st.pc
62
63let fetch_stmt st =
64  let msg =
65    Printf.sprintf "%s does not point to a statement."
66      (Val.string_of_address st.pc) in
67  if Val.is_mem_address st.pc then
68    let off = Val.offset_of_address st.pc in
69    let def = int_fun_of_ptr st.mem st.pc in
70    List.nth def (Val.Offset.to_int off)
71  else error msg
72
73let init_fun_call st ptr =
74  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
75
76let next_pc st =
77  change_pc st (Val.add_address st.pc Val.Offset.one)
78
79let add_reg r v st =
80  let renv = I8051.RegisterMap.add r v st.renv in
81  change_renv st renv
82
83let get_reg r st =
84  if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
85  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
86
87let push st v =
88  let mem = Mem.store st.mem chunk st.isp v in
89  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
90  change_mem (change_isp st isp) mem
91
92let pop st =
93  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
94  let st = change_isp st isp in
95  let v = Mem.load st.mem chunk st.isp in
96  (st, v)
97
98let save_ra st =
99  let ra = Val.add_address st.pc Val.Offset.one in
100  let st = push st (List.nth ra 0) in
101  let st = push st (List.nth ra 1) in
102  st
103
104let find_label lbl =
105  let rec aux i = function
106  | [] -> error (Printf.sprintf "Unknown label %s." lbl)
107  | LIN.St_label lbl' :: _ when lbl' = lbl -> i
108  | _ :: code -> aux (i+1) code
109  in
110  aux 0
111
112let pointer_of_label st lbl =
113  let code = current_int_fun st in
114  let off = find_label lbl code in
115  Val.change_address_offset st.pc (Val.Offset.of_int off)
116
117let goto st lbl =
118  change_pc st (pointer_of_label st lbl)
119
120let return_pc st =
121  let (st, pch) = pop st in
122  let (st, pcl) = pop st in
123  (st, [pcl ; pch])
124
125let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
126
127
128(* State pretty-printing *)
129
130let print_renv renv =
131  let f r v =
132    if not (Val.eq v Val.undef) then
133    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
134  I8051.RegisterMap.iter f renv
135
136let print_state st =
137  Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
138  Printf.printf "SP: %s\n%!"
139    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
140  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
141  print_renv st.renv ;
142  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
143  Mem.print st.mem ;
144  Printf.printf "\n%!"
145
146
147module InterpretExternal = Primitive.Interpret (Mem)
148
149let interpret_external mem f args = match InterpretExternal.t mem f args with
150  | (mem', InterpretExternal.V vs) -> (mem', vs)
151  | (mem', InterpretExternal.A addr) -> (mem', addr)
152
153let fetch_external_args f st =
154  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
155  let params = MiscPottier.prefix size I8051.parameters in
156  List.map (fun r -> get_reg r st) params
157
158let set_result st vs =
159  let f st (r, v) = add_reg r v st in
160  List.fold_left f st (MiscPottier.combine I8051.rets vs)
161
162let interpret_external_call st f =
163  let args = fetch_external_args f st in
164  let (mem, vs) = interpret_external st.mem f args in
165  let st = change_mem st mem in
166  set_result st vs
167
168let interpret_call st ptr =
169  match Mem.find_fun_def st.mem ptr with
170    | LIN.F_int def ->
171      let st = save_ra st in
172      init_fun_call st ptr
173    | LIN.F_ext def ->
174      let st = next_pc st in
175      interpret_external_call st def.AST.ef_tag
176
177let interpret_return st =
178  let (st, pc) = return_pc st in
179  change_pc st pc
180
181let interpret_stmt st stmt =
182  match stmt with
183
184    | LIN.St_goto lbl ->
185      goto st lbl
186
187    | LIN.St_label _ ->
188      next_pc st
189
190    | LIN.St_comment s ->
191(*
192      Printf.printf "*** %s ***\n\n%!" s ;
193*)
194      next_pc st
195
196    | LIN.St_cost cost_lbl ->
197      let st = add_trace st cost_lbl in
198      next_pc st
199
200    | LIN.St_int (r, i) ->
201      let st = add_reg r (Val.of_int i) st in
202      next_pc st
203
204    | LIN.St_pop ->
205      let (st, v) = pop st in
206      let st = add_reg I8051.a v st in
207      next_pc st
208
209    | LIN.St_push ->
210      let v = get_reg I8051.a st in
211      let st = push st v in
212      next_pc st
213
214    | LIN.St_addr x ->
215      let vs = Mem.find_global st.mem x in
216      let st = add_reg I8051.dpl (List.nth vs 0) st in
217      let st = add_reg I8051.dph (List.nth vs 1) st in
218      next_pc st
219
220    | LIN.St_from_acc destr ->
221      let st = add_reg destr (get_reg I8051.a st) st in
222      next_pc st
223
224    | LIN.St_to_acc srcr ->
225      let st = add_reg I8051.a (get_reg srcr st) st in
226      next_pc st
227
228    | LIN.St_opaccs opaccs ->
229      let (a, b) =
230        Eval.opaccs opaccs
231          (get_reg I8051.a st)
232          (get_reg I8051.b st) in
233      let st = add_reg I8051.a a st in
234      let st = add_reg I8051.b b st in
235      next_pc st
236
237    | LIN.St_op1 op1 ->
238      let v = Eval.op1 op1 (get_reg I8051.a st) in
239      let st = add_reg I8051.a v st in
240      next_pc st
241
242    | LIN.St_op2 (op2, srcr) ->
243      let (v, carry) =
244        Eval.op2 st.carry op2
245          (get_reg I8051.a st)
246          (get_reg srcr st) in
247      let st = change_carry st carry in
248      let st = add_reg I8051.a v st in
249      next_pc st
250
251    | LIN.St_clear_carry ->
252      let st = change_carry st Val.zero in
253      next_pc st
254
255    | LIN.St_set_carry ->
256      let st = change_carry st (Val.of_int 1) in
257      next_pc st
258
259    | LIN.St_load ->
260      let addr = dptr st in
261      let v = Mem.load st.mem chunk addr in
262      let st = add_reg I8051.a v st in
263      next_pc st
264
265    | LIN.St_store ->
266      let addr = dptr st in
267      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
268      let st = change_mem st mem in
269      next_pc st
270
271    | LIN.St_call_id f ->
272      interpret_call st (Mem.find_global st.mem f)
273
274    | LIN.St_call_ptr (f1, f2) ->
275      let addr = List.map (fun r -> get_reg r st) [f1 ; f2] in
276      interpret_call st addr
277
278    | LIN.St_condacc lbl_true ->
279      let v = get_reg I8051.a st in
280      if Val.is_true v then goto st lbl_true
281      else
282        if Val.is_false v then next_pc st
283        else error "Undecidable branchment."
284
285    | LIN.St_return ->
286      interpret_return st
287
288
289let compute_result st =
290  let vs = List.map (fun r -> get_reg r st) I8051.rets in
291  let f res v = res && (Val.is_int v) in
292  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
293  if is_int vs then
294    let chunks =
295      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
296    IntValue.Int32.merge chunks
297  else IntValue.Int32.zero
298
299let rec iter_small_step debug st =
300  let print_and_return_result (res, cost_labels) =
301    if debug then Printf.printf "Result = %s\n%!"
302      (IntValue.Int32.to_string res) ;
303    (res, cost_labels) in
304  if debug then print_state st ;
305  match fetch_stmt st with
306    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
307      print_and_return_result (compute_result st, List.rev st.trace)
308    | stmt ->
309      let st' = interpret_stmt st stmt in
310      iter_small_step debug st'
311
312
313let add_global_vars =
314  List.fold_left
315    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
316
317let add_fun_defs =
318  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
319
320let init_prog (st : state) (p : LIN.program) : state =
321  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
322  change_mem st mem
323
324let init_sp st =
325  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
326  let sp =
327    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
328  let st = change_mem st mem in
329  (st, sp)
330
331let init_isp st =
332  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
333  let st = change_mem (change_isp st isp) mem in
334  let (mem, exit) = Mem.alloc st.mem 1 in
335  let st = change_exit st exit in
336  let st = push st (List.nth exit 0) in
337  let st = push st (List.nth exit 1) in
338  st 
339
340let init_renv st sp =
341  let f r st = add_reg r Val.undef st in
342  let st = I8051.RegisterSet.fold f I8051.registers st in
343  let spl = List.nth sp 0 in
344  let sph = List.nth sp 1 in
345  let st = add_reg I8051.spl spl st in
346  let st = add_reg I8051.sph sph st in
347  st
348
349let init_main_call st main =
350  let ptr = Mem.find_global st.mem main in
351  match Mem.find_fun_def st.mem ptr with
352    | LIN.F_int def ->
353      init_fun_call st ptr
354    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
355
356
357(* Before interpreting, the environment is initialized:
358   - Add function definitions to the memory and reserve space for the globals.
359   - Allocate memory to emulate the external stack and initialize the external
360     stack pointer.
361   - Allocate memory to emulate the internal stack and initialize the internal
362     stack pointer.
363   - Initialiaze the physical register environment. All are set to 0, except for
364     the stack pointer registers that take the high and low bits of the external
365     stack pointer.
366   - Initialize a call to the main (set the current program counter to the
367     beginning of the function).
368   - Initialize the carry flag to 0. *)
369
370let interpret debug p =
371  Printf.printf "*** LIN interpret ***\n%!" ;
372  match p.LIN.main with
373    | None -> (IntValue.Int32.zero, [])
374    | Some main ->
375      let st = empty_state in
376      let st = init_prog st p in
377      let (st, sp) = init_sp st in
378      let st = init_isp st in
379      let st = init_renv st sp in
380      let st = init_main_call st main in
381      let st = change_carry st Val.zero in
382      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.