boogie-org / boogie Goto Github PK

Boogie

Home Page: http://research.microsoft.com/en-us/projects/boogie/

License: MIT License

C# 17.13% Makefile 0.01% Python 0.05% TeX 0.02% Batchfile 0.01% Shell 0.01% Vim Snippet 0.04% Boogie 82.72% Vim Script 0.02% Lean 0.02%

boogie's People

Stargazers

Watchers

Forkers

delcypher richardlford checkmate50 diepbp iijin tsakur hertzel001 lleraromero bacelar frothenberger chubbymaggie vrnithinkumar subhajitroy qunyanm rohitjha sunjun-group plaidfinch graydon barrybo vincentjzimmer pramod ismailkuru pombredanne wilcoxjay pramodsu shaobo-he epfl-lara yanntm stephenfreund xujiesi yuepeng-wang wuestholz zjlavender lijiaying xurongchen seanmcl mschlaipfer channgo2203 amaurremi txiang61 ck624 marcoeilers soroushe barrettcw stdvivi yahyazadeh suhaorhun alexanderjsummers rustanleino cbarrettfb c0de3 keram88 blauj parashar-gaurav rospoly dddejan sethpoulsen jaylorch zvonimir jingmeihu keyboarddrummer charlyb123 cyjseagull emmazzz dipakc smh0960 gauravpartha stjordanis yoni206 beillahi ying1123 wrwg parno emptylambda kbansal mewbak typersniper tigerzz88 kryptine robin-aws seebees lambda2023 dataronio atomb bobismijnnaam uq-pac arminvakil linusboyle anjiang-wei plsyssec dargones linpelvis seanpm2001 chuyuesun nkolotov mayanksolanki393 zafer-esen jialong-zhu namrathag jamestiotio

boogie's Issues

Specifying procedure name with /proc

I want to check only some specific procedures in a boogie file. When I try to use the /proc:abc option Boogie verifies all the procedures which contain the string "abc" in their names.
I am running Boogie on Ubuntu-14.04.

mono /path/to/Binaries/Boogie.exe /proc:"abc" /trace /traceTimes test.bpl

Above command even verifies procedures with names "abcd" , "function_abc" , etc. How can I verify some specific procedure?

Contributing to boogie

Hello,

I want to contribute to this project, how do I get started?

Also, is there some IRC channel where discussions happen?

Rename Model/Core DLLs

I would like to rename the DLLs Model.dll and Core.dll to BoogieModel.dll and BoogieCore.dll. I need these DLLs to have less generic names, for easy telemetry when we deploy as part of the Static Driver Verifier.

Would there be any objections to this? I'll go ahead in a few days if I don't any hear objections.

Boogie generates invalid assert command

When I run the latest version of Boogie (8e5a035) with Z3 4.4.1 on this example program:

function {:identity} Lit<T>(x: T) : T;
axiom Lit(true);

procedure test()
{
    assert false;
}

Z3 (via Boogie) reports "Prover error: line 94 column 29: invalid assert command, term is not Boolean"

The line in question is "(assert (Lit (bool_2_U true)))", which appears to need a call to U_2_bool around the call to Lit.

crlf issues in git

Git is a bit unix-centric and tends to get confused by carriage returns in files. The result is you get whole-file diffs when editing on different platforms because one version has crlf line endings and one version has lf line endings. This makes branching and merging impossible. I would suggest adding this line to the file .gitattributes in the main directory:

text=auto

If you do this git will check out files with the appropriate line endings for your platform but check them in in some standard way (I think in unix style). I also think this will update the whole repository once to make the line endings standard.

Or if you want crlf always, even on unix/mac, then use this:

text eol=crlf

I think either is OK but the default behavior creates a mess when you edit on both unix and windows.

Crash in ProverInterface when using AbstractHoudini

Here is a small example causing this crash:

function {:existential true} b0(x:bool): bool;

var g: [int]int;
var g1: [int]int;

procedure main()
ensures b0(g == g1);
{}

Invoked command:

boogie.exe /doModSetAnalysis test.bpl /contractInfer /printAssignment /abstractHoudini:PredicateAbs /noinfer /inlineDepth:1

Akash helped in figuring out what is happening here. AbsHoudini tries to evaluate the value of the predicate; so it sends the following to the theorem prover:

(get-value ((= g g1)))

Z3 returns:

{(() (() (= g g1) true))}

Saying that the value is true. But the following method in ProverInterface isn't able to parse this string and crashes:

public override object Evaluate(VCExpr expr)

The fix would be to correct the parsing routine, but we don't understand this well enough. And we don't know why Z3 didn't just say "(true)" in the first place.

Equivalent expression fails assert

I am trying to zero a page. The first ensure below passes an assert, but the second does not. I may be missing something, but I thought to pass it on.

ensures (forall a : bv8 :: a[8:4] == page ==> mem[a] == 0bv8);
ensures (forall low : bv4 :: mem[page ++ low] == 0bv8);

Test code with come comments and context is below.

This is Boogie 2.3.0.61016 on Mono 3.2.8 on Debian 3.2.8+dfsg-10.

--Michael

/* Memory is an 8 bit address space of bytes.
Providing 2^4 = 16 'pages' of 16 bytes each.
*/

type Byte = bv8;
type Addr = bv8;
type Ram = [Addr] Byte;
type Page = bv4;

var mem : Ram;

/* Zero a page, leave others unchanged. */
procedure zeroPage(page : Page);
modifies mem;
// Zero bytes of page
// First version passes assert below, it 'mirrors' the ensures for unchanged.
// Second version fails it.
//ensures (forall a : Addr :: a[8:4] == page ==> mem[a] == 0bv8);
ensures (forall low : bv4 :: mem[page ++ low] == 0bv8);

// Other pages unchanged.
ensures (forall a : Addr :: a[8:4] != page ==> mem[a] == old(mem)[a]);

procedure hv()
modifies mem;
{
call zeroPage(2bv4);

// test page is zeroed
assert (forall a: Addr :: a[8:4] == 2bv4 ==> mem[a] == 0bv8);
}

AbsHoudini tests need to be enabled and fixed

The tests in Test/AbsHoudini are currently disabled because some of them are broken. This is bad because we aren't tracking regressions introduced for this feature.

UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32)
UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32)
UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32)
UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32)
FAIL: Boogie :: AbsHoudini/quant3.bpl (24 of 32)
FAIL: Boogie :: AbsHoudini/quant5.bpl (25 of 32)

The the lit.local.cfg file needs to removed from the directory and then those tests need to be fixed.

Problems updating to the latest release of Z3

Team Z3 released version 4.5.0 last week, containing a bunch of bug fixes and improvements. It would be great for Boogie to keep tracking Z3 if possible. We tried this update on our end, but we are encountering many unexpected results in Boogie regressions. It seems that this problem has something to do with model extraction in Boogie.
We (meaning team SMACK) would greatly appreciate if a Boogie expert could take a look at this. Thanks!

Make Z3 4.4.1 the recommended version?

Is there any reason for not making Z3 4.4.1 the recommended version? There are just minor differences in the output of two test cases (livevars/daytona_bug2_ioctl_example_2.bpl and test15/CaptureState.bpl). In one case the model is slightly different and in the other case the trace is slightly different (for a STORM-generated file that supposedly has quite some non-determinism due to thread interleavings).

