Changeset 774 for src

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:

• CHANGES (modified) (1 diff)
• RTLabs/semantics.ma (modified) (2 diffs)
• common/FrontEndOps.ma (modified) (4 diffs)

src/CHANGES

@@ -46 +46 @@
   The constants follow CompCert's rather than the prototype's with the result
   that they match up more closely with the addressing modes in RTLabs.
+
+  One of the front end operations for subtraction (subpp) appears to be missing
+  from the prototype at present.

src/RTLabs/semantics.ma

@@ -74 +74 @@
 [ Aindexed i ⇒ λargs.
     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
-    opt_to_res … (ev_add v (Vint i))
+    opt_to_res … (ev_addp v (Vint i))
 | Aindexed2 ⇒ λargs.
     do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
     do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
-    opt_to_res … (ev_add v1 v2)
+    opt_to_res … (ev_addp v1 v2)
 | Aglobal id off ⇒ λargs.
     do loc ← opt_to_res … (find_symbol ?? ge id);
@@ -85 +85 @@
     do loc ← opt_to_res … (find_symbol ?? ge id);
     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
-    opt_to_res … (ev_add (Vptr Any loc ? zero_offset) v)
+    opt_to_res … (ev_addp (Vptr Any loc ? zero_offset) v)
 | Ainstack off ⇒ λargs.
     OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))

src/common/FrontEndOps.ma

@@ -67 +67 @@
   | Ocmpf: comparison -> binary_operation  (**r float comparison *)
   | Oaddp: binary_operation                (**r add an integer to a pointer *)
-  | Osubp: binary_operation                (**r subtract two pointers *)
+  | Osubpi: binary_operation               (**r subtract int from a pointers *)
+  | Osubpp: binary_operation               (**r subtract two pointers *)
   | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
 
@@ -197 +198 @@
   ].
 
-(* TODO: add zero to null? *)
 definition ev_add ≝ λv1,v2: val.
   match v1 with
   [ Vint n1 ⇒ match v2 with
     [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
-    | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
-    | _ ⇒ None ? ]
-  | Vptr r b1 p ofs1 ⇒ match v2 with
+    | _ ⇒ None ? ]
+  | _ ⇒ None ? ].
+
+definition ev_sub ≝ λv1,v2: val.
+  match v1 with
+  [ Vint n1 ⇒ match v2 with
+    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
+    | _ ⇒ None ? ]
+  | _ ⇒ None ? ].
+
+(* NB: requires arguments to be presented pointer first. *)
+definition ev_addp ≝ λv1,v2: val.
+  match v1 with
+  [ Vptr r b1 p ofs1 ⇒ match v2 with
     [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
     | _ ⇒ None ? ]
-  | _ ⇒ None ? ].
-
-definition ev_sub ≝ λv1,v2: val.
-  match v1 with
-  [ Vint n1 ⇒ match v2 with
-    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
-    | _ ⇒ None ? ]
-  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
+  | Vnull r ⇒ match v2 with
+    [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
+    | _ ⇒ None ?
+    ]
+  | _ ⇒ None ? ].
+
+definition ev_subpi ≝ λv1,v2: val.
+  match v1 with
+  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
-    | Vptr r2 b2 p2 ofs2 ⇒
+    | _ ⇒ None ? ]
+  | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
+  | _ ⇒ None ? ].
+
+definition ev_subpp ≝ λv1,v2: val.
+  match v1 with
+  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
+    [ Vptr r2 b2 p2 ofs2 ⇒
         if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
     | _ ⇒ None ? ]
@@ -398 +417 @@
     [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     | _ ⇒ None ? ]
-  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
+  | _ ⇒ None ? ].
+
+definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
+  match v1 with
+  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     [ Vptr r2 b2 p2 ofs2 ⇒
         if eq_block b1 b2
@@ -450 +473 @@
   | Ocmpu c ⇒ ev_cmpu c
   | Ocmpf c ⇒ ev_cmpf c
-  (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)
-  | Oaddp ⇒ ev_add
-  | Osubp ⇒ ev_sub
-  | Ocmpp c ⇒ ev_cmp c
-  ].
-
+  | Oaddp ⇒ ev_addp
+  | Osubpi ⇒ ev_subpi
+  | Osubpp ⇒ ev_subpp
+  | Ocmpp c ⇒ ev_cmpp c
+  ].
+