Costless by clause in `assert .. by { }` when using --isolate-assertions

[keyboardDrummer]

trafficstars

Given a program:

// --isolate-assertions

method Foo() {
 assert E by { X };
 assert F;
}

The SMT input for proving assert F should be the same as for the program

// --isolate-assertions

method Foo() {
 assert E;
 assert F;
}

Implementation hints

by clauses are implemented by translating

assert E by { X }; 
assert F;

to

if (*) { 
  X; 
  assert E; 
  assume false; 
} 
assume E; 
assert F;

which is then passified into

label Root:
  goto If, AfterIf;

label If:
  X;
  assert E;
  assume false;

label AfterIf:
  assume E; 
  assert F;

When we use --isolate-assertions and try to prove a particular assertion, we can drop any goto targets that do not lead to that assertion, so the above would simplify to:

label Root:
  goto AfterIf;

label AfterIf:
  assume E; 
  assert F;

Which can then be simplified to:

assume E;
assert F;

[MikaelMayer]

I think that you mean:

// --isolate-assertions

method Foo() {
 assert E by { X }; // Here the X should be dropped if we only want to prove F.
assert F;
}

[keyboardDrummer]

I think that you mean:

// --isolate-assertions

method Foo() {
 assert E by { X }; // Here the X should be dropped if we only want to prove F.
assert F;
}

Agreed, updated.

[keyboardDrummer]

Upon further investigation: the current splitting implementation already tries to remove blocks that do not contain any assert statements. The only remnants of an unused if is an extra block and jump:

The Boogie program:

procedure Foo()
{
  if (*) { 
    assert 2 == 1 + 1; 
    assume false; 
  } 
  assume 2 == 1 + 1; 
  assert {:split_here} 3 == 2 + 1;
}

Turns into this when processing the split assert:

implementation Foo()
{
  anon0:
    goto anon3_Else;

  anon3_Else:
    assume 2 == 1 + 1;
    assert {:split_here} 3 == 2 + 1;
    goto ;
}