Vsd meet and assume #6023

jezhiggins · 2021-04-12T15:13:47Z

Two related strands of work in this PR.

Extending abstract_environmentt::assume to cover all value representations. Up until now, assume was only correct for constants. It may have evaluated a given expression correctly for intervals and value-sets, but not reliably. These changes all assume expressions to be properly evaluated for all value representation, and in the face of different representations within the same expression.
Filling out the implementation of abstract_objectt::meet for value representations. Where merge is the union of two values, meet is the intersection. meet is used when evaluating an assumed equality expression.

+2,331/-384 looks alarming, but the major bulk of that is test cases exercising various combinations of constants, intervals, value-sets, and operators in assume and in meet.

jezhiggins · 2021-04-12T16:00:32Z

MacOS build failures look to be a meta-problem getting the tool dependencies

==> Downloading https://homebrew.bintray.com/bottles/ninja-1.10.2.catalina.bottle.tar.gz
curl: (22) The requested URL returned error: 403 Forbidden
Error: Failed to download resource "ninja"
Download failed: https://homebrew.bintray.com/bottles/ninja-1.10.2.catalina.bottle.tar.gz
Error: Process completed with exit code 1.

martin-cs · 2021-04-12T16:05:16Z

Paging @NlightNFotis and @thomasspriggs for the Mac OS CI issues.

NlightNFotis · 2021-04-12T16:21:00Z

I took a quick look at it - in the beginning I thought that they upgraded the version so it's hitting the wrong URL because of outdated database issues (kind of like needing an apt-get update, if you want).

But it looks like it's still the same version of the formula (https://formulae.brew.sh/formula/ninja), and it's 403 if you hit the URL, which seems to be sitting on their servers, so I'm assuming this must be a temporary issue they are having.

Could you try it again (just restart the jobs from the github interface) later, and let me know if it doesn't work? I'll take a deeper look at it then.

codecov · 2021-04-12T17:06:50Z

Codecov Report

Merging #6023 (b23e00d) into develop (0002950) will increase coverage by 8.01%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6023      +/-   ##
===========================================
+ Coverage    67.40%   75.42%   +8.01%     
===========================================
  Files         1157     1454     +297     
  Lines        95236   159739   +64503     
===========================================
+ Hits         64197   120477   +56280     
- Misses       31039    39262    +8223

Flag	Coverage Δ
cproversmt2	`?`
regression	`?`
unit	`?`

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	`52.94% <0.00%> (-47.06%)`	⬇️
src/ansi-c/gcc_types.cpp	`41.86% <0.00%> (-46.38%)`	⬇️
src/solvers/prop/prop.cpp	`42.85% <0.00%> (-41.76%)`	⬇️
src/solvers/flattening/boolbv_member.cpp	`53.65% <0.00%> (-38.65%)`	⬇️
src/cpp/cpp_storage_spec.cpp	`65.00% <0.00%> (-35.00%)`	⬇️
src/util/cmdline.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/solvers/strings/array_pool.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/solvers/strings/string_refinement.h	`66.66% <0.00%> (-33.34%)`	⬇️
...rs/strings/string_concatenation_builtin_function.h	`0.00% <0.00%> (-33.34%)`	⬇️
src/ansi-c/c_typecheck_base.cpp	`50.54% <0.00%> (-30.35%)`	⬇️
... and 1433 more

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 b84b37d...b23e00d. Read the comment docs.

tautschnig · 2021-04-13T08:31:15Z

MacOS build failures look to be a meta-problem getting the tool dependencies

==> Downloading https://homebrew.bintray.com/bottles/ninja-1.10.2.catalina.bottle.tar.gz
curl: (22) The requested URL returned error: 403 Forbidden
Error: Failed to download resource "ninja"
Download failed: https://homebrew.bintray.com/bottles/ninja-1.10.2.catalina.bottle.tar.gz
Error: Process completed with exit code 1.

For the record: actions/runner-images#3165 - presumably the current run will have updated runners already.

martin-cs

In principle happy but there are a few details to check.

regression/goto-analyzer/branching-ge/test-always-intervals.desc

src/analyses/variable-sensitivity/abstract_environment.cpp

Seperates the assume evaluation from the action arising.

This is the first step on splitting out assume so we can given sensible answers for all value representations, not just constants.

Consider cases when one or other operand is not a value, or is unknown. Implement meet for write_location_context.

For intervals and value-sets it's possible for, say, (a > b) and !(a > b) to both be true. When evaluationing !(expr) we can't simply flip the result. Instead, where we can, we need to rewrite !(a > b) as (a <= b) and evaluate that instead.

We can bail out early if an operand evals to false. Otherwise we must evaluate al lthe operands, so that any pruning is applied. That done, we return true iff all operands are true, otherwise we return nil if anywhere nil.

Implemented for intervals and value-sets which are not top.

These operations are symmetric, so we can rewrite x > y as y < x, and x >= y as y <= x. As a consequence of rewriting, greater than assumptions now also prune.

… is -INF

Remove duplication in data_dependency & write_location merge and meet. Correct data_dependency_contextt:: has_been_modified to verify child object is also unchanged

Found and fixed a problem in interval_abstract_value::to_constant(), for case when interval is a valid single value, but the whole thing is also top. This could arise in a merge of, say, [0, 0] and TOP.

