Changeset 1872 for src/Cminor


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/Cminor
Files:
4 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].
  • 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
  • src/Cminor/syntax.ma

    r1680 r1872  
    1010| Cst : ∀t. constant → expr t
    1111| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    12 | Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    13 | Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
     12| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
     13| Mem : ∀t,r. expr (ASTptr r) → expr t
    1414| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1515| Ecost : ∀t. costlabel → expr t → expr t.
     
    2222| Op1 _ _ _ e ⇒ expr_vars ? e P
    2323| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    24 | Mem _ _ _ e ⇒ expr_vars ? e P
     24| Mem _ _ e ⇒ expr_vars ? e P
    2525| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
    2626| Ecost _ _ e ⇒ expr_vars ? e P
     
    4040| St_skip : stmt
    4141| St_assign : ∀t. ident → expr t → stmt
    42 | St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
     42| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    4444| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     
    8282match s with
    8383[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    84 | St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     84| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    8585| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8686(*
     
    115115[ //
    116116| #t #id #e * /4/
    117 | #t #r #q #e1 #e2 * /4/
     117| #t #r #e1 #e2 * /4/
    118118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
    119119(*
  • src/Cminor/toRTLabs.ma

    r1680 r1872  
    526526    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
    527527    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    528     let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
     528    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
    529529    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
    530530    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    531531      «pi1 … f, ?»
    532 | Mem _ _ q e' ⇒ λEnv,dst.
     532| Mem t _ e' ⇒ λEnv,dst.
    533533    let ❬f,r❭ ≝ choose_reg … e' f Env in
    534     let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
     534    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
    535535    let f ≝ add_expr … env ? e' Env f «r,?» in
    536536      «pi1 … f, ?»
     
    682682    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    683683    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    684 | St_store _ _ q e1 e2 ⇒ λEnv.
     684| St_store t _ e1 e2 ⇒ λEnv.
    685685    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    686686    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
    687     let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
     687    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    688688    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
    689689    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
     
    752752      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    753753      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    754       let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
     754      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmpu I8 Unsigned Ceq) (* signed? *) br r cr) f ?? in
    755755      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
    756756        OK ? «pi1 … f, ?») (OK ? f) tab;
Note: See TracChangeset for help on using the changeset viewer.