Skip to content

Commit

Permalink
Update names for adjusted visibility
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Oct 18, 2024
1 parent 80c4e24 commit 6e1f15f
Show file tree
Hide file tree
Showing 24 changed files with 532 additions and 532 deletions.
86 changes: 43 additions & 43 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
24 changes: 12 additions & 12 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 Down Expand Up @@ -387,7 +387,7 @@ public 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 @@ public 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 @@ public 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 @@ public 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 @@ public 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 @@ -1420,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 @@ -1567,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
10 changes: 5 additions & 5 deletions Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,10 @@ public partial class BoogieGenerator {
/// </summary>
void AddPrefixPredicateAxioms(PrefixPredicate pp) {
Contract.Requires(pp != null);
Contract.Requires(predef != null);
Contract.Requires(Predef != null);
var co = pp.ExtremePred;
var tok = pp.tok;
var etran = new ExpressionTranslator(this, predef, tok, pp);
var etran = new ExpressionTranslator(this, Predef, tok, pp);

var tyvars = MkTyParamBinders(GetTypeParams(pp), out var tyexprs);

Expand All @@ -63,7 +63,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
var prefixArgsLimited = new List<Bpl.Expr>(tyexprs);
var prefixArgsLimitedM = new List<Bpl.Expr>(tyexprs);
if (pp.IsFuelAware()) {
var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", predef.LayerType));
var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", Predef.LayerType));
var s = new Bpl.IdentifierExpr(tok, sV);
var succS = FunctionCall(tok, BuiltinFunction.LayerSucc, null, s);
bvs.Add(sV);
Expand All @@ -75,7 +75,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {

Bpl.Expr h;
if (pp.ReadsHeap) {
var heapIdent = new Bpl.TypedIdent(tok, predef.HeapVarName, predef.HeapType);
var heapIdent = new Bpl.TypedIdent(tok, Predef.HeapVarName, Predef.HeapType);
var bv = new Bpl.BoundVariable(tok, heapIdent);
h = new Bpl.IdentifierExpr(tok, bv);
bvs.Add(bv);
Expand Down Expand Up @@ -180,7 +180,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
moreBvs.Add(k);
var z = Bpl.Expr.Eq(kId,
pp.Ins[0].Type.IsBigOrdinalType
? (Bpl.Expr)FunctionCall(tok, "ORD#FromNat", predef.BigOrdinalType, Bpl.Expr.Literal(0))
? (Bpl.Expr)FunctionCall(tok, "ORD#FromNat", Predef.BigOrdinalType, Bpl.Expr.Literal(0))
: Bpl.Expr.Literal(0));
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
Bpl.Expr prefixLimitedBody = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimited);
Expand Down
Loading

0 comments on commit 6e1f15f

Please sign in to comment.