Changeset 1872 for src/Cminor/syntax.ma

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:

• src/Cminor/syntax.ma (modified) (5 diffs)

src/Cminor/syntax.ma

@@ -10 +10 @@
 | Cst : ∀t. constant → expr t
 | Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
-| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
-| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
+| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
+| Mem : ∀t,r. expr (ASTptr r) → expr t
 | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
 | Ecost : ∀t. costlabel → expr t → expr t.
@@ -22 +22 @@
 | Op1 _ _ _ e ⇒ expr_vars ? e P
 | Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
-| Mem _ _ _ e ⇒ expr_vars ? e P
+| Mem _ _ e ⇒ expr_vars ? e P
 | Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
 | Ecost _ _ e ⇒ expr_vars ? e P
@@ -40 +40 @@
 | St_skip : stmt
 | St_assign : ∀t. ident → expr t → stmt
-| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
+| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
 (* ident for returned value, expression to identify fn, args. *)
 | St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
@@ -82 +82 @@
 match s with
 [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
-| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
+| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
 | 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
 (*
@@ -115 +115 @@
 [ //
 | #t #id #e * /4/
-| #t #r #q #e1 #e2 * /4/
+| #t #r #e1 #e2 * /4/
 | * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 
 (*