Changeset 1213 for src/common
- Timestamp:
- Sep 15, 2011, 2:01:56 PM (10 years ago)
- Location:
- src/common
- Files:
-
- 2 added
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1139 r1213 84 84 try ( @Ptrue // ) 85 85 @Pfalse % #E destruct 86 qed. 87 88 lemma reflexive_eq_region: ∀r. eq_region r r = true. 89 * // 86 90 qed. 87 91 -
src/common/Animation.ma
r963 r1213 18 18 inductive snapshot (state:Type[0]) : Type[0] ≝ 19 19 | running : trace → state → snapshot state 20 | finished : trace → int → mem→ snapshot state20 | finished : trace → int → state → snapshot state 21 21 | input_exhausted : trace → snapshot state. 22 22 … … 48 48 inductive snapshot' (state:Type[0]) : Type[0] ≝ 49 49 | running' : trace → state → snapshot' state 50 | finished' : nat → trace → int → mem→ snapshot' state50 | finished' : nat → trace → int → state → snapshot' state 51 51 | input_exhausted' : trace → snapshot' state 52 52 | 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 ]. 96 96 97 include "common/Mem.ma". 98 97 99 (* Hide the representation of memory to make displaying the results easier. *) 98 100 -
src/common/SmallstepExec.ma
r1181 r1213 1 2 1 include "utilities/extralib.ma". 3 2 include "common/IOMonad.ma". 4 3 include "common/Integers.ma". 5 4 include "common/Events.ma". 6 include "common/Mem.ma".7 5 8 6 record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝ 9 { genv : Type[0] 7 { mem : Type[0] 8 ; genv : Type[0] 10 9 ; state : Type[0] 11 10 ; is_final : state → option int … … 35 34 (* A (possibly non-terminating) execution. *) 36 35 coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝ 37 | e_stop : trace → int → mem→ execution state output input36 | e_stop : trace → int → state → execution state output input 38 37 | e_step : trace → state → execution state output input → execution state output input 39 38 | e_wrong : errmsg → execution state output input … … 52 51 | Value v ⇒ match v with [ pair t s' ⇒ 53 52 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' 55 54 | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ] 56 55 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v)) … … 70 69 | Value v ⇒ match v with [ pair t s' ⇒ 71 70 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' 73 72 | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ] 74 73 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v)) -
src/common/Values.ma
r961 r1213 18 18 19 19 include "utilities/Coqlib.ma". 20 include "common/AST.ma".21 20 include "common/Floats.ma". 22 21 include "common/Errors.ma". 23 24 include "ASM/BitVectorZ.ma". 25 22 include "common/Pointers.ma". 26 23 include "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 of33 memory they address and the pointer's representation.34 35 Pointers are given as kind, block, offset triples, where a block identifies36 some memory in a given region with an arbitrary concrete address. A proof37 is also required that the representation is suitable for the region the38 memory resides in. Note that blocks cannot extend out of a region (in39 particular, a pdata pointer can address any byte in a pdata block - we never40 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 : region47 ; block_id : Z48 }.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 #H260 whd in ⊢ (?%) @eq_region_elim #H361 [ 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 @refl67 qed.68 69 (* Characterise the memory regions which the pointer representations can70 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) s76 | pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData77 | 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 destruct83 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 have89 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).108 24 109 25 (* * A value is either:
Note: See TracChangeset
for help on using the changeset viewer.