Merge pull request #253 from microsoft/shuvendu-tokens

first draft of locals in modifiers #248

Sources/SolToBoogie/HarnessGenerator.cs

@@ -242,7 +242,7 @@ private BoogieStmtList GenerateHavocBlock(ContractDefinition contract, List<Boog
             }
 
             stmtList.AddStatement((new BoogieAssignCmd(new BoogieMapSelect(new BoogieIdentifierExpr("Alloc"), new BoogieIdentifierExpr("msgsender_MSG")), new BoogieLiteralExpr(true))));
-            
+
             return stmtList;
         }
 

Sources/SolToBoogie/ModifierCollector.cs

@@ -5,6 +5,9 @@ namespace SolToBoogie
     using SolidityAST;
     using BoogieAST;
     using System.Collections.Generic;
+    using System;
+    using System.Security.Cryptography.X509Certificates;
+    using System.Linq;
 
     /**
      * Collect all modifier definitions and put them in the translator context.
@@ -41,16 +44,36 @@ public override bool Visit(ModifierDefinition modifier)
             bool hasPost = false;
             List<Statement> postlude = new List<Statement>();
 
+            // this list does not include locals introduced during translation
+            List<BoogieLocalVariable> localVarsDeclared = new List<BoogieLocalVariable>();
+
             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<BoogieAttribute>();
+            attributes.Add(new BoogieAttribute("inline", 1));
+
             if (hasPre)
             {
-                List<BoogieVariable> inParams = modifierInParams;
+                List<BoogieVariable> inParams = new List<BoogieVariable>(modifierInParams);
                 List<BoogieVariable> outParams = new List<BoogieVariable>();
-                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<BoogieVariable> inParams = modifierInParams;
+                List<BoogieVariable> inParams = new List<BoogieVariable>(modifierInParams);
+                inParams.AddRange(localVarsDeclared);
                 List<BoogieVariable> outParams = new List<BoogieVariable>();
-                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",

Sources/SolToBoogie/ProcedureTranslator.cs

@@ -377,14 +377,24 @@ public override bool Visit(FunctionDefinition node)
                 // if (node.Modifiers.Count == 1)
                 for (int i = 0; i < node.Modifiers.Count; ++i)
                 {
+                    var outVars = new List<BoogieIdentifierExpr>();
+
                     // 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<BoogieExpr> arguments = TransUtils.GetDefaultArguments();
                         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 +404,7 @@ public override bool Visit(FunctionDefinition node)
                         List<BoogieExpr> 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 +516,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<BoogieVariable>();
                     continue;
@@ -530,9 +549,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<BoogieVariable>();
                 context.ModifierToBoogiePreImpl[node.Name].StructuredStmts = prelude;
             }
             if (hasPost)
@@ -1309,7 +1333,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

Sources/SolToBoogie/TranslatorContext.cs

@@ -89,6 +89,9 @@ public class TranslatorContext
         // M -> BoogieImplementation(B) for Modifier M {Stmt A; _; Stmt B}
         public Dictionary<string, BoogieImplementation> ModifierToBoogiePostImpl { get; private set;}
 
+        // M -> the set of local variables declared in the prelude (will become outputs to prelude call)
+        public Dictionary<string, List<BoogieLocalVariable>> ModifierToPreludeLocalVars { get; private set; }
+
         public String EntryPointContract { get; private set; }
 
         // Options flags
@@ -135,6 +138,7 @@ public TranslatorContext(HashSet<Tuple<string, string>> ignoreMethods, bool _gen
             ModifierToBoogiePostProc = new Dictionary<string, BoogieProcedure>();
             ModifierToBoogiePreImpl = new Dictionary<string, BoogieImplementation>();
             ModifierToBoogiePostImpl = new Dictionary<string, BoogieImplementation>();
+            ModifierToPreludeLocalVars = new Dictionary<string, List<BoogieLocalVariable>>();
             usingMap = new Dictionary<ContractDefinition, Dictionary<UserDefinedTypeName, TypeName>>();
             IgnoreMethods = ignoreMethods;
             genInlineAttrInBpl = _genInlineAttrInBpl;
@@ -543,6 +547,18 @@ public void AddModiferToPostImpl(string modifier, BoogieImplementation procedure
             }
         }
 
+        public void AddPreludeLocalsToModifier(string modifier, List<BoogieLocalVariable> 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))) ;

Test/config/ModifierLocal.json

@@ -0,0 +1,6 @@
+{
+    "recursionBound": 8,
+    "k": 1,
+    "main": "CorralEntry_ReentrancyGuard",
+    "expectedResult": "Program has a potential bug: True bug"
+}

Test/records.txt

@@ -146,6 +146,7 @@ NestedArray.sol
 Modifier.sol
 ModifierPost.sol
 ModifierReturn.sol
+ModifierLocal.sol
 NoConstructor.sol
 ReturnNamedParam.sol
 EmptyContract.sol

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); 
+    }    
+}