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).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.