source: src/LIN/semantics.ma @ 1324

Last change on this file since 1324 was 1324, checked in by sacerdot, 10 years ago

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

File size: 2.6 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) ≝ λst. OK … st.
29definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
30
31definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
32 mk_more_sem_params1 ? lin_params1 lin_more_sem_params
33  lin_init_locals lin_pop_frame lin_save_frame.
34
35(*CSC: XXXXXXXXXX *)
36axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state lin_sem_params → res (pre_lin_statement globals).
37
38(*CSC: XXXXX, for is_final only *)
39axiom lin_fetch_result: state lin_sem_params → nat → res val.
40
41(*CSC: XXXX, for external functions only*)
42axiom lin_fetch_external_args: external_function → state lin_sem_params → res (list val).
43axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params).
44
45definition 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))
46 ≝ λglobals,ge,abs. ⊥.
47@abs qed.
48
49definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝
50 λglobals.
51  mk_more_sem_params2 … lin_more_sem_params1
52   (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result
53    (lin_exec_extended …).
54
55definition lin_fullexec ≝
56 joint_fullexec … (λp. lin_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.