source: src/joint/semanticsUtils.ma @ 2674

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