source: Deliverables/D2.2/8051/src/LIN/LINInterpret.ml @ 1568

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