Skip to content

New modifies clauses with buffers, references and regions

Jump to bottom Edit New page
Tahina Ramananandro (professional account) edited this page May 12, 2021 · 6 revisions

Context and motivation

What is a modifies clause?

A modifies clause is an assertion, within a stateful F* function, which tracks the set l of memory locations modified by the function, in such a way that any memory location disjoint from l has its liveness and contents preserved.

Modifies clauses are meant to avoid quantifications when reasoning about framing: this is called the small footprint approach. Thus, a modifies clause is most often part of the postcondition of a stateful F* function.

NOTE: this page assumes that the reader is familiar with the HyperStack (or at least the HyperHeap) memory model of F* and Low*.

The current modifies clauses from FStar.HyperStack and FStar.Buffer

F* has had modifies clauses for references and buffers since the inception of the HyperStack model. We explain them in this section, before proposing a more general alternative in the next section.

References

The following code illustrates the effects of using the current modifies clauses for references.

module Set = FStar.Set
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

assume
val f (x: HS.reference int) : HST.ST unit
  (requires (fun h -> h `HS.contains` x))
  (ensures (fun h _ h' ->
    h' `HS.contains` x /\
    HS.modifies_one (HS.frameOf x) h h' /\
    HS.modifies_ref (HS.frameOf x) (Set.singleton (HS.as_addr x)) h h'
  ))

let g (x y: HS.reference int) : HST.ST unit
  (requires (fun h ->
    h `HS.contains` y /\ h `HS.contains` x /\
    (HS.frameOf x == HS.frameOf y ==> HS.as_addr x <> HS.as_addr y)
  ))
  (ensures (fun h _ h' ->
    h' `HS.contains` y /\
    HS.sel h' y == HS.sel h y
  ))
= f x

Independently of the actual implementation of f, F* derives the preservation of the liveness and contents of y in g from the modifies clauses in the specification of f, and the disjointness of x and y as specified in the precondition of g.

The modifies clause is split into two parts: one for the set of regions, and one per region for the set of addresses modified in the given region. This eases reasoning about sets of references located in different regions, but may complicate reasoning about references whose regions are unknown. In particular, it is possible, but very hard, to write a modifies clause for a function (e.g. swap) taking two disjoint references from arbitrary regions (maybe the same.) Here is the solution:

let swap (x y: HST.reference int) : HST.ST unit
  (requires (fun h ->
    h `HS.contains` y /\ h `HS.contains` x /\
    (HS.frameOf x == HS.frameOf y ==> HS.as_addr x <> HS.as_addr y)
  ))
  (ensures (fun h _ h' ->
    h' `HS.contains` y /\
    h' `HS.contains` x /\
    HS.sel h' y == HS.sel h x /\
    HS.sel h' x == HS.sel h y /\
    HS.modifies (Set.union (Set.singleton (HS.frameOf x)) (Set.singleton (HS.frameOf y))) h h' /\ (
    if HS.frameOf x = HS.frameOf y
    then
      HS.modifies_ref
        (HS.frameOf x)
        (Set.union (Set.singleton (HS.as_addr x)) (Set.singleton (HS.as_addr y)))
        h h'
    else
      HS.modifies_ref (HS.frameOf x) (Set.singleton (HS.as_addr x)) h h' /\
      HS.modifies_ref (HS.frameOf y) (Set.singleton (HS.as_addr y)) h h'
  )))
= let vx = HST.op_Bang x in
  let vy = HST.op_Bang y in
  x `HST.op_Colon_Equals` vy;
  y `HST.op_Colon_Equals` vx

Of course, as one may think, this is untractable with 3 or more references.

Moreover, for a given region r, modifies_ref only works if the livenesses of all objects in r are preserved. Thus, it cannot be used for deallocations.

Buffers

The following code illustrates the effects of using the current modifies clauses for buffers.

module B = FStar.Buffer

assume
val f (x: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` x))
  (ensures (fun h _ h' ->
    h' `B.live` x /\
    B.modifies_1 x h h'
  ))

let g (x y: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` y /\ h `B.live` x /\ x `B.disjoint` y))
  (ensures (fun h _ h' ->
    h' `B.live` y /\
    B.as_seq h' y == B.as_seq h y
  ))
= f x

