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/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].
Note: See TracChangeset for help on using the changeset viewer.