Merge pull request #254 from microsoft/shuvendu-bugfixes

example and fix for #195

Sources/SolToBoogie/ProcedureTranslator.cs

@@ -2768,61 +2768,77 @@ private void TranslateNewStatement(FunctionCall node, BoogieExpr lhs)
         {
             VeriSolAssert(node.Expression is NewExpression);
             NewExpression newExpr = node.Expression as NewExpression;
-            VeriSolAssert(newExpr.TypeName is UserDefinedTypeName);
-            UserDefinedTypeName udt = newExpr.TypeName as UserDefinedTypeName;
-
-            ContractDefinition contract = context.GetASTNodeById(udt.ReferencedDeclaration) as ContractDefinition;
-            VeriSolAssert(contract != null);
 
             // define a local variable to temporarily hold the object
+            // even though we don't need a temp in some branches, the caller expects a 
             BoogieTypedIdent freshAllocTmpId = context.MakeFreshTypedIdent(BoogieType.Ref);
             BoogieLocalVariable allocTmpVar = new BoogieLocalVariable(freshAllocTmpId);
             boogieToLocalVarsMap[currentBoogieProc].Add(allocTmpVar);
+            BoogieIdentifierExpr tmpVarIdentExpr = new BoogieIdentifierExpr(freshAllocTmpId.Name);
 
-            // define a local variable to store the new msg.value
-            BoogieTypedIdent freshMsgValueId = context.MakeFreshTypedIdent(BoogieType.Int);
-            BoogieLocalVariable msgValueVar = new BoogieLocalVariable(freshMsgValueId);
-            boogieToLocalVarsMap[currentBoogieProc].Add(msgValueVar);
+            if (newExpr.TypeDescriptions.IsArray())
+            {
+                // lhs = new A[](5);
 
-            BoogieIdentifierExpr tmpVarIdentExpr = new BoogieIdentifierExpr(freshAllocTmpId.Name);
-            BoogieIdentifierExpr msgValueIdentExpr = new BoogieIdentifierExpr(freshMsgValueId.Name);
-            BoogieIdentifierExpr allocIdentExpr = new BoogieIdentifierExpr("Alloc");
+                // call tmp := FreshRefGenerator();
+                currentStmtList.AddStatement(
+                    new BoogieCallCmd(
+                        "FreshRefGenerator",
+                        new List<BoogieExpr>(),
+                        new List<BoogieIdentifierExpr>() {tmpVarIdentExpr}
+                        ));
+                // length[tmp] = 5
+                currentStmtList.AddStatement(
+                    new BoogieAssignCmd(
+                        new BoogieMapSelect(new BoogieIdentifierExpr("Length"), tmpVarIdentExpr), 
+                        TranslateExpr(node.Arguments[0])
+                        )
+                    );
+                // lhs := tmp;
+                currentStmtList.AddStatement(new BoogieAssignCmd(lhs, tmpVarIdentExpr));
+            }
+            else if (newExpr.TypeName is UserDefinedTypeName udt)
+            {
+                //VeriSolAssert(newExpr.TypeName is UserDefinedTypeName);
+                //UserDefinedTypeName udt = newExpr.TypeName as UserDefinedTypeName;
 
-            // suppose the statement is lhs := new A(args);
+                ContractDefinition contract = context.GetASTNodeById(udt.ReferencedDeclaration) as ContractDefinition;
+                VeriSolAssert(contract != null);
 
-            // call tmp := FreshRefGenerator();
-            currentStmtList.AddStatement(
-                new BoogieCallCmd(
-                    "FreshRefGenerator",
-                    new List<BoogieExpr>(),
-                    new List<BoogieIdentifierExpr>() { tmpVarIdentExpr }
-                    ));
+                // suppose the statement is lhs := new A(args);
 
-            // call constructor of A with this = tmp, msg.sender = this, msg.value = tmpMsgValue, args
-            string callee = TransUtils.GetCanonicalConstructorName(contract);
-            List<BoogieExpr> inputs = new List<BoogieExpr>()
-            {
-                tmpVarIdentExpr,
-                new BoogieIdentifierExpr("this"),
-                new BoogieLiteralExpr(BigInteger.Zero)//assuming msg.value is 0 for new
-            };
-            foreach (Expression arg in node.Arguments)
-            {
-                BoogieExpr argument = TranslateExpr(arg);
-                inputs.Add(argument);
+                // call tmp := FreshRefGenerator();
+                currentStmtList.AddStatement(
+                    new BoogieCallCmd(
+                        "FreshRefGenerator",
+                        new List<BoogieExpr>(),
+                        new List<BoogieIdentifierExpr>() { tmpVarIdentExpr }
+                        ));
+
+                // call constructor of A with this = tmp, msg.sender = this, msg.value = tmpMsgValue, args
+                string callee = TransUtils.GetCanonicalConstructorName(contract);
+                List<BoogieExpr> inputs = new List<BoogieExpr>() {
+                   tmpVarIdentExpr,
+                   new BoogieIdentifierExpr("this"),
+                   new BoogieLiteralExpr(BigInteger.Zero)//assuming msg.value is 0 for new
+                };
+                foreach (Expression arg in node.Arguments)
+                {
+                    BoogieExpr argument = TranslateExpr(arg);
+                    inputs.Add(argument);
+                }
+                // assume DType[tmp] == A
+                BoogieMapSelect dtypeMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("DType"), tmpVarIdentExpr);
+                BoogieIdentifierExpr contractIdent = new BoogieIdentifierExpr(contract.Name);
+                BoogieExpr dtypeAssumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, dtypeMapSelect, contractIdent);
+                currentStmtList.AddStatement(new BoogieAssumeCmd(dtypeAssumeExpr));
+                // The assume DType[tmp] == A is before the call as the constructor may do a dynamic 
+                // dispatch and the DType[tmp] is unconstrained before the call
+                List<BoogieIdentifierExpr> outputs = new List<BoogieIdentifierExpr>();
+                currentStmtList.AddStatement(new BoogieCallCmd(callee, inputs, outputs));
+                // lhs := tmp;
+                currentStmtList.AddStatement(new BoogieAssignCmd(lhs, tmpVarIdentExpr));
             }
