2 (** This module provides an interpreter for the LIN language. *)
5 let error_prefix = "LIN interpret"
6 let error s = Error.global_error error_prefix s
9 module Mem = Driver.LINMemory
10 module Val = Mem.Value
11 let chunk = Driver.LINMemory.int_size
12 module Eval = I8051.Eval (Val)
17 type memory = LIN.function_def Mem.memory
19 (* Hardware registers environments. They associate a value to each hardware
22 type hdw_reg_env = Val.t I8051.RegisterMap.t
24 (* Execution states. *)
33 trace : CostLabel.t list }
38 let change_pc st pc = { st with pc = pc }
39 let change_isp st isp = { st with isp = isp }
40 let change_exit st exit = { st with exit = exit }
41 let change_carry st carry = { st with carry = carry }
42 let change_renv st renv = { st with renv = renv }
43 let change_mem st mem = { st with mem = mem }
44 let change_trace st trace = { st with trace = trace }
45 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
52 renv = I8051.RegisterMap.empty ;
57 let int_fun_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
58 | LIN.F_int def -> def
59 | _ -> error "Trying to fetch the definition of an external function."
61 let current_int_fun st = int_fun_of_ptr st.mem st.pc
65 Printf.sprintf "%s does not point to a statement."
66 (Val.string_of_address st.pc) in
67 if Val.is_mem_address st.pc then
68 let off = Val.offset_of_address st.pc in
69 let def = int_fun_of_ptr st.mem st.pc in
70 List.nth def (Val.Offset.to_int off)
73 let init_fun_call st ptr =
74 change_pc st (Val.change_address_offset ptr Val.Offset.zero)
77 change_pc st (Val.add_address st.pc Val.Offset.one)
80 let renv = I8051.RegisterMap.add r v st.renv in
84 if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
85 else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
88 let mem = Mem.store st.mem chunk st.isp v in
89 let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
90 change_mem (change_isp st isp) mem
93 let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
94 let st = change_isp st isp in
95 let v = Mem.load st.mem chunk st.isp in
99 let ra = Val.add_address st.pc Val.Offset.one in
100 let st = push st (List.nth ra 0) in
101 let st = push st (List.nth ra 1) in
105 let rec aux i = function
106 | [] -> error (Printf.sprintf "Unknown label %s." lbl)
107 | LIN.St_label lbl' :: _ when lbl' = lbl -> i
108 | _ :: code -> aux (i+1) code
112 let pointer_of_label st lbl =
113 let code = current_int_fun st in
114 let off = find_label lbl code in
115 Val.change_address_offset st.pc (Val.Offset.of_int off)
118 change_pc st (pointer_of_label st lbl)
121 let (st, pch) = pop st in
122 let (st, pcl) = pop st in
125 let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
128 (* State pretty-printing *)
130 let print_renv renv =
132 if not (Val.eq v Val.undef) then
133 Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
134 I8051.RegisterMap.iter f renv
137 Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
138 Printf.printf "SP: %s\n%!"
139 (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
140 Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
142 Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
147 module InterpretExternal = Primitive.Interpret (Mem)
149 let interpret_external mem f args = match InterpretExternal.t mem f args with
150 | (mem', InterpretExternal.V vs) -> (mem', vs)
151 | (mem', InterpretExternal.A addr) -> (mem', addr)
153 let fetch_external_args f st =
154 let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
155 let params = MiscPottier.prefix size I8051.parameters in
156 List.map (fun r -> get_reg r st) params
158 let set_result st vs =
159 let f st (r, v) = add_reg r v st in
160 List.fold_left f st (MiscPottier.combine I8051.rets vs)
162 let interpret_external_call st f =
163 let args = fetch_external_args f st in
164 let (mem, vs) = interpret_external st.mem f args in
165 let st = change_mem st mem in
168 let interpret_call st ptr =
169 match Mem.find_fun_def st.mem ptr with
171 let st = save_ra st in
174 let st = next_pc st in
175 interpret_external_call st def.AST.ef_tag
177 let interpret_return st =
178 let (st, pc) = return_pc st in
181 let interpret_stmt st stmt =
190 | LIN.St_comment s ->
192 Printf.printf "*** %s ***\n\n%!" s ;
196 | LIN.St_cost cost_lbl ->
197 let st = add_trace st cost_lbl in
200 | LIN.St_int (r, i) ->
201 let st = add_reg r (Val.of_int i) st in
205 let (st, v) = pop st in
206 let st = add_reg I8051.a v st in
210 let v = get_reg I8051.a st in
211 let st = push st v in
215 let vs = Mem.find_global st.mem x in
216 let st = add_reg I8051.dpl (List.nth vs 0) st in
217 let st = add_reg I8051.dph (List.nth vs 1) st in
220 | LIN.St_from_acc destr ->
221 let st = add_reg destr (get_reg I8051.a st) st in
224 | LIN.St_to_acc srcr ->
225 let st = add_reg I8051.a (get_reg srcr st) st in
228 | LIN.St_opaccs opaccs ->
232 (get_reg I8051.b st) in
233 let st = add_reg I8051.a a st in
234 let st = add_reg I8051.b b st in
238 let v = Eval.op1 op1 (get_reg I8051.a st) in
239 let st = add_reg I8051.a v st in
242 | LIN.St_op2 (op2, srcr) ->
244 Eval.op2 st.carry op2
247 let st = change_carry st carry in
248 let st = add_reg I8051.a v st in
251 | LIN.St_clear_carry ->
252 let st = change_carry st Val.zero in
255 | LIN.St_set_carry ->
256 let st = change_carry st (Val.of_int 1) in
260 let addr = dptr st in
261 let v = Mem.load st.mem chunk addr in
262 let st = add_reg I8051.a v st in
266 let addr = dptr st in
267 let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
268 let st = change_mem st mem in
271 | LIN.St_call_id f ->
272 interpret_call st (Mem.find_global st.mem f)
275 interpret_call st (dptr st)
277 | LIN.St_condacc lbl_true ->
278 let v = get_reg I8051.a st in
279 if Val.is_true v then goto st lbl_true
281 if Val.is_false v then next_pc st
282 else error "Undecidable branchment."
288 let compute_result st =
289 let vs = List.map (fun r -> get_reg r st) I8051.rets in
290 let f res v = res && (Val.is_int v) in
291 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
294 List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
295 IntValue.Int32.merge chunks
296 else IntValue.Int32.zero
298 let rec iter_small_step debug st =
299 let print_and_return_result (res, cost_labels) =
300 if debug then Printf.printf "Result = %s\n%!"
301 (IntValue.Int32.to_string res) ;
302 (res, cost_labels) in
303 if debug then print_state st ;
304 match fetch_stmt st with
305 | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
306 print_and_return_result (compute_result st, List.rev st.trace)
308 let st' = interpret_stmt st stmt in
309 iter_small_step debug st'
312 let add_global_vars =
314 (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
317 List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
319 let init_prog (st : state) (p : LIN.program) : state =
320 let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
324 let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
326 Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
327 let st = change_mem st mem in
331 let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
332 let st = change_mem (change_isp st isp) mem in
333 let (mem, exit) = Mem.alloc st.mem 1 in
334 let st = change_exit st exit in
335 let st = push st (List.nth exit 0) in
336 let st = push st (List.nth exit 1) in
339 let init_renv st sp =
340 let f r st = add_reg r Val.undef st in
341 let st = I8051.RegisterSet.fold f I8051.registers st in
342 let spl = List.nth sp 0 in
343 let sph = List.nth sp 1 in
344 let st = add_reg I8051.spl spl st in
345 let st = add_reg I8051.sph sph st in
348 let init_main_call st main =
349 let ptr = Mem.find_global st.mem main in
350 match Mem.find_fun_def st.mem ptr with
353 | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
356 (* Before interpreting, the environment is initialized:
357 - Add function definitions to the memory and reserve space for the globals.
358 - Allocate memory to emulate the external stack and initialize the external
360 - Allocate memory to emulate the internal stack and initialize the internal
362 - Initialiaze the physical register environment. All are set to 0, except for
363 the stack pointer registers that take the high and low bits of the external
365 - Initialize a call to the main (set the current program counter to the
366 beginning of the function).
367 - Initialize the carry flag to 0. *)
369 let interpret debug p =
370 Printf.printf "*** LIN interpret ***\n%!" ;
371 match p.LIN.main with
372 | None -> (IntValue.Int32.zero, [])
374 let st = empty_state in
375 let st = init_prog st p in
376 let (st, sp) = init_sp st in
377 let st = init_isp st in
378 let st = init_renv st sp in
379 let st = init_main_call st main in
380 let st = change_carry st Val.zero in
381 iter_small_step debug st