Skip to content

Selective modelling of volatile variables #5374

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Conversation

danpoe
Copy link
Contributor

@danpoe danpoe commented Jun 4, 2020

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@danpoe danpoe force-pushed the feature/selective-modelling-of-volatile-variables branch 3 times, most recently from 66d99c4 to d13a50b Compare June 8, 2020 08:25
@danpoe danpoe marked this pull request as ready for review June 8, 2020 08:26
@danpoe danpoe added the aws Bugs or features of importance to AWS CBMC users label Jun 8, 2020
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm OK with the code changes, if you have the time I think the commits themselves could be cleaned up a bit.

#include <assert.h>

volatile int a;
volatile int b;

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think one of these should have a regression test involving the interaction with non-volatile variables; E.g.

volatile int x;
int y = x;
assert(x == y); // fails because volatile

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added

@@ -20,7 +20,29 @@ Date: September 2011

using havoc_predicatet = std::function<bool(const exprt &)>;

static bool is_volatile(const namespacet &ns, const typet &src)
class nondet_volatilet

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So... this is just a namespace? Maybe the commit should say why you’re doing this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mentioned in the commit message that this is in preparation for changes to come.

if(ns.lookup(id, symbol))
{
throw invalid_command_line_argument_exceptiont(
"given name `" + id2string(id) + "` not found in symbol table",

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ Should this also be "symbol" rather than "given name"?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Changed

{
throw invalid_command_line_argument_exceptiont(
"given name `" + id2string(id) + "` not found in symbol table",
NONDET_VOLATILE_VARIABLE_OPT);

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ Usually we start these with -- because the _OPT things don’t have it; Without the -- it might be slightly harder to recognise that this is referring to a command line option.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added

NONDET_VOLATILE_VARIABLE_OPT);
}

if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a bit unclear to me why this only works with global variables.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the volatile variables will typically model hardware resources, it would probably make less sense to have volatile variables with automatic storage duration.


void main()
{
int result = a + b;

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, does this work if the global is read via volatile pointer? (I'm assuming no, just for clarification).

Copy link
Contributor Author

@danpoe danpoe Jun 9, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes that's right, it currently only works for direct variable reads.

(One could also mark a pointer as nondet, in which case the pointer dereferences would be nondet as well. Though when --pointer-check would be enabled it would fail.)

const optionst &options)
{
PRECONDITION(!all_nondet);

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ There's a lot happening in 782395c which makes it a bit hard to recognise as a refactoring (i.e. there's so much code moving around its a bit hard to see where what is moving).

@@ -101,27 +108,67 @@ bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src)

void nondet_volatilet::handle_volatile_expression(
exprt &expr,
const namespacet &ns)
const namespacet &ns,

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ bd81144

Says it adds a new --nondet-volatile-model option, but this option is actually added in a different commit.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Changed commit message.

{
if(expr.id()==ID_if)
{
nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), should_havoc);
nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond());

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

❓ Is this case match already covered by existing tests somewhere?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is currently untested as the original nondet volatile code on which this builds was untested. I'll add more tests for the existing code in a separate PR.

danpoe added 7 commits June 9, 2020 11:42
This is in preparation of adding a new feature to selectively provide
models for volatile reads. For this member variables will be added to
nondet_volatilet to store configuration.
This refactors the command line handling and typechecking in class
nondet_volatilet, and adds a new option --nondet-volatile-model
(unimplemented) which will allow selectivly providing models for
volatile reads.
Refactor the code such as to allow later addition of new feature to
selectively provide models for volatile reads
Implements the option --nondet-volatile-model <variable>:<model> to
allow to specify models which are called whenever the given volatile
variable is read. The return value of the model is used as the value
read from the volatile variable.
@danpoe danpoe force-pushed the feature/selective-modelling-of-volatile-variables branch 2 times, most recently from 424f44e to d8c6441 Compare June 9, 2020 11:32
@codecov
Copy link

codecov bot commented Jun 9, 2020

Codecov Report

Merging #5374 into develop will increase coverage by 0.01%.
The diff coverage is 85.95%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5374      +/-   ##
===========================================
+ Coverage    68.16%   68.17%   +0.01%     
===========================================
  Files         1173     1173              
  Lines        97401    97461      +60     
===========================================
+ Hits         66390    66445      +55     
- Misses       31011    31016       +5     
Flag Coverage Δ
#cproversmt2 42.47% <ø> (ø)
#regression 65.38% <85.95%> (+0.01%) ⬆️
#unit 32.18% <ø> (ø)
Impacted Files Coverage Δ
src/goto-instrument/nondet_volatile.cpp 86.80% <85.95%> (+3.47%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 8b604a7...d8c6441. Read the comment docs.

@danpoe danpoe merged commit c7067b0 into diffblue:develop Jun 9, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants