133 open Hints_declaration
154 (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
157 (** val ps_reg_store :
158 PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
159 (ByteValues.beval Identifiers.identifier_map,
160 SemanticsUtils.hw_register_env) Types.prod Errors.res **)
161 let ps_reg_store r v local_env =
162 let res = SemanticsUtils.reg_store r v local_env.Types.fst in
163 Errors.OK { Types.fst = res; Types.snd = local_env.Types.snd }
165 (** val ps_reg_retrieve :
166 ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res **)
167 let ps_reg_retrieve local_env =
168 SemanticsUtils.reg_retrieve local_env.Types.fst
170 (** val hw_reg_store :
171 I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
172 Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
174 let hw_reg_store r v local_env =
175 Errors.OK { Types.fst = local_env.Types.fst; Types.snd =
176 (SemanticsUtils.hwreg_store r v local_env.Types.snd) }
178 (** val hw_reg_retrieve :
179 ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res **)
180 let hw_reg_retrieve local_env reg =
181 Errors.OK (SemanticsUtils.hwreg_retrieve local_env.Types.snd reg)
183 (** val ps_arg_retrieve :
184 ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
186 let ps_arg_retrieve local_env = function
187 | Joint.Reg r -> ps_reg_retrieve local_env r
190 (Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
192 (** val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res **)
194 SemanticsUtils.hwreg_retrieve_sp st.Types.snd
196 (** val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env **)
198 { Types.fst = st.Types.fst; Types.snd =
199 (SemanticsUtils.hwreg_store_sp st.Types.snd sp) }
201 (** val eRTL_state : Joint_semantics.sem_state_params **)
203 { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
204 Joint_semantics.empty_regsT = (fun sp ->
205 Obj.magic { Types.fst =
206 (Identifiers.empty_map PreIdentifiers.RegisterTag); Types.snd =
207 (SemanticsUtils.init_hw_register_env sp) }); Joint_semantics.load_sp =
208 (Obj.magic get_hwsp); Joint_semantics.save_sp = (Obj.magic set_hwsp) }
210 (** val ertl_eval_move :
211 ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod
213 let ertl_eval_move env pr =
214 Monad.m_bind0 (Monad.max_def Errors.res0)
215 (match pr.Types.snd with
218 | ERTL.PSD r -> Obj.magic (ps_reg_retrieve env r)
219 | ERTL.HDW r -> Obj.magic (hw_reg_retrieve env r))
221 Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
223 match pr.Types.fst with
224 | ERTL.PSD r -> Obj.magic (ps_reg_store r v env)
225 | ERTL.HDW r -> Obj.magic (hw_reg_store r v env))
227 (** val ertl_allocate_local :
228 PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
229 Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod **)
230 let ertl_allocate_local reg lenv =
232 (Identifiers.add PreIdentifiers.RegisterTag lenv.Types.fst reg
233 ByteValues.BVundef); Types.snd = lenv.Types.snd }
235 (** val ertl_save_frame :
236 Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
237 Joint_semantics.state Errors.res **)
238 let ertl_save_frame x x0 st =
240 (Monad.m_bind0 (Monad.max_def Errors.res0)
242 (Joint_semantics.push_ra eRTL_state st.Joint_semantics.st_no_pc
243 st.Joint_semantics.pc)) (fun st' ->
244 Monad.m_bind0 (Monad.max_def Errors.res0)
246 (Errors.opt_to_res (List.Cons ((Errors.MSG
247 ErrorMessages.FrameErrorOnPush), List.Nil))
248 st'.Joint_semantics.st_frms)) (fun frms ->
249 Monad.m_return0 (Monad.max_def Errors.res0)
250 (Joint_semantics.set_frms eRTL_state
251 (Obj.magic (List.Cons ({ Types.fst =
252 (Obj.magic st'.Joint_semantics.regs).Types.fst; Types.snd =
253 st.Joint_semantics.pc.ByteValues.pc_block }, frms)))
254 (Joint_semantics.set_regs eRTL_state
255 (Obj.magic { Types.fst =
256 (Identifiers.empty_map PreIdentifiers.RegisterTag);
257 Types.snd = (Obj.magic st'.Joint_semantics.regs).Types.snd })
260 (** val ertl_pop_frame :
261 Joint_semantics.state -> (Joint_semantics.state,
262 ByteValues.program_counter) Types.prod Errors.res **)
263 let ertl_pop_frame st =
265 (Monad.m_bind0 (Monad.max_def Errors.res0)
267 (Errors.opt_to_res (List.Cons ((Errors.MSG
268 ErrorMessages.FrameErrorOnPop), List.Nil))
269 st.Joint_semantics.st_frms)) (fun frms ->
272 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
273 ErrorMessages.FramesEmptyOnPop), List.Nil)))
274 | List.Cons (hd, tl) ->
275 let { Types.fst = local_mem; Types.snd = bl } = hd in
277 Joint_semantics.set_regs eRTL_state
278 (Obj.magic { Types.fst = local_mem; Types.snd =
279 (Obj.magic st.Joint_semantics.regs).Types.snd })
280 (Joint_semantics.set_frms eRTL_state (Obj.magic tl) st)
282 Monad.m_bind2 (Monad.max_def Errors.res0)
283 (Obj.magic (Joint_semantics.pop_ra eRTL_state st')) (fun st'' pc ->
284 match Pointers.eq_block (Types.pi1 bl)
285 (Types.pi1 pc.ByteValues.pc_block) with
287 Obj.magic (Errors.OK { Types.fst = st''; Types.snd = pc })
289 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
290 ErrorMessages.BlockInFramesCorrupted), List.Nil))))))
292 (** val ertl_fetch_external_args :
293 AST.external_function -> Joint_semantics.state -> __ -> Values.val0
294 List.list Errors.res **)
295 let ertl_fetch_external_args _ =
296 failwith "AXIOM TO BE REALIZED"
298 (** val ertl_set_result :
299 Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
300 Joint_semantics.state Errors.res **)
301 let ertl_set_result _ =
302 failwith "AXIOM TO BE REALIZED"
304 (** val ps_reg_store_status :
305 Registers.register -> ByteValues.beval -> Joint_semantics.state ->
306 Joint_semantics.state Errors.res **)
307 let ps_reg_store_status dst v st =
308 let env = st.Joint_semantics.regs in
310 (Monad.m_bind0 (Monad.max_def Errors.res0)
311 (Obj.magic (ps_reg_store dst v (Obj.magic env))) (fun env' ->
312 Monad.m_return0 (Monad.max_def Errors.res0)
313 (Joint_semantics.set_regs eRTL_state env' st)))
315 (** val eval_ertl_seq :
316 AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
317 AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res **)
318 let eval_ertl_seq globals ge stm id st =
320 (Monad.m_bind0 (Monad.max_def Errors.res0)
322 (Errors.opt_to_res (Errors.msg ErrorMessages.FunctionNotFound)
323 (ge.Joint_semantics.stack_sizes id))) (fun framesize ->
325 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
326 (Nat.S (Nat.S Nat.O)))))))) framesize
329 | ERTL.Ertl_new_frame ->
330 Monad.m_bind0 (Monad.max_def Errors.res0)
331 (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
333 Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
334 (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
336 Monad.m_return0 (Monad.max_def Errors.res0)
337 (Joint_semantics.set_sp eRTL_state newsp st))
338 | ERTL.Ertl_del_frame ->
339 Monad.m_bind0 (Monad.max_def Errors.res0)
340 (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
342 Pointers.shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
343 (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
345 Monad.m_return0 (Monad.max_def Errors.res0)
346 (Joint_semantics.set_sp eRTL_state newsp st))
347 | ERTL.Ertl_frame_size dst ->
349 (ps_reg_store_status dst (ByteValues.BVByte framesize0) st))))
351 (** val eRTL_sem_uns : 'a1 Joint_semantics.sem_unserialized_params **)
353 { Joint_semantics.st_pars = eRTL_state; Joint_semantics.acca_store_ =
354 (Obj.magic ps_reg_store); Joint_semantics.acca_retrieve_ =
355 (Obj.magic ps_reg_retrieve); Joint_semantics.acca_arg_retrieve_ =
356 (Obj.magic ps_arg_retrieve); Joint_semantics.accb_store_ =
357 (Obj.magic ps_reg_store); Joint_semantics.accb_retrieve_ =
358 (Obj.magic ps_reg_retrieve); Joint_semantics.accb_arg_retrieve_ =
359 (Obj.magic ps_arg_retrieve); Joint_semantics.dpl_store_ =
360 (Obj.magic ps_reg_store); Joint_semantics.dpl_retrieve_ =
361 (Obj.magic ps_reg_retrieve); Joint_semantics.dpl_arg_retrieve_ =
362 (Obj.magic ps_arg_retrieve); Joint_semantics.dph_store_ =
363 (Obj.magic ps_reg_store); Joint_semantics.dph_retrieve_ =
364 (Obj.magic ps_reg_retrieve); Joint_semantics.dph_arg_retrieve_ =
365 (Obj.magic ps_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
366 (Obj.magic ps_arg_retrieve); Joint_semantics.pair_reg_move_ =
367 (Obj.magic ertl_eval_move); Joint_semantics.save_frame =
368 (Obj.magic ertl_save_frame); Joint_semantics.setup_call =
370 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
371 Joint_semantics.fetch_external_args = ertl_fetch_external_args;
372 Joint_semantics.set_result = (Obj.magic ertl_set_result);
373 Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
374 Joint_semantics.call_dest_for_main = (Obj.magic Types.It);
375 Joint_semantics.read_result = (fun x x0 x1 st ->
377 (Monad.m_return0 (Monad.max_def Errors.res0)
379 (SemanticsUtils.hwreg_retrieve
380 (Obj.magic st.Joint_semantics.regs).Types.snd)
381 I8051.registerRets))); Joint_semantics.eval_ext_seq =
382 (fun gl ge stm id -> eval_ertl_seq gl ge (Obj.magic stm) id);
383 Joint_semantics.pop_frame = (fun x x0 x1 x2 -> ertl_pop_frame) }
385 (** val eRTL_semantics : SemanticsUtils.sem_graph_params **)
387 { SemanticsUtils.sgp_pars =
388 (Joint.gp_to_p__o__stmt_pars__o__uns_pars ERTL.eRTL);
389 SemanticsUtils.sgp_sup = (fun _ -> eRTL_sem_uns);
390 SemanticsUtils.graph_pre_main_generator = ERTL.eRTL_premain }