Changeset 1213 for src/common

Timestamp:

Sep 15, 2011, 2:01:56 PM (10 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:

• AST.ma (modified) (1 diff)
• Animation.ma (modified) (3 diffs)
• GenMem.ma (added)
• Pointers.ma (added)
• SmallstepExec.ma (modified) (4 diffs)
• Values.ma (modified) (1 diff)

src/common/AST.ma

@@ -84 +84 @@
 try ( @Ptrue // )
 @Pfalse % #E destruct
+qed.
+
+lemma reflexive_eq_region: ∀r. eq_region r r = true.
+ * //
 qed.
 

src/common/Animation.ma

@@ -18 +18 @@
 inductive snapshot (state:Type[0]) : Type[0] ≝
 | running : trace → state → snapshot state
-| finished : trace → int → mem → snapshot state
+| finished : trace → int → state → snapshot state
 | input_exhausted : trace → snapshot state.
 
@@ -48 +48 @@
 inductive snapshot' (state:Type[0]) : Type[0] ≝
 | running' : trace → state → snapshot' state
-| finished' : nat → trace → int → mem → snapshot' state
+| finished' : nat → trace → int → state → snapshot' state
 | input_exhausted' : trace → snapshot' state
 | failed' : errmsg → nat → state → snapshot' state
@@ -95 +95 @@
 λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
 
+include "common/Mem.ma".
+
 (* Hide the representation of memory to make displaying the results easier. *)
 

src/common/SmallstepExec.ma

@@ -1 @@
-
 include "utilities/extralib.ma".
 include "common/IOMonad.ma".
 include "common/Integers.ma".
 include "common/Events.ma".
-include "common/Mem.ma".
 
 record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
-{ genv  : Type[0]
+{ mem : Type[0]
+; genv  : Type[0]
 ; state : Type[0]
 ; is_final : state → option int
@@ -35 +34 @@
 (* A (possibly non-terminating) execution.   *)
 coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
-| e_stop : trace → int → mem → execution state output input
+| e_stop : trace → int → state → execution state output input
 | e_step : trace → state → execution state output input → execution state output input
 | e_wrong : errmsg → execution state output input
@@ -52 +51 @@
 | Value v ⇒ match v with [ pair t s' ⇒ 
     match is_final ?? exec s' with
-    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
+    [ Some r ⇒ e_stop ??? t r s'
     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
@@ -70 +69 @@
 | Value v ⇒ match v with [ pair t s' ⇒ 
     match is_final ?? exec s' with
-    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
+    [ Some r ⇒ e_stop ??? t r s'
     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))

src/common/Values.ma

@@ -18 +18 @@
 
 include "utilities/Coqlib.ma".
-include "common/AST.ma".
 include "common/Floats.ma".
 include "common/Errors.ma".
-
-include "ASM/BitVectorZ.ma".
-
+include "common/Pointers.ma".
 include "basics/logic.ma".
-
-include "utilities/extralib.ma".
-
-(* To define pointers we need a few details about the memory model.
-
-   There are several kinds of pointers, which differ in which regions of
-   memory they address and the pointer's representation.
-   
-   Pointers are given as kind, block, offset triples, where a block identifies
-   some memory in a given region with an arbitrary concrete address.  A proof
-   is also required that the representation is suitable for the region the
-   memory resides in.  Note that blocks cannot extend out of a region (in
-   particular, a pdata pointer can address any byte in a pdata block - we never
-   need to switch to a larger xdata pointer).
- *)
-
-(* blocks - represented by the region the memory resides in and a unique id *)
-
-record block : Type[0] ≝
-{ block_region : region
-; block_id : Z
-}.
-
-definition eq_block ≝
-λb1,b2.
-  eq_region (block_region b1) (block_region b2) ∧
-  eqZb (block_id b1) (block_id b2)
-.
-
-lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
-  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
-  P (eq_block b1 b2).
-#P * #r1 #i1 * #r2 #i2 #H1 #H2
-whd in ⊢ (?%) @eq_region_elim #H3
-[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
-| @H2 % #E destruct elim H3 /2/
-] qed.
-
-lemma eq_block_b_b : ∀b. eq_block b b = true.
-* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
-qed.
-
-(* Characterise the memory regions which the pointer representations can
-   address.
-
-   pointer_compat <block> <pointer representation> *)
-
-inductive pointer_compat : block → region → Prop ≝
-|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
-|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
-|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
-
-lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
-* * #id *;
-try ( %1 // )
-%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
-qed.
-
-definition is_pointer_compat : block → region → bool ≝
-λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
-
-(* Offsets into the block.  We allow integers like CompCert so that we have
-   the option of extending blocks backwards. *)
-
-record offset : Type[0] ≝ { offv : Z }.
-
-definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
-definition shift_offset : ∀n. offset → BitVector n → offset ≝
-  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
-(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
-definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
-  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
-definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
-  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
-definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
-  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
-definition sub_offset : ∀n. offset → offset → BitVector n ≝
-  λn,x,y. bitvector_of_Z ? (offv x - offv y).
-definition zero_offset ≝ mk_offset OZ.
-definition lt_offset : offset → offset → bool ≝
-  λx,y. Zltb (offv x) (offv y).
 
 (* * A value is either: