in Sources/SolToBoogie/ProcedureTranslator.cs [277:490]
public override bool Visit(FunctionDefinition node)
{
preTranslationAction(node);
// VeriSolAssert(node.IsConstructor || node.Modifiers.Count <= 1, "Multiple Modifiers are not supported yet");
VeriSolAssert(currentContract != null);
currentFunction = node;
// procedure name
string procName = node.Name + "_" + currentContract.Name;
if (node.IsConstructor)
{
procName += "_NoBaseCtor";
}
currentBoogieProc = procName;
// input parameters
List<BoogieVariable> inParams = TransUtils.GetDefaultInParams();
// initialize statement list to include assumption about parameter types
currentStmtList = new BoogieStmtList();
// get all formal input parameters
node.Parameters.Accept(this);
inParams.AddRange(currentParamList);
// Print function argument values to corral.txt for counterexample:
PrintArguments(node, inParams, currentStmtList);
// output parameters
isReturnParameterList = true;
node.ReturnParameters.Accept(this);
isReturnParameterList = false;
List<BoogieVariable> outParams = currentParamList;
var assumesForParamsAndReturn = currentStmtList;
currentStmtList = new BoogieStmtList();
// attributes
List<BoogieAttribute> attributes = new List<BoogieAttribute>();
if ((node.Visibility == EnumVisibility.PUBLIC || node.Visibility == EnumVisibility.EXTERNAL)
&& !node.IsConstructor
&& !node.IsFallback) //don't expose fallback for calling directly
{
attributes.Add(new BoogieAttribute("public"));
}
// generate inline attribute for a function only when /noInlineAttrs is specified
if (genInlineAttrsInBpl)
attributes.Add(new BoogieAttribute("inline", 1));
if (currentContract.ContractKind == EnumContractKind.LIBRARY &&
currentContract.Name.Equals("VeriSol"))
{
return false;
}
// we add any pre/post conditions after analyzing the boy later
BoogieProcedure procedure = new BoogieProcedure(procName, inParams, outParams, attributes);
context.Program.AddDeclaration(procedure);
// could be just a declaration
if (!node.Implemented)
{
return false;
}
// skip if it in ignored set
if (context.IsMethodInIgnoredSet(node, currentContract))
{
Console.WriteLine($"Warning!: Ignoring method {node.Name} in contract {currentContract.Name} specified using /ignoreMethod:");
}
else
{
// local variables and function body
// TODO: move to earlier
boogieToLocalVarsMap[currentBoogieProc] = new List<BoogieVariable>();
// TODO: each local array variable should be distinct and 0 initialized
BoogieStmtList procBody = new BoogieStmtList();
currentPostlude = new BoogieStmtList();
// Add possible assume statements from parameters
procBody.AppendStmtList(assumesForParamsAndReturn);
// if payable, then modify the balance
if (node.StateMutability == EnumStateMutability.PAYABLE)
{
procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function START "));
var balnSender = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("msgsender_MSG"));
var balnThis = new BoogieMapSelect(new BoogieIdentifierExpr("Balance"), new BoogieIdentifierExpr("this"));
var msgVal = new BoogieIdentifierExpr("msgvalue_MSG");
//assume Balance[msg.sender] >= msg.value
procBody.AddStatement(new BoogieAssumeCmd(new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, balnSender, msgVal)));
//balance[msg.sender] = balance[msg.sender] - msg.value
procBody.AddStatement(new BoogieAssignCmd(balnSender, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, balnSender, msgVal)));
//balance[this] = balance[this] + msg.value
procBody.AddStatement(new BoogieAssignCmd(balnThis, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.ADD, balnThis, msgVal)));
procBody.AddStatement(new BoogieCommentCmd("---- Logic for payable function END "));
}
// 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, outVars);
procBody.AddStatement(callCmd);
}
// insert call to modifier postlude
if (context.ModifierToBoogiePostImpl.ContainsKey(node.Modifiers[i].ModifierName.Name))
{
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);
}
}
try
{
procBody.AppendStmtList(TranslateStatement(node.Body));
}
catch (NotImplementedException e)
{
// In case of an inline assembly in the body of the function, do not emit procedure body (aka implementation):
if (e.Message.Equals("inline assembly"))
{
inlineAssemblyPresent = true;
}
else
{
throw e;
}
}
// add modifier postlude call if function body has no return
if (currentPostlude != null)
{
procBody.AppendStmtList(currentPostlude);
currentPostlude = null;
}
// initialization statements
if (node.IsConstructor)
{
BoogieStmtList oldCurrentStmtList = currentStmtList;
currentStmtList = new BoogieStmtList();
BoogieStmtList initStmts;
GenerateInitializationStmts(currentContract);
initStmts = currentStmtList;
currentStmtList = oldCurrentStmtList;
initStmts.AppendStmtList(procBody);
procBody = initStmts;
}
// is it a VeriSol Contract Invariant function?
List<BoogieExpr> contractInvs = null;
if (IsVeriSolContractInvariantFunction(node, procBody, out contractInvs))
{
//add contract invs as loop invariants to outer loop
VeriSolAssert(!contractInvariants.ContainsKey(currentContract.Name), $"More than one function defining the contract invariant for contract {currentContract.Name}");
contractInvariants[currentContract.Name] = contractInvs;
}
else
{
//extract the specifications from within the body
BoogieStmtList procBodyWoRequires, procBodyWoEnsures, procBodyWoModifies;
var preconditions = ExtractSpecifications("Requires_VeriSol", procBody, out procBodyWoRequires);
var postconditions = ExtractSpecifications("Ensures_VeriSol", procBodyWoRequires, out procBodyWoEnsures);
var modifies = ExtractSpecifications("Modifies_VeriSol", procBodyWoEnsures, out procBodyWoModifies);
procedure.AddPreConditions(preconditions);
procedure.AddPostConditions(postconditions);
procedure.AddPostConditions(modifies);
List<BoogieVariable> localVars = boogieToLocalVarsMap[currentBoogieProc];
if (!inlineAssemblyPresent)
{
BoogieImplementation impelementation = new BoogieImplementation(procName, inParams, outParams, localVars, procBodyWoModifies);
context.Program.AddDeclaration(impelementation);
}
else
{
inlineAssemblyPresent = false;
}
}
}
// generate real constructors
if (node.IsConstructor)
{
GenerateConstructorWithBaseCalls(node, inParams);
}
return false;
}