Changeset 1213


Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (8 years ago)
Author:
sacerdot
Message:

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

Location:
src
Files:
4 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1139 r1213  
    8484try ( @Ptrue // )
    8585@Pfalse % #E destruct
     86qed.
     87
     88lemma reflexive_eq_region: ∀r. eq_region r r = true.
     89 * //
    8690qed.
    8791
  • src/common/Animation.ma

    r963 r1213  
    1818inductive snapshot (state:Type[0]) : Type[0] ≝
    1919| running : trace → state → snapshot state
    20 | finished : trace → int → mem → snapshot state
     20| finished : trace → int → state → snapshot state
    2121| input_exhausted : trace → snapshot state.
    2222
     
    4848inductive snapshot' (state:Type[0]) : Type[0] ≝
    4949| running' : trace → state → snapshot' state
    50 | finished' : nat → trace → int → mem → snapshot' state
     50| finished' : nat → trace → int → state → snapshot' state
    5151| input_exhausted' : trace → snapshot' state
    5252| failed' : errmsg → nat → state → snapshot' state
     
    9595λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
    9696
     97include "common/Mem.ma".
     98
    9799(* Hide the representation of memory to make displaying the results easier. *)
    98100
  • src/common/SmallstepExec.ma

    r1181 r1213  
    1 
    21include "utilities/extralib.ma".
    32include "common/IOMonad.ma".
    43include "common/Integers.ma".
    54include "common/Events.ma".
    6 include "common/Mem.ma".
    75
    86record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9 { genv  : Type[0]
     7{ mem : Type[0]
     8; genv  : Type[0]
    109; state : Type[0]
    1110; is_final : state → option int
     
    3534(* A (possibly non-terminating) execution.   *)
    3635coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
    37 | e_stop : trace → int → mem → execution state output input
     36| e_stop : trace → int → state → execution state output input
    3837| e_step : trace → state → execution state output input → execution state output input
    3938| e_wrong : errmsg → execution state output input
     
    5251| Value v ⇒ match v with [ pair t s' ⇒
    5352    match is_final ?? exec s' with
    54     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     53    [ Some r ⇒ e_stop ??? t r s'
    5554    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    5655| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     
    7069| Value v ⇒ match v with [ pair t s' ⇒
    7170    match is_final ?? exec s' with
    72     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     71    [ Some r ⇒ e_stop ??? t r s'
    7372    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    7473| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
  • src/common/Values.ma

    r961 r1213  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "common/AST.ma".
    2120include "common/Floats.ma".
    2221include "common/Errors.ma".
    23 
    24 include "ASM/BitVectorZ.ma".
    25 
     22include "common/Pointers.ma".
    2623include "basics/logic.ma".
    27 
    28 include "utilities/extralib.ma".
    29 
    30 (* To define pointers we need a few details about the memory model.
    31 
    32    There are several kinds of pointers, which differ in which regions of
    33    memory they address and the pointer's representation.
    34    
    35    Pointers are given as kind, block, offset triples, where a block identifies
    36    some memory in a given region with an arbitrary concrete address.  A proof
    37    is also required that the representation is suitable for the region the
    38    memory resides in.  Note that blocks cannot extend out of a region (in
    39    particular, a pdata pointer can address any byte in a pdata block - we never
    40    need to switch to a larger xdata pointer).
    41  *)
    42 
    43 (* blocks - represented by the region the memory resides in and a unique id *)
    44 
    45 record block : Type[0] ≝
    46 { block_region : region
    47 ; block_id : Z
    48 }.
    49 
    50 definition eq_block ≝
    51 λb1,b2.
    52   eq_region (block_region b1) (block_region b2) ∧
    53   eqZb (block_id b1) (block_id b2)
    54 .
    55 
    56 lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
    57   (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    58   P (eq_block b1 b2).
    59 #P * #r1 #i1 * #r2 #i2 #H1 #H2
    60 whd in ⊢ (?%) @eq_region_elim #H3
    61 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    62 | @H2 % #E destruct elim H3 /2/
    63 ] qed.
    64 
    65 lemma eq_block_b_b : ∀b. eq_block b b = true.
    66 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
    67 qed.
    68 
    69 (* Characterise the memory regions which the pointer representations can
    70    address.
    71 
    72    pointer_compat <block> <pointer representation> *)
    73 
    74 inductive pointer_compat : block → region → Prop ≝
    75 |        same_compat : ∀s,id. pointer_compat (mk_block s id) s
    76 |      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
    77 |   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    78 
    79 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    80 * * #id *;
    81 try ( %1 // )
    82 %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
    83 qed.
    84 
    85 definition is_pointer_compat : block → region → bool ≝
    86 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    87 
    88 (* Offsets into the block.  We allow integers like CompCert so that we have
    89    the option of extending blocks backwards. *)
    90 
    91 record offset : Type[0] ≝ { offv : Z }.
    92 
    93 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    94 definition shift_offset : ∀n. offset → BitVector n → offset ≝
    95   λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    96 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
    97 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    98   λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
    99 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    100   λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    101 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    102   λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
    103 definition sub_offset : ∀n. offset → offset → BitVector n ≝
    104   λn,x,y. bitvector_of_Z ? (offv x - offv y).
    105 definition zero_offset ≝ mk_offset OZ.
    106 definition lt_offset : offset → offset → bool ≝
    107   λx,y. Zltb (offv x) (offv y).
    10824
    10925(* * A value is either:
  • src/joint/semantics.ma

    r1186 r1213  
    44include "common/SmallstepExec.ma".
    55include "joint/Joint.ma".
    6 (*
     6include "joint/BEMem.ma".
     7
    78(* CSC: external functions never fail (??) and always return something of the
    89   size of one register, both in the frontend and in the backend.
     
    1011   only the head is kept (or Undef if the list is empty) ??? *)
    1112
    12 (* CSC: carries are values and booleans are not values; so we use integers.
    13    But why using values at all? To have undef? *)
    14 (* CSC: ???????????? *)
     13definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)
     14
     15definition eq_address: address → address → bool ≝
     16 λaddr1,addr2.
     17  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
     18(*axiom val_of_address: address → val. (* CSC: only to shift the sp *)
     19axiom address_of_val: val → address. (* CSC: only to shift the sp *)
     20axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp*)
    1521*)
    16 axiom smerge: val → val → res val.
    17 (* CSC: ???????????? In OCaml: IntValue.Int32.merge
    18    Note also that the translation can fail; so it should be a res int! *)
    19 axiom smerge2: list val → int.
    20 (* CSC: I have a byte, I need a value, but it is complex to do so *)
    21 axiom val_of_Byte: Byte → val.
    22 axiom Byte_of_val: val → res Byte.
    23 (*
    24 axiom val_of_nat: nat → val.
    25 (* Map from the front-end memory model to the back-end memory model *)
    26 *)
    27 axiom represent_block: block → val × val.
    28 (* CSC: fixed size chunk *)
    29 axiom chunk: memory_chunk.
    30 axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
    31 axiom address: Type[0].
    32 axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    33 axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    34 (* CSC: ??? *)
    35 axiom address_of_label: mem → label → address.
    36 axiom address_chunks_of_label: mem → label → Byte × Byte.
    37 axiom label_of_address_chunks: Byte → Byte → label.
    38 axiom address_of_address_chunks: Byte → Byte → address.
     22axiom address_of_label: bemem → label → address.
    3923
    4024record sem_params: Type[1] ≝
     
    4529 ; pop_frame_: framesT → res framesT
    4630 ; save_frame_: framesT → regsT → framesT
    47  ; greg_store_: generic_reg p → val → regsT → res regsT
    48  ; greg_retrieve_: regsT → generic_reg p → res val
    49  ; acca_store_: acc_a_reg p → val → regsT → res regsT
    50  ; acca_retrieve_: regsT → acc_a_reg p → res val
    51  ; accb_store_: acc_b_reg p → val → regsT → res regsT
    52  ; accb_retrieve_: regsT → acc_b_reg p → res val
    53  ; dpl_store_: dpl_reg p → val → regsT → res regsT
    54  ; dpl_retrieve_: regsT → dpl_reg p → res val
    55  ; dph_store_: dph_reg p → val → regsT → res regsT
    56  ; dph_retrieve_: regsT → dph_reg p → res val
     31 ; greg_store_: generic_reg p → beval → regsT → res regsT
     32 ; greg_retrieve_: regsT → generic_reg p → res beval
     33 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
     34 ; acca_retrieve_: regsT → acc_a_reg p → res beval
     35 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
     36 ; accb_retrieve_: regsT → acc_b_reg p → res beval
     37 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
     38 ; dpl_retrieve_: regsT → dpl_reg p → res beval
     39 ; dph_store_: dph_reg p → beval → regsT → res regsT
     40 ; dph_retrieve_: regsT → dph_reg p → res beval
    5741 ; pair_reg_move_: regsT → pair_reg p → regsT
    5842 
     
    6448 ; pc: address
    6549 ; sp: address
    66  ; carry: val
     50 ; carry: beval
    6751 ; regs: regsT p
    68  ; m: mem
     52 ; m: bemem
    6953 }.
    7054
     
    7862 ; fetch_external_args: external_function → state sparams → res (list val)
    7963 ; set_result: list val → state sparams → res (state sparams)
    80  ; fetch_result: state sparams → nat → res (list val)
     64 ; fetch_result: state sparams → nat → res val
    8165
    8266 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
    8367 }.
    8468
    85 definition set_m: ∀p. mem → state p → state p ≝
     69definition set_m: ∀p. bemem → state p → state p ≝
    8670 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
    8771
     
    9276 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
    9377
    94 definition set_carry: ∀p. val → state p → state p ≝
     78definition set_carry: ∀p. beval → state p → state p ≝
    9579 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
    9680
     
    10589 λp,l,st. set_pc … (address_of_label … (m … st) l) st.
    10690
    107 definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
    108  λp,dst,v,st.
    109   (*CSC: monadic notation missing here *)
    110   bind ?? (greg_store_ … dst v (regs … st)) (λregs.
    111   OK ? (set_regs … regs st)).
    112 
    113 definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res val ≝
     91definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
     92 λp,dst,v,st.
     93  do regs  ← greg_store_ … dst v (regs … st);
     94  OK ? (set_regs … regs st).
     95
     96definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
    11497 λp,st,dst.greg_retrieve_ … (regs … st) dst.
    11598
    116 definition acca_store: ∀p:sem_params. acc_a_reg p → val → state p → res (state p) ≝
    117  λp,dst,v,st.
    118   (*CSC: monadic notation missing here *)
    119   bind ?? (acca_store_ … dst v (regs … st)) (λregs.
    120   OK ? (set_regs … regs st)).
    121 
    122 definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res val ≝
     99definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
     100 λp,dst,v,st.
     101  do regs ← acca_store_ … dst v (regs … st);
     102  OK ? (set_regs … regs st).
     103
     104definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
    123105 λp,st,dst.acca_retrieve_ … (regs … st) dst.
    124106
    125 definition accb_store: ∀p:sem_params. acc_b_reg p → val → state p → res (state p) ≝
    126  λp,dst,v,st.
    127   (*CSC: monadic notation missing here *)
    128   bind ?? (accb_store_ … dst v (regs … st)) (λregs.
    129   OK ? (set_regs … regs st)).
    130 
    131 definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res val ≝
     107definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
     108 λp,dst,v,st.
     109  do regs ← accb_store_ … dst v (regs … st);
     110  OK ? (set_regs … regs st).
     111
     112definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
    132113 λp,st,dst.accb_retrieve_ … (regs … st) dst.
    133114
    134 definition dpl_store: ∀p:sem_params. dpl_reg p → val → state p → res (state p) ≝
    135  λp,dst,v,st.
    136   (*CSC: monadic notation missing here *)
    137   bind ?? (dpl_store_ … dst v (regs … st)) (λregs.
    138   OK ? (set_regs … regs st)).
    139 
    140 definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res val ≝
     115definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
     116 λp,dst,v,st.
     117  do regs ← dpl_store_ … dst v (regs … st);
     118  OK ? (set_regs … regs st).
     119
     120definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
    141121 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
    142122
    143 definition dph_store: ∀p:sem_params. dph_reg p → val → state p → res (state p) ≝
    144  λp,dst,v,st.
    145   (*CSC: monadic notation missing here *)
    146   bind ?? (dph_store_ … dst v (regs … st)) (λregs.
    147   OK ? (set_regs … regs st)).
    148 
    149 definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res val ≝
     123definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
     124 λp,dst,v,st.
     125  do regs ← dph_store_ … dst v (regs … st);
     126  OK ? (set_regs … regs st).
     127
     128definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
    150129 λp,st,dst.dph_retrieve_ … (regs … st) dst.
    151130
     
    160139 (* CSC: monadic notation missing here *)
    161140 λp,st.
    162   bind ?? (pop_frame_ p (st_frms … st)) (λframes.
    163   OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st))).
     141  do frames ← pop_frame_ p (st_frms … st);
     142  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
    164143
    165144axiom FailedStore: String.
    166145
    167 definition push: ∀p. state p → Byte → res (state p)
     146axiom push: ∀p. state p → beval → res (state p).(*
    168147 λp,st,v.
    169   let sp ≝ val_of_address (sp … st) in
    170   (*CSC: no monadic notation here *)
    171   bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m … st) sp (val_of_Byte v)))
    172    (λm.
    173     let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    174     OK ? (set_m ? m (set_sp … sp st))).
    175 
    176 definition pop: ∀p. state p → res (state p × Byte) ≝
     148  let sp ≝ (*val_of_address*) (sp ? st) in
     149  do m ← opt_to_res ? (msg FailedStore) (bestorev (m ? st) sp (BVByte v));
     150  let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
     151  OK ? (set_m ? m (set_sp … sp st)).*)
     152
     153axiom pop: ∀p. state p → res (state p × beval).(* ≝
    177154 λp,st.
    178155  let sp ≝ val_of_address (sp … st) in
     
    181158  (*CSC: no monadic notation here *)
    182159  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))
    183    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
     160   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).*)
    184161
    185162definition save_ra : ∀p. state p → label → res (state p) ≝
    186163 λp,st,l.
    187   let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
     164  let 〈addrl,addrh〉 ≝ address_of_label … (m … st) l in
    188165  (* No monadic notation here *)
    189166  bind ?? (push … st addrl) (λst.push … st addrh).
    190167
    191 definition fetch_ra : ∀p.state p → res (state p × label) ≝
     168definition fetch_ra : ∀p.state p → res (state p × address) ≝
    192169 λp,st.
    193170  (* No monadic notation here *)
    194171  bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in
    195172  bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in
    196    OK ? 〈st, label_of_address_chunks addrl addrh〉)).
     173   OK ? 〈st, 〈addrl,addrh〉〉)).
    197174
    198175axiom MissingSymbol : String.
     
    215192      | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
    216193      | joint_instr_int dest v ⇒
    217         ! st ← greg_store … dest (val_of_Byte v) st;
     194        ! st ← greg_store … dest (BVByte v) st;
    218195          ret ? 〈E0, goto … l st〉
    219196      | joint_instr_load dst addrl addrh ⇒
    220197        ! vaddrh ← dph_retrieve … st addrh;
    221198        ! vaddrl ← dpl_retrieve … st addrl;
    222         ! vaddr ← smerge vaddrl vaddrh;
    223         ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m … st) vaddr);
     199        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
     200        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    224201        ! st ← acca_store … dst v st;
    225202          ret ? 〈E0, goto … l st〉
     
    227204        ! vaddrh ← dph_retrieve … st addrh;
    228205        ! vaddrl ← dpl_retrieve … st addrl;
    229         ! vaddr ← smerge vaddrl vaddrh;
     206        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
    230207        ! v ← acca_retrieve … st src;
    231         ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m … st) vaddr v);
     208        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    232209          ret ? 〈E0, goto … l (set_m … m' st)〉
    233210      | joint_instr_cond src ltrue ⇒
    234211        ! v ← acca_retrieve … st src;
    235         ! b ← eval_bool_of_val v;
     212        ! b ← bool_of_beval v;
    236213          ret ? 〈E0, goto … (if b then ltrue else l) st〉
    237214      | joint_instr_address ident prf ldest hdest ⇒
    238215        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    239           let 〈laddr,haddr〉 ≝ represent_block addr in
     216        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
    240217        ! st ← dpl_store … ldest laddr st;
    241218        ! st ← dph_store … hdest haddr st;
     
    244221        ! v ← acca_retrieve … st acc_a;
    245222        ! v ← Byte_of_val v;
    246           let v' ≝ val_of_Byte (op1 eval op v) in
     223          let v' ≝ BVByte (op1 eval op v) in
    247224        ! st ← acca_store … acc_a v' st;
    248225          ret ? 〈E0, goto … l st〉
     
    252229        ! v2 ← greg_retrieve … st src;
    253230        ! v2 ← Byte_of_val v2;
    254         ! carry ← eval_bool_of_val (carry … st);
     231        ! carry ← bool_of_beval (carry … st);
    255232          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    256           let v' ≝ val_of_Byte v' in
    257           let carry ≝ of_bool carry in
     233          let v' ≝ BVByte v' in
     234          let carry ≝ beval_of_bool carry in
    258235        ! st ← acca_store … acc_a v' st;
    259236          ret ? 〈E0, goto … l (set_carry … carry st)〉
    260       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vfalse st)〉
    261       | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue st)〉
     237      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVfalse st)〉
     238      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVtrue st)〉
    262239      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    263240        ! v1 ← acca_retrieve … st acc_a_reg;
     
    266243        ! v2 ← Byte_of_val v2;
    267244          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    268           let v1' ≝ val_of_Byte v1' in
    269           let v2' ≝ val_of_Byte v2' in
     245          let v1' ≝ BVByte v1' in
     246          let v2' ≝ BVByte v2' in
    270247        ! st ← acca_store … acc_a_reg v1' st;
    271248        ! st ← accb_store … acc_b_reg v2' st;
     
    273250      | joint_instr_pop dst ⇒
    274251        ! 〈st,v〉 ← pop … st;
    275         ! st ← acca_store … dst (val_of_Byte v) st;
     252        ! st ← acca_store … dst v st;
    276253          ret ? 〈E0, goto … l st〉
    277254      | joint_instr_push src ⇒
    278255        ! v ← acca_retrieve … st src;
    279         ! v ← Byte_of_val v;
    280256        ! st ← push … st v;
    281257          ret ? 〈E0, goto … l st〉
     
    307283      ! 〈st,pch〉 ← pop … st;
    308284      ! 〈st,pcl〉 ← pop … st;
    309         let pc ≝ address_of_address_chunks pcl pch in
    310         ret ? 〈E0,set_pc … pc st〉
     285        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
    311286    | joint_st_extension c ⇒ exec_extended … p ge c st
    312287    ].
    313 
    314 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. label → nat → state p → option ((*CSC: why not res*) int) ≝
     288cases addr //
     289qed.
     290
     291definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option ((*CSC: why not res*) int) ≝
    315292  λglobals: list ident.
    316293  λp.
     
    321298  match fetch_statement … st with
    322299  [ Error _ ⇒ None ?
    323   | OK s ⇒
     300  | OK s ⇒ 
    324301    match s with
    325302      [ joint_st_return ⇒
     
    328305         | OK st_l ⇒
    329306           let 〈st,l〉 ≝ st_l in
    330            match label_eq l exit with
    331            [ inl _ ⇒
     307           if eq_address l exit then
    332308             (* CSC: monadic notation missing here *)
    333              match fetch_result st registersno with
     309             match fetch_result globals p st registersno with
    334310             [ Error _ ⇒ None ?
    335              | OK vals ⇒ Some ? (smerge2 vals)
    336              ]
    337            | inr _ ⇒ None ?
    338            ]
    339          ]
    340       | _ ⇒ None ?
    341       ]
    342   ].
    343 
    344 definition joint_exec: ∀globals:list ident. sem_params2 globals → label → nat → execstep io_out io_in ≝
     311             | OK val ⇒
     312                match val with
     313                 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
     314                 | _ ⇒ None ?]]
     315           else
     316            None ? ]
     317      | _ ⇒ None ? ]].
     318
     319definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
    345320  λglobals,p.
    346321  λexit.
    347322  λregistersno.
    348   mk_execstep ? ? ? ? (is_final globals p exit registersno) (m p) (eval_statement globals p).
     323  mk_execstep (is_final globals p exit registersno) (m p) (eval_statement globals p).
    349324
    350325(* CSC: XXX the program type does not fit with the globalenv and init_mem *)
Note: See TracChangeset for help on using the changeset viewer.