source: src/joint/semanticsUtils.ma @ 2675

Last change on this file since 2675 was 2675, checked in by tranquil, 8 years ago
  • a generic graph program transformation
File size: 5.1 KB
Line 
1include "joint/joint_semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5
6record hw_register_env : Type[0] ≝
7  { reg_env : BitVectorTrie beval 6
8  ; other_bit : bebit
9  }.
10
11definition empty_hw_register_env: hw_register_env ≝
12  mk_hw_register_env (Stub …) BBundef.
13
14include alias "ASM/BitVectorTrie.ma".
15
16definition hwreg_retrieve: hw_register_env → Register → beval ≝
17 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
18
19definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
20 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
21  (other_bit env).
22
23definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
24λv,env.mk_hw_register_env (reg_env env) v.
25
26definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
27λenv.
28let spl ≝ hwreg_retrieve env RegisterSPL in
29let sph ≝ hwreg_retrieve env RegisterSPH in
30! ptr ← pointer_of_address 〈spl, sph〉 ;
31match ptype ptr return λx.ptype ptr = x → res xpointer with
32[ XData ⇒ λprf.return «ptr, prf»
33| _ ⇒ λ_.Error … [MSG BadPointer]
34] (refl …).
35
36definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
37λenv,sp.
38let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
39hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
40
41(*** Store/retrieve on pseudo-registers ***)
42include alias "common/Identifiers.ma".
43
44record reg_sp : Type[0] ≝
45{ reg_sp_env :> identifier_map RegisterTag beval
46; stackp : xpointer
47}.
48
49definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
50
51definition reg_retrieve : register_env beval → register → res beval ≝
52 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
53
54definition reg_sp_store ≝ λreg,v,locals.
55! locals' ← reg_store reg v (reg_sp_env locals) ;
56return mk_reg_sp locals' (stackp locals).
57
58definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
59
60(*** Store/retrieve on hardware registers ***)
61
62definition init_hw_register_env: xpointer → hw_register_env ≝
63 λsp.hwreg_store_sp empty_hw_register_env sp.
64
65(******************************** GRAPHS **************************************)
66
67record sem_graph_params : Type[1] ≝
68{ sgp_pars : unserialized_params
69; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
70}.
71
72definition sem_graph_params_to_graph_params :
73  ∀pars : sem_graph_params.graph_params ≝
74  λpars.mk_graph_params (sgp_pars pars).
75
76coercion graph_params_from_sem_graph_params nocomposites :
77  ∀pars : sem_graph_params.
78  graph_params ≝ sem_graph_params_to_graph_params
79  on _pars : sem_graph_params to graph_params.
80
81definition sem_graph_params_to_sem_params :
82  ∀pars : sem_graph_params.
83  sem_params ≝
84  λpars.
85  mk_sem_params
86    (pars : graph_params)
87    (sgp_sup pars ?)
88    (word_of_identifier ?)
89    (an_identifier ?)
90    ? (refl …).
91* #p % qed.
92
93coercion sem_params_from_sem_graph_params :
94  ∀pars : sem_graph_params.
95  sem_params ≝ sem_graph_params_to_sem_params
96  on _pars : sem_graph_params to sem_params.
97
98
99(******************************** LINEAR **************************************)
100
101lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
102@pos_elim [%]
103#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
104
105record sem_lin_params : Type[1] ≝
106{ slp_pars : unserialized_params
107; slp_sup : ∀F.sem_unserialized_params slp_pars F
108}.
109
110definition sem_lin_params_to_lin_params :
111  ∀pars : sem_lin_params.lin_params ≝
112  λpars.mk_lin_params (slp_pars pars).
113
114coercion lin_params_from_sem_lin_params nocomposites :
115  ∀pars : sem_lin_params.
116  lin_params ≝ sem_lin_params_to_lin_params
117  on _pars : sem_lin_params to lin_params.
118
119definition sem_lin_params_to_sem_params :
120  ∀pars : sem_lin_params.
121  sem_params ≝
122  λpars.
123  mk_sem_params
124    (pars : lin_params)
125    (slp_sup pars ?)
126    succ_pos_of_nat
127    (λp.pred (nat_of_pos p))
128    ??.
129[ #n >nat_succ_pos %
130| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
131] qed.
132
133coercion sem_params_from_sem_lin_params :
134  ∀pars : sem_lin_params.
135  sem_params ≝ sem_lin_params_to_sem_params
136  on _pars : sem_lin_params to sem_params.
137
138
139lemma fetch_statement_eq : ∀p:sem_params.∀g.
140  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
141  ∀i,fn,s.
142  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
143  let pt ≝ point_of_pc … ptr in
144  stmt_at … (joint_if_code … fn) pt = Some ? s →
145  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
146#p #g #ge #ptr #i #f #s #EQ1 #EQ2
147whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
148>EQ2 %
149qed.
150
151lemma fetch_statement_inv : ∀p:sem_params.∀g.
152  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
153  ∀i,fn,s.
154  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
155  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
156  let pt ≝ point_of_pc p ptr in
157  stmt_at … (joint_if_code … fn) pt = Some ? s.
158#p #g #ge #ptr #i #fn #s #H
159elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
160elim (bind_inversion ????? H) #s' * #H
161lapply (opt_eq_from_res ???? H) -H #EQ2
162whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
163qed.
Note: See TracBrowser for help on using the repository browser.