1 | |
---|
2 | (** This module provides an interpreter for the ERTL language. *) |
---|
3 | |
---|
4 | |
---|
5 | let error_prefix = "ERTL interpret" |
---|
6 | let error s = Error.global_error error_prefix s |
---|
7 | |
---|
8 | |
---|
9 | module Mem = Driver.ERTLMemory |
---|
10 | module Val = Mem.Value |
---|
11 | let chunk = Driver.ERTLMemory.int_size |
---|
12 | module Eval = I8051.Eval (Val) |
---|
13 | |
---|
14 | |
---|
15 | (* Memory *) |
---|
16 | |
---|
17 | type memory = ERTL.function_def Mem.memory |
---|
18 | |
---|
19 | (* Local environments. They associate a value to the pseudo-registers of the |
---|
20 | function being executed. *) |
---|
21 | |
---|
22 | type local_env = Val.t Register.Map.t |
---|
23 | |
---|
24 | (* Hardware registers environments. They associate a value to each hardware |
---|
25 | register. *) |
---|
26 | |
---|
27 | type hdw_reg_env = Val.t I8051.RegisterMap.t |
---|
28 | |
---|
29 | (* Call frames. The execution state has a call stack, each element of the stack |
---|
30 | being composed of the local environment to resume the execution of the |
---|
31 | caller. *) |
---|
32 | |
---|
33 | type stack_frame = local_env |
---|
34 | |
---|
35 | (* Execution states. *) |
---|
36 | |
---|
37 | type state = |
---|
38 | { st_frs : stack_frame list ; |
---|
39 | pc : Val.address ; |
---|
40 | isp : Val.address ; |
---|
41 | exit : Val.address ; |
---|
42 | lenv : local_env ; |
---|
43 | carry : Val.t ; |
---|
44 | renv : hdw_reg_env ; |
---|
45 | mem : memory ; |
---|
46 | trace : CostLabel.t list } |
---|
47 | |
---|
48 | |
---|
49 | (* Helpers *) |
---|
50 | |
---|
51 | let add_st_frs st frame = { st with st_frs = frame :: st.st_frs } |
---|
52 | let pop_st_frs st = match st.st_frs with |
---|
53 | | [] -> error "Empty stack frames." |
---|
54 | | lenv :: st_frs -> { st with st_frs = st_frs ; lenv = lenv } |
---|
55 | let change_pc st pc = { st with pc = pc } |
---|
56 | let change_isp st isp = { st with isp = isp } |
---|
57 | let change_exit st exit = { st with exit = exit } |
---|
58 | let change_lenv st lenv = { st with lenv = lenv } |
---|
59 | let change_carry st carry = { st with carry = carry } |
---|
60 | let change_renv st renv = { st with renv = renv } |
---|
61 | let change_mem st mem = { st with mem = mem } |
---|
62 | let change_trace st trace = { st with trace = trace } |
---|
63 | let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) |
---|
64 | |
---|
65 | let empty_state = |
---|
66 | { st_frs = [] ; |
---|
67 | pc = Val.null ; |
---|
68 | isp = Val.null ; |
---|
69 | exit = Val.null ; |
---|
70 | lenv = Register.Map.empty ; |
---|
71 | carry = Val.undef ; |
---|
72 | renv = I8051.RegisterMap.empty ; |
---|
73 | mem = Mem.empty ; |
---|
74 | trace = [] } |
---|
75 | |
---|
76 | |
---|
77 | (* Each label of each function is associated an address. The base of this |
---|
78 | address is the base of the function in memory. Inside a function, offsets are |
---|
79 | bijectively associated to labels. *) |
---|
80 | |
---|
81 | module Labels_Offsets = Bijection.Make (Label) (Val.Offset) |
---|
82 | |
---|
83 | let labels_offsets_internal int_fun = |
---|
84 | let f lbl _ (lbls_offs, i) = |
---|
85 | (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in |
---|
86 | Label.Map.fold f int_fun.ERTL.f_graph |
---|
87 | |
---|
88 | (* [labels_offsets p] builds a bijection between the labels found in the |
---|
89 | functions of [p] and some memory addresses. *) |
---|
90 | |
---|
91 | let labels_offsets p = |
---|
92 | let f (lbls_offs, i) (_, def) = match def with |
---|
93 | | ERTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i) |
---|
94 | | _ -> (lbls_offs, i) in |
---|
95 | fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.ERTL.functs) |
---|
96 | |
---|
97 | let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with |
---|
98 | | ERTL.F_int def -> def |
---|
99 | | _ -> error "Trying to fetch the definition of an external function." |
---|
100 | |
---|
101 | let fetch_stmt lbls_offs st = |
---|
102 | let msg = |
---|
103 | Printf.sprintf "%s does not point to a statement." |
---|
104 | (Val.string_of_address st.pc) in |
---|
105 | if Val.is_mem_address st.pc then |
---|
106 | let off = Val.offset_of_address st.pc in |
---|
107 | let def = fun_def_of_ptr st.mem st.pc in |
---|
108 | let lbl = Labels_Offsets.find2 off lbls_offs in |
---|
109 | Label.Map.find lbl def.ERTL.f_graph |
---|
110 | else error msg |
---|
111 | |
---|
112 | let entry_pc lbls_offs ptr def = |
---|
113 | let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in |
---|
114 | Val.change_address_offset ptr off |
---|
115 | |
---|
116 | let init_fun_call lbls_offs st ptr def = |
---|
117 | let f r lenv = Register.Map.add r Val.undef lenv in |
---|
118 | let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in |
---|
119 | let pc = entry_pc lbls_offs ptr def in |
---|
120 | change_lenv (change_pc st pc) lenv |
---|
121 | |
---|
122 | let next_pc lbls_offs st lbl = |
---|
123 | let off = Labels_Offsets.find1 lbl lbls_offs in |
---|
124 | change_pc st (Val.change_address_offset st.pc off) |
---|
125 | |
---|
126 | let framesize st = |
---|
127 | if Val.is_mem_address st.pc then |
---|
128 | let def = fun_def_of_ptr st.mem st.pc in |
---|
129 | def.ERTL.f_stacksize |
---|
130 | else error "No function at the given address." |
---|
131 | |
---|
132 | type register = Hdw of I8051.register | Psd of Register.t |
---|
133 | |
---|
134 | let add_reg r v st = match r with |
---|
135 | | Hdw r -> |
---|
136 | let renv = I8051.RegisterMap.add r v st.renv in |
---|
137 | change_renv st renv |
---|
138 | | Psd r -> |
---|
139 | let lenv = Register.Map.add r v st.lenv in |
---|
140 | change_lenv st lenv |
---|
141 | |
---|
142 | let get_reg r st = match r with |
---|
143 | | Hdw r -> |
---|
144 | if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv |
---|
145 | else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".") |
---|
146 | | Psd r -> |
---|
147 | if Register.Map.mem r st.lenv then Register.Map.find r st.lenv |
---|
148 | else error ("Unknown local register " ^ (Register.print r) ^ ".") |
---|
149 | |
---|
150 | let push st v = |
---|
151 | let mem = Mem.store st.mem chunk st.isp v in |
---|
152 | let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in |
---|
153 | change_mem (change_isp st isp) mem |
---|
154 | |
---|
155 | let pop st = |
---|
156 | let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in |
---|
157 | let st = change_isp st isp in |
---|
158 | let v = Mem.load st.mem chunk st.isp in |
---|
159 | (st, v) |
---|
160 | |
---|
161 | let get_ra st = |
---|
162 | let (st, pch) = pop st in |
---|
163 | let (st, pcl) = pop st in |
---|
164 | [pcl ; pch] |
---|
165 | |
---|
166 | let save_ra lbls_offs st lbl = |
---|
167 | let ra = |
---|
168 | Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in |
---|
169 | let st = push st (List.nth ra 0) in |
---|
170 | let st = push st (List.nth ra 1) in |
---|
171 | st |
---|
172 | |
---|
173 | let save_frame st = add_st_frs st st.lenv |
---|
174 | |
---|
175 | let label_of_pointer lbls_offs ptr = |
---|
176 | (* |
---|
177 | Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ; |
---|
178 | *) |
---|
179 | let off = Val.offset_of_address ptr in |
---|
180 | Labels_Offsets.find2 off lbls_offs |
---|
181 | |
---|
182 | let pointer_of_label lbls_offs ptr lbl = |
---|
183 | Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs) |
---|
184 | |
---|
185 | let get_sp st = |
---|
186 | List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph] |
---|
187 | |
---|
188 | let set_sp vs st = |
---|
189 | let spl = List.nth vs 0 in |
---|
190 | let sph = List.nth vs 1 in |
---|
191 | let st = add_reg (Hdw I8051.spl) spl st in |
---|
192 | let st = add_reg (Hdw I8051.sph) sph st in |
---|
193 | st |
---|
194 | |
---|
195 | |
---|
196 | module InterpretExternal = Primitive.Interpret (Mem) |
---|
197 | |
---|
198 | let interpret_external mem f args = match InterpretExternal.t mem f args with |
---|
199 | | (mem', InterpretExternal.V vs) -> (mem', vs) |
---|
200 | | (mem', InterpretExternal.A addr) -> (mem', addr) |
---|
201 | |
---|
202 | let fetch_external_args f st = |
---|
203 | let size = Mem.size_of_quantity (Primitive.args_byte_size f) in |
---|
204 | let params = MiscPottier.prefix size I8051.parameters in |
---|
205 | List.map (fun r -> get_reg (Hdw r) st) params |
---|
206 | |
---|
207 | let set_result st vs = |
---|
208 | let f st (r, v) = add_reg (Hdw r) v st in |
---|
209 | List.fold_left f st (MiscPottier.combine I8051.rets vs) |
---|
210 | |
---|
211 | let interpret_external_call st f next_pc = |
---|
212 | let args = fetch_external_args f st in |
---|
213 | let (mem, vs) = interpret_external st.mem f args in |
---|
214 | let st = change_mem st mem in |
---|
215 | let st = set_result st vs in |
---|
216 | change_pc st next_pc |
---|
217 | |
---|
218 | let interpret_call lbls_offs st f ra = |
---|
219 | let ptr = Mem.find_global st.mem f in |
---|
220 | match Mem.find_fun_def st.mem ptr with |
---|
221 | | ERTL.F_int def -> |
---|
222 | let st = save_ra lbls_offs st ra in |
---|
223 | let st = save_frame st in |
---|
224 | init_fun_call lbls_offs st ptr def |
---|
225 | | ERTL.F_ext def -> |
---|
226 | let next_pc = |
---|
227 | Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in |
---|
228 | interpret_external_call st def.AST.ef_tag next_pc |
---|
229 | |
---|
230 | let interpret_return lbls_offs st = |
---|
231 | let st = pop_st_frs st in |
---|
232 | let (st, pch) = pop st in |
---|
233 | let (st, pcl) = pop st in |
---|
234 | let pc = [pcl ; pch] in |
---|
235 | change_pc st pc |
---|
236 | |
---|
237 | |
---|
238 | (* Interpret statements. *) |
---|
239 | |
---|
240 | let interpret_stmt lbls_offs st stmt = |
---|
241 | let next_pc = next_pc lbls_offs in |
---|
242 | match stmt with |
---|
243 | |
---|
244 | | ERTL.St_skip lbl -> |
---|
245 | next_pc st lbl |
---|
246 | |
---|
247 | | ERTL.St_comment (s, lbl) -> |
---|
248 | (* |
---|
249 | Printf.printf "*** %s ***\n\n%!" s ; |
---|
250 | *) |
---|
251 | next_pc st lbl |
---|
252 | |
---|
253 | | ERTL.St_cost (cost_lbl, lbl) -> |
---|
254 | let st = add_trace st cost_lbl in |
---|
255 | next_pc st lbl |
---|
256 | |
---|
257 | | ERTL.St_get_hdw (destr, srcr, lbl) -> |
---|
258 | let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in |
---|
259 | next_pc st lbl |
---|
260 | |
---|
261 | | ERTL.St_set_hdw (destr, srcr, lbl) -> |
---|
262 | let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in |
---|
263 | next_pc st lbl |
---|
264 | |
---|
265 | | ERTL.St_hdw_to_hdw (destr, srcr, lbl) -> |
---|
266 | let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in |
---|
267 | next_pc st lbl |
---|
268 | |
---|
269 | | ERTL.St_newframe lbl -> |
---|
270 | let size = framesize st in |
---|
271 | let sp = get_sp st in |
---|
272 | let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in |
---|
273 | let st = set_sp new_sp st in |
---|
274 | next_pc st lbl |
---|
275 | |
---|
276 | | ERTL.St_delframe lbl -> |
---|
277 | let size = framesize st in |
---|
278 | let sp = get_sp st in |
---|
279 | let new_sp = Val.add_address sp (Val.Offset.of_int size) in |
---|
280 | let st = set_sp new_sp st in |
---|
281 | next_pc st lbl |
---|
282 | |
---|
283 | | ERTL.St_framesize (destr, lbl) -> |
---|
284 | let size = framesize st in |
---|
285 | let st = add_reg (Psd destr) (Val.of_int size) st in |
---|
286 | next_pc st lbl |
---|
287 | |
---|
288 | | ERTL.St_pop (destr, lbl) -> |
---|
289 | let (st, v) = pop st in |
---|
290 | let st = add_reg (Psd destr) v st in |
---|
291 | next_pc st lbl |
---|
292 | |
---|
293 | | ERTL.St_push (srcr, lbl) -> |
---|
294 | let v = get_reg (Psd srcr) st in |
---|
295 | let st = push st v in |
---|
296 | next_pc st lbl |
---|
297 | |
---|
298 | | ERTL.St_addrH (r, x, lbl) -> |
---|
299 | let vs = Mem.find_global st.mem x in |
---|
300 | let st = add_reg (Psd r) (List.nth vs 1) st in |
---|
301 | next_pc st lbl |
---|
302 | |
---|
303 | | ERTL.St_addrL (r, x, lbl) -> |
---|
304 | let vs = Mem.find_global st.mem x in |
---|
305 | let st = add_reg (Psd r) (List.nth vs 0) st in |
---|
306 | next_pc st lbl |
---|
307 | |
---|
308 | | ERTL.St_int (r, i, lbl) -> |
---|
309 | let st = add_reg (Psd r) (Val.of_int i) st in |
---|
310 | next_pc st lbl |
---|
311 | |
---|
312 | | ERTL.St_move (destr, srcr, lbl) -> |
---|
313 | let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in |
---|
314 | next_pc st lbl |
---|
315 | |
---|
316 | | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) -> |
---|
317 | let (v, _) = |
---|
318 | Eval.opaccs opaccs |
---|
319 | (get_reg (Psd srcr1) st) |
---|
320 | (get_reg (Psd srcr2) st) in |
---|
321 | let st = add_reg (Psd destr) v st in |
---|
322 | next_pc st lbl |
---|
323 | |
---|
324 | | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) -> |
---|
325 | let (_, v) = |
---|
326 | Eval.opaccs opaccs |
---|
327 | (get_reg (Psd srcr1) st) |
---|
328 | (get_reg (Psd srcr2) st) in |
---|
329 | let st = add_reg (Psd destr) v st in |
---|
330 | next_pc st lbl |
---|
331 | |
---|
332 | | ERTL.St_op1 (op1, destr, srcr, lbl) -> |
---|
333 | let v = Eval.op1 op1 (get_reg (Psd srcr) st) in |
---|
334 | let st = add_reg (Psd destr) v st in |
---|
335 | next_pc st lbl |
---|
336 | |
---|
337 | | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) -> |
---|
338 | let (v, carry) = |
---|
339 | Eval.op2 st.carry op2 |
---|
340 | (get_reg (Psd srcr1) st) |
---|
341 | (get_reg (Psd srcr2) st) in |
---|
342 | let st = change_carry st carry in |
---|
343 | let st = add_reg (Psd destr) v st in |
---|
344 | next_pc st lbl |
---|
345 | |
---|
346 | | ERTL.St_clear_carry lbl -> |
---|
347 | let st = change_carry st Val.zero in |
---|
348 | next_pc st lbl |
---|
349 | |
---|
350 | | ERTL.St_set_carry lbl -> |
---|
351 | let st = change_carry st (Val.of_int 1) in |
---|
352 | next_pc st lbl |
---|
353 | |
---|
354 | | ERTL.St_load (destr, addr1, addr2, lbl) -> |
---|
355 | let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in |
---|
356 | let v = Mem.load st.mem chunk addr in |
---|
357 | let st = add_reg (Psd destr) v st in |
---|
358 | next_pc st lbl |
---|
359 | |
---|
360 | | ERTL.St_store (addr1, addr2, srcr, lbl) -> |
---|
361 | let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in |
---|
362 | let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in |
---|
363 | let st = change_mem st mem in |
---|
364 | next_pc st lbl |
---|
365 | |
---|
366 | | ERTL.St_call_id (f, _, lbl) -> |
---|
367 | interpret_call lbls_offs st f lbl |
---|
368 | |
---|
369 | | ERTL.St_cond (srcr, lbl_true, lbl_false) -> |
---|
370 | let v = get_reg (Psd srcr) st in |
---|
371 | let lbl = |
---|
372 | if Val.is_true v then lbl_true |
---|
373 | else |
---|
374 | if Val.is_false v then lbl_false |
---|
375 | else error "Undecidable branchment." in |
---|
376 | next_pc st lbl |
---|
377 | |
---|
378 | | ERTL.St_return _ -> |
---|
379 | interpret_return lbls_offs st |
---|
380 | |
---|
381 | |
---|
382 | let print_lenv lenv = |
---|
383 | let f r v = |
---|
384 | if not (Val.eq v Val.undef) then |
---|
385 | Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in |
---|
386 | Register.Map.iter f lenv |
---|
387 | |
---|
388 | let print_renv renv = |
---|
389 | let f r v = |
---|
390 | if not (Val.eq v Val.undef) then |
---|
391 | Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in |
---|
392 | I8051.RegisterMap.iter f renv |
---|
393 | |
---|
394 | let current_label lbls_offs st = |
---|
395 | Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs |
---|
396 | |
---|
397 | let print_state lbls_offs st = |
---|
398 | Printf.printf "PC: %s (%s)\n%!" |
---|
399 | (Val.string_of_address st.pc) (current_label lbls_offs st) ; |
---|
400 | Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ; |
---|
401 | Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ; |
---|
402 | Printf.printf "Carry: %s%!" (Val.to_string st.carry) ; |
---|
403 | print_lenv st.lenv ; |
---|
404 | print_renv st.renv ; |
---|
405 | Mem.print st.mem ; |
---|
406 | Printf.printf "\n%!" |
---|
407 | |
---|
408 | let compute_result st ret_regs = |
---|
409 | let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in |
---|
410 | let f res v = res && (Val.is_int v) in |
---|
411 | let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in |
---|
412 | if is_int vs then |
---|
413 | let chunks = |
---|
414 | List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in |
---|
415 | IntValue.Int32.merge chunks |
---|
416 | else IntValue.Int32.zero |
---|
417 | |
---|
418 | let rec iter_small_step debug lbls_offs st = |
---|
419 | let print_and_return_result (res, cost_labels) = |
---|
420 | if debug then Printf.printf "Result = %s\n%!" |
---|
421 | (IntValue.Int32.to_string res) ; |
---|
422 | (res, cost_labels) in |
---|
423 | if debug then print_state lbls_offs st ; |
---|
424 | match fetch_stmt lbls_offs st with |
---|
425 | | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit -> |
---|
426 | print_and_return_result (compute_result st ret_regs, List.rev st.trace) |
---|
427 | | stmt -> |
---|
428 | let st' = interpret_stmt lbls_offs st stmt in |
---|
429 | iter_small_step debug lbls_offs st' |
---|
430 | |
---|
431 | |
---|
432 | let add_global_vars = |
---|
433 | List.fold_left |
---|
434 | (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None) |
---|
435 | |
---|
436 | let add_fun_defs = |
---|
437 | List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def) |
---|
438 | |
---|
439 | let init_prog (st : state) (p : ERTL.program) : state = |
---|
440 | let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in |
---|
441 | change_mem st mem |
---|
442 | |
---|
443 | let init_sp st = |
---|
444 | let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in |
---|
445 | let sp = |
---|
446 | Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in |
---|
447 | let st = change_mem st mem in |
---|
448 | (st, sp) |
---|
449 | |
---|
450 | let init_isp st = |
---|
451 | let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in |
---|
452 | let st = change_mem (change_isp st isp) mem in |
---|
453 | let (mem, exit) = Mem.alloc st.mem 1 in |
---|
454 | let st = change_exit st exit in |
---|
455 | let st = push st (List.nth exit 0) in |
---|
456 | let st = push st (List.nth exit 1) in |
---|
457 | st |
---|
458 | |
---|
459 | let init_renv st sp = |
---|
460 | let f r renv = I8051.RegisterMap.add r Val.undef renv in |
---|
461 | let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in |
---|
462 | let spl = List.nth sp 0 in |
---|
463 | let sph = List.nth sp 1 in |
---|
464 | let renv = I8051.RegisterMap.add I8051.sph sph renv in |
---|
465 | let renv = I8051.RegisterMap.add I8051.spl spl renv in |
---|
466 | change_renv st renv |
---|
467 | |
---|
468 | let init_main_call lbls_offs st main = |
---|
469 | let ptr = Mem.find_global st.mem main in |
---|
470 | match Mem.find_fun_def st.mem ptr with |
---|
471 | | ERTL.F_int def -> |
---|
472 | init_fun_call lbls_offs st ptr def |
---|
473 | | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.") |
---|
474 | |
---|
475 | |
---|
476 | (* Before interpreting, the environment is initialized: |
---|
477 | - Build a bijection between the labels in the program and some values (taken |
---|
478 | amongst the offsets). |
---|
479 | - Add function definitions to the memory and reserve space for the globals. |
---|
480 | - Allocate memory to emulate the external stack and initialize the external |
---|
481 | stack pointer. |
---|
482 | - Allocate memory to emulate the internal stack and initialize the internal |
---|
483 | stack pointer. |
---|
484 | - Initialiaze the physical register environment. All are set to 0, except for |
---|
485 | the stack pointer registers that take the high and low bits of the external |
---|
486 | stack pointer. |
---|
487 | - Initialize a call to the main (set the current program counter to the |
---|
488 | beginning of the function). |
---|
489 | - Initialize the carry flag to 0. *) |
---|
490 | |
---|
491 | let interpret debug p = |
---|
492 | Printf.printf "*** ERTL interpret ***\n%!" ; |
---|
493 | match p.ERTL.main with |
---|
494 | | None -> (IntValue.Int32.zero, []) |
---|
495 | | Some main -> |
---|
496 | let lbls_offs = labels_offsets p in |
---|
497 | let st = empty_state in |
---|
498 | let st = init_prog st p in |
---|
499 | let (st, sp) = init_sp st in |
---|
500 | let st = init_isp st in |
---|
501 | let st = init_renv st sp in |
---|
502 | let st = init_main_call lbls_offs st main in |
---|
503 | let st = change_carry st Val.zero in |
---|
504 | iter_small_step debug lbls_offs st |
---|