From 5dcda744e4ace3b8f627fe98ac837ec10624272d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 16 May 2011 18:20:08 -0700 Subject: Dafny: To help verifications involving sequences of (boxed) booleans along, added function $IsCanonicalBoolBox --- Binaries/DafnyPrelude.bpl | 79 ++++++++++++++++++++++++---------------------- Source/Dafny/Translator.cs | 23 +++++++++++++- 2 files changed, 63 insertions(+), 39 deletions(-) diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 646b16f1..a358e3c0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -20,14 +20,14 @@ const null: ref; type Set T = [T]bool; -function Set#Empty() returns (Set T); +function Set#Empty(): Set T; axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]); -function Set#Singleton(T) returns (Set T); +function Set#Singleton(T): Set T; axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]); axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); -function Set#UnionOne(Set T, T) returns (Set T); +function Set#UnionOne(Set T, T): Set T; axiom (forall a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] } Set#UnionOne(a,x)[o] <==> o == x || a[o]); axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } @@ -35,7 +35,7 @@ axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } a[y] ==> Set#UnionOne(a, x)[y]); -function Set#Union(Set T, Set T) returns (Set T); +function Set#Union(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] } Set#Union(a,b)[o] <==> a[o] || b[o]); axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] } @@ -47,7 +47,7 @@ axiom (forall a, b: Set T :: { Set#Union(a, b) } Set#Difference(Set#Union(a, b), a) == b && Set#Difference(Set#Union(a, b), b) == a); -function Set#Intersection(Set T, Set T) returns (Set T); +function Set#Intersection(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } Set#Intersection(a,b)[o] <==> a[o] && b[o]); @@ -60,27 +60,27 @@ axiom (forall a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) } axiom (forall a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) } Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b)); -function Set#Difference(Set T, Set T) returns (Set T); +function Set#Difference(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] } Set#Difference(a,b)[o] <==> a[o] && !b[o]); axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] } b[y] ==> !Set#Difference(a, b)[y] ); -function Set#Subset(Set T, Set T) returns (bool); +function Set#Subset(Set T, Set T): bool; axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) } Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); -function Set#Equal(Set T, Set T) returns (bool); +function Set#Equal(Set T, Set T): bool; axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets Set#Equal(a,b) ==> a == b); -function Set#Disjoint(Set T, Set T) returns (bool); +function Set#Disjoint(Set T, Set T): bool; axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); -function Set#Choose(Set T, TickType) returns (T); +function Set#Choose(Set T, TickType): T; axiom (forall a: Set T, tick: TickType :: { Set#Choose(a, tick) } a != Set#Empty() ==> a[Set#Choose(a, tick)]); @@ -90,25 +90,25 @@ axiom (forall a: Set T, tick: TickType :: { Set#Choose(a, tick) } type Seq T; -function Seq#Length(Seq T) returns (int); +function Seq#Length(Seq T): int; axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); -function Seq#Empty() returns (Seq T); +function Seq#Empty(): Seq T; axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); axiom (forall s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty()); -function Seq#Singleton(T) returns (Seq T); +function Seq#Singleton(T): Seq T; axiom (forall t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1); -function Seq#Build(s: Seq T, index: int, val: T, newLength: int) returns (Seq T); +function Seq#Build(s: Seq T, index: int, val: T, newLength: int): Seq T; axiom (forall s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) } 0 <= len ==> Seq#Length(Seq#Build(s,i,v,len)) == len); -function Seq#Append(Seq T, Seq T) returns (Seq T); +function Seq#Append(Seq T, Seq T): Seq T; axiom (forall s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) } Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1)); -function Seq#Index(Seq T, int) returns (T); +function Seq#Index(Seq T, int): T; axiom (forall t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t); axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) && @@ -118,7 +118,7 @@ axiom (forall s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Bui (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) && (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n))); -function Seq#Update(Seq T, int, T) returns (Seq T); +function Seq#Update(Seq T, int, T): Seq T; axiom (forall s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s)); axiom (forall s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) } @@ -126,7 +126,7 @@ axiom (forall s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v) (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) && (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n))); -function Seq#Contains(Seq T, T) returns (bool); +function Seq#Contains(Seq T, T): bool; axiom (forall s: Seq T, x: T :: { Seq#Contains(s,x) } Seq#Contains(s,x) <==> (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x)); @@ -153,22 +153,22 @@ axiom (forall s: Seq T, n: int, x: T :: (exists i: int :: { Seq#Index(s, i) } 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); -function Seq#Equal(Seq T, Seq T) returns (bool); +function Seq#Equal(Seq T, Seq T): bool; axiom (forall s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) } Seq#Equal(s0,s1) <==> Seq#Length(s0) == Seq#Length(s1) && (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j))); -axiom(forall a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences +axiom (forall a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences Seq#Equal(a,b) ==> a == b); -function Seq#SameUntil(Seq T, Seq T, int) returns (bool); +function Seq#SameUntil(Seq T, Seq T, int): bool; axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) } Seq#SameUntil(s0,s1,n) <==> (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j))); -function Seq#Take(s: Seq T, howMany: int) returns (Seq T); +function Seq#Take(s: Seq T, howMany: int): Seq T; axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) && @@ -177,7 +177,7 @@ axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:w 0 <= j && j < n && j < Seq#Length(s) ==> Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j)); -function Seq#Drop(s: Seq T, howMany: int) returns (Seq T); +function Seq#Drop(s: Seq T, howMany: int): Seq T; axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) && @@ -197,8 +197,8 @@ axiom (forall s, t: Seq T :: type BoxType; -function $Box(T) returns (BoxType); -function $Unbox(BoxType) returns (T); +function $Box(T): BoxType; +function $Unbox(BoxType): T; axiom (forall x: T :: { $Box(x) } $Unbox($Box(x)) == x); axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b); @@ -206,7 +206,10 @@ axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b); axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b); axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b); axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b); -// note: an axiom like this for bool would not be sound +// Note: an axiom like this for bool would not be sound; instead, we do: +function $IsCanonicalBoolBox(BoxType): bool; +axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true)); +axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b); // --------------------------------------------------------------- // -- Encoding of type names ------------------------------------- @@ -218,12 +221,12 @@ const unique class.bool: ClassName; const unique class.set: ClassName; const unique class.seq: ClassName; -function /*{:never_pattern true}*/ dtype(ref) returns (ClassName); -function /*{:never_pattern true}*/ TypeParams(ref, int) returns (ClassName); +function /*{:never_pattern true}*/ dtype(ref): ClassName; +function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName; -function TypeTuple(a: ClassName, b: ClassName) returns (ClassName); -function TypeTupleCar(ClassName) returns (ClassName); -function TypeTupleCdr(ClassName) returns (ClassName); +function TypeTuple(a: ClassName, b: ClassName): ClassName; +function TypeTupleCar(ClassName): ClassName; +function TypeTupleCdr(ClassName): ClassName; // TypeTuple is injective in both arguments: axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } TypeTupleCar(TypeTuple(a,b)) == a && @@ -235,13 +238,13 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type DatatypeType; -function /*{:never_pattern true}*/ DtType(DatatypeType) returns (ClassName); // the analog of dtype for datatype values -function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int) returns (ClassName); // the analog of TypeParams +function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName; // the analog of dtype for datatype values +function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams type DtCtorId; -function DatatypeCtorId(DatatypeType) returns (DtCtorId); +function DatatypeCtorId(DatatypeType): DtCtorId; -function DtRank(DatatypeType) returns (int); +function DtRank(DatatypeType): int; // --------------------------------------------------------------- // -- Axiom contexts --------------------------------------------- @@ -274,7 +277,7 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } MultiIndexField_Inverse1(MultiIndexField(f,i)) == i); -function DeclType(Field T) returns (ClassName); +function DeclType(Field T): ClassName; // --------------------------------------------------------------- // -- Allocatedness ---------------------------------------------- @@ -339,10 +342,10 @@ type HeapType = [ref,Field alpha]alpha; function {:inline true} read(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] } function {:inline true} update(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] } -function $IsGoodHeap(HeapType) returns (bool); +function $IsGoodHeap(HeapType): bool; var $Heap: HeapType where $IsGoodHeap($Heap); -function $HeapSucc(HeapType, HeapType) returns (bool); +function $HeapSucc(HeapType, HeapType): bool; axiom (forall h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) } $HeapSucc(h, update(h, r, f, x))); axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 253a1f9b..67559aee 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3676,11 +3676,15 @@ namespace Microsoft.Dafny { Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i); Bpl.Expr unbox = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI); + Bpl.Expr c = GetBoolBoxCondition(xSubI, st.Arg); Bpl.Expr wh = GetWhereClause(tok, unbox, st.Arg, etran); if (wh != null) { + c = BplAnd(c, wh); + } + if (c != Bpl.Expr.True) { Bpl.Expr range = InSeqRange(tok, i, x, true, null, false); Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI)); - return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, wh)); + return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, c)); } } else if (type.IsRefType) { @@ -3706,6 +3710,18 @@ namespace Microsoft.Dafny { return null; } + Bpl.Expr GetBoolBoxCondition(Expr box, Type type) { + Contract.Requires(box != null); + Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); + + if (type is BoolType) { + return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box); + } else { + return Bpl.Expr.True; + } + } + void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) { @@ -4826,6 +4842,7 @@ namespace Microsoft.Dafny { Box, Unbox, + IsCanonicalBoolBox, IsGoodHeap, HeapSucc, @@ -4957,6 +4974,10 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation); + case BuiltinFunction.IsCanonicalBoolBox: + Contract.Assert(args.Length == 1); + Contract.Assert(typeInstantiation == null); + return FunctionCall(tok, "$IsCanonicalBoolBox", Bpl.Type.Bool, args); case BuiltinFunction.IsGoodHeap: Contract.Assert(args.Length == 1); -- cgit v1.2.3 From c76d588dd2768de8505d3d08f43f3de0b5f84dae Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 16 May 2011 18:24:57 -0700 Subject: Dafny: Test case for sequence of boxed booleans --- Test/dafny0/Answer | 2 +- Test/dafny0/SmallTests.dfy | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 070aa6be..2463b0e5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -209,7 +209,7 @@ Execution trace: (0,0): anon15 (0,0): anon25_Else -Dafny program verifier finished with 39 verified, 14 errors +Dafny program verifier finished with 41 verified, 14 errors -------------------- Definedness.dfy -------------------- Definedness.dfy(8,7): Error: possible division by zero diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index ef2049a3..a5f02dc6 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -308,3 +308,13 @@ method QuantifierRange2(a: seq, x: T, y: T, N: int) assert x == y; } } + +// ----------------------- tests that involve sequences of boxed booleans -------- + +ghost method M(zeros: seq, Z: bool) + requires 1 <= |zeros| && Z == false; + requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z; +{ + var x := [Z]; + assert zeros[0..1] == [Z]; +} -- cgit v1.2.3 From eb1d4129ff71a4b1d7752fff7ae7b7fc418490e8 Mon Sep 17 00:00:00 2001 From: CodeplexBot Date: Tue, 17 May 2011 07:55:08 +0200 Subject: Boogie build succeeded --- _admin/Boogie/aste/summary.log | 67 ++++++++++++------------------------------ 1 file changed, 19 insertions(+), 48 deletions(-) diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index b837237b..c0185e9c 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,50 +1,23 @@ -# Aste started: 2011-05-14 07:00:16 +# Aste started: 2011-05-17 07:00:09 # Host id: Boogiebox -# [2011-05-14 07:02:49] SpecSharp revision: 5fb7af71cc82 -# [2011-05-14 07:02:49] SscBoogie revision: 5fb7af71cc82 -# [2011-05-14 07:04:08] Boogie revision: 76b4d17abc74 -[2011-05-14 07:06:08] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked +# [2011-05-17 07:02:41] SpecSharp revision: 5fb7af71cc82 +# [2011-05-17 07:02:41] SscBoogie revision: 5fb7af71cc82 +# [2011-05-17 07:03:56] Boogie revision: e6ac2aed917f +[2011-05-17 07:06:14] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode() D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode() D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected - D:\Temp\aste\Boogie\Source\Core\ResolutionContext.cs(173,7): error CC1016: Contract.Assert/Contract.Assume cannot be used in contract section. Use only Requires and Ensures. D:\Temp\aste\Boogie\Source\Core\Absy.cs(682,7): warning CC1036: Detected call to method 'Graphing.Graph`1.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'. D:\Temp\aste\Boogie\Source\Core\Parser.cs(109,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires. D:\Temp\aste\Boogie\Source\Core\Parser.cs(114,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires. D:\Temp\aste\Boogie\Source\Core\Parser.cs(117,65): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires. - C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(215,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite" /level:4 /rewrite "/assemblyMode=standard" /throwonfailure /libpaths:"D:\Temp\aste\Boogie\Source\AIFramework\bin\Checked\;D:\Temp\aste\Boogie\Source\Basetypes\bin\Checked\;D:\Temp\aste\Boogie\Source\CodeContractsExtender\bin\Checked\;D:\Temp\aste\Boogie\Source\Graph\bin\Checked\;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.0\Profile\Client\;D:\Temp\aste\Boogie\Source\ParserHelper\bin\Checked\;D:\Temp\aste\Boogie\Source\AIFramework\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\Basetypes\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\CodeContractsExtender\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\Graph\bin\Checked\CodeContracts;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.0\Profile\Client\CodeContracts;D:\Temp\aste\Boogie\Source\ParserHelper\bin\Checked\CodeContracts;C:\Program Files (x86)\Microsoft\Contracts\Contracts\.NETFramework\v4.0 " "Core.dll"" exited with code 1. - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\TPTP\bin\Checked\Provers.TPTP.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Isabelle\bin\Checked\Provers.Isabelle.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found + D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(111,7): warning CS0162: Unreachable code detected + D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(290,7): warning CS0162: Unreachable code detected + D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(309,7): warning CS0162: Unreachable code detected + D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1662,11): warning CS0162: Unreachable code detected + D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1822,11): warning CS0162: Unreachable code detected + D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(662,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires. warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode() warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode() warning CS0162: Unreachable code detected @@ -52,13 +25,11 @@ warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires. warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires. warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires. - 1 error - 1 error - 2 error - 3 error - 3 error - 4 error - 4 error - 5 error - 8 error - 10 failed + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires. +[2011-05-17 07:54:06] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed +# [2011-05-17 07:55:08] Released nightly of Boogie -- cgit v1.2.3 From a80851ee6dd439c8f5894b80481837ce41d6fb55 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 17 May 2011 12:45:58 -0700 Subject: added spec for GetType --- BCT/BytecodeTranslator/Heap.cs | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index f38e0093..78774876 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -39,7 +39,6 @@ var $Heap: HeapType; var $Alloc: [Ref] bool; procedure {:inline 1} Alloc() returns (x: Ref) - free ensures x != null; modifies $Alloc; { assume $Alloc[x] == false && x != null; @@ -57,6 +56,11 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x ); axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); +procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) +{ + $result := $TypeOf($DynamicType(this)); +} + "; private Sink sink; @@ -83,6 +87,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateFieldVariable(IFieldReference field) { Bpl.Variable v; string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value; + fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname); Bpl.IToken tok = field.Token(); Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType); @@ -101,6 +106,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateEventVariable(IEventDefinition e) { Bpl.Variable v; string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value; + eventName = TranslationHelper.TurnStringIntoValidIdentifier(eventName); Bpl.IToken tok = e.Token(); Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType); @@ -109,7 +115,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); v = new Bpl.GlobalVariable(tok, tident); } else { - Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t); + Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.RefType), t); Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, mt); v = new Bpl.GlobalVariable(tok, tident); } @@ -126,11 +132,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); /// public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType) { if (accessType == AccessType.Struct) - return Bpl.Expr.Select(o, f); + return Unbox(f.tok, unboxType, Bpl.Expr.Select(o, f)); else if (accessType == AccessType.Heap) return Bpl.Expr.Select(f, o); else - return Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f); + return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f)); } /// @@ -140,11 +146,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType) { Debug.Assert(o != null); if (accessType == AccessType.Struct) - return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, value); + return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, Box(f.tok, boxType, value)); else if (accessType == AccessType.Heap) return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)f, o, value); else - return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, value))); + return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value)))); } } @@ -176,7 +182,6 @@ type HeapType = [Ref,Field]Box; var $Alloc: [Ref] bool; procedure {:inline 1} Alloc() returns (x: Ref) - free ensures x != null; modifies $Alloc; { assume $Alloc[x] == false && x != null; @@ -194,6 +199,11 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x ); axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); +procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) +{ + $result := $TypeOf($DynamicType(this)); +} + "; private Sink sink; @@ -241,6 +251,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateEventVariable(IEventDefinition e) { Bpl.Variable v; string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value; + fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname); Bpl.IToken tok = e.Token(); if (e.Adder.ResolvedMethod.IsStatic) { -- cgit v1.2.3