From 5e891663fb9b05c0eb2a98caa3a2dc33e826ee9b Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Mon, 13 Apr 2020 01:00:57 -0700 Subject: [PATCH] example and fix for #195 --- Sources/SolToBoogie/ProcedureTranslator.cs | 104 ++++++++++++--------- Test/config/ArrayAlloc.json | 6 ++ Test/records.txt | 1 + Test/regressions/ArrayAlloc.sol | 18 ++++ 4 files changed, 85 insertions(+), 44 deletions(-) create mode 100644 Test/config/ArrayAlloc.json create mode 100644 Test/regressions/ArrayAlloc.sol diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs index 6bb1500a..d456df19 100644 --- a/Sources/SolToBoogie/ProcedureTranslator.cs +++ b/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(), + new List() {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(), - new List() { 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 inputs = new List() - { - 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(), + new List() { tmpVarIdentExpr } + )); + + // call constructor of A with this = tmp, msg.sender = this, msg.value = tmpMsgValue, args + string callee = TransUtils.GetCanonicalConstructorName(contract); + List inputs = new List() { + 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 outputs = new List(); + 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 outputs = new List(); - currentStmtList.AddStatement(new BoogieCallCmd(callee, inputs, outputs)); - // lhs := tmp; - currentStmtList.AddStatement(new BoogieAssignCmd(lhs, tmpVarIdentExpr)); - return; } private void TranslateStructConstructor(FunctionCall node, BoogieExpr lhs) diff --git a/Test/config/ArrayAlloc.json b/Test/config/ArrayAlloc.json new file mode 100644 index 00000000..aaa8b4b6 --- /dev/null +++ b/Test/config/ArrayAlloc.json @@ -0,0 +1,6 @@ +{ + "recursionBound": 8, + "k": 1, + "main": "CorralEntry_A", + "expectedResult": "Program has no bugs" +} diff --git a/Test/records.txt b/Test/records.txt index 4e6cea9d..01341b36 100644 --- a/Test/records.txt +++ b/Test/records.txt @@ -84,6 +84,7 @@ EnumParam.sol #StructOfMapping.sol InputParameters.sol #ArrayAlias.sol +ArrayAlloc.sol #LoopNestedWhile.sol #ArrayLowerDimRef.sol OutputParameters.sol diff --git a/Test/regressions/ArrayAlloc.sol b/Test/regressions/ArrayAlloc.sol new file mode 100644 index 00000000..5f8b5699 --- /dev/null +++ b/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); + } + + +}