Changeset 1215


Ignore:
Timestamp:
Sep 15, 2011, 3:04:22 PM (8 years ago)
Author:
sacerdot
Message:

1) Added shifting directly on pointers
2) More temporary axioms closed.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1213 r1215  
    9797 }.
    9898
     99definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
     100 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
     101
     102definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
     103 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     104
    99105definition eq_pointer: pointer → pointer → bool ≝
    100106 λp1,p2.
  • src/joint/semantics.ma

    r1214 r1215  
    1616 λaddr1,addr2.
    1717  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 *)
    19 axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    20 axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp*)
    21 *)
     18
    2219axiom address_of_label: bemem → label → address.
    2320
     
    4744 { st_frms: framesT p
    4845 ; pc: address
    49  ; sp: address
     46 ; sp: pointer
    5047 ; carry: beval
    5148 ; regs: regsT p
     
    7370 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
    7471
    75 definition set_sp: ∀p. address → state p → state p ≝
     72definition set_sp: ∀p. pointer → state p → state p ≝
    7673 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
    7774
     
    144141axiom FailedStore: String.
    145142
    146 axiom push: ∀p. state p → beval → res (state p).(*
     143definition push: ∀p. state p → beval → res (state p)
    147144 λp,st,v.
    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 
    153 axiom pop: ∀p. state p → res (state p × beval).(*
     145  let sp ≝ sp … st in
     146  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
     147  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
     148  OK … (set_m … m (set_sp … sp st)).
     149
     150definition pop: ∀p. state p → res (state p × beval)
    154151 λp,st.
    155   let sp ≝ val_of_address (sp … st) in
    156   let sp ≝ sub sp (val_of_memory_chunk chunk) in
    157   let st ≝ set_sp … (address_of_val sp) st in
    158   do v ← opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp);
    159   do v ← Byte_of_val v;
    160   OK ? 〈st,v〉).*)
     152  let sp ≝ sp ? st in
     153  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
     154  let st ≝ set_sp … sp st in
     155  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
     156  OK ? 〈st,v〉.
    161157
    162158definition save_ra : ∀p. state p → label → res (state p) ≝
Note: See TracChangeset for help on using the changeset viewer.