Changeset 1329


Ignore:
Timestamp:
Oct 7, 2011, 6:19:41 PM (8 years ago)
Author:
sacerdot
Message:
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1327 r1329  
    9494      ! v ← framesize globals st;
    9595      ! sp ← get_hwsp st;
    96         let newsp ≝ ?(*addr_sub sp v*) in
     96      ! newsp ← addr_sub sp v;
    9797      ! st ← set_hwsp newsp st;
    9898        ret ? 〈E0,goto … l st〉
     
    100100      ! v ← framesize globals st;
    101101      ! sp ← get_hwsp st;
    102         let newsp ≝ ?(*addr_add sp v*) in
     102      ! newsp ← addr_add sp v;
    103103      ! st ← set_hwsp newsp st;
    104104        ret ? 〈E0,goto … l st〉
     
    108108        ret ? 〈E0, goto … l st〉
    109109   ].
    110 qed.
    111110
    112111definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
  • src/joint/BEMem.ma

    r1213 r1329  
    1919axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
    2020axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.
     21
     22(* CSC: only pointers to XRAM or code memory ATM *)
     23definition address ≝ beval × beval.
     24
     25definition eq_address: address → address → bool ≝
     26 λaddr1,addr2.
     27  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
     28
     29definition pointer_of_address: address → res pointer ≝
     30 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
     31
     32(*CSC: for pointers of type Code and XData, the next function type can be
     33 strengthtened to never fail *)
     34definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
     35
     36definition addr_add: address → nat → res address ≝
     37 λaddr,n.
     38  do ptr ← pointer_of_address addr ;
     39  address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).
     40
     41definition addr_sub: address → nat → res address ≝
     42 λaddr,n.
     43  do ptr ← pointer_of_address addr ;
     44  address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).
  • src/joint/SemanticUtils.ma

    r1302 r1329  
    4040  Maybe there is a better way to organize the code!!! *)
    4141definition graph_succ_p: label → address → address.
    42  #l #_ generalize in match (refl … (beval_pair_of_pointer (pointer_of_label l)))
    43  cases (beval_pair_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
     42 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
     43 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    4444  [ #res #_ @res
    4545  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     
    5252   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    5353 λparams1,sem_params,globals,ge,st.
    54   (*CSC: the next two lines implement pointer_of_address;
    55     duplicated twice in joint/semantics.ma *)
    56   let 〈v1,v2〉 ≝ pc … st in
    57   do p ← pointer_of_bevals [v1;v2] ;
    58 
     54  do p ← pointer_of_address (pc … st) ;
    5955  let b ≝ pblock p in
    6056  do l ← label_of_pointer p;
  • src/joint/semantics.ma

    r1324 r1329  
    1010   Is this reasonable??? In OCaml it always return a list, but in the frontend
    1111   only the head is kept (or Undef if the list is empty) ??? *)
    12 
    13 definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)
    14 
    15 definition eq_address: address → address → bool ≝
    16  λaddr1,addr2.
    17   eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1812
    1913record more_sem_params (p:params_): Type[1] ≝
     
    10599
    106100definition address_of_label: sem_params → label → address.
    107  #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
    108  cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
     101 #p #l generalize in match (refl … (address_of_pointer (pointer_of_label … p l)))
     102 cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
    109103  [ #res #_ @res
    110104  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
     
    229223        ! vaddrh ← dph_retrieve … st addrh;
    230224        ! vaddrl ← dpl_retrieve … st addrl;
    231         ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
     225        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    232226        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    233227        ! st ← acca_store p … dst v st;
     
    236230        ! vaddrh ← dph_retrieve … st addrh;
    237231        ! vaddrl ← dpl_retrieve … st addrl;
    238         ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
     232        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    239233        ! v ← acca_retrieve … st src;
    240234        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     
    246240      | ADDRESS ident prf ldest hdest ⇒
    247241        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    248         ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
     242        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
    249243        ! st ← dpl_store p ldest laddr st;
    250244        ! st ← dph_store p hdest haddr st;
Note: See TracChangeset for help on using the changeset viewer.