Changeset 736
- Timestamp:
- Apr 4, 2011, 5:13:08 PM (9 years ago)
- Location:
- src
- Files:
-
- 1 added
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabs-sem.ma
r731 r736 51 51 λrs,v,locals. match rs with [ dp n regs ⇒ 52 52 do vs ← break n v; 53 OK ? (fold_right2_i ??? (λ_. register_update split_val) locals n regs vs)53 OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs) 54 54 ]. 55 55 … … 64 64 definition reg_retrieve : register_env ? → registers → res val ≝ 65 65 λlocals,rs. match rs with [ dp n regs ⇒ 66 do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … ( register_lookup? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;66 do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs; 67 67 merge n vs 68 68 ]. … … 111 111 match st with 112 112 [ State f fs m ⇒ 113 ! s ← graph_lookup? (f_graph (func f)) (next f);113 ! s ← lookup ?? (f_graph (func f)) (next f); 114 114 match s with 115 115 [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉 … … 194 194 match fd with 195 195 [ Internal fn ⇒ 196 ! locals ← params_store (f_params fn) params ( register_empty?);196 ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?); 197 197 let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in 198 198 ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉 -
src/RTLabs/RTLabs-syntax.ma
r720 r736 59 59 60 60 record internal_function : Type[0] ≝ 61 { f_labgen : label_generation62 ; f_reggen : register_generation61 { f_labgen : Universe LabelTag 62 ; f_reggen : Universe RegisterTag 63 63 ; f_sig : signature 64 64 ; f_result : registers -
src/RTLabs/import.ma
r727 r736 2 2 include "RTLabs/RTLabs-sem.ma". 3 3 4 definition new_reg : internal_function → res (register × internal_function) ≝ 5 λf. do 〈r, g〉 ← register_new (f_reggen f); 6 OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f) 7 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 8 9 definition new_label : internal_function → res (label × internal_function) ≝ 10 λf. do 〈l, g〉 ← label_new (f_labgen f); 11 OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f) 12 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 13 14 definition new_statement : internal_function → label → statement → internal_function ≝ 15 λf,l,s. mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) (f_result f) (f_params f) 16 (f_locals f) (f_stacksize f) 17 (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f). 18 19 let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝ 4 let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝ 20 5 match n with 21 6 [ O ⇒ OK ? 〈[[ ]], g〉 22 | S m ⇒ do 〈ls, g'〉 ← n_labels m g; 23 do 〈l, g''〉 ← label_new g'; 24 OK ? 〈l:::ls, g''〉 25 ]. 26 27 let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝ 28 match n with 29 [ O ⇒ OK ? 〈[[ ]], g〉 30 | S m ⇒ do 〈ls, g'〉 ← n_regs m g; 31 do 〈l, g''〉 ← register_new g'; 7 | S m ⇒ do 〈ls, g'〉 ← n_idents m tag g; 8 do 〈l, g''〉 ← fresh ? g'; 32 9 OK ? 〈l:::ls, g''〉 33 10 ]. … … 41 18 ; pf_locals : list pre_registers 42 19 ; pf_stacksize : nat 43 ; pf_graph : list (nat × ((nat → res label) → (nat → res register) → res statement))20 ; pf_graph : list (nat × ((nat → res register) → (nat → res label) → res statement)) 44 21 ; pf_entry : nat 45 22 ; pf_exit : nat … … 52 29 53 30 definition make_registers : 54 (nat → option register) → pre_registers → register_generation→55 res ((nat → option register) × register_generation× registers) ≝31 (nat → option register) → pre_registers → Universe RegisterTag → 32 res ((nat → option register) × (Universe RegisterTag) × registers) ≝ 56 33 λm,rs0,g. 57 34 match rs0 with [ dp n rs ⇒ … … 61 38 match m r with 62 39 [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉 63 | None ⇒ do 〈r',g'〉 ← register_newg;40 | None ⇒ do 〈r',g'〉 ← fresh ? g; 64 41 OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉 65 42 ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs; … … 69 46 70 47 definition make_registers_list : 71 (nat → option register) → list pre_registers → register_generation→72 res ((nat → option register) × register_generation× (list registers)) ≝48 (nat → option register) → list pre_registers → Universe RegisterTag → 49 res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝ 73 50 λm,lrs,g. 74 51 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc; … … 79 56 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ 80 57 λpre_f. 81 let rgen0 ≝ register_gen_newin58 let rgen0 ≝ new_universe RegisterTag in 82 59 do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0; 83 60 let 〈rmap1, rgen1〉 ≝ rmapgen1 in … … 88 65 let rmap ≝ λn. opt_to_res … (rmap3 n) in 89 66 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 90 do 〈labels, gen〉 ← n_ labels (S max_stmt) label_gen_new;67 do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag); 91 68 let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in 92 69 do graph ← foldr ?? (λp,g0. do g ← g0; … … 94 71 do l' ← get_label l; 95 72 do s' ← s rmap get_label; 96 OK ? ( graph_add ? g l' s')) (OK ? (empty_graph?)) (pf_graph pre_f);73 OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); 97 74 do entry ← get_label (pf_entry pre_f); 98 75 do exit ← get_label (pf_exit pre_f); -
src/common/Graphs.ma
r728 r736 2 2 3 3 include "ASM/BitVectorTrie.ma". 4 include "Clight/AST.ma". 5 include "common/Errors.ma". 4 include "common/Identifiers.ma". 6 5 7 definition label ≝ ident.6 axiom LabelTag : String. 8 7 9 definition label _eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.8 definition label ≝ Identifier LabelTag. 10 9 11 record label_generation : Type[0] ≝ { lab_next : label }.10 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 12 11 13 definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).14 12 15 definition label_new : label_generation → res (label × label_generation) ≝ 16 λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in 17 if get_index_v ?? carries 0 ? then Error ? else 18 OK ? 〈lab_next g, mk_label_generation gen〉. 19 // qed. 20 21 definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 22 definition empty_graph : ∀T. graph T ≝ λT. Stub T 16. 23 definition graph_lookup : ∀T. graph T → label → option T ≝ 24 λT,g,l. lookup_opt T 16 l g. 25 definition graph_add : ∀T. graph T → label → T → graph T ≝ 26 λT,g,l,v. insert T 16 l v g. 13 definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag. -
src/common/Registers.ma
r726 r736 5 5 6 6 include "ASM/BitVectorTrie.ma". 7 include "Clight/AST.ma". 8 include "common/Errors.ma". 7 include "common/Identifiers.ma". 9 8 10 definition register ≝ ident.9 axiom RegisterTag : String. 11 10 12 definition register _eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.11 definition register ≝ Identifier RegisterTag. 13 12 14 record register_generation : Type[0] ≝ { reg_next : register }.13 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?. 15 14 16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?). 17 18 definition register_new : register_generation → res (register × register_generation) ≝ 19 λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in 20 if get_index_v ?? carries 0 ? then Error ? else 21 OK ? 〈reg_next g, mk_register_generation gen〉. 22 // qed. 23 24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16. 26 definition register_lookup : ∀T. register_env T → register → option T ≝ 27 λT,g,l. lookup_opt T 16 l g. 28 definition register_update : ∀T. register → T → register_env T → register_env T ≝ 29 λT,l,v,g. insert T 16 l v g. 15 definition register_env ≝ IdentifierMap RegisterTag.
Note: See TracChangeset
for help on using the changeset viewer.