source: Deliverables/D2.3/8051/src/LIN/LINInterpret.ml @ 453

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

Import of the Paris's sources.

File size: 11.2 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 rec iter_small_step st =
331(*
332  print_state st ;
333*)
334  match fetch_stmt st with
335    | LIN.St_return when Val.eq (return_pc st) Val.zero ->
336(*
337      print_state st ;
338*)
339      List.rev st.trace
340    | stmt ->
341      let st' = interpret_stmt st stmt in
342      iter_small_step st'
343
344
345let add_global_vars =
346  List.fold_left
347    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
348
349let add_fun_defs =
350  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
351
352let init_prog (st : state) (p : LIN.program) : state =
353  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
354  change_mem st mem
355
356let init_renv st sp =
357  let f r st = add_reg r Val.undef st in
358  let st = I8051.RegisterSet.fold f I8051.registers st in
359  let vs = Val.break sp 2 in
360  let sph = List.nth vs 0 in
361  let spl = List.nth vs 1 in
362  let st = add_reg I8051.sph sph st in
363  let st = add_reg I8051.spl spl st in
364  st
365
366let init_sp st =
367  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
368  let (b, _) = Val.to_pointer sp in
369  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
370  let st = change_mem st mem in
371  (st, sp)
372
373let init_isp st =
374  let (mem, isp) = Mem.alloc st.mem int_ram_size in
375  let st = change_mem (change_isp st isp) mem in
376  let vs = Val.break Val.zero 2 in
377  let st = push st (List.nth vs 1) in
378  let st = push st (List.nth vs 0) in
379  st 
380
381let init_main_call st main =
382  let ptr = Mem.find_global st.mem main in
383  match Mem.find_fun_def st.mem ptr with
384    | LIN.F_int def ->
385      init_fun_call st ptr
386    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
387
388
389(* Before interpreting, the environment is initialized:
390   - Add function definitions to the memory and reserve space for the globals.
391   - Allocate memory to emulate the external stack and initialize the external
392     stack pointer.
393   - Allocate memory to emulate the internal stack and initialize the internal
394     stack pointer.
395   - Initialiaze the physical register environment. All are set to 0, except for
396     the stack pointer registers that take the high and low bits of the external
397     stack pointer.
398   - Initialize a call to the main (set the current program counter to the
399     beginning of the function).
400   - Initialize the carry flag to 0. *)
401
402let interpret p = match p.LIN.main with
403  | None -> []
404  | Some main ->
405    let st = empty_state in
406    let st = init_prog st p in
407    let (st, sp) = init_sp st in
408    let st = init_isp st in
409    let st = init_renv st sp in
410    let st = init_main_call st main in
411    let st = change_carry st Val.zero in
412    iter_small_step st
Note: See TracBrowser for help on using the repository browser.