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