Changeset 1213 for src/common


Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (8 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).

Location:
src/common
Files:
2 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1139 r1213  
    8484try ( @Ptrue // )
    8585@Pfalse % #E destruct
     86qed.
     87
     88lemma reflexive_eq_region: ∀r. eq_region r r = true.
     89 * //
    8690qed.
    8791
  • src/common/Animation.ma

    r963 r1213  
    1818inductive snapshot (state:Type[0]) : Type[0] ≝
    1919| running : trace → state → snapshot state
    20 | finished : trace → int → mem → snapshot state
     20| finished : trace → int → state → snapshot state
    2121| input_exhausted : trace → snapshot state.
    2222
     
    4848inductive snapshot' (state:Type[0]) : Type[0] ≝
    4949| running' : trace → state → snapshot' state
    50 | finished' : nat → trace → int → mem → snapshot' state
     50| finished' : nat → trace → int → state → snapshot' state
    5151| input_exhausted' : trace → snapshot' state
    5252| failed' : errmsg → nat → state → snapshot' state
     
    9595λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
    9696
     97include "common/Mem.ma".
     98
    9799(* Hide the representation of memory to make displaying the results easier. *)
    98100
  • src/common/SmallstepExec.ma

    r1181 r1213  
    1 
    21include "utilities/extralib.ma".
    32include "common/IOMonad.ma".
    43include "common/Integers.ma".
    54include "common/Events.ma".
    6 include "common/Mem.ma".
    75
    86record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9 { genv  : Type[0]
     7{ mem : Type[0]
     8; genv  : Type[0]
    109; state : Type[0]
    1110; is_final : state → option int
     
    3534(* A (possibly non-terminating) execution.   *)
    3635coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
    37 | e_stop : trace → int → mem → execution state output input
     36| e_stop : trace → int → state → execution state output input
    3837| e_step : trace → state → execution state output input → execution state output input
    3938| e_wrong : errmsg → execution state output input
     
    5251| Value v ⇒ match v with [ pair t s' ⇒
    5352    match is_final ?? exec s' with
    54     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     53    [ Some r ⇒ e_stop ??? t r s'
    5554    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    5655| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     
    7069| Value v ⇒ match v with [ pair t s' ⇒
    7170    match is_final ?? exec s' with
    72     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     71    [ Some r ⇒ e_stop ??? t r s'
    7372    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    7473| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
  • 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.