Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (9 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

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

    r499 r500  
    5252    | _ ⇒ Error ?
    5353    ]
    54   | Vptr _ _ _ ⇒ match ty with
     54  | Vptr _ _ _ _ ⇒ match ty with
    5555    [ Tpointer _ _ ⇒ OK ? true
    5656    | _ ⇒ Error ?
     
    6666#v #ty #r #H elim H; #v #t #H' elim H';
    6767  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
    68   | #p #b #i #i0 #s %{ true} % //
     68  | #r #b #pc #i #i0 #s %{ true} % //
    6969  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    7070  | #i #s %{ false} % //;
     
    164164  | _ ⇒ Error ?
    165165  ]
    166 | Vptr p b ofs ⇒
     166| Vptr r b _ ofs ⇒
    167167    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    168     do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
     168    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
    169169    do s' ← match ty' with
    170170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    171171         | _ ⇒ Error ? ];
    172     if is_pointer_compat b s'
    173     then OK ? (Vptr s' b ofs)
    174     else Error ?
     172    match pointer_compat_dec b s' with
     173    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
     174    | inr _ ⇒ Error ?
     175    ]
    175176| Vnull r ⇒
    176177    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
     
    211212      do 〈lo,tr〉 ← exec_lvalue ge en m a;
    212213      match ty with
    213       [ Tpointer r _ ⇒ OK ? 〈match lo with [ pair loc ofs ⇒  Vptr r loc ofs ], tr〉
     214      [ Tpointer r _ ⇒
     215        match lo with [ pair loc ofs ⇒
     216          match pointer_compat_dec loc r with
     217          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
     218          | inr _ ⇒ Error ?
     219          ]
     220        ]
    214221      | _ ⇒ Error ?
    215222      ]
     
    266273      do 〈v,tr〉 ← exec_expr ge en m a;
    267274      match v with
    268       [ Vptr _ l ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
     275      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
    269276      | _ ⇒ Error ?
    270277      ]
     
    669676    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    670677    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    671     | #r #b #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     678    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    672679    ]
    673680  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
     
    754761  | #fd #args #k #mem
    755762  | #v #k #mem (* for final state check *) cases k;
    756     [ cases v; [ 2,3: #v' | 4: #r | 5: #sp #loc #off ]
     763    [ cases v; [ 2,3: #v' | 4: #r | 5: #r #loc #pc #off ]
    757764    | #s' #k' | 3,4: #e #s' #k' | 5,6: #e #s' #s'' #k' | #k' | #a #b #c #d ]
    758765  ]
Note: See TracChangeset for help on using the changeset viewer.