source: src/joint/semantics_blocks.ma @ 1882

Last change on this file since 1882 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: 10.3 KB
Line 
1include "joint/blocks.ma".
2include "joint/semantics_paolo.ma".
3
4(* WARNING: all the following breaks apart if statements are allowed to depend
5   on flow. Execution of blocks does not update flow information in the state
6   (e.g. the program counter) until the end *)
7
8definition goto_no_seq : ∀g.∀p:sem_params.genv g p → label →
9  state p → Z → res (state_pc p) ≝ λg,p,ge,lbl,st,id.
10      ! newpc ← pointer_of_label ? p … ge
11        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) lbl ;
12      return mk_state_pc … st newpc. % qed.
13
14lemma goto_no_seq_to_normal : ∀p : sem_params.∀g,ge.∀st : state_pc p.∀id,lbl.
15  block_id (pblock (pc p st)) = id →
16  goto_no_seq g p ge lbl st id = goto g p ge lbl st.
17#p #g #ge * #st ** #typ * #r #id
18#H inversion H [1,3: #r'] #id'
19#EQ1 #EQ2 #EQ3 #o #EQ4 #id'' #lbl #EQ5 destruct
20whd in match goto_no_seq;
21whd in match goto; normalize nodelta //
22qed.
23
24(* executes a block of instructions, until its end or before if a
25   function call or a redirection is encountered. If executed until end,
26   or is a non-tail call is encountered, the next program counter must be
27   provided *)
28let rec eval_block_cont globals (p:sem_params) (ge : genv globals p)
29  (st : state p) id (b : block_cont p globals) (dst : option cpointer) on b :
30    IO io_out io_in (trace×(state_pc p)) ≝
31  match b with
32  [ Skip ⇒
33    ! nxt ← opt_to_res … (msg SuccessorNotProvided) dst ;
34    return 〈E0, mk_state_pc ? st nxt〉
35  | Final s ⇒
36    ! 〈flow, tr, st'〉 ← eval_statement_no_seq … ge st s;
37    ! st ← eval_stmt_flow_no_seq … ge st' id flow;
38    return 〈tr, st〉
39  | Cons hd tl ⇒
40    ! 〈flow, tr1, st'〉 ← eval_step ?? ge st hd ;
41    match flow with
42    [ Proceed ⇒
43      ! 〈tr2, st〉 ← eval_block_cont globals p ge st id tl dst ;
44      return 〈tr1 ⧺ tr2, st〉
45    | Init id fn args dest ⇒
46      ! ra ← opt_to_res … (msg SuccessorNotProvided) dst ;
47      let st' ≝ set_frms … (save_frame … ra dest st) st in
48      ! st ← do_call ?? ge st' id fn args ;
49      return 〈tr1, st〉
50    | Redirect l ⇒
51      ! st ← goto_no_seq ? p … ge l st id ;
52      return 〈tr1, st〉
53    ]
54  ].
55 
56lemma Eapp_E0 : ∀tr1 : trace.tr1 ⧺ E0 = tr1 ≝ append_nil ….
57
58(* just like repeat, but without the full_exec infrastructure *)
59let rec repeat_eval_state n globals (p:sem_params) (ge : genv globals p)
60  (st : state_pc p) on n :
61    IO io_out io_in (trace×(state_pc p)) ≝
62match n with
63[ O ⇒ return 〈E0, st〉
64| S k ⇒
65  ! 〈tr1, st〉 ← eval_state globals p ge st ;
66  ! 〈tr2, st〉 ← repeat_eval_state k globals p ge st ;
67  return 〈tr1 ⧺ tr2, st〉
68].
69
70lemma repeat_eval_state_plus : ∀n1,n2,globals, p, ge, st.
71  repeat_eval_state (n1 + n2) globals p ge st =
72  ! 〈tr1, st〉 ← repeat_eval_state n1 globals p ge st ;
73  ! 〈tr2, st〉 ← repeat_eval_state n2 globals p ge st ;
74  return 〈tr1 ⧺ tr2, st〉.
75#n1 elim n1 -n1 [| #n1 #IH]
76#n2 #globals #p #ge #st
77[ >m_return_bind change with n2 in match (0 + n2);
78  change with (! x ← ? ; ?) in ⊢ (???%);
79  <(m_bind_return … (repeat_eval_state ?????)) in ⊢ (??%?);
80  @m_bind_ext_eq * //
81| change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
82  change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S n1) ????);
83  >m_bind_bind in ⊢ (???%);
84  @m_bind_ext_eq * #tr1 #st1
85  >IH >m_bind_bind in ⊢ (??%?); >m_bind_bind in ⊢ (???%);
86  @m_bind_ext_eq * #tr2 #st2 >m_return_bind
87  >m_bind_bind @m_bind_ext_eq * #tr3 #st3 >m_return_bind >Eapp_assoc %
88]
89qed.
90
91lemma repeat_eval_state_one : ∀globals, p, ge, st.
92  repeat_eval_state 1 globals p ge st = eval_state globals p ge st.
93#globals #p #ge #st
94change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
95<(m_bind_return … (eval_state ????)) in ⊢ (???%);
96@m_bind_ext_eq * #tr1 #st1 >m_return_bind >Eapp_E0 %
97qed.
98
99lemma If_true : ∀A.∀b : bool.∀f : b → A.∀g.∀prf' : bool_to_Prop b.If b then with prf do f prf else with prf do g prf = f prf'.
100#A * #f #g * normalize % qed.
101
102lemma eval_tunnel_step :
103  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
104  fetch_function … ge (pc … st) = OK … fn →
105  point_of_pointer ? p … (pc … st) = OK … src →
106  src ~~> dst in joint_if_code … fn →
107  eval_state g p ge st =
108    OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
109#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
110change with (! s ← ? ; ?) in match (eval_state ????);
111change with (! fn ← ? ; ?) in match (fetch_statement ?????);
112>pc_pt in ⊢ (??%?); >m_return_bind
113>fetch_fn in ⊢ (??%?); >m_return_bind
114>EQ1 in ⊢ (??%?);  >m_return_bind
115>EQ2 in ⊢ (??%?);  >m_return_bind
116change with (! st ← ? ; ?) in ⊢ (??%?);
117whd in match eval_stmt_flow; normalize nodelta
118change with (! ptr ← ? ; ?) in match (goto ?????);
119whd in match pointer_of_label; normalize nodelta
120>fetch_fn in ⊢ (??%?); >m_return_bind
121>EQ2 in ⊢ (??%?); >m_return_bind %
122qed.
123
124
125lemma fetch_function_from_block_eq :
126  ∀p,g,ge.
127  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
128  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
129#p #g #ge #ptr1 #ptr2 #EQ
130whd in match fetch_function; normalize nodelta >EQ
131@m_bind_ext_eq // qed.
132
133lemma eval_tunnel :
134  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
135  fetch_function … ge (pc … st) = OK … fn →
136  point_of_pointer ? p … (pc … st) = OK … src →
137  src ~~>^* dst in joint_if_code … fn →
138  ∃n.repeat_eval_state n g p ge st =
139    OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
140#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
141lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
142elim through [2: #hd #tl #IH]
143#st #src #fetch_fn #pc_pt
144[2: #EQ <EQ %{0}
145  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
146* #H1 #H2
147letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
148elim (IH st' … H2)
149[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
150  @pointer_of_point_block
151|2:
152  whd in match st'; >point_of_pointer_of_point %
153]
154#n' #EQ %{(S n')}
155change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
156>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
157>EQ  >m_return_bind %
158qed.
159
160lemma eval_tunnel_plus :
161  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
162  fetch_function … ge (pc … st) = OK … fn →
163  point_of_pointer ? p … (pc … st) = OK … src →
164  src ~~>^+ dst in joint_if_code … fn →
165  ∃n.repeat_eval_state (S n) g p ge st =
166    OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
167#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
168letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
169elim (eval_tunnel … ge st' … H2)
170[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
171  @pointer_of_point_block
172|2:
173  whd in match st'; >point_of_pointer_of_point %
174]
175#n #EQ %{n}
176change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
177>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
178>EQ  >m_return_bind %
179qed.
180
181lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
182  ∀fn,pt,s.
183  fetch_function … ge ptr = OK … fn →
184  point_of_pointer ? p … ptr = OK … pt →
185  stmt_at … (joint_if_code … fn) pt = Some ? s →
186  fetch_statement ? p … ge ptr = OK … s.
187#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
188whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind
189>EQ1 >m_return_bind >EQ3 %
190qed.
191
192lemma eval_block_cont_in_code :
193  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
194  fetch_function … ge (pc … st) = OK … fn →
195  point_of_pointer ? p … (pc … st) = OK … src →
196  src ~❨B❩~> dst in joint_if_code … fn →
197  ∃n.repeat_eval_state n g p ge st =
198    eval_block_cont g p ge st (block_id (pblock (pc … st))) B (! x ← dst; return pointer_of_point … p (pc … st) x).
199#p #g #ge #st #fn #src #B lapply src -src
200lapply st -st elim B [|#s|#s #B' #IH]
201#st #src #dst #fetch_fn #pc_pt
202[ cases dst [*] #z @eval_tunnel assumption
203| cases dst [2: #z *]]
204* #mid * #tunn [#H | * #n * #H #G ]
205  elim (eval_tunnel … fetch_fn pc_pt tunn)
206  #n
207  letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
208  #EQ1
209  cut (point_of_pointer ? p … (pc … st') = OK … mid)
210  [1,3:
211    whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
212  cut (fetch_function p … ge (pc … st') = OK … fn)
213  [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
214    @pointer_of_point_block] #fetch_fn'
215  [ %{(n + 1)}
216  >repeat_eval_state_plus >EQ1 >m_return_bind
217  >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
218  change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
219  change with (! s ← ? ; ?) in match (eval_state ????);
220  >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
221  >m_bind_bind
222  change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
223  cases s *
224 
225  @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
226  >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
227  change with (! fn ← ? ; ?) in match (fetch_statement ?????);
228  >m_bind_bind in ⊢ (??%?);
229  change with (pointer_of_point ????) in match (pc ??);
230  >point_of_pointer_of_point >m_return_bind
231  >(fetch_function_from_block_eq ???? (pc … st))
232  [2: @pointer_of_point_block ]
233  >fetch_fn >m_return_bind >H2 >m_return_bind
234  >m_bind_bind
235  change with (! x ← ? ; ?) in ⊢ (???%);
236  >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
237  >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
238  >H1 in ⊢ (??(????%?)?);
239  whd in ⊢ (??(λ_.???%));
240elim b
241[ #st #dst #fetch_fn #prf #through
242  #H elim (block_cont_to_tunnel … H) #dst'
243  * #EQdst >EQdst >m_return_bind #G
244  elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
245  >EQ %
246|
247
248 #dst #fetch_fn #prf #through
249lapply prf -prf lapply fetch_fn -fetch_fn
250lapply b -b lapply st -st
251elim through [2: #hd #tl #IH]
252[2:
253 
254#st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
255normalize in ⊢(%→?);
256[8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
257[ * || * | * #lbl
258 * #lbl * [*] #H1 #H2 [#H3]
259 
260let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
261  (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
262  match b with
263  [ Skip ⇒
264    match following with
265    [ Some l ⇒ succ_pc p p
Note: See TracBrowser for help on using the repository browser.