find more locations in the context

examples/malloc1.c

@@ -79,8 +79,6 @@ void* slab_alloc(struct slab *s)
 void slab_free(struct slab *s, void* x)
 {
     struct freelist* f = x;
-    // unfold slab to learn that struct_freelist < entry_size
-    rc_unfold(*s);
 
     f->next = s->free;
     s->free = f;

examples/mpool.c

@@ -331,7 +331,6 @@ void *mpool_alloc(struct mpool *p) {
 [[rc::ensures("p @ &frac<q, {(n + 1)%nat} @ mpool<entry_size>>")]]
 void mpool_free(struct mpool *p, void *ptr) {
   struct mpool_entry *e = ptr;
-  rc_unfold(p->entry_size);
 
   /* Store the newly freed entry in the front of the free list. */
   sl_lock(&p->lock);
@@ -418,7 +417,6 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
         chunk->size = before_start;
       }
 
-      rc_unfold(*chunk);
       rc_uninit_strengthen_align(*start);
       ret = (void *)start;
       break;
@@ -426,7 +424,6 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
 
     prev = &chunk->next_chunk;
   }
-  rc_unfold(*prev);
 
   sl_unlock(&p->lock);
 

examples/proofs/malloc1/generated_code.v

@@ -109,28 +109,22 @@ Section code.
   Definition loc_104 : location_info := LocationInfo file_0 59 8 59 9.
   Definition loc_105 : location_info := LocationInfo file_0 59 19 59 33.
   Definition loc_108 : location_info := LocationInfo file_0 81 4 81 27.
-  Definition loc_109 : location_info := LocationInfo file_0 83 4 83 10.
-  Definition loc_110 : location_info := LocationInfo file_0 83 10 83 5.
-  Definition loc_111 : location_info := LocationInfo file_0 85 4 85 22.
-  Definition loc_112 : location_info := LocationInfo file_0 86 4 86 16.
-  Definition loc_113 : location_info := LocationInfo file_0 86 4 86 11.
-  Definition loc_114 : location_info := LocationInfo file_0 86 4 86 5.
-  Definition loc_115 : location_info := LocationInfo file_0 86 4 86 5.
-  Definition loc_116 : location_info := LocationInfo file_0 86 14 86 15.
-  Definition loc_117 : location_info := LocationInfo file_0 86 14 86 15.
-  Definition loc_118 : location_info := LocationInfo file_0 85 4 85 11.
-  Definition loc_119 : location_info := LocationInfo file_0 85 4 85 5.
-  Definition loc_120 : location_info := LocationInfo file_0 85 4 85 5.
-  Definition loc_121 : location_info := LocationInfo file_0 85 14 85 21.
-  Definition loc_122 : location_info := LocationInfo file_0 85 14 85 21.
-  Definition loc_123 : location_info := LocationInfo file_0 85 14 85 15.
-  Definition loc_124 : location_info := LocationInfo file_0 85 14 85 15.
-  Definition loc_125 : location_info := LocationInfo file_0 83 4 83 9.
-  Definition loc_126 : location_info := LocationInfo file_0 83 5 83 9.
-  Definition loc_127 : location_info := LocationInfo file_0 83 7 83 8.
-  Definition loc_128 : location_info := LocationInfo file_0 83 7 83 8.
-  Definition loc_129 : location_info := LocationInfo file_0 81 25 81 26.
-  Definition loc_130 : location_info := LocationInfo file_0 81 25 81 26.
+  Definition loc_109 : location_info := LocationInfo file_0 85 4 85 22.
+  Definition loc_110 : location_info := LocationInfo file_0 86 4 86 16.
+  Definition loc_111 : location_info := LocationInfo file_0 86 4 86 11.
+  Definition loc_112 : location_info := LocationInfo file_0 86 4 86 5.
+  Definition loc_113 : location_info := LocationInfo file_0 86 4 86 5.
+  Definition loc_114 : location_info := LocationInfo file_0 86 14 86 15.
+  Definition loc_115 : location_info := LocationInfo file_0 86 14 86 15.
+  Definition loc_116 : location_info := LocationInfo file_0 85 4 85 11.
+  Definition loc_117 : location_info := LocationInfo file_0 85 4 85 5.
+  Definition loc_118 : location_info := LocationInfo file_0 85 4 85 5.
+  Definition loc_119 : location_info := LocationInfo file_0 85 14 85 21.
+  Definition loc_120 : location_info := LocationInfo file_0 85 14 85 21.
+  Definition loc_121 : location_info := LocationInfo file_0 85 14 85 15.
+  Definition loc_122 : location_info := LocationInfo file_0 85 14 85 15.
+  Definition loc_123 : location_info := LocationInfo file_0 81 25 81 26.
+  Definition loc_124 : location_info := LocationInfo file_0 81 25 81 26.
 
   (* Definition of struct [freelist]. *)
   Program Definition struct_freelist := {|
@@ -258,15 +252,13 @@ Section code.
     f_code := (
       <[ "#0" :=
         "f" <-{ LPtr }
-          LocInfoE loc_129 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_129 (use{LPtr} (LocInfoE loc_130 ("x"))))) ;
+          LocInfoE loc_123 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_123 (use{LPtr} (LocInfoE loc_124 ("x"))))) ;
         locinfo: loc_109 ;