Independently of the actual implementation of f, F* derives the preservation of the liveness and contents of y in g from the modifies clauses in the specification of f, and the disjointness of x and y as specified in the precondition of g.

Contrary to references, the modifies clause for buffers is not split across regions. There are modifies clauses for 1 and 2 buffers, independently of their regions. The modifies clause for 2 buffers can be used to rewrite swap for two disjoint buffers of size 1 located in arbitrary regions:

let swap (x y: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` y /\ h `B.live` x /\ B.length x == 1 /\ B.length y == 1 /\ x `B.disjoint` y))
  (ensures (fun h _ h' ->
    h' `B.live` y /\
    h' `B.live` x /\
    B.as_seq h' y `Seq.equal` B.as_seq h x /\
    B.as_seq h' x `Seq.equal` B.as_seq h y /\
    B.modifies_2 x y h h'
  ))
= let vx = B.index x 0ul in
  let vy = B.index y 0ul in
  B.upd x 0ul vy;
  B.upd y 0ul vx

There is also support for 3 buffers, but not more. Moreover, there is no support for mixed buffers and references (the existing clause, FStar.Buffer.modifies_bufs_and_refs, is way too coarse since it says that the address of a buffer is modified in all regions.)

Furthermore, those modifies clauses for buffers only work for updates, not for deallocations, since they all assume that the livenesses of all objects are preserved.

The new modifies clauses: FStar.Modifies (or LowStar.Modifies for the new buffers)

As exposed above, the current modifies clauses suffer the following shortcomings:

  • no support for more than 3 memory locations
  • no support for references from unknown regions
  • no support for mixtures of memory locations of different kinds
  • no support for deallocation

We developed a new modifies clause addressing all of those at once.

These new modifies clauses are available already for F* references (FStar.HyperStack) and Low* old buffers (FStar.Buffer). They are specified in FStar.Modifies. Corresponding modifies clauses are also available for F* references and Low* new buffers (LowStar.Buffer), specified in LowStar.Modifies. In the latter case, we isolated the patterns away in LowStar.ModifiesPat, which should now be used instead of LowStar.Modifies unless you want manual reasoning.

There is now a single modifies clause: modifies l h h', where l is a "set" of memory locations. Here we write "set" although we are not using the F* standard set library (FStar.Set, FStar.TSet or FStar.GSet).

A memory location l, of type loc, can correspond to:

  • a buffer b: loc_buffer b
  • a reference r: loc_mreference r and loc_freed_mreference r (difference explained below)
  • a set a of addresses in one given region r: loc_addresses false r a and loc_addresses true r a (difference explained below)
  • a set r of regions: loc_regions false r and loc_regions true r (difference explained below)
  • the empty set: loc_none
  • a union of two memory locations l1, l2: loc_union l1 l2

The distinction between loc_addresses false r a and loc_addresses true r a is that, if only the latter appears in the modifies clause, then the liveness of any reference at these addresses is preserved. The same goes between loc_freed_mreference r and loc_mreference r: in the latter case, the liveness of r is preserved. In particular, this means that the modifies clause associated by a deallocation will use loc_addresses false or loc_freed_mreference. Other operations (e.g. update) can use loc_addresses true or loc_mreference.

Interestingly, there is no such distinction for buffers: loc_buffer b will always assume that the liveness of b is preserved. Thus, deallocating a buffer b will actually modify its address, loc_addresses false (frameOf b) (Set.singleton (as_addr b)).

Similarly, given a set r of region identifiers, modifying loc_regions true r preserves their region-liveness (live_region h r), contrary to loc_regions false r. However, neither preserve the liveness of any object contained in these regions. One way to express this property for one region could be loc_addresses true r (Set.complement Set.empty): modify an undetermined set of addresses in a region while preserving all livenesses.

(loc, loc_union, loc_none) is an associative and commutative monoid. Moreover, it is equipped with a preorder, loc_includes, which satisfies the following properties:

  • it is reflexive and transitive (as a preorder)
  • if a larger buffer includes a smaller buffer in the sense of FStar.Buffer.includes (i.e. if smaller is a sub-buffer obtained from larger by sub), then so are their memory locations
  • a buffer b is included in any memory location covering its address: loc_addresses false r a and loc_addresses true r a, if r is the region of b and a contains its address
  • a reference x is included in any memory location wholly covering its address: loc_mreference x (resp. loc_freed_mreference x) is included in loc_addresses true r a (resp. loc_addresses false r a) if r is the region of x and a contains its address
  • similarly for regions
  • loc_none is minimal (everything includes loc_none)
  • loc_union is monotonic and isotonic (just like in set theory.)

WARNING: loc_includes is NOT antisymmetric.

The main purpose of inclusion is to weaken a modifies clause with any "larger set" of memory locations.

Examples

References

The following code illustrates the effects of using the new modifies clauses for references.

module Set = FStar.Set
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module M = LowStar.ModifiesPat

assume
val f (x: HS.reference int) : HST.ST unit
  (requires (fun h -> h `HS.contains` x))
  (ensures (fun h _ h' ->
    h' `HS.contains` x /\
    M.modifies (M.loc_mreference x) h h'
  ))

let g (x y: HS.reference int) : HST.ST unit
  (requires (fun h ->
    h `HS.contains` y /\ h `HS.contains` x /\
    (HS.frameOf x == HS.frameOf y ==> HS.as_addr x <> HS.as_addr y)
  ))
  (ensures (fun h _ h' ->
    h' `HS.contains` y /\
    HS.sel h' y == HS.sel h y
  ))
= f x

Independently of the actual implementation of f, F* derives the preservation of the liveness and contents of y in g from the modifies clauses in the specification of f, and the disjointness of x and y as specified in the precondition of g.

With the new modifies clauses, it is possible, and very easy, to write a modifies clause for a function (e.g. swap) taking two disjoint references from arbitrary regions (maybe the same.) Here is the solution:

let swap (x y: HST.reference int) : HST.ST unit
  (requires (fun h ->
    h `HS.contains` y /\ h `HS.contains` x /\
    (HS.frameOf x == HS.frameOf y ==> HS.as_addr x <> HS.as_addr y)
  ))
  (ensures (fun h _ h' ->
    h' `HS.contains` y /\
    h' `HS.contains` x /\
    HS.sel h' y == HS.sel h x /\
    HS.sel h' x == HS.sel h y /\
    M.modifies (M.loc_union (M.loc_mreference x) (M.loc_mreference y)) h h'
  ))
= let vx = HST.op_Bang x in
  let vy = HST.op_Bang y in
  x `HST.op_Colon_Equals` vy;
  y `HST.op_Colon_Equals` vx

Buffers

The following code illustrates the effects of using the new modifies clauses for new buffers.

module B = LowStar.Buffer

assume
val f (x: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` x))
  (ensures (fun h _ h' ->
    h' `B.live` x /\
    M.modifies (M.loc_buffer x) h h'
  ))

