source: src/joint/semanticsUtils_paolo.ma @ 2125

Last change on this file since 2125 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 8.9 KB
Line 
1include "joint/semantics_paolo.ma".
2include alias "common/Identifiers.ma".
3
4(*** Store/retrieve on pseudo-registers ***)
5
6axiom BadRegister : String.
7
8definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
9
10definition reg_retrieve : register_env beval → register → res beval ≝
11 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
12
13(*** Store/retrieve on hardware registers ***)
14
15definition init_hw_register_env: address → hw_register_env ≝
16 λaddr.
17  let 〈dpl,dph〉 ≝ addr in
18  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
19   hwreg_store RegisterDPL dpl env.
20
21(******************************** GRAPHS **************************************)
22
23definition graph_pointer_of_label : cpointer → label → res cpointer ≝
24  λoldpc,l.
25  return (mk_pointer Code
26   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer).
27% qed.
28
29definition graph_label_of_pointer: pointer → res label ≝
30 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
31
32definition graph_fetch_statement:
33 ∀pars : graph_params.
34 ∀sem_pars : sem_state_params.
35 ∀globals.
36  genv globals pars →
37  cpointer →
38  res (joint_statement pars globals) ≝
39 λpars,sem_pars,globals,ge,p.
40  do f ← fetch_function … ge p ;
41  do l ← graph_label_of_pointer p;
42  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
43
44definition make_sem_graph_params :
45  ∀pars : graph_params.
46  ∀g_pars : more_sem_genv_params pars.
47  sem_params ≝
48  λpars,g_pars.
49  mk_sem_params
50    pars
51    (mk_more_sem_params
52      pars
53      g_pars
54      graph_pointer_of_label
55      (λ_.λ_.graph_pointer_of_label)
56      (graph_fetch_statement ? g_pars)
57    ).
58   
59(******************************** LINEAR **************************************)
60check mk_pointer
61definition lin_succ_p: cpointer → unit → res cpointer :=
62 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
63[%| cases ptr //] qed.
64
65axiom BadLabel: String.
66
67definition lin_pointer_of_label:
68 ∀pars : lin_params.
69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝
70 λpars,globals,ge,old,l.
71  do fn ← fetch_function … ge old ;
72  do pos ←
73   opt_to_res ? [MSG BadLabel]
74    (position_of ?
75      (λs. let 〈l',x〉 ≝ s in
76        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
77     (joint_if_code … pars fn)) ;
78  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
79% qed.
80
81definition lin_fetch_statement:
82 ∀pars : lin_params.
83 ∀sem_pars : sem_state_params.
84 ∀globals.
85 genv globals pars → cpointer → res (joint_statement pars globals) ≝
86 λpars,sem_pars,globals,ge,ppc.
87  do fn ← fetch_function … ge ppc ;
88  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
89  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
90  return (\snd found).
91
92definition make_sem_lin_params :
93  ∀pars : lin_params.
94  ∀g_pars : more_sem_genv_params pars.
95  sem_params ≝
96  λpars,g_pars.
97  mk_sem_params
98    pars
99    (mk_more_sem_params
100      pars
101      g_pars
102      lin_succ_p
103      (lin_pointer_of_label ?)
104      (lin_fetch_statement ? g_pars)
105    ).
106   
107definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
108  λp,globals,stp.match stp with
109  [ COND _ _ ⇒ false
110  | CALL_ID _ _ _ ⇒ false
111  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
112    match ext_step_labels … c' with
113    [ nil ⇒ true
114    | _ ⇒ false
115    ]
116  | _ ⇒ true
117  ].
118
119definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
120  λp,globals,stp.match stp with
121  [ sequential _ _ ⇒ false
122  | _ ⇒ true
123  ].
124
125inductive s_block (p : params) (globals : list ident) : Type[0] ≝
126  | Skip : s_block p globals
127  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
128  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
129  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.
130
131include "utilities/bind_new.ma".
132
133definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
134
135definition Bcons ≝ λp : params.λglobals.
136    λs : Σs.bool_to_Prop (step_unbranching p globals s).
137    λB : Block p globals.
138    ! b ← B ; return Cons ?? s b.
139
140interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
141
142let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
143  match b1 with
144  [ Skip ⇒ true
145  | FinStep _ ⇒ false
146  | FinStmt _ ⇒ false
147  | Cons _ tl ⇒ is_unbranching ?? tl
148  ].
149
150let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
151  match b1 with
152  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
153  | bnew f ⇒ ∀x.Is_unbranching … (f x)
154  ].
155
156let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
157  match b1 return λx.is_unbranching ?? x → ? with
158  [ Skip ⇒ λ_.b2
159  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
160  | _ ⇒ Ⓧ
161  ].
162
163definition s_block_append ≝
164  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
165  match b1 with
166  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].
167
168definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
169  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
170  λp,globals. ?.
171* #b elim b -b
172[ #b #H @bret @b @H
173| #f #IH #H @bnew #x @(IH x) @H
174]
175qed.
176
177lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
178#p #globals * #b elim b
179[ //
180| #f #IH #H @bnew_proper
181  #x @IH
182]
183qed.
184 
185definition Block_append ≝
186  λp,globals.λB : Σb.Is_unbranching … b.λB'.
187  ! b1 ← Is_to_is_unbr … B;
188  ! b2 ← B';
189  return s_block_append p globals b1 b2.
190
191definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
192
193let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
194    s_block p globals ≝
195  match l  with
196  [ nil ⇒ Skip ??
197  | cons hd tl ⇒
198    If step_unbranching … hd then with prf do
199      Cons ?? hd (step_list_to_s_block ?? tl)
200    else with prf do
201      FinStep ?? hd
202  ]. [assumption | >prf % ] qed.
203 
204definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
205  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).
206
207record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
208  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
209  ; genv_rel : genv globals p1 → genv globals p2 → Prop
210  ; pc_rel : cpointer → cpointer → Prop
211  ; st_rel : state p1 → state p2 → Prop
212  ; stmt_rel : joint_statement p1 globals → Block
213  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
214  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
215  }.
216 
217(* move *)
218definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
219 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
220  match pty return λpty. ? → pty = XData → ? with
221   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
222   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
223[@(pi2 … p) |6: // |7: %] destruct (abs)
224qed.
225
226definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
227cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
228lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
229%{«mk_pointer ? (mk_block ? z) H o,I»}
230% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
231qed.
232
233definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
234  λp1,p2,R,st1,st2.
235    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
236    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
237    sp_rel p1 p2 R
238      (safe_address_of_xdata_pointer (sp … st1))
239      (safe_address_of_xdata_pointer (sp … st2)) ∧
240    isp_rel p1 p2 R
241      (safe_address_of_xdata_pointer (isp … st1))
242      (safe_address_of_xdata_pointer (isp … st2)) ∧
243    sp_rel p1 p2 R
244      (safe_address_of_xdata_pointer (sp … st1))
245      (safe_address_of_xdata_pointer (sp … st2)) ∧
246    carry … st1 = carry … st2 ∧
247    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
248    mem_rel p1 p2 R (m … st1) (m … st2).
249elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
250elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
251assumption
252qed.
253 elim st2
254-st1 -st2 #st2 ** #good_pc2 # ∧
255    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
256    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
257    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
258
259
260
Note: See TracBrowser for help on using the repository browser.