Ignore:
Timestamp:
Oct 7, 2011, 6:19:41 PM (9 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.