let g (x y: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` y /\ h `B.live` x /\ x `B.disjoint` y))
  (ensures (fun h _ h' ->
    h' `B.live` y /\
    B.as_seq h' y == B.as_seq h y
  ))
= f x

Independently of the actual implementation of f, F* derives the preservation of the liveness and contents of y in g from the modifies clauses in the specification of f, and the disjointness of x and y as specified in the precondition of g.

independently of their regions. The modifies clause can be used to rewrite swap for two disjoint buffers of size 1 located in arbitrary regions:

let swap (x y: B.buffer int) : HST.ST unit
  (requires (fun h -> h `B.live` y /\ h `B.live` x /\ B.length x == 1 /\ B.length y == 1 /\ x `B.disjoint` y))
  (ensures (fun h _ h' ->
    h' `B.live` y /\
    h' `B.live` x /\
    B.as_seq h' y `Seq.equal` B.as_seq h x /\
    B.as_seq h' x `Seq.equal` B.as_seq h y /\
    M.modifies (M.loc_union (M.loc_buffer x) (M.loc_buffer y)) h h'
  ))
= let vx = B.index x 0ul in
  let vy = B.index y 0ul in
  B.upd x 0ul vy;
  B.upd y 0ul vx

Support for 3 buffers and more naturally follows the same pattern.

There is also support for mixed buffers and references, using something like loc_union (loc_mreference r) (loc_buffer b)

Furthermore, those modifies clauses for buffers also work for deallocations, if written carefully. In particular, deallocating a buffer b will not modify just loc_buffer b, but its whole address:

let free (#t: Type) (b: B.buffer t) : HST.Stack unit
  (requires (fun h -> B.live h b /\ B.freeable b))
  (ensures (fun h _ h' ->  M.modifies (M.loc_addresses false (B.frameOf b) (Set.singleton (B.as_addr b))) h h'
= B.free b

Transitioning from old to new modifies clauses

References

Operation Old New
None modifies_none h h' modifies loc_none h h'
Allocate r modifies_one (frameOf r) h h' /\ modifies_ref (frameOf r) Set.empty h h' modifies loc_none h h'
Update r modifies_one (frameOf r) h h' /\ modifies_ref (frameOf r) (Set.singleton (as_addr r)) h h' modifies (loc_mreference r) h h'
Deallocate b N/A modifies (loc_freed_mreference r) h h'

Buffers

Operation Old New
None modifies_0 h h' modifies loc_none h h'
Allocate b modifies_one (frameOf b) h h' /\ modifies_ref (frameOf b) Set.empty h h' modifies loc_none h h'
Update 1 modifies_1 b h h' modifies (loc_buffer b) h h'
Update 2 modifies_2 b1 b2 h h' modifies (loc_union (loc_buffer b1) (loc_buffer b2)) h h'
Update 3 modifies_3 b1 b2 b3 h h' modifies (loc_union (loc_union (loc_buffer b1) (loc_buffer b2)) (loc_buffer b3) h h'
Deallocate b N/A modifies (loc_addresses false (frameOf b) (Set.singleton (as_addr b))) h h'

Regions and addresses

Operation Old New
Modify some addresses in a region r, preserving all livenesses modifies_one r h h' /\ modifies_ref r a h h' modifies (loc_addresses true r a) h h'
Modify some addresses in two regions r1, r2, preserving all livenesses modifies (Set.union (Set.singleton r1 r2)) h h' /\ modifies_ref r1 a1 h h' /\ modifies_ref r2 a2 h h' modifies (loc_union (loc_addresses true r1 a1) (loc_addresses true r2 a2)) h h'
Modify a region r only, preserving its liveness but not the livenesses of its contents modifies_one r h h' modifies (loc_region_only true r) h h'
Modify a region r and all its "children", preserving their livenesses but not those of their contents modifies_transitively r h h' modifies (loc_regions true (mod_set r)) h h'

Memory locations

Calling legacy code

If you are proving the memory safety of a function with new modifies, you can still call into functions proven against old modifies clauses.

Buffers

With LowStar.ToFStarBuffer, this should be automatic, thanks to patterns defined there and on modifies_1_modifies, modifies_2_modifies, modifies_3_modifies in FStar.Modifies.

Regions and references

Currently, this has to be done manually, because of regions. If you have:

modifies (Set.union (Set.singleton r1) (Set.singleton r2)) h h' /\
modifies_ref r1 a1 h h' /\
modifies_ref r2 a2 h h' /\
r1 =!= r2 /\
live_region h' r1 /\
live_region h' r2

then you can convert them to new modifies clauses as follows:

modifies_loc_regions_intro (Set.union (Set.singleton r1) (Set.singleton r2)) h h' ;
// here we have: modifies (loc_regions true (Set.union (Set.singleton r1) (Set.singleton r2))) h h'
loc_includes_region_union_l true (loc_regions true (Set.singleton r2)) h h' ;
assert (Set.intersect (Set.singleton r2) (Set.complement (Set.singleton r1)) `Set.equal` Set.singleton r2);
loc_includes_trans (loc_region_only false r1 `loc_union` loc_region_only true r2) (loc_region_only true r1 `loc_union` loc_region_only true r2) (loc_regions true (Set.union (Set.singleton r1) (Set.singleton r2)));
modifies_loc_includes (loc_region_only false r1 `loc_union` loc_region_only false r2) h h' (loc_regions true (Set.union (Set.singleton r1) (Set.singleton r2)));
// here we have: modifies (loc_region_only false r1 `loc_union` loc_region_only false r2) h h'
modifies_loc_addresses_intro r1 a1 h h' (loc_region_only r2);
// here we have: modifies (loc_addresses true r1 a1 `loc_union` loc_region_only false r2) h h'
modifies_loc_addresses_intro r2 a2 h h' loc_none;
// here we have: modifies (loc_addresses true r1 a1 `loc_union` loc_addresses true r2 a2) h h'
Add a custom footer
Add a custom sidebar
Clone this wiki locally