Skip to content

Commit

Permalink
Extract if and match Boogie translation ccode into separate files
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Oct 18, 2024
1 parent 2db26d2 commit 80c4e24
Show file tree
Hide file tree
Showing 6 changed files with 311 additions and 290 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,7 @@ private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bp
// expressions, for instance), creates an assume statement in Boogie,
// and then adds information to track that assumption as a potential
// proof dependency.
private Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func<Bpl.Expr, Bpl.Expr> extendExpr,
public Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func<Bpl.Expr, Bpl.Expr> extendExpr,
string comment = null, bool warnWhenUnused = false, Bpl.QKeyValue attributes = null) {
var expr = etran.TrExpr(dafnyExpr);
var cmd = TrAssumeCmd(tok, extendExpr(expr), attributes);
Expand Down
55 changes: 3 additions & 52 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 @@ -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 @@ -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
89 changes: 11 additions & 78 deletions Source/DafnyCore/Verifier/BoogieGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ public void AddReferencedMember(MemberDecl m) {
}

FuelContext fuelContext = null;
IsAllocContext isAllocContext = null;
internal IsAllocContext isAllocContext = null;
Program program;

[ContractInvariantMethod]
Expand Down Expand Up @@ -209,7 +209,7 @@ bool InVerificationScope(RedirectingTypeDecl d) {
private VisibilityScope verificationScope;
private Dictionary<Declaration, Bpl.Function> declarationMapping = new();

readonly PredefinedDecls predef;
public readonly PredefinedDecls predef;

private TranslatorFlags flags;
private bool InsertChecksums { get { return flags.InsertChecksums; } }
Expand Down Expand Up @@ -2296,72 +2296,6 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List<
}


/// <summary>
/// If "declareLocals" is "false", then the locals are added only if they are new, that is, if
/// they don't already exist in "locals".
/// </summary>
Bpl.Expr CtorInvocation(MatchCase mc, Type sourceType, ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions, IsAllocType isAlloc, bool declareLocals = true) {
Contract.Requires(mc != null);
Contract.Requires(sourceType != null);
Contract.Requires(etran != null);
Contract.Requires(locals != null);
Contract.Requires(localTypeAssumptions != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

sourceType = sourceType.NormalizeExpand();
Contract.Assert(sourceType.TypeArgs.Count == mc.Ctor.EnclosingDatatype.TypeArgs.Count);
var subst = new Dictionary<TypeParameter, Type>();
for (var i = 0; i < mc.Ctor.EnclosingDatatype.TypeArgs.Count; i++) {
subst.Add(mc.Ctor.EnclosingDatatype.TypeArgs[i], sourceType.TypeArgs[i]);
}

List<Bpl.Expr> args = new List<Bpl.Expr>();
for (int i = 0; i < mc.Arguments.Count; i++) {
BoundVar p = mc.Arguments[i];
var nm = p.AssignUniqueName(currentDeclaration.IdGenerator);
var local = declareLocals ? null : locals.GetValueOrDefault(nm); // find previous local
if (local == null) {
local = locals.GetOrAdd(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, nm, TrType(p.Type))));
} else {
Contract.Assert(Bpl.Type.Equals(local.TypedIdent.Type, TrType(p.Type)));
}
var pFormalType = mc.Ctor.Formals[i].Type.Subst(subst);
var pIsAlloc = (isAlloc == ISALLOC) ? isAllocContext.Var(p) : NOALLOC;
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, local), pFormalType, etran, pIsAlloc);
if (wh != null) {
localTypeAssumptions.Add(TrAssumeCmd(p.tok, wh));
}
CheckSubrange(p.tok, new Bpl.IdentifierExpr(p.tok, local), pFormalType, p.Type, new IdentifierExpr(p.Tok, p), localTypeAssumptions);
args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), mc.Ctor.Formals[i].Type));
}
Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);
return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);
}

Bpl.Expr CtorInvocation(IToken tok, DatatypeCtor ctor, ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions) {
Contract.Requires(tok != null);
Contract.Requires(ctor != null);
Contract.Requires(etran != null);
Contract.Requires(locals != null);
Contract.Requires(localTypeAssumptions != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

// create local variables for the formals
var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("a#");
var args = new List<Bpl.Expr>();
foreach (Formal arg in ctor.Formals) {
Contract.Assert(arg != null);
var nm = varNameGen.FreshId(string.Format("#{0}#", args.Count));
var bv = locals.GetOrAdd(new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type))));
args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
}

Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(tok, ctor.FullName, predef.DatatypeType);
return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(id), args);
}

