Changeset 2667 for src/Clight
 Timestamp:
 Feb 14, 2013, 7:10:23 PM (8 years ago)
 Location:
 src/Clight
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Clight_abstract.ma
r2601 r2667 47 47 definition cl_eval_expr ≝ eval_expr. 48 48 49 (* creating aliases constructors for states and continuations *) 49 50 definition ClState ≝ State. 51 52 definition ClKseq ≝ Kseq. 
src/Clight/toCminorCorrectness.ma
r2601 r2667 209 209 ] qed. 210 210 211 212 211 lemma clight_to_cminor_matches : ∀p,p'. 213 212 clight_to_cminor p = OK ? p' → … … 242 241 (* current function (defines local environment) *) 243 242 ∀f : function. 244 (* [alloctype] maps variables to their allocation type (global, stack, register) *) 245 ∀alloctype : var_types. 246 ∀stacksize : ℕ. 247 ∀alloc_hyp : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉. 248 (* environments *) 249 ∀cl_env : cl_env. 250 ∀cm_env : cm_env. 251 (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) 252 ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉. 253 (* CL and CM memories *) 254 ∀cl_m : mem. 255 ∀cm_m : mem. 256 (* memory injection and matching *) 257 ∀embed : embedding. 258 ∀injection : memory_inj embed cl_m cm_m. 259 ∀stackptr : block. 260 ∀matching : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype. 243 ∀data : clight_cminor_data f cl_cm_inv. 261 244 (* clight expr to cminor expr *) 262 245 (∀(e:expr). 263 246 ∀(e':CMexpr (typ_of_type (typeof e))). 264 247 ∀Hexpr_vars. 265 translate_expr alloctypee = OK ? («e', Hexpr_vars») →248 translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») → 266 249 ∀cl_val,trace,Hyp_present. 267 exec_expr (ge_cl … cl_cm_inv) cl_env cl_me = OK ? 〈cl_val, trace〉 →268 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m= OK ? 〈trace, cm_val〉 ∧269 value_eq embedcl_val cm_val) ∧250 exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 → 251 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 252 value_eq (E ?? data) cl_val cm_val) ∧ 270 253 (* clight /lvalue/ to cminor /expr/ *) 271 254 (∀ed,ty. 272 255 ∀(e':CMexpr ASTptr). 273 256 ∀Hexpr_vars. 274 translate_addr alloctype(Expr ed ty) = OK ? («e', Hexpr_vars») →257 translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») → 275 258 ∀cl_blo,cl_off,trace,Hyp_present. 276 exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_med ty = OK ? 〈cl_blo, cl_off, trace〉 →277 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m= OK ? 〈trace, cm_val〉 ∧278 value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).259 exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 260 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 261 value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val). 279 262 *) 280 263 281 282 (* TODO: relate Clight continuations and Cminor ones. *) 283 (* 284 axiom clight_cminor_cont_rel : 285 clight_cminor_inv → cl_cont → cm_cont → block → stack → Prop. 286 264 definition foo ≝ 3. 265 266 (* relate Clight continuations and Cminor ones. *) 267 inductive clight_cminor_cont_rel : 268 ∀INV: clight_cminor_inv. (* stuff on global variables and functions (matching between CL and CM) *) 269 ∀cl_f: function. (* current Clight function *) 270 internal_function → (* current Cminor function *) 271 clight_cminor_data cl_f INV → (* data for the current stack frame in CL and CM *) 272 option typ → (* optional target type  uniform over a given function *) 273 cl_cont → (* CL cont *) 274 cm_cont → (* CM cont *) 275 Prop ≝ 276  ClCm_cont_stop: 277 ∀INV, cl_f, cm_f, frame_data, target_type. 278 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type Kstop Kend 279  ClCm_cont_seq: 280 ∀INV, cl_f, cm_f, frame_data, target_type. 281 ∀cl_s: statement. 282 ∀cm_s: stmt. 283 ∀cl_k': cl_cont. 284 ∀cm_k': cm_cont. 285 ∀stmt_univ, stmt_univ'. 286 ∀lbl_univ, lbl_univ'. 287 ∀lbls. 288 ∀flag. 289 ∀Htranslate_inv. 290 translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 291 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' → 292 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') 293  ClCm_cont_while: 294 (* Inductive family parameters *) 295 ∀INV, cl_f, cm_f, frame_data, target_type. 296 297 (* subcontinuations *) 298 ∀cl_k': cl_cont. 299 ∀cm_k': cm_cont. 300 301 (* elements of the source while statement *) 302 ∀sz,sg. 303 ∀cl_cond_desc. 304 ∀cl_body. 305 306 (* elements of the converted while statement *) 307 ∀cm_cond: CMexpr (ASTint sz sg). 308 ∀cm_body. 309 ∀entry,exit: identifier Label. 310 311 (* universes used to generate fresh labels and variables *) 312 ∀stmt_univ, stmt_univ'. 313 ∀lbl_univ, lbl_univ', lbl_univ''. 314 ∀lbls: lenv. 315 ∀Htranslate_inv. 316 317 (* relate CL and CM expressions *) 318 ∀Hexpr_vars. 319 translate_expr (alloc_type ?? frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») → 320 321 (* Parameters and results to find_label_always *) 322 ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f). 323 ∀Hinv. 324 325 (* Specify how the labels for the whilereplacing gotos are produced *) 326 mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 → 327 translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» → 328 find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env ?? frame_data) sInv I = 329 «〈St_label entry 330 (St_seq 331 (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip) 332 (St_label exit St_skip)), cm_k'〉, Hinv» → 333 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' → 334 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 335 336 337 (* The type of maps from labels to Clight continuations *) 338 (* definition label_map ≝ identifier_map SymbolTag cont. *) 339 340 (* Definition of the simulation relation on states. The orders of the parameters is dictated by 341 * the necessity of performing an inversion on the continuation sim relation without having to 342 * play the usual game of lapplying all previous dependent arguments. *) 287 343 inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝ 288 344  CMR_normal : 289 (* relates globals to globals and functions to functions*)345 (* Relates globals to globals and functions to functions. *) 290 346 ∀INV: clight_cminor_inv. 291 292 (*  Clight variables  *) 293 ∀cl_f: function. (* Clight enclosing function *) 347 348 (*  Statements  *) 294 349 ∀cl_s: statement. (* Clight statement *) 350 ∀cm_s: stmt. (* Cminor statement *) 351 352 (*  Continuations  *) 295 353 ∀cl_k: cl_cont. (* Clight continuation *) 296 ∀c l_e: cl_env. (* Clight environment*)297 298 (*  Cminor variables  *)299 ∀cl_ m: mem. (* Clight memory *)354 ∀cm_k: cm_cont. (* Cminor continuation *) 355 ∀cm_st: stack. (* Cminor stack *) 356 357 ∀cl_f: function. (* Clight enclosing function *) 300 358 ∀cm_f: internal_function. (* enclosing function *) 301 ∀cm_s: stmt. (* Cminor statement *) 302 ∀cm_k: cm_cont. (* Cminor contiuation *) 303 ∀cm_sp: block. (* Cminor stack pointer *) 304 ∀cm_st: stack. (* Cminor stack *) 305 ∀cm_e: cm_env. (* Cminor environment *) 306 ∀cm_m: mem. (* Cminor memory *) 307 ∀fInv: stmt_inv cm_f cm_e (f_body cm_f). (* Cminor invariants *) 308 ∀sInv: stmt_inv cm_f cm_e cm_s. 309 ∀kInv: cont_inv cm_f cm_e cm_k. 310 311 (*  specify the mapping from variables to their alloc type (global, stack, register)  *) 312 ∀alloctype: var_types. (* map from var to alloc type *) 313 ∀stack_cons: ℕ. (* stack consumption of [cl_f] *) 314 characterise_vars (globals INV) cl_f = 〈alloctype, stack_cons〉 → (* spec of [alloctype] *) 315 316 (*  linking Clight and Cminor memories  *) 317 ∀E: embedding. 318 memory_inj E cl_m cm_m → 319 memory_matching E cl_m cm_m cl_e cm_e INV cm_sp alloctype → 359 ∀frame_data: clight_cminor_data cl_f INV. 360 (*∀alloctype: var_types.*) (* map from var to alloc type *) 361 ∀rettyp. (* return type of the function *) 362 363 (*  Relate Clight continuation to Cminor continuation  *) 364 clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k → 365 366 (*  Other Cminor variables  *) 367 ∀fInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f). (* Cminor invariants *) 368 ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) cm_s. 369 ∀kInv: cont_inv cm_f (cm_env ?? frame_data) cm_k. 370 371 (*  Relate return type variable to actual return type  *) 372 rettyp = opttyp_of_type (fn_return cl_f) → 320 373 321 374 (*  specification of the contents of clight environment (needed for expr sim)  *) 322 (* the two memories are those at function entry time. *) 323 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_e,m'〉) → 324 375 325 376 (*  relate Clight and Cminor functions  *) 326 377 ∀func_univ: universe SymbolTag. … … 329 380 translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f → 330 381 331 (*  relate Clight and Cminor statements  *) 332 ∀stmt_univ : tmpgen alloctype.333 ∀lbl_univ :labgen.382 (*  relate Clight and Cminor statements  *) 383 ∀stmt_univ,stmt_univ': tmpgen (alloc_type ?? frame_data). 384 ∀lbl_univ,lbl_univ': labgen. 334 385 ∀lbls: lenv. 335 386 ∀flag: convert_flag. 336 ∀outcome: (Σsu:(tmpgen alloctype)×labgen×stmt.trans_inv alloctype lbls cl_s stmt_univ flag (opttyp_of_type (fn_return cl_f)) su). 337 translate_statement alloctype stmt_univ lbl_univ lbls flag (opttyp_of_type (fn_return cl_f)) cl_s = OK ? outcome → 338 (* TODO decompose outcome *) 339 340 (*  relate Clight continuation to Cminor continuation + stack pointer + stack  *) 341 clight_cminor_cont_rel INV cl_k cm_k cm_sp cm_st → 387 ∀Htranslate_inv. 388 translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 342 389 343 390 clight_cminor_rel INV 344 (ClState cl_f cl_s cl_k cl_e cl_m) 345 (CmState cm_f cm_s cm_e fInv sInv cm_m cm_sp cm_k kInv cm_st). 346 *) 347 348 axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. 391 (ClState cl_f cl_s cl_k (cl_env ?? frame_data) (cl_m ?? frame_data)) 392 (CmState cm_f cm_s (cm_env ?? frame_data) fInv sInv (cm_m ?? frame_data) (stackptr ?? frame_data) cm_k kInv cm_st). 393 394 lemma invert_assert : 395 ∀b. ∀P. assert b P → b = true ∧ P. 396 * #P whd in ⊢ (% → ?); #H 397 [ @conj try @refl @H 398  @False_ind @H ] 399 qed. 400 401 lemma res_to_io : 402 ∀A,B:Type[0]. ∀C. 403 ∀x: res A. ∀y. 404 match x with 405 [ OK v ⇒ Value B C ? v 406  Error m ⇒ Wrong … m ] = return y → 407 x = OK ? y. 408 #A #B #C * 409 [ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl 410  #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] 411 qed. 412 413 414 (* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *) 349 415 350 416 (* Conjectured simulation results … … 368 434 λs. match Cminor_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 369 435 370 axiom clight_cminor_normal : 436 437 lemma clight_cminor_normal : 371 438 ∀INV:clight_cminor_inv. 372 439 ∀s1,s1',s2,tr. 373 440 clight_cminor_rel INV s1 s1' → 374 clight_normal s1 →441 clight_normal s1 = true → 375 442 ¬ Clight_labelled s1 → 376 443 ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → … … 379 446 clight_cminor_rel INV s2 s2' 380 447 ). 448 #INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld 449 inversion Hstate_rel 450 #INV' #cl_s 451 (* case analysis on Clight statement *) 452 cases cl_s 453 [ 1:  2: #lhs #rhs  3: #retv #func #args  4: #stm1 #stm2  5: #cond #iftrue #iffalse  6: #cond #body 454  7: #cond #body  8: #init #cond #step #body  9,10:  11: #retval  12: #cond #switchcases  13: #lab #body 455  14: #lab  15: #cost #body ] 456 [ 1: (* Skip *) 457 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel 458 (* case analysis on continuation *) 459 inversion Hcont_rel 460 [ (* Kstop continuation *) 461 (* simplifying the goal using outcome of the inversion *) 462 #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #Heq_INV 463 #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_ 464 (* get rid of jmeqs and destruct *) 465 lapply (jmeq_to_eq ??? Heq_INV) Heq_INV #Heq_INV 466 lapply (jmeq_to_eq ??? Heq_cl_f) Heq_cl_f #Heq_cl_f 467 destruct (Heq_INV Heq_cl_f) 468 lapply (jmeq_to_eq ??? Heq_frame) Heq_frame #Heq_frame 469 lapply (jmeq_to_eq ??? Heq_cm_f) Heq_cm_f #Heq_cm_f 470 lapply (jmeq_to_eq ??? Heq_rettyp) Heq_rettyp #Heq_rettypv 471 lapply (jmeq_to_eq ??? Heq_cm_k) Heq_cm_k #Heq_cm_k 472 lapply (jmeq_to_eq ??? Heq_cl_k) Heq_cl_k #Heq_cl_k 473 destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp) 474 (* introduce everything *) 475 #fInv #sInv #kInv 476 #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 477 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 478 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 479 #Hreturn_ok #Hlabel_wf 480 (* reduce statement translation function *) 481 whd in ⊢ ((??%?) → ?); 482 #Heq_translate 483 (* In this simple case, trivial translation *) 484 destruct (Heq_translate) 485 #Heq_INV' #Heq_s1 #Heq_s1' 486 lapply (jmeq_to_eq ??? Heq_INV') Heq_INV' #Heq_INV' 487 lapply (jmeq_to_eq ??? Heq_s1) Heq_s1 #Heq_s1 488 lapply (jmeq_to_eq ??? Heq_s1') Heq_s1' #Heq_s1' 489 destruct (Heq_INV' Heq_s1 Heq_s1') #_ 490 (* unfold the clight execution *) 491 %{0} 492 whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??); 493 inversion (fn_return kcl_f) normalize nodelta 494 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 495  #structname #fieldspec  #unionname #fieldspec  #id ] 496 #Hfn_return 497 whd in ⊢ (% → ?); 498 @False_ind 499  (* KSeq continuation *) 500 #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k' 501 #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 502 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 503 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_ 504 #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_ 505 (* get rid of jmeqs and destruct *) 506 lapply (jmeq_to_eq ??? Heq_INV) Heq_INV #Heq_INV 507 lapply (jmeq_to_eq ??? Heq_cl_f) Heq_cl_f #Heq_cl_f 508 destruct (Heq_INV Heq_cl_f) 509 lapply (jmeq_to_eq ??? Heq_frame) Heq_frame #Heq_frame 510 lapply (jmeq_to_eq ??? Heq_cm_f) Heq_cm_f #Heq_cm_f 511 lapply (jmeq_to_eq ??? Heq_rettyp) Heq_rettyp #Heq_rettypv 512 lapply (jmeq_to_eq ??? Heq_cm_k) Heq_cm_k #Heq_cm_k 513 lapply (jmeq_to_eq ??? Heq_cl_k) Heq_cl_k #Heq_cl_k 514 destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp) 515 #fInv #sInv #kInv #Hktarget_type 516 #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 517 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 518 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 519 #Hreturn_ok #Hlabel_wf 520 (* reduce translation function and eliminate result *) 521 (* In this simple case, trivial translation *) 522 whd in ⊢ ((??%?) → ?); #Heq_translate 523 destruct (Heq_translate) 524 #Heq_INV' #Heq_s1 #Heq_s1' 525 lapply (jmeq_to_eq ??? Heq_INV') Heq_INV' #Heq_INV' 526 lapply (jmeq_to_eq ??? Heq_s1) Heq_s1 #Heq_s1 527 lapply (jmeq_to_eq ??? Heq_s1') Heq_s1' #Heq_s1' #_ 528 (* unfold the clight execution *) 529 %{0} 530 whd in ⊢ (% → ?); #Hassert 531 cases (invert_assert ?? Hassert) Hassert #Hclight_class 532 cases (andb_inversion … Hclight_class) Hclight_class 533 #_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq) 534 %{0} whd in ⊢ %; @conj try @refl 535 (* close simulation *) 536 %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function 537 Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag} 538 [ 3: @kHeq_translate  assumption ] 539  (* Kwhile continuation *) 540 #kINV #kcl_f #kcm_f #kframe_data #ktarget_type 541 #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body 542 #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ'' 543 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv 544 * * * * #kHentry_declared * * * * 545 * * * #kHcond_vars_declared * * * * 546 * * * #kHbody_inv * * * 547 whd in ⊢ (% → ?); #kHentry_declared' 548 * * * * * * * * * 549 whd in ⊢ (% → ?); #kHexit_declared * 550 * * * * 551 #kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_ 552 #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k 553 lapply (jmeq_to_eq ??? Heq_INV) Heq_INV #Heq_INV 554 lapply (jmeq_to_eq ??? Heq_cl_f) Heq_cl_f #Heq_cl_f 555 destruct (Heq_INV Heq_cl_f) 556 lapply (jmeq_to_eq ??? Heq_cm_f) Heq_cm_f #Heq_cm_f 557 lapply (jmeq_to_eq ??? Heq_frame) Heq_frame #Heq_frame 558 lapply (jmeq_to_eq ??? Heq_rettyp) Heq_rettyp #Heq_rettyp 559 lapply (jmeq_to_eq ??? Heq_cm_k) Heq_cm_k #Heq_cm_k 560 lapply (jmeq_to_eq ??? Heq_cl_k) Heq_cl_k #Heq_cl_k #_ 561 destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp) 562 (* introduce state relation contents *) 563 #fInv #sInv * whd in ⊢ (% → ?); * * 564 whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv 565 #Heq_rettyp 566 #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 567 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 568 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 569 #Hreturn_ok #Hlabel_wf 570 (* reduce translation function and eliminate result *) 571 (* In this simple case, trivial translation *) 572 whd in ⊢ ((??%?) → ?); #Heq_translate 573 destruct (Heq_translate) 574 #Heq_INV' #Heq_s1 #Heq_s1' 575 lapply (jmeq_to_eq ??? Heq_INV') Heq_INV' #Heq_INV' 576 lapply (jmeq_to_eq ??? Heq_s1) Heq_s1 #Heq_s1 577 lapply (jmeq_to_eq ??? Heq_s1') Heq_s1' #Heq_s1' #_ 578 (* unfold the clight execution *) 579 %{1} whd in ⊢ (% → ?); #Hawait 580 cases (await_value_bind_inv … Hawait) Hawait 581 * #cl_val #cl_trace * #Hexec_cond #Hawait 582 cases (await_value_bind_inv … Hawait) Hawait 583 #cond_outcome * #Hcond_outcome 584 cases (eval_expr_sim … kframe_data) #Hsim_expr #_ 585 (* use simulation lemma on expressions *) 586 lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) Hsim_expr 587 whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome; 588 #Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome) 589 * [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ] 590 * [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ] 591 * #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq) 592 normalize nodelta #Hi_eq 593 * #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert 594 cases (invert_assert … Hassert) Hassert #Handb 595 cases (andb_inversion … Handb) Handb #_ #HClight_not_labelled 596 whd in ⊢ (% → ?); #Heq destruct (Heq) 597 [ %{5} whd whd in ⊢ (??%?); normalize nodelta 598 >kHfind_label kHfind_label normalize nodelta 599 whd in match (proj1 ???); 600 whd in match (proj2 ???); 601 whd whd in ⊢ (??%?); normalize nodelta 602 >Hexec_cond_cm normalize nodelta 603 whd in match (m_bind ?????); 604 >(value_eq_int_inversion … Hvalue_eq) 605 whd in match (eval_bool_of_val ?); normalize nodelta 606 <Hi_eq normalize nodelta 607 whd @conj [ normalize >append_nil try @refl ] 608 whd in match (proj1 ???); 609 whd in match (proj2 ???); 610 whd whd in ⊢ (??%?); normalize nodelta 611 %{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function 612 ??????? kHeq_translate} 613  %{6} whd whd in ⊢ (??%?); normalize nodelta 614 >kHfind_label kHfind_label normalize nodelta 615 whd in match (proj1 ???); 616 whd in match (proj2 ???); 617 whd whd in ⊢ (??%?); normalize nodelta 618 >Hexec_cond_cm normalize nodelta 619 whd in match (m_bind ?????); 620 >(value_eq_int_inversion … Hvalue_eq) 621 whd in match (eval_bool_of_val ?); normalize nodelta 622 <Hi_eq normalize nodelta 623 whd @conj [ normalize >append_nil >append_nil try @refl ] 624 whd in match (proj1 ???); 625 whd in match (proj2 ???); 626 whd whd in ⊢ (??%?); normalize nodelta 627 %{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function} 628 try assumption 629 [ @conj try @conj try @conj try @conj // 630  @refl ] 631 ] 632 (* TODO: other continuations *) 633 ] 634  2: (* Assign *) 635 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel 636 #fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function 637 #Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag 638 * * * * #Hstmt_inv_cm #Huseless_hypothesis 639 #Htmps_preserved #Hreturn_ok #Hlabel_wf 640 (* casesplit on lhs in order to reduce lvalue production in Cminor *) 641 cases lhs #lhs_ed #lhs_ty 642 cases lhs_ed 643 (* intro expr contents *) 644 [ #sz #i  #var_id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 645  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 646 [ 2: #Htranslate_statement 647 cases (bind_inversion ????? Htranslate_statement) 648 * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement' 649 cases (bind_inversion ????? Htranslate_statement') 650 #lhs_dest * #Htranslate_lhs 651 cases (bind2_eq_inversion ?????? Htranslate_lhs) Htranslate_lhs 652 #alloctype * #type_of_var * #Hlookup_var_success 653 cases alloctype in Hlookup_var_success; 654 normalize nodelta 655 [ 1: (* Global *) #r 656 #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq 657 destruct (Hlhs_dest_eq) normalize nodelta 658 whd in match (proj1 ???); whd in match (proj2 ???); 659 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 660 #Heq_INV #Heq_s1 #Heq_s1' 661 lapply (jmeq_to_eq ??? Heq_INV) Heq_INV #Heq_INV 662 lapply (jmeq_to_eq ??? Heq_s1) Heq_s1 #Heq_s1 663 lapply (jmeq_to_eq ??? Heq_s1') Heq_s1' #Heq_s1' 664 destruct (Heq_INV Heq_s1 Heq_s1') #_ 665 %{1} whd in ⊢ (% → ?); #Hawait 666 cases (await_value_bind_inv … Hawait) Hawait 667 * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?); 668 #Hexec_lvalue 669 lapply (res_to_io ????? Hexec_lvalue) Hexec_lvalue #Hexec_lvalue 670 #Hawait 671 cases (await_value_bind_inv … Hawait) Hawait 672 * #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait 673 cases (await_value_bind_inv … Hawait) Hawait 674 #mem_after_store * #Hstore_value #Hawait 675 lapply (opt_to_io_Value ?????? Hstore_value) Hstore_value #Hstore_value 676 Htranslate_statement' Htranslate_statement 677 cases (invert_assert … Hawait) Hawait #Handb 678 cases (andb_inversion … Handb) Handb #_ #HClight_not_labelled #Hawait 679 (* TODO: use the memory injection to handle the store, 680 use INV contents to match up CL global with CM one. 681 Note to self: globals should be exactly matched in CL and CM, 682 maybe memory_injection is not useful in this particular case, 683 only in Stack and Local cases. 684 * *) 685 @cthulhu 686  2: (* Stack *) #n @cthulhu 687  3: (* Local *) @cthulhu 688 ] 689  *: (* memdest *) @cthulhu ] 690  *: @cthulhu 691 ] qed. 381 692 382 693 axiom clight_cminor_call_return : 
src/Clight/toCminorCorrectnessExpr.ma
r2608 r2667 389 389 qed. 390 390 391 record clight_cminor_data (f : function) (INV : clight_cminor_inv) : Type[0] ≝ 392 { alloc_type : var_types; 393 stacksize : ℕ; 394 alloc_hyp : characterise_vars (globals INV) f = 〈alloc_type, stacksize〉; 395 (* environments *) 396 cl_env : cl_env; 397 cm_env : cm_env; 398 (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) 399 cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉; 400 (* CL and CM memories *) 401 cl_m : mem; 402 cm_m : mem; 403 (* memory injection and matching *) 404 E : embedding; 405 injection : memory_inj E cl_m cm_m; 406 stackptr : block; 407 matching : memory_matching E cl_m cm_m cl_env cm_env INV stackptr alloc_type 408 }. 391 409 392 410 (*  *) … … 398 416 (* current function (defines local environment) *) 399 417 ∀f : function. 400 (* [alloctype] maps variables to their allocation type (global, stack, register) *) 401 ∀alloctype : var_types. 402 ∀stacksize : ℕ. 403 ∀alloc_hyp : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉. 404 (* environments *) 405 ∀cl_env : cl_env. 406 ∀cm_env : cm_env. 407 (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) 408 ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉. 409 (* CL and CM memories *) 410 ∀cl_m : mem. 411 ∀cm_m : mem. 412 (* memory injection and matching *) 413 ∀embed : embedding. 414 ∀injection : memory_inj embed cl_m cm_m. 415 ∀stackptr : block. 416 ∀matching : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype. 418 ∀data : clight_cminor_data f cl_cm_inv. 417 419 (* clight expr to cminor expr *) 418 420 (∀(e:expr). 419 421 ∀(e':CMexpr (typ_of_type (typeof e))). 420 422 ∀Hexpr_vars. 421 translate_expr alloctypee = OK ? («e', Hexpr_vars») →423 translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») → 422 424 ∀cl_val,trace,Hyp_present. 423 exec_expr (ge_cl … cl_cm_inv) cl_env cl_me = OK ? 〈cl_val, trace〉 →424 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m= OK ? 〈trace, cm_val〉 ∧425 value_eq embedcl_val cm_val) ∧425 exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 → 426 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 427 value_eq (E ?? data) cl_val cm_val) ∧ 426 428 (* clight /lvalue/ to cminor /expr/ *) 427 429 (∀ed,ty. 428 430 ∀(e':CMexpr ASTptr). 429 431 ∀Hexpr_vars. 430 translate_addr alloctype(Expr ed ty) = OK ? («e', Hexpr_vars») →432 translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») → 431 433 ∀cl_blo,cl_off,trace,Hyp_present. 432 exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_med ty = OK ? 〈cl_blo, cl_off, trace〉 →433 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m= OK ? 〈trace, cm_val〉 ∧434 value_eq embed(Vptr (mk_pointer cl_blo cl_off)) cm_val).435 #inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching434 exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 435 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 436 value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val). 437 #inv #f * #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching 436 438 @expr_lvalue_ind_combined 437 439 [ 7: (* binary ops *)
Note: See TracChangeset
for help on using the changeset viewer.