Symex: resolve pointer comparisons using the value-set by owen-mc-diffblue · Pull Request #4444 · diffblue/cbmc

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

    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

    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

  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

Conversation

owen-mc-diffblue commented Mar 27, 2019 • edited by smowton Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

smowton 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!

Choose a reason for hiding this comment

Uh oh!

owen-mc-diffblue commented Mar 28, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

owen-mc-diffblue commented Mar 28, 2019

Uh oh!

smowton commented Mar 28, 2019

Uh oh!

romainbrenguier commented Mar 29, 2019

Uh oh!

owen-mc-diffblue commented Mar 29, 2019

Uh oh!

owen-mc-diffblue commented Mar 29, 2019

Uh oh!

smowton commented Mar 29, 2019

Uh oh!

smowton commented Mar 29, 2019

Uh oh!

owen-mc-diffblue commented Mar 27, 2019 •

edited by smowton

Loading

owen-mc-diffblue commented Mar 28, 2019 •

edited

Loading