diff options
Diffstat (limited to 'Source')
29 files changed, 1763 insertions, 432 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0dbcaaba..6cce0aac 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -34,7 +34,8 @@ namespace Microsoft.Boogie.AbstractInterpretation public class Node
{
public readonly Variable V; // variable has type bool or int
- // For an integer variable (Lo,Hi) indicates Lo <= V < Hi, where Lo==null means no lower bound and Hi==null means no upper bound
+ // For an integer variable (Lo,Hi) indicates Lo <= V < Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
+ // For a real variable (Lo,Hi) indicates Lo <= V <= Hi, where Lo==null means no lower bound and Hi==null means no upper bound.
// For a boolean variable, (Lo,Hi) is one of: (null,null) for {false,true}, (null,1) for {false}, and (1,null) for {true}.
public readonly BigInteger? Lo;
public readonly BigInteger? Hi;
@@ -153,7 +154,7 @@ namespace Microsoft.Boogie.AbstractInterpretation if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer != CommandLineOptions.InstrumentationPlaces.Everywhere) {
// omit invariants about readonly variables
return Expr.True;
- } else if (V.TypedIdent.Type.IsBool) {
+ } else if (V.TypedIdent.Type.IsBool) {
if (Lo == null && Hi == null) {
return Expr.True;
} else {
@@ -161,21 +162,40 @@ namespace Microsoft.Boogie.AbstractInterpretation var ide = new IdentifierExpr(Token.NoToken, V);
return Hi == null ? ide : Expr.Not(ide);
}
- } else {
+ } else if (V.TypedIdent.Type.IsInt) {
Expr e = Expr.True;
if (Lo != null && Hi != null && Lo + 1 == Hi) {
// produce an equality
var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplEq(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo))));
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+ } else {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+ }
+ if (Hi != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+ }
+ }
+ return e;
+ } else {
+ Contract.Assert(V.TypedIdent.Type.IsReal);
+ Expr e = Expr.True;
+ if (Lo != null && Hi != null && Lo == Hi) {
+ // produce an equality
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
} else {
// produce a (possibly empty) conjunction of inequalities
if (Lo != null) {
var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLe(Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)), ide));
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
}
if (Hi != null) {
var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplLt(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Hi))));
+ e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
}
}
return e;
@@ -183,6 +203,17 @@ namespace Microsoft.Boogie.AbstractInterpretation }
}
+ static Expr NumberToExpr(BigInteger n, Type ty) {
+ if (n == null) {
+ return null;
+ } else if (ty.IsReal) {
+ return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+ } else {
+ Contract.Assume(ty.IsInt);
+ return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
+ }
+ }
+
List<BigInteger> upThresholds; // invariant: thresholds are sorted
List<BigInteger> downThresholds; // invariant: thresholds are sorted
@@ -281,8 +312,8 @@ namespace Microsoft.Boogie.AbstractInterpretation } else {
var lo = Node.Max(x.Lo, y.Lo, true);
var hi = Node.Min(x.Hi, y.Hi, true);
- // if hi<=lo, then we're overconstrained
- if (lo != null && hi != null && hi <= lo) {
+ // if hi<=lo (or hi<lo for reals), then we're overconstrained
+ if (lo != null && hi != null && (x.V.TypedIdent.Type.IsReal ? hi < lo : hi <= lo)) {
return bottom;
}
n = new Node(x.V, lo, hi);
@@ -446,7 +477,7 @@ namespace Microsoft.Boogie.AbstractInterpretation E_Common Constraint(Expr expr, Node state) {
Variable v;
if (IsVariable(expr, out v)) {
- var n = new Node(v, new BigInteger(1), null);
+ var n = new Node(v, BigInteger.One, null);
return new E(n);
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
@@ -456,7 +487,7 @@ namespace Microsoft.Boogie.AbstractInterpretation if (e.Fun is UnaryOperator) {
if (((UnaryOperator)e.Fun).Op == UnaryOperator.Opcode.Not) {
if (IsVariable(e.Args[0], out v)) {
- var n = new Node(v, null, new BigInteger(1));
+ var n = new Node(v, null, BigInteger.One);
return new E(n);
}
}
@@ -523,7 +554,7 @@ namespace Microsoft.Boogie.AbstractInterpretation BigInteger? lo, hi;
PartiallyEvaluate(arg0, state, out lo, out hi);
if (lo != null) {
- var n = new Node(v, lo + 1, null);
+ var n = new Node(v, v.TypedIdent.Type.IsReal ? lo : lo + 1, null);
c = new E(n);
}
}
@@ -531,7 +562,7 @@ namespace Microsoft.Boogie.AbstractInterpretation BigInteger? lo, hi;
PartiallyEvaluate(arg1, state, out lo, out hi);
if (hi != null) {
- var n = new Node(v, null, hi - 1);
+ var n = new Node(v, null, v.TypedIdent.Type.IsReal ? hi : hi - 1);
c = c == null ? new E(n) : (E_Common)Meet(c, new E(n));
}
}
@@ -556,7 +587,7 @@ namespace Microsoft.Boogie.AbstractInterpretation private E ConstrainNeq(Node state, Variable v, Expr arg) {
BigInteger? lo, hi;
if (PartiallyEvaluate(arg, state, out lo, out hi)) {
- if (lo != null && hi != null && lo + 1 == hi) {
+ if (!v.TypedIdent.Type.IsReal && lo != null && hi != null && lo + 1 == hi) {
var exclude = lo;
// If the partially evaluated arg (whose value is "exclude") is an end-point of
// the interval known for "v", then produce a constraint that excludes that bound.
@@ -610,19 +641,19 @@ namespace Microsoft.Boogie.AbstractInterpretation return lo != null || hi != null;
}
- class PEVisitor : StandardVisitor
+ class PEVisitor : ReadOnlyVisitor
{
public BigInteger? Lo;
public BigInteger? Hi;
- readonly BigInteger one = new BigInteger(1);
+ readonly BigInteger one = BigInteger.One;
Node N;
public PEVisitor(Node n) {
N = n;
}
- // Override visitors for all expressions that can return a boolean or integer result
+ // Override visitors for all expressions that can return a boolean, integer, or real result
public override Expr VisitExpr(Expr node) {
Lo = Hi = null;
@@ -634,9 +665,10 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = n;
Hi = n + 1;
} else if (node.Val is BigDec) {
- var n = ((BigDec)node.Val).Floor(-BigInteger.Pow(10, 12), BigInteger.Pow(10, 12));
- Lo = n;
- Hi = n + 1;
+ BigInteger floor, ceiling;
+ ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor;
+ Hi = ceiling;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
@@ -665,10 +697,10 @@ namespace Microsoft.Boogie.AbstractInterpretation VisitExpr(node.Args[0]);
lo = Lo; hi = Hi;
if (hi != null) {
- Lo = 1 - hi;
+ Lo = node.Type.IsReal ? -hi : 1 - hi;
}
if (lo != null) {
- Hi = 1 - lo;
+ Hi = node.Type.IsReal ? -lo : 1 - lo;
}
}
else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -689,6 +721,7 @@ namespace Microsoft.Boogie.AbstractInterpretation VisitExpr(node.Args[1]);
lo1 = Lo; hi1 = Hi;
Lo = Hi = null;
+ var isReal = node.Args[0].Type.IsReal;
switch (op.Op) {
case BinaryOperator.Opcode.And:
if (hi0 != null || hi1 != null) {
@@ -739,12 +772,16 @@ namespace Microsoft.Boogie.AbstractInterpretation // For Eq:
// If the (lo0,hi0) and (lo1,hi1) ranges do not overlap, the answer is false.
// If both ranges are the same unit range, then the answer is true.
- if (hi0 != null && lo1 != null && hi0 <= lo1) {
+ if (hi0 != null && lo1 != null && (isReal ? hi0 < lo1 : hi0 <= lo1)) {
+ // no overlap
Lo = null; Hi = one;
- } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
+ } else if (lo0 != null && hi1 != null && (isReal ? hi1 < lo0 : hi1 <= lo0)) {
Lo = null; Hi = one;
+ // no overlaop
} else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null &&
- lo0 + 1 == hi0 && lo0 == lo1 && lo1 + 1 == hi1) {
+ lo0 == lo1 && hi0 == hi1 && // ranges are the same
+ (isReal ? lo0 == hi0 : lo0 + 1 == hi0)) { // unit range
+ // both ranges are the same unit range
Lo = one; Hi = null;
}
if (op.Op == BinaryOperator.Opcode.Neq) {
@@ -752,42 +789,68 @@ namespace Microsoft.Boogie.AbstractInterpretation }
break;
case BinaryOperator.Opcode.Le:
- case BinaryOperator.Opcode.Gt:
- // If hi0 - 1 <= lo1, then the answer is true.
- // If hi1 <= lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 - 1 <= lo1) {
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
- Lo = null; Hi = one;
- }
- if (op.Op == BinaryOperator.Opcode.Gt) {
- var tmp = Lo; Lo = Hi; Hi = tmp;
+ if (isReal) {
+ // If hi0 <= lo1, then the answer is true.
+ // If hi1 < lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (hi1 != null && lo0 != null && hi1 < lo0) {
+ Lo = null; Hi = one;
+ }
+ } else {
+ // If hi0 - 1 <= lo1, then the answer is true.
+ // If hi1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 - 1 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
+ Lo = null; Hi = one;
+ }
}
break;
case BinaryOperator.Opcode.Lt:
- case BinaryOperator.Opcode.Ge:
- // If hi0 <= lo1, then the answer is true.
- // If hi1 - 1 <= lo0, then the answer is false.
- if (hi0 != null && lo1 != null && hi0 <= lo1) {
- Lo = one; Hi = null;
- } else if (lo0 != null && hi1 != null && hi1 - 1 <= lo0) {
- Lo = null; Hi = one;
- }
- if (op.Op == BinaryOperator.Opcode.Ge) {
- var tmp = Lo; Lo = Hi; Hi = tmp;
+ if (isReal) {
+ // If hi0 < lo1, then the answer is true.
+ // If hi1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 < lo1) {
+ Lo = one; Hi = null;
+ } else if (hi1 != null && lo0 != null && hi1 <= lo0) {
+ Lo = null; Hi = one;
+ }
+ } else {
+ // If hi0 <= lo1, then the answer is true.
+ // If hi1 - 1 <= lo0, then the answer is false.
+ if (hi0 != null && lo1 != null && hi0 <= lo1) {
+ Lo = one; Hi = null;
+ } else if (lo0 != null && hi1 != null && hi1 - 1 <= lo0) {
+ Lo = null; Hi = one;
+ }
}
break;
+ case BinaryOperator.Opcode.Gt:
+ // swap the operands and then continue as Lt
+ {
+ var tmp = lo0; lo0 = lo1; lo1 = tmp;
+ tmp = hi0; hi0 = hi1; hi1 = tmp;
+ }
+ goto case BinaryOperator.Opcode.Lt;
+ case BinaryOperator.Opcode.Ge:
+ // swap the operands and then continue as Le
+ {
+ var tmp = lo0; lo0 = lo1; lo1 = tmp;
+ tmp = hi0; hi0 = hi1; hi1 = tmp;
+ }
+ goto case BinaryOperator.Opcode.Le;
case BinaryOperator.Opcode.Add:
if (lo0 != null && lo1 != null) {
Lo = lo0 + lo1;
}
if (hi0 != null && hi1 != null) {
- Hi = hi0 + hi1 - 1;
+ Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1;
}
break;
case BinaryOperator.Opcode.Sub:
if (lo0 != null && hi1 != null) {
- Lo = lo0 - hi1 + 1;
+ Lo = isReal ? lo0 - hi1 : lo0 - hi1 + 1;
}
if (hi0 != null && lo1 != null) {
Hi = hi0 - lo1;
@@ -798,38 +861,38 @@ namespace Microsoft.Boogie.AbstractInterpretation if (lo0 != null && lo1 != null) {
if (0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
Lo = lo0 * lo1;
- Hi = hi0 == null || hi1 == null ? null : (hi0 - 1) * (hi1 - 1) + 1;
+ Hi = hi0 == null || hi1 == null ? null : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1;
} else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) {
Lo = null; // approximation
- Hi = lo0 * lo1 + 1;
+ Hi = isReal ? lo0 * lo1 : lo0 * lo1 + 1;
}
}
break;
case BinaryOperator.Opcode.Div:
// this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = new BigInteger(0);
+ Lo = BigInteger.Zero;
Hi = hi0;
}
break;
case BinaryOperator.Opcode.Mod:
// this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = new BigInteger(0);
+ Lo = BigInteger.Zero;
Hi = hi1;
}
break;
case BinaryOperator.Opcode.RealDiv:
// this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = new BigInteger(0);
- Hi = hi1;
+ Lo = BigInteger.Zero;
+ Hi = 1 <= (BigInteger)lo1 ? hi0 : null;
}
break;
case BinaryOperator.Opcode.Pow:
// this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
- Lo = new BigInteger(0);
+ Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero;
Hi = hi1;
}
break;
@@ -990,7 +1053,7 @@ namespace Microsoft.Boogie.AbstractInterpretation }
}
- public class ThresholdFinder : StandardVisitor
+ public class ThresholdFinder : ReadOnlyVisitor
{
readonly Implementation Impl;
public ThresholdFinder(Implementation impl) {
@@ -1041,6 +1104,7 @@ namespace Microsoft.Boogie.AbstractInterpretation Contract.Assert(node.Args.Count == 2);
var arg0 = node.Args[0];
var arg1 = node.Args[1];
+ var offset = arg0.Type.IsReal ? 0 : 1;
BigInteger? k;
switch (op.Op) {
case BinaryOperator.Opcode.Eq:
@@ -1072,22 +1136,22 @@ namespace Microsoft.Boogie.AbstractInterpretation k = AsIntLiteral(arg1);
if (k != null) {
var i = (BigInteger)k;
- ups.Add(i + 1);
- ups.Add(i + 2);
+ ups.Add(i + offset);
+ ups.Add(i + 1 + offset);
}
break;
case BinaryOperator.Opcode.Lt:
k = AsIntLiteral(arg0);
if (k != null) {
var i = (BigInteger)k;
- downs.Add(i);
+ downs.Add(i );
downs.Add(i + 1);
}
k = AsIntLiteral(arg1);
if (k != null) {
var i = (BigInteger)k;
- ups.Add(i);
- ups.Add(i + 1);
+ ups.Add(i - 1 + offset);
+ ups.Add(i + offset);
}
break;
case BinaryOperator.Opcode.Ge:
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 301774f6..feabb425 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -48,6 +48,11 @@ namespace Microsoft.Basetypes { }
[Pure]
+ public static BigDec FromBigInt(BIM v) {
+ return new BigDec(v, 0);
+ }
+
+ [Pure]
public static BigDec FromString(string v) {
if (v == null) throw new FormatException();
@@ -131,31 +136,25 @@ namespace Microsoft.Basetypes { ////////////////////////////////////////////////////////////////////////////
// Conversion operations
- [Pure]
- public BIM Floor(BIM? minimum, BIM? maximum) {
+ public void FloorCeiling(out BIM floor, out BIM ceiling) {
BIM n = this.mantissa;
-
- if (this.exponent >= 0) {
- int e = this.exponent;
- while (e > 0 && (minimum == null || minimum <= n) && (maximum == null || n <= maximum)) {
+ int e = this.exponent;
+ if (n.IsZero) {
+ floor = ceiling = n;
+ } else if (0 <= e) {
+ // it's an integer
+ for (; 0 < e; e--) {
n = n * ten;
- e = e - 1;
}
- }
- else {
- int e = -this.exponent;
- while (e > 0 && !n.IsZero) {
- n = n / ten;
- e = e - 1;
+ floor = ceiling = n;
+ } else {
+ // it's a non-zero integer, so the ceiling is one more than the fllor
+ for (; e < 0 && !n.IsZero; e++) {
+ n = n / ten; // since we're dividing by a positive number, this will round down
}
+ floor = n;
+ ceiling = n + 1;
}
-
- if (minimum != null && n < minimum)
- return (BIM)minimum;
- else if (maximum != null && maximum < n)
- return (BIM)maximum;
- else
- return n;
}
[Pure]
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 8408bf83..11e10e93 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -8,7 +8,7 @@ using System.Diagnostics; namespace Microsoft.Boogie
{
- public class LinearEraser : StandardVisitor
+ public class LinearEraser : ReadOnlyVisitor
{
private QKeyValue RemoveLinearAttribute(QKeyValue iter)
{
@@ -31,7 +31,7 @@ namespace Microsoft.Boogie CONST
}
- public class LinearTypeChecker : StandardVisitor
+ public class LinearTypeChecker : ReadOnlyVisitor
{
public Program program;
public int errorCount;
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index cde18ba4..7583d250 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -350,6 +350,10 @@ namespace Microsoft.Boogie }
returnExpr = Expr.Or(returnExpr, expr);
}
+ ResolutionContext rc = new ResolutionContext(null);
+ rc.StateMode = ResolutionContext.State.Two;
+ returnExpr.Resolve(rc);
+ returnExpr.Typecheck(new TypecheckingContext(null));
return returnExpr;
}
@@ -360,6 +364,10 @@ namespace Microsoft.Boogie {
transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path));
}
+ ResolutionContext rc = new ResolutionContext(null);
+ rc.StateMode = ResolutionContext.State.Two;
+ transitionRelation.Resolve(rc);
+ transitionRelation.Typecheck(new TypecheckingContext(null));
return transitionRelation;
}
@@ -584,8 +592,10 @@ namespace Microsoft.Boogie foreach (AssertCmd assertCmd in first.thatGate)
{
requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);
+ requiresExpr.Type = Type.Bool;
}
Expr failureExpr = Expr.Not(requiresExpr);
+ failureExpr.Type = Type.Bool;
List<Requires> requires = DisjointnessRequires(program, first, second);
requires.Add(new Requires(false, failureExpr));
foreach (AssertCmd assertCmd in second.thisGate)
@@ -616,15 +626,13 @@ namespace Microsoft.Boogie List<Variable> inputs = new List<Variable>();
inputs.AddRange(second.thisInParams);
- Expr failureExpr = Expr.True;
List<Requires> requires = DisjointnessRequires(program, null, second);
- requires.Add(new Requires(false, failureExpr));
foreach (AssertCmd assertCmd in second.thisGate)
{
requires.Add(new Requires(false, assertCmd.Expr));
}
- Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);
+ Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(Expr.True);
List<Ensures> ensures = new List<Ensures>();
Ensures ensureCheck = new Ensures(false, ensuresExpr);
ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index f442c1af..6c78f80d 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -268,35 +268,38 @@ namespace Microsoft.Boogie private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
- List<Expr> exprSeq = new List<Expr>();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
- }
- if (yieldProc == null)
+ if (!CommandLineOptions.Clo.TrustNonInterference)
{
- List<Variable> inputs = new List<Variable>();
+ List<Expr> exprSeq = new List<Expr>();
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
+ exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
}
foreach (IdentifierExpr ie in globalMods)
{
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
+ exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
}
- yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ if (yieldProc == null)
+ {
+ List<Variable> inputs = new List<Variable>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ inputs.Add(f);
+ }
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
+ inputs.Add(f);
+ }
+ yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
+ yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ }
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
+ yieldCallCmd.Proc = yieldProc;
+ newCmds.Add(yieldCallCmd);
}
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
- yieldCallCmd.Proc = yieldProc;
- newCmds.Add(yieldCallCmd);
if (pc != null)
{
@@ -417,18 +420,13 @@ namespace Microsoft.Boogie List<string> parallelCalleeNames = new List<string>();
List<Expr> ins = new List<Expr>();
List<IdentifierExpr> outs = new List<IdentifierExpr>();
+ string procName = "og";
foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
- parallelCalleeNames.Add(callCmd.Proc.Name);
+ procName = procName + "_" + callCmd.Proc.Name;
ins.AddRange(callCmd.Ins);
outs.AddRange(callCmd.Outs);
}
- parallelCalleeNames.Sort();
- string procName = "og";
- foreach (string calleeName in parallelCalleeNames)
- {
- procName = procName + "_" + calleeName;
- }
Procedure proc;
if (asyncAndParallelCallDesugarings.ContainsKey(procName))
{
@@ -460,11 +458,11 @@ namespace Microsoft.Boogie Substitution subst = Substituter.SubstitutionFromHashtable(map);
foreach (Requires req in callCmd.Proc.Requires)
{
- requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition)));
+ requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));
}
foreach (Ensures ens in callCmd.Proc.Ensures)
{
- ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition)));
+ ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));
}
count++;
}
@@ -472,7 +470,7 @@ namespace Microsoft.Boogie proc.AddAttribute("yields");
asyncAndParallelCallDesugarings[procName] = proc;
}
- CallCmd dummyCallCmd = new CallCmd(Token.NoToken, proc.Name, ins, outs);
+ CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
dummyCallCmd.Proc = proc;
newCmds.Add(dummyCallCmd);
}
@@ -555,7 +553,7 @@ namespace Microsoft.Boogie }
else
{
- AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr);
+ AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr, ensures.Attributes);
assertCmd.ErrorData = "Backwards non-interference check failed";
newCmds.Add(assertCmd);
}
@@ -859,7 +857,7 @@ namespace Microsoft.Boogie asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
}
var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
- CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
+ CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);
dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmds.Add(dummyCallCmd);
}
@@ -1186,7 +1184,7 @@ namespace Microsoft.Boogie HashSet<int> attrs = QKeyValue.FindIntAttributes(kv, "phase");
if (attrs.Count == 0)
{
- attrs.Add(int.MaxValue);
+ attrs.Add(0); // default phase of requires, ensures and assertions is 0
}
return attrs;
}
@@ -1258,6 +1256,8 @@ namespace Microsoft.Boogie Program program = linearTypeChecker.program;
foreach (int phaseNum in moverTypeChecker.allPhaseNums)
{
+ if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;
+
MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);
List<Implementation> impls = new List<Implementation>();
List<Procedure> procs = new List<Procedure>();
@@ -1273,7 +1273,7 @@ namespace Microsoft.Boogie duplicateProc.Modifies = new List<IdentifierExpr>();
program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));
CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);
- Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), action.Blocks);
+ Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, action.Blocks);
impl.Proc = duplicateProc;
impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index 45d538df..a3a621ac 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -32,8 +32,10 @@ namespace Microsoft.Boogie List<Declaration> decls = new List<Declaration>();
OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
- MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
-
+ if (!CommandLineOptions.Clo.TrustAtomicityTypes)
+ {
+ MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+ }
foreach (Declaration decl in decls)
{
Procedure proc = decl as Procedure;
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index ce29a700..27a4e6a5 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -177,7 +177,7 @@ namespace Microsoft.Boogie }
}
- public class MoverTypeChecker : StandardVisitor
+ public class MoverTypeChecker : ReadOnlyVisitor
{
public int FindPhaseNumber(Procedure proc)
{
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index b220b373..60f76232 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -325,15 +325,15 @@ namespace Microsoft.Boogie { }
}
- public IEnumerable<Implementation> Implementations() - { - return TopLevelDeclarations.OfType<Implementation>(); - } - - public IEnumerable<Block> Blocks() - { - return Implementations().Select(Item => Item.Blocks).SelectMany(Item => Item); - } + public IEnumerable<Implementation> Implementations()
+ {
+ return TopLevelDeclarations.OfType<Implementation>();
+ }
+
+ public IEnumerable<Block> Blocks()
+ {
+ return Implementations().Select(Item => Item.Blocks).SelectMany(Item => Item);
+ }
public void ComputeStronglyConnectedComponents() {
foreach (Declaration d in this.TopLevelDeclarations) {
@@ -880,30 +880,33 @@ namespace Microsoft.Boogie { fullMap[impl.Name] = null;
procsWithIrreducibleLoops.Add(impl.Name);
- // statically unroll loops in this procedure
+ if (CommandLineOptions.Clo.ExtractLoopsUnrollIrreducible)
+ {
+ // statically unroll loops in this procedure
- // First, build a map of the current blocks
- var origBlocks = new Dictionary<string, Block>();
- foreach (var blk in impl.Blocks) origBlocks.Add(blk.Label, blk);
+ // First, build a map of the current blocks
+ var origBlocks = new Dictionary<string, Block>();
+ foreach (var blk in impl.Blocks) origBlocks.Add(blk.Label, blk);
- // unroll
- Block start = impl.Blocks[0];
- impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound, false);
+ // unroll
+ Block start = impl.Blocks[0];
+ impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound, false);
- // Now construct the "map back" information
- // Resulting block label -> original block
- var blockMap = new Dictionary<string, Block>();
- foreach (var blk in impl.Blocks)
- {
- var sl = LoopUnroll.sanitizeLabel(blk.Label);
- if (sl == blk.Label) blockMap.Add(blk.Label, blk);
- else
+ // Now construct the "map back" information
+ // Resulting block label -> original block
+ var blockMap = new Dictionary<string, Block>();
+ foreach (var blk in impl.Blocks)
{
- Contract.Assert(origBlocks.ContainsKey(sl));
- blockMap.Add(blk.Label, origBlocks[sl]);
+ var sl = LoopUnroll.sanitizeLabel(blk.Label);
+ if (sl == blk.Label) blockMap.Add(blk.Label, blk);
+ else
+ {
+ Contract.Assert(origBlocks.ContainsKey(sl));
+ blockMap.Add(blk.Label, origBlocks[sl]);
+ }
}
+ fullMap[impl.Name] = blockMap;
}
- fullMap[impl.Name] = blockMap;
}
}
}
@@ -2156,14 +2159,14 @@ namespace Microsoft.Boogie { List<TypeVariable>/*!*/ quantifiedTypeVars = new List<TypeVariable>();
foreach (TypeVariable/*!*/ t in TypeParameters) {
Contract.Assert(t != null);
- quantifiedTypeVars.Add(new TypeVariable(Token.NoToken, t.Name));
+ quantifiedTypeVars.Add(new TypeVariable(tok, t.Name));
}
Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs);
// specify the type of the function, because it might be that
// type parameters only occur in the output type
call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
- Expr def = Expr.Eq(call, definition);
+ Expr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, definition);
if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) {
def = new ForallExpr(tok, quantifiedTypeVars, dummies,
kv,
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index b84770e3..c7a813d3 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1631,6 +1631,20 @@ namespace Microsoft.Boogie { return desugaring;
}
}
+ /// <summary>
+ /// This method invokes "visitor.Visit" on the desugaring, and then updates the
+ /// desugaring to the result thereof. The method's intended use is for subclasses
+ /// of StandardVisitor that need to also visit the desugaring. Note, since the
+ /// "desugaring" field is updated, this is not an appropriate method to be called
+ /// be a ReadOnlyVisitor; such visitors should instead just call
+ /// visitor.Visit(sugaredCmd.Desugaring).
+ /// </summary>
+ public void VisitDesugaring(StandardVisitor visitor) {
+ Contract.Requires(visitor != null && !(visitor is ReadOnlyVisitor));
+ if (desugaring != null) {
+ desugaring = (Cmd)visitor.Visit(desugaring);
+ }
+ }
protected abstract Cmd/*!*/ ComputeDesugaring();
public override void Emit(TokenTextWriter stream, int level) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index e2bbcdf5..63474c69 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -167,28 +167,33 @@ namespace Microsoft.Boogie { }
}
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ public override void ComputeFreeVariables(Set freeVars) {
//Contract.Requires(freeVars != null);
- foreach (Variable/*!*/ v in Dummies) {
+ ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars);
+ }
+
+ public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, QKeyValue attributes, Set freeVars) {
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+
+ foreach (var v in dummies) {
Contract.Assert(v != null);
Contract.Assert(!freeVars[v]);
}
- Body.ComputeFreeVariables(freeVars);
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- foreach (TypeVariable/*!*/ w in v.TypedIdent.Type.FreeVariables) {
- Contract.Assert(w != null);
- freeVars.Add(w);
+ body.ComputeFreeVariables(freeVars);
+ for (var a = attributes; a != null; a = a.Next) {
+ foreach (var o in a.Params) {
+ var e = o as Expr;
+ if (e != null) {
+ e.ComputeFreeVariables(freeVars);
+ }
}
}
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- freeVars.Remove(v);
- }
- foreach (TypeVariable/*!*/ v in TypeParameters) {
- Contract.Assert(v != null);
- freeVars.Remove(v);
+ foreach (var v in dummies) {
+ freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
}
+ freeVars.RemoveRange(dummies);
+ freeVars.RemoveRange(typeParameters);
}
protected List<TypeVariable> GetUnmentionedTypeParameters() {
@@ -353,6 +358,10 @@ namespace Microsoft.Boogie { newParams.Add(o);
return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
}
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ return visitor.VisitQKeyValue(this);
+ }
}
public class Trigger : Absy {
@@ -599,7 +608,7 @@ namespace Microsoft.Boogie { }
#region never triggers
- private class NeverTriggerCollector : StandardVisitor {
+ private class NeverTriggerCollector : ReadOnlyVisitor {
QuantifierExpr/*!*/ parent;
[ContractInvariantMethod]
void ObjectInvariant() {
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 4efe1aea..00e1a5c6 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -2093,6 +2093,11 @@ Contract.Requires(that != null); private static int MinBitsFor(Type t) {
Contract.Requires(t != null);
Contract.Requires(t.IsBv);
+
+ if (t is TypeSynonymAnnotation) {
+ return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType);
+ }
+
Contract.Ensures(0 <= Contract.Result<int>());
if (t is BvType) {
return t.BvBits;
@@ -2195,6 +2200,11 @@ Contract.Requires(that != null); Contract.Requires(t != null);
Contract.Requires(t.IsBv && 0 <= to && MinBitsFor(t) <= to);
Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= to);
+
+ if(t is TypeSynonymAnnotation) {
+ return IncreaseBits(((TypeSynonymAnnotation)t).ExpandedType, to);
+ }
+
t = FollowProxy(t);
if (t is BvType) {
return to - t.BvBits;
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index a4374623..98086cf0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -488,6 +488,12 @@ namespace Microsoft.Boogie { public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
public string OwickiGriesDesugaredOutputFile = null;
+ public bool TrustAtomicityTypes = false;
+ public bool TrustNonInterference = false;
+ public int TrustPhasesUpto = -1;
+ public int TrustPhasesDownto = int.MaxValue;
+
+ public bool UseParallelism = true;
public enum VCVariety {
Structured,
@@ -605,6 +611,10 @@ namespace Microsoft.Boogie { Call
};
public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;
+
+ public string PrintFixedPoint = null;
+
+ public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)
public enum TypeEncoding {
None,
@@ -733,6 +743,20 @@ namespace Microsoft.Boogie { }
return true;
+ case "trustPhasesUpto":
+ if (ps.ConfirmArgumentCount(1))
+ {
+ ps.GetNumericArgument(ref TrustPhasesUpto);
+ }
+ return true;
+
+ case "trustPhasesDownto":
+ if (ps.ConfirmArgumentCount(1))
+ {
+ ps.GetNumericArgument(ref TrustPhasesDownto);
+ }
+ return true;
+
case "proverLog":
if (ps.ConfirmArgumentCount(1)) {
SimplifyLogFilePath = args[ps.i];
@@ -1105,6 +1129,12 @@ namespace Microsoft.Boogie { }
}
return true;
+ case "printFixedPoint":
+ if (ps.ConfirmArgumentCount(1))
+ {
+ PrintFixedPoint = args[ps.i];
+ }
+ return true;
case "siVerbose":
if (ps.ConfirmArgumentCount(1)) {
StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));
@@ -1371,7 +1401,10 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
- ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)
+ ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||
+ ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
+ ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
+ ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index bdfefb04..e14d4fd3 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -38,7 +38,7 @@ namespace Microsoft.Boogie { }
}
- public class ModSetCollector : StandardVisitor {
+ public class ModSetCollector : ReadOnlyVisitor {
static Procedure enclosingProc;
static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;
static HashSet<Procedure> yieldingProcs;
@@ -264,7 +264,7 @@ namespace Microsoft.Boogie { }
}
- public class VariableCollector : StandardVisitor {
+ public class VariableCollector : ReadOnlyVisitor {
public HashSet<Variable/*!*/>/*!*/ usedVars;
public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;
[ContractInvariantMethod]
@@ -303,7 +303,7 @@ namespace Microsoft.Boogie { }
}
- public class BlockCoalescer : StandardVisitor {
+ public class BlockCoalescer : ReadOnlyVisitor {
public static void CoalesceBlocks(Program program) {
Contract.Requires(program != null);
BlockCoalescer blockCoalescer = new BlockCoalescer();
@@ -1642,7 +1642,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; }
}
- public class TokenEliminator : StandardVisitor
+ public class TokenEliminator : ReadOnlyVisitor
{
public int TokenCount = 0;
public override Expr VisitExpr(Expr node)
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 650bb146..70018a1a 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -71,6 +71,14 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Block>() != null);
return base.VisitBlock((Block)node.Clone());
}
+ public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {
+ Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
+ return base.VisitBvConcatExpr((BvConcatExpr) node.Clone());
+ }
+ public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {
+ Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
+ return base.VisitBvExtractExpr((BvExtractExpr) node.Clone());
+ }
public override Expr VisitCodeExpr(CodeExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
@@ -266,14 +274,13 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Expr>() != null);
return base.VisitOldExpr((OldExpr)node.Clone());
}
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- ParCallCmd clone = (ParCallCmd)node.Clone();
- Contract.Assert(clone != null);
- clone.CallCmds = new List<CallCmd>(node.CallCmds);
- return base.VisitParCallCmd(clone);
+ public override Cmd VisitParCallCmd(ParCallCmd node) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ ParCallCmd clone = (ParCallCmd)node.Clone();
+ Contract.Assert(clone != null);
+ clone.CallCmds = new List<CallCmd>(node.CallCmds);
+ return base.VisitParCallCmd(clone);
}
public override Procedure VisitProcedure(Procedure node) {
//Contract.Requires(node != null);
@@ -285,6 +292,20 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Program>() != null);
return base.VisitProgram((Program)node.Clone());
}
+ public override QKeyValue VisitQKeyValue(QKeyValue node) {
+ //Contract.Requires(node != null);
+ var newParams = new List<object>();
+ foreach (var o in node.Params) {
+ var e = o as Expr;
+ if (e == null) {
+ newParams.Add(o);
+ } else {
+ newParams.Add((Expr)this.Visit(e));
+ }
+ }
+ QKeyValue next = node.Next == null ? null : (QKeyValue)this.Visit(node.Next);
+ return new QKeyValue(node.tok, node.Key, newParams, next);
+ }
public override BinderExpr VisitBinderExpr(BinderExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BinderExpr>() != null);
@@ -411,14 +432,16 @@ namespace Microsoft.Boogie { }
}
+ // ----------------------------- Substitutions for Expr -------------------------------
+
/// <summary>
/// Apply a substitution to an expression. Any variables not in domain(subst)
- /// is not changed. The substitutions applies within the "old", but the "old"
+ /// is not changed. The substitutions apply within the "old", but the "old"
/// expression remains.
/// </summary>
public static Expr Apply(Substitution subst, Expr expr) {
- Contract.Requires(expr != null);
Contract.Requires(subst != null);
+ Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<Expr>() != null);
return (Expr)new NormalSubstituter(subst).Visit(expr);
}
@@ -430,23 +453,39 @@ namespace Microsoft.Boogie { /// variables in domain(forOld), apply map "always" to variables in
/// domain(always)-domain(forOld), and leave variable unchanged otherwise.
/// </summary>
- public static Expr Apply(Substitution always, Substitution forold, Expr expr)
- {
- Contract.Requires(expr != null);
- Contract.Requires(always != null);
- Contract.Requires(forold != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- return (Expr)new NormalSubstituter(always, forold).Visit(expr);
+ public static Expr Apply(Substitution always, Substitution forold, Expr expr) {
+ Contract.Requires(always != null);
+ Contract.Requires(forold != null);
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return (Expr)new NormalSubstituter(always, forold).Visit(expr);
}
/// <summary>
+ /// Apply a substitution to an expression replacing "old" expressions.
+ /// Outside "old" expressions, the substitution "always" is applied; any variable not in
+ /// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to
+ /// variables in domain(forOld), apply map "always" to variables in
+ /// domain(always)-domain(forOld), and leave variable unchanged otherwise.
+ /// </summary>
+ public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forOld, Expr expr) {
+ Contract.Requires(always != null);
+ Contract.Requires(forOld != null);
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return (Expr)new ReplacingOldSubstituter(always, forOld).Visit(expr);
+ }
+
+ // ----------------------------- Substitutions for Cmd -------------------------------
+
+ /// <summary>
/// Apply a substitution to a command. Any variables not in domain(subst)
- /// is not changed. The substitutions applies within the "old", but the "old"
+ /// is not changed. The substitutions apply within the "old", but the "old"
/// expression remains.
/// </summary>
public static Cmd Apply(Substitution subst, Cmd cmd) {
- Contract.Requires(cmd != null);
Contract.Requires(subst != null);
+ Contract.Requires(cmd != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
return (Cmd)new NormalSubstituter(subst).Visit(cmd);
}
@@ -458,46 +497,64 @@ namespace Microsoft.Boogie { /// variables in domain(forOld), apply map "always" to variables in
/// domain(always)-domain(forOld), and leave variable unchanged otherwise.
/// </summary>
- public static Cmd Apply(Substitution always, Substitution forold, Cmd cmd)
+ public static Cmd Apply(Substitution always, Substitution forOld, Cmd cmd)
{
- Contract.Requires(cmd != null);
Contract.Requires(always != null);
- Contract.Requires(forold != null);
+ Contract.Requires(forOld != null);
+ Contract.Requires(cmd != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
- return (Cmd)new NormalSubstituter(always, forold).Visit(cmd);
+ return (Cmd)new NormalSubstituter(always, forOld).Visit(cmd);
}
/// <summary>
- /// Apply a substitution to an expression replacing "old" expressions.
+ /// Apply a substitution to a command replacing "old" expressions.
/// Outside "old" expressions, the substitution "always" is applied; any variable not in
/// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to
/// variables in domain(forOld), apply map "always" to variables in
/// domain(always)-domain(forOld), and leave variable unchanged otherwise.
/// </summary>
- public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forold, Expr expr) {
- Contract.Requires(expr != null);
- Contract.Requires(forold != null);
+ public static Cmd ApplyReplacingOldExprs(Substitution always, Substitution forOld, Cmd cmd) {
Contract.Requires(always != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- return (Expr)new ReplacingOldSubstituter(always, forold).Visit(expr);
+ Contract.Requires(forOld != null);
+ Contract.Requires(cmd != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ return (Cmd)new ReplacingOldSubstituter(always, forOld).Visit(cmd);
}
+ // ----------------------------- Substitutions for QKeyValue -------------------------------
+
/// <summary>
- /// Apply a substitution to a command replacing "old" expressions.
- /// Outside "old" expressions, the substitution "always" is applied; any variable not in
- /// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to
- /// variables in domain(oldExpr), apply map "always" to variables in
- /// domain(always)-domain(oldExpr), and leave variable unchanged otherwise.
+ /// Apply a substitution to a list of attributes. Any variables not in domain(subst)
+ /// is not changed. The substitutions apply within the "old", but the "old"
+ /// expression remains.
+ /// </summary>
+ public static QKeyValue Apply(Substitution subst, QKeyValue kv) {
+ Contract.Requires(subst != null);
+ if (kv == null) {
+ return null;
+ } else {
+ return (QKeyValue)new NormalSubstituter(subst).Visit(kv);
+ }
+ }
+
+ /// <summary>
+ /// Apply a substitution to a list of attributes replacing "old" expressions.
+ /// For a further description, see "ApplyReplacingOldExprs" above for Expr.
/// </summary>
- public static Cmd ApplyReplacingOldExprs(Substitution always, Substitution forold, Cmd cmd) {
- Contract.Requires(cmd != null);
- Contract.Requires(forold != null);
+ public static QKeyValue ApplyReplacingOldExprs(Substitution always, Substitution forOld, QKeyValue kv) {
Contract.Requires(always != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- return (Cmd)new ReplacingOldSubstituter(always, forold).Visit(cmd);
+ Contract.Requires(forOld != null);
+ if (kv == null) {
+ return null;
+ } else {
+ return (QKeyValue)new ReplacingOldSubstituter(always, forOld).Visit(kv);
+ }
}
- private sealed class NormalSubstituter : Duplicator {
+ // ------------------------------------------------------------
+
+ private sealed class NormalSubstituter : Duplicator
+ {
private readonly Substitution/*!*/ always;
private readonly Substitution/*!*/ forold;
[ContractInvariantMethod]
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 9b8a09c1..51c9ee23 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -11,7 +11,7 @@ namespace Microsoft.Boogie { using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
- using Set = GSet<object>;
+ using Set = GSet<object>; // for the purposes here, "object" really means "either Variable or TypeVariable"
public static class LambdaHelper {
public static Absy Desugar(Absy node, out List<Expr/*!*/>/*!*/ axioms, out List<Function/*!*/>/*!*/ functions) {
@@ -62,117 +62,171 @@ namespace Microsoft.Boogie { static int lambdaid = 0;
- public override Program VisitProgram(Program prog) {
- //Contract.Requires(prog != null);
- Contract.Ensures(Contract.Result<Program>() != null);
- foreach (Declaration/*!*/ decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- if (decl is Axiom || decl is Function) {
- this.Visit(decl);
- }
+ public override Expr VisitLambdaExpr(LambdaExpr lambda) {
+ var baseResult = base.VisitLambdaExpr(lambda);
+ lambda = baseResult as LambdaExpr;
+ if (lambda == null) {
+ return baseResult; // apparently, the base visitor already turned the lambda into something else
}
- return prog;
- }
-
- public override Procedure VisitProcedure(Procedure node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Procedure>() != null);
- // do not visit requires/ensures when calling this on Implementation
- return node;
- }
+ // We start by getting rid of any use of "old" inside the lambda. This is done as follows.
+ // For each variable "g" occurring inside lambda as "old(... g ...)", create a new name "og".
+ // Replace each old occurrence of "g" with "og", removing the enclosing "old" wrappers.
+ var oldFinder = new OldFinder();
+ oldFinder.Visit(lambda);
+ var oldSubst = new Dictionary<Variable, Expr>(); // g -> g0
+ var callOldMapping = new Dictionary<Variable, Expr>(); // g0 -> old(g)
+ foreach (var v in oldFinder.FreeOldVars) {
+ var g = v as GlobalVariable;
+ if (g != null) {
+ var g0 = new GlobalVariable(g.tok, new TypedIdent(g.tok, g.TypedIdent.Name + "@old", g.TypedIdent.Type));
+ oldSubst.Add(g, new IdentifierExpr(g0.tok, g0));
+ callOldMapping.Add(g0, new OldExpr(g0.tok, new IdentifierExpr(g.tok, g)));
+ }
+ }
+ var lambdaBody = Substituter.ApplyReplacingOldExprs(
+ Substituter.SubstitutionFromHashtable(new Dictionary<Variable,Expr>()),
+ Substituter.SubstitutionFromHashtable(oldSubst),
+ lambda.Body);
+ var lambdaAttrs = Substituter.ApplyReplacingOldExprs(
+ Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>()),
+ Substituter.SubstitutionFromHashtable(oldSubst),
+ lambda.Attributes);
+
+ if (CommandLineOptions.Clo.VerifySnapshots && QKeyValue.FindStringAttribute(lambdaAttrs, "checksum") == null)
+ {
+ // Attach a dummy checksum to avoid issues in the dependency analysis.
+ var checksumAttr = new QKeyValue(lambda.tok, "checksum", new List<object> { "dummy" }, null);
+ if (lambdaAttrs == null)
+ {
+ lambdaAttrs = checksumAttr;
+ }
+ else
+ {
+ lambdaAttrs.AddLast(checksumAttr);
+ }
+ }
- public override Absy Visit(Absy node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- node = base.Visit(node);
-
- LambdaExpr lambda = node as LambdaExpr;
- if (lambda != null) {
- IToken/*!*/ tok = lambda.tok;
- Contract.Assert(tok != null);
-
- Set freeVars = new Set();
- lambda.ComputeFreeVariables(freeVars);
- // this is ugly, the output will depend on hashing order
- Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
- List<Variable> formals = new List<Variable>();
- List<Expr> callArgs = new List<Expr>();
- List<Expr> axCallArgs = new List<Expr>();
- List<Variable> dummies = new List<Variable>(lambda.Dummies);
- List<TypeVariable> freeTypeVars = new List<TypeVariable>();
- List<Type/*!*/> fnTypeVarActuals = new List<Type/*!*/>();
- List<TypeVariable> freshTypeVars = new List<TypeVariable>(); // these are only used in the lambda@n function's definition
- foreach (object o in freeVars) {
- // 'o' is either a Variable or a TypeVariable. Since the lambda desugaring happens only
- // at the outermost level of a program (where there are no mutable variables) and, for
- // procedure bodies, after the statements have been passified (when mutable variables have
- // been replaced by immutable incarnations), we are interested only in BoundVar's and
- // TypeVariable's.
- BoundVariable v = o as BoundVariable;
- if (v != null) {
- TypedIdent ti = new TypedIdent(v.TypedIdent.tok, v.TypedIdent.Name, v.TypedIdent.Type);
- Formal f = new Formal(v.tok, ti, true);
- formals.Add(f);
- BoundVariable b = new BoundVariable(v.tok, ti);
- dummies.Add(b);
+ // this is ugly, the output will depend on hashing order
+ var subst = new Dictionary<Variable, Expr>();
+ var substFnAttrs = new Dictionary<Variable, Expr>();
+ var formals = new List<Variable>();
+ var callArgs = new List<Expr>();
+ var axCallArgs = new List<Expr>();
+ var dummies = new List<Variable>(lambda.Dummies);
+ var freeTypeVars = new List<TypeVariable>();
+ var fnTypeVarActuals = new List<Type/*!*/>();
+ var freshTypeVars = new List<TypeVariable>(); // these are only used in the lambda@n function's definition
+
+ // compute the free variables of the lambda expression, but with lambdaBody instead of lambda.Body
+ Set freeVars = new Set();
+ BinderExpr.ComputeBinderFreeVariables(lambda.TypeParameters, lambda.Dummies, lambdaBody, lambdaAttrs, freeVars);
+
+ foreach (object o in freeVars) {
+ // 'o' is either a Variable or a TypeVariable.
+ if (o is Variable) {
+ var v = o as Variable;
+ var ti = new TypedIdent(v.TypedIdent.tok, v.TypedIdent.Name, v.TypedIdent.Type);
+ var f = new Formal(v.tok, ti, true);
+ formals.Add(f);
+ substFnAttrs.Add(v, new IdentifierExpr(f.tok, f));
+ var b = new BoundVariable(v.tok, ti);
+ dummies.Add(b);
+ if (callOldMapping.ContainsKey(v)) {
+ callArgs.Add(callOldMapping[v]);
+ } else {
callArgs.Add(new IdentifierExpr(v.tok, v));
- Expr/*!*/ id = new IdentifierExpr(f.tok, b);
- Contract.Assert(id != null);
- subst.Add(v, id);
- axCallArgs.Add(id);
- } else if (o is TypeVariable) {
- TypeVariable tv = (TypeVariable)o;
- freeTypeVars.Add(tv);
- fnTypeVarActuals.Add(tv);
- freshTypeVars.Add(new TypeVariable(tv.tok, tv.Name));
}
+ Expr id = new IdentifierExpr(b.tok, b);
+ subst.Add(v, id);
+ axCallArgs.Add(id);
+ } else {
+ var tv = (TypeVariable)o;
+ freeTypeVars.Add(tv);
+ fnTypeVarActuals.Add(tv);
+ freshTypeVars.Add(new TypeVariable(tv.tok, tv.Name));
}
+ }
- 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", lambda.Attributes);
- lambdaFunctions.Add(fn);
-
- FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
- fcall.Func = fn; // resolve here
-
- 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 = lambda.Body.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), lambda.Body);
- 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, lambda.Attributes, trig, body));
+ 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);
- NAryExpr call = new NAryExpr(tok, fcall, callArgs);
- call.Type = res.TypedIdent.Type;
- call.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
+ FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
+ fcall.Func = fn; // resolve here
- return call;
+ 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 });
+ 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;
+ call.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
+
+ return call;
+ }
+ public override Cmd VisitCallCmd(CallCmd node) {
+ var baseResult = base.VisitCallCmd(node);
+ node = baseResult as CallCmd;
+ if (node == null) {
+ return baseResult; // apparently, the base visitor already turned the lambda into something else
+ }
+ // also visit the desugaring (which the StandardVisitor does not do)
+ node.VisitDesugaring(this);
return node;
}
}
}
+ class OldFinder : ReadOnlyVisitor
+ {
+ public readonly GSet<Variable> FreeOldVars = new GSet<Variable>();
+ public override Expr VisitOldExpr(OldExpr node) {
+ Set freeVars = new Set();
+ node.Expr.ComputeFreeVariables(freeVars);
+ foreach (var v in freeVars) {
+ // Note, "v" is either a Variable or a TypeVariable
+ if (v is Variable) {
+ FreeOldVars.Add((Variable)v);
+ }
+ }
+ return node; // don't visit subexpressions, since ComputeFreeVariables has already gone through those
+ }
+ public override BinderExpr VisitBinderExpr(BinderExpr node) {
+ base.VisitBinderExpr(node);
+ // visit attributes, even though StandardVisitor does not do that (but maybe it should?)
+ if (node.Attributes != null) {
+ this.Visit(node.Attributes);
+ }
+ return node;
+ }
+ }
+
} // end namespace
\ No newline at end of file diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 4605019f..d4be8ed4 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -51,7 +51,7 @@ namespace Microsoft.Boogie { }
/// <summary>
- /// Walks an IR, mutating it into a new form
+ /// Walks an IR, mutating it into a new form. (For a subclass that does not mutate the IR, see ReadOnlyVisitor.)
/// </summary>
public abstract class StandardVisitor : Visitor {
public Visitor callingVisitor;
@@ -62,8 +62,6 @@ namespace Microsoft.Boogie { this.callingVisitor = callingVisitor;
}
public override Absy Visit(Absy node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
return node.StdDispatch(this);
}
public virtual Cmd VisitAssertCmd(AssertCmd node) {
@@ -150,8 +148,8 @@ namespace Microsoft.Boogie { return blockSeq;
}
public virtual List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {
- Contract.Requires(cce.NonNullElements(blocks));
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+ Contract.Requires(blocks != null);
+ Contract.Ensures(Contract.Result<List<Block>>() != null);
for (int i = 0, n = blocks.Count; i < n; i++) {
blocks[i] = this.VisitBlock(blocks[i]);
}
@@ -227,8 +225,8 @@ namespace Microsoft.Boogie { return node;
}
public virtual List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {
- Contract.Requires(cce.NonNullElements(declarationList));
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));
+ Contract.Requires(declarationList != null);
+ Contract.Ensures(Contract.Result<List<Declaration>>() != null);
for (int i = 0, n = declarationList.Count; i < n; i++)
declarationList[i] = cce.NonNull((Declaration/*!*/)this.Visit(declarationList[i]));
return declarationList;
@@ -297,9 +295,9 @@ namespace Microsoft.Boogie { node = (ForallExpr)this.VisitQuantifierExpr(node);
return node;
}
- public virtual LambdaExpr VisitLambdaExpr(LambdaExpr node) {
+ public virtual Expr VisitLambdaExpr(LambdaExpr node) {
Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<LambdaExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node = (LambdaExpr)this.VisitBinderExpr(node);
return node;
}
@@ -434,6 +432,20 @@ namespace Microsoft.Boogie { node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
return node;
}
+ public virtual QKeyValue VisitQKeyValue(QKeyValue node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<QKeyValue>() != null);
+ for (int i = 0, n = node.Params.Count; i < n; i++) {
+ var e = node.Params[i] as Expr;
+ if (e != null) {
+ node.Params[i] = (Expr)this.Visit(e);
+ }
+ }
+ if (node.Next != null) {
+ node.Next = (QKeyValue)this.Visit(node.Next);
+ }
+ return node;
+ }
public virtual BinderExpr VisitBinderExpr(BinderExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BinderExpr>() != null);
@@ -603,4 +615,543 @@ namespace Microsoft.Boogie { return node;
}
}
+
+ /// <summary>
+ /// A ReadOnlyVisitor visits all the nodes of a given Absy. The visitor may collect information from
+ /// the nodes, may change fields contained in the data structure, but may not replace any nodes in the
+ /// data structure. To enforce this, all Visit...(node) methods have a postcondition that says that
+ /// the return value is equal to the given "node".
+ /// </summary>
+ public abstract class ReadOnlyVisitor : StandardVisitor
+ {
+ public ReadOnlyVisitor()
+ {
+ }
+ public ReadOnlyVisitor(Visitor callingVisitor)
+ {
+ this.callingVisitor = callingVisitor;
+ }
+ public override Absy Visit(Absy node)
+ {
+ Contract.Ensures(Contract.Result<Absy>() == node);
+ return node.StdDispatch(this);
+ }
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Cmd VisitAssignCmd(AssignCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.Lhss.Count; ++i)
+ {
+ this.Visit(node.Lhss[i]);
+ this.Visit(node.Rhss[i]);
+ }
+ return node;
+ }
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override AtomicRE VisitAtomicRE(AtomicRE node)
+ {
+ Contract.Ensures(Contract.Result<AtomicRE>() == node);
+ this.VisitBlock(node.b);
+ return node;
+ }
+ public override Axiom VisitAxiom(Axiom node)
+ {
+ Contract.Ensures(Contract.Result<Axiom>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Type VisitBasicType(BasicType node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)
+ {
+ Contract.Ensures(Contract.Result<BvConcatExpr>() == node);
+ this.VisitExpr(node.E0);
+ this.VisitExpr(node.E1);
+ return node;
+ }
+ public override Type VisitBvType(BvType node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Type VisitBvTypeProxy(BvTypeProxy node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+ public override Block VisitBlock(Block node)
+ {
+ Contract.Ensures(Contract.Result<Block>() == node);
+ this.VisitCmdSeq(node.Cmds);
+ this.Visit(cce.NonNull(node.TransferCmd));
+ return node;
+ }
+ public override Expr VisitCodeExpr(CodeExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ return node;
+ }
+ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Block>>() == blockSeq);
+ for (int i = 0, n = blockSeq.Count; i < n; i++)
+ this.VisitBlock(cce.NonNull(blockSeq[i]));
+ return blockSeq;
+ }
+ public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks)
+ {
+ Contract.Ensures(Contract.Result<List<Block>>() == blocks);
+ for (int i = 0, n = blocks.Count; i < n; i++)
+ {
+ this.VisitBlock(blocks[i]);
+ }
+ return blocks;
+ }
+ public override BoundVariable VisitBoundVariable(BoundVariable node)
+ {
+ Contract.Ensures(Contract.Result<BoundVariable>() == node);
+ return (BoundVariable)this.VisitVariable(node);
+ }
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.Ins.Count; ++i)
+ if (node.Ins[i] != null)
+ this.VisitExpr(node.Ins[i]);
+ for (int i = 0; i < node.Outs.Count; ++i)
+ if (node.Outs[i] != null)
+ this.VisitIdentifierExpr(node.Outs[i]);
+ return node;
+ }
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.CallCmds.Count; i++)
+ {
+ if (node.CallCmds[i] != null)
+ this.VisitCallCmd(node.CallCmds[i]);
+ }
+ return node;
+ }
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Cmd>>() == cmdSeq);
+ for (int i = 0, n = cmdSeq.Count; i < n; i++)
+ this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor
+ return cmdSeq;
+ }
+ public override Choice VisitChoice(Choice node)
+ {
+ Contract.Ensures(Contract.Result<Choice>() == node);
+ this.VisitRESeq(node.rs);
+ return node;
+ }
+ public override Cmd VisitCommentCmd(CommentCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ return node;
+ }
+ public override Constant VisitConstant(Constant node)
+ {
+ Contract.Ensures(Contract.Result<Constant>() == node);
+ return node;
+ }
+ public override CtorType VisitCtorType(CtorType node)
+ {
+ Contract.Ensures(Contract.Result<CtorType>() == node);
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ this.Visit(node.Arguments[i]);
+ return node;
+ }
+ public override Declaration VisitDeclaration(Declaration node)
+ {
+ Contract.Ensures(Contract.Result<Declaration>() == node);
+ return node;
+ }
+ public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList)
+ {
+ Contract.Ensures(Contract.Result<List<Declaration>>() == declarationList);
+ for (int i = 0, n = declarationList.Count; i < n; i++)
+ this.Visit(declarationList[i]);
+ return declarationList;
+ }
+ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)
+ {
+ Contract.Ensures(Contract.Result<DeclWithFormals>() == node);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitVariableSeq(node.OutParams);
+ return node;
+ }
+ public override ExistsExpr VisitExistsExpr(ExistsExpr node)
+ {
+ Contract.Ensures(Contract.Result<ExistsExpr>() == node);
+ return (ExistsExpr)this.VisitQuantifierExpr(node);
+ }
+ public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node)
+ {
+ Contract.Ensures(Contract.Result<BvExtractExpr>() == node);
+ this.VisitExpr(node.Bitvector);
+ return node;
+ }
+ public override Expr VisitExpr(Expr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ return (Expr)this.Visit(node);
+ }
+ public override List<Expr> VisitExprSeq(List<Expr> exprSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Expr>>() == exprSeq);
+ for (int i = 0, n = exprSeq.Count; i < n; i++)
+ this.VisitExpr(cce.NonNull(exprSeq[i]));
+ return exprSeq;
+ }
+ public override Requires VisitRequires(Requires requires)
+ {
+ Contract.Ensures(Contract.Result<Requires>() == requires);
+ this.VisitExpr(requires.Condition);
+ return requires;
+ }
+ public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Requires>>() == requiresSeq);
+ for (int i = 0, n = requiresSeq.Count; i < n; i++)
+ this.VisitRequires(requiresSeq[i]);
+ return requiresSeq;
+ }
+ public override Ensures VisitEnsures(Ensures ensures)
+ {
+ Contract.Ensures(Contract.Result<Ensures>() == ensures);
+ this.VisitExpr(ensures.Condition);
+ return ensures;
+ }
+ public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Ensures>>() == ensuresSeq);
+ for (int i = 0, n = ensuresSeq.Count; i < n; i++)
+ this.VisitEnsures(ensuresSeq[i]);
+ return ensuresSeq;
+ }
+ public override ForallExpr VisitForallExpr(ForallExpr node)
+ {
+ Contract.Ensures(Contract.Result<ForallExpr>() == node);
+ return (ForallExpr)this.VisitQuantifierExpr(node);
+ }
+ public override Expr VisitLambdaExpr(LambdaExpr node) {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ return this.VisitBinderExpr(node);
+ }
+ public override Formal VisitFormal(Formal node)
+ {
+ Contract.Ensures(Contract.Result<Formal>() == node);
+ return node;
+ }
+ public override Function VisitFunction(Function node)
+ {
+ Contract.Ensures(Contract.Result<Function>() == node);
+ node = (Function)this.VisitDeclWithFormals(node);
+ if (node.Body != null)
+ this.VisitExpr(node.Body);
+ return node;
+ }
+ public override GlobalVariable VisitGlobalVariable(GlobalVariable node)
+ {
+ Contract.Ensures(Contract.Result<GlobalVariable>() == node);
+ return (GlobalVariable)this.VisitVariable(node);
+ }
+ public override GotoCmd VisitGotoCmd(GotoCmd node)
+ {
+ Contract.Ensures(Contract.Result<GotoCmd>() == node);
+ // do not visit the labelTargets, or control-flow loops will lead to a looping visitor
+ return node;
+ }
+ public override Cmd VisitHavocCmd(HavocCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitIdentifierExprSeq(node.Vars);
+ return node;
+ }
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ if (node.Decl != null)
+ this.VisitVariable(node.Decl);
+ return node;
+ }
+ public override List<IdentifierExpr> VisitIdentifierExprSeq(List<IdentifierExpr> identifierExprSeq)
+ {
+ Contract.Ensures(Contract.Result<List<IdentifierExpr>>() == identifierExprSeq);
+ for (int i = 0, n = identifierExprSeq.Count; i < n; i++)
+ this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));
+ return identifierExprSeq;
+ }
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ Contract.Ensures(Contract.Result<Implementation>() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ this.VisitProcedure(cce.NonNull(node.Proc));
+ return (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
+ }
+ public override LiteralExpr VisitLiteralExpr(LiteralExpr node)
+ {
+ Contract.Ensures(Contract.Result<LiteralExpr>() == node);
+ return node;
+ }
+
+ public override LocalVariable VisitLocalVariable(LocalVariable node)
+ {
+ Contract.Ensures(Contract.Result<LocalVariable>() == node);
+ return node;
+ }
+
+ public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result<AssignLhs>() == node);
+ this.Visit(node.Map);
+ for (int i = 0; i < node.Indexes.Count; ++i)
+ this.Visit(node.Indexes[i]);
+ return node;
+ }
+ public override MapType VisitMapType(MapType node)
+ {
+ Contract.Ensures(Contract.Result<MapType>() == node);
+ // not doing anything about the bound variables ... maybe
+ // these should be visited as well ...
+ //
+ // NOTE: when overriding this method, you have to make sure that
+ // the bound variables of the map type are updated correctly
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ this.Visit(node.Arguments[i]);
+ this.Visit(node.Result);
+ return node;
+ }
+ public override Type VisitMapTypeProxy(MapTypeProxy node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ this.VisitExprSeq(node.Args);
+ return node;
+ }
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ Contract.Ensures(Contract.Result<Procedure>() == node);
+ this.VisitEnsuresSeq(node.Ensures);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitIdentifierExprSeq(node.Modifies);
+ this.VisitVariableSeq(node.OutParams);
+ this.VisitRequiresSeq(node.Requires);
+ return node;
+ }
+ public override Program VisitProgram(Program node)
+ {
+ Contract.Ensures(Contract.Result<Program>() == node);
+ this.VisitDeclarationList(node.TopLevelDeclarations);
+ return node;
+ }
+ public override QKeyValue VisitQKeyValue(QKeyValue node) {
+ Contract.Ensures(Contract.Result<QKeyValue>() == node);
+ for (int i = 0, n = node.Params.Count; i < n; i++) {
+ var e = node.Params[i] as Expr;
+ if (e != null) {
+ this.Visit(e);
+ }
+ }
+ if (node.Next != null) {
+ this.Visit(node.Next);
+ }
+ return node;
+ }
+ public override BinderExpr VisitBinderExpr(BinderExpr node)
+ {
+ Contract.Ensures(Contract.Result<BinderExpr>() == node);
+ this.VisitExpr(node.Body);
+ this.VisitVariableSeq(node.Dummies);
+ // this.VisitType(node.Type);
+ return node;
+ }
+ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<QuantifierExpr>() == node);
+ this.VisitBinderExpr(node);
+ if (node.Triggers != null)
+ {
+ this.VisitTrigger(node.Triggers);
+ }
+ return node;
+ }
+ public override Cmd VisitRE(RE node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ return (Cmd)this.Visit(node); // Call general visit so subtypes get visited by their particular visitor
+ }
+ public override List<RE> VisitRESeq(List<RE> reSeq)
+ {
+ Contract.Ensures(Contract.Result<List<RE>>() == reSeq);
+ for (int i = 0, n = reSeq.Count; i < n; i++)
+ this.VisitRE(cce.NonNull(reSeq[i]));
+ return reSeq;
+ }
+ public override ReturnCmd VisitReturnCmd(ReturnCmd node)
+ {
+ Contract.Ensures(Contract.Result<ReturnCmd>() == node);
+ return (ReturnCmd)this.VisitTransferCmd(node);
+ }
+ public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node)
+ {
+ Contract.Ensures(Contract.Result<ReturnExprCmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Sequential VisitSequential(Sequential node)
+ {
+ Contract.Ensures(Contract.Result<Sequential>() == node);
+ this.VisitRE(node.first);
+ this.VisitRE(node.second);
+ return node;
+ }
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result<AssignLhs>() == node);
+ this.VisitIdentifierExpr(node.AssignedVariable);
+ return node;
+ }
+ public override Cmd VisitStateCmd(StateCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitVariableSeq(node.Locals);
+ this.VisitCmdSeq(node.Cmds);
+ return node;
+ }
+ public override TransferCmd VisitTransferCmd(TransferCmd node)
+ {
+ Contract.Ensures(Contract.Result<TransferCmd>() == node);
+ return node;
+ }
+ public override Trigger VisitTrigger(Trigger node)
+ {
+ Contract.Ensures(Contract.Result<Trigger>() == node);
+ Trigger origNext = node.Next;
+ if (origNext != null)
+ {
+ this.VisitTrigger(origNext);
+ }
+ this.VisitExprSeq(node.Tr);
+ return node;
+ }
+ // called by default for all nullary type constructors and type variables
+ public override Type VisitType(Type node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return node;
+ }
+ public override TypedIdent VisitTypedIdent(TypedIdent node)
+ {
+ Contract.Ensures(Contract.Result<TypedIdent>() == node);
+ this.Visit(node.Type);
+ return node;
+ }
+ public override Declaration VisitTypeCtorDecl(TypeCtorDecl node)
+ {
+ Contract.Ensures(Contract.Result<Declaration>() == node);
+ return this.VisitDeclaration(node);
+ }
+ public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ this.Visit(node.Arguments[i]);
+ return node;
+ }
+ public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node)
+ {
+ Contract.Ensures(Contract.Result<Declaration>() == node);
+ return this.VisitDeclaration(node);
+ }
+ public override Type VisitTypeVariable(TypeVariable node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Type VisitTypeProxy(TypeProxy node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+ public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Variable VisitVariable(Variable node)
+ {
+ Contract.Ensures(Contract.Result<Variable>() == node);
+ this.VisitTypedIdent(node.TypedIdent);
+ return node;
+ }
+ public override List<Variable> VisitVariableSeq(List<Variable> variableSeq)
+ {
+ Contract.Ensures(Contract.Result<List<Variable>>() == variableSeq);
+ for (int i = 0, n = variableSeq.Count; i < n; i++)
+ this.VisitVariable(cce.NonNull(variableSeq[i]));
+ return variableSeq;
+ }
+ public override YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ Contract.Ensures(Contract.Result<YieldCmd>() == node);
+ return node;
+ }
+ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitEnsures(node.Ensures);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitRequires(node.Requires);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ }
}
diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs index dac8ceb2..753385a1 100644 --- a/Source/Core/TypeAmbiguitySeeker.cs +++ b/Source/Core/TypeAmbiguitySeeker.cs @@ -14,7 +14,7 @@ using System.Collections.Generic; namespace Microsoft.Boogie {
- public class TypeAmbiguitySeeker : StandardVisitor {
+ public class TypeAmbiguitySeeker : ReadOnlyVisitor {
private readonly InTypeSeeker/*!*/ inTypeSeeker = new InTypeSeeker();
private readonly TypecheckingContext/*!*/ TC;
@@ -62,7 +62,7 @@ namespace Microsoft.Boogie { }
}
- internal class InTypeSeeker : StandardVisitor {
+ internal class InTypeSeeker : ReadOnlyVisitor {
internal bool FoundAmbiguity = false;
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie { private Type Instantiate(Type node, Type inst) {
Contract.Requires(inst != null);
Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Type>() != null);
+ Contract.Ensures(Contract.Result<Type>() == node);
FoundAmbiguity = true;
bool success = node.Unify(inst);
Contract.Assert(success);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 35fe4dfe..92d9f898 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -350,7 +350,7 @@ namespace Microsoft.Boogie }
- public class PolymorphismChecker : StandardVisitor
+ public class PolymorphismChecker : ReadOnlyVisitor
{
bool isMonomorphic = true;
@@ -737,7 +737,7 @@ namespace Microsoft.Boogie }
foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
{
- if (!impl.SkipVerification)
+ if (CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification)
{
Inliner.ProcessImplementation(program, impl);
}
@@ -774,6 +774,16 @@ namespace Microsoft.Boogie }
RequestIdToCancellationTokenSources[requestId] = new List<CancellationTokenSource>();
+ #region Do some pre-abstract-interpretation preprocessing on the program
+ // Doing lambda expansion before abstract interpretation means that the abstract interpreter
+ // never needs to see any lambda expressions. (On the other hand, if it were useful for it
+ // to see lambdas, then it would be better to more lambda expansion until after infererence.)
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+ #endregion
+
#region Infer invariants using Abstract Interpretation
// Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
@@ -789,7 +799,7 @@ namespace Microsoft.Boogie #endregion
- #region Do some preprocessing on the program (e.g., loop unrolling, lambda expansion)
+ #region Do some post-abstract-interpretation preprocessing on the program (e.g., loop unrolling)
if (CommandLineOptions.Clo.LoopUnrollCount != -1)
{
@@ -806,13 +816,6 @@ namespace Microsoft.Boogie {
program.Emit(new TokenTextWriter(Console.Out));
}
-
- if (CommandLineOptions.Clo.ExpandLambdas)
- {
- LambdaHelper.ExpandLambdas(program);
- //PrintBplFile ("-", program, true);
- }
-
#endregion
if (!CommandLineOptions.Clo.Verify)
@@ -851,48 +854,63 @@ namespace Microsoft.Boogie var outputCollector = new OutputCollector(stablePrioritizedImpls);
var outcome = PipelineOutcome.VerificationCompleted;
- var tasks = new Task[stablePrioritizedImpls.Length];
- for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
- {
- var taskIndex = i;
- var id = stablePrioritizedImpls[i].Id;
- CancellationTokenSource src;
- if (ImplIdToCancellationTokenSource.TryGetValue(id, out src))
- {
- src.Cancel();
- }
- src = new CancellationTokenSource();
- RequestIdToCancellationTokenSources[requestId].Add(src);
- ImplIdToCancellationTokenSource[id] = src;
- var t = Task.Factory.StartNew((dummy) =>
- {
- VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, src.Token);
- ImplIdToCancellationTokenSource.Remove(id);
- }, src.Token, TaskCreationOptions.LongRunning);
- tasks[taskIndex] = t;
- }
+
try
{
- Task.WaitAll(tasks);
- }
- catch (AggregateException ae)
- {
- ae.Handle(e =>
- {
- var pe = e as ProverException;
- if (pe != null)
+ if (CommandLineOptions.Clo.UseParallelism)
{
- printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
- outcome = PipelineOutcome.FatalError;
- return true;
+ var tasks = new Task[stablePrioritizedImpls.Length];
+ for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
+ {
+ var taskIndex = i;
+ var id = stablePrioritizedImpls[i].Id;
+ CancellationTokenSource src;
+ if (ImplIdToCancellationTokenSource.TryGetValue(id, out src))
+ {
+ src.Cancel();
+ }
+ src = new CancellationTokenSource();
+ RequestIdToCancellationTokenSources[requestId].Add(src);
+ ImplIdToCancellationTokenSource[id] = src;
+ var t = Task.Factory.StartNew((dummy) =>
+ {
+ if (src.Token.IsCancellationRequested)
+ {
+ src.Token.ThrowIfCancellationRequested();
+ }
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers);
+ ImplIdToCancellationTokenSource.Remove(id);
+ }, src.Token, TaskCreationOptions.LongRunning);
+ tasks[taskIndex] = t;
+ }
+ Task.WaitAll(tasks);
}
- var oce = e as OperationCanceledException;
- if (oce != null)
+ else
{
- return true;
+ for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
+ {
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, i, outputCollector, Checkers);
+ }
}
- return false;
- });
+ }
+ catch (AggregateException ae)
+ {
+ ae.Handle(e =>
+ {
+ var pe = e as ProverException;
+ if (pe != null)
+ {
+ printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
+ outcome = PipelineOutcome.FatalError;
+ return true;
+ }
+ var oce = e as OperationCanceledException;
+ if (oce != null)
+ {
+ return true;
+ }
+ return false;
+ });
}
finally
{
@@ -946,13 +964,8 @@ namespace Microsoft.Boogie }
- private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers, CancellationToken ct)
+ private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers)
{
- if (ct.IsCancellationRequested)
- {
- ct.ThrowIfCancellationRequested();
- }
-
Implementation impl = stablePrioritizedImpls[index];
VerificationResult verificationResult = null;
var output = new StringWriter();
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 7ccdaa19..044d84fe 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -10,7 +10,7 @@ using VC; namespace Microsoft.Boogie
{
- class DependencyCollector : StandardVisitor
+ class DependencyCollector : ReadOnlyVisitor
{
private HashSet<DeclWithFormals> dependencies;
@@ -49,7 +49,7 @@ namespace Microsoft.Boogie {
if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
{
- param.TypedIdent.WhereExpr = VisitExpr(param.TypedIdent.WhereExpr);
+ VisitExpr(param.TypedIdent.WhereExpr);
}
}
@@ -62,7 +62,7 @@ namespace Microsoft.Boogie if (node.DefinitionAxiom != null)
{
- node.DefinitionAxiom = VisitAxiom(node.DefinitionAxiom);
+ VisitAxiom(node.DefinitionAxiom);
}
return base.VisitFunction(node);
@@ -73,7 +73,7 @@ namespace Microsoft.Boogie var visited = dependencies.Contains(node.Proc);
if (!visited)
{
- node.Proc = VisitProcedure(node.Proc);
+ VisitProcedure(node.Proc);
}
return base.VisitCallCmd(node);
@@ -87,7 +87,7 @@ namespace Microsoft.Boogie var visited = dependencies.Contains(funCall.Func);
if (!visited)
{
- funCall.Func = VisitFunction(funCall.Func);
+ VisitFunction(funCall.Func);
}
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 95c29157..9f73e4a1 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -463,7 +463,7 @@ namespace Microsoft.Boogie.Houdini { }
// Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"
- class ExistentialExprModelMassage : StandardVisitor
+ class ExistentialExprModelMassage : ReadOnlyVisitor
{
List<Function> ahFuncs;
@@ -491,7 +491,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- class FunctionCollector : StandardVisitor
+ class FunctionCollector : ReadOnlyVisitor
{
public List<Tuple<Function, ExistsExpr>> functionsUsed;
ExistsExpr existentialExpr;
@@ -3683,7 +3683,7 @@ namespace Microsoft.Boogie.Houdini { }
- class GatherLiterals : StandardVisitor
+ class GatherLiterals : ReadOnlyVisitor
{
public List<Tuple<Variable, Expr>> literals;
bool inOld;
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 252321b6..6ffaef22 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -16,7 +16,7 @@ using VC; using System.Linq;
namespace Microsoft.Boogie.Houdini {
- public class ExistentialConstantCollector : StandardVisitor {
+ public class ExistentialConstantCollector : ReadOnlyVisitor {
public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out ExistentialConstantCollector collector)
{
collector = new ExistentialConstantCollector(houdini);
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index b05a2e5f..393c71eb 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -293,7 +293,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- public class InlineEnsuresVisitor : StandardVisitor {
+ public class InlineEnsuresVisitor : ReadOnlyVisitor {
public override Ensures VisitEnsures(Ensures ensures) {
ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);
return base.VisitEnsures(ensures);
@@ -448,7 +448,7 @@ namespace Microsoft.Boogie.Houdini { }
// Compute dependencies between candidates
- public class CrossDependencies : StandardVisitor
+ public class CrossDependencies : ReadOnlyVisitor
{
public CrossDependencies(HashSet<Variable> constants)
{
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index ea526591..06224d1a 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -24,7 +24,6 @@ public class SmartBlockPredicator { IdentifierExpr fp;
Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
- Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
HashSet<Block> doneBlocks = new HashSet<Block>();
bool myUseProcedurePredicates;
UniformityAnalyser uni;
@@ -79,6 +78,7 @@ public class SmartBlockPredicator { cCmd.Ins.Insert(0, p != null ? p : Expr.True);
cmdSeq.Add(cCmd);
} else if (p == null) {
+ new EnabledReplacementVisitor(Expr.True).Visit(cmd);
cmdSeq.Add(cmd);
} else if (cmd is AssignCmd) {
var aCmd = (AssignCmd)cmd;
@@ -147,10 +147,11 @@ public class SmartBlockPredicator { gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
if (gCmd.labelTargets.Count == 1) {
- if (defMap.ContainsKey(gCmd.labelTargets[0]))
+ if (defMap.ContainsKey(gCmd.labelTargets[0])) {
PredicateCmd(p, cmdSeq,
Cmd.SimpleAssign(Token.NoToken,
Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
+ }
} else {
Debug.Assert(gCmd.labelTargets.Count > 1);
Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
@@ -159,11 +160,15 @@ public class SmartBlockPredicator { if (!partInfo.ContainsKey(target))
continue;
+ // In this case we not only predicate with the current predicate p,
+ // but also with the "part predicate"; this ensures that we do not
+ // update a predicate twice when it occurs in both parts.
var part = partInfo[target];
- if (defMap.ContainsKey(part.realDest))
- PredicateCmd(p, cmdSeq,
+ if (defMap.ContainsKey(part.realDest)) {
+ PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), cmdSeq,
Cmd.SimpleAssign(Token.NoToken,
Expr.Ident(predMap[part.realDest]), part.pred));
+ }
var predsExitingLoop = new Dictionary<Block, List<Expr>>();
foreach (Block exit in LoopsExited(src, target)) {
List<Expr> predList;
@@ -174,7 +179,7 @@ public class SmartBlockPredicator { predList.Add(part.pred);
}
foreach (var pred in predsExitingLoop) {
- PredicateCmd(p, cmdSeq,
+ PredicateCmd(p == null ? part.pred : Expr.And(p, part.pred), cmdSeq,
Cmd.SimpleAssign(Token.NoToken,
Expr.Ident(predMap[pred.Key]),
Expr.Not(pred.Value.Aggregate(Expr.Or))));
@@ -202,6 +207,7 @@ public class SmartBlockPredicator { void AssignPredicates(Graph<Block> blockGraph,
DomRelation<Block> dom,
DomRelation<Block> pdom,
+ IEnumerable<Block> headerDominance,
IEnumerator<Tuple<Block, bool>> i,
Variable headPredicate,
ref int predCount) {
@@ -224,11 +230,11 @@ public class SmartBlockPredicator { return;
}
}
-
+
if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
if (blockGraph.Headers.Contains(block.Item1)) {
parentMap[block.Item1] = header;
- AssignPredicates(blockGraph, dom, pdom, i, headPredicate, ref predCount);
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, i, headPredicate, ref predCount);
}
continue;
}
@@ -238,7 +244,7 @@ public class SmartBlockPredicator { parentMap[block.Item1] = header;
var loopPred = FreshPredicate(ref predCount);
ownedPreds.Add(loopPred);
- AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, i, loopPred, ref predCount);
} else {
bool foundExisting = false;
foreach (var regionPred in regionPreds) {
@@ -253,7 +259,26 @@ public class SmartBlockPredicator { var condPred = FreshPredicate(ref predCount);
predMap[block.Item1] = condPred;
defMap[block.Item1] = condPred;
- ownedPreds.Add(condPred);
+ var headerIterator = headerDominance.GetEnumerator();
+ // Add the predicate to the loop header H that dominates the node (if one
+ // exists) such that H does not dominate another header which also dominates
+ // the node. Since predicates are owned by loop headers (or the program entry
+ // node), this is the block 'closest' to block to which we are assigning a
+ // that can be made to own the predicate.
+ Block node = null;
+ while (headerIterator.MoveNext()) {
+ var current = headerIterator.Current;
+ if (dom.DominatedBy(block.Item1, current)) {
+ node = current;
+ break;
+ }
+ }
+ if (node != null) {
+ ownedMap[node].Add(condPred);
+ } else {
+ // In this case the header is the program entry node.
+ ownedPreds.Add(condPred);
+ }
regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
}
}
@@ -266,6 +291,7 @@ public class SmartBlockPredicator { Graph<Block> dualGraph = blockGraph.Dual(new Block());
DomRelation<Block> pdom = dualGraph.DominatorMap;
+ IEnumerable<Block> headerDominance = blockGraph.SortHeadersByDominance();
var iter = sortedBlocks.GetEnumerator();
if (!iter.MoveNext()) {
@@ -279,7 +305,7 @@ public class SmartBlockPredicator { defMap = new Dictionary<Block, Variable>();
ownedMap = new Dictionary<Block, HashSet<Variable>>();
parentMap = new Dictionary<Block, Block>();
- AssignPredicates(blockGraph, dom, pdom, iter,
+ AssignPredicates(blockGraph, dom, pdom, headerDominance, iter,
myUseProcedurePredicates ? impl.InParams[0] : null,
ref predCount);
}
@@ -433,16 +459,22 @@ public class SmartBlockPredicator { prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
}
- if (parentMap.ContainsKey(block)) {
- var parent = parentMap[block];
+ Block currentBlock = block;
+ Expr pCurrentExpr = pExpr;
+ while (parentMap.ContainsKey(currentBlock)) {
+ Block parent = parentMap[currentBlock];
+ Expr pParentExpr = null;
if (predMap.ContainsKey(parent)) {
var parentPred = predMap[parent];
if (parentPred != null) {
+ pParentExpr = Expr.Ident(parentPred);
block.Cmds.Add(new AssertCmd(Token.NoToken,
- pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))
- : Expr.Ident(parentPred)));
+ pCurrentExpr != null ? (Expr)Expr.Imp(pCurrentExpr, pParentExpr)
+ : pParentExpr));
}
}
+ currentBlock = parent;
+ pCurrentExpr = pParentExpr;
}
var transferCmd = block.TransferCmd;
@@ -520,6 +552,15 @@ public class SmartBlockPredicator { }
}
}
+ } else {
+ if (impl == null) {
+ foreach (Requires r in proc.Requires) {
+ new EnabledReplacementVisitor(Expr.True).VisitExpr(r.Condition);
+ }
+ foreach (Ensures e in proc.Ensures) {
+ new EnabledReplacementVisitor(Expr.True).VisitExpr(e.Condition);
+ }
+ }
}
if (impl != null) {
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index 6119d522..a76566e4 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -396,7 +396,7 @@ namespace Microsoft.Boogie return !nonUniformBlocks[procedureName].Contains(b);
}
- class UniformExpressionAnalysisVisitor : StandardVisitor {
+ class UniformExpressionAnalysisVisitor : ReadOnlyVisitor {
private bool isUniform = true;
private Dictionary<string, bool> uniformityInfo;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 05bcdb01..4e895931 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -434,7 +434,283 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("; doing a full reset...");
}
}
+
+
+ private string StripCruft(string name){
+ if(name.Contains("@@"))
+ return name.Remove(name.LastIndexOf ("@@"));
+ return name;
+ }
+
+ private class BadExprFromProver : Exception
+ {
+ };
+
+ private delegate VCExpr ArgGetter (int pos);
+
+ private delegate VCExpr[] ArgsGetter ();
+
+ private delegate VCExprVar[] VarsGetter ();
+
+ private VCExprOp VCStringToVCOp (string op)
+ {
+ switch (op) {
+ case "+" :
+ return VCExpressionGenerator.AddIOp;
+ case "-" :
+ return VCExpressionGenerator.SubIOp;
+ case "*" :
+ return VCExpressionGenerator.MulIOp;
+ case "div" :
+ return VCExpressionGenerator.DivIOp;
+ case "=" :
+ return VCExpressionGenerator.EqOp;
+ case "<=" :
+ return VCExpressionGenerator.LeOp;
+ case "<" :
+ return VCExpressionGenerator.LtOp;
+ case ">=" :
+ return VCExpressionGenerator.GeOp;
+ case ">" :
+ return VCExpressionGenerator.GtOp;
+ case "and" :
+ return VCExpressionGenerator.AndOp;
+ case "or" :
+ return VCExpressionGenerator.OrOp;
+ case "not" :
+ return VCExpressionGenerator.NotOp;
+ case "ite" :
+ return VCExpressionGenerator.IfThenElseOp;
+ default:
+ return null;
+ }
+ }
+
+ private class MyDeclHandler : TypeDeclCollector.DeclHandler {
+ public Dictionary<string,VCExprVar> var_map = new Dictionary<string, VCExprVar>();
+ public Dictionary<string,Function> func_map = new Dictionary<string, Function>();
+ public override void VarDecl(VCExprVar v){
+ var_map[v.Name] = v;
+ }
+ public override void FuncDecl(Function f){
+ func_map[f.Name] = f;
+ }
+ public MyDeclHandler() {
+ }
+ }
+
+ private MyDeclHandler declHandler = null;
+
+ private VCExprVar SExprToVar (SExpr e)
+ {
+ if(e.Arguments.Count() != 1){
+ HandleProverError ("Prover error: bad quantifier syntax");
+ throw new BadExprFromProver ();
+ }
+ string vname = StripCruft(e.Name);
+ SExpr vtype = e[0];
+ switch(vtype.Name){
+ case "Int":
+ return gen.Variable(vname,Type.Int);
+ case "Bool":
+ return gen.Variable (vname,Type.Bool);
+ case "Array":{
+ // TODO: handle more general array types
+ var idxType = Type.Int; // well, could be something else
+ var valueType =
+ (vtype.Arguments[1].Name == "Int") ? Type.Int : Type.Bool;
+ var types = new List<Type>();
+ types.Add(idxType);
+ return gen.Variable (vname, new MapType(Token.NoToken,new List<TypeVariable>(),types,valueType));
+ }
+ default: {
+ HandleProverError ("Prover error: bad type: " + vtype.Name);
+ throw new BadExprFromProver ();
+ }
+ }
+ }
+
+ private VCExpr MakeBinary(VCExprOp op, VCExpr [] args)
+ {
+ if (args.Count() == 0)
+ {
+ // with zero args we need the identity of the op
+ if (op == VCExpressionGenerator.AndOp)
+ return VCExpressionGenerator.True;
+ if (op == VCExpressionGenerator.OrOp)
+ return VCExpressionGenerator.False;
+ if (op == VCExpressionGenerator.AddIOp)
+ {
+ Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.ZERO;
+ return gen.Integer(x);
+ }
+ HandleProverError("Prover error: bad expression ");
+ throw new BadExprFromProver();
+ }
+ var temp = args[0];
+ for (int i = 1; i < args.Count(); i++)
+ temp = gen.Function(op, temp, args[i]);
+ return temp;
+ }
+
+ private VCExpr SExprToVCExpr (SExpr e, Dictionary<string,VCExpr> bound)
+ {
+ if (e.Arguments.Count() == 0) {
+ var name = StripCruft(e.Name);
+ if (name [0] >= '0' && name [0] <= '9') {
+ Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.FromString(name);
+ return gen.Integer (x);
+ }
+ if (bound.ContainsKey (name)) {
+ return bound [name];
+ }
+ if(name == "true")
+ return VCExpressionGenerator.True;
+ if(name == "false")
+ return VCExpressionGenerator.False;
+ if(declHandler.var_map.ContainsKey(name))
+ return declHandler.var_map[name];
+ HandleProverError ("Prover error: unknown symbol:" + name);
+ throw new BadExprFromProver ();
+ }
+ ArgGetter g = i => SExprToVCExpr (e [i], bound);
+ ArgsGetter ga = () => e.Arguments.Select (x => SExprToVCExpr (x, bound)).ToArray ();
+ VarsGetter gb = () => e [0].Arguments.Select (x => SExprToVar (x)).ToArray ();
+ switch (e.Name) {
+ case "select" :
+ return gen.Select (ga ());
+ case "store" :
+ return gen.Store (ga ());
+ case "forall":
+ case "exists":
+ {
+ var binds = e.Arguments[0];
+ var vcbinds = new List<VCExprVar>();
+ for (int i = 0; i < binds.Arguments.Count(); i++)
+ {
+ var bind = binds.Arguments[i];
+ var symb = bind.Name;
+ var vcv = SExprToVar(bind);
+ vcbinds.Add(vcv);
+ bound[symb] = vcv;
+ }
+ var body = g(1);
+ if (e.Name == "forall")
+ body = gen.Forall(vcbinds, new List<VCTrigger>(), body);
+ else
+ body = gen.Exists(vcbinds, new List<VCTrigger>(), body);
+ for (int i = 0; i < binds.Arguments.Count(); i++)
+ {
+ var bind = binds.Arguments[i];
+ var symb = bind.Name;
+ bound.Remove(symb);
+ }
+ return body;
+ }
+ case "-" : // have to deal with unary case
+ {
+ if(e.ArgCount == 1){
+ var args = new VCExpr[2];
+ args[0] = gen.Integer (Microsoft.Basetypes.BigNum.ZERO);
+ args[1] = g(0);
+ return gen.Function(VCStringToVCOp("-"),args);
+ }
+ return gen.Function(VCStringToVCOp("-"),ga());
+ }
+ case "!" : // this is commentary
+ return g(0);
+ case "let" : {
+ // we expand lets exponentially since there is no let binding in Boogie surface syntax
+ bool expand_lets = true;
+ var binds = e.Arguments[0];
+ var vcbinds = new List<VCExprLetBinding>();
+ for(int i = 0; i < binds.Arguments.Count(); i++){
+ var bind = binds.Arguments[i];
+ var symb = bind.Name;
+ var def = bind.Arguments[0];
+ var vce = SExprToVCExpr(def, bound);
+ var vcv = gen.Variable(symb,vce.Type);
+ var vcb = gen.LetBinding(vcv,vce);
+ vcbinds.Add (vcb);
+ bound[symb] = expand_lets ? vce : vcv;
+ }
+ var body = g(1);
+ if(!expand_lets)
+ body = gen.Let(vcbinds,body);
+ for(int i = 0; i < binds.Arguments.Count(); i++){
+ var bind = binds.Arguments[i];
+ var symb = bind.Name;
+ bound.Remove (symb);
+ }
+ return body;
+ }
+
+ default: {
+ var op = VCStringToVCOp (e.Name);
+ if (op == null) {
+ var name = StripCruft(e.Name);
+ if(declHandler.func_map.ContainsKey(name)){
+ Function f = declHandler.func_map[name];
+ return gen.Function (f, ga());
+ }
+ HandleProverError ("Prover error: unknown operator:" + e.Name);
+ throw new BadExprFromProver ();
+ }
+ if(op.Arity == 2)
+ return MakeBinary (op, ga ());
+ return gen.Function(op, ga());
+ }
+ }
+ }
+
+ private void SExprToSoln (SExpr resp,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
+
+ foreach (var node in rpfp.nodes)
+ pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
+
+ var lines = resp.Arguments;
+
+ // get all the predicate definitions
+ for (int i = 0; i < lines.Length; i++) {
+ var line = lines [i];
+ if(line.Name != "define-fun"){
+ HandleProverError ("Prover error: expected define-fun but got:" + line.Name);
+ throw new BadExprFromProver ();
+ }
+ if(line.ArgCount != 4){
+ HandleProverError ("Prover error: define-fun has wrong number of arguments");
+ throw new BadExprFromProver ();
+ }
+ var pname = StripCruft(line.Arguments[0].Name);
+ var pvars = line.Arguments[1];
+ var pbody = line.Arguments[3]; // range has to be Bool
+ var binding = new Dictionary<string,VCExpr>();
+ var pvs = new List<VCExpr>();
+ foreach(var b in pvars.Arguments){
+ var e = SExprToVar (b);
+ pvs.Add (e);
+ binding.Add (b.Name,e);
+ }
+ VCExpr bexpr = SExprToVCExpr(pbody,binding);
+
+ var annot = rpfp.CreateRelation(pvs.ToArray(),bexpr);
+
+ if(pmap.ContainsKey(pname)){
+ var node = pmap[pname];
+ node.Annotation = annot;
+ }
+ else if(pname[0] != '@'){ // if not an internal symbol
+ HandleProverError ("Prover error: got unknown predicate:" + pname);
+ throw new BadExprFromProver ();
+ }
+ }
+
+ }
+
private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
Dictionary<int,Dictionary<string,string>> varSubst)
{
@@ -600,7 +876,7 @@ namespace Microsoft.Boogie.SMTLib return res;
#endif
}
-
+
public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler,
out RPFP.Node cex,
Dictionary<int,Dictionary<string,string>> varSubst)
@@ -610,7 +886,12 @@ namespace Microsoft.Boogie.SMTLib //Contract.Requires(handler != null);
rpfp = _rpfp;
cex = null;
-
+
+ if(CommandLineOptions.Clo.PrintFixedPoint != null){
+ declHandler = new MyDeclHandler();
+ DeclCollector.SetDeclHandler(declHandler);
+ }
+
if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
if (options.LogFilename != null && currentLogFile == null)
@@ -736,6 +1017,19 @@ namespace Microsoft.Boogie.SMTLib HandleProverError("Unexpected prover response: " + resp.ToString());
break;
}
+ case Outcome.Valid:
+ {
+ resp = Process.GetProverResponse();
+ if (resp.Name == "fixedpoint")
+ {
+ // only get the response if we need it
+ if(CommandLineOptions.Clo.PrintFixedPoint != null)
+ SExprToSoln(resp, varSubst);
+ }
+ else
+ HandleProverError("Unexpected prover response: " + resp.ToString());
+ break;
+ }
default:
break;
}
@@ -753,6 +1047,8 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(fixedpoint-pop)");
Pop();
AxiomsAreSetup = false;
+ DeclCollector.SetDeclHandler(null);
+ declHandler = null; // just so we can GC it
return result;
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 2bf8fa22..30363102 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -90,7 +90,19 @@ void ObjectInvariant() private readonly Stack<HashSet<string/*!*/>/*!*/> _KnownStoreFunctions = new Stack<HashSet<string>>();
private readonly Stack<HashSet<string/*!*/>/*!*/> _KnownSelectFunctions = new Stack<HashSet<string>>();
private readonly Stack<HashSet<string>> _KnownLBL = new Stack<HashSet<string>>();
-
+
+ // lets RPFP checker capture decls
+ public abstract class DeclHandler {
+ public abstract void VarDecl(VCExprVar v);
+ public abstract void FuncDecl(Function f);
+ }
+
+ private DeclHandler declHandler = null;
+
+ public void SetDeclHandler(DeclHandler _d){
+ declHandler = _d;
+ }
+
private void InitializeKnownDecls()
{
_KnownFunctions.Push(new HashSet<Function>());
@@ -182,6 +194,8 @@ void ObjectInvariant() if (KnownFunctions.Contains(func))
return;
KnownFunctions.Add(func);
+ if(declHandler != null)
+ declHandler.FuncDecl(func);
}
public void RegisterRelation(Function func)
@@ -242,6 +256,8 @@ void ObjectInvariant() "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
KnownVariables.Add(node);
+ if(declHandler != null)
+ declHandler.VarDecl(node);
}
return base.Visit(node, arg);
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index bd8e7c79..a9963b72 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -49,7 +49,7 @@ namespace Microsoft.Boogie.VCExprAST { public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);
- public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
+ public class Boogie2VCExprTranslator : ReadOnlyVisitor, ICloneable {
// Stack on which the various Visit-methods put the result of the translation
private readonly Stack<VCExpr/*!*/>/*!*/ SubExpressions = new Stack<VCExpr>();
[ContractInvariantMethod]
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 1286c091..deb3f2c2 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -733,6 +733,67 @@ namespace Microsoft.Boogie proc.Ensures.Add(new Ensures(true, freePostExpr));
}
}
+
+ private void FixedPointToSpecs(){
+
+ if(mode != Mode.Corral || CommandLineOptions.Clo.PrintFixedPoint == null)
+ return; // not implemented for other annotation modes yet
+
+ var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintFixedPoint);
+ Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
+
+ foreach (var node in rpfp.nodes)
+ pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
+
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ Implementation impl = decl as Implementation;
+ if (impl == null)
+ continue;
+ Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
+
+ Procedure proc = cce.NonNull(impl.Proc);
+
+ {
+ StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, boogieContext, QuantifierExpr.GetNextSkolemId());
+ implName2StratifiedInliningInfo[impl.Name] = info;
+ // We don't need controlFlowVariable for stratified Inlining
+ //impl.LocVars.Add(info.controlFlowVariable);
+ List<Expr> exprs = new List<Expr>();
+
+ {
+ // last ensures clause will be the symbolic one
+ if(info.isMain)
+ continue;
+ var ens = proc.Ensures[proc.Ensures.Count - 1];
+ if(ens.Condition == Expr.False) // this is main
+ continue;
+ var postExpr = ens.Condition as NAryExpr;
+ var args = postExpr.Args;
+ if(pmap.ContainsKey (impl.Name)){
+ RPFP.Node node = pmap[impl.Name];
+ var ind = node.Annotation.IndParams;
+ var bound = new Dictionary<VCExpr,Expr>();
+ for(int i = 0; i < args.Count; i++){
+ bound[ind[i]] = args[i];
+ }
+ var new_ens_cond = VCExprToExpr(node.Annotation.Formula,bound);
+ if (new_ens_cond != Expr.True)
+ {
+ var new_ens = new Ensures(false, new_ens_cond);
+ var enslist = new List<Ensures>();
+ enslist.Add(new_ens);
+ var new_proc = new Procedure(proc.tok, proc.Name, proc.TypeParameters, proc.InParams,
+ proc.OutParams, new List<Requires>(), new List<IdentifierExpr>(), enslist);
+ new_proc.Emit(twr, 0);
+ }
+ }
+ }
+ }
+ }
+ twr.Close ();
+ }
private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List<Term> small, Term lbl = null)
{
@@ -1545,6 +1606,7 @@ namespace Microsoft.Boogie return VC.ConditionGeneration.Outcome.Errors;
case RPFP.LBool.False:
Console.WriteLine("Procedure is correct.");
+ FixedPointToSpecs();
return Outcome.Correct;
case RPFP.LBool.Undef:
Console.WriteLine("Inconclusive result.");
@@ -2027,7 +2089,132 @@ namespace Microsoft.Boogie return m.MkElement(subst[uniqueName]);
return m.MkFunc("@undefined", 0).GetConstant();
}
-
+
+ class InternalError : Exception {
+ }
+
+
+ private BinaryOperator.Opcode VCOpToOp (VCExprOp op)
+ {
+ if (op == VCExpressionGenerator.AddIOp)
+ return BinaryOperator.Opcode.Add;
+ if (op == VCExpressionGenerator.SubIOp)
+ return BinaryOperator.Opcode.Sub;
+ if (op == VCExpressionGenerator.MulIOp)
+ return BinaryOperator.Opcode.Mul;
+ if (op == VCExpressionGenerator.DivIOp)
+ return BinaryOperator.Opcode.Div;
+ if (op == VCExpressionGenerator.EqOp)
+ return BinaryOperator.Opcode.Eq;
+ if (op == VCExpressionGenerator.LeOp)
+ return BinaryOperator.Opcode.Le;
+ if (op == VCExpressionGenerator.LtOp)
+ return BinaryOperator.Opcode.Lt;
+ if (op == VCExpressionGenerator.GeOp)
+ return BinaryOperator.Opcode.Ge;
+ if (op == VCExpressionGenerator.GtOp)
+ return BinaryOperator.Opcode.Gt;
+ if (op == VCExpressionGenerator.AndOp)
+ return BinaryOperator.Opcode.And;
+ if (op == VCExpressionGenerator.OrOp)
+ return BinaryOperator.Opcode.Or;
+ throw new InternalError();
+ }
+
+ private Expr MakeBinary (BinaryOperator.Opcode op, List<Expr> args)
+ {
+ if(args.Count == 0){
+ // with zero args we need the identity of the op
+ switch(op){
+ case BinaryOperator.Opcode.And:
+ return Expr.True;
+ case BinaryOperator.Opcode.Or:
+ return Expr.False;
+ case BinaryOperator.Opcode.Add:
+ return new LiteralExpr(Token.NoToken,Microsoft.Basetypes.BigNum.ZERO);
+ default:
+ throw new InternalError();
+ }
+ }
+ var temp = args[0];
+ for(int i = 1; i < args.Count; i++)
+ temp = Expr.Binary(Token.NoToken,op,temp,args[i]);
+ return temp;
+ }
+
+ private Variable MakeVar(VCExprVar v){
+ var foo = new TypedIdent(Token.NoToken,v.Name.ToString(),v.Type);
+ return new BoundVariable(Token.NoToken,foo);
+ }
+
+ private Expr VCExprToExpr (VCExpr e, Dictionary<VCExpr,Expr> bound)
+ {
+ if (e is VCExprVar) {
+ if(bound.ContainsKey(e))
+ return bound[e];
+ return Expr.Ident(MakeVar(e as VCExprVar)); // TODO: this isn't right
+ }
+ if (e is VCExprIntLit) {
+ var n = e as VCExprIntLit;
+ return new LiteralExpr(Token.NoToken,n.Val);
+ }
+ if (e is VCExprNAry) {
+ var f = e as VCExprNAry;
+ var args = new List<Expr>();
+ for(int i = 0; i < f.Arity; i++){
+ args.Add (VCExprToExpr (f[i],bound));
+ }
+
+ if(f.Op == VCExpressionGenerator.NotOp)
+ return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, args[0]);
+
+ if(f.Op == VCExpressionGenerator.IfThenElseOp)
+ return new NAryExpr(Token.NoToken,new IfThenElse(Token.NoToken),args);
+
+ if(f.Op is VCExprSelectOp){
+ var idx = new List<Expr>();
+ idx.Add(args[1]);
+ return Expr.Select(args[0],idx);
+ }
+
+ if(f.Op is VCExprStoreOp){
+ var idx = new List<Expr>();
+ idx.Add(args[1]);
+ return Expr.Store(args[0],idx,args[2]);
+ }
+
+ var op = VCOpToOp (f.Op);
+ return MakeBinary(op,args);
+ }
+
+ if(e is VCExprQuantifier) {
+ var f = e as VCExprQuantifier;
+ var vs = new List<Variable>();
+ var new_bound = new Dictionary<VCExpr,Expr>(bound);
+ foreach(var v in f.BoundVars){
+ var ve = MakeVar(v);
+ vs.Add(ve);
+ new_bound.Add (v,Expr.Ident (ve));
+ }
+ var bd = VCExprToExpr(f.Body,new_bound);
+ if(f.Quan == Quantifier.EX)
+ return new ExistsExpr(Token.NoToken,vs,bd);
+ else
+ return new ForallExpr(Token.NoToken,vs,bd);
+ }
+ if (e == VCExpressionGenerator.True) {
+ return Expr.True;
+ }
+ if (e == VCExpressionGenerator.False) {
+ return Expr.False;
+ }
+ if (e is VCExprLet) {
+
+ }
+
+ throw new InternalError();
+ }
+
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 49ae68e3..d2ab910b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2638,32 +2638,6 @@ namespace VC { }
#endregion Peep-hole optimizations
- if (CommandLineOptions.Clo.ExpandLambdas)
- {
- List<Expr> axioms;
- List<Function> functions;
- lock (program.TopLevelDeclarations)
- {
- LambdaHelper.Desugar(impl, out axioms, out functions);
- program.TopLevelDeclarations.AddRange(functions);
- }
-
- if (axioms.Count > 0) {
- List<Cmd> cmds = new List<Cmd>();
- foreach (Expr ax in axioms) {
- Contract.Assert(ax != null);
- cmds.Add(new AssumeCmd(ax.tok, ax));
- }
- Block entryBlock = cce.NonNull( impl.Blocks[0]);
- cmds.AddRange(entryBlock.Cmds);
- entryBlock.Cmds = cmds;
- // Make sure that all added commands are passive commands.
- Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());
- TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
- ComputeOldExpressionSubstitution(impl.Proc.Modifies));
- }
- }
-
HandleSelectiveChecking(impl);
|