Changeset 727 for src

Timestamp:

Mar 31, 2011, 5:20:00 PM (10 years ago)

Author:

campbell

Message:

Enough fixes to let an RTLabs program run.

Location:

src

Files:

• RTLabs/RTLabs-sem.ma (modified) (1 diff)
• RTLabs/import.ma (modified) (8 diffs)
• common/FrontEndOps.ma (modified) (4 diffs)

src/RTLabs/RTLabs-sem.ma

@@ -277 +277 @@
     | cons f fs' ⇒
         ! locals ← reg_store dst v (locals f);
-        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs m〉
+        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
     ]
 ].

src/RTLabs/import.ma

@@ -21 +21 @@
 [ O ⇒ OK ? 〈[[ ]], g〉
 | S m ⇒ do 〈ls, g'〉 ← n_labels m g;
-        do 〈l, g''〉 ← label_new g;
+        do 〈l, g''〉 ← label_new g';
         OK ? 〈l:::ls, g''〉
 ].
@@ -29 +29 @@
 [ O ⇒ OK ? 〈[[ ]], g〉
 | S m ⇒ do 〈ls, g'〉 ← n_regs m g;
-        do 〈l, g''〉 ← register_new g;
+        do 〈l, g''〉 ← register_new g';
         OK ? 〈l:::ls, g''〉
 ].
@@ -77 +77 @@
                    OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
 
-definition make_internal_function : pre_internal_function → res internal_function ≝
+definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
 λpre_f.
   let rgen0 ≝ register_gen_new in
@@ -88 +88 @@
   let rmap ≝ λn. opt_to_res … (rmap3 n) in
   let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
-  do 〈labels, gen〉 ← n_labels max_stmt label_gen_new;
+  do 〈labels, gen〉 ← n_labels (S max_stmt) label_gen_new;
   let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
   do graph ← foldr ?? (λp,g0. do g ← g0;
@@ -97 +97 @@
   do entry ← get_label (pf_entry pre_f);
   do exit ← get_label (pf_exit pre_f);
-  OK ? (mk_internal_function
+  OK ? (Internal ? (mk_internal_function
          gen
          rgen3
@@ -108 +108 @@
          entry
          exit
-         ).
+         )).
 
 definition make_regs : (nat → res register) → pre_registers → res registers ≝
@@ -124 +124 @@
 λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps.
 
+(* XXX move somewhere sensible *)
+let rec mmap_vec (A:Type[0]) (B:Type[0]) (f:A → res B) (n:nat) (v:Vector A n) on v : res (Vector B n) ≝
+match v with
+[ VEmpty ⇒ OK ? (VEmpty …)
+| VCons m hd tl ⇒ do hd' ← f hd;
+                  do tl' ← mmap_vec A B f m tl;
+                  OK ? (hd':::tl')
+].
+
+definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝
+λmp,m. mmap_vec ?? (make_regs mp) ?.
+
 let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
 let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
@@ -129 +141 @@
 let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src' ← make_regs r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
 let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src1' ← make_regs r src1; do src2' ← make_regs r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
-let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; OK ? (St_load chunk mode args dst' l').
-let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; OK ? (St_store chunk mode args src' l').
+let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
+let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
 let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l').
 let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l').

src/common/FrontEndOps.ma

@@ -40 +40 @@
   | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
   | Ofloatofint: unary_operation           (**r float to signed integer *)
-  | Ofloatofintu: unary_operation.         (**r float to unsigned integer *)
+  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
+  | Oid: unary_operation                   (**r identity (used to move between registers *)
+  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
+  | Ointofptr: unary_operation.            (**r pointer to int *)
 
 inductive binary_operation : Type[0] ≝
@@ -62 +65 @@
   | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
   | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
-  | Ocmpf: comparison -> binary_operation. (**r float comparison *)
+  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
+  | Oaddp: binary_operation                (**r add an integer to a pointer *)
+  | Osubp: binary_operation                (**r subtract two pointers *)
+  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
 
 
@@ -105 +111 @@
   | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
   | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
+  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
+  (* Only conversion of null pointers is specified. *)
+  | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
+  | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
   ].
 
@@ -445 +455 @@
   | 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
+  ].
+