summaryrefslogtreecommitdiff
path: root/BCT
diff options
context:
space:
mode:
authorGravatar t-espave <unknown>2011-08-15 12:04:02 -0700
committerGravatar t-espave <unknown>2011-08-15 12:04:02 -0700
commit9ea52dc03cd9e048489805bd9df6ac00215b965b (patch)
tree8fb323fce76919545f3d244ee6ddea7cdc2bc790 /BCT
parent39bfa2edfeb9a8cbbfcca1f5ed7ab870a5d4c928 (diff)
cleaning up & refactor
Diffstat (limited to 'BCT')
-rw-r--r--BCT/BytecodeTranslator/BytecodeTranslator.csproj1
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs71
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs2
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs33
-rw-r--r--BCT/BytecodeTranslator/Program.cs166
-rw-r--r--BCT/BytecodeTranslator/TraverserFactory.cs2
6 files changed, 132 insertions, 143 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 01f64519..9e5babc1 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -131,7 +131,6 @@
<Compile Include="Phone\PhoneInitializationTraverser.cs" />
<Compile Include="Phone\PhoneMethodInliningTraverser.cs" />
<Compile Include="Phone\PhoneNavigationTraverser.cs" />
- <Compile Include="Phone\PhoneCodeWrapperWriter.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="Sink.cs" />
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 6498edb9..a3b7eb99 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -407,44 +407,12 @@ namespace BytecodeTranslator
}
public override void Visit(IDefaultValue defaultValue) {
-
var typ = defaultValue.Type;
- #region Struct
if (TranslationHelper.IsStruct(typ)) {
- // then it is a struct and gets special treatment
- // translate it as if it were a call to the nullary ctor for the struct type
- // (which doesn't actually exist, but gets generated for each struct type
- // encountered during translation)
-
- var tok = defaultValue.Token();
-
- var loc = this.sink.CreateFreshLocal(typ);
- var locExpr = Bpl.Expr.Ident(loc);
-
- // First generate an Alloc() call
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(locExpr)));
-
- // Second, generate the call to the appropriate ctor
- var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typ);
- var invars = new List<Bpl.Expr>();
- invars.Add(locExpr);
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, invars, new List<Bpl.IdentifierExpr>()));
-
- // Generate an assumption about the dynamic type of the just allocated object
- this.StmtTraverser.StmtBuilder.Add(
- new Bpl.AssumeCmd(tok,
- Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
- this.sink.Heap.DynamicType(locExpr),
- this.sink.FindOrCreateType(typ)
- )
- )
- );
-
- this.TranslatedExpressions.Push(locExpr);
+ translateStructDefaultValue(defaultValue, typ);
return;
}
- #endregion
Bpl.Expr e;
var bplType = this.sink.CciTypeToBoogie(typ);
@@ -470,6 +438,39 @@ namespace BytecodeTranslator
return;
}
+ private void translateStructDefaultValue(IDefaultValue defaultValue, ITypeReference typ) {
+ // then it is a struct and gets special treatment
+ // translate it as if it were a call to the nullary ctor for the struct type
+ // (which doesn't actually exist, but gets generated for each struct type
+ // encountered during translation)
+
+ var tok = defaultValue.Token();
+
+ var loc = this.sink.CreateFreshLocal(typ);
+ var locExpr = Bpl.Expr.Ident(loc);
+
+ // First generate an Alloc() call
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(locExpr)));
+
+ // Second, generate the call to the appropriate ctor
+ var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typ);
+ var invars = new List<Bpl.Expr>();
+ invars.Add(locExpr);
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, invars, new List<Bpl.IdentifierExpr>()));
+
+ // Generate an assumption about the dynamic type of the just allocated object
+ this.StmtTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
+ this.sink.Heap.DynamicType(locExpr),
+ this.sink.FindOrCreateType(typ)
+ )
+ )
+ );
+
+ this.TranslatedExpressions.Push(locExpr);
+ }
+
#endregion
#region Translate Method Calls
@@ -729,6 +730,7 @@ namespace BytecodeTranslator
bool translationIntercepted= false;
ICompileTimeConstant constant= assignment.Source as ICompileTimeConstant;
// TODO move away phone related code from the translation, it would be better to have 2 or more translation phases
+ // NAVIGATION TODO maybe this will go away if I can handle it with stubs
if (PhoneCodeHelper.instance().PhonePlugin != null && PhoneCodeHelper.instance().PhoneNavigationToggled) {
IFieldReference target = assignment.Target.Definition as IFieldReference;
if (target != null && target.Name.Value == PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE) {
@@ -737,7 +739,6 @@ namespace BytecodeTranslator
TranslateHavocCurrentURI();
translationIntercepted = true;
}
-
StmtTraverser.StmtBuilder.Add(PhoneCodeHelper.instance().getAddNavigationCheck(sink));
}
}
@@ -1363,6 +1364,8 @@ namespace BytecodeTranslator
#endregion
*/
+
+ // TODO is this code actually needed at all? It seems that all this is already being done in the Statement traverser for the conditional
StatementTraverser thenStmtTraverser = this.StmtTraverser.factory.MakeStatementTraverser(this.sink, this.StmtTraverser.PdbReader, this.contractContext);
StatementTraverser elseStmtTraverser = this.StmtTraverser.factory.MakeStatementTraverser(this.sink, this.StmtTraverser.PdbReader, this.contractContext);
ExpressionTraverser thenExprTraverser = this.StmtTraverser.factory.MakeExpressionTraverser(this.sink, thenStmtTraverser, this.contractContext);
diff --git a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
index 026cf301..066d4cdf 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
@@ -49,8 +49,6 @@ namespace BytecodeTranslator.Phone {
delegateBody = anonDelegate.Body;
}
- // NAVIGATION TODO look for reachable method calls
-
// NAVIGATION TODO what if it has no body?
if (delegateBody != null) {
bool navigates= false, cancelsNav= false;
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
deleted file mode 100644
index 8bec1605..00000000
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
+++ /dev/null
@@ -1,33 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using TranslationPlugins;
-
-namespace BytecodeTranslator.Phone {
- class PhoneCodeWrapperWriter {
- private static Sink sink;
- public static void createCodeWrapper(Sink sink) {
- PhoneCodeWrapperWriter.sink = sink;
- /*
- * create Main procedure
- * - creates page instances, one per page -- this overapproximates as there may be more instances
- * - havoc'd loop drives controls via calls to driver
- *
- * create Driver procedure
- * - determine current page; for each page check if it is current or not
- * - call page driver accordingly
- *
- * create Page drivers
- * - one for each page
- * - havoc-ly determine control to stimulate
- * - check enabledness of control, stimulate by calling handler of chosen event if yes, nothing ig not
- * - possibly many events to handle
- * - might be slightly more efficient to nto return control until we know page navigation may have changed,
- * but this requires a lot of knowledge (ie, will the called method call NavigationService or not)
- */
- //createMainProcedure();
- }
- }
-}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4b5e205c..da0f401e 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -143,7 +143,6 @@ namespace BytecodeTranslator {
#endregion
try {
-
HeapFactory heap;
switch (options.heapRepresentation) {
case Options.HeapRepresentation.splitFields:
@@ -187,6 +186,7 @@ namespace BytecodeTranslator {
var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
+ #region Assemlies to translate (via cmd line)
modules = new List<IModule>();
var contractExtractors = new Dictionary<IUnit, IContractProvider>();
var pdbReaders = new Dictionary<IUnit, PdbReader>();
@@ -208,6 +208,9 @@ namespace BytecodeTranslator {
contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
pdbReaders.Add(module, pdbReader);
}
+ #endregion
+
+ #region Assemblies to translate (stubs)
if (stubAssemblies != null) {
foreach (var s in stubAssemblies) {
var module = host.LoadUnitFrom(s) as IModule;
@@ -242,23 +245,25 @@ namespace BytecodeTranslator {
pdbReaders.Add(module, pdbReader);
}
}
+ #endregion
+
if (modules.Count == 0) {
Console.WriteLine("No input assemblies to translate.");
return -1;
}
var primaryModule = modules[0];
+ TraverserFactory bctTraverserFactory;
+ if (wholeProgram) {
+ bctTraverserFactory = new WholeProgram();
+ } else {
+ bctTraverserFactory = new CLRSemantics();
+ }
- TraverserFactory traverserFactory;
- if (wholeProgram)
- traverserFactory = new WholeProgram();
- else
- traverserFactory = new CLRSemantics();
-
- Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);
+ Sink sink= new Sink(host, bctTraverserFactory, heapFactory, options, exemptionList, whiteList);
TranslationHelper.tmpVarCounter = 0;
MetadataTraverser translator;
- translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+ translator= bctTraverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
PhoneCodeHelper.initialize(host);
@@ -287,6 +292,10 @@ namespace BytecodeTranslator {
string outputFileName = primaryModule.Name + ".bpl";
callPostTranslationTraversers(modules, sink, phoneControlsConfigFile, outputFileName);
+ if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
+ finalizeNavigationAnalysisAndBoogieCode(phoneControlsConfigFile, sink, outputFileName);
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
@@ -294,6 +303,14 @@ namespace BytecodeTranslator {
return 0; // success
}
+ private static void finalizeNavigationAnalysisAndBoogieCode(string phoneControlsConfigFile, Sink sink, string outputFileName) {
+ outputBoogieTrackedControlConfiguration(phoneControlsConfigFile);
+ checkTransitivelyCalledBackKeyNavigations(modules);
+ createPhoneBoogieCallStubs(sink);
+ PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName);
+ outputBackKeyWarnings();
+ }
+
private static void callPostTranslationTraversers(List<IModule> modules, Sink sink, string phoneControlsConfigFile, string outputFileName) {
if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {
PhoneCodeHelper.instance().CreateFeedbackCallingMethods(sink);
@@ -310,81 +327,84 @@ namespace BytecodeTranslator {
traverser.Visit(modules);
}
+ }
- // NAVIGATION TODO: refactor warnings out of here
- if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
- string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");
- StreamWriter outputStream = new StreamWriter(outputConfigFile);
- PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream);
- outputStream.Close();
- PhoneCodeWrapperWriter.createCodeWrapper(sink);
-
- foreach (IMethodReference navMethod in PhoneCodeHelper.instance().KnownBackKeyHandlers) {
- // right now we traversed everything so we can see reachability
- IEnumerable<IMethodDefinition> indirects= PhoneCodeHelper.instance().getIndirectNavigators(modules, navMethod);
- if (indirects.Count() > 0) {
- ICollection<Tuple<IMethodReference, string>> targets = null;
- PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(navMethod.ContainingType, out targets);
- if (targets == null) {
- targets = new HashSet<Tuple<IMethodReference, string>>();
- }
- string indirectTargeting = "<unknown indirect navigation> via (";
- foreach (IMethodDefinition methDef in indirects) {
- indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";
- }
- indirectTargeting += ")";
- targets.Add(Tuple.Create<IMethodReference, string>(navMethod, indirectTargeting));
- PhoneCodeHelper.instance().BackKeyNavigatingOffenders[navMethod.ContainingType] = targets;
- }
+ private static void outputBoogieTrackedControlConfiguration(string phoneControlsConfigFile) {
+ string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");
+ StreamWriter outputStream = new StreamWriter(outputConfigFile);
+ PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream);
+ outputStream.Close();
+ }
- indirects = PhoneCodeHelper.instance().getIndirectCancellations(modules, navMethod);
- if (indirects.Count() > 0) {
- string indirectTargeting = "(";
- foreach (IMethodDefinition methDef in indirects) {
- indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";
+ private static void outputBackKeyWarnings() {
+ // NAVIGATION TODO for now I console this out
+ if (!PhoneCodeHelper.instance().OnBackKeyPressOverriden) {
+ Console.Out.WriteLine("No back navigation issues, OnBackKeyPress is not overriden");
+ } else if (PhoneCodeHelper.instance().BackKeyHandlerOverridenByUnknownDelegate) {
+ Console.Out.WriteLine("Back navigation ISSUE: BackKeyPress is overriden by unidentified delegate and may perform illegal navigation");
+ Console.Out.WriteLine("Offending pages:");
+ foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyUnknownDelegateOffenders) {
+ Console.WriteLine("\t" + type.ToString());
+ }
+ } else if (!PhoneCodeHelper.instance().BackKeyPressHandlerCancels && !PhoneCodeHelper.instance().BackKeyPressNavigates) {
+ Console.Out.WriteLine("No back navigation issues, BackKeyPress overrides do not alter navigation");
+ } else {
+ if (PhoneCodeHelper.instance().BackKeyPressNavigates) {
+ Console.Out.WriteLine("Back navigation ISSUE: back key press may navigate to pages not in backstack! From pages:");
+ foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyNavigatingOffenders.Keys) {
+ ICollection<Tuple<IMethodReference, string>> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[type];
+ Console.WriteLine("\t" + type.ToString() + " may navigate to ");
+ foreach (Tuple<IMethodReference, string> target in targets) {
+ Console.WriteLine("\t\t" + target.Item2 + " via " +
+ (target.Item1.Name == Dummy.Name ? "anonymous delegate" : target.Item1.ContainingType.ToString() + "." + target.Item1.Name.Value));
}
- indirectTargeting += ")";
- PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create<ITypeReference,string>(navMethod.ContainingType, indirectTargeting));
}
}
- foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {
- if (!PhoneCodeHelper.instance().isKnownBackKeyOverride(def))
- PhoneCodeHelper.instance().addHandlerStubCaller(sink, def);
+ if (PhoneCodeHelper.instance().BackKeyPressHandlerCancels) {
+ Console.Out.WriteLine("Back navigation ISSUE: back key press default behaviour may be cancelled! From pages:");
+ foreach (Tuple<ITypeReference, string> cancellation in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {
+ Console.WriteLine("\t" + cancellation.Item1.ToString() + " via " + cancellation.Item2);
+ }
}
- PhoneCodeHelper.instance().addNavigationUriHavocer(sink);
- PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName);
-
- // NAVIGATION TODO for now I console this out
- if (!PhoneCodeHelper.instance().OnBackKeyPressOverriden) {
- Console.Out.WriteLine("No back navigation issues, OnBackKeyPress is not overriden");
- } else if (PhoneCodeHelper.instance().BackKeyHandlerOverridenByUnknownDelegate) {
- Console.Out.WriteLine("Back navigation ISSUE: BackKeyPress is overriden by unidentified delegate and may perform illegal navigation");
- Console.Out.WriteLine("Offending pages:");
- foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyUnknownDelegateOffenders) {
- Console.WriteLine("\t" + type.ToString());
+ }
+ }
+
+ private static void createPhoneBoogieCallStubs(Sink sink) {
+ foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {
+ if (!PhoneCodeHelper.instance().isKnownBackKeyOverride(def))
+ PhoneCodeHelper.instance().addHandlerStubCaller(sink, def);
+ }
+ PhoneCodeHelper.instance().addNavigationUriHavocer(sink);
+ }
+
+ private static void checkTransitivelyCalledBackKeyNavigations(List<IModule> modules) {
+ foreach (IMethodReference navMethod in PhoneCodeHelper.instance().KnownBackKeyHandlers) {
+ // right now we traversed everything so we can see reachability
+ IEnumerable<IMethodDefinition> indirects = PhoneCodeHelper.instance().getIndirectNavigators(modules, navMethod);
+ if (indirects.Count() > 0) {
+ ICollection<Tuple<IMethodReference, string>> targets = null;
+ PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(navMethod.ContainingType, out targets);
+ if (targets == null) {
+ targets = new HashSet<Tuple<IMethodReference, string>>();
}
- } else if (!PhoneCodeHelper.instance().BackKeyPressHandlerCancels && !PhoneCodeHelper.instance().BackKeyPressNavigates) {
- Console.Out.WriteLine("No back navigation issues, BackKeyPress overrides do not alter navigation");
- } else {
- if (PhoneCodeHelper.instance().BackKeyPressNavigates) {
- Console.Out.WriteLine("Back navigation ISSUE: back key press may navigate to pages not in backstack! From pages:");
- foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyNavigatingOffenders.Keys) {
- ICollection<Tuple<IMethodReference,string>> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[type];
- Console.WriteLine("\t" + type.ToString() + " may navigate to ");
- foreach (Tuple<IMethodReference,string> target in targets) {
- Console.WriteLine("\t\t" + target.Item2 + " via " +
- (target.Item1.Name == Dummy.Name ? "anonymous delegate" : target.Item1.ContainingType.ToString() + "." + target.Item1.Name.Value));
- }
- }
+ string indirectTargeting = "<unknown indirect navigation> via (";
+ foreach (IMethodDefinition methDef in indirects) {
+ indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";
}
+ indirectTargeting += ")";
+ targets.Add(Tuple.Create<IMethodReference, string>(navMethod, indirectTargeting));
+ PhoneCodeHelper.instance().BackKeyNavigatingOffenders[navMethod.ContainingType] = targets;
+ }
- if (PhoneCodeHelper.instance().BackKeyPressHandlerCancels) {
- Console.Out.WriteLine("Back navigation ISSUE: back key press default behaviour may be cancelled! From pages:");
- foreach (Tuple<ITypeReference,string> cancellation in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {
- Console.WriteLine("\t" + cancellation.Item1.ToString() + " via " + cancellation.Item2);
- }
+ indirects = PhoneCodeHelper.instance().getIndirectCancellations(modules, navMethod);
+ if (indirects.Count() > 0) {
+ string indirectTargeting = "(";
+ foreach (IMethodDefinition methDef in indirects) {
+ indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";
}
+ indirectTargeting += ")";
+ PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create<ITypeReference, string>(navMethod.ContainingType, indirectTargeting));
}
}
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index f3481f43..fac00e42 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -20,6 +20,8 @@ using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
public abstract class TraverserFactory {
+ public int Priority { get; set; }
+
public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> sourceLocationProviders)