Changeset 1872 for src/RTLabs


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

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1713 r1872  
    105105      ! locals ← reg_store dst v' (locals f);
    106106      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    107   | St_op2 op dst src1 src2 l ⇒ λH.
     107  | St_op2 _ _ _  op dst src1 src2 l ⇒ λH.
    108108      ! v1 ← reg_retrieve (locals f) src1;
    109109      ! v2 ← reg_retrieve (locals f) src2;
    110       ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
     110      ! v' ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
    111111      ! locals ← reg_store dst v' (locals f);
    112112      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     
    298298  | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
    299299  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    300   | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     300  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    301301  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    302302  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
  • 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.