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.

File:
1 edited

Legend:

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