Please help me understand the VC and SMT-LIB output generated by Boogie

May 13, 2014 at 3:54 AM
Hello, I'm trying to understand the proof obligations sent by Boogie to the prover.

For example a simple Boogie program:
procedure Foo(x:int) 
{
  assert x>0;
}
produces the following VC
(Let anon0_correct = (Implies (Label +23 true) 
                              (And (Label @39 (> x 0)) 
                                   (Implies (> x 0) true))),    
     PreconditionGeneratedEntry_correct = (Implies (Label +29 
                                                           true)
                                                 anon0_correct) 
 PreconditionGeneratedEntry_correct)
and the following SMT-LIB script:
...
(check-sat)
(labels)
(assert %lbl%@39)
(check-sat)
(pop 1)
Qs:
  1. What are the Label @xxx and Label +yyyy terms?
  2. What is the "labels" command? I couldn't find it anywhere in the SMT-LIB manual
May 13, 2014 at 1:42 PM
Hi snedurni

These are legacy things from the days of the Simplify theorem prover. I do not understand what they do, and I don't think they are standard SMT. They relate to how error traces can be extracted from the SMT model.

You can pass /doNotUseLabels to Boogie to make it turn them off and do something else instead for error reporting. This is what we do in GPUVerify.

Ally

On 13/05/2014 03:54, snedunuri wrote:

From: snedunuri

Hello, I'm trying to understand the proof obligations sent by Boogie to the prover.

For example a simple Boogie program:
procedure Foo(x:int) 
{
  assert x>0;
}
produces the following VC
(Let anon0_correct = (Implies (Label +23 true) 
                              (And (Label @39 (> x 0)) 
                                   (Implies (> x 0) true))),    
     PreconditionGeneratedEntry_correct = (Implies (Label +29 
                                                           true)
                                                 anon0_correct) 
 PreconditionGeneratedEntry_correct)
and the following SMT-LIB script:
...
(check-sat)
(labels)
(assert %lbl%@39)
(check-sat)
(pop 1)
Qs:
  1. What are the Label @xxx and Label +yyyy terms?
  2. What is the "labels" command? I couldn't find it anywhere in the SMT-LIB manual

May 13, 2014 at 10:50 PM
hello Ally, you wrote "You can pass /doNotUseLabels to Boogie to make it turn them off and do something else instead for error reporting. This is what we do in GPUVerify."
I tried this but it had no effect. I also tried setting errorTrace to 0 and that had no effect either. BTW, the flag doNotUseLabels is mentioned nowhere in the Boogie help documentation

thanks
May 21, 2014 at 6:59 PM
On 13/05/2014 22:50, snedunuri wrote:

From: snedunuri

hello Ally, you wrote "You can pass /doNotUseLabels to Boogie to make it turn them off and do something else instead for error reporting. This is what we do in GPUVerify."

Hmm, I find that surprising. Are you compiling Boogie from source?

I tried this but it had no effect. I also tried setting errorTrace to 0 and that had no effect either. BTW, the flag doNotUseLabels is mentioned nowhere in the Boogie help documentation

Indeed; many Boogie options are not documented. It would be great if we could have a concerted effort sometime to document these things. I am not in a position to lead such an effort, but would happily contribute to it.

Cheers

Ally


thanks

May 29, 2014 at 2:22 AM
Hmm, I find that surprising. Are you compiling Boogie from source?
Yes, I built it in Visual Studio.
Actually, I'll modify my previous comment somewhat. Its not that the flag has no effect. It just has no useful effect. it does NOT remove labels from the output formula. Rather it adds a peculiar label called ControlFlow. Here's a fragment:
(assert (not
(=> (= (ControlFlow 0 0) 58) (let ((anon0_correct (=> (and %lbl%+50 true) (=> (= z@0 (F x@@0)) (and
(or %lbl%@80 (=> (= (ControlFlow 0 50) (- 0 80)) (> z@0 0))) (=> (> z@0 0) true))))))
...
As you can see the labels are still very much there