in Sources/SolToBoogie/ProcedureTranslator.cs [1456:1629]
public override bool Visit(Assignment node)
{
preTranslationAction(node);
List<BoogieExpr> lhs = new List<BoogieExpr>();
List<BoogieType> lhsTypes = new List<BoogieType>(); //stores types in case of tuples
List<Expression> lhsExprs;
bool isTupleAssignment = false;
if (node.LeftHandSide is TupleExpression tuple)
{
// we only handle the case (e1, e2, .., _, _) = funcCall(...)
lhs.AddRange(tuple.Components.ConvertAll(x => TranslateExpr(x)));
isTupleAssignment = true;
lhsTypes.AddRange(tuple.Components.ConvertAll(x => MapArrayHelper.InferExprTypeFromTypeString(x.TypeDescriptions.TypeString)));
lhsExprs = tuple.Components;
}
else
{
lhs.Add(TranslateExpr(node.LeftHandSide));
lhsExprs = new List<Expression>();
lhsExprs.Add(node.LeftHandSide);
}
// TODO: this part should go into Translate a function call expression
if (node.RightHandSide is FunctionCall funcCall)
{
// if lhs is not an identifier (e.g. a[i]), then
// we have to introduce a temporary
// we do it even when lhs is identifier to keep translation simple
var tmpVars = new List<BoogieIdentifierExpr>();
var oldStmtList = currentStmtList;
currentStmtList = new BoogieStmtList();
if (!isTupleAssignment) {
tmpVars.Add(lhs[0] is BoogieIdentifierExpr ? lhs[0] as BoogieIdentifierExpr : MkNewLocalVariableForFunctionReturn(funcCall));
} else {
// always use temporaries for tuples regardless if lhs[i] is an identifier
tmpVars.AddRange(lhsTypes.ConvertAll(x => MkNewLocalVariableWithType(x)));
}
var tmpVariableAssumes = currentStmtList;
currentStmtList = oldStmtList;
// a Boolean to decide is we needed to use tmpVar
bool usedTmpVar = true;
if (IsContractConstructor(funcCall))
{
VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Constructors");
TranslateNewStatement(funcCall, tmpVars[0]);
}
else if (IsStructConstructor(funcCall))
{
VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Constructors");
TranslateStructConstructor(funcCall, tmpVars[0]);
}
else if (IsKeccakFunc(funcCall))
{
VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for Keccak256");
TranslateKeccakFuncCall(funcCall, lhs[0]); //this is not a procedure call in Boogie
usedTmpVar = false;
}
else if (IsAbiEncodePackedFunc(funcCall))
{
TranslateAbiEncodedFuncCall(funcCall, tmpVars[0]); //this is not a procedure call in Boogie
VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for abi.encodePacked");
usedTmpVar = false;
}
else if (IsTypeCast(funcCall))
{
// assume the type cast is used as: obj = C(var);
VeriSolAssert(!isTupleAssignment, "Not expecting a tuple for type cast");
bool isElementaryCast; //not used at this site
TranslateTypeCast(funcCall, tmpVars[0], out isElementaryCast); //this is not a procedure call in Boogie
usedTmpVar = false;
}
else // normal function calls
{
VeriSolAssert(tmpVars is List<BoogieIdentifierExpr>, $"tmpVar has to be a list of Boogie identifiers: {tmpVars}");
TranslateFunctionCalls(funcCall, tmpVars);
}
if (context.TranslateFlags.InstrumentSums)
{
updateAssignedSums(BoogieBinaryOperation.Opcode.SUB, lhsExprs, lhs);
}
if (!isTupleAssignment)
{
if (usedTmpVar || !(lhs[0] is BoogieIdentifierExpr)) //bad bug: was && before!!
currentStmtList.AddStatement(new BoogieAssignCmd(lhs[0], tmpVars[0]));
} else
{
for (int i = 0; i < lhs.Count; ++i)
{
currentStmtList.AddStatement(new BoogieAssignCmd(lhs[i], tmpVars[i]));
}
}
if (context.TranslateFlags.InstrumentSums)
{
updateAssignedSums(BoogieBinaryOperation.Opcode.ADD, lhsExprs, lhs);
}
foreach(var block in tmpVariableAssumes.BigBlocks)
{
foreach(var stmt in block.SimpleCmds)
currentStmtList.AddStatement(stmt);
}
}
else
{
if (isTupleAssignment)
VeriSolAssert(false, "Not implemented...currently only support assignment of tuples as returns of a function call");
BoogieExpr rhs = TranslateExpr(node.RightHandSide);
BoogieStmtList stmtList = new BoogieStmtList();
BoogieExpr assignedExpr = new BoogieExpr();
switch (node.Operator)
{
case "=":
stmtList.AddStatement(new BoogieAssignCmd(lhs[0], rhs));
break;
case "+=":
assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, lhs[0], rhs);
assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions);
stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr));
break;
case "-=":
assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, lhs[0], rhs);
assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions);
stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr));
break;
case "*=":
assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.MUL, lhs[0], rhs);
assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions);
stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr));
break;
case "/=":
assignedExpr = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.DIV, lhs[0], rhs);
assignedExpr = AddModuloOp(node.LeftHandSide, assignedExpr, node.LeftHandSide.TypeDescriptions);
stmtList.AddStatement(new BoogieAssignCmd(lhs[0], assignedExpr));
break;
default:
VeriSolAssert(false, $"Unknown assignment operator: {node.Operator}");
break;
}
if (context.TranslateFlags.InstrumentSums)
{
updateAssignedSums(BoogieBinaryOperation.Opcode.SUB, lhsExprs, lhs);
}
currentStmtList.AppendStmtList(stmtList);
if (context.TranslateFlags.InstrumentSums)
{
updateAssignedSums(BoogieBinaryOperation.Opcode.ADD, lhsExprs, lhs);
}
}
var lhsType = node.LeftHandSide.TypeDescriptions != null ?
node.LeftHandSide.TypeDescriptions :
(node.RightHandSide.TypeDescriptions != null ?
node.RightHandSide.TypeDescriptions : null);
if (lhsType != null && !isTupleAssignment)
{
var callCmd = InstrumentForPrintingData(lhsType, lhs[0], node.LeftHandSide.ToString());
if (callCmd != null)
{
currentStmtList.AddStatement(callCmd);
}
}
return false;
}