diff options
| -rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 5 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 121 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs (renamed from BCT/BytecodeTranslator/Phone/PhoneTraverser.cs) | 39 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs | 245 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs | 9 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/stubs.bpl | 287 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 7 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 44 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 181 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 4 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 111 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 111 |
13 files changed, 507 insertions, 661 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index 0393913a..e9b8be83 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -125,7 +125,10 @@ <Compile Include="Heap.cs" />
<Compile Include="HeapFactory.cs" />
<Compile Include="MetadataTraverser.cs" />
- <Compile Include="Phone\PhoneTraverser.cs" />
+ <Compile Include="Phone\PhoneCodeHelper.cs" />
+ <Compile Include="Phone\PhoneInitializationTraverser.cs" />
+ <Compile Include="Phone\PhoneNavigationTraverser.cs" />
+ <Compile Include="Phone\PhoneURIDeclarationsTraverser.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="Sink.cs" />
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 1bbcc198..d4a125e1 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -355,9 +355,6 @@ namespace BytecodeTranslator { if (helperTypes != null) {
this.privateTypes.AddRange(helperTypes);
}
- //method.Body.Dispatch(stmtTraverser);
- stmtTraverser.StmtBuilder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));
- stmtTraverser.GenerateDispatchContinuation();
#endregion
#region Create Local Vars For Implementation
@@ -370,7 +367,6 @@ namespace BytecodeTranslator { vars.Add(v);
}
vars.Add(procInfo.LocalExcVariable);
- vars.Add(procInfo.FinallyStackVariable);
vars.Add(procInfo.LabelVariable);
Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs new file mode 100644 index 00000000..60bf3360 --- /dev/null +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -0,0 +1,121 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+
+namespace BytecodeTranslator.Phone {
+ public enum StaticURIMode {
+ NOT_STATIC, STATIC_URI_CREATION_ONSITE, STATIC_URI_ROOT_CREATION_ONSITE,
+ }
+
+ public static class PhoneCodeHelper {
+ // TODO ensure this name is unique in the program code, although it is esoteric enough
+ private const string IL_BOOGIE_VAR_PREFIX = "@__BOOGIE_";
+ public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__";
+
+ public static bool isCreateObjectInstance(this IExpression expr) {
+ ICreateObjectInstance createObjExpr = expr as ICreateObjectInstance;
+ return (createObjExpr != null);
+ }
+
+ public static bool isClass(this ITypeReference typeRef, ITypeReference targetTypeRef) {
+ while (typeRef != null) {
+ if (typeRef.ResolvedType.Equals(targetTypeRef.ResolvedType))
+ return true;
+
+ typeRef = typeRef.ResolvedType.BaseClasses.FirstOrDefault();
+ }
+
+ return false;
+ }
+
+ public static bool isStringClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ ITypeReference targetType = host.PlatformType.SystemString;
+ return typeRef.isClass(targetType);
+ }
+
+ public static bool isURIClass (this ITypeReference typeRef, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ if (platformType == null)
+ return false;
+
+ IAssemblyReference coreRef = platformType.CoreAssemblyRef;
+ AssemblyIdentity systemAssemblyId = new AssemblyIdentity(host.NameTable.GetNameFor("System"), "", coreRef.Version, coreRef.PublicKeyToken, "");
+ IAssemblyReference systemAssembly = host.FindAssembly(systemAssemblyId);
+
+ ITypeReference uriTypeRef= platformType.CreateReference(systemAssembly, "System", "Uri");
+ return typeRef.isClass(uriTypeRef);
+ }
+
+
+ public static bool isPhoneApplicationClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;
+ AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
+ coreAssemblyRef.PublicKeyToken, "");
+
+ IAssemblyReference systemAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+ ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application");
+
+ return typeRef.isClass(applicationClass);
+ }
+
+ public static bool isPhoneApplicationPageClass(ITypeReference typeDefinition, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ AssemblyIdentity MSPhoneAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
+ IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+ ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage");
+
+ ITypeReference baseClass = typeDefinition.ResolvedType.BaseClasses.FirstOrDefault();
+ while (baseClass != null) {
+ if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {
+ return true;
+ }
+ baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();
+ }
+
+ return false;
+ }
+
+ /// <summary>
+ /// checks whether a static URI root (a definite page base) can be extracted from the expression
+ /// </summary>
+ /// <param name="expr"></param>
+ /// <returns></returns>
+ public static bool IsStaticURIRootExtractable(this IExpression expr) {
+ // Pre expr.type == string
+ IMethodCall stringConcatExpr = expr as IMethodCall;
+ if (stringConcatExpr == null)
+ return false;
+
+ if (stringConcatExpr.MethodToCall.Name.Value != "Concat")
+ return false;
+
+ IList<string> constantStrings = new List<string>();
+
+ // TODO this misses so many static strings, but let's start with this for now
+ IExpression leftOp= stringConcatExpr.Arguments.FirstOrDefault();
+ while (leftOp != null && leftOp is ICompileTimeConstant) {
+ ICompileTimeConstant strConst= leftOp as ICompileTimeConstant;
+ constantStrings.Add(strConst.Value as string);
+ if (stringConcatExpr.Arguments.ToList()[1] is IMethodCall) {
+ stringConcatExpr = stringConcatExpr.Arguments.ToList()[1] as IMethodCall;
+ leftOp = stringConcatExpr.Arguments.FirstOrDefault();
+ } else if (stringConcatExpr.Arguments.ToList()[1] is ICompileTimeConstant) {
+ constantStrings.Add((stringConcatExpr.Arguments.ToList()[1] as ICompileTimeConstant).Value as string);
+ break;
+ } else {
+ break;
+ }
+ }
+
+ string constantSubstring= constantStrings.Aggregate((aggr, elem) => aggr + elem);
+ return Uri.IsWellFormedUriString(constantSubstring, UriKind.RelativeOrAbsolute);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index 5f4680a8..fd24ff65 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -18,12 +18,12 @@ using System.Diagnostics.Contracts; using TranslationPlugins;
-namespace BytecodeTranslator {
+namespace BytecodeTranslator.Phone {
/// <summary>
/// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between
/// </summary>
- public class PhoneCodeTraverser : BaseCodeTraverser {
+ public class PhoneInitializationCodeTraverser : BaseCodeTraverser {
private readonly IMethodDefinition methodBeingTraversed;
private static bool initializationFound= false;
private PhoneControlsPlugin phonePlugin;
@@ -69,7 +69,7 @@ namespace BytecodeTranslator { }
}
- public PhoneCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {
+ public PhoneInitializationCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {
this.methodBeingTraversed = traversedMethod;
this.phonePlugin = phonePlugin;
this.host = host;
@@ -140,11 +140,6 @@ namespace BytecodeTranslator { this.Visit(block);
}
- private Assignment MakeFieldAssigment(string assignType, string objectName, string objectType, string fieldName, string sourceObjName, string sourceObjType, string sourceObjFieldName) {
- /* TODO */
- return null;
- }
-
private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {
// TODO check page name against container name
IEnumerable<ControlInfoStructure> controls= phonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString());
@@ -241,6 +236,7 @@ namespace BytecodeTranslator { return new List<IStatement>();
}
+ // TODO should stop propagating the string event name
private IEnumerable<IStatement> getCodeForSettingEventHandlers(ControlInfoStructure controlInfo, string eventName) {
// TODO not implemented yet
return new List<IStatement>();
@@ -271,11 +267,11 @@ namespace BytecodeTranslator { /// <summary>
/// Traverse metadata looking only for PhoneApplicationPage's constructors
/// </summary>
- public class PhoneMetadataTraverser : BaseMetadataTraverser {
+ public class PhoneInitializationMetadataTraverser : BaseMetadataTraverser {
private PhoneControlsPlugin phoneControlsInfo;
private MetadataReaderHost host;
- public PhoneMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)
+ public PhoneInitializationMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)
: base() {
this.phoneControlsInfo = phonePlugin;
this.host = host;
@@ -294,28 +290,11 @@ namespace BytecodeTranslator { /// </summary>
///
public override void Visit(ITypeDefinition typeDefinition) {
- if (typeDefinition.IsClass && isPhoneApplicationPage(typeDefinition)) {
+ if (typeDefinition.IsClass && PhoneCodeHelper.isPhoneApplicationPageClass(typeDefinition, host)) {
base.Visit(typeDefinition);
}
}
- private bool isPhoneApplicationPage(ITypeDefinition typeDefinition) {
- ITypeReference baseClass = typeDefinition.BaseClasses.FirstOrDefault();
- ITypeDefinition baseClassDef;
- while (baseClass != null) {
- baseClassDef = baseClass.ResolvedType;
- if (baseClassDef is INamespaceTypeDefinition) {
- if (((INamespaceTypeDefinition) baseClassDef).Name.Value == "PhoneApplicationPage" &&
- ((INamespaceTypeDefinition) baseClassDef).Container.ToString() == "Microsoft.Phone.Controls") {
- return true;
- }
- }
- baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();
- }
-
- return false;
- }
-
/// <summary>
/// Check if it is traversing a constructor. If so, place necessary code after InitializeComponent() call
/// </summary>
@@ -323,7 +302,7 @@ namespace BytecodeTranslator { if (!method.IsConstructor)
return;
- PhoneCodeTraverser codeTraverser = new PhoneCodeTraverser(host, method, phoneControlsInfo);
+ PhoneInitializationCodeTraverser codeTraverser = new PhoneInitializationCodeTraverser(host, method, phoneControlsInfo);
var methodBody = method.Body as SourceMethodBody;
if (methodBody == null)
return;
@@ -331,7 +310,7 @@ namespace BytecodeTranslator { codeTraverser.injectPhoneControlsCode(block);
}
- public virtual void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
+ public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
foreach (var a in assemblies) {
a.Dispatch(this);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs new file mode 100644 index 00000000..0cb6d91e --- /dev/null +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -0,0 +1,245 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+using Microsoft.Cci.MutableCodeModel;
+
+namespace BytecodeTranslator.Phone {
+ public class PhoneNavigationCodeTraverser : BaseCodeTraverser {
+ private MetadataReaderHost host;
+ private bool navCallFound;
+ private ITypeReference navigationSvcType;
+ private ITypeReference typeTraversed;
+
+ private static readonly string[] NAV_CALLS = { "GoBack", "GoForward", "Navigate", "StopLoading" };
+
+ public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {
+ this.host = host;
+ this.typeTraversed = typeTraversed;
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+
+ // TODO obtain version, culture and signature data dynamically
+ AssemblyIdentity MSPhoneAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
+ IAssembly phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+
+ // TODO determine the needed types dynamically
+ navigationSvcType = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");
+ }
+
+ public override void Visit(IMethodDefinition method) {
+ if (method.IsConstructor && PhoneCodeHelper.isPhoneApplicationClass(typeTraversed, host)) {
+ // TODO initialize current navigation URI to mainpage, using a placeholder for now.
+ // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations
+ string URI_placeholder="URI_PLACEHOLDER";
+ SourceMethodBody sourceBody = method.Body as SourceMethodBody;
+ if (sourceBody != null) {
+ BlockStatement bodyBlock = sourceBody.Block as BlockStatement;
+ if (bodyBlock != null) {
+ Assignment uriInitAssign = new Assignment() {
+ Source = new CompileTimeConstant() {
+ Type = host.PlatformType.SystemString,
+ Value = URI_placeholder,
+ },
+ Type = host.PlatformType.SystemString,
+ Target = new TargetExpression() {
+ Type = host.PlatformType.SystemString,
+ Definition = new FieldReference() {
+ ContainingType= typeTraversed,
+ IsStatic=true,
+ Type=host.PlatformType.SystemString,
+ Name=host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
+ },
+ },
+ };
+ Statement uriInitStmt= new ExpressionStatement() {
+ Expression= uriInitAssign,
+ };
+ bodyBlock.Statements.Insert(0, uriInitStmt);
+ bodyBlock.Statements.Insert(0, uriInitStmt);
+ }
+ }
+ }
+ base.Visit(method);
+ }
+
+ public override void Visit(IBlockStatement block) {
+ IList<IStatement> navStmts = new List<IStatement>();
+ foreach (IStatement statement in block.Statements) {
+ navCallFound = false;
+ this.Visit(statement);
+ if (navCallFound) {
+ navStmts.Add(statement);
+ }
+ }
+
+ injectNavigationUpdateCode(block, navStmts);
+ }
+
+ private int navEvtCount= 0;
+ private int staticNavEvtCount = 0;
+ private int nonStaticNavEvtCount = 0;
+ public override void Visit(IMethodCall methodCall) {
+ // check whether it is a NavigationService call
+ IMethodReference methodToCall= methodCall.MethodToCall;
+ ITypeReference callType= methodToCall.ContainingType;
+ if (!callType.ResolvedType.Equals(navigationSvcType.ResolvedType))
+ return;
+
+ string methodToCallName= methodToCall.Name.Value;
+ if (!NAV_CALLS.Contains(methodToCallName))
+ return;
+
+ // TODO check what to do with these
+ if (methodToCallName == "GoForward" || methodToCallName == "StopLoading") {
+ // TODO forward navigation is not supported by the phone
+ // TODO StopLoading is very async, I don't think we may verify this behaviour
+ // TODO possibly log
+ return;
+ } else {
+ navCallFound = true;
+ bool isStatic=false;
+ string notStaticReason = "";
+ StaticURIMode staticMode = StaticURIMode.NOT_STATIC;
+
+ if (methodToCallName == "GoBack")
+ isStatic= true;
+ else { // Navigate()
+ // check for different static patterns that we may be able to verify
+ IExpression uriArg= methodCall.Arguments.First();
+ if (isArgumentURILocallyCreatedStatic(uriArg)) {
+ isStatic = true;
+ staticMode = StaticURIMode.STATIC_URI_CREATION_ONSITE;
+ } else if (isArgumentURILocallyCreatedStaticRoot(uriArg)) {
+ isStatic = true;
+ staticMode = StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE;
+ } else {
+ // get reason
+ ICreateObjectInstance creationSite = methodCall.Arguments.First() as ICreateObjectInstance;
+ if (creationSite == null)
+ notStaticReason = "URI not created at call site";
+ else
+ notStaticReason = "URI not initialized as a static string";
+ }
+ }
+
+ Console.Write("Page navigation event found. Target is static? " + (isStatic ? "YES" : "NO"));
+ if (!isStatic) {
+ nonStaticNavEvtCount++;
+ Console.WriteLine(" -- Reason: " + notStaticReason);
+ } else {
+ staticNavEvtCount++;
+ Console.WriteLine("");
+ }
+ navEvtCount++;
+ }
+ }
+
+ /// <summary>
+ /// checks if argument is locally created URI with static URI target
+ /// </summary>
+ /// <param name="arg"></param>
+ /// <returns></returns>
+ private bool isArgumentURILocallyCreatedStatic(IExpression arg) {
+ if (!arg.isCreateObjectInstance())
+ return false;
+
+ if (!arg.Type.isURIClass(host))
+ return false;
+
+ ICreateObjectInstance creationSite = arg as ICreateObjectInstance;
+ IExpression uriTargetArg= creationSite.Arguments.First();
+
+ if (!uriTargetArg.Type.isStringClass(host))
+ return false;
+
+ ICompileTimeConstant staticURITarget = uriTargetArg as ICompileTimeConstant;
+ return (staticURITarget != null);
+ }
+
+ /// <summary>
+ /// checks if argument is locally created URI where target has statically created URI root
+ /// </summary>
+ /// <param name="arg"></param>
+ /// <returns></returns>
+ private bool isArgumentURILocallyCreatedStaticRoot(IExpression arg) {
+ // Pre: !isArgumentURILocallyCreatedStatic
+ if (!arg.isCreateObjectInstance())
+ return false;
+
+ if (!arg.Type.isURIClass(host))
+ return false;
+
+ ICreateObjectInstance creationSite = arg as ICreateObjectInstance;
+ IExpression uriTargetArg = creationSite.Arguments.First();
+
+ if (!uriTargetArg.Type.isStringClass(host))
+ return false;
+
+ return uriTargetArg.IsStaticURIRootExtractable();
+ }
+
+ private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable<IStatement> stmts) {
+ // TODO Here there is the STRONG assumption that a given method will only navigate at most once per method call
+ // TODO (or at most will re-navigate to the same page). Quick "page flipping" on the same method
+ // TODO would not be captured correctly
+ }
+ }
+
+ /// <summary>
+ /// Traverse metadata looking only for PhoneApplicationPage's constructors
+ /// </summary>
+ public class PhoneNavigationMetadataTraverser : BaseMetadataTraverser {
+ private MetadataReaderHost host;
+ private ITypeDefinition typeBeingTraversed;
+
+ public PhoneNavigationMetadataTraverser(MetadataReaderHost host)
+ : base() {
+ this.host = host;
+ }
+
+ public override void Visit(IModule module) {
+ base.Visit(module);
+ }
+
+ public override void Visit(IAssembly assembly) {
+ base.Visit(assembly);
+ }
+
+ // TODO can we avoid visiting every type? Are there only a few, identifiable, types that may perform navigation?
+ public override void Visit(ITypeDefinition typeDefinition) {
+ typeBeingTraversed = typeDefinition;
+ if (typeDefinition.isPhoneApplicationClass(host)) {
+ NamespaceTypeDefinition mutableTypeDef = typeDefinition as NamespaceTypeDefinition;
+ if (mutableTypeDef != null) {
+ FieldDefinition fieldDef = new FieldDefinition() {
+ ContainingTypeDefinition= mutableTypeDef,
+ InternFactory= host.InternFactory,
+ IsStatic= true,
+ Name= host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
+ Type= host.PlatformType.SystemString,
+ Visibility= TypeMemberVisibility.Public,
+ };
+ mutableTypeDef.Fields.Add(fieldDef);
+ }
+ }
+ base.Visit(typeDefinition);
+ }
+
+ // TODO same here. Are there specific methods (and ways to identfy those) that can perform navigation?
+ public override void Visit(IMethodDefinition method) {
+
+ PhoneNavigationCodeTraverser codeTraverser = new PhoneNavigationCodeTraverser(host, typeBeingTraversed);
+ codeTraverser.Visit(method);
+ }
+
+ public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
+ foreach (var a in assemblies) {
+ a.Dispatch(this);
+ }
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs new file mode 100644 index 00000000..fa330439 --- /dev/null +++ b/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs @@ -0,0 +1,9 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace BytecodeTranslator.Phone {
+ class PhoneURIDeclarationsTraverser {
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/stubs.bpl b/BCT/BytecodeTranslator/Phone/stubs.bpl index caa8210b..ae97e03f 100644 --- a/BCT/BytecodeTranslator/Phone/stubs.bpl +++ b/BCT/BytecodeTranslator/Phone/stubs.bpl @@ -1,286 +1,3 @@ -// BEGIN INJECTED CODE
-
-procedure UpdateNavigation(uri:Ref);
-implementation UpdateNavigation(uri:Ref) {
- CurrentNavigationPage := uri;
-}
-
-procedure DriveControls();
-implementation DriveControls() {
- var isCurrentPage1: bool;
- var isCurrentPage2: bool;
- var isCurrentPage3: bool;
- var isCurrentPage4: bool;
-
- // TODO there can be parameters in the URI and other stuff that makes this checks quite unreliable
- call isCurrentPage1 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page1.xaml_0);
- call isCurrentPage2 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page2.xaml_1);
- call isCurrentPage3 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page3.xaml_2);
- call isCurrentPage4 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page4.xaml_3);
-
- if (isCurrentPage1) {
- call drivePage1Controls();
- } else if (isCurrentPage2) {
- call drivePage2Controls();
- } else if (isCurrentPage3) {
- call drivePage3Controls();
- } else if (isCurrentPage4) {
- call drivePage4Controls();
- }
-}
-
-procedure drivePage1Controls();
-implementation drivePage1Controls() {
- var $continueOnPage: bool;
- var $activeControl: int;
- var $control: Ref;
- var $isEnabledRef: Ref;
- var $isEnabled: bool;
-
- $continueOnPage:=true;
- havoc $activeControl;
- while ($continueOnPage) {
- if ($activeControl==0) {
- // radio1 check
- $control := SimpleNavigationApp.Page1.radioButton1[$page1];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==1) {
- // radio2 check
- $control := SimpleNavigationApp.Page1.radioButton2[$page1];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==2) {
- // radio3 check
- $control := SimpleNavigationApp.Page1.radioButton3[$page1];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==3) {
- //radio4 check
- $control := SimpleNavigationApp.Page1.radioButton4[$page1];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==4) {
- //button click
- $control := SimpleNavigationApp.Page1.btnNavigate[$page1];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call SimpleNavigationApp.Page1.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page1, null, null);
- $continueOnPage := false;
- }
- }
- }
-}
-
-procedure drivePage2Controls();
-implementation drivePage2Controls() {
- var $continueOnPage: bool;
- var $activeControl: int;
- var $control: Ref;
- var $isEnabledRef: Ref;
- var $isEnabled: bool;
-
- $continueOnPage:=true;
- havoc $activeControl;
- while ($continueOnPage) {
- if ($activeControl==0) {
- // radio1 check
- $control := SimpleNavigationApp.Page2.radioButton1[$page2];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==1) {
- // radio2 check
- $control := SimpleNavigationApp.Page2.radioButton2[$page2];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==2) {
- // radio3 check
- $control := SimpleNavigationApp.Page2.radioButton3[$page2];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==3) {
- //radio4 check
- $control := SimpleNavigationApp.Page2.radioButton4[$page2];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==4) {
- //button click
- $control := SimpleNavigationApp.Page2.btnNavigate[$page2];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call SimpleNavigationApp.Page2.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page2, null, null);
- $continueOnPage := false;
- }
- }
- }
-}
-
-procedure drivePage3Controls();
-implementation drivePage3Controls() {
- var $continueOnPage: bool;
- var $activeControl: int;
- var $control: Ref;
- var $isEnabledRef: Ref;
- var $isEnabled: bool;
-
- $continueOnPage:=true;
- havoc $activeControl;
- while ($continueOnPage) {
- if ($activeControl==0) {
- // radio1 check
- $control := SimpleNavigationApp.Page3.radioButton1[$page3];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==1) {
- // radio2 check
- $control := SimpleNavigationApp.Page3.radioButton2[$page3];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==2) {
- // radio3 check
- $control := SimpleNavigationApp.Page3.radioButton3[$page3];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==3) {
- //radio4 check
- $control := SimpleNavigationApp.Page3.radioButton4[$page3];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==4) {
- //button click
- $control := SimpleNavigationApp.Page3.btnNavigate[$page3];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call SimpleNavigationApp.Page3.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page3, null, null);
- $continueOnPage := false;
- }
- }
- }
-}
-
-procedure drivePage4Controls();
-implementation drivePage4Controls() {
- var $continueOnPage: bool;
- var $activeControl: int;
- var $control: Ref;
- var $isEnabledRef: Ref;
- var $isEnabled: bool;
-
- $continueOnPage:=true;
- havoc $activeControl;
- while ($continueOnPage) {
- if ($activeControl==0) {
- // radio1 check
- $control := SimpleNavigationApp.Page4.radioButton1[$page4];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==1) {
- // radio2 check
- $control := SimpleNavigationApp.Page4.radioButton2[$page4];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==2) {
- // radio3 check
- $control := SimpleNavigationApp.Page4.radioButton3[$page4];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==3) {
- //radio4 check
- $control := SimpleNavigationApp.Page4.radioButton4[$page4];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));
- }
- } else if ($activeControl==4) {
- //button click
- $control := SimpleNavigationApp.Page4.btnNavigate[$page4];
- call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);
- $isEnabled := Box2Bool(Ref2Box($isEnabledRef));
- if ($isEnabled) {
- call SimpleNavigationApp.Page4.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page4, null, null);
- $continueOnPage := false;
- }
- }
- }
-}
-
-var $page1: Ref;
-var $page2: Ref;
-var $page3: Ref;
-var $page4: Ref;
-
-procedure SimpleNavigationApp.Main();
-implementation SimpleNavigationApp.Main() {
- var $doWork: bool;
- var $activeControl: int;
- var $isEnabledRef: Ref;
- var $isEnabled: bool;
- var $control: Ref;
-
- call SimpleNavigationApp.Page1.#ctor($page1);
- call SimpleNavigationApp.Page2.#ctor($page2);
- call SimpleNavigationApp.Page3.#ctor($page3);
- call SimpleNavigationApp.Page4.#ctor($page4);
- call SimpleNavigationApp.Page1.Page1_Loaded$System.Object$System.Windows.RoutedEventArgs($page1, null, null);
-
- CurrentNavigationPage := $string_literal_$Page1.xaml_0;
-
- havoc $doWork;
- while ($doWork) {
- call DriveControls();
- havoc $doWork;
- }
-}
-
function isControlEnabled(Ref) : bool;
function isControlChecked(Ref) : bool;
@@ -322,7 +39,3 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th $result := Box2Ref(Bool2Box(isChecked));
}
-var CurrentNavigationPage: Ref;
-var uriToNavigate: Ref;
-
-// END INJECTED CODE
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 28149cbd..0867de9f 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -18,6 +18,7 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts;
using Microsoft.Cci.MutableCodeModel.Contracts;
using TranslationPlugins;
+using BytecodeTranslator.Phone;
namespace BytecodeTranslator {
@@ -176,8 +177,10 @@ namespace BytecodeTranslator { var primaryModule = modules[0];
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- PhoneMetadataTraverser tr = new PhoneMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);
- tr.InjectPhoneCodeAssemblies(modules);
+ PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);
+ initTr.InjectPhoneCodeAssemblies(modules);
+ PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);
+ navTr.InjectPhoneCodeAssemblies(modules);
}
TraverserFactory traverserFactory;
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b5c01fc1..c14505ee 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -70,12 +70,6 @@ namespace BytecodeTranslator { return info.LocalExcVariable;
}
}
- public Bpl.LocalVariable FinallyStackCounterVariable {
- get {
- ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);
- return info.FinallyStackVariable;
- }
- }
public Bpl.LocalVariable LabelVariable {
get {
ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);
@@ -348,7 +342,6 @@ namespace BytecodeTranslator { private Bpl.Formal thisVariable;
private Bpl.Formal returnVariable;
private Bpl.LocalVariable localExcVariable;
- private Bpl.LocalVariable finallyStackVariable;
private Bpl.LocalVariable labelVariable;
private List<Bpl.Formal> typeParameters;
private List<Bpl.Formal> methodParameters;
@@ -359,7 +352,6 @@ namespace BytecodeTranslator { this.returnVariable = null;
this.thisVariable = null;
this.localExcVariable = null;
- this.finallyStackVariable = null;
this.labelVariable = null;
this.typeParameters = null;
this.methodParameters = null;
@@ -383,14 +375,12 @@ namespace BytecodeTranslator { Bpl.Formal returnVariable,
Bpl.Formal thisVariable,
Bpl.LocalVariable localExcVariable,
- Bpl.LocalVariable finallyStackVariable,
Bpl.LocalVariable labelVariable,
List<Bpl.Formal> typeParameters,
List<Bpl.Formal> methodParameters)
: this(decl, formalMap, returnVariable) {
this.thisVariable = thisVariable;
this.localExcVariable = localExcVariable;
- this.finallyStackVariable = finallyStackVariable;
this.labelVariable = labelVariable;
this.typeParameters = typeParameters;
this.methodParameters = methodParameters;
@@ -401,7 +391,6 @@ namespace BytecodeTranslator { public Bpl.Formal ThisVariable { get { return thisVariable; } }
public Bpl.Formal ReturnVariable { get { return returnVariable; } }
public Bpl.LocalVariable LocalExcVariable { get { return localExcVariable; } }
- public Bpl.LocalVariable FinallyStackVariable { get { return finallyStackVariable; } }
public Bpl.LocalVariable LabelVariable { get { return labelVariable; } }
public Bpl.Formal TypeParameter(int index) { return typeParameters[index]; }
public Bpl.Formal MethodParameter(int index) { return methodParameters[index]; }
@@ -418,7 +407,6 @@ namespace BytecodeTranslator { Bpl.Formal thisVariable = null;
Bpl.Formal retVariable = null;
Bpl.LocalVariable localExcVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$localExc", this.Heap.RefType));
- Bpl.LocalVariable finallyStackVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$finallyStackCounter", Bpl.Type.Int));
Bpl.LocalVariable labelVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$label", Bpl.Type.Int));
int in_count = 0;
@@ -533,7 +521,7 @@ namespace BytecodeTranslator { } else {
this.TranslatedProgram.TopLevelDeclarations.Add(decl);
}
- procInfo = new ProcedureInfo(decl, formalMap, retVariable, thisVariable, localExcVariable, finallyStackVariable, labelVariable, typeParameters, methodParameters);
+ procInfo = new ProcedureInfo(decl, formalMap, retVariable, thisVariable, localExcVariable, labelVariable, typeParameters, methodParameters);
this.declaredMethods.Add(key, procInfo);
// Can't visit the method's contracts until the formalMap and procedure are added to the
@@ -981,18 +969,30 @@ namespace BytecodeTranslator { }
return "continuation" + id;
}
- public string FindOrCreateDispatchContinuationLabel(ITryCatchFinallyStatement stmt) {
- int id;
- if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {
- id = tryCatchFinallyIdentifiers.Count;
- tryCatchFinallyIdentifiers[stmt] = id;
- }
- return "DispatchContinuation" + id;
- }
MostNestedTryStatementTraverser mostNestedTryStatementTraverser;
public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {
return mostNestedTryStatementTraverser.MostNestedTryStatement(label);
}
+ Dictionary<ITryCatchFinallyStatement, List<string>> escapingGotoEdges;
+ public void AddEscapingEdge(ITryCatchFinallyStatement tryCatchFinallyStatement, out int labelId, out string label) {
+ List<string> edges = null;
+ if (!escapingGotoEdges.ContainsKey(tryCatchFinallyStatement)) {
+ escapingGotoEdges[tryCatchFinallyStatement] = new List<string>();
+ }
+ edges = escapingGotoEdges[tryCatchFinallyStatement];
+ label = this.FindOrCreateFinallyLabel(tryCatchFinallyStatement) + "_" + edges.Count;
+ labelId = edges.Count;
+ edges.Add(label);
+ }
+ public List<string> EscapingEdges(ITryCatchFinallyStatement tryCatchFinallyStatement) {
+ if (!escapingGotoEdges.ContainsKey(tryCatchFinallyStatement)) {
+ escapingGotoEdges[tryCatchFinallyStatement] = new List<string>();
+ }
+ return escapingGotoEdges[tryCatchFinallyStatement];
+ }
+ public enum TryCatchFinallyContext { InTry, InCatch, InFinally };
+ public List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;
+
IMethodDefinition methodBeingTranslated;
public void BeginMethod(IMethodDefinition method) {
this.BeginMethod(method.ContainingType);
@@ -1000,6 +1000,8 @@ namespace BytecodeTranslator { this.cciLabels = new Dictionary<IName, int>();
this.tryCatchFinallyIdentifiers = new Dictionary<ITryCatchFinallyStatement, int>();
mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();
+ escapingGotoEdges = new Dictionary<ITryCatchFinallyStatement, List<string>>();
+ nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();
mostNestedTryStatementTraverser.Visit(method.Body);
}
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 6bc399c1..89a258ea 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -59,14 +59,6 @@ namespace BytecodeTranslator this.factory = sink.Factory;
PdbReader = pdbReader;
this.contractContext = contractContext;
- this.nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();
- }
- public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, List<Tuple<ITryCatchFinallyStatement,TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {
- this.sink = sink;
- this.factory = sink.Factory;
- PdbReader = pdbReader;
- this.contractContext = contractContext;
- this.nestedTryCatchFinallyStatements = nestedTryCatchFinallyStatements;
}
#endregion
@@ -93,22 +85,6 @@ namespace BytecodeTranslator this.Visit(methodBody);
return newTypes;
}
-
- public void GenerateDispatchContinuation() {
- foreach (ITryCatchFinallyStatement stmt in sink.tryCatchFinallyIdentifiers.Keys) {
- // Iterate over all labels in sink.cciLabels and generate dispatch based on sink.LabelVariable
- this.StmtBuilder.AddLabelCmd(sink.FindOrCreateDispatchContinuationLabel(stmt));
- Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);
- Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);
- foreach (IName name in sink.cciLabels.Keys) {
- Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name.Value));
- Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);
- elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
- }
- this.StmtBuilder.Add(elseIfCmd);
- this.StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));
- }
- }
#endregion
//public override void Visit(ISourceMethodBody methodBody) {
@@ -193,8 +169,8 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Works, but still a stub</remarks>
/// <param name="conditionalStatement"></param>
public override void Visit(IConditionalStatement conditionalStatement) {
- StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);
- StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);
+ 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);
@@ -248,6 +224,53 @@ namespace BytecodeTranslator throw new TranslationException("Continue statements are not handled");
}
+ public override void Visit(ISwitchStatement switchStatement) {
+ var eTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
+ eTraverser.Visit(switchStatement.Expression);
+ var conditionExpr = eTraverser.TranslatedExpressions.Pop();
+
+ // Can't depend on default case existing or its index in the collection.
+ var switchCases = new List<ISwitchCase>();
+ ISwitchCase defaultCase = null;
+ foreach (var switchCase in switchStatement.Cases) {
+ if (switchCase.IsDefault) {
+ defaultCase = switchCase;
+ } else {
+ switchCases.Add(switchCase);
+ }
+ }
+ Bpl.StmtList defaultStmts = null;
+ if (defaultCase != null) {
+ var defaultBodyTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
+ defaultBodyTraverser.Visit(defaultCase.Body);
+ defaultStmts = defaultBodyTraverser.StmtBuilder.Collect(defaultCase.Token());
+ }
+
+ Bpl.IfCmd ifCmd = null;
+
+ for (int i = switchCases.Count-1; 0 <= i; i--) {
+
+ var switchCase = switchCases[i];
+
+ var scTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
+ scTraverser.Visit(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);
+
+ ifCmd = new Bpl.IfCmd(switchCase.Token(),
+ condition,
+ scBodyTraverser.StmtBuilder.Collect(switchCase.Token()),
+ ifCmd,
+ defaultStmts);
+ defaultStmts = null; // default body goes only into the innermost if-then-else
+
+ }
+ StmtBuilder.Add(ifCmd);
+ }
+
/// <summary>
/// If the local declaration has an initial value, then generate the
/// statement "loc := e" from it. Otherwise ignore it.
@@ -320,33 +343,25 @@ namespace BytecodeTranslator #region Goto and Labels
- /// <summary>
- ///
- /// </summary>
- /// <remarks> STUB </remarks>
- /// <param name="gotoStatement"></param>
public override void Visit(IGotoStatement gotoStatement) {
IName target = gotoStatement.TargetStatement.Label;
- ITryCatchFinallyStatement targetContext = this.sink.MostNestedTryStatement(target);
+ ITryCatchFinallyStatement targetStatement = this.sink.MostNestedTryStatement(target);
int count = 0;
- while (count < this.nestedTryCatchFinallyStatements.Count) {
- int index = this.nestedTryCatchFinallyStatements.Count - count - 1;
- ITryCatchFinallyStatement nestedContext = this.nestedTryCatchFinallyStatements[index].Item1;
- if (targetContext == nestedContext)
+ while (count < this.sink.nestedTryCatchFinallyStatements.Count) {
+ int index = this.sink.nestedTryCatchFinallyStatements.Count - count - 1;
+ ITryCatchFinallyStatement nestedStatement = this.sink.nestedTryCatchFinallyStatements[index].Item1;
+ if (targetStatement == nestedStatement)
break;
- count++;
- }
- System.Diagnostics.Debug.Assert((count == nestedTryCatchFinallyStatements.Count) == (targetContext == null));
- if (count > 0) {
- int id = this.sink.FindOrCreateCciLabelIdentifier(target);
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(id)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(count-1)));
- string finallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[this.nestedTryCatchFinallyStatements.Count - 1].Item1);
+ int labelId;
+ string label;
+ this.sink.AddEscapingEdge(nestedStatement, out labelId, out label);
+ StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(labelId)));
+ string finallyLabel = this.sink.FindOrCreateFinallyLabel(nestedStatement);
StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(finallyLabel)));
+ StmtBuilder.AddLabelCmd(label);
+ count++;
}
- else {
- StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target.Value)));
- }
+ StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target.Value)));
}
/// <summary>
@@ -377,21 +392,34 @@ namespace BytecodeTranslator #endregion
- public enum TryCatchFinallyContext { InTry, InCatch, InFinally };
- List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;
-
+ public void GenerateDispatchContinuation(ITryCatchFinallyStatement tryCatchFinallyStatement) {
+ string continuationLabel = this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement);
+ Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true),
+ TranslationHelper.BuildStmtList(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(continuationLabel))), null, null);
+ List<string> edges = sink.EscapingEdges(tryCatchFinallyStatement);
+ Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);
+ for (int i = 0; i < edges.Count; i++) {
+ string label = edges[i];
+ Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(label));
+ Bpl.Expr targetExpr = Bpl.Expr.Literal(i);
+ elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr),
+ TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
+ }
+ this.StmtBuilder.Add(elseIfCmd);
+ }
+
private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {
- int count = nestedTryCatchFinallyStatements.Count;
+ int count = this.sink.nestedTryCatchFinallyStatements.Count;
if (count == 0) {
builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));
}
else {
- Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext> topOfStack = nestedTryCatchFinallyStatements[count - 1];
+ Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext> topOfStack = this.sink.nestedTryCatchFinallyStatements[count - 1];
string exceptionTarget;
- if (topOfStack.Item2 == TryCatchFinallyContext.InTry) {
+ if (topOfStack.Item2 == Sink.TryCatchFinallyContext.InTry) {
exceptionTarget = this.sink.FindOrCreateCatchLabel(topOfStack.Item1);
}
- else if (topOfStack.Item2 == TryCatchFinallyContext.InCatch) {
+ else if (topOfStack.Item2 == Sink.TryCatchFinallyContext.InCatch) {
builder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
exceptionTarget = this.sink.FindOrCreateFinallyLabel(topOfStack.Item1);
}
@@ -414,21 +442,21 @@ namespace BytecodeTranslator }
public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {
- nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InTry));
+ this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));
this.Visit(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))));
- nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
+ this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);
StmtBuilder.AddLabelCmd(this.sink.FindOrCreateCatchLabel(tryCatchFinallyStatement));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LocalExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef)));
List<Bpl.StmtList> catchStatements = new List<Bpl.StmtList>();
List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();
- this.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InCatch));
+ 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));
- StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);
+ 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)));
@@ -447,49 +475,21 @@ namespace BytecodeTranslator this.StmtBuilder.Add(elseIfCmd);
this.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));
RaiseException();
- nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
+ this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);
this.StmtBuilder.AddLabelCmd(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement));
if (tryCatchFinallyStatement.FinallyBody != null) {
- nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InFinally));
+ this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InFinally));
Bpl.Variable savedExcVariable = this.sink.CreateFreshLocal(this.sink.Heap.RefType);
Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);
- Bpl.Variable savedFinallyStackCounterVariable = 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)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));
Visit(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)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));
- nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
- }
- Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateDispatchContinuationLabel(tryCatchFinallyStatement)));
- Bpl.GotoCmd continuationCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement)));
- Bpl.IfCmd ifCmd = new Bpl.IfCmd(
- Bpl.Token.NoToken,
- Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)),
- TranslationHelper.BuildStmtList(continuationCmd),
- new Bpl.IfCmd(
- Bpl.Token.NoToken,
- Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)),
- TranslationHelper.BuildStmtList(dispatchCmd),
- null,
- null),
- null);
- this.StmtBuilder.Add(ifCmd);
- int count = this.nestedTryCatchFinallyStatements.Count;
- if (count == 0) {
- this.StmtBuilder.Add(new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));
- }
- else {
- Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);
- Bpl.AssignCmd decrementCmd = TranslationHelper.BuildAssignCmd(fsv, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, fsv, Bpl.Expr.Literal(1)));
- this.StmtBuilder.Add(decrementCmd);
- string parentFinallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[count - 1].Item1);
- Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(parentFinallyLabel));
- this.StmtBuilder.Add(parentCmd);
+ this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);
}
+ GenerateDispatchContinuation(tryCatchFinallyStatement);
StmtBuilder.AddLabelCmd(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));
Bpl.Expr raiseExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
RaiseException(raiseExpr);
@@ -506,6 +506,7 @@ namespace BytecodeTranslator StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));
RaiseException();
}
+
}
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 4685427f..78c818bd 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -27,10 +27,6 @@ namespace BytecodeTranslator { public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
return new StatementTraverser(sink, pdbReader, contractContext);
}
- public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext,
- List<Tuple<ITryCatchFinallyStatement,StatementTraverser.TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {
- return new StatementTraverser(sink, pdbReader, contractContext, nestedTryCatchFinallyStatements);
- }
public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {
return new ExpressionTraverser(sink, statementTraverser, contractContext);
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 80b15e2e..32242dcd 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -395,7 +395,6 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: {
var d: Real;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
d := d$in;
@@ -408,8 +407,6 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
return;
-
- return;
}
@@ -422,7 +419,6 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi {
var o: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
o := o$in;
@@ -435,8 +431,6 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
return;
-
- return;
}
@@ -454,7 +448,6 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) var local_0: Real;
var local_1: Real;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
@@ -491,8 +484,6 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
return;
-
- return;
}
@@ -508,7 +499,6 @@ procedure {:extern} System.Object.#ctor($this: Ref); implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -518,8 +508,6 @@ implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) }
return;
-
- return;
}
@@ -547,15 +535,12 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
$Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
return;
-
- return;
}
@@ -567,7 +552,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: R implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
$Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
@@ -579,8 +563,6 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($th }
return;
-
- return;
}
@@ -618,7 +600,6 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res var $tmp0: Ref;
var local_0: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
@@ -633,8 +614,6 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
$result := local_0;
return;
-
- return;
}
@@ -647,7 +626,6 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes {
var s: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
s := s$in;
@@ -658,8 +636,6 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
-
- return;
}
@@ -671,7 +647,6 @@ procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -681,8 +656,6 @@ implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) }
return;
-
- return;
}
@@ -714,7 +687,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() var local_1: Ref;
var $tmp2: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
@@ -737,8 +709,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() assert Box2Int($ArrayContents[local_0][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
-
- return;
}
@@ -753,7 +723,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() var local_0: Ref;
var $tmp4: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
@@ -776,8 +745,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
-
- return;
}
@@ -792,7 +759,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: var _loc0: Ref;
var _loc1: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -806,8 +772,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
-
- return;
}
@@ -820,7 +784,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ {
var xs: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
xs := xs$in;
@@ -842,8 +805,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
return;
-
- return;
}
@@ -855,7 +816,6 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
$Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));
@@ -866,8 +826,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) }
return;
-
- return;
}
@@ -894,7 +852,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -902,8 +859,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
$result := BitwiseAnd(x, y);
return;
-
- return;
}
@@ -917,7 +872,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -925,8 +879,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
$result := BitwiseOr(x, y);
return;
-
- return;
}
@@ -940,7 +892,6 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -948,8 +899,6 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
$result := BitwiseExclusiveOr(x, y);
return;
-
- return;
}
@@ -962,15 +911,12 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
$result := BitwiseNegation(x);
return;
-
- return;
}
@@ -982,7 +928,6 @@ procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -992,8 +937,6 @@ implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1025,7 +968,6 @@ procedure {:extern} System.Attribute.#ctor($this: Ref); implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Attribute.#ctor($this);
@@ -1035,8 +977,6 @@ implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1060,7 +1000,6 @@ procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns ( implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1068,8 +1007,6 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu x$out := x$out + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
return;
-
- return;
}
@@ -1081,7 +1018,6 @@ procedure RegressionTestInput.RefParameters.#ctor($this: Ref); implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -1091,8 +1027,6 @@ implementation RegressionTestInput.RefParameters.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1139,15 +1073,12 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
$result := x + 1;
return;
-
- return;
}
@@ -1162,7 +1093,6 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) var __temp_1: int;
var local_0: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1184,8 +1114,6 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) assert local_0 == RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
-
- return;
}
@@ -1199,15 +1127,12 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
return;
-
- return;
}
@@ -1220,14 +1145,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo {
var b: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
b := b$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
return;
-
- return;
}
@@ -1240,14 +1162,11 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re {
var c: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
c := c$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
return;
-
- return;
}
@@ -1260,7 +1179,6 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: {
var $tmp5: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
@@ -1272,8 +1190,6 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
-
- return;
}
@@ -1285,7 +1201,6 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: in implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1294,8 +1209,6 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
-
- return;
}
@@ -1307,7 +1220,6 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: in implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1318,8 +1230,6 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
-
- return;
}
@@ -1332,7 +1242,6 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1343,8 +1252,6 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
-
- return;
}
@@ -1357,15 +1264,12 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
$result := x;
return;
-
- return;
}
@@ -1379,7 +1283,6 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re var y: int;
var $tmp6: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
y := y$in;
@@ -1392,8 +1295,6 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re $result := $tmp6;
return;
-
- return;
}
@@ -1405,7 +1306,6 @@ procedure RegressionTestInput.Class0.#ctor($this: Ref); implementation RegressionTestInput.Class0.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -1415,8 +1315,6 @@ implementation RegressionTestInput.Class0.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1447,7 +1345,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1455,8 +1352,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
$result := x < y;
return;
-
- return;
}
@@ -1469,7 +1364,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this {
var z: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
z := z$in;
@@ -1494,8 +1388,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this }
return;
-
- return;
}
@@ -1508,7 +1400,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main() {
var $tmp7: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
@@ -1520,8 +1411,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
-
- return;
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index fc9743ca..19d98a28 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -381,7 +381,6 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: {
var d: Real;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
d := d$in;
@@ -394,8 +393,6 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
return;
-
- return;
}
@@ -408,7 +405,6 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi {
var o: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
o := o$in;
@@ -421,8 +417,6 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
return;
-
- return;
}
@@ -440,7 +434,6 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) var local_0: Real;
var local_1: Real;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
@@ -477,8 +470,6 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
return;
-
- return;
}
@@ -494,7 +485,6 @@ procedure {:extern} System.Object.#ctor($this: Ref); implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -504,8 +494,6 @@ implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) }
return;
-
- return;
}
@@ -533,15 +521,12 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
return;
-
- return;
}
@@ -553,7 +538,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: R implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;
@@ -565,8 +549,6 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($th }
return;
-
- return;
}
@@ -604,7 +586,6 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res var $tmp0: Ref;
var local_0: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
@@ -619,8 +600,6 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
$result := local_0;
return;
-
- return;
}
@@ -633,7 +612,6 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes {
var s: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
s := s$in;
@@ -644,8 +622,6 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
-
- return;
}
@@ -657,7 +633,6 @@ procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -667,8 +642,6 @@ implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) }
return;
-
- return;
}
@@ -700,7 +673,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() var local_1: Ref;
var $tmp2: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
@@ -723,8 +695,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() assert Box2Int($ArrayContents[local_0][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
-
- return;
}
@@ -739,7 +709,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() var local_0: Ref;
var $tmp4: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
@@ -762,8 +731,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
-
- return;
}
@@ -778,7 +745,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: var _loc0: Ref;
var _loc1: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -792,8 +758,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
-
- return;
}
@@ -806,7 +770,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ {
var xs: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
xs := xs$in;
@@ -828,8 +791,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
return;
-
- return;
}
@@ -841,7 +802,6 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
RegressionTestInput.ClassWithArrayTypes.a[$this] := null;
@@ -852,8 +812,6 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) }
return;
-
- return;
}
@@ -880,7 +838,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -888,8 +845,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
$result := BitwiseAnd(x, y);
return;
-
- return;
}
@@ -903,7 +858,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -911,8 +865,6 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
$result := BitwiseOr(x, y);
return;
-
- return;
}
@@ -926,7 +878,6 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -934,8 +885,6 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
$result := BitwiseExclusiveOr(x, y);
return;
-
- return;
}
@@ -948,15 +897,12 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
$result := BitwiseNegation(x);
return;
-
- return;
}
@@ -968,7 +914,6 @@ procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -978,8 +923,6 @@ implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1011,7 +954,6 @@ procedure {:extern} System.Attribute.#ctor($this: Ref); implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Attribute.#ctor($this);
@@ -1021,8 +963,6 @@ implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1046,7 +986,6 @@ procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns ( implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1054,8 +993,6 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu x$out := x$out + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
return;
-
- return;
}
@@ -1067,7 +1004,6 @@ procedure RegressionTestInput.RefParameters.#ctor($this: Ref); implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -1077,8 +1013,6 @@ implementation RegressionTestInput.RefParameters.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1125,15 +1059,12 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
$result := x + 1;
return;
-
- return;
}
@@ -1148,7 +1079,6 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) var __temp_1: int;
var local_0: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1170,8 +1100,6 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) assert local_0 == RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
-
- return;
}
@@ -1185,15 +1113,12 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
return;
-
- return;
}
@@ -1206,14 +1131,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo {
var b: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
b := b$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
return;
-
- return;
}
@@ -1226,14 +1148,11 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re {
var c: Ref;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
c := c$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
return;
-
- return;
}
@@ -1246,7 +1165,6 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: {
var $tmp5: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
@@ -1258,8 +1176,6 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
-
- return;
}
@@ -1271,7 +1187,6 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: in implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1280,8 +1195,6 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
-
- return;
}
@@ -1293,7 +1206,6 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: in implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x$out := x$in;
@@ -1304,8 +1216,6 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
-
- return;
}
@@ -1318,7 +1228,6 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1329,8 +1238,6 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
-
- return;
}
@@ -1343,15 +1250,12 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho {
var x: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
$result := x;
return;
-
- return;
}
@@ -1365,7 +1269,6 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re var y: int;
var $tmp6: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
y := y$in;
@@ -1378,8 +1281,6 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re $result := $tmp6;
return;
-
- return;
}
@@ -1391,7 +1292,6 @@ procedure RegressionTestInput.Class0.#ctor($this: Ref); implementation RegressionTestInput.Class0.#ctor($this: Ref)
{
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
call System.Object.#ctor($this);
@@ -1401,8 +1301,6 @@ implementation RegressionTestInput.Class0.#ctor($this: Ref) }
return;
-
- return;
}
@@ -1433,7 +1331,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 var x: int;
var y: int;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
x := x$in;
@@ -1441,8 +1338,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
$result := x < y;
return;
-
- return;
}
@@ -1455,7 +1350,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this {
var z: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
z := z$in;
@@ -1480,8 +1374,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this }
return;
-
- return;
}
@@ -1494,7 +1386,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main() {
var $tmp7: bool;
var $localExc: Ref;
- var $finallyStackCounter: int;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
@@ -1506,8 +1397,6 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
-
- return;
}
|