Changeset 1643 for src/joint


Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1640 r1643  
    4646 ; call_args: Type[0] (* arguments of function calls *)
    4747 ; call_dest: Type[0] (* possible destination of function computation *)
    48  ; extend_statements: Type[0] (* other statements not fitting in the general framework *)
    49  ; ext_forall_labels : (label → Prop) → extend_statements → Prop
     48 ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
     49 ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
     50 ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     51 ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
    5052 }.
    5153 
     
    6870  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    6971  | COND: acc_a_reg p → label → joint_instruction p globals
    70   | extension: extend_statements p → joint_instruction p globals.
     72  | extension: ext_instruction p → joint_instruction p globals.
    7173
    7274(* Paolo: to be moved elsewhere *)
     
    8688
    8789
    88 
    8990definition inst_forall_labels : ∀p : inst_params.∀globals.
    9091    (label → Prop) → joint_instruction p globals → Prop ≝
     
    119120  | sequential: joint_instruction p globals → succ p → joint_statement p globals
    120121  | GOTO: label → joint_statement p globals
    121   | RETURN: joint_statement p globals.
     122  | RETURN: joint_statement p globals
     123  | extension_fin : ext_fin_instruction p → joint_statement p globals.
    122124
    123125record params : Type[1] ≝
    124126 { stmt_pars :> stmt_params
    125127 ; codeT: list ident → Type[0]
    126  ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
    127  }.
    128 
    129 
    130 (* for all labels in statement. Uses succ_choice to consider the successor of
    131    a statement when such successors are labels *)
     128 ; code_has_label: ∀globals.codeT globals → label → Prop
     129 ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
     130    codeT globals → Prop
     131 }.
     132
     133
    132134definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    133135    (label → Prop) → joint_statement p globals → Prop ≝
     
    136138  | GOTO l ⇒ P l
    137139  | RETURN ⇒ True
     140  | extension_fin c ⇒ ext_fin_forall_labels … P c
    138141  ].
    139142
     
    144147
    145148definition lin_params_to_params ≝
    146   λlp : lin_params. mk_params
    147     (mk_stmt_params lp unit (λ_.λ_.True))
    148     (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    149     (* lookup ≝ *)(λglobals,code,lbl.find ??
    150         (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in
    151           ! lbl' ← lbl_opt ;
    152           if eq_identifier … lbl lbl' then return stmt else None ?) code).
     149  λlp : lin_params.let stmt_pars ≝ (mk_stmt_params lp unit (λ_.λ_.True)) in
     150     mk_params
     151      stmt_pars
     152    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement stmt_pars globals)))
     153    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
     154        (λl_stmt. \fst l_stmt = Some ? lbl) code)
     155    (* forall_statements ≝ *)(λglobals,P,code.All ?
     156        (λl_stmt. P (\snd l_stmt)) code).
    153157
    154158coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     
    157161record graph_params : Type[1] ≝
    158162  { g_u_pars :> unserialized_params }.
    159 
    160 include alias "common/Graphs.ma". (* To pick the right lookup *)
    161163
    162164(* One common instantiation of params via Graphs of joint_statements
    163165   (all languages but LIN) *)
    164166definition graph_params_to_params ≝
    165   λgp : graph_params. mk_params
    166     (mk_stmt_params gp label (λP.P))
    167     (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    168     (* lookup ≝ *)(λglobals.lookup …).
     167  λgp : graph_params.let stmt_pars ≝ mk_stmt_params gp label (λP.P) in
     168     mk_params
     169      stmt_pars
     170    (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
     171    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
     172    (* forall_statements ≝ *)(λglobals,P,code.
     173      ∀l,s.lookup … code l = Some ? s → P s).
    169174   
    170 coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
     175coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    171176on _gp : graph_params to params.
    172177   
    173178
    174 definition labels_present : ∀p : params.∀globals.
     179definition labels_present : ∀globals.∀p : params.
    175180  codeT p globals → (joint_statement p globals) → Prop ≝
    176 λglobals,p,code,s. stmt_forall_labels globals p
    177   (λl.lookup … code l ≠ None ?) s.
    178 
    179 definition forall_stmts : ∀p : params.∀globals.
    180   ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝
    181 λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s.
     181λglobals,p,code,s. stmt_forall_labels p globals
     182  (λl.code_has_label ?? code l) s.
    182183
    183184definition code_closed : ∀p : params.∀globals.
    184185  codeT p globals → Prop ≝ λp,globals,code.
    185     forall_stmts … (labels_present … code) code.
     186    forall_statements … (labels_present … code) code.
    186187
    187188(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
     
    202203  joint_if_code     : codeT p globals ;
    203204(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    204   joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
     205  joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    205206(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    206   joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
     207  joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
    207208}.
    208209
     
    216217  λexit: label.
    217218  λp:joint_internal_function globals pars.
    218   λprf: lookup … (joint_if_code … p) exit ≠ None ?.
     219  λprf: code_has_label … (joint_if_code … p) exit.
    219220   mk_joint_internal_function globals pars
    220221    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     
    238239  λgraph.
    239240  λp:joint_internal_function globals pars.
    240   λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    241   λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
     241  λentry_prf: code_has_label … graph (joint_if_entry … p).
     242  λexit_prf: code_has_label … graph (joint_if_exit … p).
    242243    set_joint_code globals pars p
    243244      graph
  • src/joint/TranslateUtils_paolo.ma

    r1640 r1643  
    9797    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    9898    (* this can be added to allow redirections: × label *)) →
     99  (label → ext_fin_instruction src_g_pars →
     100    (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
     101    ×
     102    (joint_statement dst_g_pars globals)) →
    99103  (* initialized function definition with empty graph *)
    100104  joint_internal_function globals dst_g_pars →
     
    103107  (* destination function *)
    104108  joint_internal_function globals dst_g_pars ≝
    105   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
     109  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
    106110  let f : label → joint_statement (src_g_pars : params) globals →
    107111    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    111115    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    112116    | RETURN ⇒ add_graph … lbl (RETURN …) def
     117    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     118      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     119      b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    113120    ] in
    114121  foldi … f (joint_if_code … def) empty.
     122
     123definition b_graph_translate_no_fin :
     124  ∀src_g_pars : graph_params.
     125  ext_fin_instruction src_g_pars = void →
     126  ∀dst_g_pars : graph_params.
     127  ∀globals: list ident.
     128  (* type of allocatable registers (unit if not in RTLabs) *)
     129  ∀T : Type[0].
     130  (* fresh register creation *)
     131  freshT globals dst_g_pars (localsT dst_g_pars) T →
     132  (* function dictating the translation *)
     133  (label → joint_instruction src_g_pars globals →
     134    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     135    (* this can be added to allow redirections: × label *)) →
     136  (* initialized function definition with empty graph *)
     137  joint_internal_function globals dst_g_pars →
     138  (* source function *)
     139  joint_internal_function globals src_g_pars →
     140  (* destination function *)
     141  joint_internal_function globals dst_g_pars ≝
     142  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
     143    b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
     144      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    115145 
    116146(* translation without register allocation *)
     
    121151  (label → joint_instruction src_g_pars globals →
    122152    list (joint_instruction dst_g_pars globals)) →
     153  (label → ext_fin_instruction src_g_pars →
     154    (list (joint_instruction dst_g_pars globals))
     155    ×
     156    (joint_statement dst_g_pars globals)) →
    123157  (* initialized function definition with empty graph *)
    124158  joint_internal_function … dst_g_pars →
     
    127161  (* destination function *)
    128162  joint_internal_function … dst_g_pars ≝
    129   λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
     163  λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
    130164  let f : label → joint_statement (src_g_pars : params) globals →
    131165    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
     
    136170    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    137171    | RETURN ⇒ add_graph … lbl (RETURN …) def
     172    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     173      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     174      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    138175    ] in
    139176  foldi ??? f (joint_if_code ?? def) empty.
     177 
     178definition graph_translate_no_fin :
     179  ∀src_g_pars : graph_params.
     180  ext_fin_instruction src_g_pars = void →
     181  ∀dst_g_pars : graph_params.
     182  ∀globals: list ident.
     183  (* type of allocatable registers (unit if not in RTLabs) *)
     184  (* function dictating the translation *)
     185  (label → joint_instruction src_g_pars globals →
     186    list (joint_instruction dst_g_pars globals)
     187    (* this can be added to allow redirections: × label *)) →
     188  (* initialized function definition with empty graph *)
     189  joint_internal_function globals dst_g_pars →
     190  (* source function *)
     191  joint_internal_function globals src_g_pars →
     192  (* destination function *)
     193  joint_internal_function globals dst_g_pars ≝
     194  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
     195    graph_translate src_g_pars dst_g_pars globals
     196      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     197 
     198
    140199     
    141200(*
  • src/joint/semantics_paolo.ma

    r1641 r1643  
    8686
    8787  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
    88    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     88  (* 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
     90   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    8991     type of arguments. To be fixed using a dependent type *)
    90   ; save_frame: address → nat → paramsT … uns_pars → call_args uns_pars → call_dest uns_pars →
     92  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    9193      state st_pars → res (state st_pars)
    9294  ; fetch_external_args: external_function → state st_pars →
     
    129131    return (set_regs ? r st).
    130132
     133axiom BadPointer : String.
     134
     135(* this is preamble to all calls (including tail ones). The optional argument in
     136   input tells the function whether it has to save the frame for internal
     137   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.
     140   The actual update of the pc is left to later, as it depends on
     141   serialization and on whether the call is a tail one. *)
     142definition eval_call_block_preamble:
     143 ∀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.
     147  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
     148    match fd with
     149    [ 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〉
     160    | External fn ⇒
     161      ! params ← fetch_external_args … p' fn st : IO ???;
     162      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     163      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     164      (* CSC: XXX bug here; I think I should split it into Byte-long
     165         components; instead I am making a singleton out of it. To be
     166         fixed once we fully implement external functions. *)
     167      let vs ≝ [mk_val ? evres] in
     168      ! st ← set_result … p' vs st : IO ???;
     169      return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     170      ].
     171
     172axiom FailedStore: String.
     173
     174definition push: ∀p. state p → beval → res (state p) ≝
     175 λ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_sp … isp st)).
     180
     181definition pop: ∀p. state p → res (state p × beval) ≝
     182 λ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_sp … isp st in
     186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
     187  OK ? 〈st,v〉.
     188
     189definition save_ra : ∀p. state p → address → res (state p) ≝
     190 λp,st,l.
     191  let 〈addrl,addrh〉 ≝ l in
     192  do st ← push … st addrl;
     193  push … st addrh.
     194
     195definition load_ra : ∀p.state p → res (state p × address) ≝
     196 λp,st.
     197  do 〈st,addrh〉 ← pop … st;
     198  do 〈st,addrl〉 ← pop … st;
     199  OK ? 〈st, 〈addrl,addrh〉〉.
     200
     201
    131202(* parameters that need full params to have type of functions,
    132    but are still independent of serialization *)
     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. *)
    133208record more_sem_genv_params (pp : params) : Type[1] ≝
    134209  { msu_pars :> more_sem_unserialized_params pp
    135210  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    136   ; exec_extended: ∀globals.genv globals pp → extend_statements pp →
    137       state msu_pars → IO io_out io_in ((option label) × trace × (state msu_pars))
     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))
    138215  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    139216  }.
     217 
    140218
    141219(* parameters that are defined by serialization *)
     
    165243  OK (state p) (set_pc … newpc st).
    166244
    167 axiom FailedStore: String.
    168 
    169 definition push: ∀p. state p → beval → res (state p) ≝
    170  λp,st,v.
    171   let isp ≝ isp … st in
    172   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    173   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    174   OK … (set_m … m (set_sp … isp st)).
    175 
    176 definition pop: ∀p. state p → res (state p × beval) ≝
    177  λp,st.
    178   let isp ≝ isp ? st in
    179   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    180   let ist ≝ set_sp … isp st in
    181   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    182   OK ? 〈st,v〉.
    183 
    184 definition save_ra : ∀p. state p → address → res (state p) ≝
    185  λp,st,l.
    186   let 〈addrl,addrh〉 ≝ l in
    187   do st ← push … st addrl;
    188   push … st addrh.
    189 
    190 definition load_ra : ∀p.state p → res (state p × address) ≝
    191  λp,st.
    192   do 〈st,addrh〉 ← pop … st;
    193   do 〈st,addrl〉 ← pop … st;
    194   OK ? 〈st, 〈addrl,addrh〉〉.
    195 
    196 
    197245(*
    198246definition empty_state: ∀p. more_sem_params p → state p ≝
     
    208256axiom FailedLoad : String.
    209257axiom BadFunction : String.
    210 axiom BadPointer : String.
    211258
    212259definition eval_call_block:
     
    214261  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    215262 λglobals,p,ge,st,b,args,dest,ra.
    216   ! fd ← (opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    217     match fd with
    218     [ Internal fn ⇒
    219       ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    220       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    221       let l' ≝ joint_if_entry … fn in
    222       let st ≝ set_regs p regs st in
    223       let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    224       ! newpc ← address_of_label … ge pointer_in_fn l' ;
    225       let st ≝ set_pc … newpc st in
    226       return 〈 E0, st〉
    227     | External fn ⇒
    228       ! params ← fetch_external_args … p fn st : IO ???;
    229       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    230       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    231       (* CSC: XXX bug here; I think I should split it into Byte-long
    232          components; instead I am making a singleton out of it. To be
    233          fixed once we fully implement external functions. *)
    234       let vs ≝ [mk_val ? evres] in
    235       ! st ← set_result … p vs st : IO ???;
    236       let st ≝ set_pc … ra st in
    237       return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    238       ].
     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〉.
    239272% qed.
    240273
     
    273306
    274307(* defining because otherwise typechecker stalls *)
    275 definition eval_call_id_succ:
     308definition eval_sequential :
    276309 ∀globals.∀p:sem_params. genv globals p → state p →
    277   ident → call_args p → call_dest p → succ p → IO io_out io_in (trace×(state p)) ≝
    278  λglobals,p,ge,st,id,args,dest,l.
    279    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    280    eval_call_id … ge st id args dest ra.
     310  joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
     311 λglobals,p,ge,st,seq,l.
     312  match seq with
     313  [ 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〉
     321  | COST_LABEL cl ⇒
     322    ! st ← next … p l st ;
     323    return 〈Echarge cl, st〉
     324  | COMMENT c ⇒
     325    ! st ← next … p l st ;
     326    return 〈E0, st〉
     327  | LOAD dst addrl addrh ⇒
     328    ! vaddrh ← dph_arg_retrieve … st addrh ;
     329    ! vaddrl ← dpl_arg_retrieve … st addrl;
     330    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     331    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     332    ! st ← acca_store p … dst v st ;
     333    ! st ← next … p l st ;
     334    return 〈E0, st〉
     335  | STORE addrl addrh src ⇒
     336    ! vaddrh ← dph_arg_retrieve … st addrh;
     337    ! vaddrl ← dpl_arg_retrieve … st addrl;
     338    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     339    ! v ← acca_arg_retrieve … st src;
     340    ! 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〉
     344  | COND src ltrue ⇒
     345    ! v ← acca_retrieve … st src;
     346    ! b ← bool_of_beval v;
     347    if b then
     348     ! st ← goto … p ge ltrue st ;
     349     return 〈E0, st〉
     350    else
     351     ! st ← next … p l st ;
     352     return 〈E0, st〉
     353  | ADDRESS ident prf ldest hdest ⇒
     354    eval_address … ge st ident prf ldest hdest l
     355  | OP1 op dacc_a sacc_a ⇒
     356    ! v ← acca_retrieve … st sacc_a;
     357    ! v ← Byte_of_val v;
     358    let v' ≝ BVByte (op1 eval op v) in
     359    ! st ← acca_store … dacc_a v' st;
     360    ! st ← next … l st ;
     361    return 〈E0, st〉
     362  | OP2 op dacc_a sacc_a src ⇒
     363    ! v1 ← acca_arg_retrieve … st sacc_a;
     364    ! v1 ← Byte_of_val v1;
     365    ! v2 ← snd_arg_retrieve … st src;
     366    ! v2 ← Byte_of_val v2;
     367    ! carry ← bool_of_beval (carry … st);
     368      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     369      let v' ≝ BVByte v' in
     370      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〉
     375  | CLEAR_CARRY ⇒
     376    ! st ← next … l (set_carry … BVfalse st) ;
     377    return 〈E0, st〉
     378  | SET_CARRY ⇒
     379    ! st ← next … l (set_carry … BVtrue st) ;
     380    return 〈E0, st〉
     381  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     382    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     383    ! v1 ← Byte_of_val v1;
     384    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
     385    ! v2 ← Byte_of_val v2;
     386    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     387    let v1' ≝ BVByte v1' in
     388    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〉
     393  | POP dst ⇒
     394    eval_pop … ge st dst l
     395  | PUSH src ⇒
     396    ! v ← acca_arg_retrieve … st src;
     397    ! st ← push … st v;
     398    ! st ← next … l st ;
     399    return 〈E0, st〉
     400  | MOVE dst_src ⇒
     401    ! st ← pair_reg_move … st dst_src ;
     402    ! st ← next … l st ;
     403    return 〈E0, st〉
     404  | CALL_ID id args dest ⇒
     405    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
     406    eval_call_id … ge st id args dest ra
     407  ].
    281408
    282409definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    289416       return 〈E0, st〉
    290417    | RETURN ⇒
    291       ! p ← fetch_ra … st ;
    292       let 〈st,ra〉 ≝ p in
     418      ! 〈st,ra〉 ← fetch_ra … st ;
    293419      ! st ← pop_frame … ge st;
    294420      return 〈E0,set_pc … ra st〉
    295    | sequential seq l ⇒
    296       match seq with
    297       [ extension c ⇒
    298         ! 〈lbl_opt, tr, st〉 ← exec_extended … ge c st ;
    299         match lbl_opt with
    300         [ Some lbl ⇒
    301           ! st ← goto … ge lbl st ;
    302           return 〈tr, st〉
    303         | None ⇒
    304           ! st ← next … l st ;
    305           return 〈tr, st〉
    306         ]       
    307        | COST_LABEL cl ⇒
    308          ! st ← next … p l st ;
    309          return 〈Echarge cl, st〉
    310       | COMMENT c ⇒
    311          ! st ← next … p l st ;
    312          return 〈E0, st〉
    313       | LOAD dst addrl addrh ⇒
    314         ! vaddrh ← dph_arg_retrieve … st addrh ;
    315         ! vaddrl ← dpl_arg_retrieve … st addrl;
    316         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    317         ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    318         ! st ← acca_store p … dst v st ;
    319         ! st ← next … p l st ;
    320         return 〈E0, st〉
    321       | STORE addrl addrh src ⇒
    322         ! vaddrh ← dph_arg_retrieve … st addrh;
    323         ! vaddrl ← dpl_arg_retrieve … st addrl;
    324         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    325         ! v ← acca_arg_retrieve … st src;
    326         ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    327         let st ≝ set_m … m' st in
    328         ! st ← next … p l st ;
    329         return 〈E0, st〉
    330       | COND src ltrue ⇒
    331         ! v ← acca_retrieve … st src;
    332         ! b ← bool_of_beval v;
    333         if b then
    334          ! st ← goto … p ge ltrue st ;
    335          return 〈E0, st〉
    336         else
    337          ! st ← next … p l st ;
    338          return 〈E0, st〉
    339       | ADDRESS ident prf ldest hdest ⇒
    340         eval_address … ge st ident prf ldest hdest l
    341       | OP1 op dacc_a sacc_a ⇒
    342         ! v ← acca_retrieve … st sacc_a;
    343         ! v ← Byte_of_val v;
    344         let v' ≝ BVByte (op1 eval op v) in
    345         ! st ← acca_store … dacc_a v' st;
    346         ! st ← next … l st ;
    347         return 〈E0, st〉
    348       | OP2 op dacc_a sacc_a src ⇒
    349         ! v1 ← acca_arg_retrieve … st sacc_a;
    350         ! v1 ← Byte_of_val v1;
    351         ! v2 ← snd_arg_retrieve … st src;
    352         ! v2 ← Byte_of_val v2;
    353         ! carry ← bool_of_beval (carry … st);
    354           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    355           let v' ≝ BVByte v' in
    356           let carry ≝ beval_of_bool carry in
    357         ! st ← acca_store … dacc_a v' st;
    358           let st ≝ set_carry … carry st in
    359         ! st ← next … l st ;
    360         return 〈E0, st〉
    361       | CLEAR_CARRY ⇒
    362         ! st ← next … l (set_carry … BVfalse st) ;
    363         return 〈E0, st〉
    364       | SET_CARRY ⇒
    365         ! st ← next … l (set_carry … BVtrue st) ;
    366         return 〈E0, st〉
    367       | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    368         ! v1 ← acca_arg_retrieve … st sacc_a_reg;
    369         ! v1 ← Byte_of_val v1;
    370         ! v2 ← accb_arg_retrieve … st sacc_b_reg;
    371         ! v2 ← Byte_of_val v2;
    372         let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    373         let v1' ≝ BVByte v1' in
    374         let v2' ≝ BVByte v2' in
    375         ! st ← acca_store … dacc_a_reg v1' st;
    376         ! st ← accb_store … dacc_b_reg v2' st;
    377         ! st ← next … l st ;
    378         return 〈E0, st〉
    379       | POP dst ⇒
    380         eval_pop … ge st dst l
    381       | PUSH src ⇒
    382         ! v ← acca_arg_retrieve … st src;
    383         ! st ← push … st v;
    384         ! st ← next … l st ;
    385         return 〈E0, st〉
    386       | MOVE dst_src ⇒
    387         ! st ← pair_reg_move … st dst_src ;
    388         ! st ← next … l st ;
    389         return 〈E0, st〉
    390       | CALL_ID id args dest ⇒
    391         eval_call_id_succ … ge st id args dest l
    392      ]
     421   | sequential seq l ⇒ eval_sequential … ge st seq l
     422   | extension_fin c ⇒ exec_fin_extended … ge c st
    393423   ].
    394424
Note: See TracChangeset for help on using the changeset viewer.