Add a small paragraph explaining operation on compound type objects and aggregation

Author: NlightNFotis

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

@@ -151,11 +151,94 @@ void func() {
     // 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`. 
+    // 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).
+
+### Working with Compound Type Objects
+
+When using SSM on compound type pointers (e.g. `struct`) the value used for the
+`__CPROVER_set_field` will be replicated in each of the fields of the type, and
+aggregated again when retrieving them with `__CPROVER_get_field`. The
+aggregation function is `or` for an SSM field of `_Bool` type, and `max` for
+other types.
+
+This is helpful, for example, in the case of taint analysis (as presented in the
+paper and shown below). In this case, when retrieving the taint value of a
+struct containing a tainted field the result value will indicate taint (without
+the need for changing non-tainted field values), and when setting the taint
+value of a struct then all its fields will be set to the given value.
+
+```c
+struct S {
+  unsigned long f1;
+  char f2;
+};
+
+void func() {
+  // Shadow memory field (called "field") associated with local objects.
+  // Originally assigned a value of `0`, of type `_Bool`.
+  __CPROVER_field_decl_local("shadow", (_Bool)0);
+
+  // Struct typed variable
+  struct S s;
+  
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the object `s`. Here we expect a `0` as default.
+  __CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 0, 
+                   "expected success: field defaulted to a value of 0");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f1` of the object `s`. Here we expect a `0` as default.
+  __CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 0, 
+                   "expected success: field defaulted to a value of 0");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f1` of the object `s`. Here we expect a `0` as default.
+  __CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0, 
+                   "expected success: field defaulted to a value of 0");
+
+
+  // Set the shadow memory of the field `f1` (ONLY) of the object `s`.
+  __CPROVER_set_field(&s.f1, "shadow", 1);
+
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the object `s`. Here we expect a `1` as the value of field `f1` (after
+  // aggregating all its field values using `max`).
+  __CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 1, 
+                   "expected success: field previously set to a value of 1");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f1` of the object `s`. Here we expect a `1` as set above.
+  __CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 1, 
+                   "expected success: field previously set to a value of 1");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f2` of the object `s`. Here we expect a `0` as default.
+  __CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0, 
+                   "expected success: field defaulted to a value of 0");
+
+
+  // Set the shadow memory of the object `s`. This in turns sets also the 
+  // values of each (shadow) field of `s`.
+  __CPROVER_set_field(&s, "shadow", 0);
+
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the object `s`. Here we expect a `0` as set above.
+  __CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 0, 
+                   "expected success: field previously set to a value of 0");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f1` of the object `s`. Here we expect a `0` as the set
+  // above was replicated on all the fields of `s`.
+  __CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 0, 
+                   "expected success: field previously set to a value of 0");
+  // Retrieve the value of the field named "shadow" associated with the address
+  // of the field `f2` of the object `s`. Here we expect a `0` as the set
+  // above was replicated on all the fields of `s`.
+  __CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0, 
+                   "expected success: field previously set to a value of 0");
+}
+```
+
+