1 | include "LIN/joint_LTL_LIN.ma". |
---|
2 | include "joint/SemanticUtils.ma". |
---|
3 | |
---|
4 | definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e). |
---|
5 | definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r). |
---|
6 | |
---|
7 | (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *) |
---|
8 | definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) := |
---|
9 | λsuccT,succ,pointer_of_label. |
---|
10 | mk_more_sem_params ? |
---|
11 | unit it hw_register_env init_hw_register_env 0 it succ |
---|
12 | hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA) |
---|
13 | (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB) |
---|
14 | (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL) |
---|
15 | (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH) |
---|
16 | (λlocals,dest_src. |
---|
17 | match dest_src with |
---|
18 | [ from_acc reg ⇒ |
---|
19 | do v ← hw_reg_retrieve locals RegisterA ; |
---|
20 | hw_reg_store reg v locals |
---|
21 | | to_acc reg ⇒ |
---|
22 | do v ← hw_reg_retrieve locals reg ; |
---|
23 | hw_reg_store RegisterA v locals ]) |
---|
24 | pointer_of_label. |
---|
25 | |
---|
26 | definition ltl_lin_sem_params: |
---|
27 | ∀succT,succ,pointer_of_label. sem_params ≝ |
---|
28 | λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label). |
---|
29 | |
---|
30 | |
---|
31 | definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. |
---|
32 | definition ltl_lin_pop_frame: |
---|
33 | ∀succT,succ,pointer_of_label,codeT,lookup. |
---|
34 | ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → |
---|
35 | state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝ |
---|
36 | λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t. |
---|
37 | definition ltl_lin_save_frame: |
---|
38 | ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝ |
---|
39 | λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l. |
---|
40 | |
---|
41 | (* The following implementation only works for functions that return 32 bits *) |
---|
42 | definition ltl_lin_result_regs: |
---|
43 | ∀succT,succ,pointer_of_label,codeT,lookup. |
---|
44 | ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → |
---|
45 | state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝ |
---|
46 | λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets. |
---|
47 | |
---|
48 | (*CSC: XXXX, for external functions only*) |
---|
49 | axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val). |
---|
50 | axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)). |
---|
51 | |
---|
52 | definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label))) |
---|
53 | ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥. |
---|
54 | @abs qed. |
---|
55 | |
---|
56 | definition ltl_lin_more_sem_params2: |
---|
57 | ∀succT,succ,pointer_of_label,codeT,lookup,fetch. |
---|
58 | ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝ |
---|
59 | λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals. |
---|
60 | mk_more_sem_params2 … |
---|
61 | (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label) |
---|
62 | (fetch globals) (load_ra …) (ltl_lin_result_regs …) |
---|
63 | ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …) |
---|
64 | (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …). |
---|
65 | |
---|
66 | definition ltl_lin_fullexec ≝ |
---|
67 | λsuccT,succ,pointer_of_label,codeT,lookup,fetch. |
---|
68 | joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)). |
---|