-        expr: (LocInfoE loc_125 (&(LocInfoE loc_127 (!{LPtr} (LocInfoE loc_128 ("s")))))) ;
-        locinfo: loc_111 ;
-        LocInfoE loc_118 ((LocInfoE loc_119 (!{LPtr} (LocInfoE loc_120 ("f")))) at{struct_freelist} "next") <-{ LPtr }
-          LocInfoE loc_121 (use{LPtr} (LocInfoE loc_122 ((LocInfoE loc_123 (!{LPtr} (LocInfoE loc_124 ("s")))) at{struct_slab} "free"))) ;
-        locinfo: loc_112 ;
-        LocInfoE loc_113 ((LocInfoE loc_114 (!{LPtr} (LocInfoE loc_115 ("s")))) at{struct_slab} "free") <-{ LPtr }
-          LocInfoE loc_116 (use{LPtr} (LocInfoE loc_117 ("f"))) ;
+        LocInfoE loc_116 ((LocInfoE loc_117 (!{LPtr} (LocInfoE loc_118 ("f")))) at{struct_freelist} "next") <-{ LPtr }
+          LocInfoE loc_119 (use{LPtr} (LocInfoE loc_120 ((LocInfoE loc_121 (!{LPtr} (LocInfoE loc_122 ("s")))) at{struct_slab} "free"))) ;
+        locinfo: loc_110 ;
+        LocInfoE loc_111 ((LocInfoE loc_112 (!{LPtr} (LocInfoE loc_113 ("s")))) at{struct_slab} "free") <-{ LPtr }
+          LocInfoE loc_114 (use{LPtr} (LocInfoE loc_115 ("f"))) ;
         Return (VOID)
       ]> $∅
     )%E

theories/typing/own.v

@@ -300,6 +300,17 @@ Section ptr.
     SimplifyGoalVal p (l @ ptr)%I (Some 50%N) :=
     λ T, i2p (simplify_ptr_goal_val p l T).
 
+  Lemma find_in_context_type_loc_own l T:
+    (∃ l1 β1 β ty, l1 ◁ₗ{β1} (l @ &frac{β} ty) ∗ (l1 ◁ₗ{β1} (l @ &frac{β} (singleton_place l)) -∗ T (own_state_min β1 β, ty))) -∗
+    find_in_context (FindLoc l) T.
+  Proof.
+    iDestruct 1 as (l1 β1 β ty) "[[% [Hmt Hl]] HT]".
+    iExists (_, _) => /=. iFrame. iApply "HT".
+    iSplit => //. by iFrame.
+  Qed.
+  Global Instance find_in_context_type_loc_own_inst l :
+    FindInContext (FindLoc l) 1%nat :=
+    λ T, i2p (find_in_context_type_loc_own l T).
 End ptr.
 
 Section null.

tutorial/t04_alloc.c

@@ -25,14 +25,12 @@ void *alloc(size_t size) {
 
       if(cur->size == size) {
         *prev = cur->next;
-        rc_unfold(*prev);
         sl_unlock(&allocator_state.lock);
         return cur;
       }
       if(cur->size >= size + sizeof(struct alloc_entry)) {
         cur->size -= size;
         void *ret = ((unsigned char*)cur + cur->size);
-        rc_unfold(*prev);
         sl_unlock(&allocator_state.lock);
         return ret;
       }
@@ -40,7 +38,6 @@ void *alloc(size_t size) {
       prev = &cur->next;
     }
 
-    rc_unfold(*prev);
     sl_unlock(&allocator_state.lock);
   }