Skip to content

Commit

Permalink
Remove function-context-height variable in Boogie encoding (#6046)
Browse files Browse the repository at this point in the history 
Because `CanCall` is now used everywhere, the Boogie variable
`$FunctionContextHeight` is no longer needed.

This PR also removes the variable `$ModuleContextHeight`, which has been
unused for some time now.

Depends on #6045

<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
@RustanLeino
RustanLeino authored Jan 17, 2025
1 parent 6afa6d5 commit c9cffc3
Show file tree
Hide file tree
Showing 19 changed files with 988 additions and 1,111 deletions.
8 changes: 0 additions & 8 deletions Source/DafnyCore/DafnyPrelude.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -480,14 +480,6 @@ axiom (forall o: ORDINAL, m,n: int ::
(0 <= m - n ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m-n))) &&
(m - n <= 0 ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(n-m))));

// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
// ---------------------------------------------------------------

// used to make sure function axioms are not used while their consistency is being checked
const $ModuleContextHeight: int;
const $FunctionContextHeight: int;

// ---------------------------------------------------------------
// -- Layers of function encodings -------------------------------
// ---------------------------------------------------------------
Expand Down
8 changes: 0 additions & 8 deletions Source/DafnyCore/Prelude/PreludeCore.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -480,14 +480,6 @@ axiom (forall o: ORDINAL, m,n: int ::
(0 <= m - n ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m-n))) &&
(m - n <= 0 ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(n-m))));

// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
// ---------------------------------------------------------------

// used to make sure function axioms are not used while their consistency is being checked
const $ModuleContextHeight: int;
const $FunctionContextHeight: int;

// ---------------------------------------------------------------
// -- Layers of function encodings -------------------------------
// ---------------------------------------------------------------
Expand Down
14 changes: 0 additions & 14 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,20 +290,6 @@ public Boogie.Expr ArbitraryValue(Type type) {
}
}

public Boogie.IdentifierExpr FunctionContextHeight() {
Contract.Ensures(Contract.Result<Boogie.IdentifierExpr>().Type != null);
return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int);
}

public Boogie.Expr HeightContext(ICallable m) {
Contract.Requires(m != null);
// free requires fh == FunctionContextHeight;
var module = m.EnclosingModule;
Boogie.Expr context =
Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight());
return context;
}

public Expression GetSubstitutedBody(LetExpr e) {
Contract.Requires(e != null);
Contract.Requires(e.Exact);
Expand Down
30 changes: 9 additions & 21 deletions Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,15 +37,10 @@ public partial class BoogieGenerator {
/// forall args :: (QQQ k: nat :: P#[k](args)) ==> P(args)
/// forall args,k :: k == 0 ==> NNN P#[k](args)
/// where "args" is "heap, formals". In more details:
/// AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
/// AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
/// AXIOM_ACTIVATION ==> forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
/// AXIOM_ACTIVATION ==> forall args,k,m :: args-have-appropriate-values && 0 ATMOST k LESS m ==> (P#[k](args) EEE P#[m](args)) (*)
/// where
/// AXIOM_ACTIVATION
/// means:
/// mh LESS ModuleContextHeight ||
/// (mh == ModuleContextHeight && fh ATMOST FunctionContextHeight)
/// forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
/// forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
/// forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
/// forall args,k,m :: args-have-appropriate-values && 0 ATMOST k LESS m ==> (P#[k](args) EEE P#[m](args)) (*)
/// There is also a specialized version of (*) for least predicates.
/// </summary>
void AddPrefixPredicateAxioms(PrefixPredicate pp) {
Expand Down Expand Up @@ -155,8 +150,6 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
var prefixAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);

var activation = AxiomActivation(pp, etran);

// forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
var tr = BplTrigger(prefixAppl);
var qqqK = pp.ExtremePred is GreatestPredicate
Expand All @@ -166,13 +159,11 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
kWhere == null ? prefixAppl : BplAnd(kWhere, prefixAppl));
tr = BplTriggerHeap(this, tok, coAppl, pp.ReadsHeap ? null : h);
var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), qqqK));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, allS),
"1st prefix predicate axiom for " + pp.FullSanitizedName));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, allS, "1st prefix predicate axiom for " + pp.FullSanitizedName));

// forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, qqqK), coAppl));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, allS),
"2nd prefix predicate axiom"));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, allS, "2nd prefix predicate axiom"));

// forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
var moreBvs = new List<Variable>();
Expand All @@ -188,8 +179,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {

var trigger = BplTriggerHeap(this, prefixLimitedBody.tok, prefixLimitedBody, pp.ReadsHeap ? null : h);
var trueAtZero = new Bpl.ForallExpr(tok, moreBvs, trigger, BplImp(BplAnd(ante, z), prefixLimited));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, trueAtZero),
"3rd prefix predicate axiom"));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, trueAtZero, "3rd prefix predicate axiom"));

#if WILLING_TO_TAKE_THE_PERFORMANCE_HIT
// forall args,k,m :: args-have-appropriate-values && 0 <= k <= m ==> (P#[k](args) EEE P#[m](args))
Expand All @@ -211,8 +201,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {

var trigger2 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, prefixPred_M });
var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger2, BplImp(smaller, direction));
AddRootAxiom(new Bpl.Axiom(tok, BplImp(activation, monotonicity),
"prefix predicate monotonicity axiom"));
AddRootAxiom(new Bpl.Axiom(tok, monotonicity, "prefix predicate monotonicity axiom"));
#endif
// A more targeted monotonicity axiom used to increase the power of automation for proving the limit case for
// least predicates that have more than one focal-predicate term.
Expand All @@ -237,8 +226,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {

var trigger3 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, kLessLimit, mLessLimit });
var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger3, BplImp(kLessM, direction));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, monotonicity),
"targeted prefix predicate monotonicity axiom"));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, monotonicity, "targeted prefix predicate monotonicity axiom"));
}
}

