Move CPROVER_{r,w,rw}_ok processing to back-end #7395

tautschnig · 2022-11-28T12:24:13Z

Please review commit-by-commit.

Fixes #7377.

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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-11-28T13:39:16Z

Codecov Report

Patch coverage: 84.18% and project coverage change: +0.65% 🎉

Comparison is base (92581d1) 78.27% compared to head (e261217) 78.92%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7395      +/-   ##
===========================================
+ Coverage    78.27%   78.92%   +0.65%     
===========================================
  Files         1699     1700       +1     
  Lines       195410   195594     +184     
===========================================
+ Hits        152953   154370    +1417     
+ Misses       42457    41224    -1233

Files Changed	Coverage Δ
src/ansi-c/expr2c_class.h	`100.00% <ø> (ø)`
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`88.76% <0.00%> (-0.83%)`	⬇️
src/util/simplify_expr_class.h	`90.47% <ø> (ø)`
src/ansi-c/expr2c.cpp	`67.80% <53.57%> (-0.24%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`70.63% <76.92%> (-0.07%)`	⬇️
src/solvers/flattening/bv_pointers.cpp	`86.24% <83.33%> (-0.04%)`	⬇️
src/util/pointer_expr.h	`96.39% <84.84%> (-0.36%)`	⬇️
...ncremental/smt2_incremental_decision_procedure.cpp	`95.68% <92.30%> (-0.15%)`	⬇️
src/ansi-c/goto_check_c.cpp	`91.24% <100.00%> (-0.34%)`	⬇️
src/cbmc/cbmc_parse_options.cpp	`80.00% <100.00%> (+0.04%)`	⬆️
... and 9 more

... and 55 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

src/util/pointer_expr.cpp

src/util/pointer_expr.h

src/solvers/flattening/bv_pointers.cpp

src/solvers/smt2/smt2_conv.cpp

jimgrundy · 2022-12-08T15:05:13Z

Looks like we need to add __CPROVER_is_in_range to the mix

tautschnig · 2022-12-09T01:06:01Z

Looks like we need to add __CPROVER_is_in_range to the mix

This is done (including a few fixes specific to just that).

kroening · 2022-12-12T12:25:40Z

src/ansi-c/c_typecheck_expr.cpp

@@ -2684,8 +2683,15 @@ exprt c_typecheck_baset::do_special_functions(

    typecheck_function_call_arguments(expr);

+    symbol_exprt deallocated =
+      lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    symbol_exprt dead = lookup(CPROVER_PREFIX "dead_object").symbol_expr();


There's something wrong here. The connection to deallocated is very much a mechanism for implementing the predicate, and that shouldn't happen in the front-end.

Well, I really just moved (while also making it more obvious) something from goto_check_ct to type checking. Both of which are in the front-end...

Would it help if we lowered the side-effecty function to a predicate in the built-in library?
The C implementation of the function can refer to the global state to call the built-in predicate.

kroening

There's a fundamental architectural problem with this PR.
Just imagine you had to write an SMT-LIB standard proposal for a theory like this.

feliperodri · 2023-09-05T20:48:53Z

@NlightNFotis could you give a final look?

TGWDB · 2023-09-06T08:17:10Z

@NlightNFotis could you give a final look?

If you specifically want Fotis it will take a couple of weeks, but others here can take a look much sooner than that.

tautschnig · 2023-09-06T14:52:27Z

@NlightNFotis could you give a final look?

If you specifically want Fotis it will take a couple of weeks, but others here can take a look much sooner than that.

I believe I have addressed all of Fotis's comments, so it should likely be just any code owner for the incremental SMT2 back-end. Will update assignments accordingly.

thomasspriggs

Approving for the incremental SMT2 changes.

src/ansi-c/expr2c_class.h

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

The evaluation of these expressions depends on the specific values of __CPROVER_deallocated and __CPROVER_dead_object at the time the expression is used. Therefore, create new prophecy_* variants of these expressions to retain the properties expected of an expression (as opposed to a statement/function call). These prophecy_* expressions can safely be passed on to back-ends, be simplified, and do not need to be rewritten during instrumentation. For now, they are just handled by lowering the expressions (in the SAT and SMT back-ends). We may, in future, decide to have back-end specific (and possibly more efficient) handling of these.

These expressions are now rewritten to their prophecy_* counterparts by goto-program conversion, and back-ends directly handle these prophecy_* expressions. Unconditional rewrites by goto_check_ct (even when no checks are enabled) are no longer necessary. Fixes: diffblue#7377

This reverts selected changes from "r/w/rw_ok and pointer_in_range depend on deallocated and dead_object" for transformations of goto programs can now safely introduce rw_ok expressions into the goto program. Not all analyses, however, are able to cope with these expressions. Dependence graphs (and any analyses building upon these), for example, also require this rewriting. goto-instrument is adjusted accordingly.

martin-cs

I believe that the changes have been implemented correctly and do not raise any issues in the parts of the code that I am "owner" for.

I am as yet unsure why this is needed or why this is a good design to meet that need. However, judging by the comment history, this has been considered and it is something that I should resolve with a chat with @tautschnig rather than via github.

tautschnig · 2023-09-08T14:53:00Z

I am as yet unsure why this is needed or why this is a good design to meet that need. However, judging by the comment history, this has been considered and it is something that I should resolve with a chat with @tautschnig rather than via github.

Let me try to clarify publicly nonetheless (the why-is-this-needed part):

Not all middle-ends agree on how __CPROVER_{r,w,rw}_ok ought to be processed. Notably, the cprover tool has its own way of handling these. So we shouldn't prematurely expand them in the C front-end.
Early expansion leads to redundant checks, which result in a performance penalty. See Performance problem with --pointer-checks, --pointer-primitive-checks #7378 (and related issues linked from there).
In the status before the changes in this PR, this early expansion was necessary (as not all middle-ends were able to cope with these expressions), and this was silently done as part of the property instrumentation code (even when no property checks were requested). This is surprising behaviour.

tautschnig self-assigned this Nov 28, 2022

tautschnig added the work in progress label Nov 28, 2022

tautschnig mentioned this pull request Nov 28, 2022

Silent transformation of __CPROVER_{r,w,rw}_ok causing surprising behaviour #7377

Closed

remi-delmas-3000 reviewed Nov 28, 2022

View reviewed changes

src/util/pointer_expr.cpp Outdated Show resolved Hide resolved

remi-delmas-3000 mentioned this pull request Nov 28, 2022

Remove good_pointer, good_pointer_def #7386

Merged

3 tasks

remi-delmas-3000 reviewed Nov 28, 2022

View reviewed changes

src/util/pointer_expr.cpp Outdated Show resolved Hide resolved

src/util/pointer_expr.h Show resolved Hide resolved

src/solvers/flattening/bv_pointers.cpp Outdated Show resolved Hide resolved

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

remi-delmas-3000 mentioned this pull request Dec 7, 2022

CONTRACTS: Support bounded user defined memory-predicates #7401

Merged

7 tasks

tautschnig force-pushed the feature/rw_ok-back-end branch from fabc2a1 to 6e1c30e Compare December 9, 2022 01:05

tautschnig force-pushed the feature/rw_ok-back-end branch from 6e1c30e to e34dbee Compare December 9, 2022 16:00

tautschnig marked this pull request as ready for review December 9, 2022 16:01

tautschnig requested review from peterschrammel, thomasspriggs, NlightNFotis, TGWDB, chris-ryder, kroening, martin-cs and feliperodri as code owners December 9, 2022 16:01

tautschnig assigned kroening, remi-delmas-3000, peterschrammel, martin-cs and thomasspriggs and unassigned tautschnig Dec 9, 2022

tautschnig removed the work in progress label Dec 9, 2022

kroening reviewed Dec 12, 2022

View reviewed changes

kroening requested changes Dec 12, 2022

View reviewed changes

tautschnig force-pushed the feature/rw_ok-back-end branch from bfa3212 to d015c9d Compare August 23, 2023 10:54

tautschnig requested a review from esteffin as a code owner August 23, 2023 10:54

remi-delmas-3000 approved these changes Sep 5, 2023

View reviewed changes

feliperodri unassigned remi-delmas-3000 Sep 5, 2023

tautschnig assigned esteffin, thomasspriggs and TGWDB Sep 6, 2023

thomasspriggs approved these changes Sep 7, 2023

View reviewed changes

src/ansi-c/expr2c_class.h Outdated Show resolved Hide resolved

src/solvers/smt2_incremental/convert_expr_to_smt.cpp Outdated Show resolved Hide resolved

src/solvers/smt2_incremental/convert_expr_to_smt.cpp Outdated Show resolved Hide resolved

tautschnig force-pushed the feature/rw_ok-back-end branch from d015c9d to 6248e6e Compare September 7, 2023 11:05

tautschnig assigned peterschrammel and martin-cs and unassigned NlightNFotis, esteffin, thomasspriggs and TGWDB Sep 7, 2023

tautschnig added 3 commits September 7, 2023 11:43

tautschnig force-pushed the feature/rw_ok-back-end branch from 6248e6e to e261217 Compare September 7, 2023 11:43

martin-cs approved these changes Sep 8, 2023

View reviewed changes

tautschnig unassigned martin-cs Sep 8, 2023

peterschrammel approved these changes Sep 15, 2023

View reviewed changes

peterschrammel removed their assignment Sep 15, 2023

tautschnig merged commit f0fad5e into diffblue:develop Sep 15, 2023

tautschnig deleted the feature/rw_ok-back-end branch September 15, 2023 20:21

martin-cs mentioned this pull request Sep 18, 2023

__CPROVER_r/w_ok does not require null or a valid pointer #6416

Open

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Move CPROVER_{r,w,rw}_ok processing to back-end #7395

Move CPROVER_{r,w,rw}_ok processing to back-end #7395

tautschnig commented Nov 28, 2022 •

edited by feliperodri

Loading

codecov bot commented Nov 28, 2022 •

edited

Loading

jimgrundy commented Dec 8, 2022

tautschnig commented Dec 9, 2022

kroening Dec 12, 2022

tautschnig Dec 12, 2022

peterschrammel Dec 12, 2022

kroening left a comment

feliperodri commented Sep 5, 2023

TGWDB commented Sep 6, 2023

tautschnig commented Sep 6, 2023

thomasspriggs left a comment

martin-cs left a comment

tautschnig commented Sep 8, 2023

Move CPROVER_{r,w,rw}_ok processing to back-end #7395

Move CPROVER_{r,w,rw}_ok processing to back-end #7395

Conversation

tautschnig commented Nov 28, 2022 • edited by feliperodri Loading

codecov bot commented Nov 28, 2022 • edited Loading

Codecov Report

jimgrundy commented Dec 8, 2022

tautschnig commented Dec 9, 2022

kroening Dec 12, 2022

Choose a reason for hiding this comment

tautschnig Dec 12, 2022

Choose a reason for hiding this comment

peterschrammel Dec 12, 2022

Choose a reason for hiding this comment

kroening left a comment

Choose a reason for hiding this comment

feliperodri commented Sep 5, 2023

TGWDB commented Sep 6, 2023

tautschnig commented Sep 6, 2023

thomasspriggs left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

tautschnig commented Sep 8, 2023

tautschnig commented Nov 28, 2022 •

edited by feliperodri

Loading

codecov bot commented Nov 28, 2022 •

edited

Loading