source: src/LIN/semantics.ma @ 1377

Last change on this file since 1377 was 1377, checked in by sacerdot, 9 years ago

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

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