Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2588 r2677  
    349349    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (\fst (label_function g 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)
    350350(* and the rest *)
    351 | swl_callstate : ∀g,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (\fst (label_fundef g fd)) args k' m)
     351| swl_callstate : ∀g,vf,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate vf fd args k m) (Callstate vf (\fst (label_fundef g fd)) args k' m)
    352352| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
    353353| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
     
    966966  whd in ⊢ (??%?); >label_expr_type >EX2
    967967  % [1,3: <(E0_right tr) ] /4/
    968 | #u0 *
     968| #u0 #vf *
    969969  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
    970970    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
     
    10361036lemma exec_step_interaction:
    10371037  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
    1038   ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
     1038  ∃vf,f,argtys,retty,vargs,k',m. s = Callstate vf (CL_External f argtys retty) vargs k' m.
    10391039#ge #s cases s
    10401040[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
     
    10651065    ]
    10661066  ]
    1067 | #f #args #kk #m #o #k cases f
     1067| #vf #f #args #kk #m #o #k cases f
    10681068  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    10691069    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
     
    10721072    @bindIO_res_interact #vs #Evs
    10731073    #EX whd in EX:(??%?); destruct
    1074     %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
     1074    %{vf} %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
    10751075  ]
    10761076| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
     
    10831083] qed.
    10841084
    1085 lemma state_with_labels_call : ∀f,a,k,m,s1.
    1086  state_with_labels (Callstate f a k m) s1 →
    1087  ∃k'. cont_with_labels k k' ∧ ∃u0. s1 = Callstate (\fst (label_fundef u0 f)) a k' m.
    1088 #f #a #k #m #s1 #S inversion S
     1085lemma state_with_labels_call : ∀vf,f,a,k,m,s1.
     1086 state_with_labels (Callstate vf f a k m) s1 →
     1087 ∃k'. cont_with_labels k k' ∧ ∃u0. s1 = Callstate vf (\fst (label_fundef u0 f)) a k' m.
     1088#vf #f #a #k #m #s1 #S inversion S
    10891089[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
    10901090  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
     
    10921092  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
    10931093  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
    1094   | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
     1094  | #u0 #vf' #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
    10951095  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
    10961096  | #H72 #H73 #H74 #H75 destruct
     
    11141114#ge #ge' #RG #s1 #s1' #o #k #EX
    11151115cases (exec_step_interaction … EX)
    1116 #fn * #argtys * #retty * #vargs * #k' * #m #E
     1116#vf * #fn * #argtys * #retty * #vargs * #k' * #m #E
    11171117destruct
    11181118#S cases (state_with_labels_call … S)
Note: See TracChangeset for help on using the changeset viewer.