Changeset 961 for src/Clight/Cexec.ma


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.

File:
1 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;
Note: See TracChangeset for help on using the changeset viewer.