Changeset 2677 for src/Clight


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.

Location:
src/Clight
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2645 r2677  
    370370*)
    371371    match lhs with
    372          [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
     372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate vf fd vargs (Kcall (None ?) f e k) m〉
    373373         | Some lhs' ⇒
    374374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
    375            ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
     375           ret ? 〈tr1⧺tr2⧺tr3, Callstate vf fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    376376         ]
    377377  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
     
    481481  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
    482482  ]
    483 | Callstate f0 vargs k m ⇒
     483| Callstate _ f0 vargs k m ⇒
    484484  match f0 with
    485485  [ CL_Internal f ⇒
     
    521521  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    522522  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    523   OK ? (Callstate f (nil ?) Kstop m0).
     523  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
    524524
    525525let rec is_final (s:state) : option int ≝
     
    532532#st elim st;
    533533[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    534 | #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
     534| #vf #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    535535| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
    536536| #r %1 %{r} %
  • src/Clight/CexecComplete.ma

    r2588 r2677  
    441441| #f #l #s #k #env #m @refl
    442442| #f #l #k #env #m #s #k' #H1 whd in ⊢ (??%?); >H1 @refl
    443 | #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?);
     443| #vf #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?);
    444444    >(alloc_vars_complete … H1) whd in ⊢ (??%?);
    445445    >(yields_eq ??? (bind_params_complete … H2))
    446446    //
    447 | #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
     447| #vf #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
    448448    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2;
    449449    #H1 #H2
  • src/Clight/CexecEquiv.ma

    r2428 r2677  
    533533      | *: // ]
    534534  ]
    535 | #f #args #kk #m cases f;
     535| #vf #f #args #kk #m cases f;
    536536  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    537537    #x1 #x2 whd in ⊢ (???%); @err_does_not_interact //
  • src/Clight/CexecSound.ma

    r2608 r2677  
    456456  | #l #s' //
    457457  ]
    458 | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
     458| #vf #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
    459459  [ #fn whd in ⊢ (?????%);
    460460    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
     
    496496  [ whd; %
    497497  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
    498       [ #f #s #k #e #m | #fd #args #k #m | #r #k #m | #r ] normalize
     498      [ #f #s #k #e #m | #vf #fd #args #k #m | #r #k #m | #r ] normalize
    499499      [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize
    500500      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
  • src/Clight/Clight_abstract.ma

    r2667 r2677  
    3131λs. match s with
    3232[ State _ _ _ _ _ ⇒ cl_other
    33 | Callstate _ _ _ _ ⇒ cl_call
     33| Callstate _ _ _ _ _ ⇒ cl_call
    3434| Returnstate _ _ _ ⇒ cl_return
    3535| Finalstate _ ⇒ cl_other
  • src/Clight/Csem.ma

    r2608 r2677  
    933933      ∀m: mem.  state
    934934  | Callstate:
     935      ∀fb: val. (* function pointer; used by stack instrumentation, but not the semantics *)
    935936      ∀fd: clight_fundef.
    936937      ∀args: list val.
     
    10301031      type_of_fundef fd = fun_typeof a →
    10311032      step ge (State f (Scall (None ?) a al) k e m)
    1032            (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
     1033           (tr1⧺tr2) (Callstate vf fd vargs (Kcall (None ?) f e k) m)
    10331034
    10341035  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     
    10391040      type_of_fundef fd = fun_typeof a →
    10401041      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1041            (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     1042           (tr1⧺tr2⧺tr3) (Callstate vf fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10421043
    10431044  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11651166           E0 (State f s' k' e m)
    11661167
    1167   | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
     1168  | step_internal_function: ∀vf,f,vargs,k,m,e,m1,m2.
    11681169      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11691170      bind_parameters e m1 (fn_params f) vargs m2 →
    1170       step ge (Callstate (CL_Internal f) vargs k m)
     1171      step ge (Callstate vf (CL_Internal f) vargs k m)
    11711172           E0 (State f (fn_body f) k e m2)
    11721173
    1173   | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
     1174  | step_external_function: ∀vf,id,targs,tres,vargs,k,m,vres,t.
    11741175      event_match (external_function id targs tres) vargs t vres →
    1175       step ge (Callstate (CL_External id targs tres) vargs k m)
     1176      step ge (Callstate vf (CL_External id targs tres) vargs k m)
    11761177            t (Returnstate vres k m)
    11771178
     
    12101211      find_symbol … ge (prog_main ?? p) = Some ? b →
    12111212      find_funct_ptr … ge b = Some ? f →
    1212       initial_state p (Callstate f (nil ?) Kstop m0).
     1213      initial_state p (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
    12131214
    12141215(* * A final state is a [Returnstate] with an empty continuation. *)
  • src/Clight/SimplifyCasts.ma

    r2588 r2677  
    18821882  cont_cast k k' →
    18831883  state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m)
    1884 | swc_callstate : ∀fd,args,k,k',m.
    1885   cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m)
     1884| swc_callstate : ∀vf,fd,args,k,k',m.
     1885  cont_cast k k' → state_cast (Callstate vf fd args k m) (Callstate vf (simplify_fundef fd) args k' m)
    18861886| swc_returnstate : ∀res,k,k',m.
    18871887  cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m)
     
    24402440                         %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj
    24412441                         [ 1: // | 2: %3 %1 ]
    2442                     | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
     2442                    | 2: #vf #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
    24432443                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
    24442444                    | 4: #r #Habsurd destruct (Habsurd) ]
     
    25722572                                       [ 1: whd in match (bindIO ??????) in ⊢ (% → %);
    25732573                                            #Eq destruct (Eq)
    2574                                             %{(Callstate (simplify_fundef clfd) (\fst  l)
     2574                                            %{(Callstate (\fst a) (simplify_fundef clfd) (\fst  l)
    25752575                                                         (Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
    25762576                                            @conj
     
    25822582                                            | 1: cases (exec_lvalue ge en m fptr)
    25832583                                                 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    2584                                                  | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a)))
     2584                                                 | 1: #x #Hsim #Htype_eq_fptr >(Hsim x (refl ? (OK ? x)))
    25852585                                                      whd in match (bindIO ??????) in ⊢ (% → %);
    25862586                                                      #Heq destruct (Heq)
    2587                                                       %{(Callstate (simplify_fundef clfd) (\fst  l)
    2588                                                                    (Kcall (Some (block×offset×type) 〈\fst  a,typeof (simplify_e fptr)〉)
     2587                                                      %{(Callstate (\fst a) (simplify_fundef clfd) (\fst  l)
     2588                                                                   (Kcall (Some (block×offset×type) 〈\fst  x,typeof (simplify_e fptr)〉)
    25892589                                                                   (simplify_function f) en k') m)}
    25902590                                                      @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ]
     
    28182818   ]
    28192819| 2: (* Call state *)
    2820      #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2820     #vf #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28212821     whd in match (exec_step ??) in ⊢ (% → %);
    28222822     elim fd in Heq_s1'; normalize nodelta
  • 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)
  • src/Clight/switchRemoval.ma

    r2608 r2677  
    19871987      (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext)
    19881988| sws_callstate :
     1989 ∀ssc_vf.
    19891990 ∀ssc_fd.
    19901991 ∀ssc_args.
     
    19992000    switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
    20002001  | _ ⇒ True ]) →
    2001     switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m)
    2002                         (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
     2002    switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
     2003                        (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
    20032004| sws_returnstate :
    20042005 ∀ssr_result.
Note: See TracChangeset for help on using the changeset viewer.