Changeset 1872 for src/common/Mem.ma


Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (9 years ago)
Author:
campbell
Message:

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r1599 r1872  
    124124(* * Operations on memory stores *)
    125125
    126 (* Memory reads and writes are performed by quantities called memory chunks,
    127   encoding the type, size and signedness of the chunk being addressed.
    128   The following functions extract the size information from a chunk. *)
    129 
    130 definition size_chunk : memory_chunk → nat ≝
    131   λchunk.match chunk with
    132   [ Mint8signed => 1
    133   | Mint8unsigned => 1
    134   | Mint16signed => 2
    135   | Mint16unsigned => 2
    136   | Mint32 => 4
    137   | Mfloat32 => 4
    138   | Mfloat64 => 8
    139   | Mpointer r ⇒ size_pointer r
     126definition pred_size_chunk : typ → nat ≝
     127  λchunk. match chunk with
     128  [ ASTint sz _ ⇒ pred (size_intsize sz)
     129  | ASTptr r ⇒ pred (size_pointer r)
     130  | ASTfloat sz ⇒ pred (size_floatsize sz)
    140131  ].
    141 
    142 definition pred_size_pointer : region → nat ≝
    143 λsp. match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
    144 
    145 definition pred_size_chunk : memory_chunk → nat ≝
    146   λchunk.match chunk with
    147   [ Mint8signed => 0
    148   | Mint8unsigned => 0
    149   | Mint16signed => 1
    150   | Mint16unsigned => 1
    151   | Mint32 => 3
    152   | Mfloat32 => 3
    153   | Mfloat64 => 7
    154   | Mpointer r ⇒ pred_size_pointer r
    155   ].
    156 
    157 alias symbol "plus" (instance 2) = "integer plus".
     132 
    158133lemma size_chunk_pred:
    159   ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
    160 #chunk cases chunk;//; #r cases r; @refl
    161 qed.
    162 
    163 lemma size_chunk_pos:
    164   ∀chunk. 0 < size_chunk chunk.
    165 #chunk >(size_chunk_pred ?) cases (pred_size_chunk chunk);
    166 normalize;//;
    167 qed.
     134  ∀chunk. typesize chunk = 1 + pred_size_chunk chunk.
     135* //
     136qed.
     137
    168138
    169139(* Memory reads and writes must respect alignment constraints:
     
    177147  appropriate for PowerPC and ARM. *)
    178148
    179 definition align_chunk : memory_chunk → Z ≝
     149definition align_chunk : typ → Z ≝
    180150  λchunk.match chunk return λ_.Z with
    181   [ Mint8signed ⇒ 1
    182   | Mint8unsigned ⇒ 1
    183   | Mint16signed ⇒ 1
    184   | Mint16unsigned ⇒ 1
    185   | _ ⇒ 1 ].
     151  [ ASTint _ _ ⇒ 1
     152  | ASTptr _ ⇒ 1
     153  | ASTfloat _ ⇒ 1
     154  ].
    186155
    187156lemma align_chunk_pos:
     
    191160
    192161lemma align_size_chunk_divides:
    193   ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    194 #chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/;
     162  ∀chunk. (align_chunk chunk ∣ typesize chunk).
     163#chunk cases chunk * [ 1,2,3: * ] normalize /3 by witness/
    195164qed.
    196165
    197166lemma align_chunk_compat:
    198167  ∀chunk1,chunk2.
    199     size_chunk chunk1 = size_chunk chunk2 →
     168    typesize chunk1 = typesize chunk2 →
    200169      align_chunk chunk1 = align_chunk chunk2.
    201 #chunk1 #chunk2
    202 cases chunk1; try ( #r1 #cases #r1 )
    203 cases chunk2; try ( #r2 #cases #r2 )
    204 normalize;//;
     170* * [ 1,2,3: * ]
     171* * [ 1,2,3,12,13,14,23,24,25: * ]
     172normalize //
    205173qed.
    206174
     
    595563*)
    596564
    597 inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z)
     565inductive valid_access (m: mem) (chunk: typ) (r: region) (b: block) (ofs: Z)
    598566            : Prop ≝
    599567  | valid_access_intro:
    600568      valid_block m b →
    601569      low_bound m b ≤ ofs →
    602       ofs + size_chunk chunk ≤ high_bound m b →
     570      ofs + typesize chunk ≤ high_bound m b →
    603571      (align_chunk chunk ∣ ofs) →
    604572      pointer_compat b r →
     
    610578(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    611579let rec in_bounds
    612   (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : 
     580  (m:mem) (chunk:typ) (r:region) (b:block) (ofs:Z) on b : 
    613581    Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?.
    614582cases b #br #bi
    615583@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
    616584[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
    617     [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
     585    [ @(Zleb_elim_Type0 (ofs + typesize chunk) (high_bound m (mk_block br bi))) #Hhi
    618586        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    619587          [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl
     
    653621  by a pointer with region [r]. *)
    654622
    655 definition load : memory_chunk → mem → region → block → Z → option val ≝
     623definition load : typ → mem → region → block → Z → option val ≝
    656624λchunk,m,r,b,ofs.
    657625  match in_bounds m chunk r b ofs with
     
    676644  as a single value [addr], which must be a pointer value. *)
    677645
    678 let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
     646let rec loadv (chunk:typ) (m:mem) (addr:val) on addr : option val ≝
    679647  match addr with
    680648  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
     
    684652   in block [b]. *)
    685653
    686 definition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝
     654definition unchecked_store : typ → mem → block → Z → val → mem ≝
    687655λchunk,m,b,ofs,v.
    688656  let c ≝ (blocks m b) in
     
    701669  by a pointer with region [r]. *)
    702670
    703 definition store : memory_chunk → mem → region → block → Z → val → option mem ≝
     671definition store : typ → mem → region → block → Z → val → option mem ≝
    704672λchunk,m,r,b,ofs,v.
    705673  match in_bounds m chunk r b ofs with
     
    722690  as a single value [addr], which must be a pointer value. *)
    723691
    724 definition storev : memory_chunk → mem → val → val → option mem ≝
     692definition storev : typ → mem → val → val → option mem ≝
    725693λchunk,m,addr,v.
    726694  match addr with
     
    753721lemma valid_access_compat:
    754722  ∀m,chunk1,chunk2,r,b,ofs.
    755   size_chunk chunk1 = size_chunk chunk2 →
     723  typesize chunk1 = typesize chunk2 →
    756724  valid_access m chunk1 r b ofs →
    757725  valid_access m chunk2 r b ofs.
     
    34983466lemma in_bounds_equiv:
    34993467  ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A.
    3500   size_chunk chunk1 = size_chunk chunk2 →
     3468  typesize chunk1 = typesize chunk2 →
    35013469  (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
    35023470  (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
     
    35123480lemma storev_8_signed_unsigned:
    35133481  ∀m,a,v.
    3514   storev Mint8signed m a v = storev Mint8unsigned m a v.
     3482  storev (ASTint I8 Signed) m a v = storev (ASTint I8 Unsigned) m a v.
    35153483#m #a #v whd in ⊢ (??%%); elim a //
    35163484#ptr whd in ⊢ (??%%);
    3517 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
     3485>(in_bounds_equiv (ASTint I8 Signed) (ASTint I8 Unsigned) … (option mem) ???) //
    35183486qed.
    35193487
    35203488lemma storev_16_signed_unsigned:
    35213489  ∀m,a,v.
    3522   storev Mint16signed m a v = storev Mint16unsigned m a v.
     3490  storev (ASTint I16 Signed) m a v = storev (ASTint I16 Unsigned) m a v.
    35233491#m #a #v whd in ⊢ (??%%); elim a //
    35243492#ptr whd in ⊢ (??%%);
    3525 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
     3493>(in_bounds_equiv (ASTint I16 Signed) (ASTint I16 Unsigned) … (option mem) ???) //
    35263494qed.
    35273495
Note: See TracChangeset for help on using the changeset viewer.