Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r1709 r1882  
    1212
    1313definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
     14definition cpointer ≝ Σp.ptype p = Code.
     15definition xpointer ≝ Σp.ptype p = XData.
     16unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     17unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
    1418
    1519record sem_state_params : Type[1] ≝
     
    1721 ; empty_framesT: framesT
    1822 ; regsT : Type[0]
    19  ; empty_regsT: address → regsT (* Stack pointer *)
     23 ; empty_regsT: xpointer → regsT (* Stack pointer *)
    2024 }.
    2125 
    2226record state (semp: sem_state_params): Type[0] ≝
    2327 { st_frms: framesT semp
    24  ; pc: address
    25  ; sp: pointer
    26  ; isp: pointer
     28 ; sp: xpointer
     29 ; isp: xpointer
    2730 ; carry: beval
    2831 ; regs: regsT semp
    2932 ; m: bemem
    3033 }.
    31  
     34
     35record state_pc (semp : sem_state_params) : Type[0] ≝
     36  { st_no_pc :> state semp
     37  ; pc : cpointer
     38  }.
     39
    3240definition set_m: ∀p. bemem → state p → state p ≝
    33  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    3442
    3543definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    36  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    37 
    38 definition set_sp: ∀p. pointer → state p → state p ≝
    39  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    40 
    41 definition set_isp: ∀p. pointer → state p → state p ≝
    42  λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     45
     46definition set_sp: ∀p. ? → state p → state p ≝
     47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     48
     49definition set_isp: ∀p. ? → state p → state p ≝
     50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    4351
    4452definition set_carry: ∀p. beval → state p → state p ≝
    45  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    46 
    47 definition set_pc: ∀p. address → state p → state p ≝
    48  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     54
     55definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     57
     58definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     59 λp,s,st. mk_state_pc … s (pc … st).
    4960
    5061definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    51  λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    5263
    5364axiom BadProgramCounter : String.
     
    5768 ∀globals.
    5869  genv globals pars →
    59   pointer →
     70  cpointer →
    6071  res (joint_internal_function … pars) ≝
    6172 λpars,globals,ge,p.
     
    6576  [ Internal def' ⇒ OK … def'
    6677  | External _ ⇒ Error … [MSG BadProgramCounter]].
    67  
     78
     79inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
     80  | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
     81  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
     82  | Proceed  : step_flow p globals. (* go to implicit successor *)
     83
     84inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
     85  | SRedirect : label → stmt_flow p globals
     86  | SProceed : succ p → stmt_flow p globals
     87  | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
     88  | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
     89  | SEnd  : stmt_flow p globals. (* end flow *)
     90
     91
    6892record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    6993  { st_pars :> sem_state_params
     
    82106  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    83107  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    84   ; fetch_ra: state st_pars →
    85       res ((state st_pars) × address)
    86 
    87   ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
     108  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     109
     110  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    88111  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    89   ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
     112  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
    90113   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    91114     type of arguments. To be fixed using a dependent type *)
     
    94117  ; fetch_external_args: external_function → state st_pars →
    95118      res (list val)
    96   ; set_result: list val → state st_pars →
    97       res (state st_pars)
     119  ; set_result: list val → state st_pars → res (state st_pars)
    98120  ; call_args_for_main: call_args uns_pars
    99121  ; call_dest_for_main: call_dest uns_pars
     
    111133  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
    112134  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
    113   λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
     135  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
    114136
    115137definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     
    126148definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
    127149definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    128 definition pair_reg_move : ?→?→?→?→res ?
     150definition pair_reg_move : ?→?→?→?→?
    129151  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
    130152    ! r ← pair_reg_move_ ? p (regs ? st) pm;
    131     return (set_regs ? r st).
    132 
     153    return set_regs ? r st.
     154
     155 
    133156axiom BadPointer : String.
    134 
     157 
    135158(* this is preamble to all calls (including tail ones). The optional argument in
    136159   input tells the function whether it has to save the frame for internal
    137160   calls.
    138    the first element of the triple is the label at the start of the function
    139    in case of an internal call, or None in case of an external one.
     161   the first element of the triple is the entry point of the function if
     162   it is an internal one, or false in case of an external one.
    140163   The actual update of the pc is left to later, as it depends on
    141164   serialization and on whether the call is a tail one. *)
    142 definition eval_call_block_preamble:
     165definition eval_call_block:
    143166 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    144   genv globals p → state p' → block → call_args p → option ((call_dest p) × address)
    145     IO io_out io_in ((option label)×trace×(state p')) ≝
    146  λglobals,p,p',ge,st,b,args,dest_ra.
     167  genv globals p → state p' → block → call_args p → call_dest p
     168    IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
     169 λglobals,p,p',ge,st,b,args,dest.
    147170  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    148171    match fd with
    149172    [ Internal fn ⇒
    150       let st ≝ match dest_ra with
    151         [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
    152         | None ⇒ st
    153         ] in
    154       ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    155               args st ;
    156       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    157       let l' ≝ joint_if_entry … fn in
    158       let st ≝ set_regs p' regs st in
    159       return 〈Some label l', E0, st〉
     173      return 〈Init … (block_id b) fn args dest, E0, st〉
    160174    | External fn ⇒
    161175      ! params ← fetch_external_args … p' fn st : IO ???;
     
    167181      let vs ≝ [mk_val ? evres] in
    168182      ! st ← set_result … p' vs st : IO ???;
    169       return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     183      return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    170184      ].
    171185
    172186axiom FailedStore: String.
    173187
    174 definition push: ∀p. state p → beval → res (state p) ≝
     188definition push: ∀p.state p → beval → res (state p) ≝
    175189 λp,st,v.
    176   let isp ≝ isp … st in
    177   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    178   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    179   OK … (set_m … m (set_isp … isp st)).
    180 
    181 definition pop: ∀p. state p → res (state p × beval) ≝
     190  let isp' ≝ isp ? st in
     191  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
     192  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
     193  return set_m … m (set_isp … isp'' st).
     194  normalize elim (isp p st) //
     195qed.
     196
     197definition pop: ∀p. state p → res ((state p ) × beval) ≝
    182198 λp,st.
    183   let isp ≝ isp ? st in
    184   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    185   let ist ≝ set_isp … isp st in
    186   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    187   OK ? 〈st,v〉.
    188 
    189 definition save_ra : ∀p. state p → address → res (state p) ≝
     199  let isp' ≝ isp ? st in
     200  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
     201  let ist ≝ set_isp … isp'' st in
     202  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
     203  OK ? 〈ist,v〉.
     204  normalize elim (isp p st) //
     205qed.
     206 
     207definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    190208 λp,st,l.
    191   let 〈addrl,addrh〉 ≝ l in
    192   do st ← push … st addrl;
    193   push … st addrh.
    194 
    195 definition load_ra : ∀p.state p → res (state p × address) ≝
     209  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
     210  ! st' ← push … st addrl;
     211  push … st' addrh.
     212
     213definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
    196214 λp,st.
    197   do 〈st,addrh〉 ← pop … st;
    198   do 〈st,addrl〉 ← pop … st;
    199   OK ? 〈st, 〈addrl,addrh〉〉.
    200 
     215  do 〈st',addrh〉 ← pop … st;
     216  do 〈st'',addrl〉 ← pop … st';
     217  do pr ← code_pointer_of_address 〈addrh, addrl〉;
     218  return 〈st'', pr〉.
     219
     220definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
     221  match flow with
     222  [ SProceed _ ⇒ False
     223  | SInit _ _ _ _ _ ⇒ False
     224  | _ ⇒ True
     225  ].
    201226
    202227(* parameters that need full params to have type of functions,
    203    but are still independent of serialization
    204    Paolo: the first element returned by exec extended is None if flow is
    205    left to regular sequential one, otherwise a label.
    206    The address input is the address of the next statement, to be provided to
    207    accomodate extensions that make calls. *)
     228   but are still independent of serialization *)
    208229record more_sem_genv_params (pp : params) : Type[1] ≝
    209230  { msu_pars :> more_sem_unserialized_params pp
    210231  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    211   ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
    212       state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
    213   ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
    214       state msu_pars → IO io_out io_in (trace × (state msu_pars))
     232  (* change of pc must be left to *_flow execution *)
     233  ; exec_extended: ∀globals.genv globals pp → ext_step pp →
     234      state msu_pars →
     235      IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
     236  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
     237      state msu_pars →
     238      IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
    215239  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    216240  }.
    217  
    218241
    219242(* parameters that are defined by serialization *)
    220243record more_sem_params (pp : params) : Type[1] ≝
    221244  { msg_pars :> more_sem_genv_params pp
    222   ; succ_pc: succ pp → address → res address
    223   ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
    224   ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
     245  ; offset_of_point : code_point pp → offset
     246  ; point_of_offset : offset → option (code_point pp)
     247  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
     248  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
    225249  }.
     250
     251definition pointer_of_point : ∀p.more_sem_params p →
     252  cpointer→ code_point p → cpointer ≝
     253  λp,msp,ptr,pt.
     254    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
     255[ elim ptr #ptr' #EQ <EQ @pok
     256| %] qed.
     257
     258axiom BadOffsetForCodePoint : String.
     259
     260definition point_of_pointer :
     261  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
     262  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
     263    (point_of_offset p msp (poff ptr)).
     264
     265lemma point_of_pointer_of_point :
     266  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
     267#p #msp #ptr #pt normalize
     268>point_of_offset_of_point %
     269qed.
     270
     271lemma pointer_of_point_block :
     272  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
     273/ by refl/
     274qed.
     275
     276lemma pointer_of_point_uses_block :
     277  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
     278#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     279        ** #ty2 #bl2 #H2 #o2 #EQ2
     280#pt #EQ3 destruct normalize //
     281qed.
     282
     283lemma pointer_of_point_of_pointer :
     284  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     285    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
     286    pointer_of_point p msp ptr2 pt = ptr1.
     287#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     288        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
     289destruct
     290lapply (offset_of_point_of_offset p msp o1)
     291normalize
     292elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
     293#pt' #EQ #EQ' destruct %
     294qed.
     295
     296
     297axiom ProgramCounterOutOfCode : String.
     298axiom PointNotFound : String.
     299axiom LabelNotFound : String.
     300
     301definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     302  genv globals p → cpointer → res (joint_statement p globals) ≝
     303  λp,msp,globals,ge,ptr.
     304  ! pt ← point_of_pointer ? msp ptr ;
     305  ! fn ← fetch_function … ge ptr ;
     306  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     307
     308definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     309  genv globals p → cpointer → label → res cpointer ≝
     310  λp,msp,globals,ge,ptr,lbl.
     311  ! fn ← fetch_function … ge ptr ;
     312  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     313            (point_of_label … (joint_if_code … fn) lbl) ;
     314  return pointer_of_point ? msp ptr pt.
     315
     316definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     317  cpointer → succ p → res cpointer ≝
     318  λp,msp,ptr,nxt.
     319  ! curr ← point_of_pointer p msp ptr ;
     320  return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
    226321
    227322record sem_params : Type[1] ≝
     
    230325  }.
    231326
    232 definition address_of_label: ∀globals. ∀p:sem_params.
     327(* definition address_of_label: ∀globals. ∀p:sem_params.
    233328  genv globals p → pointer → label → res address ≝
    234329 λglobals,p,ge,ptr,l.
    235330  do newptr ← pointer_of_label … p ? ge … ptr l ;
    236   OK … (address_of_code_pointer newptr).
     331  OK … (address_of_code_pointer newptr). *)
    237332
    238333definition goto: ∀globals. ∀p:sem_params.
    239   genv globals p → label → state p → res (state p) ≝
     334  genv globals p → label → state_pc p → res (state_pc p) ≝
    240335 λglobals,p,ge,l,st.
    241   ! oldpc ← pointer_of_address (pc … st);
    242   ! newpc ← address_of_label … ge oldpc l ;
    243   OK (state p) (set_pc … newpc st).
     336  ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
     337  return set_pc … newpc st.
    244338
    245339(*
     
    248342*)
    249343
    250 definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
     344definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
    251345 λp,l,st.
    252   ! l' ← succ_pc … p l (pc … st) ;
    253   OK … (set_pc … l' st).
     346 ! nw ← succ_pc ? p … (pc ? st) l ;
     347 return set_pc … nw st.
    254348
    255349axiom MissingSymbol : String.
    256350axiom FailedLoad : String.
    257351axiom BadFunction : String.
    258 
    259 definition eval_call_block:
     352axiom SuccessorNotProvided : String.
     353
     354(* the optional point must be given only for calls *)
     355definition eval_step :
    260356 ∀globals.∀p:sem_params. genv globals p → state p →
    261   block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    262  λglobals,p,ge,st,b,args,dest,ra.
    263  ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
    264  ! new_pc ← match next with
    265   [ Some lbl ⇒
    266     let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    267     address_of_label globals p ge pointer_in_fn lbl
    268   | None ⇒ return ra
    269   ] ;
    270  let st ≝ set_pc … new_pc st in
    271  return 〈tr, st〉.
    272 % qed.
    273 
    274 definition eval_call_id:
    275  ∀globals.∀p:sem_params. genv globals p → state p →
    276   ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    277  λglobals,p,ge,st,id,args,dest,ra.
    278   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
    279   eval_call_block … ge st b args dest ra.
    280 
    281 
    282 (* defining because otherwise typechecker stalls *)
    283 definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
    284   ∀i : ident.member i (eq_identifier SymbolTag) globals
    285      →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
    286      λglobals,p,ge,st,ident,prf,ldest,hdest,l.
    287      let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
    288      ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
    289      ! st ← dpl_store … ldest laddr st;
    290      ! st ← dph_store … hdest haddr st;
    291      ! st ← next … p l st ;
    292      return 〈E0, st〉.
    293   [ cases addr //
    294   | (* TODO: to prove *)
    295     elim daemon
    296   ] qed.
    297 
    298 (* defining because otherwise typechecker stalls *)
    299 definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
    300   acc_a_reg p → succ p → res (trace × (state p)) ≝
    301   λglobals,p,ge,st,dst,l.
    302         ! 〈st,v〉 ← pop p st;
    303         ! st ← acca_store p p dst v st;
    304         ! st ← next p l st ;
    305         return 〈E0, st〉.
    306 
    307 (* defining because otherwise typechecker stalls *)
    308 definition eval_sequential :
    309  ∀globals.∀p:sem_params. genv globals p → state p →
    310   joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
    311  λglobals,p,ge,st,seq,l.
     357  joint_step p globals →
     358  IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
     359 λglobals,p,ge,st,seq.
    312360  match seq with
    313361  [ extension c ⇒
    314     ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
    315     ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
    316     ! st ← match next_pc with
    317       [ None ⇒ next … p l st
    318       | Some lbl ⇒ goto … ge lbl st
    319       ] ;
    320     return 〈tr, st〉
     362    exec_extended … ge c st
    321363  | COST_LABEL cl ⇒
    322     ! st ← next … p l st ;
    323     return 〈Echarge cl, st〉
     364    return 〈Proceed ??, Echarge cl, st〉
    324365  | COMMENT c ⇒
    325     ! st ← next … p l st ;
    326     return 〈E0, st〉
     366    return 〈Proceed ??, E0, st〉
    327367  | LOAD dst addrl addrh ⇒
    328368    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    331371    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    332372    ! st ← acca_store p … dst v st ;
    333     ! st ← next … p l st ;
    334     return 〈E0, st〉
     373    return 〈Proceed ??, E0, st〉
    335374  | STORE addrl addrh src ⇒
    336375    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    339378    ! v ← acca_arg_retrieve … st src;
    340379    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    341     let st ≝ set_m … m' st in
    342     ! st ← next … p l st ;
    343     return 〈E0, st〉
     380    return 〈Proceed ??, E0, set_m … m' st〉
    344381  | COND src ltrue ⇒
    345382    ! v ← acca_retrieve … st src;
    346383    ! b ← bool_of_beval v;
    347384    if b then
    348      ! st ← goto … p ge ltrue st ;
    349      return 〈E0, st〉
     385      return 〈Redirect ?? ltrue, E0, st〉
    350386    else
    351      ! st ← next … p l st ;
    352      return 〈E0, st〉
     387      return 〈Proceed ??, E0, st〉
    353388  | ADDRESS ident prf ldest hdest ⇒
    354     eval_address … ge st ident prf ldest hdest l
     389    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     390    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
     391    ! st' ← dpl_store … ldest laddr st;
     392    ! st'' ← dph_store … hdest haddr st';
     393    return 〈Proceed ??, E0, st''〉
    355394  | OP1 op dacc_a sacc_a ⇒
    356395    ! v ← acca_retrieve … st sacc_a;
     
    358397    let v' ≝ BVByte (op1 eval op v) in
    359398    ! st ← acca_store … dacc_a v' st;
    360     ! st ← next … l st ;
    361     return 〈E0, st〉
     399    return 〈Proceed ??, E0, st〉
    362400  | OP2 op dacc_a sacc_a src ⇒
    363401    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    369407      let v' ≝ BVByte v' in
    370408      let carry ≝ beval_of_bool carry in
    371     ! st ← acca_store … dacc_a v' st;
    372       let st ≝ set_carry … carry st in
    373     ! st ← next … l st ;
    374     return 〈E0, st〉
     409    ! st' ← acca_store … dacc_a v' st;
     410      let st'' ≝ set_carry … carry st' in
     411    return 〈Proceed ??, E0, st''〉
    375412  | CLEAR_CARRY ⇒
    376     ! st ← next … l (set_carry … BVfalse st) ;
    377     return 〈E0, st
     413    let st' ≝ set_carry … BVfalse st in
     414    return 〈Proceed ??, E0, st'
    378415  | SET_CARRY ⇒
    379     ! st ← next … l (set_carry … BVtrue st) ;
    380     return 〈E0, st
     416    let st' ≝ set_carry … BVtrue st in
     417    return 〈Proceed ??, E0, st'
    381418  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    382419    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    387424    let v1' ≝ BVByte v1' in
    388425    let v2' ≝ BVByte v2' in
    389     ! st ← acca_store … dacc_a_reg v1' st;
    390     ! st ← accb_store … dacc_b_reg v2' st;
    391     ! st ← next … l st ;
    392     return 〈E0, st〉
     426    ! st' ← acca_store … dacc_a_reg v1' st;
     427    ! st'' ← accb_store … dacc_b_reg v2' st';
     428    return 〈Proceed ??, E0, st''〉
    393429  | POP dst ⇒
    394     eval_pop … ge st dst l
     430    ! 〈st',v〉 ← pop p st;
     431    ! st'' ← acca_store p p dst v st';
     432    return 〈Proceed ??, E0, st''〉
    395433  | PUSH src ⇒
    396434    ! v ← acca_arg_retrieve … st src;
    397435    ! st ← push … st v;
    398     ! st ← next … l st ;
    399     return 〈E0, st〉
     436    return 〈Proceed ??, E0, st〉
    400437  | MOVE dst_src ⇒
    401438    ! st ← pair_reg_move … st dst_src ;
    402     ! st ← next … l st ;
    403     return 〈E0, st〉
     439    return 〈Proceed ??, E0, st〉
    404440  | CALL_ID id args dest ⇒
    405     ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    406     eval_call_id … ge st id args dest ra
     441    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     442    eval_call_block … ge st b args dest
    407443  ].
     444  [ cases addr //
     445  | (* TODO: to prove *)
     446    elim daemon
     447  ] qed.
     448
     449definition eval_step_flow :
     450 ∀globals.∀p:sem_params.step_flow p globals →
     451  succ p → stmt_flow p globals ≝
     452 λglobals,p,cmd,nxt.
     453 match cmd with
     454 [ Redirect l ⇒ SRedirect … l
     455 | Init id fn args dest ⇒ SInit … id fn args dest nxt
     456 | Proceed ⇒ SProceed … nxt
     457 ].
    408458
    409459definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
    410   state p → IO io_out io_in (trace × (state p)) ≝
    411  λglobals,p,ge,st.
    412   ! s ← fetch_statement … ge st : IO ???;
    413   match s return λ_.IO io_out io_in (trace × (state p)) with
    414     [ GOTO l ⇒
    415        ! st ← goto … ge l st ;
    416        return 〈E0, st〉
    417     | RETURN ⇒
     460  state p → joint_statement … p globals →
     461  IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
     462 λglobals,p,ge,st,s.
     463  match s with
     464    [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
     465    | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
     466    | sequential seq l ⇒
     467      ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
     468      return 〈eval_step_flow … flow l, tr, st〉
     469    | extension_fin c ⇒
     470      ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
     471      return 〈pi1 … flow, tr, st〉
     472    ].
     473
     474definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     475  state p → (Σs : joint_statement … p globals.no_seq … s) →
     476  IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
     477 λglobals,p,ge,st,s_sig.
     478  match s_sig with
     479  [ mk_Sig s s_prf ⇒
     480    match s return λx.no_seq p globals x → ? with
     481    [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
     482    | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
     483    | sequential seq l ⇒ Ⓧ
     484    | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
     485    ] s_prf
     486  ]. % qed.
     487
     488let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
     489  (v2 : IO O I B) on v1 : Prop ≝
     490  match v1 with
     491  [ Value x ⇒
     492    match v2 with
     493    [ Value y ⇒
     494      P x y
     495    | _ ⇒ False
     496    ]
     497  | Wrong _ ⇒
     498    match v2 with
     499    [ Wrong _ ⇒ True
     500    | _ ⇒ False
     501    ]
     502  | Interact o1 f1 ⇒
     503    match v2 with
     504    [ Interact o2 f2 ⇒
     505      ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
     506    | _ ⇒ False
     507    ]
     508  ]. <prf @i qed.
     509
     510definition IORel ≝ λO,I.
     511  mk_MonadRel (IOMonad O I) (IOMonad O I)
     512    (rel_io O I) ???.
     513[//
     514|#X #Y #Z #W #relin #relout #m elim m
     515  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
     516    #f1 #f2 #G' whd %{(refl …)} #i
     517    @(IH … (G i) f1 f2 G')
     518  | #v * [#o #f * | #v' | #e *]
     519    #Pvv' #f #g #H normalize @H @Pvv'
     520  | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
     521  ]
     522| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
     523  [1,4,7: #o' #f' [2,3: *]
     524    normalize * #prf destruct(prf) normalize #G
     525    % [%] normalize #i @IH @G
     526  |2,5,8: #v' [1,3: *]
     527    @H
     528  |*: #e' [1,2: *] //
     529  ]
     530]
     531qed.
     532
     533lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
     534  reflexive ? (m_rel ?? (IORel O I) ?? rel).
     535#O #I #X #rel #H #m elim m
     536[ #o #f #IH whd %[%] #i normalize @IH
     537| #v @H
     538| #e %
     539]
     540qed.
     541
     542lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
     543  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
     544  ∀m,n,o.
     545  m_rel ?? (IORel O I) … rel1 m n →
     546  m_rel ?? (IORel O I) … rel2 n o →
     547  m_rel ?? (IORel O I) … rel3 m o.
     548#O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
     549[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
     550  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
     551| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
     552  @H
     553| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
     554]
     555qed.
     556
     557lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
     558  ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
     559  ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
     560                  m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
     561#M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
     562@(mr_bind … H) @G qed.
     563
     564lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
     565  m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
     566#M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
     567qed.
     568
     569lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
     570  pi1 ?? s1 = s2 →
     571  m_rel ?? (IORel ??) ??
     572    (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
     573      \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
     574    (eval_statement_no_seq globals p ge st s1)
     575    (eval_statement globals p ge st s2).
     576#globals #p #ge #st * * [#s #n | #lbl || #c ]*
     577#s2 #EQ destruct(EQ)
     578whd in match eval_statement;
     579whd in match eval_statement_no_seq;
     580normalize nodelta
     581[1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
     582<(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
     583@(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
     584#x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
     585qed.
     586
     587definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     588  state p → Z → joint_internal_function globals p → call_args p →
     589  res (state_pc p) ≝
     590  λglobals,p,ge,st,id,fn,args.
     591    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     592              args st ;
     593    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
     594    let l' ≝ joint_if_entry … fn in
     595    let st' ≝ set_regs p regs st in
     596    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
     597    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     598    return mk_state_pc ? st' pc. % qed.
     599
     600definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
     601  state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
     602  λglobals,p,ge,st,flow.
     603  match flow with
     604  [ SRedirect l ⇒ goto … ge l st
     605  | SProceed nxt ⇒ next ? nxt st
     606  | SInit id fn args dest nxt ⇒
     607    ! ra ← succ_pc ? p … (pc … st) nxt ;
     608    let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
     609    do_call ?? ge st' id fn args
     610  | STailInit id fn args ⇒
     611    do_call … ge st id fn args
     612  | SEnd ⇒
     613    ! 〈st,ra〉 ← fetch_ra … st ;
     614    ! st' ← pop_frame … ge st;
     615    return mk_state_pc ? st' ra
     616  ].
     617
     618definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     619  state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
     620    IO io_out io_in (state_pc p) ≝
     621  λglobals,p,ge,st,id,flow_sig.
     622  match flow_sig with
     623  [ mk_Sig flow prf ⇒
     624    match flow return λx.flow_no_seq p globals x → ? with
     625    [ SRedirect l ⇒ λ_.
     626      ! newpc ← pointer_of_label ? p … ge
     627        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
     628      return mk_state_pc … st newpc
     629    | STailInit id fn args ⇒ λ_.
     630      do_call … ge st id fn args
     631    | SEnd ⇒ λ_.
    418632      ! 〈st,ra〉 ← fetch_ra … st ;
    419       ! st ← pop_frame … ge st;
    420       return 〈E0,set_pc … ra st〉
    421    | sequential seq l ⇒ eval_sequential … ge st seq l
    422    | extension_fin c ⇒ exec_fin_extended … ge c st
    423    ].
     633      ! st' ← pop_frame … ge st;
     634      return mk_state_pc ? st' ra
     635    | _ ⇒ Ⓧ
     636    ] prf
     637  ]. % qed.
     638
     639lemma pointer_of_label_eq_with_id :
     640∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
     641  block_id (pblock ptr1) = block_id (pblock ptr2) →
     642  pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
     643#g #p #ge
     644** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
     645** #ty2 * #r2 #id2 #H2 inversion H2
     646[1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
     647qed.
     648
     649
     650lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
     651  ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
     652  pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
     653    (eval_stmt_flow_no_seq g p ge st id s1) =
     654    (eval_stmt_flow g p ge st s2).
     655#g#p#ge#st#id'
     656**[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
     657#s2 #EQ #EQ' destruct(EQ)
     658whd in match eval_stmt_flow_no_seq; normalize nodelta
     659whd in match eval_stmt_flow; normalize nodelta
     660[2,3: %]
     661whd in match goto; normalize nodelta
     662whd in match set_pc; normalize nodelta
     663>pointer_of_label_eq_with_id [% | >EQ' % |]
     664qed.
     665
     666definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     667  state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
     668  λglobals,p,ge,st.
     669  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
     670  ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
     671  let st ≝ set_no_pc … st_npc st in
     672  ! st ← eval_stmt_flow … ge st flow;
     673  return 〈tr, st〉.
    424674
    425675definition is_final: ∀globals:list ident. ∀p: sem_params.
    426   genv globals p → address → state p → option int ≝
     676  genv globals p → cpointer → state_pc p → option int ≝
    427677 λglobals,p,ge,exit,st.res_to_opt ? (
    428   do s ← fetch_statement … ge st;
     678  do s ← fetch_statement ? p … ge (pc … st);
    429679  match s with
    430680   [ RETURN ⇒
    431681      do 〈st,ra〉 ← fetch_ra … st;
    432       if eq_address ra exit then
     682      if eq_pointer ra exit then
    433683       do vals ← read_result … ge st ;
    434684       Word_of_list_beval vals
     
    436686       Error ? [ ]
    437687   | _ ⇒ Error ? [ ]]).
    438 
     688 
    439689record evaluation_parameters : Type[1] ≝
    440690 { globals: list ident
    441691 ; sparams:> sem_params
    442  ; exit: address
     692 ; exit: cpointer
    443693 ; genv2: genv globals sparams
    444694 }.
    445695
    446696definition joint_exec: trans_system io_out io_in ≝
    447   mk_trans_system … evaluation_parameters (λG. state G)
     697  mk_trans_system … evaluation_parameters (λG. state_pc G)
    448698   (λG.is_final (globals G) G (genv2 G) (exit G))
    449    (λG.eval_statement (globals G) G (genv2 G)).
     699   (λG.eval_state (globals G) G (genv2 G)).
    450700
    451701definition make_global :
     
    457707 let b ≝ mk_block Code (-1) in
    458708 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    459  let addr ≝ address_of_code_pointer ptr in
    460709  (λp. mk_evaluation_parameters
    461710    (prog_var_names … p)
    462711    (mk_sem_params … pars)
    463     addr
     712    ptr
    464713    (globalenv Genv … p)
    465714  ).
     
    470719definition make_initial_state :
    471720 ∀pars: sem_params.
    472  ∀p: joint_program … pars. res (state pars) ≝
     721 ∀p: joint_program … pars. res (state_pc pars) ≝
    473722λpars,p.
    474723  let sem_globals ≝ make_global pars p in
     
    480729  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
    481730  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    482   do sp ← address_of_pointer spp ;
    483731  let main ≝ prog_main … p in
    484   let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    485   let trace_state ≝
    486    eval_call_id … pars ge st0 main (call_args_for_main … pars)
    487     (call_dest_for_main … pars) (exit sem_globals) in
    488   match trace_state with
    489   [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
    490   | Wrong msg ⇒ Error … msg
    491   | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    492   ].
    493 [3: % | cases ispb | cases spb] * #r #off #E >E %
     732  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
     733  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     734  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
     735  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     736  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
     737  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
     738  match main_fd with
     739  [ Internal fn ⇒
     740    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     741  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     742  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
    494743qed.
    495744
Note: See TracChangeset for help on using the changeset viewer.