Skip to content

Assert type consistency in the simplifier #2064

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 3 commits into from
Mar 7, 2019
Merged

Assert type consistency in the simplifier #2064

merged 3 commits into from
Mar 7, 2019

Conversation

tautschnig
Copy link
Collaborator

No description provided.

@tautschnig tautschnig mentioned this pull request Apr 15, 2018
Closed
@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 6ea9073 to 4ad5c54 Compare April 16, 2018 06:39
smowton
smowton reviewed Apr 16, 2018
View reviewed changes
src/analyses/goto_check.cpp Outdated
{
exprt overflow("overflow-"+expr.id_string(), bool_typet());
overflow.operands()=expr.operands();
exprt tmp;
Copy link
Contributor

Choose a reason for hiding this comment

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

Rename binary_check_lhs?

src/analyses/goto_check.cpp Outdated
{
if(expr.operands().size()==2)
// The overflow checks are binary!
// We break these up.
Copy link
Contributor

Choose a reason for hiding this comment

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

... e.g. for "a + b + c + d" we check "a + b", "(a + b) + c", "(a + b + c) + d"

src/analyses/goto_check.cpp Outdated
tmp.operands().resize(i);
}

exprt tmp2 = expr;
Copy link
Contributor

Choose a reason for hiding this comment

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

Rename binary_check?

src/analyses/goto_check.cpp Outdated
exprt overflow("overflow-" + expr.id_string(), bool_typet());
overflow.operands() = expr.operands();

// this is overflow over integers
Copy link
Contributor

Choose a reason for hiding this comment

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

How about // check for address space overflow, since I guess the point is we're checking whether we wrap the VAS?

@kroening
Copy link
Member

Why not simply use make_binary()?

@kroening
Copy link
Member

Ok, that has type checks that will fail -- I would add a separate function make_pointer_arithmetic_binary, which relaxes the check, and then call that.

@tautschnig
Copy link
Collaborator Author

I will overhaul this PR completely as I have in parts been solving the wrong problem. Notably, the expressions passed to pointer_overflow_check are always binary. Step 1 will be adding a test that uses --pointer-overflow-check ...

@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 4ad5c54 to bdd71ab Compare April 18, 2018 12:16
@tautschnig tautschnig requested a review from kroening as a code owner April 18, 2018 12:16
@tautschnig tautschnig changed the title pointer-overflow-check: support >2 operands Fix pointer-arithmetic simplification and add tests Apr 18, 2018
@tautschnig
Copy link
Collaborator Author

@kroening @smowton This PR has been almost completely changed, please take a fresh look.

@tautschnig tautschnig force-pushed the pointer-overflow-check branch from bdd71ab to 4ea6c4c Compare April 19, 2018 00:33
@tautschnig
Copy link
Collaborator Author

This turned into a surprisingly widespread bug-fixing session. Can @romainbrenguier please take a look at the changes I had to make in the string refinement, @kroening please comment on fixes in the simplifier.

@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 4ea6c4c to 18c6c1f Compare April 19, 2018 06:06
romainbrenguier
romainbrenguier reviewed Apr 19, 2018
View reviewed changes
src/solvers/refinement/string_refinement.cpp Outdated
while(s.id() == ID_if)
{
if_exprt s_if = to_if_expr(s);
simplify(s_if.cond(), ns);
Copy link
Contributor

Choose a reason for hiding this comment

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

this copies the whole s exprt, would it be better to just copy the condition?

Copy link
Contributor

Choose a reason for hiding this comment

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

and why is this not part of simplify_expr?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I will change this to exprt simp_cond = simplify_expr(to_if_expr(s).cond(), ns); with another to_if_expr(s).{true,false}_case() below.

src/util/simplify_expr_int.cpp Outdated
@@ -894,7 +895,9 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
if(op.is_true() || op.is_false())
{
bool value=op.is_true();
op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
op = constant_exprt(
value ? ID_1 : ID_0, bitvector_typet(expr.type().id(), 1));
Copy link
Contributor

Choose a reason for hiding this comment

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

value should be const, or could be inlined here

Copy link
Collaborator Author

@tautschnig tautschnig Apr 19, 2018 •
edited
Loading

Choose a reason for hiding this comment

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

True, but unrelated to the fix here? Let me know if you insist, though. I have made the change.

@tautschnig tautschnig force-pushed the pointer-overflow-check branch 2 times, most recently from 37fbecb to ba7ce39 Compare April 20, 2018 00:40
@tautschnig tautschnig requested a review from pkesseli as a code owner February 13, 2019 12:24
@tautschnig tautschnig changed the title Fix pointer-arithmetic simplification and add tests Assert type consistency in the simplifier [depends-on: #4056] Feb 13, 2019
@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 93b83cf to 5ceaec0 Compare March 2, 2019 14:27
@tautschnig tautschnig changed the title Assert type consistency in the simplifier [depends-on: #4056] Assert type consistency in the simplifier [depends-on: #4314] Mar 2, 2019
@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 5ceaec0 to 6a4d11d Compare March 3, 2019 00:06
@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 6a4d11d to 151babd Compare March 3, 2019 21:16
@tautschnig
Note type inconsistencies in solver axioms and avoid simplifying
bbc3f63 
array_poolt::make_char_array_for_char_pointer generates conditional expressions
denoting possible array sizes. This results in types without a fixed size, and
is used to construct ifthenelse expressions that may have multiple types. This
is not permitted, and thus must be filtered out before passing to further
processing, such as simplification or flattening.
@tautschnig
Expression simplification must not alter the type
c564c2c
@tautschnig
Simplifier: As we now assert type equality we can remove a safety net
8616586 
If the simplifier receives an expression that isn't type-consistent it might
produce a type-inconsistent result, but we will now fail an invariant in that
case.
@tautschnig tautschnig force-pushed the pointer-overflow-check branch from 151babd to 8616586 Compare March 7, 2019 07:05
@tautschnig tautschnig changed the title Assert type consistency in the simplifier [depends-on: #4314] Assert type consistency in the simplifier Mar 7, 2019
@tautschnig
Copy link
Collaborator Author

This is now ready for review - @romainbrenguier in particular, but maybe also @martin-cs and @peterschrammel.

romainbrenguier
romainbrenguier reviewed Mar 7, 2019
View reviewed changes
Copy link
Contributor

@romainbrenguier romainbrenguier left a comment

Choose a reason for hiding this comment

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

I will do a TG pull request to check no invariant fails on our tests.

src/solvers/strings/string_refinement.cpp
@@ -869,7 +912,10 @@ void string_refinementt::add_lemma(

exprt simple_lemma = lemma;
if(simplify_lemma)
{
simple_lemma = adjust_if_recursive(std::move(simple_lemma), ns);
Copy link
Contributor

Choose a reason for hiding this comment

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

This will probably not get rid of all the inconsistencies, so I'm not sure about how useful it is. Ideally we should get rid of the introduction of type inconsistencies, but I'm not sure about the best way to do that.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I recall having tried removing them completely (which would be done by using type casts), but that did not seem to work very well. It's the long-term solution, and maybe that's what we should actually invest in instead of this hack. Not sure though, I'm certainly curious about the results with TG!

Copy link
Contributor

Choose a reason for hiding this comment

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

Everything is green on our side, so nothing blocking merging it.

@romainbrenguier romainbrenguier added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Mar 7, 2019
allredj
allredj reviewed Mar 7, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

@romainbrenguier romainbrenguier removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Mar 7, 2019
@tautschnig tautschnig merged commit bc6c41e into diffblue:develop Mar 7, 2019
@tautschnig tautschnig deleted the pointer-overflow-check branch March 7, 2019 10:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@thk123 thk123 thk123 left review comments

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@kroening kroening kroening approved these changes

@romainbrenguier romainbrenguier romainbrenguier approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@danpoe danpoe Awaiting requested review from danpoe

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@owen-mc-diffblue owen-mc-diffblue Awaiting requested review from owen-mc-diffblue

Assignees

@peterschrammel peterschrammel

@martin-cs martin-cs

@romainbrenguier romainbrenguier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
9 participants
@tautschnig @kroening @smowton @thk123 @martin-cs @romainbrenguier @allredj @peterschrammel @chrisr-diffblue