in ironclad-apps/tools/DafnyCC/CompileMethod.cs [1084:1183]
public void AddCall(List<RtlVar> destVars, bool isGhost, bool isHeap, List<Formal> ins, string name,
List<RtlVar> argVars, List<Expression> args, List<Formal> rets)
{
if (isGhost)
{
AddGhostCall(destVars, name, args, isHeap);
return;
}
Util.Assert(args.Count == ins.Count);
Util.Assert(args.Count == argVars.Count);
Util.Assert(rets != null || destVars.Count == 1);
List<RtlExp> rtlArgs = new List<RtlExp>();
int numIntRets = (rets == null) ? 1 : rets.Count(x => !x.IsGhost && !IsPtrType(AppType(x.Type)));
int numPtrRets = (rets == null) ? 1 : rets.Count(x => !x.IsGhost && IsPtrType(AppType(x.Type)));
int argIntIndex = numIntRets;
int argPtrIndex = numPtrRets;
List<RtlStmt> argStmts = new List<RtlStmt>();
for (int i = 0; i < args.Count; i++)
{
Util.Assert(argVars[i] != null || args[i] != null);
Util.Assert(argVars[i] == null || args[i] == null);
var arg = args[i];
var formal = ins[i];
RtlVar argVar = (argVars[i] != null) ? argVars[i] : AsVar(arg);
bool isPtr = IsPtrType((argVars[i] != null) ? argVars[i].type : AppType(arg.Type));
if (formal.IsGhost)
{
rtlArgs.Add(GhostExpression(arg));
}
else
{
if (argVar != null)
{
rtlArgs.Add(argVar);
}
else
{
RtlVar tmp = TempVar(args[i].Type);
AddExpression(tmp, args[i]);
rtlArgs.Add(tmp);
}
argStmts.Add(new RtlCallInOut(isPtr ? argPtrIndex : argIntIndex, false, rtlArgs[i])
.WithComment("push argument #" + i + " at index " + (isPtr ? argPtrIndex : argIntIndex)
+ " isPtr = " + isPtr + " argument = " + rtlArgs[i]));
if (isPtr)
{
argPtrIndex++;
}
else
{
argIntIndex++;
}
}
}
name = ProcName(isGhost, name);
if (name == procName)
{
throw new Exception("recursive calls not supported in non-ghost procedure: " + method.Name);
}
stmts.AddRange(argStmts);
calledMethods.Add(name);
stmts.Add(new RtlCall(name, destVars, rtlArgs, isGhost)
.WithComment("call:: " + String.Join(",", destVars) + " := " + name
+ "(" + String.Join(", ", rtlArgs.ToList()) + ") // isGhost = " + isGhost));
if (rets != null)
{
int retIntIndex = 0;
int retPtrIndex = 0;
Util.Assert(rets.Count == destVars.Count);
for (int i = 0; i < rets.Count; i++)
{
Util.Assert(destVars[i] == null || destVars[i].isGhost || !rets[i].IsGhost);
if (!rets[i].IsGhost)
{
RtlVar dest = destVars[i];
if (dest == null || dest.isGhost)
{
dest = TempVar(rets[i].Type);
}
bool isPtr = IsPtrType(AppType(rets[i].Type));
stmts.Add(new RtlCallInOut(isPtr ? retPtrIndex : retIntIndex, true, dest)
.WithComment("pop return value #" + i + " at index " + (isPtr ? retPtrIndex : retIntIndex)
+ " into destination " + destVars[i] + " isPtr = " + isPtr));
if (isPtr)
{
retPtrIndex++;
}
else
{
retIntIndex++;
}
}
}
}
else
{
stmts.Add(new RtlCallInOut(0, true, destVars[0])
.WithComment("pop single return value from function into destination:: " + destVars[0]));
}
}