Address comments from reviews

Author: NlightNFotis

doc/cprover-manual/modeling-shadow-memory.md

@@ -1,49 +1,52 @@
 # Shadow Memory
 
-(The original artefact's implementation is outlined in the paper [CBMC-SSM:
-Bounded Model Checking of C Programs with Symbolic Shadow
-Memory](https://dl.acm.org/doi/abs/10.1145/3551349.3559523).)
+The Symbolic Shadow Memory module described below is an implementation of
+what is outlined in the paper [CBMC-SSM: Bounded Model Checking of C Programs
+with Symbolic Shadow Memory](https://dl.acm.org/doi/abs/10.1145/3551349.3559523).
 
 ## Introduction
 
-CBMC contains a component that supports *Symbolic Shadow Memory*. Shadow memory
-allows one to create a parallel memory structure that is maintained by the
-analysis program and that shadows the standard memory of the program. In that
-memory structure, a user can create fields, for which he can later set and
-retrieve values.
+CBMC implements *Symbolic Shadow Memory*. Symbolic Shadow Memory (from now on,
+SSM) allows one to create a parallel memory structure that is maintained by the
+analysis program and that shadows the standard memory of the program. In the
+Shadow Memory structure, a user can create fields, for which he can set and get
+(retrieve) values.
 
 By doing so, one can organise his own tracking of metadata related to the code,
 in a way that is then considered by the backend of CBMC during analysis. This
-can be used to implement novel analyses that the CBMC framework itself doesn't
-support - for example, the paper above presents as an example a taint analysis
+can be used to implement novel analyses that the CBMC framework itself does not
+support. For example, the paper above presents as an example a taint analysis
 implemented with the use of the SSM component described here.
 
 ## Usage
 
-A user can interact with the Symbolic Shadow Memory component (from now on
-onwards, SSM) through four CBMC primitives, which allow one to declare shadow
-memory fields, and retrieve/set their corresponding values:
+A user can interact with the Symbolic Shadow Memory component through four CBMC
+primitives, which allow one to declare shadow memory fields, and set/get their
+corresponding values:
 
 * `__CPROVER_field_decl_local`
 * `__CPROVER_field_decl_global`
 * `__CPROVER_get_field`
 * `__CPROVER_set_field`
 
 More precisely, their signatures (in pseudo-C, because of some constraints that
-we can't express using the type system), along with some small examples of their
-usage, look like this:
+we cannot express using the type system), along with some small examples of their
+usage, are described below:
 
 ### `void __CPROVER_field_decl_local(type1 field_name, SSM_value_type init_value)`
 
 Type constraints:
 
 * `type1`: string literal, such as `"field"`,
-* `SSM_value_type`: value of maximum 8 bits, signed or unsigned or `_Bool`.
+* `SSM_value_type`: any value up to 8 bits in size (signed or unsigned).
 
-Declares a local (working for variable declared in the current function scope)
-shadow memory field called `field_name`, and initialises it with the value
-`init_value`. The field is going to be associated with local-scope objects (i.e.
-a variable on the stack).
+Declares a local shadow memory field called `field_name`, and initialises it
+with the value `init_value`. The field is going to be associated with
+local-scope objects (i.e. a variable on the stack).
+
+Note that each scope will have a separate *local* shadow memory, so value stored
+in the *local* shadow memory is not propagated to subcalls (even when the call
+is recursive).
 
 ```c
 void func() {
@@ -60,10 +63,11 @@ void func() {
 Type constraints:
 
 * `type1`: string literal, such as `"field"`,
-* `SSM_value_type`: value of maximum 8 bits, signed or unsigned or `_Bool`.
+* `SSM_value_type`: any value up to 8 bits in size (signed or unsigned).
 
-Ditto as above, but the field declared is associated with global objects (i.e.
-global variables or heap allocated objects).
+As for `__CPROVER_field_decl_local`, but the field declared is associated with
+objects whose lifetime exceeds the current function scope (i.e. global variables
+or heap allocated objects).
 
 ```c
 // Sample global object
@@ -79,18 +83,19 @@ void func() {
 
 Type constraints:
 
-* `SSM_VALUE_TYPE`: the type of the value that was used to intialise the field
-  with during declaration,
+* `SSM_VALUE_TYPE`: the type of the returned value is the same of the SSM field,
+   i.e. the type that was used to intialise the SSM field during declaration,
 * `type1 *`: a non-`void` pointer to an object of type `type1`, whose address we
    are going to use for indexing the shadow memory component for the field
    declared,
 * `type2`: a string literal-typed value, denoting the name of the field whose
    value we want to retrieve, such as `"field"`.
 
-Retrieves the value (currently) associated with a SSM field of the given
-pointer. This would be either the value the field was declared to be initialised
-with, or, if there had been subsequent changes to it through a `__CPROVER_set_field`,
-the value that it was last `set` with.
+Retrieves the latest value associated with a SSM field to the given pointer.
+This would be either the value the field was declared to be initialised with,
+or, if there had been subsequent changes to it through a `__CPROVER_set_field`
+(see `__CPROVER_set_field` section below), the value that it was last `set`
+with.
 
 ```c
 // Sample global object
@@ -106,6 +111,10 @@ void func() {
 }
 ```
 
+Note that getting the value of a local variable from a global SSM field or the
+opposite will return the default value for that SSM field (and it **will not**
+fail).
+
 ### `void __CPROVER_set_field(type1 *p, type2 field_name, type3 set_value)`
 
 Type constraints:
@@ -115,34 +124,38 @@ Type constraints:
    declared,
 * `type2`: a string literal-typed value, denoting the name of the field whose
    value we want to retrieve, such as `"field"`,
-* `type3`: type of the value to be set. This can be `_Bool` or of any integer
-  type signed or unsigned. Notice that if this type differs from the type the
-  field was declared with (`SSM_VALUE_TYPE` above) it will be implicitly casted
-  to it.
+* `type3`: type of the value to be set. This can be any integer type signed or
+   unsigned (including `_Bool`). Notice that if this type differs from the type
+   the SSM field was declared with (`SSM_VALUE_TYPE` above) it will be
+   implicitly casted to it.
 
-Sets the value of an SSM field, using the name supplied by the `field name` as an
-identifier for the field and using the pointer in `p` as the address for the location
-of the value to be changed, to the given value, supplied by the third argument
-`set_value`. This value needs to be of the same type as the type of the value the
-field was originally initialised with.
+Sets the value associated with a SSM field to the given pointer `p` with the
+given value `set_value`. If the `set_value` type is not the `SSM_VALUE_TYPE`, it
+will be implicitly casted to it.
 
 ```c
-// Sample global object
+// Sample global object, used for addressing within the SSM component.
 int a = 10;
 
 void func() {
     // Shadow memory field (called "field") associated with global objects.
-    // Originally assigned a value of `1`, of type `_Bool`.
-    __CPROVER_field_decl_global("shadow", (_Bool)1);
-
-    // Set field "shadow" for the memory location denoted by the address of `a`
-    // to a value of 0.
-    __CPROVER_set_field(&a, "shadow", 0);
+    // Originally assigned a value of `0`, of type `_Bool`.
+    __CPROVER_field_decl_global("shadow", (_Bool)0);
 
     // Retrieve the value of the field named "shadow" associated with the address
     // of the object `a`. 
     _Bool shadow_x = __CPROVER_get_field(&a, "shadow");
-    __CPROVER_assert(shadow_x == 0, "expected success: field set to a value of 0");
-    __CPROVER_assert(shadow_x == 1, "expected fail: field set to a value of 0");
+    __CPROVER_assert(shadow_x == 0, "expected success: field defaulted to a value of 0");
+
+    // Set field "shadow" for the memory location denoted by the address of `a`
+    // to a value of `1`.
+    __CPROVER_set_field(&a, "shadow", 1);
+    // Retrieve the value of the field named "shadow" associated with the address
+    // of the object `a`. 
+    shadow_x = __CPROVER_get_field(&a, "shadow");
+    __CPROVER_assert(shadow_x == 1, "expected success: field set to a value of 1");
 }
 ```
+
+Note that setting the value of a local variable from a global SSM field or the
+opposite will produce no effect (and it **will not** fail).