Changeset 2608 for src/common


Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

Location:
src/common
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2470 r2608  
    55include "common/Pointers.ma".
    66include "utilities/hide.ma".
     7
    78
    89definition cpointer ≝ Σp.ptype p = Code.
     
    1011unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    1112unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     13
    1214
    1315(* this is like a code pointer, but with unbounded offset.
  • src/common/GenMem.ma

    r2332 r2608  
    4949  λA,x,v,f.
    5050    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
    51    
     51
    5252lemma update_block_s:
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?);
     55#A * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
     
    119119qed.
    120120
    121 let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r
    122   let b ≝ mk_block r (nextblock … m) in
     121let rec alloc (m:mem) (lo:Z) (hi:Z) (*(r:region)*) on m : mem × block (*Σb:block. block_region b = r *)
     122  let b ≝ mk_block (nextblock … m) in
    123123  〈mk_mem
    124124    (update_block … b
     
    128128    (succ_nextblock_pos … m),
    129129    b〉.
    130 % qed.
     130(* % qed. *)
    131131
    132132(* Freeing a block.  Return the updated memory state where the given
  • src/common/Globalenvs.ma

    r2601 r2608  
    4747  symbols: identifier_map SymbolTag block;
    4848  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
    49                  ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
     49                 ∃id. lookup … symbols id = Some ? (mk_block (*Code*) (neg b))
    5050}.
    5151
     
    6262  [ None ⇒ functions … g
    6363  | Some b' ⇒
    64       match b' with
     64      match block_id b' with
     65      [ neg p ⇒
     66        pm_set … p (None ?) (functions … g)
     67      | _ ⇒ functions … g
     68      ]
     69(*    match b' with
    6570      [ mk_block r x ⇒
    6671        match r with
     
    7378        ]
    7479      | _ ⇒ functions … g
    75       ]
     80      ] *)
    7681  ]
    7782in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
     83whd in match fns; -fns
     84#b #L
     85cases (functions_inv ? g b ?)
     86[ #id' #L'
     87  cases (identifier_eq … id id')
     88  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
     89  | #NE %{id'} >lookup_remove_miss /2/
     90  ]
     91| cases (lookup ?? (symbols F g) id) in L;
     92  [ normalize //
     93  | normalize nodelta * * normalize nodelta try //
     94    #p
     95    @(eqb_elim … b p)
     96    [ #Heq destruct #NE
     97      >lookup_opt_pm_set_hit in NE; #Hneq
     98      @False_ind
     99      @(absurd … (refl ??) Hneq)
     100    | #id >lookup_opt_pm_set_miss // ]
     101  ]
     102] qed.
     103(*
    78104whd in match fns; -fns
    79105#b #L
     
    93119] qed.
    94120
     121*)
    95122lemma drop_fn_id : ∀F,id,ge.
    96123  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
     
    107134cases (lookup ??? id)
    108135[ normalize //
    109 | * * * [2,3,5,6: #b' ] normalize //
     136| * * [2,3: #b' ] normalize //
    110137  cases (decidable_eq_pos b b')
    111138  [ #E destruct >lookup_opt_pm_set_hit #E destruct
     
    117144λF,name_fun,g.
    118145  let blk_id ≝ nextfunction ? g in
    119   let b ≝ mk_block Code (neg blk_id) in
     146  let b ≝ mk_block (* Code *) (neg blk_id) in
    120147  let g' ≝ drop_fn F (\fst name_fun) g in
    121148  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
     
    260287      let init ≝ extract_init init_info in
    261288      let 〈g,st〉 ≝ g_st in
    262         let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
     289        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) (* r *) in
    263290          let g' ≝ add_symbol ? id b g in
    264291            〈g', st'〉
     
    360387  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
    361388  cases (varsOK … p) #E1 #E2
    362   destruct >E2 cases (alloc ????) #m' #b
     389  destruct >E2 cases (alloc ???) (* cases (alloc ????)*) #m' #b
    363390  @IH /2/
    364391  whd in match (add_symbol ????); whd in match (drop_fn ???);
     
    425452] (refl ? (symbol_for_block F ge b)).
    426453whd in H:(??%?);
    427 cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     454cases b in FFP H ⊢ %; * -b [2,3(*,5,6*): #b ] normalize in ⊢ (% → ?); [ 1,3: * #H cases (H (refl ??)) ]
     455#FFP
    428456cases (functions_inv … ge b FFP)
    429 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
    430 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     457#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block (*Code*) (neg b)) b') id (mk_block (*Code*) (neg b)))
     458lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block (* Code *) (neg b)) b') id (mk_block (* Code *) (neg b)))
    431459cases (find ????)
    432460[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
    433461| * #id' #b' #_ normalize #_ #E destruct
    434462] qed.
    435 
    436463
    437464(*
     
    492519    [ #E destruct
    493520      (* Found one, but it might be shadowed later *)
    494       whd in match (foldl ?????); normalize nodelta
    495       cases (alloc ????) #m' #b normalize nodelta
     521      whd in match (foldl ?????); normalize nodelta     
     522      cases (alloc ???) (* cases (alloc ????) *) #m' #b normalize nodelta
    496523      cut (find_symbol F (add_symbol F id b ge) id = Some ? b)
    497524      [ change with (lookup ????) in ⊢ (??%?);
     
    499526        @lookup_add_hit ]
    500527      #F @IH %2 %{b} @F
    501     | #TL whd in match (foldl ?????); normalize nodelta
    502       cases (alloc ????) #m' #b'
     528    | #TL whd in match (foldl ?????); normalize nodelta     
     529      cases (alloc ???) (*cases (alloc ????)*) #m' #b'
    503530      @IH %1 @TL
    504531    ]
    505532  | #H whd in match (foldl ?????); normalize nodelta
    506     cases (alloc ????) #m' #b' normalize nodelta
     533    cases (alloc ???) (* cases (alloc ????) *) #m' #b' normalize nodelta
    507534    @IH %2
    508535    cases (identifier_eq ? id id')
     
    693720qed.
    694721
    695 lemma alloc_pair : ∀m,m',l,h,l',h',r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].
     722lemma alloc_pair : ∀m,m',l,h,l',h'(*,r*). ∀P:mem×block (*(Σb:block. block_region b = r)*) → mem×block(*(Σb:block. block_region b = r)*) → Type[0].
    696723  nextblock m = nextblock m' →
    697724  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
    698   P (alloc m l h r) (alloc m' l' h' r).
    699 * #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H %
     725  P (alloc m l h (*r*)) (alloc m' l' h' (*r*)).
     726* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' (* #r *) #P #N destruct #H @H %
    700727qed.
    701728
     
    711738  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
    712739#F #G #V #W #P #init #init'
    713 * * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]
     740* * [ 2,3(*,5,6*): #blk ] [ 2: | 1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ]
    714741#vars elim vars
    715742[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
     
    731758      cases (lookup … id')
    732759      [ @FFP1
    733       | * * * try @FFP1 #p try @FFP1
     760      | * * (* * *) try @FFP1 #p try @FFP1
    734761        normalize
    735762        cases (decidable_eq_pos blk p)
     
    776803lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
    777804  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
    778   lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
     805  lookup … (symbols ? ge) id ≠ Some ? (mk_block (*Code*) (neg b)).
    779806#F #ge #id #b #f
    780807whd in match (drop_fn F id ge);
    781808cases (lookup … id)
    782809[ #_ % #E destruct
    783 | * * * [2,3,5,6: #b'] normalize
    784   [4: cases (decidable_eq_pos b b')
     810| * * (* * *) [2,3(*,5,6*): #b'] normalize
     811  [ 2: cases (decidable_eq_pos b b')
    785812    [ #E destruct >lookup_opt_pm_set_hit #E destruct
    786813    | #NE #_ @(not_to_not … NE) #E destruct //
     
    788815  | *: #_ % #E destruct
    789816  ]
    790 ] qed. 
     817] qed.
    791818
    792819lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
    793   lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
     820  lookup … (symbols ? ge) id ≠ Some ? (mk_block (* Code *) (neg b)) →
    794821  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
    795822#F #ge #id #b
     
    797824cases (lookup … id)
    798825[ //
    799 | * * * //
     826| * * (* * *) //
    800827  #b' normalize #NE
    801828  @lookup_opt_pm_set_miss
     
    811838#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
    812839#Mfns
    813 cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
    814 [ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
     840cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ]
     841[ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
    815842whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    816843whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
  • src/common/Pointers.ma

    r2569 r2608  
    11include "ASM/BitVectorZ.ma".
    2 include "common/AST.ma". (* For the regions *)
     2include "common/AST.ma". (* For the /s/regions/size_pointer/ *)
    33include "utilities/extralib.ma".
     4include "basics/deqsets.ma".
    45
    56
     
    2021
    2122record block : Type[0] ≝
    22 { block_region : region
    23 ; block_id : Z
     23{ (* block_region : region ; *)
     24 block_id : Z
    2425}.
     26
     27definition block_region : block → region ≝
     28  λb.
     29  if Zltb (block_id b) OZ then
     30    Code
     31  else
     32    XData.
    2533
    2634definition eq_block ≝
    2735λb1,b2.
    28   eq_region (block_region b1) (block_region b2) ∧
     36(*  eq_region (block_region b1) (block_region b2) ∧*)
    2937  eqZb (block_id b1) (block_id b2)
    3038.
     
    3341  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    3442  P (eq_block b1 b2).
     43#P * #i1 *#i2 #H1 #H2 whd in match (eq_block ??);
     44@(eqZb_elim … i1 i2)
     45[ #H @H1 >H @refl
     46| * #Hneq @H2 % #H @Hneq destruct (H) @refl ]
     47qed.
     48(*
    3549#P * #r1 #i1 * #r2 #i2 #H1 #H2
    3650whd in ⊢ (?%); @eq_region_elim #H3
    3751[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3852| @H2 % #E destruct elim H3 /2/
    39 ] qed.
     53] qed. *)
    4054
    4155lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl
     56* #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4357qed.
    4458
  • src/common/extraGlobalenvs.ma

    r2590 r2608  
    219219** #x1 #x2 #x3 #tl whd in match add_globals;
    220220normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    221 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     221cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    222222normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    223223#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     
    227227lemma globalenv_no_minus_one :
    228228 ∀F,V,i,p.
    229   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
     229  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?.
    230230#F #V #i #p
    231231whd in match find_funct_ptr; normalize nodelta
     
    237237lemma globalenv_no_zero :
    238238 ∀F,V,i,p.
    239   find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
    240 qed.
    241 
     239  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. //
     240qed.
     241
Note: See TracChangeset for help on using the changeset viewer.