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

Error handling cleanup in solvers/smt2 #2963

Merged

tautschnig merged 4 commits into diffblue:develop from danpoe:refactor/error-handling-solvers-smt2

Sep 28, 2018

Contributor

danpoe commented Sep 14, 2018

No description provided.

danpoe requested review from kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners

September 14, 2018 17:40

danpoe added the work in progress label

danpoe force-pushed the refactor/error-handling-solvers-smt2 branch 4 times, most recently from e5b5a69 to 6c4e483 Compare

September 17, 2018 16:05

danpoe removed the work in progress label

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

Passed Diffblue compatibility checks (cbmc commit: 6c4e483).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85042148

tautschnig requested changes

View reviewed changes

Collaborator

tautschnig left a comment

Mostly small issues; some of my comments repeat a couple of times, which really begs the question whether such code should be factored out.

src/util/arith_tools.h Outdated

@@ @@ -125,30 +125,31 @@ optionalt<Target> numeric_cast(const exprt &arg) @@
               }
               /// Convert an mp_integer to integral type Target
-              /// An invariant with fail with message "Bad conversion" if conversion
-              /// is not possible.
+              /// An invariant with fail if the conversion is not possible.

Collaborator

tautschnig Sep 19, 2018

Not actually your fault, but as you are touching this line: s/with/will/

src/util/arith_tools.h Outdated

                 return *maybe;
               }
               /// Convert an expression to integral type Target
-              /// An invariant with fail with message "Bad conversion" if conversion
-              /// is not possible.
+              /// An invariant with fail if the conversion is not possible.

Collaborator

tautschnig Sep 19, 2018

As above: s/with/will/

src/solvers/smt2/smt2_conv.cpp Outdated

-                mp_integer i;
-                if(to_integer(expr.op1(), i))
-                  INVALIDEXPR("byte_update takes constant as second parameter");
+                mp_integer i = numeric_cast_v<mp_integer>(expr.op1());

Collaborator

tautschnig Sep 19, 2018

Use .offset() instead of .op1()

src/solvers/smt2/smt2_conv.cpp Outdated

                   out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
                 }
                 else if(expr.id()==ID_smt2_symbol)
                 {
-                  irep_idt id=expr.get(ID_identifier);
-                  DATA_INVARIANT(!id.empty(), "smt2_symbol must have identifier");
+                  irep_idt id = to_smt2_symbol(expr).get_identifier();

Collaborator

tautschnig Sep 19, 2018

While at it: const irep_idt &id

src/solvers/smt2/smt2_conv.cpp Outdated

-                      assert(datatype_map.find(expr.type())!=datatype_map.end());
+                      INVARIANT(
+                        datatype_map.find(bitnot_expr.type()) != datatype_map.end(),
+                        "type shall have been mapped to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

Contributor Author

danpoe Sep 20, 2018 •

edited

Loading

Data types are currently only used when Z3 is used, but it now seems to be a standard SMTLIB feature. I've removed the invariants checking whether the element is in the map followed by a find() by a single call to at().

src/solvers/smt2/smt2_conv.cpp Outdated

-                    assert(datatype_map.find(type)!=datatype_map.end());
+                    INVARIANT(
+                      datatype_map.find(type) != datatype_map.end(),
+                      "type should have been mapped to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

src/solvers/smt2/smt2_conv.cpp Outdated

-                      assert(datatype_map.find(type)!=datatype_map.end());
+                      INVARIANT(
+                        datatype_map.find(type) != datatype_map.end(),
+                        "type should have been mapped to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

src/solvers/smt2/smt2_conv.cpp Outdated

-                    assert(datatype_map.find(type)!=datatype_map.end());
+                    INVARIANT(
+                      datatype_map.find(type) != datatype_map.end(),
+                      "type should have been converted to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

src/solvers/smt2/smt2_conv.cpp Outdated

-                    assert(datatype_map.find(type)!=datatype_map.end());
+                    INVARIANT(
+                      datatype_map.find(type) != datatype_map.end(),
+                      "type should have been converted to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

src/solvers/smt2/smt2_conv.cpp Outdated

-                    assert(datatype_map.find(type)!=datatype_map.end());
+                    INVARIANT(
+                      datatype_map.find(type) != datatype_map.end(),
+                      "type should have been converted to Z3 datatype");

Collaborator

tautschnig Sep 19, 2018

Z3?

tautschnig assigned danpoe

danpoe force-pushed the refactor/error-handling-solvers-smt2 branch 3 times, most recently from 244316c to b0f5db1 Compare

September 20, 2018 15:05

tautschnig mentioned this pull request

Adding extra information about invariant messages #2142

Merged

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

This PR failed Diffblue compatibility checks (cbmc commit: f88fcae).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85440531
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).

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

This PR failed Diffblue compatibility checks (cbmc commit: 244316c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85443417
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).

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

Passed Diffblue compatibility checks (cbmc commit: b0f5db1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85448831

danpoe added 4 commits

September 28, 2018 17:27


          Add functions to cast to sign_exprt

dd86120


          Improve numeric cast invariants

08347ed


          Error handling cleanup in solvers/smt2

d790011


          Refactor usage of datatype_map in smt2_conv.cpp

0f6b06c

danpoe force-pushed the refactor/error-handling-solvers-smt2 branch from b0f5db1 to 0f6b06c Compare

September 28, 2018 17:35

tautschnig approved these changes

View reviewed changes

tautschnig merged commit 762f505 into diffblue:develop

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

Passed Diffblue compatibility checks (cbmc commit: 0f6b06c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86324852

danpoe deleted the refactor/error-handling-solvers-smt2 branch

June 2, 2020 17:13

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

allredj allredj left review comments

tautschnig tautschnig approved these changes

kroening Awaiting requested review from kroening kroening is a code owner

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

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

pkesseli Awaiting requested review from pkesseli

smowton Awaiting requested review from smowton

Labels

None yet