Changeset 961 for src/Clight/Cexec.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (9 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/Clight/Cexec.ma (modified) (11 diffs)

src/Clight/Cexec.ma

@@ -48 +48 @@
 definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
   λv,ty. match v in val with
-  [ Vint i ⇒ match ty with
-    [ Tint _ _ ⇒ OK ? (¬eq i zero)
+  [ Vint sz i ⇒ match ty with
+    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
+                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
     | _ ⇒ Error ? (msg TypeMismatch)
     ]
@@ -69 +70 @@
 lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
 #v #ty #r #H elim H; #v #t #H' elim H';
-  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
+  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
   | #r #b #pc #i #i0 #s %{ true} % //
   | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
-  | #i #s %{ false} % //;
+  | * #sg %{ false} % //
   | #r #r' #t %{ false} % //;
   | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
@@ -106 +107 @@
 axiom BadCast : String. (* TODO: refine into more precise errors? *)
 
-definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
-λm:mem. λi:int. λty:type. λty':type.
-match eq i zero with
+definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
+λm:mem. λsz. λi. λty:type. λty':type.
+match eq_bv ? i (zero ?) with
 [ true ⇒
   match ty with
-  [ Tint _ _ ⇒
-    match ty' with
-    [ Tpointer r _ ⇒ OK ? (Vnull r)
-    | Tarray r _ _ ⇒ OK ? (Vnull r)
-    | Tfunction _ _ ⇒ OK ? (Vnull Code)
-    | _ ⇒ Error ? (msg BadCast)
-    ]
+  [ Tint sz' _ ⇒
+    if eq_intsize sz sz' then
+      match ty' with
+      [ Tpointer r _ ⇒ OK ? (Vnull r)
+      | Tarray r _ _ ⇒ OK ? (Vnull r)
+      | Tfunction _ _ ⇒ OK ? (Vnull Code)
+      | _ ⇒ Error ? (msg BadCast)
+      ]
+    else Error ? (msg TypeMismatch)
   | _ ⇒ Error ? (msg BadCast)
   ]
@@ -126 +129 @@
 λm:mem. λv:val. λty:type. λty':type.
 match v with
-[ Vint i ⇒
+[ Vint sz i ⇒
   match ty with
   [ Tint sz1 si1 ⇒
-    match ty' with
-    [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
-    | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
-    | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
-    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
-    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
-    | _ ⇒ Error ? (msg BadCast)
-    ]
-  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
-  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
-  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
+    intsize_eq_elim ? sz sz1 ? i
+    (λi.
+      match ty' with
+      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 sz2 si2 i))
+      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
+      | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
+      | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
+      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
+      | _ ⇒ Error ? (msg BadCast)
+      ])
+    (Error ? (msg BadCast))
+  | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
+  | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
+  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
   | _ ⇒ Error ? (msg TypeMismatch)
   ]
@@ -146 +152 @@
   [ Tfloat sz ⇒
     match ty' with
-    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
+    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
     | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
     | _ ⇒ Error ? (msg BadCast)
@@ -189 +195 @@
 [ Expr e' ty ⇒
   match e' with
-  [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
+  [ Econst_int sz i ⇒
+      match ty with
+      [ Tint sz' _ ⇒
+          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
+          else Error ? (msg BadlyTypedTerm)
+      | _ ⇒ Error ? (msg BadlyTypedTerm)
+      ]
   | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
   | Evar _ ⇒
@@ -215 +227 @@
       | _ ⇒ Error ? (msg BadlyTypedTerm)
       ]
-  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
+  | Esizeof ty' ⇒
+      match ty with
+      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
+      | _ ⇒ Error ? (msg BadlyTypedTerm)
+      ]
   | Eunop op a ⇒
       do 〈v1,tr〉 ← exec_expr ge en m a;
@@ -275 +291 @@
           do 〈lofs,tr〉 ← exec_lvalue ge en m a;
           do delta ← field_offset i fList;
-          OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
+          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
       | Tunion id fList ⇒
           do 〈lofs,tr〉 ← exec_lvalue ge en m a;
@@ -478 +494 @@
   | Sswitch a sl ⇒ 
       ! 〈v,tr〉 ← exec_expr ge e m a;
-      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
+      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
                    | _ ⇒ Wrong ??? (msg TypeMismatch)]
   | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
@@ -530 +546 @@
   [ Kstop ⇒
     match res with
-    [ Vint r ⇒ Some ? r
+    [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
     | _ ⇒ None ?
     ]
@@ -544 +560 @@
 | #v #k #m cases k; 
   [ cases v;
-    [ 2: #i %1 ; %{ i} //;
+    [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
+              | %1 ; %{ i} //;
+              ]
     | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;