Constant propagation of nondet-symbol [blocks: #35] #3619

tautschnig · 2018-12-21T16:00:03Z

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a 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.

tautschnig · 2018-12-21T16:01:11Z

@smowton I'd be curious whether this can do some of what otherwise might only be achievable via field sensitivity for Java.

smowton · 2018-12-21T16:28:12Z

Propagating a nondet symbol? I don't see how, could you elaborate what you think it might do?

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 3714d25).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95553013

tautschnig · 2018-12-21T16:38:41Z

Propagating a nondet symbol? I don't see how, could you elaborate what you think it might do?

A nondet symbol is a constant, we just don't know its value. The gain is that it does not interfere with structs that are otherwise constants (those of the kind that we know their value), see also the regression test that's included.

kroening · 2018-12-26T14:43:18Z

We should probably rename is_constantt to something like "forward_substitution".

kroening · 2018-12-26T14:44:34Z

Specifically on Java: in principle, Java objects should get zero initialised -- this should enable the propagation without this PR. It may be worth checking whether that actually works.

smowton · 2018-12-27T10:06:49Z

@kroening they do get zero-init'd; this would catch a case such as otherwise_const_thing->field = nondet_value;. Because various arithmetic operations on constants are themselves considered constants quite a lot would get propagated -- I think the objects would only stop getting propagated once there's a phi node, as if_exprt does not inherit constant-ness from its arguments.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: f241b8b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98502213
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

smowton · 2019-01-26T14:30:13Z

My inclination is this is a bad thing (propagating not just nondet_symbol#1 but also a big ball of non-constant arithmetic containing nondet_symbol#1) and will be rendered redundant by field sensitivity

tautschnig · 2019-01-26T14:46:23Z

[...] and will be rendered redundant by field sensitivity

I would have liked to believe this, but in fact these are very much complementary. On one of our verification tasks field sensitivity works as expected, but in order to handle a call to memset we also need a pointer offset to propagate (neither the changes from this PR alone nor field sensitivity alone suffice), which is computed from a sequence of pointer arithmetic. The simplifier is then able to figure out that all the nondets do not matter for the pointer offset, and yields a much-needed constant.

smowton

Fair enough, this is easy to revert if it has bad side-effects, so let's try it

smowton · 2019-01-26T15:25:30Z

src/goto-symex/goto_symex_state.cpp

+    else if(expr.id() == ID_if)
+    {
+      const if_exprt &if_expr = to_if_expr(expr);
+      if(


Seems oddly specific, add a comment saying why this particular restriction?

Comment added.

smowton · 2019-01-26T15:26:17Z

src/goto-symex/goto_symex_state.cpp

+      return true;
+    else if(expr.id() == ID_symbol)
+    {
+      const irep_idt &obj_identifier = to_ssa_expr(expr).get_object_name();


Similarly could use a comment: why this policy for guards only?

Suggest to take the guard prefix from a single place of definition.

Comment added and a refactoring commit added that makes all users use a single definition.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 69012b3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105668394

martin-cs

Seems reasonable.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ef4b9bb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105797178

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5caef74).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105812275

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 90c4a75).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105987217
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: bcb894d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107052342

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 77f93e9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107328775
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0c848d6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107800556

1) Within goto-symex, propagation of nondet_symbol_exprt is actually safe, as they are instantiations of side_effect_expr_nondett and the value of these instantiations cannot change. 2) This highlights that we also need to consider further expressions as possibly being constant in is_constantt which we would otherwise simplify away when they are constant (but cannot any longer do so when nondet_symbol_exprt are contained in there). 3) Constant propagation now yields different right-hand sides in a test, and makes another test trivial. 4) goto-symex applies filters on what is considered "constant" to keep the size of expressions contained as (repeated) simplification of large expressions is expensive. We may revisit this in future as we improve the simplifier.

In order to generate a trace value for an unbounded LHS we may need to look at its RHS as (string) refinement may have constructed values for the RHS.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 85c963c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108226898

TGWDB · 2022-08-01T08:18:04Z

Closing due to age. If you believe this is erroneous please reopen and update the PR.

tautschnig requested review from kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier and smowton as code owners December 21, 2018 16:00

tautschnig added the blocker label Dec 21, 2018

