SMT2 floating point encoding fix #4395

kroening · 2019-03-16T11:06:26Z

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.

kroening · 2019-03-17T12:41:15Z

This will need a non-recursive variant of letification, which is a few steps away from #4396.

This avoids stack overflow in the case of expressions with many unique subexpressions. PR #4395 is an exemplar.

allredj

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

allredj

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

romainbrenguier · 2019-03-20T06:41:38Z

src/solvers/smt2/smt2irep.cpp

-        throw error("unexpected end of file");
+        if(stack.empty())
+        {
+          result = irept(irep_idt());


Is this really necessary with the result.clear() above?

No, not strictly; this is primarily meant to make it clear what is returned.

I guess to really make it clear the best way would be to make parse return an optionalt<irept> instead of a bool.

+1 for using optionalt<irept>

But then also this commit should just be in a PR of its own where those kinds of changes could be made. It really doesn't relate to floating-point encoding fixes in any obvious way.

src/solvers/smt2/smt2_conv.cpp

replace recursion in letify_rec by loop [blocks: #4395]

Z3, for instance, produces newlines at the end of the response; this should be tolerated by the parser.

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

kroening · 2019-03-24T22:46:33Z

There is now a separate commit with the optional return value of smt2irep.

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

This case was missing but is used in our lowering of floating-point operations.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: efebade).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105603393
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 9d2a61e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105604164
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 8c4c5e5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105604746
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

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

src/solvers/smt2/smt2_conv.cpp

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

kroening added SMT Backend Interface bugfix labels Mar 16, 2019

kroening requested review from allredj, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners March 16, 2019 11:06

kroening force-pushed the smt2float branch from 115687d to c02a088 Compare March 16, 2019 11:07

kroening added the work in progress label Mar 17, 2019

peterschrammel assigned kroening Mar 18, 2019

kroening force-pushed the smt2float branch from c02a088 to 9de8249 Compare March 18, 2019 22:05

kroening removed the work in progress label Mar 19, 2019

kroening mentioned this pull request Mar 19, 2019

replace recursion in letify_rec by loop [blocks: #4395] #4406

Merged

4 tasks

kroening pushed a commit that referenced this pull request Mar 19, 2019

replace recursion in letify_rec by loop

a4a4073

This avoids stack overflow in the case of expressions with many unique subexpressions. PR #4395 is an exemplar.

kroening removed their assignment Mar 19, 2019

kroening force-pushed the smt2float branch from 9de8249 to 80e33fb Compare March 19, 2019 08:43

allredj reviewed Mar 19, 2019

View reviewed changes

kroening force-pushed the smt2float branch from 80e33fb to cf71d76 Compare March 19, 2019 09:28

allredj reviewed Mar 19, 2019

View reviewed changes

peterschrammel added the dependent - do not merge label Mar 19, 2019

peterschrammel approved these changes Mar 19, 2019

View reviewed changes

peterschrammel assigned kroening Mar 19, 2019

romainbrenguier reviewed Mar 20, 2019

View reviewed changes

tautschnig changed the title ~~SMT2 floating point encoding fix~~ SMT2 floating point encoding fix [depends-on: #4396] Mar 21, 2019

tautschnig changed the title ~~SMT2 floating point encoding fix [depends-on: #4396]~~ SMT2 floating point encoding fix [depends-on: #4406] Mar 21, 2019

martin-cs requested changes Mar 21, 2019

View reviewed changes

src/solvers/smt2/smt2_conv.cpp Show resolved Hide resolved

src/solvers/smt2/smt2_conv.cpp Outdated Show resolved Hide resolved

tautschnig added a commit that referenced this pull request Mar 24, 2019

Merge pull request #4406 from diffblue/non-rec-letify

d5cf916

replace recursion in letify_rec by loop [blocks: #4395]

tautschnig added Needs rebase and removed dependent - do not merge labels Mar 24, 2019

tautschnig changed the title ~~SMT2 floating point encoding fix [depends-on: #4406]~~ SMT2 floating point encoding fix Mar 24, 2019

tolerate whitespace at end of SMT2 result

4e0ad85

Z3, for instance, produces newlines at the end of the response; this should be tolerated by the parser.

kroening force-pushed the smt2float branch 2 times, most recently from efebade to 9d2a61e Compare March 24, 2019 22:44

kroening pushed a commit that referenced this pull request Mar 24, 2019

smt2irep now returns optional

a66a055

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

kroening removed the Needs rebase label Mar 24, 2019

kroening assigned tautschnig and martin-cs and unassigned kroening Mar 24, 2019

kroening force-pushed the smt2float branch from 9d2a61e to 8c4c5e5 Compare March 24, 2019 22:52

tautschnig assigned kroening and unassigned tautschnig Mar 24, 2019

Daniel Kroening added 2 commits March 24, 2019 22:54

smt2irep now returns optional

3a9b5e0

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

implement cast bv -> floatbv

be64fc1

This case was missing but is used in our lowering of floating-point operations.

kroening force-pushed the smt2float branch from 8c4c5e5 to be64fc1 Compare March 24, 2019 22:54

allredj reviewed Mar 25, 2019

View reviewed changes

martin-cs approved these changes Mar 25, 2019

View reviewed changes

src/solvers/smt2/smt2_conv.cpp Show resolved Hide resolved

tautschnig unassigned martin-cs Mar 25, 2019

kroening merged commit 84cd7fd into develop Mar 25, 2019

kroening deleted the smt2float branch March 25, 2019 21:17

kroening pushed a commit that referenced this pull request Mar 25, 2019

smt2irep now returns optional

efeff92

This is follow-up from a discussion in #4395 and clarifies the contract of this function.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

SMT2 floating point encoding fix #4395

SMT2 floating point encoding fix #4395

Uh oh!

kroening commented Mar 16, 2019

Uh oh!

kroening commented Mar 17, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

romainbrenguier Mar 20, 2019

Uh oh!

kroening Mar 20, 2019

Uh oh!

romainbrenguier Mar 20, 2019

Uh oh!

tautschnig Mar 21, 2019

Uh oh!

tautschnig Mar 21, 2019

Uh oh!

Uh oh!

Uh oh!

kroening commented Mar 24, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Uh oh!

SMT2 floating point encoding fix #4395

SMT2 floating point encoding fix #4395

Uh oh!

Conversation

kroening commented Mar 16, 2019

Uh oh!

kroening commented Mar 17, 2019

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!

romainbrenguier Mar 20, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Mar 20, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Mar 20, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 21, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 21, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

kroening commented Mar 24, 2019

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!

Uh oh!

Uh oh!