Changeset 483


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

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

Location:
Deliverables/D3.1/C-semantics
Files:
4 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.
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r481 r483  
    631631  | By_nothing: mode.
    632632
    633 ndefinition access_mode_pointer : region → mode ≝ λr.
    634 By_value (match r with
    635 [ Any   ⇒ Mint24
    636 | Data  ⇒ Mint8unsigned
    637 | IData ⇒ Mint8unsigned
    638 | PData ⇒ Mint8unsigned
    639 | XData ⇒ Mint16unsigned
    640 | Code ⇒ Mint16unsigned
    641 ]).
    642 
    643633ndefinition access_mode : type → mode ≝ λty.
    644634  match ty with
     
    654644                            | F64 ⇒ By_value Mfloat64 ]
    655645  | Tvoid ⇒ By_nothing
    656   | Tpointer r _ ⇒ access_mode_pointer r
     646  | Tpointer r _ ⇒ By_value (Mpointer r)
    657647  | Tarray _ _ _ ⇒ By_reference
    658648  | Tfunction _ _ ⇒ By_reference
    659649  | Tstruct _ fList ⇒ By_nothing
    660650  | Tunion _ fList ⇒ By_nothing
    661   | Tcomp_ptr r _ ⇒ access_mode_pointer r
     651  | Tcomp_ptr r _ ⇒ By_value (Mpointer r)
    662652  ].
    663653
  • Deliverables/D3.1/C-semantics/Mem.ma

    r480 r483  
    109109  The following functions extract the size information from a chunk. *)
    110110
    111 (* FIXME: coercions *)
     111ndefinition size_pointer : region → Z ≝
     112λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     113
    112114ndefinition size_chunk : memory_chunk → Z ≝
    113   λchunk.match chunk return λ_.Z with
     115  λchunk.match chunk with
    114116  [ Mint8signed => 1
    115117  | Mint8unsigned => 1
    116118  | Mint16signed => 2
    117119  | Mint16unsigned => 2
    118   | Mint24 ⇒ 3
    119120  | Mint32 => 4
    120121  | Mfloat32 => 4
    121   | Mfloat64 => 8 ].
    122  
     122  | Mfloat64 => 8
     123  | Mpointer r ⇒ size_pointer r
     124  ].
     125
     126ndefinition pred_size_pointer : region → nat ≝
     127λsp. match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
     128
    123129ndefinition pred_size_chunk : memory_chunk → nat ≝
    124130  λchunk.match chunk with
     
    127133  | Mint16signed => 1
    128134  | Mint16unsigned => 1
    129   | Mint24 ⇒ 2
    130135  | Mint32 => 3
    131136  | Mfloat32 => 3
    132   | Mfloat64 => 7].
     137  | Mfloat64 => 7
     138  | Mpointer r ⇒ pred_size_pointer r
     139  ].
    133140
    134141alias symbol "plus" (instance 2) = "integer plus".
    135142nlemma size_chunk_pred:
    136143  ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
    137 #chunk;ncases chunk;//;
     144#chunk;ncases chunk;//; #r; ncases r; napply refl;
    138145nqed.
    139146
     
    167174nqed.
    168175
    169 (* TODO: nicer proof (though this does mirror the coq one!) *)
    170176nlemma align_size_chunk_divides:
    171177  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    172 #chunk;ncases chunk;nnormalize;/3/;
     178#chunk;ncases chunk;##[##8:#r; ncases r ##]nnormalize;/3/;
    173179nqed.
    174180
     
    177183    size_chunk chunk1 = size_chunk chunk2 →
    178184      align_chunk chunk1 = align_chunk chunk2.
    179 #chunk1;#chunk2;ncases chunk1;ncases chunk2;nnormalize;//;#H;ndestruct;
     185#chunk1;#chunk2;
     186ncases chunk1; ntry ( #r1 ncases r1 );
     187ncases chunk2; ntry ( #r2 ncases r2 );
     188nnormalize;//;
    180189nqed.
    181190
     
    721730  | Init_int16 n ⇒
    722731      setN 1 pos (Vint n) (reccall (pos + oneZ))
    723   | Init_int24 n ⇒
    724       setN 2 pos (Vint n) (reccall (pos + oneZ))
    725732  | Init_int32 n ⇒
    726733      setN 3 pos (Vint n) (reccall (pos + oneZ))
     
    730737      setN 7 pos (Vfloat f) (reccall (pos + oneZ))
    731738  | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
     739  | Init_null r ⇒ setN (pred_size_pointer r) pos (Vint zero) (reccall (pos + oneZ))
    732740  | Init_addrof s n ⇒
    733741      (* Not handled properly yet *)
     
    748756  [ Init_int8 _ ⇒ 1
    749757  | Init_int16 _ ⇒ 2
    750   | Init_int24 _ ⇒ 3
    751758  | Init_int32 _ ⇒ 4
    752759  | Init_float32 _ ⇒ 4
    753760  | Init_float64 _ ⇒ 8
    754761  | Init_space n ⇒ Zmax n 0
     762  | Init_null r ⇒ size_pointer r
    755763  | Init_addrof _ _ ⇒ 4
    756764  | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].
  • Deliverables/D3.1/C-semantics/Values.ma

    r482 r483  
    407407    | Mint16signed ⇒ Vint (sign_ext 16 n)
    408408    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    409     | Mint24 ⇒ Vint (zero_ext 24 n)
    410409    | Mint32 ⇒ Vint n
     410    | Mpointer r ⇒ if eq n zero then Vint zero else Vundef
    411411    | _ ⇒ Vundef
    412412    ]
    413   | Vptr pty b ofs ⇒
    414     match pty with
    415     [ Any ⇒ match chunk with [ Mint24 ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    416     | Data ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    417     | IData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    418     | PData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    419     | XData ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    420     | Code ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     413  | Vptr r b ofs ⇒
     414    match chunk with
     415    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef
     416    | _ ⇒ Vundef
    421417    ]
    422418  | Vfloat f ⇒
     
    10131009  ∀chunk,v1,v2.
    10141010  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1015 #chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk; nwhd in ⊢ (?%?); //;
     1011#chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk;
     1012##[ ##8: #r ##] nwhd in ⊢ (?%?); //;
    10161013nqed.
    10171014
Note: See TracChangeset for help on using the changeset viewer.