Changeset 1213 for src/common/Values.ma


Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (9 years ago)
Author:
sacerdot
Message:

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r961 r1213  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "common/AST.ma".
    2120include "common/Floats.ma".
    2221include "common/Errors.ma".
    23 
    24 include "ASM/BitVectorZ.ma".
    25 
     22include "common/Pointers.ma".
    2623include "basics/logic.ma".
    27 
    28 include "utilities/extralib.ma".
    29 
    30 (* To define pointers we need a few details about the memory model.
    31 
    32    There are several kinds of pointers, which differ in which regions of
    33    memory they address and the pointer's representation.
    34    
    35    Pointers are given as kind, block, offset triples, where a block identifies
    36    some memory in a given region with an arbitrary concrete address.  A proof
    37    is also required that the representation is suitable for the region the
    38    memory resides in.  Note that blocks cannot extend out of a region (in
    39    particular, a pdata pointer can address any byte in a pdata block - we never
    40    need to switch to a larger xdata pointer).
    41  *)
    42 
    43 (* blocks - represented by the region the memory resides in and a unique id *)
    44 
    45 record block : Type[0] ≝
    46 { block_region : region
    47 ; block_id : Z
    48 }.
    49 
    50 definition eq_block ≝
    51 λb1,b2.
    52   eq_region (block_region b1) (block_region b2) ∧
    53   eqZb (block_id b1) (block_id b2)
    54 .
    55 
    56 lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
    57   (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    58   P (eq_block b1 b2).
    59 #P * #r1 #i1 * #r2 #i2 #H1 #H2
    60 whd in ⊢ (?%) @eq_region_elim #H3
    61 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    62 | @H2 % #E destruct elim H3 /2/
    63 ] qed.
    64 
    65 lemma eq_block_b_b : ∀b. eq_block b b = true.
    66 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
    67 qed.
    68 
    69 (* Characterise the memory regions which the pointer representations can
    70    address.
    71 
    72    pointer_compat <block> <pointer representation> *)
    73 
    74 inductive pointer_compat : block → region → Prop ≝
    75 |        same_compat : ∀s,id. pointer_compat (mk_block s id) s
    76 |      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
    77 |   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    78 
    79 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    80 * * #id *;
    81 try ( %1 // )
    82 %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
    83 qed.
    84 
    85 definition is_pointer_compat : block → region → bool ≝
    86 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    87 
    88 (* Offsets into the block.  We allow integers like CompCert so that we have
    89    the option of extending blocks backwards. *)
    90 
    91 record offset : Type[0] ≝ { offv : Z }.
    92 
    93 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    94 definition shift_offset : ∀n. offset → BitVector n → offset ≝
    95   λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    96 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
    97 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    98   λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
    99 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    100   λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    101 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    102   λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
    103 definition sub_offset : ∀n. offset → offset → BitVector n ≝
    104   λn,x,y. bitvector_of_Z ? (offv x - offv y).
    105 definition zero_offset ≝ mk_offset OZ.
    106 definition lt_offset : offset → offset → bool ≝
    107   λx,y. Zltb (offv x) (offv y).
    10824
    10925(* * A value is either:
Note: See TracChangeset for help on using the changeset viewer.