- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- Location:
- src/joint
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Erasure.ma
r1472 r1515 5 5 (globals: list ident) (the_program: list (lin_statement globals)) 6 6 (labels: list label) 7 on the_program: (( BitVectorTrie Word 16) × (list (lin_statement globals))) ≝7 on the_program: ((identifier_map ? label) × (list (lin_statement globals))) ≝ 8 8 match the_program with 9 9 [ nil ⇒ 10 10 match labels with 11 [ nil ⇒ 〈 Stub Word 16, [ ]〉 (* XXX: labels should be empty *)11 [ nil ⇒ 〈empty_map …, [ ]〉 (* XXX: labels should be empty *) 12 12 | _ ⇒ ⊥ 13 13 ] … … 26 26 ] 27 27 | Some lbl ⇒ 28 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in29 28 match instr with 30 29 [ sequential seq l ⇒ … … 33 32 | _ ⇒ 34 33 let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in 35 let maps ≝ foldr ? ? (λl. λmap. 36 match l with 37 [ an_identifier l ⇒ insert … l lbl' map 38 ]) maps (lbl :: labels) 34 let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels) 39 35 in 40 36 〈maps, instructions〉 … … 42 38 | _ ⇒ 43 39 let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in 44 let maps ≝ foldr ? ? (λl. λmap. 45 match l with 46 [ an_identifier l ⇒ insert … l lbl' map 47 ]) maps (lbl :: labels) 40 let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels) 48 41 in 49 42 〈maps, instructions〉 … … 62 55 ∀globals: list ident. 63 56 ∀params: params_. 64 BitVectorTrie Word 16→ joint_instruction params globals → joint_instruction params globals ≝57 identifier_map LabelTag label → joint_instruction params globals → joint_instruction params globals ≝ 65 58 λglobals: list ident. 66 59 λparams. … … 69 62 match instr with 70 63 [ COND acc_a lbl ⇒ 71 let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 72 let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in 64 let located ≝ lookup_def ?? map lbl lbl in 73 65 COND params globals acc_a located 74 66 | _ ⇒ instr … … 78 70 ∀globals: list ident. 79 71 ∀params: params_. 80 BitVectorTrie Word 16→ joint_statement params globals → joint_statement params globals ≝72 identifier_map LabelTag label → joint_statement params globals → joint_statement params globals ≝ 81 73 λglobals: list ident. 82 74 λparams: params_. 83 λmap: BitVectorTrie Word 16.75 λmap: identifier_map LabelTag label. 84 76 λstmt: joint_statement params globals. 85 77 match stmt with … … 89 81 | RETURN ⇒ RETURN params globals 90 82 | GOTO l ⇒ 91 let l ≝ match l with [ an_identifier l ⇒ l ] in 92 let located ≝ an_identifier LabelTag (lookup … l map l) in 83 let located ≝ lookup_def ?? map l l in 93 84 GOTO params globals located 94 85 ]. 95 86 96 87 let rec relabel_lin_internal_function' 97 (globals: list ident) (map: BitVectorTrie Word 16)88 (globals: list ident) (map: identifier_map LabelTag label) 98 89 (program: list (lin_statement globals)) 99 90 on program: list (lin_statement globals) ≝ … … 107 98 [ None ⇒ None … 108 99 | Some label ⇒ 109 let label ≝ match label with [ an_identifier l ⇒ l ] in 110 Some … (an_identifier LabelTag (lookup … label map label)) 100 Some … (lookup_def ?? map label label) 111 101 ] 112 102 in … … 122 112 definition empty_graph ≝ 123 113 λa: Type[0]. 124 an_id_map LabelTag a (Stub a 16).114 empty_map LabelTag a. 125 115 126 116 let rec pre_erase_graph_internal_function' 127 117 (params1: params1) (globals: list ident) 128 118 (the_graph: codeT globals (graph_params params1 globals)) (labels: list label) 129 (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)130 (visited: BitVectorTrie bool 16)131 on size_counter: (( BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝132 match size_counter return λ_. (( BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with119 (entry_point: label) (size_counter: nat) (map: identifier_map LabelTag label) 120 (visited: identifier_map LabelTag bool) 121 on size_counter: ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) ≝ 122 match size_counter return λ_. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with 133 123 [ O ⇒ 134 124 match labels with … … 137 127 ] 138 128 | S size_counter ⇒ 139 let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in140 129 let statement ≝ lookup LabelTag ? the_graph entry_point in 141 match statement return λs: option (joint_statement (graph_params params1 globals) globals). (( BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with130 match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with 142 131 [ None ⇒ ⊥ (* XXX: should not happen *) 143 132 | Some statement ⇒ 144 let entered_previously ≝ bvt_lookup … entry_point' visitedfalse in145 match entered_previously return λe: bool. (( BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with133 let entered_previously ≝ lookup_def … visited entry_point false in 134 match entered_previously return λe: bool. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with 146 135 [ true ⇒ 〈map, visited, the_graph〉 147 136 | false ⇒ (* XXX: never visited here before *) 148 let visited ≝ insert … entry_point' true visitedin149 match statement return λs: joint_statement (graph_params params1 globals) globals. (( BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with137 let visited ≝ add … visited entry_point true in 138 match statement return λs: joint_statement (graph_params params1 globals) globals. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with 150 139 [ sequential seq l ⇒ 151 140 match seq with … … 155 144 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 156 145 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in 157 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in146 let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in 158 147 〈map, visited, the_graph〉 159 148 | _ ⇒ 160 149 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 161 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in150 let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in 162 151 〈map, visited, the_graph〉 163 152 ] 164 153 | RETURN ⇒ 165 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in154 let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in 166 155 〈map, visited, the_graph〉 167 156 | GOTO l ⇒ 168 157 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 169 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in158 let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in 170 159 〈map, visited, the_graph〉 171 160 ] … … 183 172 [ dp entry entry_proof ⇒ 184 173 let code ≝ joint_if_code … int_fun in 185 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) ( Stub …) (Stub…) in174 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (empty_map …) (empty_map …) in 186 175 〈map, the_graph〉 187 176 ]. … … 189 178 let rec relabel_graph' 190 179 (params1: params1) (globals: list ident) 191 (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)192 (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)180 (the_graph: codeT globals (graph_params params1 globals)) (map: identifier_map LabelTag label) 181 (visited: identifier_map LabelTag bool) (entry_point: label) (size_counter: nat) 193 182 on size_counter: codeT globals (graph_params params1 globals) ≝ 194 183 match size_counter return λs: nat. codeT globals (graph_params params1 globals) with 195 184 [ O ⇒ empty_graph … 196 185 | S size_counter ⇒ 197 let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in 198 let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in 186 let relabelled_entry_point ≝ lookup_def … map entry_point entry_point in 199 187 let statement ≝ lookup LabelTag ? the_graph entry_point in 200 188 match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with 201 189 [ None ⇒ ⊥ (* XXX: should not happen *) 202 190 | Some statement ⇒ 203 let entered_previously ≝ (bvt_lookup … entry_point' visited false)in191 let entered_previously ≝ lookup_def … visited entry_point false in 204 192 match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with 205 193 [ true ⇒ the_graph 206 194 | false ⇒ (* XXX: never visited here before *) 207 let visited ≝ insert … entry_point' true visitedin195 let visited ≝ add … visited entry_point true in 208 196 match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with 209 197 [ sequential seq l ⇒ 210 let l' ≝ match l with [ an_identifier l ⇒ l ] in211 198 let 〈the_graph, new_seq〉 ≝ 212 199 match seq return λs. (codeT globals (graph_params params1 globals)) × ? with 213 200 [ COND acc_a cond_label ⇒ 214 let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in 215 let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in 201 let relabelled ≝ lookup_def … map cond_label cond_label in 216 202 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in 217 203 〈tail_graph, COND … acc_a relabelled〉 … … 220 206 in 221 207 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in 222 let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l')in208 let relabelled ≝ lookup_def … map l l in 223 209 add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled) 224 210 | RETURN ⇒ the_graph 225 211 | GOTO l ⇒ 226 let l' ≝ match l with [ an_identifier l ⇒ l ] in 227 let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in 212 let relabelled ≝ lookup_def … map l l in 228 213 add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled) 229 214 ] … … 237 222 λglobals: list ident. 238 223 λparams1: params1. 239 λmap: BitVectorTrie Word 16.224 λmap: identifier_map LabelTag label. 240 225 λint_fun: joint_internal_function globals (graph_params params1 globals). 241 226 match joint_if_entry … int_fun with 242 227 [ dp entry entry_prf ⇒ 243 228 let code ≝ joint_if_code … int_fun in 244 relabel_graph' … code map ( Stub…) entry (graph_num_nodes … code)229 relabel_graph' … code map (empty_map …) entry (graph_num_nodes … code) 245 230 ]. 246 231 … … 248 233 λglobals: list ident. 249 234 λpars: params globals. 250 λerasure_function: joint_internal_function globals pars → ( BitVectorTrie Word 16) × (codeT … pars).251 λrelabelling_function: BitVectorTrie Word 16→ joint_internal_function globals pars → codeT … pars.235 λerasure_function: joint_internal_function globals pars → (identifier_map LabelTag label) × (codeT … pars). 236 λrelabelling_function: identifier_map LabelTag label → joint_internal_function globals pars → codeT … pars. 252 237 λint_fun: joint_internal_function globals pars. 253 238 match joint_if_entry … int_fun with … … 255 240 match joint_if_exit … int_fun with 256 241 [ dp exit exit_prf ⇒ 257 let exit' ≝ word_of_identifier … exit in258 let entry' ≝ word_of_identifier … entry in259 242 let 〈maps, code〉 ≝ erasure_function int_fun in 260 243 let int_fun ≝ set_joint_code globals pars int_fun code entry exit in 261 244 let code ≝ relabelling_function maps int_fun in 262 set_joint_code globals pars int_fun code ( an_identifier … (bvt_lookup … entry' maps entry'))263 ( an_identifier … (bvt_lookup … exit' maps exit'))245 set_joint_code globals pars int_fun code (lookup_def … maps entry entry) 246 (lookup_def … maps exit exit) 264 247 ] 265 248 ]. -
src/joint/SemanticUtils.ma
r1452 r1515 25 25 λoldpc,l. 26 26 mk_pointer Code 27 (mk_block Code (block_id (pblock oldpc))) ? (mk_offset ( nat_of_bitvector ?(word_of_identifier … l))).27 (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))). 28 28 // qed. 29 29 … … 34 34 35 35 definition graph_label_of_pointer: pointer → res label ≝ 36 λp. OK … (an_identifier ? ( bitvector_of_nat … (abs (offv (poff p))))).36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). 37 37 38 38 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. -
src/joint/TranslateUtils.ma
r1352 r1515 24 24 cases (fresh_regs pars0 globals def m) normalize nodelta 25 25 #def' #regs #EQ change in EQ with (|regs| = m) <EQ 26 change with 27 (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?) 28 cases (fresh … (joint_if_runiverse … def')) normalize // ] 26 @refl 27 ] 29 28 qed. 30 29
Note: See TracChangeset
for help on using the changeset viewer.