JBMC: enable model and SSA equation verification #3747

smowton · 2019-01-10T15:05:28Z

This enables validation of the GOTO model and SSA equations in all JBMC regression tests, making the minimal modifications such that they work:

Fixing an accidentally untyped expression
Disabling basename validation for Java, which presently uses a different convention that C for name-to-basename relationship
Loosening type comparison to only require base_type_eq, not exact equality
Fixing SSA expression type verification
Fixing SSA DECL verification

I package these together here because this enables all these small fixes to be checked throughout the whole regression test suite, but if people prefer they can be split apart. Naturally, recommend reviewing commit by commit.

This had used a typeless symbol expression for ages without us noticing.

This invokes validation using the same arguments as CBMC.

This mirrors existing support in goto_modelt.

tautschnig · 2019-01-10T15:10:12Z

src/util/symbol.cpp

+  // "method")
+  if(
+    !has_suffix(id2string(name), id2string(base_name)) &&
+    mode != ID_java)


I believe @chrisr-diffblue was also looking into this as there are also cases in C where this doesn't hold. Is this correct?

Yes, I'm looking into other cases - just hadn't got as far as java yet, so Chris has saved me some work here :-)

tautschnig · 2019-01-10T15:10:44Z

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
      symbol_table);
    const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
    code_assignt get_argument(
-      init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
+      init_symbol_expression,
+      symbol_exprt(this_argument.get_identifier(), this_type));


We should really remove the single-argument constructor.

In another PR, sure

Sure, that was not meant as a request for work.

tautschnig · 2019-01-10T15:12:00Z

src/util/std_code.h

    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(code, vm);

    DATA_CHECK(
      vm,
-      code.op0().type() == code.op1().type(),
+      base_type_eq(code.op0().type(), code.op1().type(), ns),


To be debated with @kroening as this appears to work against the effort going on in other PRs.

Fair enough if we want the strict same-level-of-indirection condition in the future, but we certainly don't even try to do that at present.

Can this commit be dropped from the PR? I understand that this would mean it doesn't work for Java at the moment, but then we can get all the other improvements in the meantime.

Well, my intent was to use this as the means of testing the other improvements, by showing particular programs begin to satisfy this constraint when the fixes are applied, so I'd much prefer to have this statement of our current intended guarantee available, then we can chase after a future attempted standard later?

tautschnig · 2019-01-10T15:13:36Z

src/goto-symex/symex_target_equation.cpp

@@ -966,6 +966,8 @@ void symex_target_equationt::SSA_stept::validate(
    validate_full_expr(ssa_lhs, ns, vm);
    validate_full_expr(ssa_full_lhs, ns, vm);
    validate_full_expr(original_full_lhs, ns, vm);
+    if(type == goto_trace_stept::typet::DECL)
+      break;


In this case I'd prefer some copy&paste and just completely separate the ASSIGNMENT and DECL cases.

chrisr-diffblue

Not going to comment on the base_type_eq debate, but I'm happy for this to go in as it is. I'll leave the final say on base_type_eq to @tautschnig and @kroening

smowton · 2019-01-14T15:42:49Z

@tautschnig spoke with @kroening just now, who said he's happy to go for base_type_eq now (and fix everything that violates even that) and then subsequently go to ==.

tautschnig · 2019-01-14T15:45:50Z

@smowton Maybe then do a clean revert of the commit that switched from base_type_eq to == recently to make clear we are intentionally reverting this change?

They use a different pattern to that expected for C programs, and changing that will have some impact. For now let's make validation practically usable without making a change with potentially widespread impact.

This reverts commit caae4ce. Reverting because we can't currently meet either the weak (base_type_eq) or the strong (==) consistency requirement. Let's target the weak one first.

smowton · 2019-01-14T15:52:36Z

@tautschnig done

DECL clauses do not give an RHS, so comparing its type against the LHS is meaningless (and always fails).

The expr version expects two like-structured expressions and validates subexpressions pairwise, which is not the expected situation for VCCs.

Adding an include in a prior commit --> I must sort the other ones, apparently :)

allredj

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

peterschrammel · 2019-01-14T20:15:55Z

src/util/symbol.cpp

+  // Exception: Java symbols' base names do not have type signatures
+  // (for example, they can have name "someclass.method:(II)V" and base name
+  // "method")
+  if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)


