1 | include "joint/SemanticUtils.ma". |
---|
2 | include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) |
---|
3 | |
---|
4 | definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. |
---|
5 | definition lin_pop_frame: unit → res unit ≝ λ_. OK … it. |
---|
6 | definition lin_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it. |
---|
7 | |
---|
8 | (*CSC: XXXX*) |
---|
9 | axiom lin_succ_pc: unit → address → address. |
---|
10 | |
---|
11 | (*CSC: re-organize to take succ_pc out of lin_more_sem_params to share the |
---|
12 | following definition between LTL and LIN *) |
---|
13 | definition lin_more_sem_params: more_sem_params lin_params_ := |
---|
14 | mk_more_sem_params lin_params_ |
---|
15 | unit hw_register_env lin_succ_pc lin_pop_frame lin_save_frame |
---|
16 | hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) |
---|
17 | (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) |
---|
18 | (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL) |
---|
19 | (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH) |
---|
20 | (λlocals,dest_src. |
---|
21 | match dest_src with |
---|
22 | [ from_acc reg ⇒ |
---|
23 | do v ← hwreg_retrieve locals RegisterA ; |
---|
24 | hwreg_store reg v locals |
---|
25 | | to_acc reg ⇒ |
---|
26 | do v ← hwreg_retrieve locals reg ; |
---|
27 | hwreg_store RegisterA v locals ]) |
---|
28 | pointer_of_label. |
---|
29 | definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params. |
---|
30 | |
---|
31 | (*CSC: XXXXXXXXXX *) |
---|
32 | axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state lin_sem_params → res (pre_lin_statement globals). |
---|
33 | |
---|
34 | (*CSC: XXXXX, for is_final only *) |
---|
35 | axiom lin_fetch_result: state lin_sem_params → nat → res val. |
---|
36 | |
---|
37 | (*CSC: XXXX, for external functions only*) |
---|
38 | axiom lin_fetch_external_args: external_function → state lin_sem_params → res (list val). |
---|
39 | axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params). |
---|
40 | |
---|
41 | definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params)) |
---|
42 | ≝ λglobals,ge,abs. ⊥. |
---|
43 | @abs qed. |
---|
44 | |
---|
45 | definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝ |
---|
46 | λglobals. |
---|
47 | mk_more_sem_params2 … lin_more_sem_params lin_init_locals |
---|
48 | (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result |
---|
49 | (lin_exec_extended …). |
---|
50 | |
---|
51 | definition lin_fullexec ≝ |
---|
52 | joint_fullexec … (λp. lin_more_sem_params2 (prog_var_names … p)). |
---|