[639] | 1 | (* Operations common to the Cminor and RTLabs front end stages. *) |
---|
| 2 | |
---|
| 3 | (* Adapted from CompCert's Cminor.ma: *) |
---|
| 4 | |
---|
| 5 | (* *********************************************************************) |
---|
| 6 | (* *) |
---|
| 7 | (* The Compcert verified compiler *) |
---|
| 8 | (* *) |
---|
| 9 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
| 10 | (* *) |
---|
| 11 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
| 12 | (* Automatique. All rights reserved. This file is distributed *) |
---|
| 13 | (* under the terms of the GNU General Public License as published by *) |
---|
| 14 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
| 15 | (* (at your option) any later version. This file is also distributed *) |
---|
| 16 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
| 17 | (* *) |
---|
| 18 | (* *********************************************************************) |
---|
| 19 | |
---|
| 20 | include "Values.ma". |
---|
| 21 | |
---|
| 22 | inductive constant : Type[0] ≝ |
---|
| 23 | | Ointconst: int → constant (**r integer constant *) |
---|
| 24 | | Ofloatconst: float → constant (**r floating-point 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 *) |
---|
| 27 | |
---|
| 28 | inductive unary_operation : Type[0] ≝ |
---|
| 29 | | Ocast8unsigned: unary_operation (**r 8-bit zero extension *) |
---|
| 30 | | Ocast8signed: unary_operation (**r 8-bit sign extension *) |
---|
| 31 | | Ocast16unsigned: unary_operation (**r 16-bit zero extension *) |
---|
| 32 | | Ocast16signed: unary_operation (**r 16-bit sign extension *) |
---|
| 33 | | Onegint: unary_operation (**r integer opposite *) |
---|
| 34 | | Onotbool: unary_operation (**r boolean negation *) |
---|
| 35 | | Onotint: unary_operation (**r bitwise complement *) |
---|
| 36 | | Onegf: unary_operation (**r float opposite *) |
---|
| 37 | | Oabsf: unary_operation (**r float absolute value *) |
---|
| 38 | | Osingleoffloat: unary_operation (**r float truncation *) |
---|
| 39 | | Ointoffloat: unary_operation (**r signed integer to float *) |
---|
| 40 | | Ointuoffloat: unary_operation (**r unsigned integer to float *) |
---|
| 41 | | Ofloatofint: unary_operation (**r float to signed integer *) |
---|
| 42 | | Ofloatofintu: unary_operation. (**r float to unsigned integer *) |
---|
| 43 | |
---|
| 44 | inductive binary_operation : Type[0] ≝ |
---|
| 45 | | Oadd: binary_operation (**r integer addition *) |
---|
| 46 | | Osub: binary_operation (**r integer subtraction *) |
---|
| 47 | | Omul: binary_operation (**r integer multiplication *) |
---|
| 48 | | Odiv: binary_operation (**r integer signed division *) |
---|
| 49 | | Odivu: binary_operation (**r integer unsigned division *) |
---|
| 50 | | Omod: binary_operation (**r integer signed modulus *) |
---|
| 51 | | Omodu: binary_operation (**r integer unsigned modulus *) |
---|
| 52 | | Oand: binary_operation (**r bitwise ``and'' *) |
---|
| 53 | | Oor: binary_operation (**r bitwise ``or'' *) |
---|
| 54 | | Oxor: binary_operation (**r bitwise ``xor'' *) |
---|
| 55 | | Oshl: binary_operation (**r left shift *) |
---|
| 56 | | Oshr: binary_operation (**r right signed shift *) |
---|
| 57 | | Oshru: binary_operation (**r right unsigned shift *) |
---|
| 58 | | Oaddf: binary_operation (**r float addition *) |
---|
| 59 | | Osubf: binary_operation (**r float subtraction *) |
---|
| 60 | | Omulf: binary_operation (**r float multiplication *) |
---|
| 61 | | Odivf: binary_operation (**r float division *) |
---|
| 62 | | Ocmp: comparison -> binary_operation (**r integer signed comparison *) |
---|
| 63 | | Ocmpu: comparison -> binary_operation (**r integer unsigned comparison *) |
---|
| 64 | | Ocmpf: comparison -> binary_operation. (**r float comparison *) |
---|
| 65 | |
---|
| 66 | |
---|
| 67 | (* * Evaluation of constants and operator applications. |
---|
| 68 | [None] is returned when the computation is undefined, e.g. |
---|
| 69 | if arguments are of the wrong types, or in case of an integer division |
---|
| 70 | by zero. *) |
---|
| 71 | |
---|
| 72 | definition eval_constant : (ident → option block) → block → constant → option val ≝ |
---|
| 73 | λfind_symbol,sp,cst. |
---|
| 74 | match cst with |
---|
| 75 | [ Ointconst n ⇒ Some ? (Vint n) |
---|
| 76 | | Ofloatconst n ⇒ Some ? (Vfloat n) |
---|
| 77 | | Oaddrsymbol s ofs ⇒ |
---|
| 78 | match find_symbol s with |
---|
| 79 | [ None ⇒ None ? |
---|
| 80 | | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs)) |
---|
| 81 | ] |
---|
| 82 | | Oaddrstack ofs ⇒ |
---|
| 83 | Some ? (Vptr Any sp ? (shift_offset zero_offset ofs)) |
---|
| 84 | ]. cases sp // qed. |
---|
| 85 | |
---|
| 86 | definition eval_unop : unary_operation → val → option val ≝ |
---|
| 87 | λop,arg. |
---|
| 88 | match op with |
---|
| 89 | [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg) |
---|
| 90 | | Ocast8signed ⇒ Some ? (sign_ext 8 arg) |
---|
| 91 | | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg) |
---|
| 92 | | Ocast16signed ⇒ Some ? (sign_ext 16 arg) |
---|
| 93 | | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ] |
---|
| 94 | | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero)) |
---|
| 95 | | Vptr _ _ _ _ ⇒ Some ? Vfalse |
---|
| 96 | | Vnull _ ⇒ Some ? Vtrue |
---|
| 97 | | _ ⇒ None ? |
---|
| 98 | ] |
---|
| 99 | | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ] |
---|
| 100 | | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ] |
---|
| 101 | | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ] |
---|
| 102 | | Osingleoffloat ⇒ Some ? (singleoffloat arg) |
---|
| 103 | | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ] |
---|
| 104 | | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ] |
---|
| 105 | | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ] |
---|
| 106 | | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ] |
---|
| 107 | ]. |
---|
| 108 | |
---|
| 109 | (* I think this is duplicated somewhere else *) |
---|
| 110 | definition eval_compare_mismatch : comparison → option val ≝ |
---|
| 111 | λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ]. |
---|
| 112 | |
---|
| 113 | (* Individual operations, adapted from Values. *) |
---|
| 114 | |
---|
| 115 | definition ev_neg : val → option val ≝ λv. |
---|
| 116 | match v with |
---|
| 117 | [ Vint n ⇒ Some ? (Vint (neg n)) |
---|
| 118 | | _ ⇒ None ? |
---|
| 119 | ]. |
---|
| 120 | |
---|
| 121 | definition ev_negf : val → option val ≝ λv. |
---|
| 122 | match v with |
---|
| 123 | [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) |
---|
| 124 | | _ ⇒ None ? |
---|
| 125 | ]. |
---|
| 126 | |
---|
| 127 | definition ev_absf : val → option val ≝ λv. |
---|
| 128 | match v with |
---|
| 129 | [ Vfloat f ⇒ Some ? (Vfloat (Fabs f)) |
---|
| 130 | | _ ⇒ None ? |
---|
| 131 | ]. |
---|
| 132 | |
---|
| 133 | definition ev_intoffloat : val → option val ≝ λv. |
---|
| 134 | match v with |
---|
| 135 | [ Vfloat f ⇒ Some ? (Vint (intoffloat f)) |
---|
| 136 | | _ ⇒ None ? |
---|
| 137 | ]. |
---|
| 138 | |
---|
| 139 | definition ev_intuoffloat : val → option val ≝ λv. |
---|
| 140 | match v with |
---|
| 141 | [ Vfloat f ⇒ Some ? (Vint (intuoffloat f)) |
---|
| 142 | | _ ⇒ None ? |
---|
| 143 | ]. |
---|
| 144 | |
---|
| 145 | definition ev_floatofint : val → option val ≝ λv. |
---|
| 146 | match v with |
---|
| 147 | [ Vint n ⇒ Some ? (Vfloat (floatofint n)) |
---|
| 148 | | _ ⇒ None ? |
---|
| 149 | ]. |
---|
| 150 | |
---|
| 151 | definition ev_floatofintu : val → option val ≝ λv. |
---|
| 152 | match v with |
---|
| 153 | [ Vint n ⇒ Some ? (Vfloat (floatofintu n)) |
---|
| 154 | | _ ⇒ None ? |
---|
| 155 | ]. |
---|
| 156 | |
---|
| 157 | definition ev_notint : val → option val ≝ λv. |
---|
| 158 | match v with |
---|
| 159 | [ Vint n ⇒ Some ? (Vint (xor n mone)) |
---|
| 160 | | _ ⇒ None ? |
---|
| 161 | ]. |
---|
| 162 | |
---|
| 163 | (* FIXME: switch to alias, or rename, or … *) |
---|
| 164 | definition int_eq : int → int → bool ≝ eq. |
---|
| 165 | definition ev_notbool : val → option val ≝ λv. |
---|
| 166 | match v with |
---|
| 167 | [ Vint n ⇒ Some ? (of_bool (int_eq n zero)) |
---|
| 168 | | Vptr _ b _ ofs ⇒ Some ? Vfalse |
---|
| 169 | | Vnull _ ⇒ Some ? Vtrue |
---|
| 170 | | _ ⇒ None ? |
---|
| 171 | ]. |
---|
| 172 | |
---|
| 173 | definition ev_zero_ext ≝ λnbits: Z. λv: val. |
---|
| 174 | match v with |
---|
| 175 | [ Vint n ⇒ Some ? (Vint (zero_ext nbits n)) |
---|
| 176 | | _ ⇒ None ? |
---|
| 177 | ]. |
---|
| 178 | |
---|
| 179 | definition ev_sign_ext ≝ λnbits:Z. λv:val. |
---|
| 180 | match v with |
---|
| 181 | [ Vint i ⇒ Some ? (Vint (sign_ext nbits i)) |
---|
| 182 | | _ ⇒ None ? |
---|
| 183 | ]. |
---|
| 184 | |
---|
| 185 | definition ev_singleoffloat : val → option val ≝ λv. |
---|
| 186 | match v with |
---|
| 187 | [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f)) |
---|
| 188 | | _ ⇒ None ? |
---|
| 189 | ]. |
---|
| 190 | |
---|
| 191 | (* TODO: add zero to null? *) |
---|
| 192 | definition ev_add ≝ λv1,v2: val. |
---|
| 193 | match v1 with |
---|
| 194 | [ Vint n1 ⇒ match v2 with |
---|
| 195 | [ Vint n2 ⇒ Some ? (Vint (add n1 n2)) |
---|
| 196 | | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1)) |
---|
| 197 | | _ ⇒ None ? ] |
---|
| 198 | | Vptr r b1 p ofs1 ⇒ match v2 with |
---|
| 199 | [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2)) |
---|
| 200 | | _ ⇒ None ? ] |
---|
| 201 | | _ ⇒ None ? ]. |
---|
| 202 | |
---|
| 203 | definition ev_sub ≝ λv1,v2: val. |
---|
| 204 | match v1 with |
---|
| 205 | [ Vint n1 ⇒ match v2 with |
---|
| 206 | [ Vint n2 ⇒ Some ? (Vint (sub n1 n2)) |
---|
| 207 | | _ ⇒ None ? ] |
---|
| 208 | | Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
| 209 | [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)) |
---|
| 210 | | Vptr r2 b2 p2 ofs2 ⇒ |
---|
| 211 | if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ? |
---|
| 212 | | _ ⇒ None ? ] |
---|
| 213 | | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ] |
---|
| 214 | | _ ⇒ None ? ]. |
---|
| 215 | |
---|
| 216 | definition ev_mul ≝ λv1, v2: val. |
---|
| 217 | match v1 with |
---|
| 218 | [ Vint n1 ⇒ match v2 with |
---|
| 219 | [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) |
---|
| 220 | | _ ⇒ None ? ] |
---|
| 221 | | _ ⇒ None ? ]. |
---|
| 222 | |
---|
| 223 | definition ev_divs ≝ λv1, v2: val. |
---|
| 224 | match v1 with |
---|
| 225 | [ Vint n1 ⇒ match v2 with |
---|
| 226 | [ Vint n2 ⇒ Some ? (Vint (divs n1 n2)) |
---|
| 227 | | _ ⇒ None ? ] |
---|
| 228 | | _ ⇒ None ? ]. |
---|
| 229 | |
---|
| 230 | definition ev_mods ≝ λv1, v2: val. |
---|
| 231 | match v1 with |
---|
| 232 | [ Vint n1 ⇒ match v2 with |
---|
| 233 | [ Vint n2 ⇒ |
---|
| 234 | if eq n2 zero then None ? else Some ? (Vint (mods n1 n2)) |
---|
| 235 | | _ ⇒ None ? |
---|
| 236 | ] |
---|
| 237 | | _ ⇒ None ? |
---|
| 238 | ]. |
---|
| 239 | |
---|
| 240 | definition ev_divu ≝ λv1, v2: val. |
---|
| 241 | match v1 with |
---|
| 242 | [ Vint n1 ⇒ match v2 with |
---|
| 243 | [ Vint n2 ⇒ |
---|
| 244 | if eq n2 zero then None ? else Some ? (Vint (divu n1 n2)) |
---|
| 245 | | _ ⇒ None ? |
---|
| 246 | ] |
---|
| 247 | | _ ⇒ None ? |
---|
| 248 | ]. |
---|
| 249 | |
---|
| 250 | definition ev_modu ≝ λv1, v2: val. |
---|
| 251 | match v1 with |
---|
| 252 | [ Vint n1 ⇒ match v2 with |
---|
| 253 | [ Vint n2 ⇒ |
---|
| 254 | if eq n2 zero then None ? else Some ? (Vint (modu n1 n2)) |
---|
| 255 | | _ ⇒ None ? |
---|
| 256 | ] |
---|
| 257 | | _ ⇒ None ? |
---|
| 258 | ]. |
---|
| 259 | |
---|
| 260 | definition ev_and ≝ λv1, v2: val. |
---|
| 261 | match v1 with |
---|
| 262 | [ Vint n1 ⇒ match v2 with |
---|
| 263 | [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2)) |
---|
| 264 | | _ ⇒ None ? ] |
---|
| 265 | | _ ⇒ None ? ]. |
---|
| 266 | |
---|
| 267 | definition ev_or ≝ λv1, v2: val. |
---|
| 268 | match v1 with |
---|
| 269 | [ Vint n1 ⇒ match v2 with |
---|
| 270 | [ Vint n2 ⇒ Some ? (Vint (or n1 n2)) |
---|
| 271 | | _ ⇒ None ? ] |
---|
| 272 | | _ ⇒ None ? ]. |
---|
| 273 | |
---|
| 274 | definition ev_xor ≝ λv1, v2: val. |
---|
| 275 | match v1 with |
---|
| 276 | [ Vint n1 ⇒ match v2 with |
---|
| 277 | [ Vint n2 ⇒ Some ? (Vint (xor n1 n2)) |
---|
| 278 | | _ ⇒ None ? ] |
---|
| 279 | | _ ⇒ None ? ]. |
---|
| 280 | |
---|
| 281 | definition ev_shl ≝ λv1, v2: val. |
---|
| 282 | match v1 with |
---|
| 283 | [ Vint n1 ⇒ match v2 with |
---|
| 284 | [ Vint n2 ⇒ |
---|
| 285 | if ltu n2 iwordsize |
---|
| 286 | then Some ? (Vint (shl n1 n2)) |
---|
| 287 | else None ? |
---|
| 288 | | _ ⇒ None ? ] |
---|
| 289 | | _ ⇒ None ? ]. |
---|
| 290 | |
---|
| 291 | definition ev_shr ≝ λv1, v2: val. |
---|
| 292 | match v1 with |
---|
| 293 | [ Vint n1 ⇒ match v2 with |
---|
| 294 | [ Vint n2 ⇒ |
---|
| 295 | if ltu n2 iwordsize |
---|
| 296 | then Some ? (Vint (shr n1 n2)) |
---|
| 297 | else None ? |
---|
| 298 | | _ ⇒ None ? ] |
---|
| 299 | | _ ⇒ None ? ]. |
---|
| 300 | |
---|
| 301 | definition ev_shr_carry ≝ λv1, v2: val. |
---|
| 302 | match v1 with |
---|
| 303 | [ Vint n1 ⇒ match v2 with |
---|
| 304 | [ Vint n2 ⇒ |
---|
| 305 | if ltu n2 iwordsize |
---|
| 306 | then Some ? (Vint (shr_carry n1 n2)) |
---|
| 307 | else None ? |
---|
| 308 | | _ ⇒ None ? ] |
---|
| 309 | | _ ⇒ None ? ]. |
---|
| 310 | |
---|
| 311 | definition ev_shrx ≝ λv1, v2: val. |
---|
| 312 | match v1 with |
---|
| 313 | [ Vint n1 ⇒ match v2 with |
---|
| 314 | [ Vint n2 ⇒ |
---|
| 315 | if ltu n2 iwordsize |
---|
| 316 | then Some ? (Vint (shrx n1 n2)) |
---|
| 317 | else None ? |
---|
| 318 | | _ ⇒ None ? ] |
---|
| 319 | | _ ⇒ None ? ]. |
---|
| 320 | |
---|
| 321 | definition ev_shru ≝ λv1, v2: val. |
---|
| 322 | match v1 with |
---|
| 323 | [ Vint n1 ⇒ match v2 with |
---|
| 324 | [ Vint n2 ⇒ |
---|
| 325 | if ltu n2 iwordsize |
---|
| 326 | then Some ? (Vint (shru n1 n2)) |
---|
| 327 | else None ? |
---|
| 328 | | _ ⇒ None ? ] |
---|
| 329 | | _ ⇒ None ? ]. |
---|
| 330 | |
---|
| 331 | definition ev_rolm ≝ |
---|
| 332 | λv: val. λamount, mask: int. |
---|
| 333 | match v with |
---|
| 334 | [ Vint n ⇒ Some ? (Vint (rolm n amount mask)) |
---|
| 335 | | _ ⇒ None ? |
---|
| 336 | ]. |
---|
| 337 | |
---|
| 338 | definition ev_ror ≝ λv1, v2: val. |
---|
| 339 | match v1 with |
---|
| 340 | [ Vint n1 ⇒ match v2 with |
---|
| 341 | [ Vint n2 ⇒ |
---|
| 342 | if ltu n2 iwordsize |
---|
| 343 | then Some ? (Vint (ror n1 n2)) |
---|
| 344 | else None ? |
---|
| 345 | | _ ⇒ None ? ] |
---|
| 346 | | _ ⇒ None ? ]. |
---|
| 347 | |
---|
| 348 | definition ev_addf ≝ λv1,v2: val. |
---|
| 349 | match v1 with |
---|
| 350 | [ Vfloat f1 ⇒ match v2 with |
---|
| 351 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2)) |
---|
| 352 | | _ ⇒ None ? ] |
---|
| 353 | | _ ⇒ None ? ]. |
---|
| 354 | |
---|
| 355 | definition ev_subf ≝ λv1,v2: val. |
---|
| 356 | match v1 with |
---|
| 357 | [ Vfloat f1 ⇒ match v2 with |
---|
| 358 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) |
---|
| 359 | | _ ⇒ None ? ] |
---|
| 360 | | _ ⇒ None ? ]. |
---|
| 361 | |
---|
| 362 | definition ev_mulf ≝ λv1,v2: val. |
---|
| 363 | match v1 with |
---|
| 364 | [ Vfloat f1 ⇒ match v2 with |
---|
| 365 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) |
---|
| 366 | | _ ⇒ None ? ] |
---|
| 367 | | _ ⇒ None ? ]. |
---|
| 368 | |
---|
| 369 | definition ev_divf ≝ λv1,v2: val. |
---|
| 370 | match v1 with |
---|
| 371 | [ Vfloat f1 ⇒ match v2 with |
---|
| 372 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2)) |
---|
| 373 | | _ ⇒ None ? ] |
---|
| 374 | | _ ⇒ None ? ]. |
---|
| 375 | |
---|
| 376 | definition ev_cmp_match : comparison → option val ≝ λc. |
---|
| 377 | match c with |
---|
| 378 | [ Ceq ⇒ Some ? Vtrue |
---|
| 379 | | Cne ⇒ Some ? Vfalse |
---|
| 380 | | _ ⇒ None ? |
---|
| 381 | ]. |
---|
| 382 | |
---|
| 383 | definition ev_cmp_mismatch : comparison → option val ≝ λc. |
---|
| 384 | match c with |
---|
| 385 | [ Ceq ⇒ Some ? Vfalse |
---|
| 386 | | Cne ⇒ Some ? Vtrue |
---|
| 387 | | _ ⇒ None ? |
---|
| 388 | ]. |
---|
| 389 | |
---|
| 390 | definition ev_cmp ≝ λc: comparison. λv1,v2: val. |
---|
| 391 | match v1 with |
---|
| 392 | [ Vint n1 ⇒ match v2 with |
---|
| 393 | [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) |
---|
| 394 | | _ ⇒ None ? ] |
---|
| 395 | | Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
| 396 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
| 397 | if eq_block b1 b2 |
---|
| 398 | then Some ? (of_bool (cmp_offset c ofs1 ofs2)) |
---|
| 399 | else ev_cmp_mismatch c |
---|
| 400 | | Vnull r2 ⇒ ev_cmp_mismatch c |
---|
| 401 | | _ ⇒ None ? ] |
---|
| 402 | | Vnull r1 ⇒ match v2 with |
---|
| 403 | [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c |
---|
| 404 | | Vnull r2 ⇒ ev_cmp_match c |
---|
| 405 | | _ ⇒ None ? |
---|
| 406 | ] |
---|
| 407 | | _ ⇒ None ? ]. |
---|
| 408 | |
---|
| 409 | (* TODO: check this, it isn't the cmpu used elsewhere *) |
---|
| 410 | definition ev_cmpu ≝ λc: comparison. λv1,v2: val. |
---|
| 411 | match v1 with |
---|
| 412 | [ Vint n1 ⇒ match v2 with |
---|
| 413 | [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2)) |
---|
| 414 | | _ ⇒ None ? ] |
---|
| 415 | | _ ⇒ None ? ]. |
---|
| 416 | |
---|
| 417 | definition ev_cmpf ≝ λc: comparison. λv1,v2: val. |
---|
| 418 | match v1 with |
---|
| 419 | [ Vfloat f1 ⇒ match v2 with |
---|
| 420 | [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) |
---|
| 421 | | _ ⇒ None ? ] |
---|
| 422 | | _ ⇒ None ? ]. |
---|
| 423 | |
---|
| 424 | definition eval_binop : binary_operation → val → val → option val ≝ |
---|
| 425 | λop. |
---|
| 426 | match op with |
---|
| 427 | [ Oadd ⇒ ev_add |
---|
| 428 | | Osub ⇒ ev_sub |
---|
| 429 | | Omul ⇒ ev_mul |
---|
| 430 | | Odiv ⇒ ev_divs |
---|
| 431 | | Odivu ⇒ ev_divu |
---|
| 432 | | Omod ⇒ ev_mods |
---|
| 433 | | Omodu ⇒ ev_modu |
---|
| 434 | | Oand ⇒ ev_and |
---|
| 435 | | Oor ⇒ ev_or |
---|
| 436 | | Oxor ⇒ ev_xor |
---|
| 437 | | Oshl ⇒ ev_shl |
---|
| 438 | | Oshr ⇒ ev_shr |
---|
| 439 | | Oshru ⇒ ev_shru |
---|
| 440 | | Oaddf ⇒ ev_addf |
---|
| 441 | | Osubf ⇒ ev_subf |
---|
| 442 | | Omulf ⇒ ev_mulf |
---|
| 443 | | Odivf ⇒ ev_divf |
---|
| 444 | | Ocmp c ⇒ ev_cmp c |
---|
| 445 | | Ocmpu c ⇒ ev_cmpu c |
---|
| 446 | | Ocmpf c ⇒ ev_cmpf c |
---|
| 447 | ]. |
---|
| 448 | |
---|