Skip to content

Commit

Permalink
Extract match and if verification (#5843)
Browse files Browse the repository at this point in the history 
### Description
- Extract match and if verification

### How has this been tested?
Pure refactoring, no additional tests needed

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Oct 18, 2024
1 parent 2db26d2 commit 7681e01
Show file tree
Hide file tree
Showing 25 changed files with 836 additions and 815 deletions.
88 changes: 44 additions & 44 deletions Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
View file

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<VarDeclStmt> prevGhostLocals,
Contract.Requires(cce.NonNullElements(dafny1));
Contract.Requires(cce.NonNullElements(ee0));
Contract.Requires(cce.NonNullElements(ee1));
Contract.Requires(predef != null);
Contract.Requires(Predef != null);
Contract.Requires(dafny0.Count == dafny1.Count && dafny0.Count == ee0.Count && ee0.Count == ee1.Count);
Contract.Requires(builder == null || suffixMsg != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
Expand Down Expand Up @@ -246,7 +246,7 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
Contract.Requires(ty1 != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
Contract.Requires(predef != null);
Contract.Requires(Predef != null);
Contract.Ensures(Contract.ValueAtReturn(out less) != null);
Contract.Ensures(Contract.ValueAtReturn(out atmost) != null);
Contract.Ensures(Contract.ValueAtReturn(out eq) != null);
Expand Down Expand Up @@ -314,8 +314,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
b1 = e1;
} else {
// for maps, compare their domains as sets
b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e1);
b0 = FunctionCall(tok, BuiltinFunction.MapDomain, Predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.MapDomain, Predef.MapType, e1);
}
eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, b0, b1);
less = ProperSubset(tok, b0, b1);
Expand All @@ -330,8 +330,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
} else {
Contract.Assert(!((MapType)ty0).Finite);
// for maps, compare their domains as sets
b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e1);
b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, Predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, Predef.MapType, e1);
}
eq = FunctionCall(tok, BuiltinFunction.ISetEqual, null, b0, b1);
less = Bpl.Expr.False;
Expand Down Expand Up @@ -366,8 +366,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
} else {
// reference type
Contract.Assert(ty0.IsRefType); // otherwise, unexpected type
var b0 = Bpl.Expr.Neq(e0, predef.Null);
var b1 = Bpl.Expr.Neq(e1, predef.Null);
var b0 = Bpl.Expr.Neq(e0, Predef.Null);
var b1 = Bpl.Expr.Neq(e1, Predef.Null);
eq = BplIff(b0, b1);
less = BplAnd(Bpl.Expr.Not(b0), b1);
atmost = BplImp(b0, b1);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ void AssumeCanCallForByMethodDecl(Method method, BoogieStmtListBuilder builder)
// fn == new FunctionCallExpr(tok, f.Name, receiver, tok, tok, f.Formals.ConvertAll(Expression.CreateIdentExpr));
Bpl.IdentifierExpr canCallFuncID =
new Bpl.IdentifierExpr(method.tok, method.FullSanitizedName + "#canCall", Bpl.Type.Bool);
var etran = new ExpressionTranslator(this, predef, method.tok, method);
var etran = new ExpressionTranslator(this, Predef, method.tok, method);
List<Bpl.Expr> args = arguments.Select(arg => etran.TrExpr(arg)).ToList();
var formals = MkTyParamBinders(GetTypeParams(method), out var tyargs);
if (method.FunctionFromWhichThisIsByMethodDecl.ReadsHeap) {
Expand Down
14 changes: 7 additions & 7 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -390,7 +390,7 @@ public Boogie.Expr TrExpr(Expression expr) {
args.Add(Old.HeapExpr);
}
foreach (var heapAtLabel in e.HeapAtLabels) {
var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.predef.HeapType, out var ve);
var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.Predef.HeapType, out var ve);
args.Add(ve);
}
foreach (var arg in e.Args) {
Expand Down Expand Up @@ -1642,7 +1642,7 @@ public Boogie.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, List<Variable
Boogie.Expr typeAntecedent = Boogie.Expr.True;
var i = 0;
foreach (BoundVar bv in boundVars) {
var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type));
var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type));
Boogie.Variable bvar;
if (translateAsLocals) {
bvar = new Boogie.LocalVariable(bv.tok, tid);
Expand All @@ -1666,7 +1666,7 @@ public Boogie.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, List<Variable

var varsAndAntecedents = new List<Tuple<Boogie.Variable, Boogie.Expr>>();
foreach (BoundVar bv in boundVars) {
var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type));
var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type));
var bvar = new Boogie.BoundVariable(bv.tok, tid);
var wh = BoogieGenerator.GetWhereClause(bv.tok, new Boogie.IdentifierExpr(bv.tok, bvar), bv.Type, this, NOALLOC);
varsAndAntecedents.Add(Tuple.Create<Boogie.Variable, Boogie.Expr>(bvar, wh));
Expand All @@ -1683,10 +1683,10 @@ public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variabl
Boogie.Expr typeAntecedent = Boogie.Expr.True;
foreach (BoundVar bv in boundVars) {
var newBoundVar = new BoundVar(bv.tok, bv.Name, bv.Type);
IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator));
IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator));
ie.Var = newBoundVar; ie.Type = ie.Var.Type; // resolve ie here
substMap.Add(bv, ie);
Boogie.Variable bvar = new Boogie.BoundVariable(newBoundVar.tok, new Boogie.TypedIdent(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(newBoundVar.Type)));
Boogie.Variable bvar = new Boogie.BoundVariable(newBoundVar.tok, new Boogie.TypedIdent(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator), BoogieGenerator.TrType(newBoundVar.Type)));
bvars.Add(bvar);
var bIe = new Boogie.IdentifierExpr(bvar.tok, bvar);
Boogie.Expr wh = BoogieGenerator.GetWhereClause(bv.tok, bIe, newBoundVar.Type, this, NOALLOC);
Expand Down Expand Up @@ -2084,7 +2084,7 @@ public Boogie.Expr GoodRef(IToken tok, Boogie.Expr e, Type type) {
public Expr CanCallAssumption(Expression expr) {
Contract.Requires(expr != null);
Contract.Requires(this != null);
Contract.Requires(BoogieGenerator.predef != null);
Contract.Requires(BoogieGenerator.Predef != null);
Contract.Ensures(Contract.Result<Boogie.Expr>() != null);

if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
Expand Down Expand Up @@ -2249,7 +2249,7 @@ public Expr CanCallAssumption(Expression expr) {
var bvarsAndAntecedents = new List<Tuple<Boogie.Variable, Boogie.Expr>>();
var varNameGen = BoogieGenerator.CurrentIdGenerator.NestedFreshIdGenerator("$l#");

Boogie.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), BoogieGenerator.predef.HeapType, out heap);
Boogie.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), BoogieGenerator.Predef.HeapType, out heap);
var et = new ExpressionTranslator(this, heap);

