Changeset 484 for Deliverables/D3.1/Csemantics/Values.ma
 Timestamp:
 Jan 28, 2011, 2:41:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Values.ma
r483 r484 33 33 memory regions such a pointer could address), a memory address and 34 34 an integer offset with respect to this address; 35  a null pointer: the region denotes the representation (i.e., pointer size) 35 36  the [Vundef] value denoting an arbitrary bit pattern, such as the 36 37 value of an uninitialized variable. … … 41 42  Vint: int → val 42 43  Vfloat: float → val 44  Vnull: region → val 43 45  Vptr: region → block → int → val. 44 46 … … 58 60 *) 59 61 ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse. 60 62 (* 61 63 ndefinition has_type ≝ λv: val. λt: typ. 62 64 match v with … … 74 76 has_type v1 t1 ∧ has_type_list vs ts ] 75 77 ]. 76 78 *) 77 79 (* * Truth values. Pointers and nonzero integers are treated as [True]. 78 80 The integer 0 (also used to represent the null pointer) is [False]. … … 89 91 match v with 90 92 [ Vint n ⇒ n = zero 93  Vnull _ ⇒ True 91 94  _ ⇒ False 92 95 ]. … … 98 101 bool_of_val (Vint zero) false 99 102  bool_of_val_ptr: 100 ∀pty,b,ofs. bool_of_val (Vptr pty b ofs) true. 103 ∀r,b,ofs. bool_of_val (Vptr r b ofs) true 104  bool_of_val_null: 105 ∀r. bool_of_val (Vnull r) true. 101 106 102 107 ndefinition neg : val → val ≝ λv. … … 154 159 [ Vint n ⇒ of_bool (int_eq n zero) 155 160  Vptr _ b ofs ⇒ Vfalse 161  Vnull _ ⇒ Vtrue 156 162  _ ⇒ Vundef 157 163 ]. … … 175 181 ]. 176 182 183 (* TODO: add zero to null? *) 177 184 ndefinition add ≝ λv1,v2: val. 178 185 match v1 with … … 196 203 if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef 197 204  _ ⇒ Vundef ] 205  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero  _ ⇒ Vundef ] 198 206  _ ⇒ Vundef ]. 199 207 … … 342 350  _ ⇒ Vundef ]. 343 351 352 ndefinition cmp_match : comparison → val ≝ λc. 353 match c with 354 [ Ceq ⇒ Vtrue 355  Cne ⇒ Vfalse 356  _ ⇒ Vundef 357 ]. 358 344 359 ndefinition cmp_mismatch : comparison → val ≝ λc. 345 360 match c with … … 349 364 ]. 350 365 366 (* TODO: consider whether to check pointer representations *) 351 367 ndefinition cmp ≝ λc: comparison. λv1,v2: val. 352 368 match v1 with 353 369 [ Vint n1 ⇒ match v2 with 354 370 [ Vint n2 ⇒ of_bool (cmp c n1 n2) 355  Vptr pty2 b2 ofs2 ⇒ 356 if eq n1 zero then cmp_mismatch c else Vundef 357  _ ⇒ Vundef ] 358  Vptr pty1 b1 ofs1 ⇒ match v2 with 359 [ Vptr pty2 b2 ofs2 ⇒ 371  _ ⇒ Vundef ] 372  Vptr r1 b1 ofs1 ⇒ match v2 with 373 [ Vptr r2 b2 ofs2 ⇒ 360 374 if eqZb b1 b2 361 375 then of_bool (cmp c ofs1 ofs2) 362 376 else cmp_mismatch c 363  Vint n2 ⇒ 364 if eq n2 zero then cmp_mismatch c else Vundef 365  _ ⇒ Vundef ] 377  Vnull r2 ⇒ cmp_mismatch c 378  _ ⇒ Vundef ] 379  Vnull r1 ⇒ match v2 with 380 [ Vptr _ _ _ ⇒ cmp_mismatch c 381  Vnull r2 ⇒ cmp_match c 382  _ ⇒ Vundef 383 ] 366 384  _ ⇒ Vundef ]. 367 385 … … 370 388 [ Vint n1 ⇒ match v2 with 371 389 [ Vint n2 ⇒ of_bool (cmpu c n1 n2) 372  Vptr pty2 b2 ofs2 ⇒ 373 if eq n1 zero then cmp_mismatch c else Vundef 374  _ ⇒ Vundef ] 375  Vptr pty1 b1 ofs1 ⇒ match v2 with 376 [ Vptr pty2 b2 ofs2 ⇒ 390  _ ⇒ Vundef ] 391  Vptr r1 b1 ofs1 ⇒ match v2 with 392 [ Vptr r2 b2 ofs2 ⇒ 377 393 if eqZb b1 b2 378 394 then of_bool (cmpu c ofs1 ofs2) 379 395 else cmp_mismatch c 380  Vint n2 ⇒ 381 if eq n2 zero then cmp_mismatch c else Vundef 382  _ ⇒ Vundef ] 396  Vnull r2 ⇒ cmp_mismatch c 397  _ ⇒ Vundef ] 398  Vnull r1 ⇒ match v2 with 399 [ Vptr _ _ _ ⇒ cmp_mismatch c 400  Vnull r2 ⇒ cmp_match c 401  _ ⇒ Vundef 402 ] 383 403  _ ⇒ Vundef ]. 384 404 … … 408 428  Mint16unsigned ⇒ Vint (zero_ext 16 n) 409 429  Mint32 ⇒ Vint n 410  Mpointer r ⇒ if eq n zero then Vint zero else Vundef411 430  _ ⇒ Vundef 412 431 ] … … 414 433 match chunk with 415 434 [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef 435  _ ⇒ Vundef 436 ] 437  Vnull r ⇒ 438 match chunk with 439 [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef 416 440  _ ⇒ Vundef 417 441 ]
Note: See TracChangeset
for help on using the changeset viewer.