source: Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml @ 1349

Last change on this file since 1349 was 1349, checked in by tranquil, 9 years ago
  • work on LIN completed
  • small implementation of extensible arrays
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
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)
50
51let forget_ind st = match st.inds with
52    | _ :: tail -> {st with inds = tail}
53    | _ -> assert false (* indexing list must be non-empty *)
54let curr_ind st = match st.inds with
55    | ind :: _ -> ind
56    | _ -> assert false (* indexing list must be non-empty *)
57let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
58
59let max_depth =
60    let f_stmt j = function
61        | LIN.St_ind_0 i | LIN.St_ind_inc i -> max (i + 1) j
62        | _ -> j in
63    List.fold_left f_stmt 0 
64
65let empty_state =
66  { pc     = Val.null ;
67    isp    = Val.null ;
68    exit   = Val.null ;
69    carry  = Val.undef ;
70    renv   = I8051.RegisterMap.empty ;
71    mem    = Mem.empty ;
72                inds   = [] ;
73    trace  = [] }
74
75
76let int_fun_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
77  | LIN.F_int def -> def
78  | _ -> error "Trying to fetch the definition of an external function."
79
80let current_int_fun st = int_fun_of_ptr st.mem st.pc
81
82let fetch_stmt st =
83  let msg =
84    Printf.sprintf "%s does not point to a statement."
85      (Val.string_of_address st.pc) in
86  if Val.is_mem_address st.pc then
87    let off = Val.offset_of_address st.pc in
88    let def = int_fun_of_ptr st.mem st.pc in
89    List.nth def (Val.Offset.to_int off)
90  else error msg
91
92let init_fun_call st ptr def =
93        let st = allocate_ind st (max_depth def) in
94  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
95
96let next_pc st =
97  change_pc st (Val.add_address st.pc Val.Offset.one)
98
99let add_reg r v st =
100  let renv = I8051.RegisterMap.add r v st.renv in
101  change_renv st renv
102
103let get_reg r st =
104  if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
105  else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
106
107let push st v =
108  let mem = Mem.store st.mem chunk st.isp v in
109  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
110  change_mem (change_isp st isp) mem
111
112let pop st =
113  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
114  let st = change_isp st isp in
115  let v = Mem.load st.mem chunk st.isp in
116  (st, v)
117
118let save_ra st =
119  let ra = Val.add_address st.pc Val.Offset.one in
120  let st = push st (List.nth ra 0) in
121  let st = push st (List.nth ra 1) in
122  st
123
124let find_label lbl =
125  let rec aux i = function
126  | [] -> error (Printf.sprintf "Unknown label %s." lbl)
127  | LIN.St_label lbl' :: _ when lbl' = lbl -> i
128  | _ :: code -> aux (i+1) code
129  in
130  aux 0
131
132let pointer_of_label st lbl =
133  let code = current_int_fun st in
134  let off = find_label lbl code in
135  Val.change_address_offset st.pc (Val.Offset.of_int off)
136
137let goto st lbl =
138  change_pc st (pointer_of_label st lbl)
139
140let return_pc st =
141  let (st, pch) = pop st in
142  let (st, pcl) = pop st in
143  (st, [pcl ; pch])
144
145let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
146
147
148(* State pretty-printing *)
149
150let print_renv renv =
151  let f r v =
152    if not (Val.eq v Val.undef) then
153    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
154  I8051.RegisterMap.iter f renv
155
156let print_state st =
157  Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
158  Printf.printf "SP: %s\n%!"
159    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
160  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
161  print_renv st.renv ;
162  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
163  Mem.print st.mem ;
164  Printf.printf "\n%!"
165
166
167module InterpretExternal = Primitive.Interpret (Mem)
168
169let interpret_external mem f args = match InterpretExternal.t mem f args with
170  | (mem', InterpretExternal.V vs) -> (mem', vs)
171  | (mem', InterpretExternal.A addr) -> (mem', addr)
172
173let fetch_external_args f st =
174  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
175  let params = MiscPottier.prefix size I8051.parameters in
176  List.map (fun r -> get_reg r st) params
177
178let set_result st vs =
179  let f st (r, v) = add_reg r v st in
180  List.fold_left f st (MiscPottier.combine I8051.rets vs)
181
182let interpret_external_call st f =
183  let args = fetch_external_args f st in
184  let (mem, vs) = interpret_external st.mem f args in
185  let st = change_mem st mem in
186  set_result st vs
187
188let interpret_call st f =
189  let ptr = Mem.find_global st.mem f in
190  match Mem.find_fun_def st.mem ptr with
191    | LIN.F_int def ->
192      let st = save_ra st in
193      init_fun_call st ptr def
194    | LIN.F_ext def ->
195      let st = next_pc st in
196      interpret_external_call st def.AST.ef_tag
197
198let interpret_return st =
199        let st = forget_ind st in
200  let (st, pc) = return_pc st in
201  change_pc st pc
202
203let interpret_stmt st stmt =
204  match stmt with
205
206    | LIN.St_goto lbl ->
207      goto st lbl
208
209    | LIN.St_label _ ->
210      next_pc st
211
212    | LIN.St_comment s ->
213(*
214      Printf.printf "*** %s ***\n\n%!" s ;
215*)
216      next_pc st
217
218    | LIN.St_cost cost_lbl ->
219                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
220      let st = add_trace st cost_lbl in
221      next_pc st
222                       
223                | LIN.St_ind_0 i ->
224                        CostLabel.enter_loop (Some i) (curr_ind st);
225                        next_pc st
226
227    | LIN.St_ind_inc i ->
228            CostLabel.continue_loop (Some i) (curr_ind st);
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 vs = Mem.find_global st.mem x in
247      let st = add_reg I8051.dpl (List.nth vs 0) st in
248      let st = add_reg I8051.dph (List.nth vs 1) st in
249      next_pc st
250
251    | LIN.St_from_acc destr ->
252      let st = add_reg destr (get_reg I8051.a st) st in
253      next_pc st
254
255    | LIN.St_to_acc srcr ->
256      let st = add_reg I8051.a (get_reg srcr st) st in
257      next_pc st
258
259    | LIN.St_opaccs opaccs ->
260      let (a, b) =
261        Eval.opaccs opaccs
262          (get_reg I8051.a st)
263          (get_reg I8051.b st) in
264      let st = add_reg I8051.a a st in
265      let st = add_reg I8051.b b 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_set_carry ->
287      let st = change_carry st (Val.of_int 1) in
288      next_pc st
289
290    | LIN.St_load ->
291      let addr = dptr st in
292      let v = Mem.load st.mem chunk addr in
293      let st = add_reg I8051.a v st in
294      next_pc st
295
296    | LIN.St_store ->
297      let addr = dptr st in
298      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
299      let st = change_mem st mem in
300      next_pc st
301
302    | LIN.St_call_id f ->
303      interpret_call st f
304
305    | LIN.St_condacc lbl_true ->
306      let v = get_reg I8051.a st in
307      if Val.is_true v then goto st lbl_true
308      else
309        if Val.is_false v then next_pc st
310        else error "Undecidable branchment."
311
312    | LIN.St_return ->
313      interpret_return st
314
315
316let compute_result st =
317  let vs = List.map (fun r -> get_reg r st) I8051.rets in
318  let f res v = res && (Val.is_int v) in
319  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
320  if is_int vs then
321    let chunks =
322      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
323    IntValue.Int32.merge chunks
324  else IntValue.Int32.zero
325
326let rec iter_small_step debug st =
327  let print_and_return_result (res, cost_labels) =
328    if debug then Printf.printf "Result = %s\n%!"
329      (IntValue.Int32.to_string res) ;
330    (res, cost_labels) in
331  if debug then print_state st ;
332  match fetch_stmt st with
333    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
334      print_and_return_result (compute_result st, List.rev st.trace)
335    | stmt ->
336      let st' = interpret_stmt st stmt in
337      iter_small_step debug st'
338
339
340let add_global_vars =
341  List.fold_left
342    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
343
344let add_fun_defs =
345  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
346
347let init_prog (st : state) (p : LIN.program) : state =
348  let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
349  change_mem st mem
350
351let init_sp st =
352  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
353  let sp =
354    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
355  let st = change_mem st mem in
356  (st, sp)
357
358let init_isp st =
359  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
360  let st = change_mem (change_isp st isp) mem in
361  let (mem, exit) = Mem.alloc st.mem 1 in
362  let st = change_exit st exit in
363  let st = push st (List.nth exit 0) in
364  let st = push st (List.nth exit 1) in
365  st 
366
367let init_renv st sp =
368  let f r st = add_reg r Val.undef st in
369  let st = I8051.RegisterSet.fold f I8051.registers st in
370  let spl = List.nth sp 0 in
371  let sph = List.nth sp 1 in
372  let st = add_reg I8051.spl spl st in
373  let st = add_reg I8051.sph sph st in
374  st
375
376let init_main_call st main =
377  let ptr = Mem.find_global st.mem main in
378  match Mem.find_fun_def st.mem ptr with
379    | LIN.F_int def ->
380      init_fun_call st ptr def
381    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
382
383
384(* Before interpreting, the environment is initialized:
385   - Add function definitions to the memory and reserve space for the globals.
386   - Allocate memory to emulate the external stack and initialize the external
387     stack pointer.
388   - Allocate memory to emulate the internal stack and initialize the internal
389     stack pointer.
390   - Initialiaze the physical register environment. All are set to 0, except for
391     the stack pointer registers that take the high and low bits of the external
392     stack pointer.
393   - Initialize a call to the main (set the current program counter to the
394     beginning of the function).
395   - Initialize the carry flag to 0. *)
396
397let interpret debug p =
398  Printf.printf "*** LIN interpret ***\n%!" ;
399  match p.LIN.main with
400    | None -> (IntValue.Int32.zero, [])
401    | Some main ->
402      let st = empty_state in
403      let st = init_prog st p in
404      let (st, sp) = init_sp st in
405      let st = init_isp st in
406      let st = init_renv st sp in
407      let st = init_main_call st main in
408      let st = change_carry st Val.zero in
409      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.