Dictionary<IVariable, Expression> subst = new Dictionary<IVariable, Expression>();
Expand Down
79 changes: 15 additions & 64 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, Varia
Contract.Requires(locals != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
Contract.Requires(predef != null);
Contract.Requires(Predef != null);
if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
Expand Down Expand Up @@ -254,7 +254,7 @@ public void CheckWellformed(Expression expr, WFOptions wfOptions, Variables loca
Contract.Requires(locals != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
Contract.Requires(predef != null);
Contract.Requires(Predef != null);
CheckWellformedWithResult(expr, wfOptions, locals, builder, etran, null);
}

Expand All @@ -265,7 +265,7 @@ public void CheckWellformed(Expression expr, WFOptions wfOptions, Variables loca
/// assume the equivalent of "result == expr".
/// See class WFOptions for descriptions of the specified options.
/// </summary>
void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran,
AddResultCommands addResultCommands) {
var origOptions = wfOptions;
Expand Down Expand Up @@ -387,7 +387,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
CheckWellformed(e.Seq, wfOptions, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
if (eSeqType.IsArrayType) {
builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, predef.Null),
builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, Predef.Null),
new NonNull("array", e.Seq), builder.Context));
if (etran.UsesOldHeap) {
builder.Add(Assert(GetToken(e.Seq), MkIsAlloc(seq, eSeqType, etran.HeapExpr),
Expand All @@ -400,7 +400,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
e0 = etran.TrExpr(e.E0);
CheckWellformed(e.E0, wfOptions, locals, builder, etran);
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
Bpl.Expr inDomain = FunctionCall(selectExpr.tok, f, finite ? predef.MapType : predef.IMapType, seq);
Bpl.Expr inDomain = FunctionCall(selectExpr.tok, f, finite ? Predef.MapType : Predef.IMapType, seq);
inDomain = Bpl.Expr.Select(inDomain, BoxIfNecessary(e.tok, e0, e.E0.Type));
builder.Add(Assert(GetToken(expr), inDomain,
new ElementInDomain(e.Seq, e.E0), builder.Context, wfOptions.AssertKv));
Expand Down Expand Up @@ -467,7 +467,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
MultiSelectExpr e = selectExpr;
CheckWellformed(e.Array, wfOptions, locals, builder, etran);
Bpl.Expr array = etran.TrExpr(e.Array);
builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, predef.Null),
builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, Predef.Null),
new NonNull("array", e.Array), builder.Context));
if (etran.UsesOldHeap) {
builder.Add(Assert(GetToken(e.Array), MkIsAlloc(array, e.Array.Type, etran.HeapExpr),
Expand Down Expand Up @@ -696,12 +696,12 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
Type et = p.Type.Subst(e.GetTypeArgumentSubstitutions());
LocalVariable local = new LocalVariable(p.RangeToken, "##" + p.Name, et, p.IsGhost);
local.type = local.SyntacticType; // resolve local here
var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)) {
var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator)) {
Var = local
};
ie.Type = ie.Var.Type; // resolve ie here
substMap.Add(p, ie);
locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))));
locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(local.Type))));
Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
Expression ee = e.Args[i];
directSubstMap.Add(p, ee);
Expand Down Expand Up @@ -959,7 +959,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
nonNull = Bpl.Expr.True;
} else {
Contract.Assert(ty.IsRefType);
nonNull = Bpl.Expr.Neq(r, predef.Null);
nonNull = Bpl.Expr.Neq(r, Predef.Null);
builder.Add(Assert(GetToken(fe.E), BplImp(ante, nonNull),
new NonNull(description, fe.E, description != "object"), builder.Context));
}
Expand Down Expand Up @@ -1173,7 +1173,7 @@ void CheckOperand(Expression operand) {
var comprehensionEtran = etran;
if (lam != null) {
// Havoc heap
locals.GetOrAdd(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), predef.HeapType, out var lambdaHeap));
locals.GetOrAdd(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), Predef.HeapType, out var lambdaHeap));
comprehensionEtran = new ExpressionTranslator(comprehensionEtran, lambdaHeap);
nextBuilder.Add(new HavocCmd(e.tok, Singleton((Bpl.IdentifierExpr)comprehensionEtran.HeapExpr)));
nextBuilder.Add(new AssumeCmd(e.tok, FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, comprehensionEtran.HeapExpr)));
Expand Down Expand Up @@ -1313,7 +1313,7 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
break;
}
case MatchExpr matchExpr:
TrMatchExpr(matchExpr, wfOptions, locals, builder, etran, addResultCommands);
MatchStatementVerifier.TrMatchExpr(this, matchExpr, wfOptions, locals, builder, etran, addResultCommands);
addResultCommands = null;
break;
case DatatypeUpdateExpr updateExpr: {
Expand Down Expand Up @@ -1380,55 +1380,6 @@ public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Exp
builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType)));
}

