Changeset 2796 for src


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
Location:
src
Files:
4 added
9 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2782 r2796  
    157157(* This one by Paolo is efficient, but it is for the opposite indianess.
    158158-(* jpb: we already have bitvector_of_nat and friends in the library, maybe
    159 - * we should unify this in some way *) 
    160 -let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
    161 -  match n with
    162 -  [ O ⇒ VEmpty ?
    163 -  | S n' ⇒
    164 -    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
    165 -  ].
    166 
     159- * we should unify this in some way *)
     160(* Paolo: converted to good endianness *)
     161let rec bitvector_of_nat_aux (n_acc : nat) (acc :BitVector n_acc) n (k : nat) on n : BitVector (plus n_acc n) ≝
     162  match n return λn.BitVector (plus n_acc n) with
     163  [ O ⇒ acc⌈BitVector n_acc ↦ ?⌉
     164  | S n' ⇒
     165    bitvector_of_nat_aux (S n_acc) (eqb (k mod 2) 1 ::: acc) n' (k ÷ 2)
     166      ⌈BitVector (S n_acc + n') ↦ ?⌉
     167  ].
     168[ cases (plus_n_O ?) | cases (plus_n_Sm ??) ] % qed.
     169
     170definition bitvector_of_nat : ∀n.ℕ → BitVector n ≝ bitvector_of_nat_aux' ? [[ ]].
     171
    167172-let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
    168173-  match b with
  • src/ERTL/ERTL_semantics.ma

    r2783 r2796  
    77definition ps_reg_store: ? → ? → ? → res ? ≝
    88 λr,v.λlocal_env : ertl_reg_env.
    9   do res ← reg_store r v (\fst local_env) ;
     9  let res ≝ reg_store r v (\fst local_env) in
    1010  OK … 〈res, \snd local_env〉.
    1111
     
    6464  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
    6565
    66 (* TODO move into ErrorMessage *)
    67 axiom FramesEmptyOnPop : ErrorMessage.
    68 axiom BlockInFramesCorrupted : ErrorMessage.
    69 axiom FrameErrorOnPush : ErrorMessage.
    70 axiom FrameErrorOnPop : ErrorMessage.
    71 
    7266definition ertl_save_frame:
    7367 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
     
    7973  (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
    8074    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    81 
    8275
    8376definition ertl_pop_frame:
     
    165158  (* read_result        ≝ *) (λ_.λ_.λ_.
    166159     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    167   (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
     160  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
    168161  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
    169162
  • src/ERTLptr/ERTLptr_semantics.ma

    r2783 r2796  
    5656  (* read_result        ≝ *) (λ_.λ_.λ_.
    5757     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    58   (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
     58  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertlptr_seq F gl ge stm id)
    5959  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
    6060 
  • src/RTL/RTL_semantics.ma

    r2645 r2796  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: cpointer
    9  ; fr_sp: xpointer
     8 ; fr_pc: program_counter
    109 ; fr_carry: bebit
    11  ; fr_regs: register_env beval
     10 ; fr_regs: reg_sp
    1211 }.
    1312
    14 definition RTL_state : sem_state_params ≝
     13definition RTL_state_params : sem_state_params ≝
    1514  mk_sem_state_params
    1615    (list frame)
    1716    [ ]
    18     (register_env beval)
    19     (λ_.empty_map …).
     17    reg_sp
     18    reg_sp_init
     19    (λenv.OK … (stackp env))
     20    (λenv.mk_reg_sp env (* coercion*)).
    2021
    21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
     22definition RTL_state ≝ state RTL_state_params.
     23
     24unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
     25
     26definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
     27  λenv.λa : psd_argument.
    2228  match a with
    2329  [ Reg r ⇒ reg_retrieve env r
    24   | Imm b ⇒ return b
     30  | Imm b ⇒ OK … (BVByte b)
    2531  ].
    2632
    2733(*CSC: could we use here a dependent type to avoid the Error case? *)
    28 
    2934definition rtl_fetch_ra:
    30  RTL_state → res (RTL_state × cpointer) ≝
     35 RTL_state → res (RTL_state × program_counter) ≝
    3136 λst.
    32   match st_frms ? st with
     37 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
     38   match frms with
    3339  [ nil ⇒ Error ? [MSG EmptyStack]
    34   | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
     40  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
     41  ].
    3542
    3643definition rtl_init_local :
    37  register → register_env beval → register_env beval
    38  λlocal,env.add … env local BVundef.
     44 register → reg_sp → reg_sp
     45 λlocal.reg_sp_store … local BVundef.
    3946
    4047definition rtl_setup_call:
    4148 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    4249  λstacksize,formal_arg_regs,actual_arg_regs,st.
    43   let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     50  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
     51  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
     52  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
    4453  do new_regs ←
    4554   mfold_left2 …
    4655    (λlenv,dest,src.
    4756      do v ← rtl_arg_retrieve … (regs ? st) src ;
    48       OK … (add … lenv dest v))
    49     (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
     57      OK … (reg_sp_store dest v lenv))
     58    (OK … (reg_sp_init sp)) formal_arg_regs actual_arg_regs ;
    5059  OK …
    51    (set_regs RTL_state new_regs
    52     (set_m … mem
    53      (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
    54 cases b * #r #off #E >E %
     60   (set_regs RTL_state_params new_regs
     61    (set_m … mem st)).
     62cases daemon (* will probably change anyway *)
    5563qed.
    5664
    57 definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
    58   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
    59   OK … (set_frms RTL_state frame st).
     65definition RTL_state_pc ≝ state_pc RTL_state_params.
     66
     67unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
     68unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
     69
     70definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
     71 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
     72 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
     73  OK … (set_frms RTL_state_params frame st).
    6074
    6175(*CSC: XXXX, for external functions only*)
    62 axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
     76axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
    6377axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
    6478
    65 definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
    66 definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
     79definition rtl_reg_store ≝ λr,v,st.
     80  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
     81  set_regs RTL_state_params mem st.
     82
     83definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
    6784
    6885definition rtl_read_result :
    69  ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
    70  λglobals,ge,rets,st.
     86 list register → RTL_state → res (list beval) ≝
     87 λrets,st.
    7188 m_list_map … (rtl_reg_retrieve st) rets.
    7289
     
    7592  saves the OutOfBounds exception *)
    7693definition rtl_pop_frame:
    77  ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
    78   res RTL_state ≝
    79  λglobals,ge,curr_fn,st.
    80   let ret ≝ joint_if_result … curr_fn in
    81   do ret_vals ← rtl_read_result … ge ret st ;
    82   match st_frms ? st with
     94 list register → RTL_state →
     95  res (RTL_state × program_counter) ≝
     96 λret,st.
     97 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
     98 match frms with
    8399  [ nil ⇒ Error ? [MSG EmptyStack]
    84100  | cons hd tl ⇒
    85      do st ←
    86       mfold_left_i …
    87        (λi.λst.λreg.
    88          do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    89          rtl_reg_store reg v st)
    90        (OK … st) (fr_ret_regs hd) ;
    91      OK …
    92       (set_frms RTL_state tl
    93         (set_regs RTL_state (fr_regs hd)
    94          (set_sp … (fr_sp hd)
    95           (set_carry … (fr_carry hd)
    96            (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    97 
    98 (* This code is quite similar to eval_call_block: can we factorize it out? *)
    99 definition eval_tailcall_block:
    100  ∀globals.genv RTL globals → RTL_state →
    101   block → call_args RTL →
    102   (* this is where the result of the current function should be stored *)
    103   call_dest RTL →
    104   IO io_out io_in
    105     ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
    106  λglobals,ge,st,b,args,ret.
    107   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    108     match fd with
    109     [ Internal fd ⇒
    110       return 〈FTailInit ?? (block_id b) fd args, st〉
    111     | External fn ⇒
    112       ! params ← rtl_fetch_external_args … fn st : IO ???;
    113       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    114       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    115       (* CSC: XXX bug here; I think I should split it into Byte-long
    116          components; instead I am making a singleton out of it. To be
    117          fixed once we fully implement external functions. *)
    118       let vs ≝ [mk_val ? evres] in
    119       ! st ← rtl_set_result … vs ret st : IO ???;
    120       return 〈FEnd2 ??, st〉
    121     ].
     101    ! ret_vals ← rtl_read_result … ret st ;
     102    (* Paolo: no more OutOfBounds exception, but is it right? should be for
     103       compiled programs *)
     104    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
     105    let st ≝ foldl …
     106      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
     107      st reg_vals in
     108    ! sp ← sp … st ;  (* always succeeds in RTL *)
     109    let st ≝ set_frms RTL_state_params tl
     110        (set_regs RTL_state_params (fr_regs hd)
     111          (set_carry RTL_state_params (fr_carry hd)
     112            (set_m … (free … (m … st) (pblock sp)) st))) in
     113    let pc ≝ fr_pc hd in
     114    return 〈st, pc〉
     115  ].
    122116
    123117definition block_of_register_pair: register → register → RTL_state → res block ≝
     
    129123
    130124definition eval_rtl_seq:
    131  ∀globals. genv RTL globals →
    132   rtl_seq → joint_internal_function RTL globals → RTL_state →
    133    IO io_out io_in RTL_state ≝
    134  λglobals,ge,stm,curr_fn,st.
     125  rtl_seq → ident → RTL_state →
     126   res RTL_state ≝
     127 λstm,curr_fn,st.
    135128  match stm with
    136129   [ rtl_stack_address dreg1 dreg2  ⇒
    137       let sp ≝ sp ? st in
    138       ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    139       ! st ← rtl_reg_store dreg1 dpl st ;
    140       rtl_reg_store dreg2 dph st
     130      ! sp ← sp ? st ; (* always succeeds in RTL *)
     131      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
     132      let st ≝ rtl_reg_store dreg1 dpl st in
     133      return rtl_reg_store dreg2 dph st
    141134   ].
    142135
    143 definition eval_rtl_call:
    144  ∀globals. genv RTL globals →
    145   rtl_call → RTL_state →
    146    IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
    147  λglobals,ge,stm,st.
    148   match stm with
    149   [ rtl_call_ptr r1 r2 args dest ⇒
    150     ! b ← block_of_register_pair r1 r2 st : IO ???;
    151     ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    152     match fd with
    153     [ Internal fd ⇒
    154       return 〈Init ?? (block_id b) fd args dest, st〉
    155     | External fn ⇒
    156       ! params ← rtl_fetch_external_args … fn st : IO ???;
    157       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    158       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    159       (* CSC: XXX bug here; I think I should split it into Byte-long
    160          components; instead I am making a singleton out of it. To be
    161          fixed once we fully implement external functions. *)
    162       let vs ≝ [mk_val ? evres] in
    163       ! st ← rtl_set_result … vs dest st : IO ???;
    164       return 〈Proceed ???, st〉
    165     ]
    166   ].
    167 
    168 definition eval_rtl_tailcall:
    169  ∀globals. genv RTL globals →
    170   rtl_tailcall → joint_internal_function RTL globals → RTL_state →
    171    IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
    172    λglobals,ge,stm,curr_fn,st.
    173    let ret ≝ joint_if_result … curr_fn in
    174    match stm with
    175    [ rtl_tailcall_id id args ⇒
    176       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    177       eval_tailcall_block … ge st b args ret
    178    | rtl_tailcall_ptr r1 r2 args ⇒
    179       ! b ← block_of_register_pair r1 r2 st : IO ???;
    180       eval_tailcall_block … ge st b args ret
    181    ].
     136(* for a store living in res *)
     137definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
    182138
    183139definition RTL_semantics ≝
    184   make_sem_graph_params RTL
    185     (mk_more_sem_unserialized_params ??
    186       RTL_state
    187       reg_store reg_retrieve rtl_arg_retrieve
    188       reg_store reg_retrieve rtl_arg_retrieve
    189       reg_store reg_retrieve rtl_arg_retrieve
    190       reg_store reg_retrieve rtl_arg_retrieve
     140  mk_sem_graph_params RTL
     141    (λF.mk_sem_unserialized_params RTL F
     142      RTL_state_params
     143      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     144      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     145      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     146      reg_res_store reg_sp_retrieve rtl_arg_retrieve
    191147      rtl_arg_retrieve
    192       (λenv,p. let 〈dest,src〉 ≝ p in
     148      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
    193149        ! v ← rtl_arg_retrieve env src ;
    194         reg_store dest v env)
    195       rtl_fetch_ra
    196       rtl_init_local
    197       rtl_save_frame
     150        return reg_sp_store dest v env)
     151      (λ_.rtl_save_frame)
    198152      rtl_setup_call
    199153      rtl_fetch_external_args
    200154      rtl_set_result
    201155      [ ] [ ]
    202       rtl_read_result
    203       eval_rtl_seq
    204       eval_rtl_tailcall
    205       eval_rtl_call
    206       rtl_pop_frame
    207       (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
     156      (λ_.λ_.rtl_read_result) 
     157      (λ_.λ_.eval_rtl_seq)
     158      (λ_.λ_.λ_.rtl_pop_frame)).
  • src/common/ErrorMessages.ma

    r2795 r2796  
    7070 | BadCostLabelling : ErrorMessage
    7171 | RepeatedCostLabel : ErrorMessage
    72  | NotTerminated : ErrorMessage.
     72 | NotTerminated : ErrorMessage
     73 | RepeatedCostLabel : ErrorMessage
     74 | FramesEmptyOnPop : ErrorMessage
     75 | BlockInFramesCorrupted : ErrorMessage
     76 | FrameErrorOnPush : ErrorMessage
     77 | FrameErrorOnPop : ErrorMessage.
  • src/joint/Traces.ma

    r2785 r2796  
    291291   (* as_call_ident ≝ *) (joint_call_ident p)
    292292   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
     293
     294(* alternative definition with integrated prog_params constructor *)
     295definition joint_status :
     296 ∀p : sem_params.
     297 joint_program p → (ident → option ℕ) → abstract_status ≝
     298λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes).
  • src/joint/joint_semantics.ma

    r2783 r2796  
    199199      state st_pars → res (list beval)
    200200  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    201     ident → F globals (* current *) → state st_pars → res (state st_pars)
     201    ident (* current *) → state st_pars → res (state st_pars)
    202202  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    203     ident → F globals (* current *) → state st_pars → res (state st_pars × program_counter)
     203    ident (* current *) → call_dest uns_pars (* current ret *) →
     204      state st_pars → res (state st_pars × program_counter)
    204205  }.
    205206
     
    407408definition eval_seq_no_pc :
    408409 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
    409  joint_closed_internal_function p globals →
    410410  joint_seq p globals → state p →
    411411  res (state p) ≝
    412  λp,globals,ge,curr_id,curr_fn,seq,st.
     412 λp,globals,ge,curr_id,seq,st.
    413413 match seq with
    414414  [ extension_seq c ⇒
    415     eval_ext_seq … ge c curr_id curr_fn st
     415    eval_ext_seq … ge c curr_id st
    416416  | LOAD dst addrl addrh ⇒
    417417    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    539539definition eval_statement_no_pc :
    540540 ∀p:sem_params.∀globals.∀ge:genv p globals.
    541  ident → joint_closed_internal_function p globals (* current *) →
     541 ident (* current *) →
    542542 joint_statement p globals → state p → res (state p) ≝
    543  λp,globals,ge,curr_id,curr_fn,s,st.
     543 λp,globals,ge,curr_id,s,st.
    544544  match s with
    545545  [ sequential s next ⇒
    546546    match s with
    547     [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
     547    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st
    548548    | _ ⇒ return st
    549549    ]
     
    553553definition eval_return ≝
    554554λp : sem_params.λglobals : list ident.λge : genv p globals.
    555 λcurr_id.λcurr_fn : joint_closed_internal_function ??.
     555λcurr_id.λcurr_ret : call_dest p.
    556556λst : state p.
    557 ! st' ← pop_frame … ge curr_id curr_fn st ;
     557! st' ← pop_frame … ge curr_id curr_ret st ;
    558558! nxt ← next_of_call_pc … ge (\snd … st') ;
    559559return
     
    562562definition eval_tailcall ≝
    563563λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
    564 λcurr_fn : joint_closed_internal_function ??.
     564λcurr_ret : call_dest p.
    565565λst : state_pc p.
    566566! bl ← block_of_call … ge f st : IO ???;
     
    572572  return mk_state_pc … st' pc (last_pop … st)
    573573| External efd ⇒
    574   let curr_dest ≝ joint_if_result ?? curr_fn in
    575   ! st' ← eval_external_call … efd args curr_dest st ;
    576   eval_return … ge curr_f curr_fn st
     574  ! st' ← eval_external_call … efd args curr_ret st ;
     575  eval_return … ge curr_f curr_ret st
    577576].
    578577
     
    598597    ]
    599598  | final s ⇒
     599    let curr_ret ≝ joint_if_result … curr_fn in
    600600    match s with
    601601    [ GOTO l ⇒ goto … ge l st
    602     | RETURN ⇒ eval_return … ge curr_id curr_fn st
     602    | RETURN ⇒ eval_return … ge curr_id curr_ret st
    603603    | TAILCALL _ f args ⇒
    604       eval_tailcall … ge f args curr_id curr_fn st
     604      eval_tailcall … ge f args curr_id curr_ret st
    605605    ]
    606606  | FCOND _ a lbltrue lblfalse ⇒
     
    618618  λp,globals,ge,st.
    619619  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
    620   ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
     620  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
    621621  let st'' ≝ set_no_pc … st' st in
    622622  eval_statement_advance … ge id fn s st''.
    623623
    624 (* Paolo: what if in an intermediate language main finishes with an external
    625   tailcall? Maybe it should rely on an FEnd flow command issued, but that's
    626   not static... *)
    627624definition is_final: ∀p: sem_params.∀globals.
    628625  genv p globals → program_counter → state_pc p → option int ≝
     
    632629  [ final s' ⇒
    633630    match s' with
    634     [ RETURN ⇒
    635       do st' ← pop_frame … ge id fn st;
     631    [ RETURN ⇒
     632      let curr_ret ≝ joint_if_result … fn in
     633      do st' ← pop_frame … ge id curr_ret st;
    636634      if eq_program_counter (\snd … st') exit then
    637       do vals ← read_result … ge (joint_if_result … fn) st ;
     635      do vals ← read_result … ge curr_ret st ;
    638636        Word_of_list_beval vals
    639637      else
  • src/joint/semanticsUtils.ma

    r2783 r2796  
    5050}.
    5151
    52 definition reg_store ≝ λreg,v,locals. OK ? (add RegisterTag beval locals reg v).
     52definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
    5353
    5454definition reg_retrieve : register_env beval → register → res beval ≝
     
    5656
    5757definition reg_sp_store ≝ λreg,v,locals.
    58 ! locals' ← reg_store reg v (reg_sp_env locals) ;
    59 return mk_reg_sp locals' (stackp locals).
    60 
    61 definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
    62 
     58let locals' ≝ reg_store reg v (reg_sp_env locals) in
     59mk_reg_sp locals' (stackp locals).
     60
     61unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
     62
     63definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
     64
     65definition reg_sp_init ≝ mk_reg_sp (empty_map …).
    6366(*** Store/retrieve on hardware registers ***)
    6467
  • src/utilities/extralib.ma

    r2309 r2796  
    204204for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
    205205        λ${ident E}.$s ] (refl ? $t) }.
     206
     207inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     208    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     209
     210interpretation "exists in Type[1]" 'exists_Type1 x = (ex_Type1 ? x).
     211
     212notation < "hvbox(∃\sub 1 ident i : ty break . p)"
     213 right associative with precedence 20
     214for @{'exists_Type1 (\lambda ${ident i} : $ty. $p) }.
     215
     216notation > "\exists[1] list1 ident x sep , opt (: T). term 19 Px"
     217  with precedence 20
     218  for ${ default
     219          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}:$T.$acc)} } }
     220          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}.$acc)} } }
     221       }.
Note: See TracChangeset for help on using the changeset viewer.