From a6a47956b13c3091550ed3cd48e6929a6dc66786 Mon Sep 17 00:00:00 2001 From: Jennifer Paykin Date: Tue, 19 Oct 2021 14:46:50 -0700 Subject: [PATCH 1/5] Added documentation about heapster permissions --- heapster-saw/README.md | 6 +- heapster-saw/doc/Permissions.md | 275 ++++++++++++++++++++++++++++++++ 2 files changed, 280 insertions(+), 1 deletion(-) create mode 100644 heapster-saw/doc/Permissions.md diff --git a/heapster-saw/README.md b/heapster-saw/README.md index 2d0803473d..37478be7f8 100644 --- a/heapster-saw/README.md +++ b/heapster-saw/README.md @@ -78,7 +78,7 @@ The first argument is the Heapster environment, the second is its name, the third is its arguments (of which there are none), the fourth is the type of value that the permission applies to, and the fifth is its definition. -To define permissions which can describe unbounded data structures, you can use +To define [permissions](doc/Permissions.md) which can describe unbounded data structures, you can use the `heapster_define_recursive_perm` command. As an example, here is how to describe a linked list of 64-bit words using this command: ``` @@ -136,6 +136,10 @@ convention, we add a `_gen` suffix to the filename. heapster_export_coq env "my_file_gen.v"; ``` +### Heapster Permissions + +See this [additional documentation](doc/Permissions.md) for a reference on the syntax and meaning of heapster permissions. + ### Verifying in Coq To interact with the generated Coq code, you will first need to set up your Coq diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md new file mode 100644 index 0000000000..32aae26d73 --- /dev/null +++ b/heapster-saw/doc/Permissions.md @@ -0,0 +1,275 @@ +Summary of Metavariables +======================== + +In this document, we use the following metavariables to refer to different sorts of data. + + **Metavariable** **Description** + ------------------ -------------------------------- + `a` Permission type + `e` Permission expression + `b`, `w` Bitvector expression + `x` Permission expression variable + `rw` ReadWrite modality expression + `sh` Shape expression + `l` Lifetime expression + `p` Value permission + + + +Permission types +================ + +A permission type includes regular crucible types as well as heapster-specific types + ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| **Permission Type** | **Description** | +| **a** | | ++=====================+================================================================================================================================================================================+ +| unit | Crucible unit type | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| bool | Crucible boolean type | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| nat | Crucible type of natural numbers | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| bv w | Crucible bitvector type of width w | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| struct(a1,..,an) | Crucible struct type \[equivalent to a tuple, not to be used for C structs\] | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmptr w | llvm-specific crucible type of pointers of width w | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| rwmodality | type of modality for read or write permissions | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| permlist | type of a list of permissions - outdated | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmframe w | type of ghost objects that represent the current stack frame with respect to bitvectors of width w | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| perm(a) | type of permissions describing how to use an object of type a. That is, the proposition "x:p" for a permission p of type perm(a) means "a value x of type a has permission p". | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmshape w | type of shapes with respect to bitvectors of width w | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmblock w | type of blocks of memory with respect to bitvectors of width w | ++---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ + +Permission expressions +====================== + +Expressions that are considered \"pure\" for use in permissions. + +A llvm-pointer (aka an llvm value) is either an llvmword or a variable+an offset + +Any crucible type can have a variable of that type, and that thing is an expression + ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| **Permission Expressions** | **Type** | **Description** | +| | | | +| **e** | | | ++============================+==================+===================================================================================================================================================================================================================================================================+ +| x | any | Any expression variable | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| unit | unit | A unit literal | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| b | bool | A literal boolean number | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| n | nat | A literal natural number | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| n | bv w | A literal bitvector. | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| b1 + b2 | bv w | Sum of two bitvectors | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| b1 \* b2 | bv w | Linear multiplication of two bitvectors, meaning that one of the operands must be a constant | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| struct(e1,..,en) | struct(a1,..,an) | A (crucible) struct is a tuple of expressions for each argument of the struct type. Crucible structs are different from C structs, and we only use crucible structs when we need to, otherwise C structs are described manually as pointers into chunks of memory | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmword(e) | llvmptr(w) | An LLVM value that represents a word, i.e. whose region identifier is 0, given a bitvector expression e:bv w | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| x &+ o | llvmptr(w) | An LLVM pointer built by adding an offset o (a bitvector expression) to an LLVM pointer variable x | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| R | rwmodality | The read modality | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| W | rwmodality | The write modality | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| p | perm(a) | A permission as an expression | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ + +In addition to the above expressions, we also have shape expressions, which we separated out only for the sake of readability. + ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| **Permission Expression** | **Type** | **Description** | +| | | | +| **sh** | | | ++===========================+=============+=================================================================================================================================================================================================================================================================================================================================+ +| emptysh | llvmshape w | The empty shape | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| name\ | llvmshape w | A named shape along with arguments for it, with optional read/write and lifetime modalities that are applied to the body of the shape. Named shapes can either be (1) defined shapes (alias) (2) recursive shapes, or (3) opaque shapes (axioms-all you know is their length). There are heapster commands for defining shapes. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| eqsh(e) | llvmshape w | A shape equal to the llvmblock e, where e is an expression of type llvmblock w. Used to type memcpy. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| sh1 orsh sh2 | llvmshape w | A disjunctive shape. sh1 and sh2 need not have the same size. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| sh1 ; sh2 | llvmshape w | A sequence of two shapes | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| \[l\]ptrsh(rw,sh) | llvmshape w | A shape for a pointer to another memory block, i.e. a memblock permission, with a given shape. This memblock permission will have the same read/write and lifetime modalities as the memblock permission containing this pointer shape, unless they are specifically overridden by the pointer shape; i.e., we have that | +| | | | +| | | \[l\]memblock(rw,off,len,\[l'\]ptrsh(rw',sh))= | +| | | | +| | | \[l\]memblock(rw,off,len, | +| | | | +| | | fieldsh(\[l\'\]memblock(rw\',0,len(sh),sh)) | +| | | | +| | | ) | +| | | | +| | | where rw' and/or l\' can be Nothing, in which case they default to rw and l, respectively. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| fieldsh(p) | llvmshape w | A shape for a single pointer field, given a permission that acts on a pointer of unknown size. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| fieldsh(p,sz) | llvmshape w | Like fieldsh(p), but where the permission acts on a pointer of size sz. | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| arraysh(s,len,sh) | llvmshape w | A shape for an array with the given stride, length (in number of elements = total length / stride), and fields | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| exsh x:a.sh | llvmshape w | An existential shape | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ + +Value permissions +================= + +A value permission is a permission to do something with a value, such as use it as a pointer. This also includes a limited set of predicates on values (you can think about this as \"permission to assume the value satisfies this predicate\" if you like). + +The type of permissions, perm(a), can be thought of as a function from values of type a to a pair of a proposition and a rely-guarantee permission. + +\[\| perm(a) \|\] = a -\> (prop \* rely-guarantee permission) + +For example, informally: + +> \[\| ptr((W,0) ⊢\> true) \|\] = \\x -\> +> +> (x is allocated, you can read/write to \*x in +> +> the current memory and no one else can) + +\[\| ptr((R,0) ⊢\> true) \|\] = \\x -\> + +(x is allocated, you can read from \*x in the current memory + +> and no one else can write to it) + +For a variable x:a, the proposition "x:p" means "x has permission p": this takes \[\|p\|\]:a -\> (prop \* RG perm) and applies it to x:a to get a (prop \* rg perm) + ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| **Permissions** | **Type** | **Description** | +| | | | +| **p** | | | ++=========================================+=========================+====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================+ +| true | perm(a) | trivial permission that always holds | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| p1 or p2 | perm(a) | disjunction; both p1 and p2 must have type perm(a) | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| p1 \* p2 | perm(a) | separating conjunction; p1 and p2 (both of type perm(a)) must be atomic permissions (not a disjunction, existential, or equality permission) | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| eq(e) | perm(a) | a value equal to the expression e:a | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| exists x:a. p | perm(b) | there exists some expression e:a such that p\[e/x\]:perm(b) holds. | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| x\\@o | perm(a) | A named permission with expression arguments, with optional offset expression o. | +| | | | +| | | Named permissions can either be (1) defined permissions (aliases) (2) recursive permissions, or (3) opaque permissions (axioms). There are heapster commands for defining named permissions in these ways. | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| \[l\]array(rw, off | perm(llvmptr w) | a permission for a pointer to an array, where: | +| | | | +| ,\ p) | perm(llvmptr w) | pointer permission where | +| | | | +| | | - l is a lifetime during which the permission can be used | +| | | | +| | | - rw is a read or write token | +| | | | +| | | - o is the offset from the variable the permission applies to where the read or write is being allowed | +| | | | +| | | - p is the permission held by the value being pointed to at the offset, of type perm(llvmptr w) | +| | | | +| | | This is similar to | +| | | | +| | | exists y. | +| | | | +| | | \[l\]ptr((rw,o) ⊢\> eq(y)) \* y:p | +| | | | +| | | but we can't actually write this in Heapster because we can't write y:p on locally-bound variables | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| \[l\]ptr((rw,o,sz) \|-\> p) | perm(llvmptr w) | Similar to \[l\]ptr((rw,o) ⊢\> p) but where the value pointed to has sz bits, i.e., p:llvmptr sz. So, for | +| | | | +| | | x : llvmptr w (w = \# bits), | +| | | | +| | | the permission | +| | | | +| | | \[l\]ptr((rw,o) ⊢\> p) | +| | | | +| | | is equivalent to | +| | | | +| | | \[l\]ptr((rw,o,w) ⊢\> p) | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| shape(sh) | perm(llvmblock w) | Says that a memory block has shape expression sh | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| lowned \[ls\](x1:P1,... -o x1':P1',...) | perm(lifetime) | Permission l:lowned (\...) says that the current task/process/function/code *owns* lifetime l. A lifetime intuitively represents a period of time, during which it is "current" and after which it is "finished". Ownership of l is the permission to end l whenever you want, assuming certain conditions (described below) are met, along with the knowledge that l has not yet been ended, i.e., that l is current. This latter knowledge allows the owner of l to use permissions like \[l\]ptr(\...) that depend on l being current. | +| | | | +| | | Most of the structure of the lowned permission describes the conditions under which l can be ended. The list ls contains lifetimes that are contained in l, meaning they must end before l ends. Once all lifetimes in ls are finished, the act of ending l can be performed, and has permission type given by the implication ∏in -o ∏out, where each ∏ is a list of the form x1:P1, ..., xn:Pn. That is, ending l requires permissions ∏in to be "given back" to l, and in exchange the ender gets permissions ∏out, which are intuitively being held by l until it is finished. | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| \[l\]lcurrent | perm(lifetime) | Assertion that a lifetime is current during another lifetime expression l | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| lfinished | perm(lifetime) | Assertion that a lifetime has finished | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmfunptr{n,w}( | perm(llvmptr w) | Says an LLVM value is a pointer to a function with n arguments, each of which have type llvmptr w (i.e., have bit width w), and with output type llvmptr w. This function takes in ghost arguments x0:p\_g,\..., as well as input permissions given by permission p0 on the first argument, p1 on the second, etc.. The function returns permissions p0' on the first argument, p1' on the second, etc., along with permission pret on the return value. | +| | | | +| (x0:p\_g,...). | | Note that arg0, arg1, and ret are not variables, they must have those names, though the argument variables may occur in any order. | +| | | | +| arg0:p0,... -o | | | +| | | | +| arg0:p0',..., ret:pret) | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| llvmframe\[e1:m1,..,en:mn\] | perm(llvmframe w) | permission to allocate (via alloca) on an LLVM stack frame, and permission to delete that stack frame if we have exclusive permissions to all the given LLVM pointer objects. The frame permission is a list of permission expressions (e\_i) for pointers that have been allocated in the frame and their corresponding allocation sizes (m\_i) in words of size n. | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| struct(p1,..,pn) | perm (struct(a1,..,an)) | a struct permission is a sequence of permissions for each argument of the crucible struct type | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| | | | ++-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ From 97a40f2c71395c24de9ab9a45f41e36323b34012 Mon Sep 17 00:00:00 2001 From: jpaykin Date: Tue, 19 Oct 2021 15:50:37 -0700 Subject: [PATCH 2/5] Update Permissions.md Update formatting of tables for github-flavored markdown --- heapster-saw/doc/Permissions.md | 326 +++++++++----------------------- 1 file changed, 87 insertions(+), 239 deletions(-) diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md index 32aae26d73..871c9a7fa0 100644 --- a/heapster-saw/doc/Permissions.md +++ b/heapster-saw/doc/Permissions.md @@ -3,16 +3,16 @@ Summary of Metavariables In this document, we use the following metavariables to refer to different sorts of data. - **Metavariable** **Description** - ------------------ -------------------------------- - `a` Permission type - `e` Permission expression - `b`, `w` Bitvector expression - `x` Permission expression variable - `rw` ReadWrite modality expression - `sh` Shape expression - `l` Lifetime expression - `p` Value permission + **Metavariable** | **Description** + ------------------ | -------------------------------- + `a` | Permission type + `e` | Permission expression + `b`, `w` | Bitvector expression + `x` | Permission expression variable + `rw` | ReadWrite modality expression + `sh` | Shape expression + `l` | Lifetime expression + `p` | Value permission @@ -21,34 +21,20 @@ Permission types A permission type includes regular crucible types as well as heapster-specific types -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| **Permission Type** | **Description** | -| **a** | | -+=====================+================================================================================================================================================================================+ -| unit | Crucible unit type | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| bool | Crucible boolean type | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| nat | Crucible type of natural numbers | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| bv w | Crucible bitvector type of width w | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| struct(a1,..,an) | Crucible struct type \[equivalent to a tuple, not to be used for C structs\] | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmptr w | llvm-specific crucible type of pointers of width w | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| rwmodality | type of modality for read or write permissions | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| permlist | type of a list of permissions - outdated | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmframe w | type of ghost objects that represent the current stack frame with respect to bitvectors of width w | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| perm(a) | type of permissions describing how to use an object of type a. That is, the proposition "x:p" for a permission p of type perm(a) means "a value x of type a has permission p". | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmshape w | type of shapes with respect to bitvectors of width w | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmblock w | type of blocks of memory with respect to bitvectors of width w | -+---------------------+--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| **Permission Type `a`** | **Description** | +| :---: | :--- | +| `unit` | Crucible unit type | +| `bool` | Crucible boolean type | +| `nat` | Crucible type of natural numbers | +| `bv w` | Crucible bitvector type of width `w` | +| `struct(a1,..,an)` | Crucible struct type \[equivalent to a tuple, not to be used for C structs\] | +| `llvmptr w` | llvm-specific crucible type of pointers of width `w` | +| `rwmodality` | type of modality for read or write permissions | +| `permlist` | type of a list of permissions - outdated | +| `llvmframe w` | type of ghost objects that represent the current stack frame with respect to bitvectors of width `w` | +| `perm(a)` | type of permissions describing how to use an object of type `a`. That is, the proposition `x:p` for a permission `p` of type `perm(a)` means "`a` value `x` of type `a` has permission `p`". | +| `llvmshape w` | type of shapes with respect to bitvectors of width `w` | +| `llvmblock w` | type of blocks of memory with respect to bitvectors of width `w` | Permission expressions ====================== @@ -59,217 +45,79 @@ A llvm-pointer (aka an llvm value) is either an llvmword or a variable+an offset Any crucible type can have a variable of that type, and that thing is an expression -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| **Permission Expressions** | **Type** | **Description** | -| | | | -| **e** | | | -+============================+==================+===================================================================================================================================================================================================================================================================+ -| x | any | Any expression variable | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| unit | unit | A unit literal | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| b | bool | A literal boolean number | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| n | nat | A literal natural number | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| n | bv w | A literal bitvector. | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| b1 + b2 | bv w | Sum of two bitvectors | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| b1 \* b2 | bv w | Linear multiplication of two bitvectors, meaning that one of the operands must be a constant | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| struct(e1,..,en) | struct(a1,..,an) | A (crucible) struct is a tuple of expressions for each argument of the struct type. Crucible structs are different from C structs, and we only use crucible structs when we need to, otherwise C structs are described manually as pointers into chunks of memory | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmword(e) | llvmptr(w) | An LLVM value that represents a word, i.e. whose region identifier is 0, given a bitvector expression e:bv w | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| x &+ o | llvmptr(w) | An LLVM pointer built by adding an offset o (a bitvector expression) to an LLVM pointer variable x | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| R | rwmodality | The read modality | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| W | rwmodality | The write modality | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| p | perm(a) | A permission as an expression | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+----------------------------+------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| Permission Expressions `e` | Type | Description | +| :---: | :---: | :--- | +| `x` | any | Any expression variable | +| `unit` | `unit` | A unit literal | +| `b` | `bool` | A literal boolean value | +| `n` | `nat` | A literal natural number | +| `n` | `bv w` | A literal bitvector | +| `b1 + b2` | `bv w` | Sum of two bitvectors | +| `b1 * b2` | `bv w` | Linear multiplication of two bitvectors, meaning that one of the operands must be a constant | +| `struct(e1,..,en)` | `struct(a1,..,an)` | A (crucible) struct is a tuple of expressions for each argument of the struct type. Crucible structs are different from C structs, and we only use crucible structs when we need to, otherwise C structs are described manually as pointers into chunks of memory | +| `llvmword(e)` | `llvmptr(w)` | An LLVM value that represents a word, i.e. whose region identifier is 0, given a bitvector expression `e:bv w` | +| `x &+ o` | `llvmptr(w)` | An LLVM pointer built by adding an offset `o` (a bitvector expression) to an LLVM pointer variable `x` | +| `R` | `rwmodality` | The read modality | +| `W` | `rwmodality` | The write modality | +| `p` | `perm(a)` | A permission as an expression | In addition to the above expressions, we also have shape expressions, which we separated out only for the sake of readability. -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| **Permission Expression** | **Type** | **Description** | -| | | | -| **sh** | | | -+===========================+=============+=================================================================================================================================================================================================================================================================================================================================+ -| emptysh | llvmshape w | The empty shape | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| name\ | llvmshape w | A named shape along with arguments for it, with optional read/write and lifetime modalities that are applied to the body of the shape. Named shapes can either be (1) defined shapes (alias) (2) recursive shapes, or (3) opaque shapes (axioms-all you know is their length). There are heapster commands for defining shapes. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| eqsh(e) | llvmshape w | A shape equal to the llvmblock e, where e is an expression of type llvmblock w. Used to type memcpy. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| sh1 orsh sh2 | llvmshape w | A disjunctive shape. sh1 and sh2 need not have the same size. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| sh1 ; sh2 | llvmshape w | A sequence of two shapes | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| \[l\]ptrsh(rw,sh) | llvmshape w | A shape for a pointer to another memory block, i.e. a memblock permission, with a given shape. This memblock permission will have the same read/write and lifetime modalities as the memblock permission containing this pointer shape, unless they are specifically overridden by the pointer shape; i.e., we have that | -| | | | -| | | \[l\]memblock(rw,off,len,\[l'\]ptrsh(rw',sh))= | -| | | | -| | | \[l\]memblock(rw,off,len, | -| | | | -| | | fieldsh(\[l\'\]memblock(rw\',0,len(sh),sh)) | -| | | | -| | | ) | -| | | | -| | | where rw' and/or l\' can be Nothing, in which case they default to rw and l, respectively. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| fieldsh(p) | llvmshape w | A shape for a single pointer field, given a permission that acts on a pointer of unknown size. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| fieldsh(p,sz) | llvmshape w | Like fieldsh(p), but where the permission acts on a pointer of size sz. | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| arraysh(s,len,sh) | llvmshape w | A shape for an array with the given stride, length (in number of elements = total length / stride), and fields | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| exsh x:a.sh | llvmshape w | An existential shape | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+---------------------------+-------------+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +| Shape Permission Expressions `sh` | Type | Description | +| :---: | :---: | :--- | +| `emptysh` | `llvmshape w` | The empty shape | +| `name` | `llvmshape w` | A named shape along with arguments for it, with optional read/write and lifetime modalities that are applied to the body of the shape. Named shapes can either be (1) defined shapes (alias) (2) recursive shapes, or (3) opaque shapes (axioms-all you know is their length). | +| `eqsh(e)` | `llvmshape w` | A shape equal to the llvmblock `e`, where `e` is an expression of type `llvmblock w`. Used to type memcpy. | +| `sh1 orsh sh2` | `llvmshape w` | A disjunctive shape. `sh1` and `sh2` need not have the same size. | +| `sh1 ; sh2` | `llvmshape w` | A sequence of two shapes | +| `[l]ptrsh(rw,sh)` | `llvmshape w` | A shape for a pointer to another memory block, i.e. a memblock permission, with a given shape. This memblock permission will have the same read/write and lifetime modalities as the memblock permission containing this pointer shape, unless they are specifically overridden by the pointer shape; i.e., we have that `[l]memblock(rw,off,len,[l']ptrsh(rw',sh)) = [l]memblock(rw,off,len, fieldsh([l']memblock(rw',0,len(sh),sh)))`, where `rw'` and/or `l'` can be `Nothing`, in which case they default to `rw` and `l`, respectively. | +| `fieldsh(p)` | `llvmshape w` | A shape for a single pointer field, given a permission that acts on a pointer of unknown size. | +| `fieldsh(p,sz)` | `llvmshape w` | Like `fieldsh(p)`, but where the permission acts on a pointer of size `sz`. | +| `arraysh(s,len,sh)` | `llvmshape w` | A shape for an array with the given stride, length (in number of elements = total length / stride), and fields `sh` | +| `exsh x:a.sh` | `llvmshape w` | An existential shape | Value permissions ================= A value permission is a permission to do something with a value, such as use it as a pointer. This also includes a limited set of predicates on values (you can think about this as \"permission to assume the value satisfies this predicate\" if you like). -The type of permissions, perm(a), can be thought of as a function from values of type a to a pair of a proposition and a rely-guarantee permission. +The type of permissions, `perm(a)`, can be thought of as a function from values of type a to a pair of a proposition and a rely-guarantee permission. -\[\| perm(a) \|\] = a -\> (prop \* rely-guarantee permission) +``` +[| perm(a) |] = a -> (prop * rely-guarantee permission) +``` For example, informally: -> \[\| ptr((W,0) ⊢\> true) \|\] = \\x -\> -> -> (x is allocated, you can read/write to \*x in -> -> the current memory and no one else can) - -\[\| ptr((R,0) ⊢\> true) \|\] = \\x -\> - -(x is allocated, you can read from \*x in the current memory - -> and no one else can write to it) - -For a variable x:a, the proposition "x:p" means "x has permission p": this takes \[\|p\|\]:a -\> (prop \* RG perm) and applies it to x:a to get a (prop \* rg perm) - -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| **Permissions** | **Type** | **Description** | -| | | | -| **p** | | | -+=========================================+=========================+====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================+ -| true | perm(a) | trivial permission that always holds | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| p1 or p2 | perm(a) | disjunction; both p1 and p2 must have type perm(a) | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| p1 \* p2 | perm(a) | separating conjunction; p1 and p2 (both of type perm(a)) must be atomic permissions (not a disjunction, existential, or equality permission) | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| eq(e) | perm(a) | a value equal to the expression e:a | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| exists x:a. p | perm(b) | there exists some expression e:a such that p\[e/x\]:perm(b) holds. | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| x\\@o | perm(a) | A named permission with expression arguments, with optional offset expression o. | -| | | | -| | | Named permissions can either be (1) defined permissions (aliases) (2) recursive permissions, or (3) opaque permissions (axioms). There are heapster commands for defining named permissions in these ways. | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| \[l\]array(rw, off | perm(llvmptr w) | a permission for a pointer to an array, where: | -| | | | -| ,\ p) | perm(llvmptr w) | pointer permission where | -| | | | -| | | - l is a lifetime during which the permission can be used | -| | | | -| | | - rw is a read or write token | -| | | | -| | | - o is the offset from the variable the permission applies to where the read or write is being allowed | -| | | | -| | | - p is the permission held by the value being pointed to at the offset, of type perm(llvmptr w) | -| | | | -| | | This is similar to | -| | | | -| | | exists y. | -| | | | -| | | \[l\]ptr((rw,o) ⊢\> eq(y)) \* y:p | -| | | | -| | | but we can't actually write this in Heapster because we can't write y:p on locally-bound variables | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| \[l\]ptr((rw,o,sz) \|-\> p) | perm(llvmptr w) | Similar to \[l\]ptr((rw,o) ⊢\> p) but where the value pointed to has sz bits, i.e., p:llvmptr sz. So, for | -| | | | -| | | x : llvmptr w (w = \# bits), | -| | | | -| | | the permission | -| | | | -| | | \[l\]ptr((rw,o) ⊢\> p) | -| | | | -| | | is equivalent to | -| | | | -| | | \[l\]ptr((rw,o,w) ⊢\> p) | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| shape(sh) | perm(llvmblock w) | Says that a memory block has shape expression sh | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| lowned \[ls\](x1:P1,... -o x1':P1',...) | perm(lifetime) | Permission l:lowned (\...) says that the current task/process/function/code *owns* lifetime l. A lifetime intuitively represents a period of time, during which it is "current" and after which it is "finished". Ownership of l is the permission to end l whenever you want, assuming certain conditions (described below) are met, along with the knowledge that l has not yet been ended, i.e., that l is current. This latter knowledge allows the owner of l to use permissions like \[l\]ptr(\...) that depend on l being current. | -| | | | -| | | Most of the structure of the lowned permission describes the conditions under which l can be ended. The list ls contains lifetimes that are contained in l, meaning they must end before l ends. Once all lifetimes in ls are finished, the act of ending l can be performed, and has permission type given by the implication ∏in -o ∏out, where each ∏ is a list of the form x1:P1, ..., xn:Pn. That is, ending l requires permissions ∏in to be "given back" to l, and in exchange the ender gets permissions ∏out, which are intuitively being held by l until it is finished. | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| \[l\]lcurrent | perm(lifetime) | Assertion that a lifetime is current during another lifetime expression l | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| lfinished | perm(lifetime) | Assertion that a lifetime has finished | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmfunptr{n,w}( | perm(llvmptr w) | Says an LLVM value is a pointer to a function with n arguments, each of which have type llvmptr w (i.e., have bit width w), and with output type llvmptr w. This function takes in ghost arguments x0:p\_g,\..., as well as input permissions given by permission p0 on the first argument, p1 on the second, etc.. The function returns permissions p0' on the first argument, p1' on the second, etc., along with permission pret on the return value. | -| | | | -| (x0:p\_g,...). | | Note that arg0, arg1, and ret are not variables, they must have those names, though the argument variables may occur in any order. | -| | | | -| arg0:p0,... -o | | | -| | | | -| arg0:p0',..., ret:pret) | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| llvmframe\[e1:m1,..,en:mn\] | perm(llvmframe w) | permission to allocate (via alloca) on an LLVM stack frame, and permission to delete that stack frame if we have exclusive permissions to all the given LLVM pointer objects. The frame permission is a list of permission expressions (e\_i) for pointers that have been allocated in the frame and their corresponding allocation sizes (m\_i) in words of size n. | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| struct(p1,..,pn) | perm (struct(a1,..,an)) | a struct permission is a sequence of permissions for each argument of the crucible struct type | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ -| | | | -+-----------------------------------------+-------------------------+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+ +``` +[| ptr((W,0) ⊢> true) |] = \x -> + (x is allocated, you can read/write to *x in + the current memory and no one else can) + +[| ptr((R,0) ⊢> true) |] = \x -> + (x is allocated, you can read from *x in the current memory + and no one else can write to it) +``` + +For a variable `x:a`, the proposition `x:p` means "`x` has permission `p`": this takes `[|p|]:a -> (prop * RG perm)` and applies it to `x:a` to get a `(prop * rg perm)` + +| Permissions `p` | Type | Description | +| :---: | :---: | :--- | +| `true` | `perm(a)` | trivial permission that always holds | +| `p1 or p2` | `perm(a)` | disjunction; both `p1` and `p2` must satisfy `perm(a)` | +| `p1 * p2` | `perm(a)` | separating conjunction; `p1` and `p2` (both satisfying `perm(a)`) must be atomic permissions (not a disjunction, existential, or equality permission) | +| `eq(e)` | `perm(a)` | a value equal to the expression `e:a` | +| `exists x:a. p` | `perm(b)` | there exists some expression `e:a` such that `p[e/x]:perm(b)` holds | +| `x@o` | `perm(a)` | A named permission with expression arguments, with optional offset expression `o`. Named permissions can either be (1) defined permissions (aliases) (2) recursive permissions, or (3) opaque permissions (axioms). | +| `[l]array(rw, off,
  • `l` is the lifetime during which this permission is active;
  • `off` is a permission expression representing the offset of this array from the pointer in bytes;
  • `len` is a permission expression representing the number of cells in the array;
  • `stride` is a permission expression representing the number of bytes in a cell;
  • `sh` is a shape expression representing the shape of elements in the array
    • | +| `[l]memblock(rw,o,len,sh)` | `perm(llvmptr w)` | gives read or write access to a memory block, whose contents also give some permissions, where:
    • `rw` indicates whether this is a read or write block permission
    • `l` is the lifetime during which this block permission is active
    • `o` is the offset of the block from the pointer in bytes
    • `len` is the length of the block in bytes
    • `sh` is the shape of the block
    | +| `free(e)` | `perm(llvmptr w)` | Says that we have permission to free the memory pointed at by this pointer if we have write permission to `e` words of size `w`, where `e` is a permission expression for a bitvector of width `w`. Superseded by opaque permissions. | +| `[l]ptr((rw,o) \|-> p)` | `perm(llvmptr w)` | pointer permission where
    • `l` is a lifetime during which the permission can be used
    • `rw` is a read or write token
    • `o` is the offset from the variable the permission applies to where the read or write is being allowed
    • `p` is the permission held by the value being pointed to at the offset, of type `perm(llvmptr w)`.
    This is similar to `exists y. [l]ptr((rw,o) ⊢> eq(y)) * y:p` but we can't actually write this in Heapster because we can't write `y:p` on locally-bound variables. | +| `[l]ptr((rw,o,sz) \|-> p)` | `perm(llvmptr w)` | Similar to `[l]ptr((rw,o) ⊢> p)` but where the value pointed to has `sz` bits, i.e., `p:llvmptr sz`. So, for `x : llvmptr w` (`w` = number of bits), the permission `[l]ptr((rw,o) ⊢> p)` is equivalent to `[l]ptr((rw,o,w) ⊢> p)` | +| `shape(sh)` | `perm(llvmblock w)` | Says that a memory block has shape expression `sh` | +| `lowned [ls](x1:P1,... -o x1':P1',...)` | `perm(l)` | Permission `l:lowned (...)` says that the current task/process/function/code *owns* lifetime `l`. A lifetime intuitively represents a period of time, during which it is "current" and after which it is "finished". Ownership of `l` is the permission to end `l` whenever you want, assuming certain conditions (described below) are met, along with the knowledge that `l` has not yet been ended, i.e., that `l` is current. This latter knowledge allows the owner of `l` to use permissions like `[l]ptr(...)` that depend on `l` being current.
    Most of the structure of the lowned permission describes the conditions under which `l` can be ended. The list `ls` contains lifetimes that are contained in `l`, meaning they must end before `l` ends. Once all lifetimes in ls are finished, the act of ending `l` can be performed, and has permission type given by the implication `∏in -o ∏out`, where each `∏` is a list of the form `x1:P1, ..., xn:Pn`. That is, ending `l` requires permissions `∏in` to be "given back" to `l`, and in exchange the ender gets permissions `∏out`, which are intuitively being held by `l` until it is finished. | +| `[l']lcurrent` | `perm(l)` | Assertion that a lifetime `l` is current during another lifetime expression `l'` | +| `lfinished` | `perm(l)` | Assertion that a lifetime has finished | +| `llvmfunptr{n,w}((x0:p_g,...) arg0:p0,... -o arg0:p0',...,ret:p_ret)` | `perm(llvmptr w)` | Says an LLVM value is a pointer to a function with `n` arguments, each of which have type `llvmptr w` (i.e., have bit width `w`), and with output type `llvmptr w`. This function takes in ghost arguments `x0:p_g,...`, as well as input permissions given by permission `p0` on the first argument, `p1` on the second, etc.. The function returns permissions `p0'` on the first argument, `p1'` on the second, etc., along with permission pret on the return value.
    Note that `arg0`, `arg1`, etc, and `ret`, are not variables: they must have those names, though the argument variables may occur in any order. | +| `llvmframe[e1:m1,..,en:mn]` | `perm(llvmframe w)` | Permission to allocate (via `alloca`) on an LLVM stack frame, and permission to delete that stack frame if we have exclusive permissions to all the given LLVM pointer objects. The frame permission is a list of permission expressions (`e_i`) for pointers that have been allocated in the frame and their corresponding allocation sizes (`m_i`) in words of size `n`. | +| `struct(p1,..,pn)` | `perm (struct(a1,..,an))` | A struct permission is a sequence of permissions for each argument of the crucible struct type | From 30d7a78b69dc438750abc9d1dc3a56908883be98 Mon Sep 17 00:00:00 2001 From: jpaykin Date: Tue, 19 Oct 2021 16:23:33 -0700 Subject: [PATCH 3/5] Apply suggestions from code review Fixing formatting on tables Co-authored-by: Matthew Yacavone --- heapster-saw/doc/Permissions.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md index 871c9a7fa0..03f64a049b 100644 --- a/heapster-saw/doc/Permissions.md +++ b/heapster-saw/doc/Permissions.md @@ -45,7 +45,7 @@ A llvm-pointer (aka an llvm value) is either an llvmword or a variable+an offset Any crucible type can have a variable of that type, and that thing is an expression -| Permission Expressions `e` | Type | Description | +| Permission Expression `e` | Type | Description | | :---: | :---: | :--- | | `x` | any | Any expression variable | | `unit` | `unit` | A unit literal | @@ -65,7 +65,7 @@ In addition to the above expressions, we also have shape expressions, which we s | Shape Permission Expressions `sh` | Type | Description | | :---: | :---: | :--- | -| `emptysh` | `llvmshape w` | The empty shape | +| `emptysh` | `llvmshape w` | The empty shape | | `name` | `llvmshape w` | A named shape along with arguments for it, with optional read/write and lifetime modalities that are applied to the body of the shape. Named shapes can either be (1) defined shapes (alias) (2) recursive shapes, or (3) opaque shapes (axioms-all you know is their length). | | `eqsh(e)` | `llvmshape w` | A shape equal to the llvmblock `e`, where `e` is an expression of type `llvmblock w`. Used to type memcpy. | | `sh1 orsh sh2` | `llvmshape w` | A disjunctive shape. `sh1` and `sh2` need not have the same size. | From 04a3dc5c1163782f2dbfff53edae68817ab6c849 Mon Sep 17 00:00:00 2001 From: jpaykin Date: Tue, 19 Oct 2021 16:26:03 -0700 Subject: [PATCH 4/5] Update Permissions.md Updating heading titles --- heapster-saw/doc/Permissions.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md index 03f64a049b..6f50c8232c 100644 --- a/heapster-saw/doc/Permissions.md +++ b/heapster-saw/doc/Permissions.md @@ -21,7 +21,7 @@ Permission types A permission type includes regular crucible types as well as heapster-specific types -| **Permission Type `a`** | **Description** | +| **Permission Types `a`** | **Description** | | :---: | :--- | | `unit` | Crucible unit type | | `bool` | Crucible boolean type | @@ -45,7 +45,7 @@ A llvm-pointer (aka an llvm value) is either an llvmword or a variable+an offset Any crucible type can have a variable of that type, and that thing is an expression -| Permission Expression `e` | Type | Description | +| Permission Expressions `e` | Type | Description | | :---: | :---: | :--- | | `x` | any | Any expression variable | | `unit` | `unit` | A unit literal | From f3ef1da664ac1433f65536d373be4b51fbde5c81 Mon Sep 17 00:00:00 2001 From: jpaykin Date: Tue, 19 Oct 2021 16:30:33 -0700 Subject: [PATCH 5/5] Update Permissions.md Removing nobr tags because they didn't work to stop line breaks in the markdown table. --- heapster-saw/doc/Permissions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md index 6f50c8232c..5e4c81e22c 100644 --- a/heapster-saw/doc/Permissions.md +++ b/heapster-saw/doc/Permissions.md @@ -65,7 +65,7 @@ In addition to the above expressions, we also have shape expressions, which we s | Shape Permission Expressions `sh` | Type | Description | | :---: | :---: | :--- | -| `emptysh` | `llvmshape w` | The empty shape | +| `emptysh` | `llvmshape w` | The empty shape | | `name` | `llvmshape w` | A named shape along with arguments for it, with optional read/write and lifetime modalities that are applied to the body of the shape. Named shapes can either be (1) defined shapes (alias) (2) recursive shapes, or (3) opaque shapes (axioms-all you know is their length). | | `eqsh(e)` | `llvmshape w` | A shape equal to the llvmblock `e`, where `e` is an expression of type `llvmblock w`. Used to type memcpy. | | `sh1 orsh sh2` | `llvmshape w` | A disjunctive shape. `sh1` and `sh2` need not have the same size. |