diff --git a/INSTALL.md b/INSTALL.md index efda7f44..826a4d30 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -6,17 +6,11 @@ The following are dynamically installed at VeriSol runtime (the first time only) - Follow either **Nuget** package installation directly, or after building the **sources**. -### Install from nuget.org -Install to the **global** dotnet CLI tools cache so that you can run command `VeriSol` from anywhere: -``` -dotnet tool install VeriSol --version 0.1.1-alpha --global -``` - ### Install from sources Perform the following set of commands: ``` -git clone https://github.com/microsoft/verisol.git +git clone https://github.com/utopia-group/verisol.git ``` From %VERISOL_PATH% (the root folder of the repository), perform diff --git a/Sources/BoogieAST/BoogieAST.cs b/Sources/BoogieAST/BoogieAST.cs index f5f1af9f..504094ae 100644 --- a/Sources/BoogieAST/BoogieAST.cs +++ b/Sources/BoogieAST/BoogieAST.cs @@ -317,19 +317,29 @@ public class BoogieImplementation : BoogieDeclWithFormals public BoogieStmtList StructuredStmts { get; set; } - public BoogieImplementation(string name, List inParams, List outParams, List localVars, BoogieStmtList stmts) + public BoogieImplementation(string name, List inParams, List outParams, List localVars, BoogieStmtList stmts, List attributes = null) { this.Name = name; this.InParams = inParams; this.OutParams = outParams; this.LocalVars = localVars; this.StructuredStmts = stmts; + this.Attributes = attributes; } public override string ToString() { StringBuilder builder = new StringBuilder(); - builder.Append("implementation ").Append(Name).Append("("); + builder.Append("implementation "); + if (Attributes != null) + { + foreach (BoogieAttribute attribute in Attributes) + { + builder.Append(attribute).Append(" "); + } + } + + builder.Append(Name).Append("("); if (InParams.Count > 0) { foreach (BoogieVariable inParam in InParams) @@ -925,6 +935,14 @@ public override string ToString() public abstract class BoogieStructuredCmd : BoogieCmd { } + + public class BoogieWildcardExpr : BoogieExpr + { + public override string ToString() + { + return "*"; + } + } public class BoogieIfCmd : BoogieStructuredCmd { @@ -1212,6 +1230,8 @@ public enum Opcode UNKNOWN, } + public static bool USE_ARITH_OPS { get; set; } + public Opcode Op { get; set; } public BoogieExpr Lhs { get; set; } @@ -1245,9 +1265,9 @@ public static string OpcodeToString(Opcode op) case Opcode.MUL: return "*"; case Opcode.DIV: - return "div"; + return USE_ARITH_OPS ? "/" : "div"; case Opcode.MOD: - return "mod"; + return USE_ARITH_OPS ? "%" : "mod"; case Opcode.EQ: return "=="; case Opcode.NEQ: diff --git a/Sources/SolToBoogie/BoogieTranslator.cs b/Sources/SolToBoogie/BoogieTranslator.cs index d15bfba0..79f7b285 100644 --- a/Sources/SolToBoogie/BoogieTranslator.cs +++ b/Sources/SolToBoogie/BoogieTranslator.cs @@ -1,5 +1,8 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using SolidityAnalysis; + namespace SolToBoogie { using System; @@ -19,11 +22,10 @@ public BoogieAST Translate(AST solidityAST, HashSet> ignor bool generateInlineAttributesInBpl = _translatorFlags.GenerateInlineAttributes; SourceUnitList sourceUnits = solidityAST.GetSourceUnits(); - - TranslatorContext context = new TranslatorContext(ignoredMethods, generateInlineAttributesInBpl, _translatorFlags, entryPointContract); + + TranslatorContext context = new TranslatorContext(solidityAST, ignoredMethods, generateInlineAttributesInBpl, _translatorFlags, entryPointContract); context.IdToNodeMap = solidityAST.GetIdToNodeMap(); context.SourceDirectory = solidityAST.SourceDirectory; - // collect the absolute source path and line number for each AST node SourceInfoCollector sourceInfoCollector = new SourceInfoCollector(context); sourceUnits.Accept(sourceInfoCollector); @@ -65,8 +67,11 @@ public BoogieAST Translate(AST solidityAST, HashSet> ignor FunctionEventResolver functionEventResolver = new FunctionEventResolver(context); functionEventResolver.Resolve(); + // Generate map helper + MapArrayHelper mapHelper = new MapArrayHelper(context, solidityAST); + // add types, gobal ghost variables, and axioms - GhostVarAndAxiomGenerator generator = new GhostVarAndAxiomGenerator(context); + GhostVarAndAxiomGenerator generator = new GhostVarAndAxiomGenerator(context, mapHelper); generator.Generate(); // collect modifiers information @@ -77,8 +82,15 @@ public BoogieAST Translate(AST solidityAST, HashSet> ignor UsingCollector usingCollector = new UsingCollector(context); sourceUnits.Accept(usingCollector); + if (context.TranslateFlags.PerformFunctionSlice) + { + FunctionDependencyCollector depCollector = new FunctionDependencyCollector(context, entryPointContract, context.TranslateFlags.SliceFunctionNames); + context.TranslateFlags.SliceFunctions = depCollector.GetFunctionDeps(); + context.TranslateFlags.SliceModifiers = depCollector.getModifierDeps(); + } + // translate procedures - ProcedureTranslator procTranslator = new ProcedureTranslator(context, generateInlineAttributesInBpl); + ProcedureTranslator procTranslator = new ProcedureTranslator(context, mapHelper, generateInlineAttributesInBpl); sourceUnits.Accept(procTranslator); // generate fallbacks @@ -104,6 +116,12 @@ public BoogieAST Translate(AST solidityAST, HashSet> ignor modSetAnalysis.PerformModSetAnalysis(); } + if (context.TranslateFlags.GenerateERC20Spec) + { + ERC20SpecGenerator specGen = new ERC20SpecGenerator(context, solidityAST, entryPointContract); + specGen.GenerateSpec(); + } + return new BoogieAST(context.Program); } } diff --git a/Sources/SolToBoogie/ERC20SpecGenerator.cs b/Sources/SolToBoogie/ERC20SpecGenerator.cs new file mode 100644 index 00000000..0af83cdb --- /dev/null +++ b/Sources/SolToBoogie/ERC20SpecGenerator.cs @@ -0,0 +1,517 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Runtime.ConstrainedExecution; +using System.Runtime.Serialization; +using SolidityAST; + +namespace SolToBoogie +{ + public class ERC20SpecGenerator + { + private TranslatorContext context; + private AST solidityAST; + private List ERC20Vars = new List() {"totalSupply", "balanceOf", "allowance"}; + private List ERC20fns = new List() {"totalSupply", "balanceOf", "allowance", "approve", "transfer", "transferFrom"}; + private ContractDefinition entryContract; + private Dictionary varDecls; + private Dictionary fnContracts; + private Dictionary declToContractInd; + private List otherVars; + + public ERC20SpecGenerator(TranslatorContext context, AST solidityAST, String entryPoint) + { + this.context = context; + this.solidityAST = solidityAST; + varDecls = new Dictionary(); + fnContracts = new Dictionary(); + otherVars = new List(); + declToContractInd = new Dictionary(); + + foreach (ContractDefinition def in context.ContractDefinitions) + { + if (def.Name.Equals(entryPoint)) + { + entryContract = def; + } + } + + int contractInd = 0; + foreach (int id in entryContract.LinearizedBaseContracts) + { + contractInd++; + ContractDefinition contract = context.GetASTNodeById(id) as ContractDefinition; + + if (context.ContractToStateVarsMap.ContainsKey(contract)) + { + otherVars.AddRange(context.ContractToStateVarsMap[contract]); + foreach (VariableDeclaration decl in context.ContractToStateVarsMap[contract]) + { + declToContractInd[decl] = contractInd; + } + } + + if (!context.ContractToFunctionsMap.ContainsKey(contract)) + { + continue; + } + + HashSet fnDefs = context.ContractToFunctionsMap[contract]; + + foreach (FunctionDefinition fnDef in fnDefs) + { + if (ERC20fns.Contains(fnDef.Name) && !fnContracts.ContainsKey(fnDef.Name)) + { + fnContracts[fnDef.Name] = contract; + } + + if (ERC20Vars.Contains(fnDef.Name) && !varDecls.ContainsKey(fnDef.Name)) + { + ReturnDeclarationFinder declFinder = new ReturnDeclarationFinder(context); + VariableDeclaration decl = declFinder.findDecl(contract, fnDef); + + if (decl != null) + { + varDecls[fnDef.Name] = decl; + } + } + } + } + + foreach (VariableDeclaration decl in varDecls.Values) + { + otherVars.Remove(decl); + } + + otherVars.RemoveAll(v => v.Constant); + } + + private int CompareVars(VariableDeclaration v1, VariableDeclaration v2) + { + if (declToContractInd[v1] != declToContractInd[v2]) + { + return declToContractInd[v1] > declToContractInd[v2] ? -1 : 1; + } + + string[] v1Tokens = v1.Src.Split(':'); + int v1Pos = int.Parse(v1Tokens[0]); + string[] v2Tokens = v2.Src.Split(':'); + int v2Pos = int.Parse(v2Tokens[0]); + + if (v1Pos != v2Pos) + { + return v1Pos < v2Pos ? -1 : 1; + } + + throw new Exception("Two variables at the same position"); + /*int v1No = context.ASTNodeToSourceLineNumberMap[v1]; + int v2No = context.ASTNodeToSourceLineNumberMap[v2]; + + if (v1No != v2No) + { + return v1No < v2No ? -1 : 1; + } + + throw new Exception("Two variables declared on the same line");*/ + } + + public void GenerateSpec() + { + List allVars = new List(otherVars); + String filename = context.ASTNodeToSourcePathMap[entryContract]; + StreamWriter writer = new StreamWriter($"{filename.Substring(0, filename.Length - 4)}.config"); + + string totSupply = varDecls.ContainsKey("totalSupply") ? $"{varDecls["totalSupply"].Name}" : ""; + if (String.IsNullOrEmpty(totSupply)) + { + Console.WriteLine("Warning: Could not find totalSupply variable"); + } + else + { + allVars.Add(varDecls["totalSupply"]); + } + string bal = varDecls.ContainsKey("balanceOf") ? $"{varDecls["balanceOf"].Name}" : ""; + if (String.IsNullOrEmpty(bal)) + { + Console.WriteLine("Warning: Could not find balance variable"); + } + else + { + allVars.Add(varDecls["balanceOf"]); + } + string allowances = varDecls.ContainsKey("allowance") ? $"{varDecls["allowance"].Name}" : ""; + if (String.IsNullOrEmpty(allowances)) + { + Console.WriteLine("Warning: Could not find allowances variable"); + } + else + { + allVars.Add(varDecls["allowance"]); + } + + allVars.Sort(CompareVars); + + string totContract = fnContracts.ContainsKey("totalSupply") ? fnContracts["totalSupply"].Name : ""; + string balContract = fnContracts.ContainsKey("balanceOf") ? fnContracts["balanceOf"].Name : ""; + string allowanceContract = fnContracts.ContainsKey("allowance") ? fnContracts["allowance"].Name : ""; + string approveContract = fnContracts.ContainsKey("approve") ? fnContracts["approve"].Name : ""; + string transferContract = fnContracts.ContainsKey("transfer") ? fnContracts["transfer"].Name : ""; + string transferFromContract = + fnContracts.ContainsKey("transferFrom") ? fnContracts["transferFrom"].Name : ""; + string extraVars = String.Join(" ", otherVars.Select(v => $"this.{v.Name}")); + + writer.WriteLine($"FILE_NAME={filename}"); + writer.WriteLine($"CONTRACT_NAME={entryContract.Name}"); + writer.WriteLine($"TOTAL={totSupply}"); + writer.WriteLine($"BALANCES={bal}"); + writer.WriteLine($"ALLOWANCES={allowances}"); + writer.WriteLine($"TOT_SUP_CONTRACT={totContract}"); + writer.WriteLine($"BAL_OF_CONTRACT={balContract}"); + writer.WriteLine($"ALLOWANCE_CONTRACT={allowanceContract}"); + writer.WriteLine($"APPROVE_CONTRACT={approveContract}"); + writer.WriteLine($"TRANSFER_CONTRACT={transferContract}"); + writer.WriteLine($"TRANSFER_FROM_CONTRACT={transferFromContract}"); + writer.WriteLine($"EXTRA_VARS=({extraVars})"); + for (int i = 0; i < allVars.Count; i++) + { + writer.WriteLine($"{allVars[i].Name}={i}"); + } + writer.Close(); + } + + + private class ReturnDeclarationFinder : BasicASTVisitor + { + private VariableDeclaration retDecl; + private String findVar; + private TranslatorContext context; + private ContractDefinition curContract; + + public ReturnDeclarationFinder(TranslatorContext context) + { + this.context = context; + retDecl = null; + } + + public VariableDeclaration findDecl(ContractDefinition curContract, FunctionDefinition def) + { + if (def.Body == null) + { + return null; + } + + if (def.ReturnParameters.Parameters.Count != 1) + { + return null; + } + + if (!String.IsNullOrEmpty(def.ReturnParameters.Parameters[0].Name)) + { + findVar = def.ReturnParameters.Parameters[0].Name; + } + + this.curContract = curContract; + + def.Body.Accept(this); + return retDecl; + } + + public override bool Visit(ArrayTypeName node) + { + return false; + } + + public override bool Visit(Assignment node) + { + if (node.LeftHandSide is Identifier ident) + { + if (ident.Name.Equals(findVar)) + { + node.RightHandSide.Accept(this); + } + } + return false; + } + + public override bool Visit(SourceUnit node) + { + return false; + } + + public override bool Visit(BinaryOperation node) + { + return false; + } + + public override bool Visit(Block node) + { + for (int i = node.Statements.Count - 1; i >= 0; i--) + { + node.Statements[i].Accept(this); + } + return false; + } + + public override bool Visit(Break node) + { + return false; + } + + public override bool Visit(Conditional node) + { + return false; + } + + public override bool Visit(Continue node) + { + return false; + } + + public override bool Visit(ContractDefinition node) + { + return false; + } + + public override bool Visit(PragmaDirective node) + { + return false; + } + + public override bool Visit(DoWhileStatement node) + { + return false; + } + + public override bool Visit(ElementaryTypeName node) + { + return false; + } + + public override bool Visit(ElementaryTypeNameExpression node) + { + return false; + } + + public override bool Visit(EmitStatement node) + { + return false; + } + + public override bool Visit(EnumDefinition node) + { + return false; + } + + public override bool Visit(UsingForDirective node) + { + return false; + } + + public override bool Visit(ImportDirective node) + { + return false; + } + + public override bool Visit(InheritanceSpecifier node) + { + return false; + } + + public override bool Visit(EnumValue node) + { + return false; + } + + public override bool Visit(EventDefinition node) + { + return false; + } + + public override bool Visit(ExpressionStatement node) + { + return false; + } + + public override bool Visit(ForStatement node) + { + return false; + } + + public FunctionDefinition findFn(string fnName, bool usesSuper) + { + List searchContracts = new List(curContract.LinearizedBaseContracts); + + if (!usesSuper) + { + searchContracts.Insert(0, curContract.Id); + } + + foreach (int id in searchContracts) + { + ContractDefinition def = context.IdToNodeMap[id] as ContractDefinition; + HashSet < FunctionDefinition > fnDefs = context.ContractToFunctionsMap[def]; + Dictionary nameToFn = fnDefs.ToDictionary(v => v.Name, v => v); + if (nameToFn.ContainsKey(fnName)) + { + return nameToFn[fnName]; + } + } + + return null; + } + + public override bool Visit(FunctionCall node) + { + if (node.Expression is Identifier call) + { + FunctionDefinition def = findFn(call.Name, false); + if (def != null && def.ReturnParameters.Parameters.Count != 0) + { + def.Body.Accept(this); + } + } + else if (node.Expression is MemberAccess access) + { + if (access.Expression is Identifier ident && ident.Name.Equals("super")) + { + FunctionDefinition def = findFn(access.MemberName, true); + if (def != null && def.ReturnParameters.Parameters.Count != 0) + { + def.Body.Accept(this); + } + } + } + + return false; + } + + public override bool Visit(FunctionDefinition node) + { + return false; + } + + public override bool Visit(Identifier node) + { + int id = node.ReferencedDeclaration; + VariableDeclaration varDecl = context.IdToNodeMap[id] as VariableDeclaration; + + if (varDecl.StateVariable) + { + retDecl = varDecl; + return false; + } + + findVar = node.Name; + return false; + } + + public override bool Visit(ParameterList node) + { + return false; + } + + public override bool Visit(ModifierDefinition node) + { + return false; + } + + public override bool Visit(IfStatement node) + { + return false; + } + + public override bool Visit(ModifierInvocation node) + { + return false; + } + + public override bool Visit(StructDefinition node) + { + return false; + } + + public override bool Visit(IndexAccess node) + { + node.BaseExpression.Accept(this); + return false; + } + + public override bool Visit(VariableDeclaration node) + { + return false; + } + + public override bool Visit(UserDefinedTypeName node) + { + return false; + } + + public override bool Visit(InlineAssembly node) + { + return false; + } + + public override bool Visit(Literal node) + { + return false; + } + + public override bool Visit(Mapping node) + { + return false; + } + + public override bool Visit(MemberAccess node) + { + return false; + } + + public override bool Visit(NewExpression node) + { + return false; + } + + public override bool Visit(PlaceholderStatement node) + { + return false; + } + + public override bool Visit(WhileStatement node) + { + return false; + } + + public override bool Visit(Return node) + { + node.Expression.Accept(this); + return false; + } + + public override bool Visit(SourceUnitList node) + { + return false; + } + + public override bool Visit(Throw node) + { + return false; + } + + public override bool Visit(UnaryOperation node) + { + return false; + } + + public override bool Visit(TupleExpression node) + { + return false; + } + + public override bool Visit(VariableDeclarationStatement node) + { + return false; + } + } + } +} diff --git a/Sources/SolToBoogie/FallbackGenerator.cs b/Sources/SolToBoogie/FallbackGenerator.cs index e4edce2b..d8aade54 100644 --- a/Sources/SolToBoogie/FallbackGenerator.cs +++ b/Sources/SolToBoogie/FallbackGenerator.cs @@ -58,7 +58,7 @@ public void Generate() BoogieStmtList fbBody = new BoogieStmtList(); var fbLocalVars = new List(); - if (context.TranslateFlags.ModelStubsAsSkips() || context.TranslateFlags.ModelStubsAsCallbacks()) + if (context.TranslateFlags.ModelStubsAsSkips() || context.TranslateFlags.ModelStubsAsCallbacks() || context.TranslateFlags.ModelStubsAsMultipleCallbacks()) { fbBody.AppendStmtList(CreateBodyOfUnknownFallback(fbLocalVars, inParams)); } @@ -103,6 +103,17 @@ private BoogieStmtList CreateBodyOfSend(List inParams, List inParams, List locals) + { + BoogieStmtList stmtList = new BoogieStmtList(); + foreach (BoogieVariable localVar in locals) + { + string varName = localVar.TypedIdent.Name; + if (!varName.Equals("this")) + { + stmtList.AddStatement(new BoogieHavocCmd(new BoogieIdentifierExpr(varName))); + } + } + + return stmtList; + } private BoogieStmtList CreateBodyOfUnknownFallback(List fbLocalVars, List inParams) { - Debug.Assert(context.TranslateFlags.ModelStubsAsSkips() || context.TranslateFlags.ModelStubsAsCallbacks(), + Debug.Assert(context.TranslateFlags.ModelStubsAsSkips() || context.TranslateFlags.ModelStubsAsCallbacks() || context.TranslateFlags.ModelStubsAsMultipleCallbacks(), "CreateBodyOfUnknownFallback called in unexpected context"); var procBody = new BoogieStmtList(); - procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + /*procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr(inParams[0].Name)); var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr(inParams[1].Name)); var msgVal = new BoogieIdentifierExpr("amount"); @@ -129,16 +154,92 @@ private BoogieStmtList CreateBodyOfUnknownFallback(List fbLocalV procBody.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal))); //balance[to] = balance[to] + msg.value procBody.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); - procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); + procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function END "));*/ + + BoogieStmtList body = procBody; + if (context.TranslateFlags.ModelStubsAsCallbacks() || + context.TranslateFlags.ModelStubsAsMultipleCallbacks()) + { + if (context.TranslateFlags.ModelReverts) + { + BoogieBinaryOperation revertGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, new BoogieIdentifierExpr("choice"), new BoogieLiteralExpr(BigInteger.Zero)); + BoogieStmtList thenBody = new BoogieStmtList(); + thenBody.AddStatement(new BoogieAssignCmd(new BoogieIdentifierExpr("revert"), new BoogieLiteralExpr(true))); + thenBody.AddStatement(new BoogieReturnCmd()); + BoogieIfCmd earlyExitCmd = new BoogieIfCmd(revertGuard, thenBody, null); + body.AddStatement(earlyExitCmd); + } + if (context.TranslateFlags.InstrumentGas) + { + BoogieBinaryOperation gasGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.LT, new BoogieIdentifierExpr("gas"), new BoogieLiteralExpr(TranslatorContext.TX_GAS_COST)); + BoogieIfCmd earlyExitCmd = new BoogieIfCmd(gasGuard, BoogieStmtList.MakeSingletonStmtList(new BoogieReturnCmd()), null); + body.AddStatement(earlyExitCmd); + } + + } + + if (context.TranslateFlags.ModelStubsAsMultipleCallbacks()) + { + fbLocalVars.Add(new BoogieLocalVariable(new BoogieTypedIdent("iterate", BoogieType.Bool))); + BoogieBinaryOperation gasGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, new BoogieIdentifierExpr("gas"), new BoogieLiteralExpr(TranslatorContext.TX_GAS_COST)); + BoogieBinaryOperation guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.AND, new BoogieIdentifierExpr("iterate"), gasGuard); + BoogieStmtList loopBody = new BoogieStmtList(); + procBody.AddStatement(new BoogieWhileCmd(guard, loopBody, new List())); + body = loopBody; + } - if (context.TranslateFlags.ModelStubsAsCallbacks()) + if (context.TranslateFlags.ModelStubsAsCallbacks() || context.TranslateFlags.ModelStubsAsMultipleCallbacks()) { - fbLocalVars.AddRange(TransUtils.CollectLocalVars(context.ContractDefinitions.ToList(), context)); + List localVars = TransUtils.CollectLocalVars(context.ContractDefinitions.ToList(), context); + fbLocalVars.AddRange(localVars); // if (*) fn1(from, *, ...) // we only redirect the calling contract, but the msg.sender need not be to, as it can call into anohter contract that calls // into from - procBody.AddStatement(TransUtils.GenerateChoiceBlock(context.ContractDefinitions.ToList(), context, Tuple.Create(inParams[0].Name, inParams[1].Name))); + + if (context.TranslateFlags.ModelStubsAsMultipleCallbacks()) + { + body.AppendStmtList(HavocLocals(localVars)); + body.AddStatement(new BoogieHavocCmd(new BoogieIdentifierExpr("iterate"))); + } + + + BoogieIfCmd typeIf = null; + foreach (ContractDefinition curDef in context.ContractDefinitions.ToList()) + { + BoogieIfCmd reentrantCalls = TransUtils.GenerateChoiceBlock(new List() {curDef}, + context, false, Tuple.Create(inParams[0].Name, inParams[1].Name)); + + if (reentrantCalls == null) + { + continue; + } + + BoogieExpr dtype = new BoogieMapSelect(new BoogieIdentifierExpr("DType"), new BoogieIdentifierExpr(inParams[0].Name)); + BoogieBinaryOperation guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, dtype, new BoogieIdentifierExpr(curDef.Name)); + typeIf = new BoogieIfCmd(guard, BoogieStmtList.MakeSingletonStmtList(reentrantCalls), typeIf == null ? null : BoogieStmtList.MakeSingletonStmtList(typeIf)); + } + + /*BoogieIfCmd ifCmd = null; + + if (context.TranslateFlags.ModelReverts) + { + BoogieExpr guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, + new BoogieIdentifierExpr("choice"), + new BoogieLiteralExpr(choices.Item2 + 1)); + + BoogieAssignCmd assign = new BoogieAssignCmd(new BoogieIdentifierExpr("revert"), new BoogieLiteralExpr(true)); + ifCmd = new BoogieIfCmd(guard, BoogieStmtList.MakeSingletonStmtList(assign), BoogieStmtList.MakeSingletonStmtList(choices.Item1)); + } + else + { + ifCmd = choices.Item1; + }*/ + + body.AddStatement(typeIf); } + + + return procBody; } @@ -193,12 +294,18 @@ private BoogieStmtList GenerateBodyOfFallbackDispatch(List inPar if (function != null) { + if (context.TranslateFlags.PerformFunctionSlice && + !context.TranslateFlags.SliceFunctions.Contains(function)) + { + continue; + } + List arguments = new List() - { - new BoogieIdentifierExpr(inParams[1].Name), - new BoogieIdentifierExpr(inParams[0].Name), - new BoogieIdentifierExpr(inParams[2].Name) - }; + { + new BoogieIdentifierExpr(inParams[1].Name), + new BoogieIdentifierExpr(inParams[0].Name), + new BoogieIdentifierExpr(inParams[2].Name) + }; string callee = TransUtils.GetCanonicalFunctionName(function, context); // to.fallback(from, amount), thus need to switch param0 and param1 diff --git a/Sources/SolToBoogie/FunctionCallHelper.cs b/Sources/SolToBoogie/FunctionCallHelper.cs new file mode 100644 index 00000000..f296a468 --- /dev/null +++ b/Sources/SolToBoogie/FunctionCallHelper.cs @@ -0,0 +1,325 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using SolidityAST; + +namespace SolToBoogie +{ + public class FunctionCallHelper + { + public static bool IsDynamicDispatching(FunctionCall node) + { + return node.Expression is Identifier; + } + + public static bool IsTypeCast(FunctionCall node) + { + return node.Kind.Equals("typeConversion"); + } + + public static bool IsStaticDispatching(TranslatorContext context, FunctionCall node) + { + if (node.Expression is MemberAccess memberAccess) + { + if (memberAccess.Expression is Identifier ident) + { + if (context.GetASTNodeById(ident.ReferencedDeclaration) is ContractDefinition) + { + return true; + } + } + } + return false; + } + + public static ContractDefinition GetStaticDispatchingContract(TranslatorContext context, FunctionCall node) + { + VeriSolAssert(node.Expression is MemberAccess); + MemberAccess memberAccess = node.Expression as MemberAccess; + + Identifier contractId = memberAccess.Expression as Identifier; + VeriSolAssert(contractId != null, $"Unknown contract name: {memberAccess.Expression}"); + + ContractDefinition contract = context.GetASTNodeById(contractId.ReferencedDeclaration) as ContractDefinition; + VeriSolAssert(contract != null); + return contract; + } + + public static ContractDefinition GetUsedLibrary(TranslatorContext context, ContractDefinition curContract, + MemberAccess memberAccess) + { + FunctionDefinition fnDef = context.GetASTNodeById(memberAccess.ReferencedDeclaration.Value) as FunctionDefinition; + + if (fnDef == null || !context.FunctionToContractMap.ContainsKey(fnDef)) + { + return null; + } + + ContractDefinition fnContract = context.GetContractByFunction(fnDef); + + Dictionary usingLibs = new Dictionary(); + List contractIds = new List(); + contractIds.Add(curContract.Id); + contractIds.AddRange(curContract.LinearizedBaseContracts); + + foreach (int id in contractIds) + { + ContractDefinition baseContract = context.GetASTNodeById(id) as ContractDefinition; + + foreach (UserDefinedTypeName typeName in context.UsingMap[baseContract].Keys) + { + ContractDefinition libDef = context.GetASTNodeById(typeName.ReferencedDeclaration) as ContractDefinition; + if (!usingLibs.ContainsKey(libDef)) + { + usingLibs[libDef] = typeName; + } + } + } + + if (usingLibs.ContainsKey(fnContract)) + { + if (memberAccess.Expression.TypeDescriptions.IsContract() && + !memberAccess.Expression.TypeDescriptions.IsArray()) + { + //search sub-types + UserDefinedTypeName libType = usingLibs[fnContract]; + String contractName = memberAccess.Expression.TypeDescriptions.TypeString.Split(" ")[1]; + ContractDefinition contractDef = context.GetContractByName(contractName); + HashSet usedBy = context.UsingMap[curContract][libType].FindAll(t => + t is UserDefinedTypeName u && + context.GetASTNodeById(u.ReferencedDeclaration) is ContractDefinition).Select(c => + context.GetASTNodeById(((UserDefinedTypeName) (c)) + .ReferencedDeclaration) as ContractDefinition).ToHashSet(); + + bool usesLib = usedBy.Contains(contractDef); + + foreach (int id in contractDef.LinearizedBaseContracts) + { + ContractDefinition baseContract = context.GetASTNodeById(id) as ContractDefinition; + if (usedBy.Contains(baseContract)) + { + usesLib = true; + } + } + + return usesLib ? fnContract : null; + } + else + { + return fnContract; + } + } + + return null; + } + + public static bool IsUsingBasedLibraryCall(TranslatorContext context, ContractDefinition curContract, MemberAccess memberAccess) + { + // since we only permit "using A for B" for non-contract types + // this is sufficient, but not necessary in general since non + // contracts (including libraries) do not have support methods + return GetUsedLibrary(context, curContract, memberAccess) != null; + } + + public static ContractDefinition IsLibraryFunctionCall(TranslatorContext context, FunctionCall node) + { + if (node.Expression is MemberAccess memberAccess) + { + if (memberAccess.Expression is Identifier identifier) + { + var contract = context.GetASTNodeById(identifier.ReferencedDeclaration) as ContractDefinition; + // a Library is treated as an external function call + // we need to do it here as the Lib.Foo, Lib is not an expression but name of a contract + if (contract.ContractKind == EnumContractKind.LIBRARY) + { + return contract; + } + } + } + return null; + } + + public static bool IsExternalFunctionCall(TranslatorContext context, FunctionCall node) + { + if (node.Expression is MemberAccess memberAccess) + { + if (memberAccess.Expression is Identifier identifier) + { + if (identifier.Name == "this") + { + return true; + } + + if (identifier.Name == "super") + { + return true; + } + + if (!context.HasASTNodeId(identifier.ReferencedDeclaration)) + { + return true; + } + + var contract = context.GetASTNodeById(identifier.ReferencedDeclaration) as ContractDefinition; + if (contract == null) + { + return true; + } + } + else if (memberAccess.Expression is MemberAccess structSelect) + { + //a.b.c.foo(...) + //TODO: do we want to check that the contract the struct variable is declared + // is not in the "context"? Why this isn't done for IndexAccess? + return true; + } + else if (memberAccess.Expression.ToString().Equals("msg.sender")) + { + // calls can be of the form "msg.sender.call()" or "msg.sender.send()" or "msg.sender.transfer()" + return true; + } + else if (memberAccess.Expression is FunctionCall) + { + // TODO: example? + return true; + } else if (memberAccess.Expression is IndexAccess) + { + //a[i].foo(..) + return true; + } + else if (memberAccess.Expression is TupleExpression) + { + return true; + } + } + return false; + } + + public static bool IsImplicitFunc(FunctionCall node) + { + return + IsKeccakFunc(node) || + IsAbiEncodePackedFunc(node) || + IsGasleft(node) || + IsTypeCast(node) || + IsStructConstructor(node) || + IsContractConstructor(node) || + IsAbiFunction(node); + } + + public static bool IsAbiFunction(FunctionCall node) + { + if (node.Expression is MemberAccess member) + { + if (member.Expression is Identifier ident) + { + if (ident.Name.Equals("abi")) + { + return true; + } + } + } + return false; + } + + public static bool IsContractConstructor(FunctionCall node) + { + return node.Expression is NewExpression; + } + + public static bool IsStructConstructor(FunctionCall node) + { + return node.Kind.Equals("structConstructorCall"); + } + + public static bool IsGasleft(FunctionCall node) + { + if (node.Expression is Identifier ident) + { + return ident.Name.Equals("gasleft") && node.Arguments.Count == 0; + } + + return false; + } + + public static bool IsKeccakFunc(FunctionCall node) + { + if (node.Expression is Identifier ident) + { + return ident.Name.Equals("keccak256"); + } + return false; + } + + public static bool IsBuiltInTransferFunc(string functionName, FunctionCall node) + { + if (!functionName.Equals("transfer")) return false; + if (node.Expression is MemberAccess member) + { + if (member.Expression.TypeDescriptions.IsAddress()) + return true; + } + return false; + } + + public static bool IsAbiEncodePackedFunc(FunctionCall node) + { + if (node.Expression is MemberAccess member) + { + if (member.Expression is Identifier ident) + { + if (ident.Name.Equals("abi")) + { + if (member.MemberName.Equals("encodePacked")) + return true; + } + } + } + return false; + } + + public static bool IsAssert(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("assert"); + } + + public static bool IsRequire(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("require"); + } + + public static bool IsRevert(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("revert"); + } + + public static bool IsLowLevelCall(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("call"); + } + + public static bool isDelegateCall(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("delegatecall"); + } + + public static bool isSend(FunctionCall node) + { + var functionName = TransUtils.GetFuncNameFromFuncCall(node); + return functionName.Equals("send"); + } + + private static void VeriSolAssert(bool cond, string message = "") + { + if (!cond) + { + throw new Exception ($"{message}...."); + } + } + } +} \ No newline at end of file diff --git a/Sources/SolToBoogie/FunctionDependencyCollector.cs b/Sources/SolToBoogie/FunctionDependencyCollector.cs new file mode 100644 index 00000000..8ad6855a --- /dev/null +++ b/Sources/SolToBoogie/FunctionDependencyCollector.cs @@ -0,0 +1,153 @@ +using System; +using System.Collections.Generic; +using SolidityAST; + +namespace SolToBoogie +{ + public class FunctionDependencyCollector : BasicASTVisitor + { + private TranslatorContext context; + private HashSet fnDeps; + private HashSet modDeps; + private Dictionary> nameToFn; + private HashSet seenFns; + private FunctionDefinition curFn; + private LinkedList worklist; + + + + public FunctionDependencyCollector(TranslatorContext context, String baseContractName, HashSet fnNames) + { + this.context = context; + nameToFn = new Dictionary>(); + fnDeps = new HashSet(); + modDeps = new HashSet(); + seenFns = new HashSet(); + worklist = new LinkedList(); + ContractDefinition baseContract = null; + + foreach (ContractDefinition def in context.ContractDefinitions) + { + if (def.Name.Equals(baseContractName)) + { + baseContract = def; + } + + if (context.ContractToFunctionsMap.ContainsKey(def)) + { + foreach (FunctionDefinition fnDef in context.ContractToFunctionsMap[def]) + { + if (nameToFn.ContainsKey(fnDef.Name)) + { + nameToFn[fnDef.Name].Add(fnDef); + } + else + { + nameToFn[fnDef.Name] = new List() {fnDef}; + } + } + } + } + + foreach (FunctionDefinition fnDef in context.GetVisibleFunctionsByContract(baseContract)) + { + if (fnNames.Contains(fnDef.Name)) + { + worklist.AddLast(fnDef); + seenFns.Add(fnDef); + } + } + + while (worklist.Count != 0) + { + curFn = worklist.First.Value; + worklist.RemoveFirst(); + fnDeps.Add(curFn); + + if (curFn.Modifiers != null) + { + foreach (ModifierInvocation mod in curFn.Modifiers) + { + int id = mod.ModifierName.ReferencedDeclaration; + ASTNode node = context.GetASTNodeById(id); + + if (node is ModifierDefinition modDef) + { + if (!modDeps.Contains(modDef)) + { + modDeps.Add(modDef); + modDef.Body.Accept(this); + } + } + else + { + throw new Exception("Modifier id does not reference a modifier declaration"); + } + } + } + + if (curFn.Body != null) + { + curFn.Body.Accept(this); + } + } + } + + public bool IsDependent(FunctionDefinition dep) + { + return fnDeps.Contains(dep); + } + + public HashSet GetFunctionDeps() + { + return fnDeps; + } + + public HashSet getModifierDeps() + { + return modDeps; + } + + private bool isBuiltinFn(FunctionCall call) + { + return FunctionCallHelper.IsLowLevelCall(call) || FunctionCallHelper.isSend(call) || + FunctionCallHelper.IsAssert(call) || FunctionCallHelper.isDelegateCall(call) || + FunctionCallHelper.IsRequire(call) || FunctionCallHelper.IsRevert(call) || + FunctionCallHelper.IsKeccakFunc(call) || FunctionCallHelper.IsAbiEncodePackedFunc(call) || + FunctionCallHelper.IsTypeCast(call) || FunctionCallHelper.IsBuiltInTransferFunc(TransUtils.GetFuncNameFromFuncCall(call), call); + } + + public override bool Visit(FunctionCall node) + { + if (FunctionCallHelper.IsLowLevelCall(node) || FunctionCallHelper.isDelegateCall(node)) + { + worklist.Clear(); + foreach (FunctionDefinition def in context.FunctionToContractMap.Keys) + { + fnDeps.Add(def); + } + } + else if (isBuiltinFn(node)) + { + return true; + } + else + { + string fnName = TransUtils.GetFuncNameFromFuncCall(node); + if (nameToFn.ContainsKey(fnName)) + { + foreach (FunctionDefinition fnDef in nameToFn[fnName]) + { + if (!seenFns.Contains(fnDef)) + { + worklist.AddLast(fnDef); + seenFns.Add(fnDef); + } + } + } + } + + return true; + } + } +} \ No newline at end of file diff --git a/Sources/SolToBoogie/FunctionEventCollector.cs b/Sources/SolToBoogie/FunctionEventCollector.cs index 7978bc0a..e00ac2e5 100644 --- a/Sources/SolToBoogie/FunctionEventCollector.cs +++ b/Sources/SolToBoogie/FunctionEventCollector.cs @@ -1,5 +1,9 @@ -// Copyright (c) Microsoft Corporation. All rights reserved. +// Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using System.Collections.Generic; +using System.Linq; + namespace SolToBoogie { using System.Diagnostics; @@ -16,6 +20,7 @@ public class FunctionEventCollector : BasicASTVisitor // current contract that the visitor is visiting private ContractDefinition currentContract = null; + private List nodesToAdd = null; public FunctionEventCollector(TranslatorContext context) { @@ -25,12 +30,15 @@ public FunctionEventCollector(TranslatorContext context) public override bool Visit(ContractDefinition node) { currentContract = node; + nodesToAdd = new List(); return true; } public override void EndVisit(ContractDefinition node) { + currentContract.Nodes.AddRange(nodesToAdd); currentContract = null; + nodesToAdd = null; } public override bool Visit(EventDefinition node) @@ -46,5 +54,112 @@ public override bool Visit(FunctionDefinition node) context.AddFunctionToContract(currentContract, node); return false; } + + public FunctionDefinition GenerateGetter(VariableDeclaration varDecl) + { + FunctionDefinition fnDef = new FunctionDefinition(); + Block body = new Block(); + body.Scope = 0; + body.Statements = new List(); + ParameterList fnParams = new ParameterList(); + fnParams.Parameters = new List(); + ParameterList rets = new ParameterList(); + rets.Parameters = new List(); + + fnDef.Visibility = EnumVisibility.PUBLIC; + fnDef.Implemented = true; + fnDef.Name = varDecl.Name; + fnDef.StateMutability = EnumStateMutability.VIEW; + fnDef.Body = body; + fnDef.Parameters = fnParams; + fnDef.ReturnParameters = rets; + fnDef.Modifiers = new List(); + + TypeName curType = varDecl.TypeName; + + Identifier ident = new Identifier(); + ident.Name = varDecl.Name; + ident.ReferencedDeclaration = varDecl.Id; + ident.OverloadedDeclarations = new List(); + ident.TypeDescriptions = varDecl.TypeDescriptions; + + int id = context.IdToNodeMap.Keys.Max() + 1; + + Expression curExpr = ident; + List localIds = new List(); + + while (curType is Mapping || curType is ArrayTypeName) + { + VariableDeclaration paramDecl = new VariableDeclaration(); + paramDecl.Name = "arg" + id; + paramDecl.Visibility = EnumVisibility.DEFAULT; + paramDecl.StorageLocation = EnumLocation.DEFAULT; + paramDecl.Id = id; + context.IdToNodeMap.Add(id, paramDecl); + fnParams.Parameters.Add(paramDecl); + + if (curType is Mapping map) + { + paramDecl.TypeName = map.KeyType; + paramDecl.TypeDescriptions = map.KeyType.TypeDescriptions; + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + TypeDescription intDescription = new TypeDescription(); + intDescription.TypeString = "uint256"; + ElementaryTypeName intTypeName = new ElementaryTypeName(); + intTypeName.TypeDescriptions = intDescription; + paramDecl.TypeName = intTypeName; + paramDecl.TypeDescriptions = intDescription; + curType = arr.BaseType; + } + + Identifier paramIdent = new Identifier(); + paramIdent.Name = paramDecl.Name; + paramIdent.OverloadedDeclarations = new List(); + paramIdent.TypeDescriptions = paramDecl.TypeDescriptions; + paramIdent.ReferencedDeclaration = paramDecl.Id; + + IndexAccess access = new IndexAccess(); + access.BaseExpression = curExpr; + access.IndexExpression = paramIdent; + access.TypeDescriptions = TransUtils.TypeNameToTypeDescription(curType); + + curExpr = access; + id++; + } + + VariableDeclaration retVar = new VariableDeclaration(); + retVar = new VariableDeclaration(); + retVar.Name = null; + retVar.TypeDescriptions = TransUtils.TypeNameToTypeDescription(curType); + retVar.TypeName = curType; + rets.Parameters.Add(retVar); + + Return ret = new Return(); + ret.Expression = curExpr; + + context.ASTNodeToSourcePathMap[ret] = context.ASTNodeToSourcePathMap[varDecl]; + context.ASTNodeToSourceLineNumberMap[ret] = context.ASTNodeToSourceLineNumberMap[varDecl]; + context.ASTNodeToSourcePathMap[body] = context.ASTNodeToSourcePathMap[varDecl]; + context.ASTNodeToSourceLineNumberMap[body] = context.ASTNodeToSourceLineNumberMap[varDecl]; + + body.Statements.Add(ret); + + return fnDef; + } + + public override bool Visit(VariableDeclaration varDecl) + { + if (context.TranslateFlags.GenerateGetters && varDecl.Visibility.Equals(EnumVisibility.PUBLIC)) + { + FunctionDefinition getter = GenerateGetter(varDecl); + nodesToAdd.Add(getter); + context.AddFunctionToContract(currentContract, getter); + } + + return false; + } } } diff --git a/Sources/SolToBoogie/GhostVarAndAxiomGenerator.cs b/Sources/SolToBoogie/GhostVarAndAxiomGenerator.cs index 00866ebf..c6392021 100644 --- a/Sources/SolToBoogie/GhostVarAndAxiomGenerator.cs +++ b/Sources/SolToBoogie/GhostVarAndAxiomGenerator.cs @@ -13,11 +13,14 @@ public class GhostVarAndAxiomGenerator // require the ContractDefintions member is populated private TranslatorContext context; + private MapArrayHelper mapHelper; + private BoogieCtorType contractType = new BoogieCtorType("ContractName"); - public GhostVarAndAxiomGenerator(TranslatorContext context) + public GhostVarAndAxiomGenerator(TranslatorContext context, MapArrayHelper mapHelper) { this.context = context; + this.mapHelper = mapHelper; } public void Generate() @@ -44,12 +47,44 @@ private void GenerateFunctions() if (context.TranslateFlags.QuantFreeAllocs) { - context.Program.AddDeclaration(GenerateZeroRefIntArrayFunction()); - context.Program.AddDeclaration(GenerateZeroIntIntArrayFunction()); - context.Program.AddDeclaration(GenerateZeroRefBoolArrayFunction()); - context.Program.AddDeclaration(GenerateZeroIntBoolArrayFunction()); - context.Program.AddDeclaration(GenerateZeroRefRefArrayFunction()); - context.Program.AddDeclaration(GenerateZeroIntRefArrayFunction()); + if (context.TranslateFlags.UseMultiDim) + { + foreach(VariableDeclaration decl in context.Analysis.Alias.getResults()) + { + TypeName type = decl.TypeName; + if (type is Mapping || type is ArrayTypeName) + { + BoogieFunction initFn = MapArrayHelper.GenerateMultiDimZeroFunction(decl); + + if (!context.initFns.Contains(initFn.Name)) + { + context.Program.AddDeclaration(initFn); + context.initFns.Add(initFn.Name); + } + + } + } + } + else + { + context.Program.AddDeclaration(GenerateZeroRefIntArrayFunction()); + context.Program.AddDeclaration(GenerateZeroIntIntArrayFunction()); + context.Program.AddDeclaration(GenerateZeroRefBoolArrayFunction()); + context.Program.AddDeclaration(GenerateZeroIntBoolArrayFunction()); + context.Program.AddDeclaration(GenerateZeroRefRefArrayFunction()); + context.Program.AddDeclaration(GenerateZeroIntRefArrayFunction()); + } + + + + } + + if (context.TranslateFlags.NoNonlinearArith) + { + context.Program.AddDeclaration(generateNonlinearMulFunction()); + context.Program.AddDeclaration(generateNonlinearDivFunction()); + context.Program.AddDeclaration(generateNonlinearPowFunction()); + context.Program.AddDeclaration(generateNonlinearModFunction()); } } @@ -184,11 +219,12 @@ private BoogieFunction GenerateConstToRefFunction() //function for Int to Ref var inVar = new BoogieFormalParam(new BoogieTypedIdent("x", BoogieType.Int)); var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", BoogieType.Ref)); + BoogieAttribute attr = new BoogieAttribute("smtdefined", "\"x\""); return new BoogieFunction( "ConstantToRef", new List() { inVar }, new List() { outVar }, - null); + new List() { attr }); } private BoogieFunction GenerateRefToInt() @@ -229,6 +265,50 @@ private BoogieFunction GenerateVeriSolSumFunction() null); } + private BoogieFunction generateNonlinearMulFunction() + { + string fnName = "nonlinearMul"; + var inVar1 = new BoogieFormalParam(new BoogieTypedIdent("x", BoogieType.Int)); + var inVar2 = new BoogieFormalParam(new BoogieTypedIdent("y", BoogieType.Int)); + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", BoogieType.Int)); + + return new BoogieFunction(fnName, new List() {inVar1, inVar2}, + new List() {outVar}); + } + + private BoogieFunction generateNonlinearDivFunction() + { + string fnName = "nonlinearDiv"; + var inVar1 = new BoogieFormalParam(new BoogieTypedIdent("x", BoogieType.Int)); + var inVar2 = new BoogieFormalParam(new BoogieTypedIdent("y", BoogieType.Int)); + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", BoogieType.Int)); + + return new BoogieFunction(fnName, new List() {inVar1, inVar2}, + new List() {outVar}); + } + + private BoogieFunction generateNonlinearPowFunction() + { + string fnName = "nonlinearPow"; + var inVar1 = new BoogieFormalParam(new BoogieTypedIdent("x", BoogieType.Int)); + var inVar2 = new BoogieFormalParam(new BoogieTypedIdent("y", BoogieType.Int)); + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", BoogieType.Int)); + + return new BoogieFunction(fnName, new List() {inVar1, inVar2}, + new List() {outVar}); + } + + private BoogieFunction generateNonlinearModFunction() + { + string fnName = "nonlinearMod"; + var inVar1 = new BoogieFormalParam(new BoogieTypedIdent("x", BoogieType.Int)); + var inVar2 = new BoogieFormalParam(new BoogieTypedIdent("y", BoogieType.Int)); + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", BoogieType.Int)); + + return new BoogieFunction(fnName, new List() {inVar1, inVar2}, + new List() {outVar}); + } + private void GenerateTypes() { @@ -308,13 +388,6 @@ private void GenerateGlobalVariables() context.Program.AddDeclaration(gas); } - if (context.TranslateFlags.InstrumentSums) - { - BoogieTypedIdent sumId = new BoogieTypedIdent("sum", new BoogieMapType(BoogieType.Ref, BoogieType.Int)); - BoogieGlobalVariable sum = new BoogieGlobalVariable(sumId); - context.Program.AddDeclaration(sum); - } - // Solidity-specific vars BoogieTypedIdent nowVar = new BoogieTypedIdent("now", BoogieType.Int); context.Program.AddDeclaration(new BoogieGlobalVariable(nowVar)); @@ -652,7 +725,7 @@ private BoogieAxiom GenerateAbiEncodePackedAxiomTwoArgsOneRef() private void GenerateMemoryVariables() { - HashSet> generatedTypes = new HashSet>(); + HashSet generatedMaps = new HashSet(); // mappings foreach (ContractDefinition contract in context.ContractToMappingsMap.Keys) { @@ -660,7 +733,18 @@ private void GenerateMemoryVariables() { Debug.Assert(varDecl.TypeName is Mapping); Mapping mapping = varDecl.TypeName as Mapping; - GenerateMemoryVariablesForMapping(mapping, generatedTypes); + GenerateMemoryVariablesForMapping(varDecl, mapping, generatedMaps, 0); + + if (context.TranslateFlags.InstrumentSums) + { + String sumName = mapHelper.GetSumName(varDecl); + if (!generatedMaps.Contains(sumName)) + { + generatedMaps.Add(sumName); + BoogieType sumType = new BoogieMapType(BoogieType.Ref, BoogieType.Int); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(sumName, sumType))); + } + } } } // arrays @@ -670,24 +754,48 @@ private void GenerateMemoryVariables() { Debug.Assert(varDecl.TypeName is ArrayTypeName); ArrayTypeName array = varDecl.TypeName as ArrayTypeName; - GenerateMemoryVariablesForArray(array, generatedTypes); + GenerateMemoryVariablesForArray(varDecl, array, generatedMaps, 0); + + if (context.TranslateFlags.InstrumentSums) + { + String sumName = mapHelper.GetSumName(varDecl); + if (!generatedMaps.Contains(sumName)) + { + generatedMaps.Add(sumName); + BoogieType sumType = new BoogieMapType(BoogieType.Ref, BoogieType.Int); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(sumName, sumType))); + } + } } } } - private void GenerateMemoryVariablesForMapping(Mapping mapping, HashSet> generatedTypes) + private void GenerateMemoryVariablesForMapping(VariableDeclaration decl, Mapping mapping, HashSet generatedMaps, int lvl) { BoogieType boogieKeyType = TransUtils.GetBoogieTypeFromSolidityTypeName(mapping.KeyType); BoogieType boogieValType = null; if (mapping.ValueType is Mapping submapping) { boogieValType = BoogieType.Ref; - GenerateMemoryVariablesForMapping(submapping, generatedTypes); + GenerateMemoryVariablesForMapping(decl, submapping, generatedMaps, lvl + 1); + + // The last level gets initialized all at once + if (context.TranslateFlags.LazyAllocNoMod) + { + BoogieMapType mapType = new BoogieMapType(BoogieType.Ref, new BoogieMapType(boogieKeyType, BoogieType.Bool)); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(mapHelper.GetNestedAllocName(decl, lvl), mapType))); + } } else if (mapping.ValueType is ArrayTypeName array) { boogieValType = BoogieType.Ref; - GenerateMemoryVariablesForArray(array, generatedTypes); + GenerateMemoryVariablesForArray(decl, array, generatedMaps, lvl + 1); + + if (context.TranslateFlags.LazyAllocNoMod) + { + BoogieMapType mapType = new BoogieMapType(BoogieType.Ref, new BoogieMapType(boogieKeyType, BoogieType.Bool)); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(mapHelper.GetNestedAllocName(decl, lvl), mapType))); + } } else { @@ -695,47 +803,66 @@ private void GenerateMemoryVariablesForMapping(Mapping mapping, HashSet pair = new KeyValuePair(boogieKeyType, boogieValType); - if (!generatedTypes.Contains(pair)) - { - generatedTypes.Add(pair); - GenerateSingleMemoryVariable(boogieKeyType, boogieValType); - } + + GenerateSingleMemoryVariable(decl, boogieKeyType, boogieValType, generatedMaps); } - private void GenerateMemoryVariablesForArray(ArrayTypeName array, HashSet> generatedTypes) + private void GenerateMemoryVariablesForArray(VariableDeclaration decl, ArrayTypeName array, HashSet generatedMaps, int lvl) { BoogieType boogieKeyType = BoogieType.Int; BoogieType boogieValType = null; if (array.BaseType is ArrayTypeName subarray) { boogieValType = BoogieType.Ref; - GenerateMemoryVariablesForArray(subarray, generatedTypes); + GenerateMemoryVariablesForArray(decl, subarray, generatedMaps, lvl + 1); + + // The last level gets initialized all at once + if (context.TranslateFlags.LazyAllocNoMod) + { + BoogieMapType mapType = new BoogieMapType(BoogieType.Ref, new BoogieMapType(boogieKeyType, BoogieType.Bool)); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(mapHelper.GetNestedAllocName(decl, lvl), mapType))); + } } else if (array.BaseType is Mapping mapping) { boogieValType = BoogieType.Ref; - GenerateMemoryVariablesForMapping(mapping, generatedTypes); + GenerateMemoryVariablesForMapping(decl, mapping, generatedMaps, lvl + 1); + + if (context.TranslateFlags.LazyAllocNoMod) + { + BoogieMapType mapType = new BoogieMapType(BoogieType.Ref, new BoogieMapType(boogieKeyType, BoogieType.Bool)); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(mapHelper.GetNestedAllocName(decl, lvl), mapType))); + } } else { boogieValType = TransUtils.GetBoogieTypeFromSolidityTypeName(array.BaseType); } + + KeyValuePair pair = new KeyValuePair(boogieKeyType, boogieValType); - if (!generatedTypes.Contains(pair)) - { - generatedTypes.Add(pair); - GenerateSingleMemoryVariable(boogieKeyType, boogieValType); - } + GenerateSingleMemoryVariable(decl, boogieKeyType, boogieValType, generatedMaps); } - private void GenerateSingleMemoryVariable(BoogieType keyType, BoogieType valType) + private void GenerateSingleMemoryVariable(VariableDeclaration decl, BoogieType keyType, BoogieType valType, HashSet generatedMaps) { BoogieMapType map = new BoogieMapType(keyType, valType); map = new BoogieMapType(BoogieType.Ref, map); - string name = MapArrayHelper.GetMemoryMapName(keyType, valType); - context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(name, map))); + string name = mapHelper.GetMemoryMapName(decl, keyType, valType); + if (!generatedMaps.Contains(name)) + { + BoogieFunction initFn = MapArrayHelper.GenerateMultiDimZeroFunction(keyType, valType); + if (!context.initFns.Contains(initFn.Name)) + { + context.initFns.Add(initFn.Name); + context.Program.AddDeclaration(initFn); + } + + generatedMaps.Add(name); + context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(name, map))); + } } } } diff --git a/Sources/SolToBoogie/HarnessGenerator.cs b/Sources/SolToBoogie/HarnessGenerator.cs index a2710454..6a27bf59 100644 --- a/Sources/SolToBoogie/HarnessGenerator.cs +++ b/Sources/SolToBoogie/HarnessGenerator.cs @@ -1,5 +1,9 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using System; +using System.Numerics; + namespace SolToBoogie { using System.Collections.Generic; @@ -98,7 +102,8 @@ private void GenerateBoogieHarnessForContract(ContractDefinition contract, Dicti BoogieProcedure harness = new BoogieProcedure(harnessName, inParams, outParams); context.Program.AddDeclaration(harness); - List localVars = TransUtils.CollectLocalVars(new List() { contract }, context); + //List localVars = TransUtils.CollectLocalVars(new List() { contract }, context); + List localVars = CollectLocalVars(contract); localVars.Add(new BoogieLocalVariable(new BoogieTypedIdent("tmpNow", BoogieType.Int))); BoogieStmtList harnessBody = new BoogieStmtList(); harnessBody.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, new BoogieIdentifierExpr("now"), new BoogieLiteralExpr(0)))); @@ -158,6 +163,31 @@ private List GenerateConstructorCall(ContractDefinition contract) if (context.IsConstructorDefined(contract)) { FunctionDefinition ctor = context.GetConstructorByContract(contract); + if (ctor.StateMutability.Equals(EnumStateMutability.PAYABLE)) + { + BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, + new BoogieIdentifierExpr("msgvalue_MSG"), new BoogieLiteralExpr(BigInteger.Zero)); + localStmtList.Add(new BoogieAssumeCmd(assumeExpr)); + + localStmtList.Add(new BoogieCommentCmd("---- Logic for payable function START ")); + var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("msgsender_MSG")); + var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("this")); + var msgVal = new BoogieIdentifierExpr("msgvalue_MSG"); + //assume Balance[msg.sender] >= msg.value + localStmtList.Add(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgVal))); + //balance[msg.sender] = balance[msg.sender] - msg.value + localStmtList.Add(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal))); + //balance[this] = balance[this] + msg.value + localStmtList.Add(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); + localStmtList.Add(new BoogieCommentCmd("---- Logic for payable function END ")); + } + else + { + BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, + new BoogieIdentifierExpr("msgvalue_MSG"), new BoogieLiteralExpr(BigInteger.Zero)); + localStmtList.Add(new BoogieAssumeCmd(assumeExpr)); + } + foreach (VariableDeclaration param in ctor.Parameters.Parameters) { string name = TransUtils.GetCanonicalLocalVariableName(param, context); @@ -171,6 +201,12 @@ private List GenerateConstructorCall(ContractDefinition contract) } } } + else + { + BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, + new BoogieIdentifierExpr("msgvalue_MSG"), new BoogieLiteralExpr(BigInteger.Zero)); + localStmtList.Add(new BoogieAssumeCmd(assumeExpr)); + } if (context.TranslateFlags.InstrumentGas) { @@ -188,7 +224,8 @@ private BoogieWhileCmd GenerateWhileLoop(ContractDefinition contract, Dictionary BoogieStmtList body = GenerateHavocBlock(contract, localVars); // generate the choice block - body.AddStatement(TransUtils.GenerateChoiceBlock(new List() { contract }, context)); + //body.AddStatement(TransUtils.GenerateChoiceBlock(new List() { contract }, context)); + body.AddStatement(GenerateChoices(contract)); // generate candidate invariants for Houdini List candidateInvs = new List(); @@ -233,16 +270,22 @@ private BoogieStmtList GenerateHavocBlock(ContractDefinition contract, List localVars = RemoveThisFromVariables(TransUtils.CollectLocalVars(new List() { contract }, context)); + List localVars = RemoveThisFromVariables(CollectLocalVars(contract)); localVars.Add(new BoogieLocalVariable(new BoogieTypedIdent("tmpNow", BoogieType.Int))); BoogieStmtList procBody = GenerateHavocBlock(contract, localVars); - procBody.AddStatement(TransUtils.GenerateChoiceBlock(new List() { contract }, context)); + //procBody.AddStatement(TransUtils.GenerateChoiceBlock(new List() { contract }, context)); + procBody.AddStatement(GenerateChoices(contract)); BoogieImplementation procImpl = new BoogieImplementation(procName, inParams, outParams, localVars, procBody); context.Program.AddDeclaration(procImpl); } + private List CollectLocalVars(ContractDefinition contract) + { + List contracts = new List() {contract}; + + if (context.TranslateFlags.TxnsOnFields) + { + HashSet contractFields = context.GetStateVarsByContract(contract); + foreach (VariableDeclaration contractField in contractFields) + { + if (contractField.TypeDescriptions.IsContract() && contractField.TypeName is UserDefinedTypeName) + { + String fieldContractName = contractField.TypeName.ToString(); + ContractDefinition fieldDef = context.GetContractByName(fieldContractName); + contracts.Add(fieldDef); + } + } + } + + return TransUtils.CollectLocalVars(contracts, context); + } + + private BoogieIfCmd GenerateChoices(ContractDefinition contract) + { + BoogieExpr thisVal = new BoogieIdentifierExpr("this"); + Tuple curChoices = TransUtils.GeneratePartialChoiceBlock(new List() {contract}, context, thisVal, 0, context.TranslateFlags.ModelReverts); + if (context.TranslateFlags.TxnsOnFields) + { + HashSet contractFields = context.GetStateVarsByContract(contract); + + foreach (VariableDeclaration contractField in contractFields) + { + if (contractField.TypeDescriptions.IsContract() && contractField.TypeName is UserDefinedTypeName) + { + BoogieExpr fieldInstance = new BoogieMapSelect(new BoogieIdentifierExpr(TransUtils.GetCanonicalVariableName(contractField, context)), thisVal); + String fieldContractName = contractField.TypeName.ToString(); + ContractDefinition fieldDef = context.GetContractByName(fieldContractName); + curChoices = TransUtils.GeneratePartialChoiceBlock(new List() {fieldDef}, + context, fieldInstance, curChoices.Item2, context.TranslateFlags.ModelReverts, curChoices.Item1); + } + } + } + + return curChoices.Item1; + } + private void GenerateCorralHarnessForContract(ContractDefinition contract) { string harnessName = "CorralEntry_" + contract.Name; @@ -304,7 +393,11 @@ private void GenerateCorralHarnessForContract(ContractDefinition contract) harnessBody.AddStatement(new BoogieCallCmd("FreshRefGenerator", new List(), new List() {new BoogieIdentifierExpr("this")})); harnessBody.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, new BoogieIdentifierExpr("now"), new BoogieLiteralExpr(0)))); harnessBody.AddStatement(GenerateDynamicTypeAssumes(contract)); - GenerateConstructorCall(contract).ForEach(x => harnessBody.AddStatement(x)); + if (!context.TranslateFlags.PrePostHarness) + { + GenerateConstructorCall(contract).ForEach(x => harnessBody.AddStatement(x)); + } + if (context.TranslateFlags.ModelReverts) { BoogieExpr assumePred = new BoogieUnaryOperation(BoogieUnaryOperation.Opcode.NOT, new BoogieIdentifierExpr("revert")); @@ -315,20 +408,36 @@ private void GenerateCorralHarnessForContract(ContractDefinition contract) harnessBody.AddStatement(new BoogieAssumeCmd(assumePred)); } - harnessBody.AddStatement(GenerateCorralWhileLoop(contract)); + + if (context.TranslateFlags.PrePostHarness) + { + harnessBody.AddStatement(GenerateCorralCall(contract)); + BoogieStmtList body = new BoogieStmtList(); + harnessBody.AddStatement(new BoogieWhileCmd(new BoogieLiteralExpr(true), body)); + } + else + { + harnessBody.AddStatement(GenerateCorralWhileLoop(contract)); + } + BoogieImplementation harnessImpl = new BoogieImplementation(harnessName, inParams, outParams, localVars, harnessBody); context.Program.AddDeclaration(harnessImpl); } - private BoogieWhileCmd GenerateCorralWhileLoop(ContractDefinition contract) + private BoogieCallCmd GenerateCorralCall(ContractDefinition contract) { - BoogieStmtList body = new BoogieStmtList(); string callee = "CorralChoice_" + contract.Name; List inputs = new List() { new BoogieIdentifierExpr("this"), }; - body.AddStatement(new BoogieCallCmd(callee, inputs, null)); + + return new BoogieCallCmd(callee, inputs, null); + } + private BoogieWhileCmd GenerateCorralWhileLoop(ContractDefinition contract) + { + BoogieStmtList body = new BoogieStmtList(); + body.AddStatement(GenerateCorralCall(contract)); List candidateInvs = new List(); // add the contract invariant if present diff --git a/Sources/SolToBoogie/MapArrayHelper.cs b/Sources/SolToBoogie/MapArrayHelper.cs index bd7fa1d3..a9b7a691 100644 --- a/Sources/SolToBoogie/MapArrayHelper.cs +++ b/Sources/SolToBoogie/MapArrayHelper.cs @@ -1,5 +1,12 @@ -// Copyright (c) Microsoft Corporation. All rights reserved. +// Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using System.Collections.Generic; +using System.Runtime.CompilerServices; +using Microsoft.Extensions.Primitives; +using solidityAnalysis; +using SolidityAST; + namespace SolToBoogie { using System; @@ -10,23 +17,96 @@ public class MapArrayHelper { private static Regex mappingRegex = new Regex(@"mapping\((\w+)\s*\w*\s*=>\s*(.+)\)$"); //mapping(string => uint) appears as mapping(string memory => uint) - private static Regex arrayRegex = new Regex(@"(.+)\[\w*\] (storage ref|storage pointer|memory|calldata)$"); + private static Regex arrayRegex = new Regex(@"(.+)\[\w*\]( storage ref| storage pointer| memory| calldata)?$"); // mapping (uint => uint[]) does not have storage/memory in Typestring // private static Regex arrayRegex = new Regex(@"(.+)\[\w*\]$"); + + private TranslatorContext context { get; } + + private AST solidityAst { get; } + + public MapArrayHelper(TranslatorContext ctxt, AST solidityAst) + { + this.context = ctxt; + this.solidityAst = solidityAst; + } + + public Boolean notAliased(VariableDeclaration decl) + { + return context.TranslateFlags.RunAliasAnalysis && context.Analysis.Alias.getResults().Contains(decl); + } - public static string GetMemoryMapName(BoogieType keyType, BoogieType valType) + public static string GetCanonicalMemName(BoogieType keyType, BoogieType valType) { return "M_" + keyType.ToString() + "_" + valType.ToString(); } - public static BoogieExpr GetMemoryMapSelectExpr(BoogieType mapKeyType, BoogieType mapValType, BoogieExpr baseExpr, BoogieExpr indexExpr) + public VariableDeclaration getDecl(Expression access) { - string mapName = GetMemoryMapName(mapKeyType, mapValType); + DeclarationFinder declFinder = new DeclarationFinder(access, solidityAst); + return declFinder.getDecl(); + } + + public string GetMemoryMapName(VariableDeclaration decl, BoogieType keyType, BoogieType valType) + { + if (notAliased(decl) && !context.TranslateFlags.UseMultiDim) + { + return GetCanonicalMemName(keyType, valType) + "_" + context.Analysis.Alias.getGroupName(decl); + } + + return GetCanonicalMemName(keyType, valType); + } + + public BoogieExpr GetMemoryMapSelectExpr(VariableDeclaration decl, BoogieType mapKeyType, BoogieType mapValType, BoogieExpr baseExpr, BoogieExpr indexExpr) + { + string mapName = GetMemoryMapName(decl, mapKeyType, mapValType); BoogieIdentifierExpr mapIdent = new BoogieIdentifierExpr(mapName); BoogieMapSelect mapSelectExpr = new BoogieMapSelect(mapIdent, baseExpr); mapSelectExpr = new BoogieMapSelect(mapSelectExpr, indexExpr); return mapSelectExpr; } + + public static String GetCanonicalSumName() + { + return "sum"; + } + + public String GetSumName(VariableDeclaration decl) + { + if (notAliased(decl)) + { + return GetCanonicalSumName() + "_" + context.Analysis.Alias.getGroupName(decl); + } + + return GetCanonicalSumName(); + } + + public BoogieExpr GetSumExpr(VariableDeclaration decl, BoogieExpr varExpr) + { + BoogieIdentifierExpr sumIdent = new BoogieIdentifierExpr(GetSumName(decl)); + BoogieMapSelect sumSelect = new BoogieMapSelect(sumIdent, varExpr); + return sumSelect; + } + + public static BoogieType InferExprTypeFromTupleTypeString(string typeString, int ind) + { + if (!typeString.StartsWith("tuple")) + { + return null; + } + + int start = typeString.IndexOf("("); + int end = typeString.IndexOf(")"); + + String[] tupleTypes = typeString.Substring(start + 1, end - start - 1).Split(","); + + if (ind >= tupleTypes.Length) + { + return null; + } + + return InferExprTypeFromTypeString(tupleTypes[ind]); + } public static BoogieType InferExprTypeFromTypeString(string typeString) { @@ -54,7 +134,7 @@ public static BoogieType InferExprTypeFromTypeString(string typeString) else if (typeString.StartsWith("int") && !typeString.Contains("[")) { return BoogieType.Int; - } + } else if (typeString.StartsWith("byte") && !typeString.Contains("[")) { return BoogieType.Int; @@ -97,9 +177,9 @@ public static BoogieType InferKeyTypeFromTypeString(string typeString) { return BoogieType.Ref; } - else if (typeString.StartsWith("bytes") && !typeString.Equals("bytes")) - { - return BoogieType.Int; + else if (typeString.StartsWith("bytes") && !typeString.Equals("bytes")) + { + return BoogieType.Int; } else { @@ -123,9 +203,9 @@ public static BoogieType InferValueTypeFromTypeString(string typeString) { return BoogieType.Ref; } - else if (typeString.StartsWith("bytes") && !typeString.Equals("bytes")) - { - return BoogieType.Int; + else if (typeString.StartsWith("bytes") && !typeString.Equals("bytes")) + { + return BoogieType.Int; } else { @@ -149,6 +229,22 @@ public static string GetValueTypeString(string typeString) return null; } + + public static string GetIndexTypeString(string typeString) + { + if (mappingRegex.IsMatch(typeString)) + { + Match match = mappingRegex.Match(typeString); + return match.Groups[1].Value; + } + + if (arrayRegex.IsMatch(typeString)) + { + return "uint256"; + } + + return null; + } public static bool IsMappingTypeString(string typeString) { @@ -159,5 +255,313 @@ public static bool IsArrayTypeString(string typeString) { return arrayRegex.IsMatch(typeString); } + + public string GetNestedAllocName(VariableDeclaration decl, int lvl) + { + return "alloc_" + TransUtils.GetCanonicalVariableName(decl, context) + "_lvl" + lvl; + } + + public static BoogieFuncCallExpr GetCallExprForZeroInit(BoogieType key, BoogieType value) + { + /*var keyStr = char.ToUpper(key.ToString()[0]) + key.ToString().Substring(1); + var valStr = char.ToUpper(value.ToString()[0]) + value.ToString().Substring(1);*/ + return new BoogieFuncCallExpr("zero" + key.ToString() + value.ToString() + "Arr", new List()); + } + + public static string GetSmtType(BoogieType type) + { + if (type.Equals(BoogieType.Bool)) + { + return "Bool"; + } + else if (type.Equals(BoogieType.Int)) + { + return "Int"; + } + else if (type.Equals(BoogieType.Ref)) + { + return "Int"; + } + + throw new Exception($"Unknown BoogieType {type}"); + } + + public static BoogieFunction GenerateMultiDimZeroFunction(BoogieType keyType, BoogieType valType) + { + BoogieExpr boogieInit = TransUtils.GetDefaultVal(valType); + string smtType = GetSmtType(valType); + BoogieType mapType = new BoogieMapType(keyType, valType); + string fnName = $"zero{keyType.ToString()}{valType.ToString()}Arr"; + + string smtInit = boogieInit.ToString().Equals("null") ? "0" : boogieInit.ToString(); + smtInit = $"((as const (Array {GetSmtType(keyType)} {smtType})) {smtInit})"; + + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", mapType)); + var smtDefinedAttr = new BoogieAttribute("smtdefined", $"\"{smtInit}\""); + return new BoogieFunction(fnName, new List(), new List() {outVar}, new List() {smtDefinedAttr}); + } + + public static BoogieFunction GenerateMultiDimZeroFunction(VariableDeclaration decl) + { + TypeName curType = decl.TypeName; + List boogieType = new List(); + + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping map) + { + boogieType.Insert(0, TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType)); + curType = map.ValueType; + } + else if(curType is ArrayTypeName arr) + { + boogieType.Insert(0, BoogieType.Int); + curType = arr.BaseType; + } + } + + BoogieType valType = TransUtils.GetBoogieTypeFromSolidityTypeName(curType); + BoogieExpr boogieInit = TransUtils.GetDefaultVal(valType); + + string smtType = GetSmtType(valType); + string smtInit = boogieInit.ToString().Equals("null") ? "0" : boogieInit.ToString(); + BoogieType mapType = valType; + string fnName = $"{valType.ToString()}Arr"; + + foreach (BoogieType type in boogieType) + { + smtType = $"(Array {GetSmtType(type)} {smtType})"; + mapType = new BoogieMapType(type, mapType); + smtInit = $"((as const {smtType}) {smtInit})"; + fnName = $"{type.ToString()}{fnName}"; + } + + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", mapType)); + var smtDefinedAttr = new BoogieAttribute("smtdefined", $"\"{smtInit}\""); + return new BoogieFunction($"zero{fnName}", new List(), new List() {outVar}, new List() {smtDefinedAttr}); + } + + public static BoogieFunction GenerateMultiDimInitFunction(BoogieMapType type) + { + BoogieType curType = type; + List boogieType = new List(); + + while (curType is BoogieMapType map) + { + if (map.Arguments.Count != 1) + { + throw new Exception("Boogie map must have one argument"); + } + boogieType.Insert(0, map.Arguments[0]); + curType = map.Result; + } + + BoogieVariable arg = new BoogieFormalParam(new BoogieTypedIdent("n", curType)); + string smtInit = "n"; + string smtType = GetSmtType(curType); + string fnName = $"{curType.ToString()}Arr"; + + foreach (BoogieType dimType in boogieType) + { + smtType = $"(Array {GetSmtType(dimType)} {smtType})"; + smtInit = $"((as const {smtType}) {smtInit})"; + fnName = $"{dimType.ToString()}{fnName}"; + } + + var outVar = new BoogieFormalParam(new BoogieTypedIdent("ret", type)); + var smtDefinedAttr = new BoogieAttribute("smtdefined", $"\"{smtInit}\""); + return new BoogieFunction($"init{fnName}", new List() {arg}, new List() {outVar}, new List() {smtDefinedAttr}); + } + + public static BoogieExpr GetCallExprForInit(BoogieType curType, BoogieExpr initExpr) + { + if (!(curType is BoogieMapType)) + { + return initExpr; + } + + string fnName = "init"; + + while (curType is BoogieMapType map) + { + fnName = $"{fnName}{String.Join("", map.Arguments)}"; + curType = map.Result; + } + + fnName = $"{fnName}{curType}Arr"; + return new BoogieFuncCallExpr(fnName, new List() {initExpr}); + } + + public static BoogieFuncCallExpr GetCallExprForZeroInit(BoogieType curType) + { + string fnName = "zero"; + + while (curType is BoogieMapType map) + { + fnName = $"{fnName}{String.Join("", map.Arguments)}"; + curType = map.Result; + } + + fnName = $"{fnName}{curType}Arr"; + return new BoogieFuncCallExpr(fnName, new List()); + } + + public static BoogieFuncCallExpr GetCallExprForZeroInit(TypeName curType) + { + string fnName = "zero"; + + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping map) + { + fnName = $"{fnName}{TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType).ToString()}"; + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + fnName = $"{fnName}{BoogieType.Int.ToString()}"; + curType = arr.BaseType; + } + } + + fnName = $"{fnName}{TransUtils.GetBoogieTypeFromSolidityTypeName(curType).ToString()}Arr"; + return new BoogieFuncCallExpr(fnName, new List()); + } + public static BoogieFuncCallExpr GetCallExprForZeroInit(VariableDeclaration decl) + { + return GetCallExprForZeroInit(decl.TypeName); + } + + public static BoogieType GetMultiDimBoogieType(TypeName varType) + { + if (!(varType is Mapping || varType is ArrayTypeName)) + { + return TransUtils.GetBoogieTypeFromSolidityTypeName(varType); + } + + BoogieType resultType = null; + if (varType is Mapping map) + { + BoogieType valType = GetMultiDimBoogieType(map.ValueType); + BoogieType keyType = GetMultiDimBoogieType(map.KeyType); + resultType = new BoogieMapType(keyType, valType); + } + else if (varType is ArrayTypeName arr) + { + BoogieType baseType = GetMultiDimBoogieType(arr.BaseType); + resultType = new BoogieMapType(BoogieType.Int, baseType); + } + + return resultType; + } + + public static TypeName GetMappedType(VariableDeclaration varDecl) + { + TypeName curType = varDecl.TypeName; + + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping map) + { + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + curType = arr.BaseType; + } + } + + return curType; + } + + public string GetMultiDimLengthName(VariableDeclaration varDecl, int lvl) + { + return $"Length_{TransUtils.GetCanonicalVariableName(varDecl, context)}_lvl{lvl}"; + } + + public List GetMultiDimArrayLens(VariableDeclaration decl) + { + List lenVars = new List(); + TypeName curType = decl.TypeName; + + List indTypes = new List() {BoogieType.Ref}; + + int lvl = 0; + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping map) + { + curType = map.ValueType; + indTypes.Add(TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType)); + } + else if (curType is ArrayTypeName arr) + { + BoogieType mapType = BoogieType.Int; + BoogieType initType = BoogieType.Int; + for (int i = indTypes.Count - 1; i >= 0; i--) + { + initType = mapType; + mapType = new BoogieMapType(indTypes[i], mapType); + } + + if (arr.Length != null && initType is BoogieMapType lenMap) + { + BoogieFunction initFn = GenerateMultiDimInitFunction(lenMap); + lenVars.Add(initFn); + } + + BoogieGlobalVariable lenVar = new BoogieGlobalVariable(new BoogieTypedIdent(GetMultiDimLengthName(decl, lvl), mapType)); + lenVars.Add(lenVar); + + curType = arr.BaseType; + indTypes.Add(BoogieType.Int); + } + + lvl++; + } + + return lenVars; + } + + public BoogieExpr GetLength(VariableDeclaration varDecl, BoogieExpr receiver) + { + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(varDecl)) + { + BoogieExpr curExpr = receiver; + int lvl = -1; + List keys = new List(); + while (curExpr is BoogieMapSelect sel) + { + curExpr = sel.BaseExpr; + keys.Insert(0, sel.Arguments[0]); + lvl++; + } + + string lenName = GetMultiDimLengthName(varDecl, lvl); + BoogieExpr lenExpr = new BoogieIdentifierExpr(lenName); + + foreach (BoogieExpr key in keys) + { + lenExpr = new BoogieMapSelect(lenExpr, key); + } + + return lenExpr; + } + + return new BoogieMapSelect(new BoogieIdentifierExpr("Length"), receiver); + } + + public BoogieExpr GetLength(Expression solExpr, BoogieExpr receiver) + { + VariableDeclaration decl = getDecl(solExpr); + + //this can happen in the case of newExpression + if (decl == null) + { + return new BoogieMapSelect(new BoogieIdentifierExpr("Length"), receiver); + } + + return GetLength(decl, receiver); + } } } diff --git a/Sources/SolToBoogie/ModifierCollector.cs b/Sources/SolToBoogie/ModifierCollector.cs index 30e96611..1b4961b6 100644 --- a/Sources/SolToBoogie/ModifierCollector.cs +++ b/Sources/SolToBoogie/ModifierCollector.cs @@ -15,12 +15,10 @@ namespace SolToBoogie public class ModifierCollector : BasicASTVisitor { private TranslatorContext context; - private ProcedureTranslator localTranslator; public ModifierCollector(TranslatorContext context) { this.context = context; - this.localTranslator = new ProcedureTranslator(context); } public override bool Visit(ModifierDefinition modifier) diff --git a/Sources/SolToBoogie/ParseUtils.cs b/Sources/SolToBoogie/ParseUtils.cs index 6c51ec21..68fdae96 100644 --- a/Sources/SolToBoogie/ParseUtils.cs +++ b/Sources/SolToBoogie/ParseUtils.cs @@ -4,6 +4,7 @@ using System.Diagnostics; using System.Linq; using System.Text; +using BoogieAST; namespace SolToBoogie { @@ -44,6 +45,18 @@ public static void ParseCommandLineArgs(string[] args, out string solidityFile, var contract = str.Substring(str.IndexOf("@") + 1); ignoredMethods.Add(Tuple.Create(method, contract)); } + + foreach (var arg in args.Where(x => x.StartsWith("/SliceFunctions:"))) + { + var str = arg.Substring("/SliceFunctions:".Length); + String[] fns = str.Split(","); + translatorFlags.PerformFunctionSlice = true; + foreach (String fn in fns) + { + translatorFlags.SliceFunctionNames.Add(fn); + } + } + if (args.Any(x => x.StartsWith("/ignoreMethod:"))) { Console.WriteLine($"Ignored method/contract pairs ==> \n\t {string.Join(",", ignoredMethods.Select(x => x.Item1 + "@" + x.Item2))}"); @@ -114,8 +127,8 @@ public static void ParseCommandLineArgs(string[] args, out string solidityFile, { Debug.Assert(stubModels.Count() == 1, "Multiple instances of /stubModel:"); var model = stubModels.First().Substring("/stubModel:".Length); - Debug.Assert(model.Equals("skip") || model.Equals("havoc") || model.Equals("callback"), - $"The argument to /stubModel: can be either {{skip, havoc, callback}}, found {model}"); + Debug.Assert(model.Equals("skip") || model.Equals("havoc") || model.Equals("callback") || model.Equals("multipleCallbacks"), + $"The argument to /stubModel: can be either {{skip, havoc, callback, multipleCallbacks}}, found {model}"); translatorFlags.ModelOfStubs = model; } if (args.Any(x => x.StartsWith("/inlineDepth:"))) @@ -138,6 +151,13 @@ public static void ParseCommandLineArgs(string[] args, out string solidityFile, translatorFlags.LazyNestedAlloc = true; } + if (args.Any(x => x.Equals("/LazyAllocNoMod"))) + { + translatorFlags.LazyNestedAlloc = true; + translatorFlags.LazyAllocNoMod = true; + translatorFlags.QuantFreeAllocs = true; + } + if (args.Any(x => x.Equals("/OmitAssumeFalseForDynDispatch"))) { translatorFlags.OmitAssumeFalseForDynDispatch = true; @@ -152,11 +172,63 @@ public static void ParseCommandLineArgs(string[] args, out string solidityFile, translatorFlags.LazyNestedAlloc = true; } + if (args.Any(x => x.Equals("/allowTxnsFromContract"))) + { + translatorFlags.NoTxnsFromContract = false; + } + if (args.Any(x => x.Equals("/instrumentSums"))) { translatorFlags.InstrumentSums = true; } + if (args.Any(x => x.Equals("/alias"))) + { + translatorFlags.RunAliasAnalysis = true; + } + + if (args.Any(x => x.Equals("/useMultiDim"))) + { + translatorFlags.RunAliasAnalysis = true; + translatorFlags.UseMultiDim = true; + } + + if (args.Any(x => x.Equals("/txnsOnFields"))) + { + translatorFlags.TxnsOnFields = true; + } + + if (args.Any(x => x.Equals("/noNonlinearArith"))) + { + translatorFlags.NoNonlinearArith = true; + } + + if (args.Any(x => x.Equals("/useNumericOperators"))) + { + translatorFlags.UseNumericOperators = true; + BoogieBinaryOperation.USE_ARITH_OPS = true; + } + + if (args.Any(x => x.Equals("/prePostHarness"))) + { + translatorFlags.PrePostHarness = true; + } + + if (args.Any(x => x.Equals("/generateGetters"))) + { + translatorFlags.GenerateGetters = true; + } + + if (args.Any(x => x.Equals("/generateERC20Spec"))) + { + translatorFlags.GenerateERC20Spec = true; + } + + if (args.Any(x => x.Equals("/modelAssemblyAsHavoc"))) + { + translatorFlags.AssemblyAsHavoc = true; + } + translatorFlags.PerformContractInferce = args.Any(x => x.StartsWith("/contractInfer")); // don't perform verification for some of these omitFlags diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs index 00ac9b07..be39d939 100644 --- a/Sources/SolToBoogie/ProcedureTranslator.cs +++ b/Sources/SolToBoogie/ProcedureTranslator.cs @@ -1,5 +1,8 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using Newtonsoft.Json.Linq; + namespace SolToBoogie { using System; @@ -44,6 +47,8 @@ public class ProcedureTranslator : BasicASTVisitor // to collect contract invariants private Dictionary> contractInvariants = null; + private MapArrayHelper mapHelper; + private static void emitGasCheck(BoogieStmtList newBody) { BoogieStmtList thenBody = new BoogieStmtList(); @@ -74,9 +79,10 @@ private void preTranslationAction(ASTNode node) } } - public ProcedureTranslator(TranslatorContext context, bool _genInlineAttrsInBpl = true) + public ProcedureTranslator(TranslatorContext context, MapArrayHelper mapHelper, bool _genInlineAttrsInBpl = true) { this.context = context; + this.mapHelper = mapHelper; boogieToLocalVarsMap = new Dictionary>(); genInlineAttrsInBpl = _genInlineAttrsInBpl; contractInvariants = new Dictionary>(); @@ -130,12 +136,166 @@ private void TranslateStructDefinition(StructDefinition structDefn) } } + private String GetAccessPattern(VariableDeclaration varDecl, String boogieName) + { + Identifier varIdent = new Identifier(); + varIdent.Name = varDecl.Name; + varIdent.OverloadedDeclarations = new List(); + varIdent.ReferencedDeclaration = varDecl.Id; + varIdent.TypeDescriptions = varDecl.TypeDescriptions; + + Expression varExpr = varIdent; + + TypeName curType = varDecl.TypeName; + List localIds = new List(); + + int i = 1; + while (curType is Mapping || curType is ArrayTypeName) + { + ElementaryTypeName indType = null; + if (curType is Mapping map) + { + indType = map.KeyType; + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + TypeDescription intDescription = new TypeDescription(); + intDescription.TypeString = "uint"; + ElementaryTypeName intTypeName = new ElementaryTypeName(); + intTypeName.TypeDescriptions = intDescription; + indType = intTypeName; + curType = arr.BaseType; + } + + VariableDeclaration local = new VariableDeclaration(); + local.Constant = false; + local.Indexed = false; + local.Name = $"i{i}"; + local.Value = null; + local.Visibility = EnumVisibility.DEFAULT; + local.StateVariable = false; + local.StorageLocation = EnumLocation.DEFAULT; + local.TypeName = indType; + local.TypeDescriptions = indType.TypeDescriptions; + int id = -1 - i; + localIds.Add(id); + + //remove later + context.IdToNodeMap.Add(id, local); + + IndexAccess access = new IndexAccess(); + access.BaseExpression = varExpr; + Identifier localIdent = new Identifier(); + localIdent.Name = $"i{i}"; + localIdent.OverloadedDeclarations = new List(); + localIdent.ReferencedDeclaration = id; + localIdent.TypeDescriptions = local.TypeDescriptions; + access.IndexExpression = localIdent; + access.TypeDescriptions = TransUtils.TypeNameToTypeDescription(curType); + //access.TypeDescriptions.TypeString = curType.ToString(); + + varExpr = access; + i++; + } + + BoogieStmtList oldList = currentStmtList; + BoogieExpr oldExpr = currentExpr; + currentBoogieProc = ""; + currentExpr = null; + currentStmtList = new BoogieStmtList(); + this.boogieToLocalVarsMap.Add(currentBoogieProc, new List()); + + if (varExpr is Identifier ident) + { + Visit(ident); + } + else if (varExpr is IndexAccess access) + { + Visit(access); + } + + BoogieExpr translatedExpr = currentExpr; + currentExpr = oldExpr; + currentStmtList = oldList; + this.boogieToLocalVarsMap.Remove(currentBoogieProc); + currentBoogieProc = null; + string accessPattern = $"this.{varExpr}={translatedExpr}"; + + for (int j = 1; j < i; j++) + { + accessPattern = Regex.Replace(accessPattern, $"i{j}" + @"_[^\]]+", $"i{j}"); + } + + foreach(int id in localIds) + { + context.IdToNodeMap.Remove(id); + } + + return $"\"{accessPattern}\""; + + /*String solAccess = $"this.{varDecl.Name}"; + String boogieAccess = $"{boogieName}[this]"; + TypeName solType = varDecl.TypeName; + int dim = 0; + + while (solType is Mapping || solType is ArrayTypeName) + { + String dimName = $"i{dim}"; + dim++; + BoogieType keyType = null; + BoogieType valType = null; + + if (solType is Mapping map) + { + keyType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType); + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.ValueType); + solType = map.ValueType; + } + else if (solType is ArrayTypeName arr) + { + keyType = BoogieType.Int; + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(arr.BaseType); + solType = arr.BaseType; + } + + String memMap = mapHelper.GetMemoryMapName(varDecl, keyType, valType); + solAccess = $"{solAccess}[{dimName}]"; + boogieAccess = $"{memMap}[{boogieAccess}][{dimName}]"; + } + + return $"\"{solAccess}={boogieAccess}\"";*/ + } + + private String GetSumAccessPattern(VariableDeclaration varDecl, String boogieName) + { + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(varDecl)) + { + return $"\"sum(this.{varDecl.Name})={mapHelper.GetSumName(varDecl)}[this]\""; + } + + return $"\"sum(this.{varDecl.Name})={mapHelper.GetSumName(varDecl)}[{boogieName}[this]]\""; + } + private void TranslateStateVarDeclaration(VariableDeclaration varDecl) { VeriSolAssert(varDecl.StateVariable, $"{varDecl} is not a state variable"); string name = TransUtils.GetCanonicalStateVariableName(varDecl, context); - BoogieType type = TransUtils.GetBoogieTypeFromSolidityTypeName(varDecl.TypeName); + + BoogieType type = null; + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(varDecl)) + { + List lenVars = mapHelper.GetMultiDimArrayLens(varDecl); + lenVars.ForEach(context.Program.AddDeclaration); + + type = MapArrayHelper.GetMultiDimBoogieType(varDecl.TypeName); + } + else + { + type = TransUtils.GetBoogieTypeFromSolidityTypeName(varDecl.TypeName); + } + BoogieMapType mapType = new BoogieMapType(BoogieType.Ref, type); // Issue a warning for intXX variables in case /useModularArithemtic option is used: @@ -143,19 +303,37 @@ private void TranslateStateVarDeclaration(VariableDeclaration varDecl) { Console.WriteLine($"Warning: signed integer arithmetic is not handled with /useModularArithmetic option"); } - + if (varDecl.TypeName is Mapping) { - context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType))); + BoogieGlobalVariable global = new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType)); + global.Attributes = new List(); + global.Attributes.Add(new BoogieAttribute("access", GetAccessPattern(varDecl, name))); + if (context.TranslateFlags.InstrumentSums) + { + global.Attributes.Add(new BoogieAttribute("sum", GetSumAccessPattern(varDecl, name))); + } + context.Program.AddDeclaration(global); } else if (varDecl.TypeName is ArrayTypeName) { //array variables can be assigned - context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType))); + BoogieGlobalVariable global = new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType)); + global.Attributes = new List(); + global.Attributes.Add(new BoogieAttribute("access", GetAccessPattern(varDecl, name))); + if (context.TranslateFlags.InstrumentSums) + { + global.Attributes.Add(new BoogieAttribute("sum", GetSumAccessPattern(varDecl, name))); + } + + context.Program.AddDeclaration(global); } else // other type of state variables { - context.Program.AddDeclaration(new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType))); + BoogieGlobalVariable global = new BoogieGlobalVariable(new BoogieTypedIdent(name, mapType)); + global.Attributes = new List(); + global.Attributes.Add(new BoogieAttribute("access", GetAccessPattern(varDecl, name))); + context.Program.AddDeclaration(global); } } @@ -276,6 +454,18 @@ private void PrintArguments(FunctionDefinition node, List inPara } public override bool Visit(FunctionDefinition node) { + if (context.TranslateFlags.PerformFunctionSlice) + { + /*if (!node.IsConstructor && !node.IsFallback && !context.TranslateFlags.SliceFunctions.Contains(node)) + { + return false; + } */ + if (!context.TranslateFlags.SliceFunctions.Contains(node)) + { + return false; + } + } + preTranslationAction(node); // VeriSolAssert(node.IsConstructor || node.Modifiers.Count <= 1, "Multiple Modifiers are not supported yet"); VeriSolAssert(currentContract != null); @@ -283,11 +473,16 @@ public override bool Visit(FunctionDefinition node) currentFunction = node; // procedure name - string procName = node.Name + "_" + currentContract.Name; + //string procName = node.Name + "_" + currentContract.Name; + string procName = null; if (node.IsConstructor) { - procName += "_NoBaseCtor"; + procName = $"{TransUtils.GetCanonicalConstructorName(currentContract)}_NoBaseCtor"; + } + else + { + procName = TransUtils.GetCanonicalFunctionName(node, context); } currentBoogieProc = procName; @@ -319,6 +514,12 @@ public override bool Visit(FunctionDefinition node) { attributes.Add(new BoogieAttribute("public")); } + + if (node.StateMutability == EnumStateMutability.PAYABLE) + { + attributes.Add(new BoogieAttribute("payable")); + } + // generate inline attribute for a function only when /noInlineAttrs is specified if (genInlineAttrsInBpl) attributes.Add(new BoogieAttribute("inline", 1)); @@ -359,7 +560,7 @@ public override bool Visit(FunctionDefinition node) procBody.AppendStmtList(assumesForParamsAndReturn); // if payable, then modify the balance - if (node.StateMutability == EnumStateMutability.PAYABLE) + /*if (node.StateMutability == EnumStateMutability.PAYABLE) { procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("msgsender_MSG")); @@ -372,7 +573,7 @@ public override bool Visit(FunctionDefinition node) //balance[this] = balance[this] + msg.value procBody.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); - } + }*/ // if (node.Modifiers.Count == 1) for (int i = 0; i < node.Modifiers.Count; ++i) @@ -505,6 +706,14 @@ private bool IsVeriSolContractInvariantFunction(FunctionDefinition node, BoogieS public override bool Visit(ModifierDefinition node) { + if (context.TranslateFlags.PerformFunctionSlice) + { + if (!context.TranslateFlags.SliceModifiers.Contains(node)) + { + return false; + } + } + preTranslationAction(node); currentBoogieProc = node.Name + "_pre"; boogieToLocalVarsMap[currentBoogieProc] = new List(); @@ -580,11 +789,11 @@ private BoogieStmtList GenerateInitializationStmts(ContractDefinition contract) BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.NEQ, assumeLhs, new BoogieIdentifierExpr("null")); BoogieAssumeCmd assumeCmd = new BoogieAssumeCmd(assumeExpr); currentStmtList.AddStatement(assumeCmd); - + BoogieAssignCmd balanceInit = new BoogieAssignCmd( new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("this")), - new BoogieLiteralExpr(0)); + new BoogieIdentifierExpr("msgvalue_MSG")); currentStmtList.AddStatement(balanceInit); foreach (VariableDeclaration varDecl in context.GetStateVarsByContract(contract)) @@ -618,9 +827,162 @@ private BoogieStmtList GenerateInitializationStmts(ContractDefinition contract) return currentStmtList; } + + public BoogieStmtList GetMultiDimInitialization(VariableDeclaration decl, BoogieMapSelect contractVar, bool quantFree) + { + BoogieStmtList init = new BoogieStmtList(); + if (quantFree) + { + TypeName type = decl.TypeName; + + int curLvl = 0; + List indTypes = new List() {}; + while (type is Mapping || type is ArrayTypeName) + { + if (type is Mapping map) + { + type = map.ValueType; + indTypes.Add(TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType)); + } + else if (type is ArrayTypeName arr) + { + /*ArrayTypeName lenType = new ArrayTypeName(); + ElementaryTypeName intType = new ElementaryTypeName(); + intType.TypeDescriptions = new TypeDescription(); + intType.TypeDescriptions.TypeString = "uint"; + lenType.BaseType = intType; + + if (arr.Length != null) + { + throw new Exception("Must add support for static arrays"); + } + + BoogieFuncCallExpr lenZero = MapArrayHelper.GetCallExprForZeroInit(lenType); + + string lenName = MapArrayHelper.GetMultiDimLengthName(decl, curLvl); + BoogieMapSelect lenAccess = new BoogieMapSelect(new BoogieIdentifierExpr(lenName), contractVar.Arguments); + init.AddStatement(new BoogieAssignCmd(lenAccess, lenZero));*/ + + BoogieExpr initVal = null; + if (arr.Length == null) + { + initVal = new BoogieLiteralExpr(BigInteger.Zero); + } + else + { + initVal = TranslateExpr(arr.Length); + } + + BoogieType lenType = BoogieType.Int; + BoogieType initType = BoogieType.Int; + for (int i = indTypes.Count - 1; i >= 0; i--) + { + initType = lenType; + lenType = new BoogieMapType(indTypes[i], lenType); + } + + String lenName = mapHelper.GetMultiDimLengthName(decl, curLvl); + BoogieMapSelect lenAccess = new BoogieMapSelect(new BoogieIdentifierExpr(lenName), contractVar.Arguments); + + BoogieExpr lenZero = MapArrayHelper.GetCallExprForInit(initType, initVal); + /*if (lenZero is BoogieFuncCallExpr callExpr && !context.initFns.Contains(callExpr.Function)) + { + MapArrayHelper.Generate + }*/ + /*if (lenType is BoogieMapType) + { + lenZero = + } + else + { + lenZero = new BoogieLiteralExpr(BigInteger.Zero); + }*/ + + init.AddStatement(new BoogieAssignCmd(lenAccess, lenZero)); + + type = arr.BaseType; + indTypes.Add(BoogieType.Int); + } + + curLvl++; + } + + init.AddStatement(new BoogieAssignCmd(contractVar, MapArrayHelper.GetCallExprForZeroInit(decl))); + return init; + } + + List qvars = new List(); + List qVarTypes = new List(); + BoogieExpr accessExpr = contractVar; + + int lvl = 0; + TypeName curType = decl.TypeName; + while (curType is Mapping || curType is ArrayTypeName) + { + var qVar = QVarGenerator.NewQVar(0, lvl); + qvars.Add(qVar); + + if (curType is Mapping map) + { + qVarTypes.Add(TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType)); + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + qVarTypes.Add(BoogieType.Int); + string lenName = mapHelper.GetMultiDimLengthName(decl, lvl); + BoogieMapSelect lenAccess = new BoogieMapSelect(new BoogieIdentifierExpr(lenName), contractVar.Arguments[0]); + + List lenQVars = new List(); + List lenQVarTypes = new List(); + for (int i = 0; i < qvars.Count - 1; i++) + { + lenAccess = new BoogieMapSelect(lenAccess, qvars[i]); + lenQVars.Add(qvars[i]); + lenQVarTypes.Add(qVarTypes[i]); + } + /*foreach (BoogieIdentifierExpr qv in qvars) + { + lenAccess = new BoogieMapSelect(lenAccess, qv); + }*/ + + var lengthExpr = arr.Length == null ? TransUtils.GetDefaultVal(BoogieType.Int) : TranslateExpr(arr.Length); + BoogieExpr lenExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, lenAccess, lengthExpr); + if (lenQVars.Count != 0) + { + lenExpr = new BoogieQuantifiedExpr(true, lenQVars, lenQVarTypes, lenExpr); + } + + init.AddStatement(new BoogieAssumeCmd(lenExpr)); + + curType = arr.BaseType; + } + + accessExpr = new BoogieMapSelect(accessExpr, qVar); + lvl++; + } + + BoogieQuantifiedExpr qExpr = new BoogieQuantifiedExpr(true, qvars, qVarTypes, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, accessExpr, TransUtils.GetDefaultVal(curType))); + init.AddStatement(new BoogieAssumeCmd(qExpr)); + return init; + } private void GenerateInitializationForArrayStateVar(VariableDeclaration varDecl, ArrayTypeName array) { + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(varDecl)) + { + string name = TransUtils.GetCanonicalStateVariableName(varDecl, context); + BoogieMapSelect contractInstance = new BoogieMapSelect(new BoogieIdentifierExpr(name), new BoogieIdentifierExpr("this")); + currentStmtList.AppendStmtList(GetMultiDimInitialization(varDecl, contractInstance, context.TranslateFlags.QuantFreeAllocs)); + + TypeName mappedType = MapArrayHelper.GetMappedType(varDecl); + if (context.TranslateFlags.InstrumentSums && mappedType is ElementaryTypeName elem && (elem.TypeDescriptions.IsInt() || elem.TypeDescriptions.IsUint())) + { + currentStmtList.AddStatement(new BoogieAssignCmd(mapHelper.GetSumExpr(varDecl, new BoogieIdentifierExpr("this")), new BoogieLiteralExpr(BigInteger.Zero))); + } + + return; + } // Issue a warning for intXX type in case /useModularArithemtic option is used: if (context.TranslateFlags.UseModularArithmetic && array.BaseType.ToString().StartsWith("int")) { @@ -630,7 +992,8 @@ private void GenerateInitializationForArrayStateVar(VariableDeclaration varDecl, BoogieMapSelect lhsMap = CreateDistinctArrayMappingAddress(currentStmtList, varDecl); // lets also initialize the array Lengths (only for Arrays declared in this class) - var lengthMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), lhsMap); + //var lengthMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), lhsMap); + var lengthMapSelect = mapHelper.GetLength(varDecl, lhsMap); var lengthExpr = array.Length == null ? new BoogieLiteralExpr(BigInteger.Zero) : TranslateExpr(array.Length); // var lengthEqualsZero = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, lengthMapSelect, new BoogieLiteralExpr(0)); var lengthConstraint = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, lengthMapSelect, lengthExpr); @@ -658,34 +1021,29 @@ private void GenerateInitializationForStructStateVar(VariableDeclaration varDecl currentStmtList.AddStatement(new BoogieAssignCmd(lhsMap, tmpVarIdentExpr)); } - private BoogieFuncCallExpr GetCallExprForZeroInit(BoogieType key, BoogieType value) - { - var keyStr = char.ToUpper(key.ToString()[0]) + key.ToString().Substring(1); - var valStr = char.ToUpper(value.ToString()[0]) + value.ToString().Substring(1); - return new BoogieFuncCallExpr("zero" + keyStr + valStr + "Arr", new List()); - } - - private BoogieExpr getSumArray() - { - return new BoogieIdentifierExpr("sum"); - } - - private BoogieExpr getSumAccess(BoogieExpr key) - { - return new BoogieMapSelect(getSumArray(), key); - } - - public BoogieAssignCmd adjustSum(BoogieBinaryOperation.Opcode op, BoogieExpr sumInd, BoogieExpr amt) + public BoogieAssignCmd adjustSum(VariableDeclaration decl, BoogieBinaryOperation.Opcode op, BoogieExpr sumInd, BoogieExpr amt) { - /*BoogieExpr arrExpr = accessExpr.BaseExpr; - BoogieExpr arrExpr1 = TranslateExpr(baseExpression);*/ - BoogieExpr sumAccess = getSumAccess(sumInd); + BoogieExpr sumAccess = mapHelper.GetSumExpr(decl, sumInd); BoogieExpr sumSub = new BoogieBinaryOperation(op, sumAccess, amt); return new BoogieAssignCmd(sumAccess, sumSub); } private void GenerateInitializationForMappingStateVar(VariableDeclaration varDecl, Mapping mapping) { + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(varDecl)) + { + string name = TransUtils.GetCanonicalStateVariableName(varDecl, context); + BoogieMapSelect contractInstance = new BoogieMapSelect(new BoogieIdentifierExpr(name), new BoogieIdentifierExpr("this")); + currentStmtList.AppendStmtList(GetMultiDimInitialization(varDecl, contractInstance, context.TranslateFlags.QuantFreeAllocs)); + + TypeName mappedType = MapArrayHelper.GetMappedType(varDecl); + if (context.TranslateFlags.InstrumentSums && mappedType is ElementaryTypeName elem && (elem.TypeDescriptions.IsInt() || elem.TypeDescriptions.IsUint())) + { + currentStmtList.AddStatement(new BoogieAssignCmd(mapHelper.GetSumExpr(varDecl, new BoogieIdentifierExpr("this")), new BoogieLiteralExpr(BigInteger.Zero))); + } + return; + } + BoogieMapSelect lhsMap = CreateDistinctArrayMappingAddress(currentStmtList, varDecl); //nested arrays (only 1 level for now) @@ -731,9 +1089,9 @@ private void GenerateInitializationForMappingStateVar(VariableDeclaration varDec { if (mapping.ValueType.ToString().StartsWith("bytes")) currentStmtList.AddStatement(new BoogieAssignCmd(lhs, - GetCallExprForZeroInit(mapKeyType, BoogieType.Int))); + MapArrayHelper.GetCallExprForZeroInit(mapKeyType, BoogieType.Int))); else - currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Ref))); + currentStmtList.AddStatement(new BoogieAssignCmd(lhs, MapArrayHelper.GetCallExprForZeroInit(mapKeyType, BoogieType.Ref))); } } else if (mapping.ValueType.ToString().Equals("bool")) @@ -754,7 +1112,7 @@ private void GenerateInitializationForMappingStateVar(VariableDeclaration varDec } else { - currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Bool))); + currentStmtList.AddStatement(new BoogieAssignCmd(lhs, MapArrayHelper.GetCallExprForZeroInit(mapKeyType, BoogieType.Bool))); } } // TODO: Cleanup, StartsWith("uint") can include uint[12] as well. @@ -785,12 +1143,12 @@ private void GenerateInitializationForMappingStateVar(VariableDeclaration varDec } else { - currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Int))); + currentStmtList.AddStatement(new BoogieAssignCmd(lhs, MapArrayHelper.GetCallExprForZeroInit(mapKeyType, BoogieType.Int))); } if (context.TranslateFlags.InstrumentSums) { - currentStmtList.AddStatement(new BoogieAssignCmd(getSumAccess(lhsMap), new BoogieLiteralExpr(BigInteger.Zero))); + currentStmtList.AddStatement(new BoogieAssignCmd(mapHelper.GetSumExpr(varDecl, lhsMap), new BoogieLiteralExpr(BigInteger.Zero))); } } else @@ -866,7 +1224,7 @@ private void InitializeNestedArrayMappingStateVar(VariableDeclaration varDecl, M currentStmtList.AddStatement(new BoogieCommentCmd($"Initialize length of 1-level nested array in {varDecl.Name}")); // Issue with inferring Array[] expressions in GetBoogieTypesFromMapping (TODO: use GetBoogieTypesFromMapping after fix) var mapKeyType = MapArrayHelper.InferExprTypeFromTypeString(mapping.KeyType.TypeDescriptions.ToString()); - string mapName = MapArrayHelper.GetMemoryMapName(mapKeyType, BoogieType.Ref); + string mapName = mapHelper.GetMemoryMapName(varDecl, mapKeyType, BoogieType.Ref); string varName = TransUtils.GetCanonicalStateVariableName(varDecl, context); var varExpr = new BoogieIdentifierExpr(varName); //lhs is Mem_t_ref[x[this]] @@ -880,10 +1238,14 @@ private void InitializeNestedArrayMappingStateVar(VariableDeclaration varDecl, M if (!context.TranslateFlags.LazyNestedAlloc) { //Length[Mem_t_ref[x[this]][i]] == 0 - var bodyExpr = new BoogieBinaryOperation( + /*var bodyExpr = new BoogieBinaryOperation( BoogieBinaryOperation.Opcode.EQ, new BoogieMapSelect(new BoogieIdentifierExpr("Length"), lhs1), - new BoogieLiteralExpr(0)); + new BoogieLiteralExpr(0));*/ + var bodyExpr = new BoogieBinaryOperation( + BoogieBinaryOperation.Opcode.EQ, + mapHelper.GetLength(varDecl, lhs1), + new BoogieLiteralExpr(0)); var qExpr = new BoogieQuantifiedExpr(true, new List() {qVar1}, new List() {mapKeyType}, bodyExpr); currentStmtList.AddStatement(new BoogieAssumeCmd(qExpr)); @@ -918,9 +1280,122 @@ private void InitializeNestedArrayMappingStateVar(VariableDeclaration varDecl, M } else { - if (context.TranslateFlags.QuantFreeAllocs) + BoogieExpr index = new BoogieMapSelect(varExpr, new BoogieIdentifierExpr("this")); + TypeName curType = varDecl.TypeName; + + if (context.TranslateFlags.LazyAllocNoMod) + { + BoogieType keyType = null; + BoogieType valType = null; + if (curType is Mapping map) + { + keyType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType); + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.ValueType); + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + keyType = BoogieType.Int; + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(arr.BaseType); + curType = arr.BaseType; + } + + VeriSolAssert(curType is Mapping || curType is ArrayTypeName, "Expected a nested structure"); + /*if (!(curType is Mapping || curType is ArrayTypeName)) + { + string memName = mapHelper.GetMemoryMapName(varDecl, keyType, valType); + BoogieMapSelect lhs = new BoogieMapSelect(new BoogieIdentifierExpr(memName), index); + if (context.TranslateFlags.QuantFreeAllocs) + { + currentStmtList.AddStatement( + (new BoogieAssignCmd(lhs, GetCallExprForZeroInit(keyType, valType)))); + } + else + { + + } + + }*/ + + int lvl = 0; + while (curType is Mapping || curType is ArrayTypeName) + { + string allocName = mapHelper.GetNestedAllocName(varDecl, lvl); + BoogieMapSelect lhs = new BoogieMapSelect(new BoogieIdentifierExpr(allocName), index); + if (context.TranslateFlags.QuantFreeAllocs) + { + BoogieFuncCallExpr zeroCall = + MapArrayHelper.GetCallExprForZeroInit(keyType, BoogieType.Bool); + if (!context.initFns.Contains(zeroCall.Function)) + { + context.initFns.Add(zeroCall.Function); + context.Program.AddDeclaration(MapArrayHelper.GenerateMultiDimZeroFunction(keyType, BoogieType.Bool)); + } + currentStmtList.AddStatement((new BoogieAssignCmd(lhs, zeroCall))); + } + else + { + var negAllocExpr = new BoogieUnaryOperation(BoogieUnaryOperation.Opcode.NOT, new BoogieMapSelect(lhs, qVar1)); + var negAllocQExpr = new BoogieQuantifiedExpr(true, new List() {qVar1}, + new List() {mapKeyType}, negAllocExpr); + //assume forall i !Alloc[M_t_ref[x[this]][i]] + currentStmtList.AddStatement(new BoogieAssumeCmd(negAllocQExpr)); + } + + if (curType is Mapping m) + { + keyType = TransUtils.GetBoogieTypeFromSolidityTypeName(m.KeyType); + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(m.ValueType); + curType = m.ValueType; + } + else if (curType is ArrayTypeName arr) + { + keyType = BoogieType.Int; + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(arr.BaseType); + curType = arr.BaseType; + } + + lvl++; + } + } + else if (context.TranslateFlags.QuantFreeAllocs) { - currentStmtList.AddStatement(new BoogieAssignCmd(lhs0, GetCallExprForZeroInit(mapKeyType, BoogieType.Ref))); + //currentStmtList.AddStatement(new BoogieAssignCmd(lhs0, GetCallExprForZeroInit(mapKeyType, BoogieType.Ref))); + + while (curType is Mapping || curType is ArrayTypeName) + { + BoogieType keyType = null; + BoogieType valType = null; + if (curType is Mapping map) + { + keyType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.KeyType); + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(map.ValueType); + curType = map.ValueType; + } + else if (curType is ArrayTypeName arr) + { + keyType = BoogieType.Int; + valType = TransUtils.GetBoogieTypeFromSolidityTypeName(arr.BaseType); + curType = arr.BaseType; + } + + string memName = mapHelper.GetMemoryMapName(varDecl, keyType, valType); + BoogieMapSelect lhs = new BoogieMapSelect(new BoogieIdentifierExpr(memName), index); + currentStmtList.AddStatement((new BoogieAssignCmd(lhs, + MapArrayHelper.GetCallExprForZeroInit(keyType, valType)))); + if (valType.Equals(BoogieType.Int)) + { + index = new BoogieLiteralExpr(BigInteger.Zero); + } + else if (valType.Equals(BoogieType.Ref)) + { + index = new BoogieIdentifierExpr("null"); + } + else + { + index = new BoogieLiteralExpr(false); + } + } } else { @@ -965,7 +1440,7 @@ private void GetBoogieTypesFromMapping(VariableDeclaration varDecl, Mapping mapp mapping.ValueType.ToString(); // needed as a mapping(int => contract A) only has "A" as the valueType.ToSTring() var mapValueType = MapArrayHelper.InferExprTypeFromTypeString(mapValueTypeString); - string mapName = MapArrayHelper.GetMemoryMapName(mapKeyType, mapValueType); + string mapName = mapHelper.GetMemoryMapName(varDecl, mapKeyType, mapValueType); string varName = TransUtils.GetCanonicalStateVariableName(varDecl, context); var varExpr = new BoogieIdentifierExpr(varName); @@ -977,8 +1452,13 @@ private void GetBoogieTypesFromMapping(VariableDeclaration varDecl, Mapping mapp // TODO: refactor this code with the code to generate constructor code when definition is present private void GenerateDefaultConstructor(ContractDefinition contract) { + if (context.TranslateFlags.PerformFunctionSlice && context.TranslateFlags.PrePostHarness) + { + return; + } + // generate the internal one without base constructors - string procName = contract.Name + "_" + contract.Name + "_NoBaseCtor"; + string procName = TransUtils.GetCanonicalConstructorName(contract) + "_NoBaseCtor"; currentBoogieProc = procName; if (!boogieToLocalVarsMap.ContainsKey(currentBoogieProc)) { @@ -994,7 +1474,7 @@ private void GenerateDefaultConstructor(ContractDefinition contract) }; BoogieProcedure procedure = new BoogieProcedure(procName, inParams, outParams, attributes); context.Program.AddDeclaration(procedure); - + BoogieStmtList procBody = GenerateInitializationStmts(contract); List localVars = boogieToLocalVarsMap[currentBoogieProc]; BoogieImplementation implementation = new BoogieImplementation(procName, inParams, outParams, localVars, procBody); @@ -1348,6 +1828,11 @@ public override bool Visit(VariableDeclarationStatement node) preTranslationAction(node); foreach (VariableDeclaration varDecl in node.Declarations) { + if (varDecl == null) + { + continue; + } + string name = TransUtils.GetCanonicalLocalVariableName(varDecl, context); BoogieType type = TransUtils.GetBoogieTypeFromSolidityTypeName(varDecl.TypeName); // Issue a warning for intXX variables in case /useModularArithemtic option is used: @@ -1362,25 +1847,67 @@ public override bool Visit(VariableDeclarationStatement node) // handle the initial value of variable declaration if (node.InitialValue != null) { - VeriSolAssert(node.Declarations.Count == 1, "Invalid multiple variable declarations"); - // de-sugar to variable declaration and an assignment - VariableDeclaration varDecl = node.Declarations[0]; + List components = new List(); + foreach (VariableDeclaration varDecl in node.Declarations) + { + if (varDecl == null) + { + components.Add(null); + } + else + { + Identifier ident = new Identifier(); + ident.Name = varDecl.Name; + ident.ReferencedDeclaration = varDecl.Id; + ident.TypeDescriptions = varDecl.TypeDescriptions; + components.Add(ident); + } + } - Identifier identifier = new Identifier(); - identifier.Name = varDecl.Name; - identifier.ReferencedDeclaration = varDecl.Id; - identifier.TypeDescriptions = varDecl.TypeDescriptions; + Expression lhs = null; + if (components.Count == 1) + { + lhs = components[0]; + } + else + { + TupleExpression tupleExpr = new TupleExpression(); + tupleExpr.Id = node.Id; + tupleExpr.IsLValue = true; + tupleExpr.LValueRequested = true; + tupleExpr.Components = components; + lhs = tupleExpr; + } + Assignment assignment = new Assignment(); - assignment.LeftHandSide = identifier; + assignment.LeftHandSide = lhs; assignment.Operator = "="; assignment.RightHandSide = node.InitialValue; - + // call the visitor for assignments assignment.Accept(this); - } - else + + + /* + VeriSolAssert(node.Declarations.Count == 1, "Invalid multiple variable declarations"); + VariableDeclaration varDecl = node.Declarations[0]; + + Identifier identifier = new Identifier(); + identifier.Name = varDecl.Name; + identifier.ReferencedDeclaration = varDecl.Id; + identifier.TypeDescriptions = varDecl.TypeDescriptions; + + Assignment assignment = new Assignment(); + assignment.LeftHandSide = identifier; + assignment.Operator = "="; + assignment.RightHandSide = node.InitialValue; + + // call the visitor for assignments + assignment.Accept(this);*/ + } + else { // havoc the declared variables List varsToHavoc = new List(); @@ -1423,7 +1950,7 @@ public override bool Visit(VariableDeclarationStatement node) private BoogieExpr AddModuloOp(Expression srcExpr, BoogieExpr expr, TypeDescription type) { - if (context.TranslateFlags.UseModularArithmetic) + if (context.TranslateFlags.UseModularArithmetic && !context.TranslateFlags.UseNumericOperators) { if (type != null) { @@ -1436,6 +1963,15 @@ private BoogieExpr AddModuloOp(Expression srcExpr, BoogieExpr expr, TypeDescript } } } + else if (context.TranslateFlags.UseModularArithmetic && context.TranslateFlags.UseNumericOperators) + { + if (type.IsUintWSize(srcExpr, out uint uintSize)) + { + BigInteger maxUIntValue = (BigInteger)Math.Pow(2, uintSize); + return new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MOD, expr, new BoogieLiteralExpr(maxUIntValue)); + } + } + return expr; } @@ -1445,14 +1981,57 @@ public void updateAssignedSums(BoogieBinaryOperation.Opcode op, List for (int i = 0; i < exprs.Count; i++) { Expression expr = exprs[i]; + if (expr == null) + { + continue; + } + var isInt = expr.TypeDescriptions.IsInt() || expr.TypeDescriptions.IsUint(); if (isInt && expr is IndexAccess access && boogieExprs[i] is BoogieMapSelect sel && sel.BaseExpr is BoogieMapSelect arrIdent) { - currentStmtList.AddStatement(adjustSum(op, arrIdent.Arguments[0], boogieExprs[i])); + VariableDeclaration decl = mapHelper.getDecl(access); + currentStmtList.AddStatement(adjustSum(decl, op, arrIdent.Arguments[0], boogieExprs[i])); } } } + public BoogieStmtList performAssignment(Assignment node, BoogieExpr lhs, BoogieExpr rhs) + { + BoogieStmtList stmtList = new BoogieStmtList(); + + switch (node.Operator) + { + case "=": + stmtList.AddStatement(new BoogieAssignCmd(lhs, rhs)); + break; + case "+=": + BoogieExpr addExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, lhs, rhs); + addExpr = AddModuloOp(node.LeftHandSide, addExpr, node.LeftHandSide.TypeDescriptions); + stmtList.AddStatement(new BoogieAssignCmd(lhs, addExpr)); + break; + case "-=": + BoogieExpr subExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, lhs, rhs); + subExpr = AddModuloOp(node.LeftHandSide, subExpr, node.LeftHandSide.TypeDescriptions); + stmtList.AddStatement(new BoogieAssignCmd(lhs, subExpr)); + break; + case "*=": + BoogieExpr mulExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MUL, lhs, rhs); + mulExpr = AddModuloOp(node.LeftHandSide, mulExpr, node.LeftHandSide.TypeDescriptions); + stmtList.AddStatement(new BoogieAssignCmd(lhs, mulExpr)); + break; + case "/=": + BoogieExpr divExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.DIV, lhs, rhs); + divExpr = AddModuloOp(node.LeftHandSide, divExpr, node.LeftHandSide.TypeDescriptions); + stmtList.AddStatement(new BoogieAssignCmd(lhs, divExpr)); + break; + default: + VeriSolAssert(false, $"Unknown assignment operator: {node.Operator}"); + break; + } + + return stmtList; + } + public override bool Visit(Assignment node) { preTranslationAction(node); @@ -1465,9 +2044,28 @@ public override bool Visit(Assignment node) if (node.LeftHandSide is TupleExpression tuple) { // we only handle the case (e1, e2, .., _, _) = funcCall(...) - lhs.AddRange(tuple.Components.ConvertAll(x => TranslateExpr(x))); + lhs.AddRange(tuple.Components.ConvertAll(x => x == null ? null : TranslateExpr(x))); isTupleAssignment = true; - lhsTypes.AddRange(tuple.Components.ConvertAll(x => MapArrayHelper.InferExprTypeFromTypeString(x.TypeDescriptions.TypeString))); + + lhsTypes = new List(); + for (int i = 0; i < tuple.Components.Count; i++) + { + Expression expr = tuple.Components[i]; + if (expr == null) + { + BoogieType rhsType = + MapArrayHelper.InferExprTypeFromTupleTypeString( + node.RightHandSide.TypeDescriptions.TypeString, i); + VeriSolAssert(rhsType != null, "Could not determine type within tuple from rhs string"); + lhsTypes.Add(rhsType); + } + else + { + lhsTypes.Add(MapArrayHelper.InferExprTypeFromTypeString(expr.TypeDescriptions.TypeString)); + } + } + + //lhsTypes.AddRange(tuple.Components.ConvertAll(x => MapArrayHelper.InferExprTypeFromTypeString(x.TypeDescriptions.TypeString))); lhsExprs = tuple.Components; } else @@ -1501,29 +2099,35 @@ public override bool Visit(Assignment node) // a Boolean to decide is we needed to use tmpVar bool usedTmpVar = true; - if (IsContractConstructor(funcCall)) + if (FunctionCallHelper.IsContractConstructor(funcCall)) { VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Constructors"); TranslateNewStatement(funcCall, tmpVars[0]); } - else if (IsStructConstructor(funcCall)) + else if (FunctionCallHelper.IsStructConstructor(funcCall)) { VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Constructors"); TranslateStructConstructor(funcCall, tmpVars[0]); } - else if (IsKeccakFunc(funcCall)) + else if (FunctionCallHelper.IsKeccakFunc(funcCall)) { VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Keccak256"); TranslateKeccakFuncCall(funcCall, lhs[0]); //this is not a procedure call in Boogie usedTmpVar = false; } - else if (IsAbiEncodePackedFunc(funcCall)) + else if (FunctionCallHelper.IsGasleft(funcCall)) + { + VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for gasleft"); + TranslateGasleftCall(funcCall, lhs[0]); + usedTmpVar = false; + } + else if (FunctionCallHelper.IsAbiEncodePackedFunc(funcCall)) { TranslateAbiEncodedFuncCall(funcCall, tmpVars[0]); //this is not a procedure call in Boogie VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for abi.encodePacked"); usedTmpVar = false; } - else if (IsTypeCast(funcCall)) + else if (FunctionCallHelper.IsTypeCast(funcCall)) { // assume the type cast is used as: obj = C(var); VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for type cast"); @@ -1543,12 +2147,17 @@ public override bool Visit(Assignment node) if (!isTupleAssignment) { if (usedTmpVar || !(lhs[0] is BoogieIdentifierExpr)) //bad bug: was && before!! - currentStmtList.AddStatement(new BoogieAssignCmd(lhs[0], tmpVars[0])); + { + currentStmtList.AppendStmtList(performAssignment(node, lhs[0], tmpVars[0])); + } } else { for (int i = 0; i < lhs.Count; ++i) { - currentStmtList.AddStatement(new BoogieAssignCmd(lhs[i], tmpVars[i])); + if (lhs[i] != null) + { + currentStmtList.AddStatement(new BoogieAssignCmd(lhs[i], tmpVars[i])); + } } } if (context.TranslateFlags.InstrumentSums) @@ -1568,43 +2177,14 @@ public override bool Visit(Assignment node) VeriSolAssert(false, "Not implemented...currently only support assignment of tuples as returns of a function call"); BoogieExpr rhs = TranslateExpr(node.RightHandSide); - BoogieStmtList stmtList = new BoogieStmtList(); - BoogieExpr assignedExpr = new BoogieExpr(); - switch (node.Operator) - { - case "=": - stmtList.AddStatement(new BoogieAssignCmd(lhs[0], rhs)); - break; - case "+=": - assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, lhs[0], rhs); - assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions); - stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr)); - break; - case "-=": - assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, lhs[0], rhs); - assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions); - stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr)); - break; - case "*=": - assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MUL, lhs[0], rhs); - assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions); - stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr)); - break; - case "/=": - assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.DIV, lhs[0], rhs); - assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions); - stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr)); - break; - default: - VeriSolAssert(false, $"Unknown assignment operator: {node.Operator}"); - break; - } - + if (context.TranslateFlags.InstrumentSums) { updateAssignedSums(BoogieBinaryOperation.Opcode.SUB, lhsExprs, lhs); } - currentStmtList.AppendStmtList(stmtList); + + currentStmtList.AppendStmtList(performAssignment(node, lhs[0], rhs)); + if (context.TranslateFlags.InstrumentSums) { updateAssignedSums(BoogieBinaryOperation.Opcode.ADD, lhsExprs, lhs); @@ -1635,7 +2215,7 @@ private void TranslateInBuiltFunction(FunctionCall funcCall, BoogieExpr lhs) private void TranslateFunctionCalls(FunctionCall funcCall, List outParams) { - if (IsExternalFunctionCall(funcCall)) + if (FunctionCallHelper.IsExternalFunctionCall(context, funcCall)) { TranslateExternalFunctionCall(funcCall, outParams); } @@ -1648,8 +2228,12 @@ private void TranslateFunctionCalls(FunctionCall funcCall, List ExtractSpecifications(string specStringCall, BoogieStmt private BoogieExpr TranslateModifiesStmt(BoogieExpr boogieExpr1, BoogieExpr boogieExpr2) { //has to be M_ref_int[mapp[this]] instead of mapp[this] - var mapName = MapArrayHelper.GetMemoryMapName(BoogieType.Ref, BoogieType.Int); + //TODO: this is not the proper way of finding the correct map. Come back and fix. + var mapName = MapArrayHelper.GetCanonicalMemName(BoogieType.Ref, BoogieType.Int); var mappingExpr = new BoogieMapSelect(new BoogieIdentifierExpr(mapName), boogieExpr1); //boogieExpr2 is a tuple, we need to flatten it into an array @@ -1989,7 +2574,8 @@ public override bool Visit(ExpressionStatement node) if (context.TranslateFlags.InstrumentSums && isInt && unaryOperation.SubExpression is IndexAccess access && lhs is BoogieMapSelect sel && sel.BaseExpr is BoogieMapSelect arrIdent) { - currentStmtList.AddStatement(adjustSum(oper, arrIdent.Arguments[0], new BoogieLiteralExpr(BigInteger.One))); + VariableDeclaration decl = mapHelper.getDecl(access); + currentStmtList.AddStatement(adjustSum(decl, oper, arrIdent.Arguments[0], new BoogieLiteralExpr(BigInteger.One))); } //print the value @@ -2012,7 +2598,8 @@ public override bool Visit(ExpressionStatement node) if (typeDescription.IsDynamicArray()) { BoogieExpr element = TranslateExpr(unaryOperation.SubExpression); - BoogieExpr lengthMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), element); + //BoogieExpr lengthMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), element); + BoogieExpr lengthMapSelect = mapHelper.GetLength(unaryOperation.SubExpression, element); BoogieExpr rhs = new BoogieLiteralExpr(BigInteger.Zero); var assignCmd = new BoogieAssignCmd(lengthMapSelect, rhs); currentStmtList.AddStatement(assignCmd); @@ -2020,7 +2607,8 @@ public override bool Visit(ExpressionStatement node) var isInt = typeDescription.IsInt() || typeDescription.IsUint(); if (context.TranslateFlags.InstrumentSums && isInt) { - BoogieExpr sumExpr = getSumAccess(element); + VariableDeclaration decl = mapHelper.getDecl(unaryOperation.SubExpression); + BoogieExpr sumExpr = mapHelper.GetSumExpr(decl, element); var sumAssign = new BoogieAssignCmd(sumExpr, new BoogieLiteralExpr(BigInteger.Zero)); currentStmtList.AddStatement(sumAssign); } @@ -2037,7 +2625,8 @@ public override bool Visit(ExpressionStatement node) if (context.TranslateFlags.InstrumentSums && isInt && unaryOperation.SubExpression is IndexAccess access && lhs is BoogieMapSelect sel && sel.BaseExpr is BoogieMapSelect arrIdent) { - currentStmtList.AddStatement(adjustSum(BoogieBinaryOperation.Opcode.SUB, arrIdent.Arguments[0], lhs)); + VariableDeclaration decl = mapHelper.getDecl(access); + currentStmtList.AddStatement(adjustSum(decl, BoogieBinaryOperation.Opcode.SUB, arrIdent.Arguments[0], lhs)); } BoogieExpr rhs = null; @@ -2075,7 +2664,7 @@ public override bool Visit(ExpressionStatement node) private BoogieExpr TranslateExpr(Expression expr) { currentExpr = null; - if (expr is FunctionCall && IsTypeCast((FunctionCall) expr)) + if (expr is FunctionCall && FunctionCallHelper.IsTypeCast((FunctionCall) expr)) { expr.Accept(this); VeriSolAssert(currentExpr != null); @@ -2142,7 +2731,7 @@ private BoogieExpr TranslateNumberToExpr(Literal node) } else { - num = BigInteger.Parse(node.Value); + num = BigInteger.Parse(node.Value, NumberStyles.AllowExponent); } //if (node.TypeDescriptions.IsAddress()) @@ -2168,6 +2757,10 @@ public override bool Visit(Identifier node) { currentExpr = new BoogieIdentifierExpr("this"); } + else if (node.Name.Equals("super")) + { + currentExpr = new BoogieIdentifierExpr("this"); + } else if (node.Name.Equals("now")) { currentExpr = new BoogieIdentifierExpr("now"); @@ -2257,7 +2850,7 @@ public override bool Visit(MemberAccess node) } else if (identifier.Name.Equals("block")) { - if (node.MemberName.Equals("timestamp")) + if (node.MemberName.Equals("timestamp") || node.MemberName.Equals("number")) currentExpr = new BoogieIdentifierExpr("now"); else //we will havoc the value @@ -2324,7 +2917,8 @@ private BoogieExpr TranslateArrayLength(MemberAccess node) VeriSolAssert(node.MemberName.Equals("length")); BoogieExpr indexExpr = TranslateExpr(node.Expression); - var mapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), indexExpr); + //var mapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), indexExpr); + var mapSelect = mapHelper.GetLength(node.Expression, indexExpr); return mapSelect; } @@ -2388,24 +2982,26 @@ public override bool Visit(FunctionCall node) emitRevertLogic(currentStmtList); } } - else if (IsImplicitFunc(node)) + else if (FunctionCallHelper.IsImplicitFunc(node)) { BoogieIdentifierExpr tmpVarExpr = MkNewLocalVariableForFunctionReturn(node); bool isElementaryCast = false; - if (IsContractConstructor(node)) { + if (FunctionCallHelper.IsContractConstructor(node)) { TranslateNewStatement(node, tmpVarExpr); - } else if (IsTypeCast(node)) { + } else if (FunctionCallHelper.IsTypeCast(node)) { TranslateTypeCast(node, tmpVarExpr, out isElementaryCast); - } else if (IsAbiEncodePackedFunc(node)) { + } else if (FunctionCallHelper.IsAbiEncodePackedFunc(node)) { TranslateAbiEncodedFuncCall(node, tmpVarExpr); - } else if (IsKeccakFunc(node)) { + } else if (FunctionCallHelper.IsKeccakFunc(node)) { TranslateKeccakFuncCall(node, tmpVarExpr); - } else if (IsStructConstructor(node)) { + } else if (FunctionCallHelper.IsGasleft(node)) { + TranslateGasleftCall(node, tmpVarExpr); + } else if (FunctionCallHelper.IsStructConstructor(node)) { TranslateStructConstructor(node, tmpVarExpr); } else { - VeriSolAssert(false, $"Unexpected implicit function {node.ToString()}"); + VeriSolAssert(false, $"Unsupported implicit function {node.ToString()}"); } if (!isElementaryCast) @@ -2436,7 +3032,7 @@ public override bool Visit(FunctionCall node) { VeriSolAssert(false, "low-level delegatecall statements not supported..."); } - else if (IsBuiltInTransferFunc(functionName, node)) + else if (FunctionCallHelper.IsBuiltInTransferFunc(functionName, node)) { TranslateTransferCallStmt(node); } @@ -2451,7 +3047,7 @@ public override bool Visit(FunctionCall node) { TranslateDynamicArrayPush(node); } - else if (IsExternalFunctionCall(node)) + else if (FunctionCallHelper.IsExternalFunctionCall(context, node)) { // external function calls @@ -2491,17 +3087,6 @@ public override bool Visit(FunctionCall node) return false; } - private bool IsBuiltInTransferFunc(string functionName, FunctionCall node) - { - if (!functionName.Equals("transfer")) return false; - if (node.Expression is MemberAccess member) - { - if (member.Expression.TypeDescriptions.IsAddress()) - return true; - } - return false; - } - private BoogieExpr TranslateVeriSolCodeContractFuncCall(FunctionCall node) { var verisolFunc = GetVeriSolCodeContractFunction(node); @@ -2510,9 +3095,16 @@ private BoogieExpr TranslateVeriSolCodeContractFuncCall(FunctionCall node) // HACK for Sum if (verisolFunc.Equals("_SumMapping_VeriSol")) { - //has to be M_ref_int[mapp[this]] instead of mapp[this] - var mapName = MapArrayHelper.GetMemoryMapName(BoogieType.Ref, BoogieType.Int); - boogieExprs[0] = new BoogieMapSelect(new BoogieIdentifierExpr(mapName), boogieExprs[0]); + + VariableDeclaration decl = mapHelper.getDecl(node.Arguments[0]); + VeriSolAssert(decl != null, "Could not find declaration of " + node.Arguments[0]); + if (!(context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(decl))) + { + //has to be M_ref_int[mapp[this]] instead of mapp[this] + var mapName = mapHelper.GetMemoryMapName(decl, BoogieType.Ref, BoogieType.Int); + boogieExprs[0] = new BoogieMapSelect(new BoogieIdentifierExpr(mapName), boogieExprs[0]); + } + } return new BoogieFuncCallExpr(verisolFunc, boogieExprs); } @@ -2585,57 +3177,21 @@ private BoogieIdentifierExpr MkNewLocalVariableWithType(BoogieType boogieTypeCal return tmpVarExpr; } - #region implicit functions + #region implicit functions + /// /// Implicit function calls /// /// /// - private bool IsImplicitFunc(FunctionCall node) - { - return - IsKeccakFunc(node) || - IsAbiEncodePackedFunc(node) || - IsTypeCast(node) || - IsStructConstructor(node) || - IsContractConstructor(node); - } - - private bool IsContractConstructor(FunctionCall node) - { - return node.Expression is NewExpression; - } - - private bool IsStructConstructor(FunctionCall node) - { - return node.Kind.Equals("structConstructorCall"); - } - - private bool IsKeccakFunc(FunctionCall node) - { - if (node.Expression is Identifier ident) - { - return ident.Name.Equals("keccak256"); - } - return false; - } - private bool IsAbiEncodePackedFunc(FunctionCall node) + private void TranslateGasleftCall(FunctionCall node, BoogieExpr lhs) { - if (node.Expression is MemberAccess member) - { - if (member.Expression is Identifier ident) - { - if (ident.Name.Equals("abi")) - { - if (member.MemberName.Equals("encodePacked")) - return true; - } - } - } - return false; + currentStmtList.AddStatement(new BoogieCommentCmd("gasleft Translation")); + BoogieAssignCmd gasAssign = new BoogieAssignCmd(lhs, new BoogieIdentifierExpr("gas")); + currentStmtList.AddStatement(gasAssign); } - + private void TranslateKeccakFuncCall(FunctionCall funcCall, BoogieExpr lhs) { var expression = funcCall.Arguments[0]; @@ -2674,6 +3230,8 @@ private void TranslateCallStatement(FunctionCall node, List outParams = null) { VeriSolAssert(node.Expression is MemberAccess, $"Expecting a member access expression here {node.Expression.ToString()}"); @@ -3054,13 +3557,13 @@ private void TranslateExternalFunctionCall(FunctionCall node, List= msg.value + currentStmtList.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgValueExpr))); + //balance[msg.sender] = balance[msg.sender] - msg.value + currentStmtList.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgValueExpr))); + //balance[this] = balance[this] + msg.value + currentStmtList.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgValueExpr))); + currentStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); } else { @@ -3079,13 +3593,24 @@ private void TranslateExternalFunctionCall(FunctionCall node, List arguments = new List() + List arguments = null; + + if (isSuper) { - receiver, - new BoogieIdentifierExpr("this"), - msgValueExpr, - }; + arguments = TransUtils.GetDefaultArguments(); + } + else + { + arguments = new List() { + receiver, + new BoogieIdentifierExpr("this"), + msgValueExpr, + }; + } + foreach (Expression arg in node.Arguments) { @@ -3093,11 +3618,13 @@ private void TranslateExternalFunctionCall(FunctionCall node, List usingRange = new HashSet(); - - // may need to look into base contracts as well (UsingInBase.sol) - foreach (int id in currentContract.LinearizedBaseContracts) - { - ContractDefinition baseContract = context.GetASTNodeById(id) as ContractDefinition; - Debug.Assert(baseContract != null); - if (!context.UsingMap.ContainsKey(baseContract)) continue; - foreach (var kv in context.UsingMap[baseContract]) - { - if (kv.Value.ToString().Equals(typedescr)) - { - usingRange.Add(kv.Key); - } - } - } - VeriSolAssert(usingRange.Count > 0, $"Expecting at least one using A for B for {typedescr}"); - - string signature = TransUtils.InferFunctionSignature(context, node); - VeriSolAssert(context.HasFuncSignature(signature), $"Cannot find a function with signature: {signature}"); - var dynamicTypeToFuncMap = context.GetAllFuncDefinitions(signature); - VeriSolAssert(dynamicTypeToFuncMap.Count > 0); - - //intersect the types with a matching function with usingRange - var candidateLibraries = new List>(); - foreach(var tf in dynamicTypeToFuncMap) - { - if (usingRange.Any(x => x.Name.Equals(tf.Key.Name.ToString()))) - { - candidateLibraries.Add(Tuple.Create(tf.Key, tf.Value)); - } - } - - VeriSolAssert(candidateLibraries.Count == 1, $"Expecting a library call to match exactly one function, found {candidateLibraries.Count}"); - var funcDefn = candidateLibraries[0]; + + var funcDefn = context.GetASTNodeById(memberAccess.ReferencedDeclaration.Value) as FunctionDefinition; //x.f(y1, y2) in Solidity becomes f_lib(this, this, 0, x, y1, y2) var arguments = new List() { @@ -3172,18 +3645,38 @@ private void TranslateUsingLibraryCall(FunctionCall node, List TranslateExpr(x))); - var callee = TransUtils.GetCanonicalFunctionName(funcDefn.Item2, context); + var callee = TransUtils.GetCanonicalFunctionName(funcDefn, context); var callCmd = new BoogieCallCmd(callee, arguments, outParams); currentStmtList.AddStatement(callCmd); // throw new NotImplementedException("not done implementing using A for B yet"); } - private bool IsUsingBasedLibraryCall(MemberAccess memberAccess) + private void TranslateStaticDispatchCall(FunctionCall node, List arguments, + List outParams) { - // since we only permit "using A for B" for non-contract types - // this is sufficient, but not necessary in general since non - // contracts (including libraries) do not have support methods - return !memberAccess.Expression.TypeDescriptions.IsContract(); + ContractDefinition contract = FunctionCallHelper.GetStaticDispatchingContract(context, node); + string signature = TransUtils.InferFunctionSignature(context, node); + VeriSolAssert(context.HasFuncSignature(signature), $"Cannot find a function with signature: {signature}"); + var dynamicTypeToFuncMap = context.GetAllFuncDefinitions(signature); + VeriSolAssert(dynamicTypeToFuncMap.ContainsKey(contract)); + FunctionDefinition fnDef = dynamicTypeToFuncMap[contract]; + string callee = null; + if (contract.Name.Equals("VeriSol")) + { + callee = $"{fnDef.Name}_{contract.Name}"; + } + else + { + callee = TransUtils.GetCanonicalFunctionName(fnDef, context); + } + + BoogieCallCmd callCmd = new BoogieCallCmd(callee, arguments, outParams); + currentStmtList.AddStatement(callCmd); + + /*string functionName = TransUtils.GetFuncNameFromFuncCall(node); + string callee = functionName + "_" + contract.Name; + BoogieCallCmd callCmd = new BoogieCallCmd(callee, arguments, outParams); + currentStmtList.AddStatement(callCmd);*/ } private void TranslateInternalFunctionCall(FunctionCall node, List outParams = null) @@ -3192,7 +3685,7 @@ private void TranslateInternalFunctionCall(FunctionCall node, List outParams, List arguments, bool condition, BoogieExpr receiver) + private void TranslateDynamicDispatchCall(FunctionCall node, List outParams, List arguments, bool condition, bool isSuper, BoogieExpr receiver) { ContractDefinition contractDefn; VariableDeclaration varDecl; // Solidity internally generates foo() getter for any public state // variable foo in a contract. - if (IsGetterForPublicVariable(node, out varDecl, out contractDefn)) + + if (IsGetterForPublicVariable(node, out varDecl, out contractDefn) && !(context.TranslateFlags.GenerateGetters && node.Arguments.Count != 0)) { + VeriSolAssert(node.Arguments.Count == 0, "Cannot access mappings or arrays using public getter right now"); + VeriSolAssert(!isSuper, "Super is not supported for public getters right now"); List subtypes = new List(context.GetSubTypesOfContract(contractDefn)); Debug.Assert(subtypes.Count > 0); @@ -3259,7 +3750,7 @@ private void TranslateDynamicDispatchCall(FunctionCall node, List dynamicTypeToFuncMap; - string signature = TransUtils.InferFunctionSignature(context, node); + string signature = TransUtils.InferFunctionSignature(context, node, IsGetterForPublicVariable(node, out varDecl, out contractDefn)); VeriSolAssert(context.HasFuncSignature(signature), $"Cannot find a function with signature: {signature}"); dynamicTypeToFuncMap = context.GetAllFuncDefinitions(signature); VeriSolAssert(dynamicTypeToFuncMap.Count > 0); @@ -3274,7 +3765,37 @@ private void TranslateDynamicDispatchCall(FunctionCall node, List /// @@ -3445,7 +3933,7 @@ private void TranslateTypeCast(FunctionCall node, BoogieExpr lhs, out bool isEle } // We do not handle downcasts between unsigned integers, when /useModularArithmetic option is enabled: - if (context.TranslateFlags.UseModularArithmetic) + if (context.TranslateFlags.UseModularArithmetic && !context.TranslateFlags.UseNumericOperators) { bool argTypeIsUint = node.Arguments[0].TypeDescriptions.IsUintWSize(node.Arguments[0], out uint argSz); if (argTypeIsUint && elemType.ToString().StartsWith("uint")) @@ -3457,6 +3945,14 @@ private void TranslateTypeCast(FunctionCall node, BoogieExpr lhs, out bool isEle } } } + else if (context.TranslateFlags.UseModularArithmetic && context.TranslateFlags.UseNumericOperators) + { + if (node.TypeDescriptions.IsUintWSize(node, out uint uintSize)) + { + BigInteger maxUIntValue = (BigInteger)Math.Pow(2, uintSize); + rhsExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MOD, rhsExpr, new BoogieLiteralExpr(maxUIntValue)); + } + } // lets update currentExpr with rhsExpr. The caller may update it with the temporary currentExpr = rhsExpr; @@ -3603,19 +4099,60 @@ public override bool Visit(BinaryOperation node) binaryExpr = new BoogieLiteralExpr((BigInteger)Math.Pow((double)valueLeft, (double)valueRight)); } + else if (context.TranslateFlags.NoNonlinearArith) + { + binaryExpr = new BoogieFuncCallExpr("nonlinearPow", new List() { leftExpr, rightExpr}); + } else { Console.WriteLine($"VeriSol translation error: power operation for non-constants or with constant subexpressions is not supported; hint: use temps for subexpressions"); return false; } } + else if (context.TranslateFlags.NoNonlinearArith && node.Operator == "*") + { + if ((node.LeftExpression is Literal leftLiteral && leftLiteral.Kind.Equals("number")) || + (node.RightExpression is Literal rightLiteral && rightLiteral.Kind.Equals("number"))) + { + binaryExpr = new BoogieBinaryOperation(op, leftExpr, rightExpr); + } + else + { + //BoogieCallCmd callCmd = new BoogieCallCmd(callee, arguments, outParams); + binaryExpr = new BoogieFuncCallExpr("nonlinearMul", new List() { leftExpr, rightExpr}); + } + } + else if (context.TranslateFlags.NoNonlinearArith && node.Operator == "/") + { + if ((node.LeftExpression is Literal leftLiteral && leftLiteral.Kind.Equals("number")) || + (node.RightExpression is Literal rightLiteral && rightLiteral.Kind.Equals("number"))) + { + binaryExpr = new BoogieBinaryOperation(op, leftExpr, rightExpr); + } + else + { + binaryExpr = new BoogieFuncCallExpr("nonlinearDiv", new List() { leftExpr, rightExpr}); + } + } + else if (context.TranslateFlags.NoNonlinearArith && node.Operator == "%") + { + if ((node.LeftExpression is Literal leftLiteral && leftLiteral.Kind.Equals("number")) || + (node.RightExpression is Literal rightLiteral && rightLiteral.Kind.Equals("number"))) + { + binaryExpr = new BoogieBinaryOperation(op, leftExpr, rightExpr); + } + else + { + binaryExpr = new BoogieFuncCallExpr("nonlinearMod", new List() { leftExpr, rightExpr}); + } + } else { binaryExpr = new BoogieBinaryOperation(op, leftExpr, rightExpr); } currentExpr = binaryExpr; - if (context.TranslateFlags.UseModularArithmetic) + if (context.TranslateFlags.UseModularArithmetic && !context.TranslateFlags.UseNumericOperators) { //if (node.Operator == "+" || node.Operator == "-" || node.Operator == "*" || node.Operator == "/" || node.Operator == "**") if (node.Operator == "+" || node.Operator == "-" || node.Operator == "*" || node.Operator == "/") @@ -3640,6 +4177,15 @@ public override bool Visit(BinaryOperation node) } } } + else if (context.TranslateFlags.UseModularArithmetic && context.TranslateFlags.UseNumericOperators) + { + if (node.TypeDescriptions.IsUintWSize(node, out uint uintSize)) + { + BigInteger maxUIntValue = (BigInteger)Math.Pow(2, uintSize); + currentExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MOD, currentExpr, new BoogieLiteralExpr(maxUIntValue)); + } + } + return false; } @@ -3657,6 +4203,101 @@ public override bool Visit(Conditional node) return false; } + public int GetMaxLvl(VariableDeclaration decl) + { + int lvl = -1; + TypeName curType = decl.TypeName; + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping mapping) + { + curType = mapping.ValueType; + } + else if (curType is ArrayTypeName arr) + { + curType = arr.BaseType; + } + + lvl++; + } + + return lvl; + } + + public int GetIndexLvl(VariableDeclaration decl, IndexAccess node) + { + int maxLvl = GetMaxLvl(decl); + string typeStr = node.TypeDescriptions.TypeString; + + int lvl = 0; + while (MapArrayHelper.IsMappingTypeString(typeStr) || MapArrayHelper.IsArrayTypeString(typeStr)) + { + typeStr = MapArrayHelper.GetValueTypeString(typeStr); + lvl++; + } + + return maxLvl - lvl; + } + + /*public int GetIndexLvl(VariableDeclaration decl, IndexAccess node) + { + Expression val = decl.Value; + string typeStr = node.TypeDescriptions.TypeString; + string valTypeStr = MapArrayHelper.GetValueTypeString(typeStr); + string indTypeStr = MapArrayHelper.GetIndexTypeString(typeStr); + + int lvl = 0; + TypeName curType = decl.TypeName; + while (curType is Mapping || curType is ArrayTypeName) + { + if (curType is Mapping mapping) + { + curType = mapping.ValueType; + } + else if (curType is ArrayTypeName arr) + { + curType = arr.BaseType; + } + + if (curType is Mapping map && MapArrayHelper.IsMappingTypeString(typeStr) && valTypeStr.Equals(map.ValueType.ToString()) && indTypeStr.Equals(map.KeyType.ToString())) + { + return lvl; + } + else if (curType is ArrayTypeName arr && MapArrayHelper.IsArrayTypeString(typeStr) && valTypeStr.Equals(arr.BaseType.ToString())) + { + return lvl; + } + else if (curType.ToString().Equals(typeStr)) + { + return lvl; + } + + lvl++; + } + + VeriSolAssert(false, "Could not determine access index"); + return -1; + }*/ + + public BoogieExpr GetDefaultVal(BoogieType boogieType) + { + if (boogieType.Equals(BoogieType.Int)) + { + return new BoogieLiteralExpr(BigInteger.Zero); + } + else if (boogieType.Equals(BoogieType.Bool)) + { + return new BoogieLiteralExpr(false); + } + else if (boogieType.Equals(BoogieType.Ref)) + { + return new BoogieIdentifierExpr("null"); + } + + VeriSolAssert(false, "Unknown solidity type"); + return null; + } + public override bool Visit(IndexAccess node) { preTranslationAction(node); @@ -3685,10 +4326,92 @@ public override bool Visit(IndexAccess node) // VeriSolAssert(false, $"Unknown base in index access: {node.BaseExpression}"); //} - BoogieExpr indexAccessExpr = new BoogieMapSelect(baseExpr, indexExpr); - currentExpr = MapArrayHelper.GetMemoryMapSelectExpr(baseKeyType, baseValType, baseExpr, indexExpr); + + VariableDeclaration decl = mapHelper.getDecl(node); + + if (context.TranslateFlags.UseMultiDim && context.Analysis.Alias.getResults().Contains(decl)) + { + currentExpr = new BoogieMapSelect(baseExpr, indexExpr); + return false; + } + + currentExpr = mapHelper.GetMemoryMapSelectExpr(decl, baseKeyType, baseValType, baseExpr, indexExpr); + + if (context.TranslateFlags.LazyAllocNoMod) + { + var valTypeString = MapArrayHelper.GetValueTypeString(baseExpression.TypeDescriptions.TypeString); + var valIsMapping = MapArrayHelper.IsMappingTypeString(valTypeString); + var valIsArray = MapArrayHelper.IsArrayTypeString(valTypeString); + + if (valIsArray || valIsMapping) + { + BoogieStmtList allocAndInit = new BoogieStmtList(); + var tmpVarIdentExpr = MkNewLocalVariableWithType(baseValType); + allocAndInit.AddStatement(new BoogieCallCmd("FreshRefGenerator", + new List(), + new List() {tmpVarIdentExpr} + )); + + if (valIsArray) + { + //allocAndInit.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, new BoogieMapSelect(new BoogieIdentifierExpr("Length"), currentExpr), new BoogieLiteralExpr(0)))); + allocAndInit.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, mapHelper.GetLength(decl, currentExpr), new BoogieLiteralExpr(0)))); + } + + //allocAndInit.AddStatement(new BoogieAssignCmd(currentExpr, tmpVarIdentExpr)); + int lvl = GetIndexLvl(decl, node); + + string nestedVal = MapArrayHelper.GetValueTypeString(valTypeString); + bool isNestedStructure = MapArrayHelper.IsMappingTypeString(nestedVal) || + MapArrayHelper.IsArrayTypeString(nestedVal); + string allocName = mapHelper.GetNestedAllocName(decl, lvl); + + //var mapName = new BoogieIdentifierExpr(mapHelper.GetMemoryMapName(decl, nestedKeyType, nestedValType)); + //var derefCurrExpr = new BoogieMapSelect(mapName, currentExpr); + + var allocMap = new BoogieIdentifierExpr(allocName); + var allocExpr = new BoogieMapSelect(new BoogieMapSelect(allocMap, baseExpr), indexExpr); + allocAndInit.AddStatement(new BoogieAssignCmd(allocExpr, new BoogieLiteralExpr(true))); + + if (!isNestedStructure) + { + BoogieType nestedValType = MapArrayHelper.InferValueTypeFromTypeString(valTypeString); + BoogieType nestedKeyType = MapArrayHelper.InferKeyTypeFromTypeString(valTypeString); + + var mapName = new BoogieIdentifierExpr(mapHelper.GetMemoryMapName(decl, nestedKeyType, nestedValType)); + var derefCurrExpr = new BoogieMapSelect(mapName, currentExpr); + + //allocate struct + if (context.TranslateFlags.QuantFreeAllocs) + { + BoogieFuncCallExpr zeroInit = MapArrayHelper.GetCallExprForZeroInit(nestedKeyType, nestedValType); + allocAndInit.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, derefCurrExpr, zeroInit))); + } + else + { + var qVar = QVarGenerator.NewQVar(0, 0); + BoogieExpr defaultVal = GetDefaultVal(nestedValType); + var bodyExpr = new BoogieBinaryOperation( + BoogieBinaryOperation.Opcode.EQ, + new BoogieMapSelect(derefCurrExpr, qVar), + defaultVal); + var qExpr = new BoogieQuantifiedExpr(true, new List() {qVar}, + new List() {nestedKeyType}, bodyExpr); + allocAndInit.AddStatement(new BoogieAssumeCmd(qExpr)); + } + } - if (context.TranslateFlags.LazyNestedAlloc) + allocAndInit.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, currentExpr, tmpVarIdentExpr))); + + if (context.TranslateFlags.InstrumentSums) + { + allocAndInit.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, mapHelper.GetSumExpr(decl, currentExpr), new BoogieLiteralExpr(BigInteger.Zero)))); + } + + currentStmtList.AddStatement(new BoogieIfCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, allocExpr, new BoogieLiteralExpr(false)), allocAndInit, null)); + } + } + else if (context.TranslateFlags.LazyNestedAlloc) { var valTypeString = MapArrayHelper.GetValueTypeString(baseExpression.TypeDescriptions.TypeString); var valIsMapping = MapArrayHelper.IsMappingTypeString(valTypeString); @@ -3707,13 +4430,14 @@ public override bool Visit(IndexAccess node) if (valIsArray) { - allocAndInit.AddStatement(new BoogieAssignCmd(new BoogieMapSelect(new BoogieIdentifierExpr("Length"), currentExpr), new BoogieLiteralExpr(0))); + //allocAndInit.AddStatement(new BoogieAssignCmd(new BoogieMapSelect(new BoogieIdentifierExpr("Length"), currentExpr), new BoogieLiteralExpr(0))); + allocAndInit.AddStatement(new BoogieAssignCmd(mapHelper.GetLength(decl, currentExpr), new BoogieLiteralExpr(0))); } BoogieType nestedValType = MapArrayHelper.InferValueTypeFromTypeString(valTypeString); BoogieType nestedKeyType = MapArrayHelper.InferKeyTypeFromTypeString(valTypeString); - var mapName = new BoogieIdentifierExpr(MapArrayHelper.GetMemoryMapName(nestedKeyType, nestedValType)); + var mapName = new BoogieIdentifierExpr(mapHelper.GetMemoryMapName(decl, nestedKeyType, nestedValType)); var derefCurrExpr = new BoogieMapSelect(mapName, currentExpr); var qVar1 = QVarGenerator.NewQVar(0, 0); @@ -3722,7 +4446,7 @@ public override bool Visit(IndexAccess node) { if (context.TranslateFlags.QuantFreeAllocs) { - allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Bool))); + allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, MapArrayHelper.GetCallExprForZeroInit(nestedKeyType, BoogieType.Bool))); } else { @@ -3739,7 +4463,7 @@ public override bool Visit(IndexAccess node) { if (context.TranslateFlags.QuantFreeAllocs) { - allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Int))); + allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, MapArrayHelper.GetCallExprForZeroInit(nestedKeyType, BoogieType.Int))); } else { @@ -3754,14 +4478,14 @@ public override bool Visit(IndexAccess node) if (context.TranslateFlags.InstrumentSums) { - allocAndInit.AddStatement(new BoogieAssignCmd(getSumAccess(currentExpr), new BoogieLiteralExpr(BigInteger.Zero))); + allocAndInit.AddStatement(new BoogieAssignCmd(mapHelper.GetSumExpr(decl, currentExpr), new BoogieLiteralExpr(BigInteger.Zero))); } } else if (nestedValType == BoogieType.Ref) { if (context.TranslateFlags.QuantFreeAllocs) { - allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Ref))); + allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, MapArrayHelper.GetCallExprForZeroInit(nestedKeyType, BoogieType.Ref))); } else { @@ -3790,6 +4514,31 @@ public override bool Visit(IndexAccess node) public override bool Visit(InlineAssembly node) { preTranslationAction(node); + + if (context.TranslateFlags.AssemblyAsHavoc) + { + this.currentStmtList.AddStatement(new BoogieCommentCmd("---- modeling inline assembly ----")); + string ops = node.Operations; + foreach(Dictionary refs in node.ExternalReferences) + { + foreach (ExternalReference extRef in refs.Values) + { + VariableDeclaration varDecl = context.GetASTNodeById(extRef.declaration) as VariableDeclaration; + Regex assignChk = new Regex($"{varDecl.Name}([^a-zA-Z_0-9].*:=|:=)"); + Regex storeCheck = new Regex(@"store.?\s*\(\s*" + varDecl.Name + @"_slot\s*,"); + if (assignChk.IsMatch(ops) || storeCheck.IsMatch(ops)) + { + string boogieVar = TransUtils.GetCanonicalVariableName(varDecl, context); + BoogieHavocCmd varHavoc = new BoogieHavocCmd(new BoogieIdentifierExpr(boogieVar)); + this.currentStmtList.AddStatement(varHavoc); + } + + } + } + + return false; + } + Console.WriteLine($"Warning: Inline assembly in function {currentFunction.Name}; replacing function result with non-det value"); throw new NotImplementedException("inline assembly"); } diff --git a/Sources/SolToBoogie/RevertLogicGenerator.cs b/Sources/SolToBoogie/RevertLogicGenerator.cs index ecdcecde..5fbbba04 100644 --- a/Sources/SolToBoogie/RevertLogicGenerator.cs +++ b/Sources/SolToBoogie/RevertLogicGenerator.cs @@ -37,6 +37,21 @@ private bool isPublic(BoogieProcedure proc) return false; } + private bool isPayable(BoogieProcedure proc) + { + //return true; + if (proc.Attributes != null) + { + foreach (var attr in proc.Attributes) + { + if (attr.Key.Equals("payable")) + return true; + } + } + + return false; + } + private BoogieProcedure duplicateProcedure(BoogieProcedure proc, string newNameSuffix, bool dropPublic = false) { BoogieProcedure dup = new BoogieProcedure(proc.Name + "__" + newNameSuffix, @@ -402,6 +417,20 @@ public void Generate() // Call Successful version. BoogieStmtList successCallStmtList = new BoogieStmtList(); + if (isPayable(proc)) + { + successCallStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("msgsender_MSG")); + var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("this")); + var msgVal = new BoogieIdentifierExpr("msgvalue_MSG"); + //assume Balance[msg.sender] >= msg.value + successCallStmtList.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgVal))); + //balance[msg.sender] = balance[msg.sender] - msg.value + successCallStmtList.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal))); + //balance[this] = balance[this] + msg.value + successCallStmtList.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); + successCallStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); + } successCallStmtList.AddStatement(new BoogieCallCmd(impl.Name + "__success", impl.InParams.Select(inParam => (BoogieExpr)new BoogieIdentifierExpr(inParam.Name)).ToList(), impl.OutParams.Select(outParam => new BoogieIdentifierExpr(outParam.Name)).ToList())); @@ -422,6 +451,21 @@ public void Generate() string shadowName = shadowGlobalPair.Value.Name; failCallStmtList.AddStatement(new BoogieAssignCmd(new BoogieIdentifierExpr(shadowName), new BoogieIdentifierExpr(origVarName))); } + + if (isPayable(proc)) + { + failCallStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr("msgsender_MSG")); + var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr("this")); + var msgVal = new BoogieIdentifierExpr("msgvalue_MSG"); + //assume Balance[msg.sender] >= msg.value + failCallStmtList.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgVal))); + //balance[msg.sender] = balance[msg.sender] - msg.value + failCallStmtList.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal))); + //balance[this] = balance[this] + msg.value + failCallStmtList.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); + failCallStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); + } failCallStmtList.AddStatement(new BoogieCallCmd(impl.Name + "__fail", impl.InParams.Select(inParam => (BoogieExpr)new BoogieIdentifierExpr(inParam.Name)).ToList(), impl.OutParams.Select(outParam => new BoogieIdentifierExpr(outParam.Name)).ToList())); @@ -516,8 +560,20 @@ private BoogieImplementation CreateSendFail() exceptionCase.AddStatement(new BoogieAssignCmd(new BoogieIdentifierExpr(tmpLocalName), new BoogieIdentifierExpr(shadowName))); } - - exceptionCase.AddStatement(new BoogieIfCmd(checkTmpBalGuard, BoogieStmtList.MakeSingletonStmtList(callFailDispatch), null)); + + BoogieStmtList exStmtList = new BoogieStmtList(); + exStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var exBalFrom = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr(inParams[0].Name)); + var exBalTo = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr(inParams[1].Name)); + var exMsgVal = new BoogieIdentifierExpr(inParams[2].Name); + //balance[msg.sender] = balance[msg.sender] - msg.value + exStmtList.AddStatement(new BoogieAssignCmd(exBalFrom, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, exBalFrom, exMsgVal))); + //balance[this] = balance[this] + msg.value + exStmtList.AddStatement(new BoogieAssignCmd(exBalTo, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, exBalTo, exMsgVal))); + exStmtList.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); + exStmtList.AddStatement(callFailDispatch); + + exceptionCase.AddStatement(new BoogieIfCmd(checkTmpBalGuard, exStmtList, null)); exceptionCase.AddStatement(new BoogieAssignCmd(successId, new BoogieLiteralExpr(false))); BoogieExpr failAssumePred = revertId; if (context.TranslateFlags.InstrumentGas) @@ -540,6 +596,12 @@ private BoogieImplementation CreateSendFail() var successCase = new BoogieStmtList(); var successDispatchCall = new BoogieStmtList(); + successDispatchCall.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + //balance[msg.sender] = balance[msg.sender] - msg.value + successDispatchCall.AddStatement(new BoogieAssignCmd(exBalFrom, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, exBalFrom, exMsgVal))); + //balance[this] = balance[this] + msg.value + successDispatchCall.AddStatement(new BoogieAssignCmd(exBalTo, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, exBalTo, exMsgVal))); + successDispatchCall.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); successDispatchCall.AddStatement(callFailDispatch); successDispatchCall.AddStatement(new BoogieAssignCmd(successId, new BoogieLiteralExpr(true))); @@ -632,9 +694,22 @@ private BoogieImplementation CreateSendSucess() var checkTmpBalGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), fromId), amtId); + + + BoogieStmtList exceptionThen = new BoogieStmtList(); + exceptionThen.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var exBalFrom = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr(inParams[0].Name)); + var exBalTo = new BoogieMapSelect(new BoogieIdentifierExpr(shadowGlobals["Balance"].Name), new BoogieIdentifierExpr(inParams[1].Name)); + var exMsgVal = new BoogieIdentifierExpr(inParams[2].Name); + //balance[msg.sender] = balance[msg.sender] - msg.value + exceptionThen.AddStatement(new BoogieAssignCmd(exBalFrom, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, exBalFrom, exMsgVal))); + //balance[this] = balance[this] + msg.value + exceptionThen.AddStatement(new BoogieAssignCmd(exBalTo, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, exBalTo, exMsgVal))); + exceptionThen.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); var callFailDispatch = new BoogieCallCmd("FallbackDispatch__fail", new List() {fromId, toId, amtId}, null); + exceptionThen.AddStatement(callFailDispatch); - exceptionCase.AddStatement(new BoogieIfCmd(checkTmpBalGuard, BoogieStmtList.MakeSingletonStmtList(callFailDispatch), null)); + exceptionCase.AddStatement(new BoogieIfCmd(checkTmpBalGuard, exceptionThen, null)); exceptionCase.AddStatement(new BoogieAssignCmd(successId, new BoogieLiteralExpr(false))); @@ -654,6 +729,15 @@ private BoogieImplementation CreateSendSucess() amtId); var successCaseStmts = new BoogieStmtList(); + successCaseStmts.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var balFrom = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr(inParams[0].Name)); + var balTo = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr(inParams[1].Name)); + var msgVal = new BoogieIdentifierExpr(inParams[2].Name); + //balance[msg.sender] = balance[msg.sender] - msg.value + successCaseStmts.AddStatement(new BoogieAssignCmd(balFrom, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balFrom, msgVal))); + //balance[this] = balance[this] + msg.value + successCaseStmts.AddStatement(new BoogieAssignCmd(balTo, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balTo, msgVal))); + successCaseStmts.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); var callSuccessDispatch = new BoogieCallCmd("FallbackDispatch__success", new List(){fromId, toId, amtId}, null); successCaseStmts.AddStatement(callSuccessDispatch); successCaseStmts.AddStatement(new BoogieAssignCmd(successId, new BoogieLiteralExpr(true))); diff --git a/Sources/SolToBoogie/SolToBoogie.csproj b/Sources/SolToBoogie/SolToBoogie.csproj index ce0e4a13..b42c4b98 100644 --- a/Sources/SolToBoogie/SolToBoogie.csproj +++ b/Sources/SolToBoogie/SolToBoogie.csproj @@ -14,6 +14,7 @@ + diff --git a/Sources/SolToBoogie/TransUtils.cs b/Sources/SolToBoogie/TransUtils.cs index 7a3acac3..2720b56f 100644 --- a/Sources/SolToBoogie/TransUtils.cs +++ b/Sources/SolToBoogie/TransUtils.cs @@ -1,5 +1,8 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using System.Security.Cryptography; + namespace SolToBoogie { using System; @@ -7,13 +10,13 @@ namespace SolToBoogie using System.ComponentModel.DataAnnotations; using System.Diagnostics; using System.Numerics; - using System.Text; - using System.Text.RegularExpressions; + using System.Text; + using System.Text.RegularExpressions; using BoogieAST; using SolidityAST; - public static class Extensions - { + public static class Extensions + { public static bool IsInt(this TypeDescription typeDescription) { return !typeDescription.IsDynamicArray() && !typeDescription.IsStaticArray() @@ -262,21 +265,21 @@ public static bool IsDynamicArray(this TypeDescription typeDescription) { var match = Regex.Match(typeDescription.TypeString, @".*\[\]").Success; return match; - } - - // TODO: Provide a better way to check for array type + } + + // TODO: Provide a better way to check for array type public static bool IsStaticArray(this TypeDescription typeDescription) { var match = Regex.Match(typeDescription.TypeString, @".*\[\d+\]").Success; - return match; + return match; } - + public static bool IsArray(this TypeDescription typeDescription) { return IsStaticArray(typeDescription) || IsDynamicArray(typeDescription); } - } - + } + public static class TransUtils { public static BoogieType GetBoogieTypeFromSolidityTypeName(TypeName type) @@ -459,7 +462,36 @@ public static string GetCanonicalStateVariableName(VariableDeclaration varDecl, public static string GetCanonicalFunctionName(FunctionDefinition funcDef, TranslatorContext context) { ContractDefinition contract = context.GetContractByFunction(funcDef); - return funcDef.Name + "_" + contract.Name; + string paramStr = ""; + + if (funcDef.Parameters != null) + { + foreach (VariableDeclaration paramDecl in funcDef.Parameters.Parameters) + { + String typeStr = ""; + if (paramDecl.TypeName is Mapping map) + { + typeStr = "map" + map.KeyType.ToString(); + } + else if (paramDecl.TypeName is UserDefinedTypeName userDef) + { + typeStr = userDef.Name; + } + else if (paramDecl.TypeName is ArrayTypeName arr) + { + typeStr = "arr"; + } + else + { + typeStr = paramDecl.TypeName.ToString().Replace(" ", ""); + } + + paramStr = $"{paramStr}~{typeStr}"; + } + } + + return $"{funcDef.Name}{paramStr}_{contract.Name}"; + //return funcDef.Name + "_" + contract.Name; } public static string GetCanonicalConstructorName(ContractDefinition contract) @@ -525,11 +557,12 @@ public static string ComputeEventSignature(EventDefinition eventDef) return builder.ToString(); } - public static string InferFunctionSignature(TranslatorContext context, FunctionCall node) + public static string InferFunctionSignature(TranslatorContext context, FunctionCall node, + bool forceNameLookup = false) { Debug.Assert(node.Arguments != null); - if (node.Expression is MemberAccess memberAccess) + if (!forceNameLookup && node.Expression is MemberAccess memberAccess) { Debug.Assert(memberAccess.ReferencedDeclaration != null); FunctionDefinition function = context.GetASTNodeById(memberAccess.ReferencedDeclaration.Value) as FunctionDefinition; @@ -562,9 +595,9 @@ public static string InferFunctionSignature(TranslatorContext context, FunctionC } builder.Length -= 2; } - builder.Append(")"); - return builder.ToString(); - } + builder.Append(")"); + return builder.ToString(); + } } private static string InferTypeFromTypeString(string typestr) @@ -607,104 +640,104 @@ private static string InferTypeFromTypeString(string typestr) return typeString; } - public static string InferTypeFromExpression(Expression expression) - { - Debug.Assert(expression.TypeDescriptions != null, $"Null type description for {expression}"); - string typeString = expression.TypeDescriptions.TypeString; - if (typeString.Equals("bool")) - { - return "bool"; - } - else if (typeString.StartsWith("uint")) - { - return "uint"; - } - else if (typeString.StartsWith("int")) - { - return "int"; - } - else if (typeString.Equals("address") || typeString.Equals("address payable")) - { - return "address"; - } - else - { - throw new SystemException($"Unknown type string {typeString} for expression {expression}"); - } - } - - public static string GetFuncNameFromFuncCall(FunctionCall node) - { - if (node.Expression is FunctionCall funcCall) - { - if (funcCall.Expression is MemberAccess memberAccess) - { - return GetFuncNameFromFuncCallExpr(memberAccess.Expression); - } - else - { - return GetFuncNameFromFuncCallExpr(funcCall.Expression); - } - } - else - { - return GetFuncNameFromFuncCallExpr(node.Expression); - } - } - - public static string GetFuncNameFromFuncCallExpr(Expression expr) - { - string functionName = null; - if (expr is Identifier ident) - { - functionName = ident.Name; - } + public static string InferTypeFromExpression(Expression expression) + { + Debug.Assert(expression.TypeDescriptions != null, $"Null type description for {expression}"); + string typeString = expression.TypeDescriptions.TypeString; + if (typeString.Equals("bool")) + { + return "bool"; + } + else if (typeString.StartsWith("uint")) + { + return "uint"; + } + else if (typeString.StartsWith("int")) + { + return "int"; + } + else if (typeString.Equals("address") || typeString.Equals("address payable")) + { + return "address"; + } + else + { + throw new SystemException($"Unknown type string {typeString} for expression {expression}"); + } + } + + public static string GetFuncNameFromFuncCall(FunctionCall node) + { + if (node.Expression is FunctionCall funcCall) + { + if (funcCall.Expression is MemberAccess memberAccess) + { + return GetFuncNameFromFuncCallExpr(memberAccess.Expression); + } + else + { + return GetFuncNameFromFuncCallExpr(funcCall.Expression); + } + } + else + { + return GetFuncNameFromFuncCallExpr(node.Expression); + } + } + + public static string GetFuncNameFromFuncCallExpr(Expression expr) + { + string functionName = null; + if (expr is Identifier ident) + { + functionName = ident.Name; + } else if (expr is ElementaryTypeNameExpression elemExpr) { functionName = elemExpr.TypeName; - } - else if (expr is MemberAccess memberAccess) - { - functionName = memberAccess.MemberName; - } - else if (expr is FunctionCall funcCall) - { - functionName = GetFuncNameFromFuncCall(funcCall); - } - else - { - throw new SystemException($"Unknown form of function call expr: {expr}"); - } - Debug.Assert(functionName != null); - return functionName; - } - - public static Tuple GenerateSourceInfoAnnotation(ASTNode node, TranslatorContext context) - { - return (Tuple.Create(context.GetAbsoluteSourcePathOfASTNode(node), context.GetLineNumberOfASTNode(node))); - } - - public static List GetDefaultInParams() - { - return new List() - { - // add a parameter for this object - new BoogieFormalParam(new BoogieTypedIdent("this", BoogieType.Ref)), - // add a parameter for msg.sender - new BoogieFormalParam(new BoogieTypedIdent("msgsender_MSG", BoogieType.Ref)), - // add a parameter for msg.value - new BoogieFormalParam(new BoogieTypedIdent("msgvalue_MSG", BoogieType.Int)), - }; - } - - public static List GetDefaultArguments() - { - return new List() - { - new BoogieIdentifierExpr("this"), - new BoogieIdentifierExpr("msgsender_MSG"), - new BoogieIdentifierExpr("msgvalue_MSG"), - }; + } + else if (expr is MemberAccess memberAccess) + { + functionName = memberAccess.MemberName; + } + else if (expr is FunctionCall funcCall) + { + functionName = GetFuncNameFromFuncCall(funcCall); + } + else + { + throw new SystemException($"Unknown form of function call expr: {expr}"); + } + Debug.Assert(functionName != null); + return functionName; + } + + public static Tuple GenerateSourceInfoAnnotation(ASTNode node, TranslatorContext context) + { + return (Tuple.Create(context.GetAbsoluteSourcePathOfASTNode(node), context.GetLineNumberOfASTNode(node))); + } + + public static List GetDefaultInParams() + { + return new List() + { + // add a parameter for this object + new BoogieFormalParam(new BoogieTypedIdent("this", BoogieType.Ref)), + // add a parameter for msg.sender + new BoogieFormalParam(new BoogieTypedIdent("msgsender_MSG", BoogieType.Ref)), + // add a parameter for msg.value + new BoogieFormalParam(new BoogieTypedIdent("msgvalue_MSG", BoogieType.Int)), + }; + } + + public static List GetDefaultArguments() + { + return new List() + { + new BoogieIdentifierExpr("this"), + new BoogieIdentifierExpr("msgsender_MSG"), + new BoogieIdentifierExpr("msgvalue_MSG"), + }; } public static List CollectLocalVars(List contracts, TranslatorContext context) @@ -769,7 +802,7 @@ public static List CollectLocalVars(List con } return localVars; } - + /// /// generate a non-deterministic choice block to call every public visible functions except constructors /// @@ -778,10 +811,15 @@ public static List CollectLocalVars(List con /// /// If non-null, this will be the msg.sender for calling back into the contracts /// - public static BoogieIfCmd GenerateChoiceBlock(List contracts, TranslatorContext context, Tuple callBackTarget = null) + public static BoogieIfCmd GenerateChoiceBlock(List contracts, TranslatorContext context, bool canRevert, Tuple callBackTarget = null) + { + return GeneratePartialChoiceBlock(contracts, context, new BoogieIdentifierExpr("this"), 0, canRevert, null, callBackTarget).Item1; + } + + public static Tuple GeneratePartialChoiceBlock(List contracts, TranslatorContext context, BoogieExpr thisExpr, int startingPoint, bool canRevert, BoogieIfCmd alternatives = null, Tuple callBackTarget = null) { - BoogieIfCmd ifCmd = null; - int j = 0; + BoogieIfCmd ifCmd = alternatives; + int j = startingPoint; foreach (var contract in contracts) { if (contract.ContractKind != EnumContractKind.CONTRACT) continue; @@ -792,6 +830,12 @@ public static BoogieIfCmd GenerateChoiceBlock(List contracts { if (funcDef.IsConstructor) continue; if (funcDef.IsFallback) continue; //let us not call fallback directly in harness + if (context.TranslateFlags.PerformFunctionSlice && + !context.TranslateFlags.SliceFunctions.Contains(funcDef)) + { + continue; + } + if (funcDef.Visibility == EnumVisibility.PUBLIC || funcDef.Visibility == EnumVisibility.EXTERNAL) { publicFuncDefs.Add(funcDef); @@ -811,7 +855,7 @@ public static BoogieIfCmd GenerateChoiceBlock(List contracts List inputs = new List() { // let us just call back into the calling contract - callBackTarget != null ? new BoogieIdentifierExpr(callBackTarget.Item1) : new BoogieIdentifierExpr("this"), + callBackTarget != null ? new BoogieIdentifierExpr(callBackTarget.Item1) : thisExpr, callBackTarget != null ? new BoogieIdentifierExpr(callBackTarget.Item2) : new BoogieIdentifierExpr("msgsender_MSG"), new BoogieIdentifierExpr("msgvalue_MSG"), }; @@ -823,7 +867,9 @@ public static BoogieIfCmd GenerateChoiceBlock(List contracts { name = TransUtils.GetCanonicalLocalVariableName(param, context); } - inputs.Add(new BoogieIdentifierExpr(name)); + + BoogieIdentifierExpr boogieVar = new BoogieIdentifierExpr(name); + inputs.Add(boogieVar); if (param.TypeName is ArrayTypeName array) { thenBody.AddStatement(new BoogieCallCmd( @@ -831,6 +877,7 @@ public static BoogieIfCmd GenerateChoiceBlock(List contracts new List(), new List() { new BoogieIdentifierExpr(name) })); } + thenBody.AppendStmtList(constrainVarValues(context, param, boogieVar)); } List outputs = new List(); @@ -848,20 +895,84 @@ public static BoogieIfCmd GenerateChoiceBlock(List contracts outputs.Add(new BoogieIdentifierExpr(name)); } + if (funcDef.StateMutability.Equals(EnumStateMutability.PAYABLE)) + { + BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, + new BoogieIdentifierExpr("msgvalue_MSG"), new BoogieLiteralExpr(BigInteger.Zero)); + thenBody.AddStatement(new BoogieAssumeCmd(assumeExpr)); + + if (!canRevert) + { + thenBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function START ")); + var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("msgsender_MSG")); + var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("this")); + var msgVal = new BoogieIdentifierExpr("msgvalue_MSG"); + //assume Balance[msg.sender] >= msg.value + thenBody.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgVal))); + //balance[msg.sender] = balance[msg.sender] - msg.value + thenBody.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal))); + //balance[this] = balance[this] + msg.value + thenBody.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal))); + thenBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function END ")); + } + + } + else + { + BoogieExpr assumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, + new BoogieIdentifierExpr("msgvalue_MSG"), new BoogieLiteralExpr(BigInteger.Zero)); + thenBody.AddStatement(new BoogieAssumeCmd(assumeExpr)); + } + + BoogieCallCmd callCmd = new BoogieCallCmd(callee, inputs, outputs); + thenBody.AddStatement(callCmd); + if (context.TranslateFlags.InstrumentGas) { var gasVar = new BoogieIdentifierExpr("gas"); + + BoogieBinaryOperation gasGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, gasVar, new BoogieLiteralExpr(BigInteger.Zero)); + + BoogieIfCmd ifExpr = new BoogieIfCmd(gasGuard, thenBody, null); + + thenBody = new BoogieStmtList(); + //thenBody.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, gasVar, new BoogieLiteralExpr(TranslatorContext.TX_GAS_COST)))); thenBody.AddStatement(new BoogieAssignCmd(gasVar, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, gasVar, new BoogieLiteralExpr(TranslatorContext.TX_GAS_COST)))); + thenBody.AddStatement(ifExpr); } - BoogieCallCmd callCmd = new BoogieCallCmd(callee, inputs, outputs); - thenBody.AddStatement(callCmd); BoogieStmtList elseBody = ifCmd == null ? null : BoogieStmtList.MakeSingletonStmtList(ifCmd); ifCmd = new BoogieIfCmd(guard, thenBody, elseBody); } } - return ifCmd; + return new Tuple(ifCmd, j); + } + + public static BoogieStmtList constrainVarValues(TranslatorContext context, VariableDeclaration var, BoogieIdentifierExpr boogieVar) + { + BoogieStmtList stmts = new BoogieStmtList(); + + if (context.TranslateFlags.UseModularArithmetic) + { + if (var.TypeDescriptions.IsUintWSize(null, out uint uintSize)) + { + BigInteger maxUIntValue = (BigInteger)Math.Pow(2, uintSize); + BoogieBinaryOperation lower = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, boogieVar, new BoogieLiteralExpr(BigInteger.Zero)); + BoogieBinaryOperation upper = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.LT, boogieVar, new BoogieLiteralExpr(maxUIntValue)); + stmts.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.AND, lower, upper))); + } + else if (var.TypeDescriptions.IsIntWSize(out uint intSize)) + { + BigInteger maxIntValue = (BigInteger)Math.Pow(2, intSize); + BoogieBinaryOperation lower = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, boogieVar, new BoogieLiteralExpr(-maxIntValue)); + BoogieBinaryOperation upper = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.LT, boogieVar, new BoogieLiteralExpr(maxIntValue)); + stmts.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.AND, lower, upper))); + } + } + + return stmts; } + public static void havocGas(BoogieStmtList list) { List cmdList = new List(); @@ -877,6 +988,63 @@ public static void havocGas(List list) new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GT, gasVar, new BoogieLiteralExpr(TranslatorContext.MIN_GAS_LIMIT)), new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.LE, gasVar, new BoogieLiteralExpr(TranslatorContext.MAX_GAS_LIMIT))))); } - - } -} + + public static BoogieExpr GetDefaultVal(TypeName type) + { + return GetDefaultVal(TransUtils.GetBoogieTypeFromSolidityTypeName(type)); + } + public static BoogieExpr GetDefaultVal(BoogieType boogieType) + { + if (boogieType.Equals(BoogieType.Int)) + { + return new BoogieLiteralExpr(BigInteger.Zero); + } + else if (boogieType.Equals(BoogieType.Bool)) + { + return new BoogieLiteralExpr(false); + } + else if (boogieType.Equals(BoogieType.Ref)) + { + return new BoogieIdentifierExpr("null"); + } + + throw new Exception($"Unknown BoogieType {boogieType}"); + } + + public static TypeDescription TypeNameToTypeDescription(TypeName typeName) + { + if (typeName is ArrayTypeName arr) + { + TypeDescription desc = TypeNameToTypeDescription(arr.BaseType); + desc.TypeIndentifier = $"{desc.TypeIndentifier}[]"; + desc.TypeString = $"{desc.TypeString}[]"; + return desc; + } + else if (typeName is Mapping map) + { + TypeDescription keyDesc = TypeNameToTypeDescription(map.KeyType); + TypeDescription valDesc = TypeNameToTypeDescription(map.ValueType); + TypeDescription desc = new TypeDescription(); + desc.TypeIndentifier = $"mapping({keyDesc.TypeIndentifier} => {valDesc.TypeIndentifier})"; + desc.TypeString = $"mapping({keyDesc.TypeString} => {valDesc.TypeString})"; + return desc; + } + else if (typeName is ElementaryTypeName elem) + { + TypeDescription desc = new TypeDescription(); + desc.TypeIndentifier = elem.TypeDescriptions.TypeIndentifier; + desc.TypeString = elem.TypeDescriptions.TypeString; + return desc; + } + else if (typeName is UserDefinedTypeName user) + { + TypeDescription desc = new TypeDescription(); + desc.TypeIndentifier = user.TypeDescriptions.TypeIndentifier; + desc.TypeString = user.TypeDescriptions.TypeString; + return desc; + } + + throw new Exception("Unknown type name"); + } + } +} diff --git a/Sources/SolToBoogie/TranslatorContext.cs b/Sources/SolToBoogie/TranslatorContext.cs index 558fbdfa..9f6c5a21 100644 --- a/Sources/SolToBoogie/TranslatorContext.cs +++ b/Sources/SolToBoogie/TranslatorContext.cs @@ -1,5 +1,8 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using SolidityAnalysis; + namespace SolToBoogie { using System; @@ -93,11 +96,13 @@ public class TranslatorContext public Dictionary> ModifierToPreludeLocalVars { get; private set; } public String EntryPointContract { get; private set; } + + public SolidityAnalyzer Analysis { get; private set; } // Options flags public TranslatorFlags TranslateFlags { get; private set; } - public Dictionary> UsingMap => usingMap; + public Dictionary>> UsingMap => usingMap; // num of fresh identifiers, should be incremented when making new fresh id private int freshIdentifierCount = 0; @@ -110,9 +115,11 @@ public class TranslatorContext // data structures for using // maps Contract C --> (source, dest), where source is a library type - private readonly Dictionary> usingMap; + private readonly Dictionary>> usingMap; + + public HashSet initFns { get; set; } - public TranslatorContext(HashSet> ignoreMethods, bool _genInlineAttrInBpl, TranslatorFlags _translateFlags = null, String entryPointContract = "") + public TranslatorContext(AST solidityAST, HashSet> ignoreMethods, bool _genInlineAttrInBpl, TranslatorFlags _translateFlags = null, String entryPointContract = "") { Program = new BoogieProgram(); ContractDefinitions = new HashSet(); @@ -139,11 +146,13 @@ public TranslatorContext(HashSet> ignoreMethods, bool _gen ModifierToBoogiePreImpl = new Dictionary(); ModifierToBoogiePostImpl = new Dictionary(); ModifierToPreludeLocalVars = new Dictionary>(); - usingMap = new Dictionary>(); + usingMap = new Dictionary>>(); IgnoreMethods = ignoreMethods; genInlineAttrInBpl = _genInlineAttrInBpl; TranslateFlags = _translateFlags; EntryPointContract = entryPointContract; + Analysis = new SolidityAnalyzer(solidityAST, ignoreMethods, entryPointContract); + initFns = new HashSet(); } public bool HasASTNodeId(int id) @@ -471,6 +480,12 @@ public bool HasStateVarName(string varName) return StateVarNameResolutionMap.ContainsKey(varName); } + public bool HasStateVar(string varName, ContractDefinition dynamicType) + { + return StateVarNameResolutionMap.ContainsKey(varName) && + StateVarNameResolutionMap[varName].ContainsKey(dynamicType); + } + public VariableDeclaration GetStateVarByDynamicType(string varName, ContractDefinition dynamicType) { return StateVarNameResolutionMap[varName][dynamicType]; diff --git a/Sources/SolToBoogie/TranslatorFlags.cs b/Sources/SolToBoogie/TranslatorFlags.cs index 1726aada..6965ef50 100644 --- a/Sources/SolToBoogie/TranslatorFlags.cs +++ b/Sources/SolToBoogie/TranslatorFlags.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Text; +using SolidityAST; namespace SolToBoogie { @@ -25,14 +26,47 @@ public TranslatorFlags() PerformContractInferce = false; DoModSetAnalysis = false; RemoveScopeInVarName = false; - QuantFreeAllocs = false; - LazyNestedAlloc = false; InstrumentSums = false; NoBoogieHarness = false; CreateMainHarness = false; NoCustomTypes = false; OmitAssumeFalseForDynDispatch = false; + NoTxnsFromContract = true; + RunAliasAnalysis = false; + UseMultiDim = false; + TxnsOnFields = false; + NoNonlinearArith = false; + UseNumericOperators = false; + LazyAllocNoMod = false; + QuantFreeAllocs = false; + LazyNestedAlloc = false; + PrePostHarness = false; + GenerateGetters = false; + GenerateERC20Spec = false; + SliceFunctionNames = new HashSet(); + SliceFunctions = new HashSet(); + SliceModifiers = new HashSet(); + PerformFunctionSlice = false; + AssemblyAsHavoc = false; } + + public bool PerformFunctionSlice { get; set; } + + public bool AssemblyAsHavoc { get; set; } + + public HashSet SliceModifiers { get; set; } + public HashSet SliceFunctions { get; set; } + + public HashSet SliceFunctionNames { get; set; } + public bool UseNumericOperators { get; set; } + public bool NoNonlinearArith { get; set; } + + public bool TxnsOnFields { get; set; } + + public bool RunAliasAnalysis { get; set; } + + public bool NoTxnsFromContract { get; set; } + public bool NoCustomTypes { get; set; } public bool CreateMainHarness { get; set; } @@ -85,6 +119,8 @@ public TranslatorFlags() /// Allocate nested maps lazily, i.e., eliminate HavocAllocMany /// public bool LazyNestedAlloc { get; set; } + + public bool LazyAllocNoMod { get; set; } /// /// Remove assume false for the default branch of dyn dispatch @@ -97,6 +133,8 @@ public TranslatorFlags() public bool ModelStubsAsSkips() { return ModelOfStubs.Equals("skip"); } public bool ModelStubsAsCallbacks() { return ModelOfStubs.Equals("callback"); } + public bool ModelStubsAsMultipleCallbacks() { return ModelOfStubs.Equals("multipleCallbacks"); } + // this translates to /inlineDepth:k when calling Boogie with /contractInfer public int InlineDepthForBoogie { get; set; } public bool PerformContractInferce { get; set; } @@ -106,5 +144,13 @@ public TranslatorFlags() // remove the scoping from variable name (risky and not exposed) public bool RemoveScopeInVarName { get; set; } + + public bool PrePostHarness { get; set; } + + public bool UseMultiDim { get; set; } + + public bool GenerateGetters { get; set; } + + public bool GenerateERC20Spec { get; set; } } } diff --git a/Sources/SolToBoogie/UsingCollector.cs b/Sources/SolToBoogie/UsingCollector.cs index 0b37269b..f864b977 100644 --- a/Sources/SolToBoogie/UsingCollector.cs +++ b/Sources/SolToBoogie/UsingCollector.cs @@ -1,5 +1,8 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. + +using System.Linq; + namespace SolToBoogie { using SolidityAST; @@ -21,25 +24,28 @@ public UsingCollector(TranslatorContext context) this.context = context; } - public override bool Visit(ContractDefinition node) - { - currentContract = node; - context.UsingMap[currentContract] = new Dictionary(); - return true; - } - - public override void EndVisit(ContractDefinition node) - { - currentContract = null; + public override bool Visit(ContractDefinition node) + { + currentContract = node; + context.UsingMap[currentContract] = new Dictionary>(); + return true; + } + + public override void EndVisit(ContractDefinition node) + { + currentContract = null; } public override bool Visit(UsingForDirective node) { - if (node.TypeName is UserDefinedTypeName userType) + if (context.UsingMap[currentContract].ContainsKey(node.LibraryName)) + { + context.UsingMap[currentContract][node.LibraryName].Add(node.TypeName); + } + else { - Debug.Assert(!userType.TypeDescriptions.IsContract(), $"VeriSol does not support using A for B where B is a contract name, found {userType.ToString()}"); + context.UsingMap[currentContract][node.LibraryName] = new List() {node.TypeName}; } - context.UsingMap[currentContract][node.LibraryName] = node.TypeName; return true; } } diff --git a/Sources/SolidityAST/SolidityAST.cs b/Sources/SolidityAST/SolidityAST.cs index 4666e9bf..a86a48c2 100644 --- a/Sources/SolidityAST/SolidityAST.cs +++ b/Sources/SolidityAST/SolidityAST.cs @@ -881,7 +881,7 @@ public override T Accept(IASTGenericVisitor visitor) public override string ToString() { StringBuilder builder = new StringBuilder(); - builder.Append("mapping (").Append(KeyType).Append(" => ").Append(ValueType).Append(")"); + builder.Append("mapping(").Append(KeyType).Append(" => ").Append(ValueType).Append(")"); return builder.ToString(); } } @@ -1261,7 +1261,7 @@ public override string ToString() public class VariableDeclarationStatement : Statement { - public List Assignments { get; set; } + public List Assignments { get; set; } public List Declarations { get; set; } @@ -1271,8 +1271,15 @@ public override void Accept(IASTVisitor visitor) { if (visitor.Visit(this)) { - Debug.Assert(Declarations.Count == 1); - Utils.AcceptList(Declarations, visitor); + //Debug.Assert(Declarations.Count == 1); + //Utils.AcceptList(Declarations, visitor); + foreach (VariableDeclaration varDecl in Declarations) + { + if (varDecl != null) + { + varDecl.Accept(visitor); + } + } if (InitialValue != null) { InitialValue.Accept(visitor); @@ -1289,8 +1296,16 @@ public override T Accept(IASTGenericVisitor visitor) public override string ToString() { StringBuilder builder = new StringBuilder(); - Debug.Assert(Declarations.Count == 1, $"Multiple variable declarations: {Declarations.Count}"); - builder.Append(Declarations[0]); + //Debug.Assert(Declarations.Count == 1, $"Multiple variable declarations: {Declarations.Count}"); + if (Declarations.Count > 1) + { + builder.Append($"({String.Join(", ", Declarations)})"); + } + else + { + builder.Append(Declarations[0]); + } + if (InitialValue != null) { builder.Append(" = ").Append(InitialValue); @@ -1300,9 +1315,18 @@ public override string ToString() } } + public class ExternalReference + { + public int declaration { get; set; } + public bool isOffset { get; set; } + public bool isSlot { get; set; } + public String src { get; set; } + public int valueSize { get; set; } + } public class InlineAssembly : Statement { - public List ExternalReferences { get; set; } + //public List ExternalReferences { get; set; } + public List> ExternalReferences { get; set; } public string Operations { get; set; } diff --git a/Sources/SolidityAST/SolidityCompiler.cs b/Sources/SolidityAST/SolidityCompiler.cs index 6721b3f1..24b603f2 100644 --- a/Sources/SolidityAST/SolidityCompiler.cs +++ b/Sources/SolidityAST/SolidityCompiler.cs @@ -1,4 +1,4 @@ -// Copyright (c) Microsoft Corporation. All rights reserved. +// Copyright (c) Microsoft Corporation. All rights reserved. // Licensed under the MIT license. namespace SolidityAST { @@ -20,7 +20,7 @@ public CompilerOutput Compile(string solcPath, string derivedFilePath) } derivedFilePath = derivedFilePath.Replace("\\", "/" /*, StringComparison.CurrentCulture*/); - + Console.WriteLine(solcPath); string jsonString = RunSolc(solcPath, derivedFilePath); List errors = new List(); @@ -33,6 +33,7 @@ public CompilerOutput Compile(string solcPath, string derivedFilePath) }, }; + CompilerOutput compilerOutput = JsonConvert.DeserializeObject(jsonString); if (errors.Count != 0) { @@ -41,10 +42,10 @@ public CompilerOutput Compile(string solcPath, string derivedFilePath) return compilerOutput; } - /// - /// - /// - /// Path to the top-level solidty file + /// + /// + /// + /// Path to the top-level solidty file /// private string RunSolc(string solcPath, string derivedFilePath) { @@ -62,7 +63,7 @@ private string RunSolc(string solcPath, string derivedFilePath) p.Start(); string configString = "{ \"language\": \"Solidity\", \"sources\": { %SOLPLACEHOLDER%: { \"urls\": [ %URLPLACEHOLDER% ]}}," - + "\"settings\": {\"evmVersion\": \"byzantium\", \"outputSelection\": {\"*\": {\"\": [ \"ast\" ]}}}}"; + + "\"settings\": {\"evmVersion\": \"constantinople\", \"outputSelection\": {\"*\": {\"\": [ \"ast\" ]}}}}"; configString = configString.Replace("%SOLPLACEHOLDER%", "\"" + derivedFileName + "\"" /*, StringComparison.CurrentCulture*/); configString = configString.Replace("%URLPLACEHOLDER%", "\"" + derivedFilePath + "\""/*, StringComparison.CurrentCulture*/); diff --git a/Sources/SolidityAnalysis/AliasAnalysis.cs b/Sources/SolidityAnalysis/AliasAnalysis.cs new file mode 100644 index 00000000..80b47f8f --- /dev/null +++ b/Sources/SolidityAnalysis/AliasAnalysis.cs @@ -0,0 +1,241 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using solidityAnalysis; +using SolidityAST; + +namespace SolidityAnalysis +{ + + public class AliasAnalysis : BasicASTVisitor + { + private List results; + //private Dictionary nameToStruct; + private AST solidityAST; + private HashSet> ignoredMethods; + private String entryPoint; + + public AliasAnalysis(AST solidityAST, HashSet> ignoredMethods, String entryPointContract = "") + { + this.solidityAST = solidityAST; + this.ignoredMethods = ignoredMethods; + this.entryPoint = entryPointContract; + //this.nameToStruct = new Dictionary(); + this.results = null; + } + + public List getResults() + { + if (results == null) + { + runAnalysis(); + } + + return results; + } + + public void runAnalysis() + { + results = new List(); + solidityAST.GetSourceUnits().Accept(this); + } + + public String getGroupName(VariableDeclaration varDec) + { + if (getResults().Contains(varDec)) + { + return varDec.Name + results.IndexOf(varDec); + } + + return ""; + } + + public override bool Visit(StructDefinition def) + { + //nameToStruct.Add(def.Name, def); + return true; + } + + public override bool Visit(VariableDeclaration decl) + { + TypeName type = decl.TypeName; + if (decl.Name == "" || type is ElementaryTypeName || decl.StateVariable == false) + { + return false; + } + + if (type is Mapping || type is ArrayTypeName) + { + results.Add(decl); + } + + /* Can we add in user-defined types? + else if (type is UserDefinedTypeName userDefined) + { + results.Add(decl); + }*/ + + return true; + } + + public override bool Visit(Identifier ident) + { + if (!solidityAST.GetIdToNodeMap().ContainsKey(ident.ReferencedDeclaration)) + { + return true; + } + + ASTNode node = solidityAST.GetASTNodeByID(ident.ReferencedDeclaration); + if (!(node is VariableDeclaration)) + { + return true; + } + + VariableDeclaration decl = (VariableDeclaration) node; + results.Remove(decl); + return false; + } + + public TypeName getBaseType(TypeName ty) + { + while (ty is Mapping || ty is ArrayTypeName) + { + if (ty is Mapping mapping) + { + ty = mapping.ValueType; + } + else if (ty is ArrayTypeName arr) + { + ty = arr.BaseType; + } + } + + return ty; + } + + public int getIndexDimSize(TypeName ty) + { + int dimSize = 0; + while (ty is Mapping || ty is ArrayTypeName) + { + dimSize++; + if (ty is Mapping mapping) + { + ty = mapping.ValueType; + } + else if (ty is ArrayTypeName arr) + { + ty = arr.BaseType; + } + } + + return dimSize; + } + + public override bool Visit(IndexAccess access) + { + if (access.BaseExpression.ToString().Equals("msg.data")) + { + return false; + } + + DeclarationFinder declFinder = new DeclarationFinder(access, solidityAST); + VariableDeclaration decl = declFinder.getDecl(); + + if (results.Contains(decl)) + { + int numAccesses = declFinder.getNumAccesses(); + int numIndexDims = getIndexDimSize(decl.TypeName); + + if (numIndexDims != numAccesses) + { + results.Remove(decl); + } + } + + return false; + } + + /* + * Guide analysis to statements that can cause aliasing. i.e. rhs expressions, function arguments, etc + */ + + public override bool Visit(Assignment node) + { + if (node.Operator == "=") + { + node.LeftHandSide.Accept(this); + node.RightHandSide.Accept(this); + } + + return false; + } + + public override bool Visit(FunctionDefinition node) + { + return node.Implemented; + } + + /* + * Nodes that cannot cause aliasing + */ + + public override bool Visit(ArrayTypeName node) + { + return false; + } + + public override bool Visit(Break node) + { + return false; + } + + public override bool Visit(BinaryOperation node) + { + return false; + } + + public override bool Visit(EmitStatement node) + { + return false; + } + + public override bool Visit(UnaryOperation node) + { + return false; + } + + public override bool Visit(EventDefinition node) + { + return false; + } + + public override bool Visit(UsingForDirective node) + { + return false; + } + + public override bool Visit(PragmaDirective node) + { + return false; + } + + public override bool Visit(ImportDirective node) + { + return false; + } + + public override bool Visit(Continue node) + { + return false; + } + + public void assert(bool cond, String msg) + { + if (!cond) + { + throw new Exception("AliasAnalysis Exception: " + msg); + } + } + } +} \ No newline at end of file diff --git a/Sources/SolidityAnalysis/DeclarationFinder.cs b/Sources/SolidityAnalysis/DeclarationFinder.cs new file mode 100644 index 00000000..4a174fb6 --- /dev/null +++ b/Sources/SolidityAnalysis/DeclarationFinder.cs @@ -0,0 +1,67 @@ +using System; +using SolidityAST; + +namespace solidityAnalysis +{ + public class DeclarationFinder : BasicASTVisitor + { + private Expression start; + private int numAccesses; + private VariableDeclaration result; + private AST solidityAST; + + public DeclarationFinder(Expression access, AST solidityAst) + { + this.solidityAST = solidityAst; + this.start = access; + this.numAccesses = 0; + start.Accept(this); + } + public override bool Visit(IndexAccess access) + { + numAccesses++; + access.BaseExpression.Accept(this); + return false; + } + + public override bool Visit(MemberAccess access) + { + if (access.ReferencedDeclaration.HasValue) + { + ASTNode node = solidityAST.GetASTNodeByID(access.ReferencedDeclaration.Value); + if (node is VariableDeclaration decl) + { + result = decl; + return false; + } + + throw new Exception("Analysis Exception: Expected member access declaration to be of VariableDeclaration type, not " + node.GetType()); + } + + access.Expression.Accept(this); + return false; + } + + public override bool Visit(Identifier ident) + { + ASTNode node = solidityAST.GetASTNodeByID(ident.ReferencedDeclaration); + if (node is VariableDeclaration decl) + { + result = decl; + return false; + } + + throw new Exception("Analysis Exception: Expected identifier declaration to be of VariableDeclaration type, not " + node.GetType()); + } + + public VariableDeclaration getDecl() + { + return result; + } + + public int getNumAccesses() + { + return numAccesses; + } + } +} diff --git a/Sources/SolidityAnalysis/SolidityAnalysis.csproj b/Sources/SolidityAnalysis/SolidityAnalysis.csproj new file mode 100644 index 00000000..dd2f9204 --- /dev/null +++ b/Sources/SolidityAnalysis/SolidityAnalysis.csproj @@ -0,0 +1,16 @@ + + + Library + netcoreapp2.2 + true + + + + + + + + + + + \ No newline at end of file diff --git a/Sources/SolidityAnalysis/SolidityAnalyzer.cs b/Sources/SolidityAnalysis/SolidityAnalyzer.cs new file mode 100644 index 00000000..c3ef1fe1 --- /dev/null +++ b/Sources/SolidityAnalysis/SolidityAnalyzer.cs @@ -0,0 +1,16 @@ +namespace SolidityAnalysis +{ + using System; + using System.Collections.Generic; + using SolidityAST; + + public class SolidityAnalyzer + { + public AliasAnalysis Alias { get; } + + public SolidityAnalyzer(AST solidityAST, HashSet> ignoredMethods, String entryPointContract = "") + { + Alias = new AliasAnalysis(solidityAST, ignoredMethods, entryPointContract); + } + } +} \ No newline at end of file diff --git a/Sources/VeriSol.sln b/Sources/VeriSol.sln index c5272132..f251cb1e 100644 --- a/Sources/VeriSol.sln +++ b/Sources/VeriSol.sln @@ -17,6 +17,8 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "VeriSol", "VeriSol\VeriSol. EndProject Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "ExternalToolsManager", "ExternalToolsManager\ExternalToolsManager.csproj", "{BF09262B-4902-4B54-8888-A9BDB65AF0D0}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SolidityAnalysis", "SolidityAnalysis\SolidityAnalysis.csproj", "{9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -111,6 +113,18 @@ Global {BF09262B-4902-4B54-8888-A9BDB65AF0D0}.Release|x64.Build.0 = Release|Any CPU {BF09262B-4902-4B54-8888-A9BDB65AF0D0}.Release|x86.ActiveCfg = Release|Any CPU {BF09262B-4902-4B54-8888-A9BDB65AF0D0}.Release|x86.Build.0 = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|Any CPU.Build.0 = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|x64.ActiveCfg = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|x64.Build.0 = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|x86.ActiveCfg = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Debug|x86.Build.0 = Debug|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|Any CPU.ActiveCfg = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|Any CPU.Build.0 = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|x64.ActiveCfg = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|x64.Build.0 = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|x86.ActiveCfg = Release|Any CPU + {9177A69B-7FDE-48DC-9A2C-22AAB5ED3768}.Release|x86.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Test/regressions/UnreachableAssertion.sol b/Test/regressions/UnreachableAssertion.sol new file mode 100644 index 00000000..edcdf138 --- /dev/null +++ b/Test/regressions/UnreachableAssertion.sol @@ -0,0 +1,20 @@ +pragma solidity ^0.5.0; + + +contract UnreachableAssertion { + address private owner; + + constructor() public { + owner = address(this); + require(owner != address(0)); + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function neverSuccessful() onlyOwner view public { + assert(false); + } +} diff --git a/resetInstall.sh b/resetInstall.sh new file mode 100644 index 00000000..343776da --- /dev/null +++ b/resetInstall.sh @@ -0,0 +1,5 @@ +dotnet tool uninstall --global VeriSol +dotnet tool uninstall --global SolToBoogieTest +dotnet build Sources/VeriSol.sln +dotnet tool install VeriSol --version 0.1.1-alpha --global --add-source ./nupkg/ +dotnet tool install --global SolToBoogieTest --version 0.1.1-alpha --add-source ./nupkg/ diff --git a/resetInstallwsl.sh b/resetInstallwsl.sh new file mode 100644 index 00000000..dcb03f32 --- /dev/null +++ b/resetInstallwsl.sh @@ -0,0 +1,5 @@ +dotnet.exe tool uninstall --global VeriSol +dotnet.exe tool uninstall --global SolToBoogieTest +dotnet.exe build Sources/VeriSol.sln +dotnet.exe tool install VeriSol --version 0.1.1-alpha --global --add-source $(wslpath -w ./nupkg/) +dotnet.exe tool install --global SolToBoogieTest --version 0.1.1-alpha --add-source $(wslpath -w ./nupkg/)