Changeset 961 for src/Clight


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

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

Location:
src/Clight
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • 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        | _ ⇒
Note: See TracChangeset for help on using the changeset viewer.