private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, Variables locals,
BoogieStmtListBuilder builder, ExpressionTranslator etran, AddResultCommands addResultCommands) {
FillMissingCases(me);

CheckWellformed(me.Source, wfOptions, locals, builder, etran);
Bpl.Expr src = etran.TrExpr(me.Source);
Bpl.IfCmd ifCmd = null;
BoogieStmtListBuilder elsBldr = new BoogieStmtListBuilder(this, options, builder.Context);
elsBldr.Add(TrAssumeCmd(me.tok, Bpl.Expr.False));
StmtList els = elsBldr.Collect(me.tok);
foreach (var missingCtor in me.MissingCases) {
// havoc all bound variables
var b = new BoogieStmtListBuilder(this, options, builder.Context);
Variables newLocals = new();
Bpl.Expr r = CtorInvocation(me.tok, missingCtor, etran, newLocals, b);
locals.AddRange(newLocals.Values);

if (newLocals.Count != 0) {
List<Bpl.IdentifierExpr> havocIds = new List<Bpl.IdentifierExpr>();
foreach (Variable local in newLocals.Values) {
havocIds.Add(new Bpl.IdentifierExpr(local.tok, local));
}

builder.Add(new Bpl.HavocCmd(me.tok, havocIds));
}

String missingStr = me.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles().ToString();
b.Add(Assert(GetToken(me), Bpl.Expr.False,
new MatchIsComplete("expression", missingStr), builder.Context));

Bpl.Expr guard = Bpl.Expr.Eq(src, r);
ifCmd = new Bpl.IfCmd(me.tok, guard, b.Collect(me.tok), ifCmd, els);
els = null;
}

for (int i = me.Cases.Count; 0 <= --i;) {
MatchCaseExpr mc = me.Cases[i];
var b = new BoogieStmtListBuilder(this, options, builder.Context);
Bpl.Expr ct = CtorInvocation(mc, me.Source.Type, etran, locals, b, NOALLOC, false);
// generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...

CheckWellformedWithResult(mc.Body, wfOptions, locals, b, etran, addResultCommands);
ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els);
els = null;
}

