Changeset 2532
 Timestamp:
 Dec 5, 2012, 6:57:16 PM (7 years ago)
 Location:
 src/joint
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r2490 r2532 80 80 ; snd_arg : Type[0] (* second argument of binary op *) 81 81 ; pair_move: Type[0] (* argument of move instructions *) 82 ; call_spec: Type[0] (* type of call (ident/pointer) *) 82 83 ; call_args: Type[0] (* arguments of function calls *) 83 84 ; call_dest: Type[0] (* possible destination of function computation *) 84 85 (* other instructions not fitting in the general framework *) 85 86 ; ext_seq : Type[0] 87 ; ext_seq_labels : ext_seq → list label 86 88 ; has_tailcalls : bool 87 89 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) … … 106 108  LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals 107 109  STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals 108  CALL: (ident + dpl_arg p×(dph_arg p))→ call_args p → call_dest p → joint_seq p globals110  CALL: call_spec p → call_args p → call_dest p → joint_seq p globals 109 111  extension_seq : ext_seq p → joint_seq p globals. 110 112 … … 145 147 λp, globals.λs : joint_step p globals. 146 148 match s with 147 [ step_seq s ⇒ [ ] 149 [ step_seq s ⇒ 150 match s with 151 [ extension_seq ext ⇒ ext_seq_labels … ext 152  _ ⇒ [ ] 153 ] 148 154  COND _ l ⇒ [l] 149 155 ]. … … 157 163 ; succ : Type[0] 158 164 ; succ_label : succ → option label 159 }. 165 ; has_fcond : bool 166 }. 160 167 161 168 inductive joint_fin_step (p: unserialized_params): Type[0] ≝ … … 163 170  RETURN: joint_fin_step p 164 171  TAILCALL : 165 has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p))→172 has_tailcalls p → call_spec p → 166 173 call_args p → joint_fin_step p. 167 174 … … 174 181 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 175 182  sequential: joint_step p globals → succ p → joint_statement p globals 176  final: joint_fin_step p → joint_statement p globals. 183  final: joint_fin_step p → joint_statement p globals 184  FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals. 177 185 178 186 coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. … … 193 201 194 202 (* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *) 195 203 (* 196 204 definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). 197 205 unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)). … … 206 214 ]. normalize in pt_prf; 207 215 >abs in pt_prf; // qed. 216 *) 208 217 209 218 definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals) ≝ … … 234 243 [ sequential c _ ⇒ step_labels … c 235 244  final c ⇒ fin_step_labels … c 245  FCOND _ _ l1 l2 ⇒ [l1 ; l2] 236 246 ]. 237 247 … … 316 326 λlp : lin_params. 317 327 mk_params 318 (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) )328 (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true) 319 329 (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) 320 330 (* code_point ≝ *)ℕ … … 358 368 λgp : graph_params. 359 369 mk_params 360 (mk_stmt_params (g_u_pars gp) label (Some ?) )370 (mk_stmt_params (g_u_pars gp) label (Some ?) false) 361 371 (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) 362 372 (* code_point ≝ *)label … … 403 413 joint_if_stacksize: nat; 404 414 joint_if_code : codeT p globals ; 405 joint_if_entry : point_in_code … joint_if_code;406 joint_if_exit : point_in_code … joint_if_code415 joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ; 416 joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) 407 417 }. 408 418 
src/joint/TranslateUtils.ma
r2443 r2532 270 270  final inst ⇒ 271 271 b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def 272  FCOND abs _ _ _ ⇒ Ⓧabs 272 273 ] in 273 274 foldi … f (joint_if_code … def) empty. … … 297 298  final inst ⇒ 298 299 adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def 300  FCOND abs _ _ _ ⇒ Ⓧabs 299 301 ] in 300 302 foldi … f (joint_if_code … def) empty. 
src/joint/linearise.ma
r2529 r2532 1 include "joint/TranslateUtils.ma". 2 include " common/extraGlobalenvs.ma".1 (* include "joint/TranslateUtils.ma". *) 2 include "joint/Joint.ma". 3 3 include "utilities/hide.ma". 4 4 5 5 definition graph_to_lin_statement : 6 6 ∀p : unserialized_params.∀globals. 7 ∀A.identifier_map LabelTag A → 7 8 joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ 8 λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params ?) ? with 9 [ sequential c _ ⇒ sequential … c it 9 λp,globals,A,visited,stmt. 10 match stmt return λ_.joint_statement (mk_lin_params ?) ? with 11 [ sequential c nxt ⇒ 12 match c with 13 [ COND a ltrue ⇒ 14 if nxt ∈ visited then FCOND … I a ltrue nxt else 15 sequential (mk_lin_params p) … c it 16  _ ⇒ sequential … c it 17 ] 10 18  final c ⇒ final … c 19  FCOND abs _ _ _ ⇒ Ⓧabs 11 20 ]. 12 21 22 (* 13 23 lemma graph_to_lin_labels : 14 24 ∀p : unserialized_params.∀globals,s. … … 17 27 #p#globals * [//] * // 18 28 qed. 29 *) 19 30 20 31 (* discard all elements passing test, return first element failing it *) … … 59 70 list lo ≡ codeT lp globals. 60 71 61 62 72 definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. 63 73 λentry : label. … … 68 78 (lookup ?? visited' entry = Some ? 0) 69 79 (required' ⊆ visited')) 70 (∃last.stmt_at … generated' 0 = Some ? (final … last))) 80 ((∃last.stmt_at … generated' 0 = Some ? (final … last)) ∨ 81 (∃a,ltrue,lfalse.stmt_at … generated' 0 = Some ? (FCOND … I a ltrue lfalse)))) 71 82 (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated'))) 72 83 (∀l,n.lookup ?? visited' l = Some ? n → 73 84 And (bool_to_Prop (code_has_label … (rev ? generated') l)) 74 (∃s.And (And85 (∃s.And 75 86 (lookup … g l = Some ? s) 76 (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) 77 (opt_All ? 78 (λnext.Or (lookup … visited' next = Some ? (S n)) 79 (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉)) 80 (stmt_implicit_label … s)))))). 87 (match s with 88 [ sequential s' nxt ⇒ 89 match s' with 90 [ step_seq _ ⇒ 91 And 92 (nth_opt … n (rev … generated') = 93 Some ? 〈Some ? l, sequential … s' it〉) 94 (Or (lookup … visited' nxt = Some ? (S n)) 95 (nth_opt … (S n) (rev … generated') = 96 Some ? 〈None ?, GOTO … nxt〉)) 97  COND a ltrue ⇒ 98 Or 99 (And (nth_opt … n (rev … generated') = 100 Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉) 101 (lookup … visited' nxt = Some ? (S n))) 102 (nth_opt … n (rev … generated') = 103 Some ? 〈Some ? l, FCOND … I a ltrue nxt〉) 104 ] 105  final s' ⇒ 106 nth_opt … n (rev … generated') = 107 Some ? 〈Some ? l, final … s'〉 108  FCOND abs _ _ _ ⇒ Ⓧabs 109 ]))))). 81 110 82 111 unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit. … … 85 114 86 115 lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf. 87 (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf) .88 #tag #A #P #m #i #prf #H @H @lookup_eq_safe qed.116 (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf) ≝ 117 λtag,A,P,m,i,prf,H.(H … (lookup_eq_safe …)). 89 118 90 119 let rec graph_visit … … 106 135 (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop ( 107 136 And (bool_to_Prop (code_has_label … (rev ? generated) l)) 108 (∃s.And (And137 (∃s.And 109 138 (lookup … g l = Some ? s) 110 (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) 111 (opt_All ? (λnext.match lookup … visited next with 112 [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉) 113  None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s))))) 139 (match s with 140 [ sequential s' nxt ⇒ 141 match s' with 142 [ step_seq _ ⇒ 143 And 144 (nth_opt … n (rev … generated) = 145 Some ? 〈Some ? l, sequential … s' it〉) 146 (match lookup … visited nxt with 147 [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉) 148  None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length) 149 ]) 150  COND a ltrue ⇒ 151 Or 152 (And (nth_opt … n (rev … generated) = 153 Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉) 154 (match lookup … visited nxt with 155 [ Some n' ⇒ n' = S n 156  None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length) 157 ])) 158 (nth_opt … n (rev … generated) = 159 Some ? 〈Some ? l, FCOND … I a ltrue nxt〉) 160 ] 161  final s' ⇒ 162 nth_opt … n (rev … generated) = 163 Some ? 〈Some ? l, final … s'〉 164  FCOND abs _ _ _ ⇒ Ⓧabs 165 ])))) 114 166 (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated)) 115 167 (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨ 168 (∃a,ltrue,lfalse.stmt_at … generated 0 = Some ? (FCOND … a ltrue lfalse)) ∨ 116 169 (¬All ? (λx.bool_to_Prop (x∈visited)) visiting)) 117 170 (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting) … … 138 191 let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in 139 192 (* translate it to its linear version *) 140 let translated_statement ≝ graph_to_lin_statement p globalsstatement in193 let translated_statement ≝ graph_to_lin_statement … visited' statement in 141 194 (* add the translated statement to the code (which will be reversed later) *) 142 195 let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in 143 let required' ≝ union_set ??? (set_from_list … (stmt_explicit_labels … statement)) required in 196 let required' ≝ union_set ??? 197 (set_from_list … (stmt_explicit_labels … translated_statement)) 198 required in 144 199 (* put successors in the visiting worklist *) 145 200 let visiting' ≝ stmt_labels … statement @ vis_tl in … … 147 202 (* if it has been already visited, we need to add a GOTO *) 148 203 let add_req_gen ≝ 149 match stmt_implicit_label … statement 150 with 151 [ Some next ⇒ 152 if next ∈ visited' then 153 〈1, {(next)}, [〈None label, (GOTO … next : joint_statement ??)〉]〉 154 else 〈0, ∅, [ ]〉 155  None ⇒ 〈0, ∅, [ ]〉 204 match statement with 205 [ sequential s nxt ⇒ 206 match s with 207 [ COND _ _ ⇒ 〈0, ∅, [ ]〉 208  _ ⇒ 209 if nxt ∈ visited' then 210 〈1, {(nxt)}, [〈None label, (GOTO … nxt : joint_statement ??)〉]〉 211 else 〈0, ∅, [ ]〉 212 ] 213  _ ⇒ 〈0, ∅, [ ]〉 156 214 ] in 157 215 (* prepare a common utility to deal with add_req_gen *) 158 216 let add_req_gen_prf : 159 217 ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop. 160 (opt_All ? (λnext.¬bool_to_Prop (next ∈ visited')) (stmt_implicit_label … statement) → 161 P 〈0,∅,[ ]〉) → 162 (∀next.stmt_implicit_label … statement = Some ? next → 163 next ∈ visited' → 164 P 〈1, {(next)}, [〈None ?, GOTO (mk_lin_params p) next〉]〉) → 218 (match statement with 219 [ sequential s nxt ⇒ 220 match s with [ COND _ _ ⇒ True  _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ] 221  _ ⇒ True] → P 〈0,∅,[ ]〉) → 222 (∀s,nxt. 223 statement = sequential … (step_seq … s) nxt → 224 nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) → 165 225 P add_req_gen ≝ hide_prf ?? in 166 226 graph_visit ??? … … 186 246  assumption 187 247 ] 188  cases generated_prf3 [/ /]248  cases generated_prf3 [/2 by /] 189 249 * #ABS @⊥ @ABS assumption 190 250  assumption 191  #l #n #H elim (generated_prf1 … H) 192 #H1 * #s ** #H2 #H3 #H4 193 % [assumption] %{s} % 194 [% assumption 195  @(opt_All_mp … H4) l #l 196 lapply (in_map_domain … visited l) 197 elim (true_or_false_Prop (l∈visited)) #l_vis >l_vis 198 normalize nodelta [ * #n' ] #EQlookup >EQlookup 251  #l #n #H elim (generated_prf1 … H) H 252 #H1 * #s * #H2 #H3 %{H1} %{s} %{H2} 253 cases s in H3; [3: *] 254 [ * ] normalize nodelta 255 [ #s' #nxt * #EQnth_opt #H %{EQnth_opt} 256 inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup 199 257 normalize nodelta * 200 [ #EQn' % >EQn' %258 [ #EQn' %1 >EQn' % 201 259  #H %2{H} 202  #H' lapply (All_nth … H … H') >l_vis * 260  #H' lapply (All_nth … H … H') 261 whd in ⊢ (?%→?); >EQlookup * 203 262 ] 263  #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1} 264 inversion (lookup … visited lfalse) in H2; 265 [ #ABS * #H' lapply (All_nth … H … H') 266 whd in ⊢ (?%→?); >ABS * 267  #n' #_ normalize nodelta #EQ >EQ % 268 ] 269  #s #H @H 204 270 ] 205 271 ] … … 220 286 #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) % 221 287  #l #H 222 elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s * * #s_in_g #_#_288 elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s * #s_in_g #_ 223 289 whd in ⊢ (?%); >s_in_g % 224 290 ] … … 228 294 [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2 229 295 @(All_append … G1) 230 whd in G2; lapply G2 elim statement normalize nodelta #s [2: #_ %]231 # l#G' %{G'} %296 cases statement in G2; [2: // 3: * ] 297 #s #nxt #G' %{G'} % 232 298  >H2 in visiting_prf; 233 299 #H' lapply (All_append_r … H') H' * #_ // … … 257 323 12: (* add_req_gen utility *) 258 324 #P whd in match add_req_gen; 259 elim (stmt_implicit_label ???) 260 [ #H #_ @H % ] 261 #next normalize nodelta elim (true_or_false_Prop (next ∈ visited')) #next_vis 262 >next_vis normalize nodelta 263 [ #_ #H @H [%  assumption] 264  #H #_ @H whd >next_vis % * 265 ] 266  elim H #pre ** #H1 #H2 #_ 325 cases statement [ * ] [*: [ #a #ltrue #lfalse  #s  * ] #H #_ @(H I) ] 326 #s #nxt normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta 327 #H1 #H2 [ @(H2 … (refl …)) >EQ %  @H1 % * ] 328 3: elim H #pre ** #H1 #H2 #_ 267 329 #i >mem_set_union 268 330 #H elim (orb_Prop_true … H) H 269 331 [ @add_req_gen_prf [ #_ >mem_set_empty * ] 270 # next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption332 #s #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption 271 333  >mem_set_union 272 334 #H elim (orb_Prop_true … H) H 273 [ #i_expl %1 @Exists_append_l @Exists_append_r 274 @mem_list_as_set 275 @i_expl 335 [ #i_expl %1 @Exists_append_l 336 lapply i_expl whd in match translated_statement; 337 cases statement [ * [ #s  #a #ltrue ] #nxt  #s  *] normalize nodelta #H 338 lapply (mem_list_as_set … H) H #H 339 [1,3: @Exists_append_r assumption ] 340 cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]] 341 #EQ destruct(EQ) [ %1 % *: %2 %1 % ] 276 342  (* i was already required *) 277 343 #i_req … … 280 346 [ (* i in preamble → i∈visited *) 281 347 #i_pre %2 >mem_set_add @orb_Prop_r 282 lapply (All_In … H1 i_pre) #H @H348 @(All_In … H1 i_pre) 283 349  * 284 350 [ (* i is vis_hd *) … … 307 373 cases (pt  ?) 308 374 [ whd in match (nth_opt ???); whd in ⊢ (??%?→?); 309 #EQ destruct(EQ) whd 310 >graph_to_lin_labels in ⊢ (???%); 375 #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ) whd 311 376 whd in match required'; 312 generalize in match (stmt_explicit_labels … statement); 377 cut (∀p : lin_params.∀globals.∀s. 378 stmt_implicit_label p globals s = None ?) 379 [ #p #globals * normalize // ] 380 #lin_implicit_label change with (? @ ?) in match (stmt_labels ???); 381 >lin_implicit_label 382 change with (All ?? (stmt_explicit_labels ???)) 383 generalize in match (stmt_explicit_labels … translated_statement); 313 384 #l @list_as_set_All 314 385 #i >mem_set_union >mem_set_union 315 #i_l @orb_Prop_r @orb_Prop_l @i_l386 #i_l @orb_Prop_r @orb_Prop_l assumption 316 387  @add_req_gen_prf 317 [ #_  # next #_ #next_vis *388 [ #_  #s #next #_ #next_vis * 318 389 [ whd in ⊢ (??%?→?); 319 390 #EQ' destruct(EQ') whd %{I} >mem_set_union … … 326 397 @(eq_identifier_elim … i vis_hd) 327 398 [ #EQi >EQi i #pos 328 >lookup_add_hit #EQpos (* too slow: destruct(EQpos) *)399 >lookup_add_hit in ⊢ (%→?); #EQpos (* too slow: destruct(EQpos) *) 329 400 cut (gen_length = pos) 330 [ 1,3,5: (* BUG: graph_visit *)visited destruct(EQpos) %]401 [ visited destruct(EQpos) %] 331 402 EQpos #EQpos <EQpos pos 332 403 % … … 334 405 @add_req_gen_prf 335 406 [ #_ 336  # next #_ #next_vis407  #s #next #_ #next_vis 337 408 change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 338 409 <associative_append >occurs_exactly_once_None … … 344 415 >H3 normalize nodelta // 345 416  %{statement} 346 % [ % ]417 % 347 418 [ @lookup_eq_safe 348  <associative_append @nth_opt_append_hit_l 349 >nth_opt_append_r 350 >rev_length 351 <gen_length_prf 352 [<minus_n_n] % 353  @add_req_gen_prf 354 [ lapply (refl … (stmt_implicit_label ?? statement)) 355 cases (stmt_implicit_label ???) in ⊢ (???%→%); 356 [#_ #_ %] 357 #next #K change with (¬bool_to_Prop (?∈?)→?) #next_vis 358  #next #K >K #next_vis 359 ] whd 360 >mem_set_add in next_vis; 361 @eq_identifier_elim 362 [1,3: #EQnext >EQnext * [#ABS elim(ABS I)] 363 >lookup_add_hit 364 *: #NEQ >(lookup_add_miss … visited … NEQ) 365 change with (?∈?) in match (false∨?); 366 #next_vis lapply(in_map_domain … visited next) >next_vis 367 whd in ⊢ (% → ?); [2: * #s ] 368 #EQlookup >EQlookup 369 ] whd 370 [1,2: %2 <associative_append 371 >nth_opt_append_r >append_length >rev_length >commutative_plus 372 <gen_length_prf 373 [1,3: <minus_n_n ] % 374  % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement); 375 >K % 419  normalize nodelta 420 change with statement in match (lookup_safe ?????); 421 cases statement; 422 [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 423 [1,2: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ] 424 [1,2: %  %2  %1 % ] 425 [1,3,5,6,8: 426 >nth_opt_append_r >rev_length <gen_length_prf try % 427 <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta 428 >nxt_vis % 429 *: 430 lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta 431 [ * #n' ] #EQlookup >EQlookup normalize nodelta 432 [ %2 >nth_opt_append_r >rev_length <gen_length_prf [2: %2 %1 ] 433 <minus_Sn_n % 434 *: %% 435 ] 376 436 ] 377 437 ] … … 379 439  #NEQ #n_i >(lookup_add_miss … visited … NEQ) 380 440 #Hlookup elim (generated_prf1 … Hlookup) 381 #G1 * #s * * #G2 #G3 #G4441 #G1 * #s * #G2 #G3 382 442 % 383 443 [ >lin_code_has_label <associative_append … … 388 448 normalize nodelta >lin_code_has_label in G1; #K @K 389 449  @add_req_gen_prf 390 [ #_ %  # next #_ #_ % ]450 [ #_ %  #s' #next #_ #_ % ] 391 451 ] 392 452  %{s} 393 % [ % ]394 [ assumption395  @nth_opt_append_hit_l assumption396  @(opt_All_mp … G4)397 #x398 @(eq_identifier_elim … x vis_hd) #Heq399 [ >Heq453 %{G2} 454 cases s in G3; 455 [ * [ #s  #a #ltrue ] #nxt  #s  * ] 456 [ * #EQnth_opt #next_spec %  * [*] #EQnth_opt [#next_spec %1 %  %2]  #EQnth_opt ] 457 [1,3,5,6: @nth_opt_append_hit_l assumption 458 *: @(eq_identifier_elim … nxt vis_hd) 459 [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ] 400 460 lapply (in_map_domain … visited vis_hd) 401 >H3 normalize nodelta in ⊢ (%→?); 402 #EQlookup >EQlookup * #nth_opt_visiting #gen_length_eq 403 >lookup_add_hit %1 >gen_length_eq % 404  >(lookup_add_miss ?????? Heq) 405 lapply (in_map_domain … visited x) 406 elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis 407 normalize nodelta in ⊢ (%→?); [ * #n' ] 408 #EQlookupx >EQlookupx whd in ⊢ (%→%); * 409 [ #G %1{G} 410  #G %2 @nth_opt_append_hit_l 411 assumption 412  #G elim(absurd ?? Heq) 413 (* BUG (but useless): required g generated *) 414 >H2 in G; lapply H1 cases pre 415 [ #_ 416  #hd #tl * #hd_vis #_ 417 ] normalize #EQ' destruct(EQ') 418 [ % 419  >x_vis in hd_vis; * 461 >H3 #EQ >EQ in next_spec; * #_ #OK >OK % 462 *: #NEQ' >(lookup_add_miss … visited … NEQ') 463 lapply (in_map_domain … visited nxt) 464 inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup' 465 >EQlookup' in next_spec; whd in ⊢ (%→%); 466 [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption 467  #H @H 468 *: * >H2 469 cases pre in H1; 470 [1,3: #_ 471 *: #frst #pre_tl * #ABS #_ 472 ] whd in ⊢ (??%?→?); #EQ destruct(EQ) 473 [1,2: cases NEQ' #ABS cases (ABS ?) % 474 *: >nxt_vis in ABS; * 420 475 ] 421 476 ] … … 433 488  change with (bool_to_Prop (¬eq_identifier ??? ∧ ?)) 434 489 >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ] 435 @add_req_gen_prf [ #_  # next #_ #_ ] %490 @add_req_gen_prf [ #_  #s #next #_ #_ ] % 436 491 ] 437 492 ] 438 493  @add_req_gen_prf 439 [ #K  # next #K #next_vis%1 %{(GOTO … next)} % ]494 [ #K  #s #next #K #next_vis %1 %1 %{(GOTO … next)} % ] 440 495 whd in match generated'; whd in match translated_statement; 441 lapply K whd in match visiting'; 442 whd in match (stmt_labels ???); cases statement #last 443 [2: #_ %1 %{last} % ] #next whd in ⊢ (%→?); #next_vis 444 %2 % * >next_vis * 496 normalize nodelta 497 change with statement in match (lookup_safe ?????); 498 cases statement in K; 499 [ * [ #s  #a #ltrue ] #nxt  #s #_ %1 %1 %{s} %  * ] normalize nodelta 500 [2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis 501 [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ] 502  #nxt_vis ] 503 %2 % * >nxt_vis * 445 504  whd in match generated'; 446 @add_req_gen_prf [ #_  #next #_ #_ ] normalize >gen_length_prf % 505 @add_req_gen_prf [ #_  #s #next #_ #_ ] normalize >gen_length_prf % 506  447 507 ] 448 508 qed. … … 567 627 ∀l,n.sigma l = Some ? n → 568 628 ∃s. stmt_at … g l = Some ? s ∧ 569 All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ 570 opt_All ? 571 (λnext.Or (sigma next = Some ? (S n)) 572 (stmt_at … c (S n) = Some ? (GOTO … next))) 573 (stmt_implicit_label … s) ∧ 574 stmt_at … c n = Some ? (graph_to_lin_statement … s). 629 All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ 630 (match s with 631 [ sequential s' nxt ⇒ 632 match s' with 633 [ step_seq _ ⇒ 634 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 635 ((sigma nxt = Some ? (S n)) ∨ 636 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 637  COND a ltrue ⇒ 638 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ 639 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) 640 ] 641  final s' ⇒ 642 stmt_at … c n = Some ? (final … s') 643  FCOND abs _ _ _ ⇒ Ⓧabs 644 ]). 575 645 576 646 definition linearise_code: … … 633 703 lapply (in_map_domain … visited lbl) >(req_vis … H2) 634 704 * #n_lbl #EQsigma 635 elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_ 636 >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H) 637 [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 638  >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 705 elim (sigma_prop … EQsigma) #_ * #stmt * #_ 706 cases stmt [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 707 [ * #EQnth_opt #_  * [ * ] #EQnth_opt [ #_ ]  #EQnth_opt ] 708 >(nth_opt_index_of_label ???? n_lbl ? H) 709 [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 710 3: @(sequential … s it) 6: @(sequential … (COND … a ltrue) it) 711 9: @(FCOND … I a ltrue nxt) 12: @(final … s) 712 2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 639 713 >H2 % 640 714 ] 641 715  #eq_lookup elim (sigma_prop ?? eq_lookup) 642 #lbl_in_gen * #stmt * * #stmt_in_g #nth_opt_is_stmt #succ_is_in643 % [2: % [ % [ % [ assumption ]]] ]716 #lbl_in_gen * #stmt * #stmt_in_g #stmt_spec 717 % [2: % [ % [ assumption ]] ] 644 718 [ @All_append 645 [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ] 646 #nxt #nxt_spec % [2: %] cases nxt_spec nxt_spec 647 [ #EQ >EQ % #ABS destruct(ABS) 648  #goto_in lapply (in_map_domain … visited nxt) 649 >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ] 650 @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 651 whd in ⊢ (??%?); >goto_in % 719 [ cases stmt in stmt_spec; 720 [ * [ #s  #a #ltrue ] #nxt  #s #_ %  * ] 721 normalize nodelta * [ #stmt_at_EQ * #nxt_spec  * #stmt_at_EQ #nxt_spec  #stmt_at_EQ ] 722 %{I} 723 [1,3: >nxt_spec % #ABS destruct(ABS) 724 *: lapply (in_map_domain … visited nxt) 725 >req_vis 726 [1,3: * #x #EQ >EQ % #ABS destruct(ABS) 727 2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 728 whd in ⊢ (??%?); >nxt_spec % 729 4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) 730 whd in ⊢ (??%?); >stmt_at_EQ % 731 ] 652 732 ] 653  <graph_to_lin_labels @(All_mp … (labels_in_req …)) 654 [ #lbl #H 655 lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS) 656  whd in ⊢ (??%?); >nth_opt_is_stmt %  733  cases stmt in stmt_spec; 734 [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 735 [ * #EQ #_  * [ * #EQ #_  #EQ ]  #EQ ] 736 whd in match stmt_explicit_labels; normalize nodelta 737 [ @(All_mp … (labels_in_req n (sequential … s it) ?)) 738  @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?)) 739  cases (labels_in_req n (FCOND … I a ltrue nxt) ?) 740 [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue) 741 >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ] 742  @(All_mp … (labels_in_req n (final … s) ?)) 743 ] 744 [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS) 745 *: whd in ⊢ (??%?); >EQ % 657 746 ] 658 747 ] 659  lapply succ_is_in 660 cases (stmt_implicit_label … stmt) [#_ %] 661 #next * 662 [ #H %1{H} ] 663 #H %2 664 >stmt_at_filter_labels whd in ⊢ (??%?); >H % 665  >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt % 748  cases stmt in stmt_spec; 749 [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 750 [ * #EQ #H  * [ * #EQ #H  #EQ ]  #EQ ] 751 >stmt_at_filter_labels 752 whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta 753 [ % [%] cases H H [#H %1{H}  #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ] 754  %1 %{H} % 755  %2 % 756  % 757 ] 666 758 ] 667 759 ] … … 676 768 elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req))) 677 769 >lin_code_has_label #H #_ @H 678  lapply EQ cases s #s' [2:#_ % ]679 *EQ #EQ change with (bool_to_Prop (code_has_point ????))770  lapply EQ cases s [ #s' *  #s' #_ %  * #a #ltrue #lfalse #_ % ] 771 EQ #EQ change with (bool_to_Prop (code_has_point ????)) 680 772 whd in match (point_of_succ ???); 681 773 >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse … … 687 779 @(nth_opt_hit_length … EQ1) 688 780 ] #EQ_length 689 elim last_fin #fin#EQ'781 elim last_fin * [ #fin  #a * #ltrue * #lfalse ] #EQ' 690 782 lapply EQ whd in match (stmt_at ????); 691 >nth_opt_reverse_hit >EQ_length [2 : % ] <minus_n_n783 >nth_opt_reverse_hit >EQ_length [2,4: % ] <minus_n_n 692 784 change with (stmt_at ???? = ? → ?) 693 785 >EQ' #ABS destruct(ABS) … … 737 829  @H1 738 830  cases H1 * #H3 #H4 #H5 elim (H5 … H3) 739 #s *** #_ #_ #_ >lin_code_has_point cases code 740 [ #ABS normalize in ABS; destruct(ABS)  #hd #tl #_ % ] 831 #s ** #_ #_ >lin_code_has_point cases code 832 [ cases s [ * [ #s'  #a #ltrue ] #nxt  #s'  * ] 833 [ * #ABS #_  * [ * #ABS #_  #ABS ]  #ABS ] normalize in ABS; destruct(ABS) 834  #hd #tl #_ % 835 ] 741 836 ] 742 837 qed. 
src/joint/semantics.ma
r2529 r2532 5 5 include "joint/Joint.ma". 6 6 include "ASM/I8051bis.ma". 7 include "common/extraGlobalenvs.ma". 7 (* include "common/extraGlobalenvs.ma". *) 8 8 9 9 (* CSC: external functions never fail (??) and always return something of the … … 162 162 ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval 163 163 ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) 164 164 165 165 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 166 166 ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars … … 177 177 178 178 (* from now on, parameters that use the type of functions *) 179 ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) 179 ; block_of_call : ∀globals.genv_t (fundef (F globals)) → call_spec uns_pars → 180 state st_pars → res (Σbl.block_region bl = Code) 181 ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → 182 state st_pars → res (list beval) 180 183 ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → 181 184 ident → F globals (* current *) → state st_pars → res (state st_pars) … … 374 377 ] (refl …). 375 378 376 definition block_of_call ≝ λp:sem_params.λglobals. 377 λge: genv_t (joint_function p globals).λst : state p.λf. 378 ! bl ← match f with 379 [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) 380  inr addr ⇒ 381 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 382 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 383 ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ; 384 if eq_bv … (bv_zero …) (offv (poff ptr)) then 385 return (pblock … ptr) 386 else 387 Error … [MSG BadFunction; MSG BadPointer] 388 ] ; 389 opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl). 379 (* to be used in implementations *) 380 definition block_of_call_id ≝ λF.λsp:sem_state_params. 381 λge: genv_t F.λid.λst:state sp. 382 opt_to_res … [MSG BadFunction; CTX … id] ( 383 ! bl ← find_symbol … ge id; 384 code_block_of_block bl). 385 386 definition block_of_call_id_ptr ≝ λp,F.λsp : sem_unserialized_params p F. 387 λglobals.λge: genv_t (F globals).λf.λst : state sp. 388 match f with 389 [ inl id ⇒ block_of_call_id … ge id st 390  inr addr ⇒ 391 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 392 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 393 ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ; 394 if eq_bv … (bv_zero …) (offv (poff ptr)) then 395 opt_to_res … [MSG BadFunction; MSG BadPointer] 396 (code_block_of_block (pblock … ptr)) 397 else 398 Error … [MSG BadFunction; MSG BadPointer] 399 ]. 390 400 391 401 (* Paolo: why external calls do not need args?? *) … … 488 498 λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt. 489 499 λst : state_pc p. 490 ! bl ← block_of_call … ge st f: IO ???;500 ! bl ← block_of_call … ge f st : IO ???; 491 501 ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; 492 502 match fd with … … 523 533  COND a l ⇒ return st 524 534 ] 525  final s⇒ return st535  _ ⇒ return st 526 536 ]. 527 537 … … 538 548 λcurr_fn : joint_closed_internal_function ??. 539 549 λst : state_pc p. 540 ! bl ← block_of_call … ge st f: IO ???;550 ! bl ← block_of_call … ge f st : IO ???; 541 551 ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; 542 552 match fd with … … 557 567 IO io_out io_in (state_pc p) ≝ 558 568 λp,g,ge,curr_id,curr_fn,s,st. 559 match s with569 match s return λ_.IO ??? with 560 570 [ sequential s nxt ⇒ 561 571 match s return λ_.IO ??? with … … 577 587 eval_tailcall … ge f args curr_id curr_fn st 578 588 ] 589  FCOND _ a lbltrue lblfalse ⇒ 590 ! v ← acca_retrieve … st a ; 591 ! b ← bool_of_beval … v ; 592 if b then 593 goto … ge lbltrue st 594 else 595 goto … ge lblfalse st 579 596 ]. 580 597
Note: See TracChangeset
for help on using the changeset viewer.