diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 228 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 32 |
3 files changed, 134 insertions, 130 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 137d5776..cc51aaf9 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -23,7 +23,7 @@ using BytecodeTranslator.Phone; namespace BytecodeTranslator
{
- public class ExpressionTraverser : BaseCodeTraverser
+ public class ExpressionTraverser : CodeTraverser
{
public readonly Stack<Bpl.Expr> TranslatedExpressions;
@@ -65,7 +65,7 @@ namespace BytecodeTranslator /// </summary>
/// <param name="addressableExpression"></param>
/// <remarks>still a stub</remarks>
- public override void Visit(IAddressableExpression addressableExpression)
+ public override void TraverseChildren(IAddressableExpression addressableExpression)
{
ILocalDefinition/*?*/ local = addressableExpression.Definition as ILocalDefinition;
if (local != null)
@@ -86,7 +86,7 @@ namespace BytecodeTranslator if (instance == null) {
TranslatedExpressions.Push(f);
} else {
- this.Visit(instance);
+ this.Traverse(instance);
Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(field.ResolvedField.Type));
this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, temp.Type)));
@@ -97,18 +97,18 @@ namespace BytecodeTranslator IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;
if (arrayIndexer != null)
{
- this.Visit(arrayIndexer);
+ this.Traverse(arrayIndexer);
return;
}
IAddressDereference/*?*/ addressDereference = addressableExpression.Definition as IAddressDereference;
if (addressDereference != null)
{
- this.Visit(addressDereference);
+ this.Traverse(addressDereference);
return;
}
IBlockExpression block = addressableExpression.Definition as IBlockExpression;
if (block != null) {
- this.Visit(block);
+ this.Traverse(block);
return;
}
IMethodReference/*?*/ method = addressableExpression.Definition as IMethodReference;
@@ -121,7 +121,7 @@ namespace BytecodeTranslator Contract.Assert(addressableExpression.Definition is IThisReference);
}
- public override void Visit(IAddressDereference addressDereference)
+ public override void TraverseChildren(IAddressDereference addressDereference)
{
IBoundExpression be = addressDereference.Address as IBoundExpression;
if (be != null)
@@ -134,22 +134,22 @@ namespace BytecodeTranslator return;
}
}
- this.Visit(addressDereference.Address);
+ this.Traverse(addressDereference.Address);
return;
}
- public override void Visit(IArrayIndexer arrayIndexer) {
+ public override void TraverseChildren(IArrayIndexer arrayIndexer) {
if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {
// Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);
- this.Visit(se);
+ this.Traverse(se);
return;
}
- this.Visit(arrayIndexer.IndexedObject);
+ this.Traverse(arrayIndexer.IndexedObject);
Bpl.Expr arrayExpr = TranslatedExpressions.Pop();
- this.Visit(arrayIndexer.Indices);
+ this.Traverse(arrayIndexer.Indices);
int count = arrayIndexer.Indices.Count();
Bpl.Expr[] indexExprs = new Bpl.Expr[count];
for (int i = count; i > 0; i--) {
@@ -167,24 +167,24 @@ namespace BytecodeTranslator this.TranslatedExpressions.Push(this.sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, this.sink.CciTypeToBoogie(arrayIndexer.Type)));
}
- public override void Visit(ITargetExpression targetExpression)
+ public override void TraverseChildren(ITargetExpression targetExpression)
{
Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
}
- public override void Visit(IThisReference thisReference)
+ public override void TraverseChildren(IThisReference thisReference)
{
TranslatedExpressions.Push(new Bpl.IdentifierExpr(thisReference.Token(),
this.sink.ThisVariable));
}
- public override void Visit(IBoundExpression boundExpression)
+ public override void TraverseChildren(IBoundExpression boundExpression)
{
if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {
// Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);
- this.Visit(se);
+ this.Traverse(se);
return;
}
@@ -214,7 +214,7 @@ namespace BytecodeTranslator if (instance == null) {
TranslatedExpressions.Push(f);
} else {
- this.Visit(instance);
+ this.Traverse(instance);
Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
var bplType = this.sink.CciTypeToBoogie(field.Type);
var e = this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, bplType);
@@ -228,7 +228,7 @@ namespace BytecodeTranslator IArrayIndexer/*?*/ indexer = boundExpression.Definition as IArrayIndexer;
if (indexer != null)
{
- Visit(indexer);
+ this.Traverse(indexer);
return;
}
#endregion
@@ -240,18 +240,18 @@ namespace BytecodeTranslator IAddressOf/*?*/ addressOf = deref.Address as IAddressOf;
if (addressOf != null)
{
- this.Visit(addressOf.Expression);
+ this.Traverse(addressOf.Expression);
return;
}
if (boundExpression.Instance != null)
{
// TODO
- this.Visit(boundExpression.Instance);
+ this.Traverse(boundExpression.Instance);
Console.Write("->");
}
else if (deref.Address.Type is IPointerTypeReference)
Console.Write("*");
- this.Visit(deref.Address);
+ this.Traverse(deref.Address);
return;
}
else
@@ -279,9 +279,9 @@ namespace BytecodeTranslator return be.Instance == null;
}
- public override void Visit(IPopValue popValue) {
+ public override void TraverseChildren(IPopValue popValue) {
var locExpr = this.StmtTraverser.operandStack.Pop();
- this.Visit(locExpr);
+ this.Traverse(locExpr);
this.TranslatedExpressions.Push(this.TranslatedExpressions.Pop());
}
@@ -290,15 +290,15 @@ namespace BytecodeTranslator /// Otherwise it just translates the expression and skips the address-of
/// operation.
/// </summary>
- public override void Visit(IAddressOf addressOf)
+ public override void TraverseChildren(IAddressOf addressOf)
{
- Visit(addressOf.Expression);
+ this.Traverse(addressOf.Expression);
}
#endregion
#region Translate Constant Access
- public override void Visit(ICompileTimeConstant constant) {
+ public override void TraverseChildren(ICompileTimeConstant constant) {
if (constant.Value == null) {
var bplType = sink.CciTypeToBoogie(constant.Type);
if (bplType == Bpl.Type.Int) {
@@ -406,7 +406,7 @@ namespace BytecodeTranslator return;
}
- public override void Visit(IDefaultValue defaultValue) {
+ public override void TraverseChildren(IDefaultValue defaultValue) {
var typ = defaultValue.Type;
if (TranslationHelper.IsStruct(typ)) {
@@ -463,7 +463,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(tok,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(locExpr),
- this.sink.FindOrCreateType(typ)
+ this.sink.FindOrCreateTypeReference(typ)
)
)
);
@@ -479,7 +479,7 @@ namespace BytecodeTranslator /// </summary>
/// <param name="methodCall"></param>
/// <remarks>Stub, This one really needs comments!</remarks>
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;
if (resolvedMethod == Dummy.Method) {
throw new TranslationException(
@@ -494,7 +494,7 @@ namespace BytecodeTranslator var methodName = MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None);
if (methodName.Equals("GetMeHere.GetMeHere.Assert")) {
// for now, just translate it as "assert e"
- this.Visit(methodCall.Arguments.First());
+ this.Traverse(methodCall.Arguments.First());
Bpl.Expr e = this.TranslatedExpressions.Pop();
this.StmtTraverser.StmtBuilder.Add(new Bpl.AssertCmd(methodCallToken, e));
return;
@@ -627,7 +627,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(methodCallToken,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(thisExpr),
- this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
+ this.sink.FindOrCreateTypeReference(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
)
)
);
@@ -641,7 +641,7 @@ namespace BytecodeTranslator #region Create the 'this' argument for the function call
thisExpr = null;
if (thisArg != null) {
- this.Visit(thisArg);
+ this.Traverse(thisArg);
var e = this.TranslatedExpressions.Pop();
var identifierExpr = e as Bpl.IdentifierExpr;
@@ -663,7 +663,7 @@ namespace BytecodeTranslator if (penum.Current == null) {
throw new TranslationException("More arguments than parameters in method call");
}
- this.Visit(exp);
+ this.Traverse(exp);
Bpl.Expr e = this.TranslatedExpressions.Pop();
if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter)
inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(exp.Type), e));
@@ -689,13 +689,13 @@ namespace BytecodeTranslator List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);
foreach (ITypeReference typeReference in consolidatedTypeArguments) {
- inexpr.Add(sink.FindOrCreateType(typeReference));
+ inexpr.Add(sink.FindOrCreateTypeReference(typeReference));
}
}
IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;
if (methodInstanceReference != null) {
foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {
- inexpr.Add(sink.FindOrCreateType(typeReference));
+ inexpr.Add(sink.FindOrCreateTypeReference(typeReference));
}
}
@@ -728,7 +728,7 @@ namespace BytecodeTranslator /// </summary>
/// <remarks>(mschaef) Works, but still a stub </remarks>
/// <param name="assignment"></param>
- public override void Visit(IAssignment assignment) {
+ public override void TraverseChildren(IAssignment assignment) {
Contract.Assert(TranslatedExpressions.Count == 0);
var tok = assignment.Token();
@@ -784,7 +784,7 @@ namespace BytecodeTranslator var/*?*/ local = container as ILocalDefinition;
if (local != null) {
Contract.Assume(instance == null);
- this.Visit(source);
+ this.Traverse(source);
var e = this.TranslatedExpressions.Pop();
var bplLocal = Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local));
if (structCopy) {
@@ -799,7 +799,7 @@ namespace BytecodeTranslator var/*?*/ parameter = container as IParameterDefinition;
if (parameter != null) {
Contract.Assume(instance == null);
- this.Visit(source);
+ this.Traverse(source);
var e = this.TranslatedExpressions.Pop();
var bplParam = Bpl.Expr.Ident(this.sink.FindParameterVariable(parameter, this.contractContext));
if (structCopy) {
@@ -813,7 +813,7 @@ namespace BytecodeTranslator var/*?*/ field = container as IFieldReference;
if (field != null) {
- this.Visit(source);
+ this.Traverse(source);
var e = this.TranslatedExpressions.Pop();
var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));
if (instance == null) {
@@ -821,7 +821,7 @@ namespace BytecodeTranslator StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));
}
else {
- this.Visit(instance);
+ this.Traverse(instance);
var x = this.TranslatedExpressions.Pop();
var boogieType = sink.CciTypeToBoogie(field.Type);
StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,
@@ -833,11 +833,11 @@ namespace BytecodeTranslator var/*?*/ arrayIndexer = container as IArrayIndexer;
if (arrayIndexer != null) {
- this.Visit(instance);
+ this.Traverse(instance);
var x = this.TranslatedExpressions.Pop();
- this.Visit(arrayIndexer.Indices);
+ this.Traverse(arrayIndexer.Indices);
var indices_prime = this.TranslatedExpressions.Pop();
- this.Visit(source);
+ this.Traverse(source);
var e = this.TranslatedExpressions.Pop();
StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, x, indices_prime, e, AccessType.Array, sink.CciTypeToBoogie(arrayIndexer.Type)));
return;
@@ -876,7 +876,7 @@ namespace BytecodeTranslator // ctor (probably only ever done in a different ctor for the
// struct). The assignment actually looks like "*this := DefaultValue(S)"
Contract.Assume(instance == null);
- this.Visit(source);
+ this.Traverse(source);
var e = this.TranslatedExpressions.Pop();
var bplLocal = Bpl.Expr.Ident(this.sink.ThisVariable);
cmd = Bpl.Cmd.SimpleAssign(tok, bplLocal, e);
@@ -896,7 +896,7 @@ namespace BytecodeTranslator /// For "new A(...)" generate "{ A a = Alloc(); A..ctor(a); return a; }" where
/// "a" is a fresh local.
/// </summary>
- public override void Visit(ICreateObjectInstance createObjectInstance)
+ public override void TraverseChildren(ICreateObjectInstance createObjectInstance)
{
var ctor = createObjectInstance.MethodToCall;
var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;
@@ -908,7 +908,7 @@ namespace BytecodeTranslator createObjectInstance.Type.TypeCode == PrimitiveTypeCode.UIntPtr) {
List<Bpl.Expr> args = new List<Bpl.Expr>();
foreach (IExpression e in createObjectInstance.Arguments) {
- this.Visit(e);
+ this.Traverse(e);
args.Add(TranslatedExpressions.Pop());
}
System.Diagnostics.Debug.Assert(args.Count == 1);
@@ -933,7 +933,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(token,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(Bpl.Expr.Ident(a)),
- this.sink.FindOrCreateType(createObjectInstance.Type)
+ this.sink.FindOrCreateTypeReference(createObjectInstance.Type)
)
)
);
@@ -941,7 +941,7 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
- public override void Visit(ICreateArray createArrayInstance)
+ public override void TraverseChildren(ICreateArray createArrayInstance)
{
Bpl.IToken cloc = createArrayInstance.Token();
var a = this.sink.CreateFreshLocal(createArrayInstance.Type);
@@ -949,7 +949,7 @@ namespace BytecodeTranslator Debug.Assert(createArrayInstance.Rank > 0);
Bpl.Expr lengthExpr = Bpl.Expr.Literal(1);
foreach (IExpression expr in createArrayInstance.Sizes) {
- this.Visit(expr);
+ this.Traverse(expr);
lengthExpr = Bpl.Expr.Mul(lengthExpr, TranslatedExpressions.Pop());
}
@@ -959,14 +959,14 @@ namespace BytecodeTranslator this.StmtTraverser.StmtBuilder.Add(new Bpl.AssumeCmd(cloc, assumeExpr));
TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
-
- public override void Visit(ICreateDelegateInstance createDelegateInstance)
+
+ public override void TraverseChildren(ICreateDelegateInstance createDelegateInstance)
{
if (createDelegateInstance.Instance == null) {
TranslatedExpressions.Push(Bpl.Expr.Literal(0));
}
else {
- this.Visit(createDelegateInstance.Instance);
+ this.Traverse(createDelegateInstance.Instance);
}
TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
@@ -990,13 +990,13 @@ namespace BytecodeTranslator List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);
foreach (ITypeReference typeReference in consolidatedTypeArguments) {
- typeParameterExprs.Add(sink.FindOrCreateType(typeReference));
+ typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));
}
}
IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;
if (methodInstanceReference != null) {
foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {
- typeParameterExprs.Add(sink.FindOrCreateType(typeReference));
+ typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));
}
}
Bpl.Expr typeParameterExpr =
@@ -1014,9 +1014,9 @@ namespace BytecodeTranslator #region Translate Binary Operators
- public override void Visit(IAddition addition)
+ public override void TraverseChildren(IAddition addition)
{
- base.Visit(addition);
+ base.TraverseChildren(addition);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1036,8 +1036,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IBitwiseAnd bitwiseAnd) {
- base.Visit(bitwiseAnd);
+ public override void TraverseChildren(IBitwiseAnd bitwiseAnd) {
+ base.TraverseChildren(bitwiseAnd);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1054,8 +1054,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IBitwiseOr bitwiseOr) {
- base.Visit(bitwiseOr);
+ public override void TraverseChildren(IBitwiseOr bitwiseOr) {
+ base.TraverseChildren(bitwiseOr);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1072,8 +1072,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IModulus modulus) {
- base.Visit(modulus);
+ public override void TraverseChildren(IModulus modulus) {
+ base.TraverseChildren(modulus);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1093,9 +1093,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IDivision division)
+ public override void TraverseChildren(IDivision division)
{
- base.Visit(division);
+ base.TraverseChildren(division);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1115,8 +1115,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IExclusiveOr exclusiveOr) {
- base.Visit(exclusiveOr);
+ public override void TraverseChildren(IExclusiveOr exclusiveOr) {
+ base.TraverseChildren(exclusiveOr);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
var e = new Bpl.NAryExpr(
@@ -1127,9 +1127,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(ISubtraction subtraction)
+ public override void TraverseChildren(ISubtraction subtraction)
{
- base.Visit(subtraction);
+ base.TraverseChildren(subtraction);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1149,9 +1149,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IMultiplication multiplication)
+ public override void TraverseChildren(IMultiplication multiplication)
{
- base.Visit(multiplication);
+ base.TraverseChildren(multiplication);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e;
@@ -1171,9 +1171,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IGreaterThan greaterThan)
+ public override void TraverseChildren(IGreaterThan greaterThan)
{
- base.Visit(greaterThan);
+ base.TraverseChildren(greaterThan);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1195,9 +1195,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IGreaterThanOrEqual greaterEqual)
+ public override void TraverseChildren(IGreaterThanOrEqual greaterEqual)
{
- base.Visit(greaterEqual);
+ base.TraverseChildren(greaterEqual);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1219,9 +1219,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(ILessThan lessThan)
+ public override void TraverseChildren(ILessThan lessThan)
{
- base.Visit(lessThan);
+ base.TraverseChildren(lessThan);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1243,9 +1243,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(ILessThanOrEqual lessEqual)
+ public override void TraverseChildren(ILessThanOrEqual lessEqual)
{
- base.Visit(lessEqual);
+ base.TraverseChildren(lessEqual);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1267,24 +1267,24 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IEquality equal)
+ public override void TraverseChildren(IEquality equal)
{
- base.Visit(equal);
+ base.TraverseChildren(equal);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, lexp, rexp));
}
- public override void Visit(INotEquality nonEqual)
+ public override void TraverseChildren(INotEquality nonEqual)
{
- base.Visit(nonEqual);
+ base.TraverseChildren(nonEqual);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, lexp, rexp));
}
- public override void Visit(IRightShift rightShift) {
- base.Visit(rightShift);
+ public override void TraverseChildren(IRightShift rightShift) {
+ base.TraverseChildren(rightShift);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e = new Bpl.NAryExpr(
@@ -1295,8 +1295,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(ILeftShift leftShift) {
- base.Visit(leftShift);
+ public override void TraverseChildren(ILeftShift leftShift) {
+ base.TraverseChildren(leftShift);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
Bpl.Expr e = new Bpl.NAryExpr(
@@ -1313,7 +1313,7 @@ namespace BytecodeTranslator /// TODO:
/// If it isn't either of these short forms then emit the proper expression!
/// </summary>
- public override void Visit(IConditional conditional) {
+ public override void TraverseChildren(IConditional conditional) {
/*
#region Try and reconstruct And, Or, Not expressions
if (conditional.Type.TypeCode == PrimitiveTypeCode.Boolean) {
@@ -1387,10 +1387,10 @@ namespace BytecodeTranslator StatementTraverser elseStmtTraverser = this.StmtTraverser.factory.MakeStatementTraverser(this.sink, this.StmtTraverser.PdbReader, this.contractContext);
ExpressionTraverser thenExprTraverser = this.StmtTraverser.factory.MakeExpressionTraverser(this.sink, thenStmtTraverser, this.contractContext);
ExpressionTraverser elseExprTraverser = this.StmtTraverser.factory.MakeExpressionTraverser(this.sink, elseStmtTraverser, this.contractContext);
- thenExprTraverser.Visit(conditional.ResultIfTrue);
- elseExprTraverser.Visit(conditional.ResultIfFalse);
+ thenExprTraverser.Traverse(conditional.ResultIfTrue);
+ elseExprTraverser.Traverse(conditional.ResultIfFalse);
- this.Visit(conditional.Condition);
+ this.Traverse(conditional.Condition);
Bpl.Expr conditionExpr = this.TranslatedExpressions.Pop();
Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditional.Token(),
@@ -1433,10 +1433,10 @@ namespace BytecodeTranslator #region Translate Unary Operators
- public override void Visit(ICastIfPossible castIfPossible) {
- base.Visit(castIfPossible.ValueToCast);
+ public override void TraverseChildren(ICastIfPossible castIfPossible) {
+ base.Traverse(castIfPossible.ValueToCast);
var exp = TranslatedExpressions.Pop();
- var e = this.sink.FindOrCreateType(castIfPossible.TargetType);
+ var e = this.sink.FindOrCreateTypeReference(castIfPossible.TargetType);
var callAs = new Bpl.NAryExpr(
castIfPossible.Token(),
new Bpl.FunctionCall(this.sink.Heap.AsFunction),
@@ -1445,14 +1445,14 @@ namespace BytecodeTranslator TranslatedExpressions.Push(callAs);
return;
}
- public override void Visit(ICheckIfInstance checkIfInstance) {
- var e = this.sink.FindOrCreateType(checkIfInstance.TypeToCheck);
+ public override void TraverseChildren(ICheckIfInstance checkIfInstance) {
+ var e = this.sink.FindOrCreateTypeReference(checkIfInstance.TypeToCheck);
//var callTypeOf = new Bpl.NAryExpr(
// checkIfInstance.Token(),
// new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
// new Bpl.ExprSeq(new Bpl.IdentifierExpr(checkIfInstance.Token(), v))
// );
- base.Visit(checkIfInstance.Operand);
+ base.TraverseChildren(checkIfInstance.Operand);
var exp = TranslatedExpressions.Pop();
var dynTypeOfOperand = this.sink.Heap.DynamicType(exp);
//var subtype = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, dynTypeOfOperand, e);
@@ -1467,9 +1467,9 @@ namespace BytecodeTranslator return;
}
- public override void Visit(IConversion conversion) {
+ public override void TraverseChildren(IConversion conversion) {
var tok = conversion.ValueToConvert.Token();
- Visit(conversion.ValueToConvert);
+ this.Traverse(conversion.ValueToConvert);
var boogieTypeOfValue = this.sink.CciTypeToBoogie(conversion.ValueToConvert.Type);
var boogieTypeToBeConvertedTo = this.sink.CciTypeToBoogie(conversion.TypeAfterConversion);
if (boogieTypeOfValue == boogieTypeToBeConvertedTo) {
@@ -1578,8 +1578,8 @@ namespace BytecodeTranslator }
}
- public override void Visit(IOnesComplement onesComplement) {
- base.Visit(onesComplement);
+ public override void TraverseChildren(IOnesComplement onesComplement) {
+ base.TraverseChildren(onesComplement);
var exp = TranslatedExpressions.Pop();
var e = new Bpl.NAryExpr(
onesComplement.Token(),
@@ -1589,9 +1589,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(IUnaryNegation unaryNegation)
+ public override void TraverseChildren(IUnaryNegation unaryNegation)
{
- base.Visit(unaryNegation);
+ base.TraverseChildren(unaryNegation);
Bpl.Expr exp = TranslatedExpressions.Pop();
Bpl.Expr e, zero, realZero;
zero = Bpl.Expr.Literal(0);
@@ -1612,9 +1612,9 @@ namespace BytecodeTranslator TranslatedExpressions.Push(e);
}
- public override void Visit(ILogicalNot logicalNot)
+ public override void TraverseChildren(ILogicalNot logicalNot)
{
- base.Visit(logicalNot.Operand);
+ base.Traverse(logicalNot.Operand);
Bpl.Expr exp = TranslatedExpressions.Pop();
Bpl.Type operandType = this.sink.CciTypeToBoogie(logicalNot.Operand.Type);
if (operandType == this.sink.Heap.RefType) {
@@ -1631,8 +1631,8 @@ namespace BytecodeTranslator Bpl.UnaryOperator.Opcode.Not, exp));
}
- public override void Visit(ITypeOf typeOf) {
- var e = this.sink.FindOrCreateType(typeOf.TypeToGet);
+ public override void TraverseChildren(ITypeOf typeOf) {
+ var e = this.sink.FindOrCreateTypeReference(typeOf.TypeToGet);
var callTypeOf = new Bpl.NAryExpr(
typeOf.Token(),
new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
@@ -1641,8 +1641,8 @@ namespace BytecodeTranslator TranslatedExpressions.Push(callTypeOf);
}
- public override void Visit(IVectorLength vectorLength) {
- base.Visit(vectorLength.Vector);
+ public override void TraverseChildren(IVectorLength vectorLength) {
+ base.Traverse(vectorLength.Vector);
var e = TranslatedExpressions.Pop();
TranslatedExpressions.Push(new Bpl.NAryExpr(vectorLength.Token(), new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(e)));
}
@@ -1650,14 +1650,14 @@ namespace BytecodeTranslator #endregion
#region CodeContract Expressions
- public override void Visit(IOldValue oldValue)
+ public override void TraverseChildren(IOldValue oldValue)
{
- base.Visit(oldValue);
+ base.TraverseChildren(oldValue);
TranslatedExpressions.Push(new Bpl.OldExpr(oldValue.Token(),
TranslatedExpressions.Pop()));
}
- public override void Visit(IReturnValue returnValue)
+ public override void TraverseChildren(IReturnValue returnValue)
{
if (this.sink.ReturnVariable == null)
{
@@ -1669,9 +1669,9 @@ namespace BytecodeTranslator }
#endregion
- public override void Visit(IBlockExpression blockExpression) {
- this.StmtTraverser.Visit(blockExpression.BlockStatement);
- this.Visit(blockExpression.Expression);
+ public override void TraverseChildren(IBlockExpression blockExpression) {
+ this.StmtTraverser.Traverse(blockExpression.BlockStatement);
+ this.Traverse(blockExpression.Expression);
}
/// <summary>
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index d5e9b797..0c9a7513 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -201,10 +201,10 @@ namespace Microsoft.Boogie.SMTLib datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
if (f.InParams.Length == 0) {
- datatypeString += f.Name + " ";
+ datatypeString += Namer.GetQuotedName(f, f.Name) + " ";
}
else {
- datatypeString += "(" + f.Name + " ";
+ datatypeString += "(" + Namer.GetQuotedName(f, f.Name) + " ";
foreach (Variable v in f.InParams) {
datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index f4973efd..8d4a4256 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -483,23 +483,27 @@ namespace Microsoft.Boogie.SMTLib ExprLineariser.Linearise(VCExpressionGenerator.True, options);
} else {
var groupings = node.GroupBy(e => e.Type).Where(g => g.Count() > 1).ToArray();
+ if (groupings.Length == 0) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ if (groupings.Length > 1)
+ wr.Write("(and ");
+
+ foreach (var g in groupings) {
+ wr.Write("(distinct");
+ foreach (VCExpr e in g) {
+ Contract.Assert(e != null);
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options);
+ }
+ wr.Write(")");
+ }
- if (groupings.Length > 1)
- wr.Write("(and ");
+ if (groupings.Length > 1)
+ wr.Write(")");
- foreach (var g in groupings) {
- wr.Write("(distinct");
- foreach (VCExpr e in g) {
- Contract.Assert(e != null);
- wr.Write(" ");
- ExprLineariser.Linearise(e, options);
- }
- wr.Write(")");
+ wr.Write("\n");
}
-
- if (groupings.Length > 1)
- wr.Write(")");
- wr.Write("\n");
}
return true;
|