Fix a crash during SMT translation of structs #5904

SaswatPadhi · 2021-03-09T20:21:23Z

This PR fixes a bug with SMT translation of structs using data types (not bit vectors). CBMC --smt2 --z3 was crashing on the attached regression test with a key not found exception from a map::at call.

Each commit message has a non-empty body, explaining why the change was made.
NA ~~Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.~~
NA ~~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).
NA ~~My commit message includes data points confirming performance improvements (if claimed).~~
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-03-09T21:31:07Z

Codecov Report

Merging #5904 (c2ec649) into develop (e76d811) will increase coverage by 0.02%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5904      +/-   ##
===========================================
+ Coverage    75.12%   75.14%   +0.02%     
===========================================
  Files         1435     1435              
  Lines       156301   156303       +2     
===========================================
+ Hits        117416   117455      +39     
+ Misses       38885    38848      -37

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/solvers/smt2/smt2_conv.cpp	`60.86% <100.00%> (+1.47%)`	⬆️

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 2f7dcb5...c2ec649. Read the comment docs.

martin-cs

Please can you reformat this a little to fix with current conventions.

regression/cbmc-smt2-z3/Makefile

regression/cbmc-smt2-z3/struct/test.desc

kroening · 2021-03-10T10:05:41Z

Should there be a similar change for union_tags?

SaswatPadhi · 2021-03-10T16:10:50Z

Should there be a similar change for union_tags?

Unions are currently not encoded using data types in SMT, so this particular issue doesn't appear with unions.

But I haven't checked if we would have a similar issue with non-DT encoding of unions and structs. We do something similar for bit vector encodings -- instead of looking up the datatype_map, we look up boolbv_width of the type. I will check this and create a separate PR to fix the BV encoding, if needed.

SaswatPadhi · 2021-03-10T17:28:28Z

I think the test is failing in CI because it cannot find z3.

Is there a way we can just test the SMT constraint generation with data types enabled, without actually solving them using z3? Alternatively, we can install z3 on our CI :)

thomasspriggs · 2021-03-12T10:41:11Z

I think the test is failing in CI because it cannot find z3.

Is there a way we can just test the SMT constraint generation with data types enabled, without actually solving them using z3? Alternatively, we can install z3 on our CI :)

It seems reasonable to install an SMT solver in CI in order to test the SMT output properly. Just so long as we don't end up giving it anything to solve which inflates the overall run time too much. @diffblue/diffblue-opensource What do the rest of you think?

Please note that I haven't reviewed the rest of this PR, I am just trying to help with this particular issue.

SaswatPadhi · 2021-03-12T21:04:10Z

Thanks @thomasspriggs.

@martin-cs I think I have addressed your comment regarding conventions. There is one remaining issue with smt-backend tag which I have described above. Could you please take another look?

thomasspriggs

The fix appears reasonable to me. But we need get the test to run and pass in CI, before I will be happy to approve. This so that the additional CI related changes can be reviewed and approved before merging.

src/solvers/smt2/smt2_conv.cpp

regression/cbmc/struct15/test.desc

SaswatPadhi · 2021-03-21T23:56:57Z

Blocked on #5949.

thomasspriggs · 2021-03-22T11:13:07Z

Blocked on #5949.

I only raised that PR to run CI, it is in Draft status and the work in known to be incomplete. We are currently giving higher priority to other pieces of work. It could be a week or so, before we come back to those CI changes. Is that going to be a problem for you?

SaswatPadhi · 2021-03-22T13:36:21Z

Hi @thomasspriggs,

No problem. I was going through all of my PRs and rebased some of them with develop. This is just a note to myself. I have things running locally for demos etc. so this is not a high priority for now.

Thanks.

martin-cs

Looks good; thanks.

regression/cbmc/struct15/test.desc

This commit fixes a `key not found` exception in `convert_type` during SMT2 encoding of structs using data types. Although structs were being mapped to SMT2 datatypes (in `datatype_map`) struct_tags were not.

SaswatPadhi requested review from allredj, kroening, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners March 9, 2021 20:21

feliperodri assigned SaswatPadhi Mar 9, 2021

feliperodri added the aws Bugs or features of importance to AWS CBMC users label Mar 9, 2021

SaswatPadhi force-pushed the smt_struct_fix branch from 19b2cae to 42a448a Compare March 9, 2021 20:23

martin-cs requested changes Mar 9, 2021

View reviewed changes

regression/cbmc-smt2-z3/Makefile Outdated Show resolved Hide resolved

regression/cbmc-smt2-z3/struct/test.desc Outdated Show resolved Hide resolved

SaswatPadhi force-pushed the smt_struct_fix branch 3 times, most recently from 7442aa6 to 5c0a2ca Compare March 10, 2021 17:00

thomasspriggs mentioned this pull request Mar 16, 2021

Add z3 package installation to CI pull request checks #5944

Merged

7 tasks

thomasspriggs reviewed Mar 17, 2021

View reviewed changes

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

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

regression/cbmc/struct15/test.desc Show resolved Hide resolved

SaswatPadhi force-pushed the smt_struct_fix branch 2 times, most recently from f6001d7 to dec30a2 Compare March 17, 2021 20:08

SaswatPadhi changed the title ~~Fixes a crash in SMT translation of structs~~ Fix a crash in SMT translation of structs Mar 18, 2021

thomasspriggs mentioned this pull request Mar 18, 2021

CBMC 5.12 crashes on converting structs to SMT2 #5297

Closed

SaswatPadhi mentioned this pull request Mar 20, 2021

Initialization of a flexible array member leads to cbmc crash or verification failure. #4206

Closed

SaswatPadhi force-pushed the smt_struct_fix branch from dec30a2 to c982bb3 Compare March 22, 2021 23:35

SaswatPadhi force-pushed the smt_struct_fix branch from c982bb3 to bd3715f Compare March 25, 2021 00:53

martin-cs approved these changes Mar 25, 2021

View reviewed changes

peterschrammel reviewed Mar 25, 2021

View reviewed changes

regression/cbmc/struct15/test.desc Outdated Show resolved Hide resolved

SaswatPadhi added bugfix SMT Backend Interface labels Mar 29, 2021

SaswatPadhi force-pushed the smt_struct_fix branch from bd3715f to 2dfea99 Compare March 29, 2021 14:44

thomasspriggs mentioned this pull request Mar 31, 2021

Fix z3 installation on PR CI jobs #5983

Merged

7 tasks

Fix SMT2 DT encoding of structs

c2ec649

This commit fixes a `key not found` exception in `convert_type` during SMT2 encoding of structs using data types. Although structs were being mapped to SMT2 datatypes (in `datatype_map`) struct_tags were not.

SaswatPadhi force-pushed the smt_struct_fix branch from 2dfea99 to c2ec649 Compare March 31, 2021 14:10

SaswatPadhi changed the title ~~Fix a crash in SMT translation of structs~~ Fix a crash during SMT translation of structs Mar 31, 2021

SaswatPadhi merged commit e42cc6c into diffblue:develop Mar 31, 2021

SaswatPadhi deleted the smt_struct_fix branch March 31, 2021 17:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix a crash during SMT translation of structs #5904

Fix a crash during SMT translation of structs #5904

SaswatPadhi commented Mar 9, 2021 •

edited

Loading

codecov bot commented Mar 9, 2021 •

edited

Loading

martin-cs left a comment

kroening commented Mar 10, 2021

SaswatPadhi commented Mar 10, 2021

SaswatPadhi commented Mar 10, 2021 •

edited

Loading

thomasspriggs commented Mar 12, 2021

SaswatPadhi commented Mar 12, 2021

thomasspriggs left a comment

SaswatPadhi commented Mar 21, 2021

thomasspriggs commented Mar 22, 2021

SaswatPadhi commented Mar 22, 2021

martin-cs left a comment

Fix a crash during SMT translation of structs #5904

Fix a crash during SMT translation of structs #5904

Conversation

SaswatPadhi commented Mar 9, 2021 • edited Loading

codecov bot commented Mar 9, 2021 • edited Loading

Codecov Report

martin-cs left a comment

Choose a reason for hiding this comment

kroening commented Mar 10, 2021

SaswatPadhi commented Mar 10, 2021

SaswatPadhi commented Mar 10, 2021 • edited Loading

thomasspriggs commented Mar 12, 2021

SaswatPadhi commented Mar 12, 2021

thomasspriggs left a comment

Choose a reason for hiding this comment

SaswatPadhi commented Mar 21, 2021

thomasspriggs commented Mar 22, 2021

SaswatPadhi commented Mar 22, 2021

martin-cs left a comment

Choose a reason for hiding this comment

SaswatPadhi commented Mar 9, 2021 •

edited

Loading

codecov bot commented Mar 9, 2021 •

edited

Loading

SaswatPadhi commented Mar 10, 2021 •

edited

Loading