[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 | |
---|
[702] | 20 | include "common/Values.ma". |
---|
[639] | 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 *) |
---|
[727] | 42 | | Ofloatofintu: unary_operation (**r float to unsigned integer *) |
---|
| 43 | | Oid: unary_operation (**r identity (used to move between registers *) |
---|
| 44 | | Optrofint: region → unary_operation (**r int to pointer with given representation *) |
---|
| 45 | | Ointofptr: unary_operation. (**r pointer to int *) |
---|
[639] | 46 | |
---|
| 47 | inductive binary_operation : Type[0] ≝ |
---|
| 48 | | Oadd: binary_operation (**r integer addition *) |
---|
| 49 | | Osub: binary_operation (**r integer subtraction *) |
---|
| 50 | | Omul: binary_operation (**r integer multiplication *) |
---|
| 51 | | Odiv: binary_operation (**r integer signed division *) |
---|
| 52 | | Odivu: binary_operation (**r integer unsigned division *) |
---|
| 53 | | Omod: binary_operation (**r integer signed modulus *) |
---|
| 54 | | Omodu: binary_operation (**r integer unsigned modulus *) |
---|
| 55 | | Oand: binary_operation (**r bitwise ``and'' *) |
---|
| 56 | | Oor: binary_operation (**r bitwise ``or'' *) |
---|
| 57 | | Oxor: binary_operation (**r bitwise ``xor'' *) |
---|
| 58 | | Oshl: binary_operation (**r left shift *) |
---|
| 59 | | Oshr: binary_operation (**r right signed shift *) |
---|
| 60 | | Oshru: binary_operation (**r right unsigned shift *) |
---|
| 61 | | Oaddf: binary_operation (**r float addition *) |
---|
| 62 | | Osubf: binary_operation (**r float subtraction *) |
---|
| 63 | | Omulf: binary_operation (**r float multiplication *) |
---|
| 64 | | Odivf: binary_operation (**r float division *) |
---|
| 65 | | Ocmp: comparison -> binary_operation (**r integer signed comparison *) |
---|
| 66 | | Ocmpu: comparison -> binary_operation (**r integer unsigned comparison *) |
---|
[727] | 67 | | Ocmpf: comparison -> binary_operation (**r float comparison *) |
---|
| 68 | | Oaddp: binary_operation (**r add an integer to a pointer *) |
---|
[774] | 69 | | Osubpi: binary_operation (**r subtract int from a pointers *) |
---|
| 70 | | Osubpp: binary_operation (**r subtract two pointers *) |
---|
[727] | 71 | | Ocmpp: comparison → binary_operation. (**r compare pointers *) |
---|
[639] | 72 | |
---|
| 73 | |
---|
| 74 | (* * Evaluation of constants and operator applications. |
---|
| 75 | [None] is returned when the computation is undefined, e.g. |
---|
| 76 | if arguments are of the wrong types, or in case of an integer division |
---|
| 77 | by zero. *) |
---|
| 78 | |
---|
| 79 | definition eval_constant : (ident → option block) → block → constant → option val ≝ |
---|
| 80 | λfind_symbol,sp,cst. |
---|
| 81 | match cst with |
---|
| 82 | [ Ointconst n ⇒ Some ? (Vint n) |
---|
| 83 | | Ofloatconst n ⇒ Some ? (Vfloat n) |
---|
| 84 | | Oaddrsymbol s ofs ⇒ |
---|
| 85 | match find_symbol s with |
---|
| 86 | [ 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)) |
---|
| 88 | ] |
---|
| 89 | | Oaddrstack ofs ⇒ |
---|
| 90 | Some ? (Vptr Any sp ? (shift_offset zero_offset ofs)) |
---|
| 91 | ]. cases sp // qed. |
---|
| 92 | |
---|
| 93 | definition eval_unop : unary_operation → val → option val ≝ |
---|
| 94 | λop,arg. |
---|
| 95 | 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)) |
---|
| 102 | | Vptr _ _ _ _ ⇒ Some ? Vfalse |
---|
| 103 | | Vnull _ ⇒ Some ? Vtrue |
---|
| 104 | | _ ⇒ None ? |
---|
| 105 | ] |
---|
| 106 | | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ] |
---|
| 107 | | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ] |
---|
| 108 | | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ] |
---|
| 109 | | Osingleoffloat ⇒ Some ? (singleoffloat arg) |
---|
| 110 | | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ] |
---|
| 111 | | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ] |
---|
| 112 | | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ] |
---|
| 113 | | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ] |
---|
[727] | 114 | | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *) |
---|
| 115 | (* Only conversion of null pointers is specified. *) |
---|
| 116 | | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ] |
---|
| 117 | | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ] |
---|
[639] | 118 | ]. |
---|
| 119 | |
---|
| 120 | (* I think this is duplicated somewhere else *) |
---|
| 121 | definition eval_compare_mismatch : comparison → option val ≝ |
---|
| 122 | λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ]. |
---|
| 123 | |
---|
| 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 | |
---|
[744] | 182 | definition ev_zero_ext ≝ λnbits: nat. λv: val. |
---|
[639] | 183 | match v with |
---|
| 184 | [ Vint n ⇒ Some ? (Vint (zero_ext nbits n)) |
---|
| 185 | | _ ⇒ None ? |
---|
| 186 | ]. |
---|
| 187 | |
---|
[744] | 188 | definition ev_sign_ext ≝ λnbits:nat. λv:val. |
---|
[639] | 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 | ]. |
---|
| 199 | |
---|
| 200 | definition ev_add ≝ λv1,v2: val. |
---|
| 201 | match v1 with |
---|
| 202 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 203 | [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2)) |
---|
[639] | 204 | | _ ⇒ None ? ] |
---|
| 205 | | _ ⇒ None ? ]. |
---|
| 206 | |
---|
| 207 | definition ev_sub ≝ λv1,v2: val. |
---|
| 208 | match v1 with |
---|
| 209 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 210 | [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) |
---|
[639] | 211 | | _ ⇒ None ? ] |
---|
[774] | 212 | | _ ⇒ None ? ]. |
---|
| 213 | |
---|
| 214 | (* NB: requires arguments to be presented pointer first. *) |
---|
| 215 | definition ev_addp ≝ λv1,v2: val. |
---|
| 216 | match v1 with |
---|
| 217 | [ Vptr r b1 p ofs1 ⇒ match v2 with |
---|
| 218 | [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2)) |
---|
| 219 | | _ ⇒ None ? ] |
---|
| 220 | | Vnull r ⇒ match v2 with |
---|
| 221 | [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? |
---|
| 222 | | _ ⇒ None ? |
---|
| 223 | ] |
---|
| 224 | | _ ⇒ None ? ]. |
---|
| 225 | |
---|
| 226 | definition ev_subpi ≝ λv1,v2: val. |
---|
| 227 | match v1 with |
---|
| 228 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
[639] | 229 | [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)) |
---|
[774] | 230 | | _ ⇒ None ? ] |
---|
| 231 | | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ] |
---|
| 232 | | _ ⇒ None ? ]. |
---|
| 233 | |
---|
| 234 | definition ev_subpp ≝ λv1,v2: val. |
---|
| 235 | match v1 with |
---|
| 236 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
| 237 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
[639] | 238 | if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ? |
---|
| 239 | | _ ⇒ None ? ] |
---|
| 240 | | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ] |
---|
| 241 | | _ ⇒ None ? ]. |
---|
| 242 | |
---|
| 243 | definition ev_mul ≝ λv1, v2: val. |
---|
| 244 | match v1 with |
---|
| 245 | [ Vint n1 ⇒ match v2 with |
---|
| 246 | [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) |
---|
| 247 | | _ ⇒ None ? ] |
---|
| 248 | | _ ⇒ None ? ]. |
---|
| 249 | |
---|
| 250 | definition ev_divs ≝ λv1, v2: val. |
---|
| 251 | match v1 with |
---|
| 252 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 253 | [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2) |
---|
[639] | 254 | | _ ⇒ None ? ] |
---|
| 255 | | _ ⇒ None ? ]. |
---|
| 256 | |
---|
| 257 | definition ev_mods ≝ λv1, v2: val. |
---|
| 258 | match v1 with |
---|
| 259 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 260 | [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2) |
---|
[639] | 261 | | _ ⇒ None ? |
---|
| 262 | ] |
---|
| 263 | | _ ⇒ None ? |
---|
| 264 | ]. |
---|
| 265 | |
---|
| 266 | definition ev_divu ≝ λv1, v2: val. |
---|
| 267 | match v1 with |
---|
| 268 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 269 | [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2) |
---|
[639] | 270 | | _ ⇒ None ? |
---|
| 271 | ] |
---|
| 272 | | _ ⇒ None ? |
---|
| 273 | ]. |
---|
| 274 | |
---|
| 275 | definition ev_modu ≝ λv1, v2: val. |
---|
| 276 | match v1 with |
---|
| 277 | [ Vint n1 ⇒ match v2 with |
---|
[744] | 278 | [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2) |
---|
[639] | 279 | | _ ⇒ None ? |
---|
| 280 | ] |
---|
| 281 | | _ ⇒ None ? |
---|
| 282 | ]. |
---|
| 283 | |
---|
| 284 | definition ev_and ≝ λv1, v2: val. |
---|
| 285 | match v1 with |
---|
| 286 | [ Vint n1 ⇒ match v2 with |
---|
| 287 | [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2)) |
---|
| 288 | | _ ⇒ None ? ] |
---|
| 289 | | _ ⇒ None ? ]. |
---|
| 290 | |
---|
| 291 | definition ev_or ≝ λv1, v2: val. |
---|
| 292 | match v1 with |
---|
| 293 | [ Vint n1 ⇒ match v2 with |
---|
| 294 | [ Vint n2 ⇒ Some ? (Vint (or n1 n2)) |
---|
| 295 | | _ ⇒ None ? ] |
---|
| 296 | | _ ⇒ None ? ]. |
---|
| 297 | |
---|
| 298 | definition ev_xor ≝ λv1, v2: val. |
---|
| 299 | match v1 with |
---|
| 300 | [ Vint n1 ⇒ match v2 with |
---|
| 301 | [ Vint n2 ⇒ Some ? (Vint (xor n1 n2)) |
---|
| 302 | | _ ⇒ None ? ] |
---|
| 303 | | _ ⇒ None ? ]. |
---|
| 304 | |
---|
| 305 | definition ev_shl ≝ λv1, v2: val. |
---|
| 306 | match v1 with |
---|
| 307 | [ Vint n1 ⇒ match v2 with |
---|
| 308 | [ Vint n2 ⇒ |
---|
| 309 | if ltu n2 iwordsize |
---|
| 310 | then Some ? (Vint (shl n1 n2)) |
---|
| 311 | else None ? |
---|
| 312 | | _ ⇒ None ? ] |
---|
| 313 | | _ ⇒ None ? ]. |
---|
| 314 | |
---|
| 315 | definition ev_shr ≝ λv1, v2: val. |
---|
| 316 | match v1 with |
---|
| 317 | [ Vint n1 ⇒ match v2 with |
---|
| 318 | [ Vint n2 ⇒ |
---|
| 319 | if ltu n2 iwordsize |
---|
| 320 | then Some ? (Vint (shr n1 n2)) |
---|
| 321 | else None ? |
---|
| 322 | | _ ⇒ None ? ] |
---|
| 323 | | _ ⇒ None ? ]. |
---|
| 324 | |
---|
| 325 | definition ev_shr_carry ≝ λv1, v2: val. |
---|
| 326 | match v1 with |
---|
| 327 | [ Vint n1 ⇒ match v2 with |
---|
| 328 | [ Vint n2 ⇒ |
---|
| 329 | if ltu n2 iwordsize |
---|
| 330 | 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 with |
---|
| 337 | [ Vint n1 ⇒ match v2 with |
---|
| 338 | [ Vint n2 ⇒ |
---|
| 339 | if ltu n2 iwordsize |
---|
| 340 | then Some ? (Vint (shrx n1 n2)) |
---|
| 341 | else None ? |
---|
| 342 | | _ ⇒ None ? ] |
---|
| 343 | | _ ⇒ None ? ]. |
---|
| 344 | |
---|
| 345 | definition ev_shru ≝ λv1, v2: val. |
---|
| 346 | 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)) |
---|
| 368 | else None ? |
---|
| 369 | | _ ⇒ None ? ] |
---|
| 370 | | _ ⇒ None ? ]. |
---|
| 371 | |
---|
| 372 | definition ev_addf ≝ λv1,v2: val. |
---|
| 373 | match v1 with |
---|
| 374 | [ Vfloat f1 ⇒ match v2 with |
---|
| 375 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2)) |
---|
| 376 | | _ ⇒ None ? ] |
---|
| 377 | | _ ⇒ None ? ]. |
---|
| 378 | |
---|
| 379 | definition ev_subf ≝ λv1,v2: val. |
---|
| 380 | match v1 with |
---|
| 381 | [ Vfloat f1 ⇒ match v2 with |
---|
| 382 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) |
---|
| 383 | | _ ⇒ None ? ] |
---|
| 384 | | _ ⇒ None ? ]. |
---|
| 385 | |
---|
| 386 | definition ev_mulf ≝ λv1,v2: val. |
---|
| 387 | match v1 with |
---|
| 388 | [ Vfloat f1 ⇒ match v2 with |
---|
| 389 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) |
---|
| 390 | | _ ⇒ None ? ] |
---|
| 391 | | _ ⇒ None ? ]. |
---|
| 392 | |
---|
| 393 | definition ev_divf ≝ λv1,v2: val. |
---|
| 394 | match v1 with |
---|
| 395 | [ Vfloat f1 ⇒ match v2 with |
---|
| 396 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2)) |
---|
| 397 | | _ ⇒ None ? ] |
---|
| 398 | | _ ⇒ None ? ]. |
---|
| 399 | |
---|
| 400 | definition ev_cmp_match : comparison → option val ≝ λc. |
---|
| 401 | match c with |
---|
| 402 | [ Ceq ⇒ Some ? Vtrue |
---|
| 403 | | Cne ⇒ Some ? Vfalse |
---|
| 404 | | _ ⇒ None ? |
---|
| 405 | ]. |
---|
| 406 | |
---|
| 407 | definition ev_cmp_mismatch : comparison → option val ≝ λc. |
---|
| 408 | match c with |
---|
| 409 | [ Ceq ⇒ Some ? Vfalse |
---|
| 410 | | Cne ⇒ Some ? Vtrue |
---|
| 411 | | _ ⇒ None ? |
---|
| 412 | ]. |
---|
| 413 | |
---|
| 414 | definition ev_cmp ≝ λc: comparison. λv1,v2: val. |
---|
| 415 | match v1 with |
---|
| 416 | [ Vint n1 ⇒ match v2 with |
---|
| 417 | [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) |
---|
| 418 | | _ ⇒ None ? ] |
---|
[774] | 419 | | _ ⇒ None ? ]. |
---|
| 420 | |
---|
| 421 | definition ev_cmpp ≝ λc: comparison. λv1,v2: val. |
---|
| 422 | match v1 with |
---|
| 423 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
[639] | 424 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
| 425 | if eq_block b1 b2 |
---|
| 426 | then Some ? (of_bool (cmp_offset c ofs1 ofs2)) |
---|
| 427 | else ev_cmp_mismatch c |
---|
| 428 | | Vnull r2 ⇒ ev_cmp_mismatch c |
---|
| 429 | | _ ⇒ None ? ] |
---|
| 430 | | Vnull r1 ⇒ match v2 with |
---|
| 431 | [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c |
---|
| 432 | | Vnull r2 ⇒ ev_cmp_match c |
---|
| 433 | | _ ⇒ None ? |
---|
| 434 | ] |
---|
| 435 | | _ ⇒ None ? ]. |
---|
| 436 | |
---|
| 437 | (* TODO: check this, it isn't the cmpu used elsewhere *) |
---|
| 438 | definition ev_cmpu ≝ λc: comparison. λv1,v2: val. |
---|
| 439 | match v1 with |
---|
| 440 | [ Vint n1 ⇒ match v2 with |
---|
| 441 | [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2)) |
---|
| 442 | | _ ⇒ None ? ] |
---|
| 443 | | _ ⇒ None ? ]. |
---|
| 444 | |
---|
| 445 | definition ev_cmpf ≝ λc: comparison. λv1,v2: val. |
---|
| 446 | match v1 with |
---|
| 447 | [ Vfloat f1 ⇒ match v2 with |
---|
| 448 | [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) |
---|
| 449 | | _ ⇒ None ? ] |
---|
| 450 | | _ ⇒ None ? ]. |
---|
| 451 | |
---|
| 452 | definition eval_binop : binary_operation → val → val → option val ≝ |
---|
| 453 | λop. |
---|
| 454 | match op with |
---|
| 455 | [ Oadd ⇒ ev_add |
---|
| 456 | | Osub ⇒ ev_sub |
---|
| 457 | | Omul ⇒ ev_mul |
---|
| 458 | | Odiv ⇒ ev_divs |
---|
| 459 | | Odivu ⇒ ev_divu |
---|
| 460 | | Omod ⇒ ev_mods |
---|
| 461 | | Omodu ⇒ ev_modu |
---|
| 462 | | Oand ⇒ ev_and |
---|
| 463 | | Oor ⇒ ev_or |
---|
| 464 | | Oxor ⇒ ev_xor |
---|
| 465 | | Oshl ⇒ ev_shl |
---|
| 466 | | Oshr ⇒ ev_shr |
---|
| 467 | | Oshru ⇒ ev_shru |
---|
| 468 | | Oaddf ⇒ ev_addf |
---|
| 469 | | Osubf ⇒ ev_subf |
---|
| 470 | | Omulf ⇒ ev_mulf |
---|
| 471 | | Odivf ⇒ ev_divf |
---|
| 472 | | Ocmp c ⇒ ev_cmp c |
---|
| 473 | | Ocmpu c ⇒ ev_cmpu c |
---|
| 474 | | Ocmpf c ⇒ ev_cmpf c |
---|
[774] | 475 | | Oaddp ⇒ ev_addp |
---|
| 476 | | Osubpi ⇒ ev_subpi |
---|
| 477 | | Osubpp ⇒ ev_subpp |
---|
| 478 | | Ocmpp c ⇒ ev_cmpp c |
---|
[639] | 479 | ]. |
---|
| 480 | |
---|