Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/MemProperties.ma

    r2448 r2468  
    144144#m1 #m2 #Hloadsim #ptr #ty #v
    145145cases ty
    146 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
    147 | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
     146[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
     147| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
    148148whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
    149 [ 1,7,8: #Habsurd destruct (Habsurd)
    150 | 5,6: #H @H
    151 | 2,3,4,9:
     149[ 1,6,7: #Habsurd destruct (Habsurd)
     150| 4,5: #H @H
     151| 2,3,8:
    152152  generalize in match (mk_pointer (pblock ptr) (poff ptr));
    153153  elim (typesize ?)
    154   [ 1,3,5,7: #p #H @H
    155   | 2,4,6,8: #n' #Hind #p
     154  [ 1,3,5: #p #H @H
     155  | *: #n' #Hind #p
    156156      lapply (load_sim_loadn … Hloadsim (S n') p)
    157157      cases (loadn m1 p (S n')) normalize nodelta
     
    200200cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
    201201normalize nodelta try // #Habsurd destruct (Habsurd)
     202qed.
     203
     204lemma bestorev_to_valid_pointer_after : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer res ptr = true.
     205* #contents #next #nextpos #ptr #v #res
     206whd in match (bestorev ???);
     207whd in match (valid_pointer ??); #Hvalid
     208cases (if_opt_inversion ???? Hvalid) #Hnextblock normalize nodelta -Hvalid #Hvalid
     209cases (if_opt_inversion ???? Hvalid) #Hin_bounds #Heq destruct (Heq) normalize
     210>Hnextblock normalize nodelta cases (block_region (pblock ptr)) normalize nodelta
     211>eqZb_z_z normalize nodelta @Hin_bounds
    202212qed.
    203213
     
    591601] qed.
    592602
     603(* extension of [bestorev_to_valid_pointer] to storen *)
     604lemma storen_to_valid_pointer :
     605  ∀data,xd,m,ptr,m'. storen m ptr (xd::data) = Some ? m' →
     606    (∀b.low (blocks m' b) = low (blocks m b) ∧
     607         high (blocks m' b) = high (blocks m b)) ∧
     608    nextblock m' = nextblock m ∧         
     609    valid_pointer m ptr = true ∧
     610    valid_pointer m' ptr = true.
     611#data elim data
     612[ 1: #xd #m #ptr #res #Hstoren whd in Hstoren:(??%?);
     613     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren'
     614     normalize in Hstoren'; destruct (Hstoren')
     615     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
     616     lapply (bestorev_to_valid_pointer … Hbestorev) #Hvalid_ptr @conj try @conj try @conj try assumption
     617     @(bestorev_to_valid_pointer_after … Hbestorev)
     618| 2: #hd #tl #Hind #xd #m #ptr #res whd in match (storen ???); #Hstoren
     619     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' -Hstoren
     620     whd in match (shift_pointer ???) in Hstoren';
     621     lapply (bestorev_to_valid_pointer … Hbestorev) #H @conj try @conj try @conj try //
     622     lapply (Hind … Hstoren') * * * #Hbounds #Hnext #Hvalid1 #Hvalid2
     623     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
     624     [ 1: #b @conj cases (Hbounds b) #HG #HH cases (HB b) #HI #HJ try //
     625     | 2: >Hnext >HA @refl ]
     626     @valid_pointer_of_Prop @conj try @conj try @conj
     627     cases (Hbounds (pblock ptr)) #HG #HH cases (HB (pblock ptr)) #HI #HJ
     628     [ 2: cases HC #Hlow #_ whd in match (low_bound ??);
     629           whd in match (Z_of_offset ?) in Hlow;
     630           >HG >HI @Hlow
     631     | 3: cases HC #_ #Hhigh whd in match (high_bound ??); >HH >HJ @Hhigh ]
     632     lapply (valid_pointer_to_Prop … Hvalid2) * * #Hnext #Hlow #Hhigh //
     633] qed.
     634
     635lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl.
     636*
     637[ 2:  * /3 by ex_intro/ * #i
     638      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
     639           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
     640           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
     641      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
     642           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
     643           <(vsplit_prod … Heq) normalize nodelta
     644           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
     645            /3 by ex_intro/
     646      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
     647           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
     648           <(vsplit_prod … Heq) normalize nodelta
     649           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
     650           <(vsplit_prod … Heq') normalize nodelta
     651           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
     652           <(vsplit_prod … Heq'') normalize nodelta
     653           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
     654            /3 by ex_intro/ ]
     655| 1: #sz #sg * /3 by ex_intro/ * #i
     656      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
     657           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
     658           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
     659      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
     660           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
     661           <(vsplit_prod … Heq) normalize nodelta
     662           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
     663            /3 by ex_intro/
     664      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
     665           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
     666           <(vsplit_prod … Heq) normalize nodelta
     667           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
     668           <(vsplit_prod … Heq') normalize nodelta
     669           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
     670           <(vsplit_prod … Heq'') normalize nodelta
     671           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
     672            /3 by ex_intro/ ]
     673] qed.           
     674
     675lemma storen_to_valid_pointer_fe_to_be :
     676  ∀typ,v,m,ptr,m'. storen m ptr (fe_to_be_values typ v) = Some ? m' →
     677    (∀b.low (blocks m' b) = low (blocks m b) ∧
     678         high (blocks m' b) = high (blocks m b)) ∧
     679    nextblock m' = nextblock m ∧         
     680    valid_pointer m ptr = true ∧
     681    valid_pointer m' ptr = true.
     682#typ #v cases (fe_to_be_values_nonempty … typ v) #hd * #tl #Heq >Heq
     683@storen_to_valid_pointer
     684qed.
     685
    593686lemma storen_beloadv_ok :
    594687  ∀m,m',b,ofs,hd,tl.
     
    709802   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
    710803lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
    711 * try //
    712 [ 1: * try //
    713 | 2: * try //
    714 ] qed.
     804* try // * try // qed.
    715805
    716806(* Lifting bound on make_list *)
     
    746836  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
    747837#ty cases ty
    748 [ 3: #fsz #v whd in match (fe_to_be_values ??);
     838[ 1: #sz #sg ]
     839#v whd in match (fe_to_be_values ??);
    749840     cases v normalize nodelta
    750      [ 1: @makelist_bounded @typesize_bounded
    751      | 2: * normalize nodelta #bv
     841     [ 1,5: @makelist_bounded @typesize_bounded
     842     | 2,6: * normalize nodelta #bv
    752843          >map_bounded >bytes_of_bitvector_bounded //
    753      | 3: #fl @makelist_bounded @typesize_bounded
    754      | 4: //
    755      | 5: #ptr // ]
    756 | 2: #v whd in match (fe_to_be_values ??);
    757      cases v normalize nodelta
    758      [ 1: @makelist_bounded @typesize_bounded
    759      | 2: * normalize nodelta #bv
    760           >map_bounded >bytes_of_bitvector_bounded //
    761      | 3: #fl @makelist_bounded @typesize_bounded
    762      | 4: //
    763      | 5: #ptr // ]
    764 | 1: #sz #sg #v whd in match (fe_to_be_values ??);
    765      cases v normalize nodelta
    766      [ 1: @makelist_bounded @typesize_bounded
    767      | 2: * normalize nodelta #bv
    768           >map_bounded >bytes_of_bitvector_bounded //
    769      | 3: #fl @makelist_bounded @typesize_bounded
    770      | 4: //
    771      | 5: #ptr // ]
    772 ] qed.
    773 
     844     | 3,7: //
     845     | 4,8: #ptr // ]
     846qed.     
    774847
    775848lemma mem_bounds_after_store_value_of_type :
     
    782855lapply (fe_to_be_values_bounded (typ_of_type ty) v)
    783856cases ty
    784 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    785 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     857[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
     858| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
    786859whd in match (typ_of_type ?); #Hbounded
    787860whd in match (store_value_of_type ?????);
    788 [ 1,5,6,7,8: #Habsurd destruct (Habsurd)
     861[ 1,4,5,6,7: #Habsurd destruct (Habsurd)
    789862| *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren)
    790863     * * * * * #Hnextblock #Hbounds_eq #Hnonempty
     
    814887    [ Vptr p ⇒ True
    815888    | _ ⇒ False ]
    816   | ASTfloat fsz ⇒
    817     match v with
    818     [ Vfloat _ ⇒ True
    819     | _ ⇒ False ]   
    820889  ].
    821890
     
    835904     whd in match (fe_to_be_values ??); cases v
    836905     normalize in ⊢ (% → ?);
    837      [ 1,4: @False_ind
     906     [ 1,3: @False_ind
    838907     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
    839908          >map_bounded >bytes_of_bitvector_bounded cases sz' //
    840      | 3: #f normalize in ⊢ (% → ?); @False_ind
    841      | 5: #p normalize in ⊢ (% → ?); @False_ind ]
     909     | 4: #p normalize in ⊢ (% → ?); @False_ind ]
    842910| 2: #v cases v
    843911     normalize in ⊢ (% → ?);
    844      [ 1,4: @False_ind
     912     [ 1,3: @False_ind
    845913     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
    846      | 3: #f normalize in ⊢ (% → ?); @False_ind
    847      | 5: #p #_ // ]
    848 | 3: #fsz #v cases v
    849      normalize in ⊢ (% → ?);
    850      [ 1: @False_ind
    851      | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
    852      | 3: #f #_ cases fsz //
    853      | 4: @False_ind
    854      | 5: #p normalize in ⊢ (% → ?); @False_ind ]
    855 ] qed.
    856 
     914     | 4: #p #_ // ]
     915] qed.
    857916
    858917(* Not verified for floats atm. Restricting to integers. *)
     
    863922whd in match (fe_to_be_values ??);
    864923cases v normalize in ⊢ (% → ?);
    865 [ 1,4: @False_ind
    866 | 3: #f @False_ind
    867 | 5: #p @False_ind
     924[ 1,3: @False_ind
     925| 4: #p @False_ind
    868926| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
    869927     cases sz' in i'; #i normalize nodelta
     
    924982#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
    925983cases v in H; normalize nodelta
    926 [ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #vf #_ @False_ind | 4: #_ @False_ind | 5: #vp #_ @False_ind ]
     984[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #_ @False_ind | 4: #vp #_ @False_ind ]
    927985#Heq >Heq in H; #H
    928986(* The lack of control on unfolds is extremely annoying. *)
Note: See TracChangeset for help on using the changeset viewer.