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/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
Note: See TracChangeset for help on using the changeset viewer.