diff --git a/Foxtrot/Foxtrot/Documentation/GenerateDocumentationFromPDB.cs b/Foxtrot/Foxtrot/Documentation/GenerateDocumentationFromPDB.cs index 3a304b33..ac3576e1 100644 --- a/Foxtrot/Foxtrot/Documentation/GenerateDocumentationFromPDB.cs +++ b/Foxtrot/Foxtrot/Documentation/GenerateDocumentationFromPDB.cs @@ -25,18 +25,26 @@ namespace Microsoft.Contracts.Foxtrot { public class GenerateDocumentationFromPDB : Inspector { - private int tabWidth; + readonly Func sourceFileLocator; + readonly int tabWidth; + readonly bool writeOutput; + readonly ContractNodes contracts; private int tabStops; - private bool writeOutput; - private ContractNodes contracts; - public GenerateDocumentationFromPDB(ContractNodes contracts) : this(contracts, 2, false) + public GenerateDocumentationFromPDB(ContractNodes contracts) + : this(contracts, null) { } - public GenerateDocumentationFromPDB(ContractNodes contracts, int tabWidth, bool writeOutput) + public GenerateDocumentationFromPDB(ContractNodes contracts, Func sourceFileLocator) + : this(contracts, sourceFileLocator, 2, false) + { + } + + public GenerateDocumentationFromPDB(ContractNodes contracts, Func sourceFileLocator, int tabWidth, bool writeOutput) { this.contracts = contracts; + this.sourceFileLocator = sourceFileLocator; this.tabWidth = tabWidth; this.tabStops = 0; this.writeOutput = writeOutput; @@ -798,7 +806,13 @@ private SourceDocument GetDocument(Document doc) SourceDocument result; if (!sourceTexts.TryGetValue(sourceName, out result)) { - result = new SourceDocument(sourceName); + var sourceFilePath = sourceName; + if (sourceFileLocator != null) + { + sourceFilePath = sourceFileLocator(sourceFilePath); + } + + result = new SourceDocument(sourceFilePath); sourceTexts.Add(sourceName, result); } diff --git a/Microsoft.Research/ClousotMain/ClousotMain.cs b/Microsoft.Research/ClousotMain/ClousotMain.cs index 722f1cac..94cac04b 100644 --- a/Microsoft.Research/ClousotMain/ClousotMain.cs +++ b/Microsoft.Research/ClousotMain/ClousotMain.cs @@ -911,7 +911,7 @@ int InternalAnalyze() foreach (string assembly in options.Assemblies) { Assembly assem; - if (!this.driver.MetaDataDecoder.TryLoadAssembly(assembly, assemblyCache, this.output.EmitError, out assem, options.IsLegacyAssemblyMode, options.reference, options.extractSourceText)) + if (!this.driver.MetaDataDecoder.TryLoadAssembly(assembly, assemblyCache, this.output.EmitError, out assem, options.IsLegacyAssemblyMode, options.reference, options.extractSourceText, GetSourceFileLocator())) { output.WriteLine("Cannot load assembly '{0}'", assembly); this.options.AddError(); @@ -1345,7 +1345,7 @@ private void PopulateContractAssemblies(IOutputResults output) foreach (string contractAssembly in options.ContractAssemblies) { Assembly assem; - if (!driver.MetaDataDecoder.TryLoadAssembly(contractAssembly, assemblyCache, null, out assem, this.options.IsLegacyAssemblyMode, this.options.reference, this.options.extractSourceText)) + if (!driver.MetaDataDecoder.TryLoadAssembly(contractAssembly, assemblyCache, null, out assem, this.options.IsLegacyAssemblyMode, this.options.reference, this.options.extractSourceText, null)) { output.WriteLine("Cannot load contract assembly '{0}'", contractAssembly); options.AddError(); @@ -3441,6 +3441,26 @@ public Unit Accept(IMethodCodeProvider + diff --git a/Microsoft.Research/ClousotMain/Options.cs b/Microsoft.Research/ClousotMain/Options.cs index 24e9ed6b..35115765 100644 --- a/Microsoft.Research/ClousotMain/Options.cs +++ b/Microsoft.Research/ClousotMain/Options.cs @@ -360,6 +360,14 @@ public void PrintUsage(TextWriter output) [OptionDescription("Extract the source text for the contracts")] public bool extractSourceText = true; + [OptionDescription("Paths to source files")] + [DoNotHashInCache] + public List sourcePaths = new List(); + + [OptionDescription("Alternative paths to search for source files")] + [DoNotHashInCache] + public List alternativeSourcePaths = new List(); + [OptionDescription("Redirect the output to this output file")] [DoNotHashInCache] public string outFile; diff --git a/Microsoft.Research/ClousotMain/SourceFileFinder.cs b/Microsoft.Research/ClousotMain/SourceFileFinder.cs new file mode 100644 index 00000000..c809cfc2 --- /dev/null +++ b/Microsoft.Research/ClousotMain/SourceFileFinder.cs @@ -0,0 +1,81 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.IO; +using System.Linq; +using System.Text; + +namespace Microsoft.Research.CodeAnalysis +{ + [ContractVerification(true)] + class SourceFileFinder + { + public SourceFileFinder(IEnumerable originalSourcePaths, IEnumerable alternativeSourcePaths) + { + Contract.Requires(originalSourcePaths != null); + Contract.Requires(alternativeSourcePaths != null); + + this.originalSourcePaths = originalSourcePaths; + this.alternativeSourcePaths = alternativeSourcePaths; + } + + readonly IEnumerable originalSourcePaths; + readonly IEnumerable alternativeSourcePaths; + const StringComparison Comparison = StringComparison.OrdinalIgnoreCase; // Ignore case in Windows. Re-evalute this for Mono/.NET Core + + public string Find(string originalPath) + { + if (originalPath == null || File.Exists(originalPath)) + { + return originalPath; + } + + foreach (var originalSourcePath in originalSourcePaths) + { + // Find the source path that this is a sub-path of. + if (!originalPath.StartsWith(originalSourcePath, Comparison)) + { + continue; + } + + // Extract the path relative to the source path; + var relativePath = originalPath.Substring(originalSourcePath.Length); + + foreach (var alternativeSourcePath in alternativeSourcePaths) + { + // Graft the relative path onto the alternative source path, as though the file + // exists within that source tree instead. + var alternativePath = alternativeSourcePath + relativePath; + + if (File.Exists(alternativePath)) + { + return alternativePath; + } + } + } + + return originalPath; + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(originalSourcePaths != null); + Contract.Invariant(alternativeSourcePaths != null); + } + } +} diff --git a/Microsoft.Research/CodeProviders/CCI1/CodeProvider.cs b/Microsoft.Research/CodeProviders/CCI1/CodeProvider.cs index a7736683..9966bad6 100644 --- a/Microsoft.Research/CodeProviders/CCI1/CodeProvider.cs +++ b/Microsoft.Research/CodeProviders/CCI1/CodeProvider.cs @@ -2194,7 +2194,7 @@ public Guid AssemblyGuid(AssemblyNode assem) { return assem.Mvid; } - public bool TryLoadAssembly(string fileName, System.Collections.IDictionary assemblyCache, Action errorHandler, out AssemblyNode assem, bool legacyContractMode, List referencedAssemblies, bool extractContractText) + public bool TryLoadAssembly(string fileName, System.Collections.IDictionary assemblyCache, Action errorHandler, out AssemblyNode assem, bool legacyContractMode, List referencedAssemblies, bool extractContractText, SourceFileLocator sourceFileLocator) { var attacher = this.contractAttacher; if (attacher == null) @@ -2223,7 +2223,7 @@ public bool TryLoadAssembly(string fileName, System.Collections.IDictionary asse if (extractContractText) { // extract doc first, then run checker - var gd = new Microsoft.Contracts.Foxtrot.GenerateDocumentationFromPDB(usedContracts); + var gd = new Microsoft.Contracts.Foxtrot.GenerateDocumentationFromPDB(usedContracts, AdaptSourceFileLocator(sourceFileLocator)); gd.VisitForDoc(assem); } @@ -2260,6 +2260,15 @@ public IEnumerable AssemblyReferences(AssemblyNode assembly) } } + private static Func AdaptSourceFileLocator(SourceFileLocator locator) + { + if (locator == null) + { + return null; + } + return new Func(locator); + } + #endregion #region Attributes diff --git a/Microsoft.Research/CodeProviders/CCI2/CodeProvider.cs b/Microsoft.Research/CodeProviders/CCI2/CodeProvider.cs index 2b496672..9f37db11 100644 --- a/Microsoft.Research/CodeProviders/CCI2/CodeProvider.cs +++ b/Microsoft.Research/CodeProviders/CCI2/CodeProvider.cs @@ -9916,7 +9916,7 @@ public void RegisterSourceLocationProvider(IUnitReference unit, ISourceLocationP /// The unit the locations are from. (Locations don't necessarily have a link to the unit they /// belong to.) The unit is used to find a source location provider for that unit. (Providers are maintained /// in a cache in the MetadataDecoder.) If a provider cannot be found for the then - /// an emtpy enumerable is returned. + /// an empty enumerable is returned. /// /// /// If a source location provider is found, then the location of the operation indexed in @@ -9929,7 +9929,7 @@ public void RegisterSourceLocationProvider(IUnitReference unit, ISourceLocationP /// The index of the operation from whose location the corresponding primary source locations are to be found. /// /// - /// True iff the client wants primary source locations only for the operation indexed by . + /// True if the client wants primary source locations only for the operation indexed by . /// /// /// If is false, then this will be the greatest index of the operation in @@ -9984,7 +9984,7 @@ public void ProvideResidualMethodBody(IMethodDefinition methodDefinition, IBlock /// /// /// Must return null if assembly cannot be loaded! - public bool TryLoadAssembly(string fileName, System.Collections.IDictionary assemblyCache, Action errorHandler, out IAssemblyReference assembly, bool legacyContractMode, List referencedAssemblies, bool extractContractText) + public bool TryLoadAssembly(string fileName, System.Collections.IDictionary assemblyCache, Action errorHandler, out IAssemblyReference assembly, bool legacyContractMode, List referencedAssemblies, bool extractContractText, SourceFileLocator sourceFileLocator) { IUnit unit = host.PossiblyCompileFirstLoadUnitFrom(fileName, referencedAssemblies, this.RegisterSourceLocationProvider); if (unit is Dummy) { assembly = null; return false; } diff --git a/Microsoft.Research/ControlFlow/MetadataInterfaces.cs b/Microsoft.Research/ControlFlow/MetadataInterfaces.cs index 0ba6e54b..82614660 100644 --- a/Microsoft.Research/ControlFlow/MetadataInterfaces.cs +++ b/Microsoft.Research/ControlFlow/MetadataInterfaces.cs @@ -34,6 +34,11 @@ namespace Microsoft.Research.CodeAnalysis /// public delegate void BlockInfoPrinter