builder.Add(ifCmd);
}

private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Variables locals,
BoogieStmtListBuilder builder, ExpressionTranslator etran, AddResultCommands addResultCommands) {

Expand Down Expand Up @@ -1469,9 +1420,9 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Var
void BuildWithHeapAs(IToken token, Bpl.Expr temporaryHeap, string heapVarSuffix, Variables locals,
BoogieStmtListBuilder builder, System.Action build) {
var suffix = CurrentIdGenerator.FreshId(heapVarSuffix);
var tmpHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "Heap$" + suffix, predef.HeapType)));
var tmpHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "Heap$" + suffix, Predef.HeapType)));
var tmpHeap = new Bpl.IdentifierExpr(token, tmpHeapVar);
var generalEtran = new ExpressionTranslator(this, predef, token, null);
var generalEtran = new ExpressionTranslator(this, Predef, token, null);
var theHeap = generalEtran.HeapCastToIdentifierExpr;

// tmpHeap := $Heap;
Expand Down Expand Up @@ -1527,7 +1478,7 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp
}
}

delegate void AddResultCommands(BoogieStmtListBuilder builder, Expression result);
public delegate void AddResultCommands(BoogieStmtListBuilder builder, Expression result);

void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Variables locals,
BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs, AddResultCommands addResultCommands) {
Expand Down Expand Up @@ -1616,7 +1567,7 @@ void CheckFrameWellFormed(WFOptions wfo, List<FrameExpression> fes, Variables lo
foreach (var fe in fes) {
CheckWellformed(fe.E, wfo, locals, builder, etran);
if (fe.Field != null && fe.E.Type.IsRefType) {
builder.Add(Assert(fe.tok, Bpl.Expr.Neq(etran.TrExpr(fe.E), predef.Null), new FrameDereferenceNonNull(fe.E), builder.Context));
builder.Add(Assert(fe.tok, Bpl.Expr.Neq(etran.TrExpr(fe.E), Predef.Null), new FrameDereferenceNonNull(fe.E), builder.Context));
}
}
}
Expand Down
Loading

0 comments on commit 7681e01

Please sign in to comment.