Changeset 727
 Timestamp:
 Mar 31, 2011, 5:20:00 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabssem.ma
r718 r727 277 277  cons f fs' ⇒ 278 278 ! locals ← reg_store dst v (locals f); 279 ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs m〉279 ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉 280 280 ] 281 281 ]. 
src/RTLabs/import.ma
r726 r727 21 21 [ O ⇒ OK ? 〈[[ ]], g〉 22 22  S m ⇒ do 〈ls, g'〉 ← n_labels m g; 23 do 〈l, g''〉 ← label_new g ;23 do 〈l, g''〉 ← label_new g'; 24 24 OK ? 〈l:::ls, g''〉 25 25 ]. … … 29 29 [ O ⇒ OK ? 〈[[ ]], g〉 30 30  S m ⇒ do 〈ls, g'〉 ← n_regs m g; 31 do 〈l, g''〉 ← register_new g ;31 do 〈l, g''〉 ← register_new g'; 32 32 OK ? 〈l:::ls, g''〉 33 33 ]. … … 77 77 OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs. 78 78 79 definition make_internal_function : pre_internal_function → res internal_function≝79 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ 80 80 λpre_f. 81 81 let rgen0 ≝ register_gen_new in … … 88 88 let rmap ≝ λn. opt_to_res … (rmap3 n) in 89 89 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 90 do 〈labels, gen〉 ← n_labels max_stmtlabel_gen_new;90 do 〈labels, gen〉 ← n_labels (S max_stmt) label_gen_new; 91 91 let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in 92 92 do graph ← foldr ?? (λp,g0. do g ← g0; … … 97 97 do entry ← get_label (pf_entry pre_f); 98 98 do exit ← get_label (pf_exit pre_f); 99 OK ? ( mk_internal_function99 OK ? (Internal ? (mk_internal_function 100 100 gen 101 101 rgen3 … … 108 108 entry 109 109 exit 110 ) .110 )). 111 111 112 112 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. 125 125 126 (* XXX move somewhere sensible *) 127 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) ≝ 128 match v with 129 [ VEmpty ⇒ OK ? (VEmpty …) 130  VCons m hd tl ⇒ do hd' ← f hd; 131 do tl' ← mmap_vec A B f m tl; 132 OK ? (hd':::tl') 133 ]. 134 135 definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝ 136 λmp,m. mmap_vec ?? (make_regs mp) ?. 137 126 138 let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l'). 127 139 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'). 130 142 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'). 131 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 argsdst' l').132 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 argssrc' l').143 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'). 144 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'). 133 145 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'). 134 146 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
r702 r727 40 40  Ointuoffloat: unary_operation (**r unsigned integer to float *) 41 41  Ofloatofint: unary_operation (**r float to signed integer *) 42  Ofloatofintu: unary_operation. (**r float to unsigned integer *) 42  Ofloatofintu: unary_operation (**r float to unsigned integer *) 43  Oid: unary_operation (**r identity (used to move between registers *) 44  Optrofint: region → unary_operation (**r int to pointer with given representation *) 45  Ointofptr: unary_operation. (**r pointer to int *) 43 46 44 47 inductive binary_operation : Type[0] ≝ … … 62 65  Ocmp: comparison > binary_operation (**r integer signed comparison *) 63 66  Ocmpu: comparison > binary_operation (**r integer unsigned comparison *) 64  Ocmpf: comparison > binary_operation. (**r float comparison *) 67  Ocmpf: comparison > binary_operation (**r float comparison *) 68  Oaddp: binary_operation (**r add an integer to a pointer *) 69  Osubp: binary_operation (**r subtract two pointers *) 70  Ocmpp: comparison → binary_operation. (**r compare pointers *) 65 71 66 72 … … 105 111  Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1))  _ ⇒ None ? ] 106 112  Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1))  _ ⇒ None ? ] 113  Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *) 114 (* Only conversion of null pointers is specified. *) 115  Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ?  _ ⇒ None ? ] 116  Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero)  _ ⇒ None ? ] 107 117 ]. 108 118 … … 445 455  Ocmpu c ⇒ ev_cmpu c 446 456  Ocmpf c ⇒ ev_cmpf c 447 ]. 448 457 (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *) 458  Oaddp ⇒ ev_add 459  Osubp ⇒ ev_sub 460  Ocmpp c ⇒ ev_cmp c 461 ]. 462
Note: See TracChangeset
for help on using the changeset viewer.