-            // assume DType[tmp] == A
-            BoogieMapSelect dtypeMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("DType"), tmpVarIdentExpr);
-            BoogieIdentifierExpr contractIdent = new BoogieIdentifierExpr(contract.Name);
-            BoogieExpr dtypeAssumeExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, dtypeMapSelect, contractIdent);
-            currentStmtList.AddStatement(new BoogieAssumeCmd(dtypeAssumeExpr));
-            // The assume DType[tmp] == A is before the call as the constructor may do a dynamic 
-            // dispatch and the DType[tmp] is unconstrained before the call
-            List<BoogieIdentifierExpr> outputs = new List<BoogieIdentifierExpr>();
-            currentStmtList.AddStatement(new BoogieCallCmd(callee, inputs, outputs));
-            // lhs := tmp;
-            currentStmtList.AddStatement(new BoogieAssignCmd(lhs, tmpVarIdentExpr));
-            return;
         }
 
         private void TranslateStructConstructor(FunctionCall node, BoogieExpr lhs)

Test/config/ArrayAlloc.json

@@ -0,0 +1,6 @@
+{
+    "recursionBound": 8,
+    "k": 1,
+    "main": "CorralEntry_A",
+    "expectedResult": "Program has no bugs"
+}

Test/records.txt

@@ -84,6 +84,7 @@ EnumParam.sol
 #StructOfMapping.sol
 InputParameters.sol
 #ArrayAlias.sol
+ArrayAlloc.sol
 #LoopNestedWhile.sol
 #ArrayLowerDimRef.sol
 OutputParameters.sol

Test/regressions/ArrayAlloc.sol

@@ -0,0 +1,18 @@
+// Example with allocation for arrays
+
+pragma solidity >=0.4.24 <0.6.0;
+
+contract A {
+
+     mapping (address => uint256[]) private lockTime;
+
+     function Foo() public {
+        uint256[] memory tempLockTime = new uint256[](50);
+	for (uint i = 0; i < 50; ++i) {
+	      tempLockTime[i] = lockTime[address(9)][i] + 44;
+	}
+        assert(tempLockTime.length == 50);
+     }
+
+
+}