Changeset 1872 for src/RTLabs/syntax.ma


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/RTLabs/syntax.ma

    r1705 r1872  
    1414| St_const : register → constant → label → statement
    1515| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    16 | St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    17 | St_load : memory_chunk → register → register → label → statement
    18 | St_store : memory_chunk → register → register → label → statement
     16| St_op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
     17| St_load : typ → register → register → label → statement
     18| St_store : typ → register → register → label → statement
    1919| St_call_id : ident → list register → option register → label → statement
    2020| St_call_ptr : register → list register → option register → label → statement
     
    4343| St_const _ _ l ⇒ P l
    4444| St_op1 _ _ _ _ _ l ⇒ P l
    45 | St_op2 _ _ _ _ l ⇒ P l
     45| St_op2 _ _ _ _ _ _ _ l ⇒ P l
    4646| St_load _ _ _ l ⇒ P l
    4747| St_store _ _ _ l ⇒ P l
Note: See TracChangeset for help on using the changeset viewer.