Changeset 3178


Ignore:
Timestamp:
Apr 25, 2013, 6:03:24 PM (4 years ago)
Author:
campbell
Message:

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r2645 r3178  
    346346
    347347(* * Natural alignment of a type, in bytes. *)
    348 let rec alignof (t: type) : nat ≝ (*1*)
    349 (* these are old values for 32 bit machines *)
     348let rec alignof (t: type) : nat ≝ 1.
     349(* these are old values for 32 bit machines
    350350  match t with
    351351  [ Tvoid ⇒ 1
     
    363363  [ Fnil ⇒ 1
    364364  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
    365   ].
     365  ].*)
    366366
    367367(*
     
    412412                        (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f')
    413413  ].
    414 
     414(*
    415415lemma alignof_fields_pos:
    416416  ∀f. alignof_fields f > 0.
    417417@fieldlist_ind //;
    418418#i #t #fs' #IH @max_r @IH qed.
    419 
     419*)
    420420lemma alignof_pos:
    421421  ∀t. alignof t > 0.
    422 #t elim t; normalize; //;
     422#t elim t; normalize; //;(*
    423423[ 1,2: #z cases z; /2/;
    424424| 3,4: #i @alignof_fields_pos
    425 ] qed.
     425]*) qed.
    426426
    427427(* * Size of a type, in bytes. *)
     
    450450  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
    451451  ].
    452 (* TODO: needs some Z_times results
     452
    453453lemma sizeof_pos:
    454454  ∀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(*
    482467Lemma sizeof_struct_incr:
    483468  forall fld pos, pos <= sizeof_struct fld pos.
  • src/Clight/memoryInjections.ma

    r2822 r3178  
    759759#Halloc destruct (Halloc) /2/
    760760qed.
     761
     762lemma 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 *)
     767whd in match (alloc ???(*?*)); whd in match (valid_block ??);
     768#Halloc destruct (Halloc) /2/
     769qed.
     770
    761771
    762772(* All data in a valid block is unchanged after an alloc. *)
     
    14671477] qed.   
    14681478
     1479(* And show the compatibility of the new injection. *)
     1480
     1481lemma 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
     1491whd
     1492#b @eq_block_elim
     1493[ #E destruct %1 @(mi_freeblock … MI) /2/
     1494| #_ %2 %
     1495] qed.
     1496
     1497
    14691498(* -------------------------------------- *)
    14701499(* Lemmas pertaining to [free] *)
  • src/Clight/toCminorCorrectness.ma

    r3170 r3178  
    17471747#A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed.
    17481748
     1749lemma 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/
     1757qed.
     1758
     1759(* TODO: move *)
     1760lemma 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
     1764whd in E:(??%%); destruct
     1765whd in ⊢ (??%?); >update_block_s
     1766%
     1767qed.
     1768
     1769lemma 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
     1773whd in E:(??%%); destruct
     1774whd in ⊢ (??%?); >update_block_s
     1775%
     1776qed.
     1777
     1778(* Weaker version of Zlt_to_Zle *)
     1779lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y.
     1780#x #y #H
     1781@(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H
     1782qed.
     1783
     1784axiom unZoo : ∀off:Z.
     1785  off < Z_two_power_nat 16 →
     1786  Zoo (offset_of_Z off) = off.
     1787
     1788lemma 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
     1794lemma 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
     1799qed.
     1800
     1801lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z.
     1802/2/
     1803qed.
     1804
     1805lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y.
     1806/2/
     1807qed.
     1808
     1809theorem 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
     1812qed.
     1813
     1814
     1815(* This roughly corresponds to lemma 69 of Leroy and Blazy *)
     1816(*
     1817lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame.
     1818∀Em. memory_inj Em cl_m cm_m →
     1819Z_of_nat stacksize < Z_two_power_nat 16 →
     1820alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 →
     1821∀L, cl_env, cl_m1.
     1822exec_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
     1842cut (block_implementable_bv cm_m1 cm_frame)
     1843[ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % //
     1844  cases stacksize // ] #cm_bi
     1845lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi)
     1846lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid
     1847cut (∀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
     1855generalize 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*)
    17491880(*
    17501881lemma lset_inclusion_Exists :
     
    17901921   subtrace corresponding to a measurable Clight subtrace.
    17911922 *)
    1792 (* WIP
     1923(* WIP
     1924include "common/ExtraMonads.ma".
     1925
    17931926lemma clight_cminor_call :
    17941927    ∀g,g'.
     
    18311964      whd in STEP1:(??%%); destruct ]
    18321965  -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
    18331987
    18341988  (* Invert Clight STEP1 *) 
     
    18361990  cases (bindIO_inversion ??????? STEP1) -STEP1 #cl_m2 * #BIND #STEP1
    18371991  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)
     1997We need to build an extended memory injection to reflect the new allocations;
     1998then the bind functions put the correct local variables in;
     1999then after execution the appropriate number of Cminor steps the stored values
     2000match.
     2001
     2002Oh, and there are the locals too.
     2003
     2004
     2005alloc_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〉) →
     2009exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 →
     2010alloc 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
     2021translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f →
     2022All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
     2023exec_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
    18382028*)
    18392029
  • src/Clight/toCminorMeasurable.ma

    r3155 r3178  
    6464  #ge #ge' #RG #Xs1 #Xs2 * //
    6565  [ #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 #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 #E
    6767  | #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
    6868  ] whd in E:(??%?); destruct
     
    7171  [ #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 *
    7272  | #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 #H296
     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
    7474  | #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 *
    7575  ] (* FIXME *) cases daemon
Note: See TracChangeset for help on using the changeset viewer.