in ironclad-apps/tools/DafnySpec/Compile.cs [352:747]
public RtlExp GhostExpressionRec(Expression exp, bool inRecSpec = false, bool inRequiresOrOld = false)
{
Util.Assert(!isPrinting);
exp = GetExp(exp);
StmtExpr stmtExpr = exp as StmtExpr;
IdentifierExpr idExp = exp as IdentifierExpr;
LiteralExpr literal = exp as LiteralExpr;
BinaryExpr binary = exp as BinaryExpr;
UnaryExpr unary = exp as UnaryExpr;
ITEExpr ite = exp as ITEExpr;
ExistsExpr existsExp = exp as ExistsExpr;
ForallExpr forallExp = exp as ForallExpr;
LetExpr letExp = exp as LetExpr;
MatchExpr matchExp = exp as MatchExpr;
OldExpr oldExp = exp as OldExpr;
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;
Func<Expression,RtlExp> G = e => GhostExpression(e, inRecSpec, inRequiresOrOld);
if (stmtExpr != null)
{
if (stmtExprEnabled)
{
if (ignoreStmtExpr == 0)
{
AddGhostStatement(stmtExpr.S, null);
}
return G(stmtExpr.E);
}
else
{
throw new Exception("not implemented: cannot handle statement expression here");
}
}
else if (idExp != null)
{
return AsVar(idExp);
}
else if (literal != null && literal.Value is BigInteger)
{
return new RtlInt((BigInteger)(literal.Value));
}
else if (literal != null && literal.Value is bool)
{
return new RtlLiteral((bool)(literal.Value) ? "true" : "false");
}
else if (literal != null && literal.Value == null)
{
return new RtlLiteral("ArrayOfInt(0 - 1, NO_ABS)");
}
else if (literal != null && literal.Value is Microsoft.Basetypes.BigDec)
{
return new RtlLiteral(((Microsoft.Basetypes.BigDec)literal.Value).ToDecimalString());
}
else if (binary != null)
{
string op = null;
string internalOp = null;
CompileFunction compileFunction = this as CompileFunction;
string thisFuncName = (compileFunction == null) ? null : compileFunction.function.Name;
switch (binary.ResolvedOp)
{
case BinaryExpr.ResolvedOpcode.SeqEq:
return new RtlApply(dafnySpec.GetSeqOperationName(AppType(binary.E0.Type), "Seq_Equal"),
new RtlExp[] { G(binary.E0), G(binary.E1) });
case BinaryExpr.ResolvedOpcode.SeqNeq:
return new RtlLiteral("(!" +
new RtlApply(dafnySpec.GetSeqOperationName(AppType(binary.E0.Type), "Seq_Equal"),
new RtlExp[] { G(binary.E0), G(binary.E1) }) + ")");
case BinaryExpr.ResolvedOpcode.Concat:
return new RtlApply(dafnySpec.GetSeqOperationName(AppType(binary.Type), "Seq_Append"),
new RtlExp[] { G(binary.E0), G(binary.E1) });
}
if (binary.Op == BinaryExpr.Opcode.Exp)
{
binary = new BinaryExpr(binary.tok, BinaryExpr.Opcode.Imp, binary.E0, binary.E1);
}
switch (binary.Op)
{
case BinaryExpr.Opcode.Disjoint:
case BinaryExpr.Opcode.In:
case BinaryExpr.Opcode.NotIn:
throw new Exception("not implemented: binary operator '" + BinaryExpr.OpcodeString(binary.Op) + "'");
}
if (AppType(binary.E0.Type) is IntType && AppType(binary.E1.Type) is IntType)
{
switch (binary.Op)
{
case BinaryExpr.Opcode.Le: internalOp = "INTERNAL_le_boogie"; break;
case BinaryExpr.Opcode.Lt: internalOp = "INTERNAL_lt_boogie"; break;
case BinaryExpr.Opcode.Ge: internalOp = "INTERNAL_ge_boogie"; break;
case BinaryExpr.Opcode.Gt: internalOp = "INTERNAL_gt_boogie"; break;
case BinaryExpr.Opcode.Add: internalOp = "INTERNAL_add_boogie"; break;
case BinaryExpr.Opcode.Sub: internalOp = "INTERNAL_sub_boogie"; break;
case BinaryExpr.Opcode.Mul:
op = "*";
if (thisFuncName != "INTERNAL_mul")
{
internalOp = FunName("INTERNAL__mul");
}
break;
case BinaryExpr.Opcode.Div:
op = "div";
if (thisFuncName != "INTERNAL_div")
{
internalOp = FunName("INTERNAL__div");
}
break;
case BinaryExpr.Opcode.Mod:
op = "mod";
if (thisFuncName != "INTERNAL_mod")
{
internalOp = FunName("INTERNAL__mod");
}
break;
default:
op = BinaryExpr.OpcodeString(binary.Op);
break;
}
}
else
{
op = BinaryExpr.OpcodeString(binary.Op);
}
if (internalOp == null)
{
return new RtlBinary(op, G(binary.E0), G(binary.E1));
}
else
{
return new RtlApply(internalOp, new RtlExp[]
{ G(binary.E0), G(binary.E1) });
}
} else if (unary != null) {
if (unary is UnaryOpExpr) {
UnaryOpExpr unaryOp = (UnaryOpExpr)unary;
if (unaryOp.Op == UnaryOpExpr.Opcode.Not) {
return new RtlLiteral("(!(" + G(unaryOp.E) + "))");
} else if (unaryOp.Op == UnaryOpExpr.Opcode.Cardinality) {
return new RtlApply(dafnySpec.GetSeqOperationName(AppType(unaryOp.E.Type), "Seq_Length"),
new RtlExp[] { G(unaryOp.E) });
} else if (unaryOp.Op == UnaryOpExpr.Opcode.Fresh) {
Util.Assert(DafnySpec.IsArrayType(unaryOp.E.Type));
string abs = G(unaryOp.E) + ".arrAbs";
return new RtlLiteral("(heap_old.absData[" + abs + "] is AbsNone)");
} else {
throw new Exception("not implemented: " + exp);
}
} else if (unary is ConversionExpr) {
var e = (ConversionExpr)unary;
var fromInt = e.E.Type.IsNumericBased(Type.NumericPersuation.Int);
var toInt = e.ToType.IsNumericBased(Type.NumericPersuation.Int);
if (fromInt && !toInt) {
return new RtlApply("real", new RtlExp[] { G(e.E) });
} else if (!fromInt && toInt) {
return new RtlApply("int", new RtlExp[] { G(e.E) });
} else {
Util.Assert(fromInt == toInt);
return GhostExpressionRec(e.E, inRecSpec, inRequiresOrOld);
}
} else {
throw new Exception("not implemented: " + exp);
}
}
else if (ite != null)
{
return GhostIfThenElse(G(ite.Test), () => G(ite.Thn), () => G(ite.Els));
}
else if (funCall != null)
{
switch (funCall.Function.Name)
{
case "left":
case "right":
case "relation":
case "public":
Util.Assert(funCall.Args.Count == 1);
return new RtlApply(funCall.Function.Name, new RtlExp[] { G(funCall.Args[0]) });
case "sizeof":
Util.Assert(funCall.Args.Count == 1);
return new RtlApply(funCall.Function.Name + "##" + TypeString(AppType(funCall.Args[0].Type)),
new RtlExp[] { G(funCall.Args[0]) });
case "INTERNAL_add_raw":
Util.Assert(funCall.Args.Count == 2);
return new RtlBinary("+", G(funCall.Args[0]), G(funCall.Args[1]));
case "INTERNAL_sub_raw":
Util.Assert(funCall.Args.Count == 2);
return new RtlBinary("-", G(funCall.Args[0]), G(funCall.Args[1]));
}
TypeApply app = dafnySpec.Compile_Function(funCall.Function,
funCall.TypeArgumentSubstitutions.ToDictionary(p => p.Key, p => AppType(p.Value)));
string name = FunName(SimpleName(app.AppName()));
string fullName = FunName(SimpleName(app.AppFullName()));
List<RtlExp> rtlArgs = funCall.Args.Select(G).ToList();
List<RtlExp> rtlReads = funCall.Function.Reads.Where(e => e.Field != null).ToList()
.ConvertAll(e => (RtlExp)new RtlVar(
GhostVar(e.FieldName), e.Field.IsGhost, AppType(e.Field.Type)));
rtlArgs = rtlReads.Concat(rtlArgs).ToList();
if (name.EndsWith("__INTERNAL__HEAP"))
{
name = name.Substring(0, name.Length - "__INTERNAL__HEAP".Length);
}
else if (DafnySpec.IsHeapFunction(funCall.Function))
{
rtlArgs.Insert(0, new RtlLiteral(inRequiresOrOld ? "$absMem_old" : "$absMem"));
}
if (Attributes.Contains(funCall.Function.Attributes, "opaque")
&& funCall.Function.Formals.Count + rtlReads.Count == 0)
{
rtlArgs.Insert(0, new RtlLiteral("true"));
}
if (fullName == recFunName)
{
name = fullName;
}
if (name == recFunName)
{
recCalls.Add(new List<RtlExp>(rtlArgs));
rtlArgs.Insert(0, new RtlApply("decreases_" + name, new List<RtlExp>(rtlArgs)));
rtlArgs.Insert(1, new RtlLiteral(inRecSpec ? "__unroll" : "__unroll + 1"));
name = "rec_" + name;
}
return new RtlApply(name, rtlArgs);
}
else if (dataVal != null)
{
bool isSeq = dataVal.Type.TypeName(null).StartsWith("Seq<");
return new RtlApply((isSeq ? "_" : "") + dafnySpec.Compile_Constructor(
dataVal.Type, dataVal.Ctor.Name, dataVal.InferredTypeArgs, typeApply.typeArgs).AppName(),
dataVal.Arguments.Select(G));
}
else if (existsExp != null || forallExp != null)
{
QuantifierExpr qExp = (QuantifierExpr)exp;
bool isForall = forallExp != null;
var varTuples = qExp.BoundVars.Select(v => Tuple.Create(GhostVar(v.Name), v.IsGhost, v.Type));
var oldRenamer = PushRename(qExp.BoundVars.Select(v => v.Name));
var oldStmtExprEnabled = stmtExprEnabled;
stmtExprEnabled = false;
RtlExp rExp = new RtlLiteral((isForall ? "(forall " : "(exists ")
+ string.Join(", ", qExp.BoundVars.Select(v => GhostVar(v.Name) + ":" + TypeString(AppType(v.Type))))
+ " :: " + Triggers(qExp.Attributes, G) + " "
+ GetTypeWellFormedExp(varTuples.ToList(), isForall ? "==>" : "&&", G(qExp.Term)) + ")");
stmtExprEnabled = oldStmtExprEnabled;
PopRename(oldRenamer);
return rExp;
}
else if (letExp != null)
{
List<RtlExp> rhss;
if (letExp.Exact)
{
rhss = letExp.RHSs.ConvertAll(e => G(e));
}
else if (letExp.LHSs.Count == 1 && LiteralExpr.IsTrue(letExp.RHSs[0]) && AppType(letExp.LHSs[0].Var.Type) is IntType)
{
rhss = new List<RtlExp> { new RtlLiteral("0") };
}
else
{
throw new Exception("not implemented: LetExpr: " + letExp);
}
return GhostLet(exp.tok, letExp.LHSs.ConvertAll(lhs => lhs.Var), rhss, () => G(letExp.Body));
}
else if (matchExp != null)
{
if (matchExp.MissingCases.Count != 0)
{
throw new Exception("not implemented: MatchExpr with missing cases: " + matchExp);
}
//- match src case c1(ps1) => e1 ... cn(psn) => en
//- -->
//- let x := src in
//- if x is c1 then let ps1 := ...x.f1... in e1 else
//- if x is c2 then let ps2 := ...x.f2... in e2 else
//- let ps3 := ...x.f3... in e3
var src = G(matchExp.Source);
var cases = matchExp.Cases;
string x = TempName();
Func<RtlExp> body = null;
for (int i = cases.Count; i > 0; )
{
i--;
MatchCaseExpr c = cases[i];
Func<List<RtlExp>> cRhss = () => c.Ctor.Formals.ConvertAll(f => (RtlExp)new RtlLiteral("("
+ f.Name + "#" + c.Ctor.Name + "(" + GhostVar(x) + "))"));
Func<RtlExp> ec = () => GhostLet(exp.tok, c.Arguments, cRhss(), () => G(c.Body));
if (body == null)
{
body = ec;
}
else
{
var prevBody = body;
body = () => GhostIfThenElse(new RtlLiteral("(" + GhostVar(x) + " is " + c.Ctor.Name + ")"),
ec, prevBody);
}
}
return GhostLet(exp.tok, new List<BoundVar> { new BoundVar(exp.tok, x, matchExp.Source.Type) },
new List<RtlExp> { src }, body);
}
else if (oldExp != null)
{
return new RtlLiteral("old(" + GhostExpression(oldExp.E, inRecSpec, true) + ")");
}
else if (memberSelect != null && memberSelect.MemberName.EndsWith("?"))
{
string constructor = memberSelect.MemberName.Substring(0, memberSelect.MemberName.Length - 1);
constructor = dafnySpec.Compile_Constructor(memberSelect.Obj.Type, constructor, null, typeApply.typeArgs).AppName();
bool isSeq = memberSelect.Obj.Type.TypeName(null).StartsWith("Seq<");
return isSeq
? new RtlLiteral("is_" + constructor + "(" + G(memberSelect.Obj) + ")")
: new RtlLiteral("((" + G(memberSelect.Obj) + ") is " + constructor + ")");
}
else if (memberSelect != null && memberSelect.Member is Field && !memberSelect.Member.IsStatic && AppType(memberSelect.Obj.Type) is UserDefinedType
&& memberSelect.Member is DatatypeDestructor)
{
DatatypeDestructor field = (DatatypeDestructor) memberSelect.Member;
string constructor = dafnySpec.Compile_Constructor(memberSelect.Obj.Type,
field.EnclosingCtor.Name, null, typeApply.typeArgs).AppName();
bool isSeq = memberSelect.Obj.Type.TypeName(null).StartsWith("Seq<");
return new RtlLiteral("(" + memberSelect.MemberName + (isSeq ? "_" : "#") + constructor
+ "(" + G(memberSelect.Obj) + "))");
}
else if (memberSelect != null && memberSelect.Member is Field && DafnySpec.IsArrayType(AppType(memberSelect.Obj.Type))
&& memberSelect.MemberName == "Length")
{
return new RtlLiteral("(Arr_Length(" + G(memberSelect.Obj) + "))");
}
else if (memberSelect != null && memberSelect.Member is Field && memberSelect.Obj is ImplicitThisExpr)
{
//- we don't support objects yet, so interpret this as a global variable
return new RtlVar(GhostVar(memberSelect.MemberName), true, memberSelect.Type);
}
else if (seqSelect != null)
{
if (seqSelect.SelectOne && DafnySpec.IsArrayType(AppType(seqSelect.Seq.Type)))
{
return new RtlExpComputed(e => "fun_INTERNAL__array__elems__index("
+ (inRequiresOrOld ? "$absMem_old" : "$absMem") + "[" + e.args[0] + ".arrAbs], ("
+ e.args[1] + "))", new RtlExp[] { G(seqSelect.Seq), G(seqSelect.E0) });
}
else if (seqSelect.SelectOne)
{
return new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqSelect.Seq.Type), "Seq_Index"),
new RtlExp[] { G(seqSelect.Seq), G(seqSelect.E0) });
}
else
{
RtlExp seq = G(seqSelect.Seq);
if (DafnySpec.IsArrayType(AppType(seqSelect.Seq.Type)))
{
seq = new RtlApply(FunName("Seq__FromArray"), new RtlExp[] {
new RtlLiteral(inRequiresOrOld ? "$absMem_old" : "$absMem"), seq });
}
if (seqSelect.E1 != null)
{
seq = new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqSelect.Type), "Seq_Take"),
new RtlExp[] { seq, G(seqSelect.E1) });
}
if (seqSelect.E0 != null)
{
seq = new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqSelect.Type), "Seq_Drop"),
new RtlExp[] { seq, G(seqSelect.E0) });
}
return seq;
}
}
else if (seqUpdate != null)
{
if (seqUpdate.ResolvedUpdateExpr != null) {
return GhostExpressionRec(seqUpdate.ResolvedUpdateExpr, inRecSpec, inRequiresOrOld);
}
return new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqUpdate.Seq.Type), "Seq_Update"),
new RtlExp[] { G(seqUpdate.Seq), G(seqUpdate.Index), G(seqUpdate.Value) });
}
else if (seqDisplay != null)
{
RtlExp seq = new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqDisplay.Type), "Seq_Empty"), new RtlExp[0]);
foreach (Expression ei in seqDisplay.Elements)
{
seq = new RtlApply(dafnySpec.GetSeqOperationName(AppType(seqDisplay.Type), "Seq_Build"),
new RtlExp[] { seq, G(ei) });
}
return seq;
}
else
{
throw new Exception("not implemented: " + exp);
}
}