 Timestamp:
 Mar 10, 2013, 1:21:00 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2825 r2838 487 487 (St_label exit St_skip)), cm_k'〉, Hinv» → 488 488 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' → 489 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type 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')). 490 489 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type ( 490 Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') 491 (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 491 492 492 493 (* TODO XXX *) … … 636 637 cl_fun_id = cm_fun_id → 637 638 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval. 638 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs. 639 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs. 639 640 (* Explain where the lhs of the postreturn assign comes from *) 640 641 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 → 641 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») → 642 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») → 642 643 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the 643 644 * right type, etc *) … … 667 668 ∀cm_cond, cm_body. 668 669 ∀cm_stack. 670 ∀rettyp. 669 671 ∀kInv: cont_inv cm_f cm_env cm_k. 670 672 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f). … … 673 675 (St_seq 674 676 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) 675 (St_label exit_label St_skip))). 676 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbls. 677 (St_label exit_label St_skip))). 678 (*  relate return type variable to actual return type  *) 679 rettyp = opttyp_of_type (fn_return cl_f) → 680 (*  relate Clight and Cminor functions  *) 681 ∀func_univ: universe SymbolTag. 682 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ. 683 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ. 684 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f → 685 (*  relate continuations  *) 686 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k → 687 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls. 677 688 (* Invariants *) 678 689 ∀Em: embedding. … … 682 693 memory_inj Em cl_m cm_m → (* memory injection *) 683 694 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → (* map CL env to CM env *) 695 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) → (* Force embedding to compute identity on functions *) 684 696 (* Expression translation and related hypotheses *) 685 697 ∀Hcond_tr. (* invariant after converting conditional expr *) 686 698 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? «cm_cond, Hcond_tr » → 699 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) → 700 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → 687 701 (* Statement translation *) 688 ∀target_type, Htranslate_inv. 689 translate_statement alloc_type stmt_univ lbl_univ lbls 690 (ConvertTo entry_label exit_label) target_type cl_body 691 = OK ? «〈stmt_univ',lbl_univ',cm_body〉,Htranslate_inv» → 692 (* translate_statement alloc_type *) 702 ∀Htranslate_inv. 703 mklabels lbl_univ = 〈〈entry_label, exit_label〉, lbl_univ'〉 → 704 translate_statement alloc_type stmt_univ lbl_univ' lbls 705 (ConvertTo entry_label exit_label) rettyp cl_body 706 = OK ? «〈stmt_univ',lbl_univ'',cm_body〉,Htranslate_inv» → 707 (* Express the fact that the label points where it ought to *) 708 ∀Hinv1, Hinv2, Hinv3. 709 find_label_always entry_label (f_body cm_f) Kend Hinv1 cm_f cm_env fInv Hinv2 710 = «〈St_label entry_label 711 (St_seq 712 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) 713 St_skip) 714 (St_label exit_label St_skip)), 715 cm_k〉, 716 Hinv3» → 693 717 (clight_cminor_rel cl_ge cm_ge INV 694 718 (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m) … … 699 723 (St_label exit_label St_skip))) 700 724 cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)). 725 726 701 727 702 728 definition clight_normal : Clight_state → bool ≝ … … 1700 1726 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1701 1727 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1702 #Hugly generalize in match (conj ????); #Hugly' 1728 #Hugly 1729 generalize in match (conj ????); #Hugly' 1703 1730 (* In this simple case, trivial translation *) 1704 1731 #Heq_translate destruct (Heq_translate) … … 1714 1741 generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant 1715 1742 #kHfind_label 1743 (* Kwhile cont case *) 1716 1744 %{2} whd whd in ⊢ (??%?); normalize nodelta generalize in match (proj2 ???); #Hmore_noise 1717 1745 generalize in match (proj1 ???); #Hmore_noise' … … 1722 1750 [ 2: #Habsurd destruct (Habsurd) ] 1723 1751 (* go to a special simulation state for while loops *) 1724 @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kH eq_translate)1752 @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels … kHeq_translate) 1725 1753 try assumption 1726 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 1727 @cthulhu 1728 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 1754 [ 1: @cthulhu 1755 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 1756 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 1757  2: cases Hmore_invariant * * * #_ * * * * * * * 1758 #_ #_ #_ * * #_ #H #_ #_ @H ] 1729 1759 ] 1730 1760  2: (* Assign *) … … 1850 1880 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1851 1881 %{1} whd whd in ⊢ (??%?); normalize nodelta 1852 whd in match (eval_expr ???????); 1882 whd in match (eval_expr ???????); 1853 1883 whd in match (eval_constant ????); 1854 1884 whd in match (m_bind ?????); … … 2006 2036 #cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type 2007 2037 #cl_k #cm_k #sz #sg #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body 2008 #cm_stack #kInv #fInv #sInv #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2038 #cm_stack #rettyp #kInv #fInv #sInv #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function 2039 #Htranslate_function #Hcont_rel 2040 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls 2009 2041 #Em #Htmp_vars_well_allocated #Halloc_hyp 2010 #Hcl_env_hyp #Hinjection #Hmatching #Hexpr_vars #Htranslate_expr #target_type 2011 #Htranslate_inv #Htranslate_statement 2042 #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hexpr_vars #Htranslate_expr 2043 #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement 2044 #Hinv1 #Hinv2 #Hinv3 #Hfind_label 2012 2045 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2013 2046 destruct (HA HB) … … 2035 2068 normalize nodelta whd 2036 2069 generalize in match (proj1 ???); #Hnoise' 2037 generalize in match (conj ????); #Hnoise'' @conj try @conj 2070 generalize in match (conj ????); #Hnoise'' @conj try @conj 2038 2071 [ 3: #Habsurd destruct (Habsurd) 2039 2072  1: normalize >append_nil @refl 2040  2: @cthulhu 2041 (* @(CMR_normal … Htranslate_statement) try assumption *) 2042 (* TODO: new continuation relation 2043 * pump the necessary invariants up in CMR_while so that CMR_normal can complete here *) 2073  2: @(CMR_normal … Htranslate_function … Htranslate_statement) try assumption 2074 @(ClCm_cont_while … Htranslate_inv … Hmk_labels … Htranslate_statement) try assumption 2044 2075 ] 2045 2076  (* cond = false: stop looping *) 2046 2077 #Hcl_bool_of_val 2047 %{ 3} whd whd in ⊢ (??%?); normalize nodelta2078 %{5} whd whd in ⊢ (??%?); normalize nodelta 2048 2079 generalize in match (proj1 ???); #Hpresent_ifthenelse 2049 2080 (* Exhibit simulation of condition evaluation *) … … 2057 2088 generalize in match (proj2 ???); #Hnoise'' 2058 2089 generalize in match (conj ????); #Hnoise''' 2059 @conj try @conj2090 whd @conj try @conj 2060 2091 [ 3: #Habsurd destruct (Habsurd) 2061  1: normalize @refl 2062  2: @cthulhu 2063 (* @(CMR_normal … Htranslate_statement) try assumption *) 2064 (* TODO: new continuation relation 2065 * pump the necessary invariants up in CMR_while so that CMR_normal can complete here *) 2092  1: normalize >append_nil >append_nil @refl 2093  2: @(CMR_normal … DoNotConvert) try assumption 2094 [ 2: @refl  ] 2066 2095 ] 2067 2096 ] 2068 2097 2069 ] qed. 2098 ] qed. 2099 2070 2100 2071 2101 (* TODO: adapt the following to the new goal shape. *)
Note: See TracChangeset
for help on using the changeset viewer.