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

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

Deliverable D2.2

File size: 11.4 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(* External RAM size *)
15let ext_ram_size = 1000
16(* Internal RAM size *)
17let int_ram_size = 100
18
19
20let change_offset v off =
21  if Val.is_pointer v then
22    let (b, _) = Val.to_pointer v in
23    Val.of_pointer (b, off)
24  else error ((Val.to_string v) ^ " is not a pointer.")
25
26
27(* Memory *)
28
29type memory = LIN.function_def Mem.memory
30
31(* Hardware registers environments. They associate a value to the each hardware
32   register. *)
33
34type hdw_reg_env = Val.t I8051.RegisterMap.t
35
36(* Execution states. *)
37
38type state =
39    { pc     : Val.t ;
40      isp    : Val.t ;
41      carry  : Val.t ;
42      renv   : hdw_reg_env ;
43      mem    : memory ;
44      trace  : AST.trace }
45
46
47(* Helpers *)
48
49let change_pc st pc = { st with pc = pc }
50let change_isp st isp = { st with isp = isp }
51let change_carry st carry = { st with carry = carry }
52let change_renv st renv = { st with renv = renv }
53let change_mem st mem = { st with mem = mem }
54let change_trace st trace = { st with trace = trace }
55
56let empty_state =
57  { pc     = Val.undef ;
58    isp    = Val.undef ;
59    carry  = Val.undef ;
60    renv   = I8051.RegisterMap.empty ;
61    mem    = Mem.empty ;
62    trace  = [] }
63
64
65let int_fun_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
66  | LIN.F_int def -> def
67  | _ -> error "Trying to fetch the definition of an external function."
68
69let current_int_fun st = int_fun_of_ptr st.mem st.pc
70
71let fetch_stmt st =
72  let msg =
73    Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
74  let error () = error msg in
75  if Val.is_pointer st.pc then
76    let (_, off) = Val.to_pointer st.pc in
77    let def = int_fun_of_ptr st.mem st.pc in
78    List.nth def (Val.Offset.to_int off)
79  else error ()
80
81let init_fun_call st ptr =
82  change_pc st (change_offset ptr Val.Offset.zero)
83
84let next_pc st =
85  change_pc st (Val.succ st.pc)
86
87let add_reg r v st =
88  let renv = I8051.RegisterMap.add r v st.renv in
89  change_renv st renv
90
91let get_reg r st =
92  if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
93  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
94
95let push st v =
96  let mem = Mem.store2 st.mem chunk st.isp v in
97  let isp = Val.succ st.isp in
98  change_mem (change_isp st isp) mem
99
100let pop st =
101  let isp = Val.pred st.isp in
102  let st = change_isp st isp in
103  let v = Mem.load2 st.mem chunk st.isp in
104  (st, v)
105
106let save_ra st =
107  let ra = Val.succ st.pc in
108  let vs = Val.break ra 2 in
109  let st = push st (List.nth vs 1) in
110  let st = push st (List.nth vs 0) in
111  st
112
113let find_label lbl =
114  let rec aux i = function
115  | [] -> error (Printf.sprintf "Unknown label %s." lbl)
116  | LIN.St_label lbl' :: _ when lbl' = lbl -> i
117  | _ :: code -> aux (i+1) code
118  in
119  aux 0
120
121let pointer_of_label st lbl =
122  let code = current_int_fun st in
123  let off = find_label lbl code in
124  change_offset st.pc (Val.Offset.of_int off)
125
126let goto st lbl =
127  change_pc st (pointer_of_label st lbl)
128
129let return_pc st =
130  let (st, pch) = pop st in
131  let (st, pcl) = pop st in
132  Val.merge [pch ; pcl]
133
134
135(*
136let get_int () =
137  try Val.of_int (int_of_string (read_line ()))
138  with Failure "int_of_string" -> error "Failed to scan an integer."
139let get_float () =
140  try Val.of_float (float_of_string (read_line ()))
141  with Failure "float_of_string" -> error "Failed to scan a float."
142
143let interpret_external
144    (mem  : memory)
145    (def  : AST.external_function)
146    (args : Val.t list) :
147    memory * Val.t list =
148  match def.AST.ef_tag, args with
149    | s, _ when s = Primitive.scan_int ->
150      (mem, [get_int ()])
151    | "scan_float", _ ->
152      (mem, [get_float ()])
153    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
154      Printf.printf "%d" (Val.to_int v) ;
155      (mem, [Val.zero])
156    | "print_float", v :: _ when Val.is_float v ->
157      Printf.printf "%f" (Val.to_float v) ;
158      (mem, [Val.zero])
159    | "print_ptr", v :: _ when Val.is_pointer v ->
160      let (b, off) = Val.to_pointer v in
161      Printf.printf "block: %s, offset: %s"
162        (Val.Block.to_string b) (Val.Offset.to_string off) ;
163      (mem, [Val.zero])
164    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
165      Printf.printf "%d\n" (Val.to_int v) ;
166      (mem, [Val.zero])
167    | "print_floatln", v :: _ when Val.is_float v ->
168      Printf.printf "%f" (Val.to_float v) ;
169      (mem, [Val.zero])
170    | "print_ptrln", v :: _ when Val.is_pointer v ->
171      let (b, off) = Val.to_pointer v in
172      Printf.printf "block: %s, offset: %s\n"
173        (Val.Block.to_string b) (Val.Offset.to_string off) ;
174      (mem, [Val.zero])
175    | s, v :: _ when s = Primitive.alloc ->
176      let (mem, ptr) = Mem.alloc mem v in
177      let vs = Val.break ptr 2 in
178      (mem, vs)
179    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
180      (mem, [Val.modulo v1 v2])
181
182    (* The other cases are either a type error (only integers and pointers
183       may not be differenciated during type checking) or an unknown
184       function. *)
185    | "print_int", _ | "print_intln", _ ->
186      error "Illegal cast from pointer to integer."
187    | "print_ptr", _ | "print_ptrln", _ ->
188      error "Illegal cast from integer to pointer."
189    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
190*)
191
192
193let interpret_call st f =
194  let ptr = Mem.find_global st.mem f in
195  match Mem.find_fun_def st.mem ptr with
196    | LIN.F_int def ->
197(*
198      Printf.printf "Pushing return address in IRAM: %s\n%!"
199        (Val.to_string (next_pc st).pc) ;
200*)
201      let st = save_ra st in
202      init_fun_call st ptr
203    | LIN.F_ext def -> assert false (* TODO *)
204
205let interpret_return st =
206  let pc = return_pc st in
207(*
208  Printf.printf "Returning to %s\n%!" (Val.to_string pc) ;
209*)
210  change_pc st pc
211
212let interpret_stmt st stmt =
213  match stmt with
214
215    | LIN.St_goto lbl ->
216      goto st lbl
217
218    | LIN.St_label _ ->
219      next_pc st
220
221    | LIN.St_comment s ->
222(*
223      Printf.printf "*** %s ***\n\n%!" s ;
224*)
225      next_pc st
226
227    | LIN.St_cost cost_lbl ->
228      let st = change_trace st (cost_lbl :: st.trace) in
229      next_pc st
230
231    | LIN.St_int (r, i) ->
232      let st = add_reg r (Val.of_int i) st in
233      next_pc st
234
235    | LIN.St_pop ->
236      let (st, v) = pop st in
237      let st = add_reg I8051.a v st in
238      next_pc st
239
240    | LIN.St_push ->
241      let v = get_reg I8051.a st in
242      let st = push st v in
243      next_pc st
244
245    | LIN.St_addr x ->
246      let v = Mem.find_global st.mem x in
247      let vs = Val.break v 2 in
248      let st = add_reg I8051.dph (List.nth vs 0) st in
249      let st = add_reg I8051.dpl (List.nth vs 1) st in
250      next_pc st
251
252    | LIN.St_from_acc destr ->
253      let st = add_reg destr (get_reg I8051.a st) st in
254      next_pc st
255
256    | LIN.St_to_acc srcr ->
257      let st = add_reg I8051.a (get_reg srcr st) st in
258      next_pc st
259
260    | LIN.St_opaccs opaccs ->
261      let v =
262        Eval.opaccs opaccs
263          (get_reg I8051.a st)
264          (get_reg I8051.b st) in
265      let st = add_reg I8051.a v st in
266      next_pc st
267
268    | LIN.St_op1 op1 ->
269      let v = Eval.op1 op1 (get_reg I8051.a st) in
270      let st = add_reg I8051.a v st in
271      next_pc st
272
273    | LIN.St_op2 (op2, srcr) ->
274      let (v, carry) =
275        Eval.op2 st.carry op2
276          (get_reg I8051.a st)
277          (get_reg srcr st) in
278      let st = change_carry st carry in
279      let st = add_reg I8051.a v st in
280      next_pc st
281
282    | LIN.St_clear_carry ->
283      let st = change_carry st Val.zero in
284      next_pc st
285
286    | LIN.St_load ->
287      let addr =
288        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
289      let v = Mem.load2 st.mem chunk addr in
290      let st = add_reg I8051.a v st in
291      next_pc st
292
293    | LIN.St_store ->
294      let addr =
295        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
296      let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
297      let st = change_mem st mem in
298      next_pc st
299
300    | LIN.St_call_id f ->
301      interpret_call st f
302
303    | LIN.St_condacc lbl_true ->
304      let v = get_reg I8051.a st in
305      if Val.is_true v then goto st lbl_true
306      else
307        if Val.is_false v then next_pc st
308        else error "Undecidable branchment."
309
310    | LIN.St_return ->
311      interpret_return st
312
313
314let print_renv renv =
315  let f r v =
316    if not (Val.eq v Val.undef) then
317    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
318  I8051.RegisterMap.iter f renv
319
320let print_state st =
321  Printf.printf "PC: %s\n%!" (Val.to_string st.pc) ;
322  Printf.printf "SP: %s\n%!"
323    (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
324  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
325  print_renv st.renv ;
326  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
327  Mem.print st.mem ;
328  Printf.printf "\n%!"
329
330let print_result st =
331  let string_of_reg r = Val.to_string (get_reg r st) in
332  Printf.printf "DPH: %s - DPL: %s\n%!"
333    (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
334
335let rec iter_small_step st =
336(*
337  print_state st ;
338*)
339  match fetch_stmt st with
340    | LIN.St_return when Val.eq (return_pc st) Val.zero ->
341(*
342      print_state st ;
343      print_result st ;
344*)
345      List.rev st.trace
346    | stmt ->
347      let st' = interpret_stmt st stmt in
348      iter_small_step st'
349
350
351let add_global_vars =
352  List.fold_left
353    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
354
355let add_fun_defs =
356  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
357
358let init_prog (st : state) (p : LIN.program) : state =
359  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
360  change_mem st mem
361
362let init_renv st sp =
363  let f r st = add_reg r Val.undef st in
364  let st = I8051.RegisterSet.fold f I8051.registers st in
365  let vs = Val.break sp 2 in
366  let sph = List.nth vs 0 in
367  let spl = List.nth vs 1 in
368  let st = add_reg I8051.sph sph st in
369  let st = add_reg I8051.spl spl st in
370  st
371
372let init_sp st =
373  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
374  let (b, _) = Val.to_pointer sp in
375  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
376  let st = change_mem st mem in
377  (st, sp)
378
379let init_isp st =
380  let (mem, isp) = Mem.alloc st.mem int_ram_size in
381  let st = change_mem (change_isp st isp) mem in
382  let vs = Val.break Val.zero 2 in
383  let st = push st (List.nth vs 1) in
384  let st = push st (List.nth vs 0) in
385  st 
386
387let init_main_call st main =
388  let ptr = Mem.find_global st.mem main in
389  match Mem.find_fun_def st.mem ptr with
390    | LIN.F_int def ->
391      init_fun_call st ptr
392    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
393
394
395(* Before interpreting, the environment is initialized:
396   - Add function definitions to the memory and reserve space for the globals.
397   - Allocate memory to emulate the external stack and initialize the external
398     stack pointer.
399   - Allocate memory to emulate the internal stack and initialize the internal
400     stack pointer.
401   - Initialiaze the physical register environment. All are set to 0, except for
402     the stack pointer registers that take the high and low bits of the external
403     stack pointer.
404   - Initialize a call to the main (set the current program counter to the
405     beginning of the function).
406   - Initialize the carry flag to 0. *)
407
408let interpret p = match p.LIN.main with
409  | None -> []
410  | Some main ->
411    let st = empty_state in
412    let st = init_prog st p in
413    let (st, sp) = init_sp st in
414    let st = init_isp st in
415    let st = init_renv st sp in
416    let st = init_main_call st main in
417    let st = change_carry st Val.zero in
418    iter_small_step st
Note: See TracBrowser for help on using the repository browser.