Changeset 484


Ignore:
Timestamp:
Jan 28, 2011, 2:41:49 PM (6 years ago)
Author:
campbell
Message:

Separate out null values from integer zeros.

Location:
Deliverables/D3.1/C-semantics
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r481 r484  
    4545  [ Vint i ⇒ match ty with
    4646    [ Tint _ _ ⇒ OK ? (¬eq i zero)
    47     | Tpointer _ _ ⇒ OK ? (¬eq i zero)
    4847    | _ ⇒ Error ?
    4948    ]
     
    5352    ]
    5453  | 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
    5759    | _ ⇒ Error ?
    5860    ]
     
    6466  ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    6567  ##| #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; @; //
    6868  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    6969  ##| #i s; @ false; @; //;
    70   ##| #p t; @ false; @; //;
     70  ##| #r r' t; @ false; @; //;
    7171  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    7272  ##]
     
    131131  [ Tint _ _ ⇒
    132132    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)
    157136    | _ ⇒ Error ?
    158137    ]
     
    161140| false ⇒ Error ?
    162141].
    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.
    166142
    167143ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
     
    196172| Vptr p b ofs ⇒
    197173    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 ? ];
    199175    do s' ← match ty' with
    200176         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
     
    203179    then OK ? (Vptr s' b ofs)
    204180    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')
    205188| _ ⇒ Error ?
    206189].
     
    390373    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    391374| 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 ⇒
    393376      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    394377      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
    395378    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    396379| 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 ⇒
    398381      match type_eq_dec t t' with [ inl e2 ⇒
    399382        match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
     
    423406    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    424407| 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 ⇒
    426409      match ident_eq i i' with [ inl e2 ⇒ inl ???
    427410      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     
    700683  let m0 ≝ init_mem Genv ?? p in
    701684    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 ? ]);
    703686    do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    704687    OK ? (Callstate f (nil ?) Kstop m0).
     
    713696    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    714697    ##| #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;
    716700    ##]
    717701  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     
    794778  ##| #fd args k mem
    795779  ##| #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 ##]
    797781    ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##]
    798782  ##]
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r481 r484  
    4949##] nqed.
    5050
    51 nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
     51nlemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
    5252##[ #s; ncases s; napply refl;
    5353##| ##skip
     
    100100    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
    101101    nwhd in ⊢ (??%?);
    102     ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]
     102    ##[ ##1,2: nrewrite > (eq_region_dec_true …); nwhd in ⊢ (??%?); ##]
    103103    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
    104104    #H3; nwhd in ⊢ (??%?);
    105105    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;
    108109##] nqed.
    109110
     
    125126  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    126127  ##| #p b i i0 s; @ true; @; //
    127   ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    128   ##| #p b i p0 t0; @ true; @; //
    129128  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    130129  ##| #i s; @ false; @; //;
    131   ##| #p t; @ false; @; //;
     130  ##| #r r' t; @ false; @; //;
    132131  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    133132  ##]
     
    138137  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
    139138  ##| #p b i i0 s; //
    140   ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //;
    141   ##| #p b i p0 t0; //
    142139  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
    143140  ##]
     
    147144#v ty H; nelim H;
    148145  ##[ #i s; //;
    149   ##| #p t; //;
     146  ##| #r r' t; //;
    150147  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
    151148  ##]
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r481 r484  
    44 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    55#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 ##]
     6ncases v; ##[ ##| #i ##| #f ##| #r1 ##| #r b of ##]
     7ncases 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 ##]
    98#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);
    1514  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
    1615  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
    1716  ##]
    18 ##| ##2,5: napply bool_of_val_true; //
     17##| napply bool_of_val_false; //
     18##| napply bool_of_val_true; //
    1919##] nqed.
    2020
     
    3636##[ #e; nrewrite > e;
    3737    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; //;
    4241##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
    4342##]
     
    8180                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
    8281                    ##]
     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; //;
    8387##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
    8488    nelim (bind_inversion ????? e); #s; *; #es e';
    8589    nelim (bind_inversion ????? e'); #u; *; #eu e'';
    8690    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    87     ncut (type_space ty s);
     91    ncut (type_region ty s);
    8892    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8993        nwhd in e:(??%?); ndestruct; //;
    9094    ##| #Hty;
    91         ncut (type_space ty' s');
     95        ncut (type_region ty' s');
    9296        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    9397            nwhd in e:(??%?); ndestruct; //;
    9498        ##| #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.
    96100            #e; nrewrite < e;
    97101            nwhd in match (is_pointer_compat ??) in e''';
  • Deliverables/D3.1/C-semantics/Csem.ma

    r481 r484  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint zero) (Tint sz sg)
    41   | is_false_pointer: ∀s,t.
    42       is_false (Vint zero) (Tpointer s t)
     41  | is_false_pointer: ∀r,r',t.
     42      is_false (Vnull r) (Tpointer r' t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
     
    4848      n ≠ zero →
    4949      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)
    5550  | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
    5651      is_true (Vptr psp b ofs) (Tpointer s t)
     
    136131      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    137132        [ 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 ?
    138136        | _ ⇒ None ? ]
    139137      | _ ⇒ None ? ]
     
    176174          else None ?
    177175        | _ ⇒ None ? ]
     176      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
    178177      | _ ⇒ None ? ]
    179178  | sub_default ⇒ None ?
     
    299298  ].
    300299
     300nlet rec sem_cmp_match (c: comparison): option val ≝
     301  match c with
     302  [ Ceq =>  Some ? Vtrue
     303  | Cne =>  Some ? Vfalse
     304  | _   => None ?
     305  ].
     306 
    301307nlet rec sem_cmp (c:comparison)
    302308                  (v1: val) (t1: type) (v2: val) (t2: type)
     
    313319      [ Vint n1 ⇒ match v2 with
    314320         [ 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 ?
    316321         | _ ⇒ None ?
    317322         ]
    318       | Vptr pcl1 b1 ofs1 ⇒
     323      | Vptr r1 b1 ofs1 ⇒
    319324        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) then
     325        [ Vptr r2 b2 ofs2 ⇒
     326          if valid_pointer m r1 b1 (signed ofs1)
     327          ∧ valid_pointer m r2 b2 (signed ofs2) then
    323328            if eqZb b1 b2
    324329            then Some ? (of_bool (cmp c ofs1 ofs2))
    325330            else sem_cmp_mismatch c
    326331          else None ?
    327         | Vint n ⇒
    328           if eq n zero then sem_cmp_mismatch c else None ?
     332        | Vnull r2 ⇒ sem_cmp_mismatch c
    329333        | _ ⇒ 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        ]
    330340      | _ ⇒ None ? ]
    331341  | cmp_case_ff ⇒
     
    400410  ].
    401411
    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
     412ninductive 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
    411415(* 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.
    413417
    414418ninductive cast : mem → val → type → type → val → Prop ≝
     
    425429      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    426430           (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').
    449443
    450444(* * * Operational semantics *)
  • Deliverables/D3.1/C-semantics/Mem.ma

    r483 r484  
    737737      setN 7 pos (Vfloat f) (reccall (pos + oneZ))
    738738  | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
    739   | Init_null r ⇒ setN (pred_size_pointer r) pos (Vint zero) (reccall (pos + oneZ))
     739  | Init_null r ⇒ setN (pred_size_pointer r) pos (Vnull r) (reccall (pos + oneZ))
    740740  | Init_addrof s n ⇒
    741741      (* Not handled properly yet *)
  • Deliverables/D3.1/C-semantics/Values.ma

    r483 r484  
    3333             memory regions such a pointer could address), a memory address and
    3434             an integer offset with respect to this address;
     35- a null pointer: the region denotes the representation (i.e., pointer size)
    3536- the [Vundef] value denoting an arbitrary bit pattern, such as the
    3637  value of an uninitialized variable.
     
    4142  | Vint: int → val
    4243  | Vfloat: float → val
     44  | Vnull: region → val
    4345  | Vptr: region → block → int → val.
    4446
     
    5860*)
    5961ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
    60 
     62(*
    6163ndefinition has_type ≝ λv: val. λt: typ.
    6264  match v with
     
    7476               has_type v1 t1 ∧ has_type_list vs ts ]
    7577  ].
    76 
     78*)
    7779(* * Truth values.  Pointers and non-zero integers are treated as [True].
    7880  The integer 0 (also used to represent the null pointer) is [False].
     
    8991  match v with
    9092  [ Vint n ⇒ n = zero
     93  | Vnull _ ⇒ True
    9194  | _ ⇒ False
    9295  ].
     
    98101      bool_of_val (Vint zero) false
    99102  | 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.
    101106
    102107ndefinition neg : val → val ≝ λv.
     
    154159  [ Vint n ⇒ of_bool (int_eq n zero)
    155160  | Vptr _ b ofs ⇒ Vfalse
     161  | Vnull _ ⇒ Vtrue
    156162  | _ ⇒ Vundef
    157163  ].
     
    175181  ].
    176182
     183(* TODO: add zero to null? *)
    177184ndefinition add ≝ λv1,v2: val.
    178185  match v1 with
     
    196203        if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    197204    | _ ⇒ Vundef ]
     205  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
    198206  | _ ⇒ Vundef ].
    199207
     
    342350  | _ ⇒ Vundef ].
    343351
     352ndefinition cmp_match : comparison → val ≝ λc.
     353  match c with
     354  [ Ceq ⇒ Vtrue
     355  | Cne ⇒ Vfalse
     356  | _   ⇒ Vundef
     357  ].
     358
    344359ndefinition cmp_mismatch : comparison → val ≝ λc.
    345360  match c with
     
    349364  ].
    350365
     366(* TODO: consider whether to check pointer representations *)
    351367ndefinition cmp ≝ λc: comparison. λv1,v2: val.
    352368  match v1 with
    353369  [ Vint n1 ⇒ match v2 with
    354370    [ 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 ⇒
    360374        if eqZb b1 b2
    361375        then of_bool (cmp c ofs1 ofs2)
    362376        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    ]
    366384  | _ ⇒ Vundef ].
    367385
     
    370388  [ Vint n1 ⇒ match v2 with
    371389    [ 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 ⇒
    377393        if eqZb b1 b2
    378394        then of_bool (cmpu c ofs1 ofs2)
    379395        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    ]
    383403  | _ ⇒ Vundef ].
    384404
     
    408428    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    409429    | Mint32 ⇒ Vint n
    410     | Mpointer r ⇒ if eq n zero then Vint zero else Vundef
    411430    | _ ⇒ Vundef
    412431    ]
     
    414433    match chunk with
    415434    [ 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
    416440    | _ ⇒ Vundef
    417441    ]
Note: See TracChangeset for help on using the changeset viewer.