diff options
Diffstat (limited to 'BCT/BytecodeTranslator/Program.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 894 |
1 files changed, 0 insertions, 894 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs deleted file mode 100644 index 403067be..00000000 --- a/BCT/BytecodeTranslator/Program.cs +++ /dev/null @@ -1,894 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Linq;
-using System.IO;
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using System.Collections.Generic;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-using Microsoft.Cci.MutableContracts;
-
-using Bpl = Microsoft.Boogie;
-using System.Diagnostics.Contracts;
-using Microsoft.Cci.MutableCodeModel.Contracts;
-using TranslationPlugins;
-using BytecodeTranslator.Phone;
-using System.Text.RegularExpressions;
-using BytecodeTranslator.TranslationPlugins;
-using BytecodeTranslator.TranslationPlugins.BytecodeTranslator;
-using BytecodeTranslator.TranslationPlugins.PhoneTranslator;
-
-namespace BytecodeTranslator {
-
- public class Options : OptionParsing {
-
- [OptionDescription("The names of the assemblies to use as input", ShortForm = "a")]
- public List<string> assemblies = null;
-
- [OptionDescription("Break into debugger", ShortForm = "break")]
- public bool breakIntoDebugger = false;
-
- [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
- public bool captureState = false;
-
- [OptionDescription("Model exceptional control flow, (0: none, 1: explicit exceptions, 2: conservatively, default: 2)", ShortForm = "e")]
- public int modelExceptions = 2;
-
- [OptionDescription("Translation should be done for Get Me Here functionality, (default: false)", ShortForm = "gmh")]
- public bool getMeHere = false;
-
- [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
- public List<string> libpaths = new List<string>();
-
- public enum HeapRepresentation { splitFields, twoDInt, twoDBox, general }
- [OptionDescription("Heap representation to use", ShortForm = "heap")]
- public HeapRepresentation heapRepresentation = HeapRepresentation.general;
-
- [OptionDescription("Translate using whole-program assumptions", ShortForm = "whole")]
- public bool wholeProgram = false;
-
- [OptionDescription("Stub assembly", ShortForm = "s")]
- public List<string>/*?*/ stub = null;
-
- [OptionDescription("Phone translation controls configuration")]
- public string phoneControls = null;
-
- [OptionDescription("Add phone navigation code on translation. Requires /phoneControls. Default false", ShortForm = "wpnav")]
- public bool phoneNavigationCode= false;
-
- [OptionDescription("Add phone feedback code on translation. Requires /phoneControls. Default false", ShortForm = "wpfb")]
- public bool phoneFeedbackCode = false;
-
- [OptionDescription("File containing white/black list (optionally end file name with + for white list, - for black list, default is white list", ShortForm = "exempt")]
- public string exemptionFile = "";
-
- [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]
- public bool instrumentBranches = false;
-
- [OptionDescription("Add free ensures that express heap monotonicity", ShortForm = "heapM")]
- public bool monotonicHeap = false;
-
- public enum Dereference { Assert, Assume, None, }
- [OptionDescription("Assert/Assume on all object dereferences", ShortForm = "deref")]
- public Dereference dereference = Dereference.Assume;
-
- }
-
- public class BCT {
-
- public static IMetadataHost Host;
-
- static int Main(string[] args)
- {
- int errorReturnValue = -1;
-
- #region Parse options and check for errors
- var options = new Options();
- options.Parse(args);
- if (options.HelpRequested) {
- options.PrintOptions("");
- return errorReturnValue;
- }
- if (options.HasErrors) {
- options.PrintErrorsAndExit(Console.Out);
- }
- if (!String.IsNullOrWhiteSpace(options.exemptionFile)) {
- string fileName = options.exemptionFile;
- var c = fileName[fileName.Length - 1];
- if (c == '+' || c == '-') fileName = options.exemptionFile.Remove(fileName.Length - 1);
- if (!File.Exists(fileName)) {
- Console.WriteLine("Specified exemption file '{0}' not found.", fileName);
- }
- }
- if (options.stub != null) {
- Console.WriteLine("/s is no longer used to specify stub assemblies");
- return errorReturnValue;
- }
-
- if (options.modelExceptions == 1 && !options.wholeProgram) {
- Console.WriteLine("can specify a precise modeling of exceptions only when doing whole program analysis");
- return errorReturnValue;
- }
-
- if (options.breakIntoDebugger) {
- System.Diagnostics.Debugger.Break();
- }
-
- #endregion
-
- var assemblyNames = options.assemblies;
- if (assemblyNames == null || assemblyNames.Count == 0) {
- assemblyNames = new List<string>();
- foreach (var g in options.GeneralArguments) {
- assemblyNames.Add(g);
- }
- }
-
- #region If an exclusion file has been specified, read in each line as a regular expression
- List<Regex> exemptionList = null;
- bool whiteList = false;
- if (!String.IsNullOrWhiteSpace(options.exemptionFile)) {
- int i = 0;
- exemptionList = new List<Regex>();
- string fileName = options.exemptionFile;
- var c = fileName[fileName.Length - 1];
- whiteList = true;
- if (c == '+' || c == '-') {
- fileName = options.exemptionFile.Remove(fileName.Length - 1);
- if (c == '-') whiteList = false;
- }
- try {
- // Create an instance of StreamReader to read from a file.
- // The using statement also closes the StreamReader.
- using (StreamReader sr = new StreamReader(fileName)) {
- String line;
- // Read and display lines from the file until the end of
- // the file is reached.
- while ((line = sr.ReadLine()) != null) {
- exemptionList.Add(new Regex(line));
- i++;
- }
- //Console.WriteLine("Read {0} lines from the exclusion file '{1}'.",
- // i, options.exemptionFile);
- }
- } catch (Exception e) {
- Console.WriteLine("Something went wrong reading the exclusion file '{0}'; read in {1} lines, continuing processing.",
- fileName, i);
- Console.WriteLine(e.Message);
- }
- }
- #endregion
-
- try {
- HeapFactory heap;
- switch (options.heapRepresentation) {
- case Options.HeapRepresentation.splitFields:
- heap = new SplitFieldsHeap();
- break;
- case Options.HeapRepresentation.general:
- heap = new GeneralHeap();
- break;
- default:
- Console.WriteLine("Unknown setting for /heap");
- return 1;
- }
-
- if ((options.phoneFeedbackCode || options.phoneNavigationCode) && (options.phoneControls == null || options.phoneControls == "")) {
- Console.WriteLine("Options /phoneNavigationCode and /phoneFeedbackCode need /phoneControls option set.");
- return 1;
- }
-
- var pgm = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);
- var fileName = assemblyNames[0];
- fileName = Path.GetFileNameWithoutExtension(fileName);
- string outputFileName = fileName + ".bpl";
- Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter("_" + outputFileName);
- Prelude.Emit(writer);
- pgm.Emit(writer);
- writer.Close();
- return Inline(outputFileName);
- } catch (Exception e) { // swallow everything and just return an error code
- Console.WriteLine("The byte-code translator failed: {0}", e.Message);
- // Console.WriteLine("Stack trace: {0}", e.StackTrace);
- return -1;
- }
- }
-
- private static List<IModule> modules;
-
- public static int Inline(string bplFileName) {
- Bpl.CommandLineOptions options = new Bpl.CommandLineOptions();
- Bpl.CommandLineOptions.Install(options);
- Bpl.CommandLineOptions.Clo.DoModSetAnalysis = true;
- Bpl.Program program;
- string _bplFileName = "_" + bplFileName;
-
- Bpl.Parser.Parse(_bplFileName, new List<string>(), out program);
- int errorCount = program.Resolve();
- if (errorCount != 0) {
- Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, _bplFileName);
- return -1;
- }
- errorCount = program.Typecheck();
- if (errorCount != 0) {
- Console.WriteLine("{0} type checking errors detected in {1}", errorCount, _bplFileName);
- return -1;
- }
- bool inline = false;
- foreach (var d in program.TopLevelDeclarations) {
- if (d.FindExprAttribute("inline") != null) {
- inline = true;
- }
- }
- if (inline) {
- foreach (var d in program.TopLevelDeclarations) {
- var impl = d as Bpl.Implementation;
- if (impl != null) {
- impl.OriginalBlocks = impl.Blocks;
- impl.OriginalLocVars = impl.LocVars;
- }
- }
- foreach (var d in program.TopLevelDeclarations) {
- var impl = d as Bpl.Implementation;
- if (impl != null && !impl.SkipVerification) {
- Bpl.Inliner.ProcessImplementation(program, impl);
- }
- }
- foreach (var d in program.TopLevelDeclarations) {
- var impl = d as Bpl.Implementation;
- if (impl != null) {
- impl.OriginalBlocks = null;
- impl.OriginalLocVars = null;
- }
- }
- }
- Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(bplFileName);
- options.PrintInstrumented = true;
- program.Emit(writer);
- writer.Close();
- return 0;
- }
-
- public static int TranslateAssemblyAndWriteOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
- Contract.Requires(assemblyNames != null);
- Contract.Requires(heapFactory != null);
- try {
- var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList);
- var fileName = assemblyNames[0];
- fileName = Path.GetFileNameWithoutExtension(fileName);
- string outputFileName = fileName + ".bpl";
- using (var writer = new Microsoft.Boogie.TokenTextWriter(outputFileName)) {
- Prelude.Emit(writer);
- pgm.Emit(writer);
- writer.Close();
- }
- return 0; // success
- } catch (Exception e) { // swallow everything and just return an error code
- Console.WriteLine("The byte-code translator failed: {0}", e.Message);
- // Console.WriteLine("Stack trace: {0}", e.StackTrace);
- return -1;
- }
- }
-
- public static Bpl.Program/*?*/ TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
- Contract.Requires(assemblyNames != null);
- Contract.Requires(heapFactory != null);
-
- var libPaths = options.libpaths;
- var wholeProgram = options.wholeProgram;
- var/*?*/ stubAssemblies = options.stub;
- var phoneControlsConfigFile = options.phoneControls;
- var doPhoneNav = options.phoneNavigationCode;
- var doPhoneFeedback = options.phoneFeedbackCode;
-
- var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
- Host = host;
-
- Bpl.CommandLineOptions.Install(new Bpl.CommandLineOptions());
-
- #region Assemlies to translate (via cmd line)
- modules = new List<IModule>();
- var contractExtractors = new Dictionary<IUnit, IContractProvider>();
- var pdbReaders = new Dictionary<IUnit, PdbReader>();
- #region Load *all* of the assemblies before doing anything else so that they can all vote on unification matters
- foreach (var a in assemblyNames) {
- var module = host.LoadUnitFrom(a) as IModule;
- if (module == null || module == Dummy.Module || module == Dummy.Assembly) {
- Console.WriteLine(a + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");
- Console.WriteLine("Skipping it, continuing with other input assemblies");
- continue;
- }
- modules.Add(module);
- }
- #endregion
- #region Decompile all of the assemblies
- var decompiledModules = new List<IModule>();
- foreach (var m in modules) {
- PdbReader/*?*/ pdbReader = null;
- string pdbFile = Path.ChangeExtension(m.Location, "pdb");
- if (File.Exists(pdbFile)) {
- Stream pdbStream = File.OpenRead(pdbFile);
- pdbReader = new PdbReader(pdbStream, host);
- }
- var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;
- // The decompiler does not turn calls to Assert/Assume into Code Model nodes
- m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);
- decompiledModules.Add(m2);
- host.RegisterAsLatest(m2);
- contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));
- pdbReaders.Add(m2, pdbReader);
- }
- modules = decompiledModules;
- #endregion
- #endregion
-
- #region Assemblies to translate (stubs)
- if (stubAssemblies != null) {
- foreach (var s in stubAssemblies) {
- var module = host.LoadUnitFrom(s) as IModule;
- if (module == null || module == Dummy.Module || module == Dummy.Assembly) {
- Console.WriteLine(s + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");
- Console.WriteLine("Skipping it, continuing with other input assemblies");
- }
- PdbReader/*?*/ pdbReader = null;
- string pdbFile = Path.ChangeExtension(module.Location, "pdb");
- if (File.Exists(pdbFile)) {
- Stream pdbStream = File.OpenRead(pdbFile);
- pdbReader = new PdbReader(pdbStream, host);
- }
- module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
-
- var copier = new CodeDeepCopier(host);
- var mutableModule = copier.Copy(module);
-
- var mscorlib = TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType);
-
- //var mutator = new ReparentModule(host, mscorlib, mutableModule);
- //module = mutator.Rewrite(mutableModule);
- //modules.Add(Tuple.Create(module, pdbReader));
-
- RewriteUnitReferences renamer = new RewriteUnitReferences(host, mutableModule);
- var mscorlibAssembly = (IAssembly)mscorlib;
- renamer.targetAssembly = mscorlibAssembly;
- renamer.originalAssemblyIdentity = mscorlibAssembly.AssemblyIdentity;
- renamer.RewriteChildren(mutableModule);
- modules.Add((IModule)mutableModule);
- contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
- pdbReaders.Add(module, pdbReader);
- }
- }
- #endregion
-
- if (modules.Count == 0) {
- throw new TranslationException("No input assemblies to translate.");
- }
-
- var primaryModule = modules[0];
- Sink sink= new Sink(host, heapFactory, options, exemptionList, whiteList);
- TranslationHelper.tmpVarCounter = 0;
-
- // TODO move away, get all plugin and translators from a config file or alike
- #region Plugged translators
- List<Translator> translatorsPlugged = new List<Translator>();
- ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin(wholeProgram);
- Translator bcTranslator = bctPlugin.getTranslator(sink, contractExtractors, pdbReaders);
- translatorsPlugged.Add(bcTranslator);
-
- if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- // TODO this should be part of the translator initialziation
- PhoneCodeHelper.initialize(host);
- PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
-
- if (doPhoneNav) {
- // TODO this should be part of the translator initialziation
- PhoneCodeHelper.instance().PhoneNavigationToggled = true;
-
- ITranslationPlugin phoneInitPlugin = new PhoneInitializationPlugin();
- ITranslationPlugin phoneNavPlugin = new PhoneNavigationPlugin();
- Translator phInitTranslator = phoneInitPlugin.getTranslator(sink, contractExtractors, pdbReaders);
- Translator phNavTranslator = phoneNavPlugin.getTranslator(sink, contractExtractors, pdbReaders);
- translatorsPlugged.Add(phInitTranslator);
- translatorsPlugged.Add(phNavTranslator);
- }
-
- if (doPhoneFeedback) {
- // TODO this should be part of the translator initialziation
- PhoneCodeHelper.instance().PhoneFeedbackToggled = true;
-
- ITranslationPlugin phoneFeedbackPlugin = new PhoneFeedbackPlugin();
- Translator phFeedbackTranslator = phoneFeedbackPlugin.getTranslator(sink, contractExtractors, pdbReaders);
- translatorsPlugged.Add(phFeedbackTranslator);
- }
- }
- #endregion
- sink.TranslationPlugins = translatorsPlugged;
-
- /*
- if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- // TODO send this all way to initialization of phone plugin translator
- PhoneCodeHelper.initialize(host);
- PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
-
- // TODO these parameters will eventually form part of plugin configuration
- if (doPhoneNav) {
- PhoneCodeHelper.instance().PhoneNavigationToggled = true;
- PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);
- initTr.InjectPhoneCodeAssemblies(modules);
- PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);
- navTr.InjectPhoneCodeAssemblies(modules);
- }
-
- if (doPhoneFeedback) {
- PhoneCodeHelper.instance().PhoneFeedbackToggled = true;
- PhoneControlFeedbackMetadataTraverser fbMetaDataTraverser= new PhoneControlFeedbackMetadataTraverser(host);
- fbMetaDataTraverser.Visit(modules);
- }
- }
- */
-
- // TODO replace the whole translation by a translator initialization and an orchestrator calling back for each element
- // TODO for the current BC translator it will possibly just implement onMetadataElement(IModule)
- // TODO refactor this away, handle priorities between plugged translators
- IOrderedEnumerable<Translator> prioritizedTranslators = translatorsPlugged.OrderBy(t => t.getPriority());
- foreach (Translator t in prioritizedTranslators) {
- t.initialize();
- if (t.isOneShot())
- t.TranslateAssemblies(modules);
- }
-
- foreach (var pair in sink.delegateTypeToDelegates.Values) {
- CreateDispatchMethod(sink, pair.Item1, pair.Item2);
- }
-
- string outputFileName = primaryModule.Name + ".bpl";
- callPostTranslationTraversers(modules, sink, phoneControlsConfigFile, outputFileName);
- if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
- finalizeNavigationAnalysisAndBoogieCode(phoneControlsConfigFile, sink, outputFileName);
- }
-
- //sink.CreateIdentifierCorrespondenceTable(primaryModule.Name.Value);
-
- //var rc = new Bpl.ResolutionContext((Bpl.IErrorSink)null);
- //foreach (var decl in sink.TranslatedProgram.TopLevelDeclarations) {
- // decl.Register(rc);
- //}
- //sink.TranslatedProgram.Resolve(rc);
- //var goodDecls = new List<Bpl.Declaration>();
- //var tc = new Bpl.TypecheckingContext(null);
- //foreach (var decl in sink.TranslatedProgram.TopLevelDeclarations) {
- // var impl = decl as Bpl.Implementation;
- // if (impl == null) {
- // goodDecls.Add(decl);
- // continue;
- // }
- // try {
- // //var tc = new Bpl.TypecheckingContext(null);
- // impl.Typecheck(tc);
- // goodDecls.Add(impl);
- // } catch {
- // Console.WriteLine("Deleting implementation for: " + impl.Name);
- // // nothing to do, just continue
- // }
- //}
- //sink.TranslatedProgram.TopLevelDeclarations = goodDecls;
- return sink.TranslatedProgram;
- }
-
-
- 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);
- }
-
- if (PhoneCodeHelper.instance().PhoneFeedbackToggled || PhoneCodeHelper.instance().PhoneNavigationToggled) {
- PhoneMethodInliningMetadataTraverser inlineTraverser =
- new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance());
- inlineTraverser.findAllMethodsToInline(modules);
- PhoneCodeHelper.updateInlinedMethods(sink, inlineTraverser.getMethodsToInline());
- System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
-
- PhoneBackKeyCallbackTraverser traverser = new PhoneBackKeyCallbackTraverser(sink.host);
- traverser.Traverse(modules);
-
- }
- }
-
- private static void outputBoogieTrackedControlConfiguration(string phoneControlsConfigFile) {
- string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");
- StreamWriter outputStream = new StreamWriter(outputConfigFile);
- PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream);
- outputStream.Close();
- }
-
- 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));
- }
- }
- }
-
- 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);
- }
- }
- }
- }
-
- 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>>();
- }
- 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;
- }
-
- 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));
- }
- }
- }
-
- private static string NameUpToFirstPeriod(string name) {
- var i = name.IndexOf('.');
- if (i == -1)
- return name;
- else
- return name.Substring(0, i);
- }
-
- private class ReparentModule : CodeRewriter {
- private IUnit targetUnit;
- private IUnit sourceUnit;
- public ReparentModule(IMetadataHost host, IUnit targetUnit, IUnit sourceUnit)
- : base(host) {
- this.targetUnit = targetUnit;
- this.sourceUnit = sourceUnit;
- }
-
- public override void RewriteChildren(RootUnitNamespace rootUnitNamespace) {
- if (rootUnitNamespace.Unit.UnitIdentity.Equals(this.sourceUnit.UnitIdentity))
- rootUnitNamespace.Unit = this.targetUnit;
- base.RewriteChildren(rootUnitNamespace);
- }
- }
-
- private static Bpl.IfCmd BuildIfCmd(Bpl.Expr b, Bpl.Cmd cmd, Bpl.IfCmd ifCmd) {
- Bpl.StmtListBuilder ifStmtBuilder;
- ifStmtBuilder = new Bpl.StmtListBuilder();
- ifStmtBuilder.Add(cmd);
- return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), ifCmd, null);
- }
- private static Bpl.IfCmd BuildReturnCmd(Bpl.Expr b) {
- Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
- ifStmtBuilder.Add(new Bpl.ReturnCmd(b.tok));
- return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);
- }
- private static void BuildAssignment(Sink sink, Bpl.StmtListBuilder stmtBuilder, List<Bpl.Variable> lvars, List<Bpl.Variable> rvars) {
- for (int i = 0; i < lvars.Count; i++) {
- Bpl.Variable lvar = lvars[i];
- Bpl.Type ltype = lvar.TypedIdent.Type;
- Bpl.Variable rvar = rvars[i];
- Bpl.Type rtype = rvar.TypedIdent.Type;
- Bpl.IdentifierExpr lexpr = Bpl.Expr.Ident(lvar);
- Bpl.Expr rexpr = Bpl.Expr.Ident(rvar);
- if (rtype == ltype) {
- // do nothing
- } else if (ltype == sink.Heap.UnionType) {
- rexpr = sink.Heap.ToUnion(Bpl.Token.NoToken, rtype, rexpr);
- }
- else if (rtype == sink.Heap.UnionType) {
- rexpr = sink.Heap.FromUnion(Bpl.Token.NoToken, ltype, rexpr);
- }
- else {
- System.Diagnostics.Debug.Assert(false);
- }
- stmtBuilder.Add(TranslationHelper.BuildAssignCmd(lexpr, rexpr));
- }
- }
-
- private static void GenerateInAndOutExprs(Bpl.Expr e, Bpl.VariableSeq invars, Bpl.VariableSeq outvars, out Bpl.ExprSeq inExprs, out Bpl.IdentifierExprSeq outExprs) {
- inExprs = new Bpl.ExprSeq();
- inExprs.Add(e);
- for (int i = 1; i < invars.Length; i++) {
- Bpl.Variable f = invars[i];
- inExprs.Add(Bpl.Expr.Ident(f));
- }
- outExprs = new Bpl.IdentifierExprSeq();
- foreach (Bpl.Formal f in outvars) {
- outExprs.Add(Bpl.Expr.Ident(f));
- }
- }
-
- private static void CreateDispatchMethod(Sink sink, ITypeDefinition type, HashSet<IMethodDefinition> delegates) {
- Contract.Assert(type.IsDelegate);
- IMethodDefinition invokeMethod = null;
- foreach (IMethodDefinition m in type.Methods) {
- if (m.Name.Value == "Invoke") {
- invokeMethod = m;
- break;
- }
- }
-
- try {
- IMethodDefinition unspecializedInvokeMethod = Sink.Unspecialize(invokeMethod).ResolvedMethod;
- Bpl.Procedure invokeProcedure = (Bpl.Procedure) sink.FindOrCreateProcedure(unspecializedInvokeMethod).Decl;
- invokeProcedure.AddAttribute("inline", Bpl.Expr.Literal(1));
- var invars = invokeProcedure.InParams;
- var outvars = invokeProcedure.OutParams;
-
- Bpl.IToken token = invokeMethod.Token();
-
- Bpl.Formal delegateVariable = new Bpl.Formal(token, new Bpl.TypedIdent(token, "delegate", sink.Heap.DelegateType), true);
- Bpl.VariableSeq dispatchProcInvars = new Bpl.VariableSeq();
- List<Bpl.Variable> dispatchProcInExprs = new List<Bpl.Variable>();
- dispatchProcInvars.Add(delegateVariable);
- for (int i = 1; i < invars.Length; i++) {
- Bpl.Variable v = invars[i];
- Bpl.Formal f = new Bpl.Formal(token, new Bpl.TypedIdent(token, v.Name, v.TypedIdent.Type), true);
- dispatchProcInvars.Add(f);
- dispatchProcInExprs.Add(f);
- }
- Bpl.VariableSeq dispatchProcOutvars = new Bpl.VariableSeq();
- List<Bpl.Variable> dispatchProcOutExprs = new List<Bpl.Variable>();
- foreach (Bpl.Variable v in outvars) {
- Bpl.Formal f = new Bpl.Formal(token, new Bpl.TypedIdent(token, v.Name, v.TypedIdent.Type), false);
- dispatchProcOutvars.Add(f);
- dispatchProcOutExprs.Add(f);
- }
- Bpl.Procedure dispatchProcedure =
- new Bpl.Procedure(token,
- "DispatchOne." + invokeProcedure.Name,
- new Bpl.TypeVariableSeq(),
- dispatchProcInvars,
- dispatchProcOutvars,
- new Bpl.RequiresSeq(),
- new Bpl.IdentifierExprSeq(),
- new Bpl.EnsuresSeq());
- dispatchProcedure.AddAttribute("inline", Bpl.Expr.Literal(1));
- sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProcedure);
-
- Bpl.LocalVariable method = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int));
- Bpl.LocalVariable receiver = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "receiver", sink.Heap.RefType));
- Bpl.LocalVariable typeParameter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "typeParameter", sink.Heap.TypeType));
- Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
- localVariables.Add(method);
- localVariables.Add(receiver);
- localVariables.Add(typeParameter);
-
- Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);
- int localCounter = 0;
- foreach (IMethodDefinition defn in delegates) {
- Sink.ProcedureInfo delegateProcedureInfo = sink.FindOrCreateProcedure(defn);
- Bpl.Procedure delegateProcedure = (Bpl.Procedure) delegateProcedureInfo.Decl;
- Bpl.Formal thisVariable = delegateProcedureInfo.ThisVariable;
- int numArguments = defn.ParameterCount;
-
- List<Bpl.Variable> tempInputs = new List<Bpl.Variable>();
- List<Bpl.Variable> tempOutputs = new List<Bpl.Variable>();
-
- for (int i = 0; i < defn.ParameterCount; i++) {
- Bpl.Variable v = delegateProcedure.InParams[(thisVariable == null ? 0 : 1) + i];
- Bpl.LocalVariable localVariable = new Bpl.LocalVariable(Bpl.Token.NoToken,
- new Bpl.TypedIdent(Bpl.Token.NoToken, "local" + localCounter++, v.TypedIdent.Type));
- localVariables.Add(localVariable);
- tempInputs.Add(localVariable);
- }
-
- for (int i = 0; i < delegateProcedure.OutParams.Length; i++) {
- Bpl.Variable v = delegateProcedure.OutParams[i];
- Bpl.LocalVariable localVariable = new Bpl.LocalVariable(Bpl.Token.NoToken,
- new Bpl.TypedIdent(Bpl.Token.NoToken, "local" + localCounter++, v.TypedIdent.Type));
- localVariables.Add(localVariable);
- tempOutputs.Add(localVariable);
- }
-
- Bpl.ExprSeq ins = new Bpl.ExprSeq();
- Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
- if (!defn.IsStatic)
- ins.Add(Bpl.Expr.Ident(receiver));
- for (int i = 0; i < tempInputs.Count; i++) {
- ins.Add(Bpl.Expr.Ident(tempInputs[i]));
- }
- if (defn.IsGeneric) {
- for (int i = 0; i < defn.GenericParameterCount; i++) {
- ins.Add(new Bpl.NAryExpr(Bpl.Token.NoToken,
- new Bpl.FunctionCall(sink.FindOrCreateTypeParameterFunction(i)),
- new Bpl.ExprSeq(Bpl.Expr.Ident(typeParameter))));
- }
- }
- if (defn.IsStatic) {
- int numTypeParameters = Sink.ConsolidatedGenericParameterCount(defn.ContainingType);
- for (int i = 0; i < numTypeParameters; i++) {
- ins.Add(new Bpl.NAryExpr(Bpl.Token.NoToken,
- new Bpl.FunctionCall(sink.FindOrCreateTypeParameterFunction(i)),
- new Bpl.ExprSeq(Bpl.Expr.Ident(typeParameter))));
- }
- }
- for (int i = 0; i < tempOutputs.Count; i++) {
- outs.Add(Bpl.Expr.Ident(tempOutputs[i]));
- }
- Bpl.Constant c = sink.FindOrCreateDelegateMethodConstant(defn);
- Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c));
- Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
- System.Diagnostics.Debug.Assert(tempInputs.Count == dispatchProcInExprs.Count);
- if (tempInputs.Count > 0) {
- BuildAssignment(sink, ifStmtBuilder, tempInputs, dispatchProcInExprs);
- }
- ifStmtBuilder.Add(EmitDummySourceContext());
- ifStmtBuilder.Add(new Bpl.CallCmd(token, delegateProcedure.Name, ins, outs));
- System.Diagnostics.Debug.Assert(tempOutputs.Count == dispatchProcOutExprs.Count);
- if (tempOutputs.Count > 0) {
- BuildAssignment(sink, ifStmtBuilder, dispatchProcOutExprs, tempOutputs);
- }
- ifCmd = new Bpl.IfCmd(bexpr.tok, bexpr, ifStmtBuilder.Collect(bexpr.tok), ifCmd, null);
- }
- Bpl.StmtListBuilder stmtBuilder = new Bpl.StmtListBuilder();
- stmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(method),
- sink.ReadMethod(Bpl.Expr.Ident(delegateVariable))));
- stmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(receiver),
- sink.ReadReceiver(Bpl.Expr.Ident(delegateVariable))));
- stmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(typeParameter),
- sink.ReadTypeParameters(Bpl.Expr.Ident(delegateVariable))));
- stmtBuilder.Add(ifCmd);
-
- Bpl.Implementation dispatchImpl =
- new Bpl.Implementation(token,
- dispatchProcedure.Name,
- new Bpl.TypeVariableSeq(),
- dispatchProcedure.InParams,
- dispatchProcedure.OutParams,
- localVariables,
- stmtBuilder.Collect(token)
- );
- dispatchImpl.Proc = dispatchProcedure;
- sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchImpl);
-
- Bpl.ExprSeq inExprs;
- Bpl.IdentifierExprSeq outExprs;
-
- Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", sink.Heap.DelegateMultisetType));
- Bpl.LocalVariable d = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "d", sink.Heap.DelegateType));
- Bpl.LocalVariable all = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "all", sink.Heap.DelegateMultisetType));
-
- Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder();
- implStmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Neq(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(sink.Heap.NullRef))));
- GenerateInAndOutExprs(sink.ReadDelegate(Bpl.Expr.Ident(invars[0])), invars, outvars, out inExprs, out outExprs);
- implStmtBuilder.Add(new Bpl.CallCmd(token, dispatchProcedure.Name, inExprs, outExprs));
- implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(all), sink.ReadDelegateMultiset(Bpl.Expr.Ident(invars[0]))));
- implStmtBuilder.Add(
- TranslationHelper.BuildAssignCmd(
- Bpl.Expr.Ident(iter),
- new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(sink.Heap.MultisetSingleton), new Bpl.ExprSeq(sink.ReadDelegate(Bpl.Expr.Ident(invars[0]))))));
-
- Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder();
- whileStmtBuilder.Add(BuildReturnCmd(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(iter), Bpl.Expr.Ident(all))));
- whileStmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, Bpl.Expr.Select(new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(sink.Heap.MultisetMinus), new Bpl.ExprSeq(Bpl.Expr.Ident(all), Bpl.Expr.Ident(iter))), Bpl.Expr.Ident(d)), new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0)))));
-
- whileStmtBuilder.Add(EmitDummySourceContext());
- GenerateInAndOutExprs(Bpl.Expr.Ident(d), invars, outvars, out inExprs, out outExprs);
- whileStmtBuilder.Add(new Bpl.CallCmd(token, dispatchProcedure.Name, inExprs, outExprs));
- whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(sink.Heap.MultisetPlus), new Bpl.ExprSeq(Bpl.Expr.Ident(iter), new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(sink.Heap.MultisetSingleton), new Bpl.ExprSeq(Bpl.Expr.Ident(d)))))));
- whileStmtBuilder.Add(new Bpl.HavocCmd(Bpl.Token.NoToken, new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(d))));
- Bpl.WhileCmd whileCmd = new Bpl.WhileCmd(token, Bpl.Expr.True, new List<Bpl.PredicateCmd>(), whileStmtBuilder.Collect(token));
-
- implStmtBuilder.Add(whileCmd);
-
- Bpl.Implementation impl =
- new Bpl.Implementation(token,
- invokeProcedure.Name,
- new Bpl.TypeVariableSeq(),
- invars,
- outvars,
- new Bpl.VariableSeq(iter, d, all),
- implStmtBuilder.Collect(token)
- );
- impl.Proc = invokeProcedure;
- sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
- } catch (TranslationException te) {
- throw new NotImplementedException(te.ToString());
- } catch {
- throw;
- } finally {
- // Maybe this is a good place to add the procedure to the toplevel declarations
- }
- }
-
- private static Bpl.AssertCmd EmitDummySourceContext() {
- string fileName = "BCTAutoGenerated";
- int lineNumber = 0;
- var tok = Bpl.Token.NoToken;
- var attrib = new Bpl.QKeyValue(tok, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);
- attrib = new Bpl.QKeyValue(tok, "sourceFile", new List<object> { fileName }, attrib);
- return new Bpl.AssertCmd(tok, Bpl.Expr.True, attrib);
- }
-
- private class RewriteUnitReferences : MetadataRewriter {
- private UnitIdentity sourceUnitIdentity = null;
- internal IAssembly/*?*/ targetAssembly = null;
- internal AssemblyIdentity/*?*/ originalAssemblyIdentity = null;
-
- Dictionary<uint, bool> internedKeys = new Dictionary<uint, bool>();
-
- public RewriteUnitReferences(IMetadataHost host, Module sourceUnit)
- : base(host) {
- this.sourceUnitIdentity = sourceUnit.UnitIdentity;
- }
-
- public override IModuleReference Rewrite(IModuleReference moduleReference) {
- if (this.sourceUnitIdentity.Equals(moduleReference.UnitIdentity)) {
- return this.targetAssembly;
- }
- return base.Rewrite(moduleReference);
- }
- public override IAssemblyReference Rewrite(IAssemblyReference assemblyReference) {
- if (this.sourceUnitIdentity.Equals(assemblyReference.UnitIdentity)) {
- return this.targetAssembly;
- }
- return base.Rewrite(assemblyReference);
- }
-
- }
-
- }
-
-}
|