Adding a Floating-Point Type

Boogie Team,

I'm Dietrich Geisler, and undergraduate student working for Dr. Zvonimir Rakamaric at the University of Utah. Over the last year, I have worked on adding the floating point type to boogie based on the floating point update to z3.

The merge I am proposing adds the floating point type to boogie, allowing variables and constants to be declared as described below. There are several issues with my implementation that I have listed. I'm sure that there are more issues and bugs I haven't found, so if you find any issues, please let me know.

Syntax Documentation

Declaring Variables:

The syntax for declaring a floating point variable is as follows:
var name: float(exp man);
Where exp is the size of the float exponent and man is the size of the float mantissa

It is also acceptable to use the following syntax:
var name: float();
This syntax assumes the float exponent to be size 8 and the mantissa to be size 24

example:
var x: float(11 53)
Declares a variable called x with a exponent sized 11 and mantissa sized 53

Declaring Constants:

All of the following syntax are viable for declaring a floating point constant:
float(dec)
float(exp_val man_val)
float(dec exp man)
float(exp_val man_val exp man)

Where dec is the decimal value of the constant,
exp_val/man_value are the integer values of their respective fields,
And exp/man are the sizes of their respective fields.
Note that when exp and man are not specified, they are given sizes 8 and 24 respectively

Defined Operations:

Given two floating point values x and y with the same size of exponent and mantissa
The following operations operate as defined in Operators section of this document:
http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
(Note that rounding mode is always assumed to be Round to Nearest Even (RNE))
(Also note that operations not listed here are undefined)

operatation boogie syntax
neg(x) -x
add(x, y) x + y
sub(x, y) x - y
mul(x, y) x * y
div(x, y) x / y
leq(x, y) x <= y
lt(x, y) x < y
geq(x, y) x >= y
gt(x, y) x > y
eq(x, y) x == y

Other:

The following special values can be declared with the following syntax:
Value Declaration
NaN fp(nan exp man)
+oo fp(oo exp man) OR fp(INF exp man)
-oo fp(-oo exp man) OR fp(INF exp man)
-zero fp(-zero exp man)
Where exp and man are the sizes of the exponent and mantissa respectively

Known Issues:

There is currently no way to convert from a floating point to any other data type

There is currently no way to convert the value of a variable to a floating point type
For example, the following statements fails:
var x : real;
fp(x);

Statements of the following form cause a parser error (parenthesis followed by fp constant)
... (fp(1) + fp(1));

Attempts by Boogie to infer the behavior of loops fail when floating points are involved

Describing loop behavior manually is untested (using loop unroll appears to work)

Details/Question: I primarily modified Absy, AbsyExpr, Parser, VCExpr, VCExprAST, TypeErasure, and SimplifyLikeLineariser. I also added the file BigFloat.cs, allowing creation of float instances internally. Note in particular that I modified the Parser manually; if this is incorrect or if you notice any poor or unmaintainable implementation choices, please let me know. I would be glad to make any changes to improve performance, accuracy, or code design.

Feel free to comment below or contact me at [email protected] if you have any concerns, suggestions, or questions. Thank you for your time, and I hope this update proves valuable to the boogie community.

Best Regards,
Dietrich Geisler

Boogie crash involving floating point variables

Boogie crashes on the following input:

type Ref;
var Heap: HeapType;
type Field A B;
type HeapType = <A, B> [Ref, Field A B]B;

procedure mfl(one: float23e11, two: float23e11) returns ()
{
  assert two == one; 
}

The problem disappears if the Heap variable is removed, the type parameters of HeapType are removed, the assertion is removed or if the parameters of mfl have types other than floats.

I get the following stack trace:

