Ignore:
Timestamp:
Mar 26, 2013, 2:01:15 PM (7 years ago)
Author:
tranquil
Message:
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2946 r2952  
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    1818; stack_sizes : ident → option ℕ
    19 ; get_pc_from_label : ident (* current function *) → label → res program_counter
     19; premain : F globals
    2020}.
    2121
     
    119119*)
    120120
     121definition pre_main_id : ident ≝ an_identifier … one.
     122
    121123(* this can replace graph_fetch function and lin_fetch_function *)
    122124definition fetch_function:
    123  ∀F.
    124  ∀ge : genv_t F.
     125 ∀F,globals.
     126 ∀ge : genv_gen F globals.
    125127  (Σb.block_region b = Code) →
    126   res (ident×F) ≝
    127  λF,ge,bl.
    128  opt_to_res … [MSG BadFunction]
    129   (! id ← symbol_for_block … ge bl ;
    130    ! fd ← find_funct_ptr … ge bl ;
    131    return 〈id, fd〉).
     128  res (ident×(fundef (F globals))) ≝
     129 λF,g,ge,bl.
     130 if eqZb (block_id bl) (-1) then
     131   return 〈pre_main_id, Internal ? (premain … ge)〉
     132 else
     133   opt_to_res … [MSG BadFunction]
     134    (! id ← symbol_for_block … ge bl ;
     135     ! fd ← find_funct_ptr … ge bl ;
     136     return 〈id, fd〉).
    132137
    133138definition fetch_internal_function :
    134  ∀F.
    135  ∀ge : genv_t (fundef F).
     139 ∀F,globals.
     140 ∀ge : genv_gen F globals.
    136141  (Σb.block_region b = Code) →
    137   res (ident×F) ≝
    138  λF,ge,bl.
     142  res (ident×(F globals)) ≝
     143 λF,g,ge,bl.
    139144 ! 〈id, fd〉 ← fetch_function … ge bl ;
    140145 match fd with
     
    143148 ].
    144149 
    145 lemma fetch_internal_function_no_minus_one :
     150(* lemma fetch_internal_function_minus_one :
    146151  ∀F,V,i,p,bl.
    147152  block_id (pi1 … bl) = -1 →
     
    154159  cases (symbol_for_block ???) normalize //
    155160qed.
     161*)
    156162
    157163inductive call_kind : Type[0] ≝
     
    317323
    318324definition fetch_statement: ∀p : sem_params.∀globals.
    319   ∀ge : genv_t (joint_function p globals). program_counter →
     325  ∀ge : genv p globals. program_counter →
    320326  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
    321327  λp,globals,ge,ptr.
     
    326332
    327333definition pc_of_label : ∀p : sem_params.∀globals.
    328   genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
     334  genv p globals → (Σb.block_region b = Code) → label → res program_counter ≝
    329335  λp,globals,ge,bl,lbl.
    330336  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
     
    378384
    379385definition goto: ∀p : sem_params.∀globals.
    380   genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
     386  genv p globals → label → state_pc p → res (state_pc p) ≝
    381387 λp,globals,ge,l,st.
    382388  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
     
    393399 set_pc … newpc st.
    394400
    395 definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
     401definition next_of_call_pc : ∀p : sem_params.∀globals.
     402  genv p globals →
    396403  program_counter → res (succ p) ≝
    397404λp,globals,ge,pc.
     
    488495    ! bl ← find_symbol … ge id;
    489496    code_block_of_block bl).
    490  
     497
     498definition get_pc_from_label :
     499  ∀p : sem_params.∀globals.
     500  genv p globals →
     501  ident (* current function *) → label → res program_counter ≝
     502  λp,g,ge,id,lbl.
     503  ! bl ← block_of_funct_id … p ge id ;
     504  pc_of_label … ge bl lbl.
     505   
    491506definition block_of_call ≝ λp : sem_params.
    492507  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
Note: See TracChangeset for help on using the changeset viewer.