Changeset 1471 for src/joint/ProofUtils.ma
 Timestamp:
 Oct 28, 2011, 3:05:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/ProofUtils.ma
r1470 r1471 1 include "joint/Joint.ma".2 1 include "LIN/LIN.ma". 2 include "joint/SemanticUtils.ma". 3 3 4 4 let rec pre_erase_lin_internal_function' … … 54 54 qed. 55 55 56 definition pre_erase_lin_internal_function ≝ 57 λglobals: list ident. 58 λint_fun: joint_internal_function … (lin_params globals). 59 pre_erase_lin_internal_function' … (joint_if_code … (lin_params …) int_fun) [ ]. 60 56 61 definition relabel_joint_instruction: 57 62 ∀globals: list ident. … … 89 94 ]. 90 95 91 let rec relabel 96 let rec relabel_lin_internal_function' 92 97 (globals: list ident) (map: BitVectorTrie Word 16) 93 98 (program: list (lin_statement globals)) … … 106 111 ] 107 112 in 108 〈label, relabelled〉 :: relabel globals map tl 109 ]. 110 111 definition pre_erase_lin_internal_function: 112 ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝ 113 〈label, relabelled〉 :: relabel_lin_internal_function' globals map tl 114 ]. 115 116 definition relabel_lin_internal_function ≝ 113 117 λglobals. 114 λfunction. 115 let luniverse ≝ joint_if_luniverse … function in 116 let runiverse ≝ joint_if_runiverse … function in 117 let result ≝ joint_if_result … function in 118 let params ≝ joint_if_params … function in 119 let locals ≝ joint_if_locals … function in 120 let stacksize ≝ joint_if_stacksize … function in 121 let code ≝ joint_if_code … function in 122 let entry ≝ ? in 123 let exit ≝ ? in 124 let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in 125 let code ≝ relabel globals maps code in 126 mk_joint_internal_function … 127 luniverse runiverse result params 128 locals stacksize code entry exit. 129 cases daemon (* XXX *) 130 qed. 131 132 definition erase_lin_program: lin_program → lin_program ≝ 133 λprogram. 134 transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)). 135 136 include "joint/SemanticUtils.ma". 118 λmap. 119 λint_fun: joint_internal_function globals (lin_params globals). 120 relabel_lin_internal_function' globals map (joint_if_code … int_fun). 137 121 138 122 definition empty_graph ≝ … … 158 142 [ None ⇒ ⊥ (* XXX: should not happen *) 159 143  Some statement ⇒ 160 let entered_previously ≝ ? in 161 let visited ≝ insert … entry_point' true visited in 144 let entered_previously ≝ bvt_lookup … entry_point' visited false in 162 145 match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 163 146 [ true ⇒ 〈map, visited, the_graph〉 164 147  false ⇒ (* XXX: never visited here before *) 148 let visited ≝ insert … entry_point' true visited in 165 149 match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 166 150 [ sequential seq l ⇒ … … 169 153 pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited 170 154  COND acc_a cond_label ⇒ 171 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in 172 match size_counter with 173 [ O ⇒ ⊥ (* XXX: should never happen *) 174  S size_counter ⇒ 175 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels cond_label size_counter map visited in 176 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 177 〈map, visited, the_graph〉 178 ] 155 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 156 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) in 158 〈map, visited, the_graph〉 179 159  _ ⇒ 180 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labelsl size_counter map visited in160 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 181 161 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 182 162 〈map, visited, the_graph〉 … … 186 166 〈map, visited, the_graph〉 187 167  GOTO l ⇒ 188 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labelsl size_counter map visited in168 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in 189 169 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 190 170 〈map, visited, the_graph〉 … … 193 173 ] 194 174 ]. 195 [4: @(lookup … entry_point' visited false) 196 *: cases daemon 197 ] 175 cases daemon 198 176 qed. 199 177 … … 201 179 λparams1: params1. 202 180 λglobals: list ident. 203 λthe_graph: codeT globals (graph_params params1 globals). 204 λentry_point: label. 205 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] entry_point (graph_num_nodes … the_graph) (Stub …) (Stub …) in 206 〈map, the_graph〉. 181 λint_fun: joint_internal_function globals (graph_params params1 globals). 182 match joint_if_entry … int_fun with 183 [ dp entry entry_proof ⇒ 184 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 …) in 186 〈map, the_graph〉 187 ]. 207 188 208 189 let rec relabel_graph' … … 215 196  S size_counter ⇒ 216 197 let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in 217 let relabelled_entry_point ≝ an_identifier LabelTag ?in198 let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in 218 199 let statement ≝ lookup LabelTag ? the_graph entry_point in 219 200 match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with 220 201 [ None ⇒ ⊥ (* XXX: should not happen *) 221 202  Some statement ⇒ 222 let entered_previously ≝ ? in 223 let visited ≝ insert … entry_point' true visited in 203 let entered_previously ≝ (bvt_lookup … entry_point' visited false) in 224 204 match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with 225 205 [ true ⇒ the_graph 226 206  false ⇒ (* XXX: never visited here before *) 207 let visited ≝ insert … entry_point' true visited in 227 208 match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with 228 209 [ sequential seq l ⇒ … … 232 213 [ COND acc_a cond_label ⇒ 233 214 let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in 234 let relabelled ≝ an_identifier LabelTag ?in215 let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in 235 216 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in 236 217 〈tail_graph, COND … acc_a relabelled〉 … … 238 219 ] 239 220 in 240 match size_counter with 241 [ O ⇒ ⊥ (* XXX: impossible *) 242  S size_counter ⇒ 243 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in 244 let relabelled ≝ an_identifier LabelTag ? in 245 add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled) 246 ] 221 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') in 223 add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled) 247 224  RETURN ⇒ the_graph 248 225  GOTO l ⇒ 249 226 let l' ≝ match l with [ an_identifier l ⇒ l ] in 250 let relabelled ≝ an_identifier LabelTag ?in227 let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in 251 228 add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled) 252 229 ] … … 254 231 ] 255 232 ]. 256 [3: @(lookup … l' map l') 257 4: @(lookup … cond_label' map cond_label') 258 5: @(lookup … l' map l') 259 6: @(lookup … entry_point' visited false) 260 7: @(lookup … entry_point' map entry_point') 261 *: cases daemon 262 ] 233 cases daemon 263 234 qed. 264 235 265 236 definition relabel_graph ≝ 237 λglobals: list ident. 266 238 λparams1: params1. 267 λglobals: list ident.268 λthe_graph: codeT globals (graph_params params1 globals).269 λentry_point: label.270 239 λmap: BitVectorTrie Word 16. 271 relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph).272 273 definition pre_erase_graph_joint_internal_function ≝274 λparams1: params1.275 λglobals: list ident.276 240 λint_fun: joint_internal_function globals (graph_params params1 globals). 277 let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in 278 let runiverse ≝ joint_if_runiverse … int_fun in 279 let result ≝ joint_if_result … int_fun in 280 let params ≝ joint_if_params … int_fun in 281 let locals ≝ joint_if_locals … int_fun in 282 let stacksize ≝ joint_if_stacksize … int_fun in 283 let code ≝ joint_if_code … int_fun in 241 match joint_if_entry … int_fun with 242 [ dp entry entry_prf ⇒ 243 let code ≝ joint_if_code … int_fun in 244 relabel_graph' … code map (Stub …) entry (graph_num_nodes … code) 245 ]. 246 247 definition pre_erase_joint_internal_function ≝ 248 λglobals: list ident. 249 λ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. 252 λint_fun: joint_internal_function globals pars. 284 253 match joint_if_entry … int_fun with 285 254 [ dp entry entry_prf ⇒ 286 255 match joint_if_exit … int_fun with 287 256 [ dp exit exit_prf ⇒ 288 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in 289 let code ≝ relabel_graph params1 globals code entry maps in 290 mk_joint_internal_function … 291 luniverse runiverse result params 292 locals stacksize code entry exit 257 let exit' ≝ word_of_identifier … exit in 258 let entry' ≝ word_of_identifier … entry in 259 let 〈maps, code〉 ≝ erasure_function int_fun in 260 let int_fun ≝ set_joint_code globals pars int_fun code entry exit in 261 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')) 293 264 ] 294 265 ]. 295 266 cases daemon (* XXX *) 296 267 qed. 268 269 definition erase_graph_program: 270 ∀params1: params1. joint_program (graph_params params1) → joint_program (graph_params params1) ≝ 271 λparams1. 272 λprogram. 273 transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))). 274 275 definition erase_lin_program: lin_program → lin_program ≝ 276 λprogram. 277 transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_lin_internal_function …) (relabel_lin_internal_function …))).
Note: See TracChangeset
for help on using the changeset viewer.