Relational operators support for pointers in new SMT backend

[NlightNFotis]

This PR is adding support for relational operators as applied
to pointers in the new SMT backend.

• 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.

[kroening]

Please revise these tests -- relations on nondeterministic pointers have no meaning. You need to make those pointers point to the same object.

[NlightNFotis]

Hi Daniel, do the changes in 36e0955 look like an acceptable fix to this?

[kroening]

Yes, that's fine. It may confuse one or the other reader that you are using x both as a source of nondeterminism and as "target" for the pointers.

[codecov]

Codecov Report

Merging #6905 (118b5b1) into develop (f7a33df) will decrease coverage by 0.02%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6905      +/-   ##
===========================================
- Coverage    77.81%   77.79%   -0.03%     
===========================================
  Files         1568     1568              
  Lines       179985   180301     +316     
===========================================
+ Hits        140054   140262     +208     
- Misses       39931    40039     +108     

Impacted Files	Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	87.80% <100.00%> (+0.10%)	⬆️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	99.66% <100.00%> (+0.01%)	⬆️
src/util/bitvector_expr.cpp	58.55% <0.00%> (-35.65%)	⬇️
src/solvers/flattening/boolbv_overflow.cpp	43.94% <0.00%> (-4.74%)	⬇️
src/goto-programs/goto_inline_class.cpp	85.08% <0.00%> (-3.04%)	⬇️
src/util/simplify_expr.cpp	83.08% <0.00%> (-2.66%)	⬇️
src/solvers/flattening/boolbv_width.cpp	73.80% <0.00%> (-1.90%)	⬇️
src/goto-checker/report_util.cpp	60.73% <0.00%> (-0.53%)	⬇️
src/solvers/flattening/boolbv_constant.cpp	36.20% <0.00%> (-0.46%)	⬇️
src/goto-programs/goto_convert_side_effect.cpp	95.13% <0.00%> (-0.41%)	⬇️
... and 48 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 8bf3ea6...118b5b1. Read the comment docs.

[thomasspriggs]

⛏️ Isn't stack_malloc a contradiction, given than malloc allocates heap memory, not stack memory?

[thomasspriggs]

ℹ️ This test is pretty close to running into the unimplemented array functionality. Adding --no-array-field-sensitivity to cbmc will cause a failure. Also replacing the last for loop using a non-det range for the i variable will do the same -

#include <stdlib.h>

int main()
{
  int *a = malloc(sizeof(int) * 5);

  for(int i = 0; i < 5; i++)
    *(a + i) = i;

  int i;
  __CPROVER_assume(i >= 0);
  __CPROVER_assume(i < 5);

  {
    __CPROVER_assert(*(a + i) >= i, "*(a + i) >= i: expected successful");
    __CPROVER_assert(*(a + i) <= i, "*(a + i) <= i: expected successful");
    __CPROVER_assert(*(a + i) == i, "*(a + i) <= i: expected successful");
    __CPROVER_assert(*(a + i) != i, "*(a + i) <= i: expected failure");
  }
}

No need to action this comment. I just wanted to make note of my findings into why this array using example works despite the unimplemented array functionality.