Changeset 961


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

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

Location:
src
Files:
30 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r949 r961  
    344344  λb, c: BitVector n.
    345345    full_add n b c false.
     346
     347definition sign_bit : ∀n. BitVector n → bool ≝
     348λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
     349
     350definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
     351λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
     352
     353definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
     354λm,n.
     355  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
     356  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
     357  | nat_eq n' ⇒ λv. v
     358  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     359  ].
     360
     361definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
     362λm,n.
     363  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
     364  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
     365  | nat_eq n' ⇒ λv. v
     366  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     367  ].
     368
  • src/ASM/BitVector.ma

    r868 r961  
    110110#Q * *; normalize /3/
    111111qed.
     112
     113lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
     114@eq_v_true * @refl
     115qed.
     116
     117lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
     118#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
     119qed.
    112120   
    113121axiom bitvector_of_string:
  • src/ASM/Vector.ma

    r889 r961  
    477477] qed.
    478478
     479lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
     480#A #f #f_true #n #v elim v
     481[ //
     482| #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
     483] qed.
     484
     485lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
     486#A #n #h #t #t' * #NE % #E @NE >E @refl
     487qed.
     488
     489lemma  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.
     490#A #f #f_true #n elim n
     491[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
     492| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
     493  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
     494] qed.
     495
    479496(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    480497(* Subvectors.                                                                *)
  • src/Clight/Cexec.ma

    r891 r961  
    4848definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
    4949  λv,ty. match v in val with
    50   [ Vint i ⇒ match ty with
    51     [ Tint _ _ ⇒ OK ? (¬eq i zero)
     50  [ Vint sz i ⇒ match ty with
     51    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
     52                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
    5253    | _ ⇒ Error ? (msg TypeMismatch)
    5354    ]
     
    6970lemma 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.
    7071#v #ty #r #H elim H; #v #t #H' elim H';
    71   [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
     72  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
    7273  | #r #b #pc #i #i0 #s %{ true} % //
    7374  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    74   | #i #s %{ false} % //;
     75  | * #sg %{ false} % //
    7576  | #r #r' #t %{ false} % //;
    7677  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
     
    106107axiom BadCast : String. (* TODO: refine into more precise errors? *)
    107108
    108 definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
    109 λm:mem. λi:int. λty:type. λty':type.
    110 match eq i zero with
     109definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
     110λm:mem. λsz. λi. λty:type. λty':type.
     111match eq_bv ? i (zero ?) with
    111112[ true ⇒
    112113  match ty with
    113   [ Tint _ _ ⇒
    114     match ty' with
    115     [ Tpointer r _ ⇒ OK ? (Vnull r)
    116     | Tarray r _ _ ⇒ OK ? (Vnull r)
    117     | Tfunction _ _ ⇒ OK ? (Vnull Code)
    118     | _ ⇒ Error ? (msg BadCast)
    119     ]
     114  [ Tint sz' _ ⇒
     115    if eq_intsize sz sz' then
     116      match ty' with
     117      [ Tpointer r _ ⇒ OK ? (Vnull r)
     118      | Tarray r _ _ ⇒ OK ? (Vnull r)
     119      | Tfunction _ _ ⇒ OK ? (Vnull Code)
     120      | _ ⇒ Error ? (msg BadCast)
     121      ]
     122    else Error ? (msg TypeMismatch)
    120123  | _ ⇒ Error ? (msg BadCast)
    121124  ]
     
    126129λm:mem. λv:val. λty:type. λty':type.
    127130match v with
    128 [ Vint i ⇒
     131[ Vint sz i ⇒
    129132  match ty with
    130133  [ Tint sz1 si1 ⇒
    131     match ty' with
    132     [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
    133     | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
    134     | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    135     | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    136     | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    137     | _ ⇒ Error ? (msg BadCast)
    138     ]
    139   | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    140   | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    141   | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     134    intsize_eq_elim ? sz sz1 ? i
     135    (λi.
     136      match ty' with
     137      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 sz2 si2 i))
     138      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
     139      | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     140      | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     141      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     142      | _ ⇒ Error ? (msg BadCast)
     143      ])
     144    (Error ? (msg BadCast))
     145  | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     146  | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     147  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    142148  | _ ⇒ Error ? (msg TypeMismatch)
    143149  ]
     
    146152  [ Tfloat sz ⇒
    147153    match ty' with
    148     [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
     154    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
    149155    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
    150156    | _ ⇒ Error ? (msg BadCast)
     
    189195[ Expr e' ty ⇒
    190196  match e' with
    191   [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
     197  [ Econst_int sz i ⇒
     198      match ty with
     199      [ Tint sz' _ ⇒
     200          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
     201          else Error ? (msg BadlyTypedTerm)
     202      | _ ⇒ Error ? (msg BadlyTypedTerm)
     203      ]
    192204  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
    193205  | Evar _ ⇒
     
    215227      | _ ⇒ Error ? (msg BadlyTypedTerm)
    216228      ]
    217   | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
     229  | Esizeof ty' ⇒
     230      match ty with
     231      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
     232      | _ ⇒ Error ? (msg BadlyTypedTerm)
     233      ]
    218234  | Eunop op a ⇒
    219235      do 〈v1,tr〉 ← exec_expr ge en m a;
     
    275291          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    276292          do delta ← field_offset i fList;
    277           OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
     293          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
    278294      | Tunion id fList ⇒
    279295          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
     
    478494  | Sswitch a sl ⇒
    479495      ! 〈v,tr〉 ← exec_expr ge e m a;
    480       match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
     496      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    481497                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
    482498  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
     
    530546  [ Kstop ⇒
    531547    match res with
    532     [ Vint r ⇒ Some ? r
     548    [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
    533549    | _ ⇒ None ?
    534550    ]
     
    544560| #v #k #m cases k;
    545561  [ cases v;
    546     [ 2: #i %1 ; %{ i} //;
     562    [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
     563              | %1 ; %{ i} //;
     564              ]
    547565    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    548566    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
  • src/Clight/CexecComplete.ma

    r891 r961  
    100100#m #v #ty #ty' #v' #H
    101101elim H;
    102 [ #m #i #sz1 #sz2 #sg1 #sg2 @refl
     102[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
    103103| #m #f #sz #szi #sg @refl
    104 | #m #i #sz #sz' #sg @refl
     104| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106106| #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
     
    111111    #pc' whd in ⊢ (??%?)
    112112    @(dec_true ? (pointer_compat_dec b sp2) pc') //
    113 | #m #sz #si #ty'' #r #H cases H; //;
     113| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
     114  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
    114115| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    115116    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     
    131132lemma 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.
    132133#v #ty #r #H elim H; #v #t #H' elim H';
    133   [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
     134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
     135    >(eq_bv_false … ne) //
    134136  | #r #b #pc #i #i0 #s %{ true} % //
    135137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    136   | #i #s %{ false} % //;
     138  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
    137139  | #r #r' #t %{ false} % //;
    138140  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
     
    142144lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
    143145#v #ty #H elim H;
    144   [ #i #is #s #ne whd; >(eq_false … ne) //;
     146  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
    145147  | #p #b #i #i0 #s //
    146148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
     
    150152lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
    151153#v #ty #H elim H;
    152   [ #i #s //;
     154  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
    153155  | #r #r' #t //;
    154156  | #s whd; >(Feq_zero_true …) //;
     
    163165  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    164166  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    165 [ #i #ty @refl
     167[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
    166168| #f #ty @refl
    167169| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
     
    179181    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
    180182    @refl
    181 | #ty' #ty @refl
     183| #ty' #sz #sg @refl
    182184| #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
    183185    >(yields_eq ??? H3)
     
    342344lemma eventval_match_complete': ∀ev,ty,v.
    343345  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
    344 #ev #ty #v #H elim H; //; qed.
     346#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
    345347
    346348lemma eventval_list_match_complete: ∀vs,tys,evs.
     
    431433    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    432434    ]
    433 | #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
     435| #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
    434436    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    435437    @refl
     
    446448    #H1 #H2
    447449    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    448     whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     450    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
    449451    @refl
    450452| #v #f #env #k #m @refl
  • src/Clight/CexecEquiv.ma

    r891 r961  
    158158lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    159159exec_from ge s (se_interact o k i (se_stop tr r m)) →
    160 step ge s tr (Returnstate (Vint r) Kstop m).
     160step ge s tr (Returnstate (Vint I32 r) Kstop m).
    161161#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    162162[ #tr #r #m #E1 #E2 destruct
     
    278278lemma final_step: ∀ge,tr,r,m,s.
    279279  exec_from ge s (se_stop tr r m) →
    280   step ge s tr (Returnstate (Vint r) Kstop m).
     280  step ge s tr (Returnstate (Vint I32 r) Kstop m).
    281281#ge #tr #r #m #s #EXEC
    282282whd in EXEC;
     
    302302lemma e_stop_inv: ∀ge,x,tr,r,m.
    303303  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m →
    304   x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
     304  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉.
    305305#ge #x #tr #r #m
    306306>(exec_inf_aux_unfold …) cases x;
     
    317317  execution_terminates tr s (se_step E0 s e) r m →
    318318  exec_from ge s e →
    319   star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
     319  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    320320#ge #tr0 #s0 #r #m #e0 #H inversion H;
    321321[ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
  • src/Clight/CexecSound.ma

    r891 r961  
    88 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    99#v #ty #r
    10 cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    11 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 ]
    12 #H whd in H:(??%?);
    13 [ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ %
    14   [ #E1 #E2 destruct @bool_of_val_false @is_false_int
    15   | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2 | destruct @refl ]
    16   ]
    17 | 8: cases (eq_dec f Fzero)
     10cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
     11cases 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 ]
     12whd in ⊢ (??%? → ?)
     13[ 2: @intsize_eq_elim_elim
     14  [ #NE #H destruct
     15  | *; whd @eq_bv_elim
     16    [ #E1 #E2 destruct @bool_of_val_false @is_false_int
     17    | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E1 | destruct @refl ]
     18    ]
     19  ]
     20| 8: #H cases (eq_dec f Fzero)
    1821  [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    1922  | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ]
    2023  ]
    21 | 14: >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
    22 | 15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
    23 | *: destruct
     24| 14: #H >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
     25| 15: #H >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
     26| *: #H destruct
    2427] qed.
    2528
     
    3538qed.
    3639
    37 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'.
    38 #m #i #ty #ty' #v'
    39 whd in ⊢ (??%? → ?);
    40 lapply (eq_spec i zero); cases (eq i zero);
     40lemma 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'.
     41#m #sz #i #ty #ty' #v'
     42whd in ⊢ (??%? → ?)
     43@eq_bv_elim
    4144[ #e >e
    42     cases ty; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
    43     whd in ⊢ (??%? → ?); #H destruct;
    44     cases ty' in H ⊢ %; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
    45     whd in ⊢ (??%? → ?); #H destruct (H); @cast_ip_z //;
     45    cases ty; [ | #sz' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     46    whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ]
     47    cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     48    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
    4649| #_ whd in ⊢ (??%? → ?); #H destruct
    4750]
     
    5255cases v;
    5356[ #H whd in H:(??%?); destruct;
    54 | #i cases ty;
     57| #sz #i cases ty;
    5558  [ #H whd in H:(??%?); destruct;
    5659  | 3: #a #H whd in H:(??%?); destruct;
    5760  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
    5861  | #sz1 #si1 cases ty';
    59     [ #H whd in H:(??%?); destruct;
    60     | 3: #a #H whd in H:(??%?); destruct; //
    61     | 2,7,8,9: #a #b #H whd in H:(??%?); destruct; //
     62    [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     63      [ #NE #H destruct
     64      | *; whd #H whd in H:(??%?); destruct;
     65      ]
     66    | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     67      [ #E #H whd in H:(??%?); destruct
     68      | *; whd #H whd in H:(??%?); destruct; @cast_if
     69      ]
     70    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     71      [ 1,3,5,7: #NE #H destruct
     72      | *: *; whd #H whd in H:(??%?); destruct; //
     73      ]
    6274    | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
    6375                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    6476                 | #args #rty letin t ≝ (Tfunction args rty) ]
    65         whd in ⊢ (??%? → ?);
    66         lapply (try_cast_null_sound m i (Tint sz1 si1) t v');
    67         cases (try_cast_null m i (Tint sz1 si1) t);
    68         [ 1,3,5: #v'' #H' #e @H' @e
    69         | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
     77        whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     78        [ 1,3,5: #NE #H destruct
     79        | *: *; whd
     80          lapply (try_cast_null_sound m sz i (Tint sz si1) t v');
     81          cases (try_cast_null m sz i (Tint sz si1) t);
     82          [ 1,3,5: #v'' #H' #e @H' @e
     83          | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
     84          ]
    7085        ]
    7186    ]
     
    7489           | #args #rty letin t ≝ (Tfunction args rty) ]
    7590        whd in ⊢ (??%? → ?);
    76         lapply (try_cast_null_sound m i t ty' v');
    77         cases (try_cast_null m i t ty');
     91        lapply (try_cast_null_sound m sz i t ty' v');
     92        cases (try_cast_null m sz i t ty');
    7893        [ 1,3,5: #v'' #H' #e @H' @e
    7994        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
     
    113128  (P:expr → Prop)
    114129  (Q:expr_descr → type → Prop)
    115   (ci:∀ty,i.P (Expr (Econst_int i) ty))
     130  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    116131  (cf:∀ty,f.P (Expr (Econst_float f) ty))
    117132  (lv:∀e,ty. Q e ty → Plvalue P e ty)
     
    133148[ Expr e' ty ⇒
    134149  match e' with
    135   [ Econst_int i ⇒ ci ty i
     150  [ Econst_int sz i ⇒ ci sz ty i
    136151  | Econst_float f ⇒ cf ty f
    137152  | Evar v ⇒ lv (Evar v) ty (vr v ty)
     
    152167  (P:expr → Prop)
    153168  (Q:expr_descr → type → Prop)
    154   (ci:∀ty,i.P (Expr (Econst_int i) ty))
     169  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    155170  (cf:∀ty,f.P (Expr (Econst_float f) ty))
    156171  (lv:∀e,ty. Q e ty → Plvalue P e ty)
     
    181196#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)
    182197(* XXX // fails [ 1,2: #ty #c whd //  *)
    183 [ #ty #c whd %
     198[ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
     199  @eq_intsize_elim #E try @I <E whd %
    184200| #ty #c whd %2
    185201(* expressions that are lvalues *)
     
    248264        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
    249265    ]
    250 | #ty #ty' whd; (* XXX //*) @eval_Esizeof
     266| #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof
    251267| #ty #e' #ty' #i cases ty'; //;
    252268    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     
    261277(* exec_lvalue fails on non-lvalues. *)
    262278| #e' #ty cases e';
    263     [ 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 ]
     279    [ 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 ]
    264280    @I
    265281] qed.
     
    269285eval_lvalue ge en m e loc off tr.
    270286#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    271 [ 1,2,5: #a #b #H @False_ind destruct (H);
     287[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    272288| #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
    273289    @(eval_lvalue_inv_ind … H1)
     
    369385  [ //
    370386  | #ty #tys whd in ⊢ (???%)
    371     cases ty cases v // #v' #sz try #sg
    372     @bind_OK #evs #CHECK
    373     @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECK)) //
     387    cases ty [ #sz #sg | #sz | #r ] cases v //
     388    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
     389      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
     390    | #v ] @bind_OK #evs #CHECKevs
     391      @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs))
     392      //
    374393  ]
    375394] qed.
     
    483502        whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
    484503    ]
    485   | #ex #ls @res_bindIO2_OK #v cases v; //; #n #tr #Hv
     504  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
    486505    @step_switch @(exec_expr_sound' … Hv)
    487506  | #l #s' whd; @step_label (* XXX //; *)
     
    542561
    543562lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
    544 * [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct %
     563* [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct %
    545564                            | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
    546565                            ]
  • src/Clight/Csem.ma

    r816 r961  
    3838inductive is_false: val → type → Prop ≝
    3939  | is_false_int: ∀sz,sg.
    40       is_false (Vint zero) (Tint sz sg)
     40      is_false (Vint sz (zero ?)) (Tint sz sg)
    4141  | is_false_pointer: ∀r,r',t.
    4242      is_false (Vnull r) (Tpointer r' t)
     
    4545
    4646inductive is_true: val → type → Prop ≝
    47   | is_true_int_int: ∀n,sz,sg.
    48       n ≠ zero
    49       is_true (Vint n) (Tint sz sg)
     47  | is_true_int_int: ∀sz,sg,n.
     48      n ≠ (zero ?)
     49      is_true (Vint sz n) (Tint sz sg)
    5050  | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
    5151      is_true (Vptr r b pc ofs) (Tpointer s t)
     
    7272let rec sem_neg (v: val) (ty: type) : option val ≝
    7373  match ty with
    74   [ Tint _ _ ⇒
     74  [ Tint sz _ ⇒
    7575      match v with
    76       [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n))
     76      [ Vint sz' n ⇒ if eq_intsize sz sz'
     77                     then Some ? (Vint ? (two_complement_negation ? n))
     78                     else None ?
    7779      | _ ⇒ None ?
    7880      ]
     
    8789let rec sem_notint (v: val) : option val ≝
    8890  match v with
    89   [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *)
     91  [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *)
    9092  | _ ⇒ None ?
    9193  ].
     
    9395let rec sem_notbool (v: val) (ty: type) : option val ≝
    9496  match ty with
    95   [ Tint _ _ ⇒
     97  [ Tint sz _ ⇒
    9698      match v with
    97       [ Vint n ⇒ Some ? (of_bool (eq n zero))
     99      [ Vint sz' n ⇒ if eq_intsize sz sz'
     100                     then Some ? (of_bool (eq_bv ? n (zero ?)))
     101                     else None ?
    98102      | _ ⇒ None ?
    99103      ]
     
    116120  [ add_case_ii ⇒                       (**r integer addition *)
    117121      match v1 with
    118       [ Vint n1 ⇒ match v2 with
    119         [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2))
     122      [ Vint sz1 n1 ⇒ match v2 with
     123        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     124                        (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?)
    120125        | _ ⇒ None ? ]
    121126      | _ ⇒ None ? ]
     
    129134      match v1 with
    130135      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    131         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
     136        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2))
    132137        | _ ⇒ None ? ]
    133138      | Vnull r ⇒ match v2 with
    134         [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     139        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    135140        | _ ⇒ None ? ]
    136141      | _ ⇒ None ? ]
    137142  | add_case_ip ty ⇒                    (**r integer plus pointer *)
    138143      match v1 with
    139       [ Vint n1 ⇒ match v2 with
    140         [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1)))
    141         | Vnull r ⇒ if eq n1 zero then Some ? (Vnull r) else None ?
     144      [ Vint sz1 n1 ⇒ match v2 with
     145        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1))
     146        | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
    142147        | _ ⇒ None ? ]
    143148      | _ ⇒ None ? ]
     
    149154  [ sub_case_ii ⇒                (**r integer subtraction *)
    150155      match v1 with
    151       [ Vint n1 ⇒ match v2 with
    152         [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2))
     156      [ Vint sz1 n1 ⇒ match v2 with
     157        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     158                        (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?)
    153159        | _ ⇒ None ? ]
    154160      | _ ⇒ None ? ]
     
    162168      match v1 with
    163169      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    164         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
     170        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2))
    165171        | _ ⇒ None ? ]
    166172      | Vnull r ⇒ match v2 with
    167         [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     173        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    168174        | _ ⇒ None ? ]
    169175      | _ ⇒ None ? ]
     
    173179        [ Vptr r2 b2 p2 ofs2 ⇒
    174180          if eq_block b1 b2 then
    175             if eq (repr (sizeof ty)) zero then None ?
    176             else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
     181            if eqb (sizeof ty) 0 then None ?
     182            else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with
    177183                 [ None ⇒ None ?
    178                  | Some v ⇒ Some ? (Vint v)
     184                 | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
    179185                 ]
    180186          else None ?
    181187        | _ ⇒ None ? ]
    182       | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     188      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
    183189      | _ ⇒ None ? ]
    184190  | sub_default ⇒ None ?
     
    189195  [ mul_case_ii ⇒
    190196      match v1 with
    191       [ Vint n1 ⇒ match v2 with
    192           [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
    193 (*        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*)
     197      [ Vint sz1 n1 ⇒ match v2 with
     198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     199                          (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
    194200        | _ ⇒ None ? ]
    195201      | _ ⇒ None ? ]
     
    208214  [ div_case_I32unsi ⇒
    209215      match v1 with
    210       [ Vint n1 ⇒ match v2 with
    211         [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
     216      [ Vint sz1 n1 ⇒ match v2 with
     217        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     218                        (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
    212219        | _ ⇒ None ? ]
    213220      | _ ⇒ None ? ]
    214221  | div_case_ii ⇒
    215222      match v1 with
    216        [ Vint n1 ⇒ match v2 with
    217          [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
     223       [ Vint sz1 n1 ⇒ match v2 with
     224         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     225                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
    218226         | _ ⇒ None ? ]
    219227      | _ ⇒ None ? ]
     
    232240  [ mod_case_I32unsi ⇒
    233241      match v1 with
    234       [ Vint n1 ⇒ match v2 with
    235         [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
     242      [ Vint sz1 n1 ⇒ match v2 with
     243        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     244                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
    236245        | _ ⇒ None ? ]
    237246      | _ ⇒ None ? ]
    238247  | mod_case_ii ⇒
    239248      match v1 with
    240       [ Vint n1 ⇒ match v2 with
    241         [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
     249      [ Vint sz1 n1 ⇒ match v2 with
     250        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     251                        (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
    242252        | _ ⇒ None ? ]
    243253      | _ ⇒ None ? ]
     
    248258let rec sem_and (v1,v2: val) : option val ≝
    249259  match v1 with
    250   [ Vint n1 ⇒ match v2 with
    251     [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2))
     260  [ Vint sz1 n1 ⇒ match v2 with
     261    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     262                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?)
    252263    | _ ⇒ None ? ]
    253264  | _ ⇒ None ?
     
    256267let rec sem_or (v1,v2: val) : option val ≝
    257268  match v1 with
    258   [ Vint n1 ⇒ match v2 with
    259     [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2))
     269  [ Vint sz1 n1 ⇒ match v2 with
     270    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     271                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?)
    260272    | _ ⇒ None ? ]
    261273  | _ ⇒ None ?
     
    264276let rec sem_xor (v1,v2: val) : option val ≝
    265277  match v1 with
    266   [ Vint n1 ⇒ match v2 with
    267     [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2))
     278  [ Vint sz1 n1 ⇒ match v2 with
     279    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     280                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?)
    268281    | _ ⇒ None ? ]
    269282  | _ ⇒ None ?
     
    272285let rec sem_shl (v1,v2: val): option val ≝
    273286  match v1 with
    274   [ Vint n1 ⇒ match v2 with
    275     [ Vint n2 ⇒
    276         if ltu n2 iwordsize then Some ? (Vint(shl n1 n2)) else None ?
     287  [ Vint sz1 n1 ⇒ match v2 with
     288    [ Vint sz2 n2 ⇒
     289        if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     290        then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
     291        else None ?
    277292    | _ ⇒ None ? ]
    278293  | _ ⇒ None ? ].
     
    282297  [ shr_case_I32unsi ⇒
    283298      match v1 with
    284       [ Vint n1 ⇒ match v2 with
    285         [ Vint n2 ⇒
    286             if ltu n2 iwordsize then Some ? (Vint (shru n1 n2)) else None ?
     299      [ Vint sz1 n1 ⇒ match v2 with
     300        [ Vint sz2 n2 ⇒
     301            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     302            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
     303            else None ?
    287304        | _ ⇒ None ? ]
    288305      | _ ⇒ None ? ]
    289306   | shr_case_ii =>
    290307      match v1 with
    291       [ Vint n1 ⇒ match v2 with
    292         [ Vint n2 ⇒
    293             if ltu n2 iwordsize then Some ? (Vint (shr n1 n2)) else None ?
     308      [ Vint sz1 n1 ⇒ match v2 with
     309        [ Vint sz2 n2 ⇒
     310            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     311            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
     312            else None ?
    294313        | _ ⇒ None ? ]
    295314      | _ ⇒ None ? ]
     
    318337  [ cmp_case_I32unsi ⇒
    319338      match v1 with
    320       [ Vint n1 ⇒ match v2 with
    321         [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
     339      [ Vint sz1 n1 ⇒ match v2 with
     340        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     341                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
    322342        | _ ⇒ None ? ]
    323343      | _ ⇒ None ? ]
    324344  | cmp_case_ii ⇒
    325345      match v1 with
    326       [ Vint n1 ⇒ match v2 with
    327          [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     346      [ Vint sz1 n1 ⇒ match v2 with
     347         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     348                         (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
    328349         | _ ⇒ None ?
    329350         ]
     
    396417  resulting in value [v2].  *)
    397418
    398 let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝
    399   match sz with
    400   [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ]
    401   | I16 ⇒ match sg with [ Signed => sign_ext 16 i | Unsigned ⇒ zero_ext 16 i ]
    402   | I32 ⇒ i
    403   ].
    404 
    405 let rec cast_int_float (si : signedness) (i: int) : float ≝
     419let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
     420  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
     421
     422let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝
    406423  match si with
    407   [ Signed ⇒ floatofint i
    408   | Unsigned ⇒ floatofintu i
    409   ].
    410 
    411 let rec cast_float_int (si : signedness) (f: float) : int
     424  [ Signed ⇒ floatofint ? i
     425  | Unsigned ⇒ floatofintu ? i
     426  ].
     427
     428let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz)
    412429  match si with
    413   [ Signed ⇒ intoffloat f
    414   | Unsigned ⇒ intuoffloat f
     430  [ Signed ⇒ intoffloat ? f
     431  | Unsigned ⇒ intuoffloat ? f
    415432  ].
    416433
     
    428445
    429446inductive cast : mem → val → type → type → val → Prop ≝
    430   | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
    431       cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
    432            (Vint (cast_int_int sz2 si2 i))
     447  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
     448      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
     449           (Vint sz2 (cast_int_int ? sz2 si2 i))
    433450  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
    434451      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
    435            (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
    436   | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
    437       cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
    438           (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
     452           (Vint sz2 (cast_float_int sz2 si2 f))
     453  | cast_if:   ∀m,sz1,sz2,si1,i.                (**r int to float  *)
     454      cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2)
     455          (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
    439456  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
    440457      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
     
    447464  | cast_ip_z: ∀m,sz,sg,ty',r.
    448465      type_region ty' r →
    449       cast m (Vint zero) (Tint sz sg) ty' (Vnull r)
     466      cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
    450467  | cast_pp_z: ∀m,ty,ty',r,r'.
    451468      type_region ty r →
     
    546563(* * Selection of the appropriate case of a [switch], given the value [n]
    547564  of the selector expression. *)
    548 
    549 let rec select_switch (n: int) (sl: labeled_statements)
     565(* FIXME: now that we have several sizes of integer, it isn't clear whether we
     566   should allow case labels to be of a different size to the switch expression. *)
     567let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
    550568                       on sl : labeled_statements ≝
    551569  match sl with
    552570  [ LSdefault _ ⇒ sl
    553   | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl'
     571  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
     572                         (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl')
    554573  ].
    555574
     
    559578  match sl with
    560579  [ LSdefault s ⇒ s
    561   | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
     580  | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
    562581  ].
    563582
     
    579598
    580599inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    581   | eval_Econst_int:   ∀i,ty.
    582       eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
     600  | eval_Econst_int:   ∀sz,sg,i.
     601      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
    583602  | eval_Econst_float:   ∀f,ty.
    584603      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
     
    591610      ∀pc:pointer_compat loc r.
    592611      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
    593   | eval_Esizeof: ∀ty',ty.
    594       eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     612  | eval_Esizeof: ∀ty',sz,sg.
     613      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
    595614  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
    596615      eval_expr ge e m a v1 tr →
     
    663682      typeof a = Tstruct id fList →
    664683      field_offset i fList = OK ? delta →
    665       eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr
     684      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
    666685 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
    667686      eval_lvalue ge e m a l ofs tr →
     
    671690let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
    672691  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    673   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     692  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    674693  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    675694  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    676695  (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
    677   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     696  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    678697  (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))
    679698  (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))
     
    688707  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
    689708  match ev with
    690   [ eval_Econst_int i ty ⇒ eci i ty
     709  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    691710  | eval_Econst_float f ty ⇒ ecF f ty
    692711  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    693712  | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
    694   | eval_Esizeof ty' ty ⇒ esz ty' ty
     713  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    695714  | 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)
    696715  | 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)
     
    779798  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    780799  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    781   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     800  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    782801  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    783802  (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))
    784803  (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))
    785   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     804  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    786805  (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))
    787806  (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))
     
    802821  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
    803822  match ev with
    804   [ eval_Econst_int i ty ⇒ eci i ty
     823  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    805824  | eval_Econst_float f ty ⇒ ecF f ty
    806825  | 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)
    807826  | 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)
    808   | eval_Esizeof ty' ty ⇒ esz ty' ty
     827  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    809828  | 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)
    810829  | 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)
     
    821840  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    822841  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    823   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     842  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    824843  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    825844  (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))
    826845  (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))
    827   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     846  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    828847  (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))
    829848  (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))
     
    9831002  match sl with
    9841003  [ LSdefault s => find_label lbl s k
    985   | LScase _ s sl' =>
     1004  | LScase _ _ s sl' =>
    9861005      match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
    9871006      [ Some sk => Some ? sk
     
    11351154           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11361155
    1137   | step_switch: ∀f,a,sl,k,e,m,n,tr.
    1138       eval_expr ge e m a (Vint n) tr →
     1156  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
     1157      eval_expr ge e m a (Vint sz n) tr →
    11391158      step ge (State f (Sswitch a sl) k e m)
    1140            tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
     1159           tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m)
    11411160  | step_skip_break_switch: ∀f,x,k,e,m.
    11421161      x = Sskip ∨ x = Sbreak →
     
    15031522inductive final_state: state -> int -> Prop :=
    15041523  | final_state_intro: ∀r,m.
    1505       final_state (Returnstate (Vint r) Kstop m) r.
     1524      final_state (Returnstate (Vint I32 r) Kstop m) r.
    15061525
    15071526(* * Execution of a whole program: [exec_program p beh]
  • src/Clight/Csyntax.ma

    r879 r961  
    156156
    157157with expr_descr : Type[0] ≝
    158   | Econst_int: int → expr_descr       (**r integer literal *)
     158  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
    159159  | Econst_float: float → expr_descr   (**r float literal *)
    160160  | Evar: ident → expr_descr           (**r variable *)
     
    207207with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
    208208  | LSdefault: statement → labeled_statements
    209   | LScase: int → statement → labeled_statements → labeled_statements.
     209  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
    210210
    211211let rec statement_ind2
     
    227227  (Scs:∀l,s. P s → P (Scost l s))
    228228  (LSd:∀s. P s → Q (LSdefault s))
    229   (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     229  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    230230  (s:statement) on s : P s ≝
    231231match s with
     
    276276  (Scs:∀l,s. P s → P (Scost l s))
    277277  (LSd:∀s. P s → Q (LSdefault s))
    278   (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     278  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    279279  (ls:labeled_statements) on ls : Q ls ≝
    280280match ls with
    281281[ LSdefault s ⇒ LSd s
    282282    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    283 | LScase i s t ⇒ LSc i s t
     283| LScase sz i s t ⇒ LSc sz i s t
    284284    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    285285    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
     
    288288definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
    289289  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
    290   (λ_,_. I) (λ_,_,_,_,_.I).
     290  (λ_,_. I) (λ_,_,_,_,_,_.I).
    291291
    292292(* * ** Functions *)
  • src/Clight/casts.ma

    r824 r961  
    1 include "common/Integers.ma".
     1include "common/Values.ma".
    22
    33definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
     
    55
    66lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
    7 #A #n #x elim x //
     7#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
    88qed.
    99
     
    8282lemma truncate_tail : ∀m,n,v.
    8383  truncate (S m) n v = truncate m n (tail … v).
    84   //
     84#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
    8585  qed.
    8686
     
    118118qed.
    119119
    120 definition sign_bit : ∀n. BitVector n → bool ≝
    121 λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
    122 
    123120definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
    124121λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
    125 
     122 
    126123lemma truncate_sign : ∀m,n,x.
    127124  truncate m n (sign … x) = x.
     
    178175#m #n #x @(vector_inv_n … x) #h #t elim n
    179176[ @refl
    180 | #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl
     177| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
    181178] qed.
    182179
  • src/Clight/label.ma

    r781 r961  
    5454    do 〈e2,costgen〉 ← label_expr e2 costgen;
    5555    do 〈e2,costgen〉 ← add_cost_expr e2 costgen;
    56     do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int zero) (Tint I32 Signed)) costgen;
     56    do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen;
    5757    OK ? 〈Econdition e1 e2 ef, costgen〉
    5858| Eorbool e1 e2 ⇒
    5959    do 〈e1,costgen〉 ← label_expr e1 costgen;
    60     do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int one) (Tint I32 Signed)) costgen;
     60    do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen;
    6161    do 〈e2,costgen〉 ← label_expr e2 costgen;
    6262    do 〈e2,costgen〉 ← add_cost_expr e2 costgen;
     
    165165    do 〈s,costgen〉 ← add_cost_before s costgen;
    166166    OK ? 〈LSdefault s, costgen〉
    167 | LScase i s ls' ⇒
     167| LScase sz i s ls' ⇒
    168168    do 〈s,costgen〉 ← label_statement s costgen;
    169169    do 〈s,costgen〉 ← add_cost_before s costgen;
    170170    do 〈ls',costgen〉 ← label_lstatements ls' costgen;
    171     OK ? 〈LScase i s ls', costgen〉
     171    OK ? 〈LScase sz i s ls', costgen〉
    172172].
    173173
  • src/Clight/test/memorymodel.ma

    r717 r961  
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
     29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
    3030
    3131  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    3434(* overwrite the first byte of the value *)
    3535definition store3 : mem.
    36   letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
     36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    4242example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
    4343
    44 (* The read is successful and returns a signed version of the value. *)
    45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
     44(* The read is successful and returns the value. *)
     45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
     
    6363definition storeIIblk := alloc storeA 0 4 Any.
    6464definition storeIII : mem.
    65  letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
     65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
    6666  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
    6767  | #rr #_ @rr ] qed.
  • src/Clight/test/search.ma

    r816 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    99         (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    1212       (Ssequence
     
    1717               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    1818               (Tint I32 Signed  ))
    19              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     19             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2020             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    2121       (Ssequence
     
    3939                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    4040                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    41                (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     41               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    4242               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4343         (Ssequence
     
    8080                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    8181                   (Tint I32 Signed  ))
    82                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     82                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    8383                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    8484           Sskip)
     
    103103                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    104104                   (Tint I32 Signed  ))
    105                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     105                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    106106                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    107107           Sskip)))))
    108108       Sskip)
    109109       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    110                              (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
     110                             (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    111111                                                 (Tint I32 Signed  )))
    112112                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
     
    122122                   (Expr (Evar (ident_of_nat 4))
    123123                     (Tarray Any (Tint I8 Unsigned ) 5))
    124                    (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    125                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    126         (Expr (Ecast (Tint I8 Unsigned )
    127           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    128           (Tint I8 Unsigned )))
    129       (Ssequence
    130       (Sassign (Expr (Ederef
    131                  (Expr (Ebinop Oadd
    132                    (Expr (Evar (ident_of_nat 4))
    133                      (Tarray Any (Tint I8 Unsigned ) 5))
    134                    (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    135                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    136         (Expr (Ecast (Tint I8 Unsigned )
    137           (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
    138           (Tint I8 Unsigned )))
    139       (Ssequence
    140       (Sassign (Expr (Ederef
    141                  (Expr (Ebinop Oadd
    142                    (Expr (Evar (ident_of_nat 4))
    143                      (Tarray Any (Tint I8 Unsigned ) 5))
    144                    (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    145                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    146         (Expr (Ecast (Tint I8 Unsigned )
    147           (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
    148           (Tint I8 Unsigned )))
    149       (Ssequence
    150       (Sassign (Expr (Ederef
    151                  (Expr (Ebinop Oadd
    152                    (Expr (Evar (ident_of_nat 4))
    153                      (Tarray Any (Tint I8 Unsigned ) 5))
    154                    (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
    155                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    156         (Expr (Ecast (Tint I8 Unsigned )
    157           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
    158           (Tint I8 Unsigned )))
    159       (Ssequence
    160       (Sassign (Expr (Ederef
    161                  (Expr (Ebinop Oadd
    162                    (Expr (Evar (ident_of_nat 4))
    163                      (Tarray Any (Tint I8 Unsigned ) 5))
    164                    (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
    165                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    166         (Expr (Ecast (Tint I8 Unsigned )
    167           (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
     124                   (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     125                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     126        (Expr (Ecast (Tint I8 Unsigned )
     127          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     128          (Tint I8 Unsigned )))
     129      (Ssequence
     130      (Sassign (Expr (Ederef
     131                 (Expr (Ebinop Oadd
     132                   (Expr (Evar (ident_of_nat 4))
     133                     (Tarray Any (Tint I8 Unsigned ) 5))
     134                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     135                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     136        (Expr (Ecast (Tint I8 Unsigned )
     137          (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
     138          (Tint I8 Unsigned )))
     139      (Ssequence
     140      (Sassign (Expr (Ederef
     141                 (Expr (Ebinop Oadd
     142                   (Expr (Evar (ident_of_nat 4))
     143                     (Tarray Any (Tint I8 Unsigned ) 5))
     144                   (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     145                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     146        (Expr (Ecast (Tint I8 Unsigned )
     147          (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
     148          (Tint I8 Unsigned )))
     149      (Ssequence
     150      (Sassign (Expr (Ederef
     151                 (Expr (Ebinop Oadd
     152                   (Expr (Evar (ident_of_nat 4))
     153                     (Tarray Any (Tint I8 Unsigned ) 5))
     154                   (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     155                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     156        (Expr (Ecast (Tint I8 Unsigned )
     157          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     158          (Tint I8 Unsigned )))
     159      (Ssequence
     160      (Sassign (Expr (Ederef
     161                 (Expr (Ebinop Oadd
     162                   (Expr (Evar (ident_of_nat 4))
     163                     (Tarray Any (Tint I8 Unsigned ) 5))
     164                   (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
     165                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     166        (Expr (Ecast (Tint I8 Unsigned )
     167          (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
    168168          (Tint I8 Unsigned )))
    169169      (Ssequence
     
    173173        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    174174        (Expr (Ecast (Tint I8 Unsigned )
    175           (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
     175          (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
    176176          (Tint I8 Unsigned ));
    177177        (Expr (Ecast (Tint I8 Unsigned )
    178           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
     178          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    179179          (Tint I8 Unsigned ))])
    180180      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     
    189189.
    190190
    191 example exec: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     191example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    192192normalize  (* you can examine the result here *)
    193193@refl
     
    197197include "Cminor/semantics.ma".
    198198
    199 example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     199example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    200200normalize
    201201@refl
  • src/Clight/test/sum.ma

    r881 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    99         (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    1212       (Ssequence
    1313       (Ssequence
    1414       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    15                (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     15               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1616         (Expr (Ebinop Olt
    1717           (Expr (Ecast (Tint I32 Unsigned)
     
    2323           (Expr (Ebinop Oadd
    2424             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    25              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     25             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2626             (Tint I32 Signed  )))
    2727         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     
    5151  (ident_of_nat 0)
    5252  [〈〈〈ident_of_nat 3 (* src *),
    53      [(Init_int8 (repr 28)) ; (Init_int8 (repr 17)) ; (Init_int8 (repr 17)) ;
    54      (Init_int8 (repr 8)) ; (Init_int8 (repr 4)) ]〉, Any〉,
     53     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
     54     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
    5555     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5656.
    5757
    58 example exec: finishes_with (repr 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     58example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    5959normalize  (* you can examine the result here *)
    6060@refl
  • src/Clight/toCminor.ma

    r886 r961  
    141141match ls with
    142142[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
    143 | LScase _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
    144                     gather_mem_vars_ls ls1
     143| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
     144                      gather_mem_vars_ls ls1
    145145].
    146146
     
    217217[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
    218218| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
    219 | add_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
    220 | add_case_ip ty ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst (repr (sizeof ty))))))
     219(* XXX using the integer size for e2 as the offset's size isn't right, because
     220   if e2 produces an 8bit value then the true offset might overflow *)
     221| add_case_pi ty ⇒
     222    match ty2' with
     223    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
     224    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     225    ]
     226| add_case_ip ty ⇒
     227    match ty1' with
     228    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
     229    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     230    ]
    221231| add_default ⇒ Error ? (msg TypeMismatch)
    222232].
     
    229239[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
    230240| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
    231 | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
    232 | sub_case_pp ty ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' Osubpp e1 e2) (Cst ? (Ointconst (repr (sizeof ty)))))
     241(* XXX choosing offset sizes? *)
     242| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     243| sub_case_pp ty ⇒
     244    match ty' with (* XXX overflow *)
     245    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
     246    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     247    ]
    233248| sub_default ⇒ Error ? (msg TypeMismatch)
    234249].
     
    249264let ty2' ≝ typ_of_type ty2 in
    250265match classify_div ty1 ty2 with
    251 [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) (* FIXME: should be 8 bit only *)
     266[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
    252267| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
    253268| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
     
    260275let ty2' ≝ typ_of_type ty2 in
    261276match classify_mod ty1 ty2 with
    262 [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) (* FIXME: should be 8 bit only *)
     277[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
    263278| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
    264279| mod_default ⇒ Error ? (msg TypeMismatch)
     
    270285let ty2' ≝ typ_of_type ty2 in
    271286match classify_shr ty1 ty2 with
    272 [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) (* FIXME: should be 8 bit only *)
     287[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
    273288| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
    274289| shr_default ⇒ Error ? (msg TypeMismatch)
     
    331346[ Tint sz1 sg1 ⇒ λe.
    332347    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    333     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
     348    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sz2 sg2) e)
    334349    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
    335350    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
     
    339354| Tfloat sz1 ⇒ λe.
    340355    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    341     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
     356    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    342357    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
    343358    | _ ⇒ Error ? (msg TypeMismatch)
     
    345360| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    346361    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    347     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Ointofptr e)
     362    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
    348363    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    349364    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     
    352367| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    353368    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    354     [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) Ointofptr e)
     369    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
    355370    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    356371    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     
    393408[ Expr ed ty ⇒
    394409  match ed with
    395   [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
     410  [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
    396411  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
    397412  | Evar id ⇒
     
    400415      [ Global r ⇒
    401416          match access_mode ty with
    402           [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id zero)))
    403           | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
     417          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
     418          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
    404419          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    405420          ]
    406421      | Stack n ⇒
    407422          match access_mode ty with
    408           [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack (repr n))))
    409           | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
     423          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
     424          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
    410425          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    411426          ]
     
    457472      do e1' ← translate_expr vars e1;
    458473      do e2' ← translate_expr vars e2;
    459       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    460       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    461       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
    462       | _ ⇒ λ_.Error ? (msg TypeMismatch)
    463       ] e1'
     474      match ty with
     475      [ Tint sz _ ⇒
     476        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     477        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
     478        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
     479        | _ ⇒ λ_.Error ? (msg TypeMismatch)
     480        ] e1'
     481      | _ ⇒ Error ? (msg TypeMismatch)
     482      ]
    464483  | Eorbool e1 e2 ⇒
    465484      do e1' ← translate_expr vars e1;
    466485      do e2' ← translate_expr vars e2;
    467       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    468       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    469       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
    470       | _ ⇒ λ_.Error ? (msg TypeMismatch)
    471       ] e1'
    472   | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
     486      match ty with
     487      [ Tint sz _ ⇒
     488        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     489        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
     490        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
     491        | _ ⇒ λ_.Error ? (msg TypeMismatch)
     492        ] e1'
     493      | _ ⇒ Error ? (msg TypeMismatch)
     494      ]
     495  | Esizeof ty1 ⇒
     496      match ty with
     497      [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
     498      | _ ⇒ Error ? (msg TypeMismatch)
     499      ]
    473500  | Efield e1 id ⇒
    474501      do e' ← match typeof e1 with
     
    479506            do off ← field_offset id fl;
    480507            match access_mode ty with
    481             [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
    482             | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
     508            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
     509            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
    483510            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    484511            ]
     
    509536      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    510537      match c return λ_. res (Σr.CMexpr (ASTptr r)) with
    511       [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id zero)))
    512       | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack (repr n))))
     538      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
     539      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
    513540      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
    514541      ]
     
    525552          do off ← field_offset id fl;
    526553          match e1' with
    527           [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst (repr off)))))
     554          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
    528555          ]
    529556      | Tunion _ _ ⇒ translate_addr vars e1
     
    554581            match c with
    555582            [ Local ⇒ OK ? (IdDest id)
    556             | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id zero)))
    557             | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack (repr n))))
     583            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
     584            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
    558585            ]
    559586        | _ ⇒
  • src/Cminor/initialisation.ma

    r887 r961  
    99λinit.
    1010match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
    11 [ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
    12 | Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
    13 | Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
     11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
    1414| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
    1515| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
    1818| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1919].
     
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
     24definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
    2525λid,r,init,off.
    2626match init_expr init with
     
    3737  (λdatum,os.
    3838   let 〈off,s〉 ≝ os in
    39      〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
    40   〈zero, St_skip〉 init).
     39     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
     40  〈0, St_skip〉 init).
    4141
    4242definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
  • src/Cminor/semantics.ma

    r886 r961  
    9191].
    9292
    93 let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
     93let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
    9494match cs with
    9595[ nil ⇒ default
    9696| cons h t ⇒
    9797    let 〈hi,a〉 ≝ h in
    98     if eq i hi then a else find_case A i t default
     98    if eq_bv ? i hi then a else find_case A sz i t default
    9999].
    100100
     
    199199        ! k' ← k_exit n k;
    200200        ret ? 〈E0, State f St_skip en m sp k'〉
    201     | St_switch _ _ e cs default ⇒
     201    | St_switch sz _ e cs default ⇒
    202202        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    203203        match v with
    204         [ Vint i ⇒
    205             ! k' ← k_exit (find_case ? i cs default) k;
    206             ret ? 〈tr, State f St_skip en m sp k'〉
     204        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
     205            ! k' ← k_exit (find_case ?? i cs default) k;
     206            ret ? 〈tr, State f St_skip en m sp k'〉)
     207            (Wrong ??? (msg BadSwitchValue))
    207208        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    208209        ]
     
    257258        | Some v ⇒
    258259            match v with
    259             [ Vint i ⇒ Some ? i
     260            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    260261            | _ ⇒ None ?
    261262            ]
  • src/Cminor/syntax.ma

    r886 r961  
    2727| St_exit : nat → stmt
    2828(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    29 | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    3030| St_return : option (Σt. expr t) → stmt
    3131| St_label : ident → stmt → stmt
  • src/Cminor/toRTLabs.ma

    r888 r961  
    210210      do f ← add_fresh_to_graph (St_cond br l_case) f;
    211211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
    212       add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
     212      add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;
    213213    add_expr env ? e r f
    214214| St_return opt_e ⇒
  • src/RTLabs/semantics.ma

    r888 r961  
    148148      ! v ← reg_retrieve (locals f) r;
    149149      match v with
    150       [ Vint i ⇒
     150      [ Vint _ i ⇒
    151151          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
    152152          ret ? 〈E0, build_state f fs m l〉
     
    193193| Callstate _ _ _ _ _ ⇒ None ?
    194194| Returnstate v _ fs _ ⇒
    195     match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
     195    match fs with [ nil ⇒
     196      match v with [ Some v' ⇒
     197        match v' with
     198        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
     199        | _ ⇒ None ? ]
     200      | None ⇒ None ? ]
     201    | cons _ _ ⇒ None ? ]
    196202].
    197203
  • src/common/AST.ma

    r882 r961  
    2020include "common/Integers.ma".
    2121include "common/Floats.ma".
    22 include "ASM/BitVector.ma".
     22include "ASM/Arithmetic.ma".
    2323include "common/Identifiers.ma".
    2424
     
    110110definition SigType_Ptr ≝ ASTptr Any.
    111111
     112(* Define these carefully so that we always know that the result is nonzero,
     113   and can be used in dependent types of the form (S n).
     114   (At the time of writing this is only used for bitsize_of_intsize.) *)
     115
    112116definition size_intsize : intsize → nat ≝
    113 λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
     117λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     118
     119definition bitsize_of_intsize : intsize → nat ≝
     120λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
     121
     122definition eq_intsize : intsize → intsize → bool ≝
     123λsz1,sz2.
     124  match sz1 with
     125  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
     126  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
     127  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
     128  ].
     129
     130lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
     131  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
     132* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     133qed.
     134
     135lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
     136* @refl
     137qed.
     138
     139lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
     140* * * #NE try @refl @False_ind @NE @refl
     141qed.
     142
     143(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
     144   if it is returns [e1] where the type of [n] has its dependency on [sz1]
     145   changed to [sz2], and if not returns [e2]. *)
     146let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
     147  P sz1 → (P sz2 → A) → A → A ≝
     148match sz1 return λsz. P sz → (P sz2 → A) → A → A with
     149[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     150| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     151| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     152].
     153
     154lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
     155  intsize_eq_elim A sz sz P p f d = f p.
     156#A * //
     157qed.
     158
     159lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
     160  (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).
     161#A * * #P #p #f #d #Q #Hne #Heq
     162[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
     163| *: whd in ⊢ (?%) @Hne % #E destruct
     164] qed.
     165
     166
     167(* A type for the integers that appear in the semantics. *)
     168definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
     169
     170definition repr : ∀sz:intsize. nat → bvint sz ≝
     171λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
     172
    114173
    115174definition size_floatsize : floatsize → nat ≝
    116 λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
     175λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
    117176
    118177definition typesize : typ → nat ≝ λty.
     
    187246
    188247inductive init_data: Type[0] ≝
    189   | Init_int8: int → init_data
    190   | Init_int16: int → init_data
    191   | Init_int32: int → init_data
     248  | Init_int8: bvint I8 → init_data
     249  | Init_int16: bvint I16 → init_data
     250  | Init_int32: bvint I32 → init_data
    192251  | Init_float32: float → init_data
    193252  | Init_float64: float → init_data
    194253  | Init_space: nat → init_data
    195254  | Init_null: region → init_data
    196   | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
     255  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
    197256
    198257(* * Whole programs consist of:
  • src/common/Animation.ma

    r879 r961  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     12[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
    1313| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
    1414| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
  • src/common/Events.ma

    r879 r961  
    3737  world. *)
    3838
    39 inductive eventval: Type[0] :=
    40   | EVint: int -> eventval
    41   | EVfloat: float -> eventval.
     39inductive eventval: Type[0]
     40  | EVint: ∀sz. bvint sz → eventval
     41  | EVfloat: float eventval.
    4242
    4343inductive event : Type[0] ≝
     
    193193inductive eventval_match: eventval -> typ -> val -> Prop :=
    194194  | ev_match_int:
    195       ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
     195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
    196196  | ev_match_float:
    197197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
  • src/common/Floats.ma

    r700 r961  
    3434axiom Fabs: float → float.
    3535axiom singleoffloat: float → float.
    36 axiom intoffloat: float → int.
    37 axiom intuoffloat: float → int.
    38 axiom floatofint: int → float.
    39 axiom floatofintu: int → float.
     36axiom intoffloat: ∀n. float → BitVector n.
     37axiom intuoffloat: ∀n. float → BitVector n.
     38axiom floatofint: ∀n. BitVector n → float.
     39axiom floatofintu: ∀n. BitVector n → float.
    4040
    4141axiom Fadd: float → float → float.
  • src/common/FrontEndOps.ma

    r774 r961  
    2121
    2222inductive constant : Type[0] ≝
    23   | Ointconst: int → constant     (**r integer constant *)
    24   | Ofloatconst: float → constant (**r floating-point constant *)
    25   | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
    26   | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)
     23  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
     24  | Ofloatconst: float → constant          (**r floating-point constant *)
     25  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
    2727
    2828inductive unary_operation : Type[0] ≝
    29   | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
    30   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
    31   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
    32   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
     29  | Ocastint: intsize → signedness → unary_operation (**r 8-bit zero extension  *)
    3330  | Onegint: unary_operation               (**r integer opposite *)
    3431  | Onotbool: unary_operation              (**r boolean negation  *)
     
    3734  | Oabsf: unary_operation                 (**r float absolute value *)
    3835  | Osingleoffloat: unary_operation        (**r float truncation *)
    39   | Ointoffloat: unary_operation          (**r signed integer to float *)
    40   | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
     36  | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
     37  | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
    4138  | Ofloatofint: unary_operation           (**r float to signed integer *)
    4239  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
    4340  | Oid: unary_operation                   (**r identity (used to move between registers *)
    4441  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
    45   | Ointofptr: unary_operation.            (**r pointer to int *)
     42  | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
    4643
    4744inductive binary_operation : Type[0] ≝
     
    6865  | Oaddp: binary_operation                (**r add an integer to a pointer *)
    6966  | Osubpi: binary_operation               (**r subtract int from a pointers *)
    70   | Osubpp: binary_operation               (**r subtract two pointers *)
     67  | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
    7168  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    7269
     
    8077λfind_symbol,sp,cst.
    8178  match cst with
    82   [ Ointconst n ⇒ Some ? (Vint n)
     79  [ Ointconst sz n ⇒ Some ? (Vint sz n)
    8380  | Ofloatconst n ⇒ Some ? (Vfloat n)
    8481  | Oaddrsymbol s ofs ⇒
    8582      match find_symbol s with
    8683      [ None ⇒ None ?
    87       | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
     84      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
    8885      ]
    8986  | Oaddrstack ofs ⇒
    90       Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
     87      Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
    9188  ]. cases sp // qed.
    9289
     
    9491λop,arg.
    9592  match op with
    96   [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
    97   | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
    98   | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
    99   | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
    100   | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
    101   | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
     93  [ Ocastint sz sg ⇒
     94      match sg with
     95      [ Unsigned ⇒ Some ? (zero_ext sz arg)
     96      |   Signed ⇒ Some ? (sign_ext sz arg)
     97      ]
     98  | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
     99  | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
    102100                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
    103101                              | Vnull _ ⇒ Some ? Vtrue
    104102                              | _ ⇒ None ?
    105103                              ]
    106   | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
     104  | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    107105  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    108106  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
    109107  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    110   | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
    111   | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
    112   | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
    113   | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
     108  | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
     109  | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
     110  | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
     111  | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
    114112  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    115113  (* Only conversion of null pointers is specified. *)
    116   | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    117   | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     114  | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     115  | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    118116  ].
    119117
     
    122120λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
    123121
    124 (* Individual operations, adapted from Values. *)
    125 
    126 definition ev_neg : val → option val ≝ λv.
    127   match v with
    128   [ Vint n ⇒ Some ? (Vint (neg n))
    129   | _ ⇒ None ?
    130   ].
    131 
    132 definition ev_negf : val → option val ≝ λv.
    133   match v with
    134   [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
    135   | _ ⇒ None ?
    136   ].
    137 
    138 definition ev_absf : val → option val ≝ λv.
    139   match v with
    140   [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
    141   | _ ⇒ None ?
    142   ].
    143 
    144 definition ev_intoffloat : val → option val ≝ λv.
    145   match v with
    146   [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
    147   | _ ⇒ None ?
    148   ].
    149 
    150 definition ev_intuoffloat : val → option val ≝ λv.
    151   match v with
    152   [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
    153   | _ ⇒ None ?
    154   ].
    155 
    156 definition ev_floatofint : val → option val ≝ λv.
    157   match v with
    158   [ Vint n ⇒ Some ? (Vfloat (floatofint n))
    159   | _ ⇒ None ?
    160   ].
    161 
    162 definition ev_floatofintu : val → option val ≝ λv.
    163   match v with
    164   [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
    165   | _ ⇒ None ?
    166   ].
    167 
    168 definition ev_notint : val → option val ≝ λv.
    169   match v with
    170   [ Vint n ⇒ Some ? (Vint (xor n mone))
    171   | _ ⇒ None ?
    172   ].
    173  
    174 definition ev_notbool : val → option val ≝ λv.
    175   match v with
    176   [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
    177   | Vptr _ b _ ofs ⇒ Some ? Vfalse
    178   | Vnull _ ⇒ Some ? Vtrue
    179   | _ ⇒ None ?
    180   ].
    181 
    182 definition ev_zero_ext ≝ λnbits: nat. λv: val.
    183   match v with
    184   [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
    185   | _ ⇒ None ?
    186   ].
    187 
    188 definition ev_sign_ext ≝ λnbits:nat. λv:val.
    189   match v with
    190   [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
    191   | _ ⇒ None ?
    192   ].
    193 
    194 definition ev_singleoffloat : val → option val ≝ λv.
    195   match v with
    196   [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
    197   | _ ⇒ None ?
    198   ].
     122(* Individual operations, adapted from Values.  These differ in that they
     123   implement the plain Cminor/RTLabs operations (e.g., with separate addition
     124   for ints,floats and pointers) and use option rather than Vundef.  The ones
     125   in Value are probably not needed. *)
    199126
    200127definition ev_add ≝ λv1,v2: val.
    201128  match v1 with
    202   [ Vint n1 ⇒ match v2 with
    203     [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
     129  [ Vint sz1 n1 ⇒ match v2 with
     130    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     131                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
     132                    (None ?)
    204133    | _ ⇒ None ? ]
    205134  | _ ⇒ None ? ].
     
    207136definition ev_sub ≝ λv1,v2: val.
    208137  match v1 with
    209   [ Vint n1 ⇒ match v2 with
    210     [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
     138  [ Vint sz1 n1 ⇒ match v2 with
     139    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     140                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
     141                    (None ?)
    211142    | _ ⇒ None ? ]
    212143  | _ ⇒ None ? ].
     
    216147  match v1 with
    217148  [ Vptr r b1 p ofs1 ⇒ match v2 with
    218     [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
     149    [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
    219150    | _ ⇒ None ? ]
    220151  | Vnull r ⇒ match v2 with
    221     [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     152    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    222153    | _ ⇒ None ?
    223154    ]
     
    227158  match v1 with
    228159  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    229     [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
    230     | _ ⇒ None ? ]
    231   | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    232   | _ ⇒ None ? ].
    233 
    234 definition ev_subpp ≝ λv1,v2: val.
     160    [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
     161    | _ ⇒ None ? ]
     162  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     163  | _ ⇒ None ? ].
     164
     165definition ev_subpp ≝ λsz. λv1,v2: val.
    235166  match v1 with
    236167  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    237168    [ Vptr r2 b2 p2 ofs2 ⇒
    238         if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    239     | _ ⇒ None ? ]
    240   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     169        if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
     170    | _ ⇒ None ? ]
     171  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    241172  | _ ⇒ None ? ].
    242173
    243174definition ev_mul ≝ λv1, v2: val.
    244175  match v1 with
    245   [ Vint n1 ⇒ match v2 with
    246     [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     176  [ Vint sz1 n1 ⇒ match v2 with
     177    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     178                    (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
     179                    (None ?)
    247180    | _ ⇒ None ? ]
    248181  | _ ⇒ None ? ].
     
    250183definition ev_divs ≝ λv1, v2: val.
    251184  match v1 with
    252   [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
     185  [ Vint sz1 n1 ⇒ match v2 with
     186    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     187                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
     188                    (None ?)
    254189    | _ ⇒ None ? ]
    255190  | _ ⇒ None ? ].
     
    257192definition ev_mods ≝ λv1, v2: val.
    258193  match v1 with
    259   [ Vint n1 ⇒ match v2 with
    260     [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
     194  [ Vint sz1 n1 ⇒ match v2 with
     195    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     196                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
     197                    (None ?)
    261198    | _ ⇒ None ?
    262199    ]
     
    266203definition ev_divu ≝ λv1, v2: val.
    267204  match v1 with
    268   [ Vint n1 ⇒ match v2 with
    269     [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
     205  [ Vint sz1 n1 ⇒ match v2 with
     206    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     207                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
     208                    (None ?)
    270209    | _ ⇒ None ?
    271210    ]
     
    275214definition ev_modu ≝ λv1, v2: val.
    276215  match v1 with
    277   [ Vint n1 ⇒ match v2 with
    278     [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
     216  [ Vint sz1 n1 ⇒ match v2 with
     217    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     218                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
     219                    (None ?)
    279220    | _ ⇒ None ?
    280221    ]
     
    284225definition ev_and ≝ λv1, v2: val.
    285226  match v1 with
    286   [ Vint n1 ⇒ match v2 with
    287     [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
     227  [ Vint sz1 n1 ⇒ match v2 with
     228    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     229                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
     230                    (None ?)
    288231    | _ ⇒ None ? ]
    289232  | _ ⇒ None ? ].
     
    291234definition ev_or ≝ λv1, v2: val.
    292235  match v1 with
    293   [ Vint n1 ⇒ match v2 with
    294     [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
     236  [ Vint sz1 n1 ⇒ match v2 with
     237    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     238                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
     239                    (None ?)
    295240    | _ ⇒ None ? ]
    296241  | _ ⇒ None ? ].
     
    298243definition ev_xor ≝ λv1, v2: val.
    299244  match v1 with
    300   [ Vint n1 ⇒ match v2 with
    301     [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
     245  [ Vint sz1 n1 ⇒ match v2 with
     246    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     247                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
     248                    (None ?)
    302249    | _ ⇒ None ? ]
    303250  | _ ⇒ None ? ].
     
    305252definition ev_shl ≝ λv1, v2: val.
    306253  match v1 with
    307   [ Vint n1 ⇒ match v2 with
    308     [ Vint n2 ⇒
    309        if ltu n2 iwordsize
    310        then Some ? (Vint (shl n1 n2))
     254  [ Vint sz1 n1 ⇒ match v2 with
     255    [ Vint sz2 n2 ⇒
     256       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     257       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
    311258       else None ?
    312259    | _ ⇒ None ? ]
     
    315262definition ev_shr ≝ λv1, v2: val.
    316263  match v1 with
    317   [ Vint n1 ⇒ match v2 with
    318     [ Vint n2 ⇒
    319        if ltu n2 iwordsize
    320        then Some ? (Vint (shr n1 n2))
     264  [ Vint sz1 n1 ⇒ match v2 with
     265    [ Vint sz2 n2 ⇒
     266       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     267       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
    321268       else None ?
    322269    | _ ⇒ None ? ]
    323270  | _ ⇒ None ? ].
    324271
    325 definition ev_shr_carry ≝ λv1, v2: val.
    326   match v1 with
    327   [ Vint n1 ⇒ match v2 with
    328     [ Vint n2 ⇒
    329        if ltu n2 iwordsize
    330        then Some ? (Vint (shr_carry n1 n2))
    331        else None ?
    332     | _ ⇒ None ? ]
    333   | _ ⇒ None ? ].
    334 
    335 definition ev_shrx ≝ λv1, v2: val.
    336   match v1 with
    337   [ Vint n1 ⇒ match v2 with
    338     [ Vint n2 ⇒
    339        if ltu n2 iwordsize
    340        then Some ? (Vint (shrx n1 n2))
    341        else None ?
    342     | _ ⇒ None ? ]
    343   | _ ⇒ None ? ].
    344 
    345272definition ev_shru ≝ λv1, v2: val.
    346273  match v1 with
    347   [ Vint n1 ⇒ match v2 with
    348     [ Vint n2 ⇒
    349        if ltu n2 iwordsize
    350        then Some ? (Vint (shru n1 n2))
    351        else None ?
    352     | _ ⇒ None ? ]
    353   | _ ⇒ None ? ].
    354 
    355 definition ev_rolm ≝
    356 λv: val. λamount, mask: int.
    357   match v with
    358   [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
    359   | _ ⇒ None ?
    360   ].
    361 
    362 definition ev_ror ≝ λv1, v2: val.
    363   match v1 with
    364   [ Vint n1 ⇒ match v2 with
    365     [ Vint n2 ⇒
    366        if ltu n2 iwordsize
    367        then Some ? (Vint (ror n1 n2))
     274  [ Vint sz1 n1 ⇒ match v2 with
     275    [ Vint sz2 n2 ⇒
     276       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     277       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
    368278       else None ?
    369279    | _ ⇒ None ? ]
     
    414324definition ev_cmp ≝ λc: comparison. λv1,v2: val.
    415325  match v1 with
    416   [ Vint n1 ⇒ match v2 with
    417     [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     326  [ Vint sz1 n1 ⇒ match v2 with
     327    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     328                    (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
     329                    (None ?)
    418330    | _ ⇒ None ? ]
    419331  | _ ⇒ None ? ].
     
    438350definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
    439351  match v1 with
    440   [ Vint n1 ⇒ match v2 with
    441     [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
     352  [ Vint sz1 n1 ⇒ match v2 with
     353    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     354                    (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
     355                    (None ?)
    442356    | _ ⇒ None ? ]
    443357  | _ ⇒ None ? ].
     
    475389  | Oaddp ⇒ ev_addp
    476390  | Osubpi ⇒ ev_subpi
    477   | Osubpp ⇒ ev_subpp
     391  | Osubpp sz ⇒ ev_subpp sz
    478392  | Ocmpp c ⇒ ev_cmpp c
    479393  ].
  • src/common/Globalenvs.ma

    r797 r961  
    406406  let r ≝ block_region m b in
    407407  match id with
    408   [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
    409   | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
    410   | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
     408  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
     409  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
     410  | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
    411411  | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
    412412  | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
    419419        | inr _ ⇒ None ?
    420420        ]
  • src/common/IO.ma

    r879 r961  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
     8λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
     
    2525λev,ty.
    2626match ty with
    27 [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     27[ ASTint sz _ ⇒ match ev with
     28  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
     29  | _ ⇒ Error ? (msg IllTypedEvent)]
    2830| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2931| _ ⇒ Error ? (msg IllTypedEvent)
     
    3335λv,ty.
    3436match ty with
    35 [ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     37[ ASTint sz _ ⇒ match v with
     38  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
     39  | _ ⇒ Error ? (msg IllTypedEvent) ]
    3640| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3741| _ ⇒ Error ? (msg IllTypedEvent)
  • src/common/Integers.ma

    r889 r961  
    436436#x #y change with (eq_bv ??? = eq_bv ???)
    437437 @eq_bv_elim @eq_bv_elim /2/
    438 [ #NE #E @False_ind >E in NE * /2/
    439 | #E #NE @False_ind >E in NE * /2/
    440 ] qed.
     438#E >E * #NE @False_ind @NE @refl
     439qed.
    441440
    442441theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
  • src/common/Values.ma

    r891 r961  
    1919include "utilities/Coqlib.ma".
    2020include "common/AST.ma".
    21 include "common/Integers.ma".
    2221include "common/Floats.ma".
    2322include "common/Errors.ma".
     
    2726include "basics/logic.ma".
    2827
    29 include "utilities/binary/Z.ma".
    3028include "utilities/extralib.ma".
    3129
     
    9492
    9593definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    96 definition shift_offset : offset → int → offset ≝
    97   λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    98 definition neg_shift_offset : offset → int → offset ≝
    99   λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    100 definition sub_offset : offset → offset → int ≝
    101   λx,y. bitvector_of_Z ? (offv x - offv y).
     94definition shift_offset : ∀n. offset → BitVector n → offset ≝
     95  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
     96(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
     97definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     98  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
     99definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
     100  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
     101definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     102  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
     103definition sub_offset : ∀n. offset → offset → BitVector n ≝
     104  λn,x,y. bitvector_of_Z ? (offv x - offv y).
    102105definition zero_offset ≝ mk_offset OZ.
    103106definition lt_offset : offset → offset → bool ≝
     
    117120inductive val: Type[0] ≝
    118121  | Vundef: val
    119   | Vint: int → val
     122  | Vint: ∀sz:intsize. bvint sz → val
    120123  | Vfloat: float → val
    121124  | Vnull: region → val
    122125  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
    123126
    124 definition Vzero: val ≝ Vint zero.
    125 definition Vone: val ≝ Vint one.
    126 definition Vmone: val ≝ Vint mone.
    127 
    128 definition Vtrue: val ≝ Vint one.
    129 definition Vfalse: val ≝ Vint zero.
     127definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
     128definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1).
     129definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one).
     130definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?).
     131
     132(* XXX 32bit booleans are Clight specific. *)
     133definition Vtrue: val ≝ Vone I32.
     134definition Vfalse: val ≝ Vzero I32.
    130135
    131136(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
     
    140145λv. match v with
    141146[ Vundef ⇒ True
    142 | Vint _ ⇒ True
     147| Vint _ _ ⇒ True
    143148| Vfloat _ ⇒ False
    144149| Vnull r ⇒ ptr_may_be_single r = true
     
    148153definition may_be_split : val → Prop ≝
    149154λv.match v with
    150 [ Vint _ ⇒ False
     155[ Vint _ _ ⇒ False
    151156| Vnull r ⇒ ptr_may_be_single r = false
    152157| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
     
    248253definition is_true : val → Prop ≝ λv.
    249254  match v with
    250   [ Vint n ⇒ n ≠ zero
     255  [ Vint _ n ⇒ n ≠ (zero ?)
    251256  | Vptr _ b _ ofs ⇒ True
    252257  | _ ⇒ False
     
    255260definition is_false : val → Prop ≝ λv.
    256261  match v with
    257   [ Vint n ⇒ n = zero
     262  [ Vint _ n ⇒ n = (zero ?)
    258263  | Vnull _ ⇒ True
    259264  | _ ⇒ False
     
    262267inductive bool_of_val: val → bool → Prop ≝
    263268  | bool_of_val_int_true:
    264       ∀n. n ≠ zero → bool_of_val (Vint n) true
     269      ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true
    265270  | bool_of_val_int_false:
    266       bool_of_val (Vint zero) false
     271      ∀sz. bool_of_val (Vzero sz) false
    267272  | bool_of_val_ptr:
    268273      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
     
    274279definition eval_bool_of_val : val → res bool ≝
    275280λv. match v with
    276 [ Vint i ⇒ OK ? (notb (eq i zero))
     281[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    277282| Vnull _ ⇒ OK ? false
    278283| Vptr _ _ _ _ ⇒ OK ? true
     
    282287definition neg : val → val ≝ λv.
    283288  match v with
    284   [ Vint n ⇒ Vint (neg n)
     289  [ Vint sz n ⇒ Vint sz (two_complement_negation ? n)
    285290  | _ ⇒ Vundef
    286291  ].
     
    298303  ].
    299304
    300 definition intoffloat : val → val ≝ λv.
    301   match v with
    302   [ Vfloat f ⇒ Vint (intoffloat f)
     305definition intoffloat : intsize → val → val ≝ λsz,v.
     306  match v with
     307  [ Vfloat f ⇒ Vint sz (intoffloat ? f)
    303308  | _ ⇒ Vundef
    304309  ].
    305310
    306 definition intuoffloat : val → val ≝ λv.
    307   match v with
    308   [ Vfloat f ⇒ Vint (intuoffloat f)
     311definition intuoffloat : intsize → val → val ≝ λsz,v.
     312  match v with
     313  [ Vfloat f ⇒ Vint sz (intuoffloat ? f)
    309314  | _ ⇒ Vundef
    310315  ].
     
    312317definition floatofint : val → val ≝ λv.
    313318  match v with
    314   [ Vint n ⇒ Vfloat (floatofint n)
     319  [ Vint sz n ⇒ Vfloat (floatofint ? n)
    315320  | _ ⇒ Vundef
    316321  ].
     
    318323definition floatofintu : val → val ≝ λv.
    319324  match v with
    320   [ Vint n ⇒ Vfloat (floatofintu n)
     325  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
    321326  | _ ⇒ Vundef
    322327  ].
     
    324329definition notint : val → val ≝ λv.
    325330  match v with
    326   [ Vint n ⇒ Vint (xor n mone)
     331  [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?))
    327332  | _ ⇒ Vundef
    328333  ].
    329334 
    330 (* FIXME: switch to alias, or rename, or … *)
    331 definition int_eq : int → int → bool ≝ eq.
    332335definition notbool : val → val ≝ λv.
    333336  match v with
    334   [ Vint n ⇒ of_bool (int_eq n zero)
     337  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    335338  | Vptr _ b _ ofs ⇒ Vfalse
    336339  | Vnull _ ⇒ Vtrue
     
    338341  ].
    339342
    340 definition zero_ext ≝ λnbits: nat. λv: val.
    341   match v with
    342   [ Vint n ⇒ Vint (zero_ext nbits n)
     343definition zero_ext ≝ λrsz: intsize. λv: val.
     344  match v with
     345  [ Vint sz n ⇒ Vint rsz (zero_ext … n)
    343346  | _ ⇒ Vundef
    344347  ].
    345348
    346 definition sign_ext ≝ λnbits:nat. λv:val.
    347   match v with
    348   [ Vint i ⇒ Vint (sign_ext nbits i)
     349definition sign_ext ≝ λrsz:intsize. λv:val.
     350  match v with
     351  [ Vint sz i ⇒ Vint rsz (sign_ext … i)
    349352  | _ ⇒ Vundef
    350353  ].
     
    359362definition add ≝ λv1,v2: val.
    360363  match v1 with
    361   [ Vint n1 ⇒ match v2 with
    362     [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    363     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
     364  [ Vint sz1 n1 ⇒ match v2 with
     365    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     366                    (λn1. Vint sz2 (addition_n ? n1 n2))
     367                    Vundef
     368    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
    364369    | _ ⇒ Vundef ]
    365370  | Vptr r b1 p ofs1 ⇒ match v2 with
    366     [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    367     | _ ⇒ Vundef ]
    368   | _ ⇒ Vundef ].
     371    [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
     372    | _ ⇒ Vundef ]
     373  | _ ⇒ Vundef ].
     374
     375(* XXX Is I32 the best answer for ptr subtraction? *)
    369376
    370377definition sub ≝ λv1,v2: val.
    371378  match v1 with
    372   [ Vint n1 ⇒ match v2 with
    373     [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
     379  [ Vint sz1 n1 ⇒ match v2 with
     380    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     381                    (λn1. Vint sz2 (subtraction ? n1 n2))
     382                    Vundef
    374383    | _ ⇒ Vundef ]
    375384  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    376     [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
     385    [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
    377386    | Vptr r2 b2 p2 ofs2 ⇒
    378         if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    379     | _ ⇒ Vundef ]
    380   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     387        if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
     388    | _ ⇒ Vundef ]
     389  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
    381390  | _ ⇒ Vundef ].
    382391
    383392definition mul ≝ λv1, v2: val.
    384393  match v1 with
    385   [ Vint n1 ⇒ match v2 with
    386     [ Vint n2 ⇒ Vint (mul n1 n2)
     394  [ Vint sz1 n1 ⇒ match v2 with
     395    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     396                    (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
     397                    Vundef
    387398    | _ ⇒ Vundef ]
    388399  | _ ⇒ Vundef ].
     
    418429definition v_and ≝ λv1, v2: val.
    419430  match v1 with
    420   [ Vint n1 ⇒ match v2 with
    421     [ Vint n2 ⇒ Vint (i_and n1 n2)
     431  [ Vint sz1 n1 ⇒ match v2 with
     432    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     433                    (λn1. Vint ? (conjunction_bv ? n1 n2))
     434                    Vundef
    422435    | _ ⇒ Vundef ]
    423436  | _ ⇒ Vundef ].
     
    425438definition or ≝ λv1, v2: val.
    426439  match v1 with
    427   [ Vint n1 ⇒ match v2 with
    428     [ Vint n2 ⇒ Vint (or n1 n2)
     440  [ Vint sz1 n1 ⇒ match v2 with
     441    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     442                    (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2))
     443                    Vundef
    429444    | _ ⇒ Vundef ]
    430445  | _ ⇒ Vundef ].
     
    432447definition xor ≝ λv1, v2: val.
    433448  match v1 with
    434   [ Vint n1 ⇒ match v2 with
    435     [ Vint n2 ⇒ Vint (xor n1 n2)
     449  [ Vint sz1 n1 ⇒ match v2 with
     450    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     451                    (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2))
     452                    Vundef
    436453    | _ ⇒ Vundef ]
    437454  | _ ⇒ Vundef ].
     
    550567  ].
    551568
     569definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     570λn,c,x,y.
     571  match c with
     572  [ Ceq ⇒ eq_bv ? x y
     573  | Cne ⇒ notb (eq_bv ? x y)
     574  | Clt ⇒ lt_s ? x y
     575  | Cle ⇒ notb (lt_s ? y x)
     576  | Cgt ⇒ lt_s ? y x
     577  | Cge ⇒ notb (lt_s ? x y)
     578  ].
     579
     580definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     581λn,c,x,y.
     582  match c with
     583  [ Ceq ⇒ eq_bv ? x y
     584  | Cne ⇒ notb (eq_bv ? x y)
     585  | Clt ⇒ lt_u ? x y
     586  | Cle ⇒ notb (lt_u ? y x)
     587  | Cgt ⇒ lt_u ? y x
     588  | Cge ⇒ notb (lt_u ? x y)
     589  ].
     590
    552591definition cmp ≝ λc: comparison. λv1,v2: val.
    553592  match v1 with
    554   [ Vint n1 ⇒ match v2 with
    555     [ Vint n2 ⇒ of_bool (cmp c n1 n2)
     593  [ Vint sz1 n1 ⇒ match v2 with
     594    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     595                    (λn1. of_bool (cmp_int ? c n1 n2))
     596                    Vundef
    556597    | _ ⇒ Vundef ]
    557598  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    571612definition cmpu ≝ λc: comparison. λv1,v2: val.
    572613  match v1 with
    573   [ Vint n1 ⇒ match v2 with
    574     [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
     614  [ Vint sz1 n1 ⇒ match v2 with
     615    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     616                    (λn1. of_bool (cmpu_int ? c n1 n2))
     617                    Vundef
    575618    | _ ⇒ Vundef ]
    576619  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    588631  | _ ⇒ Vundef ].
    589632
    590 definition cmpf ≝ λc: comparison. λv1,v2: val.
     633definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
    591634  match v1 with
    592635  [ Vfloat f1 ⇒ match v2 with
     
    603646  is performed and [0xFFFFFFFF] is returned.   Type mismatches
    604647  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
     648(* XXX update comment *)
     649(* XXX is this even necessary now?
     650       should we be able to extract bytes? *)
    605651
    606652let rec load_result (chunk: memory_chunk) (v: val) ≝
    607653  match v with
    608   [ Vint n ⇒
     654  [ Vint sz n ⇒
    609655    match chunk with
    610     [ Mint8signed ⇒ Vint (sign_ext 8 n)
    611     | Mint8unsigned ⇒ Vint (zero_ext 8 n)
    612     | Mint16signed ⇒ Vint (sign_ext 16 n)
    613     | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    614     | Mint32 ⇒ Vint n
     656    [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     657    | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     658    | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     659    | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     660    | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
    615661    | _ ⇒ Vundef
    616662    ]
  • src/utilities/extranat.ma

    r744 r961  
    1919    ]
    2020].
     21
     22lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
     23#n elim n
     24[ @refl
     25| #m #IH whd in ⊢ (??%?) > IH @refl
     26] qed.
     27
     28lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
     29#n #m elim n
     30[ //
     31| #n' #IH whd in ⊢ (??%?) > IH @refl
     32] qed.
     33
     34lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
     35#n #m elim m
     36[ //
     37| #m' #IH whd in ⊢ (??%?) > IH @refl
     38] qed.
    2139
    2240lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
Note: See TracChangeset for help on using the changeset viewer.