Feature: Add LTL time step specifications to Boogie input files

[martin-neuhaeusser]

While the C front end does support the definition of LTL time steps by calling the special function __VERIFIER_ltl_step(), similar functionality seems to be missing for bare Boogie input files.

With this patch, one can label assume, assert, and call statements in Boogie input files with a parameterless attribute ltl_step. The Boogie preprocessor then attaches internal LTLStepAnnotation labels to the respective nodes, thereby making the step specification available to the Büchi product generator.

Goal of this PR is to support LTL time step boundaries via inserting assume {: ltl_step } true statements at the appropriate control flow locations.

[Heizmann]

Thanks! I have to discuss the next step operator with Daniel and Vincent before I can say something. However, I might not find enough time for that Today.

[martin-neuhaeusser]

No worries. It is not really urgent.

The background for this PR is that we would like to do LTL model checking on Boogie models that we generate; but we need some way to precisely define when a time step occurs within the Boogie source files. Please see this PR only as a proposal how it could be done.

[maul-esel]

You could also try wrapping the individual steps in atomic blocks (see here for some explanation and an example), IIRC that should have a similar effect for LTL. Though I am unsure if it's as powerful as the proposed annotations; the code that can appear inside an atomic block is limited (no loops, possibly no procedure calls except if they are inlined, ...)

[martin-neuhaeusser]

Thanks for pointing out the atomic block feature! I was not aware of that. Reading the explanation, I fear that this will not be sufficient (I will experiment with it to verify). Our intention is to generate a time step only at specific points in the program execution (something like a big-step semantics). The models are large and we generally will not be able to impose restrictions (e.g. no branching, no function calls, no loops) on the statements that can execute within one time steps.

An (artificial) example that I used to test is

var a : int;
var b : int;

procedure ULTIMATE.start() returns ()
modifies a, b;
{
    a := 1;
    while (true) {
          havoc a;
          b := a;
          b := b;
          assume {: ltl_step } true;
    }
}

//#Safe
// #LTLProperty: [](AP(a == 1) ==> X(AP(a + b == 3)))

I will try to see if that example can be expressed using atomic blocks and how Ultimate Automizer deals with it.

[Langenfeld]

Thanks! I have to discuss the next step operator with Daniel and Vincent before I can say something.

On the BüchiProduct side, this should work fine. But I am not sure of the interaction with large bock encoding though (e.g. loop free blocks with several assumes with the ltl annotation).

[martin-neuhaeusser]

@Langenfeld I was assuming that LBE is applied after product construction is complete. Is that right? If applied at that stage, I am running into problems with more aggressive LBE settings. The reason is that the step annotations are preserved on the product automaton. When LBE merges two locations that are labeled with an instance of LTLStepAnnotation, it tries to combine the two annotations into one. That fails (I guess rightfully) with an exception. As I suspect that the step annotations are no longer needed once the product construction is finished, I thought about removing all step annotations in a final pass after product construction. In that way, LBE should remain unaffected. But I am not sure about the step annotations that the C front end introduces and did not want make too intrusive changes or break anything.

[Langenfeld]

@martin-neuhaeusser Sorry, yes, it runs after the product generation (and therefore does not have any negative effect in that case).

[martin-neuhaeusser]

A general issue with the combination of block encoding and LTL model checking that I observed:

LTLStepAnnotations are preserved throughout the toolchain. If you apply large block encoding after the product construction, lbe tries to merge edges that have LTLStepAnnotations. During the merge operation, it attempts to also merge successive LTLStepAnnotations, which raises an exception. However, this bug is independent of the changes proposed in this PR, i.e. it can be reproduced on C files via the CACSL front end on the current dev branch, too.

My naive proposal is to remove LTLStepAnnotations during the product construction as done in PR #587 (commit 2e35eee)

[Heizmann]

The CACSL front end writes the LTLStepAnnotations directly to the nodes of the Boogie AST. I think this is a rather unwanted workaround because it disallows us to reproduce verification problems by dumping them as Boogie files. The LTLStepAnnotation is however (to the best of my knowledge) our desired way to store the step information in a control flow graph. So an option might be to translate the assume {: ltl_step } true; only to an LTLStepAnnotation (i.e., drop the assume true) while building the control flow graph.

I am not absolutely sure, I want to discuss this and related things (e.g., the mentioned bug) with Daniel first. But unfortunately I won't find time this week.

