[BUG] The function **TranslateCallStatement** may cause Null Pointer Exception.

[BigGan]

Problem

I found that VERISOL will throw an exception "VeriSol translation error: Object reference not set to an instance of an object." when my solidity code contain the to.call.value(amount)("");.

Cause

In the function TranslateCallStatement (Sources/SolToBoogie/ProcedureTranslator.cs), the parameter outParams may be null. However, This code BoogieIdentifierExpr tmpVarExpr = outParams[0]; will call directly outParams[0] without judging whether the outParams is null.

private void TranslateCallStatement(FunctionCall node, List<BoogieIdentifierExpr> outParams = null)
{
    VeriSolAssert(outParams == null || outParams.Count == 2, "Number of outPArams for call statement should be 2");
    // only handle call.value(x).gas(y)("") 
    var arg0 = node.Arguments[0].ToString();
    if (!string.IsNullOrEmpty(arg0) && !arg0.Equals("\'\'"))
    {
        currentStmtList.AddStatement(new BoogieSkipCmd(node.ToString()));
        VeriSolAssert(false, "low-level call statements with non-empty signature not implemented..");
    }

    // almost identical to send(amount)
    BoogieIdentifierExpr tmpVarExpr = outParams[0]; //bool part of the tuple
    if (tmpVarExpr == null)
    {
        tmpVarExpr = MkNewLocalVariableWithType(BoogieType.Bool);
    }

    var amountExpr = node.MsgValue != null ? TranslateExpr(node.MsgValue) : new BoogieLiteralExpr(BigInteger.Zero);
    TranslateSendCallStmt(node, tmpVarExpr, amountExpr, true);
    currentExpr = tmpVarExpr;
}

So, before the BoogieIdentifierExpr tmpVarExpr = outParams[0];, we need to judge wether outParams is null. The Fixed code as follow:

private void TranslateCallStatement(FunctionCall node, List<BoogieIdentifierExpr> outParams = null)
{
    VeriSolAssert(outParams == null || outParams.Count == 2, "Number of outPArams for call statement should be 2");
    // only handle call.value(x).gas(y)("") 
    var arg0 = node.Arguments[0].ToString();
    if (!string.IsNullOrEmpty(arg0) && !arg0.Equals("\'\'"))
    {
        currentStmtList.AddStatement(new BoogieSkipCmd(node.ToString()));
        VeriSolAssert(false, "low-level call statements with non-empty signature not implemented..");
    }

    BoogieIdentifierExpr tmpVarExpr;
    if (null == outParams)
     {
         tmpVarExpr = MkNewLocalVariableWithType(BoogieType.Bool);
     }
    else
    {
        // almost identical to send(amount)
        tmpVarExpr = outParams[0]; //bool part of the tuple
        if (null == tmpVarExpr)
        {
            tmpVarExpr = MkNewLocalVariableWithType(BoogieType.Bool);
        }
    }

    var amountExpr = node.MsgValue != null ? TranslateExpr(node.MsgValue) : new BoogieLiteralExpr(BigInteger.Zero);
    TranslateSendCallStmt(node, tmpVarExpr, amountExpr, true);
    currentExpr = tmpVarExpr;
}

[shuvendu-lahiri]

Thanks. Can you please create a Pull Request with the test case that causes the null dereference and the fix?

[BigGan]

Thanks. Can you please create a Pull Request with the test case that causes the null dereference and the fix?

OK. I have committed a new Pull Request !