Conversion of `pointer_object_exprt` and `pointer_offset_exprt` for new SMT backend #6815

NlightNFotis · 2022-04-19T09:38:44Z

This PR adds the implementation (along with unit and regression tests)
for the conversion of pointer_object_exprts and pointer_offset_exprts for the new SMT backend.

(Because of some limitations for now in our support for arrays, pointer arithmetic, pointer_offset_exprts are covered by unit tests only)

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.

TGWDB · 2022-04-19T09:45:33Z

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

+{
+  // Prelude similar to the one used for address-of expression conversion.
+
+  // The config lines are necessary to ensure that pointer width in configured.


Looks like this still needs fixing.

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

src/solvers/smt2_incremental/object_tracking.cpp

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-04-19T11:30:44Z

The SAT back end can produce a counter example for the following input. Whereas the SMT back end in your branch cannot -

#include <assert.h>
#include <stdbool.h>

int main()
{
	int x;
	int y;
	int z;
	bool nondet1;
	bool nondet2;
	int *a = nondet1 ? &x : &y;
	int *b = nondet2 ? &y : &z;
	__CPROVER_assert(!__CPROVER_same_object(a, b), "Can be violated.");
}

codecov · 2022-04-20T09:18:05Z

Codecov Report

Merging #6815 (eaea1de) into develop (7e785d0) will increase coverage by 0.01%.
The diff coverage is 88.56%.

❗ Current head eaea1de differs from pull request most recent head e5f91f2. Consider uploading reports for the commit e5f91f2 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6815      +/-   ##
===========================================
+ Coverage    77.03%   77.04%   +0.01%     
===========================================
  Files         1594     1594              
  Lines       185011   185276     +265     
===========================================
+ Hits        142514   142748     +234     
- Misses       42497    42528      +31

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_convert_type.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_code.cpp	`77.15% <43.75%> (-2.89%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`94.42% <93.47%> (-0.07%)`	⬇️
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`85.31% <96.96%> (+0.77%)`	⬆️
src/ansi-c/ansi_c_convert_type.cpp	`80.69% <100.00%> (+0.55%)`	⬆️
src/ansi-c/c_expr.h	`100.00% <100.00%> (ø)`
src/ansi-c/c_typecheck_base.cpp	`78.88% <100.00%> (+0.55%)`	⬆️
src/ansi-c/parser.y	`80.22% <100.00%> (+0.18%)`	⬆️
... and 9 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 142db0b...e5f91f2. Read the comment docs.

regression/cbmc-incr-smt2/pointers/pointers_simple.c

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-04-20T19:17:03Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+    smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
+  if(pointer_width > offset_bits)
+  {
+    return smt_bit_vector_theoryt::zero_extend(pointer_width - offset_bits)(


🤔 The result type of pointer_offset_exprt is usually signed. Therefore we should probably be using sign_extend instead of zero_extend. Note that the old SMT2 back end may may wrong in this case. Note also that the signed-ness is currently set in pointer_predicates.cpp but we have no guarantees that these expressions will always have signed/unsigned results (unless we add appropriate invariants).
ℹ️ Negative offsets may occur in the the case of pointer offset overflows.

thomasspriggs · 2022-04-20T19:20:20Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+  const auto converted_expr = converted.at(pointer_expr);
+  const std::size_t pointer_width = type->get_width();
+  std::size_t offset_bits = pointer_width - config.bv_encoding.object_bits;
+  if(offset_bits > pointer_width)


⛏️ Are we actually truncating the result in this case? Might be worth adding a comment to that effect as this is slightly surprising and it might be worth just adding an invariant to avoid surprise truncation instead.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

…tegers.

thomasspriggs · 2022-04-28T16:34:38Z

regression/cbmc-incr-smt2/pointers/pointer_offset.c

+
+  // *q = p + 2;
+
+  // __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), "expected failure");


⛏️ This assertion looks like it should pass once we have support for integer arithmetic. The assignment above will give q an offset of 2 * sizeof(int) and p will still have an offset of zero.

NlightNFotis requested a review from peterschrammel as a code owner April 19, 2022 09:38

NlightNFotis self-assigned this Apr 19, 2022

NlightNFotis requested review from TGWDB, chris-ryder and thomasspriggs as code owners April 19, 2022 09:38

TGWDB approved these changes Apr 19, 2022

View reviewed changes

thomasspriggs suggested changes Apr 19, 2022

View reviewed changes

NlightNFotis force-pushed the pointer_objects_smt branch 5 times, most recently from 4a49085 to 0685591 Compare April 20, 2022 08:43

NlightNFotis changed the title ~~Conversion of pointer_object_exprt for new SMT backend~~ Conversion of pointer_object_exprt and pointer_offset_exprt for new SMT backend Apr 20, 2022

NlightNFotis force-pushed the pointer_objects_smt branch from 0685591 to 0e33060 Compare April 20, 2022 08:49

thomasspriggs suggested changes Apr 20, 2022

View reviewed changes

NlightNFotis force-pushed the pointer_objects_smt branch 2 times, most recently from 7b0b681 to 71ad410 Compare April 28, 2022 10:45

Add extra test for address-of objects and pointer dereferencing to in…

074d3be

…tegers.

NlightNFotis force-pushed the pointer_objects_smt branch from 71ad410 to eaea1de Compare April 28, 2022 15:48

NlightNFotis and others added 7 commits April 28, 2022 16:51

Add conversion of pointer_object_exprt and a regression test for that.

15423e3

Add unit tests for pointer object expression conversion

f02ee6a

Add an extra test to the regression test suite, suggested by Thomas S.

d4d3aa1

Convert pointer_offset_exprt to SMT

061ce17

Add unit tests for conversion of pointer_offset_exprt to SMT

ac0bb15

Add regression test using __CPROVER_POINTER_OBJECT directly

e2dca8a

Add regression test for __CPROVER_POINTER_OFFSET

e5f91f2

NlightNFotis force-pushed the pointer_objects_smt branch from eaea1de to e5f91f2 Compare April 28, 2022 15:51

thomasspriggs reviewed Apr 28, 2022

View reviewed changes

thomasspriggs approved these changes Apr 28, 2022

View reviewed changes

NlightNFotis merged commit da7edc5 into diffblue:develop Apr 28, 2022

NlightNFotis deleted the pointer_objects_smt branch April 28, 2022 17:46


		// *q = p + 2;

		// __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), "expected failure");

Conversion of pointer_object_exprt and pointer_offset_exprt for new SMT backend #6815

Conversion of pointer_object_exprt and pointer_offset_exprt for new SMT backend #6815

Uh oh!

Conversation

NlightNFotis commented Apr 19, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TGWDB Apr 19, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Apr 28, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs commented Apr 19, 2022

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Apr 20, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Apr 20, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Apr 28, 2022

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversion of `pointer_object_exprt` and `pointer_offset_exprt` for new SMT backend #6815

Conversion of `pointer_object_exprt` and `pointer_offset_exprt` for new SMT backend #6815

NlightNFotis commented Apr 19, 2022 •

edited

Loading

codecov bot commented Apr 20, 2022 •

edited

Loading