Ignore:
Timestamp:
Jan 28, 2011, 2:41:48 PM (9 years ago)
Author:
campbell
Message:

Use pointer-specific "chunks" of memory for pointer loads and stores,
in particular getting rid of Mint24.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r480 r483  
    9191  ].
    9292
    93 (* * Memory accesses (load and store instructions) are annotated by
    94   a ``memory chunk'' indicating the type, size and signedness of the
    95   chunk of memory being accessed. *)
    96 
    97 ninductive memory_chunk : Type[0] ≝
    98   | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
    99   | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
    100   | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
    101   | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
    102   | Mint24 : memory_chunk
    103   | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
    104   | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
    105   | Mfloat64 : memory_chunk.       (*r 64-bit double-precision float *)
    106 
    10793(* Memory spaces *)
    10894
     
    115101  | Code : region.
    116102
     103ndefinition eq_region : region → region → bool ≝
     104λr1,r2.
     105  match r1 with
     106  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
     107  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
     108  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
     109  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
     110  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
     111  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
     112  ].
     113
     114nlemma eq_region_elim : ∀P:bool → Type. ∀r1,r2.
     115  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
     116  P (eq_region r1 r2).
     117#P r1 r2; ncases r1; ncases r2; #Ptrue Pfalse;
     118ntry ( napply Ptrue // );
     119napply Pfalse; @; #E; ndestruct;
     120nqed.
     121
     122ndefinition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
     123#r1 r2; napply (eq_region_elim ? r1 r2); /2/; nqed.
     124
     125(* * Memory accesses (load and store instructions) are annotated by
     126  a ``memory chunk'' indicating the type, size and signedness of the
     127  chunk of memory being accessed. *)
     128
     129ninductive memory_chunk : Type[0] ≝
     130  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
     131  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
     132  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
     133  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
     134  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
     135  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
     136  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
     137  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
     138
    117139(* * Initialization data for global variables. *)
    118140
     
    120142  | Init_int8: int → init_data
    121143  | Init_int16: int → init_data
    122   | Init_int24: int → init_data
    123144  | Init_int32: int → init_data
    124145  | Init_float32: float → init_data
    125146  | Init_float64: float → init_data
    126147  | Init_space: Z → init_data
     148  | Init_null: region → init_data
    127149  | Init_addrof: ident → int → init_data   (*r address of symbol + offset *)
    128150  | Init_pointer: list init_data → init_data.
Note: See TracChangeset for help on using the changeset viewer.