Expand Down
2 changes: 0 additions & 2 deletions Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -188,8 +188,6 @@ void AddWellformednessCheck(ConstantField decl) {

// the procedure itself
var req = new List<Bpl.Requires>();
// free requires mh == ModuleContextHeight && fh == TypeContextHeight;
req.Add(FreeRequires(decl.Origin, etran.HeightContext(decl), null));
foreach (var typeBoundAxiom in TypeBoundAxioms(decl.Origin, decl.EnclosingClass.TypeArgs)) {
req.Add(FreeRequires(decl.Origin, typeBoundAxiom, null));
}
Expand Down
4 changes: 0 additions & 4 deletions Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -372,13 +372,9 @@ private List<Variable> GetWellformednessProcedureOutParameters(Function f, Expre

private List<Bpl.Requires> GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran) {
var requires = new List<Bpl.Requires>();
// free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
requires.Add(generator.FreeRequires(f.Origin, etran.HeightContext(f), null));

foreach (var typeBoundAxiom in generator.TypeBoundAxioms(f.Origin, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) {
requires.Add(generator.Requires(f.Origin, true, null, typeBoundAxiom, null, null, null));
}

return requires;
}

Expand Down
51 changes: 5 additions & 46 deletions Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,29 +87,16 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
// return type and postconditions
//
// axiom // consequence axiom
// AXIOM_ACTIVATION
// ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(s, args) }
// f#canCall(args) || USE_VIA_CONTEXT
// f#canCall(args)
// ==>
// ens &&
// OlderCondition &&
// f(s, args)-has-the-expected type);
//
// where:
//
// AXIOM_ACTIVATION
// means:
// fh <= FunctionContextHeight
//
// USE_VIA_CONTEXT
// fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,formals)
//
// OlderCondition is added if the function has some 'older' parameters.
//
// Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
Expand Down Expand Up @@ -233,10 +220,6 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
foreach (AttributedExpression req in ConjunctsOf(f.Req)) {
pre = BplAnd(pre, etran.TrExpr(req.E));
}
// useViaContext: fh < FunctionContextHeight
Expr useViaContext = !(InVerificationScope(f) || (f.EnclosingClass is TraitDecl))
? Bpl.Expr.True
: Bpl.Expr.Lt(Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
// useViaCanCall: f#canCall(args)
var canCallFuncID = new Bpl.IdentifierExpr(f.Origin, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
var useViaCanCall = new Bpl.NAryExpr(f.Origin, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
Expand Down Expand Up @@ -268,10 +251,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis

Bpl.Expr axBody = BplImp(ante, post);
Bpl.Expr ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), formals, null, tr, axBody);
var activate = AxiomActivation(f, etran);
if (RemoveLit(axBody) != Bpl.Expr.True) {
AddOtherDefinition(boogieFunction, new Bpl.Axiom(f.Origin, BplImp(activate, ax),
"consequence axiom for " + f.FullSanitizedName));
AddOtherDefinition(boogieFunction, new Bpl.Axiom(f.Origin, ax, "consequence axiom for " + f.FullSanitizedName));
}

if (f.ResultType.MayInvolveReferences) {
Expand All @@ -289,8 +270,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), formals, null, BplTrigger(whr), axBody);

if (RemoveLit(axBody) != Bpl.Expr.True) {
var comment = "alloc consequence axiom for " + f.FullSanitizedName;
var allocConsequenceAxiom = new Bpl.Axiom(f.Origin, BplImp(activate, ax), comment);
var allocConsequenceAxiom = new Bpl.Axiom(f.Origin, ax, "alloc consequence axiom for " + f.FullSanitizedName);
AddOtherDefinition(boogieFunction, allocConsequenceAxiom);
}
}
Expand All @@ -310,33 +290,13 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
// This method generates the Definition Axiom, suitably modified according to the optional "lits".
//
// axiom // definition axiom
// AXIOM_ACTIVATION
// ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(Succ(s), args) } // (*)
// (f#canCall(args) || USE_VIA_CONTEXT)
// f#canCall(args)
// ==>
// BODY-can-make-its-calls &&
// f(Succ(s), args) == BODY); // (*)
//
// where:
//
// AXIOM_ACTIVATION
// for visibility==ForeignModuleOnly, means:
// true
// for visibility==IntraModuleOnly, means:
// fh <= FunctionContextHeight
//
// USE_VIA_CONTEXT
// for visibility==ForeignModuleOnly, means:
// GOOD_PARAMETERS
// for visibility==IntraModuleOnly, means:
// fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,formals)
//
// NOTE: this is lifted out to a #requires function for intra module calls,
// and used in the function pseudo-handles for top level functions.
// For body-less functions, this is emitted when body is null.
Expand Down Expand Up @@ -609,7 +569,6 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {

Bpl.Expr ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), forallFormals, kv, tr,
BplImp(ante, tastyVegetarianOption));
var activate = AxiomActivation(f, etran);
string comment;
comment = "definition axiom for " + f.FullSanitizedName;
if (lits != null) {
Expand All @@ -625,7 +584,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
} else {
comment += " (opaque)";
}
var axe = new Axiom(f.Origin, BplImp(activate, ax), comment) {
var axe = new Axiom(f.Origin, ax, comment) {
CanHide = true
};
if (proofDependencies == null) {
Expand Down
4 changes: 0 additions & 4 deletions Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,10 +79,6 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
var mod = new List<Bpl.IdentifierExpr>();
var ens = new List<Bpl.Ensures>();
// FREE PRECONDITIONS
if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition
// free requires mh == ModuleContextHeight && fh = FunctionContextHeight;
req.Add(FreeRequires(iter.Origin, etran.HeightContext(iter), null));
}
mod.Add(etran.HeapCastToIdentifierExpr);

if (kind != MethodTranslationKind.SpecWellformedness) {
Expand Down
Loading

0 comments on commit c9cffc3

Please sign in to comment.