tautschnig changed the title ~~Constant propagation of nondet-symbol~~ Constant propagation of nondet-symbol [blocks: #35] Dec 21, 2018

allredj reviewed Dec 21, 2018

View reviewed changes

tautschnig force-pushed the nondet-prop branch from 3714d25 to 6d92174 Compare January 8, 2019 18:53

tautschnig self-assigned this Jan 9, 2019

tautschnig force-pushed the nondet-prop branch from 6d92174 to f241b8b Compare January 24, 2019 15:24

tautschnig requested a review from chrisr-diffblue as a code owner January 24, 2019 15:24

tautschnig assigned smowton, kroening, peterschrammel, martin-cs and chrisr-diffblue and unassigned tautschnig Jan 24, 2019

allredj reviewed Jan 24, 2019

View reviewed changes

smowton approved these changes Jan 26, 2019

View reviewed changes

tautschnig unassigned smowton Jan 27, 2019

tautschnig force-pushed the nondet-prop branch from 4d0f073 to 69012b3 Compare March 25, 2019 11:40

tautschnig changed the title ~~Constant propagation of nondet-symbol [blocks: #35]~~ Constant propagation of nondet-symbol [depends-on: #4374, blocks: #35] Mar 25, 2019

tautschnig added the dependent - do not merge label Mar 25, 2019

allredj reviewed Mar 25, 2019

View reviewed changes

martin-cs approved these changes Mar 25, 2019

View reviewed changes

tautschnig force-pushed the nondet-prop branch from 69012b3 to ef4b9bb Compare March 26, 2019 07:36

allredj reviewed Mar 26, 2019

View reviewed changes

tautschnig force-pushed the nondet-prop branch from ef4b9bb to 5caef74 Compare March 26, 2019 08:33

tautschnig removed the dependent - do not merge label Mar 26, 2019

tautschnig changed the title ~~Constant propagation of nondet-symbol [depends-on: #4374, blocks: #35]~~ Constant propagation of nondet-symbol [blocks: #35] Mar 26, 2019

tautschnig assigned romainbrenguier Mar 26, 2019

allredj reviewed Mar 26, 2019

View reviewed changes

tautschnig force-pushed the nondet-prop branch from 5caef74 to 90c4a75 Compare March 27, 2019 09:20

allredj reviewed Mar 27, 2019

View reviewed changes

tautschnig removed their assignment Mar 30, 2019

smowton mentioned this pull request Apr 2, 2019

Use sharing_mapt to store propagation map #4464

Merged

4 tasks

tautschnig force-pushed the nondet-prop branch from 90c4a75 to bcb894d Compare April 4, 2019 09:17

allredj reviewed Apr 4, 2019

View reviewed changes

tautschnig force-pushed the nondet-prop branch from bcb894d to 77f93e9 Compare April 6, 2019 15:47

allredj reviewed Apr 6, 2019

View reviewed changes

tautschnig force-pushed the nondet-prop branch from 77f93e9 to 0c848d6 Compare April 10, 2019 11:44

allredj reviewed Apr 10, 2019

View reviewed changes

tautschnig added 2 commits April 13, 2019 15:25

Add arrayst::get to return RHS of unbounded arrays

85c963c

In order to generate a trace value for an unbounded LHS we may need to look at its RHS as (string) refinement may have constructed values for the RHS.

tautschnig force-pushed the nondet-prop branch from 0c848d6 to 85c963c Compare April 13, 2019 15:25

allredj reviewed Apr 13, 2019

View reviewed changes

smowton mentioned this pull request May 10, 2019

Symex: resolve pointer comparisons using the value-set #4444

Merged

7 tasks

tautschnig mentioned this pull request Dec 8, 2021

How to create constant non-deterministic array? #6362

Closed

TGWDB closed this Aug 1, 2022

Constant propagation of nondet-symbol [blocks: #35] #3619

Constant propagation of nondet-symbol [blocks: #35] #3619

Uh oh!

Conversation

tautschnig commented Dec 21, 2018

Uh oh!

tautschnig commented Dec 21, 2018

Uh oh!

smowton commented Dec 21, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Dec 21, 2018

Uh oh!

kroening commented Dec 26, 2018

Uh oh!

kroening commented Dec 26, 2018

Uh oh!

smowton commented Dec 27, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jan 26, 2019

Uh oh!

tautschnig commented Jan 26, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Jan 26, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 30, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Jan 26, 2019

Choose a reason for hiding this comment

Uh oh!

peterschrammel Jan 28, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 30, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

TGWDB commented Aug 1, 2022

Uh oh!

Uh oh!

tautschnig commented Jan 26, 2019 •

edited

Loading