Heapster tutorial #1727
Heapster tutorial #1727
Conversation
| ### Build the Coq backend for Saw | ||
|
|
||
| In this tutorial we will also interact with Heapster's Coq output. So you'll need | ||
| to follow the instructions in the README in the `saw-core-coq` subdirectory. |
There was a problem hiding this comment.
Please add a link to that README
There was a problem hiding this comment.
What do you have in mind for this link? Do you mean a hyperlink to the README in the master branch in github?
The location would be different if the tutorial is being read online or locally. That's why I tend to use local commands when I can.
|
|
||
| **TODO: How do we check if this is properly installed before continuing?** | ||
|
|
||
| Before continuing, return to the top-level directory with `cd ..`. |
There was a problem hiding this comment.
This should be cd ../..
| ``` | ||
|
|
||
| (The alternative command `make examples/linked_list.bc` won't work | ||
| because the shorcut is not defined in the Makefile of heapster.) |
There was a problem hiding this comment.
I'm confused by this comment, because make linked_list.bc works for me (when run in the heapster-saw/examples directory)
| #### 3. Load the file and extract the two function specifications. | ||
|
|
||
| To load a file into heapster you can use `heapster_init_env`. Let's | ||
| check it's documentation first |
There was a problem hiding this comment.
Typo: "it's" -> "its"
| #### 4. Writing heapster specifications for your functions | ||
|
|
||
| ##### Pen and paper specification | ||
|
|
There was a problem hiding this comment.
You should use the term "Heapster types" instead of "Heapster specifications", because, like you say later, Heapster types aren't full functional specifications, but instead mostly deal with memory shapes and whether LLVM values are pointers or word values.
| "unfoldList (Vec 64 Bool)"; | ||
| ``` | ||
|
|
||
| Its first four arguments are the same as for `heapster_define_perm`, |
There was a problem hiding this comment.
Explain the rw argument, because this is the first example that uses it
| 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. the new permission is created and added to the | ||
| environment. |
There was a problem hiding this comment.
Mention that uses of named permissions are written like int64<>, where the <> is the empty list of arguments.
|
@eddywestbrook This has been updated with:
|
|
This PR also fixes alignment in The only substantive changes to |
| - [Tutorial to learn the basics of heapster-saw](#tutorial-to-learn-the-basics-of-heapster-saw) | ||
| - [Building](#building) | ||
| - [Build Saw](#build-saw) | ||
| - [Build the Coq backend for Saw](#build-the-coq-backend-for-saw) |
There was a problem hiding this comment.
A minor thing: this tutorial is inconsistent about how it capitalizes "SAW", as it also uses "Saw" (as is used here) and "saw" at various points. It would be worth picking one convention and using it throughout the tutorial. Similary for "SAWScript" versus "sawscript".
There was a problem hiding this comment.
Agreed, please use SAW and SAWScript
| We will not go into detail about the proof, but notice that the | ||
| important steps are handled by custom automation. Namely we use the | ||
| commands `prove_refinement_match_letRecM_l` and `prove_refinement` to | ||
| handle refinments with and without recursion (respectively). The rest |
There was a problem hiding this comment.
| handle refinments with and without recursion (respectively). The rest | |
| handle refinements with and without recursion (respectively). The rest |
| but we need a new predicate for lists. Before we look at the | ||
| definition of a `List64<rw>` lets focus on its permission type. First | ||
| of all, `List64<rw>` takes a single argument `rw:rwmodality` which | ||
| determines if the list is readable or writable, jus like 3D |
There was a problem hiding this comment.
| determines if the list is readable or writable, jus like 3D | |
| determines if the list is readable or writable, just like 3D |
| the definition shows the diferent cases for a list, separated by a | ||
| coma. In the first case, a `List64` can be a null pointer, expressed | ||
| with the type `eq(llvmword(0))`. In the second case, a list is a | ||
| pointer where offset `0` is the head, an `Int64`, and offset `8` it's | ||
| the tail, is recursively a `List64<rw>`. In the later case, | ||
| both elements are tagged with `rw`, describing if they are readable or | ||
| writable, as determined by the argument to `List64<rw>`. |
There was a problem hiding this comment.
| the definition shows the diferent cases for a list, separated by a | |
| coma. In the first case, a `List64` can be a null pointer, expressed | |
| with the type `eq(llvmword(0))`. In the second case, a list is a | |
| pointer where offset `0` is the head, an `Int64`, and offset `8` it's | |
| the tail, is recursively a `List64<rw>`. In the later case, | |
| both elements are tagged with `rw`, describing if they are readable or | |
| writable, as determined by the argument to `List64<rw>`. | |
| The definition shows the diferent cases for a list, separated by a | |
| comma. In the first case, a `List64` can be a null pointer, expressed | |
| with the type `eq(llvmword(0))`. In the second case, a list is a | |
| pointer where offset `0` is the head, an `Int64`, and offset `8` is | |
| the tail, is recursively a `List64<rw>`. In the later case, | |
| both elements are tagged with `rw`, describing if they are readable or | |
| writable, as determined by the argument to `List64<rw>`. |
|
|
||
| To define [permissions](doc/Permissions.md) which can describe | ||
| unbounded data structures, you can use the | ||
| `heapster_define_recursive_perm` command. here is how to use the |
There was a problem hiding this comment.
| `heapster_define_recursive_perm` command. here is how to use the | |
| `heapster_define_recursive_perm` command. Here is how to use the |
|
|
||
| Its first four arguments are the same as for `heapster_define_perm`, | ||
| namely the environment, the name, the arguments and the type of value | ||
| that the permission applies to. The fifth argument is its permision |
There was a problem hiding this comment.
| that the permission applies to. The fifth argument is its permision | |
| that the permission applies to. The fifth argument is its permission |
Typo, spelling, and grammar corrections from Ryan Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
eddywestbrook
added
PR: ready to merge
Add a tutorial to get up to speed with Heapster.