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

Separate out null values from integer zeros.

File:
1 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  ##]
Note: See TracChangeset for help on using the changeset viewer.