Symex: resolve pointer comparisons using the value-set #4444

owen-mc-diffblue · 2019-03-27T14:47:38Z

This allows us to evaluate boolean expressions (including GOTO conditions) that test pointer equality or inequality (particularly "ptr == null" or "!= null") where the value-set contains sufficient information. We can already handle simple cases where ptr has a single known alias via constant propagation and aliasing, but not cases where ptr is non-constant, for example because it is drawn from an array.

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.

owen-mc-diffblue · 2019-03-27T14:55:35Z

src/goto-symex/goto_symex.h

@@ -287,6 +287,10 @@ class goto_symext
    statet &,
    bool keep_array);

+  exprt try_evaluate_pointer_comparisons(


Any suggestions for a better name?

I like this one!

owen-mc-diffblue · 2019-03-27T14:57:00Z

src/goto-symex/goto_symex.h

@@ -333,6 +337,11 @@ class goto_symext
    const exprt &new_guard,
    const namespacet &ns);

+  optionalt<exprt> build_reference_to_value_set_element(


This function might fit better somewhere else - perhaps in value_set_dereferencet, since it's mainly a wrapper around value_set_dereferencet::build_reference_to?

Proooobably. No strong opinion.

owen-mc-diffblue · 2019-03-27T14:57:51Z

src/goto-symex/symex_goto.cpp

+      op = try_evaluate_pointer_comparisons(std::move(op), value_set);
+    }
+  }
+  else if(condition.id() == ID_not)


anything else I should be recursing over, other than AND, OR and NOT?

No I think that's enough

Oh wait, how about the arguments of a boolean-typed if_exprt

(e.g. x == y ? z == w : a == b)

Or indeed the first arg of an if_exprt in any context. Total recursion looking for == and != nodes might be the simplest thing.

I 100% think these comments through before beginning to write FYI

owen-mc-diffblue · 2019-03-27T14:59:08Z

src/goto-symex/symex_goto.cpp

+    {
+      symbol_exprt *symbol_expr =
+        expr_try_dynamic_cast<symbol_exprt>(condition.op0());
+      exprt &constant = condition.op1();


Currently it assumes the symbol is on the lhs and the constant is on the rhs. I will fix that up.

owen-mc-diffblue · 2019-03-27T15:00:43Z

src/goto-symex/symex_main.cpp

@@ -583,6 +583,38 @@ find_unique_pointer_typed_symbol(const exprt &expr)
  return return_value;
 }

