Allow checks to be performed inside quantifier statements. #6399

NlightNFotis · 2021-10-18T17:27:49Z

This allows checks from CLI flags like --pointer-check to be performed inside
expressions in quantifier statements.

This should be addressing issue #6231 .

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.

martin-cs

I can't immediately see anything wrong with this BUT the whole thing makes me uneasy. The comments have been there since 2013 which makes me think that they were probably there for a reason. My immediate thought is about scoping and whether the quantified variable is actually live when the variable is checked. I am also unsure about how nested quantifiers are going to work and to what degree the guards are applied to the checks as well.

Can you please say a little more about how you are expecting things to work?

codecov · 2021-10-18T18:44:03Z

Codecov Report

Merging #6399 (e9585bd) into develop (5f33908) will increase coverage by 0.00%.
The diff coverage is 92.30%.

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

@@           Coverage Diff            @@
##           develop    #6399   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1578     1578           
  Lines       180910   180931   +21     
========================================
+ Hits        137467   137487   +20     
- Misses       43443    43444    +1

Impacted Files	Coverage Δ
src/analyses/goto_check_c.cpp	`90.29% <92.30%> (-0.10%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`95.11% <0.00%> (+0.07%)`	⬆️
src/solvers/smt2/smt2_dec.cpp	`76.52% <0.00%> (+0.86%)`	⬆️

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 eeddb3f...bc772e4. Read the comment docs.

martin-cs

A few more concrete requests for other functionality.

regression/cbmc-primitives/forall_6231_2/test.c

regression/cbmc-primitives/forall_6231_1/test.c

regression/cbmc-primitives/forall_6231_2/test.c

regression/cbmc-primitives/forall_6231_2/test.desc

kroening

This happens to work for the specific case of positive forall, since this is doing Skolemisation implicitly.

This will fail (generating VCCs that are too strong) for exists.
I would much prefer that the Skolemisation is done explicitly, i.e., by introducing a Skolem constant and instantiating the quantifier with it.

NlightNFotis · 2021-10-21T13:22:44Z

Hi Daniel @kroening.

With regards to your first query, we have pushed some changes that show that existentially quantified statements appear to be working as they should (or at least, how we expect them to). Could you review these and let us know if these much your expectations, or if there's a counterexample case you could think of that would help us test our change in a way that exposes a weakness of our current implementation?

regression/cbmc-primitives/exists_6231_2/test.c

regression/cbmc-primitives/exists_6231_2/test.desc

regression/cbmc-primitives/forall_6231_3/test.c

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.c

martin-cs

Do you have examples of quantifiers in assumptions?
Can you briefly outline how this works? What logical expression is generated? How does this interact with scoping?

regression/cbmc-primitives/exists_6231_2/test.c

regression/cbmc-primitives/exists_6231_2/test.desc

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

regression/cbmc-primitives/forall_6231_1/test.c

regression/cbmc-primitives/forall_6231_2/test.c

regression/cbmc-primitives/forall_6231_2/test.desc

SaswatPadhi

Thanks for fixing this! This would help us catch issues in code contracts. Earlier, invariants and function contracts that used implications but performed incorrect/unsafe operations were not caught.

All test cases in this PR seem to check that the consequent is safe. May be the fix already checks the antecedent as well, but can we also add a regression test for that? Something like:

__CPROVER_forall {
  int i;
  (0 <= i && i <= (n / 0))    /* (n/0) should be caught by `--div-by-zero` */
  ==> ...
}

martin-cs · 2021-10-21T17:43:50Z

@SaswatPadhi makes a good point. It is not clear to me whether this treats quantified expressions as guard/statement pairs and if so, whether it checks in both, does it use the guard for the checks in the statement?

NlightNFotis · 2021-10-29T15:34:26Z

@SaswatPadhi makes a good point. It is not clear to me whether this treats quantified expressions as guard/statement pairs and if so, whether it checks in both, does it use the guard for the checks in the statement?

Hi Martin, yes, it does treat quantified expressions as guard/statement pairs and yes it uses the guard for the checks in the statement. I have factored the change that does that in its own commit, with an explanation of how it works there.

As a shorter explanation here, goto_checkt::check in the same file calls check_rec on the expression with true_exprt as a guard, which is then refined based on the exact nature of the expression. We already have support for refining the guard for logical operators, but we were dispatching to that only if the expression had expr.id() == ID_and or expr.id() == ID_or. This appears to be a latent bug that was not manifest because we didn't have any expressions of the particular form that the tests submitted for this PR, so we didn't observe that. As soon as we started performing checks for quantifier expressions (basically, not immediately bailing upon seeing one), we hit this bug.

Does that answer your question?

NlightNFotis · 2021-10-31T23:20:27Z

Hi @kroening ,

I'm trying to better understand the requirement of the second part of your comment, which I quote:

I would much prefer that the Skolemisation is done explicitly, i.e., by introducing a Skolem constant and instantiating the quantifier with it.

My understanding is that Skolemization is being done the same way it was being done before this patch, i.e. in goto_symext::symex_assert() of src/goto-symex/symex_main.cpp:157, which appears to convert existential quantifiers into universals (the first part of the Skolemization process) and then performs a renaming of the bound variable (which performs the substitution by a Skolem function/Skolem constant).

Is that not adequate in some capacity? We have performed extended testing and it seems like this bug fix is working as intended - but if you believe that there's a chance some input might fail we're happy to investigate further and tighten the coverage of the tests for this.

Or is your request that we lift this all into a separate module? If yes, where do you think this would be better plugged in - the simplification modules, a completely different pass over the goto-program that hooks into the transformation pipeline, or somewhere else entirely?

martin-cs · 2021-11-01T13:53:09Z

@NlightNFotis Thanks for your response, the explanation does indeed help and yes, I think you are correct about this being a latent bug. Would it be possible to write a test case that doesn't use quantifiers that triggers this? Would something like y != 0 ==> 10/y <= 10 and --div-by-zero-check do? That way the fixes could be split from the new feature and be approved even if there is more discussion over the checks in quantifiers.

Please could you have a look at, check and if necessary update:

cbmc/src/analyses/goto_check.cpp

Line 111 in ce2680b

/// Check a logical operation: check each operand in separation while

cbmc/src/analyses/goto_check.cpp

Line 1623 in ce2680b

guard.add(expr.id() == ID_or ? boolean_negate(op) : op);

( The real cherry on top would be adding a PRECONDITION that checks for the expression types that are intended to be supported. )

kroening · 2021-11-01T15:04:52Z

The problem is that the identifiers used in quantifiers are no longer guaranteed to be unique, i.e., you could have something like
i[2]== 2 && exists i:int. x/i
which will yield a check that reads
(i[2] != 2) => i!=0
In this formula, i is used twice, and isn't even type consistent -- the first instance is an array, and the second is an int. Formulas like that must not be generated.

You can't test that in the C front-end, since the C front-end's treatment of quantifiers pre-dates the introduction of scoping in the solver backends. Please don't even think about reintroducing this restriction, not even as a temporary hack.

The way to do this properly is to introduce a Skolem symbol for the bound identifier. You'll find that the classes for exists and forall have convenient methods for making that easy!

martin-cs · 2021-11-01T18:01:24Z

@NlightNFotis while reviewing the changes you had kindly described I ran into some concerns. I have documented them here: #6423 I don't consider them a precondition for this PR, but, obviously, they are linked.

NlightNFotis · 2021-11-05T22:04:28Z

@kroening Hi Daniel, the last commit is performing scolemisation of the formula in goto_check. Can you please review it now and let us know if this is adequate for what you had in mind?

@martin-cs Given that the bug-fix has now been merged on its own PR, could you please re-review this and let me know if there's anything more that needs be done?

NlightNFotis · 2021-11-18T18:18:15Z

Hi @kroening, can you take a look at the PR now and let us know if it is more or less what you envisioned for skolemization as a pass?

Specifically, it's the last commit that implements this.

src/goto-programs/skolemization.cpp

src/analyses/goto_check.cpp

src/goto-programs/skolemization.cpp

thomasspriggs · 2021-11-19T12:47:27Z

src/analyses/goto_check.cpp

+      CPROVER_PREFIX,
+      id2string(ns.lookup(quantifier_sym.get_identifier()).base_name),
+      quantified_expr.source_location(),
+      ID_C,


This is still hard coded in your new rename_and_substitute function and still needs fixing.

src/goto-programs/skolemization.h

src/goto-programs/skolemization.cpp

NlightNFotis · 2021-11-23T14:46:32Z

Hello @martin-cs and @kroening , would it be possible to have a look at this again?

It's past our internal reviews and blocked on your reviews right now. I want to take this forward, either in terms of performing improvements and revisions if deemed necessary, or getting this merged.

martin-cs · 2021-11-30T18:14:35Z

@NlightNFotis My apologies for the delay in reviewing. I will look ASAP.

martin-cs

I am removing my block on this but I still have some concerns:

There are no tests using assume; that matters from a user point of view because of code contracts and also from a technical point of view as these are "flipped" during symex so what works with the SAT engine is different.
A lot of the issues with quantifiers are simplified when there is only one level of quantifier alternation. So I feel that alternating tests would be useful.
The renaming code is not, IMHO, Skolemization and to me, doesn't match what @kroening requested. However I believe that it fixes the immediate issue he raised and I will leave it to him to pursue that one.
I'm still struggling a bit to see what is generated; I /think/ it is something like

A && __CPROVER_forall { int i; B ==> C}

will create a VC:

assert(A && __CPROVER_forall { int i; B ==> CHECK_FROM_C } );

it would be good to get that confirmed.

martin-cs · 2021-11-30T18:31:08Z

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE


Would it be possible to check that the assertion passes?

regression/cbmc-primitives/forall_6231_2/test.c

regression/cbmc-primitives/forall_6231_1/test.c

martin-cs · 2021-11-30T18:50:18Z

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+line 9 dereference failure:.*SUCCESS


A more complete check line as you have in other tests would be good.

martin-cs · 2021-11-30T18:51:52Z

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -0,0 +1,15 @@
+CORE
+smt_missing_range_check.c
+--pointer-check -z3


As we still don't have a CI run that doesn't have Z3 set up, please can this be tagged so that the regression tests still work on machines that don't have Z3 installed?

Yes, in the last commit I have added a check for the z3 binary in CMakeLists.txt

martin-cs · 2021-11-30T18:52:25Z

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+line 9 dereference failure:.*SUCCESS


More complete matching against results would be good.

martin-cs · 2021-11-30T18:53:30Z

regression/cbmc-primitives/forall_6231_1/test.c

+
+  assert(*a == *a);
+
+  // BUG: no errors even with `--pointer-check` enabled -- now fixed.


I am not quite sure what this comment is trying to tell me. Whatever it is, it feels like there might be a better place and way or saying it.

Apologies, I added this comment in a haste, and now realise that my phrasing was not the best 😞

I have rephrased that in commit 604d12c. Can you let me know if that's clearer?

martin-cs · 2021-11-30T18:54:12Z

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.c

+
+  assert(*a == *a);
+
+  // BUG: no errors even with `--pointer-check` enabled -- now fixed.


martin-cs · 2021-11-30T18:58:56Z

src/goto-programs/skolemization.cpp

+  exprt &condition,
+  symbol_table_baset &symbol_table)
+{
+  condition.visit_post([&symbol_table](exprt &sub_expression) {


martin-cs · 2021-11-30T19:09:17Z

src/goto-programs/skolemization.cpp

@@ -0,0 +1,57 @@
+/// \file skolemization.h
+/// Rename variables in existentially quantified statements.


This is not what I would think of as Skolemization; this is renaming. For me, Skolemization has to remove the existential so:

assert(__CPROVER_exists { int i; (0 <= i && i < 10) && a[i] == i *i });

becomes:

int skolem_23_i; // Note that if it is nested in a forall then it will need to be an uninterpreted function. assert( (0 <= skolem_23_i && skolem_23_i < 10) && a[skolem_23_i] == skolem_23_i * skolem_23_i );

The general use-case for this is so that provers only have to deal with one kind of quantifier.

Note that the symex engine performs on-the-fly Skolemization where it can; that's how the SAT engine can handle quantifiers at all. However it dynamically handles polarity, so depending on whether the quantifiers are in assume or assert, negated, etc. it will do the right thing.

Hi Martin,

Apologies for that - I'm aware of how skolemization works (in contrast to the code here), but when implemented in its proper form, it resulted in elimination of the existential quantifier far too early in the pipeline. There's code in goto-check or goto-symex (can't remember which of the two) - which depended on the quantifiers being there during VCC generation, and we were left with vccs that didn't semantically match the intended meaning, getting results that were all over the place.

The intended effect of the code above was to do a partial-skolemization, if we can admit that as a thing: perform the renaming, and let the existential quantifier stay, with the result being that the correct VCCs where generated, and it was being eliminated later in the pipeline in a way that felt safer (given that the variables were renamed before hand).

Definitely wasn't ideal, but there was a lot of uncertainty around the implementation of that feature in our pipeline.

My aim now is to drop this and substitute for Daniel's implementation (assuming it passes all tests).

martin-cs

Annoying -- github won't let me just remove my "Request changes" and return to a neutral state. So, I am "approving" this but please don't treat this approved and merge.

kroening · 2021-11-30T20:58:31Z

Please look at https://github.com/diffblue/cbmc/tree/goto_check_guard for an alternative approach, which relegates the problem of introducing the Skolem functions to the solver.

A key benefit of the alternative approach is that this means that there won't be two different kinds of goto-programs, one where bound symbols are unique and one where they aren't.

NlightNFotis · 2021-12-09T18:03:43Z

Hi @martin-cs and @kroening ,

as requested, I've made several enhancements to the tests (added the extra checks Martin requested, tests based on the behaviour of the quantifiers in assumes, and alternating quantifier tests - each of which are in their own commits) and changed the implementation to be using Daniel's code (I lost the commit information because I couldn't cleanly cherry-pick after some changes to goto-check, but I hope my commit message preserves authorship information in an acceptable way).

Could you please have a look again and let me know how it looks to you now?

kroening · 2021-12-09T21:00:21Z

May I suggest squashing the 9 commits that add/change the tests? Otherwise looks fine.

NlightNFotis · 2021-12-13T11:21:39Z

Hi @kroening, if all is fine are you happy to lift your blocking review?

I will of course squash all the test commits before the final merge, I just want to give a chance to @martin-cs to review them on a commit by commit basis so that he can more easily check if his concerns have been addressed accordingly, and assuming he's also happy I will squash and merge.

These are checked against `--pointer-check` and one of them is sourced from the code reported in diffblue#6231.

We are now producing more checks, which was messing with the expectations of the tests. Now made it a bit more general and all is good again.

@kroening

Original code by @kroening in branch `goto_check_guard`.

@kroening

Original code by @kroening in `goto_check_guard` branch.

NlightNFotis requested a review from SaswatPadhi October 18, 2021 17:27

NlightNFotis requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners October 18, 2021 17:27

martin-cs reviewed Oct 18, 2021

View reviewed changes

martin-cs requested changes Oct 18, 2021

View reviewed changes

kroening requested changes Oct 19, 2021

View reviewed changes

NlightNFotis force-pushed the fix_6231 branch from 201bb39 to 5be5efc Compare October 20, 2021 10:36

TGWDB requested changes Oct 21, 2021

View reviewed changes

martin-cs requested changes Oct 21, 2021

View reviewed changes

SaswatPadhi reviewed Oct 21, 2021

View reviewed changes

NlightNFotis force-pushed the fix_6231 branch 3 times, most recently from bbdcd3f to ff47efb Compare October 29, 2021 15:26

TGWDB approved these changes Nov 1, 2021

View reviewed changes

martin-cs mentioned this pull request Nov 1, 2021

goto_check treats ID_and / and_exprt in a non-commutative way #6423

Closed

NlightNFotis mentioned this pull request Nov 3, 2021

Refinement of guard based on antecedent of implication statement #6434

Merged

7 tasks

NlightNFotis force-pushed the fix_6231 branch 4 times, most recently from aec0b8b to 63f6830 Compare November 5, 2021 22:01

NlightNFotis force-pushed the fix_6231 branch from 112cf8f to e675709 Compare November 18, 2021 16:55

thomasspriggs reviewed Nov 19, 2021

View reviewed changes

src/goto-programs/skolemization.cpp Outdated Show resolved Hide resolved

src/analyses/goto_check.cpp Outdated Show resolved Hide resolved

thomasspriggs reviewed Nov 19, 2021

View reviewed changes

src/goto-programs/skolemization.h Outdated Show resolved Hide resolved

src/goto-programs/skolemization.cpp Outdated Show resolved Hide resolved

src/goto-programs/skolemization.cpp Outdated Show resolved Hide resolved

src/goto-programs/skolemization.cpp Outdated Show resolved Hide resolved

NlightNFotis force-pushed the fix_6231 branch from f28976d to c813374 Compare November 21, 2021 23:17

thomasspriggs approved these changes Nov 22, 2021

View reviewed changes

martin-cs reviewed Nov 30, 2021

View reviewed changes

martin-cs approved these changes Nov 30, 2021

View reviewed changes

kroening mentioned this pull request Dec 2, 2021

Split goto_check #6497

Merged

4 tasks

NlightNFotis force-pushed the fix_6231 branch 3 times, most recently from 06cc456 to 38c80f2 Compare December 9, 2021 18:02

NlightNFotis force-pushed the fix_6231 branch 2 times, most recently from ae2e381 to 38c80f2 Compare December 13, 2021 10:41

kroening approved these changes Dec 13, 2021

View reviewed changes

NlightNFotis and others added 4 commits December 15, 2021 14:05

Add regression tests for quantifier checks.

c232b4e

These are checked against `--pointer-check` and one of them is sourced from the code reported in diffblue#6231.

Relax property identity-number checks in enum_is_in_range test.

27d211b

We are now producing more checks, which was messing with the expectations of the tests. Now made it a bit more general and all is good again.

goto_check: use a functor to guard the assertions

031cd8c

Original code by @kroening in branch `goto_check_guard`.

goto_check: check expressions inside exists and forall

bc772e4

Original code by @kroening in `goto_check_guard` branch.

NlightNFotis force-pushed the fix_6231 branch from e9585bd to bc772e4 Compare December 15, 2021 14:05

NlightNFotis merged commit 47c1c7e into diffblue:develop Dec 15, 2021

NlightNFotis deleted the fix_6231 branch December 15, 2021 16:04

NlightNFotis mentioned this pull request Dec 15, 2021

Check flags are not respected within quantified expressions #6231

Closed


		assert(a == a);

		// BUG: no errors even with `--pointer-check` enabled -- now fixed.

		@@ -0,0 +1,57 @@
		/// \file skolemization.h
		/// Rename variables in existentially quantified statements.

Allow checks to be performed inside quantifier statements. #6399

Allow checks to be performed inside quantifier statements. #6399

Uh oh!

Conversation

NlightNFotis commented Oct 18, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Oct 18, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kroening left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Oct 21, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SaswatPadhi left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Oct 21, 2021

Uh oh!

NlightNFotis commented Oct 29, 2021

Uh oh!

NlightNFotis commented Oct 31, 2021

Uh oh!

martin-cs commented Nov 1, 2021

Uh oh!

kroening commented Nov 1, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martin-cs commented Nov 1, 2021

Uh oh!

NlightNFotis commented Nov 5, 2021

Uh oh!

NlightNFotis commented Nov 18, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

NlightNFotis commented Nov 23, 2021

Uh oh!

martin-cs commented Nov 30, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Oct 18, 2021 •

edited

Loading

SaswatPadhi left a comment •

edited

Loading

kroening commented Nov 1, 2021 •

edited

Loading

NlightNFotis Dec 1, 2021 •

edited

Loading