diff options
| -rw-r--r-- | Source/Core/Absy.cs | 20 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 8 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 18 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 68 | ||||
| -rw-r--r-- | Source/Core/AlphaEquality.cs | 162 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 1 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 85 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 15 | ||||
| -rw-r--r-- | Test/test2/LambdaExt.bpl | 146 | ||||
| -rw-r--r-- | Test/test2/LambdaExt.bpl.expect | 56 |
12 files changed, 527 insertions, 62 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d961eb3e..5ed619d6 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1865,14 +1865,14 @@ namespace Microsoft.Boogie { }
}
- public byte[] MD5DependenciesChecksum_;
- public byte[] MD5DependenciesChecksum
+ public byte[] MD5DependencyChecksum_;
+ public byte[] MD5DependencyChecksum
{
get
{
Contract.Requires(DependenciesCollected);
- if (MD5DependenciesChecksum_ == null && MD5Checksum != null)
+ if (MD5DependencyChecksum_ == null && MD5Checksum != null)
{
var c = MD5Checksum;
var transFuncDeps = new HashSet<Function>();
@@ -1918,9 +1918,9 @@ namespace Microsoft.Boogie { }
}
}
- MD5DependenciesChecksum_ = c;
+ MD5DependencyChecksum_ = c;
}
- return MD5DependenciesChecksum_;
+ return MD5DependencyChecksum_;
}
}
@@ -1932,16 +1932,16 @@ namespace Microsoft.Boogie { }
}
- string dependenciesChecksum;
- public string DependenciesChecksum
+ string dependencyChecksum;
+ public string DependencyChecksum
{
get
{
- if (dependenciesChecksum == null && MD5DependenciesChecksum != null)
+ if (dependencyChecksum == null && MD5DependencyChecksum != null)
{
- dependenciesChecksum = BitConverter.ToString(MD5DependenciesChecksum);
+ dependencyChecksum = BitConverter.ToString(MD5DependencyChecksum);
}
- return dependenciesChecksum;
+ return dependencyChecksum;
}
}
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index b16fb1ba..26a28e0e 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1999,7 +1999,7 @@ namespace Microsoft.Boogie { public string/*!*/ callee { get; set; }
public Procedure Proc;
public LocalVariable AssignedAssumptionVariable;
- public bool EmitDependenciesChecksum;
+ public bool EmitDependencyChecksum;
// Element of the following lists can be null, which means that
// the call happens with * as these parameters
@@ -2087,12 +2087,12 @@ namespace Microsoft.Boogie { stream.Write(" := ");
}
stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
- if (stream.UseForComputingChecksums && EmitDependenciesChecksum)
+ if (stream.UseForComputingChecksums && EmitDependencyChecksum)
{
- var c = Proc.DependenciesChecksum;
+ var c = Proc.DependencyChecksum;
if (c != null)
{
- stream.Write(string.Format("[dependencies_checksum:{0}]", c));
+ stream.Write(string.Format("[dependency_checksum:{0}]", c));
}
}
stream.Write("(");
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 8d372b0c..95a11a65 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1804,10 +1804,10 @@ namespace Microsoft.Boogie { this.name.Emit(stream, 0xF0, false);
if (stream.UseForComputingChecksums)
{
- var c = Func.DependenciesChecksum;
+ var c = Func.DependencyChecksum;
if (c != null)
{
- stream.Write(string.Format("[dependencies_checksum:{0}]", c));
+ stream.Write(string.Format("[dependency_checksum:{0}]", c));
}
}
stream.Write("(");
@@ -1893,7 +1893,19 @@ namespace Microsoft.Boogie { this.Type = type;
}
- public string/*!*/ FunctionName {
+ public override bool Equals(object obj) {
+ TypeCoercion other = obj as TypeCoercion;
+ if (other == null) {
+ return false;
+ } else {
+ return object.Equals(Type, other.Type);
+ }
+ }
+
+
+
+ public
+ string/*!*/ FunctionName {
get {
Contract.Ensures(Contract.Result<string>() != null);
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index eefc7102..32985053 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -57,7 +57,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Body != null);
}
-
public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
: base(tok)
@@ -77,24 +76,43 @@ namespace Microsoft.Boogie { get;
}
+ protected static bool CompareAttributesAndTriggers = false;
+
+ public static bool EqualWithAttributesAndTriggers(object a, object b) {
+ CompareAttributesAndTriggers = true;
+ var res = object.Equals(a, b);
+ Contract.Assert(CompareAttributesAndTriggers);
+ CompareAttributesAndTriggers = false;
+ return res;
+ }
+
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object obj) {
- if (obj == null)
+ return BinderEquals(obj);
+ }
+
+ public bool BinderEquals(object obj) {
+ if (obj == null) {
return false;
+ }
if (!(obj is BinderExpr) ||
- this.Kind != ((BinderExpr)obj).Kind)
+ this.Kind != ((BinderExpr) obj).Kind) {
return false;
+ }
+
+ var other = (BinderExpr) obj;
- BinderExpr other = (BinderExpr)obj;
- // Note, we consider quantifiers equal modulo the Triggers.
return this.TypeParameters.SequenceEqual(other.TypeParameters)
&& this.Dummies.SequenceEqual(other.Dummies)
+ && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))
&& object.Equals(this.Body, other.Body);
}
[Pure]
public override int GetHashCode() {
+ // Note, we don't hash triggers and attributes
+
// DO NOT USE Dummies.GetHashCode() because we want structurally
// identical Expr to have the same hash code **not** identical references
// to have the same hash code.
@@ -103,7 +121,6 @@ namespace Microsoft.Boogie { h = ( 53 * h ) + dummyVar.GetHashCode();
}
- // Note, we consider quantifiers equal modulo the Triggers.
h ^= this.Body.GetHashCode();
// DO NOT USE TypeParameters.GetHashCode() because we want structural
@@ -351,6 +368,22 @@ namespace Microsoft.Boogie { public override Absy StdDispatch(StandardVisitor visitor) {
return visitor.VisitQKeyValue(this);
}
+
+ public override bool Equals(object obj) {
+ var other = obj as QKeyValue;
+ if (other == null) {
+ return false;
+ } else {
+ return Key == other.Key && object.Equals(Params, other.Params) &&
+ (Next == null
+ ? other.Next == null
+ : object.Equals(Next, other.Next));
+ }
+ }
+
+ public override int GetHashCode() {
+ throw new NotImplementedException();
+ }
}
public class Trigger : Absy {
@@ -448,6 +481,20 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTrigger(this);
}
+
+ public override bool Equals(object obj) {
+ var other = obj as Trigger;
+ if (other == null) {
+ return false;
+ } else {
+ return this.Tr.SequenceEqual(other.Tr) &&
+ (Next == null ? other.Next == null : object.Equals(Next, other.Next));
+ }
+ }
+
+ public override int GetHashCode() {
+ throw new NotImplementedException();
+ }
}
public class ForallExpr : QuantifierExpr {
@@ -736,6 +783,15 @@ namespace Microsoft.Boogie { }
}
+ public override bool Equals(object obj) {
+ var other = obj as QuantifierExpr;
+ if (other == null) {
+ return false;
+ } else {
+ return this.BinderEquals(obj) &&
+ (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers));
+ }
+ }
}
diff --git a/Source/Core/AlphaEquality.cs b/Source/Core/AlphaEquality.cs new file mode 100644 index 00000000..1d4a1d95 --- /dev/null +++ b/Source/Core/AlphaEquality.cs @@ -0,0 +1,162 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System.ComponentModel;
+
+namespace Microsoft.Boogie
+{
+
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+ using System.Diagnostics.Contracts;
+
+ public class AlphaEquality : IEqualityComparer<Expr>
+ {
+ private readonly DeBruijnRenamer deBruijn = new DeBruijnRenamer();
+
+ bool IEqualityComparer<Expr>.Equals(Expr x, Expr y) {
+ var nx = deBruijn.Rename(x);
+ var ny = deBruijn.Rename(y);
+ return BinderExpr.EqualWithAttributesAndTriggers(nx, ny);
+ }
+
+ int IEqualityComparer<Expr>.GetHashCode(Expr obj) {
+ return 0;
+ // Best we can do because GetHashCode for Expression don't respect its equality.
+ // When it does, we can instead use:
+ // return deBruijn.Rename(obj).GetHashCode();
+ }
+
+ // Renames expressions into deBruijn indicies, such as
+ // (lambda x : int :: x + a)
+ // into
+ // (lambda bv#0 : int :: bv#0 + fv#0)
+ // It does not handle type variables yet, but it could be added.
+ //
+ // This class could be made public, but it is not since the Rename method
+ // could then leak FreeVariables out of here.
+ private class DeBruijnRenamer : Duplicator
+ {
+
+ // Maps from index positions and types to new variables
+ private readonly TypeDict<BoundVariable> boundVars =
+ new TypeDict<BoundVariable>("bv", ti => new BoundVariable(Token.NoToken, ti));
+
+ private readonly TypeDict<FreeVariable> freeVars =
+ new TypeDict<FreeVariable>("fv", ti => new FreeVariable(ti));
+
+ // These three variables are reset at the beginning of every renaming
+ private int boundVarCount, freeVarCount;
+ private Dictionary<Variable, FreeVariable> freeVarMap;
+
+ // Cached, previous results
+ private readonly Dictionary<Expr, Expr> cache = new Dictionary<Expr, Expr>();
+
+ public Expr Rename(Expr e) {
+ Expr ne;
+ if (!cache.TryGetValue(e, out ne)) {
+ boundVarCount = 0;
+ freeVarCount = 0;
+ freeVarMap = new Dictionary<Variable, FreeVariable>();
+
+ ne = VisitExpr(e);
+ cache[e] = ne;
+#if DEBUG_ALPHA_RENAMING
+ var wr = new TokenTextWriter("<console>", Console.Out, true);
+ Console.Write("nm( ");
+ e.Emit(wr);
+ Console.WriteLine(" )");
+ Console.Write(" = ");
+ ne.Emit(wr);
+ Console.WriteLine("");
+ Console.WriteLine("h = " + ne.GetHashCode());
+#endif
+ }
+ return ne;
+ }
+
+ public override BinderExpr VisitBinderExpr(BinderExpr node) {
+ var subst = new Dictionary<Variable, Expr>();
+ var newBound = new List<Variable>();
+ foreach (var bv in node.Dummies) {
+ var bvNew = boundVars[boundVarCount++, bv.TypedIdent.Type];
+ newBound.Add(bvNew);
+ subst[bv] = new IdentifierExpr(Token.NoToken, bvNew);
+ }
+ node.Dummies = this.VisitVariableSeq(newBound);
+ node.Body = this.VisitExpr(Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), node.Body));
+ return node;
+ }
+
+ public override Variable VisitVariable(Variable node) {
+ FreeVariable fv;
+ var bv = node as BoundVariable;
+ if (boundVars.ContainsValue(bv)) {
+ return node;
+ } else if (freeVarMap.TryGetValue(node, out fv)) {
+ return fv;
+ } else {
+ return freeVarMap[node] = freeVars[freeVarCount++, node.TypedIdent.Type];
+ }
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ var ie = (IdentifierExpr) base.VisitIdentifierExpr(node);
+ // Need to fix up the name, since IdentifierExpr's equality also checks the name
+ ie.Name = ie.Decl.TypedIdent.Name;
+ return ie;
+ }
+
+ private class TypeDict<A>
+ {
+ private readonly Dictionary<Tuple<int, Type>, A> vars = new Dictionary<Tuple<int, Type>, A>();
+
+ private readonly string Prefix; // either "bv" or "fv"
+ private readonly Func<TypedIdent, A> Mk; // either new BoundVar or new FreeVar
+
+ public TypeDict(string prefix, Func<TypedIdent, A> mk) {
+ Prefix = prefix;
+ Mk = mk;
+ }
+
+ // For debugging purposes, we create unique names when types differ, but the index are the same.
+ private int created = 0;
+
+ // Make sure that this index and this type is always mapped to the same variable
+ public A this[int i, Type t] {
+ get {
+ A v;
+ if (!vars.TryGetValue(Tuple.Create(i, t), out v)) {
+ v = Mk(new TypedIdent(Token.NoToken, Prefix + i + "#" + created++, t));
+ vars[Tuple.Create(i, t)] = v;
+ }
+ return v;
+ }
+ }
+
+ public bool ContainsValue(A a) {
+ return vars.ContainsValue(a);
+ }
+ }
+
+ private class FreeVariable : Variable
+ {
+ public FreeVariable(TypedIdent ti) : base(Token.NoToken, ti) {}
+
+ public override bool IsMutable {
+ get { throw new cce.UnreachableException(); }
+ }
+
+ public override void Register(ResolutionContext rc) {
+ throw new cce.UnreachableException();
+ }
+ }
+ }
+ }
+}
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 881daa7f..27f4eea7 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -164,6 +164,7 @@ <Compile Include="AbsyExpr.cs" />
<Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
+ <Compile Include="AlphaEquality.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index c884be3c..45c68fdd 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -52,6 +52,9 @@ namespace Microsoft.Boogie { }
private class LambdaVisitor : StandardVisitor {
+ private readonly Dictionary<Expr, FunctionCall> liftedLambdas =
+ new Dictionary<Expr, FunctionCall>(new AlphaEquality());
+
internal List<Expr/*!*/>/*!*/ lambdaAxioms = new List<Expr/*!*/>();
internal List<Function/*!*/>/*!*/ lambdaFunctions = new List<Function/*!*/>();
[ContractInvariantMethod]
@@ -148,43 +151,61 @@ namespace Microsoft.Boogie { }
}
+ var sw = new System.IO.StringWriter();
+ var wr = new TokenTextWriter(sw, true);
+ lambda.Emit(wr);
+ string lam_str = sw.ToString();
+
+ FunctionCall fcall;
IToken tok = lambda.tok;
Formal res = new Formal(tok, new TypedIdent(tok, TypedIdent.NoName, cce.NonNull(lambda.Type)), false);
- Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function",
- Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));
- lambdaFunctions.Add(fn);
- FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
- fcall.Func = fn; // resolve here
+ if (liftedLambdas.TryGetValue(lambda, out fcall)) {
+ if (CommandLineOptions.Clo.TraceVerify) {
+ Console.WriteLine("Old lambda: {0}", lam_str);
+ }
+ } else {
+ if (CommandLineOptions.Clo.TraceVerify) {
+ Console.WriteLine("New lambda: {0}", lam_str);
+ }
+ Function fn = new Function(tok, "lambda#" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function",
+ Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));
+
+ fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
+ fcall.Func = fn; // resolve here
+ liftedLambdas[lambda] = fcall;
- List<Expr/*!*/> selectArgs = new List<Expr/*!*/>();
- foreach (Variable/*!*/ v in lambda.Dummies) {
- Contract.Assert(v != null);
- selectArgs.Add(new IdentifierExpr(v.tok, v));
- }
- NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);
- axcall.Type = res.TypedIdent.Type;
- axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
- NAryExpr select = Expr.Select(axcall, selectArgs);
- select.Type = lambdaBody.Type;
- List<Type/*!*/> selectTypeParamActuals = new List<Type/*!*/>();
- List<TypeVariable> forallTypeVariables = new List<TypeVariable>();
- foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) {
- Contract.Assert(tp != null);
- selectTypeParamActuals.Add(tp);
- forallTypeVariables.Add(tp);
+ List<Expr/*!*/> selectArgs = new List<Expr/*!*/>();
+ foreach (Variable/*!*/ v in lambda.Dummies) {
+ Contract.Assert(v != null);
+ selectArgs.Add(new IdentifierExpr(v.tok, v));
+ }
+ NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);
+ axcall.Type = res.TypedIdent.Type;
+ axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
+ NAryExpr select = Expr.Select(axcall, selectArgs);
+ select.Type = lambdaBody.Type;
+ List<Type/*!*/> selectTypeParamActuals = new List<Type/*!*/>();
+ List<TypeVariable> forallTypeVariables = new List<TypeVariable>();
+ foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) {
+ Contract.Assert(tp != null);
+ selectTypeParamActuals.Add(tp);
+ forallTypeVariables.Add(tp);
+ }
+ forallTypeVariables.AddRange(freeTypeVars);
+ select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals);
+
+ Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody);
+ NAryExpr body = Expr.Eq(select, bb);
+ body.Type = Type.Bool;
+ body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ Trigger trig = new Trigger(select.tok, true, new List<Expr> { select });
+
+ lambdaFunctions.Add(fn);
+ lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies,
+ Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs),
+ trig, body));
}
- forallTypeVariables.AddRange(freeTypeVars);
- select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals);
-
- Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody);
- NAryExpr body = Expr.Eq(select, bb);
- body.Type = Type.Bool;
- body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- Trigger trig = new Trigger(select.tok, true, new List<Expr> { select });
- lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies,
- Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs),
- trig, body));
NAryExpr call = new NAryExpr(tok, fcall, callArgs);
call.Type = res.TypedIdent.Type;
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 05c4b44b..a9220a4c 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1066,7 +1066,7 @@ namespace Microsoft.Boogie {
#region Verify the implementation
- verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, programId);
+ verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependencyChecksum, impl.Name, impl.tok, programId);
using (var vcgen = CreateVCGen(program, checkers))
{
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index b5f6d1cd..d44aff7f 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -197,7 +197,7 @@ namespace Microsoft.Boogie // TODO(wuestholz): Maybe we should speed up this lookup.
var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);
if (oldProc != null
- && oldProc.DependenciesChecksum != node.Proc.DependenciesChecksum
+ && oldProc.DependencyChecksum != node.Proc.DependencyChecksum
&& node.AssignedAssumptionVariable == null)
{
if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
@@ -236,7 +236,7 @@ namespace Microsoft.Boogie }
else
{
- node.EmitDependenciesChecksum = true;
+ node.EmitDependencyChecksum = true;
}
}
@@ -308,7 +308,7 @@ namespace Microsoft.Boogie // TODO(wuestholz): Maybe we should speed up this lookup.
var funcs = newProg.TopLevelDeclarations.OfType<Function>();
return oldProc.DependenciesCollected
- && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependenciesChecksum == dep.DependenciesChecksum)));
+ && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));
}
public override Procedure VisitProcedure(Procedure node)
@@ -437,7 +437,7 @@ namespace Microsoft.Boogie {
priority = Priority.MEDIUM;
}
- else if (impl.DependenciesChecksum == null || result.DependeciesChecksum != impl.DependenciesChecksum)
+ else if (impl.DependencyChecksum == null || result.DependeciesChecksum != impl.DependencyChecksum)
{
priority = Priority.LOW;
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index d88d4667..fe40618e 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -112,6 +112,11 @@ namespace VC { return ret;
}
}
+
+ public override string ToString()
+ {
+ return info.impl.Name;
+ }
}
public class CallSite {
@@ -175,7 +180,13 @@ namespace VC { }
scs.interfaceExprs = newInterfaceExprs;
}
- return gen.Implies(callSiteExpr, svc.vcexpr);
+ //return gen.Implies(callSiteExpr, svc.vcexpr);
+ return svc.vcexpr;
+ }
+
+ public override string ToString()
+ {
+ return callSite.calleeName;
}
}
@@ -404,7 +415,7 @@ namespace VC { i++;
AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i];
IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr;
- CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, callSiteAssumeCmd.Attributes);
+ CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, assumeCmd.Attributes);
if (!callSites.ContainsKey(block))
callSites[block] = new List<CallSite>();
callSites[block].Add(cs);
diff --git a/Test/test2/LambdaExt.bpl b/Test/test2/LambdaExt.bpl new file mode 100644 index 00000000..be0d84ee --- /dev/null +++ b/Test/test2/LambdaExt.bpl @@ -0,0 +1,146 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure Simplest() { + var id1, id2 : [int]int; + id1 := (lambda x: int :: x); + id2 := (lambda x: int :: x); + assert id1 == id2; + id2 := (lambda x: int :: 0); + assert id1 == id2; // fail +} + +procedure Const() { + var v, w : [int][int]int; + var f, g : [int, int]int; + + v := (lambda x : int :: (lambda y : int :: x)); + + w := (lambda x : int :: (lambda i : int :: x)); + assert v == w; + + w := (lambda i : int :: (lambda y : int :: i)); + assert v == w; + + w := (lambda a : int :: (lambda b : int :: b)); + assert v == w; // should fail, now two different functions + + f := (lambda x : int, y : int :: x); + assert f == (lambda p : int, q : int :: p); + assert f == (lambda p : int, q : int :: q); // should fail, different functions +} + +procedure PolyConst() { + assert (lambda<A> x: A :: x) == (lambda<A>x: A :: x); // fails because of type parameters. this could be fixed. + /* // more tests, when it is fixed + var k1 : <A1>[A1]<B1>[B1]A1; + var k2 : <A2>[A2]<B2>[B2]A2; + k1 := (lambda<A> x: A :: (lambda<B> y: B :: x)); + k2 := (lambda<A> x: A :: (lambda<C> z: C :: x)); + assert k1 == k2; + k2 := (lambda<X> u: X :: (lambda<Y> v: Y :: u)); + assert k1 == k2; */ +} + +procedure FreeVarP() { + var k : real; + var m : [int]real; + m := (lambda x:int :: k); + assert m[0] == k; +} + +procedure FreeVarQ() { + var k : int; + var m : [int]int; + m := (lambda x:int :: k); // should be a different lambda from in FreeVarP, because they have different types + assert m[0] == k; +} + +procedure Quantifiers() { + var k1 : [int]bool; + var k2 : [int]bool; + k1 := (lambda x: int :: (exists y: int :: x > y)); + k2 := (lambda x: int :: (exists y: int :: x > y)); + assert k1 == k2; + k2 := (lambda x: int :: (exists z: int :: x > z)); + assert k1 == k2; +} + +procedure FreeVariables() { + var m : [bool,bool,bool]bool; + var k : [bool,bool]bool; + + var f : [bool]bool; + var g : [bool]bool; + + var a : bool; + var b : bool; + + f := (lambda r: bool :: a); + g := (lambda s: bool :: b); + if (a == b) { + assert f == g; // should be OK + } else { + assert f == g; // should fail + } + + f := (lambda r: bool :: k[a,b]); + g := (lambda s: bool :: k[b,a]); + if (a == b) { + assert f == g; // should be OK + } else { + assert f == g; // should fail + } + + f := (lambda r: bool :: m[a,a,b]); + g := (lambda s: bool :: m[a,b,b]); + if (a == b) { + assert f == g; // should fail because they are different lambda + } else { + assert f == g; // should fail because they are different lambda + } +} + +function f(int) : int; + +procedure Triggers() { + var a,b : [int]bool; + a := (lambda x:int :: (forall u:int :: { f(u) } x == f(u))); + b := (lambda y:int :: (forall v:int :: { f(v) } y == f(v))); + assert a == b; + b := (lambda y:int :: (forall v:int :: y == f(v))); + assert a == b; // should fail because triggers are different +} + +procedure Attributes() { + var a,b : [int]bool; + a := (lambda x:int :: (forall u:int :: {:attrib f(u) } x == f(u))); + b := (lambda y:int :: (forall v:int :: {:attrib f(v) } y == f(v))); + assert a == b; + b := (lambda y:int :: (forall v:int :: {:battrib f(v) } y == f(v))); + assert a == b; // should fail since attributes are different + a := (lambda x:int :: (forall u:int :: {:battrib f(x) } x == f(u))); + assert a == b; // should fail since attributes are different +} + +procedure Old() { + var u,v : [int]int; + var a,b : int; + u := (lambda x:int :: old(x+a)); + v := (lambda y:int :: old(y+b)); + if (a == b) { + assert u == v; // ok + } else { + assert u == v; // fails + } +} + +type Box; +function $Box<T>(T) : Box; +function $Unbox<T>(Box) : T; + +procedure Coercion() { + assert (lambda x: Box :: $Box($Unbox(x): int)) + == (lambda y: Box :: $Box($Unbox(y): int)); +} + diff --git a/Test/test2/LambdaExt.bpl.expect b/Test/test2/LambdaExt.bpl.expect new file mode 100644 index 00000000..fac42eb2 --- /dev/null +++ b/Test/test2/LambdaExt.bpl.expect @@ -0,0 +1,56 @@ +LambdaExt.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(6,7): anon0 +LambdaExt.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(17,5): anon0 +LambdaExt.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(17,5): anon0 +LambdaExt.bpl(34,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(34,3): anon0 +LambdaExt.bpl(84,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else +LambdaExt.bpl(92,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(92,5): anon10_Else +LambdaExt.bpl(98,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(82,5): anon9_Then + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(90,5): anon10_Then + LambdaExt.bpl(95,5): anon6 + LambdaExt.bpl(98,5): anon11_Then +LambdaExt.bpl(100,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(92,5): anon10_Else + LambdaExt.bpl(95,5): anon6 + LambdaExt.bpl(100,5): anon11_Else +LambdaExt.bpl(112,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(108,5): anon0 +LambdaExt.bpl(119,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(121,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(123,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(134,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(129,5): anon0 + LambdaExt.bpl(134,5): anon3_Else + +Boogie program verifier finished with 4 verified, 13 errors |