void AddCasePatternVarSubstitutions(CasePattern<BoundVar> pat, Bpl.Expr rhs, Dictionary<IVariable, Expression> substMap) {
Contract.Requires(pat != null);
Contract.Requires(rhs != null);
Expand Down Expand Up @@ -3132,7 +3066,7 @@ static Type NormalizeToVerificationTypeRepresentation(Type type) {
// Translates a type into the representation Boogie type,
// c.f. TypeToTy which translates a type to its Boogie expression
// to be used in $Is and $IsAlloc.
Bpl.Type TrType(Type type) {
public Bpl.Type TrType(Type type) {
Contract.Requires(type != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Type>() != null);
Expand Down Expand Up @@ -3429,7 +3363,7 @@ Bpl.Requires Requires(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr
return req;
}

Bpl.StmtList TrStmt2StmtList(BoogieStmtListBuilder builder,
public Bpl.StmtList TrStmt2StmtList(BoogieStmtListBuilder builder,
Statement block, Variables locals, ExpressionTranslator etran, bool introduceScope = false) {
Contract.Requires(builder != null);
Contract.Requires(block != null);
Expand Down Expand Up @@ -3621,7 +3555,7 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary<IVariable, Expression> sub
}


void AddComment(BoogieStmtListBuilder builder, Statement stmt, string comment) {
public void AddComment(BoogieStmtListBuilder builder, Statement stmt, string comment) {
Contract.Requires(builder != null);
Contract.Requires(stmt != null);
Contract.Requires(comment != null);
Expand Down Expand Up @@ -3796,7 +3730,7 @@ Bpl.Expr MkIsAlloc(Bpl.Expr x, Bpl.Expr t, Bpl.Expr h, bool box = false) {
/// To do this in Dafny, Dafny would have to compute loop targets, which is better done in Boogie (which
/// already has to do it).
/// </summary>
Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran, IsAllocType alloc,
public Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran, IsAllocType alloc,
bool allocatednessOnly = false, bool alwaysUseSymbolicName = false) {
Contract.Requires(tok != null);
Contract.Requires(x != null);
Expand Down Expand Up @@ -4004,7 +3938,7 @@ Bpl.Expr GetSubrangeCheck(
return cre;
}

void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType, Expression source, BoogieStmtListBuilder builder, string errorMsgPrefix = "") {
public void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType, Expression source, BoogieStmtListBuilder builder, string errorMsgPrefix = "") {
Contract.Requires(tok != null);
Contract.Requires(bSource != null);
Contract.Requires(sourceType != null);
Expand Down Expand Up @@ -4063,7 +3997,7 @@ void CreateMapComprehensionProjectionFunctions(MapComprehension mc) {
}

int projectionFunctionCount = 0;
private Declaration currentDeclaration;
public Declaration currentDeclaration;

// ----- Expression ---------------------------------------------------------------------------

Expand Down Expand Up @@ -4441,10 +4375,8 @@ public static FuelContext PopFuelContext() {
}

}

internal enum IsAllocType { ISALLOC, NOALLOC, NEVERALLOC }; // NEVERALLOC is like NOALLOC, but overrides AlwaysAlloc
static IsAllocType ISALLOC { get { return IsAllocType.ISALLOC; } }
static IsAllocType NOALLOC { get { return IsAllocType.NOALLOC; } }
public static IsAllocType ISALLOC { get { return IsAllocType.ISALLOC; } }
public static IsAllocType NOALLOC { get { return IsAllocType.NOALLOC; } }
private bool DisableNonLinearArithmetic => DetermineDisableNonLinearArithmetic(forModule, options);
private int ArithmeticSolver {
get {
Expand Down Expand Up @@ -4870,3 +4802,4 @@ public Expr GetRevealConstant(Function f) {
public enum AssertMode { Keep, Assume, Check }
}

public enum IsAllocType { ISALLOC, NOALLOC, NEVERALLOC }; // NEVERALLOC is like NOALLOC, but overrides AlwaysAlloc
Loading

0 comments on commit 80c4e24

Please sign in to comment.