Changeset 961 for src

Timestamp:

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

Author:

campbell

Message:

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

Location:

src

Files:

• ASM/Arithmetic.ma (modified) (1 diff)
• ASM/BitVector.ma (modified) (1 diff)
• ASM/Vector.ma (modified) (1 diff)
• Clight/Cexec.ma (modified) (11 diffs)
• Clight/CexecComplete.ma (modified) (10 diffs)
• Clight/CexecEquiv.ma (modified) (4 diffs)
• Clight/CexecSound.ma (modified) (14 diffs)
• Clight/Csem.ma (modified) (35 diffs)
• Clight/Csyntax.ma (modified) (5 diffs)
• Clight/casts.ma (modified) (5 diffs)
• Clight/label.ma (modified) (2 diffs)
• Clight/test/memorymodel.ma (modified) (4 diffs)
• Clight/test/search.ma (modified) (9 diffs)
• Clight/test/sum.ma (modified) (3 diffs)
• Clight/toCminor.ma (modified) (17 diffs)
• Cminor/initialisation.ma (modified) (3 diffs)
• Cminor/semantics.ma (modified) (3 diffs)
• Cminor/syntax.ma (modified) (1 diff)
• Cminor/toRTLabs.ma (modified) (1 diff)
• RTLabs/semantics.ma (modified) (2 diffs)
• common/AST.ma (modified) (3 diffs)
• common/Animation.ma (modified) (1 diff)
• common/Events.ma (modified) (2 diffs)
• common/Floats.ma (modified) (1 diff)
• common/FrontEndOps.ma (modified) (21 diffs)
• common/Globalenvs.ma (modified) (2 diffs)
• common/IO.ma (modified) (3 diffs)
• common/Integers.ma (modified) (1 diff)
• common/Values.ma (modified) (24 diffs)
• utilities/extranat.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -344 +344 @@
   λb, c: BitVector n.
     full_add n b c false.
+
+definition sign_bit : ∀n. BitVector n → bool ≝
+λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
+
+definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
+λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
+
+definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
+λm,n.
+  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
+  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
+  | nat_eq n' ⇒ λv. v
+  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
+  ].
+
+definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
+λm,n.
+  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
+  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
+  | nat_eq n' ⇒ λv. v
+  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
+  ].
+

src/ASM/BitVector.ma

@@ -110 +110 @@
 #Q * *; normalize /3/
 qed.
+
+lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
+@eq_v_true * @refl
+qed.
+
+lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
+#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
+qed.
     
 axiom bitvector_of_string:

src/ASM/Vector.ma

@@ -477 +477 @@
 ] qed.
 
+lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
+#A #f #f_true #n #v elim v
+[ //
+| #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
+] qed.
+
+lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
+#A #n #h #t #t' * #NE % #E @NE >E @refl
+qed.
+
+lemma  eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
+#A #f #f_true #n elim n
+[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
+| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
+  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
+] qed.
+
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 (* Subvectors.                                                                *)

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;

src/Clight/CexecComplete.ma

@@ -100 +100 @@
 #m #v #ty #ty' #v' #H
 elim H;
