Changeset 1872 for src/common


Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (8 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).

Location:
src/common
Files:
5 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. *)
  • src/common/FrontEndOps.ma

    r1545 r1872  
    4444  | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
    4545
    46 inductive binary_operation : Type[0] ≝
    47   | Oadd: binary_operation                 (**r integer addition *)
    48   | Osub: binary_operation                 (**r integer subtraction *)
    49   | Omul: binary_operation                 (**r integer multiplication *)
    50   | Odiv: binary_operation                 (**r integer signed division *)
    51   | Odivu: binary_operation                (**r integer unsigned division *)
    52   | Omod: binary_operation                 (**r integer signed modulus *)
    53   | Omodu: binary_operation                (**r integer unsigned modulus *)
    54   | Oand: binary_operation                 (**r bitwise ``and'' *)
    55   | Oor: binary_operation                  (**r bitwise ``or'' *)
    56   | Oxor: binary_operation                 (**r bitwise ``xor'' *)
    57   | Oshl: binary_operation                 (**r left shift *)
    58   | Oshr: binary_operation                 (**r right signed shift *)
    59   | Oshru: binary_operation                (**r right unsigned shift *)
    60   | Oaddf: binary_operation                (**r float addition *)
    61   | Osubf: binary_operation                (**r float subtraction *)
    62   | Omulf: binary_operation                (**r float multiplication *)
    63   | Odivf: binary_operation                (**r float division *)
    64   | Ocmp: comparison -> binary_operation  (**r integer signed comparison *)
    65   | Ocmpu: comparison -> binary_operation (**r integer unsigned comparison *)
    66   | Ocmpf: comparison -> binary_operation (**r float comparison *)
    67   | Oaddp: binary_operation                (**r add an integer to a pointer *)
    68   | Osubpi: binary_operation               (**r subtract int from a pointers *)
    69   | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
    70   | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
     46inductive binary_operation : typ → typ → typ → Type[0] ≝
     47  | Oadd:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer addition *)
     48  | Osub:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer subtraction *)
     49  | Omul:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer multiplication *)
     50  | Odiv:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed division *)
     51  | Odivu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned division *)
     52  | Omod:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed modulus *)
     53  | Omodu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned modulus *)
     54  | Oand:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``and'' *)
     55  | Oor:   ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``or'' *)
     56  | Oxor:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``xor'' *)
     57  | Oshl:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r left shift *)
     58  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
     59  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
     60  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float addition *)
     61  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float subtraction *)
     62  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float multiplication *)
     63  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float division *)
     64  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
     65  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
     66  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
     67  | Oaddp: ∀sz,r.  binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r add an integer to a pointer *)
     68  | Osubpi: ∀sz,r. binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r subtract int from a pointers *)
     69  | Osubpp: ∀sz,r1,r2. binary_operation (ASTptr r1)      (ASTptr r2)          (ASTint sz Signed)   (**r subtract two pointers *)
     70  | Ocmpp: ∀r,sg'. comparison → binary_operation (ASTptr r) (ASTptr r) (ASTint I8 sg').  (**r compare pointers *)
    7171
    7272
     
    361361  | _ ⇒ None ? ].
    362362
     363definition FEtrue : val ≝ Vint I8 (repr I8 1).
     364definition FEfalse : val ≝ Vint I8 (repr I8 0).
     365definition FE_of_bool : bool → val ≝
     366λb. if b then FEtrue else FEfalse.
     367
    363368definition ev_cmp_match : comparison → option val ≝ λc.
    364369  match c with
    365   [ Ceq ⇒ Some ? Vtrue
    366   | Cne ⇒ Some ? Vfalse
     370  [ Ceq ⇒ Some ? FEtrue
     371  | Cne ⇒ Some ? FEfalse
    367372  | _   ⇒ None ?
    368373  ].
     
    370375definition ev_cmp_mismatch : comparison → option val ≝ λc.
    371376  match c with
    372   [ Ceq ⇒ Some ? Vfalse
    373   | Cne ⇒ Some ? Vtrue
     377  [ Ceq ⇒ Some ? FEfalse
     378  | Cne ⇒ Some ? FEtrue
    374379  | _   ⇒ None ?
    375380  ].
     
    379384  [ Vint sz1 n1 ⇒ match v2 with
    380385    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    381                     (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
     386                    (λn1. Some ? (FE_of_bool (cmp_int ? c n1 n2)))
    382387                    (None ?)
    383388    | _ ⇒ None ? ]
     
    389394    [ Vptr ptr2 ⇒
    390395        if eq_block (pblock ptr1) (pblock ptr2)
    391         then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
     396        then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    392397        else ev_cmp_mismatch c
    393398    | Vnull r2 ⇒ ev_cmp_mismatch c
     
    405410  [ Vint sz1 n1 ⇒ match v2 with
    406411    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    407                     (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
     412                    (λn1. Some ? (FE_of_bool (cmpu_int ? c n1 n2)))
    408413                    (None ?)
    409414    | _ ⇒ None ? ]
     
    413418  match v1 with
    414419  [ Vfloat f1 ⇒ match v2 with
    415     [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
    416     | _ ⇒ None ? ]
    417   | _ ⇒ None ? ].
    418 
    419 definition eval_binop : binary_operation → val → val → option val ≝
    420 λop.
     420    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
     421    | _ ⇒ None ? ]
     422  | _ ⇒ None ? ].
     423
     424definition eval_binop : ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
     425λt1,t2,t',op.
    421426  match op with
    422   [ Oadd ⇒ ev_add
    423   | Osub ⇒ ev_sub
    424   | Omul ⇒ ev_mul
    425   | Odiv ⇒ ev_divs
    426   | Odivu ⇒ ev_divu
    427   | Omod ⇒ ev_mods
    428   | Omodu ⇒ ev_modu
    429   | Oand ⇒ ev_and
    430   | Oor ⇒ ev_or
    431   | Oxor ⇒ ev_xor
    432   | Oshl ⇒ ev_shl
    433   | Oshr ⇒ ev_shr
    434   | Oshru ⇒ ev_shru
    435   | Oaddf ⇒ ev_addf
    436   | Osubf ⇒ ev_subf
    437   | Omulf ⇒ ev_mulf
    438   | Odivf ⇒ ev_divf
    439   | Ocmp c ⇒ ev_cmp c
    440   | Ocmpu c ⇒ ev_cmpu c
    441   | Ocmpf c ⇒ ev_cmpf c
    442   | Oaddp ⇒ ev_addp
    443   | Osubpi ⇒ ev_subpi
    444   | Osubpp sz ⇒ ev_subpp sz
    445   | Ocmpp c ⇒ ev_cmpp c
    446   ].
    447 
     427  [ Oadd _ _ ⇒ ev_add
     428  | Osub _ _ ⇒ ev_sub
     429  | Omul _ _ ⇒ ev_mul
     430  | Odiv _ ⇒ ev_divs
     431  | Odivu _ ⇒ ev_divu
     432  | Omod _ ⇒ ev_mods
     433  | Omodu _ ⇒ ev_modu
     434  | Oand _ _ ⇒ ev_and
     435  | Oor _ _ ⇒ ev_or
     436  | Oxor _ _ ⇒ ev_xor
     437  | Oshl _ _ ⇒ ev_shl
     438  | Oshr _ _ ⇒ ev_shr
     439  | Oshru _ _ ⇒ ev_shru
     440  | Oaddf _ ⇒ ev_addf
     441  | Osubf _ ⇒ ev_subf
     442  | Omulf _ ⇒ ev_mulf
     443  | Odivf _ ⇒ ev_divf
     444  | Ocmp _ _ _ c ⇒ ev_cmp c
     445  | Ocmpu _ _ c ⇒ ev_cmpu c
     446  | Ocmpf _ _ c ⇒ ev_cmpf c
     447  | Oaddp _ _ ⇒ ev_addp
     448  | Osubpi _ _ ⇒ ev_subpi
     449  | Osubpp sz _ _ ⇒ ev_subpp sz
     450  | Ocmpp _ _ c ⇒ ev_cmpp c
     451  ].
     452
     453lemma eval_binop_typ_correct : ∀t1,t2,t',op,v1,v2,v'.
     454  val_typ v1 t1 → val_typ v2 t2 →
     455  eval_binop t1 t2 t' op v1 v2 = Some ? v' →
     456  val_typ v' t'.
     457#t1x #t2x #tx' *
     458[ 1,2,3,8,9,10:
     459  #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     460  whd in ⊢ (??%? → ?); >intsize_eq_elim_true #E destruct //
     461| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     462  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_s ???) [ | #res ] #E whd in E:(??%?); destruct //
     463| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     464  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_u ???) [ | #res ] #E whd in E:(??%?); destruct //
     465| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     466  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_s ???) [ | #res ] #E whd in E:(??%?); destruct //
     467| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     468  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_u ???) [ | #res ] #E whd in E:(??%?); destruct //
     469(* shifts *)
     470| 11,12,13: #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     471  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
     472(* floats *)
     473| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     474  whd in ⊢ (??%? → ?); #E destruct //
     475(* comparisons *)
     476| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     477  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmp_int ????) #E destruct //
     478| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     479  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
     480| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     481  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
     482(* pointers *)
     483| 21,22: #sz #r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c #o ] @(elim_val_typ … V2) #i2
     484  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
     485| #sz #r1 #r2 #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     486  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
     487| #r #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     488  whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
     489] qed.
     490
     491
  • src/common/Globalenvs.ma

    r1599 r1872  
    406406  let r ≝ block_region m b in
    407407  match id with
    408   [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
    409   | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
    410   | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
    411   | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
    412   | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     408  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m r b p (Vint I8 n)
     409  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m r b p (Vint I16 n)
     410  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m r b p (Vint I32 n)
     411  | Init_float32 n ⇒ store (ASTfloat F32) m r b p (Vfloat n)
     412  | Init_float64 n ⇒ store (ASTfloat F64) m r b p (Vfloat n)
    413413  | Init_addrof r' symb ofs ⇒
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
     418        [ inl pc ⇒ store (ASTptr r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
    421421      ]
    422422  | Init_space n ⇒ Some ? m
    423   | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r')
     423  | Init_null r' ⇒ store (ASTptr r') m r b p (Vnull r')
    424424  ].
    425425
  • 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
  • src/common/Values.ma

    r1545 r1872  
    470470       should we be able to extract bytes? *)
    471471
    472 let rec load_result (chunk: memory_chunk) (v: val) ≝
     472let rec load_result (chunk: typ) (v: val) ≝
    473473  match v with
    474474  [ Vint sz n ⇒
    475475    match chunk with
    476     [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
    477     | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
    478     | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
    479     | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
    480     | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
     476    [ ASTint sz' sg ⇒ if eq_intsize sz sz' then v else Vundef
    481477    | _ ⇒ Vundef
    482478    ]
    483479  | Vptr ptr ⇒
    484480    match chunk with
    485     [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
     481    [ ASTptr r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
    486482    | _ ⇒ Vundef
    487483    ]
    488484  | Vnull r ⇒
    489485    match chunk with
    490     [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
     486    [ ASTptr r' ⇒ if eq_region r r' then Vnull r else Vundef
    491487    | _ ⇒ Vundef
    492488    ]
    493489  | Vfloat f ⇒
    494490    match chunk with
    495     [ Mfloat32 ⇒ Vfloat(singleoffloat f)
    496     | Mfloat64 ⇒ Vfloat f
     491    [ ASTfloat sz ⇒ match sz with [ F32 ⇒ Vfloat(singleoffloat f) | F64 ⇒ Vfloat f ]
    497492    | _ ⇒ Vundef
    498493    ]
     
    10851080  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    10861081#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
    1087 [ 8: #r ] whd in ⊢ (?%?); //;
     1082[ #sz #sg | #r | #sz ] whd in ⊢ (?%?); //;
    10881083qed.
    10891084
Note: See TracChangeset for help on using the changeset viewer.