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

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

Update of D2.2 from Paris.

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  : CostLabel.t list }
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      let st = save_ra st in
198      init_fun_call st ptr
199    | LIN.F_ext def -> assert false (* TODO *)
200
201let interpret_return st =
202  let pc = return_pc st in
203  change_pc st pc
204
205let interpret_stmt st stmt =
206  match stmt with
207
208    | LIN.St_goto lbl ->
209      goto st lbl
210
211    | LIN.St_label _ ->
212      next_pc st
213
214    | LIN.St_comment s ->
215(*
216      Printf.printf "*** %s ***\n\n%!" s ;
217*)
218      next_pc st
219
220    | LIN.St_cost cost_lbl ->
221      let st = change_trace st (cost_lbl :: st.trace) in
222      next_pc st
223
224    | LIN.St_int (r, i) ->
225      let st = add_reg r (Val.of_int i) st in
226      next_pc st
227
228    | LIN.St_pop ->
229      let (st, v) = pop st in
230      let st = add_reg I8051.a v st in
231      next_pc st
232
233    | LIN.St_push ->
234      let v = get_reg I8051.a st in
235      let st = push st v in
236      next_pc st
237
238    | LIN.St_addr x ->
239      let v = Mem.find_global st.mem x in
240      let vs = Val.break v 2 in
241      let st = add_reg I8051.dph (List.nth vs 0) st in
242      let st = add_reg I8051.dpl (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 v =
255        Eval.opaccs opaccs
256          (get_reg I8051.a st)
257          (get_reg I8051.b st) in
258      let st = add_reg I8051.a v st in
259      next_pc st
260
261    | LIN.St_op1 op1 ->
262      let v = Eval.op1 op1 (get_reg I8051.a st) in
263      let st = add_reg I8051.a v st in
264      next_pc st
265
266    | LIN.St_op2 (op2, srcr) ->
267      let (v, carry) =
268        Eval.op2 st.carry op2
269          (get_reg I8051.a st)
270          (get_reg srcr st) in
271      let st = change_carry st carry in
272      let st = add_reg I8051.a v st in
273      next_pc st
274
275    | LIN.St_clear_carry ->
276      let st = change_carry st Val.zero in
277      next_pc st
278
279    | LIN.St_load ->
280      let addr =
281        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
282      let v = Mem.load2 st.mem chunk addr in
283      let st = add_reg I8051.a v st in
284      next_pc st
285
286    | LIN.St_store ->
287      let addr =
288        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
289      let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
290      let st = change_mem st mem in
291      next_pc st
292
293    | LIN.St_call_id f ->
294      interpret_call st f
295
296    | LIN.St_condacc lbl_true ->
297      let v = get_reg I8051.a st in
298      if Val.is_true v then goto st lbl_true
299      else
300        if Val.is_false v then next_pc st
301        else error "Undecidable branchment."
302
303    | LIN.St_return ->
304      interpret_return st
305
306
307let print_renv renv =
308  let f r v =
309    if not (Val.eq v Val.undef) then
310    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
311  I8051.RegisterMap.iter f renv
312
313let print_state st =
314  Printf.printf "PC: %s\n%!" (Val.to_string st.pc) ;
315  Printf.printf "SP: %s\n%!"
316    (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
317  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
318  print_renv st.renv ;
319  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
320  Mem.print st.mem ;
321  Printf.printf "\n%!"
322
323let compute_result st =
324  let v = get_reg I8051.dpl st in
325  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
326  else IntValue.Int8.zero
327
328let rec iter_small_step print_result st =
329(*
330  (* <DEBUG> *)
331  print_state st ;
332  (* </DEBUG> *)
333*)
334  match fetch_stmt st with
335    | LIN.St_return when Val.eq (return_pc st) Val.zero ->
336      let (res, cost_labels) as trace =
337        (compute_result st, List.rev st.trace) in
338      if print_result then
339        Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ;
340      trace
341    | stmt ->
342      let st' = interpret_stmt st stmt in
343      iter_small_step print_result st'
344
345
346let add_global_vars =
347  List.fold_left
348    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
349
350let add_fun_defs =
351  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
352
353let init_prog (st : state) (p : LIN.program) : state =
354  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
355  change_mem st mem
356
357let init_renv st sp =
358  let f r st = add_reg r Val.undef st in
359  let st = I8051.RegisterSet.fold f I8051.registers st in
360  let vs = Val.break sp 2 in
361  let sph = List.nth vs 0 in
362  let spl = List.nth vs 1 in
363  let st = add_reg I8051.sph sph st in
364  let st = add_reg I8051.spl spl st in
365  st
366
367let init_sp st =
368  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
369  let (b, _) = Val.to_pointer sp in
370  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
371  let st = change_mem st mem in
372  (st, sp)
373
374let init_isp st =
375  let (mem, isp) = Mem.alloc st.mem int_ram_size in
376  let st = change_mem (change_isp st isp) mem in
377  let vs = Val.break Val.zero 2 in
378  let st = push st (List.nth vs 1) in
379  let st = push st (List.nth vs 0) in
380  st 
381
382let init_main_call st main =
383  let ptr = Mem.find_global st.mem main in
384  match Mem.find_fun_def st.mem ptr with
385    | LIN.F_int def ->
386      init_fun_call st ptr
387    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
388
389
390(* Before interpreting, the environment is initialized:
391   - Add function definitions to the memory and reserve space for the globals.
392   - Allocate memory to emulate the external stack and initialize the external
393     stack pointer.
394   - Allocate memory to emulate the internal stack and initialize the internal
395     stack pointer.
396   - Initialiaze the physical register environment. All are set to 0, except for
397     the stack pointer registers that take the high and low bits of the external
398     stack pointer.
399   - Initialize a call to the main (set the current program counter to the
400     beginning of the function).
401   - Initialize the carry flag to 0. *)
402
403let interpret print_result p = match p.LIN.main with
404  | None -> (IntValue.Int8.zero, [])
405  | Some main ->
406    let st = empty_state in
407    let st = init_prog st p in
408    let (st, sp) = init_sp st in
409    let st = init_isp st in
410    let st = init_renv st sp in
411    let st = init_main_call st main in
412    let st = change_carry st Val.zero in
413    iter_small_step print_result st
Note: See TracBrowser for help on using the repository browser.