Changeset 2176 for src/common


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:
src/common
Files:
10 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2105 r2176  
    5454
    5555
    56 (* Memory spaces *)
     56(* Memory spaces
     57
     58   For full 8051 memory spaces support we have internal memory pointers,
     59   PData pointers which are 8 bit pointers to the first page of XData, and
     60   a tagged Any pointer for any of the spaces.
     61   
     62   We only support the 16 bit XData and Code pointers for now.  Some commented
     63   out code is still present to suggest how to add the rest, which includes
     64   having pointers and pointer types contain a region field to indicate what
     65   kind of pointer they are (in addition to the region in the block which
     66   indicates where the pointer points to).
     67
     68 *)
    5769
    5870inductive region : Type[0] ≝
    59   | Any : region
     71(*  | Any : region
    6072  | Data : region
    6173  | IData : region
    62   | PData : region
     74  | PData : region*)
    6375  | XData : region
    6476  | Code : region.
     
    6779λr1,r2.
    6880  match r1 with
    69   [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
     81  [ (*Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
    7082  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
    7183  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
    7284  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
    73   | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
     85  |*) XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
    7486  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
    7587  ].
     
    90102#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    91103
     104(*
    92105(* Carefully defined to be convertably nonzero *)
    93106definition size_pointer : region → nat ≝
    94107λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
     108*)
     109definition size_pointer : nat ≝ 2.
    95110
    96111(* We maintain some reasonable type information through the front end of the
     
    115130inductive typ : Type[0] ≝
    116131  | ASTint : intsize → signedness → typ
    117   | ASTptr : region → typ
     132  | ASTptr : (*region →*) typ
    118133  | ASTfloat : floatsize → typ.
    119134
     
    124139| SigType_Float: SigType
    125140*)
    126 definition SigType_Ptr ≝ ASTptr Any.
     141definition SigType_Ptr ≝ ASTptr (*Any*).
    127142
    128143(* Define these carefully so that we always know that the result is nonzero,
     
    233248  match ty with
    234249  [ ASTint sz _ ⇒ size_intsize sz
    235   | ASTptr r ⇒ size_pointer r
     250  | ASTptr  ⇒ size_pointer
    236251  | ASTfloat sz ⇒ size_floatsize sz ].
    237252
     
    282297  | Init_float64: float → init_data
    283298  | Init_space: nat → init_data
    284   | Init_null: region → init_data
    285   | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
     299  | Init_null: (*region →*) init_data
     300  | Init_addrof: (*region →*) ident → nat → init_data.   (*r address of symbol + offset *)
    286301
    287302(* * Whole programs consist of:
  • src/common/Animation.ma

    r1993 r2176  
    1313[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
    1414| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
    15 | ASTptr _ ⇒ Error ? (msg IllTypedEvent)
     15| ASTptr ⇒ Error ? (msg IllTypedEvent)
    1616].
    1717
  • src/common/ByteValues.ma

    r1987 r2176  
    55include "common/Pointers.ma".
    66
    7 record part (r: region): Type[0] ≝
     7record part (*r: region*): Type[0] ≝
    88 { part_no:> nat
    9  ; part_no_ok: part_no < size_pointer r
     9 ; part_no_ok: part_no < size_pointer (*r*)
    1010 }.
    1111
     
    2525  | BVundef: beval
    2626  | BVByte: Byte → beval
    27   | BVnull: ∀r:region. part r → beval
    28   | BVptr: ∀p:pointer. part (ptype p) → beval.
     27  | BVnull: (*∀r:region.*) part → beval
     28  | BVptr: ∀p:pointer. part (*ptype p*) → beval.
    2929
    3030definition eq_beval: beval → beval → bool ≝
     
    3333   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
    3434   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
    35    | BVnull r1 p1 ⇒ match v2 with [ BVnull r2 p2 ⇒ eq_region … r1 r2 ∧ eqb p1 p2  | _ ⇒ false ]
     35   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
    3636   | BVptr P1 p1  ⇒ match v2 with [ BVptr P2 p2  ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]].
    3737
     
    4141 match l with
    4242  [ nil ⇒
    43      if eqb part (size_pointer (ptype p)) then
     43     if eqb part (size_pointer (*ptype p*)) then
    4444      OK … p
    4545     else
     
    7070(* CSC: use vectors in place of lists? Or even better products of tuples
    7171   (more easily pattern matchable in the finite case)? *)
    72 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (ptype p)) on n: list beval ≝
     72let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (*ptype p*)) on n: list beval ≝
    7373 match n with
    7474  [ O ⇒ λ_.[]
     
    7777
    7878definition bevals_of_pointer: pointer → list beval ≝
    79  λp. bevals_of_pointer_aux p 0 (size_pointer (ptype p)) ….
     79 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
    8080// qed.
    8181
    8282lemma pointer_of_bevals_bevals_of_pointer:
    8383 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
    84 * * #pbl #pok #poff
     84* #pbl #poff
    8585try %
    86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
    87 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) %
     86whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*)
     87whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) %
    8888qed.
    8989
     
    9999(* Fails if the address is not representable as a pair *)
    100100definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
     101 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
     102(*
    101103 λp. match p with [ mk_pointer pty pbl pok poff ⇒
    102104  match pty with
    103105   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
    104106   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
    105    | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].
     107   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    106108% qed.
    107109
    108110definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
     111 λp. list_to_pair ? (bevals_of_pointer p) ?.
     112(*
    109113 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
    110114  match pty return λpty. ? → pty = Code → ? with
    111115   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
    112116   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
    113 [@(pi2 … p) |7: // |8: %] destruct (abs)
     117[@(pi2 … p) |7: // |8: %] destruct (abs)*) %
    114118qed.
    115119
     
    131135  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
    132136  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    133   | BVnull x y ⇒  OK … false
     137  | BVnull y ⇒  OK … false
    134138  | BVptr p q ⇒ OK ? true ].
    135139
  • src/common/FrontEndOps.ma

    r2032 r2176  
    2323  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
    2424  | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
    25   | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *)
    26   | Oaddrstack: nat → constant (ASTptr Any).         (**r stack pointer plus the given offset *)
    27 
    28 definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
     25  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
     27
     28definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ].
    2929
    3030inductive unary_operation : typ → typ → Type[0] ≝
     
    4141  | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
    4242  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
    43   | Optrofint: ∀sz,sg,r. unary_operation (ASTint sz sg) (ASTptr r)             (**r int to pointer with given representation *)
    44   | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
     43  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
     44  | Ointofptr: ∀sz,sg. unary_operation ASTptr (ASTint sz sg).                  (**r pointer to int *)
    4545
    4646inductive binary_operation : typ → typ → typ → Type[0] ≝
     
    6565  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    6666  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
    67   | Oaddp: ∀sz,r.  binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r add an integer to a pointer *)
    68   | Osubpi: ∀sz,r. binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r subtract int from a pointers *)
    69   | Osubpp: ∀sz,r1,r2. binary_operation (ASTptr r1)      (ASTptr r2)          (ASTint sz Signed)   (**r subtract two pointers *)
    70   | Ocmpp: ∀r,sg'. comparison → binary_operation (ASTptr r) (ASTptr r) (ASTint I8 sg').  (**r compare pointers *)
     67  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     68  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
     69  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
     70  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
    7171
    7272
     
    7676[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    7777| ASTfloat sz ⇒ ∀f.P (Vfloat f)
    78 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
     78| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
    7979] →
    8080P v.
    8181#v #t #P *
    8282[ 1,2: //
    83 | #r * //
    84 | #r #b #c #o * //
     83| * //
     84| #b #o * //
    8585] qed.
    8686
     
    9595  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
    9696  | Ofloatconst sz n ⇒ Some ? (Vfloat n)
    97   | Oaddrsymbol r s ofs ⇒
     97  | Oaddrsymbol s ofs ⇒
    9898      match find_symbol s with
    9999      [ None ⇒ None ?
    100       | Some b ⇒ match pointer_compat_dec b r with
     100      | Some b ⇒ (*match pointer_compat_dec b r with
    101101                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
    102102                 | inr _ ⇒ None ?
    103                  ]
     103                 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs))))
    104104      ]
    105105  | Oaddrstack ofs ⇒
    106       Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    107   ]. cases sp // qed.
     106      Some ? (Vptr (mk_pointer sp (shift_offset ? zero_offset (repr I16 ofs))))
     107  ]. (*cases sp // qed.*)
    108108
    109109lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
     
    113113[ #sz #sg #i #v #E normalize in E; destruct //
    114114| #sz #f #v #E normalize in E; destruct //
    115 | #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
    116   cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct
     115| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
     116(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
    117117  //
    118118| #n #v #E whd in E:(??%?); destruct //
     
    132132      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
    133133      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
    134       | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
     134      | Vnull ⇒ Some ? (Vint sz (repr ? 1))
    135135      | _ ⇒ None ?
    136136      ]
     
    145145  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    146146  (* Only conversion of null pointers is specified. *)
    147   | Optrofint sz sg r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    148   | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     147  | Optrofint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
     148  | Ointofptr sz sg ⇒ match arg with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    149149  ].
    150150
     
    159159| #t'' #sz #sg cases t''
    160160  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
    161   | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
     161  | #H #v #v' #H1 @(elim_val_typ … H1) whd %
    162162    [ whd in ⊢ (??%? → ?); #E' destruct; %
    163     | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
     163    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
    164164    ]
    165165  | #f *
     
    174174| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
    175175| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
    176 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     176| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
    177177  whd in ⊢ (??%? → ?); #E destruct //
    178 | #sz #sg #r #v #v' #H @(elim_val_typ … H) %
     178| #sz #sg #v #v' #H @(elim_val_typ … H) %
    179179  [ whd in ⊢ (??%? → ?); #E destruct %
    180   | #b #c #o whd in ⊢ (??%? → ?); #E destruct
     180  | #b #o whd in ⊢ (??%? → ?); #E destruct
    181181  ]
    182182] qed.
     
    215215    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
    216216    | _ ⇒ None ? ]
    217   | Vnull r ⇒ match v2 with
    218     [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
     217  | Vnull ⇒ match v2 with
     218    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
    219219    | _ ⇒ None ?
    220220    ]
     
    226226    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
    227227    | _ ⇒ None ? ]
    228   | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     228  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
    229229  | _ ⇒ None ? ].
    230230
     
    237237          else None ?
    238238    | _ ⇒ None ? ]
    239   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     239  | Vnull  ⇒ match v2 with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    240240  | _ ⇒ None ? ].
    241241
     
    411411        then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    412412        else ev_cmp_mismatch c
    413     | Vnull r2 ⇒ ev_cmp_mismatch c
    414     | _ ⇒ None ? ]
    415   | Vnull r1 ⇒ match v2 with
     413    | Vnull ⇒ ev_cmp_mismatch c
     414    | _ ⇒ None ? ]
     415  | Vnull ⇒ match v2 with
    416416    [ Vptr _ ⇒ ev_cmp_mismatch c
    417     | Vnull r2 ⇒ ev_cmp_match c
     417    | Vnull ⇒ ev_cmp_match c
    418418    | _ ⇒ None ?
    419419    ]
     
    460460  | Ocmpu _ _ c ⇒ ev_cmpu c
    461461  | Ocmpf _ _ c ⇒ ev_cmpf c
    462   | Oaddp _ _ ⇒ ev_addp
    463   | Osubpi _ _ ⇒ ev_subpi
    464   | Osubpp sz _ _ ⇒ ev_subpp sz
    465   | Ocmpp _ _ c ⇒ ev_cmpp c
     462  | Oaddp _ ⇒ ev_addp
     463  | Osubpi _ ⇒ ev_subpi
     464  | Osubpp sz ⇒ ev_subpp sz
     465  | Ocmpp _ c ⇒ ev_cmpp c
    466466  ].
    467467
     
    496496  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
    497497(* pointers *)
    498 | 21,22: #sz #r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c #o ] @(elim_val_typ … V2) #i2
     498| 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    499499  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    500 | #sz #r1 #r2 #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     500| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    501501  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
    502 | #r #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     502| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    503503  whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
    504504] qed.
  • src/common/FrontEndVal.ma

    r2032 r2176  
    66   resolve the sizes; they are not strictly checked. *)
    77
    8 let rec make_parts_aux (r:region) (n:nat) (H:lt n (size_pointer r)) (tl:list (part r)) on n : list (part r) ≝
     8let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝
    99match n return λn.lt n ? → ? with
    10 [ O ⇒ λH'. (mk_part r O H')::tl
    11 | S m ⇒ λH'. make_parts_aux r m ? ((mk_part r n H)::tl)
     10[ O ⇒ λH'. (mk_part (*r*) O H')::tl
     11| S m ⇒ λH'. make_parts_aux (*r*) m ? ((mk_part (*r*) n H)::tl)
    1212] H.
    1313/2/
    1414qed.
    1515
    16 definition make_parts : ∀r:region. list (part r) ≝
    17 λr. make_parts_aux r (pred (size_pointer r)) ? [ ].
     16definition make_parts : (*∀r:region.*) list (part (*r*)) ≝
     17(*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ].
    1818//
    1919qed.
    2020
    21 definition make_be_null : region → list beval ≝
    22 λr. map ?? (λp. BVnull r p) (make_parts r).
     21definition make_be_null : (*region →*) list beval ≝
     22(*λr.*) map ?? (λp. BVnull (*r*) p) (make_parts (*r*)).
    2323
    2424let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
     
    3434| Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *)
    3535| Vptr ptr ⇒ bevals_of_pointer ptr
    36 | Vnull r ⇒ make_be_null r
     36| Vnull  ⇒ make_be_null
    3737].
    3838cases sz in i ⊢ %; //
     
    4141let rec check_be_ptr ptr n t on t ≝
    4242match t with
    43 [ nil ⇒ eqb (size_pointer (ptype ptr)) n
     43[ nil ⇒ eqb (size_pointer (*ptype ptr*)) n
    4444| cons hd tl ⇒
    4545    match hd with
    46     [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no ? pt) n ∧ check_be_ptr ptr (S n) tl
     46    [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no pt) n ∧ check_be_ptr ptr (S n) tl
    4747    | _ ⇒ false
    4848    ]
    4949].
    5050
    51 let rec check_be_null r n t on t ≝
     51let rec check_be_null n t on t ≝
    5252match t with
    53 [ nil ⇒ eqb (size_pointer r) n
     53[ nil ⇒ eqb (size_pointer ) n
    5454| cons hd tl ⇒
    5555    match hd with
    56     [ BVnull r' pt ⇒ eq_region r r' ∧ eqb (part_no ? pt) n ∧ check_be_null r (S n) tl
     56    [ BVnull  pt ⇒  eqb (part_no  pt) n ∧ check_be_null (S n) tl
    5757    | _ ⇒ false
    5858    ]
     
    8888    [ BVundef ⇒ Vundef
    8989    | BVByte b ⇒ build_integer_val ty l
    90     | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
    91     | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef
     90    | BVptr ptr pt ⇒ if eqb (part_no pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
     91    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull else Vundef
    9292    ]
    9393].
  • src/common/GenMem.ma

    r2105 r2176  
    106106definition empty: mem ≝
    107107 mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    108 
    109 definition nullptr: block ≝ mk_block Any OZ.
    110108
    111109(* Allocation of a fresh block with the given bounds.  Return an updated
  • src/common/Globalenvs.ma

    r2117 r2176  
    8282     addresses of the memory region in question - here there are no real
    8383     pointers, so use the real region. *)
    84   let ptr ≝ mk_pointer (block_region m b) b ? (mk_offset p) in
     84  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in
    8585  match id with
    8686  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    8989  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
    9090  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
    91   | Init_addrof r' symb ofs ⇒
     91  | Init_addrof (*r'*) symb ofs ⇒
    9292      match find_symbol … ge symb with
    9393      [ None ⇒ None ?
    94       | Some b' ⇒
     94      | Some b' ⇒ (*
    9595        match pointer_compat_dec b' r' with
    96         [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    97         | inr _ ⇒ None ?
    98         ]
     96        [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs))))
     97        (*| inr _ ⇒ None ?
     98        ]*)
    9999      ]
    100100  | Init_space n ⇒ Some ? m
    101   | Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')
     101  | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*))
    102102  ].
    103 cases b //
    104 qed.
     103(*cases b //
     104qed.*)
    105105
    106106definition size_init_data : init_data → nat ≝
     
    112112  | Init_float64 _ ⇒ 8
    113113  | Init_space n ⇒ max n 0
    114   | Init_null r ⇒ size_pointer r
    115   | Init_addrof r _ _ ⇒ size_pointer r].
     114  | Init_null (*r*) ⇒ size_pointer (*r*)
     115  | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)].
    116116
    117117let rec store_init_data_list (F:Type[0]) (ge:genv_t F)
     
    230230lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
    231231  find_funct F ge v = Some F f →
    232   ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
     232  ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
    233233#F #ge *
    234234[ #f #E normalize in E; destruct
    235235| #sz #i #f #E normalize in E; destruct
    236236| #f #fn #E normalize in E; destruct
    237 | #r #f #E normalize in E; destruct
    238 | * #pty #b #c * #off #f #E whd in E:(??%?);
     237| (*#r*) #f #E normalize in E; destruct
     238| * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?);
    239239  cases off in E ⊢ %; [ 2,3: #x ]
    240240  #E whd in E:(??%?); destruct
    241   %{pty} %{b} %{c} % // @E
     241  (*%{pty}*) %{b} (*%{c}*) % // @E
    242242] qed.
    243243
     
    510510  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
    511511#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
    512 cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ]
    513 [ 12: | *: #F whd in F:(??%?); destruct ]
     512cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
     513[ 4: (*12:*) | *: #F whd in F:(??%?); destruct ]
    514514>vars_irrelevant_to_find_funct_ptr
    515515>vars_irrelevant_to_find_funct_ptr
     
    656656#A #B #V #iV #tf #p #v #f #FF
    657657cases (find_funct_find_funct_ptr ???? FF)
    658 #r * #b * #pc * #E destruct #FFP
     658#b * #E destruct #FFP
    659659change with (find_funct_ptr ???) in ⊢ (??%?);
    660660@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
     
    676676#A #B #ge #ge' #m #b #o #d #SYM
    677677whd in ⊢ (??%%);
    678 cases d #d' try @refl
    679 #id #n whd in ⊢ (??%%);
     678cases d try #d' try @refl
     679#n whd in ⊢ (??%%);
    680680whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
    681681qed.
  • src/common/IO.ma

    r961 r2176  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
     8λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr ⇒ False | ASTfloat _ ⇒ float ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
  • src/common/Pointers.ma

    r1882 r2176  
    4343qed.
    4444
     45(* This is only required for full 8051 memory spaces.
     46
    4547(* Characterise the memory regions which the pointer representations can
    4648   address.
     
    6163definition is_pointer_compat : block → region → bool ≝
    6264λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     65*)
    6366
    6467(* Offsets into the block.  We allow integers like CompCert so that we have
     
    9194(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
    9295record pointer: Type[0] ≝ {
    93    ptype: region;
     96(*   ptype: region;*)
    9497   pblock: block;
    95    pok: pointer_compat pblock ptype;
     98(*   pok: pointer_compat pblock ptype;*)
    9699   poff: offset
    97100 }.
    98101
     102(* As we don't have full memory space support, grab the region from the block
     103   instead. *)
     104definition ptype : pointer → region ≝ λp. block_region (pblock p).
     105
    99106definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    100  λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
     107 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
    101108
    102109(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
    103110definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    104  λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).
     111 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
    105112
    106113definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    107  λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     114 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
    108115
    109116definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    110  λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).
     117 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
    111118
    112119definition eq_pointer: pointer → pointer → bool ≝
    113120 λp1,p2.
    114   eq_region (ptype p1) (ptype p2) ∧ (eq_block (pblock p1) (pblock p2)) ∧
     121  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
    115122   eq_offset (poff p1) (poff p2).
    116123
     
    121128lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
    122129  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
    123 #P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
     130#P * #b0 * #o0 * #b1 * #o1
    124131#Ptrue #Pfalse
    125132whd in match (eq_pointer ??);
    126 @eq_region_elim #reg_eq
    127 [ @eq_block_elim #block_eq
    128   [ change with (eqZb ??) in match (eq_offset ??);
    129     @eqZb_elim #offset_eq
    130     [ destruct @Ptrue %
    131     ]
     133@eq_block_elim #block_eq
     134[ change with (eqZb ??) in match (eq_offset ??);
     135  @eqZb_elim #offset_eq
     136  [ destruct @Ptrue %
    132137  ]
    133138]
  • src/common/Values.ma

    r2032 r2176  
    3838  | Vint: ∀sz:intsize. bvint sz → val
    3939  | Vfloat: float → val
    40   | Vnull: region → val
     40  | Vnull: (*region →*) val
    4141  | Vptr: pointer → val.
    4242
     
    5353  | VTint: ∀sz,sg,i. val_typ (Vint sz i) (ASTint sz sg)
    5454  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
    55   | VTnull: ∀r. val_typ (Vnull r) (ASTptr r)
    56   | VTptr: ∀r,b,c,o. val_typ (Vptr (mk_pointer r b c o)) (ASTptr r).
     55  | VTnull: val_typ Vnull ASTptr
     56  | VTptr: ∀b,o. val_typ (Vptr (mk_pointer b o)) ASTptr.
    5757
    5858(*
     
    7979  match v with
    8080  [ Vint _ n ⇒ n = (zero ?)
    81   | Vnull _ ⇒ True
     81  | Vnull ⇒ True
    8282  | _ ⇒ False
    8383  ].
     
    9191      ∀p. bool_of_val (Vptr p) true
    9292  | bool_of_val_null:
    93       ∀r. bool_of_val (Vnull r) true.
     93      bool_of_val Vnull true.
    9494
    9595axiom ValueNotABoolean : String.
     
    9898λv. match v with
    9999[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    100 | Vnull _ ⇒ OK ? false
     100| Vnull ⇒ OK ? false
    101101| Vptr _ ⇒ OK ? true
    102102| _ ⇒ Error ? (msg ValueNotABoolean)
     
    155155  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    156156  | Vptr _ ⇒ Vfalse
    157   | Vnull _ ⇒ Vtrue
     157  | Vnull ⇒ Vtrue
    158158  | _ ⇒ Vundef
    159159  ].
     
    207207          else Vundef
    208208    | _ ⇒ Vundef ]
    209   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
     209  | Vnull ⇒ match v2 with [ Vnull ⇒ Vzero I32 | _ ⇒ Vundef ]
    210210  | _ ⇒ Vundef ].
    211211
     
    421421        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    422422        else cmp_mismatch c
    423     | Vnull r2 ⇒ cmp_mismatch c
    424     | _ ⇒ Vundef ]
    425   | Vnull r1 ⇒ match v2 with
     423    | Vnull ⇒ cmp_mismatch c
     424    | _ ⇒ Vundef ]
     425  | Vnull ⇒ match v2 with
    426426    [ Vptr _ ⇒ cmp_mismatch c
    427     | Vnull r2 ⇒ cmp_match c
     427    | Vnull ⇒ cmp_match c
    428428    | _ ⇒ Vundef
    429429    ]
     
    442442        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    443443        else cmp_mismatch c
    444     | Vnull r2 ⇒ cmp_mismatch c
    445     | _ ⇒ Vundef ]
    446   | Vnull r1 ⇒ match v2 with
     444    | Vnull ⇒ cmp_mismatch c
     445    | _ ⇒ Vundef ]
     446  | Vnull ⇒ match v2 with
    447447    [ Vptr _ ⇒ cmp_mismatch c
    448     | Vnull r2 ⇒ cmp_match c
     448    | Vnull ⇒ cmp_match c
    449449    | _ ⇒ Vundef
    450450    ]
     
    479479  | Vptr ptr ⇒
    480480    match chunk with
    481     [ ASTptr r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
     481    [ ASTptr ⇒ Vptr ptr
    482482    | _ ⇒ Vundef
    483483    ]
    484   | Vnull r
     484  | Vnull
    485485    match chunk with
    486     [ ASTptr r' ⇒ if eq_region r r' then Vnull r else Vundef
     486    [ ASTptr ⇒ Vnull
    487487    | _ ⇒ Vundef
    488488    ]
     
    10801080  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    10811081#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
    1082 [ #sz #sg | #r | #sz ] whd in ⊢ (?%?); //;
     1082[ #sz #sg | | #sz ] whd in ⊢ (?%?); //;
    10831083qed.
    10841084
Note: See TracChangeset for help on using the changeset viewer.