-[ #m #i #sz1 #sz2 #sg1 #sg2 @refl
+[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
 | #m #f #sz #szi #sg @refl
-| #m #i #sz #sz' #sg @refl
+| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
 | #m #f #sz #sz' @refl
 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
@@ -111 +111 @@
     #pc' whd in ⊢ (??%?) 
     @(dec_true ? (pointer_compat_dec b sp2) pc') //
-| #m #sz #si #ty'' #r #H cases H; //;
+| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
+  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
 | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
     whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
@@ -131 +132 @@
 lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
 #v #ty #r #H elim H; #v #t #H' elim H';
-  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
+  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
+    >(eq_bv_false … ne) //
   | #r #b #pc #i #i0 #s %{ true} % //
   | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
-  | #i #s %{ false} % //;
+  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
   | #r #r' #t %{ false} % //;
   | #s %{ false} % //; whd; >(Feq_zero_true …) //;
@@ -142 +144 @@
 lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
 #v #ty #H elim H;
-  [ #i #is #s #ne whd; >(eq_false … ne) //;
+  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
   | #p #b #i #i0 #s //
   | #f #s #ne whd; >(Feq_zero_false … ne) //;
@@ -150 +152 @@
 lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
 #v #ty #H elim H;
-  [ #i #s //;
+  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
   | #r #r' #t //;
   | #s whd; >(Feq_zero_true …) //;
@@ -163 +165 @@
   (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
   (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
-[ #i #ty @refl
+[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
 | #f #ty @refl
 | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
@@ -179 +181 @@
     @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
     @refl
-| #ty' #ty @refl
+| #ty' #sz #sg @refl
 | #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     >(yields_eq ??? H3)
@@ -342 +344 @@
 lemma eventval_match_complete': ∀ev,ty,v.
   eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
-#ev #ty #v #H elim H; //; qed.
+#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
 
 lemma eventval_list_match_complete: ∀vs,tys,evs.
@@ -431 +433 @@
     | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
     ]
-| #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
+| #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     @refl
@@ -446 +448 @@
     #H1 #H2
     >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
-    whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
+    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     @refl
 | #v #f #env #k #m @refl

src/Clight/CexecEquiv.ma

@@ -158 +158 @@
 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
 exec_from ge s (se_interact o k i (se_stop tr r m)) →
-step ge s tr (Returnstate (Vint r) Kstop m).
+step ge s tr (Returnstate (Vint I32 r) Kstop m).
 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
 [ #tr #r #m #E1 #E2 destruct
@@ -278 +278 @@
 lemma final_step: ∀ge,tr,r,m,s.
   exec_from ge s (se_stop tr r m) →
-  step ge s tr (Returnstate (Vint r) Kstop m).
+  step ge s tr (Returnstate (Vint I32 r) Kstop m).
 #ge #tr #r #m #s #EXEC
 whd in EXEC;
@@ -302 +302 @@
 lemma e_stop_inv: ∀ge,x,tr,r,m.
   exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m →
-  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
+  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉.
 #ge #x #tr #r #m
 >(exec_inf_aux_unfold …) cases x;
@@ -317 +317 @@
   execution_terminates tr s (se_step E0 s e) r m →
   exec_from ge s e →
-  star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
+  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
 #ge #tr0 #s0 #r #m #e0 #H inversion H;
 [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC

src/Clight/CexecSound.ma

@@ -8 +8 @@
  exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
 #v #ty #r
-cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
-cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
-#H whd in H:(??%?);
-[ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ %
-  [ #E1 #E2 destruct @bool_of_val_false @is_false_int
-  | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2 | destruct @refl ]
-  ]
-| 8: cases (eq_dec f Fzero)
+cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
+cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
+whd in ⊢ (??%? → ?)
+[ 2: @intsize_eq_elim_elim
+  [ #NE #H destruct
+  | *; whd @eq_bv_elim
+    [ #E1 #E2 destruct @bool_of_val_false @is_false_int
+    | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E1 | destruct @refl ]
+    ]
+  ]
+| 8: #H cases (eq_dec f Fzero)
   [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
   | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ] 
   ]
-| 14: >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
-| 15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
-| *: destruct
+| 14: #H >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
+| 15: #H >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
+| *: #H destruct
 ] qed.
 
@@ -35 +38 @@
 qed.
 
-lemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
-#m #i #ty #ty' #v'
-whd in ⊢ (??%? → ?);
-lapply (eq_spec i zero); cases (eq i zero);
+lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
+#m #sz #i #ty #ty' #v'
+whd in ⊢ (??%? → ?)
+@eq_bv_elim
 [ #e >e
-    cases ty; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
-    whd in ⊢ (??%? → ?); #H destruct; 
-    cases ty' in H ⊢ %; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
-    whd in ⊢ (??%? → ?); #H destruct (H); @cast_ip_z //;
+    cases ty; [ | #sz' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
+    whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ] 
+    cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
+    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
 | #_ whd in ⊢ (??%? → ?); #H destruct
 ]
@@ -52 +55 @@
 cases v;
 [ #H whd in H:(??%?); destruct;
-| #i cases ty;
+| #sz #i cases ty;
   [ #H whd in H:(??%?); destruct;
   | 3: #a #H whd in H:(??%?); destruct;
   | 7,8,9: #a #b #H whd in H:(??%?); destruct;
   | #sz1 #si1 cases ty';
-    [ #H whd in H:(??%?); destruct;
-    | 3: #a #H whd in H:(??%?); destruct; //
-    | 2,7,8,9: #a #b #H whd in H:(??%?); destruct; //
+    [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+      [ #NE #H destruct
+      | *; whd #H whd in H:(??%?); destruct;
+      ]
+    | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+      [ #E #H whd in H:(??%?); destruct
+      | *; whd #H whd in H:(??%?); destruct; @cast_if
+      ]
+    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+      [ 1,3,5,7: #NE #H destruct
+      | *: *; whd #H whd in H:(??%?); destruct; //
+      ]
     | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
                  | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
                  | #args #rty letin t ≝ (Tfunction args rty) ]
-        whd in ⊢ (??%? → ?);
-        lapply (try_cast_null_sound m i (Tint sz1 si1) t v');
-        cases (try_cast_null m i (Tint sz1 si1) t);
-        [ 1,3,5: #v'' #H' #e @H' @e
-        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
+        whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+        [ 1,3,5: #NE #H destruct
+        | *: *; whd
+          lapply (try_cast_null_sound m sz i (Tint sz si1) t v');
+          cases (try_cast_null m sz i (Tint sz si1) t);
+          [ 1,3,5: #v'' #H' #e @H' @e
+          | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
+          ]
         ]
     ]
@@ -74 +89 @@
            | #args #rty letin t ≝ (Tfunction args rty) ]
         whd in ⊢ (??%? → ?);
-        lapply (try_cast_null_sound m i t ty' v');
-        cases (try_cast_null m i t ty');
+        lapply (try_cast_null_sound m sz i t ty' v');
+        cases (try_cast_null m sz i t ty');
         [ 1,3,5: #v'' #H' #e @H' @e
         | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
@@ -113 +128 @@
   (P:expr → Prop)
   (Q:expr_descr → type → Prop)
-  (ci:∀ty,i.P (Expr (Econst_int i) ty))
+  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
   (cf:∀ty,f.P (Expr (Econst_float f) ty))
   (lv:∀e,ty. Q e ty → Plvalue P e ty)
@@ -133 +148 @@
 [ Expr e' ty ⇒
   match e' with
-  [ Econst_int i ⇒ ci ty i
+  [ Econst_int sz i ⇒ ci sz ty i
   | Econst_float f ⇒ cf ty f
   | Evar v ⇒ lv (Evar v) ty (vr v ty)
@@ -152 +167 @@
   (P:expr → Prop)
   (Q:expr_descr → type → Prop)
-  (ci:∀ty,i.P (Expr (Econst_int i) ty))
+  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
   (cf:∀ty,f.P (Expr (Econst_float f) ty))
   (lv:∀e,ty. Q e ty → Plvalue P e ty)
@@ -181 +196 @@
 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
 (* XXX // fails [ 1,2: #ty #c whd //  *)
-[ #ty #c whd % 
+[ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
+  @eq_intsize_elim #E try @I <E whd % 
 | #ty #c whd %2
 (* expressions that are lvalues *)
@@ -248 +264 @@
         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     ]
-| #ty #ty' whd; (* XXX //*) @eval_Esizeof
+| #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof
 | #ty #e' #ty' #i cases ty'; //;
     [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
@@ -261 +277 @@
 (* exec_lvalue fails on non-lvalues. *)
 | #e' #ty cases e';
-    [ 1,2,5,12: #a #H | 3,4: #a * | 13,14: #a #b * | 6,8,10,11: #a #b #H | 7,9: #a #b #c #H ]
+    [ 2,5,12: #a #H | 3,4: #a * | 13,14: #a #b * | 1,6,8,10,11: #a #b #H | 7,9: #a #b #c #H ]
     @I
 ] qed.
@@ -269 +285 @@
 eval_lvalue ge en m e loc off tr.
 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
-[ 1,2,5: #a #b #H @False_ind destruct (H);
+[ 1,2,5: #a #b #c #H @False_ind destruct (H);
 | #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
     @(eval_lvalue_inv_ind … H1)
@@ -369 +385 @@
   [ //
   | #ty #tys whd in ⊢ (???%)
-    cases ty cases v // #v' #sz try #sg
-    @bind_OK #evs #CHECK
-    @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECK)) //
+    cases ty [ #sz #sg | #sz | #r ] cases v //
+    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
+      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct 
+    | #v ] @bind_OK #evs #CHECKevs
+      @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs))
+      //
   ]
 ] qed.
@@ -483 +502 @@
         whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
     ]
-  | #ex #ls @res_bindIO2_OK #v cases v; //; #n #tr #Hv
+  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
     @step_switch @(exec_expr_sound' … Hv)
   | #l #s' whd; @step_label (* XXX //; *)
@@ -542 +561 @@
 
 lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
-* [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct %
+* [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct %
                             | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
                             ]

src/Clight/Csem.ma

@@ -38 +38 @@
 inductive is_false: val → type → Prop ≝
   | is_false_int: ∀sz,sg.
-      is_false (Vint zero) (Tint sz sg)
+      is_false (Vint sz (zero ?)) (Tint sz sg)
   | is_false_pointer: ∀r,r',t.
       is_false (Vnull r) (Tpointer r' t)
@@ -45 +45 @@
 
 inductive is_true: val → type → Prop ≝
-  | is_true_int_int: ∀n,sz,sg.
-      n ≠ zero →
-      is_true (Vint n) (Tint sz sg)
+  | is_true_int_int: ∀sz,sg,n.
+      n ≠ (zero ?) →
+      is_true (Vint sz n) (Tint sz sg)
   | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
       is_true (Vptr r b pc ofs) (Tpointer s t)
@@ -72 +72 @@
 let rec sem_neg (v: val) (ty: type) : option val ≝
   match ty with
-  [ Tint _ _ ⇒
+  [ Tint sz _ ⇒
       match v with
-      [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n))
+      [ Vint sz' n ⇒ if eq_intsize sz sz'
+                     then Some ? (Vint ? (two_complement_negation ? n))
+                     else None ?
       | _ ⇒ None ?
       ]
@@ -87 +89 @@
 let rec sem_notint (v: val) : option val ≝
   match v with
-  [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *)
+  [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *)
   | _ ⇒ None ?
   ].
@@ -93 +95 @@
 let rec sem_notbool (v: val) (ty: type) : option val ≝
   match ty with
-  [ Tint _ _ ⇒
+  [ Tint sz _ ⇒
       match v with
-      [ Vint n ⇒ Some ? (of_bool (eq n zero))
+      [ Vint sz' n ⇒ if eq_intsize sz sz'
+                     then Some ? (of_bool (eq_bv ? n (zero ?)))
+                     else None ?
       | _ ⇒ None ?
       ]
@@ -116 +120 @@
   [ add_case_ii ⇒                       (**r integer addition *)
       match v1 with 
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2))
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                        (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -129 +134 @@
       match v1 with
       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
-        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
+        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2))
         | _ ⇒ None ? ]
       | Vnull r ⇒ match v2 with
-        [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
+        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
   | add_case_ip ty ⇒                    (**r integer plus pointer *)
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1)))
-        | Vnull r ⇒ if eq n1 zero then Some ? (Vnull r) else None ?
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1))
+        | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -149 +154 @@
   [ sub_case_ii ⇒                (**r integer subtraction *)
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2))
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 
+                        (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -162 +168 @@
       match v1 with
       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
-        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
+        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2))
         | _ ⇒ None ? ]
       | Vnull r ⇒ match v2 with
-        [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
+        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -173 +179 @@
         [ Vptr r2 b2 p2 ofs2 ⇒
           if eq_block b1 b2 then
-            if eq (repr (sizeof ty)) zero then None ?
-            else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
+            if eqb (sizeof ty) 0 then None ?
+            else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with
                  [ None ⇒ None ?
-                 | Some v ⇒ Some ? (Vint v)
+                 | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
                  ]
           else None ?
         | _ ⇒ None ? ]
-      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
+      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
       | _ ⇒ None ? ]
   | sub_default ⇒ None ?
@@ -189 +195 @@
   [ mul_case_ii ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-          [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
-(*        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*)
+      [ Vint sz1 n1 ⇒ match v2 with
+          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                          (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -208 +214 @@
   [ div_case_I32unsi ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                        (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
   | div_case_ii ⇒
       match v1 with
-       [ Vint n1 ⇒ match v2 with
-         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
+       [ Vint sz1 n1 ⇒ match v2 with
+         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
          | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -232 +240 @@
   [ mod_case_I32unsi ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
   | mod_case_ii ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                        (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -248 +258 @@
 let rec sem_and (v1,v2: val) : option val ≝
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ?
@@ -256 +267 @@
 let rec sem_or (v1,v2: val) : option val ≝
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ?
@@ -264 +276 @@
 let rec sem_xor (v1,v2: val) : option val ≝
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ?
@@ -272 +285 @@
 let rec sem_shl (v1,v2: val): option val ≝
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒
-        if ltu n2 iwordsize then Some ? (Vint(shl n1 n2)) else None ?
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒
+        if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+        then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
+        else None ?
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -282 +297 @@
   [ shr_case_I32unsi ⇒
       match v1 with 
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒
-            if ltu n2 iwordsize then Some ? (Vint (shru n1 n2)) else None ?
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒
+            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
+            else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
    | shr_case_ii => 
       match v1 with 
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒
-            if ltu n2 iwordsize then Some ? (Vint (shr n1 n2)) else None ?
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒
+            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
+            else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -318 +337 @@
   [ cmp_case_I32unsi ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-        [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
+      [ Vint sz1 n1 ⇒ match v2 with
+        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
   | cmp_case_ii ⇒
       match v1 with
-      [ Vint n1 ⇒ match v2 with
-         [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
+      [ Vint sz1 n1 ⇒ match v2 with
+         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                         (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
          | _ ⇒ None ?
          ]
@@ -396 +417 @@
   resulting in value [v2].  *)
 
-let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝
-  match sz with
-  [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ]
-  | I16 ⇒ match sg with [ Signed => sign_ext 16 i | Unsigned ⇒ zero_ext 16 i ]
-  | I32 ⇒ i
-  ].
-
-let rec cast_int_float (si : signedness) (i: int) : float ≝
+let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
+  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
+
+let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝
   match si with
-  [ Signed ⇒ floatofint i
-  | Unsigned ⇒ floatofintu i
-  ].
-
-let rec cast_float_int (si : signedness) (f: float) : int ≝
+  [ Signed ⇒ floatofint ? i
+  | Unsigned ⇒ floatofintu ? i
+  ].
+
+let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz) ≝
   match si with
-  [ Signed ⇒ intoffloat f
-  | Unsigned ⇒ intuoffloat f
+  [ Signed ⇒ intoffloat ? f
+  | Unsigned ⇒ intuoffloat ? f
   ].
 
@@ -428 +445 @@
 
 inductive cast : mem → val → type → type → val → Prop ≝
-  | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
-      cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 i))
+  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
+      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
+           (Vint sz2 (cast_int_int ? sz2 si2 i))
   | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
       cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
-  | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
-      cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
-          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+           (Vint sz2 (cast_float_int sz2 si2 f))
+  | cast_if:   ∀m,sz1,sz2,si1,i.                (**r int to float  *)
+      cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2)
+          (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
   | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
       cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
@@ -447 +464 @@
   | cast_ip_z: ∀m,sz,sg,ty',r.
       type_region ty' r →
-      cast m (Vint zero) (Tint sz sg) ty' (Vnull r)
+      cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
   | cast_pp_z: ∀m,ty,ty',r,r'.
       type_region ty r →
@@ -546 +563 @@
 (* * Selection of the appropriate case of a [switch], given the value [n]
   of the selector expression. *)
-
-let rec select_switch (n: int) (sl: labeled_statements)
+(* FIXME: now that we have several sizes of integer, it isn't clear whether we
+   should allow case labels to be of a different size to the switch expression. *)
+let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
                        on sl : labeled_statements ≝
   match sl with
   [ LSdefault _ ⇒ sl
-  | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl'
+  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
+                         (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl')
   ].
 
@@ -559 +578 @@
   match sl with
   [ LSdefault s ⇒ s
-  | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
+  | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
   ].
 
@@ -579 +598 @@
 
 inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
-  | eval_Econst_int:   ∀i,ty.
-      eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
+  | eval_Econst_int:   ∀sz,sg,i.
+      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
   | eval_Econst_float:   ∀f,ty.
       eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
@@ -591 +610 @@
       ∀pc:pointer_compat loc r.
       eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
-  | eval_Esizeof: ∀ty',ty.
-      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
+  | eval_Esizeof: ∀ty',sz,sg.
+      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
   | eval_Eunop:  ∀op,a,ty,v1,v,tr.
       eval_expr ge e m a v1 tr →
@@ -663 +682 @@
       typeof a = Tstruct id fList →
       field_offset i fList = OK ? delta →
-      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr
+      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
  | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
       eval_lvalue ge e m a l ofs tr →
@@ -671 +690 @@
 let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
   (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
-  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
+  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
   (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
   (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
-  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
+  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
   (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
   (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
@@ -688 +707 @@
   (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
   match ev with
-  [ eval_Econst_int i ty ⇒ eci i ty
+  [ eval_Econst_int sz sg i ⇒ eci sz sg i
   | eval_Econst_float f ty ⇒ ecF f ty
   | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
   | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
-  | eval_Esizeof ty' ty ⇒ esz ty' ty
+  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
   | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
   | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2)
@@ -779 +798 @@
   (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
   (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
-  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
+  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
   (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
-  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
+  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
   (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
   (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
@@ -802 +821 @@
   (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
   match ev with
-  [ eval_Econst_int i ty ⇒ eci i ty
+  [ eval_Econst_int sz sg i ⇒ eci sz sg i
   | eval_Econst_float f ty ⇒ ecF f ty
   | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
   | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
-  | eval_Esizeof ty' ty ⇒ esz ty' ty
+  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
   | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
   | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2)
@@ -821 +840 @@
   (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
   (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
-  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
+  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
   (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
-  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
+  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
   (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
   (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
@@ -983 +1002 @@
   match sl with
   [ LSdefault s => find_label lbl s k
-  | LScase _ s sl' =>
+  | LScase _ _ s sl' =>
       match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
       [ Some sk => Some ? sk
@@ -1135 +1154 @@
            E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
 
-  | step_switch: ∀f,a,sl,k,e,m,n,tr.
-      eval_expr ge e m a (Vint n) tr →
+  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
+      eval_expr ge e m a (Vint sz n) tr →
       step ge (State f (Sswitch a sl) k e m)
-           tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
+           tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m)
   | step_skip_break_switch: ∀f,x,k,e,m.
       x = Sskip ∨ x = Sbreak →
@@ -1503 +1522 @@
 inductive final_state: state -> int -> Prop :=
   | final_state_intro: ∀r,m.
-      final_state (Returnstate (Vint r) Kstop m) r.
+      final_state (Returnstate (Vint I32 r) Kstop m) r.
 
 (* * Execution of a whole program: [exec_program p beh]

src/Clight/Csyntax.ma

@@ -156 +156 @@
 
 with expr_descr : Type[0] ≝
-  | Econst_int: int → expr_descr       (**r integer literal *)
+  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
   | Econst_float: float → expr_descr   (**r float literal *)
   | Evar: ident → expr_descr           (**r variable *)
@@ -207 +207 @@
 with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
   | LSdefault: statement → labeled_statements
-  | LScase: int → statement → labeled_statements → labeled_statements.
+  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
 
 let rec statement_ind2
@@ -227 +227 @@
   (Scs:∀l,s. P s → P (Scost l s))
   (LSd:∀s. P s → Q (LSdefault s))
-  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
+  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
   (s:statement) on s : P s ≝
 match s with
@@ -276 +276 @@
   (Scs:∀l,s. P s → P (Scost l s))
   (LSd:∀s. P s → Q (LSdefault s))
-  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
+  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
   (ls:labeled_statements) on ls : Q ls ≝
 match ls with
 [ LSdefault s ⇒ LSd s
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| LScase i s t ⇒ LSc i s t
+| LScase sz i s t ⇒ LSc sz i s t
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
@@ -288 +288 @@
 definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
   statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
-  (λ_,_. I) (λ_,_,_,_,_.I).
+  (λ_,_. I) (λ_,_,_,_,_,_.I).
 
 (* * ** Functions *)

src/Clight/casts.ma

@@ -1 @@
-include "common/Integers.ma".
+include "common/Values.ma".
 
 definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
@@ -5 +5 @@
 
 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
-#A #n #x elim x //
+#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
 qed.
 
@@ -82 +82 @@
 lemma truncate_tail : ∀m,n,v.
   truncate (S m) n v = truncate m n (tail … v).
-  //
+#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
   qed.
 
@@ -118 +118 @@
 qed.
 
-definition sign_bit : ∀n. BitVector n → bool ≝
-λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
-
 definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
 λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
-
+ 
 lemma truncate_sign : ∀m,n,x.
   truncate m n (sign … x) = x.
@@ -178 +175 @@
 #m #n #x @(vector_inv_n … x) #h #t elim n
 [ @refl
-| #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl
+| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
 ] qed.
 

src/Clight/label.ma

@@ -54 +54 @@
     do 〈e2,costgen〉 ← label_expr e2 costgen; 
     do 〈e2,costgen〉 ← add_cost_expr e2 costgen; 
-    do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int zero) (Tint I32 Signed)) costgen;
+    do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen;
     OK ? 〈Econdition e1 e2 ef, costgen〉
 | Eorbool e1 e2 ⇒
     do 〈e1,costgen〉 ← label_expr e1 costgen; 
-    do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int one) (Tint I32 Signed)) costgen;
+    do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen;
     do 〈e2,costgen〉 ← label_expr e2 costgen; 
     do 〈e2,costgen〉 ← add_cost_expr e2 costgen; 
@@ -165 +165 @@
     do 〈s,costgen〉 ← add_cost_before s costgen;
     OK ? 〈LSdefault s, costgen〉
-| LScase i s ls' ⇒
+| LScase sz i s ls' ⇒
     do 〈s,costgen〉 ← label_statement s costgen;
     do 〈s,costgen〉 ← add_cost_before s costgen;
     do 〈ls',costgen〉 ← label_lstatements ls' costgen;
-    OK ? 〈LScase i s ls', costgen〉
+    OK ? 〈LScase sz i s ls', costgen〉
 ].
 

src/Clight/test/memorymodel.ma

@@ -27 +27 @@
 (* write a value *)
 definition store2 : mem.
-  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
+  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
 
   lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
@@ -34 +34 @@
 (* overwrite the first byte of the value *)
 definition store3 : mem.
-  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
+  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
 
   lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
@@ -42 +42 @@
 example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
 
-(* The read is successful and returns a signed version of the value. *)
-example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
+(* The read is successful and returns the value. *)
+example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
 
 (* NB: Double frees are allowed by the memory model (although not necessarily
@@ -63 +63 @@
 definition storeIIblk := alloc storeA 0 4 Any.
 definition storeIII : mem.
- letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
+ letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
   lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
   | #rr #_ @rr ] qed.

src/Clight/test/search.ma

@@ -8 +8 @@
        (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
          (Expr (Ecast (Tint I8 Unsigned )
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tint I8 Unsigned )))
        (Ssequence
@@ -17 +17 @@
                (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
                (Tint I32 Signed  ))
-             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
              (Tint I32 Signed  ))) (Tint I8 Unsigned )))
        (Ssequence
@@ -39 +39 @@
                    (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
                    (Tint I32 Signed  ))) (Tint I32 Signed  ))
-               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
+               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
          (Ssequence
@@ -80 +80 @@
                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
                    (Tint I32 Signed  ))
-                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
            Sskip)
@@ -103 +103 @@
                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
                    (Tint I32 Signed  ))
-                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
            Sskip)))))
        Sskip)
        (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
-                             (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
+                             (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
                                                  (Tint I32 Signed  )))
                                (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
@@ -122 +122 @@
                    (Expr (Evar (ident_of_nat 4))
                      (Tarray Any (Tint I8 Unsigned ) 5))
-                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
-                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
-        (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
-          (Tint I8 Unsigned )))
-      (Ssequence
-      (Sassign (Expr (Ederef
-                 (Expr (Ebinop Oadd
-                   (Expr (Evar (ident_of_nat 4))
-                     (Tarray Any (Tint I8 Unsigned ) 5))
-                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
-                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
-        (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
-          (Tint I8 Unsigned )))
-      (Ssequence
-      (Sassign (Expr (Ederef
-                 (Expr (Ebinop Oadd
-                   (Expr (Evar (ident_of_nat 4))
-                     (Tarray Any (Tint I8 Unsigned ) 5))
-                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
-                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
-        (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
-          (Tint I8 Unsigned )))
-      (Ssequence
-      (Sassign (Expr (Ederef
-                 (Expr (Ebinop Oadd
-                   (Expr (Evar (ident_of_nat 4))
-                     (Tarray Any (Tint I8 Unsigned ) 5))
-                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
-                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
-        (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
-          (Tint I8 Unsigned )))
-      (Ssequence
-      (Sassign (Expr (Ederef
-                 (Expr (Ebinop Oadd
-                   (Expr (Evar (ident_of_nat 4))
-                     (Tarray Any (Tint I8 Unsigned ) 5))
-                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
-                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
-        (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
+                   (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
+                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
+        (Expr (Ecast (Tint I8 Unsigned )
+          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
+          (Tint I8 Unsigned )))
+      (Ssequence
+      (Sassign (Expr (Ederef
+                 (Expr (Ebinop Oadd
+                   (Expr (Evar (ident_of_nat 4))
+                     (Tarray Any (Tint I8 Unsigned ) 5))
+                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
+                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
+        (Expr (Ecast (Tint I8 Unsigned )
+          (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
+          (Tint I8 Unsigned )))
+      (Ssequence
+      (Sassign (Expr (Ederef
+                 (Expr (Ebinop Oadd
+                   (Expr (Evar (ident_of_nat 4))
+                     (Tarray Any (Tint I8 Unsigned ) 5))
+                   (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
+                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
+        (Expr (Ecast (Tint I8 Unsigned )
+          (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
+          (Tint I8 Unsigned )))
+      (Ssequence
+      (Sassign (Expr (Ederef
+                 (Expr (Ebinop Oadd
+                   (Expr (Evar (ident_of_nat 4))
+                     (Tarray Any (Tint I8 Unsigned ) 5))
+                   (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
+                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
+        (Expr (Ecast (Tint I8 Unsigned )
+          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
+          (Tint I8 Unsigned )))
+      (Ssequence
+      (Sassign (Expr (Ederef
+                 (Expr (Ebinop Oadd
+                   (Expr (Evar (ident_of_nat 4))
+                     (Tarray Any (Tint I8 Unsigned ) 5))
+                   (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
+                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
+        (Expr (Ecast (Tint I8 Unsigned )
+          (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
           (Tint I8 Unsigned )))
       (Ssequence
@@ -173 +173 @@
         [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
         (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
+          (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
           (Tint I8 Unsigned ));
         (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
+          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
           (Tint I8 Unsigned ))])
       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
@@ -189 +189 @@
 .
 
-example exec: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
+example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
 normalize  (* you can examine the result here *)
 @refl
@@ -197 +197 @@
 include "Cminor/semantics.ma".
 
-example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
+example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
 normalize
 @refl

src/Clight/test/sum.ma

@@ -8 +8 @@
        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
          (Expr (Ecast (Tint I8 Unsigned )
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tint I8 Unsigned )))
        (Ssequence
        (Ssequence
        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
-               (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
          (Expr (Ebinop Olt
            (Expr (Ecast (Tint I32 Unsigned)
@@ -23 +23 @@
            (Expr (Ebinop Oadd
              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
-             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
              (Tint I32 Signed  )))
          (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
@@ -51 +51 @@
   (ident_of_nat 0)
   [〈〈〈ident_of_nat 3 (* src *),
-     [(Init_int8 (repr 28)) ; (Init_int8 (repr 17)) ; (Init_int8 (repr 17)) ;
-     (Init_int8 (repr 8)) ; (Init_int8 (repr 4)) ]〉, Any〉,
+     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
+     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
      (Tarray Any (Tint I8 Unsigned ) 5)〉]
 .
 
-example exec: finishes_with (repr 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
+example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
 normalize  (* you can examine the result here *)
 @refl

src/Clight/toCminor.ma

@@ -141 +141 @@
 match ls with
 [ LSdefault s1 ⇒ gather_mem_vars_stmt s1
-| LScase _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
-                    gather_mem_vars_ls ls1
+| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
+                      gather_mem_vars_ls ls1
 ].
 
@@ -217 +217 @@
 [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
 | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
-| add_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
-| add_case_ip ty ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst (repr (sizeof ty))))))
+(* XXX using the integer size for e2 as the offset's size isn't right, because
+   if e2 produces an 8bit value then the true offset might overflow *)
+| add_case_pi ty ⇒
+    match ty2' with
+    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
+    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
+    ]
+| add_case_ip ty ⇒
+    match ty1' with
+    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
+    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
+    ]
 | add_default ⇒ Error ? (msg TypeMismatch)
 ].
@@ -229 +239 @@
 [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
 | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
-| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
-| sub_case_pp ty ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' Osubpp e1 e2) (Cst ? (Ointconst (repr (sizeof ty)))))
+(* XXX choosing offset sizes? *)
+| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
+| sub_case_pp ty ⇒ 
+    match ty' with (* XXX overflow *)
+    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
+    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
+    ]
 | sub_default ⇒ Error ? (msg TypeMismatch)
 ].
@@ -249 +264 @@
 let ty2' ≝ typ_of_type ty2 in
 match classify_div ty1 ty2 with
-[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) (* FIXME: should be 8 bit only *)
+[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
 | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
 | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
@@ -260 +275 @@
 let ty2' ≝ typ_of_type ty2 in
 match classify_mod ty1 ty2 with
-[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) (* FIXME: should be 8 bit only *)
+[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
 | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
 | mod_default ⇒ Error ? (msg TypeMismatch)
@@ -270 +285 @@
 let ty2' ≝ typ_of_type ty2 in
 match classify_shr ty1 ty2 with
-[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) (* FIXME: should be 8 bit only *)
+[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
 | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
 | shr_default ⇒ Error ? (msg TypeMismatch)
@@ -331 +346 @@
 [ Tint sz1 sg1 ⇒ λe.
     match ty2 return λx.res (CMexpr (typ_of_type x)) with
-    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
+    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sz2 sg2) e)
     | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
     | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
@@ -339 +354 @@
 | Tfloat sz1 ⇒ λe.
     match ty2 return λx.res (CMexpr (typ_of_type x)) with
-    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
+    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
     | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
     | _ ⇒ Error ? (msg TypeMismatch)
@@ -345 +360 @@
 | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
     match ty2 return λx.res (CMexpr (typ_of_type x)) with
-    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Ointofptr e)
+    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
@@ -352 +367 @@
 | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
     match ty2 return λx.res (CMexpr (typ_of_type x)) with
-    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) Ointofptr e)
+    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
@@ -393 +408 @@
 [ Expr ed ty ⇒
   match ed with
-  [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
+  [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
   | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
   | Evar id ⇒
@@ -400 +415 @@
       [ Global r ⇒
           match access_mode ty with
-          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id zero)))
-          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
+          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
+          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
           ]
       | Stack n ⇒
           match access_mode ty with
-          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack (repr n))))
-          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
+          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
+          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
           ]
@@ -457 +472 @@
       do e1' ← translate_expr vars e1;
       do e2' ← translate_expr vars e2;
-      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
-      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
-      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
-      | _ ⇒ λ_.Error ? (msg TypeMismatch)
-      ] e1'
+      match ty with
+      [ Tint sz _ ⇒
+        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
+        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
+        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
+        | _ ⇒ λ_.Error ? (msg TypeMismatch)
+        ] e1'
+      | _ ⇒ Error ? (msg TypeMismatch)
+      ]
   | Eorbool e1 e2 ⇒
       do e1' ← translate_expr vars e1;
       do e2' ← translate_expr vars e2;
-      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
-      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
-      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
-      | _ ⇒ λ_.Error ? (msg TypeMismatch)
-      ] e1'
-  | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
+      match ty with
+      [ Tint sz _ ⇒
+        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
+        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
+        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
+        | _ ⇒ λ_.Error ? (msg TypeMismatch)
+        ] e1'
+      | _ ⇒ Error ? (msg TypeMismatch)
+      ]
+  | Esizeof ty1 ⇒
+      match ty with
+      [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
+      | _ ⇒ Error ? (msg TypeMismatch)
+      ]
   | Efield e1 id ⇒
       do e' ← match typeof e1 with
@@ -479 +506 @@
             do off ← field_offset id fl;
             match access_mode ty with
-            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
-            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
+            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
+            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
             | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
             ]
@@ -509 +536 @@
       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
       match c return λ_. res (Σr.CMexpr (ASTptr r)) with
-      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id zero)))
-      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack (repr n))))
+      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
+      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
       | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
       ]
@@ -525 +552 @@
           do off ← field_offset id fl;
           match e1' with
-          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst (repr off)))))
+          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
           ]
       | Tunion _ _ ⇒ translate_addr vars e1
@@ -554 +581 @@
             match c with
             [ Local ⇒ OK ? (IdDest id)
-            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id zero)))
-            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack (repr n))))
+            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
+            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
             ]
         | _ ⇒

src/Cminor/initialisation.ma

@@ -9 +9 @@
 λinit.
 match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
-[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
-| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
-| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
+[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
+| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
+| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
 | Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
 | Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
 | Init_space n         ⇒ None ?
-| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
+| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
 | Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
 ].
@@ -22 +22 @@
    away. *)
 
-definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
+definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
 λid,r,init,off.
 match init_expr init with
@@ -37 +37 @@
   (λdatum,os.
    let 〈off,s〉 ≝ os in
-     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
-  〈zero, St_skip〉 init).
+     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
+  〈0, St_skip〉 init).
 
 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝

src/Cminor/semantics.ma

@@ -91 +91 @@
 ].
 
-let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
+let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
 match cs with
 [ nil ⇒ default
 | cons h t ⇒
     let 〈hi,a〉 ≝ h in
-    if eq i hi then a else find_case A i t default
+    if eq_bv ? i hi then a else find_case A sz i t default
 ].
 
@@ -199 +199 @@
         ! k' ← k_exit n k;
         ret ? 〈E0, State f St_skip en m sp k'〉
-    | St_switch _ _ e cs default ⇒
+    | St_switch sz _ e cs default ⇒
         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
         match v with
-        [ Vint i ⇒
-            ! k' ← k_exit (find_case ? i cs default) k;
-            ret ? 〈tr, State f St_skip en m sp k'〉
+        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
+            ! k' ← k_exit (find_case ?? i cs default) k;
+            ret ? 〈tr, State f St_skip en m sp k'〉)
+            (Wrong ??? (msg BadSwitchValue))
         | _ ⇒ Wrong ??? (msg BadSwitchValue)
         ]
@@ -257 +258 @@
         | Some v ⇒
             match v with
-            [ Vint i ⇒ Some ? i
+            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
             | _ ⇒ None ?
             ]

src/Cminor/syntax.ma

@@ -27 +27 @@
 | St_exit : nat → stmt
 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
-| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
+| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
 | St_return : option (Σt. expr t) → stmt
 | St_label : ident → stmt → stmt

src/Cminor/toRTLabs.ma

@@ -210 +210 @@
       do f ← add_fresh_to_graph (St_cond br l_case) f;
       do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
-      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
+      add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;
     add_expr env ? e r f
 | St_return opt_e ⇒

src/RTLabs/semantics.ma

@@ -148 +148 @@
       ! v ← reg_retrieve (locals f) r;
       match v with
-      [ Vint i ⇒
+      [ Vint _ i ⇒
           ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
           ret ? 〈E0, build_state f fs m l〉
@@ -193 +193 @@
 | Callstate _ _ _ _ _ ⇒ None ?
 | Returnstate v _ fs _ ⇒
-    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
+    match fs with [ nil ⇒
+      match v with [ Some v' ⇒
+        match v' with
+        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
+        | _ ⇒ None ? ]
+      | None ⇒ None ? ]
+    | cons _ _ ⇒ None ? ]
 ].
 

src/common/AST.ma

@@ -20 +20 @@
 include "common/Integers.ma".
 include "common/Floats.ma".
-include "ASM/BitVector.ma".
+include "ASM/Arithmetic.ma".
 include "common/Identifiers.ma".
 
@@ -110 +110 @@
 definition SigType_Ptr ≝ ASTptr Any.
 
+(* Define these carefully so that we always know that the result is nonzero,
+   and can be used in dependent types of the form (S n).
+   (At the time of writing this is only used for bitsize_of_intsize.) *)
+
 definition size_intsize : intsize → nat ≝
-λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
+λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
+
+definition bitsize_of_intsize : intsize → nat ≝
+λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
+
+definition eq_intsize : intsize → intsize → bool ≝
+λsz1,sz2.
+  match sz1 with
+  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
+  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
+  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
+  ].
+
+lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
+  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
+* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
+qed.
+
+lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
+* @refl
+qed.
+
+lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
+* * * #NE try @refl @False_ind @NE @refl
+qed.
+
+(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
+   if it is returns [e1] where the type of [n] has its dependency on [sz1]
+   changed to [sz2], and if not returns [e2]. *)
+let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
+  P sz1 → (P sz2 → A) → A → A ≝
+match sz1 return λsz. P sz → (P sz2 → A) → A → A with
+[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
+| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
+| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
+].
+
+lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
+  intsize_eq_elim A sz sz P p f d = f p.
+#A * //
+qed.
+
+lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
+  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
+#A * * #P #p #f #d #Q #Hne #Heq
+[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
+| *: whd in ⊢ (?%) @Hne % #E destruct
+] qed.
+
+
+(* A type for the integers that appear in the semantics. *)
+definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
+
+definition repr : ∀sz:intsize. nat → bvint sz ≝
+λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
+
 
 definition size_floatsize : floatsize → nat ≝
-λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
+λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
 
 definition typesize : typ → nat ≝ λty.
@@ -187 +246 @@
 
 inductive init_data: Type[0] ≝ 
-  | Init_int8: int → init_data
-  | Init_int16: int → init_data
-  | Init_int32: int → init_data
+  | Init_int8: bvint I8 → init_data
+  | Init_int16: bvint I16 → init_data
+  | Init_int32: bvint I32 → init_data
   | Init_float32: float → init_data
   | Init_float64: float → init_data
   | Init_space: nat → init_data 
   | Init_null: region → init_data
-  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
+  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
 
 (* * Whole programs consist of:

src/common/Animation.ma

@@ -10 +10 @@
 λo,ev.
 match io_in_typ o return λt. res (eventval_type t) with
-[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
+[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
 | ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
 | ASTptr _ ⇒ Error ? (msg IllTypedEvent)

src/common/Events.ma

@@ -37 +37 @@
   world. *)
 
-inductive eventval: Type[0] :=
-  | EVint: int -> eventval
-  | EVfloat: float -> eventval.
+inductive eventval: Type[0] ≝
+  | EVint: ∀sz. bvint sz → eventval
+  | EVfloat: float → eventval.
 
 inductive event : Type[0] ≝
@@ -193 +193 @@
 inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_int:
-      ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
+      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
   | ev_match_float:
       ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).

src/common/Floats.ma

@@ -34 +34 @@
 axiom Fabs: float → float.
 axiom singleoffloat: float → float.
-axiom intoffloat: float → int.
-axiom intuoffloat: float → int.
-axiom floatofint: int → float.
-axiom floatofintu: int → float.
+axiom intoffloat: ∀n. float → BitVector n.
+axiom intuoffloat: ∀n. float → BitVector n.
+axiom floatofint: ∀n. BitVector n → float.
+axiom floatofintu: ∀n. BitVector n → float.
 
 axiom Fadd: float → float → float.

src/common/FrontEndOps.ma

@@ -21 +21 @@
 
 inductive constant : Type[0] ≝
-  | Ointconst: int → constant     (**r integer constant *)
-  | Ofloatconst: float → constant (**r floating-point constant *)
-  | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
-  | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)
+  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
+  | Ofloatconst: float → constant          (**r floating-point constant *)
+  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
+  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
 
 inductive unary_operation : Type[0] ≝
-  | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
-  | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
-  | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
-  | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
+  | Ocastint: intsize → signedness → unary_operation (**r 8-bit zero extension  *)
   | Onegint: unary_operation               (**r integer opposite *)
   | Onotbool: unary_operation              (**r boolean negation  *)
@@ -37 +34 @@
   | Oabsf: unary_operation                 (**r float absolute value *)
   | Osingleoffloat: unary_operation        (**r float truncation *)
-  | Ointoffloat: unary_operation           (**r signed integer to float *)
-  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
+  | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
+  | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
   | Ofloatofint: unary_operation           (**r float to signed integer *)
   | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
   | Oid: unary_operation                   (**r identity (used to move between registers *)
   | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
-  | Ointofptr: unary_operation.            (**r pointer to int *)
+  | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
 
 inductive binary_operation : Type[0] ≝
@@ -68 +65 @@
   | Oaddp: binary_operation                (**r add an integer to a pointer *)
   | Osubpi: binary_operation               (**r subtract int from a pointers *)
-  | Osubpp: binary_operation               (**r subtract two pointers *)
+  | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
   | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
 
@@ -80 +77 @@
 λfind_symbol,sp,cst.
   match cst with
-  [ Ointconst n ⇒ Some ? (Vint n)
+  [ Ointconst sz n ⇒ Some ? (Vint sz n)
   | Ofloatconst n ⇒ Some ? (Vfloat n)
   | Oaddrsymbol s ofs ⇒
       match find_symbol s with
       [ None ⇒ None ?
-      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
+      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
       ]
   | Oaddrstack ofs ⇒
-      Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
+      Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
   ]. cases sp // qed.
 
@@ -94 +91 @@
 λop,arg.
   match op with
-  [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
-  | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
-  | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
-  | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
-  | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
-  | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
+  [ Ocastint sz sg ⇒
+      match sg with
+      [ Unsigned ⇒ Some ? (zero_ext sz arg)
+      |   Signed ⇒ Some ? (sign_ext sz arg)
+      ]
+  | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
+  | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
                               | Vptr _ _ _ _ ⇒ Some ? Vfalse
                               | Vnull _ ⇒ Some ? Vtrue
                               | _ ⇒ None ?
                               ]
-  | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
+  | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
   | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
   | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
   | Osingleoffloat ⇒ Some ? (singleoffloat arg)
-  | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
-  | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
-  | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
-  | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
+  | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
+  | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
+  | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
+  | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
   | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
   (* Only conversion of null pointers is specified. *)
-  | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
-  | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
+  | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
+  | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
   ].
 
@@ -122 +120 @@
 λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
 
-(* Individual operations, adapted from Values. *)
-
-definition ev_neg : val → option val ≝ λv.
-  match v with
-  [ Vint n ⇒ Some ? (Vint (neg n))
-  | _ ⇒ None ?
-  ].
-
-definition ev_negf : val → option val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
-  | _ ⇒ None ?
-  ].
-
-definition ev_absf : val → option val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
-  | _ ⇒ None ?
-  ].
-
-definition ev_intoffloat : val → option val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
-  | _ ⇒ None ?
-  ].
-
-definition ev_intuoffloat : val → option val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
-  | _ ⇒ None ?
-  ].
-
-definition ev_floatofint : val → option val ≝ λv.
-  match v with
-  [ Vint n ⇒ Some ? (Vfloat (floatofint n))
-  | _ ⇒ None ?
-  ].
-
-definition ev_floatofintu : val → option val ≝ λv.
-  match v with
-  [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
-  | _ ⇒ None ?
-  ].
-
-definition ev_notint : val → option val ≝ λv.
-  match v with
-  [ Vint n ⇒ Some ? (Vint (xor n mone))
-  | _ ⇒ None ?
-  ].
-  
-definition ev_notbool : val → option val ≝ λv.
-  match v with
-  [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
-  | Vptr _ b _ ofs ⇒ Some ? Vfalse
-  | Vnull _ ⇒ Some ? Vtrue
-  | _ ⇒ None ?
-  ].
-
-definition ev_zero_ext ≝ λnbits: nat. λv: val.
-  match v with
-  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
-  | _ ⇒ None ?
-  ].
-
-definition ev_sign_ext ≝ λnbits:nat. λv:val.
-  match v with
-  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
-  | _ ⇒ None ?
-  ].
-
-definition ev_singleoffloat : val → option val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
-  | _ ⇒ None ?
-  ].
+(* Individual operations, adapted from Values.  These differ in that they
+   implement the plain Cminor/RTLabs operations (e.g., with separate addition
+   for ints,floats and pointers) and use option rather than Vundef.  The ones
+   in Value are probably not needed. *)
 
 definition ev_add ≝ λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -207 +136 @@
 definition ev_sub ≝ λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -216 +147 @@
   match v1 with
   [ Vptr r b1 p ofs1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
+    [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
     | _ ⇒ None ? ]
   | Vnull r ⇒ match v2 with
-    [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
+    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
     | _ ⇒ None ?
     ]
@@ -227 +158 @@
   match v1 with
   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
-    | _ ⇒ None ? ]
-  | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
-  | _ ⇒ None ? ].
-
-definition ev_subpp ≝ λv1,v2: val.
+    [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
+    | _ ⇒ None ? ]
+  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
+  | _ ⇒ None ? ].
+
+definition ev_subpp ≝ λsz. λv1,v2: val.
   match v1 with
   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     [ Vptr r2 b2 p2 ofs2 ⇒
-        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
-    | _ ⇒ None ? ]
-  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
+        if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
+    | _ ⇒ None ? ]
+  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
   | _ ⇒ None ? ].
 
 definition ev_mul ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -250 +183 @@
 definition ev_divs ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -257 +192 @@
 definition ev_mods ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
+                    (None ?)
     | _ ⇒ None ?
     ]
@@ -266 +203 @@
 definition ev_divu ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
+                    (None ?)
     | _ ⇒ None ?
     ]
@@ -275 +214 @@
 definition ev_modu ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
+                    (None ?)
     | _ ⇒ None ?
     ]
@@ -284 +225 @@
 definition ev_and ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -291 +234 @@
 definition ev_or ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -298 +243 @@
 definition ev_xor ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -305 +252 @@
 definition ev_shl ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (shl n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with 
+    [ Vint sz2 n2 ⇒
+       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
        else None ?
     | _ ⇒ None ? ]
@@ -315 +262 @@
 definition ev_shr ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (shr n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with 
+    [ Vint sz2 n2 ⇒
+       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
        else None ?
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
 
-definition ev_shr_carry ≝ λv1, v2: val.
-  match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (shr_carry n1 n2))
-       else None ?
-    | _ ⇒ None ? ]
-  | _ ⇒ None ? ].
-
-definition ev_shrx ≝ λv1, v2: val.
-  match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (shrx n1 n2))
-       else None ?
-    | _ ⇒ None ? ]
-  | _ ⇒ None ? ].
-
 definition ev_shru ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (shru n1 n2))
-       else None ?
-    | _ ⇒ None ? ]
-  | _ ⇒ None ? ].
-
-definition ev_rolm ≝
-λv: val. λamount, mask: int.
-  match v with
-  [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
-  | _ ⇒ None ?
-  ].
-
-definition ev_ror ≝ λv1, v2: val.
-  match v1 with
-  [ Vint n1 ⇒ match v2 with 
-    [ Vint n2 ⇒
-       if ltu n2 iwordsize
-       then Some ? (Vint (ror n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with 
+    [ Vint sz2 n2 ⇒
+       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
+       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
        else None ?
     | _ ⇒ None ? ]
@@ -414 +324 @@
 definition ev_cmp ≝ λc: comparison. λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -438 +350 @@
 definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
+                    (None ?)
     | _ ⇒ None ? ]
   | _ ⇒ None ? ].
@@ -475 +389 @@
   | Oaddp ⇒ ev_addp
   | Osubpi ⇒ ev_subpi
-  | Osubpp ⇒ ev_subpp
+  | Osubpp sz ⇒ ev_subpp sz
   | Ocmpp c ⇒ ev_cmpp c
   ].

src/common/Globalenvs.ma

@@ -406 +406 @@
   let r ≝ block_region m b in
   match id with
-  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
-  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
-  | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
+  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
+  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
+  | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
   | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
   | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
@@ -416 +416 @@
       | Some b' ⇒ 
         match pointer_compat_dec b' r' with
-        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
+        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
         | inr _ ⇒ None ?
         ]

src/common/IO.ma

@@ -6 +6 @@
 
 definition eventval_type : ∀ty:typ. Type[0] ≝
-λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
+λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
 
 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
-λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
+λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
 *; qed.
 
 definition mk_val: ∀ty:typ. eventval_type ty → val ≝
-λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
+λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
 *; qed.
 
@@ -25 +25 @@
 λev,ty.
 match ty with
-[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
+[ ASTint sz _ ⇒ match ev with
+  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
+  | _ ⇒ Error ? (msg IllTypedEvent)]
 | ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
 | _ ⇒ Error ? (msg IllTypedEvent)
@@ -33 +35 @@
 λv,ty.
 match ty with
-[ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
+[ ASTint sz _ ⇒ match v with
+  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
+  | _ ⇒ Error ? (msg IllTypedEvent) ]
 | ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
 | _ ⇒ Error ? (msg IllTypedEvent)

src/common/Integers.ma

@@ -436 +436 @@
 #x #y change with (eq_bv ??? = eq_bv ???)
  @eq_bv_elim @eq_bv_elim /2/
-[ #NE #E @False_ind >E in NE * /2/
-| #E #NE @False_ind >E in NE * /2/
-] qed.
+#E >E * #NE @False_ind @NE @refl 
+qed.
 
 theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).

src/common/Values.ma

@@ -19 +19 @@
 include "utilities/Coqlib.ma".
 include "common/AST.ma".
-include "common/Integers.ma".
 include "common/Floats.ma".
 include "common/Errors.ma".
@@ -27 +26 @@
 include "basics/logic.ma".
 
-include "utilities/binary/Z.ma".
 include "utilities/extralib.ma".
 
@@ -94 +92 @@
 
 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
-definition shift_offset : offset → int → offset ≝
-  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
-definition neg_shift_offset : offset → int → offset ≝
-  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
-definition sub_offset : offset → offset → int ≝
-  λx,y. bitvector_of_Z ? (offv x - offv y).
+definition shift_offset : ∀n. offset → BitVector n → offset ≝
+  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
+(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
+definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
+  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
+definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
+  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
+definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
+  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
+definition sub_offset : ∀n. offset → offset → BitVector n ≝
+  λn,x,y. bitvector_of_Z ? (offv x - offv y).
 definition zero_offset ≝ mk_offset OZ.
 definition lt_offset : offset → offset → bool ≝
@@ -117 +120 @@
 inductive val: Type[0] ≝
   | Vundef: val
-  | Vint: int → val
+  | Vint: ∀sz:intsize. bvint sz → val
   | Vfloat: float → val
   | Vnull: region → val
   | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
 
-definition Vzero: val ≝ Vint zero.
-definition Vone: val ≝ Vint one.
-definition Vmone: val ≝ Vint mone.
-
-definition Vtrue: val ≝ Vint one.
-definition Vfalse: val ≝ Vint zero.
+definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
+definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1).
+definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one).
+definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?).
+
+(* XXX 32bit booleans are Clight specific. *)
+definition Vtrue: val ≝ Vone I32.
+definition Vfalse: val ≝ Vzero I32.
 
 (* Values split into bytes.  Ideally we'd use some kind of sizeof for the
@@ -140 +145 @@
 λv. match v with
 [ Vundef ⇒ True
-| Vint _ ⇒ True
+| Vint _ _ ⇒ True
 | Vfloat _ ⇒ False
 | Vnull r ⇒ ptr_may_be_single r = true
@@ -148 +153 @@
 definition may_be_split : val → Prop ≝
 λv.match v with
-[ Vint _ ⇒ False
+[ Vint _ _ ⇒ False
 | Vnull r ⇒ ptr_may_be_single r = false
 | Vptr r _ _ _ ⇒ ptr_may_be_single r = false
@@ -248 +253 @@
 definition is_true : val → Prop ≝ λv.
   match v with
-  [ Vint n ⇒ n ≠ zero
+  [ Vint _ n ⇒ n ≠ (zero ?)
   | Vptr _ b _ ofs ⇒ True
   | _ ⇒ False
@@ -255 +260 @@
 definition is_false : val → Prop ≝ λv.
   match v with
-  [ Vint n ⇒ n = zero
+  [ Vint _ n ⇒ n = (zero ?)
   | Vnull _ ⇒ True
   | _ ⇒ False
@@ -262 +267 @@
 inductive bool_of_val: val → bool → Prop ≝
   | bool_of_val_int_true:
-      ∀n. n ≠ zero → bool_of_val (Vint n) true
+      ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true
   | bool_of_val_int_false:
-      bool_of_val (Vint zero) false
+      ∀sz. bool_of_val (Vzero sz) false
   | bool_of_val_ptr:
       ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
@@ -274 +279 @@
 definition eval_bool_of_val : val → res bool ≝
 λv. match v with
-[ Vint i ⇒ OK ? (notb (eq i zero))
+[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
 | Vnull _ ⇒ OK ? false
 | Vptr _ _ _ _ ⇒ OK ? true
@@ -282 +287 @@
 definition neg : val → val ≝ λv.
   match v with
-  [ Vint n ⇒ Vint (neg n)
+  [ Vint sz n ⇒ Vint sz (two_complement_negation ? n)
   | _ ⇒ Vundef
   ].
@@ -298 +303 @@
   ].
 
-definition intoffloat : val → val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Vint (intoffloat f)
+definition intoffloat : intsize → val → val ≝ λsz,v.
+  match v with
+  [ Vfloat f ⇒ Vint sz (intoffloat ? f)
   | _ ⇒ Vundef
   ].
 
-definition intuoffloat : val → val ≝ λv.
-  match v with
-  [ Vfloat f ⇒ Vint (intuoffloat f)
+definition intuoffloat : intsize → val → val ≝ λsz,v.
+  match v with
+  [ Vfloat f ⇒ Vint sz (intuoffloat ? f)
   | _ ⇒ Vundef
   ].
@@ -312 +317 @@
 definition floatofint : val → val ≝ λv.
   match v with
-  [ Vint n ⇒ Vfloat (floatofint n)
+  [ Vint sz n ⇒ Vfloat (floatofint ? n)
   | _ ⇒ Vundef
   ].
@@ -318 +323 @@
 definition floatofintu : val → val ≝ λv.
   match v with
-  [ Vint n ⇒ Vfloat (floatofintu n)
+  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
   | _ ⇒ Vundef
   ].
@@ -324 +329 @@
 definition notint : val → val ≝ λv.
   match v with
-  [ Vint n ⇒ Vint (xor n mone)
+  [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?))
   | _ ⇒ Vundef
   ].
   
-(* FIXME: switch to alias, or rename, or … *)
-definition int_eq : int → int → bool ≝ eq.
 definition notbool : val → val ≝ λv.
   match v with
-  [ Vint n ⇒ of_bool (int_eq n zero)
+  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
   | Vptr _ b _ ofs ⇒ Vfalse
   | Vnull _ ⇒ Vtrue
@@ -338 +341 @@
   ].
 
-definition zero_ext ≝ λnbits: nat. λv: val.
-  match v with
-  [ Vint n ⇒ Vint (zero_ext nbits n)
+definition zero_ext ≝ λrsz: intsize. λv: val.
+  match v with
+  [ Vint sz n ⇒ Vint rsz (zero_ext … n)
   | _ ⇒ Vundef
   ].
 
-definition sign_ext ≝ λnbits:nat. λv:val.
-  match v with
-  [ Vint i ⇒ Vint (sign_ext nbits i)
+definition sign_ext ≝ λrsz:intsize. λv:val.
+  match v with
+  [ Vint sz i ⇒ Vint rsz (sign_ext … i)
   | _ ⇒ Vundef
   ].
@@ -359 +362 @@
 definition add ≝ λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
-    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint sz2 (addition_n ? n1 n2))
+                    Vundef
+    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
     | _ ⇒ Vundef ]
   | Vptr r b1 p ofs1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
-    | _ ⇒ Vundef ]
-  | _ ⇒ Vundef ].
+    [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
+    | _ ⇒ Vundef ]
+  | _ ⇒ Vundef ].
+
+(* XXX Is I32 the best answer for ptr subtraction? *)
 
 definition sub ≝ λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint sz2 (subtraction ? n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
+    [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
     | Vptr r2 b2 p2 ofs2 ⇒
-        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
-    | _ ⇒ Vundef ]
-  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
+        if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
+    | _ ⇒ Vundef ]
+  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
   | _ ⇒ Vundef ].
 
 definition mul ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (mul n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
+                    Vundef
     | _ ⇒ Vundef ]
   | _ ⇒ Vundef ].
@@ -418 +429 @@
 definition v_and ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (i_and n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint ? (conjunction_bv ? n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | _ ⇒ Vundef ].
@@ -425 +438 @@
 definition or ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (or n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | _ ⇒ Vundef ].
@@ -432 +447 @@
 definition xor ≝ λv1, v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Vint (xor n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | _ ⇒ Vundef ].
@@ -550 +567 @@
   ].
 
+definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
+λn,c,x,y.
+  match c with
+  [ Ceq ⇒ eq_bv ? x y
+  | Cne ⇒ notb (eq_bv ? x y)
+  | Clt ⇒ lt_s ? x y
+  | Cle ⇒ notb (lt_s ? y x)
+  | Cgt ⇒ lt_s ? y x
+  | Cge ⇒ notb (lt_s ? x y)
+  ].
+
+definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
+λn,c,x,y.
+  match c with
+  [ Ceq ⇒ eq_bv ? x y
+  | Cne ⇒ notb (eq_bv ? x y)
+  | Clt ⇒ lt_u ? x y
+  | Cle ⇒ notb (lt_u ? y x)
+  | Cgt ⇒ lt_u ? y x
+  | Cge ⇒ notb (lt_u ? x y)
+  ].
+
 definition cmp ≝ λc: comparison. λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. of_bool (cmp_int ? c n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
@@ -571 +612 @@
 definition cmpu ≝ λc: comparison. λv1,v2: val.
   match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
+  [ Vint sz1 n1 ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
+                    (λn1. of_bool (cmpu_int ? c n1 n2))
+                    Vundef
     | _ ⇒ Vundef ]
   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
@@ -588 +631 @@
   | _ ⇒ Vundef ].
 
-definition cmpf ≝ λc: comparison. λv1,v2: val.
+definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
   match v1 with
   [ Vfloat f1 ⇒ match v2 with
@@ -603 +646 @@
   is performed and [0xFFFFFFFF] is returned.   Type mismatches
   (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
+(* XXX update comment *)
+(* XXX is this even necessary now?
+       should we be able to extract bytes? *)
 
 let rec load_result (chunk: memory_chunk) (v: val) ≝
   match v with
-  [ Vint n ⇒
+  [ Vint sz n ⇒
     match chunk with
-    [ Mint8signed ⇒ Vint (sign_ext 8 n)
-    | Mint8unsigned ⇒ Vint (zero_ext 8 n)
-    | Mint16signed ⇒ Vint (sign_ext 16 n)
-    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
-    | Mint32 ⇒ Vint n
+    [ 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 ]
     | _ ⇒ Vundef
     ]

src/utilities/extranat.ma

@@ -19 +19 @@
     ]
 ].
+
+lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
+#n elim n
+[ @refl
+| #m #IH whd in ⊢ (??%?) > IH @refl
+] qed.
+
+lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
+#n #m elim n
+[ //
+| #n' #IH whd in ⊢ (??%?) > IH @refl
+] qed.
+
+lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
+#n #m elim m
+[ //
+| #m' #IH whd in ⊢ (??%?) > IH @refl
+] qed.
 
 lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.