Changeset 774
 Timestamp:
 Apr 26, 2011, 4:51:44 PM (10 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/CHANGES
r773 r774 46 46 The constants follow CompCert's rather than the prototype's with the result 47 47 that they match up more closely with the addressing modes in RTLabs. 48 49 One of the front end operations for subtraction (subpp) appears to be missing 50 from the prototype at present. 
src/RTLabs/semantics.ma
r766 r774 74 74 [ Aindexed i ⇒ λargs. 75 75 do v ← reg_retrieve (locals f) ((args !!! 0) ?); 76 opt_to_res … (ev_add v (Vint i))76 opt_to_res … (ev_addp v (Vint i)) 77 77  Aindexed2 ⇒ λargs. 78 78 do v1 ← reg_retrieve (locals f) ((args !!! 0) ?); 79 79 do v2 ← reg_retrieve (locals f) ((args !!! 1) ?); 80 opt_to_res … (ev_add v1 v2)80 opt_to_res … (ev_addp v1 v2) 81 81  Aglobal id off ⇒ λargs. 82 82 do loc ← opt_to_res … (find_symbol ?? ge id); … … 85 85 do loc ← opt_to_res … (find_symbol ?? ge id); 86 86 do v ← reg_retrieve (locals f) ((args !!! 0) ?); 87 opt_to_res … (ev_add (Vptr Any loc ? zero_offset) v)87 opt_to_res … (ev_addp (Vptr Any loc ? zero_offset) v) 88 88  Ainstack off ⇒ λargs. 89 89 OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off)) 
src/common/FrontEndOps.ma
r744 r774 67 67  Ocmpf: comparison > binary_operation (**r float comparison *) 68 68  Oaddp: binary_operation (**r add an integer to a pointer *) 69  Osubp: binary_operation (**r subtract two pointers *) 69  Osubpi: binary_operation (**r subtract int from a pointers *) 70  Osubpp: binary_operation (**r subtract two pointers *) 70 71  Ocmpp: comparison → binary_operation. (**r compare pointers *) 71 72 … … 197 198 ]. 198 199 199 (* TODO: add zero to null? *)200 200 definition ev_add ≝ λv1,v2: val. 201 201 match v1 with 202 202 [ Vint n1 ⇒ match v2 with 203 203 [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2)) 204  Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1)) 205  _ ⇒ None ? ] 206  Vptr r b1 p ofs1 ⇒ match v2 with 204  _ ⇒ None ? ] 205  _ ⇒ None ? ]. 206 207 definition ev_sub ≝ λv1,v2: val. 208 match v1 with 209 [ Vint n1 ⇒ match v2 with 210 [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) 211  _ ⇒ None ? ] 212  _ ⇒ None ? ]. 213 214 (* NB: requires arguments to be presented pointer first. *) 215 definition ev_addp ≝ λv1,v2: val. 216 match v1 with 217 [ Vptr r b1 p ofs1 ⇒ match v2 with 207 218 [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2)) 208 219  _ ⇒ None ? ] 209  _ ⇒ None ? ]. 210 211 definition ev_sub ≝ λv1,v2: val. 212 match v1 with 213 [ Vint n1 ⇒ match v2 with 214 [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) 215  _ ⇒ None ? ] 216  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 220  Vnull r ⇒ match v2 with 221 [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? 222  _ ⇒ None ? 223 ] 224  _ ⇒ None ? ]. 225 226 definition ev_subpi ≝ λv1,v2: val. 227 match v1 with 228 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 217 229 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)) 218  Vptr r2 b2 p2 ofs2 ⇒ 230  _ ⇒ None ? ] 231  Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?  _ ⇒ None ? ] 232  _ ⇒ None ? ]. 233 234 definition ev_subpp ≝ λv1,v2: val. 235 match v1 with 236 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 237 [ Vptr r2 b2 p2 ofs2 ⇒ 219 238 if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ? 220 239  _ ⇒ None ? ] … … 398 417 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 399 418  _ ⇒ None ? ] 400  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 419  _ ⇒ None ? ]. 420 421 definition ev_cmpp ≝ λc: comparison. λv1,v2: val. 422 match v1 with 423 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 401 424 [ Vptr r2 b2 p2 ofs2 ⇒ 402 425 if eq_block b1 b2 … … 450 473  Ocmpu c ⇒ ev_cmpu c 451 474  Ocmpf c ⇒ ev_cmpf c 452 (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)453  O addp ⇒ ev_add454  Osubp ⇒ ev_sub455  Ocmpp c ⇒ ev_cmp c456 ]. 457 475  Oaddp ⇒ ev_addp 476  Osubpi ⇒ ev_subpi 477  Osubpp ⇒ ev_subpp 478  Ocmpp c ⇒ ev_cmpp c 479 ]. 480
Note: See TracChangeset
for help on using the changeset viewer.