From 76a041a475db3a9d7cf2cac8598ecc5ffcc70ca0 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 22 Jun 2011 11:09:37 -0700 Subject: partial fixes to these regressions --- Test/z3api/Boog24.bpl | 1 + Test/z3api/boog0.bpl | 7 ++++--- Test/z3api/boog1.bpl | 4 +++- Test/z3api/boog10.bpl | 4 +++- Test/z3api/boog11.bpl | 4 +++- Test/z3api/boog12.bpl | 4 +++- Test/z3api/boog13.bpl | 7 +++++-- Test/z3api/boog14.bpl | 1 + Test/z3api/boog15.bpl | 1 + Test/z3api/boog16.bpl | 1 + Test/z3api/boog17.bpl | 2 ++ Test/z3api/boog18.bpl | 1 + Test/z3api/boog19.bpl | 2 ++ Test/z3api/boog2.bpl | 4 +++- Test/z3api/boog20.bpl | 1 + Test/z3api/boog21.bpl | 4 +++- Test/z3api/boog22.bpl | 1 + Test/z3api/boog23.bpl | 2 ++ Test/z3api/boog25.bpl | 2 ++ Test/z3api/boog28.bpl | 1 + Test/z3api/boog29.bpl | 1 + Test/z3api/boog3.bpl | 1 + Test/z3api/boog30.bpl | 1 + Test/z3api/boog31.bpl | 1 + Test/z3api/boog34.bpl | 1 + Test/z3api/boog4.bpl | 7 +++++-- Test/z3api/boog5.bpl | 7 +++++-- Test/z3api/boog6.bpl | 4 +++- Test/z3api/boog7.bpl | 4 +++- Test/z3api/boog8.bpl | 4 +++- Test/z3api/boog9.bpl | 4 +++- Test/z3api/runtest.bat | 14 ++++++++++++-- 32 files changed, 82 insertions(+), 21 deletions(-) (limited to 'Test') diff --git a/Test/z3api/Boog24.bpl b/Test/z3api/Boog24.bpl index c5e2eea6..d3da775d 100644 --- a/Test/z3api/Boog24.bpl +++ b/Test/z3api/Boog24.bpl @@ -1,3 +1,4 @@ +type ref; function LIFT(a:bool) returns (int); axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0); diff --git a/Test/z3api/boog0.bpl b/Test/z3api/boog0.bpl index 1b9bee36..4206152b 100644 --- a/Test/z3api/boog0.bpl +++ b/Test/z3api/boog0.bpl @@ -1,3 +1,4 @@ +type ref; type Wicket; const w: Wicket; var favorite: Wicket; @@ -6,7 +7,7 @@ function age(Wicket) returns (int); axiom age(w)==7; procedure NewFavorite(p: Wicket); - modifies favorite ; + modifies favorite; ensures favorite==p; @@ -19,7 +20,7 @@ const myRef: ref; const v: Wicket; axiom 7 < 8; -axiom 7 <= 8; +axiom 7 <= 8; axiom 8 > 7; axiom 8 >= 7; axiom 6 != 7; @@ -37,7 +38,7 @@ axiom ((7==7) && (8==8)); var favorite2: Wicket; procedure SwapFavorites() - modifies favorite,favorite2 ; + modifies favorite,favorite2; ensures (favorite==old(favorite2)) && (favorite2==old(favorite)); { diff --git a/Test/z3api/boog1.bpl b/Test/z3api/boog1.bpl index 6b6cce75..9f4d2349 100644 --- a/Test/z3api/boog1.bpl +++ b/Test/z3api/boog1.bpl @@ -1,3 +1,4 @@ +type ref; type Wicket; const w: Wicket; var favorite: Wicket; @@ -7,7 +8,8 @@ function age(Wicket) returns (int); axiom age(w)==7; procedure NewFavorite(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl index 5ac43287..075432d7 100644 --- a/Test/z3api/boog10.bpl +++ b/Test/z3api/boog10.bpl @@ -1,3 +1,4 @@ +type ref; // types type Color; const unique red: Color; @@ -9,7 +10,8 @@ var myColor: Color; // procedure procedure SetTo(c: Color); - modifies myColor ; + modifies myColor +; ensures myColor==c; diff --git a/Test/z3api/boog11.bpl b/Test/z3api/boog11.bpl index e66802ea..5b83de6a 100644 --- a/Test/z3api/boog11.bpl +++ b/Test/z3api/boog11.bpl @@ -1,10 +1,12 @@ +type ref; // types const top: ref; var myRef: ref; // procedure procedure SetTo(r: ref); - modifies myRef ; + modifies myRef +; ensures myRef==r; diff --git a/Test/z3api/boog12.bpl b/Test/z3api/boog12.bpl index d20a8f35..c277a674 100644 --- a/Test/z3api/boog12.bpl +++ b/Test/z3api/boog12.bpl @@ -1,3 +1,4 @@ +type ref; // types type Color; const blue: Color; @@ -7,7 +8,8 @@ var myMatrix:[int,int] Color; // procedure procedure SetTo(c: Color); - modifies myArray, myMatrix ; + modifies myArray, myMatrix +; ensures myArray[0]==c; diff --git a/Test/z3api/boog13.bpl b/Test/z3api/boog13.bpl index a4f854f5..9cd873c6 100644 --- a/Test/z3api/boog13.bpl +++ b/Test/z3api/boog13.bpl @@ -1,3 +1,4 @@ +type ref; // types type Wicket; var favorite: Wicket; @@ -6,14 +7,16 @@ var v: Wicket; function age(w:Wicket) returns (int); axiom (exists v:Wicket :: age(v)<8 && - (forall v:Wicket :: age(v)==7) + (forall v:Wicket + :: age(v)==7) ); // procedure procedure SetToSeven(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog14.bpl b/Test/z3api/boog14.bpl index c163ed18..41450d85 100644 --- a/Test/z3api/boog14.bpl +++ b/Test/z3api/boog14.bpl @@ -1,3 +1,4 @@ +type ref; function choose(a:bool, b:int, c:int) returns (x:int); axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b); diff --git a/Test/z3api/boog15.bpl b/Test/z3api/boog15.bpl index ef792b2b..428c0f6e 100644 --- a/Test/z3api/boog15.bpl +++ b/Test/z3api/boog15.bpl @@ -1,3 +1,4 @@ +type ref; function AtLeast(int, int) returns ([int]bool); axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]); diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl index 48afd41d..a002c166 100644 --- a/Test/z3api/boog16.bpl +++ b/Test/z3api/boog16.bpl @@ -1,3 +1,4 @@ +type ref; function choose(a:bool, b:int, c:int) returns (x:int); axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} !a ==> choose(a,b,c) == c); diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl index 6f886f49..89159af1 100644 --- a/Test/z3api/boog17.bpl +++ b/Test/z3api/boog17.bpl @@ -1,3 +1,5 @@ +type name; +type ref; const unique g : int; axiom(g != 0); diff --git a/Test/z3api/boog18.bpl b/Test/z3api/boog18.bpl index fe0cbc10..35f7d48a 100644 --- a/Test/z3api/boog18.bpl +++ b/Test/z3api/boog18.bpl @@ -1,3 +1,4 @@ +type ref; const A100INT4_name:int; function Match(a:int, t:int) returns (int); diff --git a/Test/z3api/boog19.bpl b/Test/z3api/boog19.bpl index 17b199dd..178bb04f 100644 --- a/Test/z3api/boog19.bpl +++ b/Test/z3api/boog19.bpl @@ -1,3 +1,5 @@ +type name; +type ref; var alloc:[int]name; diff --git a/Test/z3api/boog2.bpl b/Test/z3api/boog2.bpl index 74c05a28..315c51af 100644 --- a/Test/z3api/boog2.bpl +++ b/Test/z3api/boog2.bpl @@ -1,10 +1,12 @@ +type ref; type Wicket; var favorite: Wicket; var hate: Wicket; procedure NewFavorite(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog20.bpl b/Test/z3api/boog20.bpl index fa714972..10181400 100644 --- a/Test/z3api/boog20.bpl +++ b/Test/z3api/boog20.bpl @@ -1,3 +1,4 @@ +type ref; function PLUS(int, int, int) returns (int); function Rep(int, int) returns (int); diff --git a/Test/z3api/boog21.bpl b/Test/z3api/boog21.bpl index 1f4fa6dc..8e3abde7 100644 --- a/Test/z3api/boog21.bpl +++ b/Test/z3api/boog21.bpl @@ -1,3 +1,4 @@ +type ref; function PLUS(int, int, int) returns (int); function Rep(int,int) returns (int); @@ -5,7 +6,8 @@ function Rep(int,int) returns (int); // ERROR -axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z )); +axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z +)); axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x)); // END ERROR diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl index 95e45849..c255a3c5 100644 --- a/Test/z3api/boog22.bpl +++ b/Test/z3api/boog22.bpl @@ -1,3 +1,4 @@ +type ref; type W; function f1(W,int) returns (int); diff --git a/Test/z3api/boog23.bpl b/Test/z3api/boog23.bpl index 41c68790..4e0fc4d0 100644 --- a/Test/z3api/boog23.bpl +++ b/Test/z3api/boog23.bpl @@ -1,3 +1,5 @@ +type name; +type ref; type byte; function OneByteToInt(byte) returns (int); function TwoBytesToInt(byte, byte) returns (int); diff --git a/Test/z3api/boog25.bpl b/Test/z3api/boog25.bpl index 0a8b5e92..0ee4163c 100644 --- a/Test/z3api/boog25.bpl +++ b/Test/z3api/boog25.bpl @@ -1,3 +1,5 @@ +type name; +type ref; type byte; function OneByteToInt(byte) returns (int); function TwoBytesToInt(byte, byte) returns (int); diff --git a/Test/z3api/boog28.bpl b/Test/z3api/boog28.bpl index 989dbf75..ab7f4ad2 100644 --- a/Test/z3api/boog28.bpl +++ b/Test/z3api/boog28.bpl @@ -1,3 +1,4 @@ +type ref; function LIFT(x:bool) returns (int); axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0); diff --git a/Test/z3api/boog29.bpl b/Test/z3api/boog29.bpl index 8a97944d..035e69fd 100644 --- a/Test/z3api/boog29.bpl +++ b/Test/z3api/boog29.bpl @@ -1,3 +1,4 @@ +type ref; function LIFT(x:bool) returns (int); axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0); diff --git a/Test/z3api/boog3.bpl b/Test/z3api/boog3.bpl index 9e04ac5b..207ddbd0 100644 --- a/Test/z3api/boog3.bpl +++ b/Test/z3api/boog3.bpl @@ -1,3 +1,4 @@ +type ref; type Wicket; procedure Dummy(); diff --git a/Test/z3api/boog30.bpl b/Test/z3api/boog30.bpl index ae682156..81e04f20 100644 --- a/Test/z3api/boog30.bpl +++ b/Test/z3api/boog30.bpl @@ -1,3 +1,4 @@ +type ref; function LIFT(x:bool) returns (int); axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0); diff --git a/Test/z3api/boog31.bpl b/Test/z3api/boog31.bpl index 219effce..86386a90 100644 --- a/Test/z3api/boog31.bpl +++ b/Test/z3api/boog31.bpl @@ -1,3 +1,4 @@ +type ref; const b1:bool; const b2:bool; diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl index 62e7e82b..88a587aa 100644 --- a/Test/z3api/boog34.bpl +++ b/Test/z3api/boog34.bpl @@ -1,3 +1,4 @@ +type ref; function Rep(int, int) returns (int); axiom(forall n:int, x:int :: {Rep(n,x)} diff --git a/Test/z3api/boog4.bpl b/Test/z3api/boog4.bpl index 46eda549..95ec7011 100644 --- a/Test/z3api/boog4.bpl +++ b/Test/z3api/boog4.bpl @@ -1,3 +1,4 @@ +type ref; type Wicket; const w: Wicket; @@ -10,7 +11,8 @@ function age(Wicket) returns (int); axiom age(w)==7; axiom 7 < 8; -axiom 7 <= 8; +axiom 7 <= 8; + axiom 8 > 7; axiom 8 >= 7; axiom 6 != 7; @@ -28,7 +30,8 @@ axiom 7!=7; procedure NewFavorite(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog5.bpl b/Test/z3api/boog5.bpl index 0db94bba..4b76fd22 100644 --- a/Test/z3api/boog5.bpl +++ b/Test/z3api/boog5.bpl @@ -1,3 +1,4 @@ +type ref; // types type Wicket; @@ -23,7 +24,8 @@ axiom age(x)==4; // procedure procedure SetToSeven(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; @@ -32,7 +34,8 @@ implementation SetToSeven(l: Wicket) { favorite:=l; } else { favorite:=v; - } + } + } diff --git a/Test/z3api/boog6.bpl b/Test/z3api/boog6.bpl index 55c1dc7e..f6c3c23f 100644 --- a/Test/z3api/boog6.bpl +++ b/Test/z3api/boog6.bpl @@ -1,3 +1,4 @@ +type ref; // types type Wicket; @@ -10,7 +11,8 @@ axiom b==true; // procedure procedure SetToSeven(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog7.bpl b/Test/z3api/boog7.bpl index 36f952d1..78e5e3e6 100644 --- a/Test/z3api/boog7.bpl +++ b/Test/z3api/boog7.bpl @@ -1,3 +1,4 @@ +type ref; // consts const w: int; @@ -7,7 +8,8 @@ var favorite: int; // procedure procedure SetToSeven(p: int); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog8.bpl b/Test/z3api/boog8.bpl index 0ac4f163..121f27cf 100644 --- a/Test/z3api/boog8.bpl +++ b/Test/z3api/boog8.bpl @@ -1,3 +1,4 @@ +type ref; // types type Wicket; var favorite: Wicket; @@ -12,7 +13,8 @@ axiom myBool==true; // procedure procedure SetToSeven(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/boog9.bpl b/Test/z3api/boog9.bpl index 55897a1d..3bd6ff63 100644 --- a/Test/z3api/boog9.bpl +++ b/Test/z3api/boog9.bpl @@ -1,3 +1,4 @@ +type ref; // types type Wicket; var favorite: Wicket; @@ -9,7 +10,8 @@ axiom (exists v:Wicket :: age(v)<8); // procedure procedure SetToSeven(p: Wicket); - modifies favorite ; + modifies favorite +; ensures favorite==p; diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index 5daa36c0..08a27b9b 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,8 +3,18 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe -for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do ( +for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do ( echo. echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /prover:z3api %%f + %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f ) +REM boog8.bpl +REM boog12.bpl +REM boog14.bpl +REM boog15.bpl +REM boog16.bpl +REM boog17.bpl + +REM boog19.bpl +REM boog23.bpl +REM boog25.bpl \ No newline at end of file -- cgit v1.2.3 From 2b81b9d7e787409913f4c0488c0b3310a4e9e5a0 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 22 Jun 2011 22:54:58 -0700 Subject: clean up in z3api --- Source/Provers/Z3api/ContextLayer.cs | 499 ++++++++++++++++++++++---- Source/Provers/Z3api/ProverLayer.cs | 26 +- Source/Provers/Z3api/SafeContext.cs | 636 ---------------------------------- Source/Provers/Z3api/StubContext.cs | 3 + Source/Provers/Z3api/TypeAdapter.cs | 73 ++-- Source/Provers/Z3api/VCExprVisitor.cs | 191 +++++----- Source/Provers/Z3api/Z3api.csproj | 2 - Test/z3api/runtest.bat | 7 +- 8 files changed, 595 insertions(+), 842 deletions(-) (limited to 'Test') diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index e6ba7b66..ed45c4fc 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -69,38 +69,6 @@ namespace Microsoft.Boogie.Z3 } } - public abstract class Z3TermAst { } - public abstract class Z3PatternAst { } - public abstract class Z3ConstDeclAst { } - public abstract class Z3LabeledLiterals { } - - public interface Z3Context - { - void CreateBacktrackPoint(); - void Backtrack(); - void AddAxiom(VCExpr axiom, LineariserOptions linOptions); - void AddConjecture(VCExpr vc, LineariserOptions linOptions); - void AddSmtlibString(string smtlibString); - string GetDeclName(Z3ConstDeclAst constDeclAst); - Z3PatternAst MakePattern(List exprs); - Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body); - ProverInterface.Outcome Check(out List boogieErrors); - void TypeCheckBool(Z3TermAst t); - void TypeCheckInt(Z3TermAst t); - void DeclareType(string typeName); - void DeclareConstant(string constantName, Type boogieType); - void DeclareFunction(string functionName, List domain, Type range); - Z3TermAst GetConstant(string constantName, Type constantType); - Z3TermAst MakeIntLiteral(string numeral); - Z3TermAst MakeTrue(); - Z3TermAst MakeFalse(); - Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child); - Z3LabeledLiterals GetRelevantLabels(); - Z3TermAst Make(string op, List children); - Z3TermAst MakeArraySelect(List args); - Z3TermAst MakeArrayStore(List args); - } - internal class PartitionMap { private Context ctx; @@ -138,43 +106,51 @@ namespace Microsoft.Boogie.Z3 Sort boolSort = ctx.MkBoolSort(); Sort intSort = ctx.MkIntSort(); ArrayValue av; - + if (s.Equals(boolSort)) { return ctx.GetBoolValue(v); } - else if (s.Equals(intSort)) - { - int i; - if (ctx.TryGetNumeralInt(v, out i)) - { - return BigNum.FromInt(i); - } - else - { - return BigNum.FromString(ctx.GetNumeralString(v)); - } + else if (s.Equals(intSort)) { + int i; + long il; + uint u; + ulong ul; + if (ctx.TryGetNumeralInt(v, out i)) { + return BigNum.FromInt(i); + } + else if (ctx.TryGetNumeralInt64(v, out il)) { + return BigNum.FromLong(il); + } + else if (ctx.TryGetNumeralUInt(v, out u)) { + return BigNum.FromUInt(u); + } + else if (ctx.TryGetNumeralUInt64(v, out ul)) { + return BigNum.FromULong(ul); + } + else { + string str = v.ToString(); + return GetPartition(v); + //return BigNum.FromString(ctx.GetNumeralString(v)); + } } - else if (model.TryGetArrayValue(v, out av)) - { - List> arrayValue = new List>(); - List tuple; - for (int i = 0; i < av.Domain.Length; i++) - { - tuple = new List(); - tuple.Add(GetPartition(av.Domain[i])); - tuple.Add(GetPartition(av.Range[i])); - arrayValue.Add(tuple); - } + else if (model.TryGetArrayValue(v, out av)) { + List> arrayValue = new List>(); + List tuple; + for (int i = 0; i < av.Domain.Length; i++) { tuple = new List(); - tuple.Add(GetPartition(av.ElseCase)); + tuple.Add(GetPartition(av.Domain[i])); + tuple.Add(GetPartition(av.Range[i])); arrayValue.Add(tuple); - return arrayValue; + } + tuple = new List(); + tuple.Add(GetPartition(av.ElseCase)); + arrayValue.Add(tuple); + return arrayValue; } - else - { - // The term is uninterpreted; just return the partition id. - return GetPartition(v); + else { + // The term is uninterpreted; just return the partition id. + return GetPartition(v); } } @@ -249,7 +225,7 @@ namespace Microsoft.Boogie.Z3 public BoogieErrorModelBuilder(Z3Context container, Model z3Model) { this.container = container; - this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3, z3Model); + this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model); } private Dictionary CreateConstantToPartition(Model z3Model) @@ -257,7 +233,7 @@ namespace Microsoft.Boogie.Z3 Dictionary constantToPartition = new Dictionary(); foreach (FuncDecl c in z3Model.GetModelConstants()) { - string name = container.GetDeclName(new Z3TypeSafeConstDecl(c)); + string name = container.GetDeclName(c); int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0])); constantToPartition.Add(name, pid); } @@ -285,7 +261,7 @@ namespace Microsoft.Boogie.Z3 foreach (KeyValuePair kv in z3Model.GetFunctionGraphs()) { List> f_tuples = new List>(); - string f_name = container.GetDeclName(new Z3TypeSafeConstDecl(kv.Key)); + string f_name = container.GetDeclName(kv.Key); FunctionGraph graph = kv.Value; foreach (FunctionEntry entry in graph.Entries) { @@ -310,8 +286,8 @@ namespace Microsoft.Boogie.Z3 Dictionary constantToPartition = CreateConstantToPartition(z3Model); Dictionary>> functionToPartition = CreateFunctionToPartition(z3Model); List> partitionToConstant = CreatePartitionToConstant(constantToPartition); - List partitionToValue = partitionMap.PartitionToValue(((Z3SafeContext)container).z3); - Dictionary valueToPartition = partitionMap.ValueToPartition(((Z3SafeContext)container).z3); + List partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3); + Dictionary valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3); return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition); } } @@ -334,4 +310,395 @@ namespace Microsoft.Boogie.Z3 this._relevantLabels = relevantLabels; } } + + public class Z3Context { + private BacktrackDictionary symbols = new BacktrackDictionary(); + internal BacktrackDictionary constants = new BacktrackDictionary(); + internal BacktrackDictionary functions = new BacktrackDictionary(); + internal BacktrackDictionary labels = new BacktrackDictionary(); + + public Context z3; + public Z3Config config; + public Z3apiProverContext ctxt; + private VCExpressionGenerator gen; + private Z3TypeCachedBuilder tm; + private UniqueNamer namer; + public UniqueNamer Namer { + get { return namer; } + } + private StreamWriter z3log; + public Z3Context(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen) { + Context z3 = new Context(config.Config); + if (config.LogFilename != null) + z3.OpenLog(config.LogFilename); + foreach (string tag in config.DebugTraces) + z3.EnableDebugTrace(tag); + this.ctxt = ctxt; + this.z3 = z3; + this.config = config; + this.tm = new Z3TypeCachedBuilder(this); + this.gen = gen; + this.namer = new UniqueNamer(); + this.z3.SetPrintMode(PrintMode.Smtlib2Compliant); + this.z3log = null; + } + + public void log(string format, params object[] args) { + // Currently, this is a no-op because z3log is always null + // We use the default (automatic) tracing facility of z3 + if (z3log != null) { + var str = string.Format(format, args); + // Do standard string replacement + str = str.Replace("array", "Array"); + z3log.WriteLine(str); + z3log.Flush(); + } + } + + public void CloseLog() { + z3.CloseLog(); + if (z3log != null) { + z3log.Close(); + } + z3log = null; + } + + public void CreateBacktrackPoint() { + symbols.CreateBacktrackPoint(); + constants.CreateBacktrackPoint(); + functions.CreateBacktrackPoint(); + labels.CreateBacktrackPoint(); + z3.Push(); + log("(push)"); + } + + public void Backtrack() { + z3.Pop(); + labels.Backtrack(); + functions.Backtrack(); + constants.Backtrack(); + symbols.Backtrack(); + log("(pop)"); + } + + public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { + Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); + Term term = (Term)axiom.Accept(visitor, linOptions); + log("(assert {0})", term); + z3.AssertCnstr(term); + } + + public void AddConjecture(VCExpr vc, LineariserOptions linOptions) { + VCExpr not_vc = (VCExpr)this.gen.Not(vc); + Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); + Term term = (Term)not_vc.Accept(visitor, linOptions); + log("(assert {0})", term); + z3.AssertCnstr(term); + } + + public void AddSmtlibString(string smtlibString) { + FuncDecl[] decls; + Term[] assumptions; + Term[] terms; + Sort[] sorts; + string tmp; + + z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { }, + out assumptions, out terms, out decls, out sorts, out tmp); + // TBD: check with Nikolaj about the correct position of assumptions + foreach (FuncDecl decl in decls) { + Symbol symbol = z3.GetDeclName(decl); + string functionName = z3.GetSymbolString(symbol); + functions.Add(functionName, decl); + } + foreach (Term assumption in assumptions) { + log("(assert {0})", assumption); + z3.AssertCnstr(assumption); + } + } + + public string GetDeclName(FuncDecl constDeclAst) { + Symbol symbol = z3.GetDeclName(constDeclAst); + return z3.GetSymbolString(symbol); + } + + public Pattern MakePattern(List exprs) { + Pattern pattern = z3.MkPattern(exprs.ToArray()); + return pattern; + } + + private List GetTypes(List boogieTypes) { + List z3Types = new List(); + foreach (Type boogieType in boogieTypes) { + Sort type = tm.GetType(boogieType); + z3Types.Add(type); + } + return z3Types; + } + + public Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List varNames, List boogieTypes, List patterns, List no_patterns, Term body) { + List bound = new List(); + for (int i = 0; i < varNames.Count; i++) { + Term t = GetConstant(varNames[i], boogieTypes[i]); + bound.Add(t); + } + + Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body); + return termAst; + } + + private static bool Equals(List l, List r) { + Debug.Assert(l != null); + if (r == null) + return false; + + if (l.Count != r.Count) + return false; + + for (int i = 0; i < l.Count; i++) + if (!l[i].Equals(r[i])) + return false; + return true; + } + + private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List relevantLabels) { + BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model); + Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model); + return new Z3ErrorModelAndLabels(boogieModel, new List(relevantLabels)); + } + + private void DisplayRelevantLabels(List relevantLabels) { + foreach (string labelName in relevantLabels) { + System.Console.Write(labelName + ","); + } + System.Console.WriteLine("---"); + } + + public ProverInterface.Outcome Check(out List boogieErrors) { + Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover"); + boogieErrors = new List(); + LBool outcome = LBool.Undef; + Debug.Assert(0 < this.config.Counterexamples); + while (true) { + Model z3Model; + outcome = z3.CheckAndGetModel(out z3Model); + log("(check-sat)"); + if (outcome == LBool.False) + break; + + if (outcome == LBool.Undef && z3Model == null) { + // Blame this on timeout + return ProverInterface.Outcome.TimeOut; + } + + Debug.Assert(z3Model != null); + LabeledLiterals labels = z3.GetRelevantLabels(); + Debug.Assert(labels != null); + + List labelStrings = new List(); + uint numLabels = labels.GetNumLabels(); + for (uint i = 0; i < numLabels; ++i) { + Symbol sym = labels.GetLabel(i); + string labelName = z3.GetSymbolString(sym); + if (!labelName.StartsWith("@")) { + labels.Disable(i); + } + labelStrings.Add(labelName); + } + boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + if (boogieErrors.Count < this.config.Counterexamples) { + z3.BlockLiterals(labels); + log("block-literals {0}", labels); + } + + labels.Dispose(); + z3Model.Dispose(); + if (boogieErrors.Count == this.config.Counterexamples) + break; + } + + if (boogieErrors.Count > 0) { + return ProverInterface.Outcome.Invalid; + } + else if (outcome == LBool.False) { + return ProverInterface.Outcome.Valid; + } + else { + Debug.Assert(outcome == LBool.Undef); + return ProverInterface.Outcome.Undetermined; + } + } + + public ProverInterface.Outcome CheckAssumptions(List assumptions, LineariserOptions linOptions, + out List boogieErrors, + out List unsatCore) { + Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover"); + boogieErrors = new List(); + unsatCore = new List(); + LBool outcome = LBool.Undef; + + Model z3Model; + Term proof; + Term[] core; + Term[] assumption_terms = new Term[assumptions.Count]; + var logstring = ""; + for (int i = 0; i < assumptions.Count; i++) { + Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); + Term z3ast = (Term)assumptions[i].Accept(visitor, linOptions); + assumption_terms[i] = z3ast; + logstring += string.Format("({0}) ", assumption_terms[i]); + } + + log("(get-core {0})", logstring); + outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core); + + if (outcome != LBool.False) { + Debug.Assert(z3Model != null); + LabeledLiterals labels = z3.GetRelevantLabels(); + Debug.Assert(labels != null); + + List labelStrings = new List(); + uint numLabels = labels.GetNumLabels(); + for (uint i = 0; i < numLabels; ++i) { + Symbol sym = labels.GetLabel(i); + string labelName = z3.GetSymbolString(sym); + if (!labelName.StartsWith("@")) { + labels.Disable(i); + } + labelStrings.Add(labelName); + } + boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + labels.Dispose(); + z3Model.Dispose(); + } + + if (boogieErrors.Count > 0) { + return ProverInterface.Outcome.Invalid; + } + else if (outcome == LBool.False) { + foreach (Term t in core) { + for (int i = 0; i < assumption_terms.Length; i++) { + if (t.Equals(assumption_terms[i])) + unsatCore.Add(i); + } + } + return ProverInterface.Outcome.Valid; + } + else { + Debug.Assert(outcome == LBool.Undef); + return ProverInterface.Outcome.Undetermined; + } + } + + public void DeclareType(string typeName) { + log("(declare-sort {0})", typeName); + } + + public void DeclareConstant(string constantName, Type boogieType) { + Symbol symbolAst = GetSymbol(constantName); + Sort typeAst = tm.GetType(boogieType); + + Term constAst = z3.MkConst(symbolAst, typeAst); + constants.Add(constantName, constAst); + log("(declare-funs (({0} {1})))", constAst, typeAst); + } + + public void DeclareFunction(string functionName, List domain, Type range) { + Symbol symbolAst = GetSymbol(functionName); + var domainStr = ""; + List domainAst = new List(); + foreach (Type domainType in domain) { + Sort type = tm.GetType(domainType); + domainAst.Add(type); + domainStr += type.ToString() + " "; + } + Sort rangeAst = tm.GetType(range); + FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst); + functions.Add(functionName, constDeclAst); + log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst); + } + + private List GetSymbols(List symbolNames) { + List symbols = new List(); + foreach (string symbolName in symbolNames) + symbols.Add(GetSymbol(symbolName)); + return symbols; + } + + private Symbol GetSymbol(string symbolName) { + if (!symbols.ContainsKey(symbolName)) { + Symbol symbolAst = z3.MkSymbol(symbolName); + symbols.Add(symbolName, symbolAst); + } + Symbol result; + if (!symbols.TryGetValue(symbolName, out result)) + throw new Exception("symbol " + symbolName + " is undefined"); + return result; + } + + private FuncDecl GetFunction(string functionName) { + FuncDecl function; + if (!functions.TryGetValue(functionName, out function)) + throw new Exception("function " + functionName + " is undefined"); + return function; + } + + public Term GetConstant(string constantName, Type constantType) { + Term typeSafeTerm; + if (!constants.ContainsKey(constantName)) + this.DeclareConstant(constantName, constantType); + + if (!constants.TryGetValue(constantName, out typeSafeTerm)) + throw new Exception("constant " + constantName + " is not defined"); + return typeSafeTerm; + } + + public Term MakeLabel(string labelName, bool pos, Term child) { + Symbol labelSymbol = this.GetSymbol(labelName); + Term labeledExpr = z3.MkLabel(labelSymbol, pos, child); + labels.Add(labelName, labeledExpr); + return labeledExpr; + } + + public LabeledLiterals GetRelevantLabels() { + LabeledLiterals safeLiterals = z3.GetRelevantLabels(); + log("get-relevant-labels"); + return safeLiterals; + } + + public Term Make(string op, List children) { + Term[] unwrapChildren = children.ToArray(); + Term term; + switch (op) { + // formulas + case "AND": term = z3.MkAnd(unwrapChildren); break; + case "OR": term = z3.MkOr(unwrapChildren); break; + case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break; + case "NOT": term = z3.MkNot(unwrapChildren[0]); break; + case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break; + // terms + case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break; + case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break; + case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break; + // terms + case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break; + case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break; + case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break; + case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break; + case "+": term = z3.MkAdd(unwrapChildren); break; + case "-": term = z3.MkSub(unwrapChildren); break; + case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break; + case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break; + case "*": term = z3.MkMul(unwrapChildren); break; + default: { + FuncDecl f = GetFunction(op); + term = z3.MkApp(f, unwrapChildren); + } + break; + } + return term; + } + } } \ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 7bdc07a0..f691cffc 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.Z3 public override void Close() { base.Close(); - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.CloseLog(); cm.z3.Dispose(); cm.config.Config.Dispose(); @@ -55,7 +55,7 @@ namespace Microsoft.Boogie.Z3 public void PushAxiom(VCExpr axiom) { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.CreateBacktrackPoint(); LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); cm.AddAxiom(axiom, linOptions); @@ -64,7 +64,7 @@ namespace Microsoft.Boogie.Z3 private void PushConjecture(VCExpr conjecture) { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.CreateBacktrackPoint(); LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); cm.AddConjecture(conjecture, linOptions); @@ -78,14 +78,14 @@ namespace Microsoft.Boogie.Z3 public void CreateBacktrackPoint() { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.CreateBacktrackPoint(); } public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; Push(); cm.AddAxiom(context.Axioms, linOptions); cm.AddConjecture(vc, linOptions); @@ -95,33 +95,33 @@ namespace Microsoft.Boogie.Z3 public override void Check() { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; outcome = cm.Check(out z3LabelModels); } public override void CheckAssumptions(List assumptions, out List unsatCore) { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore); } public override void Push() { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.CreateBacktrackPoint(); } public override void Pop() { - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.Backtrack(); } public override void Assert(VCExpr vc, bool polarity) { LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; if (polarity) cm.AddAxiom(vc, linOptions); else @@ -131,7 +131,7 @@ namespace Microsoft.Boogie.Z3 public override void AssertAxioms() { LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - Z3SafeContext cm = context.cm; + Z3Context cm = context.cm; cm.AddAxiom(context.Axioms, linOptions); } @@ -191,13 +191,13 @@ namespace Microsoft.Boogie.Z3 public class Z3apiProverContext : DeclFreeProverContext { - public Z3SafeContext cm; + public Z3Context cm; public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen) : base(gen, new VCGenerationOptions(new List())) { Z3Config config = BuildConfig(opts.Timeout * 1000, true); - this.cm = new Z3SafeContext(this, config, gen); + this.cm = new Z3Context(this, config, gen); } private static Z3Config BuildConfig(int timeout, bool nativeBv) { diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 30207e75..72192804 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -12,641 +12,5 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie.Z3 { - internal class Z3TypeSafeTerm : Z3TermAst - { - private Term termAst; - public Z3TypeSafeTerm(Term termAst) - { - this.termAst = termAst; - } - public Term TermAst - { - get { return this.termAst; } - } - } - - internal class Z3TypeSafePattern : Z3PatternAst - { - private Pattern patternAst; - public Z3TypeSafePattern(Pattern patternAst) - { - this.patternAst = patternAst; - } - public Pattern PatternAst - { - get { return this.patternAst; } - } - } - - internal class Z3TypeSafeConstDecl : Z3ConstDeclAst - { - private FuncDecl constDeclAst; - public Z3TypeSafeConstDecl(FuncDecl constDeclAst) - { - this.constDeclAst = constDeclAst; - } - public FuncDecl ConstDeclAst - { - get { return this.constDeclAst; } - } - } - - public class Z3SafeType : Z3Type - { - private Sort typeAst; - public Z3SafeType(Sort typeAst) - { - this.typeAst = typeAst; - } - public Sort TypeAst - { - get { return this.typeAst; } - } - } - - public class Z3SafeLabeledLiterals : Z3LabeledLiterals - { - private LabeledLiterals labeledLiterals; - public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals) - { - this.labeledLiterals = labeledLiterals; - } - public LabeledLiterals LabeledLiterals - { - get { return this.labeledLiterals; } - } - } - - public class Z3SafeContext : Z3Context - { - private BacktrackDictionary symbols = new BacktrackDictionary(); - internal BacktrackDictionary constants = new BacktrackDictionary(); - internal BacktrackDictionary functions = new BacktrackDictionary(); - internal BacktrackDictionary labels = new BacktrackDictionary(); - - public Context z3; - public Z3Config config; - public Z3apiProverContext ctxt; - private VCExpressionGenerator gen; - private Z3TypeCachedBuilder tm; - private UniqueNamer namer; - public UniqueNamer Namer - { - get { return namer; } - } - private StreamWriter z3log; - public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen) - { - Context z3 = new Context(config.Config); - if (config.LogFilename != null) - z3.OpenLog(config.LogFilename); - foreach (string tag in config.DebugTraces) - z3.EnableDebugTrace(tag); - this.ctxt = ctxt; - this.z3 = z3; - this.config = config; - this.tm = new Z3TypeCachedBuilder(this); - this.gen = gen; - this.namer = new UniqueNamer(); - this.z3.SetPrintMode(PrintMode.Smtlib2Compliant); - this.z3log = null; - } - - public void log(string format, params object[] args) - { - // Currently, this is a no-op because z3log is always null - // We use the default (automatic) tracing facility of z3 - if (z3log != null) - { - var str = string.Format(format, args); - // Do standard string replacement - str = str.Replace("array", "Array"); - z3log.WriteLine(str); - z3log.Flush(); - } - } - - public void CloseLog() - { - z3.CloseLog(); - if (z3log != null) - { - z3log.Close(); - } - z3log = null; - } - - public void CreateBacktrackPoint() - { - symbols.CreateBacktrackPoint(); - constants.CreateBacktrackPoint(); - functions.CreateBacktrackPoint(); - labels.CreateBacktrackPoint(); - z3.Push(); - log("(push)"); - } - - public void Backtrack() - { - z3.Pop(); - labels.Backtrack(); - functions.Backtrack(); - constants.Backtrack(); - symbols.Backtrack(); - log("(pop)"); - } - - public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) - { - Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); - Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions); - Term term = Unwrap(z3ast); - log("(assert {0})", term); - z3.AssertCnstr(term); - } - - public void AddConjecture(VCExpr vc, LineariserOptions linOptions) - { - VCExpr not_vc = (VCExpr)this.gen.Not(vc); - Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); - Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions); - Term term = Unwrap(z3ast); - log("(assert {0})", term); - z3.AssertCnstr(term); - } - - public void AddSmtlibString(string smtlibString) - { - FuncDecl[] decls; - Term[] assumptions; - Term[] terms; - Sort[] sorts; - string tmp; - - z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { }, - out assumptions, out terms, out decls, out sorts, out tmp); - // TBD: check with Nikolaj about the correct position of assumptions - foreach (FuncDecl decl in decls) - { - Symbol symbol = z3.GetDeclName(decl); - string functionName = z3.GetSymbolString(symbol); - functions.Add(functionName, new Z3TypeSafeConstDecl(decl)); - } - foreach (Term assumption in assumptions) - { - log("(assert {0})", assumption); - z3.AssertCnstr(assumption); - } - } - - public string GetDeclName(Z3ConstDeclAst constDeclAst) - { - Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst; - Symbol symbol = z3.GetDeclName(typeSafeConstDecl.ConstDeclAst); - return z3.GetSymbolString(symbol); - } - - private List Unwrap(List terms) - { - List unwrap = new List(); - foreach (Z3TermAst term in terms) - { - Term unwrapTerm = Unwrap(term); - unwrap.Add(unwrapTerm); - } - return unwrap; - } - - private List Unwrap(List patterns) - { - List unwrap = new List(); - foreach (Z3PatternAst pattern in patterns) - { - Z3TypeSafePattern typeSafePattern = (Z3TypeSafePattern)pattern; - unwrap.Add(typeSafePattern.PatternAst); - } - return unwrap; - } - - private Sort Unwrap(Z3Type type) - { - Z3SafeType typeSafeTerm = (Z3SafeType)type; - return typeSafeTerm.TypeAst; - } - - private Term Unwrap(Z3TermAst term) - { - Z3TypeSafeTerm typeSafeTerm = (Z3TypeSafeTerm)term; - return typeSafeTerm.TermAst; - } - - private FuncDecl Unwrap(Z3ConstDeclAst constDeclAst) - { - Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst; - return typeSafeConstDecl.ConstDeclAst; - } - - private Z3TypeSafeTerm Wrap(Term term) - { - return new Z3TypeSafeTerm(term); - } - - private Z3TypeSafeConstDecl Wrap(FuncDecl constDecl) - { - return new Z3TypeSafeConstDecl(constDecl); - } - - private Z3TypeSafePattern Wrap(Pattern pattern) - { - return new Z3TypeSafePattern(pattern); - } - - public Z3PatternAst MakePattern(List exprs) - { - List unwrapExprs = Unwrap(exprs); - Pattern pattern = z3.MkPattern(unwrapExprs.ToArray()); - Z3PatternAst wrapPattern = Wrap(pattern); - return wrapPattern; - } - - private List GetTypes(List boogieTypes) - { - List z3Types = new List(); - foreach (Type boogieType in boogieTypes) - { - Z3Type type = tm.GetType(boogieType); - Sort unwrapType = Unwrap(type); - z3Types.Add(unwrapType); - } - return z3Types; - } - - public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) - { - List unwrapPatterns = Unwrap(patterns); - List unwrapNoPatterns = Unwrap(no_patterns); - Term unwrapBody = Unwrap(body); - - List bound = new List(); - for (int i = 0; i < varNames.Count; i++) - { - Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]); - bound.Add(Unwrap(t)); - } - - Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody); - return Wrap(termAst); - } - private static bool Equals(List l, List r) - { - Debug.Assert(l != null); - if (r == null) - return false; - - if (l.Count != r.Count) - return false; - - for (int i = 0; i < l.Count; i++) - if (!l[i].Equals(r[i])) - return false; - return true; - } - - private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List relevantLabels) - { - BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model); - Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model); - return new Z3ErrorModelAndLabels(boogieModel, new List(relevantLabels)); - } - - private void DisplayRelevantLabels(List relevantLabels) - { - foreach (string labelName in relevantLabels) - { - System.Console.Write(labelName + ","); - } - System.Console.WriteLine("---"); - } - - public ProverInterface.Outcome Check(out List boogieErrors) - { - Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover"); - boogieErrors = new List(); - LBool outcome = LBool.Undef; - Debug.Assert(0 < this.config.Counterexamples); - while (true) - { - Model z3Model; - outcome = z3.CheckAndGetModel(out z3Model); - log("(check-sat)"); - if (outcome == LBool.False) - break; - - if (outcome == LBool.Undef && z3Model == null) - { - // Blame this on timeout - return ProverInterface.Outcome.TimeOut; - } - - Debug.Assert(z3Model != null); - LabeledLiterals labels = z3.GetRelevantLabels(); - Debug.Assert(labels != null); - - List labelStrings = new List(); - uint numLabels = labels.GetNumLabels(); - for (uint i = 0; i < numLabels; ++i) - { - Symbol sym = labels.GetLabel(i); - string labelName = z3.GetSymbolString(sym); - if (!labelName.StartsWith("@")) - { - labels.Disable(i); - } - labelStrings.Add(labelName); - } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); - - if (boogieErrors.Count < this.config.Counterexamples) - { - z3.BlockLiterals(labels); - log("block-literals {0}", labels); - } - - labels.Dispose(); - z3Model.Dispose(); - if (boogieErrors.Count == this.config.Counterexamples) - break; - } - - if (boogieErrors.Count > 0) - { - return ProverInterface.Outcome.Invalid; - } - else if (outcome == LBool.False) - { - return ProverInterface.Outcome.Valid; - } - else - { - Debug.Assert(outcome == LBool.Undef); - return ProverInterface.Outcome.Undetermined; - } - } - - public ProverInterface.Outcome CheckAssumptions(List assumptions, LineariserOptions linOptions, - out List boogieErrors, - out List unsatCore) - { - Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover"); - boogieErrors = new List(); - unsatCore = new List(); - LBool outcome = LBool.Undef; - - Model z3Model; - Term proof; - Term[] core; - Term[] assumption_terms = new Term[assumptions.Count]; - var logstring = ""; - for (int i = 0; i < assumptions.Count; i++) - { - Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); - Z3TermAst z3ast = (Z3TermAst)assumptions[i].Accept(visitor, linOptions); - assumption_terms[i] = Unwrap(z3ast); - logstring += string.Format("({0}) ", assumption_terms[i]); - } - - log("(get-core {0})", logstring); - outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core); - - if (outcome != LBool.False) - { - Debug.Assert(z3Model != null); - LabeledLiterals labels = z3.GetRelevantLabels(); - Debug.Assert(labels != null); - - List labelStrings = new List(); - uint numLabels = labels.GetNumLabels(); - for (uint i = 0; i < numLabels; ++i) - { - Symbol sym = labels.GetLabel(i); - string labelName = z3.GetSymbolString(sym); - if (!labelName.StartsWith("@")) - { - labels.Disable(i); - } - labelStrings.Add(labelName); - } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); - - labels.Dispose(); - z3Model.Dispose(); - } - - if (boogieErrors.Count > 0) - { - return ProverInterface.Outcome.Invalid; - } - else if (outcome == LBool.False) - { - foreach (Term t in core) - { - for (int i = 0; i < assumption_terms.Length; i++) - { - if (t.Equals(assumption_terms[i])) - unsatCore.Add(i); - } - } - return ProverInterface.Outcome.Valid; - } - else - { - Debug.Assert(outcome == LBool.Undef); - return ProverInterface.Outcome.Undetermined; - } - } - - public void TypeCheckBool(Z3TermAst term) - { - Term unwrapTerm = Unwrap(term); - bool boolType = z3.GetSort(unwrapTerm).Equals(z3.MkBoolSort()); - if (!boolType) - throw new Exception("Failed Bool Typecheck"); - } - - public void TypeCheckInt(Z3TermAst term) - { - Term unwrapTerm = Unwrap(term); - bool intType = z3.GetSort(unwrapTerm).Equals(z3.MkIntSort()); - if (!intType) - throw new Exception("Failed Int Typecheck"); - } - - public void DeclareType(string typeName) - { - log("(declare-sort {0})", typeName); - } - - public void DeclareConstant(string constantName, Type boogieType) - { - Symbol symbolAst = GetSymbol(constantName); - Z3Type typeAst = tm.GetType(boogieType); - Sort unwrapTypeAst = Unwrap(typeAst); - - Term constAst = z3.MkConst(symbolAst, unwrapTypeAst); - constants.Add(constantName, Wrap(constAst)); - log("(declare-funs (({0} {1})))", constAst, unwrapTypeAst); - } - - public void DeclareFunction(string functionName, List domain, Type range) - { - Symbol symbolAst = GetSymbol(functionName); - - var domainStr = ""; - List domainAst = new List(); - foreach (Type domainType in domain) - { - Z3Type type = tm.GetType(domainType); - Sort unwrapType = Unwrap(type); - domainAst.Add(unwrapType); - domainStr += unwrapType.ToString() + " "; - } - Z3Type rangeAst = tm.GetType(range); - Sort unwrapRangeAst = Unwrap(rangeAst); - FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), unwrapRangeAst); - Z3TypeSafeConstDecl typeSafeConstDecl = Wrap(constDeclAst); - functions.Add(functionName, typeSafeConstDecl); - log("(declare-funs (({0} {1} {2})))", functionName, domainStr, unwrapRangeAst); - } - - private List GetSymbols(List symbolNames) - { - List symbols = new List(); - foreach (string symbolName in symbolNames) - symbols.Add(GetSymbol(symbolName)); - return symbols; - } - - private Symbol GetSymbol(string symbolName) - { - if (!symbols.ContainsKey(symbolName)) - { - Symbol symbolAst = z3.MkSymbol(symbolName); - symbols.Add(symbolName, symbolAst); - } - Symbol result; - if (!symbols.TryGetValue(symbolName, out result)) - throw new Exception("symbol " + symbolName + " is undefined"); - return result; - } - - public Z3TermAst GetConstant(string constantName, Type constantType) - { - Z3TypeSafeTerm typeSafeTerm; - if (!constants.ContainsKey(constantName)) - this.DeclareConstant(constantName, constantType); - - if (!constants.TryGetValue(constantName, out typeSafeTerm)) - throw new Exception("constant " + constantName + " is not defined"); - return typeSafeTerm; - } - - public Z3TermAst MakeIntLiteral(string numeral) - { - Term term = z3.MkNumeral(numeral, z3.MkIntSort()); - Z3TypeSafeTerm typeSafeTerm = Wrap(term); - return typeSafeTerm; - } - - public Z3TermAst MakeTrue() - { - Term term = z3.MkTrue(); - Z3TypeSafeTerm typeSafeTerm = Wrap(term); - return typeSafeTerm; - } - - public Z3TermAst MakeFalse() - { - Term term = z3.MkFalse(); - Z3TypeSafeTerm typeSafeTerm = Wrap(term); - return typeSafeTerm; - } - - public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) - { - Symbol labelSymbol = this.GetSymbol(labelName); - Term unwrapChild = Unwrap(child); - - Term labeledExpr = z3.MkLabel(labelSymbol, pos, unwrapChild); - - Z3TypeSafeTerm wrapLabeledExpr = Wrap(labeledExpr); - labels.Add(labelName, wrapLabeledExpr); - return wrapLabeledExpr; - } - - public Z3LabeledLiterals GetRelevantLabels() - { - Z3SafeLabeledLiterals safeLiterals = new Z3SafeLabeledLiterals(z3.GetRelevantLabels()); - log("get-relevant-labels"); - return safeLiterals; - } - - public Z3TermAst Make(string op, List children) - { - Term[] unwrapChildren = Unwrap(children).ToArray(); - Term term; - switch (op) - { - // formulas - case "AND": term = z3.MkAnd(unwrapChildren); break; - case "OR": term = z3.MkOr(unwrapChildren); break; - case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break; - case "NOT": term = z3.MkNot(unwrapChildren[0]); break; - case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break; - // terms - case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break; - case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break; - case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break; - // terms - case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break; - case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break; - case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break; - case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break; - case "+": term = z3.MkAdd(unwrapChildren); break; - case "-": term = z3.MkSub(unwrapChildren); break; - case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break; - case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break; - case "*": term = z3.MkMul(unwrapChildren); break; - default: - { - FuncDecl f = GetFunction(op); - term = z3.MkApp(f, unwrapChildren); - } - break; - } - Z3TypeSafeTerm typeSafeTerm = Wrap(term); - return typeSafeTerm; - } - - private FuncDecl GetFunction(string functionName) - { - Z3TypeSafeConstDecl function; - if (!functions.TryGetValue(functionName, out function)) - throw new Exception("function " + functionName + " is undefined"); - FuncDecl unwrapFunction = Unwrap(function); - return unwrapFunction; - } - - public Z3TermAst MakeArraySelect(List args) - { - Term[] unwrapChildren = Unwrap(args).ToArray(); - return Wrap(z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1])); - } - - public Z3TermAst MakeArrayStore(List args) - { - Term[] unwrapChildren = Unwrap(args).ToArray(); - return Wrap(z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2])); - } - } } \ No newline at end of file diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs index b8aa607f..b129b378 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -45,6 +45,9 @@ namespace Microsoft.Boogie.Z3 { public Z3TermAst MakeIntLiteral(string numeral) { return new Z3StubTermAst(); } + public Z3TermAst MakeBvLiteral(int i, uint bvSize) { + return new Z3StubTermAst(); + } public Z3TermAst MakeTrue() { return new Z3StubTermAst(); } diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index dec25e97..de5ebd8f 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -75,10 +75,10 @@ namespace Microsoft.Boogie.Z3 } } - private Dictionary mapTypes = new Dictionary(new MapTypeComparator()); - private Dictionary bvTypes = new Dictionary(new BvTypeComparator()); - private Dictionary basicTypes = new Dictionary(new BasicTypeComparator()); - private Dictionary ctorTypes = new Dictionary(new CtorTypeComparator()); + private Dictionary mapTypes = new Dictionary(new MapTypeComparator()); + private Dictionary bvTypes = new Dictionary(new BvTypeComparator()); + private Dictionary basicTypes = new Dictionary(new BasicTypeComparator()); + private Dictionary ctorTypes = new Dictionary(new CtorTypeComparator()); private Z3Context container; @@ -87,61 +87,61 @@ namespace Microsoft.Boogie.Z3 this.container = context; } - private Z3Type GetMapType(MapType mapType) + private Sort GetMapType(MapType mapType) { - Context z3 = ((Z3SafeContext)container).z3; + Context z3 = ((Z3Context)container).z3; if (!mapTypes.ContainsKey(mapType)) { Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1"); - Z3Type domain = GetType(mapType.Arguments[0]); - Z3Type range = GetType(mapType.Result); - Z3Type typeAst = BuildMapType(domain, range); + Sort domain = GetType(mapType.Arguments[0]); + Sort range = GetType(mapType.Result); + Sort typeAst = BuildMapType(domain, range); mapTypes.Add(mapType, typeAst); } - Z3Type result; + Sort result; bool containsKey = mapTypes.TryGetValue(mapType, out result); Debug.Assert(containsKey); return result; } - private Z3Type GetBvType(BvType bvType) + private Sort GetBvType(BvType bvType) { if (!bvTypes.ContainsKey(bvType)) { - Z3Type typeAst = BuildBvType(bvType); + Sort typeAst = BuildBvType(bvType); bvTypes.Add(bvType, typeAst); } - Z3Type result; + Sort result; bool containsKey = bvTypes.TryGetValue(bvType, out result); Debug.Assert(containsKey); return result; } - private Z3Type GetBasicType(BasicType basicType) + private Sort GetBasicType(BasicType basicType) { if (!basicTypes.ContainsKey(basicType)) { - Z3Type typeAst = BuildBasicType(basicType); + Sort typeAst = BuildBasicType(basicType); basicTypes.Add(basicType, typeAst); } - Z3Type result; + Sort result; bool containsKey = basicTypes.TryGetValue(basicType, out result); Debug.Assert(containsKey); return result; } - private Z3Type GetCtorType(CtorType ctorType) { + private Sort GetCtorType(CtorType ctorType) { if (!ctorTypes.ContainsKey(ctorType)) { - Z3Type typeAst = BuildCtorType(ctorType); + Sort typeAst = BuildCtorType(ctorType); ctorTypes.Add(ctorType, typeAst); } - Z3Type result; + Sort result; bool containsKey = ctorTypes.TryGetValue(ctorType, out result); Debug.Assert(containsKey); return result; } - public virtual Z3Type GetType(Type boogieType) { + public virtual Sort GetType(Type boogieType) { System.Type type = boogieType.GetType(); if (type.Equals(typeof(BvType))) return GetBvType((BvType)boogieType); @@ -155,28 +155,23 @@ namespace Microsoft.Boogie.Z3 throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown"); } - private Z3Type WrapType(Sort typeAst) + public Sort BuildMapType(Sort domain, Sort range) { - return new Z3SafeType(typeAst); + Context z3 = ((Z3Context)container).z3; + Sort typeAst = z3.MkArraySort(domain, range); + return typeAst; } - public Z3Type BuildMapType(Z3Type domain, Z3Type range) + public Sort BuildBvType(BvType bvType) { - Context z3 = ((Z3SafeContext)container).z3; - Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst); - return WrapType(typeAst); - } - - public Z3Type BuildBvType(BvType bvType) - { - Context z3 = ((Z3SafeContext)container).z3; + Context z3 = ((Z3Context)container).z3; Sort typeAst = z3.MkBvSort((uint)bvType.Bits); - return WrapType(typeAst); + return typeAst; } - public Z3Type BuildBasicType(BasicType basicType) + public Sort BuildBasicType(BasicType basicType) { - Context z3 = ((Z3SafeContext)container).z3; + Context z3 = ((Z3Context)container).z3; Sort typeAst; if (basicType.IsBool) { @@ -188,18 +183,16 @@ namespace Microsoft.Boogie.Z3 } else throw new Exception("Unknown Basic Type " + basicType.ToString()); - return WrapType(typeAst); + return typeAst; } - public Z3Type BuildCtorType(CtorType ctorType) { - Context z3 = ((Z3SafeContext)container).z3; + public Sort BuildCtorType(CtorType ctorType) { + Context z3 = ((Z3Context)container).z3; Sort typeAst; if (ctorType.Arguments.Length > 0) throw new Exception("Type constructor of non-zero arity are not handled"); typeAst = z3.MkSort(ctorType.Decl.Name); - return WrapType(typeAst); + return typeAst; } } - - public class Z3Type { } } \ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index c2eeb45f..aa47d7e0 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -11,13 +11,14 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; +using Microsoft.Z3; namespace Microsoft.Boogie.Z3 { - public class Z3apiExprLineariser : IVCExprVisitor + public class Z3apiExprLineariser : IVCExprVisitor { private Z3apiOpLineariser OpLinObject = null; - private IVCExprOpVisitor OpLineariser + private IVCExprOpVisitor OpLineariser { get { @@ -29,36 +30,36 @@ namespace Microsoft.Boogie.Z3 } internal readonly UniqueNamer namer; - internal readonly Dictionary letBindings; + internal readonly Dictionary letBindings; protected Z3Context cm; public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer) { this.cm = cm; this.namer = namer; - this.letBindings = new Dictionary(); + this.letBindings = new Dictionary(); } - public Z3TermAst Linearise(VCExpr expr, LineariserOptions options) + public Term Linearise(VCExpr expr, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(expr != null); - return expr.Accept(this, options); + return expr.Accept(this, options); } ///////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options) + public Term Visit(VCExprLiteral node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); if (node == VCExpressionGenerator.True) - return cm.MakeTrue(); + return cm.z3.MkTrue(); else if (node == VCExpressionGenerator.False) - return cm.MakeFalse(); + return cm.z3.MkFalse(); else if (node is VCExprIntLit) - return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString()); + return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort()); else { Contract.Assert(false); @@ -66,7 +67,7 @@ namespace Microsoft.Boogie.Z3 } } - public Z3TermAst Visit(VCExprNAry node, LineariserOptions options) + public Term Visit(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -76,7 +77,7 @@ namespace Microsoft.Boogie.Z3 if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp)) { // handle these operators without recursion - List asts = new List(); + List asts = new List(); string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR"; IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); @@ -93,10 +94,10 @@ namespace Microsoft.Boogie.Z3 return cm.Make(opString, asts); } - return node.Accept(OpLineariser, options); + return node.Accept(OpLineariser, options); } - public Z3TermAst Visit(VCExprVar node, LineariserOptions options) + public Term Visit(VCExprVar node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -111,7 +112,7 @@ namespace Microsoft.Boogie.Z3 } } - public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options) + public Term Visit(VCExprQuantifier node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -123,11 +124,11 @@ namespace Microsoft.Boogie.Z3 List varNames; List varTypes; VisitBounds(node.BoundVars, out varNames, out varTypes); - List patterns; - List no_patterns; + List patterns; + List no_patterns; VisitTriggers(node.Triggers, options, out patterns, out no_patterns); - Z3TermAst body = Linearise(node.Body, options); - Z3TermAst result; + Term body = Linearise(node.Body, options); + Term result; uint weight = 1; string qid = ""; int skolemid = 0; @@ -153,9 +154,9 @@ namespace Microsoft.Boogie.Z3 switch (node.Quan) { - case Quantifier.ALL: + case Microsoft.Boogie.VCExprAST.Quantifier.ALL: result = cm.MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break; - case Quantifier.EX: + case Microsoft.Boogie.VCExprAST.Quantifier.EX: result = cm.MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break; default: throw new Exception("unknown quantifier kind " + node.Quan); @@ -180,44 +181,44 @@ namespace Microsoft.Boogie.Z3 } } - private void VisitTriggers(List triggers, LineariserOptions options, out List patterns, out List no_patterns) + private void VisitTriggers(List triggers, LineariserOptions options, out List patterns, out List no_patterns) { - patterns = new List(); - no_patterns = new List(); + patterns = new List(); + no_patterns = new List(); foreach (VCTrigger trigger in triggers) { - List exprs = new List(); + List exprs = new List(); foreach (VCExpr expr in trigger.Exprs) { System.Diagnostics.Debug.Assert(expr != null); - Z3TermAst termAst = Linearise(expr, options); + Term termAst = Linearise(expr, options); exprs.Add(termAst); } if (exprs.Count > 0) { if (trigger.Pos) { - Z3PatternAst pattern = cm.MakePattern(exprs); + Pattern pattern = cm.MakePattern(exprs); patterns.Add(pattern); } else { System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats"); - foreach (Z3TermAst expr in exprs) + foreach (Term expr in exprs) no_patterns.Add(expr); } } } } - public Z3TermAst Visit(VCExprLet node, LineariserOptions options) + public Term Visit(VCExprLet node, LineariserOptions options) { foreach (VCExprLetBinding b in node) { - Z3TermAst defAst = Linearise(b.E, options); + Term defAst = Linearise(b.E, options); letBindings.Add(b.V, defAst); } - Z3TermAst letAst = Linearise(node.Body, options); + Term letAst = Linearise(node.Body, options); foreach (VCExprLetBinding b in node) { letBindings.Remove(b.V); @@ -227,7 +228,7 @@ namespace Microsoft.Boogie.Z3 ///////////////////////////////////////////////////////////////////////////////////// - internal class Z3apiOpLineariser : IVCExprOpVisitor + internal class Z3apiOpLineariser : IVCExprOpVisitor { [ContractInvariantMethod] void ObjectInvariant() @@ -245,13 +246,13 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////// - private Z3TermAst WriteApplication(string op, IEnumerable terms, LineariserOptions options) + private Term WriteApplication(string op, IEnumerable terms, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(op != null); Contract.Requires(cce.NonNullElements(terms)); - List args = new List(); + List args = new List(); foreach (VCExpr e in terms) { Contract.Assert(e != null); @@ -262,51 +263,51 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst VisitNotOp(VCExprNAry node, LineariserOptions options) + public Term VisitNotOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("NOT", node, options); } - public Z3TermAst VisitEqOp(VCExprNAry node, LineariserOptions options) + public Term VisitEqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("EQ", node, options); } - public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options) + public Term VisitNeqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("NEQ", node, options); } - public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options) + public Term VisitAndOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("AND", node, options); } - public Z3TermAst VisitOrOp(VCExprNAry node, LineariserOptions options) + public Term VisitOrOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("OR", node, options); } - public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options) + public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); if (options.InverseImplies) { - List args = new List(); + List args = new List(); args.Add(ExprLineariser.Linearise(node[1], options)); - List t = new List(); + List t = new List(); t.Add(ExprLineariser.Linearise(node[0], options)); args.Add(ExprLineariser.cm.Make("NOT", t)); return ExprLineariser.cm.Make("OR", args); @@ -317,7 +318,7 @@ namespace Microsoft.Boogie.Z3 } } - public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options) + public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -328,7 +329,7 @@ namespace Microsoft.Boogie.Z3 } else { - List args = new List(); + List args = new List(); foreach (VCExpr e in node) { Contract.Assert(e != null); @@ -338,7 +339,7 @@ namespace Microsoft.Boogie.Z3 } } - public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options) + public Term VisitLabelOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -347,73 +348,103 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); } - public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options) + public Term VisitSelectOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - List args = new List(); + List args = new List(); foreach (VCExpr e in node) { Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - return ExprLineariser.cm.MakeArraySelect(args); + + Term[] unwrapChildren = args.ToArray(); + return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]); // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args); } - public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options) + public Term VisitStoreOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - List args = new List(); + List args = new List(); foreach (VCExpr e in node) { Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - return ExprLineariser.cm.MakeArrayStore(args); + + Term[] unwrapChildren = args.ToArray(); + return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args); } - public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options) + public Term VisitBvOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("$make_bv" + node.Type.BvBits, node, options); + List args = new List(); + foreach (VCExpr e in node) { + VCExprIntLit literal = e as VCExprIntLit; + System.Diagnostics.Debug.Assert(literal != null); + args.Add(literal.Val.ToInt); + } + System.Diagnostics.Debug.Assert(args.Count == 1); + return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits)); } - public Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options) - { - Contract.Requires(options != null); - Contract.Requires(node != null); - return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options); + public Term VisitBvExtractOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + + VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op; + Contract.Assert(op != null); + System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End); + + List args = new List(); + foreach (VCExpr e in node) { + Contract.Assert(e != null); + args.Add(ExprLineariser.Linearise(e, options)); + } + System.Diagnostics.Debug.Assert(args.Count == 1); + return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]); } - public Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options) - { - Contract.Requires(options != null); - Contract.Requires(node != null); - return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options); + public Term VisitBvConcatOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + + VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op; + Contract.Assert(op != null); + + List args = new List(); + foreach (VCExpr e in node) { + Contract.Assert(e != null); + args.Add(ExprLineariser.Linearise(e, options)); + } + System.Diagnostics.Debug.Assert(args.Count == 2); + return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]); } - public Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) + public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - List args = new List(); + List args = new List(); args.Add(ExprLineariser.Linearise(node[0], options)); args.Add(ExprLineariser.Linearise(node[1], options)); args.Add(ExprLineariser.Linearise(node[2], options)); return ExprLineariser.cm.Make("ITE", args); } - public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options) + public Term VisitCustomOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(node != null); Contract.Requires(options != null); VCExprCustomOp op = (VCExprCustomOp)node.Op; - List args = new List(); + List args = new List(); foreach (VCExpr arg in node) { args.Add(ExprLineariser.Linearise(arg, options)); @@ -421,7 +452,7 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.Make(op.Name, args); } - public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options) + public Term VisitAddOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -435,77 +466,77 @@ namespace Microsoft.Boogie.Z3 } } - public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options) + public Term VisitSubOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("-", node, options); } - public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options) + public Term VisitMulOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("*", node, options); } - public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options) + public Term VisitDivOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("/", node, options); } - public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options) + public Term VisitModOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("%", node, options); } - public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options) + public Term VisitLtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("<", node, options); } - public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options) + public Term VisitLeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("<=", node, options); } - public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options) + public Term VisitGtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication(">", node, options); } - public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options) + public Term VisitGeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication(">=", node, options); } - public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options) + public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("<:", node, options); } - public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options) + public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); return WriteApplication("<::", node, options); } - public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) + public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); @@ -516,7 +547,7 @@ namespace Microsoft.Boogie.Z3 string bvzName = op.Func.FindStringAttribute("external"); if (bvzName != null) funcName = bvzName; - List args = new List(); + List args = new List(); foreach (VCExpr e in node) { Contract.Assert(e != null); diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 05cc8f9f..e02243ce 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -169,8 +169,6 @@ - - Code diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index 08a27b9b..e9bc968e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,17 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe -for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do ( +for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do ( echo. echo -------------------- %%f -------------------- %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f ) -REM boog8.bpl + REM boog12.bpl -REM boog14.bpl REM boog15.bpl -REM boog16.bpl -REM boog17.bpl REM boog19.bpl REM boog23.bpl -- cgit v1.2.3 From c57b12c920527690c1fd234e14ef7ca1c09e4185 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 24 Jun 2011 06:53:00 -0700 Subject: fixes to z3api --- Source/Provers/Z3api/ContextLayer.cs | 336 ++++++++++++---------------------- Source/Provers/Z3api/ProverLayer.cs | 9 +- Source/Provers/Z3api/TypeAdapter.cs | 34 ++-- Source/Provers/Z3api/VCExprVisitor.cs | 150 ++++++--------- Source/Provers/Z3api/Z3api.csproj | 8 + Test/z3api/Answer | 174 ++++++++++++------ Test/z3api/runtest.bat | 13 +- 7 files changed, 319 insertions(+), 405 deletions(-) (limited to 'Test') diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index ed45c4fc..390d875d 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -11,6 +11,9 @@ using Microsoft.Z3; using Microsoft.Boogie.VCExprAST; using Microsoft.Basetypes; +using Z3Model = Microsoft.Z3.Model; +using BoogieModel = Microsoft.Boogie.Model; + namespace Microsoft.Boogie.Z3 { public class Z3Config @@ -20,21 +23,6 @@ namespace Microsoft.Boogie.Z3 private string logFilename; private List debugTraces = new List(); - public void SetModel(bool enabled) - { - config.SetParamValue("MODEL", (enabled ? "true" : "false")); - } - - public void SetSoftTimeout(string timeout) - { - config.SetParamValue("SOFT_TIMEOUT", timeout); - } - - public void SetTypeCheck(bool enabled) - { - config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false")); - } - public void SetCounterExample(int counterexample) { this.counterexamples = counterexample; @@ -69,102 +57,6 @@ namespace Microsoft.Boogie.Z3 } } - internal class PartitionMap - { - private Context ctx; - private Model model; - private Dictionary termToPartition = new Dictionary(); - private Dictionary valueToPartition = new Dictionary(); - private List partitionToValue = new List(); - private int partitionCounter = 0; - public int PartitionCounter { get { return partitionCounter; } } - - public PartitionMap(Context ctx, Model z3Model) - { - this.ctx = ctx; - this.model = z3Model; - } - - public int GetPartition(Term value) - { - int result; - if (!termToPartition.TryGetValue(value, out result)) - { - result = partitionCounter++; - termToPartition.Add(value, result); - partitionToValue.Add(null); - object constant = Evaluate(value); - valueToPartition.Add(constant, result); - partitionToValue[result] = constant; - } - return result; - } - - private object Evaluate(Term v) - { - Sort s = v.GetSort(); - Sort boolSort = ctx.MkBoolSort(); - Sort intSort = ctx.MkIntSort(); - ArrayValue av; - - if (s.Equals(boolSort)) - { - return ctx.GetBoolValue(v); - } - else if (s.Equals(intSort)) { - int i; - long il; - uint u; - ulong ul; - if (ctx.TryGetNumeralInt(v, out i)) { - return BigNum.FromInt(i); - } - else if (ctx.TryGetNumeralInt64(v, out il)) { - return BigNum.FromLong(il); - } - else if (ctx.TryGetNumeralUInt(v, out u)) { - return BigNum.FromUInt(u); - } - else if (ctx.TryGetNumeralUInt64(v, out ul)) { - return BigNum.FromULong(ul); - } - else { - string str = v.ToString(); - return GetPartition(v); - //return BigNum.FromString(ctx.GetNumeralString(v)); - } - } - else if (model.TryGetArrayValue(v, out av)) { - List> arrayValue = new List>(); - List tuple; - for (int i = 0; i < av.Domain.Length; i++) { - tuple = new List(); - tuple.Add(GetPartition(av.Domain[i])); - tuple.Add(GetPartition(av.Range[i])); - arrayValue.Add(tuple); - } - tuple = new List(); - tuple.Add(GetPartition(av.ElseCase)); - arrayValue.Add(tuple); - return arrayValue; - } - else { - // The term is uninterpreted; just return the partition id. - return GetPartition(v); - } - } - - public List PartitionToValue(Context ctx) - { - return partitionToValue; - } - - public Dictionary ValueToPartition(Context ctx) - { - return valueToPartition; - } - } - internal class BacktrackDictionary { private Dictionary dictionary = new Dictionary(); @@ -217,86 +109,11 @@ namespace Microsoft.Boogie.Z3 } } - internal class BoogieErrorModelBuilder - { - private Z3Context container; - private PartitionMap partitionMap; - - public BoogieErrorModelBuilder(Z3Context container, Model z3Model) - { - this.container = container; - this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model); - } - - private Dictionary CreateConstantToPartition(Model z3Model) - { - Dictionary constantToPartition = new Dictionary(); - foreach (FuncDecl c in z3Model.GetModelConstants()) - { - string name = container.GetDeclName(c); - int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0])); - constantToPartition.Add(name, pid); - } - return constantToPartition; - } - - private List> CreatePartitionToConstant(Dictionary constantToPartition) - { - List> partitionToConstant = new List>(); - for (int i = 0; i < partitionMap.PartitionCounter; i++) - { - partitionToConstant.Add(new List()); - } - foreach (string s in constantToPartition.Keys) - { - partitionToConstant[constantToPartition[s]].Add(s); - } - return partitionToConstant; - } - - private Dictionary>> CreateFunctionToPartition(Model z3Model) - { - Dictionary>> functionToPartition = new Dictionary>>(); - - foreach (KeyValuePair kv in z3Model.GetFunctionGraphs()) - { - List> f_tuples = new List>(); - string f_name = container.GetDeclName(kv.Key); - FunctionGraph graph = kv.Value; - foreach (FunctionEntry entry in graph.Entries) - { - List tuple = new List(); - foreach (Term v in entry.Arguments) - { - tuple.Add(partitionMap.GetPartition(z3Model.Eval(v))); - } - tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result))); - f_tuples.Add(tuple); - } - List else_tuple = new List(); - else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else))); - f_tuples.Add(else_tuple); - functionToPartition.Add(f_name, f_tuples); - } - return functionToPartition; - } - - public Z3ErrorModel BuildBoogieModel(Model z3Model) - { - Dictionary constantToPartition = CreateConstantToPartition(z3Model); - Dictionary>> functionToPartition = CreateFunctionToPartition(z3Model); - List> partitionToConstant = CreatePartitionToConstant(constantToPartition); - List partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3); - Dictionary valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3); - return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition); - } - } - public class Z3ErrorModelAndLabels { - private Z3ErrorModel _errorModel; + private ErrorModel _errorModel; private List _relevantLabels; - public Z3ErrorModel ErrorModel + public ErrorModel ErrorModel { get { return this._errorModel; } } @@ -304,7 +121,7 @@ namespace Microsoft.Boogie.Z3 { get { return this._relevantLabels; } } - public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List relevantLabels) + public Z3ErrorModelAndLabels(ErrorModel errorModel, List relevantLabels) { this._errorModel = errorModel; this._relevantLabels = relevantLabels; @@ -461,12 +278,13 @@ namespace Microsoft.Boogie.Z3 return true; } - private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List relevantLabels) { + /* + private Z3ErrorModelAndLabels BuildZ3ErrorModel(Z3Model z3Model, List relevantLabels) { BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model); Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model); return new Z3ErrorModelAndLabels(boogieModel, new List(relevantLabels)); } - + */ private void DisplayRelevantLabels(List relevantLabels) { foreach (string labelName in relevantLabels) { System.Console.Write(labelName + ","); @@ -480,8 +298,9 @@ namespace Microsoft.Boogie.Z3 LBool outcome = LBool.Undef; Debug.Assert(0 < this.config.Counterexamples); while (true) { - Model z3Model; + Z3Model z3Model; outcome = z3.CheckAndGetModel(out z3Model); + log("(check-sat)"); if (outcome == LBool.False) break; @@ -505,13 +324,27 @@ namespace Microsoft.Boogie.Z3 } labelStrings.Add(labelName); } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + + + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List(labelStrings)); + + + boogieErrors.Add(e); if (boogieErrors.Count < this.config.Counterexamples) { z3.BlockLiterals(labels); log("block-literals {0}", labels); } + + labels.Dispose(); z3Model.Dispose(); if (boogieErrors.Count == this.config.Counterexamples) @@ -538,7 +371,7 @@ namespace Microsoft.Boogie.Z3 unsatCore = new List(); LBool outcome = LBool.Undef; - Model z3Model; + Z3Model z3Model; Term proof; Term[] core; Term[] assumption_terms = new Term[assumptions.Count]; @@ -568,7 +401,16 @@ namespace Microsoft.Boogie.Z3 } labelStrings.Add(labelName); } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List(labelStrings)); + boogieErrors.Add(e); labels.Dispose(); z3Model.Dispose(); @@ -668,37 +510,83 @@ namespace Microsoft.Boogie.Z3 return safeLiterals; } - public Term Make(string op, List children) { + public Term Make(VCExprOp op, List children) { Term[] unwrapChildren = children.ToArray(); - Term term; - switch (op) { - // formulas - case "AND": term = z3.MkAnd(unwrapChildren); break; - case "OR": term = z3.MkOr(unwrapChildren); break; - case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break; - case "NOT": term = z3.MkNot(unwrapChildren[0]); break; - case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break; - // terms - case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break; - case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break; - case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break; - // terms - case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break; - case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break; - case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break; - case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break; - case "+": term = z3.MkAdd(unwrapChildren); break; - case "-": term = z3.MkSub(unwrapChildren); break; - case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break; - case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break; - case "*": term = z3.MkMul(unwrapChildren); break; - default: { - FuncDecl f = GetFunction(op); - term = z3.MkApp(f, unwrapChildren); - } - break; + VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp; + if (boogieFunctionOp != null) { + FuncDecl f = GetFunction(boogieFunctionOp.Func.Name); + return z3.MkApp(f, unwrapChildren); + } + VCExprDistinctOp distinctOp = op as VCExprDistinctOp; + if (distinctOp != null) { + return z3.MkDistinct(unwrapChildren); + } + + if (op == VCExpressionGenerator.AndOp) { + return z3.MkAnd(unwrapChildren); + } + + if (op == VCExpressionGenerator.OrOp) { + return z3.MkOr(unwrapChildren); + } + + if (op == VCExpressionGenerator.ImpliesOp) { + return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NotOp) { + return z3.MkNot(unwrapChildren[0]); + } + + if (op == VCExpressionGenerator.EqOp) { + return z3.MkEq(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NeqOp) { + return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); + } + + if (op == VCExpressionGenerator.LtOp) { + return z3.MkLt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.LeOp) { + return z3.MkLe(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GtOp) { + return z3.MkGt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GeOp) { + return z3.MkGe(unwrapChildren[0], unwrapChildren[1]); } - return term; + + if (op == VCExpressionGenerator.AddOp) { + return z3.MkAdd(unwrapChildren); + } + + if (op == VCExpressionGenerator.SubOp) { + return z3.MkSub(unwrapChildren); + } + + if (op == VCExpressionGenerator.DivOp) { + return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.MulOp) { + return z3.MkMul(unwrapChildren); + } + + if (op == VCExpressionGenerator.ModOp) { + return z3.MkMod(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.IfThenElseOp) { + return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); + } + + throw new Exception("unhandled boogie operator"); } } } \ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index f691cffc..39acc5db 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -202,7 +202,10 @@ namespace Microsoft.Boogie.Z3 private static Z3Config BuildConfig(int timeout, bool nativeBv) { Z3Config config = new Z3Config(); - config.SetModel(true); + config.Config.SetParamValue("MODEL", "true"); + config.Config.SetParamValue("MODEL_V2", "true"); + config.Config.SetParamValue("MODEL_COMPLETION", "true"); + config.Config.SetParamValue("MBQI", "false"); if (0 <= CommandLineOptions.Clo.ProverCCLimit) { @@ -211,7 +214,7 @@ namespace Microsoft.Boogie.Z3 if (0 <= timeout) { - config.SetSoftTimeout(timeout.ToString()); + config.Config.SetParamValue("SOFT_TIMEOUT", timeout.ToString()); } if (CommandLineOptions.Clo.SimplifyLogFilePath != null) @@ -219,7 +222,7 @@ namespace Microsoft.Boogie.Z3 config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath); } - config.SetTypeCheck(true); + config.Config.SetParamValue("TYPE_CHECK", "true"); return config; } diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index de5ebd8f..b0dd1eb4 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -87,21 +87,17 @@ namespace Microsoft.Boogie.Z3 this.container = context; } - private Sort GetMapType(MapType mapType) - { - Context z3 = ((Z3Context)container).z3; - if (!mapTypes.ContainsKey(mapType)) - { - Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1"); - Sort domain = GetType(mapType.Arguments[0]); - Sort range = GetType(mapType.Result); - Sort typeAst = BuildMapType(domain, range); - mapTypes.Add(mapType, typeAst); + private Sort GetMapType(MapType mapType) { + Context z3 = ((Z3Context)container).z3; + if (!mapTypes.ContainsKey(mapType)) { + Type result = mapType.Result; + for (int i = mapType.Arguments.Length-1; i > 0; i--) { + GetType(result); + result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result); } - Sort result; - bool containsKey = mapTypes.TryGetValue(mapType, out result); - Debug.Assert(containsKey); - return result; + mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result))); + } + return mapTypes[mapType]; } private Sort GetBvType(BvType bvType) @@ -158,15 +154,13 @@ namespace Microsoft.Boogie.Z3 public Sort BuildMapType(Sort domain, Sort range) { Context z3 = ((Z3Context)container).z3; - Sort typeAst = z3.MkArraySort(domain, range); - return typeAst; + return z3.MkArraySort(domain, range); } public Sort BuildBvType(BvType bvType) { Context z3 = ((Z3Context)container).z3; - Sort typeAst = z3.MkBvSort((uint)bvType.Bits); - return typeAst; + return z3.MkBvSort((uint)bvType.Bits); } public Sort BuildBasicType(BasicType basicType) @@ -188,11 +182,9 @@ namespace Microsoft.Boogie.Z3 public Sort BuildCtorType(CtorType ctorType) { Context z3 = ((Z3Context)container).z3; - Sort typeAst; if (ctorType.Arguments.Length > 0) throw new Exception("Type constructor of non-zero arity are not handled"); - typeAst = z3.MkSort(ctorType.Decl.Name); - return typeAst; + return z3.MkSort(ctorType.Decl.Name); } } } \ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index aa47d7e0..bf6dab94 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -17,15 +17,15 @@ namespace Microsoft.Boogie.Z3 { public class Z3apiExprLineariser : IVCExprVisitor { - private Z3apiOpLineariser OpLinObject = null; + private Z3apiOpLineariser opLineariser = null; private IVCExprOpVisitor OpLineariser { get { Contract.Ensures(Contract.Result>() != null); - if (OpLinObject == null) - OpLinObject = new Z3apiOpLineariser(this); - return OpLinObject; + if (opLineariser == null) + opLineariser = new Z3apiOpLineariser(this); + return opLineariser; } } @@ -91,7 +91,7 @@ namespace Microsoft.Boogie.Z3 } } - return cm.Make(opString, asts); + return cm.Make(op, asts); } return node.Accept(OpLineariser, options); @@ -246,7 +246,7 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////// - private Term WriteApplication(string op, IEnumerable terms, LineariserOptions options) + private Term WriteApplication(VCExprOp op, IEnumerable terms, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(op != null); @@ -267,76 +267,49 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("NOT", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitEqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("EQ", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitNeqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("NEQ", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitAndOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("AND", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitOrOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("OR", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - if (options.InverseImplies) - { - List args = new List(); - - args.Add(ExprLineariser.Linearise(node[1], options)); - List t = new List(); - t.Add(ExprLineariser.Linearise(node[0], options)); - args.Add(ExprLineariser.cm.Make("NOT", t)); - return ExprLineariser.cm.Make("OR", args); - } - else - { - return WriteApplication("IMPLIES", node, options); - } + return WriteApplication(node.Op, node, options); } - public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) + public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) { - Contract.Requires(options != null); - Contract.Requires(node != null); - - if (node.Length < 2) - { - return ExprLineariser.Linearise(VCExpressionGenerator.True, options); - } - else - { - List args = new List(); - foreach (VCExpr e in node) - { - Contract.Assert(e != null); - args.Add(ExprLineariser.Linearise(e, options)); - } - return ExprLineariser.cm.Make("DISTINCT", args); - } + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); } public Term VisitLabelOp(VCExprNAry node, LineariserOptions options) @@ -358,10 +331,24 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } + System.Diagnostics.Debug.Assert(args.Count >= 2); - Term[] unwrapChildren = args.ToArray(); - return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]); - // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args); + Term selectTerm = args[0]; + for (int i = 1; i < args.Count; i++) { + selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]); + } + return selectTerm; + } + + private Term ConstructStoreTerm(Term mapTerm, List args, int index) { + System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1); + if (index == args.Count - 2) { + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]); + } + else { + Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1); + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t); + } } public Term VisitStoreOp(VCExprNAry node, LineariserOptions options) @@ -374,10 +361,7 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - - Term[] unwrapChildren = args.ToArray(); - return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); - // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args); + return ConstructStoreTerm(args[0], args, 1); } public Term VisitBvOp(VCExprNAry node, LineariserOptions options) @@ -431,129 +415,97 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - - List args = new List(); - args.Add(ExprLineariser.Linearise(node[0], options)); - args.Add(ExprLineariser.Linearise(node[1], options)); - args.Add(ExprLineariser.Linearise(node[2], options)); - return ExprLineariser.cm.Make("ITE", args); + return WriteApplication(node.Op, node, options); } public Term VisitCustomOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(node != null); Contract.Requires(options != null); - VCExprCustomOp op = (VCExprCustomOp)node.Op; - List args = new List(); - foreach (VCExpr arg in node) - { - args.Add(ExprLineariser.Linearise(arg, options)); - } - return ExprLineariser.cm.Make(op.Name, args); + return WriteApplication(node.Op, node, options); } - public Term VisitAddOp(VCExprNAry node, LineariserOptions options) - { - Contract.Requires(options != null); - Contract.Requires(node != null); - if (CommandLineOptions.Clo.ReflectAdd) - { - return WriteApplication("Reflect$Add", node, options); - } - else - { - return WriteApplication("+", node, options); - } + public Term VisitAddOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); } public Term VisitSubOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("-", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitMulOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("*", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitDivOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("/", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitModOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("%", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitLtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitLeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<=", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitGtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitGeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">=", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<:", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<::", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op; - Contract.Assert(op != null); - string funcName = op.Func.Name; - Contract.Assert(funcName != null); - string bvzName = op.Func.FindStringAttribute("external"); - if (bvzName != null) funcName = bvzName; - - List args = new List(); - foreach (VCExpr e in node) - { - Contract.Assert(e != null); - args.Add(ExprLineariser.Linearise(e, options)); - } - return ExprLineariser.cm.Make(funcName, args); + return WriteApplication(node.Op, node, options); } } } diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index e02243ce..94184957 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -146,6 +146,14 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} + Model + + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} VCExpr diff --git a/Test/z3api/Answer b/Test/z3api/Answer index 782aa852..d18f12ef 100644 --- a/Test/z3api/Answer +++ b/Test/z3api/Answer @@ -1,9 +1,9 @@ -------------------- boog0.bpl -------------------- -boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement. -boog0.bpl(45,3): Related location: This is the postcondition that might not hold. +boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path. +boog0.bpl(43,3): Related location: This is the postcondition that might not hold. Execution trace: - boog0.bpl(48,7): anon0 + boog0.bpl(46,7): anon0 Boogie program verifier finished with 1 verified, 1 error @@ -12,17 +12,17 @@ Boogie program verifier finished with 1 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- boog2.bpl -------------------- -boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement. -boog2.bpl(19,3): Related location: This is the postcondition that might not hold. +boog2.bpl(24,1): Error BP5003: A postcondition might not hold on this return path. +boog2.bpl(20,3): Related location: This is the postcondition that might not hold. Execution trace: - boog2.bpl(22,8): anon0 + boog2.bpl(23,8): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- boog3.bpl -------------------- -boog3.bpl(6,3): Error BP5001: This assertion might not hold. +boog3.bpl(7,3): Error BP5001: This assertion might not hold. Execution trace: - boog3.bpl(6,3): anon0 + boog3.bpl(7,3): anon0 Boogie program verifier finished with 0 verified, 1 error @@ -31,11 +31,11 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- boog5.bpl -------------------- -boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement. -boog5.bpl(29,3): Related location: This is the postcondition that might not hold. +boog5.bpl(37,3): Error BP5003: A postcondition might not hold on this return path. +boog5.bpl(30,3): Related location: This is the postcondition that might not hold. Execution trace: - boog5.bpl(32,3): anon0 - boog5.bpl(35,13): anon3_Else + boog5.bpl(33,3): anon0 + boog5.bpl(36,13): anon3_Else Boogie program verifier finished with 0 verified, 1 error @@ -44,91 +44,92 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- boog7.bpl -------------------- -boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement. -boog7.bpl(13,3): Related location: This is the postcondition that might not hold. +boog7.bpl(18,1): Error BP5003: A postcondition might not hold on this return path. +boog7.bpl(14,3): Related location: This is the postcondition that might not hold. Execution trace: - boog7.bpl(16,11): anon0 + boog7.bpl(17,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog8.bpl -------------------- -boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag -boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag -2 type checking errors detected in boog8.bpl +boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path. +boog8.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + boog8.bpl(22,11): anon0 + +Boogie program verifier finished with 0 verified, 1 error -------------------- boog9.bpl -------------------- -boog9.bpl(19,1): Error BP5003: A postcondition might not hold at this return statement. -boog9.bpl(15,3): Related location: This is the postcondition that might not hold. +boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path. +boog9.bpl(16,3): Related location: This is the postcondition that might not hold. Execution trace: - boog9.bpl(18,11): anon0 + boog9.bpl(19,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog10.bpl -------------------- -boog10.bpl(18,3): Error BP5001: This assertion might not hold. +boog10.bpl(19,3): Error BP5001: This assertion might not hold. Execution trace: - boog10.bpl(18,3): anon0 + boog10.bpl(19,3): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog11.bpl -------------------- -boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement. -boog11.bpl(10,3): Related location: This is the postcondition that might not hold. +boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path. +boog11.bpl(11,3): Related location: This is the postcondition that might not hold. Execution trace: - boog11.bpl(13,8): anon0 + boog11.bpl(14,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog12.bpl -------------------- -boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement. -boog12.bpl(13,3): Related location: This is the postcondition that might not hold. +boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path. +boog12.bpl(14,3): Related location: This is the postcondition that might not hold. Execution trace: - boog12.bpl(16,16): anon0 + boog12.bpl(17,16): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog13.bpl -------------------- -boog13.bpl(9,11): Error: more than one declaration of variable name: v +boog13.bpl(10,18): Error: more than one declaration of variable name: v 1 name resolution errors detected in boog13.bpl -------------------- boog14.bpl -------------------- -boog14.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement. -boog14.bpl(8,1): Related location: This is the postcondition that might not hold. +boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +boog14.bpl(9,1): Related location: This is the postcondition that might not hold. Execution trace: - boog14.bpl(10,8): anon0 + boog14.bpl(11,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog15.bpl -------------------- -boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement. -boog15.bpl(7,1): Related location: This is the postcondition that might not hold. +boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path. +boog15.bpl(8,1): Related location: This is the postcondition that might not hold. Execution trace: - boog15.bpl(9,8): anon0 + boog15.bpl(10,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog16.bpl -------------------- -boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement. -boog16.bpl(8,1): Related location: This is the postcondition that might not hold. +boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +boog16.bpl(9,1): Related location: This is the postcondition that might not hold. Execution trace: - boog16.bpl(10,8): anon0 + boog16.bpl(11,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog17.bpl -------------------- -boog17.bpl(24,3): Error BP5001: This assertion might not hold. +boog17.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - boog17.bpl(15,1): start - boog17.bpl(19,1): label_3 - boog17.bpl(22,1): label_4 + boog17.bpl(17,1): start Boogie program verifier finished with 0 verified, 1 error -------------------- boog18.bpl -------------------- -boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement. -boog18.bpl(12,1): Related location: This is the postcondition that might not hold. +boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path. +boog18.bpl(13,1): Related location: This is the postcondition that might not hold. Execution trace: - boog18.bpl(14,4): anon0 + boog18.bpl(15,4): anon0 Boogie program verifier finished with 0 verified, 1 error @@ -137,9 +138,9 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- boog20.bpl -------------------- -boog20.bpl(15,1): Error BP5001: This assertion might not hold. +boog20.bpl(16,1): Error BP5001: This assertion might not hold. Execution trace: - boog20.bpl(15,1): anon0 + boog20.bpl(16,1): anon0 Boogie program verifier finished with 0 verified, 1 error @@ -148,7 +149,7 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- boog22.bpl -------------------- -boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1 +boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1 1 name resolution errors detected in boog22.bpl -------------------- boog23.bpl -------------------- @@ -176,12 +177,83 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors -------------------- boog31.bpl -------------------- -boog31.bpl(12,1): Error BP5001: This assertion might not hold. +boog31.bpl(13,1): Error BP5001: This assertion might not hold. Execution trace: - boog31.bpl(12,1): anon0 + boog31.bpl(13,1): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog34.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors + +-------------------- boog35.bpl -------------------- +boog35.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + boog35.bpl(14,11): anon0 + +Boogie program verifier finished with 1 verified, 1 error + +-------------------- bar1.bpl -------------------- +bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path. +bar1.bpl(21,1): Related location: This is the postcondition that might not hold. +Execution trace: + bar1.bpl(24,3): anon0 + Inlined call to procedure foo begins + bar1.bpl(13,5): anon0 + Inlined call to procedure bar begins + bar1.bpl(7,5): anon0 + Inlined call to procedure bar ends + Inlined call to procedure bar begins + bar1.bpl(7,5): anon0 + Inlined call to procedure bar ends + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- bar2.bpl -------------------- +bar2.bpl(21,3): Error BP5001: This assertion might not hold. +Execution trace: + bar2.bpl(19,3): anon0 + Inlined call to procedure foo begins + bar2.bpl(5,3): anon0 + bar2.bpl(9,7): anon3_Else + Inlined call to procedure foo ends + Inlined call to procedure foo begins + bar2.bpl(5,3): anon0 + bar2.bpl(6,7): anon3_Then + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- bar3.bpl -------------------- +bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path. +bar3.bpl(34,1): Related location: This is the postcondition that might not hold. +Execution trace: + bar3.bpl(38,3): anon0 + Inlined call to procedure foo begins + bar3.bpl(18,3): anon0 + bar3.bpl(24,7): anon3_Else + Inlined call to procedure bar begins + bar3.bpl(7,3): anon0 + bar3.bpl(10,7): anon3_Else + Inlined call to procedure bar ends + Inlined call to procedure bar begins + bar3.bpl(7,3): anon0 + bar3.bpl(10,7): anon3_Else + Inlined call to procedure bar ends + Inlined call to procedure foo ends + Inlined call to procedure bar begins + bar3.bpl(7,3): anon0 + bar3.bpl(10,7): anon3_Else + Inlined call to procedure bar ends + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- bar4.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- bar6.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index e9bc968e..6645667e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,15 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe -for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do ( +for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl boog35.bpl) do ( echo. echo -------------------- %%f -------------------- %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f ) -REM boog12.bpl -REM boog15.bpl - -REM boog19.bpl -REM boog23.bpl -REM boog25.bpl \ No newline at end of file +for %%f in (bar1.bpl bar2.bpl bar3.bpl bar4.bpl bar6.bpl) do ( + echo. + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /stratifiedInline:1 /prover:z3api %%f +) \ No newline at end of file -- cgit v1.2.3 From 6590c272066ee1c0aa45d735083847dc9c3e5d5f Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 24 Jun 2011 06:54:06 -0700 Subject: extra test files --- Test/z3api/bar1.bpl | 26 ++++++++++++++++++++++++++ Test/z3api/bar2.bpl | 24 ++++++++++++++++++++++++ Test/z3api/bar3.bpl | 41 +++++++++++++++++++++++++++++++++++++++++ Test/z3api/bar4.bpl | 38 ++++++++++++++++++++++++++++++++++++++ Test/z3api/bar6.bpl | 36 ++++++++++++++++++++++++++++++++++++ Test/z3api/boog35.bpl | 17 +++++++++++++++++ 6 files changed, 182 insertions(+) create mode 100644 Test/z3api/bar1.bpl create mode 100644 Test/z3api/bar2.bpl create mode 100644 Test/z3api/bar3.bpl create mode 100644 Test/z3api/bar4.bpl create mode 100644 Test/z3api/bar6.bpl create mode 100644 Test/z3api/boog35.bpl (limited to 'Test') diff --git a/Test/z3api/bar1.bpl b/Test/z3api/bar1.bpl new file mode 100644 index 00000000..845954d5 --- /dev/null +++ b/Test/z3api/bar1.bpl @@ -0,0 +1,26 @@ +var x: int; +var y: int; + +procedure {:inline 1} bar() +modifies y; +{ + y := y + 1; +} + +procedure {:inline 1} foo() +modifies x, y; +{ + x := x + 1; + call bar(); + call bar(); + x := x + 1; +} + +procedure main() +requires x == y; +ensures x != y; +modifies x, y; +{ + call foo(); +} + diff --git a/Test/z3api/bar2.bpl b/Test/z3api/bar2.bpl new file mode 100644 index 00000000..76991a8f --- /dev/null +++ b/Test/z3api/bar2.bpl @@ -0,0 +1,24 @@ + +procedure {:inline 1} foo() returns (x: bool) +{ + var b: bool; + if (b) { + x := false; + return; + } else { + x := true; + return; + } +} + +procedure main() +{ + var b1: bool; + var b2: bool; + + call b1 := foo(); + call b2 := foo(); + assert b1 == b2; +} + + diff --git a/Test/z3api/bar3.bpl b/Test/z3api/bar3.bpl new file mode 100644 index 00000000..7bd91184 --- /dev/null +++ b/Test/z3api/bar3.bpl @@ -0,0 +1,41 @@ +var y: int; +var x: int; + +procedure {:inline 1} bar(b: bool) +modifies y; +{ + if (b) { + y := y + 1; + } else { + y := y - 1; + } +} + +procedure {:inline 1} foo() +modifies x, y; +{ + var b: bool; + if (b) { + x := x + 1; + call bar(true); + call bar(true); + x := x + 1; + } else { + x := x - 1; + call bar(false); + call bar(false); + x := x - 1; + } +} + + +procedure main() +requires x == y; +ensures x == y; +modifies x, y; +modifies y; +{ + call foo(); + assert x == y; + call bar(false); +} diff --git a/Test/z3api/bar4.bpl b/Test/z3api/bar4.bpl new file mode 100644 index 00000000..84640811 --- /dev/null +++ b/Test/z3api/bar4.bpl @@ -0,0 +1,38 @@ +var y: int; +var x: int; + +procedure {:inline 1} bar() returns (b: bool) +modifies y; +{ + if (b) { + y := y + 1; + } else { + y := y - 1; + } +} + +procedure {:inline 1} foo() +modifies x, y; +{ + var b: bool; + + call b := bar(); + if (b) { + x := x + 1; + } else { + x := x - 1; + } +} + + +procedure main() returns (b: bool) +requires x == y; +ensures !b ==> x == y+1; +ensures b ==> x+1 == y; +modifies x, y; +modifies y; +{ + call foo(); + assert x == y; + call b := bar(); +} diff --git a/Test/z3api/bar6.bpl b/Test/z3api/bar6.bpl new file mode 100644 index 00000000..e133aef7 --- /dev/null +++ b/Test/z3api/bar6.bpl @@ -0,0 +1,36 @@ +var M: [int]int; + +procedure {:inline 1} bar(y: int) returns (b: bool) +modifies M; +{ + if (b) { + M[y] := M[y] + 1; + } else { + M[y] := M[y] - 1; + } +} + +procedure {:inline 1} foo(x: int, y: int) +modifies M; +{ + var b: bool; + + call b := bar(y); + if (b) { + M[x] := M[x] + 1; + } else { + M[x] := M[x] - 1; + } +} + +procedure main(x: int, y: int) returns (b: bool) +requires x != y; +requires M[x] == M[y]; +ensures !b ==> M[x] == M[y]+1; +ensures b ==> M[x]+1 == M[y]; +modifies M; +{ + call foo(x, y); + assert M[x] == M[y]; + call b := bar(y); +} diff --git a/Test/z3api/boog35.bpl b/Test/z3api/boog35.bpl new file mode 100644 index 00000000..beae0c74 --- /dev/null +++ b/Test/z3api/boog35.bpl @@ -0,0 +1,17 @@ +procedure foo1(x: int, y: int) +{ + var a: [int][int]int; + + a[x][y] := 42; + + assert a[x][y] == 42; +} + +procedure foo2(x: int, y: int) +{ + var a: [int][int]int; + + a[x][y] := 42; + + assert a[x][y] == 43; +} \ No newline at end of file -- cgit v1.2.3 From e2c44fac506e82fde3342193138c1e99f3af5136 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 28 Jun 2011 15:18:05 -0700 Subject: Changed regression test answer for dafny0 to reflect new error messages. --- Test/dafny0/Answer | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 29b8e708..2abd64b2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -147,16 +147,16 @@ Execution trace: SmallTests.dfy(81,5): anon9_LoopHead (0,0): anon9_LoopBody (0,0): anon10_Then -SmallTests.dfy(116,5): Error: call may violate caller's modifies clause +SmallTests.dfy(116,5): Error: call may violate context's modifies clause Execution trace: (0,0): anon0 (0,0): anon4_Else (0,0): anon3 -SmallTests.dfy(129,9): Error: call may violate caller's modifies clause +SmallTests.dfy(129,9): Error: call may violate context's modifies clause Execution trace: (0,0): anon0 (0,0): anon3_Then -SmallTests.dfy(131,9): Error: call may violate caller's modifies clause +SmallTests.dfy(131,9): Error: call may violate context's modifies clause Execution trace: (0,0): anon0 (0,0): anon3_Else @@ -453,7 +453,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator 9 parse errors detected in ParseErrors.dfy -------------------- Array.dfy -------------------- -Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 (0,0): anon5_Then @@ -468,13 +468,13 @@ Execution trace: Array.dfy(48,20): Error: assertion violation Execution trace: (0,0): anon0 -Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(56,8): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon2 (0,0): anon6_Then -Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 (0,0): anon5_Then @@ -493,10 +493,10 @@ Execution trace: (0,0): anon7_Else (0,0): anon8_Then (0,0): anon9_Then -Array.dfy(131,6): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 -Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 @@ -632,7 +632,7 @@ Basics.dfy(147,10): Error: target object may be null Execution trace: (0,0): anon0 (0,0): anon3 -Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause +Basics.dfy(147,10): Error: assignment may update an object not in the enclosing context's modifies clause Execution trace: (0,0): anon0 (0,0): anon3 -- cgit v1.2.3 From c20df3142c40f76d843ce4e512293c8eca6a75e8 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 28 Jun 2011 16:09:34 -0700 Subject: Added regression test for loop modifies clauses. --- Test/dafny0/Answer | 85 +++++++++++++++++++++++++++++++++++++++++++++++++ Test/dafny0/runtest.bat | 2 +- 2 files changed, 86 insertions(+), 1 deletion(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 2abd64b2..da82fd59 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1000,3 +1000,88 @@ RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M RefinementErrors.dfy(34,10): Error: Different number of output variables 6 resolution/type errors detected in RefinementErrors.dfy + +-------------------- LoopModifies.dfy -------------------- +LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 +LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(14,4): anon9_LoopHead + (0,0): anon9_LoopBody + LoopModifies.dfy(14,4): anon10_Else + (0,0): anon5 + LoopModifies.dfy(14,4): anon12_Else + (0,0): anon7 +LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(42,4): anon9_LoopHead + (0,0): anon9_LoopBody + LoopModifies.dfy(42,4): anon10_Else + (0,0): anon5 + LoopModifies.dfy(42,4): anon12_Else + (0,0): anon7 +LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(57,4): anon9_LoopHead + (0,0): anon9_LoopBody + LoopModifies.dfy(57,4): anon10_Else + (0,0): anon5 + LoopModifies.dfy(57,4): anon12_Else + (0,0): anon7 +LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause +Execution trace: + (0,0): anon0 +LoopModifies.dfy(98,5): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(90,4): anon9_LoopHead + (0,0): anon9_LoopBody + LoopModifies.dfy(90,4): anon10_Else + (0,0): anon5 + LoopModifies.dfy(90,4): anon12_Else + (0,0): anon7 +LoopModifies.dfy(146,5): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(134,4): anon17_LoopHead + (0,0): anon17_LoopBody + LoopModifies.dfy(134,4): anon18_Else + (0,0): anon5 + LoopModifies.dfy(134,4): anon20_Else + (0,0): anon7 + LoopModifies.dfy(139,7): anon21_LoopHead + (0,0): anon21_LoopBody + LoopModifies.dfy(139,7): anon22_Else + (0,0): anon12 + LoopModifies.dfy(139,7): anon24_Else + (0,0): anon14 +LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(193,4): anon9_LoopHead + (0,0): anon9_LoopBody + LoopModifies.dfy(193,4): anon10_Else + (0,0): anon5 + LoopModifies.dfy(193,4): anon12_Else + (0,0): anon7 +LoopModifies.dfy(260,10): Error: assignment may update an array element not in the enclosing context's modifies clause +Execution trace: + (0,0): anon0 + LoopModifies.dfy(248,4): anon17_LoopHead + (0,0): anon17_LoopBody + LoopModifies.dfy(248,4): anon18_Else + (0,0): anon5 + LoopModifies.dfy(248,4): anon20_Else + (0,0): anon7 + LoopModifies.dfy(256,7): anon21_LoopHead + (0,0): anon21_LoopBody + LoopModifies.dfy(256,7): anon22_Else + (0,0): anon12 + LoopModifies.dfy(256,7): anon24_Else + (0,0): anon14 + +Dafny program verifier finished with 21 verified, 9 errors diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index aed9ee8a..3c64f623 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy Termination.dfy DTypes.dfy TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy - Refinement.dfy RefinementErrors.dfy) do ( + Refinement.dfy RefinementErrors.dfy LoopModifies.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 %* %%f -- cgit v1.2.3 From 5a0db96c13bea139372e1c5ad118065678821f2c Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Wed, 29 Jun 2011 11:00:53 -0700 Subject: Added regression test file LoopModifies.dfy. --- Test/dafny0/LoopModifies.dfy | 293 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 293 insertions(+) create mode 100644 Test/dafny0/LoopModifies.dfy (limited to 'Test') diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy new file mode 100644 index 00000000..17a4228e --- /dev/null +++ b/Test/dafny0/LoopModifies.dfy @@ -0,0 +1,293 @@ + +// regular modifies sanity test: +method Testing1(a: array) + requires a != null && a.Length > 0; +{ + a[0] := 0; +} + +// array inside while loop, without explict modifies clause: +method Testing2(a: array) + requires a != null && a.Length > 0; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + { + a[0] := i; + i := i + 1; + } +} + +// array inside while loop, without explict modifies clause: +method Testing2A(a: array) + requires a != null && a.Length > 0; + modifies a; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + { + // now there is no problem. + a[0] := i; + i := i + 1; + } +} + +// array inside while loop, with explict modifies clause: +method Testing3(a: array) + requires a != null && a.Length > 0; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + modifies; + { + a[0] := i; + i := i + 1; + } +} + +// modifies restricts: +method Testing4(a: array) + requires a != null && a.Length > 0; + modifies a; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + modifies; + { + a[0] := i; + i := i + 1; + } + // should be ok. + a[0] := 1; +} + +// modifies not a subset: +method Testing5(a: array) + requires a != null && a.Length > 0; + modifies; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + modifies a; + { + a[0] := i; + i := i + 1; + } +} + +// modifies is a subset, but modifications occur outside: +method Testing6(a: array, b: array) + requires a != null && a.Length > 0; + requires b != null && b.Length > 0; + modifies a, b; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + modifies a; + { + // cool. + a[0] := i; + + // not cool. + b[0] := i; + i := i + 1; + } +} + +// heap outside modifies is actually preserved: +method Testing7(a: array, b: array) + requires a != null && a.Length > 0; + requires b != null && b.Length > 0; + requires a != b; + modifies a, b; +{ + var i := 0; + b[0] := 4; + while(i < 10) + invariant 0 <= i <= 10; + modifies a; + { + // still good. + a[0] := i; + i := i + 1; + } + // this is new, and good: + assert b[0] == 4; +} + +// modifies actually restrict frame when nested: +method Testing8(a: array, b: array, c: array) + requires a != null && a.Length > 0; + requires b != null && b.Length > 0; + requires c != null && c.Length > 0; + requires a != b && b != c && c != a; + modifies a, b, c; +{ + var i := 0; + b[0] := 4; + while(i < 10) + invariant 0 <= i <= 10; + modifies a, b; + { + var j := 0; + while(j < 10) + invariant 0 <= j <= 10; + modifies a; + { + // happy: + a[0] := j; + // not happy: + b[0] := i; + j := j + 1; + } + i := i + 1; + } + c[0] := 1; +} + +// heap outside modifies preserved when nested: +method Testing9(a: array, b: array, c: array) + requires a != null && a.Length > 0; + requires b != null && b.Length > 0; + requires c != null && c.Length > 0; + requires a != b && b != c && c != a; + modifies a, b, c; +{ + var i := 0; + b[0] := 4; + while(i < 10) + invariant 0 <= i <= 10; + modifies a, b; + { + var j := 0; + b[0] := i; + while(j < 10) + invariant 0 <= j <= 10; + modifies a; + { + a[0] := j; + j := j + 1; + } + assert b[0] == i; + i := i + 1; + } + c[0] := 1; +} + +// allocation, fresh tests: + +// allocated things not automatically in modifies of loops: +method Testing10(a: array) + requires a != null && a.Length > 0; + modifies a; +{ + var i := 0; + var arr := new int[1]; + arr[0] := 1; // good, even though not in method modifies. + while(i < 10) + invariant 0 <= i <= 10; + modifies a; + { + arr[0] := 1; // bad. + i := i + 1; + } +} + +// unless no modifies given, in which case the context is used: +method Testing10a(a: array) + requires a != null && a.Length > 0; + modifies a; +{ + var i := 0; + var arr := new int[1]; + arr[0] := 1; // still good. + while(i < 10) + invariant 0 <= i <= 10; + { + arr[0] := 1; // no modifies, so allowed to touch arr. + i := i + 1; + } +} + +// arr still accessible after loop that can't touch it. +method Testing11() +{ + var i := 0; + var arr := new int[1]; + while(i < 10) + invariant 0 <= i <= 10; + modifies; + { + arr := new int[1]; + arr[0] := 1; + var j := 0; + while(j < 10) + invariant 0 <= j <= 10; + modifies; + { + // can't touch arr in here. + j := j + 1; + } + arr[0] := 2; + i := i + 1; + } +} + +// allocation inside a loop is still ok: +method Testing11a(a: array) + requires a != null && a.Length > 0; + modifies a; +{ + var i := 0; + while(i < 10) + invariant 0 <= i <= 10; + modifies a; + { + var arr := new int[1]; + arr[0] := 1; // can modify arr, even though it + // is not in modifies because it is fresh. + var j := 0; + while(j < 10) + invariant 0 <= j <= 10; + modifies a; + { + arr[0] := 3; // can't touch arr, as allocated before modifies captured. + j := j + 1; + } + i := i + 1; + } +} + +class Elem +{ + var i: int; +} + +// capture of modifies clause at beginning of loop: +method Testing12(a: Elem, b: Elem, c: Elem) + requires a != null && b != null && c != null; + requires a != b && b != c && c != a; // all different. + modifies a, b, c; +{ + var i := 0; + var S := {a, b, c}; + // S "captured" here for purposes of modifies clause. + while(S != {}) + modifies S; + decreases S; + { + var j := choose S; + // these still good, even though S shrinks to not include them. + a.i := i; + b.i := i; + c.i := i; + S := S - {j}; + i := i + 1; + } +} \ No newline at end of file -- cgit v1.2.3