Changeset 484 for Deliverables/D3.1
 Timestamp:
 Jan 28, 2011, 2:41:49 PM (9 years ago)
 Location:
 Deliverables/D3.1/Csemantics
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Cexec.ma
r481 r484 45 45 [ Vint i ⇒ match ty with 46 46 [ Tint _ _ ⇒ OK ? (¬eq i zero) 47  Tpointer _ _ ⇒ OK ? (¬eq i zero)48 47  _ ⇒ Error ? 49 48 ] … … 53 52 ] 54 53  Vptr _ _ _ ⇒ match ty with 55 [ Tint _ _ ⇒ OK ? true 56  Tpointer _ _ ⇒ OK ? true 54 [ Tpointer _ _ ⇒ OK ? true 55  _ ⇒ Error ? 56 ] 57  Vnull _ ⇒ match ty with 58 [ Tpointer _ _ ⇒ OK ? false 57 59  _ ⇒ Error ? 58 60 ] … … 64 66 ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; 65 67 ## #p b i i0 s; @ true; @; // 66 ## #i p t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;67 ## #p b i p0 t0; @ true; @; //68 68 ## #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //; 69 69 ## #i s; @ false; @; //; 70 ## # pt; @ false; @; //;70 ## #r r' t; @ false; @; //; 71 71 ## #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //; 72 72 ##] … … 131 131 [ Tint _ _ ⇒ 132 132 match ty' with 133 [ Tpointer _ _ ⇒ OK ? (Vint i) 134  Tarray _ _ _ ⇒ OK ? (Vint i) 135  Tfunction _ _ ⇒ OK ? (Vint i) 136  _ ⇒ Error ? 137 ] 138  Tpointer _ _ ⇒ 139 match ty' with 140 [ Tpointer _ _ ⇒ OK ? (Vint i) 141  Tarray _ _ _ ⇒ OK ? (Vint i) 142  Tfunction _ _ ⇒ OK ? (Vint i) 143  _ ⇒ Error ? 144 ] 145  Tarray _ _ _ ⇒ 146 match ty' with 147 [ Tpointer _ _ ⇒ OK ? (Vint i) 148  Tarray _ _ _ ⇒ OK ? (Vint i) 149  Tfunction _ _ ⇒ OK ? (Vint i) 150  _ ⇒ Error ? 151 ] 152  Tfunction _ _ ⇒ 153 match ty' with 154 [ Tpointer _ _ ⇒ OK ? (Vint i) 155  Tarray _ _ _ ⇒ OK ? (Vint i) 156  Tfunction _ _ ⇒ OK ? (Vint i) 133 [ Tpointer r _ ⇒ OK ? (Vnull r) 134  Tarray r _ _ ⇒ OK ? (Vnull r) 135  Tfunction _ _ ⇒ OK ? (Vnull Code) 157 136  _ ⇒ Error ? 158 137 ] … … 161 140  false ⇒ Error ? 162 141 ]. 163 164 ndefinition ms_eq_dec : ∀s1,s2:region. (s1 = s2) + (s1 ≠ s2).165 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.166 142 167 143 ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝ … … 196 172  Vptr p b ofs ⇒ 197 173 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ]; 198 do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something  inr _ ⇒ Error ? ];174 do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? something  inr _ ⇒ Error ? ]; 199 175 do s' ← match ty' with 200 176 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code … … 203 179 then OK ? (Vptr s' b ofs) 204 180 else Error ? 181  Vnull r ⇒ 182 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ]; 183 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? something  inr _ ⇒ Error ? ]; 184 do s' ← match ty' with 185 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code 186  _ ⇒ Error ? ]; 187 OK ? (Vnull s') 205 188  _ ⇒ Error ? 206 189 ]. … … 390 373  _ ⇒ inr ?? (nmk ? (λH.?)) ] 391 374  Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t') with [ Tpointer s' t' ⇒ 392 match ms_eq_dec s s' with [ inl e1 ⇒375 match eq_region_dec s s' with [ inl e1 ⇒ 393 376 match type_eq_dec t t' with [ inl e2 ⇒ inl ??? 394 377  inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ] 395 378  inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ]  _ ⇒ inr ?? (nmk ? (λH.?)) ] 396 379  Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t') with [ Tarray s' t' n' ⇒ 397 match ms_eq_dec s s' with [ inl e1 ⇒380 match eq_region_dec s s' with [ inl e1 ⇒ 398 381 match type_eq_dec t t' with [ inl e2 ⇒ 399 382 match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ??? … … 423 406  _ ⇒ inr ?? (nmk ? (λH.?)) ] 424 407  Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t') with [ Tcomp_ptr r' i' ⇒ 425 match ms_eq_dec r r' with [ inl e1 ⇒408 match eq_region_dec r r' with [ inl e1 ⇒ 426 409 match ident_eq i i' with [ inl e2 ⇒ inl ??? 427 410  inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] … … 700 683 let m0 ≝ init_mem Genv ?? p in 701 684 do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p)); 702 do u ← opt_to_res ? (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something  inr _ ⇒ None ? ]);685 do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something  inr _ ⇒ None ? ]); 703 686 do f ← opt_to_res ? (find_funct_ptr ? ? ge b); 704 687 OK ? (Callstate f (nil ?) Kstop m0). … … 713 696 ## ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct; 714 697 ## #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 715 ## #pcl b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 698 ## #r; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 699 ## #r b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 716 700 ##] 717 701 ## #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct; … … 794 778 ## #fd args k mem 795 779 ## #v k mem; (* for final state check *) ncases k; 796 ##[ ncases v; ##[ ##2,3: #v' ## ##4: # sp loc off ##]780 ##[ ncases v; ##[ ##2,3: #v' ## ##4: #r ## ##5: #sp loc off ##] 797 781 ## #s' k' ## ##3,4: #e s' k' ## ##5,6: #e s' s'' k' ## #k' ## #a b c d ##] 798 782 ##] 
Deliverables/D3.1/Csemantics/CexecComplete.ma
r481 r484 49 49 ##] nqed. 50 50 51 nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.51 nlemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???. 52 52 ##[ #s; ncases s; napply refl; 53 53 ## ##skip … … 100 100 nelim H1; ##[ #sp1 ty1 ## #sp1 ty1 n1 ## #tys1 ty1; nletin sp1 ≝ Code ##] 101 101 nwhd in ⊢ (??%?); 102 ##[ ##1,2: nrewrite > ( ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]102 ##[ ##1,2: nrewrite > (eq_region_dec_true …); nwhd in ⊢ (??%?); ##] 103 103 nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ## ##2,5,8: #sp2 ty2 n2 ## ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##] 104 104 #H3; nwhd in ⊢ (??%?); 105 105 nrewrite > (is_pointer_compat_true …); //; 106 ## #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ## #sp1 ty1 n1 ## #args rty ##] napply refl; 107 ## #m t t' H H'; ncases H; ncases H'; //; 106 ## #m sz si ty'' r H; ncases H; //; 107 ## #m t t' r r' H H'; ncases H; ntry #a; ntry #b; ntry #c; ncases H'; ntry #d; ntry #e; ntry #f; 108 nwhd in ⊢ (??%?); ntry napply refl; nrewrite > eq_region_dec_true; napply refl; 108 109 ##] nqed. 109 110 … … 125 126 ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; 126 127 ## #p b i i0 s; @ true; @; // 127 ## #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;128 ## #p b i p0 t0; @ true; @; //129 128 ## #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; 130 129 ## #i s; @ false; @; //; 131 ## # pt; @ false; @; //;130 ## #r r' t; @ false; @; //; 132 131 ## #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; 133 132 ##] … … 138 137 ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //; 139 138 ## #p b i i0 s; // 140 ## #i p t ne; nwhd; nrewrite > (eq_false … ne); //;141 ## #p b i p0 t0; //142 139 ## #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //; 143 140 ##] … … 147 144 #v ty H; nelim H; 148 145 ##[ #i s; //; 149 ## # pt; //;146 ## #r r' t; //; 150 147 ## #s; nwhd; nrewrite > (Feq_zero_true …); //; 151 148 ##] 
Deliverables/D3.1/Csemantics/CexecSound.ma
r481 r484 4 4 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). 5 5 #v ty r; 6 ncases v; ##[ ##2: #i ## ##3: #f ## ##4: #sp b of ##] 7 nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##] 8 ncases ty; ##[ ##2,11,20: #sz sg ## ##3,12,21: #sz ## ##4,13,22: #sp ty ## ##5,14,23: #sp ty n ## ##6,15,24: #args rty ## ##7,8,16,17,25,26: #id fs ## ##9,18,27: #r id ##] 6 ncases v; ##[ ## #i ## #f ## #r1 ## #r b of ##] 7 ncases ty; ##[ ##2,11,20,29,38: #sz sg ## ##3,12,21,30,39: #sz ## ##4,13,22,31,40: #r ty ## ##5,14,23,32,41: #r ty n ## ##6,15,24,33,42: #args rty ## ##7,8,16,17,25,26,34,35,43,44: #id fs ## ##9,18,27,36,45: #r id ##] 9 8 #H; nwhd in H:(??%?); ndestruct; 10 ##[ ##1,4:nlapply (eq_spec i zero); nelim (eq i zero);11 ##[ # #1,3: #e; nrewrite > e; napply bool_of_val_false; //;12 ## # #2,4: #ne; napply bool_of_val_true; /2/;13 ##] 14 ## ##3:nelim (eq_dec f Fzero);9 ##[ nlapply (eq_spec i zero); nelim (eq i zero); 10 ##[ #e; nrewrite > e; napply bool_of_val_false; //; 11 ## #ne; napply bool_of_val_true; /2/; 12 ##] 13 ## nelim (eq_dec f Fzero); 15 14 ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //; 16 15 ## #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/; 17 16 ##] 18 ## ##2,5: napply bool_of_val_true; // 17 ## napply bool_of_val_false; // 18 ## napply bool_of_val_true; // 19 19 ##] nqed. 20 20 … … 36 36 ##[ #e; nrewrite > e; 37 37 ncases ty; ##[ ## #sz sg ## #fs ## #sp ty ## #sp ty n ## #args rty ## #id fs ## #id fs ## #r id ##] 38 nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##] 39 ncases ty'; ##[ ##2,11,20,29: #sz' sg' ## ##3,12,21,30: #sz' ## ##4,13,22,31: #sp' ty' ## ##5,14,23,32: #sp' ty' n' ## ##6,15,24,33: #args' res' ## ##7,8,16,17,25,26,34,35: #id' fs' ## ##9,18,27,36: #r id' ##] 40 nwhd in ⊢ (??%? → ?); #H; ndestruct (H); 41 ##[ ##1,5,9: napply cast_ip_z ## ##*: napply cast_pp_z ##] //; 38 nwhd in ⊢ (??%? → ?); #H; ndestruct; 39 ncases ty' in H ⊢ %; ##[ ## #sz sg ## #fs ## #sp ty ## #sp ty n ## #args rty ## #id fs ## #id fs ## #r id ##] 40 nwhd in ⊢ (??%? → ?); #H; ndestruct (H); napply cast_ip_z; //; 42 41 ## #_; nwhd in ⊢ (??%? → ?); #H; ndestruct 43 42 ##] … … 81 80 ## ##*: #e; nwhd in e:(??%?); ndestruct 82 81 ##] 82 ## #r; ncases ty; ##[ ##3: #x; ## ##2,4,6,7,8,9: #x y; ## ##5: #x y z; ##] 83 nwhd in ⊢ (??%? → ?); #H; ndestruct; ncases (eq_region_dec r ?) in H; 84 nwhd in ⊢ (? → ??%? → ?); #H1 H2; ndestruct; 85 ncases ty' in H2; nnormalize; ntry #a; ntry #b; ntry #c; ntry #d; ndestruct; 86 napply cast_pp_z; //; 83 87 ## #sp b of; nwhd in ⊢ (??%? → ?); #e; 84 88 nelim (bind_inversion ????? e); #s; *; #es e'; 85 89 nelim (bind_inversion ????? e'); #u; *; #eu e''; 86 90 nelim (bind_inversion ????? e''); #s'; *; #es' e'''; 87 ncut (type_ spacety s);91 ncut (type_region ty s); 88 92 ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ## ##3: #a e; ## ##2,4,6,7,8,9: #a b e; ## #a b c e; ##] 89 93 nwhd in e:(??%?); ndestruct; //; 90 94 ## #Hty; 91 ncut (type_ spacety' s');95 ncut (type_region ty' s'); 92 96 ##[ ncases ty' in es' ⊢ %; ##[ #e; ## ##3: #a e; ## ##2,4,6,7,8,9: #a b e; ## #a b c e; ##] 93 97 nwhd in e:(??%?); ndestruct; //; 94 98 ## #Hty'; 95 ncut (s = sp). nelim ( ms_eq_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.99 ncut (s = sp). nelim (eq_region_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct. 96 100 #e; nrewrite < e; 97 101 nwhd in match (is_pointer_compat ??) in e'''; 
Deliverables/D3.1/Csemantics/Csem.ma
r481 r484 39 39  is_false_int: ∀sz,sg. 40 40 is_false (Vint zero) (Tint sz sg) 41  is_false_pointer: ∀ s,t.42 is_false (V int zero) (Tpointer st)41  is_false_pointer: ∀r,r',t. 42 is_false (Vnull r) (Tpointer r' t) 43 43  is_false_float: ∀sz. 44 44 is_false (Vfloat Fzero) (Tfloat sz). … … 48 48 n ≠ zero → 49 49 is_true (Vint n) (Tint sz sg) 50  is_true_pointer_int: ∀psp,b,ofs,sz,sg.51 is_true (Vptr psp b ofs) (Tint sz sg)52  is_true_int_pointer: ∀n,s,t.53 n ≠ zero →54 is_true (Vint n) (Tpointer s t)55 50  is_true_pointer_pointer: ∀psp,b,ofs,s,t. 56 51 is_true (Vptr psp b ofs) (Tpointer s t) … … 136 131 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 137 132 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2))) 133  _ ⇒ None ? ] 134  Vnull r ⇒ match v2 with 135 [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? 138 136  _ ⇒ None ? ] 139 137  _ ⇒ None ? ] … … 176 174 else None ? 177 175  _ ⇒ None ? ] 176  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero)  _ ⇒ None ? ] 178 177  _ ⇒ None ? ] 179 178  sub_default ⇒ None ? … … 299 298 ]. 300 299 300 nlet rec sem_cmp_match (c: comparison): option val ≝ 301 match c with 302 [ Ceq => Some ? Vtrue 303  Cne => Some ? Vfalse 304  _ => None ? 305 ]. 306 301 307 nlet rec sem_cmp (c:comparison) 302 308 (v1: val) (t1: type) (v2: val) (t2: type) … … 313 319 [ Vint n1 ⇒ match v2 with 314 320 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 315  Vptr psp b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?316 321  _ ⇒ None ? 317 322 ] 318  Vptr pcl1 b1 ofs1 ⇒323  Vptr r1 b1 ofs1 ⇒ 319 324 match v2 with 320 [ Vptr pcl2 b2 ofs2 ⇒321 if valid_pointer m pcl1 b1 (signed ofs1)322 ∧ valid_pointer m pcl2 b2 (signed ofs2) then325 [ Vptr r2 b2 ofs2 ⇒ 326 if valid_pointer m r1 b1 (signed ofs1) 327 ∧ valid_pointer m r2 b2 (signed ofs2) then 323 328 if eqZb b1 b2 324 329 then Some ? (of_bool (cmp c ofs1 ofs2)) 325 330 else sem_cmp_mismatch c 326 331 else None ? 327  Vint n ⇒ 328 if eq n zero then sem_cmp_mismatch c else None ? 332  Vnull r2 ⇒ sem_cmp_mismatch c 329 333  _ ⇒ None ? ] 334  Vnull r1 ⇒ 335 match v2 with 336 [ Vptr r2 b2 ofs2 ⇒ sem_cmp_mismatch c 337  Vnull r2 ⇒ sem_cmp_match c 338  _ ⇒ None ? 339 ] 330 340  _ ⇒ None ? ] 331 341  cmp_case_ff ⇒ … … 400 410 ]. 401 411 402 ninductive type_pointable : type → Prop ≝ 403 (* All integer sizes can represent at least one kind of pointer *) 404  type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t) 405  type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n) 406  type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty). 407 408 ninductive type_space : type → region → Prop ≝ 409  type_spc_pointer : ∀s,t. type_space (Tpointer s t) s 410  type_spc_array : ∀s,t,n. type_space (Tarray s t n) s 412 ninductive type_region : type → region → Prop ≝ 413  type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s 414  type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s 411 415 (* XXX Is the following necessary? *) 412  type_ spc_code : ∀tys,ty. type_space(Tfunction tys ty) Code.416  type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. 413 417 414 418 ninductive cast : mem → val → type → type → val → Prop ≝ … … 425 429 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 426 430 (Vfloat (cast_float_float sz2 f)) 427  cast_pp: ∀m,psp,psp',ty,ty',b,ofs. 428 type_space ty psp → 429 type_space ty' psp' → 430 pointer_compat (block_space m b) psp' → 431 cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs) 432  cast_ip_z: ∀m,sz,sg,ty'. 433 type_pointable ty' → 434 cast m (Vint zero) (Tint sz sg) ty' (Vint zero) 435  cast_pp_z: ∀m,ty,ty'. 436 type_pointable ty → 437 type_pointable ty' → 438 cast m (Vint zero) ty ty' (Vint zero). 439 (* Should probably also allow pointers to pass through sufficiently large 440 unsigned integers. *) 441 (* Perhaps a little too generous? For example, some integers may not 442 represent a valid generic pointer. 443  cast_pp_i: ∀m,n,ty,ty',t1,t2. (**r no change in data representation *) 444 type_pointable ty → 445 type_pointable ty' → 446 sizeof ty ≤ sizeof ty' → 447 cast m (Vint n) t1 t2 (Vint n). 448 *) 431  cast_pp: ∀m,r,r',ty,ty',b,ofs. 432 type_region ty r → 433 type_region ty' r' → 434 pointer_compat (block_space m b) r' → 435 cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs) 436  cast_ip_z: ∀m,sz,sg,ty',r. 437 type_region ty' r → 438 cast m (Vint zero) (Tint sz sg) ty' (Vnull r) 439  cast_pp_z: ∀m,ty,ty',r,r'. 440 type_region ty r → 441 type_region ty' r' → 442 cast m (Vnull r) ty ty' (Vnull r'). 449 443 450 444 (* * * Operational semantics *) 
Deliverables/D3.1/Csemantics/Mem.ma
r483 r484 737 737 setN 7 pos (Vfloat f) (reccall (pos + oneZ)) 738 738  Init_space n ⇒ reccall (pos + Zmax n 0) (*??*) 739  Init_null r ⇒ setN (pred_size_pointer r) pos (V int zero) (reccall (pos + oneZ))739  Init_null r ⇒ setN (pred_size_pointer r) pos (Vnull r) (reccall (pos + oneZ)) 740 740  Init_addrof s n ⇒ 741 741 (* Not handled properly yet *) 
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.