Stop asserting positive array size #4928

xbauch · 2019-07-19T13:46:12Z

when generating non-deterministic arrays. Zero-sized arrays are (unfortunately)
legal C construct (as for example the regression test shows).

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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).
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.

hannes-steffenhagen-diffblue · 2019-07-19T13:48:04Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -163,7 +163,6 @@ void symbol_factoryt::gen_nondet_array_init(
  const auto &size = array_type.size();
  PRECONDITION(size.id() == ID_constant);
  auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
-  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");


I wasn't properly taking this situation into account when writing this.

allredj

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

codecov-io · 2019-07-19T15:57:36Z

Codecov Report

Merging #4928 into develop will decrease coverage by 0.09%.
The diff coverage is 57.14%.

@@            Coverage Diff             @@
##           develop    #4928     +/-   ##
==========================================
- Coverage    69.29%    69.2%   -0.1%     
==========================================
  Files         1306     1307      +1     
  Lines       108263   108058    -205     
==========================================
- Hits         75023    74777    -246     
- Misses       33240    33281     +41

Impacted Files	Coverage Δ
src/ansi-c/c_nondet_symbol_factory.cpp	`100% <ø> (ø)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`60.03% <57.14%> (+0.44%)`	⬆️
src/statement-list/statement_list_typecheck.cpp	`63.35% <0%> (-10.99%)`	⬇️
...olvers/strings/string_constraint_instantiation.cpp	`90.1% <0%> (-3.3%)`	⬇️
src/util/format_expr.cpp	`72.18% <0%> (-3.01%)`	⬇️
src/goto-symex/renaming_level.cpp	`92.53% <0%> (-2.52%)`	⬇️
src/statement-list/parser.y	`89.66% <0%> (-1.48%)`	⬇️
src/cpp/cpp_declarator_converter.cpp	`76.06% <0%> (-0.99%)`	⬇️
jbmc/src/java_bytecode/java_bytecode_parser.cpp	`89.59% <0%> (-0.98%)`	⬇️
src/pointer-analysis/value_set_fi.cpp	`58.42% <0%> (-0.88%)`	⬇️
... and 47 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 9643ec2...30923ab. Read the comment docs.

allredj

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

when generating non-deterministic arrays. Zero-sized arrays are (unfortunately) legal C construct (as for example the regression test shows).

allredj

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

kroening · 2019-07-25T12:58:14Z

src/solvers/smt2/smt2_conv.cpp

-  CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
-
+  if(size == 0)
+    return;


This is suspicious -- this produces an SMT file that might now parse.
Did you want to make that a precondition, and then check at the call site?

I reverted here to the original CHECK_RETURN and pushed the check to the above convert_struct.

kroening

The SMT-Lib2 file would not parse!

xbauch · 2019-07-25T13:48:47Z

The SMT-Lib2 file would not parse!

It should now (I had to fix another, seemingly unrelated, bug in the last commit). I added a test that runs --smt2.

xbauch · 2019-07-25T13:55:15Z

src/solvers/smt2/smt2_conv.cpp

+        {
+          const array_typet &array_type = to_array_type(op.type());
+          const auto &size_expr = array_type.size();
+          PRECONDITION(size_expr.id() == ID_constant);


Not really a precondition, check-return?

smowton

Looks sensible

when converting to SMT2 queries.

xbauch · 2019-07-30T09:01:33Z

@kroening --smt2 test removed (z3 is unavailable on CI).

allredj

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

tautschnig · 2019-08-05T10:11:08Z

@kroening ?

kroening · 2019-08-05T14:29:14Z

src/solvers/smt2/smt2_conv.cpp

+          const array_typet &array_type = to_array_type(op.type());
+          const auto &size_expr = array_type.size();
+          CHECK_RETURN(size_expr.id() == ID_constant);
+


This prevents using arrays with variable size.

kroening · 2019-08-05T14:29:53Z

src/solvers/smt2/smt2_conv.cpp

+
+          if(numeric_cast_v<mp_integer>(to_constant_expr(size_expr)) != 0)
+            flatten_array(op);
+        }


In principle, this check would now need to be done in front of every call to flatten array, to make that a precondition of that function.
I think this is the wrong approach. I would let flatten_array handle this case.

NlightNFotis · 2022-03-15T15:56:25Z

@kroening Is this something that has value, and we should rework to get in develop?

Or has this been sunset on the basis of other changes (I can see there are merge conflicts).

I'm inclined to believe that there's not a lot of enthusiasm for this to get in (given that the last update on this was on 2019) but figured I should ask before I close the PR.

kroening · 2022-03-15T16:34:02Z

It certainly makes sense to systematically check that we can do zero-sized arrays with all the solver back-ends.

The PR itself is not quite done yet, and would need a bit of work.

xbauch requested review from kroening and tautschnig as code owners July 19, 2019 13:46

hannes-steffenhagen-diffblue approved these changes Jul 19, 2019

View reviewed changes

xbauch requested review from allredj, martin-cs, peterschrammel and romainbrenguier as code owners July 19, 2019 15:01

allredj reviewed Jul 19, 2019

View reviewed changes

xbauch force-pushed the fix/zero-size-array-init branch 3 times, most recently from 8cb270e to 6fd4b0e Compare July 22, 2019 09:28

allredj reviewed Jul 22, 2019

View reviewed changes

Stop asserting positive array size

f585e60

when generating non-deterministic arrays. Zero-sized arrays are (unfortunately) legal C construct (as for example the regression test shows).

xbauch force-pushed the fix/zero-size-array-init branch from 6fd4b0e to 80b914e Compare July 22, 2019 09:39

allredj reviewed Jul 22, 2019

View reviewed changes

kroening reviewed Jul 25, 2019

View reviewed changes

kroening requested changes Jul 25, 2019

View reviewed changes

xbauch commented Jul 25, 2019

View reviewed changes

xbauch requested review from chrisr-diffblue and smowton as code owners July 25, 2019 14:25

xbauch force-pushed the fix/zero-size-array-init branch from df3f3b7 to fbd8e10 Compare July 25, 2019 14:36

smowton approved these changes Jul 25, 2019

View reviewed changes

xbauch force-pushed the fix/zero-size-array-init branch from fbd8e10 to 4a28b11 Compare July 25, 2019 14:57

xbauch requested a review from thk123 as a code owner July 25, 2019 14:57

xbauch force-pushed the fix/zero-size-array-init branch from 4a28b11 to bc5d042 Compare July 30, 2019 08:53

Also skip flattening zero-sized arrays

30923ab

when converting to SMT2 queries.

xbauch force-pushed the fix/zero-size-array-init branch from bc5d042 to 30923ab Compare July 30, 2019 08:58

allredj reviewed Jul 30, 2019

View reviewed changes

tautschnig assigned kroening Aug 5, 2019

tautschnig added the bugfix label Aug 5, 2019

kroening reviewed Aug 5, 2019

View reviewed changes

tautschnig mentioned this pull request Sep 22, 2022

gen_nondet_array_init: arrays may have size 0 #5342

Open

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Stop asserting positive array size #4928

Stop asserting positive array size #4928

xbauch commented Jul 19, 2019

hannes-steffenhagen-diffblue Jul 19, 2019

allredj left a comment

codecov-io commented Jul 19, 2019 •

edited

Loading

allredj left a comment

allredj left a comment

kroening Jul 25, 2019

xbauch Jul 25, 2019

kroening left a comment

xbauch commented Jul 25, 2019

xbauch Jul 25, 2019

smowton left a comment

xbauch commented Jul 30, 2019

allredj left a comment

tautschnig commented Aug 5, 2019

kroening Aug 5, 2019

kroening Aug 5, 2019

NlightNFotis commented Mar 15, 2022

kroening commented Mar 15, 2022

Stop asserting positive array size #4928

Are you sure you want to change the base?

Stop asserting positive array size #4928

Conversation

xbauch commented Jul 19, 2019

hannes-steffenhagen-diffblue Jul 19, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

codecov-io commented Jul 19, 2019 • edited Loading

Codecov Report

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

kroening Jul 25, 2019

Choose a reason for hiding this comment

xbauch Jul 25, 2019

Choose a reason for hiding this comment

kroening left a comment

Choose a reason for hiding this comment

xbauch commented Jul 25, 2019

xbauch Jul 25, 2019

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

xbauch commented Jul 30, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Aug 5, 2019

kroening Aug 5, 2019

Choose a reason for hiding this comment

kroening Aug 5, 2019

Choose a reason for hiding this comment

NlightNFotis commented Mar 15, 2022

kroening commented Mar 15, 2022

codecov-io commented Jul 19, 2019 •

edited

Loading