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

Last change on this file since 1542 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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
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 push st v =
99  let mem = Mem.store st.mem chunk st.isp v in
100  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
101  change_mem (change_isp st isp) mem
102
103let pop st =
104  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
105  let st = change_isp st isp in
106  let v = Mem.load st.mem chunk st.isp in
107  (st, v)
108
109let save_ra st =
110  let ra = Val.add_address st.pc Val.Offset.one in
111  let st = push st (List.nth ra 0) in
112  let st = push st (List.nth ra 1) in
113  st
114
115let find_label lbl =
116  let rec aux i = function
117  | [] -> error (Printf.sprintf "Unknown label %s." lbl)
118  | LIN.St_label lbl' :: _ when lbl' = lbl -> i
119  | _ :: code -> aux (i+1) code
120  in
121  aux 0
122
123let pointer_of_label st lbl =
124  let code = current_int_fun st in
125  let off = find_label lbl code in
126  Val.change_address_offset st.pc (Val.Offset.of_int off)
127
128let goto st lbl =
129  change_pc st (pointer_of_label st lbl)
130
131let return_pc st =
132  let (st, pch) = pop st in
133  let (st, pcl) = pop st in
134  (st, [pcl ; pch])
135
136let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
137
138
139(* State pretty-printing *)
140
141let print_renv renv =
142  let f r v =
143    if not (Val.eq v Val.undef) then
144    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
145  I8051.RegisterMap.iter f renv
146
147let print_state st =
148  Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
149  Printf.printf "SP: %s\n%!"
150    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
151  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
152  print_renv st.renv ;
153  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
154  Mem.print st.mem ;
155  Printf.printf "\n%!"
156
157
158module InterpretExternal = Primitive.Interpret (Mem)
159
160let interpret_external mem f args = match InterpretExternal.t mem f args with
161  | (mem', InterpretExternal.V vs) -> (mem', vs)
162  | (mem', InterpretExternal.A addr) -> (mem', addr)
163
164let fetch_external_args f st =
165  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
166  let params = MiscPottier.prefix size I8051.parameters in
167  List.map (fun r -> get_reg r st) params
168
169let set_result st vs =
170  let f st (r, v) = add_reg r v st in
171  List.fold_left f st (MiscPottier.combine I8051.rets vs)
172
173let interpret_external_call st f =
174  let args = fetch_external_args f st in
175  let (mem, vs) = interpret_external st.mem f args in
176  let st = change_mem st mem in
177  set_result st vs
178
179let interpret_call st ptr =
180  match Mem.find_fun_def st.mem ptr with
181    | LIN.F_int def ->
182      let st = save_ra st in
183      init_fun_call st ptr
184    | LIN.F_ext def ->
185      let st = next_pc st in
186      interpret_external_call st def.AST.ef_tag
187
188let interpret_return st =
189  let st = forget_ind st in
190  let (st, pc) = return_pc st in
191  change_pc st pc
192
193let interpret_stmt st stmt =
194  match stmt with
195
196    | LIN.St_goto lbl ->
197      goto st lbl
198
199    | LIN.St_label _ ->
200      next_pc st
201
202    | LIN.St_comment s ->
203(*
204      Printf.printf "*** %s ***\n\n%!" s ;
205*)
206      next_pc st
207
208    | LIN.St_cost cost_lbl ->
209      let cost_lbl = ev_label st cost_lbl in
210      let st = add_trace st cost_lbl in
211      next_pc st
212
213    | LIN.St_ind_0 i ->
214      enter_loop st i;
215      next_pc st
216
217    | LIN.St_ind_inc i ->
218      continue_loop st i;
219      next_pc st
220
221    | LIN.St_int (r, i) ->
222      let st = add_reg r (Val.of_int i) st in
223      next_pc st
224
225    | LIN.St_pop ->
226      let (st, v) = pop st in
227      let st = add_reg I8051.a v st in
228      next_pc st
229
230    | LIN.St_push ->
231      let v = get_reg I8051.a st in
232      let st = push st v in
233      next_pc st
234
235    | LIN.St_addr x ->
236      let vs = Mem.find_global st.mem x in
237      let st = add_reg I8051.dpl (List.nth vs 0) st in
238      let st = add_reg I8051.dph (List.nth vs 1) st in
239      next_pc st
240
241    | LIN.St_from_acc destr ->
242      let st = add_reg destr (get_reg I8051.a st) st in
243      next_pc st
244
245    | LIN.St_to_acc srcr ->
246      let st = add_reg I8051.a (get_reg srcr st) st in
247      next_pc st
248
249    | LIN.St_opaccs opaccs ->
250      let (a, b) =
251        Eval.opaccs opaccs
252          (get_reg I8051.a st)
253          (get_reg I8051.b st) in
254      let st = add_reg I8051.a a st in
255      let st = add_reg I8051.b b st in
256      next_pc st
257
258    | LIN.St_op1 op1 ->
259      let v = Eval.op1 op1 (get_reg I8051.a st) in
260      let st = add_reg I8051.a v st in
261      next_pc st
262
263    | LIN.St_op2 (op2, srcr) ->
264      let (v, carry) =
265        Eval.op2 st.carry op2
266          (get_reg I8051.a st)
267          (get_reg srcr st) in
268      let st = change_carry st carry in
269      let st = add_reg I8051.a v st in
270      next_pc st
271
272    | LIN.St_clear_carry ->
273      let st = change_carry st Val.zero in
274      next_pc st
275
276    | LIN.St_set_carry ->
277      let st = change_carry st (Val.of_int 1) in
278      next_pc st
279
280    | LIN.St_load ->
281      let addr = dptr st in
282      let v = Mem.load 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 = dptr st in
288      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
289      let st = change_mem st mem in
290      next_pc st
291
292    | LIN.St_call_id f ->
293      interpret_call st (Mem.find_global st.mem f)
294
295    | LIN.St_call_ptr ->
296      interpret_call st (dptr st)
297
298    | LIN.St_condacc lbl_true ->
299      let v = get_reg I8051.a st in
300      if Val.is_true v then goto st lbl_true
301      else
302        if Val.is_false v then next_pc st
303        else error "Undecidable branchment."
304
305    | LIN.St_return ->
306      interpret_return st
307
308
309let compute_result st =
310  let vs = List.map (fun r -> get_reg r st) I8051.rets in
311  let f res v = res && (Val.is_int v) in
312  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
313  if is_int vs then
314    let chunks =
315      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
316    IntValue.Int32.merge chunks
317  else IntValue.Int32.zero
318
319let rec iter_small_step debug st =
320  let print_and_return_result (res, cost_labels) =
321    if debug then Printf.printf "Result = %s\n%!"
322      (IntValue.Int32.to_string res) ;
323    (res, cost_labels) in
324  if debug then print_state st ;
325  match fetch_stmt st with
326    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
327      print_and_return_result (compute_result st, List.rev st.trace)
328    | stmt ->
329      let st' = interpret_stmt st stmt in
330      iter_small_step debug st'
331
332
333let add_global_vars =
334  List.fold_left
335    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
336
337let add_fun_defs =
338  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
339
340let init_prog (st : state) (p : LIN.program) : state =
341  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
342  change_mem st mem
343
344let init_sp st =
345  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
346  let sp =
347    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
348  let st = change_mem st mem in
349  (st, sp)
350
351let init_isp st =
352  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
353  let st = change_mem (change_isp st isp) mem in
354  let (mem, exit) = Mem.alloc st.mem 1 in
355  let st = change_exit st exit in
356  let st = push st (List.nth exit 0) in
357  let st = push st (List.nth exit 1) in
358  st 
359
360let init_renv st sp =
361  let f r st = add_reg r Val.undef st in
362  let st = I8051.RegisterSet.fold f I8051.registers st in
363  let spl = List.nth sp 0 in
364  let sph = List.nth sp 1 in
365  let st = add_reg I8051.spl spl st in
366  let st = add_reg I8051.sph sph st in
367  st
368
369let init_main_call st main =
370  let ptr = Mem.find_global st.mem main in
371  match Mem.find_fun_def st.mem ptr with
372    | LIN.F_int def ->
373      init_fun_call st ptr
374    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
375
376
377(* Before interpreting, the environment is initialized:
378   - Add function definitions to the memory and reserve space for the globals.
379   - Allocate memory to emulate the external stack and initialize the external
380     stack pointer.
381   - Allocate memory to emulate the internal stack and initialize the internal
382     stack pointer.
383   - Initialiaze the physical register environment. All are set to 0, except for
384     the stack pointer registers that take the high and low bits of the external
385     stack pointer.
386   - Initialize a call to the main (set the current program counter to the
387     beginning of the function).
388   - Initialize the carry flag to 0. *)
389
390let interpret debug p =
391  Printf.printf "*** LIN interpret ***\n%!" ;
392  match p.LIN.main with
393    | None -> (IntValue.Int32.zero, [])
394    | Some main ->
395      let st = empty_state in
396      let st = init_prog st p in
397      let (st, sp) = init_sp st in
398      let st = init_isp st in
399      let st = init_renv st sp in
400      let st = init_main_call st main in
401      let st = change_carry st Val.zero in
402      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.