Changeset 3165
 Timestamp:
 Apr 19, 2013, 11:46:59 AM (5 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r3155 r3165 811 811 (* Cminor env/mem *) 812 812 ∀cm_env, cm_m. 813 (* fresh label generator for function *) 814 ∀func_univ: universe SymbolTag. 815 (* specify fblock *) 816 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef → 817 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef → 818 ∀cl_fun_id, cm_fun_id. 813 (* specify fblock; as a consequence of these and INV we can deduce that 814 cm_fundef is the translation of cl_fundef *) 815 ∀fun_id. 816 find_funct_id clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cl_fundef,fun_id〉 → 817 find_funct_id (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cm_fundef,fun_id〉 → 819 818 ∀tmpenv. 820 819 (*match cl_fundef with … … 852 851 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values → 853 852 clight_cminor_rel cl_ge cm_ge INV 854 (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m)855 (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st)853 (ClCallstate fun_id cl_fundef cl_args_values cl_k cl_m) 854 (CmCallstate fun_id cm_fundef cm_args_values cm_m cm_st) 856 855 (*  *) 857 856 (* special while state *) … … 1740 1739 qed. 1741 1740 1741 (* TODO: move *) 1742 lemma extract_pair' : ∀A,B,C. ∀u:A×B. ∀Q:A → B → C. ∀x. 1743 ((let 〈a,b〉 ≝ u in Q a b) = x) → 1744 ∃a,b. 〈a,b〉 = u ∧ Q a b = x. 1745 #A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed. 1746 1742 1747 (* 1743 1748 lemma lset_inclusion_Exists : … … 1783 1788 subtrace corresponding to a measurable Clight subtrace. 1784 1789 *) 1790 (* WIP 1791 lemma clight_cminor_call : 1792 ∀g,g'. 1793 ∀INV:clight_cminor_inv g g'. 1794 ∀s1,s1'. 1795 clight_cminor_rel g g' INV s1 s1' → 1796 Clight_classify s1 = cl_call → 1797 ∀s2,tr2,s3,tr3. 1798 step … (pcs_exec cl_pre) g s1 = Value … 〈tr2,s2〉 → 1799 step … (pcs_exec cl_pre) g s2 = Value … 〈tr3,s3〉 → 1800 Clight_labelled s2 → 1801 after_n_steps 1 ?? (pcs_exec cm_pre) g' s1' (λs.cminor_normal s) (λtr2',s2'. 1802 tr2 = tr2' ∧ 1803 bool_to_Prop (Cminor_labelled s2') ∧ 1804 ∃m. 1805 after_n_steps m ?? (pcs_exec cm_pre) g' s2' (λs.cminor_normal s) (λtr3',s3'. 1806 tr3 = tr3' ∧ 1807 clight_cminor_rel g g' INV s2 s2') 1808 ). 1809 #Xg #Xg' #XINV #Xs1 #Xs1' * 1810 [ #g #g' #INV #cl_s #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #fInv #sInv #kInv #Erettyp #func_univ #Hfresh_globals #Hfresh_function #Htranslate_fn #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag #Htranslate_inv #Htranslate_s #Hlbls_inc #tmpenv #Htmpenv #CONT #Em #HtmpEm #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #Henv_below 1811 #CL whd in CL:(??%?); destruct 1812  #g #g' #INV #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #stmt_univ #tmpenv #Htmpenv #Em #HEm_tmp #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #CONT 1813 #CL whd in CL:(??%?); destruct 1814  #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #INJ #HEm_fn #cl_args #cm_args #Hargs 1815 #CL #s2 #tr2 #s3 #tr3 #STEP1 #STEP2 #CS2 1816 1817 (* Note that cm_fd is the translation of cl_fd *) 1818 cases (trans_fn … INV … Hfind_cl) 1819 #func_univ * #cm_fd' * #Hglobals_fresh * #Hfundef_fresh * #Htranslate 1820 >Hfind_cm #E destruct 1821 1822 (* Must be a CL_Internal function *) 1823 cases cl_fd in Hfundef_fresh Htranslate Hfind_cl CONT STEP1; 1824 [ #cl_f 1825  #ext #ext_argtys #ext_retty 1826 ] 1827 #Hfundef_fresh #Htranslate #Hfind_cl #CONT #STEP1 1828 [2: cases (bindIO_inversion ??????? STEP1) STEP1 #vs * #_ #STEP1 1829 whd in STEP1:(??%%); destruct ] 1830 cl_fd 1831 1832 (* Invert Clight STEP1 *) 1833 cases (extract_pair' ?????? STEP1) STEP1 #cl_env * #cl_m1 * #ALLOC #STEP1 1834 cases (bindIO_inversion ??????? STEP1) STEP1 #cl_m2 * #BIND #STEP1 1835 whd in STEP1:(??%%); destruct 1836 *) 1837 1785 1838 (* 1786 1839 lemma clight_cminor_call_return : … … 2353 2406 [ 1,2: >addition_n_0 >mk_offset_offv_id 2354 2407  3: ] 2355 > (find_funct_to_find_funct_id ???? Hfind_funct_cm)2408 >Hfind_funct_cm 2356 2409 whd in match (opt_to_res ???); normalize nodelta 2357 2410 (* Again, isolate cases by type similarity *) … … 2877 2930 #cl_ge #cm_ge #INV' #cl_k #cm_st #cl_fundef #cm_fundef 2878 2931 #fblock #target_type #cl_env #cl_m #cm_env #cm_m 2879 #f unc_univ#Hfind_cl #Hfind_cm2880 # cl_id #cm_id #tmpenv #Hcont_rel2932 #fn_id #Hfind_cl #Hfind_cm 2933 #tmpenv #Hcont_rel 2881 2934 #Em #Hinj #Hem_fn_id 2882 2935 #cl_args_values #cm_args_values #Hall2 … … 2983 3036 2984 3037 (* TODO: move to globalenvs *) 2985 lemma find_funct_match: 2986 ∀M:matching.∀initV,initW. 3038 (* The hypotheses are a little strong  we don't need to know that the size of 3039 the initialisation data is the same. *) 3040 lemma find_funct_id_match: 3041 ∀M:matching. 3042 ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 2987 3043 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 2988 3044 ∀MATCH:match_program … M p p'. 2989 ∀v. ∀f: m_A M (prog_var_names … p). 2990 find_funct … (globalenv … initV p) v = Some ? f→3045 ∀v. ∀f: m_A M (prog_var_names … p). ∀id. 3046 find_funct_id … (globalenv … initV p) v = Some ? 〈f,id〉 → 2991 3047 ∃tf : m_B M (prog_var_names … p'). 2992 find_funct … (globalenv … initW p') v = Some ? tf∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).3048 find_funct_id … (globalenv … initW p') v = Some ? 〈tf,id〉 ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). 2993 3049 [ 2: >(matching_vars … (mp_vars … MATCH)) % ] 2994 #M #initV #initW # p #p' #MP * [  #sz #i   #p ] #f3050 #M #initV #initW #varsOK #p #p' #MP * [  #sz #i   #p ] #f #id 2995 3051 [ 1,2,3: #FF whd in FF:(??%?); destruct ] 2996 whd in ⊢ (??%? → ?); @eq_offset_elim #OFF #FFP 2997 [2: whd in FFP:(??%?); destruct ] 2998 cases (find_funct_ptr_match M initV initW … MP (pblock p)f FFP)3052 #FFI cases (find_funct_id_ptr ????? FFI) #b * * #E destruct #FS #FFPI 3053 cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SFB 3054 cases (find_funct_ptr_match M initV initW … MP ? f FFP) 2999 3055 #f' * #FFP' #MF %{f'} % 3000 [ whd in ⊢ (??%?); >OFF >reflexive_eq_offset @FFP' 3056 [ @find_funct_ptr_id_conv 3057 @(make_find_funct_ptr_id ???? id FFP' ?) 3058 whd in ⊢ (??%?); >(symbols_match … initV … MP) [ @SFB  @varsOK ] 3001 3059  @MF 3002 3060 ] qed. … … 3010 3068 [2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES) 3011 3069 [4: #H @sym_eq @H  #X #Y * #id #r #v1 #v2 * %  skip  skip ] 3012 3: #v #f # FF cases (find_funct_match … MATCHES … FF)3070 3: #v #f #id #FF cases (find_funct_id_match … MATCHES … FF) 3013 3071 [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd 3014 3072 % [2: %{f'} %{H1} %{H2} % [ >Efd … … 3022 3080 ] 3023 3081  skip 3082  #X #Y * #id' #r #v1 #v2 * % 3024 3083 ] 3025 3084  skip … … 3191 3250 whd in ⊢ (??%?); >FFP' 3192 3251 whd in ⊢ (??%?); % 3193  @(CMR_call … FFP FFP' … (ClCm_cont_stop …)) 3194 [ @(Some ? (ASTint I32 Signed)) 3195  @(empty_map …) 3196  @(empty_map …) 3197  @(new_universe …) 3252  @(CMR_call … b (Some ? (ASTint I32 Signed)) (empty_map …) ? (empty_map …) … (ClCm_cont_stop …)) 3253 [ @find_funct_ptr_id_conv @make_find_funct_ptr_id 3254 [ @FFP 3255  @(symbol_for_block_fn … FINDSYM FFP) 3256 ] 3257  @find_funct_ptr_id_conv @make_find_funct_ptr_id 3258 [ @FFP' 3259  @(symbol_for_block_fn … FFP') >M_findsym @FINDSYM 3260 ] 3198 3261  @([ ]) 3199 3262  % 
src/Clight/toCminorCorrectnessExpr.ma
r2822 r3165 11 11 globals : list (ident × region × type); 12 12 eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s; 13 trans_fn : ∀v,f . find_funct … ge_cl v = Some ? f→13 trans_fn : ∀v,f,id. find_funct_id … ge_cl v = Some ? 〈f,id〉 → 14 14 ∃tmp_u,f',H1,H2. 15 15 translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧ 16 find_funct … ge_cm v = Some ? f'16 find_funct_id … ge_cm v = Some ? 〈f',id〉 17 17 }. 18 18
Note: See TracChangeset
for help on using the changeset viewer.