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

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

File size: 10.5 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 f =
169  let ptr = Mem.find_global st.mem f in
170  match Mem.find_fun_def st.mem ptr with
171    | LIN.F_int def ->
172      let st = save_ra st in
173      init_fun_call st ptr
174    | LIN.F_ext def ->
175      let st = next_pc st in
176      interpret_external_call st def.AST.ef_tag
177
178let interpret_return st =
179  let (st, pc) = return_pc st in
180  change_pc st pc
181
182let interpret_stmt st stmt =
183  match stmt with
184
185    | LIN.St_goto lbl ->
186      goto st lbl
187
188    | LIN.St_label _ ->
189      next_pc st
190
191    | LIN.St_comment s ->
192(*
193      Printf.printf "*** %s ***\n\n%!" s ;
194*)
195      next_pc st
196
197    | LIN.St_cost cost_lbl ->
198      let st = add_trace st cost_lbl in
199      next_pc st
200
201    | LIN.St_int (r, i) ->
202      let st = add_reg r (Val.of_int i) st in
203      next_pc st
204
205    | LIN.St_pop ->
206      let (st, v) = pop st in
207      let st = add_reg I8051.a v st in
208      next_pc st
209
210    | LIN.St_push ->
211      let v = get_reg I8051.a st in
212      let st = push st v in
213      next_pc st
214
215    | LIN.St_addr x ->
216      let vs = Mem.find_global st.mem x in
217      let st = add_reg I8051.dpl (List.nth vs 0) st in
218      let st = add_reg I8051.dph (List.nth vs 1) st in
219      next_pc st
220
221    | LIN.St_from_acc destr ->
222      let st = add_reg destr (get_reg I8051.a st) st in
223      next_pc st
224
225    | LIN.St_to_acc srcr ->
226      let st = add_reg I8051.a (get_reg srcr st) st in
227      next_pc st
228
229    | LIN.St_opaccs opaccs ->
230      let (a, b) =
231        Eval.opaccs opaccs
232          (get_reg I8051.a st)
233          (get_reg I8051.b st) in
234      let st = add_reg I8051.a a st in
235      let st = add_reg I8051.b b st in
236      next_pc st
237
238    | LIN.St_op1 op1 ->
239      let v = Eval.op1 op1 (get_reg I8051.a st) in
240      let st = add_reg I8051.a v st in
241      next_pc st
242
243    | LIN.St_op2 (op2, srcr) ->
244      let (v, carry) =
245        Eval.op2 st.carry op2
246          (get_reg I8051.a st)
247          (get_reg srcr st) in
248      let st = change_carry st carry in
249      let st = add_reg I8051.a v st in
250      next_pc st
251
252    | LIN.St_clear_carry ->
253      let st = change_carry st Val.zero in
254      next_pc st
255
256    | LIN.St_set_carry ->
257      let st = change_carry st (Val.of_int 1) in
258      next_pc st
259
260    | LIN.St_load ->
261      let addr = dptr st in
262      let v = Mem.load st.mem chunk addr in
263      let st = add_reg I8051.a v st in
264      next_pc st
265
266    | LIN.St_store ->
267      let addr = dptr st in
268      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
269      let st = change_mem st mem in
270      next_pc st
271
272    | LIN.St_call_id f ->
273      interpret_call st f
274
275    | LIN.St_condacc lbl_true ->
276      let v = get_reg I8051.a st in
277      if Val.is_true v then goto st lbl_true
278      else
279        if Val.is_false v then next_pc st
280        else error "Undecidable branchment."
281
282    | LIN.St_return ->
283      interpret_return st
284
285
286let compute_result st =
287  let vs = List.map (fun r -> get_reg r st) I8051.rets in
288  let f res v = res && (Val.is_int v) in
289  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
290  if is_int vs then
291    let chunks =
292      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
293    IntValue.Int32.merge chunks
294  else IntValue.Int32.zero
295
296let rec iter_small_step debug st =
297  let print_and_return_result (res, cost_labels) =
298    if debug then Printf.printf "Result = %s\n%!"
299      (IntValue.Int32.to_string res) ;
300    (res, cost_labels) in
301  if debug then print_state st ;
302  match fetch_stmt st with
303    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
304      print_and_return_result (compute_result st, List.rev st.trace)
305    | stmt ->
306      let st' = interpret_stmt st stmt in
307      iter_small_step debug st'
308
309
310let add_global_vars =
311  List.fold_left
312    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
313
314let add_fun_defs =
315  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
316
317let init_prog (st : state) (p : LIN.program) : state =
318  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
319  change_mem st mem
320
321let init_sp st =
322  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
323  let sp =
324    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
325  let st = change_mem st mem in
326  (st, sp)
327
328let init_isp st =
329  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
330  let st = change_mem (change_isp st isp) mem in
331  let (mem, exit) = Mem.alloc st.mem 1 in
332  let st = change_exit st exit in
333  let st = push st (List.nth exit 0) in
334  let st = push st (List.nth exit 1) in
335  st 
336
337let init_renv st sp =
338  let f r st = add_reg r Val.undef st in
339  let st = I8051.RegisterSet.fold f I8051.registers st in
340  let spl = List.nth sp 0 in
341  let sph = List.nth sp 1 in
342  let st = add_reg I8051.spl spl st in
343  let st = add_reg I8051.sph sph st in
344  st
345
346let init_main_call st main =
347  let ptr = Mem.find_global st.mem main in
348  match Mem.find_fun_def st.mem ptr with
349    | LIN.F_int def ->
350      init_fun_call st ptr
351    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
352
353
354(* Before interpreting, the environment is initialized:
355   - Add function definitions to the memory and reserve space for the globals.
356   - Allocate memory to emulate the external stack and initialize the external
357     stack pointer.
358   - Allocate memory to emulate the internal stack and initialize the internal
359     stack pointer.
360   - Initialiaze the physical register environment. All are set to 0, except for
361     the stack pointer registers that take the high and low bits of the external
362     stack pointer.
363   - Initialize a call to the main (set the current program counter to the
364     beginning of the function).
365   - Initialize the carry flag to 0. *)
366
367let interpret debug p =
368  Printf.printf "*** LIN interpret ***\n%!" ;
369  match p.LIN.main with
370    | None -> (IntValue.Int32.zero, [])
371    | Some main ->
372      let st = empty_state in
373      let st = init_prog st p in
374      let (st, sp) = init_sp st in
375      let st = init_isp st in
376      let st = init_renv st sp in
377      let st = init_main_call st main in
378      let st = change_carry st Val.zero in
379      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.