From c82ec7171ebfd240f9437eb7f8fb6cc0a3fe8e1f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 11 Oct 2022 09:44:12 -0400 Subject: [PATCH 1/3] Minor documentation fix for heapster_assume_fun_rename `nm_t` is a typo and is actually meant to refer to `nm_to`. [ci skip] --- src/SAWScript/Interpreter.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 7046982d4d..6eca285a21 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -4068,7 +4068,7 @@ primitives = Map.fromList "HeapsterEnv -> String -> String -> String -> String -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun_rename) Experimental - [ "heapster_assume_fun_rename nm nm_t perms trans assumes that function nm" + [ "heapster_assume_fun_rename nm nm_to perms trans assumes that function nm" , " has permissions perms and translates to the SAW core term trans. If" , " trans is not an identifier then it is bound to the defined name nm_to." ] From 588b88fe4e493e968d5f341cae928c42dab52a85 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 11 Oct 2022 09:49:50 -0400 Subject: [PATCH 2/3] Permissions.md: More precise documentation for fieldsh The documentation for `fieldsh(p)` claims that it acts on a pointer of unknown size. This isn't really true, however, as it is really a shorthand for `fieldsh(w,p)`, where `w` is the current pointer size. I found the original documentation misleading enough to the point where I think it deserves to be rewritten, which I have accomplished in this patch. [ci skip] --- heapster-saw/doc/Permissions.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/heapster-saw/doc/Permissions.md b/heapster-saw/doc/Permissions.md index 3409b24b7c..fab2b1653c 100644 --- a/heapster-saw/doc/Permissions.md +++ b/heapster-saw/doc/Permissions.md @@ -13,8 +13,8 @@ In this document, we use the following metavariables to refer to different sorts `sh` | Shape expression `l` | Lifetime expression `p` | Value permission - - + + Value Types ================ @@ -71,8 +71,8 @@ In addition to the above expressions, we also have shape expressions, which we s | `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(sz,p)` | `llvmshape w` | Like `fieldsh(p)`, but where the permission acts on a pointer of size `sz`. | +| `fieldsh(sz,p)` | `llvmshape w` | A shape for a single pointer field, given a permission `p` that acts on a pointer of size `sz`. | +| `fieldsh(p)` | `llvmshape w` | Equivalent to `fieldsh(w,p)`. | | `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 | | `falsesh` | `llvmshape w` | The unsatisfiable or contradictory shape | From 48436061c2554903e8ec1e71cbd2308a4cd71291 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 11 Oct 2022 10:04:08 -0400 Subject: [PATCH 3/3] Add missing env arguments to Heapster functions' docs [ci skip] --- src/SAWScript/Interpreter.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 6eca285a21..9bc466c467 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -4060,7 +4060,7 @@ primitives = Map.fromList "HeapsterEnv -> String -> String -> String -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun) Experimental - [ "heapster_assume_fun nm perms trans assumes that function nm has" + [ "heapster_assume_fun env nm perms trans assumes that function nm has" , " permissions perms and translates to the SAW core term trans" ] @@ -4068,7 +4068,7 @@ primitives = Map.fromList "HeapsterEnv -> String -> String -> String -> String -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun_rename) Experimental - [ "heapster_assume_fun_rename nm nm_to perms trans assumes that function nm" + [ "heapster_assume_fun_rename env nm nm_to perms trans assumes that function nm" , " has permissions perms and translates to the SAW core term trans. If" , " trans is not an identifier then it is bound to the defined name nm_to." ] @@ -4078,7 +4078,7 @@ primitives = Map.fromList (bicVal heapster_assume_fun_rename_prim) Experimental [ - "heapster_assume_fun_rename_prim nm nm_to perms assumes that function nm" + "heapster_assume_fun_rename_prim env nm nm_to perms assumes that function nm" , " has permissions perms as a primitive." ] @@ -4086,7 +4086,7 @@ primitives = Map.fromList "HeapsterEnv -> String -> [(String, String)] -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun_multi) Experimental - [ "heapster_assume_fun_multi nm [(perm1, trans1), ...] assumes that function" + [ "heapster_assume_fun_multi env nm [(perm1, trans1), ...] assumes that function" , " nm can be typed with 0 or more permissions, each with the corresponding" , " translation to SAW core" ]