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.

File:
1 edited

Legend:

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