diff options
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 10 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 23 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 21 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 5 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 22 |
5 files changed, 50 insertions, 31 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 3367610a..dd1396cd 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -520,10 +520,12 @@ namespace BytecodeTranslator }
}
- if (PhoneCodeHelper.PhoneFeedbackToggled && PhoneCodeHelper.isMethodKnownUIChanger(methodCall, sink.host)) {
- Bpl.AssumeCmd assumeFalse = new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
- this.StmtTraverser.StmtBuilder.Add(assumeFalse);
- // FEEDBACK TODO make sure that the call to this method (not the called one but the one in context) is inlined (how?)
+ if (PhoneCodeHelper.PhoneFeedbackToggled) {
+ if (PhoneCodeHelper.isMethodKnownUIChanger(methodCall, sink.host)) {
+ Bpl.AssumeCmd assumeFalse = new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
+ this.StmtTraverser.StmtBuilder.Add(assumeFalse);
+ // FEEDBACK TODO make sure that the call to this method (not the called one but the one in context) is inlined (how?)
+ }
}
}
}
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 37eba5ec..f9b83348 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -306,6 +306,22 @@ namespace BytecodeTranslator { try {
StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ // FEEDBACK if this is a feedback method it will be plagued with false asserts. They will trigger if $Exception becomes other than null
+ // FEEDBACK for modular analysis we need it to be non-null at the start
+ // FEEDBACK also, callee is obviously non null
+ IMethodDefinition translatedMethod= sink.getMethodBeingTranslated();
+ if (PhoneCodeHelper.PhoneFeedbackToggled && translatedMethod != null &&
+ PhoneCodeHelper.isMethodInputHandlerOrFeedbackOverride(translatedMethod, sink.host)) {
+ // assign null to exception
+ List<Bpl.AssignLhs> assignee= new List<Bpl.AssignLhs>();
+ Bpl.AssignLhs exceptionAssignee= new Bpl.SimpleAssignLhs(Bpl.Token.NoToken, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable));
+ assignee.Add(exceptionAssignee);
+ List<Bpl.Expr> value= new List<Bpl.Expr>();
+ value.Add(Bpl.Expr.Ident(this.sink.Heap.NullRef));
+ Bpl.Cmd exceptionAssign= new Bpl.AssignCmd(Bpl.Token.NoToken, assignee, value);
+ stmtTraverser.StmtBuilder.Add(exceptionAssign);
+ }
+
#region Add assignments from In-Params to local-Params
foreach (MethodParameter mparam in formalMap.Values) {
@@ -395,13 +411,6 @@ namespace BytecodeTranslator { Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
- // FEEDBACK TODO what if it is a function?
- if (PhoneCodeHelper.PhoneFeedbackToggled) {
- if (PhoneCodeHelper.isMethodInputHandler(method, sink.host) || PhoneCodeHelper.isMethodKnownUIChangerOverride(method, sink.host)) {
- Bpl.AssertCmd falseAssertion = new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
- stmtTraverser.StmtBuilder.Add(falseAssertion);
- }
- }
var translatedBody = stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken);
#region Add implementation to Boogie program
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index ef6052ef..49b967a5 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -449,7 +449,7 @@ namespace BytecodeTranslator.Phone { public static bool PhoneNavigationToggled { get; set; }
public static bool PhoneFeedbackToggled { get; set; }
- public static bool isMethodInputHandler(IMethodDefinition method, IMetadataHost host) {
+ public static bool isMethodInputHandlerOrFeedbackOverride(IMethodDefinition method, IMetadataHost host) {
// FEEDBACK TODO: This is extremely coarse. There must be quite a few non-UI routed events
Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ;
IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;
@@ -466,25 +466,6 @@ namespace BytecodeTranslator.Phone { return false;
}
- public static bool isMethodKnownUIChangerOverride(IMethodDefinition method, IMetadataHost host) {
- // FEEDBACK TODO In this case, assume false should be inserted after calls to base(), otherwise esentially work like input handlers
-
- // TODO what if there is no implementation? will proc be null and still work?
- 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 routedEventType = platform.CreateReference(systemAssembly, "System", "Windows", "RoutedEventArgs");
- foreach (IParameterDefinition paramDef in method.Parameters) {
- if (paramDef.Type.isClass(routedEventType))
- return true;
- }
-
- return false;
- }
-
public static bool isMethodKnownUIChanger(IMethodCall methodCall, IMetadataHost host) {
if (methodCall.MethodToCall.ContainingType.isNavigationServiceClass(host)) {
return NAV_CALLS.Contains(methodCall.MethodToCall.Name.Value);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index f1e46ef1..ae56e916 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -1048,6 +1048,11 @@ namespace BytecodeTranslator { public List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;
IMethodDefinition methodBeingTranslated;
+
+ public IMethodDefinition getMethodBeingTranslated() {
+ return methodBeingTranslated;
+ }
+
public void BeginMethod(IMethodDefinition method) {
this.BeginMethod(method.ContainingType);
this.methodBeingTranslated = method;
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 7f087a86..c1a14372 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -17,6 +17,7 @@ using Microsoft.Cci.ILToCodeModel; using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
using TranslationPlugins;
+using BytecodeTranslator.Phone;
namespace BytecodeTranslator
@@ -337,6 +338,17 @@ namespace BytecodeTranslator StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
new Bpl.IdentifierExpr(tok, this.sink.ReturnVariable), etrav.TranslatedExpressions.Pop()));
}
+
+
+ // FEEDBACK TODO extract into a method
+ if (PhoneCodeHelper.PhoneFeedbackToggled) {
+ IMethodDefinition methodTranslated = sink.getMethodBeingTranslated();
+ if (methodTranslated != null && PhoneCodeHelper.isMethodInputHandlerOrFeedbackOverride(methodTranslated, sink.host)) {
+ Bpl.AssertCmd falseAssertion = new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
+ StmtBuilder.Add(falseAssertion);
+ }
+ }
+
StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token()));
}
#endregion
@@ -411,6 +423,16 @@ namespace BytecodeTranslator private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {
int count = this.sink.nestedTryCatchFinallyStatements.Count;
if (count == 0) {
+ // FEEDBACK TODO unfortunately return statements are created here too
+ // FEEDBACK TODO extract into a method
+ if (PhoneCodeHelper.PhoneFeedbackToggled) {
+ IMethodDefinition methodTranslated = sink.getMethodBeingTranslated();
+ if (methodTranslated != null && PhoneCodeHelper.isMethodInputHandlerOrFeedbackOverride(methodTranslated, sink.host)) {
+ Bpl.AssertCmd falseAssertion = new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
+ builder.Add(falseAssertion);
+ }
+ }
+
builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));
}
else {
|