Changeset 2960 for extracted/traces.ml
 Timestamp:
 Mar 26, 2013, 4:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/traces.ml
r2951 r2960 152 152 153 153 type evaluation_params = { globals : AST.ident List.list; 154 sparams : Joint_semantics.sem_params;155 154 ev_genv : Joint_semantics.genv } 156 155 157 156 (** val evaluation_params_rect_Type4 : 158 (AST.ident List.list > Joint_semantics.sem_params>157 Joint_semantics.sem_params > (AST.ident List.list > 159 158 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 160 let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_5953 = 161 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5953 162 in 163 h_mk_evaluation_params globals0 sparams0 ev_genv0 159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_55 = 160 let { globals = globals0; ev_genv = ev_genv0 } = x_55 in 161 h_mk_evaluation_params globals0 ev_genv0 164 162 165 163 (** val evaluation_params_rect_Type5 : 166 (AST.ident List.list > Joint_semantics.sem_params>164 Joint_semantics.sem_params > (AST.ident List.list > 167 165 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 168 let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_5955 = 169 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5955 170 in 171 h_mk_evaluation_params globals0 sparams0 ev_genv0 166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_57 = 167 let { globals = globals0; ev_genv = ev_genv0 } = x_57 in 168 h_mk_evaluation_params globals0 ev_genv0 172 169 173 170 (** val evaluation_params_rect_Type3 : 174 (AST.ident List.list > Joint_semantics.sem_params>171 Joint_semantics.sem_params > (AST.ident List.list > 175 172 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 176 let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_5957 = 177 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5957 178 in 179 h_mk_evaluation_params globals0 sparams0 ev_genv0 173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_59 = 174 let { globals = globals0; ev_genv = ev_genv0 } = x_59 in 175 h_mk_evaluation_params globals0 ev_genv0 180 176 181 177 (** val evaluation_params_rect_Type2 : 182 (AST.ident List.list > Joint_semantics.sem_params>178 Joint_semantics.sem_params > (AST.ident List.list > 183 179 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 184 let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_5959 = 185 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5959 186 in 187 h_mk_evaluation_params globals0 sparams0 ev_genv0 180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_61 = 181 let { globals = globals0; ev_genv = ev_genv0 } = x_61 in 182 h_mk_evaluation_params globals0 ev_genv0 188 183 189 184 (** val evaluation_params_rect_Type1 : 190 (AST.ident List.list > Joint_semantics.sem_params>185 Joint_semantics.sem_params > (AST.ident List.list > 191 186 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 192 let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_5961 = 193 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5961 194 in 195 h_mk_evaluation_params globals0 sparams0 ev_genv0 187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_63 = 188 let { globals = globals0; ev_genv = ev_genv0 } = x_63 in 189 h_mk_evaluation_params globals0 ev_genv0 196 190 197 191 (** val evaluation_params_rect_Type0 : 198 (AST.ident List.list > Joint_semantics.sem_params>192 Joint_semantics.sem_params > (AST.ident List.list > 199 193 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 200 let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_5963=201 let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5963202 in203 h_mk_evaluation_params globals0 sparams0 ev_genv0 204 205 (** val globals :evaluation_params > AST.ident List.list **)206 let rec globals xxx =194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_65 = 195 let { globals = globals0; ev_genv = ev_genv0 } = x_65 in 196 h_mk_evaluation_params globals0 ev_genv0 197 198 (** val globals : 199 Joint_semantics.sem_params > evaluation_params > AST.ident List.list **) 200 let rec globals p xxx = 207 201 xxx.globals 208 202 209 (** val sparams : evaluation_params > Joint_semantics.sem_params **) 210 let rec sparams xxx = 211 xxx.sparams 212 213 (** val ev_genv : evaluation_params > Joint_semantics.genv **) 214 let rec ev_genv xxx = 203 (** val ev_genv : 204 Joint_semantics.sem_params > evaluation_params > Joint_semantics.genv **) 205 let rec ev_genv p xxx = 215 206 xxx.ev_genv 216 207 217 208 (** val evaluation_params_inv_rect_Type4 : 218 evaluation_params > (AST.ident List.list > Joint_semantics.sem_params209 Joint_semantics.sem_params > evaluation_params > (AST.ident List.list 219 210 > Joint_semantics.genv > __ > 'a1) > 'a1 **) 220 let evaluation_params_inv_rect_Type4 hterm h1 =221 let hcut = evaluation_params_rect_Type4 h1 hterm in hcut __211 let evaluation_params_inv_rect_Type4 x1 hterm h1 = 212 let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __ 222 213 223 214 (** val evaluation_params_inv_rect_Type3 : 224 evaluation_params > (AST.ident List.list > Joint_semantics.sem_params215 Joint_semantics.sem_params > evaluation_params > (AST.ident List.list 225 216 > Joint_semantics.genv > __ > 'a1) > 'a1 **) 226 let evaluation_params_inv_rect_Type3 hterm h1 =227 let hcut = evaluation_params_rect_Type3 h1 hterm in hcut __217 let evaluation_params_inv_rect_Type3 x1 hterm h1 = 218 let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __ 228 219 229 220 (** val evaluation_params_inv_rect_Type2 : 230 evaluation_params > (AST.ident List.list > Joint_semantics.sem_params221 Joint_semantics.sem_params > evaluation_params > (AST.ident List.list 231 222 > Joint_semantics.genv > __ > 'a1) > 'a1 **) 232 let evaluation_params_inv_rect_Type2 hterm h1 =233 let hcut = evaluation_params_rect_Type2 h1 hterm in hcut __223 let evaluation_params_inv_rect_Type2 x1 hterm h1 = 224 let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __ 234 225 235 226 (** val evaluation_params_inv_rect_Type1 : 236 evaluation_params > (AST.ident List.list > Joint_semantics.sem_params227 Joint_semantics.sem_params > evaluation_params > (AST.ident List.list 237 228 > Joint_semantics.genv > __ > 'a1) > 'a1 **) 238 let evaluation_params_inv_rect_Type1 hterm h1 =239 let hcut = evaluation_params_rect_Type1 h1 hterm in hcut __229 let evaluation_params_inv_rect_Type1 x1 hterm h1 = 230 let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __ 240 231 241 232 (** val evaluation_params_inv_rect_Type0 : 242 evaluation_params > (AST.ident List.list > Joint_semantics.sem_params233 Joint_semantics.sem_params > evaluation_params > (AST.ident List.list 243 234 > Joint_semantics.genv > __ > 'a1) > 'a1 **) 244 let evaluation_params_inv_rect_Type0 hterm h1 = 245 let hcut = evaluation_params_rect_Type0 h1 hterm in hcut __ 235 let evaluation_params_inv_rect_Type0 x1 hterm h1 = 236 let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __ 237 238 (** val evaluation_params_discr : 239 Joint_semantics.sem_params > evaluation_params > evaluation_params > 240 __ **) 241 let evaluation_params_discr a1 x y = 242 Logic.eq_rect_Type2 x 243 (let { globals = a0; ev_genv = a10 } = x in 244 Obj.magic (fun _ dH > dH __ __)) y 246 245 247 246 (** val evaluation_params_jmdiscr : 248 evaluation_params > evaluation_params > __ **) 249 let evaluation_params_jmdiscr x y = 247 Joint_semantics.sem_params > evaluation_params > evaluation_params > 248 __ **) 249 let evaluation_params_jmdiscr a1 x y = 250 250 Logic.eq_rect_Type2 x 251 (let { globals = a0; sparams = a1; ev_genv = a2 } = x in 252 Obj.magic (fun _ dH > dH __ __ __)) y 253 254 (** val sparams__o__spp' : 255 evaluation_params > Joint_semantics.serialized_params **) 256 let sparams__o__spp' x0 = 257 x0.sparams.Joint_semantics.spp' 258 259 (** val sparams__o__spp'__o__msu_pars : 260 evaluation_params > Joint.joint_closed_internal_function 261 Joint_semantics.sem_unserialized_params **) 262 let sparams__o__spp'__o__msu_pars x0 = 263 Joint_semantics.spp'__o__msu_pars x0.sparams 264 265 (** val sparams__o__spp'__o__msu_pars__o__st_pars : 266 evaluation_params > Joint_semantics.sem_state_params **) 267 let sparams__o__spp'__o__msu_pars__o__st_pars x0 = 268 Joint_semantics.spp'__o__msu_pars__o__st_pars x0.sparams 269 270 (** val sparams__o__spp'__o__spp : evaluation_params > Joint.params **) 271 let sparams__o__spp'__o__spp x0 = 272 Joint_semantics.spp'__o__spp x0.sparams 273 274 (** val sparams__o__spp'__o__spp__o__stmt_pars : 275 evaluation_params > Joint.stmt_params **) 276 let sparams__o__spp'__o__spp__o__stmt_pars x0 = 277 Joint_semantics.spp'__o__spp__o__stmt_pars x0.sparams 278 279 (** val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars : 280 evaluation_params > Joint.uns_params **) 281 let sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 = 282 Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.sparams 283 284 (** val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : 285 evaluation_params > Joint.unserialized_params **) 286 let sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = 287 Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars 288 x0.sparams 251 (let { globals = a0; ev_genv = a10 } = x in 252 Obj.magic (fun _ dH > dH __ __)) y 253 254 (** val dpi1__o__ev_genv__o__inject : 255 Joint_semantics.sem_params > (evaluation_params, 'a1) Types.dPair > 256 Joint_semantics.genv Types.sig0 **) 257 let dpi1__o__ev_genv__o__inject x0 x2 = 258 x2.Types.dpi1.ev_genv 259 260 (** val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject : 261 Joint_semantics.sem_params > (evaluation_params, 'a1) Types.dPair > 262 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t 263 Types.sig0 **) 264 let dpi1__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 = 265 Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) 266 x2.Types.dpi1.globals x2.Types.dpi1.ev_genv 267 268 (** val dpi1__o__ev_genv__o__genv_to_genv_t : 269 Joint_semantics.sem_params > (evaluation_params, 'a1) Types.dPair > 270 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) 271 let dpi1__o__ev_genv__o__genv_to_genv_t x0 x2 = 272 let p = Joint_semantics.spp'__o__spp x0 in 273 let globals0 = x2.Types.dpi1.globals in 274 let g = x2.Types.dpi1.ev_genv in g.Joint_semantics.ge 275 276 (** val eject__o__ev_genv__o__inject : 277 Joint_semantics.sem_params > evaluation_params Types.sig0 > 278 Joint_semantics.genv Types.sig0 **) 279 let eject__o__ev_genv__o__inject x0 x2 = 280 (Types.pi1 x2).ev_genv 281 282 (** val eject__o__ev_genv__o__genv_to_genv_t__o__inject : 283 Joint_semantics.sem_params > evaluation_params Types.sig0 > 284 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t 285 Types.sig0 **) 286 let eject__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 = 287 Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) 288 (Types.pi1 x2).globals (Types.pi1 x2).ev_genv 289 290 (** val eject__o__ev_genv__o__genv_to_genv_t : 291 Joint_semantics.sem_params > evaluation_params Types.sig0 > 292 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) 293 let eject__o__ev_genv__o__genv_to_genv_t x0 x2 = 294 let p = Joint_semantics.spp'__o__spp x0 in 295 let globals0 = (Types.pi1 x2).globals in 296 let g = (Types.pi1 x2).ev_genv in g.Joint_semantics.ge 297 298 (** val ev_genv__o__genv_to_genv_t : 299 Joint_semantics.sem_params > evaluation_params > 300 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **) 301 let ev_genv__o__genv_to_genv_t x0 x1 = 302 let p = Joint_semantics.spp'__o__spp x0 in 303 let globals0 = x1.globals in let g = x1.ev_genv in g.Joint_semantics.ge 304 305 (** val ev_genv__o__genv_to_genv_t__o__inject : 306 Joint_semantics.sem_params > evaluation_params > 307 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t 308 Types.sig0 **) 309 let ev_genv__o__genv_to_genv_t__o__inject x0 x1 = 310 Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0) 311 x1.globals x1.ev_genv 312 313 (** val ev_genv__o__inject : 314 Joint_semantics.sem_params > evaluation_params > Joint_semantics.genv 315 Types.sig0 **) 316 let ev_genv__o__inject x0 x1 = 317 x1.ev_genv 318 319 (** val dpi1__o__ev_genv : 320 Joint_semantics.sem_params > (evaluation_params, 'a1) Types.dPair > 321 Joint_semantics.genv **) 322 let dpi1__o__ev_genv x0 x2 = 323 x2.Types.dpi1.ev_genv 324 325 (** val eject__o__ev_genv : 326 Joint_semantics.sem_params > evaluation_params Types.sig0 > 327 Joint_semantics.genv **) 328 let eject__o__ev_genv x0 x2 = 329 (Types.pi1 x2).ev_genv 289 330 290 331 type prog_params = { prog_spars : Joint_semantics.sem_params; … … 295 336 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 296 337 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 297 let rec prog_params_rect_Type4 h_mk_prog_params x_ 5979=338 let rec prog_params_rect_Type4 h_mk_prog_params x_81 = 298 339 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 299 stack_sizes0 } = x_ 5979340 stack_sizes0 } = x_81 300 341 in 301 342 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 304 345 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 305 346 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 306 let rec prog_params_rect_Type5 h_mk_prog_params x_ 5981=347 let rec prog_params_rect_Type5 h_mk_prog_params x_83 = 307 348 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 308 stack_sizes0 } = x_ 5981349 stack_sizes0 } = x_83 309 350 in 310 351 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 313 354 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 314 355 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 315 let rec prog_params_rect_Type3 h_mk_prog_params x_ 5983=356 let rec prog_params_rect_Type3 h_mk_prog_params x_85 = 316 357 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 317 stack_sizes0 } = x_ 5983358 stack_sizes0 } = x_85 318 359 in 319 360 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 322 363 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 323 364 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 324 let rec prog_params_rect_Type2 h_mk_prog_params x_ 5985=365 let rec prog_params_rect_Type2 h_mk_prog_params x_87 = 325 366 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 326 stack_sizes0 } = x_ 5985367 stack_sizes0 } = x_87 327 368 in 328 369 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 331 372 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 332 373 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 333 let rec prog_params_rect_Type1 h_mk_prog_params x_ 5987=374 let rec prog_params_rect_Type1 h_mk_prog_params x_89 = 334 375 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 335 stack_sizes0 } = x_ 5987376 stack_sizes0 } = x_89 336 377 in 337 378 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 340 381 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 341 382 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 342 let rec prog_params_rect_Type0 h_mk_prog_params x_ 5989=383 let rec prog_params_rect_Type0 h_mk_prog_params x_91 = 343 384 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 344 stack_sizes0 } = x_ 5989385 stack_sizes0 } = x_91 345 386 in 346 387 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 394 435 Obj.magic (fun _ dH > dH __ __ __)) y 395 436 396 (** val make_global : prog_params > evaluation_params **) 397 let make_global pars = 398 let p = pars.prog in 399 let spars = pars.prog_spars in 400 let genv = SemanticsUtils.joint_globalenv spars p in 401 let get_pc_lbl = fun id lbl > 402 Monad.m_bind0 (Monad.max_def Errors.res0) 403 (Obj.magic 404 (Joint_semantics.block_of_funct_id 405 (Joint_semantics.spp'__o__msu_pars__o__st_pars spars) genv id)) 406 (fun bl > 407 Obj.magic 408 (Joint_semantics.pc_of_label pars.prog_spars 409 (AST.prog_var_names p.Joint.joint_prog) genv bl lbl)) 410 in 411 { globals = (AST.prog_var_names p.Joint.joint_prog); sparams = spars; 412 ev_genv = { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = 413 pars.stack_sizes; Joint_semantics.get_pc_from_label = 414 (Obj.magic get_pc_lbl) } } 415 416 (** val prog_params_to_ev_params__o__sparams : 417 prog_params > Joint_semantics.sem_params **) 418 let prog_params_to_ev_params__o__sparams x0 = 419 (make_global x0).sparams 420 421 (** val prog_params_to_ev_params__o__sparams__o__spp' : 437 (** val prog_spars__o__spp' : 422 438 prog_params > Joint_semantics.serialized_params **) 423 let prog_ params_to_ev_params__o__sparams__o__spp' x0 =424 sparams__o__spp' (make_global x0)425 426 (** val prog_ params_to_ev_params__o__sparams__o__spp'__o__msu_pars :439 let prog_spars__o__spp' x0 = 440 x0.prog_spars.Joint_semantics.spp' 441 442 (** val prog_spars__o__spp'__o__msu_pars : 427 443 prog_params > Joint.joint_closed_internal_function 428 444 Joint_semantics.sem_unserialized_params **) 429 let prog_ params_to_ev_params__o__sparams__o__spp'__o__msu_pars x0 =430 sparams__o__spp'__o__msu_pars (make_global x0)431 432 (** val prog_ params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :445 let prog_spars__o__spp'__o__msu_pars x0 = 446 Joint_semantics.spp'__o__msu_pars x0.prog_spars 447 448 (** val prog_spars__o__spp'__o__msu_pars__o__st_pars : 433 449 prog_params > Joint_semantics.sem_state_params **) 434 let prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 = 435 sparams__o__spp'__o__msu_pars__o__st_pars (make_global x0) 436 437 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp : 438 prog_params > Joint.params **) 439 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp x0 = 440 sparams__o__spp'__o__spp (make_global x0) 441 442 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars : 450 let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 = 451 Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars 452 453 (** val prog_spars__o__spp'__o__spp : prog_params > Joint.params **) 454 let prog_spars__o__spp'__o__spp x0 = 455 Joint_semantics.spp'__o__spp x0.prog_spars 456 457 (** val prog_spars__o__spp'__o__spp__o__stmt_pars : 443 458 prog_params > Joint.stmt_params **) 444 let prog_ params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars x0 =445 sparams__o__spp'__o__spp__o__stmt_pars (make_global x0)446 447 (** val prog_ params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :459 let prog_spars__o__spp'__o__spp__o__stmt_pars x0 = 460 Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars 461 462 (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars : 448 463 prog_params > Joint.uns_params **) 449 let prog_ params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =450 sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars (make_global x0)451 452 (** val prog_ params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :464 let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 = 465 Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars 466 467 (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : 453 468 prog_params > Joint.unserialized_params **) 454 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = 455 sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars 456 (make_global x0) 469 let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = 470 Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars 471 x0.prog_spars 472 473 (** val joint_make_global : prog_params > evaluation_params **) 474 let joint_make_global p = 475 { globals = (AST.prog_var_names p.prog.Joint.joint_prog); ev_genv = 476 (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) } 477 478 (** val joint_make_global__o__ev_genv : 479 prog_params > Joint_semantics.genv **) 480 let joint_make_global__o__ev_genv x0 = 481 (joint_make_global x0).ev_genv 482 483 (** val joint_make_global__o__ev_genv__o__genv_to_genv_t : 484 prog_params > Joint.joint_closed_internal_function AST.fundef 485 Globalenvs.genv_t **) 486 let joint_make_global__o__ev_genv__o__genv_to_genv_t x0 = 487 ev_genv__o__genv_to_genv_t x0.prog_spars (joint_make_global x0) 488 489 (** val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject : 490 prog_params > Joint.joint_closed_internal_function AST.fundef 491 Globalenvs.genv_t Types.sig0 **) 492 let joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject x0 = 493 ev_genv__o__genv_to_genv_t__o__inject x0.prog_spars (joint_make_global x0) 494 495 (** val joint_make_global__o__ev_genv__o__inject : 496 prog_params > Joint_semantics.genv Types.sig0 **) 497 let joint_make_global__o__ev_genv__o__inject x0 = 498 ev_genv__o__inject x0.prog_spars (joint_make_global x0) 499 500 (** val joint_make_global__o__inject : 501 prog_params > evaluation_params Types.sig0 **) 502 let joint_make_global__o__inject x0 = 503 joint_make_global x0 457 504 458 505 (** val make_initial_state : prog_params > Joint_semantics.state_pc **) 459 506 let make_initial_state pars = 460 507 let p = pars.prog in 461 let sem_globals = make_global pars in 462 let ge = sem_globals.ev_genv in 508 let ge = ev_genv pars.prog_spars in 463 509 let m0 = 464 510 (Globalenvs.globalenv_allocmem (fun x > x) p.Joint.joint_prog).Types.snd … … 478 524 let main = p.Joint.joint_prog.AST.prog_main in 479 525 let st = { Joint_semantics.st_frms = (Types.Some 480 (prog_ params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars481 pars).Joint_semantics.empty_framesT); Joint_semantics.istack =482 Joint_semantics. Empty_is; Joint_semantics.carry = (ByteValues.BBbit483 Bool.False);Joint_semantics.regs =484 ((prog_ params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars485 pars).Joint_semantics.empty_regsT spp); Joint_semantics.m = m;486 Joint_semantics.stack_usage =globals_size }526 (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT); 527 Joint_semantics.istack = Joint_semantics.Empty_is; 528 Joint_semantics.carry = (ByteValues.BBbit Bool.False); 529 Joint_semantics.regs = 530 ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT 531 spp); Joint_semantics.m = m; Joint_semantics.stack_usage = 532 globals_size } 487 533 in 488 534 { Joint_semantics.st_no_pc = 489 (Joint_semantics.set_sp 490 (prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars 491 pars) spp st); Joint_semantics.pc = Joint_semantics.init_pc; 535 (Joint_semantics.set_sp (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) 536 spp st); Joint_semantics.pc = Joint_semantics.init_pc; 492 537 Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) })) __ 493 538 494 539 (** val joint_classify_step : 495 evaluation_params > Joint.joint_step > StructuredTraces.status_class **) 496 let joint_classify_step p = function 540 Joint.unserialized_params > AST.ident List.list > Joint.joint_step > 541 StructuredTraces.status_class **) 542 let joint_classify_step p g = function 497 543  Joint.COST_LABEL x > StructuredTraces.Cl_other 498 544  Joint.CALL (f, args, dest) > StructuredTraces.Cl_call … … 501 547 502 548 (** val joint_classify_final : 503 evaluation_params > Joint.joint_fin_step >549 Joint.unserialized_params > Joint.joint_fin_step > 504 550 StructuredTraces.status_class **) 505 551 let joint_classify_final p = function … … 509 555 510 556 (** val joint_classify : 511 evaluation_params > Joint_semantics.state_pc > 512 StructuredTraces.status_class **) 513 let joint_classify p st = 514 match Joint_semantics.fetch_statement p.sparams p.globals 515 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 516 let globals0 = p.globals in 517 let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with 557 Joint_semantics.sem_params > evaluation_params > 558 Joint_semantics.state_pc > StructuredTraces.status_class **) 559 let joint_classify p pars st = 560 match Joint_semantics.fetch_statement p pars.globals pars.ev_genv 561 st.Joint_semantics.pc with 518 562  Errors.OK i_fn_s > 519 563 (match i_fn_s.Types.snd with 520  Joint.Sequential (s, x) > joint_classify_step p s 521  Joint.Final s > joint_classify_final p s 564  Joint.Sequential (s, x) > 565 joint_classify_step 566 (Joint.uns_pars__o__u_pars 567 (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s 568  Joint.Final s > 569 joint_classify_final 570 (Joint.uns_pars__o__u_pars 571 (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s 522 572  Joint.FCOND (x0, x1, x2) > StructuredTraces.Cl_jump) 523 573  Errors.Error x > StructuredTraces.Cl_other 524 574 525 575 (** val joint_call_ident : 526 evaluation_params > Joint_semantics.state_pc > AST.ident **) 527 let joint_call_ident p st = 576 Joint_semantics.sem_params > evaluation_params > 577 Joint_semantics.state_pc > AST.ident **) 578 let joint_call_ident p pars st = 528 579 let dummy = Positive.One in 529 (match Joint_semantics.fetch_statement p.sparams p.globals 530 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 531 let globals0 = p.globals in 532 let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with 580 (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv 581 st.Joint_semantics.pc with 533 582  Errors.OK x > 534 583 (match x.Types.snd with … … 539 588 (match Obj.magic 540 589 (Monad.m_bind0 (Monad.max_def Errors.res0) 541 (Joint_semantics.block_of_call p .sparams p.globals542 (let p0 = Joint_semantics.spp'__o__spp p .sparamsin543 let globals0 = p .globals in544 let g = p .ev_genv in g.Joint_semantics.ge) f'590 (Joint_semantics.block_of_call p pars.globals 591 (let p0 = Joint_semantics.spp'__o__spp p in 592 let globals0 = pars.globals in 593 let g = pars.ev_genv in g.Joint_semantics.ge) f' 545 594 st.Joint_semantics.st_no_pc) (fun bl > 546 595 Obj.magic 547 (Joint_semantics.fetch_internal_function 548 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 549 let globals0 = p.globals in 550 let g = p.ev_genv in g.Joint_semantics.ge) bl))) with 596 (Joint_semantics.fetch_internal_function pars.globals 597 pars.ev_genv bl))) with 551 598  Errors.OK i_f > i_f.Types.fst 552 599  Errors.Error x0 > dummy) … … 558 605 559 606 (** val joint_tailcall_ident : 560 evaluation_params > Joint_semantics.state_pc > AST.ident **) 561 let joint_tailcall_ident p st = 607 Joint_semantics.sem_params > evaluation_params > 608 Joint_semantics.state_pc > AST.ident **) 609 let joint_tailcall_ident p pars st = 562 610 let dummy = Positive.One in 563 (match Joint_semantics.fetch_statement p.sparams p.globals 564 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 565 let globals0 = p.globals in 566 let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with 611 (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv 612 st.Joint_semantics.pc with 567 613  Errors.OK x > 568 614 (match x.Types.snd with … … 575 621 (match Obj.magic 576 622 (Monad.m_bind0 (Monad.max_def Errors.res0) 577 (Joint_semantics.block_of_call p .sparams p.globals578 (let p0 = Joint_semantics.spp'__o__spp p .sparamsin579 let globals0 = p .globals in580 let g = p .ev_genv in g.Joint_semantics.ge) f'623 (Joint_semantics.block_of_call p pars.globals 624 (let p0 = Joint_semantics.spp'__o__spp p in 625 let globals0 = pars.globals in 626 let g = pars.ev_genv in g.Joint_semantics.ge) f' 581 627 st.Joint_semantics.st_no_pc) (fun bl > 582 628 Obj.magic 583 (Joint_semantics.fetch_internal_function 584 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 585 let globals0 = p.globals in 586 let g = p.ev_genv in g.Joint_semantics.ge) bl))) with 629 (Joint_semantics.fetch_internal_function pars.globals 630 pars.ev_genv bl))) with 587 631  Errors.OK i_f > i_f.Types.fst 588 632  Errors.Error x0 > dummy)) … … 595 639 596 640 (** val cost_label_of_stmt : 597 evaluation_params > Joint.joint_statement > CostLabel.costlabel598 Types.option **)599 let cost_label_of_stmt p = function641 Joint_semantics.sem_params > evaluation_params > Joint.joint_statement 642 > CostLabel.costlabel Types.option **) 643 let cost_label_of_stmt p pars = function 600 644  Joint.Sequential (s0, x) > 601 645 (match s0 with … … 608 652 609 653 (** val joint_label_of_pc : 610 evaluation_params > ByteValues.program_counter > CostLabel.costlabel 611 Types.option **) 612 let joint_label_of_pc p pc = 613 match Joint_semantics.fetch_statement p.sparams p.globals 614 (let p0 = Joint_semantics.spp'__o__spp p.sparams in 615 let globals0 = p.globals in 616 let g = p.ev_genv in g.Joint_semantics.ge) pc with 617  Errors.OK fn_stmt > cost_label_of_stmt p fn_stmt.Types.snd 654 Joint_semantics.sem_params > evaluation_params > 655 ByteValues.program_counter > CostLabel.costlabel Types.option **) 656 let joint_label_of_pc p pars pc = 657 match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with 658  Errors.OK fn_stmt > cost_label_of_stmt p pars fn_stmt.Types.snd 618 659  Errors.Error x > Types.None 619 660 … … 624 665 625 666 (** val joint_final : 626 Joint_semantics.sem_params > AST.ident List.list > Joint_semantics.genv 627 > Joint_semantics.state_pc > Integers.int Types.option **) 628 let joint_final p globals0 ge st = 629 match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with 630  Bool.True > 631 let ret = 632 (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main 633 in 634 Errors.res_to_opt 635 (Obj.magic 636 (Monad.m_bind0 (Monad.max_def Errors.res0) 637 (Obj.magic 638 (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result 639 globals0 640 (let p0 = Joint_semantics.spp'__o__spp p in 641 let globals1 = globals0 in let g = ge in g.Joint_semantics.ge) 642 ret st.Joint_semantics.st_no_pc)) (fun vals > 643 Obj.magic (ByteValues.word_of_list_beval vals)))) 644  Bool.False > Types.None 667 Joint_semantics.sem_params > evaluation_params > 668 Joint_semantics.state_pc > Integers.int Types.option **) 669 let joint_final p pars st = 670 let ge = pars.ev_genv in 671 (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with 672  Bool.True > 673 let ret = 674 (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main 675 in 676 Errors.res_to_opt 677 (Obj.magic 678 (Monad.m_bind0 (Monad.max_def Errors.res0) 679 (Obj.magic 680 (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result 681 pars.globals 682 (let p0 = Joint_semantics.spp'__o__spp p in 683 let globals0 = pars.globals in 684 let g = ge in g.Joint_semantics.ge) ret 685 st.Joint_semantics.st_no_pc)) (fun vals > 686 Obj.magic (ByteValues.word_of_list_beval vals)))) 687  Bool.False > Types.None) 645 688 646 689 (** val joint_abstract_status : … … 649 692 { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of = 650 693 (Obj.magic 651 (Joint_semantics.pc 652 (prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars 653 p))); StructuredTraces.as_classify = 654 (Obj.magic (joint_classify (make_global p))); 694 (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p))); 695 StructuredTraces.as_classify = 696 (Obj.magic (joint_classify p.prog_spars (joint_make_global p))); 655 697 StructuredTraces.as_label_of_pc = 656 (Obj.magic (joint_label_of_pc (make_global p)));698 (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p))); 657 699 StructuredTraces.as_result = 658 (Obj.magic 659 (joint_final (prog_params_to_ev_params__o__sparams p) 660 (make_global p).globals (make_global p).ev_genv)); 700 (Obj.magic (joint_final p.prog_spars (joint_make_global p))); 661 701 StructuredTraces.as_call_ident = (fun st > 662 joint_call_ident (make_global p) (Types.pi1 (Obj.magic st))); 663 StructuredTraces.as_tailcall_ident = (fun st > 664 joint_tailcall_ident (make_global p) (Types.pi1 (Obj.magic st))) } 702 joint_call_ident p.prog_spars (joint_make_global p) 703 (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident = 704 (fun st > 705 joint_tailcall_ident p.prog_spars (joint_make_global p) 706 (Types.pi1 (Obj.magic st))) } 665 707 666 708 (** val joint_status :
Note: See TracChangeset
for help on using the changeset viewer.