+optionalt<exprt> goto_symext::build_reference_to_value_set_element(


This code was in goto_symext::try_filter_value_sets and I've pulled it out into a function to reuse it. Perhaps I'll make that a separate commit.

smowton

Looks good except I believe the null case is broken, and at least needs tests.

smowton · 2019-03-27T15:02:07Z

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

+    possibly_reachable_12 = 7;
+
+  int unconditionally_reachable_13;
+  if((ptr_to_a == &a && c == 3) || c == 0)


Bear in mind these constant comparisons with c may well be resolved very early as c is only assigned once and never address-taken.

I've changed them to other pointer comparisons. And I now take the address of all the integers at the beginning, if that's a thing that symex cares about.

smowton · 2019-03-27T15:04:32Z

src/goto-symex/symex_goto.cpp

+        expr_try_dynamic_cast<symbol_exprt>(condition.op0());
+      exprt &constant = condition.op1();
+
+      if(symbol_expr && goto_symex_is_constantt()(constant))


Handle the reverse case too (constant OP symbol)

(and test this)

smowton · 2019-03-27T15:05:02Z

src/goto-symex/symex_goto.cpp

+      if(symbol_expr && goto_symex_is_constantt()(constant))
+      {
+        value_setst::valuest value_set_elements;
+        value_set.get_value_set(


Assert that symbol_expr is already L1 at least

smowton · 2019-03-27T15:06:23Z

src/goto-symex/symex_goto.cpp

+          to_ssa_expr(*symbol_expr).get_l1_object(), value_set_elements, ns);
+
+        INVARIANT(
+          constant.id() == ID_address_of || constant.id() == ID_NULL,


Surprising! Null is usually represented as an ID_constant with value = NULL -- suspect you need to add tests for this

smowton · 2019-03-27T15:10:38Z

src/goto-symex/symex_goto.cpp

+
+        if(!unknown_or_invalid_found)
+        {
+          if(!constant_found)


Give some brief comments setting out the logic here, as !constant_found and value_set_elements.size() == 1 don't immediately chime with "x in { a, b, c }" and "x in { x }" respectively.

owen-mc-diffblue · 2019-03-28T16:26:08Z

I've addressed all of @smowton's review comments on the draft PR and got CI working (touch wood).

smowton · 2019-03-28T16:39:11Z

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

+
+  // Equality "=="
+
+  // A non-null pointer and the correct value


correct -> matching and incorrect -> non-matching everywhere

smowton · 2019-03-28T16:40:36Z

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

+
+  // Disequality "!="
+
+  // A non-null pointer and the correct value


smowton · 2019-03-28T16:43:15Z

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

+test::1::unreachable_12[^\s]+ = 7$
+^warning: ignoring
+--
+Pointer comparisons will be resolved in symex by a mixture of constant


Suggest adding conditions that check you check for everything you should, by making sure unreachable_1[3-9]) and unreachable[2-9][0-9] for example don't occur anywhere (i.e., if someone added a test but not a cross-check this regex would complain)

smowton · 2019-03-28T16:46:03Z

src/goto-symex/symex_goto.cpp

+
+  INVARIANT(
+    other_operand.id() == ID_address_of ||
+      (typecast_expr && typecast_expr->op().id() == ID_address_of) ||


If you're not sure this is simplified you might get redundant stacked typecast ops

smowton · 2019-03-28T16:47:36Z

src/goto-symex/symex_goto.cpp

+    expr_try_dynamic_cast<symbol_exprt>(symbol_expr);
+
+  if(!symbol_expr_lhs)
+  {


No need for braces with one-liner ifs

I prefer to use them in all cases

smowton · 2019-03-28T16:51:26Z

src/goto-symex/symex_goto.cpp

+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+static bool try_evaluate_pointer_comparisons_base_case_with_check(


Instead of calling this twice, suggest something like https://github.com/diffblue/cbmc/blob/develop/src/goto-symex/goto_state.cpp#L67

smowton · 2019-03-28T16:51:59Z

src/goto-symex/symex_goto.cpp

+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+static void try_evaluate_pointer_comparisons_base_case(


How about try_evaluate_pointer_comparison, singular?

smowton · 2019-03-28T16:53:26Z

src/goto-symex/symex_goto.cpp

+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+static bool try_evaluate_pointer_comparisons_base_case_with_check(


I don't think there's much gained by the two functions (with_check vs. without) since they're both only called in one place

owen-mc-diffblue · 2019-03-28T17:02:53Z

Note also that the last two commits break sharing everywhere, so we'll have to rethink how to do that.

smowton · 2019-03-28T17:39:00Z

Suggested change: smowton@1daa2c6

That removes renamed_vectort and instead uses depth_begin/depth_end, which avoid sharing breaks when no changes are made, to selectively alter the renamed expression, only permitting changes where the renaming level is consistent. @romainbrenguier are you happy with this?

@owen-jones-diffblue note that also applies a couple of my suggestions above since it made it easier to code :)

romainbrenguier · 2019-03-29T07:18:18Z

@smowton

Suggested change: smowton/cbmc@1daa2c6
That removes renamed_vectort and instead uses depth_begin/depth_end, which avoid sharing breaks when no changes are made, to selectively alter the renamed expression, only permitting changes where the renaming level is consistent. @romainbrenguier are you happy with this?

Yes that looks better. What I'm not sure about is the fact that the mutator function takes an exprt as argument rather that a renamedt. That way you avoid calling constructors on all intermediary expressions, but I don't think it's nice for the interface. Maybe we could make renamedt privately inherit from exprt so that we can use static_cast instead of a constructor, so that conversion would be cheap and the interface nicer?
Here is the change I propose (if you want to use it): #4454

owen-mc-diffblue · 2019-03-29T07:38:20Z

Thanks @smowton, that's much better. I've cherry-picked it and squashed it in, along with fixes for all the things you mentioned. I did add an extra commit which makes selectively_mutate a free function (which is a friend of renamedt), since it doesn't make sense to be using depth iterators for anything when underlyingt is derived from exprt. I'm not sure how this interacts with @romainbrenguier's suggestion.

There are three failing tests. The first is exception_cleanup, which is failing because symex can now tell that @inflight_exception is not null, so the test needs to be changed. I'm not totally sure what it should now be. The failing lines are:

1 remaining after simplification$

in test.desc and

file Test\.java line 6 function java::Test.main:\(I\)V
no uncaught exception

in vccs.desc.

The other two are nondet_elements_longer_lists and nondet_elements_longer_lists_global, which are failing in the same way. I'm looking into that at the moment.

owen-mc-diffblue · 2019-03-29T07:54:05Z

For nondet_elements_longer_lists and nondet_elements_longer_lists_global, the test is failing to find these two lines: ```
[test_function.unwind.\d+] line \d+ unwinding assertion loop 0: SUCCESS
[test_function.unwind.\d+] line \d+ unwinding assertion loop 1: SUCCESS

Is there a good reason that we would not generate these unwinding assertions? If symex can determine that they are true then does it just not output them in the formula?

smowton · 2019-03-29T08:26:19Z

@owen-jones-diffblue unsure about the unwinding assertions (yet) but the exception one is entirely desirable -- that 1 VCC remaining was a shortcoming which we have now fixed (symex can tell no exception escaped from the whole program). Just amend the test to check all conditions are symex'd away.

smowton · 2019-03-29T08:28:22Z

@romainbrenguier I'm not sure I follow, what would your ideal interface look like?

tautschnig · 2019-03-29T08:33:56Z

@owen-jones-diffblue Presumably your changes just result in more constant propagation, and thus those unwinding assertions are resolved by the simplifier already. #2574 does the same, i.e., removes those lines from the test spec.

romainbrenguier · 2019-03-29T08:54:35Z

@smowton

@romainbrenguier I'm not sure I follow, what would your ideal interface look like?

I would think having mutator_functiont take renamedt arguments would be more useful (though in your case it doesn't really matter). For instance imagine we want to selectively apply simplify to operands of a renamedt, you could do it with a renamedt -> optinalt<renamedt> function. I'm not insisting on it, since it is not necessary here, but could be nice in the future.

smowton · 2019-03-29T09:01:15Z

Ah sure, ok. On the one hand the tag is useful if you want to call a function that demands a renamedt, but I certainly like not having to make a dedicated object for every subexpression, so your privately-inherit trick looks like a good solution.

owen-mc-diffblue · 2019-03-29T11:06:26Z

I've marked this as do not merge until we have some benchmarking data for it

owen-mc-diffblue · 2019-03-29T13:12:49Z

I've cherry-picked ##4454 and added a commit to use it. Before merging this should be cleaned up.

smowton · 2019-05-13T10:32:20Z

cbmc CORE unit tests times: unchanged

smowton · 2019-05-13T10:35:52Z

Large Webgoat example: 55 seconds to reach a particular checkpoint (down 5 seconds)

smowton · 2019-05-13T16:04:02Z

Romain's Sakai benchmark: One benchmark reduced around 15 seconds (from 145 seconds), the remainder tested showed negligible difference.

smowton · 2019-05-13T16:04:28Z

Therefore I'm pretty confident this has no noticeable cost in context of the other fairly-expensive ops we perform in symex.

peterschrammel · 2019-05-13T16:16:50Z

src/goto-symex/symex_goto.cpp

+  const symbol_exprt &symbol_expr,
+  const exprt &other_operand,
+  const value_sett &value_set,
+  const irep_idt language_mode,


peterschrammel · 2019-05-13T16:17:16Z

src/goto-symex/symex_goto.cpp

+/// \return If we were able to evaluate the condition as true or false then we
+///   return that, otherwise we return an empty optionalt
+static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
+  irep_idt operation,


peterschrammel · 2019-05-13T16:17:53Z

src/goto-symex/symex_goto.cpp

+static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
+  const renamedt<exprt, L2> &renamed_expr,
+  const value_sett &value_set,
+  const irep_idt language_mode,


peterschrammel · 2019-05-13T16:18:06Z

src/goto-symex/symex_goto.cpp

+static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
+  renamedt<exprt, L2> condition,
+  const value_sett &value_set,
+  const irep_idt language_mode,


allredj

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

value_set_dereferencet::valuet is only used as the return value of value_set_dereferencet::build_reference_to. valuet::value is an expression for the object pointed to, which is what's needed for dereferencing. In other contexts, e.g. filtering value-sets, what is needed is an expression for the pointer. This logic already existed in try_filter_value_set, but putting it directly in build_reference_to makes it easier to use it in other places and makes it clear that it didn't cope with typecasts properly.

Use the value-set to evaluate pointer comparisons as true or false where possible

At time of writing, develop fails on the following lines of the test: test::1::unconditionally_reachable_1[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+$$ [FAILED] test::1::unconditionally_reachable_6[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+$$ [FAILED] test::1::unconditionally_reachable_7[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+$$ [FAILED] test::1::unconditionally_reachable_8[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+$$ [FAILED] test::1::unconditionally_reachable_9[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+$$ [FAILED] test::1::unconditionally_reachable_10[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+$$ [FAILED] test::1::unconditionally_reachable_11[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+$$ [FAILED] test::1::unconditionally_reachable_12[^\s]+ = $goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+$$ [FAILED] test::1::unreachable_1[^\s]+ = 7$ [FAILED] test::1::unreachable_6[^\s]+ = 7$ [FAILED] test::1::unreachable_7[^\s]+ = 7$ [FAILED] test::1::unreachable_8[^\s]+ = 7$ [FAILED] test::1::unreachable_9[^\s]+ = 7$ [FAILED] test::1::unreachable_10[^\s]+ = 7$ [FAILED] test::1::unreachable_11[^\s]+ = 7$ [FAILED] test::1::unreachable_12[^\s]+ = 7$ [FAILED]

allredj

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

tautschnig · 2019-05-15T15:53:19Z

I'm afraid this actually causes spurious counterexamples being reported. I'll try to build a small regression test.

tautschnig · 2019-05-15T15:59:57Z

Actually it's pretty simple:

int main()
{
  void *ptr;
  if(ptr == 0)
  {
    return 0;
  }
  __CPROVER_assert(ptr != 0, "null");
}

I believe the problem is that ptr has never been assigned, and thus the value set has no information about it.

smowton · 2019-05-15T16:12:03Z

Discussion on Slack summary: will revert and re-submit with a fix

This is to guard against the regression earlier introduced in diffblue#4444 (and reverted in diffblue#4656).

This is to guard against the regression earlier introduced in #4444 (and reverted in #4656).

owen-mc-diffblue requested a review from smowton March 27, 2019 14:47

owen-mc-diffblue commented Mar 27, 2019

View reviewed changes

smowton reviewed Mar 27, 2019

View reviewed changes

owen-mc-diffblue force-pushed the value-set-filtering-infeasible-branch branch from 618b074 to 1081b00 Compare March 28, 2019 16:23

owen-mc-diffblue marked this pull request as ready for review March 28, 2019 16:25

owen-mc-diffblue requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli and tautschnig as code owners March 28, 2019 16:25

owen-mc-diffblue requested a review from smowton March 28, 2019 16:26

owen-mc-diffblue force-pushed the value-set-filtering-infeasible-branch branch from 1081b00 to eb55978 Compare March 28, 2019 16:28

smowton reviewed Mar 28, 2019

View reviewed changes

owen-mc-diffblue force-pushed the value-set-filtering-infeasible-branch branch from eb55978 to b20167c Compare March 29, 2019 07:31

owen-mc-diffblue force-pushed the value-set-filtering-infeasible-branch branch from b20167c to 44c25df Compare March 29, 2019 11:01

owen-mc-diffblue added the do not merge label Mar 29, 2019

tautschnig assigned smowton and owen-mc-diffblue and unassigned tautschnig May 12, 2019

smowton closed this May 13, 2019

smowton reopened this May 13, 2019

smowton force-pushed the value-set-filtering-infeasible-branch branch from 96d2f30 to 13b6290 Compare May 13, 2019 10:51

smowton force-pushed the value-set-filtering-infeasible-branch branch from 13b6290 to ff6002b Compare May 13, 2019 16:08

peterschrammel approved these changes May 13, 2019

View reviewed changes

allredj reviewed May 13, 2019

View reviewed changes

Owen added 4 commits May 14, 2019 13:40

Evaluate some pointer comparisons as true or false

af21f2b

Use the value-set to evaluate pointer comparisons as true or false where possible

Update existing tests so they pass

213a1b2

smowton force-pushed the value-set-filtering-infeasible-branch branch from ff6002b to 213a1b2 Compare May 14, 2019 12:40

smowton merged commit 0aef428 into diffblue:develop May 14, 2019

allredj reviewed May 14, 2019

View reviewed changes

owen-mc-diffblue deleted the value-set-filtering-infeasible-branch branch May 15, 2019 10:05

owen-mc-diffblue mentioned this pull request May 15, 2019

Revert "Symex: resolve pointer comparisons using the value-set" #4656

Merged

danielsn mentioned this pull request May 15, 2019

CBMC harness for aws_hash_table_find(), and related fixups. awslabs/aws-c-common#350

Merged

tautschnig added a commit to tautschnig/cbmc that referenced this pull request May 16, 2019

Regression test for null-pointer optimisation

c31309a

This is to guard against the regression earlier introduced in diffblue#4444 (and reverted in diffblue#4656).

tautschnig mentioned this pull request May 16, 2019

Regression test for null-pointer optimisation #4659

Merged

3 tasks

kroening pushed a commit that referenced this pull request May 16, 2019

Regression test for null-pointer optimisation

046ed40

This is to guard against the regression earlier introduced in #4444 (and reverted in #4656).

owen-mc-diffblue mentioned this pull request May 16, 2019

Symex: resolve pointer comparisons using the value-set (second attempt) #4664

Merged

7 tasks


		// Disequality "!="

		// A non-null pointer and the correct value

Symex: resolve pointer comparisons using the value-set #4444

Symex: resolve pointer comparisons using the value-set #4444

Conversation

owen-mc-diffblue commented Mar 27, 2019 • edited by smowton Loading

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

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

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

Choose a reason for hiding this comment

owen-mc-diffblue commented Mar 28, 2019 • edited Loading

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Mar 28, 2019

smowton commented Mar 28, 2019

romainbrenguier commented Mar 29, 2019

owen-mc-diffblue commented Mar 29, 2019

owen-mc-diffblue commented Mar 29, 2019

smowton commented Mar 29, 2019

smowton commented Mar 29, 2019

tautschnig commented Mar 29, 2019

romainbrenguier commented Mar 29, 2019

smowton commented Mar 29, 2019

owen-mc-diffblue commented Mar 29, 2019

owen-mc-diffblue commented Mar 29, 2019

smowton commented May 13, 2019

smowton commented May 13, 2019

smowton commented May 13, 2019

smowton commented May 13, 2019

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

tautschnig commented May 15, 2019

tautschnig commented May 15, 2019

smowton commented May 15, 2019

owen-mc-diffblue commented Mar 27, 2019 •

edited by smowton

Loading

owen-mc-diffblue commented Mar 28, 2019 •

edited

Loading