source: src/LIN/joint_LTL_LIN_semantics.ma @ 1383

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

Potential bug fixed and bug found: the way pointers and labels are put in
bijection must be different between LIN and graph-like languages (bug fixed).
Moreover, in both cases it must be possible to retrieve the function from the
address and the easiest (only?) way to do that is to use the block of the
address to store the block of the function, and put the offsets in bijection
with labels/offsets, preventing pointer mangling since the pointer is in
the Code region (found, to be fixed).

File size: 3.6 KB
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "joint/SemanticUtils.ma".
3
4(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
5definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
6 λsuccT,succ,pointer_of_label.
7 mk_more_sem_params ?
8  unit hw_register_env succ
9   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
10    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
11    (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
12    (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
13     (λlocals,dest_src.
14       match dest_src with
15       [ from_acc reg ⇒
16          do v ← hwreg_retrieve locals RegisterA ;
17          hwreg_store reg v locals
18       | to_acc reg ⇒
19          do v ← hwreg_retrieve locals reg ;
20          hwreg_store RegisterA v locals ])
21     pointer_of_label.
22
23definition ltl_lin_sem_params:
24 ∀succT,succ,pointer_of_label. sem_params ≝
25 λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).
26
27
28definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
29definition ltl_lin_pop_frame:
30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res ((state … (ltl_lin_sem_params … succ pointer_of_label)) × address) ≝
31 λ_.λ_.λ_.fetch_ra ….
32definition ltl_lin_save_frame:
33 ∀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)) ≝
34 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
35
36definition ltl_lin_more_sem_params1 : ∀succT,succ,pointer_of_label.more_sem_params1 … ltl_lin_params1 ≝
37 λsuccT,succ,pointer_of_label.
38 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
39  ltl_lin_init_locals (ltl_lin_pop_frame …) (ltl_lin_save_frame …).
40
41(*CSC: XXXXX, for is_final only *)
42axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
43
44(*CSC: XXXX, for external functions only*)
45axiom 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).
46axiom 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)).
47
48definition 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)))
49 ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
50@abs qed.
51
52definition ltl_lin_more_sem_params2:
53 ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
54 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
55 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
56  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
57   (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
58   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
59
60definition ltl_lin_fullexec ≝
61 λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
62  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.