From 56f5e34a962994a124f0171db5c710e827f5558b Mon Sep 17 00:00:00 2001 From: Xinxing Liu Date: Tue, 17 Sep 2019 15:17:11 -0700 Subject: [PATCH] Fix building issue --- .gitignore | 1 + LICENSE => LICENSE.txt | 0 Sources/BoogieAST/BoogieAST.csproj | 7 +- Sources/SolToBoogie/SolToBoogie.csproj | 23 +- .../SolToBoogieTest/SolToBoogieTest.csproj | 20 +- Sources/SolidityAST/SolidityAST.csproj | 7 +- Sources/SolidityCFG/SolidityCFG.csproj | 9 +- Sources/VeriSol.props | 17 ++ Sources/{SolToBoogie.sln => VeriSol.sln} | 14 - Sources/VeriSol/VeriSol.csproj | 23 +- Sources/VeriSolRunner/Program.cs | 116 -------- Sources/VeriSolRunner/VeriSolExecuter.cs | 270 ------------------ .../VeriSolOutOfBandSpecsRunner.csproj | 41 --- .../VeriSolOutOfBandSpecsRunner.nuspec | 24 -- 14 files changed, 68 insertions(+), 504 deletions(-) rename LICENSE => LICENSE.txt (100%) create mode 100644 Sources/VeriSol.props rename Sources/{SolToBoogie.sln => VeriSol.sln} (85%) delete mode 100644 Sources/VeriSolRunner/Program.cs delete mode 100644 Sources/VeriSolRunner/VeriSolExecuter.cs delete mode 100644 Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.csproj delete mode 100644 Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.nuspec diff --git a/.gitignore b/.gitignore index 3e759b75..34ba6cd9 100644 --- a/.gitignore +++ b/.gitignore @@ -23,6 +23,7 @@ bld/ [Bb]in/ [Oo]bj/ [Ll]og/ +[Nn]upkg/ # Visual Studio 2015/2017 cache/options directory .vs/ diff --git a/LICENSE b/LICENSE.txt similarity index 100% rename from LICENSE rename to LICENSE.txt diff --git a/Sources/BoogieAST/BoogieAST.csproj b/Sources/BoogieAST/BoogieAST.csproj index e50284f9..1a912bfe 100644 --- a/Sources/BoogieAST/BoogieAST.csproj +++ b/Sources/BoogieAST/BoogieAST.csproj @@ -1,9 +1,14 @@ - + Exe netcoreapp2.2 true + + + + + diff --git a/Sources/SolToBoogie/SolToBoogie.csproj b/Sources/SolToBoogie/SolToBoogie.csproj index d87e17bd..9515e229 100644 --- a/Sources/SolToBoogie/SolToBoogie.csproj +++ b/Sources/SolToBoogie/SolToBoogie.csproj @@ -1,28 +1,19 @@ - + + Exe netcoreapp2.2 - - - - - 2.0 true + + + + - - - - - - - + diff --git a/Sources/SolToBoogieTest/SolToBoogieTest.csproj b/Sources/SolToBoogieTest/SolToBoogieTest.csproj index 4181cdf4..8e86576c 100644 --- a/Sources/SolToBoogieTest/SolToBoogieTest.csproj +++ b/Sources/SolToBoogieTest/SolToBoogieTest.csproj @@ -1,4 +1,4 @@ - + Exe @@ -6,29 +6,19 @@ true true VeriSolRegressionRunner - ..\..\Binaries\ + + + - - - - - - - - - - + diff --git a/Sources/SolidityAST/SolidityAST.csproj b/Sources/SolidityAST/SolidityAST.csproj index 0867ed45..4646074a 100644 --- a/Sources/SolidityAST/SolidityAST.csproj +++ b/Sources/SolidityAST/SolidityAST.csproj @@ -1,4 +1,4 @@ - + Exe @@ -6,6 +6,9 @@ true + + + @@ -13,4 +16,6 @@ + + diff --git a/Sources/SolidityCFG/SolidityCFG.csproj b/Sources/SolidityCFG/SolidityCFG.csproj index b655e8b6..2fd944b9 100644 --- a/Sources/SolidityCFG/SolidityCFG.csproj +++ b/Sources/SolidityCFG/SolidityCFG.csproj @@ -1,13 +1,18 @@ - + Exe netcoreapp2.2 - true + true + + + + + diff --git a/Sources/VeriSol.props b/Sources/VeriSol.props new file mode 100644 index 00000000..bf0e4720 --- /dev/null +++ b/Sources/VeriSol.props @@ -0,0 +1,17 @@ + + + + Debug + $([MSBuild]::GetDirectoryNameOfFileAbove($(MSBuildProjectDirectory), `.gitignore`)) + $(RepositoryROOT)\bin\$(Configuration) + $(RepositoryROOT)\obj\$(Configuration)\$(TargetFramework)\$(MSBuildProjectName) + $(RepositoryROOT)\nupkg + false + false + + + + 0.1.0 + + + \ No newline at end of file diff --git a/Sources/SolToBoogie.sln b/Sources/VeriSol.sln similarity index 85% rename from Sources/SolToBoogie.sln rename to Sources/VeriSol.sln index 950c4751..ca8276ef 100644 --- a/Sources/SolToBoogie.sln +++ b/Sources/VeriSol.sln @@ -13,8 +13,6 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "SolidityCFG", "SolidityCFG\ EndProject Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "SolToBoogieTest", "SolToBoogieTest\SolToBoogieTest.csproj", "{6F8F5214-7E0C-4377-B5F2-6D3A553AA8D9}" EndProject -Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "VeriSolOutOfBandSpecsRunner", "VeriSolRunner\VeriSolOutOfBandSpecsRunner.csproj", "{068C4F28-49B0-448D-AEE2-71DB2908C3B7}" -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VeriSol", "VeriSol\VeriSol.csproj", "{2362BC10-65A2-419D-8A41-0FE33FF4FC16}" EndProject Global @@ -87,18 +85,6 @@ Global {6F8F5214-7E0C-4377-B5F2-6D3A553AA8D9}.Release|x64.Build.0 = Release|Any CPU {6F8F5214-7E0C-4377-B5F2-6D3A553AA8D9}.Release|x86.ActiveCfg = Release|Any CPU {6F8F5214-7E0C-4377-B5F2-6D3A553AA8D9}.Release|x86.Build.0 = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|Any CPU.Build.0 = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|x64.ActiveCfg = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|x64.Build.0 = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|x86.ActiveCfg = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Debug|x86.Build.0 = Debug|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|Any CPU.ActiveCfg = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|Any CPU.Build.0 = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|x64.ActiveCfg = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|x64.Build.0 = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|x86.ActiveCfg = Release|Any CPU - {068C4F28-49B0-448D-AEE2-71DB2908C3B7}.Release|x86.Build.0 = Release|Any CPU {2362BC10-65A2-419D-8A41-0FE33FF4FC16}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {2362BC10-65A2-419D-8A41-0FE33FF4FC16}.Debug|Any CPU.Build.0 = Debug|Any CPU {2362BC10-65A2-419D-8A41-0FE33FF4FC16}.Debug|x64.ActiveCfg = Debug|Any CPU diff --git a/Sources/VeriSol/VeriSol.csproj b/Sources/VeriSol/VeriSol.csproj index 193abc9c..12c8798e 100644 --- a/Sources/VeriSol/VeriSol.csproj +++ b/Sources/VeriSol/VeriSol.csproj @@ -1,17 +1,24 @@ - + Exe + VeriSol netcoreapp2.2 - true - 1.0.0 + true + + + + VeriSol + LICENSE.txt https://github.com/microsoft/verisol true - nupkg true VeriSol + + + @@ -30,4 +37,12 @@ + + + PreserveNewest + + + + + diff --git a/Sources/VeriSolRunner/Program.cs b/Sources/VeriSolRunner/Program.cs deleted file mode 100644 index 48d92cba..00000000 --- a/Sources/VeriSolRunner/Program.cs +++ /dev/null @@ -1,116 +0,0 @@ - -namespace VeriSolRunner -{ - using System; - using System.Collections.Generic; - using System.Diagnostics; - using System.IO; - using System.Linq; - using System.Reflection; - using System.Runtime.InteropServices; - using Microsoft.Extensions.Logging; - - /// - /// Running VeriSol when the specifications are provided out of band in a separate Solidity file - /// Highly experimental!! - /// - class Program - { - public static int Main(string[] args) - { - if (args.Length < 4) - { - ShowUsage(); - return 1; - } - - string specFilePath = args[0]; - string contractName = args[1]; // contract Name, often C_VeriSol - string contractPath = args[2]; - int corralRecursionBound = int.Parse(args[3]); // need validation - string solcName = GetSolcNameByOSPlatform(); - - ILoggerFactory loggerFactory = new LoggerFactory().AddConsole(LogLevel.Information); - ILogger logger = loggerFactory.CreateLogger("VeriSolRunner"); - - - HashSet> ignoredMethods = new HashSet>(); - foreach (var arg in args.Where(x => x.StartsWith("/ignoreMethod:"))) - { - Debug.Assert(arg.Contains("@"), $"Error: incorrect use of /ignoreMethod in {arg}"); - Debug.Assert(arg.LastIndexOf("@") == arg.IndexOf("@"), $"Error: incorrect use of /ignoreMethod in {arg}"); - var str = arg.Substring("/ignoreMethod:".Length); - var method = str.Substring(0, str.IndexOf("@")); - var contract = str.Substring(str.IndexOf("@") + 1); - ignoredMethods.Add(Tuple.Create(method, contract)); - } - Console.WriteLine($"Ignored method/contract pairs ==> \n\t {string.Join(",", ignoredMethods.Select(x => x.Item1 + "@" + x.Item2))}"); - - - var assemblyLocation = Assembly.GetExecutingAssembly().Location; - string solcPath = - Path.Combine( - Directory.GetParent(Path.GetDirectoryName(assemblyLocation)).FullName, - solcName); - if (!File.Exists(solcPath)) - { - ShowUsage(); - Console.WriteLine($"Cannot find {solcName} at {solcPath}"); - return 1; - } - - string corralPath = Path.Combine( - Directory.GetParent(Path.GetDirectoryName(assemblyLocation)).FullName, - "corral", "corral.exe"); - if (!File.Exists(corralPath)) - { - ShowUsage(); - Console.WriteLine($"Cannot find Corral.exe at {corralPath}"); - return 1; - } - - - var verisolExecuter = - new VeriSolExecuterWithSpecs( - specFilePath, - contractName, - contractPath, - corralPath, - solcPath, - solcName, - corralRecursionBound, - ignoredMethods, - logger); - return verisolExecuter.Execute(); - } - - private static void ShowUsage() - { - Console.WriteLine("Usage: VeriSolOutOfBandsSpecsRunner "); - Console.WriteLine("\t An (experimental) utility to add formal specification and verification using VeriSol on a smart contract without changing contract sources"); - Console.WriteLine("\t Currently only supports transaction-depth-bounded verification"); - } - - private static string GetSolcNameByOSPlatform() - { - string solcName = null; - if (RuntimeInformation.IsOSPlatform(OSPlatform.Windows)) - { - solcName = "solc.exe"; - } - else if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) - { - solcName = "solc-static-linux"; - } - else if (RuntimeInformation.IsOSPlatform(OSPlatform.OSX)) - { - solcName = "solc-mac"; - } - else - { - throw new SystemException("Cannot recognize OS platform"); - } - return solcName; - } - } -} diff --git a/Sources/VeriSolRunner/VeriSolExecuter.cs b/Sources/VeriSolRunner/VeriSolExecuter.cs deleted file mode 100644 index ef3660f8..00000000 --- a/Sources/VeriSolRunner/VeriSolExecuter.cs +++ /dev/null @@ -1,270 +0,0 @@ - - -namespace VeriSolRunner -{ - - using Microsoft.Extensions.Logging; - using SolidityAST; - using BoogieAST; - using SolToBoogie; - using System; - using System.Collections.Generic; - using System.Diagnostics; - using System.IO; - using System.Runtime.InteropServices; - - internal class VeriSolExecuterWithSpecs - { - private string SpecFilePath; - private string SpecFileDir; - private string ContractName; - private string ContractPath; - private string ContractDir; - private string CorralPath; - private string SolcPath; - private string SolcName; - private ILogger Logger; - private readonly string outFileName = "__SolToBoogieTest_out.bpl"; - private readonly int CorralRecursionLimit; - private readonly int CorralContextBound = 1; // always 1 for solidity - private HashSet> ignoreMethods; - - public VeriSolExecuterWithSpecs(string specFilePath, string contractName, string contractPath, string corralPath, string solcPath, string solcName, int corralRecursionLimit, HashSet> ignoreMethods, ILogger logger) - { - this.SpecFilePath = specFilePath; - this.ContractName = contractName; - this.SpecFileDir = Path.GetDirectoryName(specFilePath); - Console.WriteLine($"SpecFilesDir = {SpecFileDir}"); - if (this.SpecFileDir.TrimEnd().Equals(string.Empty)) - { - throw new Exception($"Specify the specFilePath as .\\{specFilePath} instead of {specFilePath}"); - } - this.ContractPath = contractPath; - this.ContractDir = Path.GetDirectoryName(contractPath); - this.CorralPath = corralPath; - this.SolcPath = solcPath; - this.SolcName = solcName; - this.CorralRecursionLimit = corralRecursionLimit; - this.ignoreMethods = new HashSet>(ignoreMethods); - this.Logger = logger; - } - - public int Execute() - { - // copy contractDir folder to specFileDir - CopyTargetContractFolder(); - - // replace "private " with "internal " in all sol files [HACK!!!] - RewritePrivateVariables(); - - // call SolToBoogie on specFilePath - if (!ExecuteSolToBoogie()) - { - return 1; - } - - // run Corral on outFile - var corralArgs = new List - { - // recursion bound - $"/recursionBound:{CorralRecursionLimit}", - // context bound (k) - $"/k:{CorralContextBound}", - // main method - $"/main:CorralEntry_{ContractName}", - // Boogie file - outFileName - }; - - var corralArgString = string.Join(" ", corralArgs); - Console.WriteLine($"\n-----------Running {CorralPath} {corralArgString} ...."); - var corralOut = RunCorral(corralArgString); - Console.WriteLine($"Finished Corral....\n{corralOut}"); - - // compare Corral output against expected output - if (CompareCorralOutput("Program has no bugs", corralOut)) - { - Console.WriteLine("\n-----Formal Verification successful!!"); - return 0; - } - - Console.WriteLine("\n-----Formal Verification unsuccessful!!"); - return 1; - } - - private void CopyTargetContractFolder() - { - // replicates the content of contractDir\* into specFileDir\ - DirectoryCopy(ContractDir, SpecFileDir, true); - } - - /// - /// https://docs.microsoft.com/en-us/dotnet/standard/io/how-to-copy-directories - /// - private static void DirectoryCopy(string sourceDirName, string destDirName, bool copySubDirs) - { - // Get the subdirectories for the specified directory. - DirectoryInfo dir = new DirectoryInfo(sourceDirName); - - if (!dir.Exists) - { - throw new DirectoryNotFoundException( - "Source directory does not exist or could not be found: " - + sourceDirName); - } - - DirectoryInfo[] dirs = dir.GetDirectories(); - // If the destination directory doesn't exist, create it. - if (!Directory.Exists(destDirName)) - { - Directory.CreateDirectory(destDirName); - } - - // Get the files in the directory and copy them to the new location. - FileInfo[] files = dir.GetFiles(); - foreach (FileInfo file in files) - { - string temppath = Path.Combine(destDirName, file.Name); - file.CopyTo(temppath, true); - } - - // If copying subdirectories, copy them and their contents to new location. - if (copySubDirs) - { - foreach (DirectoryInfo subdir in dirs) - { - string temppath = Path.Combine(destDirName, subdir.Name); - DirectoryCopy(subdir.FullName, temppath, copySubDirs); - } - } - } - - private void RewritePrivateVariables() - { - //recurse down to each Solidity file - var solidityFiles = Directory.EnumerateFiles(SpecFileDir, "*.sol", SearchOption.AllDirectories); - - //replace "private " with "internal " in the file - foreach (var solFile in solidityFiles) - { - var tmpFile = solFile + ".tmp"; - using (StreamReader sr = new StreamReader(solFile)) - { - using (StreamWriter sw = new StreamWriter(tmpFile)) - { - string line; - while ((line = sr.ReadLine()) != null) - { - // brute force - string replacedLine = line.Replace(" private ", " internal "); - replacedLine = replacedLine.Replace(" private(", " internal("); // private(returns bool) - replacedLine = replacedLine.Replace(" private{", " internal{"); // private{body} - replacedLine = replacedLine.Replace(")private ", ")internal "); // )private {body} - replacedLine = replacedLine.Replace(")private(", ")internal("); // )private(returns bool) - replacedLine = replacedLine.Replace(")private{", ")internal{"); // )private{body} - sw.WriteLine(replacedLine); - } - } - } - File.Delete(solFile); - File.Move(tmpFile, solFile); - } - } - - private bool ExecuteSolToBoogie() - { - // compile the program - Console.WriteLine($"\n----- Running Solc on {SpecFilePath}...."); - - SolidityCompiler compiler = new SolidityCompiler(); - CompilerOutput compilerOutput = compiler.Compile(SolcPath, SpecFilePath); - - if (compilerOutput.ContainsError()) - { - compilerOutput.PrintErrorsToConsole(); - throw new SystemException("Compilation Error"); - } - - // build the Solidity AST from solc output - AST solidityAST = new AST(compilerOutput, Path.GetDirectoryName(SpecFilePath)); - - // translate Solidity to Boogie - try - { - BoogieTranslator translator = new BoogieTranslator(); - Console.WriteLine($"\n----- Running SolToBoogie...."); - var translatorFlags = new TranslatorFlags(); - translatorFlags.GenerateInlineAttributes = true; - BoogieAST boogieAST = translator.Translate(solidityAST, ignoreMethods, translatorFlags); - - // dump the Boogie program to a file - var outFilePath = Path.Combine(SpecFileDir, outFileName); - using (var outWriter = new StreamWriter(outFileName)) - { - outWriter.WriteLine(boogieAST.GetRoot()); - } - } - catch (Exception e) - { - Console.WriteLine($"VeriSol translation error: {e.Message}"); - return false; - } - return true; - } - - private string RunCorral(string corralArguments) - { - Process p = new Process(); - p.StartInfo.UseShellExecute = false; - p.StartInfo.RedirectStandardInput = false; - p.StartInfo.RedirectStandardOutput = true; - p.StartInfo.RedirectStandardError = true; - p.StartInfo.CreateNoWindow = true; - if (RuntimeInformation.IsOSPlatform(OSPlatform.Windows)) - { - p.StartInfo.FileName = CorralPath; - p.StartInfo.Arguments = corralArguments; - } - else - { - p.StartInfo.FileName = "mono"; - p.StartInfo.Arguments = $"{CorralPath} {corralArguments}"; - Console.WriteLine(p.StartInfo.Arguments); - } - p.Start(); - - string corralOutput = p.StandardOutput.ReadToEnd(); - string errorMsg = p.StandardError.ReadToEnd(); - if (!String.IsNullOrEmpty(errorMsg)) - { - Console.WriteLine($"Error: {errorMsg}"); - } - p.StandardOutput.Close(); - p.StandardError.Close(); - - // TODO: should set up a timeout here - // but it seems there is a problem if we execute corral using mono - - return corralOutput; - } - - private bool CompareCorralOutput(string expected, string actual) - { - if (actual == null) - { - return false; - } - string[] actualList = actual.Split("Boogie verification time"); - if (actualList.Length == 2) - { - if (actualList[0].Contains(expected)) - { - return true; - } - } - return false; - } - - - } -} \ No newline at end of file diff --git a/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.csproj b/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.csproj deleted file mode 100644 index 8b77082f..00000000 --- a/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.csproj +++ /dev/null @@ -1,41 +0,0 @@ - - - - Exe - netcoreapp2.2 - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.nuspec b/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.nuspec deleted file mode 100644 index a7b6d935..00000000 --- a/Sources/VeriSolRunner/VeriSolOutOfBandSpecsRunner.nuspec +++ /dev/null @@ -1,24 +0,0 @@ - - - - $id$ - 1.0.2 - $title$ - Microsoft, VeriSol - $author$ - MIT - https://github.com/Microsoft/verisol - http://ICON_URL_HERE_OR_DELETE_THIS_LINE - false - A version of VeriSol that allows writing contracts out of band - A prototpe formal verifier for Solidity Smart contracts. - Copyright 2019 - Smart contracts, Solidity, Formal Verification - - - - - - - - \ No newline at end of file