[martin-neuhaeusser]

@Heizmann Yes, currently the CACSL annotates the assume(true) statements with an LTLStepAnnotation directly. That works but has the downside that these annotations cannot be represented once the resulting Boogie file is output. In that sense, the current approach of annotating LTL steps in CACSL suffers the same problem that we are facing, namely that Boogie is missing a means to represent LTL step annotations.

The proposal of this PR is to introduce a new attribute "ltl_step" that is interpreted by the Boogie preprocessor such that it annotates Boogie statements that bear the "ltl_step" attribute also with a corresponding LTLStepAnnotation. If we may assume that the Boogie models generted by the CACSL2BoogieTranslator are always fed into the Boogie Preprocessor, one can attach this "ltl_step" attribute to the assume(true) statements instead of adding the LTLStepAnnotation. I added this in commit 0cc1a44

Given the simple C program

//#Unsafe
//@ ltl invariant positive: [](AP(a==1) ==> X(AP(a==2)));

extern void __VERIFIER_ltl_step() __attribute__ ((__noreturn__));

int a, x = 5;

int main()
{
	x = 99;
	a = 1;
	__VERIFIER_ltl_step();
	a = 1;
	a = 2;
	__VERIFIER_ltl_step();
	a = 6;
	__VERIFIER_ltl_step();
	x = 0;
        a = 1;
	__VERIFIER_ltl_step();
        a = 2;
        a = 9;
}

the current approach results in the following Boogie model after Boogie preprocessing (the LTL steps are not represented):

implementation ULTIMATE.init() returns (){
  $Ultimate##0:
    ~a~0 := 0;
    ~x~0 := 5;
    return;
}

implementation ULTIMATE.start() returns (){
    var #t~ret0 : int;

  $Ultimate##0:
    call ULTIMATE.init();
    call #t~ret0 := main();
    return;
}

implementation main() returns (#res : int){
  $Ultimate##0:
    ~x~0 := 99;
    ~a~0 := 1;
    assume true;
    ~a~0 := 1;
    ~a~0 := 2;
    assume true;
    ~a~0 := 6;
    assume true;
    ~x~0 := 0;
    ~a~0 := 1;
    assume true;
    ~a~0 := 2;
    ~a~0 := 9;
    return;
}

var ~a~0 : int;

var ~x~0 : int;

procedure __VERIFIER_ltl_step() returns ();
modifies ;

procedure main() returns (#res : int);
modifies ~x~0, ~a~0;

procedure ULTIMATE.init() returns ();
modifies ~a~0, ~x~0;

procedure ULTIMATE.start() returns ();
modifies ~x~0, ~a~0;

With this patch, the output looks as follows:

implementation ULTIMATE.init() returns (){
  $Ultimate##0:
    ~a~0 := 0;
    ~x~0 := 5;
    return;
}

implementation ULTIMATE.start() returns (){
    var #t~ret0 : int;

  $Ultimate##0:
    call ULTIMATE.init();
    call #t~ret0 := main();
    return;
}

implementation main() returns (#res : int){
  $Ultimate##0:
    ~x~0 := 99;
    ~a~0 := 1;
    assume { :ltl_step } true;
    ~a~0 := 1;
    ~a~0 := 2;
    assume { :ltl_step } true;
    ~a~0 := 6;
    assume { :ltl_step } true;
    ~x~0 := 0;
    ~a~0 := 1;
    assume { :ltl_step } true;
    ~a~0 := 2;
    ~a~0 := 9;
    return;
}

var ~a~0 : int;

var ~x~0 : int;

procedure __VERIFIER_ltl_step() returns ();
modifies ;

procedure main() returns (#res : int);
modifies ~x~0, ~a~0;

procedure ULTIMATE.init() returns ();
modifies ~a~0, ~x~0;

procedure ULTIMATE.start() returns ();
modifies ~a~0, ~x~0;

Besides representing LTL step information in the Boogie files, the attached attribute has the additional advantage that the RCFGBuilder does not remove assume(true) statements with attributes. Hence, it renders it safe to use its Remove assume true statements option even in presence of LTL steps.

[Heizmann]

I added some information about the LTL step annotation to our wiki: https://github.com/ultimate-pa/ultimate/wiki/Boogie#ltl-specifications https://github.com/ultimate-pa/ultimate/wiki/Boogie/3c5f3fb67d0df1af1969309f230981749f94f318