Changeset 3178
 Timestamp:
 Apr 25, 2013, 6:03:24 PM (4 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csyntax.ma
r2645 r3178 346 346 347 347 (* * Natural alignment of a type, in bytes. *) 348 let rec alignof (t: type) : nat ≝ (*1*)349 (* these are old values for 32 bit machines *)348 let rec alignof (t: type) : nat ≝ 1. 349 (* these are old values for 32 bit machines 350 350 match t with 351 351 [ Tvoid ⇒ 1 … … 363 363 [ Fnil ⇒ 1 364 364  Fcons id t f' ⇒ max (alignof t) (alignof_fields f') 365 ]. 365 ].*) 366 366 367 367 (* … … 412 412 (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f') 413 413 ]. 414 414 (* 415 415 lemma alignof_fields_pos: 416 416 ∀f. alignof_fields f > 0. 417 417 @fieldlist_ind //; 418 418 #i #t #fs' #IH @max_r @IH qed. 419 419 *) 420 420 lemma alignof_pos: 421 421 ∀t. alignof t > 0. 422 #t elim t; normalize; //; 422 #t elim t; normalize; //;(* 423 423 [ 1,2: #z cases z; /2/; 424 424  3,4: #i @alignof_fields_pos 425 ] qed.425 ]*) qed. 426 426 427 427 (* * Size of a type, in bytes. *) … … 450 450  Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld') 451 451 ]. 452 (* TODO: needs some Z_times results 452 453 453 lemma sizeof_pos: 454 454 ∀t. sizeof t > 0. 455 #t0 456 napply (type_ind2 (λt. sizeof t > 0) 457 (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0)); 458 [ 1,4,6,9: //; 459  #i cases i;#s //; 460  #f cases f;// 461  #t #n #H whd in ⊢ (?%?); 462 Proof. 463 intro t0. 464 apply (type_ind2 (fun t => sizeof t > 0) 465 (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 > sizeof_struct f pos >= 0)); 466 intros; simpl; auto; try omega. 467 destruct i; omega. 468 destruct f; omega. 469 apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. 470 destruct H. 471 generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 472 generalize (Zmax1 1 (sizeof_struct f 0)). omega. 473 generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 474 generalize (Zmax1 1 (sizeof_union f)). omega. 475 split. omega. auto. 476 destruct H0. split; intros. 477 generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. 478 apply H1. 479 generalize (align_le pos (alignof t) (alignof_pos t)). omega. 480 Qed. 481 455 #t elim t // 456 [ * // 457  #t' * [ /2/  #n #H change with (0 < ?) whd in ⊢ (??%); change with (0*0) in ⊢ (?%?); @lt_times // ] 458  #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1 459 >commutative_plus cases (sizeof_struct ??) [2:#x] whd in ⊢ (?(?%?)?); 460 // 461  #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1 462 >commutative_plus cases (sizeof_union ?) [2:#x] whd in ⊢ (?(?%?)?); 463 // 464 ] qed. 465 466 (* 482 467 Lemma sizeof_struct_incr: 483 468 forall fld pos, pos <= sizeof_struct fld pos. 
src/Clight/memoryInjections.ma
r2822 r3178 759 759 #Halloc destruct (Halloc) /2/ 760 760 qed. 761 762 lemma new_block_invalid_before_alloc : 763 ∀m,m',z1,z2,new_block. 764 alloc m z1 z2 = 〈m', new_block〉 → 765 ¬valid_block m new_block. 766 * #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *) 767 whd in match (alloc ???(*?*)); whd in match (valid_block ??); 768 #Halloc destruct (Halloc) /2/ 769 qed. 770 761 771 762 772 (* All data in a valid block is unchanged after an alloc. *) … … 1467 1477 ] qed. 1468 1478 1479 (* And show the compatibility of the new injection. *) 1480 1481 lemma alloc_memory_inj_m1_to_m2_compat : 1482 ∀E:embedding. 1483 ∀m1,m2,m1':mem. 1484 ∀z1,z2:Z. 1485 ∀target,new_block. 1486 ∀delta:offset. 1487 alloc m1 z1 z2 = 〈m1', new_block〉 → 1488 memory_inj E m1 m2 → 1489 embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x). 1490 #E #m1 #m2 #m1' #z1 #z2 #target #new_block #delta #ALLOC #MI 1491 whd 1492 #b @eq_block_elim 1493 [ #E destruct %1 @(mi_freeblock … MI) /2/ 1494  #_ %2 % 1495 ] qed. 1496 1497 1469 1498 (*  *) 1470 1499 (* Lemmas pertaining to [free] *) 
src/Clight/toCminorCorrectness.ma
r3170 r3178 1747 1747 #A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed. 1748 1748 1749 lemma pair_as_elim: 1750 ∀A,B,C: Type[0]. 1751 ∀p. 1752 ∀T: ∀a:A. ∀b:B. 〈a,b〉 = p → C. 1753 ∀P: A×B → C → Prop. 1754 (∀lft, rgt. ∀E:〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt E)) → 1755 P p (let 〈lft, rgt〉 as E ≝ p in T lft rgt E). 1756 #A #B #C * /2/ 1757 qed. 1758 1759 (* TODO: move *) 1760 lemma alloc_low_bound : ∀m,l,h,m',b. 1761 alloc m l h = 〈m',b〉 → 1762 low_bound m' b = l. 1763 * #contents #next #next_ok #l #h #m' #b #E 1764 whd in E:(??%%); destruct 1765 whd in ⊢ (??%?); >update_block_s 1766 % 1767 qed. 1768 1769 lemma alloc_high_bound : ∀m,l,h,m',b. 1770 alloc m l h = 〈m',b〉 → 1771 high_bound m' b = h. 1772 * #contents #next #next_ok #l #h #m' #b #E 1773 whd in E:(??%%); destruct 1774 whd in ⊢ (??%?); >update_block_s 1775 % 1776 qed. 1777 1778 (* Weaker version of Zlt_to_Zle *) 1779 lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y. 1780 #x #y #H 1781 @(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H 1782 qed. 1783 1784 axiom unZoo : ∀off:Z. 1785 off < Z_two_power_nat 16 → 1786 Zoo (offset_of_Z off) = off. 1787 1788 lemma le_to_Zle : ∀x,y:nat. le x y → Zle x y. 1789 #x #y #H @(le_ind ????? H) 1790 [ // 1791  #m #H1 #H2 >Zsucc_pos @(transitive_Zle … (Zsucc_le m)) assumption 1792 ] qed. 1793 1794 lemma lt_to_Zlt : ∀x,y:nat. lt x y → Zlt x y. 1795 #x #y whd in ⊢ (% → ?); #H 1796 <(Zpred_Zsucc x) @Zle_to_Zlt 1797 <Zsucc_pos 1798 @le_to_Zle assumption 1799 qed. 1800 1801 lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z. 1802 /2/ 1803 qed. 1804 1805 lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y. 1806 /2/ 1807 qed. 1808 1809 theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p. 1810 #n #m #p #Hle #Hlt lapply (Zlt_to_Zle … Hlt) 1811 @Zlt_to_Zle_to_Zlt @Zle_Zlt_Zsucc assumption 1812 qed. 1813 1814 1815 (* This roughly corresponds to lemma 69 of Leroy and Blazy *) 1816 (* 1817 lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame. 1818 ∀Em. memory_inj Em cl_m cm_m → 1819 Z_of_nat stacksize < Z_two_power_nat 16 → 1820 alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 → 1821 ∀L, cl_env, cl_m1. 1822 exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 → 1823 (∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧ 1824 match c with 1825 [ Local ⇒ True 1826  Stack off ⇒ 1827 le O off ∧ le (sizeof ty + off) stacksize ∧ 1828 (∀v',off',t'. v≠v' → lookup' vartypes v' = return 〈Stack off',t'〉 → le (off' + sizeof t') off ∨ le (off + sizeof ty) off') 1829  Global _ ⇒ False 1830 ]) → 1831 ∃Em'. memory_inj Em' cl_m1 cm_m1 ∧ 1832 embedding_compatible Em Em' ∧ 1833 ∀v. Exists … (λx.\fst x = v) L → 1834 ∃b,c,t. lookup … cl_env v = Some ? b ∧ 1835 lookup' vartypes v = return 〈c,t〉 ∧ 1836 match c with 1837 [ Local ⇒ Em' b = None ? 1838  Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉 1839  Global _ ⇒ False 1840 ]. 1841 #vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L 1842 cut (block_implementable_bv cm_m1 cm_frame) 1843 [ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % // 1844 cases stacksize // ] #cm_bi 1845 lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi) 1846 lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid 1847 cut (∀b:block. ∀delta':offset. 1848 Em b=Some (block×offset) 〈cm_frame,delta'〉 → 1849 ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 → 1850 high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off) 1851 ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta') 1852 [ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V 1853 @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ] 1854 1855 generalize in match Em; Em generalize in match empty_env; elim L 1856 [ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc 1857 whd in cl_alloc:(??%%); destruct #H 1858 %{Em} % [ % [ @Inj  // ]  #v * ] 1859  * #v #ty #tl #IH 1860 #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1 1861 whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H 1862 cases (H v ty ?) [2: %1 % ] * 1863 [ #r * #L * 1864  #off * #L * * #off_low #off_high #other 1865 lapply (alloc_memory_inj_m1_to_m2 … (offset_of_Z off) cm_frame_valid … cm_bi … cl_alloc … Inj) 1866 [ #b #delta' #NE #E @(Hexisting … E … L) 1867  cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U 1868 [ /2/ 1869  @(transitive_Zle … HIGH) >unZoo 1870 [ <eq_plus_Zplus /2/ 1871  @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off)) 1872 [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/ 1873  @(transitive_Zlt … stacksize) [ <eq_plus_Zplus @(lt_to_Zlt … off_high)  // ] 1874 ] 1875 ] 1876 ] 1877  >unZoo 1878 [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc) 1879 *) 1749 1880 (* 1750 1881 lemma lset_inclusion_Exists : … … 1790 1921 subtrace corresponding to a measurable Clight subtrace. 1791 1922 *) 1792 (* WIP 1923 (* WIP 1924 include "common/ExtraMonads.ma". 1925 1793 1926 lemma clight_cminor_call : 1794 1927 ∀g,g'. … … 1831 1964 whd in STEP1:(??%%); destruct ] 1832 1965 cl_fd 1966 (* and the Cminor one must be Internal *) 1967 @('bind_inversion Htranslate) #cm_f #Htranslate' #E 1968 whd in E:(??%%); destruct 1969 1970 (* Invert function translation *) 1971 (* NB: if you want to examine the proof state in here, you probably want to 1972 turn off the pretty printer  it doesn't cope well with a large proof 1973 term. *) 1974 @('bind_inversion Htranslate') * * #lbls #Ilbls #ul #Hbuild_label_env 1975 whd in ⊢ (??%? → ?); 1976 @pair_as_elim #vartypes #stacksize #Hcharacterise 1977 letin uv ≝ (mk_tmpgen ?? [ ] ??) #H 1978 @('bind_inversion H) H #s0 #Htranslate_statement #H 1979 @('bind_inversion H) H * * #fgens #s1 #Is #Halloc_params 1980 letin cm_params ≝ (map ??? (fn_params cl_f)) 1981 whd in ⊢ (??%? → ?); 1982 letin cm_vars ≝ (map ??? (?@fn_vars cl_f)) #H 1983 @('bind_inversion H) H #D #Hcheck_distinct_env 1984 whd in ⊢ (??%% → ?); generalize in ⊢ (??(??(???????%))? → ?); 1985 (* It's safe to use the pretty printer again. *) 1986 #cm_Sinv #H destruct 1833 1987 1834 1988 (* Invert Clight STEP1 *) … … 1836 1990 cases (bindIO_inversion ??????? STEP1) STEP1 #cl_m2 * #BIND #STEP1 1837 1991 whd in STEP1:(??%%); destruct 1992 1993 whd whd in ⊢ (??%?); 1994 @pair_elim #cm_m1 #cm_frame #CM_ALLOC 1995 1996 (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f) 1997 We need to build an extended memory injection to reflect the new allocations; 1998 then the bind functions put the correct local variables in; 1999 then after execution the appropriate number of Cminor steps the stored values 2000 match. 2001 2002 Oh, and there are the locals too. 2003 2004 2005 alloc_memory_inj_m2 shows that embedding is fine after the Cminor alloc 2006 2007 ∀Em. memory_inj Em cl_m cm_m → 2008 (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) → 2009 exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 → 2010 alloc cm_m O (f_stacksize cm_f) = 〈cm_m1,cm_frame〉 → 2011 ∃Em'. 2012 memory_inj Em' cl_m1 cm_m1 ∧ 2013 (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) ∧ 2014 (∀v,v'. value_eq Em v v' → value_eq Em' v v') ∧ 2015 (∀b1.∀delta. Em' b1=Some ? 〈cm_frame,delta〉 → 2016 mem block b1 (blocks_of_env cl_env)). 2017 2018 ∀b. Em b = Em' b ∨ (Em b = None ? ∧ ∃off. Em' b = Some ? 〈cm_frame,off〉). 2019 2020 2021 translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f → 2022 All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args → 2023 exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 → 2024 ∃cm_en,Hcm_args_present. 2025 bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧ 2026 2027 1838 2028 *) 1839 2029 
src/Clight/toCminorMeasurable.ma
r3155 r3178 64 64 #ge #ge' #RG #Xs1 #Xs2 * // 65 65 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #E 66  #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 # H169 #H170 #E66  #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #E 67 67  #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #E 68 68 ] whd in E:(??%?); destruct … … 71 71 [ #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 * 72 72  #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 #H255 #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 #H266 * 73  #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 #H295 #H29673  #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 74 74  #H314 #H315 #H316 #H317 #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 #H331 #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 #H342 #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 #H356 #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 #H370 #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 * 75 75 ] (* FIXME *) cases daemon
Note: See TracChangeset
for help on using the changeset viewer.