From e299e8e41d86831e1fecf1c79a317bafb110499c Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Sat, 11 Apr 2020 01:59:56 -0700 Subject: [PATCH 1/2] first draft of locals in modifiers --- Sources/SolToBoogie/HarnessGenerator.cs | 2 +- Sources/SolToBoogie/ModifierCollector.cs | 40 ++++++++++++++++++---- Sources/SolToBoogie/ProcedureTranslator.cs | 29 ++++++++++++++-- Sources/SolToBoogie/TranslatorContext.cs | 16 +++++++++ Test/config/ModifierLocal.json | 6 ++++ Test/records.txt | 1 + Test/regressions/ModifierLocal.sol | 25 ++++++++++++++ 7 files changed, 109 insertions(+), 10 deletions(-) create mode 100644 Test/config/ModifierLocal.json create mode 100644 Test/regressions/ModifierLocal.sol diff --git a/Sources/SolToBoogie/HarnessGenerator.cs b/Sources/SolToBoogie/HarnessGenerator.cs index 47166c7b..a2710454 100644 --- a/Sources/SolToBoogie/HarnessGenerator.cs +++ b/Sources/SolToBoogie/HarnessGenerator.cs @@ -242,7 +242,7 @@ private BoogieStmtList GenerateHavocBlock(ContractDefinition contract, List postlude = new List(); + // this list does not include locals introduced during translation + List localVarsDeclared = new List(); + bool translatingPre = true; foreach (Statement statement in body.Statements) { - if (statement is VariableDeclarationStatement) + if (statement is VariableDeclarationStatement varDecls) { - throw new System.Exception("locals within modifiers not supported"); + foreach (VariableDeclaration varDecl in varDecls.Declarations) + { + string name = TransUtils.GetCanonicalLocalVariableName(varDecl, context); + BoogieType type = TransUtils.GetBoogieTypeFromSolidityTypeName(varDecl.TypeName); + // Issue a warning for intXX variables in case /useModularArithemtic option is used: + if (context.TranslateFlags.UseModularArithmetic && varDecl.TypeDescriptions.IsInt()) + { + Console.WriteLine($"Warning: signed integer arithmetic is not handled with /useModularArithmetic option"); + } + var boogieVariable = new BoogieLocalVariable(new BoogieTypedIdent(name, type)); + if (translatingPre) + localVarsDeclared.Add(boogieVariable); // don't add locals after placeholder + } + + // throw new System.Exception("locals within modifiers not supported"); } if (statement is PlaceholderStatement) { translatingPre = false; + // only capture those locals declared in the prefix, these are visible to postlude + context.AddPreludeLocalsToModifier(modifier.Name, localVarsDeclared); + continue; } if (translatingPre) @@ -63,11 +86,15 @@ public override bool Visit(ModifierDefinition modifier) } } + var attributes = new List(); + attributes.Add(new BoogieAttribute("inline", 1)); + if (hasPre) { - List inParams = modifierInParams; + List inParams = new List(modifierInParams); List outParams = new List(); - BoogieProcedure preludeProc = new BoogieProcedure(modifier.Name + "_pre", inParams, outParams); + outParams.AddRange(localVarsDeclared.Select(x => new BoogieFormalParam(new BoogieTypedIdent("__out_mod_" + x.Name, x.TypedIdent.Type)))); + BoogieProcedure preludeProc = new BoogieProcedure(modifier.Name + "_pre", inParams, outParams, attributes); context.AddModiferToPreProc(modifier.Name, preludeProc); BoogieImplementation preludeImpl = new BoogieImplementation(modifier.Name + "_pre", @@ -77,9 +104,10 @@ public override bool Visit(ModifierDefinition modifier) if (hasPost) { - List inParams = modifierInParams; + List inParams = new List(modifierInParams); + inParams.AddRange(localVarsDeclared); List outParams = new List(); - BoogieProcedure postludeProc = new BoogieProcedure(modifier.Name + "_post", inParams, outParams); + BoogieProcedure postludeProc = new BoogieProcedure(modifier.Name + "_post", inParams, outParams, attributes); context.AddModiferToPostProc(modifier.Name, postludeProc); BoogieImplementation postludeImpl = new BoogieImplementation(modifier.Name + "_post", diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs index a2a0db7d..d5cd1d1c 100644 --- a/Sources/SolToBoogie/ProcedureTranslator.cs +++ b/Sources/SolToBoogie/ProcedureTranslator.cs @@ -377,6 +377,15 @@ public override bool Visit(FunctionDefinition node) // if (node.Modifiers.Count == 1) for (int i = 0; i < node.Modifiers.Count; ++i) { + var outVars = new List(); + // local variables declared in the prelude of a modifier (before _ ) becomes out variables and then in parameters of postlude + foreach (var localVar in context.ModifierToPreludeLocalVars[node.Modifiers[i].ModifierName.ToString()]) + { + var outVar = new BoogieLocalVariable(new BoogieTypedIdent("__mod_out_" + localVar.Name, localVar.TypedIdent.Type)); + boogieToLocalVarsMap[currentBoogieProc].Add(outVar); + outVars.Add(new BoogieIdentifierExpr(outVar.Name)); + } + // insert call to modifier prelude if (context.ModifierToBoogiePreImpl.ContainsKey(node.Modifiers[i].ModifierName.Name)) { @@ -384,7 +393,7 @@ public override bool Visit(FunctionDefinition node) if (node.Modifiers[i].Arguments != null) arguments.AddRange(node.Modifiers[i].Arguments.ConvertAll(TranslateExpr)); string callee = node.Modifiers[i].ModifierName.ToString() + "_pre"; - var callCmd = new BoogieCallCmd(callee, arguments, null); + var callCmd = new BoogieCallCmd(callee, arguments, outVars); procBody.AddStatement(callCmd); } @@ -394,6 +403,7 @@ public override bool Visit(FunctionDefinition node) List arguments = TransUtils.GetDefaultArguments(); if (node.Modifiers[i].Arguments != null) arguments.AddRange(node.Modifiers[i].Arguments.ConvertAll(TranslateExpr)); + arguments.AddRange(outVars.Select(x => new BoogieIdentifierExpr(x.Name))); string callee = node.Modifiers[i].ModifierName.ToString() + "_post"; var callCmd = new BoogieCallCmd(callee, arguments, null); currentPostlude.AddStatement(callCmd); @@ -505,15 +515,23 @@ public override bool Visit(ModifierDefinition node) bool translatingPre = true; bool hasPre = false; bool hasPost = false; + foreach (Statement statement in body.Statements) { if (statement is VariableDeclarationStatement) { - VeriSolAssert(false, "locals within modifiers not supported"); + // VeriSolAssert(false, "locals within modifiers not supported"); } if (statement is PlaceholderStatement) { translatingPre = false; + // add __out_mod_x := x, for any local explicitly declared in the prelude + foreach(var localDeclared in context.ModifierToPreludeLocalVars[node.Name]) + { + var lhsExpr = new BoogieIdentifierExpr("__out_mod_" + localDeclared.Name); + var rhsExpr = new BoogieIdentifierExpr(localDeclared.Name); + prelude.AddStatement(new BoogieAssignCmd(lhsExpr, rhsExpr)); + } currentBoogieProc = node.Name + "_post"; boogieToLocalVarsMap[currentBoogieProc] = new List(); continue; @@ -530,9 +548,14 @@ public override bool Visit(ModifierDefinition node) hasPost = true; } } + + // we are going to make any locals declared in prelude visible to postlude by making htem as output variables + // and making them input to the postlude if (hasPre) { + // removig this removes local declaration of temporaries introduced in translation context.ModifierToBoogiePreImpl[node.Name].LocalVars = boogieToLocalVarsMap[node.Name + "_pre"]; + // context.ModifierToBoogiePreImpl[node.Name].LocalVars = new List(); context.ModifierToBoogiePreImpl[node.Name].StructuredStmts = prelude; } if (hasPost) @@ -1309,7 +1332,7 @@ public override bool Visit(VariableDeclarationStatement node) Console.WriteLine($"Warning: signed integer arithmetic is not handled with /useModularArithmetic option"); } var boogieVariable = new BoogieLocalVariable(new BoogieTypedIdent(name, type)); - boogieToLocalVarsMap[currentBoogieProc].Add(boogieVariable); + boogieToLocalVarsMap[currentBoogieProc].Add(boogieVariable); } // handle the initial value of variable declaration diff --git a/Sources/SolToBoogie/TranslatorContext.cs b/Sources/SolToBoogie/TranslatorContext.cs index 74b3a2e5..558fbdfa 100644 --- a/Sources/SolToBoogie/TranslatorContext.cs +++ b/Sources/SolToBoogie/TranslatorContext.cs @@ -89,6 +89,9 @@ public class TranslatorContext // M -> BoogieImplementation(B) for Modifier M {Stmt A; _; Stmt B} public Dictionary ModifierToBoogiePostImpl { get; private set;} + // M -> the set of local variables declared in the prelude (will become outputs to prelude call) + public Dictionary> ModifierToPreludeLocalVars { get; private set; } + public String EntryPointContract { get; private set; } // Options flags @@ -135,6 +138,7 @@ public TranslatorContext(HashSet> ignoreMethods, bool _gen ModifierToBoogiePostProc = new Dictionary(); ModifierToBoogiePreImpl = new Dictionary(); ModifierToBoogiePostImpl = new Dictionary(); + ModifierToPreludeLocalVars = new Dictionary>(); usingMap = new Dictionary>(); IgnoreMethods = ignoreMethods; genInlineAttrInBpl = _genInlineAttrInBpl; @@ -543,6 +547,18 @@ public void AddModiferToPostImpl(string modifier, BoogieImplementation procedure } } + public void AddPreludeLocalsToModifier(string modifier, List localVars) + { + if (ModifierToPreludeLocalVars.ContainsKey(modifier)) + { + throw new SystemException("duplicated modifier"); + } + else + { + ModifierToPreludeLocalVars[modifier] = localVars; + } + } + public bool IsMethodInIgnoredSet(FunctionDefinition func, ContractDefinition contract) { return IgnoreMethods.Any(x => x.Item2.Equals(contract.Name) && (x.Item1.Equals("*") || x.Item1.Equals(func.Name))) ; diff --git a/Test/config/ModifierLocal.json b/Test/config/ModifierLocal.json new file mode 100644 index 00000000..b46d9b37 --- /dev/null +++ b/Test/config/ModifierLocal.json @@ -0,0 +1,6 @@ +{ + "recursionBound": 8, + "k": 1, + "main": "CorralEntry_ReentrancyGuard", + "expectedResult": "Program has a potential bug: True bug" +} diff --git a/Test/records.txt b/Test/records.txt index 8a1bc21b..4e6cea9d 100644 --- a/Test/records.txt +++ b/Test/records.txt @@ -146,6 +146,7 @@ NestedArray.sol Modifier.sol ModifierPost.sol ModifierReturn.sol +ModifierLocal.sol NoConstructor.sol ReturnNamedParam.sol EmptyContract.sol diff --git a/Test/regressions/ModifierLocal.sol b/Test/regressions/ModifierLocal.sol new file mode 100644 index 00000000..0b576be1 --- /dev/null +++ b/Test/regressions/ModifierLocal.sol @@ -0,0 +1,25 @@ +pragma solidity ^0.5.0; + +contract ReentrancyGuard { + /// @dev counter to allow mutex lock with only one SSTORE operation + uint256 private _guardCounter; + + constructor () internal { + // The counter starts at one to prevent changing it from zero to a non-zero + // value, which is a more expensive operation. + _guardCounter = 1; + } + + function foo() public checkIncrement() { + _guardCounter += 1; + } + + modifier checkIncrement() { + uint256 localCounter = _guardCounter; + int x = 5; + _; + int y = 10; + assert(localCounter != _guardCounter - 1); // should fail + assert (x == y - 5); + } +} From 04e9b2d2da2ba4a64b1fc1e5c3e2a9722c50887a Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Sun, 12 Apr 2020 21:43:57 -0700 Subject: [PATCH 2/2] fix for crash --- Sources/SolToBoogie/ProcedureTranslator.cs | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs index d5cd1d1c..6bb1500a 100644 --- a/Sources/SolToBoogie/ProcedureTranslator.cs +++ b/Sources/SolToBoogie/ProcedureTranslator.cs @@ -378,17 +378,18 @@ public override bool Visit(FunctionDefinition node) for (int i = 0; i < node.Modifiers.Count; ++i) { var outVars = new List(); - // local variables declared in the prelude of a modifier (before _ ) becomes out variables and then in parameters of postlude - foreach (var localVar in context.ModifierToPreludeLocalVars[node.Modifiers[i].ModifierName.ToString()]) - { - var outVar = new BoogieLocalVariable(new BoogieTypedIdent("__mod_out_" + localVar.Name, localVar.TypedIdent.Type)); - boogieToLocalVarsMap[currentBoogieProc].Add(outVar); - outVars.Add(new BoogieIdentifierExpr(outVar.Name)); - } - + // insert call to modifier prelude if (context.ModifierToBoogiePreImpl.ContainsKey(node.Modifiers[i].ModifierName.Name)) { + // local variables declared in the prelude of a modifier (before _ ) becomes out variables and then in parameters of postlude + foreach (var localVar in context.ModifierToPreludeLocalVars[node.Modifiers[i].ModifierName.ToString()]) + { + var outVar = new BoogieLocalVariable(new BoogieTypedIdent("__mod_out_" + localVar.Name, localVar.TypedIdent.Type)); + boogieToLocalVarsMap[currentBoogieProc].Add(outVar); + outVars.Add(new BoogieIdentifierExpr(outVar.Name)); + } + List arguments = TransUtils.GetDefaultArguments(); if (node.Modifiers[i].Arguments != null) arguments.AddRange(node.Modifiers[i].Arguments.ConvertAll(TranslateExpr));