__CPROVER_r_ok and __CPROVER_w_ok preconditions #2602

kroening · 2018-07-24T16:04:21Z

This adds support for two predicates, which are particularly suitable as preconditions for library models to ensure memory safety of client code.

smowton · 2018-07-25T16:07:50Z

Guessing this doesn't want a review just yet, please assign when it does

allredj

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

smowton

Couple of style nitpicks, and a proper concern: the conditions imposed appear to be redundant?

smowton · 2018-07-27T08:16:33Z

src/analyses/goto_check.cpp

+    std::string description;
+  };
+
+  using conditionst=std::list<conditiont>;


smowton · 2018-07-27T08:19:33Z

src/analyses/goto_check.cpp

+      alloc_disjuncts.push_back(and_exprt(lb_check, ub_check));
+    }
+
+    const exprt allocs=disjunction(alloc_disjuncts);


smowton · 2018-07-27T08:19:55Z

src/analyses/goto_check.cpp

+
+    const exprt allocs=disjunction(alloc_disjuncts);
+
+    if(flags.is_unknown() || flags.is_null())


Prefer braces round multi-line if (here and below)

smowton · 2018-07-27T08:23:30Z

src/analyses/goto_check.cpp

+
+    if(flags.is_unknown() || flags.is_null())
+      conditions.push_back(conditiont(
+        or_exprt(allocs, not_exprt(null_pointer(address))),


Surely "assert x in some alloc || x != null" is redundant, unless we want to handle weird systems where you can map the zero page?

Does allocs include mmio?

Yes, I did think about this. Yes, we may wish to be able to do MMIO on address zero.

allredj

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

tautschnig · 2018-07-30T14:38:26Z

src/ansi-c/c_typecheck_expr.cpp

@@ -2334,6 +2334,23 @@ exprt c_typecheck_baset::do_special_functions(

    return malloc_expr;
  }
+  else if(identifier==CPROVER_PREFIX "r_ok" ||


Nit pick: clang-format style spacing (across this commit)

tautschnig · 2018-07-30T14:39:48Z

src/util/irep_ids.def

@@ -691,6 +691,8 @@ IREP_ID_TWO(C_unnamed_object, #unnamed_object)
 IREP_ID_TWO(C_temporary_avoided, #temporary_avoided)
 IREP_ID_TWO(C_qualifier, #qualifier)
 IREP_ID_TWO(C_array_ini, #array_ini)
+IREP_ID_ONE(r_ok)


Randomly placing this here: this badly needs comments/documentation: the commit message has zero information, and RTFS doesn't help either as the front-end just quietly eats the functions but no semantics are ever provided.

tautschnig · 2018-07-30T17:27:32Z

I'm ok with this in principle, but it seems that at least one of the commits introduces regressions on selected tests. Once that's debugged it should be good to go.

allredj

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

kroening · 2018-07-30T19:17:22Z

The AWS CodeBuild windows failure is spurious (this time it's the choco server)

tautschnig · 2018-07-30T19:30:55Z

regression/cbmc/Function5/test.desc

@@ -3,6 +3,6 @@ main.c
 --pointer-check --bounds-check
 ^SIGNAL=0$
 ^EXIT=10$
-^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$
+^\[.*\] pointer outside object bounds in \*p: FAILURE$


I'm quite surprised to read a commit message saying "refactor ..." and then see user-visible output change. What is the rationale for this change? Could it please be communicated (at bare minimum via the commit message) as this will impact users? (For a start, the SV-COMP scripts will need to be updated.)

Ok, removed change to message

allredj

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

tautschnig

There are spurious failures in the Travis job, but adjusting the line length (see below) will trigger a re-run anyway.

tautschnig · 2018-07-30T21:53:22Z

src/analyses/goto_check.cpp


-    pointer_validity_check(deref, guard, member_offset, access_ub);
+      const exprt char_pointer =
+        typecast_exprt::conditional_cast(deref.pointer(), pointer_type(char_type()));


cpp-lint says this line is too long (82 chars).

allredj

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

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 added enhancement C Front End do not merge work in progress labels Jul 24, 2018

kroening requested review from tautschnig and peterschrammel July 24, 2018 16:04

kroening requested review from chrisr-diffblue, martin-cs, smowton and thk123 as code owners July 24, 2018 16:04

kroening force-pushed the __CPROVER_r/w_ok branch 4 times, most recently from 91aebe6 to ab0d7a9 Compare July 26, 2018 15:50

kroening removed do not merge work in progress labels Jul 26, 2018

kroening assigned smowton and tautschnig Jul 26, 2018

allredj reviewed Jul 26, 2018

View reviewed changes

smowton reviewed Jul 27, 2018

View reviewed changes

kroening force-pushed the __CPROVER_r/w_ok branch 2 times, most recently from 323859a to b07710a Compare July 27, 2018 12:22

allredj reviewed Jul 27, 2018

View reviewed changes

tautschnig reviewed Jul 30, 2018

View reviewed changes

kroening force-pushed the __CPROVER_r/w_ok branch 4 times, most recently from 7e0641f to 583db8b Compare July 30, 2018 17:08

kroening force-pushed the __CPROVER_r/w_ok branch 3 times, most recently from 1d945ec to 1310416 Compare July 30, 2018 18:05

Daniel Kroening added 2 commits July 30, 2018 19:06

__CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end

acfea65

expand __CPROVER_r/w_ok in goto_check

732ce2a

kroening force-pushed the __CPROVER_r/w_ok branch from 1310416 to 60abbf0 Compare July 30, 2018 18:06

use __CPROVER_r/w_ok in string.c library

4a24ad4

kroening force-pushed the __CPROVER_r/w_ok branch from 60abbf0 to ae10d17 Compare July 30, 2018 18:35

allredj reviewed Jul 30, 2018

View reviewed changes

tautschnig reviewed Jul 30, 2018

View reviewed changes

kroening force-pushed the __CPROVER_r/w_ok branch from ae10d17 to 4b5a7f0 Compare July 30, 2018 20:33

allredj reviewed Jul 30, 2018

View reviewed changes

tautschnig approved these changes Jul 30, 2018

View reviewed changes

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Jul 30, 2018

refactor pointer_validity_check using address_check

0202f34

kroening force-pushed the __CPROVER_r/w_ok branch from 4b5a7f0 to 0202f34 Compare July 31, 2018 07:02

allredj reviewed Jul 31, 2018

View reviewed changes

smowton approved these changes Jul 31, 2018

View reviewed changes

kroening merged commit da86bdb into develop Jul 31, 2018

kroening deleted the __CPROVER_r/w_ok branch July 31, 2018 09:50

qaphla mentioned this pull request Jul 31, 2018

Adds --expand-pointer-predicates to goto-instrument [depends-on: #3769, blocks #2706] #2644

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

__CPROVER_r_ok and __CPROVER_w_ok preconditions #2602

__CPROVER_r_ok and __CPROVER_w_ok preconditions #2602

kroening commented Jul 24, 2018

smowton commented Jul 25, 2018

allredj left a comment

smowton left a comment

smowton Jul 27, 2018

smowton Jul 27, 2018

smowton Jul 27, 2018

smowton Jul 27, 2018

peterschrammel Jul 27, 2018

kroening Jul 27, 2018

allredj left a comment

allredj left a comment

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig commented Jul 30, 2018

allredj left a comment

kroening commented Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

allredj left a comment

tautschnig left a comment

tautschnig Jul 30, 2018

allredj left a comment


		const exprt allocs=disjunction(alloc_disjuncts);

		if(flags.is_unknown() \|\| flags.is_null())

__CPROVER_r_ok and __CPROVER_w_ok preconditions #2602

__CPROVER_r_ok and __CPROVER_w_ok preconditions #2602

Conversation

kroening commented Jul 24, 2018

smowton commented Jul 25, 2018

allredj left a comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Jul 30, 2018

allredj left a comment

Choose a reason for hiding this comment

kroening commented Jul 30, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment