in ironclad-apps/tools/DafnyCC/CompileMethod.cs [1296:1463]
void AddResolvedStatement(Statement stmt)
{
Util.DebugWriteLine("stmt: " + stmt.GetType());
Util.Assert(!isGhost);
Util.Assert(!stmt.IsGhost || stmt is CalcStmt);
BlockStmt block = stmt as BlockStmt;
IfStmt ifStmt = stmt as IfStmt;
WhileStmt whileStmt = stmt as WhileStmt;
BreakStmt breakStmt = stmt as BreakStmt;
ReturnStmt returnStmt = stmt as ReturnStmt;
AssertStmt assertStmt = stmt as AssertStmt;
AssignStmt assignStmt = stmt as AssignStmt;
CallStmt callStmt = stmt as CallStmt;
VarDeclStmt varDecl = stmt as VarDeclStmt;
MatchStmt matchStmt = stmt as MatchStmt;
CalcStmt calcStmt = stmt as CalcStmt;
ForallStmt forallStmt = stmt as ForallStmt;
PrintStmt printStmt = stmt as PrintStmt;
if (block != null)
{
var oldRenamer = PushRename();
block.Body.ForEach(AddStatement);
PopRename(oldRenamer);
}
else if (varDecl != null)
{
foreach (var varLocal in varDecl.Locals) {
AddVarDecl(varLocal.Name, varLocal.Type, varLocal.IsGhost);
}
if (varDecl.Update != null) {
Util.Assert(varDecl.Update is UpdateStmt);
//Util.Assert(varDecl.Update.Lhss.Count() == 1);
//AddAssignmentRhs(AsVar(varDecl.Update.Lhss[0]), ((UpdateStmt)varDecl.Update).Rhss[0]);
AddStatement(varDecl.Update);
}
}
else if (assignStmt != null)
{
IdentifierExpr idExp = assignStmt.Lhs as IdentifierExpr;
SeqSelectExpr seqSelect = assignStmt.Lhs as SeqSelectExpr;
if (idExp != null)
{
AddAssignmentRhs(AsVar(assignStmt.Lhs), assignStmt.Rhs);
}
else if (seqSelect != null && seqSelect.SelectOne && DafnySpec.IsArrayType(AppType(seqSelect.Seq.Type)))
{
RtlVar eSeq = AsVarOrTemp(seqSelect.Seq);
RtlExp eInd = AsSimpleOrTemp(seqSelect.E0);
RtlExp eVal = AssignmentRhsAsSimpleOrTemp(assignStmt.Lhs.Type, assignStmt.Rhs);
AssignSeqLhs(eSeq, eInd, eVal);
}
else
{
throw new Exception("not implemented: assignment to " + assignStmt.Lhs);
}
}
else if (callStmt != null)
{
var lhss = callStmt.Lhs.ConvertAll(AssignLhs);
AddCall(lhss.ConvertAll(lhs => lhs.Item1), stmt.IsGhost, DafnySpec.IsHeapMethod(callStmt.Method),
callStmt.Method, callStmt.Args, callStmt.Method.Outs, dafnySpec.Compile_Method(callStmt.Method,
callStmt.MethodSelect.TypeArgumentSubstitutions().ToDictionary(p => p.Key, p => AppType(p.Value))));
lhss.ForEach(lhs => lhs.Item2());
SymdiffLinearityPoint();
}
else if (ifStmt != null)
{
//- if (!e) goto skip1
//- then-body
//- goto skip2
//- skip1:
//- else-body
//- skip2:
string skip1 = NewLabel();
Jump(skip1, ifStmt.Guard, false);
AddStatement(ifStmt.Thn);
if (ifStmt.Els == null)
{
Label(skip1);
}
else
{
string skip2 = NewLabel();
Jump(skip2);
Label(skip1);
AddStatement(ifStmt.Els);
Label(skip2);
}
}
else if (whileStmt != null)
{
//- goto begin
//- loop:
//- body
//- begin:
//- assert ...;
//- if (e) goto loop
//- end:
string loop = NewLabel();
string begin = NewLabel();
string end = NewLabel();
whileEnd.Add(end);
Jump(begin);
Label(loop);
AddStatement(whileStmt.Body);
Label(begin, true);
foreach (MaybeFreeExpression mexp in whileStmt.Invariants)
{
Util.Assert(!mexp.IsFree);
if (!minVerify)
{
bool old_stmtExprEnabled = stmtExprEnabled;
stmtExprEnabled = false;
stmts.Add(new RtlAssert(GhostExpression(mexp.E), true));
stmtExprEnabled = old_stmtExprEnabled;
}
}
SymdiffLinearityPoint();
stmts.Add(new RtlLoopStart());
Jump(loop, whileStmt.Guard);
whileEnd.RemoveAt(whileEnd.Count - 1);
Label(end);
}
else if (breakStmt != null && breakStmt.TargetLabel == null)
{
Jump(whileEnd[whileEnd.Count - breakStmt.BreakCount]);
}
else if (returnStmt != null)
{
AddReturn(returnStmt.rhss);
}
else if (assertStmt != null)
{
if (minVerify)
{
return;
}
stmts.Add(new RtlAssert(GhostExpression(assertStmt.Expr)));
}
else if (matchStmt != null)
{
if (matchStmt.MissingCases.Count != 0)
{
throw new Exception("not implemented: MatchStmt with missing cases: " + matchStmt);
}
AddMatch(null, matchStmt.Source, matchStmt.Cases, null, c => c.Body);
}
else if (calcStmt != null)
{
AddGhostStatement(calcStmt, null);
}
else if (forallStmt != null)
{
AddGhostStatement(forallStmt, null);
}
else if (printStmt != null)
{
Util.Assert(printStmt.Args.Count == 1);
var m = dafnySpec.FindMethod("print_int");
AddCall(new List<RtlVar>(), false, true, m,
new List<Expression>() { printStmt.Args[0] }, m.Outs);
}
else
{
throw new Exception("not implemented: " + stmt);
}
}