Add documentation on CBMC Shadow Memory intrinsics

Author: NlightNFotis

doc/cprover-manual/index.md

@@ -24,6 +24,7 @@
    * [Floating Point](modeling/floating-point/)
    * [Generating Environments](goto-harness/)
    * [Memory-mapped I/O](modeling/mmio/)
+   * [Shadow Memory](modeling/shadow-memory/)
 
 8. Build Systems
 

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

@@ -0,0 +1,148 @@
+# 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).)
+
+## 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.
+
+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
+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:
+
+* `__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:
+
+### `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`.
+
+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).
+
+```c
+void func() {
+    // Sample local object (local variable)
+    char x = 0;
+    
+    // Shadow memory field associated with local objects.
+    __CPROVER_field_decl_local("shadow", (_Bool)1);
+}
+```
+
+### `void __CPROVER_field_decl_global(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`.
+
+Ditto as above, but the field declared is associated with global objects (i.e.
+global variables or heap allocated objects).
+
+```c
+// Sample global object
+int a = 10;
+
+void func() {
+    // Shadow memory field associated with global objects.
+    __CPROVER_field_decl_global("shadow", (_Bool)0);
+}
+```
+
+### `SSM_VALUE_TYPE __CPROVER_get_field(type1 *p, type2 field_name)`
+
+Type constraints:
+
+* `SSM_VALUE_TYPE`: the type of the value that was used to intialise the field
+  with 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.
+
+```c
+// Sample global object
+int a = 10;
+
+void func() {
+    // Shadow memory field (called "field") associated with global objects.
+    __CPROVER_field_decl_global("shadow", (_Bool)0);
+
+    _Bool shadow_x = __CPROVER_get_field(&a, "shadow");
+    __CPROVER_assert(shadow_x == 0, "expected success: field initialised with 0");
+    __CPROVER_assert(shadow_x == 1, "expected fail: field initialised with 0");
+}
+```
+
+### `void __CPROVER_set_field(type1 *p, type2 field_name, type3 set_value)`
+
+Type constraints:
+
+* `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"`,
+* `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.
+
+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.
+
+```c
+// Sample global object
+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);
+
+    // 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");
+}
+```