Changeset 774 for src


Ignore:
Timestamp:
Apr 26, 2011, 4:51:44 PM (9 years ago)
Author:
campbell
Message:

Separate out the different forms of addition and subtraction in the frontend ops.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r773 r774  
    4646  The constants follow CompCert's rather than the prototype's with the result
    4747  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  
    7474[ Aindexed i ⇒ λargs.
    7575    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))
    7777| Aindexed2 ⇒ λargs.
    7878    do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
    7979    do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
    80     opt_to_res … (ev_add v1 v2)
     80    opt_to_res … (ev_addp v1 v2)
    8181| Aglobal id off ⇒ λargs.
    8282    do loc ← opt_to_res … (find_symbol ?? ge id);
     
    8585    do loc ← opt_to_res … (find_symbol ?? ge id);
    8686    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)
    8888| Ainstack off ⇒ λargs.
    8989    OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
  • src/common/FrontEndOps.ma

    r744 r774  
    6767  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
    6868  | 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 *)
    7071  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    7172
     
    197198  ].
    198199
    199 (* TODO: add zero to null? *)
    200200definition ev_add ≝ λv1,v2: val.
    201201  match v1 with
    202202  [ Vint n1 ⇒ match v2 with
    203203    [ 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
     207definition 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. *)
     215definition ev_addp ≝ λv1,v2: val.
     216  match v1 with
     217  [ Vptr r b1 p ofs1 ⇒ match v2 with
    207218    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
    208219    | _ ⇒ 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
     226definition ev_subpi ≝ λv1,v2: val.
     227  match v1 with
     228  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    217229    [ 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
     234definition ev_subpp ≝ λv1,v2: val.
     235  match v1 with
     236  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     237    [ Vptr r2 b2 p2 ofs2 ⇒
    219238        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    220239    | _ ⇒ None ? ]
     
    398417    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    399418    | _ ⇒ None ? ]
    400   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     419  | _ ⇒ None ? ].
     420
     421definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
     422  match v1 with
     423  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    401424    [ Vptr r2 b2 p2 ofs2 ⇒
    402425        if eq_block b1 b2
     
    450473  | Ocmpu c ⇒ ev_cmpu c
    451474  | Ocmpf c ⇒ ev_cmpf c
    452   (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)
    453   | Oaddp ⇒ ev_add
    454   | Osubp ⇒ ev_sub
    455   | Ocmpp c ⇒ ev_cmp c
    456   ].
    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.