Can we check that method is between . and : instead?

It also differs for field symbols, and generics, and... I'd like to leave (a) setting a convention and (b) enforcing it for a different PR!

smowton added 3 commits January 10, 2019 10:56

Method stubs: add missing type

249fb3f

This had used a typeless symbol expression for ages without us noticing.

JBMC: support validation

eda5f14

This invokes validation using the same arguments as CBMC.

Lazy goto model: support validation

c203ef2

This mirrors existing support in goto_modelt.

smowton requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, tautschnig and thk123 as code owners January 10, 2019 15:05

smowton requested a review from chrisr-diffblue January 10, 2019 15:06

smowton changed the title ~~JBMC: enable model and SSA equation~~ JBMC: enable model and SSA equation verification Jan 10, 2019

tautschnig reviewed Jan 10, 2019

View reviewed changes

smowton force-pushed the smowton/feature/jbmc-validation branch from 88c3751 to 6db4c22 Compare January 10, 2019 15:20

chrisr-diffblue approved these changes Jan 10, 2019

View reviewed changes

smowton added 2 commits January 14, 2019 15:48

Don't validate Java symbols' base names for now

738fbde

They use a different pattern to that expected for C programs, and changing that will have some impact. For now let's make validation practically usable without making a change with potentially widespread impact.

Revert "strengthen assignment type consistency"

555ff9a

This reverts commit caae4ce. Reverting because we can't currently meet either the weak (base_type_eq) or the strong (==) consistency requirement. Let's target the weak one first.

smowton force-pushed the smowton/feature/jbmc-validation branch from 6db4c22 to 6274264 Compare January 14, 2019 15:51

smowton added 6 commits January 14, 2019 16:29

Add name to namespace parameter

03277d6

Enable model validation in all JBMC regression tests

5867785

DECL VCCs: don't check non-existent SSA-rhs

0f1abe1

DECL clauses do not give an RHS, so comparing its type against the LHS is meaningless (and always fails).

Equation validation: use base_type_eq on types, not exprs

d53bf4b

The expr version expects two like-structured expressions and validates subexpressions pairwise, which is not the expected situation for VCCs.

JBMC: enable SSA equation validation in all regression tests

b2fe035

Pacify clang-format

4232b15

Adding an include in a prior commit --> I must sort the other ones, apparently :)

smowton force-pushed the smowton/feature/jbmc-validation branch from 32bf0cf to 4232b15 Compare January 14, 2019 16:29

tautschnig approved these changes Jan 14, 2019

View reviewed changes

tautschnig mentioned this pull request Jan 14, 2019

Replace all uses of deprecated symbol_exprt constructors [blocks: #3768] #3766

Merged

3 tasks

allredj reviewed Jan 14, 2019

View reviewed changes

tautschnig assigned peterschrammel Jan 14, 2019

peterschrammel approved these changes Jan 14, 2019

View reviewed changes

peterschrammel assigned smowton and unassigned peterschrammel Jan 14, 2019

smowton merged commit 9129e09 into diffblue:develop Jan 14, 2019

JBMC: enable model and SSA equation verification #3747

JBMC: enable model and SSA equation verification #3747

Uh oh!

Conversation

smowton commented Jan 10, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jan 10, 2019 • 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!

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jan 14, 2019

Uh oh!

tautschnig commented Jan 14, 2019

Uh oh!

smowton commented Jan 14, 2019

Uh oh!

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

Uh oh!

chrisr-diffblue Jan 10, 2019 •

edited

Loading