jezhiggins force-pushed the vsd-widening-implementation branch 2 times, most recently from eeaaee8 to 1614d74 Compare April 12, 2021 15:51

jezhiggins force-pushed the vsd-widening-implementation branch from 1614d74 to 918f68d Compare April 13, 2021 08:16

jezhiggins force-pushed the vsd-widening-implementation branch 6 times, most recently from 93848ac to 83414be Compare April 22, 2021 14:39

jezhiggins mentioned this pull request Apr 22, 2021

Vsd - widening during abstract object merge #6046

Merged

jezhiggins marked this pull request as ready for review April 22, 2021 15:14

jezhiggins requested review from chrisr-diffblue, martin-cs, peterschrammel and smowton as code owners April 22, 2021 15:14

jezhiggins force-pushed the vsd-widening-implementation branch 4 times, most recently from 2492245 to ba7d4b9 Compare May 8, 2021 10:04

tautschnig assigned martin-cs May 11, 2021

jezhiggins force-pushed the vsd-widening-implementation branch from ba7d4b9 to da1e973 Compare May 11, 2021 08:43

jezhiggins force-pushed the vsd-widening-implementation branch from da1e973 to f191b3c Compare May 18, 2021 12:01

martin-cs approved these changes May 20, 2021

View reviewed changes

jezhiggins force-pushed the vsd-widening-implementation branch 2 times, most recently from 53134d6 to b427be5 Compare May 22, 2021 09:20

jezhiggins added 26 commits June 15, 2021 08:59

Split out do_assume from abstract_environment::assume

9ddd1da

Seperates the assume evaluation from the action arising.

Rewrite comparison tests in terms of environment::do_assume

2485484

Initial assume_eq

34d3dd7

This is the first step on splitting out assume so we can given sensible answers for all value representations, not just constants.

unit tests for assume, equality comparison

e163746

Refactor assume unit tests so we can more easily add further tests

46bcf6d

First pass at evaluating != in assume.

5ce31c3

Extend assume to handle negated expressions.

fa7c185

Consider cases when one or other operand is not a value, or is unknown. Implement meet for write_location_context.

Extend assume to cover <=, less than or equals

c64ab0a

Extend assume to cover <, less than

ff0903f

Replace if ladder with table lookup in do_assume

bd5f278

Pulled out eval_operands_as_values from assume_le/assume_lt

b58d811

Extend assume to cover >=, greater than or equal

8354a9f

Extended assume to cover >, greater than

a3f7099

Extended assume to cover and expressions

3b2ed1f

Extended assume to cover or expressions

3b7e91f

Test showing loop terminates using constants, intervals, or value-sets

85998ff

Correct assume_and implementation

1d7c298

We can bail out early if an operand evals to false. Otherwise we must evaluate al lthe operands, so that any pruning is applied. That done, we return true iff all operands are true, otherwise we return nil if anywhere nil.

Call ai_simplify before calling abstract_state.assume

5a8f691

Rewrite assume_or in terms of assume_and

8f27225

Unit tests for assume value pruning

546e705

Domain pruning for < and <= assumptions.

b4e2353

Implemented for intervals and value-sets which are not top.

Reimplemented assume_greater_than in terms of assume_less_than

826326f

These operations are symmetric, so we can rewrite x > y as y < x, and x >= y as y <= x. As a consequence of rewriting, greater than assumptions now also prune.

interval_abstract_value::output fix displaying upper limit when lower…

e059490

… is -INF

Prune TOP values when assuming less than expressions

9cb937d

Remove duplication in data_dependency & write_location merge and meet. Correct data_dependency_contextt:: has_been_modified to verify child object is also unchanged

Prune TOP values in assume_eq

b23e00d

Found and fixed a problem in interval_abstract_value::to_constant(), for case when interval is a valid single value, but the whole thing is also top. This could arise in a merge of, say, [0, 0] and TOP.

jezhiggins force-pushed the vsd-widening-implementation branch from 371936f to b23e00d Compare June 15, 2021 08:01

martin-cs merged commit 1ff5344 into diffblue:develop Jun 15, 2021

jezhiggins deleted the vsd-widening-implementation branch June 16, 2021 11:48

jezhiggins mentioned this pull request Aug 16, 2021

VSD - Regression tests to capture behaviour of assertions #6300

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Vsd meet and assume #6023

Vsd meet and assume #6023

Uh oh!

jezhiggins commented Apr 12, 2021 •

edited

Loading

Uh oh!

jezhiggins commented Apr 12, 2021

Uh oh!

martin-cs commented Apr 12, 2021

Uh oh!

NlightNFotis commented Apr 12, 2021

Uh oh!

codecov bot commented Apr 12, 2021 •

edited

Loading

Uh oh!

tautschnig commented Apr 13, 2021

Uh oh!

martin-cs left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Vsd meet and assume #6023

Vsd meet and assume #6023

Uh oh!

Conversation

jezhiggins commented Apr 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jezhiggins commented Apr 12, 2021

Uh oh!

martin-cs commented Apr 12, 2021

Uh oh!

NlightNFotis commented Apr 12, 2021

Uh oh!

codecov bot commented Apr 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig commented Apr 13, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jezhiggins commented Apr 12, 2021 •

edited

Loading

codecov bot commented Apr 12, 2021 •

edited

Loading