source: src/LIN/joint_LTL_LIN_semantics.ma @ 1415

Last change on this file since 1415 was 1415, checked in by sacerdot, 8 years ago
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
File size: 3.9 KB
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "joint/SemanticUtils.ma".
3
4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
5definition 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? *)
8definition 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
26definition 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
31definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
32definition 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.
37definition 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 *)
42definition 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*)
49axiom 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).
50axiom 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
52definition 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
56definition 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
66definition 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)).
Note: See TracBrowser for help on using the repository browser.