[DOCS] Add documentation on CBMC Shadow Memory intrinsics #7913

NlightNFotis · 2023-09-25T14:48:46Z

This PR adds documentation for the 4 CBMC intrinsics that allow a user to interact with the Symbolic Shadow Memory component to the CProver manual.

I would appreciate reviewers to have a closer look at the following two items:

The location of the documentation is correct (as in, this is in a place that makes sense semantically, and is discoverable).
The Shadow Memory intrinsics types and explanations are correct and lucid, and don't require a lot of mental effort for decoding.

codecov · 2023-09-25T15:44:50Z

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (99c5402) 78.56% compared to head (e68aa9d) 78.99%.
Report is 7 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7913      +/-   ##
===========================================
+ Coverage    78.56%   78.99%   +0.42%     
===========================================
  Files         1699     1701       +2     
  Lines       195804   195932     +128     
===========================================
+ Hits        153833   154769     +936     
+ Misses       41971    41163     -808

see 56 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

TGWDB · 2023-09-25T15:29:52Z

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

+(The original artefact's implementation is outlined in the paper [CBMC-SSM:
+Bounded Model Checking of C Programs with Symbolic Shadow


describes...

TGWDB · 2023-09-25T15:30:14Z

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

+
+## Introduction
+
+CBMC contains a component that supports *Symbolic Shadow Memory*. Shadow memory


CBMC supports Symbolic Shadow Memory.

TGWDB · 2023-09-25T15:30:52Z

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

+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.


In the shadow memory a user can set or retrieve values.

TGWDB · 2023-09-25T15:31:29Z

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

+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,


Shouldn't this be gender neutral? Also the person who is the object of this sentence is expected to be a user of cbmc. Therefore - "By doing so, a user can organise their own tracking of metadata"...

TGWDB · 2023-09-25T15:32:36Z

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

+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


" - for example, " -> ". For example,"

TGWDB · 2023-09-25T15:36:42Z

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

+
+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:


set/retrieve order consistency

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

TGWDB · 2023-09-25T15:38:43Z

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

+
+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:


look like this: -> are described below.

TGWDB · 2023-09-25T15:42:06Z

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

+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)

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

TGWDB · 2023-09-25T16:36:41Z

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

-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 contains a component that implements *Symbolic Shadow Memory*. Symbolic


"contains a component that" -> ""

esteffin

Looks good to me

thomasspriggs · 2023-09-28T10:59:10Z

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

+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,


Shouldn't this be gender neutral? Also the person who is the object of this sentence is expected to be a user of cbmc. Therefore - "By doing so, a user can organise their own tracking of metadata"...

thomasspriggs · 2023-09-28T11:02:45Z

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

+## 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


Suggestion "allow one" -> "support" and splitting into two sentences.
"A user can interact with the Symbolic Shadow Memory component (from now onwards, SSM) through four CBMC primitives. These support the declaration of shadow memory fields, and setting/retrieving their corresponding values:"

I changed to "allow" without "one".

Split in 2 sentences.

thomasspriggs · 2023-09-28T11:04:04Z

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

