fix: Fill in missing type substitutions

[RustanLeino]

Fixes #2947

This PR fixes some missing type substitutions that affected the Boogie translation of extreme predicates.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

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?

[RustanLeino]

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.

[keyboardDrummer]

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?

[RustanLeino]

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?)

[keyboardDrummer]

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);
              } 

[RustanLeino]

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.

[keyboardDrummer]

What's the effect of this change? I see you're changing the object pointer less often, but does that have an effect?

[RustanLeino]

There's a (possibly misguided) optimization in the Substitute(Expression expr) method, which is that if the result is pointer-equal to expr if the substitution has no effect. An illustrative example of this is:

      } else if (expr is MultiSetFormingExpr) {
        var e = (MultiSetFormingExpr)expr;
        var se = Substitute(e.E);
        if (se != e.E) {
          newExpr = new MultiSetFormingExpr(expr.tok, se);
        }

This optimization is error prone. For LiteralExpr, the optimization was missing, so I added it. In other places (like DatatypeValue, the optimization was too aggressive (meaning, "wrong") because it returned expr even when it should have returned a new DatatypeValue with a different InferredTypeArgs field.

The optimization is intended to save memory, but this may not make any difference, and the optimization makes the code significantly more complicated. If you suggest, I'd be happy to remove this optimization from Substitute(Expression.

[RustanLeino]

I built a local version with a simplified Substitute (that is, I removed the optimization). It passes. I'd be happy to add it to this PR, if you think, or to file a separate PR for it.

[keyboardDrummer]

The optimization is intended to save memory, but this may not make any difference, and the optimization makes the code significantly more complicated.

Without a measurement about the performance difference I'd prefer to leave it like it is, unless you're confident the optimisation doesn't have a significant effect. I'm not sure whether comparing the difference in the test-suite runtime is a good test.

I'm hoping we can at some point generate the code for various behaviors such as Substitutor, Cloner, SubExpressions, SubStatements, and likely some others.

[RustanLeino]

Okay, I'll leave it as is. And yes, I agree that generating code for these sorts of routines would be far better than the manual upkeep we have to do today.

[keyboardDrummer]

Approving but I expect fresh bugs related to this to be added in the future. How should a caller decide whether to call AllCallablesIncludingPrefixDeclarations or AllCallables without having to dive into the semantics of extreme lemma's? I feel that as long as there's these two options there's a source for bugs.