Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 ????);
Note: See TracChangeset for help on using the changeset viewer.