diff options
Diffstat (limited to 'BCT')
18 files changed, 489 insertions, 489 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index cc51aaf9..dbcc8dad 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -1452,7 +1452,7 @@ namespace BytecodeTranslator // new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
// new Bpl.ExprSeq(new Bpl.IdentifierExpr(checkIfInstance.Token(), v))
// );
- base.TraverseChildren(checkIfInstance.Operand);
+ base.Traverse(checkIfInstance.Operand);
var exp = TranslatedExpressions.Pop();
var dynTypeOfOperand = this.sink.Heap.DynamicType(exp);
//var subtype = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, dynTypeOfOperand, e);
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 727d09c5..45adb36e 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -114,7 +114,7 @@ namespace BytecodeTranslator { [RepresentationFor("null", "const unique null : Ref;")]
public Bpl.Constant NullRef;
- [RepresentationFor("Type", "type Type;")]
+ [RepresentationFor("Type", "type {:datatype} Type;")]
public Bpl.TypeCtorDecl TypeTypeDecl = null;
public Bpl.CtorType TypeType;
@@ -258,12 +258,8 @@ namespace BytecodeTranslator { /// </summary>
public Bpl.Variable CreateTypeVariable(ITypeReference type, List<Bpl.ConstantParent> parents)
{
- string typename = TypeHelper.GetTypeName(type);
+ string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
- // Need to append something to the name to avoid name clashes with other members (of a different
- // type) that have the same name.
- typename += "$type";
-
Bpl.IToken tok = type.Token();
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType);
Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null);
@@ -271,18 +267,21 @@ namespace BytecodeTranslator { }
public Bpl.Function CreateTypeFunction(ITypeReference type, int parameterCount) {
- System.Diagnostics.Debug.Assert(parameterCount > 0);
- string typename = TypeHelper.GetTypeName(type);
+ System.Diagnostics.Debug.Assert(parameterCount >= 0);
+ string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
- // Need to append something to the name to avoid name clashes.
- typename += "$type";
Bpl.IToken tok = type.Token();
Bpl.VariableSeq inputs = new Bpl.VariableSeq();
- for (int i = 0; i < parameterCount; i++) {
- inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));
+ //for (int i = 0; i < parameterCount; i++) {
+ // inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));
+ //}
+ foreach (var t in type.ResolvedType.GenericParameters) {
+ inputs.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, t.Name.Value, this.TypeType), true));
}
Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.TypeType), false);
Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);
+ var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List<object>(1), null);
+ func.Attributes = attrib;
return func;
}
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 19339962..4f0e3667 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -27,7 +27,7 @@ namespace BytecodeTranslator { /// Responsible for traversing all metadata elements (i.e., everything exclusive
/// of method bodies).
/// </summary>
- public class MetadataTraverser : BaseMetadataTraverser {
+ public class BCTMetadataTraverser : MetadataTraverser {
readonly Sink sink;
public readonly TraverserFactory Factory;
@@ -35,7 +35,7 @@ namespace BytecodeTranslator { public readonly IDictionary<IUnit, PdbReader> PdbReaders;
public PdbReader/*?*/ PdbReader;
- public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)
+ public BCTMetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)
: base() {
this.sink = sink;
this.Factory = factory;
@@ -47,7 +47,7 @@ namespace BytecodeTranslator { foreach (IPrecondition pre in contract.Preconditions) {
var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);
ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);
- exptravers.Visit(pre.Condition); // TODO
+ exptravers.Traverse(pre.Condition); // TODO
// Todo: Deal with Descriptions
var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
translatedPres.Add(req);
@@ -61,7 +61,7 @@ namespace BytecodeTranslator { foreach (IPostcondition post in contract.Postconditions) {
var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);
ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);
- exptravers.Visit(post.Condition);
+ exptravers.Traverse(post.Condition);
// Todo: Deal with Descriptions
var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
translatedPosts.Add(ens);
@@ -74,7 +74,7 @@ namespace BytecodeTranslator { ICollection<Bpl.IdentifierExpr> modifiedExpr = new List<Bpl.IdentifierExpr>();
foreach (IAddressableExpression mod in contract.ModifiedVariables) {
ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, null, true);
- exptravers.Visit(mod);
+ exptravers.Traverse(mod);
Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
if (idexp == null) {
throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));
@@ -88,16 +88,16 @@ namespace BytecodeTranslator { #region Overrides
- public override void Visit(IModule module) {
+ public override void TraverseChildren(IModule module) {
this.PdbReaders.TryGetValue(module, out this.PdbReader);
- base.Visit(module);
+ base.TraverseChildren(module);
}
- public override void Visit(IAssembly assembly) {
+ public override void TraverseChildren(IAssembly assembly) {
this.PdbReaders.TryGetValue(assembly, out this.PdbReader);
this.sink.BeginAssembly(assembly);
try {
- base.Visit(assembly);
+ base.TraverseChildren(assembly);
} finally {
this.sink.EndAssembly(assembly);
}
@@ -107,7 +107,7 @@ namespace BytecodeTranslator { /// Translate the type definition.
/// </summary>
///
- public override void Visit(ITypeDefinition typeDefinition) {
+ public override void TraverseChildren(ITypeDefinition typeDefinition) {
if (!this.sink.TranslateType(typeDefinition)) return;
@@ -117,11 +117,16 @@ namespace BytecodeTranslator { trackPhonePageNameVariableName(typeDefinition);
trackPhoneApplicationClassname(typeDefinition);
+ var gtp = typeDefinition as IGenericTypeParameter;
+ if (gtp != null) {
+ return;
+ }
+
if (typeDefinition.IsClass) {
bool savedSawCctor = this.sawCctor;
this.sawCctor = false;
- sink.FindOrCreateType(typeDefinition);
- base.Visit(typeDefinition);
+ sink.FindOrCreateTypeReference(typeDefinition);
+ base.TraverseChildren(typeDefinition);
if (!this.sawCctor) {
CreateStaticConstructor(typeDefinition);
}
@@ -130,23 +135,23 @@ namespace BytecodeTranslator { ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(typeDefinition).ResolvedType;
sink.AddDelegateType(unspecializedType);
} else if (typeDefinition.IsInterface) {
- sink.FindOrCreateType(typeDefinition);
- base.Visit(typeDefinition);
+ sink.FindOrCreateTypeReference(typeDefinition);
+ base.TraverseChildren(typeDefinition);
} else if (typeDefinition.IsEnum) {
return; // enums just are translated as ints
} else if (typeDefinition.IsStruct) {
- sink.FindOrCreateType(typeDefinition);
+ sink.FindOrCreateTypeReference(typeDefinition);
CreateDefaultStructConstructor(typeDefinition);
CreateStructCopyConstructor(typeDefinition);
- base.Visit(typeDefinition);
+ base.TraverseChildren(typeDefinition);
} else {
Console.WriteLine("Unknown kind of type definition '{0}' was found",
TypeHelper.GetTypeName(typeDefinition));
throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));
}
- this.Visit(typeDefinition.PrivateHelperMembers);
+ this.Traverse(typeDefinition.PrivateHelperMembers);
foreach (var t in this.privateTypes) {
- this.Visit(t);
+ this.Traverse(t);
}
}
List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();
@@ -221,7 +226,7 @@ namespace BytecodeTranslator { };
}
- stmtTranslator.Visit(stmts);
+ stmtTranslator.Traverse(stmts);
var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);
var lit = Bpl.Expr.Literal(1);
@@ -325,7 +330,7 @@ namespace BytecodeTranslator { });
}
- stmtTranslator.Visit(stmts);
+ stmtTranslator.Traverse(stmts);
var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);
List<Bpl.Variable> vars = new List<Bpl.Variable>();
@@ -352,7 +357,7 @@ namespace BytecodeTranslator { /// <summary>
///
/// </summary>
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
if (method.IsStaticConstructor) this.sawCctor = true;
@@ -406,7 +411,7 @@ namespace BytecodeTranslator { #region Add assignments from In-Params to local-Params
- foreach (MethodParameter mparam in formalMap.Values) {
+ foreach (MethodParameter mparam in formalMap) {
if (mparam.inParameterCopy != null) {
Bpl.IToken tok = method.Token();
stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
@@ -420,7 +425,9 @@ namespace BytecodeTranslator { #region For non-deferring ctors and all cctors, initialize all fields to null-equivalent values
var inits = InitializeFieldsInConstructor(method);
if (0 < inits.Count) {
- new BlockStatement() { Statements = inits, }.Dispatch(stmtTraverser);
+ foreach (var s in inits) {
+ stmtTraverser.Traverse(s);
+ }
}
#endregion
@@ -481,7 +488,7 @@ namespace BytecodeTranslator { #region Create Local Vars For Implementation
List<Bpl.Variable> vars = new List<Bpl.Variable>();
- foreach (MethodParameter mparam in formalMap.Values) {
+ foreach (MethodParameter mparam in formalMap) {
if (!mparam.underlyingParameter.IsByReference)
vars.Add(mparam.outParameterCopy);
}
@@ -597,7 +604,7 @@ namespace BytecodeTranslator { return referencedTypeDefinition;
}
- public override void Visit(IFieldDefinition fieldDefinition) {
+ public override void TraverseChildren(IFieldDefinition fieldDefinition) {
Bpl.Variable fieldVar= this.sink.FindOrCreateFieldVariable(fieldDefinition);
// if tracked by the phone plugin, we need to find out the bpl assigned name for future use
@@ -642,31 +649,30 @@ namespace BytecodeTranslator { addPhoneTopLevelDeclarations();
foreach (var a in assemblies) {
- a.Dispatch(this);
+ this.Traverse((IAssembly)a);
}
}
#endregion
#region Helpers
- private class FindCtorCall : BaseCodeTraverser {
+ private class FindCtorCall : CodeTraverser {
private bool isDeferringCtor = false;
public ITypeReference containingType;
public static bool IsDeferringCtor(IMethodDefinition method, IBlockStatement body) {
var fcc = new FindCtorCall(method.ContainingType);
- fcc.Visit(body);
+ fcc.Traverse(body);
return fcc.isDeferringCtor;
}
private FindCtorCall(ITypeReference containingType) {
this.containingType = containingType;
}
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
var md = methodCall.MethodToCall.ResolvedMethod;
if (md != null && md.IsConstructor && methodCall.ThisArgument is IThisReference) {
this.isDeferringCtor = TypeHelper.TypesAreEquivalent(md.ContainingType, containingType);
- this.stopTraversal = true;
return;
}
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs index 066d4cdf..a5ed9cf3 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs @@ -6,7 +6,7 @@ using Microsoft.Cci; using Microsoft.Cci.MutableCodeModel;
namespace BytecodeTranslator.Phone {
- class PhoneBackKeyCallbackTraverser : BaseCodeTraverser {
+ class PhoneBackKeyCallbackTraverser : CodeTraverser {
private ITypeReference typeBeingTraversed;
private IMetadataHost host;
@@ -14,12 +14,12 @@ namespace BytecodeTranslator.Phone { this.host = host;
}
- public override void Visit(ITypeDefinition typeDef) {
+ public override void TraverseChildren(ITypeDefinition typeDef) {
typeBeingTraversed = typeDef;
- base.Visit(typeDef);
+ base.TraverseChildren(typeDef);
}
-
- public override void Visit(IMethodCall methodCall) {
+
+ public override void TraverseChildren(IMethodCall methodCall) {
if (methodCall.MethodToCall.ResolvedMethod.IsSpecialName && methodCall.MethodToCall.Name.Value == "add_BackKeyPress") {
// check if it is a back key handler and if it is...
// NAVIGATION TODO this only catches really locally delegate expressions. If it is created before, we see it as a BoundExpression
@@ -91,24 +91,24 @@ namespace BytecodeTranslator.Phone { PhoneCodeHelper.instance().BackKeyUnknownDelegateOffenders.Add(typeBeingTraversed);
}
}
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
}
private void parseBlockForNavigation(IBlockStatement block, out bool navigates, out ICollection<string> navTargets) {
PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host);
- traverser.Visit(block);
+ traverser.Traverse(block);
navigates = traverser.CodeDoesNavigation;
navTargets = traverser.NavigationTargets;
}
private void parseBlockForEventCancellation(IBlockStatement block, out bool cancels) {
PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host);
- traverser.Visit(block);
+ traverser.Traverse(block);
cancels = traverser.CancelsEvents;
}
}
- public class PhoneNavigationCallsTraverser : BaseCodeTraverser {
+ public class PhoneNavigationCallsTraverser : CodeTraverser {
private IMetadataHost host;
public bool CancelsEvents { get; private set; }
@@ -120,7 +120,7 @@ namespace BytecodeTranslator.Phone { this.host = host;
}
- public override void Visit(IMethodCall call) {
+ public override void TraverseChildren(IMethodCall call) {
checkMethodCallForEventCancellation(call);
checkMethodCallForNavigation(call);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs index f3e5ac08..0ed9270c 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs @@ -6,14 +6,14 @@ using Microsoft.Cci; using Microsoft.Cci.MutableCodeModel;
namespace BytecodeTranslator.Phone {
- class PhoneControlFeedbackCodeTraverser : BaseCodeTraverser {
+ class PhoneControlFeedbackCodeTraverser : CodeTraverser {
private IMetadataReaderHost host;
public PhoneControlFeedbackCodeTraverser(IMetadataReaderHost host) : base() {
this.host = host;
}
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {
// check for handlers we do not wish to add feedback checks to
if (methodCall.MethodToCall.Name.Value.StartsWith("add_")) {
@@ -49,16 +49,16 @@ namespace BytecodeTranslator.Phone { }
- class PhoneControlFeedbackMetadataTraverser : BaseMetadataTraverser {
+ class PhoneControlFeedbackMetadataTraverser : MetadataTraverser {
private IMetadataReaderHost host;
public PhoneControlFeedbackMetadataTraverser(IMetadataReaderHost host) : base() {
this.host = host;
}
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
PhoneControlFeedbackCodeTraverser codeTraverser = new PhoneControlFeedbackCodeTraverser(host);
- codeTraverser.Visit(method);
+ codeTraverser.TraverseChildren(method);
}
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index 391aaaaa..db1aac4c 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -23,7 +23,7 @@ namespace BytecodeTranslator.Phone { /// <summary>
/// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between
/// </summary>
- public class PhoneInitializationCodeTraverser : BaseCodeTraverser {
+ public class PhoneInitializationCodeTraverser : CodeTraverser {
private readonly IMethodDefinition methodBeingTraversed;
private static bool initializationFound= false;
private MetadataReaderHost host;
@@ -185,7 +185,7 @@ namespace BytecodeTranslator.Phone { }
public void injectPhoneControlsCode(BlockStatement block) {
- this.Visit(block);
+ this.Traverse(block);
}
private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {
@@ -300,9 +300,9 @@ namespace BytecodeTranslator.Phone { return new List<IStatement>();
}
- public override void Visit(IBlockStatement block) {
+ public override void TraverseChildren(IBlockStatement block) {
foreach (IStatement statement in block.Statements) {
- this.Visit(statement);
+ this.Traverse(statement);
if (initializationFound) {
injectPhoneInitializationCode(block as BlockStatement, statement as Statement);
initializationFound = false;
@@ -311,7 +311,7 @@ namespace BytecodeTranslator.Phone { }
}
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
if (methodCall.IsStaticCall ||
!methodCall.MethodToCall.ContainingType.ResolvedType.Equals(methodBeingTraversed.Container) ||
methodCall.MethodToCall.Name.Value != "InitializeComponent" ||
@@ -325,7 +325,7 @@ namespace BytecodeTranslator.Phone { /// <summary>
/// Traverse metadata looking only for PhoneApplicationPage's constructors
/// </summary>
- public class PhoneInitializationMetadataTraverser : BaseMetadataTraverser {
+ public class PhoneInitializationMetadataTraverser : MetadataTraverser {
private MetadataReaderHost host;
public PhoneInitializationMetadataTraverser(MetadataReaderHost host)
@@ -333,30 +333,30 @@ namespace BytecodeTranslator.Phone { this.host = host;
}
- public override void Visit(IModule module) {
- base.Visit(module);
+ public override void TraverseChildren(IModule module) {
+ base.TraverseChildren(module);
}
- public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
+ public override void TraverseChildren(IAssembly assembly) {
+ base.TraverseChildren(assembly);
}
/// <summary>
/// Check if the type being defined is a PhoneApplicationPage, uninteresting otherwise
/// </summary>
///
- public override void Visit(ITypeDefinition typeDefinition) {
+ public override void TraverseChildren(ITypeDefinition typeDefinition) {
if (typeDefinition.isPhoneApplicationClass(host)) {
PhoneCodeHelper.instance().setMainAppTypeReference(typeDefinition);
} else if (typeDefinition.isPhoneApplicationPageClass(host)) {
- base.Visit(typeDefinition);
+ base.TraverseChildren(typeDefinition);
}
}
/// <summary>
/// Check if it is traversing a constructor. If so, place necessary code after InitializeComponent() call
/// </summary>
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
if (!method.IsConstructor)
return;
@@ -370,7 +370,7 @@ namespace BytecodeTranslator.Phone { public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
foreach (var a in assemblies) {
- a.Dispatch(this);
+ this.Traverse((IAssembly)a);
}
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs index 97935721..1957c2fa 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs @@ -5,7 +5,7 @@ using System.Text; using Microsoft.Cci;
namespace BytecodeTranslator.Phone {
- public class PhoneMethodInliningMetadataTraverser : BaseMetadataTraverser {
+ public class PhoneMethodInliningMetadataTraverser : MetadataTraverser {
private HashSet<IMethodDefinition> methodsToInline;
private HashSet<IMethodDefinition> iterMethodsToInline;
private PhoneCodeHelper phoneHelper;
@@ -23,21 +23,21 @@ namespace BytecodeTranslator.Phone { TotalMethodsCount = 0;
}
- public override void Visit(IEnumerable<IModule> modules) {
- foreach (IModule module in modules) {
- assemblyBeingTranslated= module.ContainingAssembly;
- this.Visit(module);
+ public override void TraverseChildren(IAssembly assembly) {
+ foreach (IModule module in assembly.MemberModules) {
+ assemblyBeingTranslated = module.ContainingAssembly;
+ this.Traverse(module);
}
firstPassDone = true;
}
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
if (!firstPassDone)
TotalMethodsCount++;
if (iterMethodsToInline.Contains(method) || (!firstPassDone && phoneHelper.mustInlineMethod(method))) {
PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser();
- codeTraverser.Visit(method);
+ codeTraverser.TraverseChildren(method);
foreach (IMethodDefinition newMethodDef in codeTraverser.getMethodsFound()) {
bool isExtern = this.assemblyBeingTranslated != null &&
!TypeHelper.GetDefiningUnitReference(newMethodDef.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);
@@ -62,15 +62,15 @@ namespace BytecodeTranslator.Phone { public void findAllMethodsToInline(List<IModule> modules) {
while (!isFinished()) {
changedOnLastPass = false;
- Visit(modules);
+ this.Traverse(modules);
}
}
}
- class PhoneMethodInliningCodeTraverser : BaseCodeTraverser {
+ class PhoneMethodInliningCodeTraverser : CodeTraverser {
private HashSet<IMethodDefinition> foundMethods = new HashSet<IMethodDefinition>();
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
foundMethods.Add(methodCall.MethodToCall.ResolvedMethod);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index a5571efa..0fa4a884 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -7,7 +7,7 @@ using Microsoft.Cci.MutableCodeModel; using TranslationPlugins;
namespace BytecodeTranslator.Phone {
- public class PhoneNavigationCodeTraverser : BaseCodeTraverser {
+ public class PhoneNavigationCodeTraverser : CodeTraverser {
private MetadataReaderHost host;
private ITypeReference navigationSvcType;
private ITypeReference cancelEventArgsType;
@@ -38,12 +38,12 @@ namespace BytecodeTranslator.Phone { navigationCallers = new HashSet<IMethodReference>();
}
- public override void Visit(ITypeDefinition typeDef) {
+ public override void TraverseChildren(ITypeDefinition typeDef) {
this.typeTraversed = typeDef;
- base.Visit(typeDef);
+ base.TraverseChildren(typeDef);
}
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
this.methodTraversed = method;
if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {
navigationCallers.Add(method);
@@ -77,7 +77,7 @@ namespace BytecodeTranslator.Phone { }
}
}
- base.Visit(method);
+ base.TraverseChildren(method);
}
@@ -87,14 +87,14 @@ namespace BytecodeTranslator.Phone { private StaticURIMode currentStaticMode= StaticURIMode.NOT_STATIC;
private string unpurifiedFoundURI="";
- public override void Visit(IBlockStatement block) {
+ public override void TraverseChildren(IBlockStatement block) {
IList<Tuple<IStatement,StaticURIMode,string>> staticNavStmts = new List<Tuple<IStatement,StaticURIMode,string>>();
IList<IStatement> nonStaticNavStmts = new List<IStatement>();
foreach (IStatement statement in block.Statements) {
navCallFound = false;
navCallIsStatic = false;
navCallIsBack = false;
- this.Visit(statement);
+ this.Traverse(statement);
if (navCallFound) {
navCallers.Add(methodTraversed);
if (navCallIsStatic) {
@@ -165,7 +165,7 @@ namespace BytecodeTranslator.Phone { return true;
}
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
string target;
if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {
ICollection<Tuple<IMethodReference,string>> targets;
@@ -316,7 +316,7 @@ namespace BytecodeTranslator.Phone { /// <summary>
/// Traverse metadata looking only for PhoneApplicationPage's constructors
/// </summary>
- public class PhoneNavigationMetadataTraverser : BaseMetadataTraverser {
+ public class PhoneNavigationMetadataTraverser : MetadataTraverser {
private MetadataReaderHost host;
private ITypeDefinition typeBeingTraversed;
private PhoneNavigationCodeTraverser codeTraverser;
@@ -326,13 +326,15 @@ namespace BytecodeTranslator.Phone { this.host = host;
}
- public override void Visit(IEnumerable<IAssemblyReference> assemblies) {
- codeTraverser = new PhoneNavigationCodeTraverser(host, assemblies);
- base.Visit(assemblies);
+ public override void TraverseChildren(IModule module) {
+ codeTraverser = new PhoneNavigationCodeTraverser(host, module.AssemblyReferences);
+ base.Traverse(module.AssemblyReferences);
+ base.TraverseChildren(module);
}
+
// TODO can we avoid visiting every type? Are there only a few, identifiable, types that may perform navigation?
- public override void Visit(ITypeDefinition typeDefinition) {
+ public override void TraverseChildren(ITypeDefinition typeDefinition) {
typeBeingTraversed = typeDefinition;
if (typeDefinition.isPhoneApplicationClass(host)) {
NamespaceTypeDefinition mutableTypeDef = typeDefinition as NamespaceTypeDefinition;
@@ -351,22 +353,22 @@ namespace BytecodeTranslator.Phone { }
}
- codeTraverser.Visit(typeDefinition);
- base.Visit(typeDefinition);
+ codeTraverser.Traverse(typeDefinition);
+ base.TraverseChildren(typeDefinition);
}
// TODO same here. Are there specific methods (and ways to identfy those) that can perform navigation?
- public override void Visit(IMethodDefinition method) {
+ public override void TraverseChildren(IMethodDefinition method) {
if (PhoneCodeHelper.instance().isBackKeyPressOverride(method)) {
PhoneCodeHelper.instance().KnownBackKeyHandlers.Add(method);
PhoneCodeHelper.instance().OnBackKeyPressOverriden = true;
}
- base.Visit(method);
+ base.TraverseChildren(method);
}
public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
foreach (var a in assemblies) {
- a.Dispatch(this);
+ this.Traverse((IAssembly)a);
}
}
}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index d3994a6c..5b9f0afe 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -210,6 +210,9 @@ namespace BytecodeTranslator { pdbReader = new PdbReader(pdbStream, host);
}
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
+ // The decompiler does not turn calls to Assert/Assume into Code Model nodes
+ module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);
+
host.RegisterAsLatest(module);
modules.Add(module);
contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
@@ -396,7 +399,7 @@ namespace BytecodeTranslator { System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
PhoneBackKeyCallbackTraverser traverser = new PhoneBackKeyCallbackTraverser(sink.host);
- traverser.Visit(modules);
+ traverser.Traverse(modules);
}
}
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index faa48773..a550d5cd 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -223,7 +223,7 @@ namespace BytecodeTranslator { var key = ((IMethodReference)sig);
this.declaredMethods.TryGetValue(key, out procAndFormalMap);
var formalMap = procAndFormalMap.FormalMap;
- formalMap.TryGetValue(param, out mp);
+ mp = formalMap[param.Index];
return contractContext ? mp.inParameterCopy : mp.outParameterCopy;
}
@@ -433,7 +433,7 @@ namespace BytecodeTranslator { public struct ProcedureInfo {
private Bpl.DeclWithFormals decl;
- private Dictionary<IParameterDefinition, MethodParameter> formalMap;
+ private MethodParameter[] formalMap; // maps parameter index to formal
private Bpl.Formal thisVariable;
private Bpl.Formal returnVariable;
private Bpl.LocalVariable localExcVariable;
@@ -453,20 +453,20 @@ namespace BytecodeTranslator { }
public ProcedureInfo(
Bpl.DeclWithFormals decl,
- Dictionary<IParameterDefinition, MethodParameter> formalMap)
+ MethodParameter[] formalMap)
: this(decl) {
this.formalMap = formalMap;
}
public ProcedureInfo(
Bpl.DeclWithFormals decl,
- Dictionary<IParameterDefinition, MethodParameter> formalMap,
+ MethodParameter[] formalMap,
Bpl.Formal returnVariable)
: this(decl, formalMap) {
this.returnVariable = returnVariable;
}
public ProcedureInfo(
Bpl.DeclWithFormals decl,
- Dictionary<IParameterDefinition, MethodParameter> formalMap,
+ MethodParameter[] formalMap,
Bpl.Formal returnVariable,
Bpl.Formal thisVariable,
Bpl.LocalVariable localExcVariable,
@@ -482,7 +482,7 @@ namespace BytecodeTranslator { }
public Bpl.DeclWithFormals Decl { get { return decl; } }
- public Dictionary<IParameterDefinition, MethodParameter> FormalMap { get { return formalMap; } }
+ public MethodParameter[] FormalMap { get { return formalMap; } }
public Bpl.Formal ThisVariable { get { return thisVariable; } }
public Bpl.Formal ReturnVariable { get { return returnVariable; } }
public Bpl.LocalVariable LocalExcVariable { get { return localExcVariable; } }
@@ -508,13 +508,13 @@ namespace BytecodeTranslator { int in_count = 0;
int out_count = 0;
MethodParameter mp;
- var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
+ var formalMap = new MethodParameter[IteratorHelper.EnumerableCount(method.Parameters)];
foreach (IParameterDefinition formal in method.Parameters) {
mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));
if (mp.inParameterCopy != null) in_count++;
if (mp.outParameterCopy != null && formal.IsByReference)
out_count++;
- formalMap.Add(formal, mp);
+ formalMap[formal.Index] = mp;
}
if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
@@ -560,7 +560,7 @@ namespace BytecodeTranslator { if (thisVariable != null)
invars[i++] = thisVariable;
- foreach (MethodParameter mparam in formalMap.Values) {
+ foreach (MethodParameter mparam in formalMap) {
if (mparam.inParameterCopy != null) {
invars[i++] = mparam.inParameterCopy;
}
@@ -675,7 +675,7 @@ namespace BytecodeTranslator { if (!TranslationHelper.IsStruct(p2.Type)) continue;
if (!TypeHelper.TypesAreEquivalent(p1.Type, p2.Type)) continue;
var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq,
- Bpl.Expr.Ident(formalMap[p1].inParameterCopy), Bpl.Expr.Ident(formalMap[p2].inParameterCopy)));
+ Bpl.Expr.Ident(formalMap[p1.Index].inParameterCopy), Bpl.Expr.Ident(formalMap[p2.Index].inParameterCopy)));
boogiePrecondition.Add(req);
}
}
@@ -715,7 +715,7 @@ namespace BytecodeTranslator { new Bpl.EnsuresSeq()
);
this.TranslatedProgram.TopLevelDeclarations.Add(proc);
- procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());
+ procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);
this.declaredStructDefaultCtors.Add(key, procAndFormalMap);
}
return procAndFormalMap.Decl;
@@ -759,7 +759,7 @@ namespace BytecodeTranslator { new Bpl.EnsuresSeq(ens)
);
this.TranslatedProgram.TopLevelDeclarations.Add(proc);
- procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());
+ procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);
this.declaredStructCopyCtors.Add(key, procAndFormalMap);
}
return procAndFormalMap.Decl;
@@ -820,16 +820,18 @@ namespace BytecodeTranslator { return result;
}
- private static int NumGenericParameters(ITypeReference typeReference) {
- ITypeDefinition typeDefinition = typeReference.ResolvedType;
- int numParameters = typeDefinition.GenericParameterCount;
- INestedTypeDefinition ntd = typeDefinition as INestedTypeDefinition;
- while (ntd != null) {
- ITypeDefinition containingType = ntd.ContainingType.ResolvedType;
- numParameters += containingType.GenericParameterCount;
- ntd = containingType as INestedTypeDefinition;
+ private static ushort ConsolidatedGenericParameterCount(ITypeReference typeReference) {
+ Contract.Requires(typeReference != null);
+
+ var typeDefinition = typeReference.ResolvedType;
+ var totalNumberOfParameters = typeDefinition.GenericParameterCount;
+ var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
+ while (nestedTypeDefinition != null) {
+ var containingType = nestedTypeDefinition.ContainingType.ResolvedType;
+ totalNumberOfParameters += containingType.GenericParameterCount;
+ nestedTypeDefinition = containingType as INestedTypeDefinition;
}
- return numParameters;
+ return totalNumberOfParameters;
}
public static ITypeReference GetUninstantiatedGenericType(ITypeReference typeReference) {
@@ -871,30 +873,29 @@ namespace BytecodeTranslator { /// <paramref name="type"/> in the Bpl program. I.e., its
/// value represents the expression "typeof(type)".
/// </summary>
- public Bpl.Expr FindOrCreateType(ITypeReference type) {
- // The Heap has to decide how to represent the field (i.e., its type),
- // all the Sink cares about is adding a declaration for it.
+ public Bpl.Expr FindOrCreateTypeReference(ITypeReference type) {
+
+ var gtir = type as IGenericTypeInstanceReference;
+ if (gtir != null) {
+ var genericType = FindOrDefineType(gtir.GenericType);
+ var gArgs = new Bpl.ExprSeq();
+ foreach (var a in gtir.GenericArguments) {
+ var a_prime = FindOrCreateTypeReference(a);
+ gArgs.Add(a_prime);
+ }
+ var typeExpression = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(genericType), gArgs);
+ }
IGenericTypeParameter gtp = type as IGenericTypeParameter;
if (gtp != null) {
- int index = gtp.Index;
- var nestedType = gtp.DefiningType as INestedTypeDefinition;
- while (nestedType != null) {
- // calculate the consolidated index: the parameter knows only its index
- // in the type that declares it, not including any outer containing types
- var containingType = nestedType.ContainingTypeDefinition;
- index += containingType.GenericParameterCount;
- nestedType = containingType as INestedTypeDefinition;
- }
-
- ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);
- if (methodBeingTranslated.IsStatic) {
- return Bpl.Expr.Ident(info.TypeParameter(index));
- }
- else {
- Bpl.Expr thisExpr = Bpl.Expr.Ident(this.ThisVariable);
- return new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(childFunctions[index]), new Bpl.ExprSeq(this.Heap.DynamicType(thisExpr)));
+ Bpl.Variable v;
+ if (!this.declaredTypeVariables.TryGetValue(gtp.InternedKey, out v)) {
+ var loc = Bpl.Token.NoToken;
+ var t = CciTypeToBoogie(gtp);
+ v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, gtp.Name.Value, t));
+ this.declaredTypeVariables.Add(gtp.InternedKey, v);
}
+ return Bpl.Expr.Ident(v);
}
IGenericMethodParameter gmp = type as IGenericMethodParameter;
@@ -908,123 +909,103 @@ namespace BytecodeTranslator { GetConsolidatedTypeArguments(consolidatedTypeArguments, type);
if (consolidatedTypeArguments.Count > 0) {
- this.FindOrCreateType(uninstantiatedGenericType);
- var key = uninstantiatedGenericType.InternedKey;
- Bpl.Function f = this.declaredTypeFunctions[key];
+ this.FindOrCreateTypeReference(uninstantiatedGenericType);
+ var k = uninstantiatedGenericType.InternedKey;
+ var f2 = this.declaredTypeFunctions[k];
Bpl.ExprSeq args = new Bpl.ExprSeq();
foreach (ITypeReference p in consolidatedTypeArguments) {
- args.Add(FindOrCreateType(p));
+ args.Add(FindOrCreateTypeReference(p));
}
- Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), args);
+ Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f2), args);
return naryExpr;
}
- int numParameters = NumGenericParameters(type);
+ var f = FindOrDefineType(type);
+ // BUGBUG: Generics!
+ var fCall = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), new Bpl.ExprSeq());
+ return fCall;
+ }
+
+
+ /// <summary>
+ /// The Heap has to decide how to represent the type.
+ /// All the Sink cares about is adding a declaration for it.
+ /// </summary>
+ private Bpl.Function FindOrDefineType(ITypeReference type) {
+
+ Bpl.Function f;
+
+ var key = type.InternedKey;
+ if (this.declaredTypeFunctions.TryGetValue(key, out f))
+ return f;
+
+ var numParameters = ConsolidatedGenericParameterCount(type);
+
+ f = this.Heap.CreateTypeFunction(type, numParameters);
+ this.declaredTypeFunctions.Add(key, f);
+ this.TranslatedProgram.TopLevelDeclarations.Add(f);
+ DeclareParents(type.ResolvedType, f);
+
bool isExtern = this.assemblyBeingTranslated != null &&
!TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);
-
- if (numParameters > 0) {
- Bpl.Function f;
- var key = type.InternedKey;
- if (!this.declaredTypeFunctions.TryGetValue(key, out f)) {
- Bpl.VariableSeq vseq = new Bpl.VariableSeq();
- for (int i = 0; i < numParameters; i++) {
- vseq.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "arg" + i, this.Heap.TypeType), true));
- }
- f = this.Heap.CreateTypeFunction(type, numParameters);
- this.declaredTypeFunctions.Add(key, f);
- this.TranslatedProgram.TopLevelDeclarations.Add(f);
- if (numParameters > childFunctions.Count) {
- for (int i = childFunctions.Count; i < numParameters; i++) {
- Bpl.Variable input = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "in", this.Heap.TypeType), true);
- Bpl.Variable output = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "out", this.Heap.TypeType), false);
- Bpl.Function g = new Bpl.Function(Bpl.Token.NoToken, "Child" + i, new Bpl.VariableSeq(input), output);
- TranslatedProgram.TopLevelDeclarations.Add(g);
- childFunctions.Add(g);
- }
- }
- if (isExtern) {
- var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
- f.Attributes = attrib;
- }
- else {
- Bpl.VariableSeq qvars = new Bpl.VariableSeq();
- Bpl.ExprSeq exprs = new Bpl.ExprSeq();
- for (int i = 0; i < numParameters; i++) {
- Bpl.Variable v = new Bpl.Constant(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "arg" + i, this.Heap.TypeType));
- qvars.Add(v);
- exprs.Add(Bpl.Expr.Ident(v));
- }
- Bpl.Expr e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), exprs);
- for (int i = 0; i < numParameters; i++) {
- Bpl.Expr appl = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(childFunctions[i]), new Bpl.ExprSeq(e));
- Bpl.Trigger trigger = new Bpl.Trigger(Bpl.Token.NoToken, true, new Bpl.ExprSeq(e));
- Bpl.Expr qexpr = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, Bpl.Expr.Eq(appl, Bpl.Expr.Ident(qvars[i])));
- TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, qexpr));
- }
- }
- }
- return null;
- }
- else {
- Bpl.Variable t;
- var key = type.InternedKey;
- if (!this.declaredTypeConstants.TryGetValue(key, out t)) {
- //List<ITypeReference> structuralParents;
- //var parents = GetParents(type.ResolvedType, out structuralParents);
- //t = this.Heap.CreateTypeVariable(type, parents);
- t = this.Heap.CreateTypeVariable(type, null);
- this.declaredTypeConstants.Add(key, t);
- //foreach (var p in structuralParents) {
- // var p_prime = FindOrCreateType(p);
- // //var e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, Bpl.Expr.Ident(t), p_prime);
- // var e = new Bpl.NAryExpr(
- // Bpl.Token.NoToken,
- // new Bpl.FunctionCall(this.Heap.Subtype),
- // new Bpl.ExprSeq(Bpl.Expr.Ident(t), p_prime)
- // );
- // var a = new Bpl.Axiom(Bpl.Token.NoToken, e);
- // this.TranslatedProgram.TopLevelDeclarations.Add(a);
- //}
- this.TranslatedProgram.TopLevelDeclarations.Add(t);
- DeclareParents(type.ResolvedType, t);
- if (isExtern) {
- var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
- t.Attributes = attrib;
- }
- }
- return Bpl.Expr.Ident(t);
+ if (isExtern) {
+ var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
+ f.Attributes = attrib;
}
+ return f;
}
- private void DeclareSuperType(Bpl.Variable typeDefinitionAsBplConstant, ITypeReference superType) {
- var superType_prime = FindOrCreateType(superType);
- var e = new Bpl.NAryExpr(
- Bpl.Token.NoToken,
- new Bpl.FunctionCall(this.Heap.Subtype),
- new Bpl.ExprSeq(Bpl.Expr.Ident(typeDefinitionAsBplConstant), superType_prime)
- );
- var a = new Bpl.Axiom(Bpl.Token.NoToken, e);
- this.TranslatedProgram.TopLevelDeclarations.Add(a);
- if (!superType.ResolvedType.IsInterface) {
- var e2 = new Bpl.NAryExpr(
- Bpl.Token.NoToken,
- new Bpl.FunctionCall(this.Heap.DisjointSubtree),
- new Bpl.ExprSeq(Bpl.Expr.Ident(typeDefinitionAsBplConstant), superType_prime)
- );
- var a2 = new Bpl.Axiom(Bpl.Token.NoToken, e2);
- this.TranslatedProgram.TopLevelDeclarations.Add(a2);
- }
- }
- private void DeclareParents(ITypeDefinition typeDefinition, Bpl.Variable typeDefinitionAsBplConstant) {
+ private void DeclareParents(ITypeDefinition typeDefinition, Bpl.Function typeDefinitionAsBplFunction) {
foreach (var p in typeDefinition.BaseClasses) {
- DeclareSuperType(typeDefinitionAsBplConstant, p);
+ DeclareSuperType(typeDefinitionAsBplFunction, p);
}
foreach (var j in typeDefinition.Interfaces) {
- DeclareSuperType(typeDefinitionAsBplConstant, j);
+ DeclareSuperType(typeDefinitionAsBplFunction, j);
}
return;
}
+ private void DeclareSuperType(Bpl.Function typeDefinitionAsBplFunction, ITypeReference superType) {
+ var superType_prime = FindOrCreateTypeReference(superType);
+ var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;
+
+ var qvars = new Bpl.VariableSeq();
+ var exprs = new Bpl.ExprSeq();
+ for (int i = 0; i < numberOfGenericParameters; i++) {
+ var t = typeDefinitionAsBplFunction.InParams[i];
+ qvars.Add(t);
+ exprs.Add(Bpl.Expr.Ident(t));
+ }
+
+ // G(t,u)
+ var callToG = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs);
+ // Subtype(G(t,u), super)
+ Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, superType_prime));
+ Bpl.Expr disjointSubtree = null;
+ var isDisjoint = !superType.ResolvedType.IsInterface;
+ if (isDisjoint) {
+ // DisjointSubtree(G(t,u), super)
+ disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, superType_prime));
+ }
+
+ if (0 < numberOfGenericParameters) {
+
+ // (forall t : Type, u : Type :: { G(t,u) } Subtype(G(t,u), super))
+ var trigger = new Bpl.Trigger(Bpl.Token.NoToken, true, new Bpl.ExprSeq(callToG));
+ var forall = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, subtype);
+ subtype = forall;
+
+ if (isDisjoint) {
+ // (forall t : Type, u : Type :: { G(t,u) } DisjointSubtree(G(t,u), super))
+ disjointSubtree = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, disjointSubtree);
+ }
+ }
+
+ this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, subtype));
+ if (isDisjoint) {
+ this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, disjointSubtree));
+ }
+
+ }
private List<Bpl.ConstantParent> GetParents(ITypeDefinition typeDefinition, out List<ITypeReference> structuralParents) {
var parents = new List<Bpl.ConstantParent>();
@@ -1034,7 +1015,7 @@ namespace BytecodeTranslator { structuralParents.Add(p);
}
else {
- var v = (Bpl.IdentifierExpr)FindOrCreateType(p);
+ var v = (Bpl.IdentifierExpr)FindOrCreateTypeReference(p);
parents.Add(new Bpl.ConstantParent(v, true));
}
}
@@ -1043,7 +1024,7 @@ namespace BytecodeTranslator { structuralParents.Add(j);
}
else {
- var v = (Bpl.IdentifierExpr)FindOrCreateType(j);
+ var v = (Bpl.IdentifierExpr)FindOrCreateTypeReference(j);
parents.Add(new Bpl.ConstantParent(v, false));
}
}
@@ -1053,7 +1034,7 @@ namespace BytecodeTranslator { /// <summary>
/// The keys to the table are the interned key of the type.
/// </summary>
- private Dictionary<uint, Bpl.Variable> declaredTypeConstants = new Dictionary<uint, Bpl.Variable>();
+ private Dictionary<uint, Bpl.Variable> declaredTypeVariables = new Dictionary<uint, Bpl.Variable>();
private Dictionary<uint, Bpl.Function> declaredTypeFunctions = new Dictionary<uint, Bpl.Function>();
private List<Bpl.Function> childFunctions = new List<Bpl.Function>();
@@ -1160,7 +1141,7 @@ namespace BytecodeTranslator { mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();
escapingGotoEdges = new Dictionary<ITryCatchFinallyStatement, List<string>>();
nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();
- mostNestedTryStatementTraverser.Visit(method.Body);
+ mostNestedTryStatementTraverser.Traverse(method.Body);
}
public void BeginAssembly(IAssembly assembly) {
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 15f59a13..7a9340db 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -22,18 +22,18 @@ using BytecodeTranslator.Phone; namespace BytecodeTranslator
{
- public class MostNestedTryStatementTraverser : BaseCodeTraverser {
+ public class MostNestedTryStatementTraverser : CodeTraverser {
Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement = new Dictionary<IName, ITryCatchFinallyStatement>();
ITryCatchFinallyStatement currStatement = null;
- public override void Visit(ILabeledStatement labeledStatement) {
+ public override void TraverseChildren(ILabeledStatement labeledStatement) {
if (currStatement != null)
mostNestedTryStatement.Add(labeledStatement.Label, currStatement);
- base.Visit(labeledStatement);
+ base.TraverseChildren(labeledStatement);
}
- public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {
+ public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {
ITryCatchFinallyStatement savedStatement = currStatement;
currStatement = tryCatchFinallyStatement;
- base.Visit(tryCatchFinallyStatement);
+ base.TraverseChildren(tryCatchFinallyStatement);
currStatement = savedStatement;
}
public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {
@@ -43,7 +43,7 @@ namespace BytecodeTranslator }
}
- public class StatementTraverser : BaseCodeTraverser {
+ public class StatementTraverser : CodeTraverser {
public readonly TraverserFactory factory;
@@ -64,6 +64,7 @@ namespace BytecodeTranslator PdbReader = pdbReader;
this.contractContext = contractContext;
this.captureState = sink.Options.captureState;
+ this.PreorderVisitor = new SourceContextEmitter(this);
}
#endregion
@@ -71,7 +72,7 @@ namespace BytecodeTranslator Bpl.Expr ExpressionFor(IExpression expression) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- etrav.Visit(expression);
+ etrav.Traverse(expression);
Contract.Assert(etrav.TranslatedExpressions.Count == 1);
return etrav.TranslatedExpressions.Pop();
}
@@ -87,11 +88,54 @@ namespace BytecodeTranslator var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);
newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);
}
- this.Visit(methodBody);
+ this.Traverse(methodBody);
return newTypes;
}
#endregion
+ #region Helper Classes
+ class SourceContextEmitter : CodeVisitor {
+ StatementTraverser parent;
+ public SourceContextEmitter(StatementTraverser parent) {
+ this.parent = parent;
+ }
+
+ public override void Visit(IStatement statement) {
+ EmitSourceContext(statement);
+ if (this.parent.sink.Options.captureState) {
+ var tok = statement.Token();
+ var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);
+ var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);
+ this.parent.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
+ }
+
+ private void EmitSourceContext(IStatement statement) {
+ if (statement is IEmptyStatement) return;
+ var tok = statement.Token();
+ string fileName = null;
+ int lineNumber = 0;
+ if (this.parent.PdbReader != null) {
+ var slocs = this.parent.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);
+ foreach (var sloc in slocs) {
+ fileName = sloc.Document.Location;
+ lineNumber = sloc.StartLine;
+ break;
+ }
+ if (fileName != null) {
+ var attrib = new Bpl.QKeyValue(tok, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);
+ attrib = new Bpl.QKeyValue(tok, "sourceFile", new List<object> { fileName }, attrib);
+ this.parent.StmtBuilder.Add(
+ new Bpl.AssertCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
+ }
+ }
+ }
+ #endregion
+
//public override void Visit(ISourceMethodBody methodBody) {
// var block = methodBody.Block as BlockStatement;
// // TODO: Error if cast fails?
@@ -103,50 +147,15 @@ namespace BytecodeTranslator // base.Visit(methodBody);
//}
- public override void Visit(IBlockStatement block) {
+ public override void TraverseChildren(IBlockStatement block) {
foreach (var s in block.Statements) {
- this.Visit(s);
- }
- }
-
- public override void Visit(IStatement statement) {
- EmitSourceContext(statement);
- if (this.sink.Options.captureState) {
- var tok = statement.Token();
- var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);
- var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);
- StmtBuilder.Add(
- new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
- );
- }
- base.Visit(statement);
- }
-
- private void EmitSourceContext(IStatement statement) {
- if (statement is IEmptyStatement) return;
- var tok = statement.Token();
- string fileName = null;
- int lineNumber = 0;
- if (this.PdbReader != null) {
- var slocs = this.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);
- foreach (var sloc in slocs) {
- fileName = sloc.Document.Location;
- lineNumber = sloc.StartLine;
- break;
- }
- if (fileName != null) {
- var attrib = new Bpl.QKeyValue(tok, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);
- attrib = new Bpl.QKeyValue(tok, "sourceFile", new List<object> { fileName }, attrib);
- StmtBuilder.Add(
- new Bpl.AssertCmd(tok, Bpl.Expr.True, attrib)
- );
- }
+ this.Traverse(s);
}
}
#region Basic Statements
- public override void Visit(IAssertStatement assertStatement) {
+ public override void TraverseChildren(IAssertStatement assertStatement) {
Bpl.Expr conditionExpr = ExpressionFor(assertStatement.Condition);
Bpl.Type conditionType = this.sink.CciTypeToBoogie(assertStatement.Condition.Type);
if (conditionType == this.sink.Heap.RefType) {
@@ -165,7 +174,7 @@ namespace BytecodeTranslator }
}
- public override void Visit(IAssumeStatement assumeStatement) {
+ public override void TraverseChildren(IAssumeStatement assumeStatement) {
Bpl.Expr conditionExpr = ExpressionFor(assumeStatement.Condition);
Bpl.Type conditionType = this.sink.CciTypeToBoogie(assumeStatement.Condition.Type);
if (conditionType == this.sink.Heap.RefType) {
@@ -185,13 +194,13 @@ namespace BytecodeTranslator /// </summary>
/// <remarks>(mschaef) Works, but still a stub</remarks>
/// <param name="conditionalStatement"></param>
- public override void Visit(IConditionalStatement conditionalStatement) {
+ public override void TraverseChildren(IConditionalStatement conditionalStatement) {
StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- condTraverser.Visit(conditionalStatement.Condition);
- thenTraverser.Visit(conditionalStatement.TrueBranch);
- elseTraverser.Visit(conditionalStatement.FalseBranch);
+ condTraverser.Traverse(conditionalStatement.Condition);
+ thenTraverser.Traverse(conditionalStatement.TrueBranch);
+ elseTraverser.Traverse(conditionalStatement.FalseBranch);
Bpl.Expr conditionExpr = condTraverser.TranslatedExpressions.Pop();
Bpl.Type conditionType = this.sink.CciTypeToBoogie(conditionalStatement.Condition.Type);
@@ -221,9 +230,9 @@ namespace BytecodeTranslator /// </summary>
/// <param name="expressionStatement"></param>
/// <remarks> TODO: might be wrong for the general case</remarks>
- public override void Visit(IExpressionStatement expressionStatement) {
+ public override void TraverseChildren(IExpressionStatement expressionStatement) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- etrav.Visit(expressionStatement.Expression);
+ etrav.Traverse(expressionStatement.Expression);
}
/// <summary>
@@ -231,18 +240,18 @@ namespace BytecodeTranslator /// </summary>
/// <remarks>(mschaef) Not Implemented</remarks>
/// <param name="breakStatement"></param>
- public override void Visit(IBreakStatement breakStatement) {
+ public override void TraverseChildren(IBreakStatement breakStatement) {
throw new TranslationException("Break statements are not handled");
//StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));
}
- public override void Visit(IContinueStatement continueStatement) {
+ public override void TraverseChildren(IContinueStatement continueStatement) {
throw new TranslationException("Continue statements are not handled");
}
- public override void Visit(ISwitchStatement switchStatement) {
+ public override void TraverseChildren(ISwitchStatement switchStatement) {
var eTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- eTraverser.Visit(switchStatement.Expression);
+ eTraverser.Traverse(switchStatement.Expression);
var conditionExpr = eTraverser.TranslatedExpressions.Pop();
// Can't depend on default case existing or its index in the collection.
@@ -258,7 +267,7 @@ namespace BytecodeTranslator Bpl.StmtList defaultStmts = null;
if (defaultCase != null) {
var defaultBodyTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
- defaultBodyTraverser.Visit(defaultCase.Body);
+ defaultBodyTraverser.Traverse(defaultCase.Body);
defaultStmts = defaultBodyTraverser.StmtBuilder.Collect(defaultCase.Token());
}
@@ -269,12 +278,12 @@ namespace BytecodeTranslator var switchCase = switchCases[i];
var scTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- scTraverser.Visit(switchCase.Expression);
+ scTraverser.Traverse(switchCase.Expression);
var scConditionExpr = scTraverser.TranslatedExpressions.Pop();
var condition = Bpl.Expr.Eq(conditionExpr, scConditionExpr);
var scBodyTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
- scBodyTraverser.Visit(switchCase.Body);
+ scBodyTraverser.Traverse(switchCase.Body);
ifCmd = new Bpl.IfCmd(switchCase.Token(),
condition,
@@ -294,7 +303,7 @@ namespace BytecodeTranslator /// the default ctor.
/// Otherwise ignore it.
/// </summary>
- public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {
+ public override void TraverseChildren(ILocalDeclarationStatement localDeclarationStatement) {
var initVal = localDeclarationStatement.InitialValue;
var typ = localDeclarationStatement.LocalVariable.Type;
var isStruct = TranslationHelper.IsStruct(typ);
@@ -329,7 +338,7 @@ namespace BytecodeTranslator return;
}
- public override void Visit(IPushStatement pushStatement) {
+ public override void TraverseChildren(IPushStatement pushStatement) {
var tok = pushStatement.Token();
var val = pushStatement.ValueToPush;
var dup = val as IDupValue;
@@ -348,12 +357,12 @@ namespace BytecodeTranslator /// </summary>
/// <remarks>(mschaef) not implemented</remarks>
/// <param name="returnStatement"></param>
- public override void Visit(IReturnStatement returnStatement) {
+ public override void TraverseChildren(IReturnStatement returnStatement) {
Bpl.IToken tok = returnStatement.Token();
if (returnStatement.Expression != null) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- etrav.Visit(returnStatement.Expression);
+ etrav.Traverse(returnStatement.Expression);
if (this.sink.ReturnVariable == null || etrav.TranslatedExpressions.Count < 1) {
throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));
@@ -380,7 +389,7 @@ namespace BytecodeTranslator #region Goto and Labels
- public override void Visit(IGotoStatement gotoStatement) {
+ public override void TraverseChildren(IGotoStatement gotoStatement) {
IName target = gotoStatement.TargetStatement.Label;
ITryCatchFinallyStatement targetStatement = this.sink.MostNestedTryStatement(target);
int count = 0;
@@ -406,24 +415,24 @@ namespace BytecodeTranslator /// </summary>
/// <remarks> (mschaef) not sure if there is more work to do</remarks>
/// <param name="labeledStatement"></param>
- public override void Visit(ILabeledStatement labeledStatement) {
+ public override void TraverseChildren(ILabeledStatement labeledStatement) {
StmtBuilder.AddLabelCmd(labeledStatement.Label.Value);
- base.Visit(labeledStatement.Statement);
+ base.Traverse(labeledStatement.Statement);
}
#endregion
#region Looping Statements
- public override void Visit(IWhileDoStatement whileDoStatement) {
+ public override void TraverseChildren(IWhileDoStatement whileDoStatement) {
throw new TranslationException("WhileDo statements are not handled");
}
- public override void Visit(IForEachStatement forEachStatement) {
+ public override void TraverseChildren(IForEachStatement forEachStatement) {
throw new TranslationException("ForEach statements are not handled");
}
- public override void Visit(IForStatement forStatement) {
+ public override void TraverseChildren(IForStatement forStatement) {
throw new TranslationException("For statements are not handled");
}
@@ -489,9 +498,9 @@ namespace BytecodeTranslator StmtBuilder.Add(ifCmd);
}
- public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {
+ public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {
this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));
- this.Visit(tryCatchFinallyStatement.TryBody);
+ this.Traverse(tryCatchFinallyStatement.TryBody);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));
this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);
@@ -503,13 +512,13 @@ namespace BytecodeTranslator List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();
this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InCatch));
foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {
- typeReferences.Insert(0, this.sink.FindOrCreateType(catchClause.ExceptionType));
+ typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType));
StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
if (catchClause.ExceptionContainer != Dummy.LocalVariable) {
Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);
catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));
}
- catchTraverser.Visit(catchClause.Body);
+ catchTraverser.Traverse(catchClause.Body);
catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
catchTraverser.StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));
catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));
@@ -532,7 +541,7 @@ namespace BytecodeTranslator Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedLabelVariable), Bpl.Expr.Ident(this.sink.LabelVariable)));
- Visit(tryCatchFinallyStatement.FinallyBody);
+ this.Traverse(tryCatchFinallyStatement.FinallyBody);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(savedExcVariable)));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Ident(savedLabelVariable)));
this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);
@@ -543,14 +552,14 @@ namespace BytecodeTranslator RaiseException(raiseExpr);
}
- public override void Visit(IThrowStatement throwStatement) {
+ public override void TraverseChildren(IThrowStatement throwStatement) {
ExpressionTraverser exceptionTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
- exceptionTraverser.Visit(throwStatement.Exception);
+ exceptionTraverser.Traverse(throwStatement.Exception);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), exceptionTraverser.TranslatedExpressions.Pop()));
RaiseException();
}
- public override void Visit(IRethrowStatement rethrowStatement) {
+ public override void TraverseChildren(IRethrowStatement rethrowStatement) {
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));
RaiseException();
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 883d0eaf..a744f405 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -15,7 +15,7 @@ using Microsoft.Cci.Contracts; using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
-
+using System.Text.RegularExpressions;
namespace BytecodeTranslator {
@@ -131,44 +131,25 @@ namespace BytecodeTranslator { }
public static string TurnStringIntoValidIdentifier(string s) {
+
+ // Do this specially just to make the resulting string a little bit more readable.
+ // REVIEW: Just let the main replacement take care of it?
s = s.Replace("[0:,0:]", "2DArray"); // TODO: Do this programmatically to handle arbitrary arity
s = s.Replace("[0:,0:,0:]", "3DArray");
s = s.Replace("[0:,0:,0:,0:]", "4DArray");
s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray");
- s = s.Replace('!', '$');
- s = s.Replace('*', '$');
- s = s.Replace('+', '$');
- s = s.Replace('(', '$');
- s = s.Replace(')', '$');
- s = s.Replace(',', '$');
s = s.Replace("[]", "array");
- s = s.Replace('<', '$');
- s = s.Replace('>', '$');
- s = s.Replace(':', '$');
- s = s.Replace(' ', '$');
- s = s.Replace('{', '$');
- s = s.Replace('}', '$');
- s = s.Replace('-', '$');
- s = s.Replace(' ', '$');
- s = s.Replace('\t', '$');
- s = s.Replace('\r', '$');
- s = s.Replace('\n', '$');
- s = s.Replace('\b', '$');
- s = s.Replace('\x1B', '$');
- s = s.Replace('/', '$');
- s = s.Replace('\\', '$');
- s = s.Replace('=', '$');
- s = s.Replace('@', '$');
- s = s.Replace(';', '$');
- s = s.Replace('%', '$');
- s = s.Replace('&', '$');
- s = s.Replace('"', '$');
- s = s.Replace('[', '$');
- s = s.Replace(']', '$');
- s = s.Replace('|', '$');
- s = s.Replace('+', '$');
- s = s.Replace('±', '$');
- s = s.Replace('√', '$');
+
+ // The definition of a Boogie identifier is from BoogiePL.atg.
+ // Just negate that to get which characters should be replaced with a dollar sign.
+
+ // letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
+ // digit = "0123456789".
+ // special = "'~#$^_.?`".
+ // nondigit = letter + special.
+ // ident = [ '\\' ] nondigit {nondigit | digit}.
+
+ s = Regex.Replace(s, "[^A-Za-z0-9'~#$^_.?`]", "$");
s = GetRidOfSurrogateCharacters(s);
return s;
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs index 60f39e03..1ceb7902 100644 --- a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs @@ -12,7 +12,7 @@ namespace BytecodeTranslator { private Sink sink;
private IDictionary<IUnit, IContractProvider> contractProviders;
private IDictionary<IUnit, PdbReader> pdbReaders;
- private MetadataTraverser traverser;
+ private BCTMetadataTraverser traverser;
public BaseTranslator(TraverserFactory factory, Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
Factory = factory;
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs index f2932ac0..ffd6fe52 100644 --- a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs @@ -28,7 +28,9 @@ namespace BytecodeTranslator.TranslationPlugins.Translators { }
public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {
- traverser.Visit(assemblies);
+ foreach (var a in assemblies) {
+ traverser.Traverse((IAssembly)a);
+ }
}
}
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 472cbb0a..bbc2f7f7 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -25,11 +25,11 @@ namespace BytecodeTranslator { public abstract Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> reader);
- public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
+ public virtual BCTMetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> sourceLocationProviders)
{
- return new MetadataTraverser(sink, sourceLocationProviders, this);
+ return new BCTMetadataTraverser(sink, sourceLocationProviders, this);
}
public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
return new StatementTraverser(sink, pdbReader, contractContext, this);
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index 83541f7d..d90176a8 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -29,13 +29,13 @@ namespace BytecodeTranslator { /// </summary>
readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();
- public override MetadataTraverser MakeMetadataTraverser(Sink sink,
+ public override BCTMetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> pdbReaders) {
return new WholeProgramMetadataSemantics(this, sink, pdbReaders, this);
}
- public class WholeProgramMetadataSemantics : MetadataTraverser {
+ public class WholeProgramMetadataSemantics : BCTMetadataTraverser {
readonly WholeProgram parent;
readonly Sink sink;
@@ -53,13 +53,13 @@ namespace BytecodeTranslator { var typeRecorder = new RecordSubtypes(this.parent.subTypes);
foreach (var a in assemblies) {
this.codeUnderAnalysis.Add(a, true);
- typeRecorder.Visit(a);
+ typeRecorder.Traverse((IAssembly)a);
}
#endregion
base.TranslateAssemblies(assemblies);
}
- class RecordSubtypes : BaseMetadataTraverser {
+ class RecordSubtypes : MetadataTraverser {
Dictionary<ITypeReference, List<ITypeReference>> subTypes;
@@ -67,14 +67,14 @@ namespace BytecodeTranslator { this.subTypes = subTypes;
}
- public override void Visit(ITypeDefinition typeDefinition) {
+ public override void TraverseChildren(ITypeDefinition typeDefinition) {
foreach (var baseClass in typeDefinition.BaseClasses) {
if (!this.subTypes.ContainsKey(baseClass)) {
this.subTypes[baseClass] = new List<ITypeReference>();
}
this.subTypes[baseClass].Add(typeDefinition);
}
- base.Visit(typeDefinition);
+ base.TraverseChildren(typeDefinition);
}
}
@@ -100,24 +100,24 @@ namespace BytecodeTranslator { this.subTypes = parent.subTypes;
}
- public override void Visit(IMethodCall methodCall) {
+ public override void TraverseChildren(IMethodCall methodCall) {
var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;
bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
if (isEventAdd || isEventRemove) {
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
return;
}
if (!methodCall.IsVirtualCall) {
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
return;
}
var containingType = methodCall.MethodToCall.ContainingType;
List<ITypeReference> subTypesOfContainingType;
if (!this.subTypes.TryGetValue(containingType, out subTypesOfContainingType)) {
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
return;
}
Contract.Assert(0 < subTypesOfContainingType.Count);
@@ -125,7 +125,7 @@ namespace BytecodeTranslator { Contract.Assert(!resolvedMethod.IsConstructor);
var overrides = FindOverrides(containingType, resolvedMethod);
if (0 == overrides.Count) {
- base.Visit(methodCall);
+ base.TraverseChildren(methodCall);
return;
}
@@ -163,6 +163,11 @@ namespace BytecodeTranslator { foreach (var typeMethodPair in overrides) {
var t = typeMethodPair.Item1;
var m = typeMethodPair.Item2;
+ var typeForT = this.sink.FindOrCreateTypeReference(t);
+ if (typeForT == null) {
+ // BUGBUG!! This just silently skips the branch that would dispatch to t's implementation of the method!
+ continue;
+ }
var thenBranch = new Bpl.StmtListBuilder();
methodname = TranslationHelper.CreateUniqueMethodName(m); // REVIEW: Shouldn't this be call to FindOrCreateProcedure?
if (attrib != null)
@@ -173,7 +178,7 @@ namespace BytecodeTranslator { ifcmd = new Bpl.IfCmd(token,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(inexpr[0]),
- this.sink.FindOrCreateType(t)
+ typeForT
),
thenBranch.Collect(token),
null,
@@ -183,6 +188,14 @@ namespace BytecodeTranslator { elseBranch.Add(ifcmd);
}
+ if (ifcmd == null) {
+ // BUGBUG: then no override made it into the if-statement.
+ // currently that happens when all types are generic.
+ // Should be able to remove this when that is fixed.
+ base.Traverse(methodCall);
+ return;
+ }
+
this.StmtTraverser.StmtBuilder.Add(ifcmd);
return;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index b03c319f..155db7c9 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -344,7 +344,7 @@ type Ref; const unique null: Ref;
-type Type;
+type {:datatype} Type;
type Real;
@@ -429,13 +429,13 @@ function $DelegateTypeParameters(Delegate) : Type; var {:thread_local} $Exception: Ref;
-const unique RegressionTestInput.RealNumbers$type: Type;
+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
-const {:extern} unique System.Object$type: Type;
+function {:extern} T$System.Object() : Type;
-axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.RealNumbers(), T$System.Object());
procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);
@@ -576,11 +576,11 @@ implementation T$RegressionTestInput.RealNumbers.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;
+function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type;
-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());
const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
@@ -635,11 +635,11 @@ implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor( -const unique RegressionTestInput.CreateStruct$type: Type;
+function {:constructor} T$RegressionTestInput.CreateStruct() : Type;
-axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.CreateStruct(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.CreateStruct(), T$System.Object());
procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);
@@ -649,17 +649,17 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref); -const unique RegressionTestInput.S$type: Type;
+function {:constructor} T$RegressionTestInput.S() : Type;
-const {:extern} unique System.ValueType$type: Type;
+function {:extern} T$System.ValueType() : Type;
-axiom $Subtype(System.ValueType$type, System.Object$type);
+axiom $Subtype(T$System.ValueType(), T$System.Object());
-axiom $DisjointSubtree(System.ValueType$type, System.Object$type);
+axiom $DisjointSubtree(T$System.ValueType(), T$System.Object());
-axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);
+axiom $Subtype(T$RegressionTestInput.S(), T$System.ValueType());
-axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);
+axiom $DisjointSubtree(T$RegressionTestInput.S(), T$System.ValueType());
const unique F$RegressionTestInput.S.x: Field;
@@ -675,12 +675,12 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res call $tmp0 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp0);
- assume $DynamicType($tmp0) == RegressionTestInput.S$type;
+ assume $DynamicType($tmp0) == T$RegressionTestInput.S();
s := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
call $tmp1 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp1);
- assume $DynamicType($tmp1) == RegressionTestInput.S$type;
+ assume $DynamicType($tmp1) == T$RegressionTestInput.S();
s := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;
@@ -745,11 +745,11 @@ implementation T$RegressionTestInput.CreateStruct.#cctor() -const unique RegressionTestInput.ClassWithArrayTypes$type: Type;
+function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type;
-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());
var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
@@ -920,11 +920,11 @@ implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor() -function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type;
-function Child0(in: Type) : Type;
+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));
-axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));
const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;
@@ -959,11 +959,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1 -const unique RegressionTestInput.BitwiseOperations$type: Type;
+function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;
-axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.BitwiseOperations(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.BitwiseOperations(), T$System.Object());
procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);
@@ -1073,21 +1073,21 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor() -const unique RegressionTestInput.AsyncAttribute$type: Type;
+function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;
-const {:extern} unique System.Attribute$type: Type;
+function {:extern} T$System.Attribute() : Type;
-axiom $Subtype(System.Attribute$type, System.Object$type);
+axiom $Subtype(T$System.Attribute(), T$System.Object());
-axiom $DisjointSubtree(System.Attribute$type, System.Object$type);
+axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());
-const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;
+function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
-axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);
+axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());
-axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
+axiom $Subtype(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());
-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
+axiom $DisjointSubtree(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());
procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);
@@ -1123,11 +1123,11 @@ implementation T$RegressionTestInput.AsyncAttribute.#cctor() -const unique RegressionTestInput.RefParameters$type: Type;
+function {:constructor} T$RegressionTestInput.RefParameters() : Type;
-axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.RefParameters(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.RefParameters(), T$System.Object());
procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);
@@ -1177,11 +1177,11 @@ implementation T$RegressionTestInput.RefParameters.#cctor() -const unique RegressionTestInput.NestedGeneric$type: Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;
-axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.NestedGeneric(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric(), T$System.Object());
procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);
@@ -1203,11 +1203,11 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -const unique RegressionTestInput.NestedGeneric.C$type: Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;
-axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());
procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);
@@ -1229,9 +1229,11 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type;
-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));
+
+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));
procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);
@@ -1273,7 +1275,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
else
{
- call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));
+ call $tmp2 := System.Activator.CreateInstance``1(T);
$tmp1 := Box2Box($tmp2);
if ($Exception != null)
{
@@ -1340,11 +1342,11 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re -const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type;
-axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());
const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;
@@ -1379,11 +1381,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.# -const unique RegressionTestInput.Class0$type: Type;
+function {:constructor} T$RegressionTestInput.Class0() : Type;
-axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.Class0(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.Class0(), T$System.Object());
var F$RegressionTestInput.Class0.StaticInt: int;
@@ -1652,11 +1654,11 @@ implementation T$RegressionTestInput.Class0.#cctor() -const unique RegressionTestInput.ClassWithBoolTypes$type: Type;
+function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type;
-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());
var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index e52668d3..1a2ff101 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -330,7 +330,7 @@ type Ref; const unique null: Ref;
-type Type;
+type {:datatype} Type;
type Real;
@@ -415,13 +415,13 @@ function $DelegateTypeParameters(Delegate) : Type; var {:thread_local} $Exception: Ref;
-const unique RegressionTestInput.RealNumbers$type: Type;
+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
-const {:extern} unique System.Object$type: Type;
+function {:extern} T$System.Object() : Type;
-axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.RealNumbers(), T$System.Object());
procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);
@@ -562,11 +562,11 @@ implementation T$RegressionTestInput.RealNumbers.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;
+function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type;
-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());
var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
@@ -621,11 +621,11 @@ implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor( -const unique RegressionTestInput.CreateStruct$type: Type;
+function {:constructor} T$RegressionTestInput.CreateStruct() : Type;
-axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.CreateStruct(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.CreateStruct(), T$System.Object());
procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);
@@ -635,17 +635,17 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref); -const unique RegressionTestInput.S$type: Type;
+function {:constructor} T$RegressionTestInput.S() : Type;
-const {:extern} unique System.ValueType$type: Type;
+function {:extern} T$System.ValueType() : Type;
-axiom $Subtype(System.ValueType$type, System.Object$type);
+axiom $Subtype(T$System.ValueType(), T$System.Object());
-axiom $DisjointSubtree(System.ValueType$type, System.Object$type);
+axiom $DisjointSubtree(T$System.ValueType(), T$System.Object());
-axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);
+axiom $Subtype(T$RegressionTestInput.S(), T$System.ValueType());
-axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);
+axiom $DisjointSubtree(T$RegressionTestInput.S(), T$System.ValueType());
var F$RegressionTestInput.S.x: [Ref]int;
@@ -661,12 +661,12 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res call $tmp0 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp0);
- assume $DynamicType($tmp0) == RegressionTestInput.S$type;
+ assume $DynamicType($tmp0) == T$RegressionTestInput.S();
s := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
call $tmp1 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp1);
- assume $DynamicType($tmp1) == RegressionTestInput.S$type;
+ assume $DynamicType($tmp1) == T$RegressionTestInput.S();
s := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
assert F$RegressionTestInput.S.x[s] == 0;
@@ -731,11 +731,11 @@ implementation T$RegressionTestInput.CreateStruct.#cctor() -const unique RegressionTestInput.ClassWithArrayTypes$type: Type;
+function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type;
-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());
var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
@@ -906,11 +906,11 @@ implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor() -function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type;
-function Child0(in: Type) : Type;
+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));
-axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));
var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: [Ref]int;
@@ -945,11 +945,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1 -const unique RegressionTestInput.BitwiseOperations$type: Type;
+function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;
-axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.BitwiseOperations(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.BitwiseOperations(), T$System.Object());
procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);
@@ -1059,21 +1059,21 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor() -const unique RegressionTestInput.AsyncAttribute$type: Type;
+function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;
-const {:extern} unique System.Attribute$type: Type;
+function {:extern} T$System.Attribute() : Type;
-axiom $Subtype(System.Attribute$type, System.Object$type);
+axiom $Subtype(T$System.Attribute(), T$System.Object());
-axiom $DisjointSubtree(System.Attribute$type, System.Object$type);
+axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());
-const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;
+function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
-axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);
+axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());
-axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
+axiom $Subtype(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());
-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
+axiom $DisjointSubtree(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());
procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);
@@ -1109,11 +1109,11 @@ implementation T$RegressionTestInput.AsyncAttribute.#cctor() -const unique RegressionTestInput.RefParameters$type: Type;
+function {:constructor} T$RegressionTestInput.RefParameters() : Type;
-axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.RefParameters(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.RefParameters(), T$System.Object());
procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);
@@ -1163,11 +1163,11 @@ implementation T$RegressionTestInput.RefParameters.#cctor() -const unique RegressionTestInput.NestedGeneric$type: Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;
-axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.NestedGeneric(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric(), T$System.Object());
procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);
@@ -1189,11 +1189,11 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -const unique RegressionTestInput.NestedGeneric.C$type: Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;
-axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());
procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);
@@ -1215,9 +1215,11 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
+function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type;
-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));
+
+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));
procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);
@@ -1259,7 +1261,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
else
{
- call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));
+ call $tmp2 := System.Activator.CreateInstance``1(T);
$tmp1 := Box2Box($tmp2);
if ($Exception != null)
{
@@ -1326,11 +1328,11 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re -const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type;
-axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());
var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
@@ -1365,11 +1367,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.# -const unique RegressionTestInput.Class0$type: Type;
+function {:constructor} T$RegressionTestInput.Class0() : Type;
-axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.Class0(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.Class0(), T$System.Object());
var F$RegressionTestInput.Class0.StaticInt: int;
@@ -1638,11 +1640,11 @@ implementation T$RegressionTestInput.Class0.#cctor() -const unique RegressionTestInput.ClassWithBoolTypes$type: Type;
+function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type;
-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
+axiom $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());
-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());
var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
|