Changeset 1872 for src/common/Values.ma

Timestamp:

Apr 4, 2012, 6:48:23 PM (9 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/common/Values.ma (modified) (2 diffs)

src/common/Values.ma

@@ -470 +470 @@
        should we be able to extract bytes? *)
 
-let rec load_result (chunk: memory_chunk) (v: val) ≝
+let rec load_result (chunk: typ) (v: val) ≝
   match v with
   [ Vint sz n ⇒
     match chunk with
-    [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
-    | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
-    | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
-    | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
-    | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
+    [ ASTint sz' sg ⇒ if eq_intsize sz sz' then v else Vundef
     | _ ⇒ Vundef
     ]
   | Vptr ptr ⇒
     match chunk with
-    [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
+    [ ASTptr r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
     | _ ⇒ Vundef
     ]
   | Vnull r ⇒
     match chunk with
-    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
+    [ ASTptr r' ⇒ if eq_region r r' then Vnull r else Vundef
     | _ ⇒ Vundef
     ]
   | Vfloat f ⇒
     match chunk with
-    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
-    | Mfloat64 ⇒ Vfloat f
+    [ ASTfloat sz ⇒ match sz with [ F32 ⇒ Vfloat(singleoffloat f) | F64 ⇒ Vfloat f ]
     | _ ⇒ Vundef
     ]
@@ -1085 +1080 @@
   Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
 #chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
-[ 8: #r ] whd in ⊢ (?%?); //;
+[ #sz #sg | #r | #sz ] whd in ⊢ (?%?); //;
 qed.