public void CompileInstruction()

in ironclad-apps/tools/DafnyCC/CompileMethod.cs [1522:1652]
125 lines of code
27 McCabe index (conditional complexity)

    public void CompileInstruction()
    {
        string name = GhostProcName(DafnySpec.SimpleSanitizedName(method));
        bool strictOperands = Attributes.Contains(method.Attributes, "strict_operands");
        List<RtlExp> reqs = method.Req.ConvertAll(a => GhostExpression(a.E, false, false, a.Attributes)); 
        List<RtlExp> enss = method.Ens.ConvertAll(a => GhostExpression(a.E, false, false, a.Attributes));
        AddTypeWellFormed(reqs, method.Ins);
        AddTypeWellFormed(enss, method.Outs);

        List<Tuple<string,string>> operands = InstructionAttributes(method.Attributes);
        List<Tuple<Formal,string>> ins = new List<Tuple<Formal,string>>();
        List<Tuple<Formal,string>> outs = new List<Tuple<Formal,string>>();

        int kIn = 0, kOut = 0;
        List<string> parms = new List<string>();
        List<string> args = new List<string>();
        Func<string,string> opnName = s => "$opn_" + DafnySpec.CleanName(s);
        string outRegs = "";
        List<string> opnReqs = new List<string>();
        List<string> allPins = operands.ConvertAll(p => p.Item2).Where(p => p != null).ToList();
        foreach (var r in operands)
        {
            string arg;
            Action<string,Func<string,string>> opnReq = (a, f) =>
            {
                if (r.Item2 != null) { opnReqs.Add(a + " == " + f(r.Item2)); }
                else if (allPins.Count > 0) { opnReqs.Add(String.Join(" && ", allPins.Select(pin => a + " != " + f(pin)))); }
            };
            switch (r.Item1)
            {
                case "in":
                    arg = opnName(method.Ins[kIn].Name);
                    parms.Add(arg + ":opn");
                    opnReq(arg, s => "OReg(" + s + ")");
                    ins.Add(Tuple.Create(method.Ins[kIn], "Eval(r_old, " + arg + ")"));
                    kIn++;
                    break;
                case "inout":
                    arg = opnName(method.Ins[kIn].Name);
                    parms.Add(arg + ":int");
                    opnReq(arg, s => s);
                    ins.Add(Tuple.Create(method.Ins[kIn], "r_old.regs[" + arg + "]"));
                    kIn++;
                    outs.Add(Tuple.Create(method.Outs[kOut], "r.regs[" + arg + "]"));
                    outRegs += "[" + arg + " := " + GhostVar(method.Outs[kOut].Name) + "]";
                    kOut++;
                    break;
                case "out":
                    arg = opnName(method.Outs[kOut].Name);
                    parms.Add(arg + ":int");
                    opnReq(arg, s => s);
                    outs.Add(Tuple.Create(method.Outs[kOut], "r.regs[" + arg + "]"));
                    outRegs += "[" + arg + " := " + GhostVar(method.Outs[kOut].Name) + "]";
                    kOut++;
                    break;
                case "mem":
                    arg = opnName(method.Ins[kIn].Name);
                    parms.Add(arg + ":opn_mem");
                    ins.Add(Tuple.Create(method.Ins[kIn], "EvalPtr(r_old, " + arg + ")"));
                    kIn++;
                    break;
                default: throw new Exception("expected 'in' or 'inout' or 'out' or 'mem' in attributes of method" + method.Name);
            }
            args.Add(arg);
        }

        if (method.Body != null)
        {
            stmtExprEnabled = true;
            instructionProcArgs = args;
            foreach (var x in method.Ins.Concat(method.Outs))
            {
                string xName = GhostVar(x.Name);
                allVars[xName] = new RtlVar(xName, x.IsGhost, AppType(x.Type));
            }
            foreach (Statement stmt in method.Body.Body)
            {
                AddStatement(stmt);
            }
            instructionProcArgs = null;
            stmtExprEnabled = false;
        }

        bool isRelational = dafnycc.relational && reqs.Concat(enss).ToList().Exists(s =>
            s is RtlApply && (((RtlApply)s).op == "public" || ((RtlApply)s).op == "relation"));
        bool modifiesIo = Attributes.Contains(method.Attributes, "modifies_io");
        string envOther = ", objLayouts:[int]ObjLayout, $S:int, $toAbs:[int]int, $absMem:[int][int]int, $commonVars:commonVars, $gcVars:gcVars, init:bool, stk:mem, statics:mem, core_state:core_state, ptMem:mem, mems:mems, $stacksFrames:[int]Frames";
        string nucArgs = "objLayouts, $S, $toAbs, $absMem, $commonVars, $gcVars, me, init, stk, statics, core_state, ptMem, mems, $stacksFrames";
        string envIn = modifiesIo ? ", linear io_old:IOState" + envOther : "";
        string envOut = modifiesIo ? ", linear io:IOState" : "";
        string pIns = String.Concat(method.Ins.Select(f => ", " + GhostVar(f.Name) + ":" + TypeString(f.Type)));
        string pOuts = String.Concat(method.Outs.Select(f => ", " + GhostVar(f.Name) + ":" + TypeString(f.Type)));
        envIn += pIns;
        envOut += pOuts;

        Util.Assert(!isPrinting);
        isPrinting = true;
        string operandList = String.Concat(parms.Select(p => ", " + p));
        iwriter.WriteLine("atomic procedure " + name + "(my r_old:regs" + envIn + operandList + ") returns(my r:regs" + envOut + ");");
        Func<string,RtlExp,string> lets_e = (lets, e) =>
            !(e is RtlApply) ? lets + e :
            ((RtlApply)e).op == "public" ? "public(" + lets + ((RtlApply)e).args[0] + ")" :
            ((RtlApply)e).op == "relation" ? "relation(" + lets + ((RtlApply)e).args[0] + ")" :
            lets + e;
        if (strictOperands) { opnReqs.ForEach(e => iwriter.WriteLine("    requires " + e + ";")); }
        ins.ForEach(p => iwriter.WriteLine("    requires " + GhostVar(p.Item1.Name) + " == " + p.Item2 + ";"));
        reqs.ForEach(e => iwriter.WriteLine("    requires " + e + ";"));
        if (modifiesIo) { WriteDefaultRelationalRequires(isRelational); }
        if (modifiesIo) { iwriter.WriteLine("    requires NucleusInv(" + nucArgs + ", io_old);"); }
        GetStaticFieldMods().ForEach(x => iwriter.WriteLine("    modifies " + x + ";"));
        enss.ForEach(e => iwriter.WriteLine("    ensures  " + e + ";"));
        iwriter.WriteLine("    ensures  r.regs == r_old.regs" + outRegs + ";");
        if (modifiesIo) { WriteDefaultRelationalEnsures(isRelational); }
        if (modifiesIo) { iwriter.WriteLine("    ensures  NucleusInv(" + nucArgs + ", io);"); }
        if (method.Body != null)
        {
            writer.WriteLine("implementation " + name + "(my r_old:regs" + envIn + operandList + ") returns(my r:regs" + envOut + ")");
            writer.WriteLine("{");
            WriteAllVars();
            writer.WriteLine("r := r_old;");
            if (modifiesIo) { writer.WriteLine("io := io_old;"); }
            dafnySpec.WriteLemmas(writer, this, visibleModules, method.Attributes);
            foreach (RtlStmt s in stmts)
            {
                writer.WriteLine(s);
            }

            writer.WriteLine("}");
        }
        isPrinting = false;
    }