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

fix: Fill in missing type substitutions #2984

Merged
merged 17 commits into from
Nov 28, 2022
Merged

fix: Fill in missing type substitutions #2984

Show file tree
Hide file tree
Changes from 15 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
443732f
chore: Rename local variables to something more readable
RustanLeino Nov 3, 2022
aef58cf
fix: Clone extreme-predicate body when making prefix predicate
RustanLeino Nov 3, 2022
1c90050
fix: Substitute types in Substitute(Expression)
RustanLeino Nov 3, 2022
dfa8ad6
Add tests
RustanLeino Nov 3, 2022
1baa9bf
Make sure to collect triggers on the cloned prefix-predicate Body
RustanLeino Nov 3, 2022
8b69cbf
Add release notes
RustanLeino Nov 3, 2022
685a806
Merge branch 'master' into issue-2947
RustanLeino Nov 4, 2022
7e67cd6
When there’s no focal predicate, say so more clearly
RustanLeino Nov 4, 2022
a74bae0
Don’t emit trigger warnings for extreme-into-prefix rewrites
RustanLeino Nov 4, 2022
aa41e2f
Merge branch 'master' into issue-2947
RustanLeino Nov 4, 2022
e6fadca
Merge branch 'master' into issue-2947
RustanLeino Nov 23, 2022
c8d660d
Merge branch 'master' into issue-2947
RustanLeino Nov 23, 2022
8344691
Improved code re PrefixLemma and PrefixPredicate declarations
RustanLeino Nov 24, 2022
cb857c6
chore: Fix spelling in code
RustanLeino Nov 24, 2022
b98fba5
Merge branch 'master' into issue-2947
RustanLeino Nov 24, 2022
c6a91ee
Merge branch 'master' into issue-2947
keyboardDrummer Nov 24, 2022
b0d0eaf
Merge branch 'master' into issue-2947
RustanLeino Nov 28, 2022
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
3 changes: 1 addition & 2 deletions Source/DafnyCore/AST/Printer.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -656,8 +656,7 @@ public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingP
} else if (m is Function) {
if (state != 0) { wr.WriteLine(); }
PrintFunction((Function)m, indent, false);
var fixp = m as ExtremePredicate;
if (fixp != null && fixp.PrefixPredicate != null) {
if (m is ExtremePredicate fixp && fixp.PrefixPredicate != null) {
Indent(indent); wr.WriteLine("/*** (note, what is printed here does not show substitutions of calls to prefix predicates)");
PrintFunction(fixp.PrefixPredicate, indent, false);
Indent(indent); wr.WriteLine("***/");
Expand Down
118 changes: 72 additions & 46 deletions Source/DafnyCore/AST/TopLevelDeclarations.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,6 @@ public override string ToString() {
public IToken NameToken => tok;
public virtual IEnumerable<INode> Children {
get {

return Enumerable.Empty<INode>();
}
}
Expand Down Expand Up @@ -352,6 +351,11 @@ public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened,
public abstract object Dereference();

public int? ResolvedHash { get; set; }

public override bool IsEssentiallyEmpty() {
// A module or import is considered "essentially empty" to its parents, but the module is going to be resolved by itself.
return true;
}
}
// Represents module X { ... }
public class LiteralModuleDecl : ModuleDecl {
Expand Down Expand Up @@ -837,44 +841,50 @@ public static IEnumerable<TopLevelDeclWithMembers> AllTypesWithMembers(List<TopL
/// declarations.
/// Note, an iterator declaration is a type, in this sense.
/// Note, if the given list are the top-level declarations of a module, the yield will include
/// greatest lemmas but not their associated prefix lemmas (which are tucked into the greatest lemma's
/// .PrefixLemma field).
/// extreme predicates/lemmas but not their associated prefix predicates/lemmas (which are tucked
/// into the extreme predicate/lemma's PrefixPredicate/PrefixLemma field).
/// </summary>
public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declarations) {
foreach (var d in declarations) {
var cl = d as TopLevelDeclWithMembers;
if (cl != null) {
foreach (var member in cl.Members) {
var clbl = member as ICallable;
if (clbl != null && !(member is ConstantField)) {
yield return clbl;
if (clbl is Function f && f.ByMethodDecl != null) {
yield return f.ByMethodDecl;
}
if (d is TopLevelDeclWithMembers cl) {
foreach (var member in cl.Members.Where(member => member is ICallable and not ConstantField)) {
yield return (ICallable)member;
if (member is Function { ByMethodDecl: { } } f) {
yield return f.ByMethodDecl;
}
}
}
}
}

/// <summary>
/// Yields all functions and methods that are members of some type in the given list of
/// declarations, including prefix lemmas and prefix predicates.
/// </summary>
public static IEnumerable<ICallable> AllCallablesIncludingPrefixDeclarations(List<TopLevelDecl> declarations) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd like to have each language construct be as independent as possible. For extreme lemmas and predicates this would also mean they have mostly outwards references. Would it be possible to achieve this?

Would it be possible to translate extremes to their prefix versions and then forget about the originals? Or maybe create the prefix versions next to the originals?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need both. A program needs the extremes, since that's what you'll ultimately will use for the property you want. The prefix predicates/lemmas give a way to prove properties about the extremes, so they are also needed.

Actually, the more surprising thing (to me) is that AllCallables (which excludes the prefix versions) is used so many times.

Copy link
Member

@keyboardDrummer keyboardDrummer Nov 6, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need both. A program needs the extremes, since that's what you'll ultimately will use for the property you want. The prefix predicates/lemmas give a way to prove properties about the extremes, so they are also needed.

Sure, but can we place both side by side instead of introducing AllCallablesIncludingPrefixDeclarations?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand. The AllCallablesIncludingPrefixDeclarations and AllCallables properties are declared side by side. Are you perhaps suggesting that the prefix predicates/lemmas be placed in the list of the enclosing module's top-level-decls (rather than being linked off the corresponding extreme predicate/lemma)? (And if so, do you think that will improve the organization for other parts of the implementation?)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you perhaps suggesting that the prefix predicates/lemmas be placed in the list of the enclosing module's top-level-decls

Yes that's what I meant.

And if so, do you think that will improve the organization for other parts of the implementation?

I think so. If I understand extreme lemma's correctly, they behave similarly to as if you'd written the prefix lemma manually next to them. Also, looking at usages of ExtremeLemma.PrefixLemma gives the impression there's a handful of snippets that handle the PrefixLemma as if it was a top level method.

Code like this:

    internal override void PostResolveIntermediate(ModuleDefinition m) {
      var forallvisiter = new ForAllStmtVisitor(Reporter);
      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
        forallvisiter.Visit(decl, true);
        if (decl is ExtremeLemma) {
          var prefixLemma = ((ExtremeLemma)decl).PrefixLemma;
          if (prefixLemma != null) {
            forallvisiter.Visit(prefixLemma, true);
          }
        }
      }

    }

or this:

              if (member is ExtremeLemma) {
                var method = (ExtremeLemma)member;
                ProcessMethodExpressions(method);
                ComputeLemmaInduction(method.PrefixLemma);
                ProcessMethodExpressions(method.PrefixLemma);
              } else if (member is Method) {
                var method = (Method)member;
                ComputeLemmaInduction(method);
                ProcessMethodExpressions(method);
              }

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I looked into this in detail for .PrefixLemma and .PrefixPredicate. In places where the code looked like your first example, I change AllCallables to AllCallablesIncludingPrefixDeclarations. I also improved code in the various other visitors, making use of newer C# constructs. And I improved the iteration over declarations in IsEssentiallyEmptyModuleBody(), to be more exact than before.

In the code base, what happens with extreme lemmas/predicates and prefix lemmas/predicates is quite varied. In some places, the extreme declaration is used and the prefix version ignored. In other places, it's the other way around. And in some places, the two are handled in different ways. Therefore, I suggest that any further improvements be done separately from this PR.

foreach (var decl in AllCallables(declarations)) {
yield return decl;
if (decl is ExtremeLemma extremeLemma) {
yield return extremeLemma.PrefixLemma;
} else if (decl is ExtremePredicate extremePredicate) {
yield return extremePredicate.PrefixPredicate;
}
}
}

/// <summary>
/// Yields all functions and methods that are members of some non-iterator type in the given
/// list of declarations, as well as any IteratorDecl's in that list.
/// </summary>
public static IEnumerable<ICallable> AllItersAndCallables(List<TopLevelDecl> declarations) {
foreach (var d in declarations) {
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
yield return iter;
} else if (d is TopLevelDeclWithMembers) {
var cl = (TopLevelDeclWithMembers)d;
foreach (var member in cl.Members) {
var clbl = member as ICallable;
if (clbl != null) {
yield return clbl;
if (clbl is Function f && f.ByMethodDecl != null) {
yield return f.ByMethodDecl;
}
yield return (IteratorDecl)d;
} else if (d is TopLevelDeclWithMembers cl) {
foreach (var member in cl.Members.Where(member => member is ICallable)) {
yield return (ICallable)member;
if (member is Function { ByMethodDecl: { } } f) {
yield return f.ByMethodDecl;
}
}
}
Expand All @@ -883,8 +893,7 @@ public static IEnumerable<ICallable> AllItersAndCallables(List<TopLevelDecl> dec

public static IEnumerable<IteratorDecl> AllIteratorDecls(List<TopLevelDecl> declarations) {
foreach (var d in declarations) {
var iter = d as IteratorDecl;
if (iter != null) {
if (d is IteratorDecl iter) {
yield return iter;
}
}
Expand All @@ -897,42 +906,26 @@ public static IEnumerable<IteratorDecl> AllIteratorDecls(List<TopLevelDecl> decl
public static IEnumerable<TopLevelDecl> AllDeclarationsAndNonNullTypeDecls(List<TopLevelDecl> declarations) {
foreach (var d in declarations) {
yield return d;
var cl = d as ClassDecl;
if (cl != null && cl.NonNullTypeDecl != null) {
if (d is ClassDecl { NonNullTypeDecl: { } } cl) {
yield return cl.NonNullTypeDecl;
}
}
}

public static IEnumerable<ExtremeLemma> AllExtremeLemmas(List<TopLevelDecl> declarations) {
foreach (var d in declarations) {
var cl = d as TopLevelDeclWithMembers;
if (cl != null) {
if (d is TopLevelDeclWithMembers cl) {
foreach (var member in cl.Members) {
var m = member as ExtremeLemma;
if (m != null) {
yield return m;
if (member is ExtremeLemma extremeLemma) {
yield return extremeLemma;
}
}
}
}
}

public bool IsEssentiallyEmptyModuleBody() {
foreach (var d in TopLevelDecls) {
if (d is ModuleDecl) {
// modules don't count
continue;
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
if (cl.Members.Count == 0) {
// the class is empty, so it doesn't count
continue;
}
}
return false;
}
return true;
return TopLevelDecls.All(decl => decl.IsEssentiallyEmpty());
}

public IToken GetFirstTopLevelToken() {
Expand Down Expand Up @@ -1058,6 +1051,14 @@ public virtual List<Type> ParentTypes(List<Type> typeArgs) {

public bool AllowsAllocation => true;
public override IEnumerable<INode> Children => Enumerable.Empty<INode>();

/// <summary>
/// A top-level declaration is considered "essentially empty" if there is no way it could generate any resolution error
/// other than introducing a duplicate name.
/// </summary>
public virtual bool IsEssentiallyEmpty() {
return Attributes == null || TypeArgs.Count != 0;
}
}

public abstract class TopLevelDeclWithMembers : TopLevelDecl {
Expand Down Expand Up @@ -1183,6 +1184,13 @@ private void AddTraitAncestors(ISet<TraitDecl> s) {
// True if non-static members can access the underlying object "this"
// False if all members are implicitly static (e.g. in a default class declaration)
public abstract bool AcceptThis { get; }

public override bool IsEssentiallyEmpty() {
if (Members.Count != 0 || ParentTraits.Count != 0) {
return false;
}
return base.IsEssentiallyEmpty();
}
}

public class TraitDecl : ClassDecl {
Expand Down Expand Up @@ -1395,6 +1403,14 @@ bool ICallable.InferredDecreases {
}

public abstract DatatypeCtor GetGroundingCtor();


public override bool IsEssentiallyEmpty() {
if (Ctors.Any(ctor => ctor.Attributes != null || ctor.Formals.Count != 0)) {
return false;
}
return base.IsEssentiallyEmpty();
}
}

public class IndDatatypeDecl : DatatypeDecl {
Expand Down Expand Up @@ -1971,6 +1987,11 @@ bool ICallable.InferredDecreases {
}

public override bool AcceptThis => true;

public override bool IsEssentiallyEmpty() {
// A "newtype" is not considered "essentially empty", because it always has a parent type to be resolved.
return false;
}
}

public abstract class TypeSynonymDeclBase : TopLevelDecl, RedirectingTypeDecl {
Expand Down Expand Up @@ -2059,6 +2080,11 @@ bool ICallable.InferredDecreases {
public override bool CanBeRevealed() {
return true;
}

public override bool IsEssentiallyEmpty() {
// A synonym/subset type is not considered "essentially empty", because it always has a parent type to be resolved.
return false;
}
}

public class TypeSynonymDecl : TypeSynonymDeclBase, RevealableTypeDecl {
Expand Down
62 changes: 31 additions & 31 deletions Source/DafnyCore/Resolver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2292,50 +2292,50 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl,
reporter.Info(MessageSource.Resolver, m.tok, string.Format("_k: {0}", k.Type));
formals.Add(k);
if (m is ExtremePredicate) {
var cop = (ExtremePredicate)m;
formals.AddRange(cop.Formals.ConvertAll(cloner.CloneFormal));
var extremePredicate = (ExtremePredicate)m;
formals.AddRange(extremePredicate.Formals.ConvertAll(cloner.CloneFormal));

List<TypeParameter> tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam);
List<TypeParameter> tyvars = extremePredicate.TypeArgs.ConvertAll(cloner.CloneTypeParam);

// create prefix predicate
cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.HasStaticKeyword,
extremePredicate.PrefixPredicate = new PrefixPredicate(extremePredicate.tok, extraName, extremePredicate.HasStaticKeyword,
tyvars, k, formals,
cop.Req.ConvertAll(cloner.CloneAttributedExpr),
cop.Reads.ConvertAll(cloner.CloneFrameExpr),
cop.Ens.ConvertAll(cloner.CloneAttributedExpr),
new Specification<Expression>(new List<Expression>() { new IdentifierExpr(cop.tok, k.Name) }, null),
cop.Body,
extremePredicate.Req.ConvertAll(cloner.CloneAttributedExpr),
extremePredicate.Reads.ConvertAll(cloner.CloneFrameExpr),
extremePredicate.Ens.ConvertAll(cloner.CloneAttributedExpr),
new Specification<Expression>(new List<Expression>() { new IdentifierExpr(extremePredicate.tok, k.Name) }, null),
cloner.CloneExpr(extremePredicate.Body),
null,
cop);
extraMember = cop.PrefixPredicate;
extremePredicate);
extraMember = extremePredicate.PrefixPredicate;
// In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles.
moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop);
moduleDef.CallGraph.AddEdge(extremePredicate.PrefixPredicate, extremePredicate);
} else {
var com = (ExtremeLemma)m;
var extremeLemma = (ExtremeLemma)m;
// _k has already been added to 'formals', so append the original formals
formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));
formals.AddRange(extremeLemma.Ins.ConvertAll(cloner.CloneFormal));
// prepend _k to the given decreases clause
var decr = new List<Expression>();
decr.Add(new IdentifierExpr(com.tok, k.Name));
decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
decr.Add(new IdentifierExpr(extremeLemma.tok, k.Name));
decr.AddRange(extremeLemma.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
// Create prefix lemma. Note that the body is not cloned, but simply shared.
// For a greatest lemma, the postconditions are filled in after the greatest lemma's postconditions have been resolved.
// For a least lemma, the preconditions are filled in after the least lemma's preconditions have been resolved.
var req = com is GreatestLemma
? com.Req.ConvertAll(cloner.CloneAttributedExpr)
var req = extremeLemma is GreatestLemma
? extremeLemma.Req.ConvertAll(cloner.CloneAttributedExpr)
: new List<AttributedExpression>();
var ens = com is GreatestLemma
var ens = extremeLemma is GreatestLemma
? new List<AttributedExpression>()
: com.Ens.ConvertAll(cloner.CloneAttributedExpr);
com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword,
com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
req, cloner.CloneSpecFrameExpr(com.Mod), ens,
: extremeLemma.Ens.ConvertAll(cloner.CloneAttributedExpr);
extremeLemma.PrefixLemma = new PrefixLemma(extremeLemma.tok, extraName, extremeLemma.HasStaticKeyword,
extremeLemma.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, extremeLemma.Outs.ConvertAll(cloner.CloneFormal),
req, cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
new Specification<Expression>(decr, null),
null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known
cloner.CloneAttributes(com.Attributes), com);
extraMember = com.PrefixLemma;
cloner.CloneAttributes(extremeLemma.Attributes), extremeLemma);
extraMember = extremeLemma.PrefixLemma;
// In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.
moduleDef.CallGraph.AddEdge(com.PrefixLemma, com);
moduleDef.CallGraph.AddEdge(extremeLemma.PrefixLemma, extremeLemma);
}

extraMember.InheritVisibility(m, false);
Expand Down Expand Up @@ -3036,7 +3036,9 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
}
}
reporter.Info(MessageSource.Resolver, com.tok,
string.Format("{0} with focal predicate{2} {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name), Util.Plural(focalPredicates.Count)));
focalPredicates.Count == 0 ?
$"{com.PrefixLemma.Name} has no focal predicates" :
$"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalPredicates.Count)} {Util.Comma(focalPredicates, p => p.Name)}");
// Compute the statement body of the prefix lemma
Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before
if (com.Body != null) {
Expand Down Expand Up @@ -9428,8 +9430,7 @@ void ResolveClassMemberTypes(TopLevelDeclWithMembers cl) {
ResolveTypeParameters(m.TypeArgs, true, m);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
var com = m as ExtremeLemma;
if (com != null && com.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) {
if (m is ExtremeLemma com && com.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) {
var mm = com.PrefixLemma;
// resolve signature of the prefix lemma
mm.EnclosingClass = cl;
Expand Down Expand Up @@ -10493,8 +10494,7 @@ void ResolveMethod(Method m) {

// Resolve body
if (m.Body != null) {
var com = m as ExtremeLemma;
if (com != null && com.PrefixLemma != null) {
if (m is ExtremeLemma com && com.PrefixLemma != null) {
// The body may mentioned the implicitly declared parameter _k. Throw it into the
// scope before resolving the body.
var k = com.PrefixLemma.Ins[0];
Expand Down
15 changes: 4 additions & 11 deletions Source/DafnyCore/Rewriter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
internal override void PostCyclicityResolve(ModuleDefinition m) {
var finder = new Triggers.QuantifierCollector(Reporter);

foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(m.TopLevelDecls)) {
finder.Visit(decl, null);
}

Expand Down Expand Up @@ -191,17 +191,10 @@ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) {
}

internal override void PostResolveIntermediate(ModuleDefinition m) {
var forallvisiter = new ForAllStmtVisitor(Reporter);
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
forallvisiter.Visit(decl, true);
if (decl is ExtremeLemma) {
var prefixLemma = ((ExtremeLemma)decl).PrefixLemma;
if (prefixLemma != null) {
forallvisiter.Visit(prefixLemma, true);
}
}
var forallVisitor = new ForAllStmtVisitor(Reporter);
foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(m.TopLevelDecls)) {
forallVisitor.Visit(decl, true);
}

}

internal class ForAllStmtVisitor : TopDownVisitor<bool> {
Expand Down
Loading