in ironclad-apps/tools/DafnyCC/CompileMethod.cs [1654:2002]
public override void Compile()
{
Util.Assert(!isPrinting);
isGhost = method is Lemma || method.IsGhost;
procName = ProcName(isGhost, SimpleName(typeApply.AppName()));
bool isAxiom = Attributes.Contains(method.Attributes, "axiom");
bool isPublic = Attributes.Contains(method.Attributes, "public");
bool isImported = Attributes.Contains(method.Attributes, "imported");
bool isInstruction = Attributes.Contains(method.Attributes, "instruction");
bool isHeapUnmodified = Attributes.Contains(method.Attributes, "dafnycc_heap_unmodified");
if (isImported && method.Body == null)
{
return;
}
if (method.Body == null && method.Name.StartsWith("reveal_"))
{
return;
}
if (isGhost)
{
if (!minVerify)
{
CompileGhost();
}
return;
}
if (isInstruction)
{
CompileInstruction();
return;
}
List<string> inVars = method.Ins.Where(x => !x.IsGhost).ToList().Select(x => GhostVar(x.Name)).ToList();
List<string> outVars = method.Outs.Where(x => !x.IsGhost).ToList().Select(x => GhostVar(x.Name)).ToList();
List<Formal> inInts = method.Ins.Where(x => !x.IsGhost && !IsPtrType(AppType(x.Type))).ToList();
List<Formal> outInts = method.Outs.Where(x => !x.IsGhost && !IsPtrType(AppType(x.Type))).ToList();
List<Formal> inPtrs = method.Ins.Where(x => !x.IsGhost && IsPtrType(AppType(x.Type))).ToList();
List<Formal> outPtrs = method.Outs.Where(x => !x.IsGhost && IsPtrType(AppType(x.Type))).ToList();
foreach (var x in method.Ins.Concat(method.Outs))
{
string name = GhostVar(x.Name);
allVars[name] = new RtlVar(name, x.IsGhost, AppType(x.Type));
}
BlockStmt body = method.Body;
if (body != null)
{
bool lastReturn = false;
stmtExprEnabled = true;
foreach (Statement stmt in body.Body)
{
lastReturn = (stmt is ReturnStmt);
AddStatement(stmt);
}
if (!lastReturn && !isGhost)
{
AddReturn(null);
}
stmtExprEnabled = false;
stmts = new Optimize(inVars, outVars, stmts).Run();
}
alloc = new RegAlloc(dafnySpec, this, inVars, outVars, inInts, outInts, inPtrs, outPtrs, allVars, stmts);
if (body != null)
{
stmts = alloc.Alloc();
}
else if (isAxiom)
{
stmts = new List<RtlStmt> { new RtlComment("dummy method body for axiom"), new RtlReturn(new RtlVar[0]) };
}
List<RtlExp> reqs = minVerify ? new List<RtlExp>()
: method.Req.ConvertAll(a => GhostExpression(a.E, false, true, a.Attributes));
List<RtlExp> enss = minVerify ? new List<RtlExp>()
: method.Ens.ConvertAll(a => GhostExpression(a.E, false, false, a.Attributes));
AddTypeWellFormed(reqs, method.Ins);
AddTypeWellFormed(enss, method.Outs);
bool isRelational = dafnycc.relational && reqs.Concat(enss).ToList().Exists(s =>
s is RtlApply && (((RtlApply)s).op == "public" || ((RtlApply)s).op == "relation"));
Util.DebugWriteLine();
Func<string, string> regold = s => "r_old.regs[" + s + "]";
Func<string, string> reg = s => "r.regs[" + s + "]";
string sMemOld = "stk_old";
string sMem = "stk";
string parms = String.Join(", ", method.Ins.Select(x => GhostVar(x.Name) + ":" + TypeString(AppType(x.Type))));
string rets = String.Join(", ", method.Outs.Select(x => GhostVar(x.Name) + ":" + TypeString(AppType(x.Type))));
string memVarsOld = "me,init,stk_old,statics_old,core_state,ptMem,mems_old";
string memVars = "me,init,stk,statics,core_state,ptMem,mems";
int frameCount = alloc.FrameCount() + dafnycc.framePointerCount;
int frameSize = frameCount * 4;
int inOutSize = 4 * alloc.InsOutsCount();
Func<List<Formal>, string> f = l => (l.Count != 0) ? ", " : "";
List<Tuple<string,string>> preserveExps = new List<Tuple<string,string>>();
for (int i = 0; i < method.Mod.Expressions.Count; i++)
{
Expression modExp = method.Mod.Expressions[i].E;
if (!(modExp is ThisExpr))
{
RtlExp e = GhostExpression(modExp, false, true);
preserveExps.Add(Tuple.Create("mod" + i, "(" + e + ").arrAbs"));
}
}
string absExtend = isHeapUnmodified
? "$toAbs == $toAbs_old && objLayouts == objLayouts_old"
: "AbsExtend($toAbs, $toAbs_old, objLayouts, objLayouts_old)";
string preserveHeap = isHeapUnmodified
? "heap == heap_old && $absMem == $absMem_old"
: DafnyCC.PreserveHeap(minVerify, preserveExps.ConvertAll(p => p.Item2));
Util.Assert(!isPrinting);
isPrinting = true;
string stackPrefix = "stack_size__DafnyCC__";
//- calculate the statck size
Func<string, string> g = s => (calledMethods.Count == 0) ? "0" : s;
if (!isPublic)
{
iwriter.WriteLine("const " + stackPrefix + procName + ":int := " + frameSize + " + "
+ g("max(" + String.Join(", max(", calledMethods.Select(s => stackPrefix + s + " + " + IPSize))
+ ", 0)" + String.Join(")", calledMethods.Select(s => ""))) + ";");
iwriter.WriteLine("procedure " + procName
+ "(my r_old:regs, const my core_state:core_state, linear stk_old:mem, linear statics_old:mem, linear io_old:IOState, linear mems_old:mems"
+ ", $commonVars_old:commonVars, $gcVars_old:gcVars"
+ ", $toAbs_old:[int]int, $absMem_old:[int][int]int, $stacksFrames_old:[int]Frames, objLayouts_old:[int]ObjLayout, heap_old:Heap"
+ f(method.Ins) + parms
+ ") returns(my r:regs, linear stk:mem, linear statics:mem, linear io:IOState, linear mems:mems"
+ ", $commonVars:commonVars, $gcVars:gcVars"
+ ", $toAbs:[int]int, $absMem:[int][int]int, $stacksFrames:[int]Frames, objLayouts:[int]ObjLayout, heap:Heap"
+ f(method.Outs) + rets + ");");
iwriter.WriteLine(" requires MemInv(" + memVarsOld + ");");
iwriter.WriteLine(" requires NucleusInv(objLayouts_old,$S,$toAbs_old,$absMem_old,$commonVars_old,$gcVars_old,me,init,stk_old,statics_old,core_state,ptMem,mems_old,$stacksFrames_old,io_old);");
iwriter.WriteLine(" requires SMemRequireGcRA(" + stackPrefix + procName + ", "
+ inOutSize + ", " + sMemOld + ", " + regold("ESP") + ", RET);");
iwriter.WriteLine(" requires HeapInv($absMem_old, objLayouts_old, heap_old);");
WriteDefaultRelationalRequires(isRelational);
foreach (var p in alloc.inInts)
{
int offset = alloc.InIntsOffset() - alloc.OutsOffset() + IPSize + p.Value;
string val = sMemOld + ".map[" + regold("ESP") + " + " + offset + "]";
iwriter.WriteLine(" requires " + IntEqTyped(allVars[p.Key].type, p.Key, val) + ";");
}
for (int i = 0; i < inPtrs.Count; i++)
{
Formal x = inPtrs[i];
int offset = alloc.InPtrsOffset() - alloc.OutsOffset() + IPSize + alloc.inPtrs[GhostVar(x.Name)];
string loc = regold("ESP") + " + " + offset + " + stackGcOffset";
iwriter.WriteLine(" requires StackAbsSlot(heap_old, $stacksFrames_old, "
+ loc + ") == Abs_"
+ TypeString(AppType(x.Type)) + "(" + GhostVar(x.Name) + ");");
if (DafnySpec.IsArrayType(AppType(x.Type)))
{
iwriter.WriteLine(" requires frameGet($stacksFrames_old, " + loc + ") == " + GhostVar(x.Name) + ".arrAbs;");
}
}
reqs.ForEach(e => iwriter.WriteLine(" requires " + e + ";"));
iwriter.WriteLine(" modifies $Time;");
GetStaticFieldMods().ForEach(x => iwriter.WriteLine(" modifies " + x + ";"));
iwriter.WriteLine(" ensures " + reg("ESP") + " == old(" + regold("ESP") + ") + " + IPSize + ";");
iwriter.WriteLine(" ensures MemInv(" + memVars + ");");
iwriter.WriteLine(" ensures NucleusInv(objLayouts,$S,$toAbs,$absMem,$commonVars,$gcVars,me,init,stk,statics,core_state,ptMem,mems,$stacksFrames,io);");
iwriter.WriteLine(" ensures SMemEnsureGcF(" + inOutSize + ", " + sMem + ", old(" + sMemOld + "), " + reg("ESP") + ", old(" + regold("ESP") + "), $stacksFrames, $stacksFrames_old);");
iwriter.WriteLine(" ensures HeapInv($absMem, objLayouts, heap);");
iwriter.WriteLine(" ensures " + absExtend + ";");
iwriter.WriteLine(" ensures " + preserveHeap + ";");
WriteDefaultRelationalEnsures(isRelational);
enss.ForEach(e => iwriter.WriteLine(" ensures " + e + ";"));
/*
foreach (var p in retMap)
{
writer.WriteLine(" ensures " + reg(p.Value) + " == " + p.Key + ";");
}
*/
foreach (var p in alloc.outInts)
{
int offset = IPSize + p.Value;
string val = sMem + ".map[" + regold("ESP") + " + " + offset + "]";
iwriter.WriteLine(" ensures " + IntEqTyped(allVars[p.Key].type, p.Key, val) + ";");
}
for (int i = 0; i < outPtrs.Count; i++)
{
Formal x = outPtrs[i];
int offset = IPSize + alloc.outPtrs[GhostVar(x.Name)];
string loc = regold("ESP") + " + " + offset + " + stackGcOffset";
iwriter.WriteLine(" ensures StackAbsSlot(heap, $stacksFrames, "
+ loc + ") == Abs_"
+ TypeString(AppType(x.Type)) + "(" + GhostVar(x.Name) + ");");
if (DafnySpec.IsArrayType(AppType(x.Type)))
{
iwriter.WriteLine(" ensures frameGet($stacksFrames, " + loc + ") == " + GhostVar(x.Name) + ".arrAbs;");
}
}
}
if (body != null || isAxiom)
{
writer.WriteLine("implementation " + procName
+ "(my r_old:regs, const my core_state:core_state, linear stk_old:mem, linear statics_old:mem, linear io_old:IOState, linear mems_old:mems"
+ ", $commonVars_old:commonVars, $gcVars_old:gcVars"
+ ", $toAbs_old:[int]int, $absMem_old:[int][int]int, $stacksFrames_old:[int]Frames, objLayouts_old:[int]ObjLayout, heap_old:Heap"
+ f(method.Ins) + parms
+ ") returns(my r:regs, linear stk:mem, linear statics:mem, linear io:IOState, linear mems:mems"
+ ", $commonVars:commonVars, $gcVars:gcVars"
+ ", $toAbs:[int]int, $absMem:[int][int]int, $stacksFrames:[int]Frames, objLayouts:[int]ObjLayout, heap:Heap"
+ f(method.Outs) + rets + ")");
writer.WriteLine("{");
writer.WriteLine(" var $absMem_tmp:[int][int]int;");
writer.WriteLine(" var objLayouts_tmp:[int]ObjLayout;");
writer.WriteLine(" var heap_tmp:Heap;");
writer.WriteLine(" var obj_tmp:int;");
writer.WriteLine(" var val_tmp:int;");
preserveExps.ForEach(p => writer.WriteLine(" var " + p.Item1 + ":int;"));
WriteAllVars();
dafnySpec.WriteLemmas(writer, this, visibleModules, method.Attributes);
writer.WriteLine(" r := r_old;");
writer.WriteLine(" stk := stk_old;");
writer.WriteLine(" statics := statics_old;");
writer.WriteLine(" io := io_old;");
writer.WriteLine(" mems := mems_old;");
writer.WriteLine(" $commonVars := $commonVars_old;");
writer.WriteLine(" $gcVars := $gcVars_old;");
writer.WriteLine(" $toAbs := $toAbs_old;");
writer.WriteLine(" $absMem := $absMem_old;");
writer.WriteLine(" $stacksFrames := $stacksFrames_old;");
writer.WriteLine(" objLayouts := objLayouts_old;");
writer.WriteLine(" heap := heap_old;");
for (int i = 0; i < inPtrs.Count; i++)
{
Formal x = inPtrs[i];
int offset = alloc.InPtrsOffset() - alloc.OutsOffset() + IPSize + alloc.inPtrs[GhostVar(x.Name)];
writer.WriteLine(" " + GhostVar(x.Name) + "__abs := frameGet($stacksFrames, "
+ regold("ESP") + " + " + offset + " + stackGcOffset);");
}
preserveExps.ForEach(p => writer.WriteLine(" " + p.Item1 + " := " + p.Item2 + ";"));
writer.WriteLine(" assert TV(" + reg("ESP") + ");");
for (int i = 0; i < frameCount; i++)
{
writer.WriteLine(" assert TO(0 - " + (i + 1) + ");");
writer.WriteLine(" assert TO(" + RegAlloc.stackGcOffset / 4 + " - " + (i + 1) + ");");
}
for (int i = frameCount; i < alloc.FrameVisibleCount(); i++)
{
writer.WriteLine(" assert TO(" + (i - frameCount) + ");");
writer.WriteLine(" assert TO(" + (RegAlloc.stackGcOffset / 4 + i - frameCount) + ");");
}
if (frameSize != 0)
{
writer.WriteLine(" call r := logical_Sub(r, ESP, OConst(" + frameSize + "));");
if (dafnycc.useFramePointer)
{
writer.WriteLine(" call stk := logical_Store(r, core_state, stk, OMem(MReg(ESP, " + (frameSize - 4) + ")), OReg(EBP));");
writer.WriteLine(" call r := instr_LeaUnchecked(r, EBP, OMem(MReg(ESP, " + (frameSize - 4) + ")));");
}
}
bool wasComment= false;
string indent = " ";
foreach (RtlStmt s in stmts)
{
RtlIndent rtlIndent = s as RtlIndent;
RtlLabel label = s as RtlLabel;
RtlCall call = s as RtlCall;
if (rtlIndent != null)
{
indent = rtlIndent.Positive ? indent + " " : indent.Substring(4);
continue;
}
if (s is RtlReturn && frameSize != 0)
{
if (dafnycc.useFramePointer)
{
writer.WriteLine(" call r := logical_Load(r, core_state, stk, EBP, OMem(MReg(ESP, " + (frameSize - 4) + ")));");
}
writer.WriteLine(indent + "call r := logical_Add(r, ESP, OConst(" + frameSize + "));");
}
/*
if (call != null && call.op == "Proc_sample")
{
writer.WriteLine(indent + GhostVar(samplemap) + " := F();");
}
*/
if (s.comment != null)
{
if (!wasComment)
{
writer.WriteLine();
}
writer.WriteLine(indent + "// " + s.comment().Replace(Environment.NewLine, Environment.NewLine + indent));
}
wasComment = true;
if (s.ToString() != "")
{
writer.WriteLine(indent + s.ToString().Replace(Environment.NewLine, Environment.NewLine + indent));
wasComment = false;
}
if (call != null)
{
writer.WriteLine(indent + "assert SMemInvGcF(" + (inOutSize + 4) + ", " + sMem + ", old(" + sMemOld + "), " + reg("ESP") + " + " + frameSize + ", old(" + regold("ESP") + "), $stacksFrames, $stacksFrames_old);");
if (dafnycc.useFramePointer) {
writer.WriteLine(indent + "call r := instr_LeaUnchecked(r, EBP, OMem(MReg(ESP, " + (frameSize - 4) + ")));");
}
}
if (label != null && label.loop)
{
writer.WriteLine(indent + "invariant MemInv(" + memVars + ");");
writer.WriteLine(indent + "invariant NucleusInv(objLayouts,$S,$toAbs,$absMem,$commonVars,$gcVars,me,init,stk,statics,core_state,ptMem,mems,$stacksFrames,io);");
writer.WriteLine(indent + "invariant SMemInvGcF(" + (inOutSize + 4) + ", " + sMem + ", old(" + sMemOld + "), " + reg("ESP") + " + " + frameSize + ", old(" + regold("ESP") + "), $stacksFrames, $stacksFrames_old);");
writer.WriteLine(indent + "invariant HeapInv($absMem, objLayouts, heap);");
writer.WriteLine(indent + "invariant " + absExtend + ";");
writer.WriteLine(indent + "invariant " + preserveHeap + ";");
if (isRelational)
{
writer.WriteLine(" invariant public(io._inCtr);");
writer.WriteLine(" invariant public(io._outCtr);");
}
else if (dafnycc.relational)
{
writer.WriteLine(" invariant io._inCtr == io_old._inCtr && io._outCtr == io_old._outCtr;");
}
}
if (s is RtlLoopStart)
{
dafnySpec.WriteLemmas(writer, this, visibleModules, method.Attributes, true);
}
}
writer.WriteLine("}");
}
isPrinting = false;
}