Changeset 2176 for src/joint


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1993 r2176  
    2323definition is_address : (beval × beval) → Prop ≝ λa.
    2424  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
    25     \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
    26     \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
     25    \fst a = BVptr p p0 ∧ part_no p0 = 0 ∧
     26    \snd a = BVptr p p1 ∧ part_no p1 = 1.
    2727
    2828definition is_addressb : (beval × beval) → bool ≝ λa.
     
    4444  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
    4545#P * *
    46 [4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
     46[4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
    4747#p0 #part0 #a1
    4848whd in match is_addressb; normalize nodelta
     
    5050#H >H
    5151[ @(eqb_elim part0 0) #Heq
    52   [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
     52  [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?);
    5353    [4: @eq_pointer_elim #Heq'
    5454      [ @(eqb_elim part1 1) #Heq''
     
    8989destruct(H0 H4)
    9090qed.
    91 
     91(* For full 8051 memory spaces
    9292definition pointer_compat' ≝ λb,r.
    9393  match b with
     
    116116]
    117117qed.
    118 
     118*)
    119119lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     120** #a0 #a1 ***** #z #o
     121#Hr
     122(*
    120123** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
    121124cases r in Hr ⊢ %; #Hr *
     125*)
    122126** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
    123127destruct normalize
     
    133137#p
    134138lapply (refl … p)
    135 generalize in match p in ⊢ (???%→%); **
     139generalize in match p in ⊢ (???%→%); *(***)
    136140whd in match (address_of_pointer ?);
    137 #b #H #o #EQp * #a0 #a1
     141#b (*#H*) #o #EQp * #a0 #a1
    138142normalize #EQ destruct(EQ)
     143%{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] %
     144(*
    139145%{p} >EQp [1,3: %]
    140146% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
     147*)
    141148qed.
    142149
     
    146153lemma address_of_pointer_is_safe :
    147154  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
     155#p normalize % qed.
     156(*
    148157****#z #H
    149158lapply (pointer_compat_from_ind ?? H) * #o
    150159normalize %
    151 qed.
     160qed.*)
    152161
    153162definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
     
    157166
    158167definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
     168cases H -H * #b #o normalize cases b * #z #EQ destruct
     169%{«mk_pointer  (mk_block Code z)  o,I»}
     170% [2: % [2: % [ % [ % ]]]] %
     171qed.
     172(*
    159173cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
    160174lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
    161175%{«mk_pointer ? (mk_block Code z) H o,I»}
    162176% [2: % [2: % [ % [ % ]] % |]|]
    163 qed.
     177qed.*)
    164178
    165179(* Paolo: why only code pointers and not XRAM too? *)
  • src/joint/SemanticUtils.ma

    r1515 r2176  
    2424 pointer → label → Σp:pointer. ptype p = Code ≝
    2525 λoldpc,l.
    26   mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
     26  mk_pointer
     27   (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))).
    2828// qed.
    2929
  • src/joint/semantics.ma

    r1999 r2176  
    228228      let l' ≝ joint_if_entry … fn in
    229229      let st ≝ set_regs p regs st in
    230       let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
     230      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) (mk_offset 0) in
    231231      ! newpc ← address_of_label … ge pointer_in_fn l' ;
    232232      let st ≝ set_pc … newpc st in
     
    244244        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    245245     ].
    246 % qed.
     246(*% qed.*)
    247247
    248248definition eval_call_id:
     
    301301      | ADDRESS ident prf ldest hdest ⇒
    302302        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol … ge ident);
    303         ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
     303        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset);
    304304        ! st ← dpl_store p ldest laddr st;
    305305        ! st ← dph_store p hdest haddr st;
     
    365365      ! st ← pop_frame … ge st;
    366366        return 〈E0,set_pc … ra st〉].
    367 cases addr //
    368 qed.
     367(*cases addr //
     368qed.*)
    369369
    370370definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
     
    401401 (* Invariant: a -1 block is unused in common/Globalenvs *)
    402402 let b ≝ mk_block Code (-1) in
    403  let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
     403 let ptr ≝ mk_pointer b (mk_offset 0) in
    404404 let addr ≝ address_of_code_pointer ptr in
    405405  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
     
    416416  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    417417  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    418   let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
    419   let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
    420   let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
     418  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset 0) in
     419  let spp ≝ mk_pointer spb (mk_offset external_ram_size) in
     420  let ispp ≝ mk_pointer ispb (mk_offset 47) in
    421421  do sp ← address_of_pointer spp ;
    422422  let main ≝ prog_main … p in
     
    430430  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    431431  ].
    432 [3: % | cases ispb | cases spb] *; #r #off #E >E %
    433 qed.
     432(*[3: % | cases ispb | cases spb] *; #r #off #E >E %
     433qed.*)
    434434
    435435definition joint_fullexec :
Note: See TracChangeset for help on using the changeset viewer.