Changeset 961 for src/common/FrontEndOps.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r774 r961 21 21 22 22 inductive constant : Type[0] ≝ 23  Ointconst: int → constant(**r integer constant *)24  Ofloatconst: float → constant (**r floatingpoint constant *)25  Oaddrsymbol: ident → int → constant(**r address of the symbol plus the offset *)26  Oaddrstack: int → constant.(**r stack pointer plus the given offset *)23  Ointconst: ∀sz. bvint sz → constant (**r integer constant *) 24  Ofloatconst: float → constant (**r floatingpoint constant *) 25  Oaddrsymbol: ident → nat → constant (**r address of the symbol plus the offset *) 26  Oaddrstack: nat → constant. (**r stack pointer plus the given offset *) 27 27 28 28 inductive unary_operation : Type[0] ≝ 29  Ocast8unsigned: unary_operation (**r 8bit zero extension *) 30  Ocast8signed: unary_operation (**r 8bit sign extension *) 31  Ocast16unsigned: unary_operation (**r 16bit zero extension *) 32  Ocast16signed: unary_operation (**r 16bit sign extension *) 29  Ocastint: intsize → signedness → unary_operation (**r 8bit zero extension *) 33 30  Onegint: unary_operation (**r integer opposite *) 34 31  Onotbool: unary_operation (**r boolean negation *) … … 37 34  Oabsf: unary_operation (**r float absolute value *) 38 35  Osingleoffloat: unary_operation (**r float truncation *) 39  Ointoffloat: unary_operation(**r signed integer to float *)40  Ointuoffloat: unary_operation(**r unsigned integer to float *)36  Ointoffloat: intsize → unary_operation (**r signed integer to float *) 37  Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *) 41 38  Ofloatofint: unary_operation (**r float to signed integer *) 42 39  Ofloatofintu: unary_operation (**r float to unsigned integer *) 43 40  Oid: unary_operation (**r identity (used to move between registers *) 44 41  Optrofint: region → unary_operation (**r int to pointer with given representation *) 45  Ointofptr: unary_operation.(**r pointer to int *)42  Ointofptr: intsize → unary_operation. (**r pointer to int *) 46 43 47 44 inductive binary_operation : Type[0] ≝ … … 68 65  Oaddp: binary_operation (**r add an integer to a pointer *) 69 66  Osubpi: binary_operation (**r subtract int from a pointers *) 70  Osubpp: binary_operation(**r subtract two pointers *)67  Osubpp: intsize → binary_operation (**r subtract two pointers *) 71 68  Ocmpp: comparison → binary_operation. (**r compare pointers *) 72 69 … … 80 77 λfind_symbol,sp,cst. 81 78 match cst with 82 [ Ointconst n ⇒ Some ? (Vintn)79 [ Ointconst sz n ⇒ Some ? (Vint sz n) 83 80  Ofloatconst n ⇒ Some ? (Vfloat n) 84 81  Oaddrsymbol s ofs ⇒ 85 82 match find_symbol s with 86 83 [ None ⇒ None ? 87  Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))84  Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs))) 88 85 ] 89 86  Oaddrstack ofs ⇒ 90 Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))87 Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs))) 91 88 ]. cases sp // qed. 92 89 … … 94 91 λop,arg. 95 92 match op with 96 [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg) 97  Ocast8signed ⇒ Some ? (sign_ext 8 arg) 98  Ocast16unsigned ⇒ Some ? (zero_ext 16 arg) 99  Ocast16signed ⇒ Some ? (sign_ext 16 arg) 100  Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1))  _ ⇒ None ? ] 101  Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero)) 93 [ Ocastint sz sg ⇒ 94 match sg with 95 [ Unsigned ⇒ Some ? (zero_ext sz arg) 96  Signed ⇒ Some ? (sign_ext sz arg) 97 ] 98  Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1))  _ ⇒ None ? ] 99  Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?))) 102 100  Vptr _ _ _ _ ⇒ Some ? Vfalse 103 101  Vnull _ ⇒ Some ? Vtrue 104 102  _ ⇒ None ? 105 103 ] 106  Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1))  _ ⇒ None ? ]104  Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?)))  _ ⇒ None ? ] 107 105  Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1))  _ ⇒ None ? ] 108 106  Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1))  _ ⇒ None ? ] 109 107  Osingleoffloat ⇒ Some ? (singleoffloat arg) 110  Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloatf1))  _ ⇒ None ? ]111  Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloatf1))  _ ⇒ None ? ]112  Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintn1))  _ ⇒ None ? ]113  Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintun1))  _ ⇒ None ? ]108  Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1))  _ ⇒ None ? ] 109  Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1))  _ ⇒ None ? ] 110  Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1))  _ ⇒ None ? ] 111  Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1))  _ ⇒ None ? ] 114 112  Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *) 115 113 (* Only conversion of null pointers is specified. *) 116  Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zerothen Some ? (Vnull r) else None ?  _ ⇒ None ? ]117  Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero)  _ ⇒ None ? ]114  Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?  _ ⇒ None ? ] 115  Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?))  _ ⇒ None ? ] 118 116 ]. 119 117 … … 122 120 λc. match c with [ Ceq ⇒ Some ? Vfalse  Cne ⇒ Some ? Vtrue  _ ⇒ None ? ]. 123 121 124 (* Individual operations, adapted from Values. *) 125 126 definition ev_neg : val → option val ≝ λv. 127 match v with 128 [ Vint n ⇒ Some ? (Vint (neg n)) 129  _ ⇒ None ? 130 ]. 131 132 definition ev_negf : val → option val ≝ λv. 133 match v with 134 [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) 135  _ ⇒ None ? 136 ]. 137 138 definition ev_absf : val → option val ≝ λv. 139 match v with 140 [ Vfloat f ⇒ Some ? (Vfloat (Fabs f)) 141  _ ⇒ None ? 142 ]. 143 144 definition ev_intoffloat : val → option val ≝ λv. 145 match v with 146 [ Vfloat f ⇒ Some ? (Vint (intoffloat f)) 147  _ ⇒ None ? 148 ]. 149 150 definition ev_intuoffloat : val → option val ≝ λv. 151 match v with 152 [ Vfloat f ⇒ Some ? (Vint (intuoffloat f)) 153  _ ⇒ None ? 154 ]. 155 156 definition ev_floatofint : val → option val ≝ λv. 157 match v with 158 [ Vint n ⇒ Some ? (Vfloat (floatofint n)) 159  _ ⇒ None ? 160 ]. 161 162 definition ev_floatofintu : val → option val ≝ λv. 163 match v with 164 [ Vint n ⇒ Some ? (Vfloat (floatofintu n)) 165  _ ⇒ None ? 166 ]. 167 168 definition ev_notint : val → option val ≝ λv. 169 match v with 170 [ Vint n ⇒ Some ? (Vint (xor n mone)) 171  _ ⇒ None ? 172 ]. 173 174 definition ev_notbool : val → option val ≝ λv. 175 match v with 176 [ Vint n ⇒ Some ? (of_bool (int_eq n zero)) 177  Vptr _ b _ ofs ⇒ Some ? Vfalse 178  Vnull _ ⇒ Some ? Vtrue 179  _ ⇒ None ? 180 ]. 181 182 definition ev_zero_ext ≝ λnbits: nat. λv: val. 183 match v with 184 [ Vint n ⇒ Some ? (Vint (zero_ext nbits n)) 185  _ ⇒ None ? 186 ]. 187 188 definition ev_sign_ext ≝ λnbits:nat. λv:val. 189 match v with 190 [ Vint i ⇒ Some ? (Vint (sign_ext nbits i)) 191  _ ⇒ None ? 192 ]. 193 194 definition ev_singleoffloat : val → option val ≝ λv. 195 match v with 196 [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f)) 197  _ ⇒ None ? 198 ]. 122 (* Individual operations, adapted from Values. These differ in that they 123 implement the plain Cminor/RTLabs operations (e.g., with separate addition 124 for ints,floats and pointers) and use option rather than Vundef. The ones 125 in Value are probably not needed. *) 199 126 200 127 definition ev_add ≝ λv1,v2: val. 201 128 match v1 with 202 [ Vint n1 ⇒ match v2 with 203 [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2)) 129 [ Vint sz1 n1 ⇒ match v2 with 130 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 131 (λn1. Some ? (Vint ? (addition_n ? n1 n2))) 132 (None ?) 204 133  _ ⇒ None ? ] 205 134  _ ⇒ None ? ]. … … 207 136 definition ev_sub ≝ λv1,v2: val. 208 137 match v1 with 209 [ Vint n1 ⇒ match v2 with 210 [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) 138 [ Vint sz1 n1 ⇒ match v2 with 139 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 140 (λn1. Some ? (Vint ? (subtraction ? n1 n2))) 141 (None ?) 211 142  _ ⇒ None ? ] 212 143  _ ⇒ None ? ]. … … 216 147 match v1 with 217 148 [ Vptr r b1 p ofs1 ⇒ match v2 with 218 [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offsetofs1 n2))149 [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2)) 219 150  _ ⇒ None ? ] 220 151  Vnull r ⇒ match v2 with 221 [ Vint n2 ⇒ if eq n2 zerothen Some ? (Vnull r) else None ?152 [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? 222 153  _ ⇒ None ? 223 154 ] … … 227 158 match v1 with 228 159 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 229 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offsetofs1 n2))230  _ ⇒ None ? ] 231  Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zerothen Some ? (Vnull r) else None ?  _ ⇒ None ? ]232  _ ⇒ None ? ]. 233 234 definition ev_subpp ≝ λ v1,v2: val.160 [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)) 161  _ ⇒ None ? ] 162  Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?  _ ⇒ None ? ] 163  _ ⇒ None ? ]. 164 165 definition ev_subpp ≝ λsz. λv1,v2: val. 235 166 match v1 with 236 167 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 237 168 [ Vptr r2 b2 p2 ofs2 ⇒ 238 if eq_block b1 b2 then Some ? (Vint (sub_offsetofs1 ofs2)) else None ?239  _ ⇒ None ? ] 240  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero)  _ ⇒ None ? ]169 if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ? 170  _ ⇒ None ? ] 171  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?))  _ ⇒ None ? ] 241 172  _ ⇒ None ? ]. 242 173 243 174 definition ev_mul ≝ λv1, v2: val. 244 175 match v1 with 245 [ Vint n1 ⇒ match v2 with 246 [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) 176 [ Vint sz1 n1 ⇒ match v2 with 177 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 178 (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2))))) 179 (None ?) 247 180  _ ⇒ None ? ] 248 181  _ ⇒ None ? ]. … … 250 183 definition ev_divs ≝ λv1, v2: val. 251 184 match v1 with 252 [ Vint n1 ⇒ match v2 with 253 [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2) 185 [ Vint sz1 n1 ⇒ match v2 with 186 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 187 (λn1. option_map ?? (Vint ?) (division_s ? n1 n2)) 188 (None ?) 254 189  _ ⇒ None ? ] 255 190  _ ⇒ None ? ]. … … 257 192 definition ev_mods ≝ λv1, v2: val. 258 193 match v1 with 259 [ Vint n1 ⇒ match v2 with 260 [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2) 194 [ Vint sz1 n1 ⇒ match v2 with 195 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 196 (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2)) 197 (None ?) 261 198  _ ⇒ None ? 262 199 ] … … 266 203 definition ev_divu ≝ λv1, v2: val. 267 204 match v1 with 268 [ Vint n1 ⇒ match v2 with 269 [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2) 205 [ Vint sz1 n1 ⇒ match v2 with 206 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 207 (λn1. option_map ?? (Vint ?) (division_u ? n1 n2)) 208 (None ?) 270 209  _ ⇒ None ? 271 210 ] … … 275 214 definition ev_modu ≝ λv1, v2: val. 276 215 match v1 with 277 [ Vint n1 ⇒ match v2 with 278 [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2) 216 [ Vint sz1 n1 ⇒ match v2 with 217 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 218 (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2)) 219 (None ?) 279 220  _ ⇒ None ? 280 221 ] … … 284 225 definition ev_and ≝ λv1, v2: val. 285 226 match v1 with 286 [ Vint n1 ⇒ match v2 with 287 [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2)) 227 [ Vint sz1 n1 ⇒ match v2 with 228 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 229 (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) 230 (None ?) 288 231  _ ⇒ None ? ] 289 232  _ ⇒ None ? ]. … … 291 234 definition ev_or ≝ λv1, v2: val. 292 235 match v1 with 293 [ Vint n1 ⇒ match v2 with 294 [ Vint n2 ⇒ Some ? (Vint (or n1 n2)) 236 [ Vint sz1 n1 ⇒ match v2 with 237 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 238 (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) 239 (None ?) 295 240  _ ⇒ None ? ] 296 241  _ ⇒ None ? ]. … … 298 243 definition ev_xor ≝ λv1, v2: val. 299 244 match v1 with 300 [ Vint n1 ⇒ match v2 with 301 [ Vint n2 ⇒ Some ? (Vint (xor n1 n2)) 245 [ Vint sz1 n1 ⇒ match v2 with 246 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 247 (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) 248 (None ?) 302 249  _ ⇒ None ? ] 303 250  _ ⇒ None ? ]. … … 305 252 definition ev_shl ≝ λv1, v2: val. 306 253 match v1 with 307 [ Vint n1 ⇒ match v2 with308 [ Vint n2 ⇒309 if lt u n2 iwordsize310 then Some ? (Vint (shl n1 n2))254 [ Vint sz1 n1 ⇒ match v2 with 255 [ Vint sz2 n2 ⇒ 256 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 257 then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false)) 311 258 else None ? 312 259  _ ⇒ None ? ] … … 315 262 definition ev_shr ≝ λv1, v2: val. 316 263 match v1 with 317 [ Vint n1 ⇒ match v2 with318 [ Vint n2 ⇒319 if lt u n2 iwordsize320 then Some ? (Vint (shr n1 n2))264 [ Vint sz1 n1 ⇒ match v2 with 265 [ Vint sz2 n2 ⇒ 266 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 267 then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1))) 321 268 else None ? 322 269  _ ⇒ None ? ] 323 270  _ ⇒ None ? ]. 324 271 325 definition ev_shr_carry ≝ λv1, v2: val.326 match v1 with327 [ Vint n1 ⇒ match v2 with328 [ Vint n2 ⇒329 if ltu n2 iwordsize330 then Some ? (Vint (shr_carry n1 n2))331 else None ?332  _ ⇒ None ? ]333  _ ⇒ None ? ].334 335 definition ev_shrx ≝ λv1, v2: val.336 match v1 with337 [ Vint n1 ⇒ match v2 with338 [ Vint n2 ⇒339 if ltu n2 iwordsize340 then Some ? (Vint (shrx n1 n2))341 else None ?342  _ ⇒ None ? ]343  _ ⇒ None ? ].344 345 272 definition ev_shru ≝ λv1, v2: val. 346 273 match v1 with 347 [ Vint n1 ⇒ match v2 with 348 [ Vint n2 ⇒ 349 if ltu n2 iwordsize 350 then Some ? (Vint (shru n1 n2)) 351 else None ? 352  _ ⇒ None ? ] 353  _ ⇒ None ? ]. 354 355 definition ev_rolm ≝ 356 λv: val. λamount, mask: int. 357 match v with 358 [ Vint n ⇒ Some ? (Vint (rolm n amount mask)) 359  _ ⇒ None ? 360 ]. 361 362 definition ev_ror ≝ λv1, v2: val. 363 match v1 with 364 [ Vint n1 ⇒ match v2 with 365 [ Vint n2 ⇒ 366 if ltu n2 iwordsize 367 then Some ? (Vint (ror n1 n2)) 274 [ Vint sz1 n1 ⇒ match v2 with 275 [ Vint sz2 n2 ⇒ 276 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 277 then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false)) 368 278 else None ? 369 279  _ ⇒ None ? ] … … 414 324 definition ev_cmp ≝ λc: comparison. λv1,v2: val. 415 325 match v1 with 416 [ Vint n1 ⇒ match v2 with 417 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 326 [ Vint sz1 n1 ⇒ match v2 with 327 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 328 (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) 329 (None ?) 418 330  _ ⇒ None ? ] 419 331  _ ⇒ None ? ]. … … 438 350 definition ev_cmpu ≝ λc: comparison. λv1,v2: val. 439 351 match v1 with 440 [ Vint n1 ⇒ match v2 with 441 [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2)) 352 [ Vint sz1 n1 ⇒ match v2 with 353 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 354 (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) 355 (None ?) 442 356  _ ⇒ None ? ] 443 357  _ ⇒ None ? ]. … … 475 389  Oaddp ⇒ ev_addp 476 390  Osubpi ⇒ ev_subpi 477  Osubpp ⇒ ev_subpp391  Osubpp sz ⇒ ev_subpp sz 478 392  Ocmpp c ⇒ ev_cmpp c 479 393 ].
Note: See TracChangeset
for help on using the changeset viewer.