 Timestamp:
 Oct 27, 2011, 3:36:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/ProofUtils.ma
r1467 r1469 141 141 142 142 let rec pre_erase_graph_internal_function' 143 (params1: params1) (sem_params: sem_params) (globals: list ident) 144 (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals)) 145 (labels: list label) (num_nodes: nat) 146 on num_nodes: ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) ≝ 147 match num_nodes return λn. ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) with 143 (params1: params1) (globals: list ident) 144 (the_graph: codeT globals (graph_params params1 globals)) (labels: list label) 145 (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16) 146 (visited: BitVectorTrie bool 16) 147 on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝ 148 match size_counter return λ_. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 148 149 [ O ⇒ 149 150 match labels with 150 [ nil ⇒ 〈 Stub Word 16, empty_graph …〉151 [ nil ⇒ 〈map, visited, the_graph〉 151 152  _ ⇒ ⊥ 152 153 ] 153  S num_nodes ⇒ 154 let program_counter ≝ (pc … state) in 155 match code_pointer_of_address program_counter with 156 [ OK code_pointer ⇒ 157 match graph_label_of_pointer code_pointer with 158 [ OK lbl ⇒ 159 match lookup … the_graph lbl with 160 [ Some statement ⇒ 161 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 162 let state ≝ set_pc … program_counter state in 163 match statement with 164 [ sequential seq l ⇒ 165 match seq with 166 [ COST_LABEL cost_label ⇒ pre_erase_graph_internal_function' params1 sem_params globals state the_graph (lbl :: labels) num_nodes 167  _ ⇒ 168 let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in 169 let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in 170 〈maps, instructions〉 154  S size_counter ⇒ 155 let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in 156 let statement ≝ lookup LabelTag ? the_graph entry_point in 157 match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 158 [ None ⇒ ⊥ (* XXX: should not happen *) 159  Some statement ⇒ 160 let visited ≝ insert … entry_point' true visited in 161 let entered_previously ≝ ? in 162 match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 163 [ true ⇒ 〈map, visited, the_graph〉 164  false ⇒ (* XXX: never visited here before *) 165 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 [ sequential seq l ⇒ 167 match seq with 168 [ COST_LABEL cost_label ⇒ 169 pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited 170  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〉 171 178 ] 172  _ ⇒ 173 let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in 174 let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in 175 〈maps, instructions〉 176 ] 177  None ⇒ ⊥ (* XXX: shouldn't happen *) 179  _ ⇒ 180 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in 181 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 182 〈map, visited, the_graph〉 178 183 ] 179  Error message ⇒ ⊥ (* XXX: shouldn't happen *) 184  RETURN ⇒ 185 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 186 〈map, visited, the_graph〉 187  GOTO l ⇒ 188 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in 189 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in 190 〈map, visited, the_graph〉 180 191 ] 181  Error message ⇒ ⊥ (* XXX: shouldn't happen *)182 192 ] 183 ]. 184 cases daemon (* XXX *) 193 ] 194 ]. 195 [4: @(lookup … entry_point' visited false) 196 *: cases daemon 197 ] 185 198 qed. 186 199 187 200 definition pre_erase_graph_internal_function ≝ 188 201 λparams1: params1. 189 λsem_params: sem_params. 190 λglobals: list ident. 191 λstate: state sem_params. 202 λglobals: list ident. 192 203 λthe_graph: codeT globals (graph_params params1 globals). 193 λlabels: list label. 194 pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels (graph_num_nodes … the_graph). 195 196 let rec relabel_graph' 197 (params1: params1) (sem_params: sem_params) (globals: list ident) 198 (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals)) 199 (map: BitVectorTrie Word 16) (num_nodes: nat) 200 on num_nodes: codeT globals (graph_params params1 globals) ≝ 201 match num_nodes with 202 [ O ⇒ empty_graph … 203  S num_nodes ⇒ 204 let program_counter ≝ (pc … state) in 205 match code_pointer_of_address program_counter with 206 [ OK code_pointer ⇒ 207 match graph_label_of_pointer code_pointer with 208 [ OK lbl ⇒ 209 match lookup … the_graph lbl with 210 [ Some statement ⇒ 211 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 212 let new_statement ≝ relabel_joint_statement globals (graph_params params1 globals) map statement in 213 let new_lbl ≝ an_identifier LabelTag ? in 214 let state' ≝ set_pc … program_counter state in 215 let tail_graph ≝ relabel_graph' params1 sem_params globals state' the_graph map num_nodes in 216 add … tail_graph new_lbl new_statement 217  None ⇒ ⊥ 218 ] 219  Error message ⇒ ⊥ 220 ] 221  Error message ⇒ ⊥ 222 ] 223 ]. 224 [2: @(lookup … lbl' map lbl') 225 *: cases daemon (* XXX *) 226 ] 227 qed. 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〉. 207 208 axiom relabel_graph': 209 ∀params1: params1. 210 ∀globals: list ident. 211 ∀the_graph: codeT globals (graph_params params1 globals). 212 ∀map: BitVectorTrie Word 16. 213 ∀visited: BitVectorTrie bool 16. 214 ∀num_nodes: nat. 215 codeT globals (graph_params params1 globals). 228 216 229 217 definition relabel_graph ≝ 230 λparams1. 231 λsem_params. 232 λglobals. 233 λstate: state sem_params. 218 λparams1: params1. 219 λglobals: list ident. 234 220 λthe_graph: codeT globals (graph_params params1 globals). 235 221 λmap: BitVectorTrie Word 16. 236 relabel_graph' params1 sem_params globals state the_graph map(graph_num_nodes … the_graph).222 relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph). 237 223 238 224 definition pre_erase_graph_joint_internal_function ≝ 239 225 λparams1: params1. 240 λsem_params: sem_params. 241 λglobals: list ident. 242 λstate: state sem_params. 226 λglobals: list ident. 243 227 λint_fun: joint_internal_function globals (graph_params params1 globals). 244 228 let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in … … 253 237 match joint_if_exit … int_fun with 254 238 [ dp exit exit_prf ⇒ 255 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ]in256 let code ≝ relabel_graph params1 sem_params globals statecode maps in239 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in 240 let code ≝ relabel_graph params1 globals code maps in 257 241 mk_joint_internal_function … 258 242 luniverse runiverse result params … … 262 246 cases daemon (* XXX *) 263 247 qed. 264 265 (* XXX: use make_initial_state to build an initial state for a program *)
Note: See TracChangeset
for help on using the changeset viewer.