fix flattening of ID_invalid_pointer #2630

kroening · 2018-07-28T20:48:57Z

This fixes an inconsistency between the SMT2 encoding and the simplifier on one hand, and the bit-level flattening on the other: NULL is not considered invalid.

allredj

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

smowton

Might be worth cleaning up language, otherwise does what it says on the tin (though I'm not familiar enough to quickly know if there are other corresponding changes that would be needed)

smowton · 2018-07-30T14:51:06Z

src/analyses/goto_check.cpp

@@ -991,7 +991,8 @@ void goto_checkt::pointer_validity_check(
      allocs=disjunction(disjuncts);
    }

-    if(flags.is_unknown() || flags.is_null())
+    if(flags.is_unknown() ||


Point of curiosity: all of these is_ tests are may_be_ tests, right?

Yes, indeed.

tautschnig

With the combination of changes I'm finding it hard to see whether the change that the commit message talks about is actually being tested in any way. Please break apart the changes into separate commits.

tautschnig · 2018-07-30T16:55:06Z

regression/cbmc/Malloc23/test.desc

@@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
 pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
-\*\* 4 of 36 failed 
+\*\* 4 of .* failed 


Not a big deal (and obviously similar changes happened elsewhere): could this please be [0-9]+ instead of .*?

tautschnig · 2018-07-30T16:56:03Z

regression/cbmc/memory_allocation1/test.desc

-\[main.assertion.1\] assertion \*p==42: SUCCESS
-\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
-\[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
+^\[main\.pointer_dereference\.2\] dereference failure: invalid integer address in \*p: SUCCESS$


Huh? I'm finding it hard to reconcile this with the commit message.

tautschnig · 2018-07-30T16:58:47Z

src/analyses/goto_check.cpp

+        expr.find_source_location(),
+        expr,
+        guard);
+    }


I suppose this change and what I mourned above just need to be moved into a separate commit.

allredj

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

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

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a

kroening assigned tautschnig Jul 28, 2018

kroening requested a review from tautschnig July 28, 2018 20:48

kroening requested review from martin-cs and peterschrammel as code owners July 28, 2018 20:48

kroening added Solvers bugfix labels Jul 28, 2018

kroening force-pushed the invalid-pointer-flattening branch from 0bbc729 to e40e87c Compare July 29, 2018 09:56

allredj reviewed Jul 29, 2018

View reviewed changes

kroening force-pushed the invalid-pointer-flattening branch from e40e87c to f98842a Compare July 30, 2018 14:46

kroening requested review from chrisr-diffblue, smowton and thk123 as code owners July 30, 2018 14:46

smowton approved these changes Jul 30, 2018

View reviewed changes

kroening force-pushed the invalid-pointer-flattening branch 2 times, most recently from dce6c8b to ea1a244 Compare July 30, 2018 16:46

tautschnig reviewed Jul 30, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Jul 30, 2018

Daniel Kroening added 2 commits July 30, 2018 18:12

fix flattening of ID_invalid_pointer

9b5847e

separate pointer check for integer addresses

060b59c

kroening force-pushed the invalid-pointer-flattening branch from ea1a244 to 060b59c Compare July 30, 2018 17:13

allredj reviewed Jul 30, 2018

View reviewed changes

tautschnig approved these changes Jul 30, 2018

View reviewed changes

allredj reviewed Jul 30, 2018

View reviewed changes

kroening merged commit 44ef8d5 into develop Jul 30, 2018

kroening deleted the invalid-pointer-flattening branch July 30, 2018 17:52

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix flattening of ID_invalid_pointer #2630

fix flattening of ID_invalid_pointer #2630

kroening commented Jul 28, 2018

allredj left a comment

smowton left a comment

smowton Jul 30, 2018

kroening Jul 30, 2018

tautschnig left a comment

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

allredj left a comment

allredj left a comment

fix flattening of ID_invalid_pointer #2630

fix flattening of ID_invalid_pointer #2630

Conversation

kroening commented Jul 28, 2018

allredj left a comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

smowton Jul 30, 2018

Choose a reason for hiding this comment

kroening Jul 30, 2018

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Jul 30, 2018

Choose a reason for hiding this comment

kroening Jul 30, 2018

Choose a reason for hiding this comment

tautschnig Jul 30, 2018

Choose a reason for hiding this comment

tautschnig Jul 30, 2018

Choose a reason for hiding this comment

kroening Jul 30, 2018

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment