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/Cminor/initialisation.ma

    r1631 r1872  
    66
    77(* XXX having to specify the return type in the match is annoying. *)
    8 definition init_expr : init_data → option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) ≝
     8definition init_expr : init_data → option (𝚺t:typ. expr t) ≝
    99λinit.
    10 match init return λ_.option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) with
    11 [ Init_int8 i          ⇒ Some ? (mk_DPair ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
    12 | Init_int16 i         ⇒ Some ? (mk_DPair ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
    13 | Init_int32 i         ⇒ Some ? (mk_DPair ?? Mint32 (Cst ? (Ointconst I32 i)))
    14 | Init_float32 f       ⇒ Some ? (mk_DPair ?? Mfloat32 (Cst ? (Ofloatconst f)))
    15 | Init_float64 f       ⇒ Some ? (mk_DPair ?? Mfloat64 (Cst ? (Ofloatconst f)))
     10match init return λ_.option (𝚺t:typ. expr t) with
     11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 i)))
     14| Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (mk_DPair ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
     17| Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
     18| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol id off)))
    1919].
    2020
     
    3434[ None ⇒ St_skip
    3535| Some x ⇒
    36     match x with [ mk_DPair chunk e ⇒
    37       St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
     36    match x with [ mk_DPair t e ⇒
     37      St_store t r (Cst ? (Oaddrsymbol id off)) e
    3838    ]
    3939].
Note: See TracChangeset for help on using the changeset viewer.