Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extract match and if verification #5843

Merged
merged 3 commits into from
Oct 18, 2024
Merged

Extract match and if verification #5843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
80c4e24
Extract if and match Boogie translation ccode into separate files
keyboardDrummer Oct 18, 2024
6e1f15f
Update names for adjusted visibility
keyboardDrummer Oct 18, 2024
304ff0f
Run formatter
keyboardDrummer Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
88 changes: 44 additions & 44 deletions Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
View file
Open in desktop

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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