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