in ironclad-apps/tools/DafnyCC/CompileMethod.cs [559:900]
void AddExpression(RtlVar dest, Expression exp)
{
Util.Assert(!isPrinting);
Util.Assert(!dest.isGhost);
exp = GetExp(exp);
Util.DebugWriteLine("exp: " + exp.GetType());
StmtExpr stmtExpr = exp as StmtExpr;
RtlVar var = AsVar(exp);
BigInteger? intExp = AsInt(exp);
BinaryExpr binary = exp as BinaryExpr;
UnaryExpr unary = exp as UnaryExpr;
ITEExpr ite = exp as ITEExpr;
LetExpr letExp = exp as LetExpr;
MatchExpr matchExp = exp as MatchExpr;
FunctionCallExpr funCall = exp as FunctionCallExpr;
DatatypeValue dataVal = exp as DatatypeValue;
MemberSelectExpr memberSelect = exp as MemberSelectExpr;
SeqSelectExpr seqSelect = exp as SeqSelectExpr;
SeqUpdateExpr seqUpdate = exp as SeqUpdateExpr;
SeqDisplayExpr seqDisplay = exp as SeqDisplayExpr;
if (stmtExpr != null)
{
if (stmtExprEnabled)
{
if (ignoreStmtExpr == 0)
{
AddGhostStatement(stmtExpr.S, null);
}
AddExpression(dest, stmtExpr.E);
return;
}
else
{
throw new Exception("not implemented: cannot handle statement expression here");
}
}
if (var != null)
{
Util.DebugWriteLine("dest = " + dest + " var = " + var);
Move(dest, var, IsPtrType(AppType(exp.Type)));
}
else if (intExp != null)
{
Move(dest, new RtlInt((BigInteger)intExp), false);
}
else if (binary != null)
{
switch (binary.ResolvedOp)
{
case BinaryExpr.ResolvedOpcode.Concat:
{
AddBuildSequence(dest, exp);
return;
}
}
if (IsPtrType(AppType(binary.E0.Type)) || IsPtrType(AppType(binary.E1.Type)))
{
throw new Exception("binary operators only implemented for integer and bool types");
}
if (jumpOps.ContainsKey(binary.Op.ToString()))
{
AddBoolViaJump(dest, exp);
}
else
{
switch (binary.Op)
{
case BinaryExpr.Opcode.And:
case BinaryExpr.Opcode.Or:
case BinaryExpr.Opcode.Imp:
case BinaryExpr.Opcode.Iff:
AddBoolViaJump(dest, exp);
break;
case BinaryExpr.Opcode.Mul:
case BinaryExpr.Opcode.Div:
case BinaryExpr.Opcode.Mod:
{
bool nonlinear = !(IsConstant(binary.E0) || IsConstant(binary.E1));
bool isDivMod = (binary.Op == BinaryExpr.Opcode.Div || binary.Op == BinaryExpr.Opcode.Mod);
string sop = isDivMod ? "DivMod" : binary.Op.ToString();
var m = dafnySpec.FindMethod((nonlinear ? "Method_" : "method_") + sop);
//Expression zero = new LiteralExpr(binary.tok, 0);
AddCallInstruction(
(binary.Op == BinaryExpr.Opcode.Mod) ? new List<RtlVar> { dest, TempVar(Type.Int) } :
new List<RtlVar> { TempVar(Type.Int), dest },
m.Ins, DafnySpec.SimpleSanitizedName(m),
isDivMod ? new List<Expression> { null, binary.E0, binary.E1 } :
new List<Expression> { binary.E0, binary.E1 },
m.Attributes,
isDivMod ? new List<RtlExp> { new RtlInt(0), null, null } : null);
break;
}
default:
AddBinary(dest, BinaryInstOp(binary.Op), binary.E0, binary.E1);
break;
}
}
}
else if (unary != null && unary is UnaryOpExpr && ((UnaryOpExpr)unary).Op == UnaryOpExpr.Opcode.Not)
{
AddBoolViaJump(dest, exp);
}
else if (unary != null && unary is UnaryOpExpr && ((UnaryOpExpr)unary).Op == UnaryOpExpr.Opcode.Cardinality)
{
var m = dafnySpec.GetSeqMethod(AppType(unary.E.Type), "seq_Length");
AddCall(new List<RtlVar> { dest }, false, false, m.Item1, new List<Expression> { unary.E },
m.Item1.Outs, m.Item2);
}
else if (ite != null)
{
//- if (!e) goto skip1
//- then-body
//- goto skip2
//- skip1:
//- else-body
//- skip2:
string skip1 = NewLabel();
Jump(skip1, ite.Test, false);
AddExpression(dest, ite.Thn);
string skip2 = NewLabel();
Jump(skip2);
Label(skip1);
AddExpression(dest, ite.Els);
Label(skip2);
}
else if (letExp != null)
{
if (!letExp.Exact)
{
throw new Exception("not implemented: LetExpr: " + letExp);
}
for (int i = 0; i < letExp.LHSs.Count; i++)
{
var lhs = letExp.LHSs[i];
var rhs = letExp.RHSs[i];
string name = GhostVar(lhs.Var.Name);
if (allVars.Keys.Contains(name))
{
AddRename(lhs.Var.Name);
name = GhostVar(lhs.Var.Name);
}
RtlVar lhsVar = new RtlVar(name, lhs.Var.IsGhost, AppType(lhs.Var.Type));
allVars.Add(name, lhsVar);
AddExpression(lhsVar, rhs);
}
AddExpression(dest, letExp.Body);
}
else if (matchExp != null)
{
if (matchExp.MissingCases.Count != 0)
{
throw new Exception("not implemented: MatchExpr with missing cases: " + matchExp);
}
AddMatch(dest, matchExp.Source, matchExp.Cases, c => c.Body, null);
}
else if (funCall != null)
{
if (Attributes.Contains(funCall.Function.Attributes, "dafnycc_inline"))
{
TypeApply app = dafnySpec.Compile_Function(funCall.Function,
funCall.TypeArgumentSubstitutions.ToDictionary(p => p.Key, p => AppType(p.Value)));
string funName = FunName(SimpleName(app.AppName()));
Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
for (int i = 0; i < funCall.Function.Formals.Count; i++)
{
substMap.Add(funCall.Function.Formals[i], funCall.Args[i]);
}
Translator.Substituter subst = new Translator.Substituter(null, substMap, new Dictionary<TypeParameter,Type>(), null);
Expression body = subst.Substitute(funCall.Function.Body);
AddExpression(dest, body);
List<RtlExp> rtlArgs = funCall.Args.ConvertAll(e => GhostExpression(e));
stmts.Add(new RtlAssert(new RtlBinary("==", dest, new RtlApply(funName, rtlArgs))));
return;
}
string name = SimpleName(funCall.Function.Name);
switch (name)
{
case "and":
case "or":
case "xor":
{
string op = "instr_" + Char.ToUpper(name[0]) + name.Substring(1);
AddBinary(dest, op, funCall.Args[0], funCall.Args[1]);
break;
}
default:
{
TypeApply app = dafnySpec.Compile_Function(funCall.Function,
funCall.TypeArgumentSubstitutions.ToDictionary(p => p.Key, p => AppType(p.Value)));
AddCall(new List<RtlVar> { dest }, false, DafnySpec.IsHeapFunction(funCall.Function),
funCall.Function, funCall.Args,
new List<Formal> { new Formal(funCall.tok, "__result", funCall.Type, false, false) }, app);
SymdiffLinearityPoint();
break;
}
}
}
else if (dataVal != null)
{
List<Expression> args = new List<Expression> { dataVal }.Concat(dataVal.Arguments).ToList();
List<Formal> ins = new List<Formal> { new Formal(dataVal.tok, "data", AppType(dataVal.Type), true, true) }
.Concat(dataVal.Ctor.Formals).ToList();
string name = dafnySpec.Compile_Constructor(dataVal.Type, dataVal.Ctor.Name,
dataVal.InferredTypeArgs, typeApply.typeArgs).AppName();
AddCall(new List<RtlVar> { dest }, false, true, ins, "Alloc_" + name, args,
new List<Formal> { new Formal(dataVal.tok, "ret", AppType(dataVal.Type), false, false) });
}
else if (memberSelect != null && memberSelect.Member is Field && memberSelect.MemberName.EndsWith("?"))
{
AddBoolViaJump(dest, exp);
}
else if (memberSelect != null && memberSelect.Member is Field && DafnySpec.IsArrayType(AppType(memberSelect.Obj.Type))
&& memberSelect.MemberName == "Length")
{
RtlVar eArr = AsVarOrTemp(memberSelect.Obj);
ArrayLength(dest, eArr);
}
else if (memberSelect != null && memberSelect.Member is Field && !memberSelect.Member.IsStatic && AppType(memberSelect.Obj.Type) is UserDefinedType
&& memberSelect.Member is DatatypeDestructor)
{
RtlVar e0 = AsVarOrTemp(memberSelect.Obj);
if (minVerify)
{
//- run-time type check
string fail = NewLabel();
string ok = NewLabel();
DatatypeDestructor field = (DatatypeDestructor) memberSelect.Member;
JumpIfHasType(ok, e0, field.EnclosingCtor.Name, memberSelect.Obj.Type, true);
Label(fail, true);
Jump(fail);
Label(ok, false);
}
AddFieldSelect(dest, e0, memberSelect.Obj.Type, memberSelect.MemberName, exp.Type, GhostExpression(exp));
}
else if (seqSelect != null)
{
if (seqSelect.SelectOne && DafnySpec.IsArrayType(AppType(seqSelect.Seq.Type)))
{
RtlVar eArr = AsVarOrTemp(seqSelect.Seq);
RtlExp eInd = AsSimpleOrTemp(seqSelect.E0);
if (minVerify)
{
//- run-time bounds check
string fail = NewLabel();
string ok = NewLabel();
RtlVar eLen = TempVar(Type.Int);
ArrayLength(eLen, eArr);
Jump(ok, new RtlBinary("<", eInd, eLen));
Label(fail, true);
Jump(fail);
Label(ok, false);
}
string abs = eArr + "__abs";
int start = stmts.Count;
stmts.Add(new RtlStmtComputed(
s => "call r, mems := loadArrayElement(r, core_state, stk, statics, io, mems, $commonVars, "
+ "$gcVars, $toAbs, $absMem, $stacksFrames, objLayouts, heap, "
+ s.args[0] + ", "
+ new RtlMem(s.args[1].e, new RtlInt(4), s.args[2].e, new RtlInt(8)).AsOperand() + ", "
+ eInd + ", " + abs + ", " + RegAlloc.Reg(s.args[1].ToString()) + ");",
new List<RtlArg> {
new RtlArg(false, true, dest),
new RtlArg(true, false, eArr),
new RtlArg(true, false, eInd)
}, false)
.WithComment("loadArrayElement"));
GroupStatements(start);
}
else if (seqSelect.SelectOne)
{
var m = dafnySpec.GetSeqMethod(AppType(seqSelect.Seq.Type), "seq_Index");
AddCall(new List<RtlVar> { dest }, false, true, m.Item1, new List<Expression> { seqSelect.Seq, seqSelect.E0 },
m.Item1.Outs, m.Item2);
}
else
{
RtlVar seq;
if (DafnySpec.IsArrayType(AppType(seqSelect.Seq.Type)))
{
seq = TempVar(seqSelect.Type);
var m = dafnySpec.FindMethod("seq_FromArray");
AddCall(new List<RtlVar> { seq }, false, true, m,
new List<Expression>() { seqSelect.Seq }, m.Outs);
}
else
{
seq = AsVarOrTemp(seqSelect.Seq);
}
if (seqSelect.E0 != null && seqSelect.E1 != null)
{
var m = dafnySpec.GetSeqMethod(AppType(seqSelect.Type), "seq_TakeDrop");
AddCall(new List<RtlVar> { dest }, false, true, m.Item1,
new List<RtlVar> { seq, null, null },
new List<Expression> { null, seqSelect.E0, seqSelect.E1 },
m.Item1.Outs, m.Item2);
}
else if (seqSelect.E1 != null)
{
var m = dafnySpec.GetSeqMethod(AppType(seqSelect.Type), "seq_Take");
AddCall(new List<RtlVar> { dest }, false, true, m.Item1,
new List<RtlVar> { seq, null },
new List<Expression> { null, seqSelect.E1 },
m.Item1.Outs, m.Item2);
}
else if (seqSelect.E0 != null)
{
var m = dafnySpec.GetSeqMethod(AppType(seqSelect.Type), "seq_Drop");
AddCall(new List<RtlVar> { dest }, false, true, m.Item1,
new List<RtlVar> { seq, null },
new List<Expression> { null, seqSelect.E0 },
m.Item1.Outs, m.Item2);
}
else
{
Move(dest, seq, true);
}
}
}
else if (seqUpdate != null)
{
if (seqUpdate.ResolvedUpdateExpr != null) {
AddExpression(dest, seqUpdate.ResolvedUpdateExpr);
} else {
var m = dafnySpec.GetSeqMethod(AppType(seqSelect.Seq.Type), "seq_Update");
AddCall(new List<RtlVar> { dest }, false, true, m.Item1,
new List<Expression> { seqUpdate.Seq, seqUpdate.Index, seqUpdate.Value },
m.Item1.Outs, m.Item2);
}
}
else if (seqDisplay != null)
{
AddBuildSequence(dest, exp);
return;
}
else
{
throw new Exception("not implemented: " + dest + " := " + exp);
}
}