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/semantics.ma

    r1713 r1872  
    104104    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
    105105    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    106     do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
     106    do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
    107107    OK ? 〈tr1 ⧺ tr2, r〉
    108 | Mem rg ty chunk e ⇒ λEnv.
     108| Mem ty rg e ⇒ λEnv.
    109109    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    110     do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
     110    do r ← opt_to_res … (msg FailedLoad) (loadv ty m v);
    111111    OK ? 〈tr, r〉
    112112| Cond sz sg ty e' e1 e2 ⇒ λEnv.
     
    306306        let en' ≝ update_present ?? en id ? v in
    307307        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    308     | St_store _ _ chunk edst e ⇒ λInv.
     308    | St_store ty _ edst e ⇒ λInv.
    309309        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
    310310        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    311         ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
     311        ! m' ← opt_to_res … (msg FailedStore) (storev ty m vdst v);
    312312        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
    313313
Note: See TracChangeset for help on using the changeset viewer.