Skip to content

Commit 36ba7df

Browse files
NlightNFotisEnrico Steffinlongo
NlightNFotis
authored and
Enrico Steffinlongo
committed
Add documentation on CBMC Shadow Memory intrinsics
1 parent 99c5402 commit 36ba7df

File tree

2 files changed

+245
-0
lines changed

2 files changed

+245
-0
lines changed

‎doc/cprover-manual/index.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
* [Floating Point](modeling/floating-point/)
2525
* [Generating Environments](goto-harness/)
2626
* [Memory-mapped I/O](modeling/mmio/)
27+
* [Shadow Memory](modeling/shadow-memory/)
2728

2829
8. Build Systems
2930

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

Lines changed: 244 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
1+
# Shadow Memory
2+
3+
The Symbolic Shadow Memory module described below is an implementation of
4+
what is outlined in the paper [CBMC-SSM: Bounded Model Checking of C Programs
5+
with Symbolic Shadow Memory](https://dl.acm.org/doi/abs/10.1145/3551349.3559523).
6+
7+
## Introduction
8+
9+
CBMC implements *Symbolic Shadow Memory*. Symbolic Shadow Memory (from now on,
10+
SSM) allows one to create a parallel memory structure that is maintained by the
11+
analysis program and that shadows the standard memory of the program. In the
12+
Shadow Memory structure, a user can create fields, for which he can get
13+
(retrieve) and set values.
14+
15+
By doing so, a user can organise their own tracking of metadata related to the
16+
code, in a way that is then considered by the backend of CBMC during analysis.
17+
This can be used to implement novel analyses that the CBMC framework itself does
18+
not support. For example, the paper above presents as an example a taint
19+
analysis implemented with the use of the SSM component described here.
20+
21+
## Usage
22+
23+
A user can interact with the Symbolic Shadow Memory component through four CBMC
24+
primitives. These allow the declaration of shadow memory fields, and get/set
25+
their corresponding values:
26+
27+
* `__CPROVER_field_decl_local`
28+
* `__CPROVER_field_decl_global`
29+
* `__CPROVER_get_field`
30+
* `__CPROVER_set_field`
31+
32+
More precisely, their signatures (in pseudo-C, because of some constraints that
33+
we cannot express using the type system), along with some small examples of their
34+
usage, are described below:
35+
36+
### `void __CPROVER_field_decl_local(type1 field_name, SSM_value_type init_value)`
37+
38+
Type constraints:
39+
40+
* `type1`: string literal, such as `"field"`,
41+
* `SSM_value_type`: any value up to 8 bits in size (signed or unsigned).
42+
43+
Declares a local shadow memory field called `field_name`, and initialises it
44+
with the value `init_value`. The field is going to be associated with
45+
function local-scope objects (i.e. a variable on the stack).
46+
47+
Note that each function scope will have a separate *local* shadow memory, so the
48+
value stored in the *local* shadow memory is not propagated to subcalls (even
49+
when the call is recursive).
50+
51+
```c
52+
void func() {
53+
// Sample local object (local variable)
54+
char x = 0;
55+
56+
// Shadow memory field associated with local objects.
57+
__CPROVER_field_decl_local("shadow", (_Bool)1);
58+
}
59+
```
60+
61+
### `void __CPROVER_field_decl_global(type1 field_name, SSM_value_type init_value)`
62+
63+
Type constraints:
64+
65+
* `type1`: string literal, such as `"field"`,
66+
* `SSM_value_type`: any value up to 8 bits in size (signed or unsigned).
67+
68+
As for `__CPROVER_field_decl_local`, but the field declared is associated with
69+
objects whose lifetime exceeds the current function scope (i.e. global variables
70+
or heap allocated objects).
71+
72+
```c
73+
// Sample global object
74+
int a = 10;
75+
76+
void func() {
77+
// Shadow memory field associated with global objects.
78+
__CPROVER_field_decl_global("shadow", (_Bool)0);
79+
}
80+
```
81+
82+
### `SSM_VALUE_TYPE __CPROVER_get_field(type1 *p, type2 field_name)`
83+
84+
Type constraints:
85+
86+
* `SSM_VALUE_TYPE`: the type of the returned value is the same of the SSM field,
87+
i.e. the type that was used to intialise the SSM field during declaration,
88+
* `type1 *`: a non-`void` pointer to an object of type `type1`, whose address we
89+
are going to use for indexing the shadow memory component for the field
90+
declared,
91+
* `type2`: a string literal-typed value, denoting the name of the field whose
92+
value we want to retrieve, such as `"field"`.
93+
94+
Retrieves the latest value associated with a SSM field to the given pointer.
95+
This would be either the value the field was declared to be initialised with,
96+
or, if there had been subsequent changes to it through a `__CPROVER_set_field`
97+
(see `__CPROVER_set_field` section below), the value that it was last `set`
98+
with.
99+
100+
```c
101+
// Sample global object
102+
int a = 10;
103+
104+
void func() {
105+
// Shadow memory field (called "field") associated with global objects.
106+
__CPROVER_field_decl_global("shadow", (_Bool)0);
107+
108+
_Bool shadow_x = __CPROVER_get_field(&a, "shadow");
109+
__CPROVER_assert(shadow_x == 0, "expected success: field initialised with 0");
110+
__CPROVER_assert(shadow_x == 1, "expected fail: field initialised with 0");
111+
}
112+
```
113+
114+
Note that getting the value of a local variable from a global SSM field or the
115+
opposite will return the default value for that SSM field (and it **will not**
116+
fail).
117+
118+
### `void __CPROVER_set_field(type1 *p, type2 field_name, type3 set_value)`
119+
120+
Type constraints:
121+
122+
* `type1 *`: a non-`void` pointer to an object of type `type1`, whose address we
123+
are going to use for indexing the shadow memory component for the field
124+
declared,
125+
* `type2`: a string literal-typed value, denoting the name of the field whose
126+
value we want to retrieve, such as `"field"`,
127+
* `type3`: type of the value to be set. This can be any integer type signed or
128+
unsigned (including `_Bool`). Notice that if this type differs from the type
129+
the SSM field was declared with (`SSM_VALUE_TYPE` above) it will be
130+
implicitly casted to it.
131+
132+
Sets the value associated with a SSM field to the given pointer `p` with the
133+
given value `set_value`. If the `set_value` type is not the `SSM_VALUE_TYPE`, it
134+
will be implicitly casted to it.
135+
136+
```c
137+
// Sample global object, used for addressing within the SSM component.
138+
int a = 10;
139+
140+
void func() {
141+
// Shadow memory field (called "field") associated with global objects.
142+
// Originally assigned a value of `0`, of type `_Bool`.
143+
__CPROVER_field_decl_global("shadow", (_Bool)0);
144+
145+
// Retrieve the value of the field named "shadow" associated with the address
146+
// of the object `a`.
147+
_Bool shadow_x = __CPROVER_get_field(&a, "shadow");
148+
__CPROVER_assert(shadow_x == 0, "expected success: field defaulted to a value of 0");
149+
150+
// Set field "shadow" for the memory location denoted by the address of `a`
151+
// to a value of `1`.
152+
__CPROVER_set_field(&a, "shadow", 1);
153+
// Retrieve the value of the field named "shadow" associated with the address
154+
// of the object `a`.
155+
shadow_x = __CPROVER_get_field(&a, "shadow");
156+
__CPROVER_assert(shadow_x == 1, "expected success: field set to a value of 1");
157+
}
158+
```
159+
160+
Note that setting the value of a local variable from a global SSM field or the
161+
opposite will produce no effect (and it **will not** fail).
162+
163+
### Working with Compound Type Objects
164+
165+
When using SSM on compound type pointers (e.g. `struct` and `union`) the value
166+
used for the `__CPROVER_set_field` will be replicated in each of the fields of
167+
the type, and aggregated again when retrieving them with `__CPROVER_get_field`.
168+
The aggregation function is `or` for an SSM field of `_Bool` type, and `max` for
169+
other types.
170+
171+
This is helpful, for example, in the case of taint analysis (as presented in the
172+
paper and shown below). In this case, when retrieving the taint value of a
173+
struct containing a tainted field the result value will indicate taint (without
174+
the need for changing non-tainted field values), and when setting the taint
175+
value of a struct then all its fields will be set to the given value.
176+
177+
```c
178+
struct S {
179+
unsigned long f1;
180+
char f2;
181+
};
182+
183+
void func() {
184+
// Shadow memory field (called "field") associated with local objects.
185+
// Originally assigned a value of `0`, of type `_Bool`.
186+
__CPROVER_field_decl_local("shadow", (_Bool)0);
187+
188+
// Struct typed variable
189+
struct S s;
190+
191+
// Retrieve the value of the field named "shadow" associated with the address
192+
// of the object `s`. Here we expect a `0` as default.
193+
__CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 0,
194+
"expected success: field defaulted to a value of 0");
195+
// Retrieve the value of the field named "shadow" associated with the address
196+
// of the field `f1` of the object `s`. Here we expect a `0` as default.
197+
__CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 0,
198+
"expected success: field defaulted to a value of 0");
199+
// Retrieve the value of the field named "shadow" associated with the address
200+
// of the field `f1` of the object `s`. Here we expect a `0` as default.
201+
__CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0,
202+
"expected success: field defaulted to a value of 0");
203+
204+
205+
// Set the shadow memory of the field `f1` (ONLY) of the object `s`.
206+
__CPROVER_set_field(&s.f1, "shadow", 1);
207+
208+
// Retrieve the value of the field named "shadow" associated with the address
209+
// of the object `s`. Here we expect a `1` as the value of field `f1` (after
210+
// aggregating all its field values using `max`).
211+
__CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 1,
212+
"expected success: field previously set to a value of 1");
213+
// Retrieve the value of the field named "shadow" associated with the address
214+
// of the field `f1` of the object `s`. Here we expect a `1` as set above.
215+
__CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 1,
216+
"expected success: field previously set to a value of 1");
217+
// Retrieve the value of the field named "shadow" associated with the address
218+
// of the field `f2` of the object `s`. Here we expect a `0` as default.
219+
__CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0,
220+
"expected success: field defaulted to a value of 0");
221+
222+
223+
// Set the shadow memory of the object `s`. This in turns sets also the
224+
// values of each (shadow) field of `s`.
225+
__CPROVER_set_field(&s, "shadow", 0);
226+
227+
// Retrieve the value of the field named "shadow" associated with the address
228+
// of the object `s`. Here we expect a `0` as set above.
229+
__CPROVER_assert(__CPROVER_get_field(&s, "shadow") == 0,
230+
"expected success: field previously set to a value of 0");
231+
// Retrieve the value of the field named "shadow" associated with the address
232+
// of the field `f1` of the object `s`. Here we expect a `0` as the set
233+
// above was replicated on all the fields of `s`.
234+
__CPROVER_assert(__CPROVER_get_field(&s.f1, "shadow") == 0,
235+
"expected success: field previously set to a value of 0");
236+
// Retrieve the value of the field named "shadow" associated with the address
237+
// of the field `f2` of the object `s`. Here we expect a `0` as the set
238+
// above was replicated on all the fields of `s`.
239+
__CPROVER_assert(__CPROVER_get_field(&s.f2, "shadow") == 0,
240+
"expected success: field previously set to a value of 0");
241+
}
242+
```
243+
244+

0 commit comments

Comments
 (0)