+
+## Usage
+
+A user can interact with the Symbolic Shadow Memory component (from now on


⛏️ Duplication when read across line breaks - "on onwards"

thomasspriggs · 2023-09-28T11:07:52Z

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

+
+Type constraints:
+
+* `type1`: string literal, such as `"field"`,


Maybe worth emphasising that by string literal we mean that the field name must be compile time constant and may not be the result of runtime string manipulation. That is, if my understanding of what you are trying to say here is correct...

What I meant is that it has to be a string literal such as "this is a string literal".

In the exprt world it has to be a constant_stringt.

Ok. My understanding is correct. I think it is worth making the documentation spell out the exact details of what is and is not allowed as an argument here.

thomasspriggs · 2023-09-28T11:09:51Z

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

+
+Type constraints:
+
+* `type1`: string literal, such as `"field"`,


See previous comment of clarifying string literal.

thomasspriggs · 2023-09-28T11:14:53Z

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

+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.


My understanding is that the shadow memory operates on the byte level. Therefore even if you declare the field as being 16 bits, if you pass in a value of say 300, than value would be truncated to fit in 8 bits. Is my understanding correct/incorrect and does that need to be explained here?

No, when declaring shadow memory we should use the exact type, so < 8 bits.

The truncation happens only on set_field and it is explained there.

thomasspriggs · 2023-09-28T11:22:38Z

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

+* `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)


If a user wants to use shadow memory for a value which goes through a function return, should the shadow memory be declared as local or global? It could be local based on it being on the stack or global based on it exceeding the lifetime of the function, so as a user I would be unsure which to declare it as.

It is based on the scope, so when you leave it everything is lost.

So does that mean the shadow memory would have to be declared as global in that case?

Nope, that is unfortunately a shortcoming of the actual implementation.

Global is for global variables and heap-allocated pointers.
Local is for the local function scope.

There may be in the future a way to propagate local shadow memory information to called functions and through return, but it is not implemented yet.

Can we add the limitation to the documentation then? Do similar limitations apply to function arguments? Do they only apply to stack memory or can the limitations be dodged by heap allocating and passing pointers?

Yes, it is possible to heap-allocate arguments and return types so they will be tracked on the global SM.

About the documentation I'm not too keen at adding a "limitation" section as it draws attention to the limitation itself.

As the documentation says already local is for local only and is not passed to sub-call, I added that the same applies to returns, so the only way around is having the passed-around values on the global SM.

I disagree on the subject of documenting limitations. If we document them, then it allows users to work around them and allows us to point to the documentation if anyone runs across them. It also adds strength to the argument that removing such limitations is a feature request, rather than a bug fix. However I am happy to leave this to your discretion.

If using global shadow memory enables support for function arguments and returns then doesn't that answer my original question of whether local or global declarations are needed for that use case?

thomasspriggs · 2023-09-28T11:25:48Z

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

+
+### Working with Compound Type Objects
+
+When using SSM on compound type pointers (e.g. `struct`) the value used for the


Does this description of shadow memory as it applies to struct types also apply to unions and arrays?

thomasspriggs · 2023-09-28T11:30:56Z

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

+* `__CPROVER_field_decl_local`
+* `__CPROVER_field_decl_global`
+* `__CPROVER_get_field`
+* `__CPROVER_set_field`


Is it worth noting that these are only currently supported for the C front end? I am kind of assuming that these are unavailable for the JBMC at the moment.

NlightNFotis added the documentation label Sep 25, 2023

NlightNFotis requested review from jimgrundy, TGWDB, kroening, tautschnig and peterschrammel as code owners September 25, 2023 14:48

TGWDB reviewed Sep 25, 2023

View reviewed changes

NlightNFotis force-pushed the shadow_mem_docs branch 2 times, most recently from 5e3d405 to a4c9364 Compare September 27, 2023 15:47

TGWDB approved these changes Sep 27, 2023

View reviewed changes

esteffin approved these changes Sep 28, 2023

View reviewed changes

thomasspriggs reviewed Sep 28, 2023

View reviewed changes

esteffin force-pushed the shadow_mem_docs branch from cced7fd to 36ba7df Compare September 28, 2023 13:35

Add documentation on CBMC Shadow Memory intrinsics

e68aa9d

esteffin force-pushed the shadow_mem_docs branch from 36ba7df to e68aa9d Compare September 28, 2023 17:34

esteffin merged commit 45fa2ca into diffblue:develop Sep 29, 2023

esteffin deleted the shadow_mem_docs branch September 29, 2023 10:23

		(The original artefact's implementation is outlined in the paper [CBMC-SSM:
		Bounded Model Checking of C Programs with Symbolic Shadow


		## Introduction

		CBMC contains a component that supports Symbolic Shadow Memory. Shadow memory


		## Usage

		A user can interact with the Symbolic Shadow Memory component (from now on


		Type constraints:

		* `type1`: string literal, such as `"field"`,


		### Working with Compound Type Objects

		When using SSM on compound type pointers (e.g. `struct`) the value used for the

[DOCS] Add documentation on CBMC Shadow Memory intrinsics #7913

[DOCS] Add documentation on CBMC Shadow Memory intrinsics #7913

Uh oh!

Conversation

NlightNFotis commented Sep 25, 2023

Uh oh!

codecov bot commented Sep 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

esteffin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

esteffin Sep 28, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Sep 25, 2023 •

edited

Loading

esteffin Sep 28, 2023 •

edited

Loading