Changeset 1872 for src/common/AST.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/AST.ma

    r1640 r1872  
    9090#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    9191
     92(* Carefully defined to be convertably nonzero *)
    9293definition size_pointer : region → nat ≝
    93 λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     94λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
    9495
    9596(* We maintain some reasonable type information through the front end of the
     
    155156* * * #NE try @refl @False_ind @NE @refl
    156157qed.
     158
     159definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
     160 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
     161λsg1,sg2,P.
     162match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
     163[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
     164| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
     165].
     166
     167let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
     168  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
     169match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
     170[ I8  ⇒ λx. match sz2 return λsz. P ?? sz ? → P I8 ? sz ? with [ I8  ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     171| I16 ⇒ λx. match sz2 return λsz. P I16 sg1 sz sg2 → P I16 sg1 sz sg2 with [ I16 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     172| I32 ⇒ λx. match sz2 return λsz. P I32 sg1 sz sg2 → P I32 sg1 sz sg2 with [ I32 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     173].
     174
     175let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
     176  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
     177match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
     178[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
     179| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
     180| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
     181].
    157182
    158183(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
     
    189214λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
    190215
     216let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
     217  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
     218match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
     219[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
     220| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
     221].
     222
     223
    191224definition typesize : typ → nat ≝ λty.
    192225  match ty with
     
    231264  | Some t ⇒ t
    232265  ].
    233 
    234 (* * Memory accesses (load and store instructions) are annotated by
    235   a ``memory chunk'' indicating the type, size and signedness of the
    236   chunk of memory being accessed. *)
    237 
    238 inductive memory_chunk : Type[0] ≝
    239   | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
    240   | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
    241   | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
    242   | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
    243   | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
    244   | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
    245   | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
    246   | Mpointer : region → memory_chunk. (* pointer addressing given region *)
    247 
    248 definition typ_of_memory_chunk : memory_chunk → typ ≝
    249 λc. match c with
    250 [ Mint8signed ⇒ ASTint I8 Signed
    251 | Mint8unsigned ⇒ ASTint I8 Unsigned
    252 | Mint16signed ⇒ ASTint I16 Signed
    253 | Mint16unsigned ⇒ ASTint I16 Unsigned
    254 | Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
    255 | Mfloat32 ⇒ ASTfloat F32
    256 | Mfloat64 ⇒ ASTfloat F64
    257 | Mpointer r ⇒ ASTptr r
    258 ].
    259266
    260267(* * Initialization data for global variables. *)
Note: See TracChangeset for help on using the changeset viewer.