Changeset 961 for src/Clight/Cexec.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r891 r961 48 48 definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝ 49 49 λ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)) 52 53 | _ ⇒ Error ? (msg TypeMismatch) 53 54 ] … … 69 70 lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b. 70 71 #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) // 72 73 | #r #b #pc #i #i0 #s %{ true} % // 73 74 | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //; 74 | #i #s %{ false} % //;75 | * #sg %{ false} % // 75 76 | #r #r' #t %{ false} % //; 76 77 | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //; … … 106 107 axiom BadCast : String. (* TODO: refine into more precise errors? *) 107 108 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 zerowith109 definition 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. 111 match eq_bv ? i (zero ?) with 111 112 [ true ⇒ 112 113 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) 120 123 | _ ⇒ Error ? (msg BadCast) 121 124 ] … … 126 129 λm:mem. λv:val. λty:type. λty':type. 127 130 match v with 128 [ Vint i ⇒131 [ Vint sz i ⇒ 129 132 match ty with 130 133 [ 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 142 148 | _ ⇒ Error ? (msg TypeMismatch) 143 149 ] … … 146 152 [ Tfloat sz ⇒ 147 153 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)) 149 155 | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f)) 150 156 | _ ⇒ Error ? (msg BadCast) … … 189 195 [ Expr e' ty ⇒ 190 196 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 ] 192 204 | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 193 205 | Evar _ ⇒ … … 215 227 | _ ⇒ Error ? (msg BadlyTypedTerm) 216 228 ] 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 ] 218 234 | Eunop op a ⇒ 219 235 do 〈v1,tr〉 ← exec_expr ge en m a; … … 275 291 do 〈lofs,tr〉 ← exec_lvalue ge en m a; 276 292 do delta ← field_offset i fList; 277 OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (reprdelta)〉,tr〉293 OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉 278 294 | Tunion id fList ⇒ 279 295 do 〈lofs,tr〉 ← exec_lvalue ge en m a; … … 478 494 | Sswitch a sl ⇒ 479 495 ! 〈v,tr〉 ← exec_expr ge e m a; 480 match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switchn 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〉 481 497 | _ ⇒ Wrong ??? (msg TypeMismatch)] 482 498 | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉 … … 530 546 [ Kstop ⇒ 531 547 match res with 532 [ Vint r ⇒ Some ? r548 [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?) 533 549 | _ ⇒ None ? 534 550 ] … … 544 560 | #v #k #m cases k; 545 561 [ 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 ] 547 565 | 1: %2 ; % *; #r #H inversion H; #i #m #e destruct; 548 566 | #f %2 ; % *; #r #H inversion H; #i #m #e destruct;
Note: See TracChangeset
for help on using the changeset viewer.