Fix cbmc crash on pointer checks of void pointer dereferences #5427

danpoe · 2020-07-20T08:15:19Z

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.

codecov · 2020-07-20T09:28:41Z

Codecov Report

Merging #5427 into develop will decrease coverage by 1.88%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5427      +/-   ##
===========================================
- Coverage    68.21%   66.32%   -1.89%     
===========================================
  Files         1178     1171       -7     
  Lines        97542    96461    -1081     
===========================================
- Hits         66537    63980    -2557     
- Misses       31005    32481    +1476

Flag	Coverage Δ
#cproversmt2	`42.76% <100.00%> (+<0.01%)`	⬆️
#regression	`65.38% <100.00%> (+<0.01%)`	⬆️
#unit	`?`

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	`81.65% <100.00%> (+0.07%)`	⬆️
src/util/freer.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/bdd/bdd_miniBDD.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/bdd/miniBDD/miniBDD.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/bdd/miniBDD/miniBDD.inc	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-programs/restrict_function_pointers.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/prop/bdd_expr.cpp	`0.00% <0.00%> (-91.79%)`	⬇️
src/util/invariant.h	`3.12% <0.00%> (-74.02%)`	⬇️
src/util/invariant.cpp	`0.00% <0.00%> (-73.69%)`	⬇️
src/solvers/floatbv/float_approximation.cpp	`0.00% <0.00%> (-73.08%)`	⬇️
... and 144 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 069db73...b8f6483. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-07-20T10:07:31Z

src/analyses/goto_check.cpp

-  auto conditions = address_check(pointer, size_of_expr_opt.value());
+  if(expr.type().id() == ID_empty)
+  {
+    size = from_integer(1, size_type());


Should we change size_of_expr to return 1 here instead?

Not sure. There are quite a number of uses in the codebase that check that the return value of size_of_expr() is not empty, and if it is throw an exception or have some other handling. Probably we should review those at some point, though that's out of scope of this PR.

Is the purpose of this to create an address check that fails?

No the address check should succeed. Basically *p with p being a pointer to void is valid as long as p points to valid memory, though then using the value would be undefined behavior.

Please explain the magic 1 in a comment.

peterschrammel · 2020-07-20T08:16:50Z

regression/cbmc/void_pointer6/test.desc

+CORE
+main.c
+--pointer-check
+^EXIT=10$


verification failed?

Not necessary I think as EXIT=10 already indicates that cbmc exited without error and verification failed.

peterschrammel · 2020-07-20T11:28:06Z

src/analyses/goto_check.cpp

-  auto conditions = address_check(pointer, size_of_expr_opt.value());
+  if(expr.type().id() == ID_empty)
+  {
+    size = from_integer(1, size_type());


Is the purpose of this to create an address check that fails?

peterschrammel · 2020-07-21T16:15:10Z

src/analyses/goto_check.cpp

-  auto conditions = address_check(pointer, size_of_expr_opt.value());
+  if(expr.type().id() == ID_empty)
+  {
+    size = from_integer(1, size_type());


Please explain the magic 1 in a comment.

danpoe requested review from chrisr-diffblue, martin-cs, peterschrammel and smowton as code owners July 20, 2020 08:15

hannes-steffenhagen-diffblue reviewed Jul 20, 2020

View reviewed changes

peterschrammel reviewed Jul 20, 2020

View reviewed changes

peterschrammel approved these changes Jul 21, 2020

View reviewed changes

Fix cbmc crash on pointer checks of void pointer dereferences

b8f6483

danpoe force-pushed the fixes/pointer-validity-check-void-dereference branch from 41fe04c to b8f6483 Compare July 21, 2020 16:51

danpoe merged commit a743af3 into diffblue:develop Jul 21, 2020

This was referenced Apr 16, 2021

Void pointer argument cannot be pointer-checked #4930

Closed

Stop assertion size-of-expr for pointer-checks #4936

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fix cbmc crash on pointer checks of void pointer dereferences #5427

Fix cbmc crash on pointer checks of void pointer dereferences #5427

Uh oh!

danpoe commented Jul 20, 2020 •

edited

Loading

Uh oh!

codecov bot commented Jul 20, 2020 •

edited

Loading

Uh oh!

hannes-steffenhagen-diffblue Jul 20, 2020

Uh oh!

danpoe Jul 20, 2020 •

edited

Loading

Uh oh!

peterschrammel Jul 20, 2020

Uh oh!

danpoe Jul 20, 2020

Uh oh!

peterschrammel Jul 21, 2020

Uh oh!

peterschrammel Jul 20, 2020

Uh oh!

danpoe Jul 21, 2020

Uh oh!

peterschrammel Jul 20, 2020

Uh oh!

peterschrammel Jul 21, 2020

Uh oh!

Uh oh!

Fix cbmc crash on pointer checks of void pointer dereferences #5427

Fix cbmc crash on pointer checks of void pointer dereferences #5427

Uh oh!

Conversation

danpoe commented Jul 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jul 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe Jul 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Jul 20, 2020 •

edited

Loading

codecov bot commented Jul 20, 2020 •

edited

Loading

danpoe Jul 20, 2020 •

edited

Loading