[ERROR] FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.Diagnostics.Contracts.ContractException: Assertion failed.
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailureImplementation (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab7736b0 + 0x00057> in <filename unknown>:0 
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailure (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab773040 + 0x00020> in <filename unknown>:0 
  at System.Diagnostics.Contracts.Contract.ReportFailure (ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab772e50 + 0x0006a> in <filename unknown>:0 
  at System.Diagnostics.Contracts.Contract.Assert (Boolean condition) <0x7f7cab7725b0 + 0x0001f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Type2Term (Microsoft.Boogie.Type type, IDictionary`2 varMapping) <0x41cf1e70 + 0x002ca> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.GenVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType, IDictionary`2 varMapping) <0x41cf1c40 + 0x00053> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.AddVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType) <0x41d224e0 + 0x00073> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Typed2Untyped (Microsoft.Boogie.VCExprAST.VCExprVar var) <0x41d223b0 + 0x000a7> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprVar node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0e4b0 + 0x00067> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprVar.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0c3c0 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArgumentsToOldType (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d1d000 + 0x0005b> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitFloatEqOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d22370 + 0x0001b> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprBinaryFloatOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21c80 + 0x00469> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArguments (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.Type argType, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e190 + 0x00053> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitLabelOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21b30 + 0x00037> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprLabelOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21ad0 + 0x00041> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d1ca10 + 0x000f7> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d8a0 + 0x00165> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprLet node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21700 + 0x00297> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprLet.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d216a0 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Erase (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d07550 + 0x0005b> in <filename unknown>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.VCExpr2String (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d06b50 + 0x00237> in <filename unknown>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d04020 + 0x00287> in <filename unknown>:0 
  at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d03950 + 0x000c4> in <filename unknown>:0 
  at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, Int32 no, Int32 timeout) <0x41cfd000 + 0x007e3> in <filename unknown>:0 
  at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) <0x41ccf1d0 + 0x018eb> in <filename unknown>:0 
  --- End of inner exception stack trace ---
  at System.AggregateException.Handle (System.Func`2 predicate) <0x7f7cab717f40 + 0x0016c> in <filename unknown>:0 
  at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, System.String programId, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId) <0x41cb80e0 + 0x01236> in <filename unknown>:0 
  at Microsoft.Boogie.ExecutionEngine.ProcessFiles (System.Collections.Generic.List`1 fileNames, Boolean lookForSnapshots, System.String programId) <0x41c7c000 + 0x0095b> in <filename unknown>:0 
  at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) <0x41c6a930 + 0x00703> in <filename unknown>:0 
---> (Inner Exception #0) System.Diagnostics.Contracts.ContractException: Assertion failed.
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailureImplementation (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab7736b0 + 0x00057> in <filename unknown>:0 
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailure (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab773040 + 0x00020> in <filename unknown>:0 
  at System.Diagnostics.Contracts.Contract.ReportFailure (ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab772e50 + 0x0006a> in <filename unknown>:0 
  at System.Diagnostics.Contracts.Contract.Assert (Boolean condition) <0x7f7cab7725b0 + 0x0001f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Type2Term (Microsoft.Boogie.Type type, IDictionary`2 varMapping) <0x41cf1e70 + 0x002ca> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.GenVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType, IDictionary`2 varMapping) <0x41cf1c40 + 0x00053> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.AddVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType) <0x41d224e0 + 0x00073> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Typed2Untyped (Microsoft.Boogie.VCExprAST.VCExprVar var) <0x41d223b0 + 0x000a7> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprVar node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0e4b0 + 0x00067> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprVar.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0c3c0 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArgumentsToOldType (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d1d000 + 0x0005b> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitFloatEqOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d22370 + 0x0001b> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprBinaryFloatOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21c80 + 0x00469> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArguments (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.Type argType, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e190 + 0x00053> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitLabelOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21b30 + 0x00037> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprLabelOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21ad0 + 0x00041> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d1ca10 + 0x000f7> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d8a0 + 0x00165> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprLet node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21700 + 0x00297> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.VCExprLet.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d216a0 + 0x00039> in <filename unknown>:0 
  at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0 
  at Microsoft.Boogie.TypeErasure.TypeEraser.Erase (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d07550 + 0x0005b> in <filename unknown>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.VCExpr2String (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d06b50 + 0x00237> in <filename unknown>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d04020 + 0x00287> in <filename unknown>:0 
  at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d03950 + 0x000c4> in <filename unknown>:0 
  at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, Int32 no, Int32 timeout) <0x41cfd000 + 0x007e3> in <filename unknown>:0 
  at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) <0x41ccf1d0 + 0x018eb> in <filename unknown>:0 <---

Erasing errordata branch

It seems to me that we can erase this branch. @qunyanm could you please confirm this? Thanks!

Debugging support in Boogie

I am working on a project using Boogie for verifying distributed applications. In my work I am in need of a better debugging support when a verification fails.

I browsed through the command line options and have found the following options useful in my context:

\mv
\z3multipleErrors
\break
I tried them and have some issues/questions.

I will try to explain my issue through a trivial example. Below is a Boogie specification for incrementing a counter.

counter.bpl :::

var counter: int;
procedure increment(value: int)
modifies counter;
ensures (counter >= 0);
{
  assume(counter >= 0);
  counter := counter + value;
}

I am executing the command line as follows : Boogie.exe /z3multipleErrors /mv:counter.model counter.bpl

The result is :

Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
counter.bpl(10,1): Error BP5003: A postcondition might not hold on this return path.
counter.bpl(5,1): Related location: This is the postcondition that might not hold.
Execution trace:
    counter.bpl(7,3): anon0

Boogie program verifier finished with 0 verified, 1 error

and the model is :

counter.model:::

*** MODEL
%lbl%@82 -> false
%lbl%+37 -> true
%lbl%+45 -> true
counter -> 0
counter@0 -> (- 1)
value -> (- 1)
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
*** END_MODEL

The counter example in this case is when the value to be incremented is -1 when counter is 0. But I would like to have more counter examples. So I have two questions here :

I expected the /z3multipleErrors option to give me multiple counter examples, in this particular case something like [counter = 0 & value = -1, -2, -3,..], [counter = 1 & value = -2, -3, ...] etc. Then I plan to use the set of values to get insights into the error, in this case value is negative. Am I missing something here?
Is the counter example the "minimal counter example"? I know this case is a trivial example, but I wish to know if I always get a minimal counter example.
Suppose I have a linked list which I am checking whether it is linear. As a counter example, I can have the following results:
1 -> 1 or 1 -> 2 -> 3 -> 4 ..... -> 1
Both are ideally counter examples, but the first one is a minimal counter example.

Now coming to the next stage of my issue.
The counter example is pretty comprehensible when the data types involved are simple. When I use maps or nested maps like below, the counter examples generated run into several pages and it is tiresome to try to understand it. I am giving a trivial example of a 2D matrix which has a constraint that all its elements should be non-negative.

matrix.bpl:::

var matrix: [int][int]int;
procedure modify(row:int, column:int, value: int)
modifies matrix;
ensures (forall r, c:int :: matrix[r][c] >= 0);
{
  assume(forall r, c:int :: matrix[r][c] >= 0);
  matrix[row][column] := matrix[row][column] + value;
}

matrix.model:::

*** MODEL
%lbl%@193 -> false
%lbl%+104 -> true
%lbl%+79 -> true
c@@0!0!0 -> 2
column -> 2
matrix -> |T@[Int][Int]Int!val!0|
matrix@0 -> |T@[Int][Int]Int!val!1|
r@@0!0!1 -> 1
row -> 1
value -> (- 563)
Store_[$int]$int -> {
  |T@[Int]Int!val!1| 2 (- 563) -> |T@[Int]Int!val!0|
  else -> |T@[Int]Int!val!0|
}
Select_[$int]$int -> {
  |T@[Int]Int!val!0| 2 -> (- 563)
  |T@[Int]Int!val!1| 2 -> 0
  else -> (- 563)
}
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
Select_[$int][$int]$int -> {
  |T@[Int][Int]Int!val!1| 1 -> |T@[Int]Int!val!0|
  |T@[Int][Int]Int!val!0| 1 -> |T@[Int]Int!val!1|
  else -> |T@[Int]Int!val!0|
}
Store_[$int][$int]$int -> {
  |T@[Int][Int]Int!val!0| 1 |T@[Int]Int!val!0| -> |T@[Int][Int]Int!val!1|
  else -> |T@[Int][Int]Int!val!1|
}
*** END_MODEL

Ideally the inference here should be the same as the non-negative counter above, ie, the value should be non-negative. But understanding that information from this counter example requires a lot of effort.

I have two questions in this context:

Is there any on going effort in making the counter example comprehensible for non-expert users? I have seen the BVD interface, but I felt it a small beautification of the plain text model.
The description of the \break flag looks promising, but I see it is not yet implemented. It would be useful to know the status of that. Is there some work in progress?

Thank you for taking your time out to read this lengthy report. I would appreciate any help, even if it only addresses a small part of the question.

--
Sreeja.

PS: I had tried to send this to the mailing list. I got a notice indicating the decision is with the moderator and it was a week back.

Parsing multiple programs concurrently

I recall that some time ago, I was not able to parse in multiple boogie programs because the Parser was populating static variables. That is not the case anymore. Does anyone know if it is safe to parse in multiple programs concurrently (with no synchronization)?

Discussing (and cleaning up) default options passed to Z3

By default, Boogie passes the following options to Z3 through queries:

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
(set-option :pp.bv_literals false)
(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.CASE_SPLIT 3)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)

I first used Boogie probably 10 years ago or so, and some of these options if I remember correctly were already there :). I wonder if it is time to revisit these given that Z3 changed a lot since then. Ideally, it would be good to let Z3 choose what the optimal setup should be by enabling AUTO_CONFIG.
Of course, such a change might break some regressions by causing time outs, but it might be a good move in the long run.
I should also add that these options are I think geared towards particular kinds of benchmarks (quantifier-heavy, etc.) and they are likely not a good setup for other usage scenarios. So I think that going with default Z3 options would be a good thing to do, while users can on top of that customize by adding options that are good for their benchmarks.
Thoughts?

Stack Overflow in LoopUnroll

Dear developers,

I am using the SMACK model checker, which is using Boogie internally and am currently facing a stack overflow in Boogie:

Stack overflow: IP: 0x7f254308adee, fault addr: 0x7fff12b2aff8
Stacktrace:
at System.Collections.Generic.List`1<T_REF>.GetEnumerator () [0x00000] in :0
<...>
at Microsoft.Boogie.LoopUnroll.Visit (Microsoft.Boogie.LoopUnroll/GraphNode) [0x000ff] in <774f387e8049413d8a81ca5a1242332e>:0
// The next line is repeated 26043 times
at Microsoft.Boogie.LoopUnroll.Visit (Microsoft.Boogie.LoopUnroll/GraphNode) [0x00138] in <774f387e8049413d8a81ca5a1242332e>:0
// The next line is repeated 17 times
at Microsoft.Boogie.LoopUnroll.Visit (Microsoft.Boogie.LoopUnroll/GraphNode) [0x00147] in <774f387e8049413d8a81ca5a1242332e>:0
at Microsoft.Boogie.LoopUnroll.UnrollLoops (Microsoft.Boogie.Block,int,bool) [0x000f1] in <774f387e8049413d8a81ca5a1242332e>:0
at Microsoft.Boogie.Program.UnrollLoops (int,bool) [0x00047] in <774f387e8049413d8a81ca5a1242332e>:0
at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program,Microsoft.Boogie.PipelineStatistics,string,Microsoft.Boogie.ErrorReporterDelegate,string) [0x000d7] in <29a4b16082574ed1951b1e8d97a5b624>:0
at Microsoft.Boogie.ExecutionEngine.ProcessFiles (System.Collections.Generic.List`1,bool,string) [0x00299] in <29a4b16082574ed1951b1e8d97a5b624>:0
at Microsoft.Boogie.OnlyBoogie.Main (string[]) [0x0025b] in :0
at (wrapper runtime-invoke) .runtime_invoke_int_object (object,intptr,intptr,intptr) [0x00054] in :0

Error invoking command:
boogie /home/vagrant/a-kB9U_7.bpl /nologo /noinfer /doModSetAnalysis /timeLimit:890 /errorLimit:1 /loopUnroll:100 /proverOpt:OPTIMIZE_FOR_BV=true /z3opt:smt.relevancy=0 /z3opt:smt.bv.enable_int2bv=true /boolControlVC
boogie returned non-zero.

Is it possible to identify the issue based on the stacktrace? I can run and submit additional debug output on demand, but because of NDAs I am unable to provide the input file in question.

Thank you for your help!

don't perform verification when there are 0 proof obligations

I have a large project that contains lots of very simple functions. I am consequently spending lots of my time waiting for things such as the following:

Verifying CheckWellformed$$_module.__default.NR__L1PTES ...
  [0.647 s, 0 proof obligations]  verified

Verifying CheckWellformed$$_module.__default.NR__L2PTES ...
  [0.717 s, 0 proof obligations]  verified

Verifying CheckWellformed$$_module.__default.reveal__smc__remove__premium ...
  [0.923 s, 0 proof obligations]  verified

Verifying CheckWellformed$$_module.__default.reveal__smc__mapSecure__premium ...
  [0.880 s, 0 proof obligations]  verified

It would be nice if Boogie could skip invoking the verifier if there are really no proof obligations.

Invoking Boogie with Spaces In Filenames

This is by no means a large issue, but it would be nice to enable spaces in filenames. If I have a Boogie program in a file called test space.bpl and I try to invoke Boogie on it, I get the error:

Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
*** Error: 'test': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).

Is there a reason why this is not currently supported? I've been developing on SMACK and have had an inquiry about this issue.

Inlining and variable capture

When Boogie inlines the spec of b inside foo, the bound variable "a" in ensures clause conflicts with the parameter "a" of foo. Is this a known bug/feature, and how to people get around it (e.g. obscure names of bound variables in quantifiers)?

For the following program foo.bpl

type ref;
var arr:[int]int;

procedure {:inline 1} b()
modifies arr;
ensures (forall a:int  :: {arr[a]} a < 10 ==> arr[a] == 0);
{
}
procedure foo(a:ref) 
modifies arr;
{
   call b();
}

When I generate the inlined version:
boogie /noVerify foo.bpl /printInstrumented > foo_1.bpl

and remove the first/last lines (Boogie verifier ...), then I get the following type checking error:

boogie /noVerify foo_1.bpl

Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
foo_1.bpl(40,19): Error: more than one declaration of variable name: a
foo_1.bpl(40,29): Error: trigger must mention all quantified variables, but does not mention: a
2 name resolution errors detected in foo_1.bpl

Multiple declarations of the same variable in a modifies clauses crashes boogie

Here is an example program:

type addr_t = bv32;
type map_t = [addr_t]int;

var mem : map_t;
var thing : [int]int;

procedure {:inline 1} do_something(a : addr_t, b : int)
  returns (mem_of_thing : int)

  modifies thing;
  modifies mem;
  modifies mem;
{
  var s : int;
  
  s := mem[a];
  mem[a] := b;
  
  mem_of_thing := thing[s];
}

procedure proof()
    modifies mem;
    modifies thing;
{
  var a : addr_t;
  var b : int;

  var m : int;

  call m := do_something(a, b);
  assert (m == thing[old(mem)[a]]);
}

This results in the error.

[ERROR] FATAL UNHANDLED EXCEPTION: System.ArgumentException: An item with the same key has already been added.
  at System.ThrowHelper.ThrowArgumentException (System.ExceptionResource resource) [0x0000b] in <f712f98eb8e445c8918edaf595bbe465>:0 
  at System.Collections.Generic.Dictionary`2[TKey,TValue].Insert (TKey key, TValue value, System.Boolean add) [0x0008e] in <f712f98eb8e445c8918edaf595bbe465>:0 
  at System.Collections.Generic.Dictionary`2[TKey,TValue].Add (TKey key, TValue value) [0x00000] in <f712f98eb8e445c8918edaf595bbe465>:0 
  at Microsoft.Boogie.Inliner.BeginInline (Microsoft.Boogie.Implementation impl) [0x00311] in <646a33ef60854832a600e48efca41b9b>:0 
  at Microsoft.Boogie.Inliner.InlineCallCmd (Microsoft.Boogie.Block block, Microsoft.Boogie.CallCmd callCmd, Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[T] newCmds, System.Collections.Generic.List`1[T] newBlocks, System.Int32 lblCount) [0x00044] in <646a33ef60854832a600e48efca41b9b>:0 
  at Microsoft.Boogie.Inliner.DoInlineBlocks (System.Collections.Generic.List`1[T] blocks, System.Boolean& inlinedSomething) [0x000c2] in <646a33ef60854832a600e48efca41b9b>:0 
  at Microsoft.Boogie.Inliner.ProcessImplementation (Microsoft.Boogie.Program program, Microsoft.Boogie.Implementation impl, Microsoft.Boogie.Inliner inliner) [0x00031] in <646a33ef60854832a600e48efca41b9b>:0 
  at Microsoft.Boogie.Inliner.ProcessImplementation (Microsoft.Boogie.Program program, Microsoft.Boogie.Implementation impl) [0x0000a] in <646a33ef60854832a600e48efca41b9b>:0 
  at Microsoft.Boogie.ExecutionEngine.Inline (Microsoft.Boogie.Program program) [0x00128] in <7673a55152514efb94ea15cd753604d2>:0 
  at Microsoft.Boogie.ExecutionEngine.ProcessFiles (System.Collections.Generic.List`1[T] fileNames, System.Boolean lookForSnapshots, System.String programId) [0x00281] in <7673a55152514efb94ea15cd753604d2>:0 
  at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) [0x0025b] in <dd98e9dc416d443a9a0695a903a5f9c7>:0

The problem is that we have two modifies mem clauses. It seems like this only happens for inlined procedures.

Declare new finite types

Hi guys,

Do you know how to declare a new finite type? It seems that the keyword "finite" isn't supported in the current version. I want to declare a new type Msg with exactly four constants M1, M2, M3, M4. I tried to use the following axiom to construct a finite type and boogie didn't show any error or warning.

type Msg;
const unique M1: Msg;
const unique M2: Msg;
const unique M3: Msg;
const unique M4: Msg;
axiom (forall m: Msg :: m == M1 || m == M2 || m == M3 || m == M4);

However, when I checked two below assertions, I received the error "Error BP5001: This assertion might not hold." Do you know how to eliminate this error? These assertions seem easy to prove because of the above axiom. I don't know why boogie can't.

const tMsg: Msg;
procedure Test()
{
	var tMsg1: Msg;
	havoc tMsg1;
	assert (tMsg1 == M1 || tMsg1 == M2  || tMsg1 == M3 || tMsg1 == M4);
	assert (tMsg == M1 || tMsg == M2  || tMsg == M3 || tMsg == M4);
}

I use Z3 v4.5.0 as a default SMT solver.

Thanks,
Thanh Hai

Boogie compilation errors under mono (without mono-develop)

Boogie does not compile (on OS X 10.10.3) using just mono (Mono JIT compiler version 4.0.1).

It gives the following compilation errors:

Errors:

/Users/utting/tools/boogie/boogie/Source/Boogie.sln (default targets) ->
(Build target) ->
/Users/utting/tools/boogie/boogie/Source/UnitTests/TestUtil/TestUtil.csproj (default targets) ->
/Library/Frameworks/Mono.framework/Versions/4.0.1/lib/mono/4.5/Microsoft.CSharp.targets (CoreCompile target) ->

ProgramLoader.cs(11,11): error CS0117: `NUnit.Framework.Assert' does not contain a definition for `IsNotNullOrEmpty'
ProgramLoader.cs(12,11): error CS0117: `NUnit.Framework.Assert' does not contain a definition for `IsNotNullOrEmpty'

 2 Warning(s)
 2 Error(s)

This seems to be because Source/UnitTests/TestUtil/ProgramLoader.cs calls the IsNotNullOrEmpty method, which is not supported under the NUnitLite framework, which is what comes standard with mono.
(mono-develop includes the full NUnit framework, so Boogie does compile within the IDE, but it should be possible to compile with just the command line mono, as the docs suggest.)

A possible fix is to change lines 11-12 of ProgramLoader.cs from:
Assert.IsNotNullOrEmpty (programText);
Assert.IsNotNullOrEmpty (fileName);
to:
Assert.IsNotNull(programText);
Assert.IsNotEmpty (programText);
Assert.IsNotNull(fileName);
Assert.IsNotEmpty(fileName);

Once this is done, boogie compiles correctly using the command line version of mono:
xbuild Source/Boogie.sln
...
51 Warning(s)
0 Error(s)

Thanks
Mark Utting

Declaration conflict between quantified variables and others

Consider the following Boogie program,

procedure foo(n:int)
{
  var q : int;
  assume n > 0 ==> (forall q: int :: q > 0);
}

Boogie will give the following warning,
test.bpl(4,27): Error: more than one declaration of variable name: q

Is this behavior expected given that the second q is bounded by a quantifier?

How Do I learn Boogie?

I'm interested in possibly using Boogie for a software verification project, but I'm having trouble understanding the language. I started going through the "This is Boogie 2" manual, but quickly began running into compatibility issues (yes, I did note the disclaimer in the README). But the language reference was never sufficient for me to resolve the problem. For instance, "This is Boogie 2" discusses finite type declarations using the "finite" keyword. Apparently this keyword no longer exists, but the language reference does not cover type declarations at all. So I was unable to figure out how to declare finite types.

So at the current project state, what is the quickest way to learn Boogie?

Weird logic when dealing with Z3 options

Recently, we observed that Boogie seems to silently drop Z3 options when they are passed to it using lower-case letters, as in /z3opt:smt.mbqi=true. We tracked this behavior to this interesting piece of logic that deals with Z3 options:

boogie/Source/Provers/SMTLib/Z3.cs

Line 374 in d93c222

 if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq))) 

It appears that the options are filtered based on whether the first character is a capital letter or not, which is very strange since Z3 options are case insensitive. For example, if Boogie is invoked with /z3opt:SMT.mbqi=true the option makes its way into the generated query, while if Boogie is invoked with /z3opt:smt.mbqi=true it is unclear what happens in that case, but the behaviors are not identical.
My hunch is that this might be legacy code that should be cleaned up, but I am not totally sure, and so help would be appreciated.

/trace output is less helpful than it could be due to buffering

Just a minor nitpick. When running Boogie with /trace, it produces output such as:

Verifying CheckWellformed$$_.foo ...
  [0.716 s, 2 proof obligations]  verified

Verifying Impl$$_.foo ...
  [187.421 s, 225 proof obligations]  verified

However, the line for "Verifying" only appears in the console window at the same time that the second line with the result information is printed, so you're never sure what Boogie is currently attempting to verify. I assume this could be fixed by adding an fflush()-equivalent between the two print statements.

This issue also applies to Dafny as dafny-lang/dafny#10

Linearity assumptions at parallel calls

Linearity assumptions are not (or not properly) injected at parallel calls. The attached test is a minimal example demonstrating the failure.

test.bpl.txt

Linux build error

Hi guys,

I'm trying to build Boogie on a linux machine while I got this error message,
mono ./nuget.exe restore Source/Boogie.sln
WARNING: The runtime version supported by this application is unavailable.
Using default runtime: v2.0.50727
Unhandled Exception: System.TypeLoadException: Could not load type 'NuGet.Program' from assembly 'NuGet, Version=2.8.60318.667, Culture=neutral, PublicKeyToken=null'.
[ERROR] FATAL UNHANDLED EXCEPTION: System.TypeLoadException: Could not load type 'NuGet.Program' from assembly 'NuGet, Version=2.8.60318.667, Culture=neutral, PublicKeyToken=null'.

I'm using mono version 2.10.8.1

Thanks,
Shaobo

Mozilla MXR site is down - who to contact?

I am kind of hoping that @delcypher would know the answer to this :).
Basically, this does not work

mozroots --import --sync

since the whole mxr Mozilla website seems to be down. Because of this, I am having trouble building Boogie on Linux. I just spent half an hour trying to figure out where to report this, without any success.
How should we go about this?

Switching Boogie build to .NET Standard/Core

Recently I started looking into how to improve the portability of Boogie across platforms, and in particular whether it can be compiled using Microsoft's dotnet core distribution for Linux. After reading a bit about various .NET implementations, it seems to me that it would be good to switch Boogie from .NET Framework v4.5 (which it currently requires) to something that is more portable, such as .NET standard/core. (Note that .NET Framework is not available on Linux from Microsoft, while .NET Core is - see https://www.microsoft.com/net/download/linux)

Based on my understanding, switching to .NET Standard/Core ought to be possible (and hopefully not too hard) since Boogie is a command line application that does not use GUI.

Note that I was quite confused about what the heck .NET Framework, Core, and Standard are, and this is a good place to start learning about this: https://msdn.microsoft.com/en-us/magazine/mt842506.aspx

Anyhow, I would like to start a discussion regarding this switch, and maybe get opinions and/or suggestions from people who understand the potential issues and how to go about this better.

Emacs mode

Hi all,

I've rewritten the Boogie mode from scratch, and it's on MELPA now. It comes with some support for completion, better syntax highlighting, support for tracing and launching the axiom profiler, real-time verification, and a few other goodies.

Are there objections to my pointing to that instead in the Util directory and removing the existing boogie-mode.el?

Clément.

polyhedra for linear inequalities not supported for abstract interpretation?

Hi,

I tried to invoke boogie with flag /infer:p while got an error message saying argument 'p' is not valid. I was wondering if it is still supported while the help message is not updated.

Thanks,
Shaobo

[civl] Commutativity check error messages contain no location information

Although the procedure names are included, tools such as the emacs mode cannot easily extract this information, which makes the the experience less enjoyable.

It would be nice if these errors contained filenames and line numbers like most other Boogie errors.

Help for Boogie Debugging Messages

boogie.txt
Hi all,

We use Boogie to prove our code holds our invariant. And we recently came across a verification failure. Attached is the boogie program.
The problematic part in boogie program is

// Caller_Dealloc Macro
procedure caller_dealloc() returns();
    //requires tmp != a;
    requires e[a] != e[b] && INV(e, dealloc, valid) && valid[e[b]];
    modifies e, dealloc, valid, ret;
    ensures (forall i:AVAR :: i != a && i != tmp ==> e[i] == old(e[i]));
    ensures (forall d:ADDR :: d != old(e[a]) && d != e[a] && d != e[tmp] ==> valid[d] == old(valid[d])); // validity invariant may not hold 
    ensures (forall i:AVAR :: i != a && i != tmp ==> dealloc[i] == old(dealloc[i]));
    ensures valid[e[a]];
    ensures dealloc[a];
    ensures INV(e, dealloc, valid);
implementation caller_dealloc() returns ()
{
    call pre_dealloc(a); // pre_dealloc(a)
    call ret := copy(b);
    e := e[tmp := ret]; // tmp:= ret
    dealloc := dealloc[tmp := false]; //tmp_dealloc := false
    call ret := reset_caller_func(tmp, false); // ret:=func(b, false);
    e := e[a := ret]; // a:=ret;
    //assert a != tmp;
    if(e[a] != e[tmp]){
        call freed(tmp);
    }
    dealloc := dealloc[a := true]; //a_dealloc := true
}

This procedure may not hold validity invariant, but could be fixed by adding ' a != tmp' pre-condition. We want to know more about the reasoning, so we print out debugging messages as follows, but do not know how to interpret the messages.

Any help would be appreciated.

$ Boogie.exe /printModel:4 boogie.bpl 
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
*** MODEL
%lbl%@2 -> false
%lbl%+0 -> true
%lbl%+10 -> true
%lbl%+15 -> true
%lbl%+7 -> true
a -> T@AVAR!val!1
b -> T@AVAR!val!0
call2formal@a@0 -> T@ADDR!val!2
call3formal@r@0 -> T@ADDR!val!3
d!31!4 -> T@ADDR!val!2
dealloc@@0 -> |T@[AVAR]Bool!val!0|
dealloc@0 -> |T@[AVAR]Bool!val!1|
dealloc@1 -> |T@[AVAR]Bool!val!2|
dealloc@2 -> |T@[AVAR]Bool!val!3|
e@@0 -> |T@[AVAR]ADDR!val!0|
e@0 -> |T@[AVAR]ADDR!val!1|
e@1 -> |T@[AVAR]ADDR!val!2|
e@2 -> |T@[AVAR]ADDR!val!3|
tmp -> T@AVAR!val!1
valid@@0 -> |T@[ADDR]Bool!val!0|
valid@0 -> |T@[ADDR]Bool!val!1|
valid@1 -> |T@[ADDR]Bool!val!2|
valid@2 -> |T@[ADDR]Bool!val!3|
valid@4 -> |T@[ADDR]Bool!val!3|
INV -> {
  |T@[AVAR]ADDR!val!0| |T@[AVAR]Bool!val!0| |T@[ADDR]Bool!val!0| -> true
  |T@[AVAR]ADDR!val!1| |T@[AVAR]Bool!val!1| |T@[ADDR]Bool!val!1| -> true
  else -> true
}
Select_[AVAR]$bool -> {
  |T@[AVAR]Bool!val!1| T@AVAR!val!1 -> false
  |T@[AVAR]Bool!val!3| T@AVAR!val!1 -> true
  |T@[AVAR]Bool!val!0| T@AVAR!val!1 -> false
  |T@[AVAR]Bool!val!2| T@AVAR!val!1 -> false
  else -> false
}
Select_[ADDR]$bool -> {
  |T@[ADDR]Bool!val!0| T@ADDR!val!1 -> true
  |T@[ADDR]Bool!val!2| T@ADDR!val!2 -> true
  |T@[ADDR]Bool!val!3| T@ADDR!val!3 -> true
  |T@[ADDR]Bool!val!0| T@ADDR!val!2 -> false
  |T@[ADDR]Bool!val!1| T@ADDR!val!1 -> true
  |T@[ADDR]Bool!val!2| T@ADDR!val!1 -> true
  |T@[ADDR]Bool!val!3| T@ADDR!val!1 -> true
  |T@[ADDR]Bool!val!3| T@ADDR!val!2 -> true
  |T@[ADDR]Bool!val!1| T@ADDR!val!2 -> false
  else -> true
}
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
Store_[AVAR]ADDR -> {
  |T@[AVAR]ADDR!val!1| T@AVAR!val!1 T@ADDR!val!2 -> |T@[AVAR]ADDR!val!2|
  |T@[AVAR]ADDR!val!2| T@AVAR!val!1 T@ADDR!val!3 -> |T@[AVAR]ADDR!val!3|
  else -> |T@[AVAR]ADDR!val!2|
}
Store_[AVAR]$bool -> {
  |T@[AVAR]Bool!val!1| T@AVAR!val!1 false -> |T@[AVAR]Bool!val!2|
  |T@[AVAR]Bool!val!2| T@AVAR!val!1 true -> |T@[AVAR]Bool!val!3|
  else -> |T@[AVAR]Bool!val!2|
}
Select_[AVAR]ADDR -> {
  |T@[AVAR]ADDR!val!0| T@AVAR!val!1 -> T@ADDR!val!0
  |T@[AVAR]ADDR!val!0| T@AVAR!val!0 -> T@ADDR!val!1
  |T@[AVAR]ADDR!val!1| T@AVAR!val!0 -> T@ADDR!val!1
  |T@[AVAR]ADDR!val!2| T@AVAR!val!1 -> T@ADDR!val!2
  |T@[AVAR]ADDR!val!3| T@AVAR!val!1 -> T@ADDR!val!3
  |T@[AVAR]ADDR!val!3| T@AVAR!val!0 -> T@ADDR!val!1
  |T@[AVAR]ADDR!val!2| T@AVAR!val!0 -> T@ADDR!val!1
  else -> T@ADDR!val!1
}
*** END_MODEL
boogie.bpl(212,1): Error BP5003: A postcondition might not hold on this return path.
boogie.bpl(194,5): Related location: This is the postcondition that might not hold.
Execution trace:
    boogie.bpl(201,5): anon0
    boogie.bpl(208,5): anon3_Else
    boogie.bpl(211,13): anon2
Boogie program verifier finished with 7 verified, 1 error

Best regards,
Min Hsien Weng

Default timeLimit leads to zero timeout

I noticed that if you don't pass a /timeLimit flag, Boogie tells Z3:

(set-option :TIMEOUT 0)

Unfortunately, due to Z3Prover/z3#1100, this is implemented as an immediate timeout on Linux, whereas presumably the intention is to have an infinite timeout. It may be safer not to emit that line when a timeout isn't desired.

Symbooglix resulting in ArgumentNullException due to Graph.cs

For quite awhile now, Symbooglix has been throwing an ArgumentNullException when it is run on some cases. Consider the following example:

procedure fn1();
implementation fn1()
{
  anon0:
    goto $bb5;
  b4:
    goto $bb5;
  $bb5:
    goto $bb10;
  b9:
    goto $bb10;
  $bb10:
    return;
}
procedure main();
implementation main()
{
  anon0:
    return;
}

When I run "symbooglix example.bpl --entry-points=main" on the above example, it throws an ArgumentNullException with the following stack trace:

System.ArgumentNullException: Value cannot be null.
Parameter name: key
   at System.Collections.Generic.Dictionary.FindEntry(TKey key)
   at System.Collections.Generic.Dictionary.get_Item(TKey key)
   at Microsoft.Boogie.GraphUtil.Graph.Predecessors(Node n) in Boogie\Source\Graph\Graph.cs:line 483
   at Microsoft.Boogie.GraphUtil.DomRelation.NewComputeDominators() in Boogie\Source\Graph\Graph.cs:line 208
   at Microsoft.Boogie.GraphUtil.DomRelation..ctor(Graph g, Node source) in Boogie\Source\Graph\Graph.cs:line 87
   at Microsoft.Boogie.GraphUtil.Graph.get_DominatorMap() in Boogie\Source\Graph\Graph.cs:line 503
   at Microsoft.Boogie.GraphUtil.Graph.ComputeReducible(Graph g, Node source) in Boogie\Source\Graph\Graph.cs:line 703
   at Microsoft.Boogie.GraphUtil.Graph.ComputeLoops() in Boogie\Source\Graph\Graph.cs:line 838
   at Symbooglix.LoopEscapingScheduler.ReceiveExecutor(Executor executor) in Symbooglix\Executor\StateSchedulers\LoopEscapingScheduler.cs:line 114
   at Symbooglix.Executor.InternalRun(Implementation entryPoint, Int32 timeout) in Symbooglix\Executor\Executor.cs:line 670
   at Symbooglix.Executor.Run(Implementation entryPoint, Int32 timeout) in Symbooglix\Executor\Executor.cs:line 611
   at SymbooglixDriver.Driver.RealMain(String[] args) in SymbooglixDriver\Driver.cs:line 625
   at SymbooglixDriver.Driver.Main(String[] args) in SymbooglixDriver\Driver.cs:line 304
Exiting with EXCEPTION_RAISED

This issue was first raised last July:

boogie-org/symbooglix#32

When I pass the above file directly to Boogie, if I print the nodes of Graph g at this line:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L82

It prints three nodes: one each for the anon0, $bb5, and $bb10 labels.

However, when I pass the above file to Symbooglix and print the nodes at that position, the Graph object contains five nodes: one for the above three labels, as well as one for b4 and one for b9. This presents a problem when this line is reached:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L195

When the nodes are mapped to integers using this traversal of the Graph object, the traversal only hits the anon0, $bb5, and $bb10 labels. So the b4 and b9 labels are unreachable from the others. Which makes sense since anon0 is considered the "source" label, and we can see by looking at the .bpl file that the b4 and b9 labels are not "children" of the anon0 label. So this Graph does not have a single source node, but three source nodes, even though this traversal method (and I'm assuming many other parts of this class) assumes that whatever graph it is traversing has only a single source node.

This results in the postOrderNumberToNode map not being set for the b4 and b9 nodes, resulting in the variable at this line being set to null:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L207

And the exception occurs at the very next line, as you can see from the above stack trace.

Note by the stack trace above the last place in Symbooglix code that is reached before Boogie code begins to be called:

https://github.com/symbooglix/symbooglix/blob/master/src/Symbooglix/Analysis/LoopInfo.cs#L58

Symbooglix is not calling impl.PruneUnreachableBlocks(), which would remove those b4 and b9 labels. I had already made a pull request (now closed) to Symbooglix making this change wherever impl.ComputeLoops() is called:

boogie-org/symbooglix#33

However, making this change resulted in another exception occurring in one of the regressions:

https://travis-ci.org/symbooglix/symbooglix/builds/336702517

Does anyone have any ideas for how to fix this issue? Should Boogie's Graph class be changed, or is there a way to fix this issue in Symbooglix?

incorrect output for Ctrl-C

On OS X (and Linux sometimes), use Dafny to prove something hard and even incorrect. It takes Dafny a long time (or never) to return, which is fine. However, press Ctrl+C and the output is the following:

Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
... (press Ctrl-C) ...

Dafny program verifier finished with 6 verified, 0 errors

The message is very misleading; the theorem, which didn't finish proving, is totally incorrect, and yet Dafny says verified.

The issue seems to be exception handling in Boogie. Ctrl-C causes some exception other than UnexpectedProverOutputException, which Checker::WaitForOutput doesn't handle:

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 7bda0022385a..b21254c12424 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -321,6 +321,10 @@ public bool IsIdle
         {
           outputExn = e;
         }
+        catch (Exception e)
+        {
+          outputExn = new UnexpectedProverOutputException(e.Message);
+        }

         switch (outcome)
         {

Apply the above patch and the output becomes the following upon Ctrl-C:

Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
... (press Ctrl-C) ...
Advisory: Impl$$_module.__default.test__ok SKIPPED because of internal error: unexpected prover output: Cannot write to a closed TextWriter.
test.dfy(20,6): Verification inconclusive (Impl$$_module.__default.test__ok)

Dafny program verifier finished with 5 verified, 0 errors, 1 inconclusive

This makes more sense than verified.

Sanitize the . (DOT) prefix for CVC4 support

Hi guys,

So SMACK can produce some constants that start with the . (DOT) prefix (e.g. const unique .str: int;). This can cause issues when Boogie sends the SMTLIBv2 formula to CVC4, because the @ and . prefixes are reserved in the standard (see * below).

I think (I might be wrong though) that there already exists some pass inside Boogie that changes the prefix @ to "AT". Could we do the same for the dot prefix?

Any thoughts?

Cheers,

Pantazis

*[quote from the SMTLIBv2 standard]: Symbols are used for attribute values, and sort, variable, logic, theory, constant and function names. A symbol can be any sequence of symbol characters that does not start with a digit and is not a reserved word. In addition, user-defined symbols may not begin with an @ or a period (.); such symbols are reserved for internal use. Some symbols consisting of punctuation characters, such as + and - have intuitively natural meanings as function symbols, though their meaning is always defined solely by the logic being used. Similarly, symbols that are English words may have obvious meanings. Good style would suggest avoiding legal but unusual symbols that mix alphanumerics and operator-like characters, such as a<b or ab+- or -1.

Large modifies clauses cause a huge blowup

We have SMACK-generated Boogie files with very large modifies clauses on all procedures. We are inlining procedures using Boogie, and so my hunch was that most modifies clauses should just be noops in that case. However, we are seeing a huge blowup inside Boogie, which likely happens during VC generation phase since Z3 does not even get a chance to be invoked.

Does anyone have any experience with this issue?

Is there maybe a Boogie switch that we can use to prune away variables from modifies clauses that are not needed?

Or maybe when inlining gets performed modifies clauses should not even be needed?

I can email this Boogie file if someone is interested to take a look. Unfortunately I could not attach it to this issue. Thx.

Boogie allows identifiers to start with . and @, which SMTLIB does not

The following legal Boogie program (based on its current language spec):

procedure foo() {
  var .x:int;
  assert .x == 0;
}

causes Boogie to throw an exception when used with CVC4:

boogie test.bpl /proverOpt:SOLVER=cvc4

Here is the exception excerpt:

Prover error: (error "Parse Error: <stdin>:11.15: cannot declare or define symbol `.x'; symbols starting with . and @ are reserved in SMT-LIB

How hard would it be to support some sort of incremental verification for non-.Net clients?

Hi there,

The current VS mode for Dafny depends heavily on Boogie's caching features to reduce latency. I'd like to implement the same in my newly released Emacs modes for Boogie and Dafny. Unlike Dafny's VS extension, though, Emacs lisp code can't easily call into Dafny or Boogie; and it seems that the VS extension does depend on that (at least IIUC; I've only had a cursory look at its source).

How hard would it be to adjust the model slightly, to make it possible to make such incremental reverification possible from other editors? Maybe through some /useCache:<filename> flag, which would instruct Boogie to look for a previously written cache in <filename>, and to write an updated cache after completing its latest run. That would have the cool property that it would totally transparent to the editor (apart from the flag)

Cheers,
Clément.

Too many comments crash due to stack overflow

On an input file with too many (successive) line comments, Boogie crashes due to overflowing the procedure stack. Discovered this on an input file which begins with 230,000 line comments. Due to file size it cannot be displayed here, but I’d be happy to email the (zipped) file if necessary.

How to produce model file?

I read following document:

https://boogie.codeplex.com/wikipage?title=BVD&referringTitle=Home

Then, I tried to create model file on Ubuntu 16.04, but can't get it:

$ pwd
/home/kiwamu/src/corral/boogie
$ ./Binaries/Boogie.exe /mv:foo.model Test/bitvectors/bv0.bpl
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Test/bitvectors/bv0.bpl(6,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32)
Test/bitvectors/bv0.bpl(7,3): Error: mismatched types in assignment command (cannot assign int to bv32)
Test/bitvectors/bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
Test/bitvectors/bv0.bpl(9,10): Error: start index in extract must be no bigger than the end index
Test/bitvectors/bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
Test/bitvectors/bv0.bpl(11,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
Test/bitvectors/bv0.bpl(12,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32)
7 type checking errors detected in Test/bitvectors/bv0.bpl
$ find . -name foo.model

How to produce the model file?

/errorLimit parameter quirks (default and 0-parameter behaviours)

By default, Boogie limits the number of errors reported per procedure. Since this isn't documented except in the /help, I found it a bit surprising when first flagged.

It seems that the /errorLimit:n parameter is, by default, set to 5. If one sets this to a higher number, more errors are reported. However, there doesn't seem to be a way (in principle) to avoid limiting the number of errors seen (of course, one can just choose a very large number each time). Passing /errorLimit:0 behaves analogously to /errorLimit:1 - one sees neither all nor zero errors.

I suggest that the default behaviour should be not to include a hard limit on the number of errors produced per procedure. One could discuss how a 0 parameter should be treated - personally I would find the "no limit" interpretation more useful there, too. In any case, the 0 shouldn't be treated as a 1.

SDV Benchmarks in Boogie

Hey Boogie users,
Are you looking for verification benchmarks in Boogie? Look no further:
https://github.com/boogie-org/sdvbench

Please help spread the word.

@boogie-org/boogie-developers
@boogie-org/corral-devs

Bug: negative numbers / arithmetic leading to vacuously verified postcondition

Hello,

We've encountered a usage of Boogie that allows an obviously incorrect postcondition to be verified. A minimal example is available at:

http://rise4fun.com/Boogie/ttW

and also at the end of this post. Note that replacing "x := -N;" with "x := -1 * N;" already changes the result of the verification. We're using the latest distribution of Boogie and the latest compiled Z3 (Boogie 2.3.0.61016 and Z3 4.4.2).

Many thanks,

-- Chris

const N: int;
axiom 0 <= N;

procedure vacuous_post()
ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N);
{
var x: int;
x := -N;
while (x != x) {
}
}

Doomed tests need to be enabled and fixed

The tests in Test/doomed are really broken. If the lit.local.cfg is removed (this is preventing them from being executed) then they hang! Some .bpl files in that directory aren't use either.

They were originally commited by schaef.

Is there any intended replacement for "call forall"?

Commit c5c2c94 removed the call forall functionality described in "This is Boogie 2". Is there any new, recommended alternative to this construct?

I have a lemma that the solver cannot directly prove as a universally-quantified formula but is easily provable when restated as a procedure with explicit parameters and a single assert in the body.

Was there a reason to remove call forall? I realize that maybe the practice of using procedures as lemma proofs is no longer recommended since well-foundedness of recursive calls is not verified.

timeLimit attribute on procedures appears to no longer work

Boogie allows a per-procedure timeLimit attribute:

procedure{:timeLimit 10} p1() {}
procedure{:timeLimit 20} p2() {}

This used to produce a different TIMEOUT option on each of the two SMT queries:

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
...
(set-option :TIMEOUT 10000)
...
(check-sat)
...
(set-option :TIMEOUT 20000)
(reset)
(set-option :TIMEOUT 20000)
(set-option :print-success false)
(set-info :smt-lib-version 2.0)
...
(set-option :TIMEOUT 20000)
...
(check-sat)
...

I think this may have unintentionally been changed in commit 09a9f17. After that commit, the TIMEOUT is 10000 in both queries.

I'm not sure what the best fix is; as the commit rightly points out, the old code was messy (e.g. TIMEOUT 20000 is printed three times in the SMT code shown above) and the timeLimit attribute handling was Z3-specific. But it would be nice if there were a way to make the timeLimit attribute work again.

boogie-org / boogie Goto Github PK

boogie's People

Stargazers

Watchers

Forkers

boogie's Issues

Syntax Documentation

It gives the following compilation errors:

Recommend Projects

Recommend Topics

Recommend Org