boogie-org / boogie Goto Github PK
View Code? Open in Web Editor NEWBoogie
Home Page: http://research.microsoft.com/en-us/projects/boogie/
License: MIT License
Boogie
Home Page: http://research.microsoft.com/en-us/projects/boogie/
License: MIT License
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.
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.
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 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 :
/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?1 -> 1
or 1 -> 2 -> 3 -> 4 ..... -> 1
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:
\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.
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:
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:
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?
Boogie does not compile (on OS X 10.10.3) using just mono (Mono JIT compiler version 4.0.1).
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
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
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
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!
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
/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.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.
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 <---
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 :0Error 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!
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).
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.
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
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.
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?
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.
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.
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.
It seems to me that we can erase this branch. @qunyanm could you please confirm this? Thanks!
Linearity assumptions are not (or not properly) injected at parallel calls. The attached test is a minimal example demonstrating the failure.
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) {
}
}
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.
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.
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:
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:
I think either is OK but the default behavior creates a mess when you edit on both unix and windows.
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);
}
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.
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.
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.
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
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?
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?
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
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
I read following document:
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?
Hello,
I want to contribute to this project, how do I get started?
Also, is there some IRC channel where discussions happen?
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.
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
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.
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
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.
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.
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)?
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
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
.
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.
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.
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.
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?
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?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.