Unit-test try_evaluate_pointer_comparison and bugfix #4774

romainbrenguier · 2019-06-11T08:37:18Z

This adds some unit test for try_evaluate_pointer_comparison, then fix a small bug, and add an unit-test for the case that was buggy, then add some checks for an implicit invariant that I noticed while unit testing, and make value_sett::output more usable in particular for debugging unit tests.

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.
[na] 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).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

This is so that we can unit-test this function.

get_l1_object suggests we are comparing the address of the object, but the actually should interpret the symbol itself as a pointer. A unit test for the case of the issue that is fixed will be added in a following commit.

Field sensitivity the value set to keep track of pointers in individal fields, making it possible to evaluate equalities such as the one in the example. This is a case which would not work if try_evaluate_pointer_comparisons was using get_l1_object_identifier instead of getting the identifier of the whole l1 expression (not the underlying object). fixup! Check pointer evaluation in the array case

smowton · 2019-06-11T11:09:51Z

src/pointer-analysis/value_set.cpp

@@ -1220,7 +1221,8 @@ void value_sett::assign(
  std::cout << "--------------------------------------------\n";
  output(ns, std::cout);
 #endif
-
+  PRECONDITION(is_l1_renamed(lhs));


This is only true when used in symex-- otherwise we expect to operate on plain un-renamed expressions. Therefore these invariants should move to symex_dereference or to some wrapper function in goto_statet.

I defined a wrapper class for value_sett (a wrapper function wouldn't ensure we didn't continue to use the unchecked one)

owen-mc-diffblue

Great unit tests. Some other edge cases you might want to consider testing: if the value-set contains ID_unknown, ID_invalid or a failed symbol then try_evaluate_pointer_comparison should not be able to determine anything.

romainbrenguier · 2019-06-11T15:34:17Z

@owen-jones-diffblue I added some cases in the unit test, in particular some with unknown in the value set.

owen-mc-diffblue · 2019-06-11T15:41:00Z

Btw failed symbols are covered by the regression test that was merged in #4659, I believe.

smowton · 2019-06-11T16:24:44Z

src/goto-symex/symex_value_set.h

+
+/// Wrapper for value_sett which ensures we access it in a consistent way.
+/// In particular level 1 names should be used.
+class symex_value_sett : value_sett


Generally prefer composition to inheritence

smowton · 2019-06-11T16:27:26Z

src/goto-symex/goto_symex_state.cpp

@@ -222,13 +138,13 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
    ssa_exprt l1_lhs(lhs);
    l1_lhs.remove_level_2();

-    if(run_validation_checks)


These should still be guarded by if(run_validation_checks)

tautschnig

This PR appears to be doing at least 3 different things (and some of them I believe are wrong, see detailed comments).

tautschnig · 2019-06-11T21:15:57Z

src/goto-symex/renamed.cpp

@@ -14,9 +14,6 @@ Author: Romain Brenguier, [email protected]
 #include <util/std_expr.h>
 bool is_l1_renamed(const exprt &expr)
 {
-  if(!is_l2_renamed(expr.type()))
-    return false;


The claim made in the commit message seems wrong: the type may well be renamed to L2 even when the object itself is only L1. On the contrary, it actually makes no sense for the type to be renamed to L1 ever.

Ok I didn't know that the type could be L2 while the object L1. But is it true that L1 object always have L2 types? It sounds wrong to me. It seems that when an ssa_exprt is renamed to L1, its type is also renamed to L1.

Renaming to L1 effectively is instantiation/determines which instance of a named object we are using. At that point the type must be complete, i.e., must be L2.

It seems to be the case in symex_decl but not in symex_dereference and the other places where L1 renaming is used. Should we make rename<L1> apply L2 renaming on the type to ensure this is consistent?

tautschnig · 2019-06-11T21:17:10Z

src/pointer-analysis/value_set.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening, [email protected]

 #include <langapi/language_util.h>
 #include <util/range.h>
+#include <util/format_expr.h>
+#include <util/format_type.h>


But then #include <langapi/language_util.h> better be removed as well (and hopefully also the corresponding entry in module_dependencies.txt).

tautschnig · 2019-06-11T21:18:06Z

src/pointer-analysis/value_set.cpp

@@ -20,10 +20,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/simplify_expr.h>

+#include <goto-symex/renamed.h>


I don't think a dependency from pointer-analysis towards goto-symex is right.

romainbrenguier · 2019-06-12T06:12:27Z

@tautschnig

This PR appears to be doing at least 3 different things (and some of them I believe are wrong, see detailed comments).

Yes you are right, I extracted what comes after the unit tests and bugfix into a new pull request
#4778 so that we can merge the fix more quickly and leave time for discussion on the other part.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e26f4cd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/115206278

codecov-io · 2019-06-12T07:01:12Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@c63c167). Click here to learn what that means.
The diff coverage is 99.18%.

@@            Coverage Diff             @@
##             develop    #4774   +/-   ##
==========================================
  Coverage           ?   68.62%           
==========================================
  Files              ?     1276           
  Lines              ?   105155           
  Branches           ?        0           
==========================================
  Hits               ?    72162           
  Misses             ?    32993           
  Partials           ?        0

Impacted Files	Coverage Δ
src/goto-symex/goto_symex.h	`92.3% <ø> (ø)`
src/goto-symex/symex_goto.cpp	`94.82% <100%> (ø)`
...it/goto-symex/try_evaluate_pointer_comparisons.cpp	`99.15% <99.15%> (ø)`

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 c63c167...767d8f0. Read the comment docs.

This test the case where ptr1 can point to value1 or value2 and we evaluate `ptr1 != &value1`

This check the case where ptr1 is either &value1 or &value2 and we compare it to null.

This adds a unit test for the case where the value set contains unknown. In that case no comparison can be decided.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 767d8f0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/115226966

romainbrenguier added Symbolic Execution bugfix Tests labels Jun 11, 2019

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, smowton and tautschnig as code owners June 11, 2019 08:37

Declare try_evaluate_pointer_comparisons in header

dcc9d79

This is so that we can unit-test this function.

romainbrenguier force-pushed the unit-test/try-evaluate-pointer-comparison branch from b74ba9d to 4bf2cd5 Compare June 11, 2019 09:35

romainbrenguier added 3 commits June 11, 2019 11:05

Unit test for try_evaluate_pointer_comparisions

1c01ee7

Replace use of get_l1_object by remove_level_2

2c34886

get_l1_object suggests we are comparing the address of the object, but the actually should interpret the symbol itself as a pointer. A unit test for the case of the issue that is fixed will be added in a following commit.

romainbrenguier force-pushed the unit-test/try-evaluate-pointer-comparison branch from 4bf2cd5 to 017cd09 Compare June 11, 2019 10:06

smowton reviewed Jun 11, 2019

View reviewed changes

romainbrenguier added the do not merge label Jun 11, 2019

owen-mc-diffblue approved these changes Jun 11, 2019

View reviewed changes

romainbrenguier force-pushed the unit-test/try-evaluate-pointer-comparison branch 2 times, most recently from b056982 to 2253cbd Compare June 11, 2019 15:19

romainbrenguier removed the do not merge label Jun 11, 2019

smowton reviewed Jun 11, 2019

View reviewed changes

tautschnig requested changes Jun 11, 2019

View reviewed changes

tautschnig assigned romainbrenguier Jun 11, 2019

romainbrenguier mentioned this pull request Jun 12, 2019

Introduce symex value set as interface to value set #4778

Closed

7 tasks

romainbrenguier force-pushed the unit-test/try-evaluate-pointer-comparison branch from ded9716 to e26f4cd Compare June 12, 2019 06:10

allredj reviewed Jun 12, 2019

View reviewed changes

romainbrenguier added 3 commits June 12, 2019 09:54

Add case to try_evaluate_pointer_comparisons test

7272dfb

This test the case where ptr1 can point to value1 or value2 and we evaluate `ptr1 != &value1`

Add case for evaluate pointer comparison with null

c024823

This check the case where ptr1 is either &value1 or &value2 and we compare it to null.

Test try_evaluate_pointer_comparisons unknown case

767d8f0

This adds a unit test for the case where the value set contains unknown. In that case no comparison can be decided.

romainbrenguier force-pushed the unit-test/try-evaluate-pointer-comparison branch from 6f1891d to 767d8f0 Compare June 12, 2019 08:58

allredj reviewed Jun 12, 2019

View reviewed changes

romainbrenguier assigned tautschnig and unassigned romainbrenguier Jun 12, 2019

tautschnig approved these changes Jun 14, 2019

View reviewed changes

tautschnig merged commit 6514482 into diffblue:develop Jun 14, 2019

romainbrenguier deleted the unit-test/try-evaluate-pointer-comparison branch June 17, 2019 07:44

Unit-test try_evaluate_pointer_comparison and bugfix #4774

Unit-test try_evaluate_pointer_comparison and bugfix #4774

Uh oh!

Conversation

romainbrenguier commented Jun 11, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

owen-mc-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Jun 11, 2019

Uh oh!

owen-mc-diffblue commented Jun 11, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Jun 12, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jun 12, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Jun 12, 2019 •

edited

Loading