Changeset 2076 for src/Clight
 Timestamp:
 Jun 14, 2012, 10:30:21 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2016 r2076 2 2 include "Clight/fresh.ma". 3 3 include "basics/lists/list.ma". 4 5 (* This file implements transformation of switches to linear, nested sequences of 4 include "common/Identifiers.ma". 5 include "Clight/Cexec.ma". 6 include "Clight/CexecInd.ma". 7 8 (*  9 *) 10 11 (*  12 Documentation 13 *) 14 15 (* This file implements transformation of switches to linear sequences of 6 16 * if/then/else. The implementation roughly follows the lines of the prototype. 7 17 * /!\ We assume that the program is welltyped (the type of the evaluated 8 18 * expression must match the constants on each branch of the switch). /!\ *) 19 20 (* Documentation. Let the follwing be our input switch construct: 21 //  22 switch(e) { 23 case v1: 24 stmt1 25 case v2: 26 stmt2 27 . 28 . 29 . 30 default: 31 stmt_default 32 } 33 //  34 35 Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting 36 the switch statement. In the absence of break, the execution falls through each case sequentially. 37 38 Given such a statement, we produce an equivalent sequence of ifthenelses chained by gotos: 39 40 //  41 fresh = e; 42 if(fresh == v1) { 43 stmt1'; 44 goto lbl_case2; 45 } 46 if(fresh == v2) { 47 lbl_case2: 48 stmt2'; 49 goto lbl_case2; 50 } 51 ... 52 stmt_default'; 53 exit_label: 54 //  55 56 where stmt1', stmt2', ... stmt_default' are the statements where all toplevel [break] statements 57 were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. 58 *) 59 60 61 (*  62 Definitions allowing to state that the program resulting of the transformation 63 is switchfree. The actual proof is done using Russell. 64 *) 9 65 10 66 (* Property of a Clight statement of containing no switch. Could be generalized into a kind of … … 54 110 ]. 55 111 112 113 (*  114 Switchremoval code for statements, functions and fundefs. 115 *) 116 117 (* Given a list of switch cases, prefixes each case by a fresh goto label. It is 118 assumed as an hypothesis that each substatement is already switchfree 119 (argument [H]). The whole function returns a list of labelled switchfree switch 120 cases, along the particular label of the default statement and its associated 121 statement. A fresh label generator [uv] is threaded through the function. *) 56 122 let rec add_starting_lbl_list 57 123 (l : labeled_statements) … … 74 140 ] qed. 75 141 142 (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) 76 143 let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ 77 144 match st with … … 91 158 ]. 92 159 160 (* Converting breaks preserves switchfreeness. *) 93 161 lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). 94 162 #s elim s // … … 101 169 ] qed. 102 170 103 (* We assume that the expression e is consistely typed w.r.t. the switch branches*)171 (* Obsolete. This version generates a nested pseudosequence of ifthenelses. *) 104 172 let rec produce_cond 105 173 (e : expr) … … 137 205 ] qed. 138 206 207 (* We assume that the expression e is consistely typed w.r.t. the switch branches *) 139 208 let rec produce_cond2 140 209 (e : expr) … … 169 238  2: elim sub_statement // ] 170 239 ] qed. 171 172 173 240 174 241 (* takes an expression, a list of switchfree cases and a freshgen and returns a … … 189 256 let rec switch_removal 190 257 (st : statement) 191 (vars : list (ident × type))192 258 (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝ 193 259 match st return λs.s = st → ? with 194 [ Sskip ⇒ λEq. 〈«st,?», vars, uv〉195  Sassign _ _ ⇒ λEq. 〈«st,?», vars, uv〉196  Scall _ _ _ ⇒ λEq. 〈«st,?», vars, uv〉260 [ Sskip ⇒ λEq. 〈«st,?», [ ], uv〉 261  Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 262  Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 197 263  Ssequence s1 s2 ⇒ λEq. 198 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 varsuv in199 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1uv' in200 〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars 2, uv''〉264 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 265 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 266 〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 201 267  Sifthenelse e s1 s2 ⇒ λEq. 202 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 varsuv in203 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1uv' in204 〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars 2, uv''〉268 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 269 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 270 〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 205 271  Swhile e body ⇒ λEq. 206 let 〈body', vars', uv'〉 ≝ switch_removal body varsuv in272 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 207 273 〈«Swhile e (pi1 … body'),?», vars', uv'〉 208 274  Sdowhile e body ⇒ λEq. 209 let 〈body', vars', uv'〉 ≝ switch_removal body varsuv in275 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 210 276 〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 211 277  Sfor s1 e s2 s3 ⇒ λEq. 212 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 varsuv in213 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1uv' in214 let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 vars2 uv'' in215 〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars 3, uv'''〉278 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 279 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 280 let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in 281 〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉 216 282  Sbreak ⇒ λEq. 217 〈«st,?», vars, uv〉283 〈«st,?», [ ], uv〉 218 284  Scontinue ⇒ λEq. 219 〈«st,?», vars, uv〉285 〈«st,?», [ ], uv〉 220 286  Sreturn _ ⇒ λEq. 221 〈«st,?», vars, uv〉287 〈«st,?», [ ], uv〉 222 288  Sswitch e branches ⇒ λEq. 223 let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches varsuv in289 let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in 224 290 match sf_branches with 225 291 [ mk_Sig branches' H ⇒ … … 231 297 ] 232 298  Slabel label body ⇒ λEq. 233 let 〈body', vars', uv'〉 ≝ switch_removal body varsuv in299 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 234 300 〈«Slabel label (pi1 … body'), ?», vars', uv'〉 235 301  Sgoto _ ⇒ λEq. 236 〈«st, ?», vars, uv〉302 〈«st, ?», [ ], uv〉 237 303  Scost cost body ⇒ λEq. 238 let 〈body', vars', uv'〉 ≝ switch_removal body varsuv in304 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 239 305 〈«Scost cost (pi1 … body'),?», vars', uv'〉 240 306 ] (refl ? st) … … 242 308 and switch_removal_branches 243 309 (l : labeled_statements) 244 (vars : list (ident × type))245 310 (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝ 246 311 match l with 247 312 [ LSdefault st ⇒ 248 let 〈st, vars', uv'〉 ≝ switch_removal st varsuv in313 let 〈st, vars', uv'〉 ≝ switch_removal st uv in 249 314 〈«LSdefault (pi1 … st), ?», vars', uv'〉 250 315  LScase sz int st tl => 251 let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl varsuv in252 let 〈st', vars'', uv''〉 ≝ switch_removal st vars'uv' in253 〈«LScase sz int st' (pi1 … tl_result), ?», vars' ', uv''〉316 let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in 317 let 〈st', vars'', uv''〉 ≝ switch_removal st uv' in 318 〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉 254 319 ]. 255 320 try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try // … … 261 326 ] qed. 262 327 328 definition function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝ 329 λf,u. 330 let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in 331 let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in 332 〈f, u'〉. 333 334 let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝ 335 match f with 336 [ CL_Internal f ⇒ 337 let 〈f',u'〉 ≝ function_switch_removal f u in 338 〈CL_Internal f', u'〉 339  CL_External _ _ _ ⇒ 340 〈f, u〉 341 ]. 342 343 344 (*  345 Switchremoval code for programs. 346 *) 347 348 (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to 349 * name clashes for labels. We have no choice but to actually run through the function and to 350 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and 351 * fresh labels using the same univ. While we're at it we also consider record fields. 352 * Cost labels are not considered, though. They already live in a separate universe. 353 * 354 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, 355 * but in the end it might be good to move the following functions into fresh.ma. 356 *) 357 358 (* This is certainly overkill: variables adressed in an expression should be declared in the 359 * enclosing function's prototype. *) 360 let rec max_of_expr (e : expr) (current : ident) : ident ≝ 361 match e with 362 [ Expr ed _ ⇒ 363 match ed with 364 [ Econst_int _ _ ⇒ current 365  Econst_float _ ⇒ current 366  Evar id ⇒ max_id id current 367  Ederef e1 ⇒ max_of_expr e1 current 368  Eaddrof e1 ⇒ max_of_expr e1 current 369  Eunop _ e1 ⇒ max_of_expr e1 current 370  Ebinop _ e1 e2 ⇒ max_of_expr e1 (max_of_expr e2 current) 371  Ecast _ e1 ⇒ max_of_expr e1 current 372  Econdition e1 e2 e3 ⇒ 373 max_of_expr e1 (max_of_expr e2 (max_of_expr e3 current)) 374  Eandbool e1 e2 ⇒ 375 max_of_expr e1 (max_of_expr e2 current) 376  Eorbool e1 e2 ⇒ 377 max_of_expr e1 (max_of_expr e2 current) 378  Esizeof _ ⇒ current 379  Efield r f ⇒ max_id f (max_of_expr r current) 380  Ecost _ e1 ⇒ max_of_expr e1 current 381 ] 382 ]. 383 384 (* Reeasoning about this promises to be a serious pain. Especially the Scall case. *) 385 let rec max_of_statement (s : statement) (current : ident) : ident ≝ 386 match s with 387 [ Sskip ⇒ current 388  Sassign e1 e2 ⇒ max_of_expr e2 (max_of_expr e1 current) 389  Scall ret f args ⇒ 390 let retmax ≝ 391 match ret with 392 [ None ⇒ current 393  Some e ⇒ max_of_expr e current ] 394 in 395 foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args 396  Ssequence s1 s2 ⇒ 397 max_of_statement s1 (max_of_statement s2 current) 398  Sifthenelse e s1 s2 ⇒ 399 max_of_expr e (max_of_statement s1 (max_of_statement s2 current)) 400  Swhile e body ⇒ 401 max_of_expr e (max_of_statement body current) 402  Sdowhile e body ⇒ 403 max_of_expr e (max_of_statement body current) 404  Sfor init test incr body ⇒ 405 max_of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current))) 406  Sbreak ⇒ current 407  Scontinue ⇒ current 408  Sreturn opt ⇒ 409 match opt with 410 [ None ⇒ current 411  Some e ⇒ max_of_expr e current 412 ] 413  Sswitch e ls ⇒ 414 max_of_expr e (max_of_ls ls current) 415  Slabel lab body ⇒ 416 max_id lab (max_of_statement body current) 417  Sgoto lab ⇒ 418 max_id lab current 419  Scost _ body ⇒ 420 max_of_statement body current 421 ] 422 and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝ 423 match ls with 424 [ LSdefault s ⇒ max_of_statement s current 425  LScase _ _ s ls' ⇒ max_of_ls ls' (max_of_statement s current) 426 ]. 427 428 definition max_id_of_function : function → ident ≝ 429 λf. max_of_statement (fn_body f) (max_id_of_fn f). 430 431 definition max_id_of_fundef_deep : clight_fundef → ident ≝ 432 λf. match f with 433 [ CL_Internal f ⇒ max_id_of_function f 434  CL_External id _ _ ⇒ id 435 ]. 436 437 let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝ 438 let func_max ≝ 439 foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs 440 in max_id func_max current. 441 442 definition max_id_of_program_deep : clight_program → ident ≝ 443 λp. 444 max_id 445 (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p)) 446 (max_id_of_globvars (prog_vars ?? p)). 447 448 (* The previous functions compute an (over?)approximation of the identifiers and labels. 449 The following function builds a "good" universe for a complete clight program. *) 450 definition universe_for_program_deep : clight_program → universe SymbolTag ≝ 451 λp. universe_of_max (max_id_of_program_deep p). 452 453 263 454 let rec program_switch_removal (p : clight_program) : clight_program ≝ 264 let uv ≝ universe_for_program p in455 let uv ≝ universe_for_program_deep p in 265 456 let prog_funcs ≝ prog_funct ?? p in 266 457 let 〈sf_funcs, final_uv〉 ≝ 267 458 foldr ?? (λcl_fundef.λacc. 268 let 〈fundefs, uv1〉 ≝ acc in 459 let 〈fundefs, uv1〉 ≝ acc in 269 460 let 〈fun_id, fun_def〉 ≝ cl_fundef in 270 match fun_def with 271 [ CL_Internal func ⇒ 272 let 〈body', fun_vars, uv2〉 ≝ switch_removal (fn_body func) (fn_vars func) uv1 in 273 let new_func ≝ mk_function (fn_return func) (fn_params func) fun_vars (pi1 … body') in 274 〈(〈fun_id, CL_Internal new_func〉 :: fundefs), uv2〉 275  CL_External _ _ _ ⇒ 276 〈cl_fundef :: fundefs, uv1〉 277 ] 461 let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in 462 〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉 278 463 ) 〈[ ], uv〉 prog_funcs 279 464 in … … 283 468 (prog_main … p). 284 469 285 286 287 288 289 290 291 292 293 470 (*  471 Simulation proof and related voodoo. 472 *) 473 474 (* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *) 475 inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ 476  SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 477  SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. 478 479 definition expr_lvalue_ind_combined ≝ 480 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. 481 conj ?? 482 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) 483 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). 484 485 let rec expr_ind2 486 (P : expr → Prop) (Q : expr_descr → type → Prop) 487 (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) 488 (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) 489 (Iconst_float : ∀f, t. Q (Econst_float f) t) 490 (Ivar : ∀id, t. Q (Evar id) t) 491 (Ideref : ∀e, t. P e → Q (Ederef e) t) 492 (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) 493 (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) 494 (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) 495 (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) 496 (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) 497 (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) 498 (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) 499 (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) 500 (Ifield : ∀e,f,t. P e → Q (Efield e f) t) 501 (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 502 (e : expr) on e : P e ≝ 503 match e with 504 [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ] 505 506 and expr_desc_ind2 507 (P : expr → Prop) (Q : expr_descr → type → Prop) 508 (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) 509 (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) 510 (Iconst_float : ∀f, t. Q (Econst_float f) t) 511 (Ivar : ∀id, t. Q (Evar id) t) 512 (Ideref : ∀e, t. P e → Q (Ederef e) t) 513 (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) 514 (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) 515 (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) 516 (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) 517 (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) 518 (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) 519 (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) 520 (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) 521 (Ifield : ∀e,f,t. P e → Q (Efield e f) t) 522 (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 523 (ed : expr_descr) (t : type) on ed : Q ed t ≝ 524 match ed with 525 [ Econst_int sz i ⇒ Iconst_int sz i t 526  Econst_float f ⇒ Iconst_float f t 527  Evar id ⇒ Ivar id t 528  Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 529  Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 530  Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 531  Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 532  Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 533  Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) 534  Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 535  Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 536  Esizeof sizeoft ⇒ Isizeof sizeoft t 537  Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 538  Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 539 ]. 540 541 (* Correctness: we can't use a lockstep simulation result. The exec_step for Sswitch will be matched 542 by a nonconstant number of evaluations in the converted program. More precisely, 543 [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps 544 necessary to execute all the "ifthenelses" corresponding to cases /before/ [n]. *) 545 546 (* A version of simplify_switch hiding the ugly proj *) 547 definition sw_rem : statement → (universe SymbolTag) → statement ≝ 548 λs,u. 549 \fst (\fst (switch_removal s u)). 550 551 definition fresh_for_expression ≝ 552 λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u. 553 554 definition fresh_for_statement ≝ 555 λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u. 556 557 definition fresh_for_function ≝ 558 λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. 559 560 let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝ 561 match k with 562 [ Kstop ⇒ True 563  Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u) 564  Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) 565  Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) 566  Kfor2 e s1 s2 k0 ⇒ 567 (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ 568 (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) 569  Kfor3 e s1 s2 k0 ⇒ 570 (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ 571 (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) 572  Kswitch k0 ⇒ fresh_for_continuation k0 u 573  Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u) 574 ]. 575 576 inductive switch_cont_sim : cont → cont → Prop ≝ 577  swc_stop : 578 switch_cont_sim Kstop Kstop 579  swc_seq : ∀s,k,k',u. 580 fresh_for_statement s u → 581 switch_cont_sim k k' → 582 switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k') 583  swc_while : ∀e,s,k,k',u. 584 fresh_for_expression e u → 585 fresh_for_statement s u → 586 switch_cont_sim k k' → 587 switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k') 588  swc_dowhile : ∀e,s,k,k',u. 589 fresh_for_expression e u → 590 fresh_for_statement s u → 591 switch_cont_sim k k' → 592 switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k') 593  swc_for1 : ∀e,s1,s2,k,k',u1,u2. 594 fresh_for_statement s1 u1 → 595 fresh_for_statement s2 u2 → 596 switch_cont_sim k k' → 597 switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k') 598  swc_for2 : ∀e,s1,s2,k,k',u1,u2. 599 fresh_for_statement s1 u1 → 600 fresh_for_statement s2 u2 → 601 switch_cont_sim k k' → 602 switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k') 603  swc_for3 : ∀e,s1,s2,k,k',u1,u2. 604 fresh_for_statement s1 u1 → 605 fresh_for_statement s2 u2 → 606 switch_cont_sim k k' → 607 switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k') 608  swc_switch : ∀k,k'. 609 switch_cont_sim k k' → 610 switch_cont_sim (Kswitch k) (Kswitch k') 611  swc_call : ∀r,f,en,k,k',u. 612 fresh_for_function f u → 613 switch_cont_sim k k' → 614 switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k'). 615 616 617 inductive switch_state_sim : state → state → Prop ≝ 618  sws_state : ∀uf,us,uk,f,s,k,k',e,m. 619 fresh_for_function f uf → 620 fresh_for_statement s us → 621 fresh_for_continuation k' uk → 622 switch_cont_sim k k' → 623 switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m) 624 (* Extra matching states that we can reach that don't quite correspond to the 625 labelling function *) 626 (* 627  sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 628 switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 629  sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 630 switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 631  sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 632 switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 633 *) 634 (* and the rest *) 635  sws_callstate : ∀ufd,fd,args,k,k',m. 636 switch_cont_sim k k' → 637 switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m) 638  sws_returnstate : ∀res,k,k',m. 639 switch_cont_sim k k' → 640 switch_state_sim (Returnstate res k m) (Returnstate res k' m) 641  sws_finalstate : ∀r. 642 switch_state_sim (Finalstate r) (Finalstate r) 643 . 644 645 inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ 646  eventually_base : ∀s,t,s'. 647 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 648 P s' → 649 eventually ge P s t 650  eventually_step : ∀s,t,s',t'. 651 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 652 eventually ge P s' t' → 653 eventually ge P s (t ⧺ t'). 654 655 (* [eventually] is not so nice to use directly, we would like to make the mandatory 656 * [exec_step ge s = Value ??? 〈t, s'] visible  and in the end we would like not 657 to give [s'] ourselves, but matita to compute it. Hence this little introwrapper. *) 658 lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 659 eventually ge P s t. 660 #ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP} 661 qed. 662 663 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 664 rg_find_symbol: ∀s. 665 find_symbol ? ge s = find_symbol ? ge' s; 666 rg_find_funct: ∀v,f. 667 find_funct ? ge v = Some ? f → 668 find_funct ? ge' v = Some ? (t f); 669 rg_find_funct_ptr: ∀b,f. 670 find_funct_ptr ? ge b = Some ? f → 671 find_funct_ptr ? ge' b = Some ? (t f) 672 }. 673 674 (* TODO ... fundef_switch_removal wants a universe which is freshforits argument. *) 675 (* 676 lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' → 677 (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ 678 (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). 679 *) 680 681 (* The return type of any function is invariant under switch removal *) 682 lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f. 683 #f #u elim f #ret #args #vars #body normalize elim (switch_removal body u) 684 * * #body' #Hswitch_free #new_vars #u' normalize // 685 qed. 686 687 lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0). 688 #e0 #s0 #us0 normalize 689 cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize // 690 qed. 691 692 lemma max_one_neutral : ∀v. max v one = v. 693 * // qed. 694 695 lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. 696 * #p whd in ⊢ (??%?); >max_one_neutral // qed. 697 698 lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. 699 * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); 700 >commutative_max // qed. 701 702 lemma transitive_le : transitive ? le. // qed. 703 704 lemma le_S_weaken : ∀a,b. le (succ a) b → le a b. 705 #a #b /2/ qed. 706 707 (* cycle of length 1 *) 708 lemma le_S_contradiction_1 : ∀a. le (succ a) a → False. 709 * /2 by absurd/ qed. 710 711 (* cycle of length 2 *) 712 lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False. 713 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) 714 #Heq @(le_S_contradiction_1 a) destruct // qed. 715 716 (* cycle of length 3 *) 717 lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False. 718 #a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4 719 @(le_S_contradiction_2 … H3 H4) 720 qed. 721 722 lemma reflexive_leb : ∀a. leb a a = true. 723 #a @(le_to_leb_true a a) // qed. 724 725 (* 726 lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False. 727 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq 728 destruct inversion H2 729 [ 2: #m #H1 #H2 #H3 730 elim b; normalize in match (succ ?); 731 [ 1: #H destruct (H) 732  2: #p #H 733 *) 734 (* This should be somewhere else. *) 735 lemma associative_max : associative ? max. 736 #a #b #c 737 whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c); 738 lapply (pos_compare_to_Prop a b) 739 cases (pos_compare a b) whd in ⊢ (% → ?); #Hab 740 [ 1: >(le_to_leb_true a b) normalize nodelta /2/ 741 lapply (pos_compare_to_Prop b c) 742 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 743 [ 1: >(le_to_leb_true b c) normalize nodelta 744 lapply (pos_compare_to_Prop a c) 745 cases (pos_compare a c) whd in ⊢ (% → ?); #Hac 746 [ 1: >(le_to_leb_true a c) /2/ 747  2: destruct cases (leb c c) // 748  3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *) 749 @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac)) 750 ] 751 @le_S_weaken // 752  2: destruct 753 cases (leb c c) normalize nodelta 754 >(le_to_leb_true a c) /2/ 755  3: >(not_le_to_leb_false b c) normalize nodelta /2/ 756 >(le_to_leb_true a b) /2/ 757 ] 758  2: destruct (Hab) >reflexive_leb normalize nodelta 759 lapply (pos_compare_to_Prop b c) 760 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 761 [ 1: >(le_to_leb_true b c) normalize nodelta 762 >(le_to_leb_true b c) normalize nodelta 763 /2/ 764  2: destruct >reflexive_leb normalize nodelta 765 >reflexive_leb // 766  3: >(not_le_to_leb_false b c) normalize nodelta 767 >reflexive_leb /2/ ] 768  3: >(not_le_to_leb_false a b) normalize nodelta /2/ 769 lapply (pos_compare_to_Prop b c) 770 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 771 [ 1: >(le_to_leb_true b c) normalize nodelta /2/ 772  2: destruct >reflexive_leb normalize nodelta @refl 773  3: >(not_le_to_leb_false b c) normalize nodelta 774 >(not_le_to_leb_false a b) normalize nodelta 775 >(not_le_to_leb_false a c) normalize nodelta 776 lapply (transitive_le … Hbc (le_S_weaken … Hab)) 777 #Hca /2/ 778 ] 779 ] qed. 780 781 lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). 782 * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // 783 qed. 784 785 lemma max_of_expr_rewrite : 786 ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id. 787 @(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id)) 788 [ 1: #ed #t // ] 789 [ 1: #sz #i  2: #fl  3: #var_id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8: #cast_ty #e1 790  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14: #cost #e1 ] 791 #ty 792 [ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta 793 whd in match (max_id ??) in ⊢ (???%); 794 >max_one_neutral // ] 795 [ 1,2,11: * * // 796  3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind 797  6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 798 >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one))) 799 >max_id_associative 800 >Hind1 801 cases (max_of_expr e1 ?) 802 #v1 <Hind2 @refl 803  8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 804 >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?); 805 >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%); 806 >max_id_associative >max_id_associative @refl 807  12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); 808 cases field #p normalize nodelta 809 >Hind cases (max_of_expr e1 ?) #e' 810 cases id #id' 811 whd in match (max_id ??); normalize nodelta 812 whd in match (max_id ??); >associative_max @refl 813 ] qed. 814 815 lemma expr_fresh_lift : 816 ∀e,u,id. 817 fresh_for_expression e u → 818 fresh_for_univ SymbolTag id u → 819 fresh_for_univ SymbolTag (max_of_expr e id) u. 820 #e #u #id 821 normalize in match (fresh_for_expression e u); 822 #H1 #H2 823 >max_of_expr_rewrite 824 normalize in match (fresh_for_univ ???); 825 cases (max_of_expr e ?) in H1; #p #H1 826 cases id in H2; #p' #H2 827 normalize nodelta 828 cases (leb p p') normalize nodelta 829 [ 1: @H2  2: @H1 ] 830 qed. 831 832 833 lemma while_fresh_lift : ∀e,s,u. 834 fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. 835 #e #s #u normalize #Hfresh_expr 836 elim (max_of_statement s (an_identifier SymbolTag one)) #p 837 #Hfresh_p 838 @expr_fresh_lift 839 [ 2: // 840  1: @Hfresh_expr ] 841 qed. 842 843 (* 844 theorem switch_removal_correction : ∀ge, ge', u. 845 related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' → 846 ∀s1, s1', tr, s2. 847 switch_state_sim s1 s1' → 848 exec_step ge s1 = Value … 〈tr,s2〉 → 849 eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr. 850 #ge #ge' #u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step 851 inversion Hsim_state 852 [ 1: (* regular state *) 853 #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_ 854 >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); 855 cases s in Hus_fresh; 856 (* Perform the intros for the statements*) 857 [ 1:  2: #lhs #rhs  3: #ret #func #args  4: #stm1 #stm2  5: #cond #iftrue #iffalse  6: #cond #body 858  7: #cond #body  8: #init #cond #step #body  9,10:  11: #retval  12: #cond #switchcases  13: #lab #body 859  14: #lab  15: #cost #body ] 860 #Hus_fresh 861 [ 1: (* Skip *) 862 whd in match (sw_rem ??); 863 inversion Hsim_cont normalize nodelta 864 [ 1: #Hk #Hk' #_ #Hexec_step 865 @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e)))) 866 [ 1: whd in match (exec_step ??); >fn_return_simplify ] 867 cases (fn_return f) in Hexec_step; 868 [ 1,10:  2,11: #sz #sg  3,12: #fsz  4,13: #rg #ptr_ty  5,14: #rg #array_ty #array_sz  6,15: #domain #codomain 869  7,16: #structname #fieldspec  8,17: #unionname #fieldspec  9,18: #rg #id ] 870 normalize nodelta 871 [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct // 872  *: #H destruct (H) ] 873  2: #s0 #k0 #k0' #us0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 874 whd in match (ret ??) in Heq; destruct (Heq) 875 @(eventually_now ????) whd in match (exec_step ??); 876 %{(State (\fst (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try // 877 %1{uf us0 uk} // 878 >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk' 879 whd in ⊢ (% → ?); * #_ // 880  3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq 881 @(eventually_now ????) whd in match (exec_step ??); 882 whd in match (ret ??) in Heq; destruct (Heq) 883 %{(State (\fst (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try // 884 >while_commute %1{uf us0 uk} // 885 [ 1: @while_fresh_lift assumption 886  2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ] 887  4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq 888 @(eventually_now ????) whd in match (exec_step ??); 889 890 891 892 [ 1: @uk 893  2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ] 894 895 whd 896 normalize 897 898 cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0)) 899 [ 1: whd in match (sw_rem (Swhile ??) ?); 900 whd in match (switch_removal ??); 901 whd in match (exec_step ??); 902 903 (* foireux pour le (Expr (Econst_int sz n) ?) *) 904 lemma convert : 905 ∀uv. 906 ∀sz,n,sl. 907 seq_of_labeled_statements (select_switch sz n sl) 908 ~~~u 909 let 〈exit_label, uv1〉 ≝ fresh ? uv in 910 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in 911 Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip) 912 913 914 lemma convert : 915 ∀f,cond,ls,k,ge,e,m. 916 ∀t. 917 ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 → 918 ∀uf,us. 919 fresh_for_function f uf → 920 fresh_for_statement (Sswitch cond ls) us → 921 ∃s',k'. 922 (exec_plus ge 923 E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m) 924 t s') 925 ∧ switch_cont_sim k k' 926 ∧ switch_state_sim 927 (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m) 928 s'. 929 #f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus 930 whd in match (sw_rem ??); 931 whd in match (switch_removal ??); 932 check eq_ind 933 934 935 936 whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec; 937 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ] 938 * #cond_val #cond_trace 939 whd in match (bindIO ??????); 940 cases cond_val 941 [ 1:  2: #sz' #n'  3: #fl  4: #rg  5: #ptr ] 942 [ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ] 943 normalize nodelta #Heq whd in match (ret ??) in Heq; 944 945 946 947 948 ! 〈v,tr〉 ← exec_expr ge e m a : IO ???; 949 match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉 950  _ ⇒ Wrong ??? (msg TypeMismatch) ] 951 952 theorem step_with_labels : ∀ge,ge'. 953 related_globals ? label_fundef ge ge' → 954 state_with_labels s1 s1' → 955 exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 → 956 (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch 957 (exec_step ge st (Sswitch e ls) 958 959 960 ∃tr',s2'. plus ge' s1' tr' s2' ∧ 961 trace_with_extra_labels tr tr' ∧ 962 state_with_labels s2 s2'). 963 964 965 *) 966
Note: See TracChangeset
for help on using the changeset viewer.