public void AddCall()

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]));
        }
    }