Fixes lost dependencies for pruning during monomorphization. #767

zafer-esen · 2023-08-03T21:06:54Z

This PR attempts to fix more axioms being pruned with the /prune flag than intended with monomorphization.

Monomorphization introduces new axioms that are monomorphized, and tries splitting all axioms (polymorphic or not) into their conjuncts. This PR adds logic to update functions and constants to point to the new axioms as dependencies.

The fix is a draft and not optimal, for instance it sometimes adds dependencies that were not part of the `uses` clauses of some functions.

shazqadeer · 2023-08-04T04:25:09Z

I am afraid we have to hit the brakes here. As I have indicated in the discussion on issue #560 , I don't understand parts of the implementation of pruning. This PR will leak some of that poorly-understood complexity into the implementation of monomorphization as well.

I have a question and a suggestion for your consideration.

First, the question:

Suppose an edge is explicitly indicated from a function to an axiom via uses. Suppose also that the function is polymorphic and the axiom has polymorphic quantifiers in it. Then, both the function and the axiom will be instantiated. What is the appropriate way of defining edges between the instantiations?

Second, the suggestion:

The most difficult to understand part of the current implementation of pruning is the automatic generation of incoming edges into axioms through the analysis of triggers. I suggest we drop this feature, thereby requiring the user of Boogie to do some analysis itself and put the appropriate annotations explicitly in Boogie code.

keyboardDrummer · 2023-08-04T10:08:54Z

There were two main issues: Monomorphization did not preserve uses clauses of constants and functions.

Are you saying it removes uses clauses from functions and constants? That seems unlikely to me. Can you clarify what you meant?

In quantified axioms outside of uses clauses, pruning depends on triggers for computing incoming edges. Since
expressions of the form forall :: {...} and exists :: {...} become unquantified after monomorphization, they were being pruned.

Can you provide an example that shows which uses clauses are missing in the monomorphized code?

The way I understood the problem is that monomorphization creates new axioms based on existing ones, and does not copy over the uses clauses for the created ones.

keyboardDrummer · 2023-08-04T09:56:23Z

Source/Core/AST/Absy.cs

-    public IList<Axiom> DefinitionAxioms { get; }
+    public IList<Axiom> DefinitionAxioms => definitionAxioms;
+
+    private IList<Axiom> definitionAxioms = new List<Axiom>();


Why use a property+field construction instead of the existing auto property?

Good point, will add a set to the auto property instead.

keyboardDrummer · 2023-08-04T09:57:23Z

Source/Core/AST/Absy.cs

+
+    private IList<Axiom> definitionAxioms = new List<Axiom>();
+
+    public bool RemoveDefinitionAxiom(Axiom axiom)


Why add these Remove and Add methods, given that they are already available through DefinitionAxioms.Remove and DefinitionAxioms.Add ? It looks like an attempt at encapsulation but I don't think it encapsulates anything.

Good point, I can change to use those instead.

keyboardDrummer · 2023-08-04T09:59:40Z

Source/Core/Monomorphization.cs

      program.RemoveTopLevelDeclarations(decl => decl is Axiom);
      program.AddTopLevelDeclarations(splitAxioms);
      program.AddTopLevelDeclarations(polymorphicMapDatatypeCtorDecls);
      Contract.Assert(MonomorphismChecker.IsMonomorphic(program));
      return monomorphizationVisitor;
    }

+    private static void UpdateDependencies(List<Axiom> splitAxioms, MonomorphizationVisitor monomorphizationVisitor,


Why do you have to update the uses clauses after the fact? Is it not simpler to update them immediately when the new axioms are created?

I tried doing exactly that initially, but there are a few reasons for doing it this way:

New axioms are also added in different classes.

Original axioms are actually quite a bit changed in-place at the point new Axiom is called (they are already possibly instantiated). What is being split is possibly a big conjunction of all axiom instantiations. To reestablish the dependencies efficiently, one needs to propagate other information down into those classes and check if the split axioms have the relevant symbols. There is also the case with axioms that are no longer quantified after instantiation (unless we turn off all automatic detection of dependencies in the pruning algorithm).

I think it might also be more resilient to changes in monomorphization code if the changes create new axioms elsewhere, as the only thing one needs to do is to add the old and new axiom to a dictionary.

Some of these points can be argued against, and it can probably be done as you suggest, but in the end I am not sure if it would be worth the effort.

zafer-esen · 2023-08-04T14:20:02Z

Thank you both for the reviews @shazqadeer and @keyboardDrummer! I was hoping the PR would initiate exactly this kind of discussion.

I don't understand parts of the implementation of pruning. This PR will leak some of that poorly-understood complexity into the implementation of monomorphization as well.

I agree, there seem to be some assumptions the pruning algorithm makes, and these seem to have changed over time since its initial implementation.

Suppose an edge is explicitly indicated from a function to an axiom via uses. Suppose also that the function is polymorphic and the axiom has polymorphic quantifiers in it. Then, both the function and the axiom will be instantiated. What is the appropriate way of defining edges between the instantiations?

This was something I was hoping to get your opinions on. Let's call the polymorphic function f, its instantiated instances f_0...f_m, the original axiom a, and its instantiated instances a_0...a_n (with n >= m if f appears in a). Currently, the edges are computed as follows:

if f appears as a symbol anywhere in a, then an edge from f_i (i = 0...m) to a_j (j = 0...n) is only added if f_i appears as a symbol anywhere in a_j.
if f does not appear as a symbol in a, then edges from f_i (i = 0...m) to all a_0...a_n are added.

There are also axioms that do not contain any polymorphic quantifiers in it, but these axioms are still split into its conjuncts. The same algorithm is applied here

The most difficult to understand part of the current implementation of pruning is the automatic generation of incoming edges into axioms through the analysis of triggers. I suggest we drop this feature, thereby requiring the user of Boogie to do some analysis itself and put the appropriate annotations explicitly in Boogie code.

I agree that this would be a good solution, and make the fix for the second issue mentioned in the PR unnecessary. It would also prevent the leak from the pruning algorithm into the monomorphization code, since I think this fix is the only part that depends on assumptions from the pruning algorithm (i.e., symbols inside triggers are considered automatically as incoming edges to axioms). However, I did not want to change anything in the pruning code since that would require changes in front-end tools that use pruning (only Dafny?).

To summarize, this PR attempts to:

Re-establish uses edges that are lost during monomorphization, I think this should be done in either case. Your feedback would be appreciated on how to best do this in the presence of instantiated functions and axioms!
Re-establish edges that were automatically added by the pruning algorithm, namely the incoming edges of axioms due to triggers. This can be dropped, but I am not sure of all its implications in the front-end tools that use pruning.

zafer-esen · 2023-08-04T14:29:48Z

Are you saying it removes uses clauses from functions and constants? That seems unlikely to me. Can you clarify what you meant?

What I meant was uses clauses were not preserved by the monomorphization code due to new axioms being generated (here and here, although I do not think the latter ever triggers since uses clauses add axioms to OtherDefinitionAxioms of functions).

Can you provide an example that shows which uses clauses are missing in the monomorphized code?

Here is an example from Dafny:
axiom (forall<T> :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0);

Putting this inside the uses clause of function Seq#Empty<T>(): Seq T; would fix it in this case. I am not aware of any others in Dafny code. Still, I wasn't sure if such axioms would show up in other places, and wanted to have a fix for it in line with the current assumptions of the pruning code (i.e., that symbols from triggers are automatically considered as incoming edges).

The way I understood the problem is that monomorphization creates new axioms based on existing ones, and does not copy over the uses clauses for the created ones.

Yes, this is the first issue mentioned in this PR. It is a bit tricky as both functions and axioms can be instantiated, and even non-instantiated axioms are split into their conjuncts during monomorphization. It would be very inefficient to add edges to all new axioms that are generated from an original axiom, as the number of new axioms can grow quickly depending on the number of polymorphic quantifiers in it. This is independent from above discussion in this comment however.

Addresses review comments in PR boogie-org#767.

shazqadeer · 2023-08-04T23:16:02Z

@zafer-esen :

Your method for adding edges between instantiated function and instantiated axioms seems fine to me. Please make sure you document it somewhere in the Boogie code.

Please reduce the scope of this PR so that it addresses only issue #1 from your PR description.

Dafny is the only user of the /prune flag in Boogie. Please examine the feasibility of Dafny not using the edge inference due to triggers. I strongly recommend deleting this aspect of the prune implementation in Boogie and supporting only explicit edges. My hope is that we would not have to address issue #2.

zafer-esen · 2023-08-05T00:45:39Z

@shazqadeer Thank you for the feedback, I will add some documentation to the code for (1) and reduce the scope of the PR.

I discussed this with @atomb and will also look into the feasibility of removing edge inference using triggers. I think something like a used_by attribute rather than a uses clause is needed for this to work. This is because an axiom can have multiple triggers, with each trigger possibly referring to multiple symbols (example and documentation here). If an axiom has the two triggers {P, Q} {R} as in the linked example, an attribute {:used_by "P, Q; R"} could be added.

One complication is that both symbol names and axioms can change during monomorphization, but I think this can be handled by updating the new axiom attributes using aforementioned method of adding edges between instantiated functions and axioms, possibly inside the proposed UpdateDependencies method in this PR.

Edit - more clarification (mostly for myself):
As I understand incoming edges to quantified axioms are currently only added via triggers, so a used_by attribute is needed to replace this edge inference. Outgoing edges are added to constants and functions via uses clauses (and by looking at their definitions), so both uses and used_by would actually be needed. Even axioms inside a uses clauses would need to be annotated with a used_by attribute. An axiom is only kept if there are both an outgoing edge from a symbol to it, and an incoming edge from that symbol to the axiom.

shazqadeer · 2023-08-07T01:10:01Z

I didn't understand why both uses and used_by would be needed. Can you provide a concrete example?

zafer-esen · 2023-08-07T14:48:52Z

Each declaration can have both incoming and outgoing declarations. I was basing my understanding on this comment:

a declaration A depends on B, if the outgoing dependents of A match with some incoming dependent of B (see method depends).

This comment is out of date. The method Depends was deleted in PR #442, and the semantics seems to have changed. In the current pruning algorithm, if I am interpreting this correctly, an edge between two nodes is established if one of the two nodes has the other one in its dependencies. In this semantics, used_by is not needed for axioms inside uses clauses. Since this is the case, uses could be completely removed and subsumed by used_by, which is more expressive. I make a case for this below.

Here are some examples to explain the current semantics:
Example 1:

function foo() : int;
axiom foo() == 42; // label: a
procedure p()
{
  assert foo() == 42;
}

Here the procedure p is at the root, and has foo is an outgoing dependency. Let's denote this p -> f (p depends on f). foo has no dependencies. Axiom a, having no triggers to establish incoming dependencies, has only foo as its outgoing dependency. So we have the following set of dependencies:
{p -> foo, a -> foo}
This implies a gets pruned away, because it is not reachable from the root node p.

If we add axiom a inside the uses clause of foo, the dependencies become:
{p -> foo -> a, a -> foo}

Since a is now reachable, it is not pruned away.

Example 2

function foo(x: int) : int;
axiom (forall x: int :: {foo(x)} foo(x) == 42); // label: a
procedure p()
{
  assert foo(0) == 42;
}

Now the axiom is quantified and has a trigger, so automatic edge inference is applied. This builds the dependencies as:
{p -> foo, foo -> a -> foo}
I.e., foo is added as an incoming edge to a. In the current semantics, the edges computed from this set is equivalent to {p -> foo -> a, a -> foo}.

Still, triggers are more expressive than uses clauses, so a uses clause is not sufficient by itself to replace the edge inference. I attempt to explain this in the next example.

Example 3:

function bar(x: int) : int;
function foo(x: int) : int;

axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42); // label: a
axiom (forall x: int :: {bar(x)} bar(x) == 0); // label: b

procedure p()
{
  assert foo(0) == 42;
}

Here the trigger of axiom a contains two function symbols. If the trigger contains more than one function or constant symbol, its dependencies are tuples, and all symbols inside the tuple must be reachable from the root for the axiom to be preserved. In this case the dependencies are:

{p -> foo, (foo, bar) -> a -> foo, b -> bar}
                           -> bar

Here bar is unreachable from the root p, hence a is pruned away. If we only add a call to bar inside p, the graph would change to

{p -> foo, (foo, bar) -> a -> foo, b -> bar}
   -> bar                  -> bar

and a and b would be both kept, and the assertion would verify.

One might at this point wonder what this expressiveness brings; one could just put both axioms inside a uses clause, and they both would be preserved anyway. Consider the following axioms from the Dafny prelude, which does exactly this:

function $Is<T>(T,Ty): bool uses {           // no heap for now
    axiom(forall v : int  :: { $Is(v,TInt) }  $Is(v,TInt));
    axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
    axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
    axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
    axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL));
    [...] // more axioms for every type
 }

Here $Is is a function symbol, and TInt, TReal etc. are constants.
As soon as $Is is reachable from any root node, none of these axioms can be pruned away. Furthermore, all symbols appearing in their bodies are also included in the dependency graph, so all axioms inside the uses clauses of those symbols are transitively included.

I tried moving these axioms out of the uses clause, and in my limited experiments I saw improvements in solver resource counts. (Takeaway: in the current semantics, uses should not be used for any axiom with more than one symbol in any of its triggers.) This improvement is achieved by the current edge inference, so it would be good to keep its expressiveness around via an attribute like used_by that would allow tuple dependencies.

Since used_by subsumes the expressiveness of uses and can be applied to any axiom with or without triggers, I propose removing uses completely, as its incorrect usage leads to more axioms being preserved than necessary.

shazqadeer · 2023-08-07T16:40:05Z

To test my understanding, I rewrote your three examples using the used_by syntax. Did I get them right?

Example 1:

function foo() : int;
axiom foo() == 42 used_by foo; // label: a
procedure p()
{
  assert foo() == 42;
}

Example 2:

function foo(x: int) : int;
axiom (forall x: int :: {foo(x)} foo(x) == 42) used_by foo; // label: a
procedure p()
{
  assert foo(0) == 42;
}

Example 3:

function bar(x: int) : int;
function foo(x: int) : int;

axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42) used_by foo; // label: a
axiom (forall x: int :: {bar(x)} bar(x) == 0) used_by foo, bar; // label: b

procedure p()
{
  assert foo(0) == 42;
}

Is it also correct that when we move to used_by, the algorithm for determining the set of included declarations will be vanilla graph reachability? I want to note here that the current algorithm is not simple reachability.

I suppose the used_by clause qualifying an axiom may contain function and constant names. Could it also contain procedure names?

Can we also get rid of :include_dep?

zafer-esen · 2023-08-07T18:48:10Z

I had the same idea with Examples 1 & 2. I had a slightly different idea in Example 3, but maybe this was not the best example: it cannot be verified even without pruning as the axioms don't trigger without both foo and bar! However, I think it still serves to illustrate the difference between uses and used_by.

If used_by is to exactly have the current edge inference semantics (which seems to be in line with how triggers work), Example 3 would be as follows:

function bar(x: int) : int;
function foo(x: int) : int;

axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42) used_by (foo, bar); // label: a
axiom (forall x: int :: {bar(x)} bar(x) == 0) used_by bar; // label: b

procedure p()
{
  assert foo(0) == 42;
}

i.e., make all symbols in the trigger used_by (added parentheses to denote a tuple as there can be multiple triggers). This still prunes away both axioms, but they would not be used anyway due to axioms not triggering.

Contrast this to using a uses clause:

function bar(x: int) : int;
function foo(x: int) : int uses {
  axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42);
  axiom (forall x: int :: {bar(x)} bar(x) == 0); // label: b
}

procedure p()
{
  assert foo(0) == 42;
}

In this case no pruning happens, but the program also does not verify, because a and b are still useless.

Is it also correct that when we move to used_by, the algorithm for determining the set of included declarations will be vanilla graph reachability? I want to note here that the current algorithm is not simple reachability.

I am not sure about this, I think the algorithm remains similar? Reachability would still be computed from the roots, but with uses_by, axioms would be connected to the graph only through their incoming edges. Removing uses has the effect of removing outgoing edges from functions and constants. Maybe @keyboardDrummer can chime in.

I suppose the used_by clause qualifying an axiom may contain function and constant names. Could it also contain procedure names?

I think it could contain any named declaration.

Can we also get rid of :include_dep?

Yes, in axioms without triggers, include_dep was adding all body symbols as incoming. The same could be achieved by adding a used_by clause and listing all symbols. In axioms with triggers, I believe it had no effect.

zafer-esen · 2023-08-07T18:52:26Z

I reduced the scope of this PR as requested. If you think adding used_by would make sense, it can perhaps be another PR.

keyboardDrummer · 2023-08-07T20:03:22Z

This was something I was hoping to get your opinions on. Let's call the polymorphic function f, its instantiated instances f_0...f_m, the original axiom a, and its instantiated instances a_0...a_n (with n >= m if f appears in a). Currently, the edges are computed as follows:

if f appears as a symbol anywhere in a, then an edge from f_i (i = 0...m) to a_j (j = 0...n) is only added if f_i appears as a symbol anywhere in a_j.

Makes sense

if f does not appear as a symbol in a, then edges from f_i (i = 0...m) to all a_0...a_n are added.

Does this occur in practice? I wonder whether we could disallow such uses/used-by clauses.

I think adding used_by (which could replace used), can be useful because then inferring dependencies based on triggers can be a compilation step where used_by declarations are added based on the triggers, so then addressing issue # 2 the details of this PR mentions, wouldn't affect the monomorphization (MM) code.

Also, I hope used_by would allow you to simplify the changes to the (MM) code this PR makes. When instantiating the axioms, you could use the functionInstantiations field together with the used_by clauses of the original axiom to determine what the used_by clauses of the instantiations would be, so you wouldn't need to maintain any additional state when doing MM or do any postprocessing.

Is it also correct that when we move to used_by, the algorithm for determining the set of included declarations will be vanilla graph reachability? I want to note here that the current algorithm is not simple reachability.

I am not sure about this, I think the algorithm remains similar? Reachability would still be computed from the roots, but with uses_by, axioms would be connected to the graph only through their incoming edges. Removing uses has the effect of removing outgoing edges from functions and constants. Maybe @keyboardDrummer can chime in.

I don't think anything would change there.

shazqadeer · 2023-08-07T20:02:41Z

Source/Core/Monomorphization.cs

+    public readonly HashSet<Function> originalFunctions;
+    public readonly HashSet<Constant> originalConstants;
+    // Note that old axioms refer to axioms of the original program which might have been updated in-place during monomorphization.
+    public readonly Dictionary<Axiom, HashSet<Axiom>> oldAxiomsToSplitAxioms;


Rename to originalAxiomToSplitAxioms

Done (I also renamed the other dictionary).

Source/Core/Monomorphization.cs

shazqadeer · 2023-08-07T20:27:01Z

Source/Core/Monomorphization.cs

@@ -1293,11 +1297,20 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor
    private HashSet<TypeCtorDecl> visitedTypeCtorDecls;
    private HashSet<Function> visitedFunctions;
    private Dictionary<Procedure, Implementation> procToImpl;
+    public readonly HashSet<Function> originalFunctions;
+    public readonly HashSet<Constant> originalConstants;
+    // Note that old axioms refer to axioms of the original program which might have been updated in-place during monomorphization.


Are you sure old axioms are updated in-place? If I remember correctly, each axiom could be instantiated multiple times so the instantiation is done on a duplicate version of the axiom which is modified in-place. The original axiom stays as is to facilitate the next instantiation. Could you please check?

Yes, I checked now and old axioms get instantiated in-place after executing this line. I think this comment also confirms that the old axioms are instantiated in-place (with the help of MonomorphizationDuplicator).

shazqadeer · 2023-08-07T20:29:54Z

@zafer-esen :

Thanks for explaining the tuple notation for each member of the used_by clause. I agree that with the flexibility of having a tuple in addition to singletons, the current reachability algorithm remains unchanged. used_by makes sense.

It would be great to see uses replaced by used_by in a separate PR. Please consult @RustanLeino about alternative keywords for used_by. The use of an - in the keyword is not ideal. Perhaps constrains?

Source/Core/AST/Absy.cs

Source/Core/Monomorphization.cs

keyboardDrummer

Could you add tests to this PR?

Source/Core/Monomorphization.cs

keyboardDrummer · 2023-08-07T21:46:49Z

Source/Core/Monomorphization.cs

+          newAxiomConstants.Add(newAxiom, newAxiomFC.Constants);
+        }
+
+        void UpdateFunctionDependencies(HashSet<Function> functions)


Adding the parameter HashSet<Function> functions seems unnecessary, since it's also available through monomorphizationVisitor.originalFunctions

I'm not always sure how much inner functions help read the code. Here I have to inspect the outer scope to understand the meaning of some of the variables used.

Removed inner functions. I used inner functions initially because they were called twice in the original version of this PR, but after reducing its scope this changed.

keyboardDrummer · 2023-08-07T21:50:54Z

Source/Core/Monomorphization.cs

+
+        void UpdateFunctionDependencies(HashSet<Function> functions)
+        {
+          foreach (var function in functions)


Consider renaming: function -> oldFunction , functions -> oldFunctions

Removed inner functions. I also changed old to original to match related dictionary names.

Source/Core/Monomorphization.cs

keyboardDrummer · 2023-08-07T21:53:46Z

Source/Core/Monomorphization.cs

+        oldAxiomFC.Visit(unmodifiedOldAxiom);
+        var oldAxiomFunctions = oldAxiomFC.Functions;
+
+        Dictionary<Axiom, HashSet<Function>> newAxiomFunctions = new Dictionary<Axiom, HashSet<Function>>();


Could you use var here? Does your IDE not suggest that?

Updated. My IDE was apparently suggesting that, which I didn't notice.

An axiom in DafnyPrelude was incorrectly being pruned away with the `monomorphic` type encoding, because it was losing its (polymorphic) quantifier and trigger. This meant automatic edge inference from triggers was no longer applicable. Moved the axiom in question into a uses clause to prevent it from being pruned. The change has no affect on other type encodings `arguments` (current default) and `predicates`. There is more discussion related to the fix here in [Boogie PR 767](boogie-org/boogie#767). 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).

shazqadeer · 2023-08-08T15:35:09Z

Source/Core/Monomorphization.cs

+    public readonly HashSet<Constant> originalConstants;
+    // Note that original axioms refer to axioms of the original program which might have been updated in-place during monomorphization.
+    public readonly Dictionary<Axiom, HashSet<Axiom>> originalAxiomToSplitAxioms;
+    public readonly Dictionary<Axiom, Axiom> originalAxiomToUninstantiatedCopies;


You want to hold on to the original axiom so that you can walk over it and calculate some state. I am wondering if you can do this calculation and stash the computed state somewhere before the original axiom is modified in-place. It seems this approach might be more intuitive to understand.

If you choose to retain the current approach, rename to originalAxiomToUninstantiatedCopy.

How about this:
We add something like the following to Absy.Axiom

public Axiom OriginalAxiom; public Axiom OriginalAxiomUninstantiatedCopy;

and update them during monomorphization. This is in line with instantiated DeclWithFormals in Absy.cs. We can fill in OriginalAxiomUninstantiatedCopy at entry to monomorphization, and fill in OriginalAxiom when splitting (instantiated and uninstantiated) axioms.

We could also add to Absy.Axiom:

public ISet<Function> Functions; public ISet<Function> Constants;

which could return body functions & symbols for an axiom. Then we would no longer need the additional dictionaries. The function and constant collector could also be moved out somewhere, maybe to Absy.cs.

I implemented the version I proposed above, but I am not sure if it ended up being any better. In the new implementation members of Axiom need to be initialized in the right places during monomorphization, as opposed to adding entries to the dictionaries. The dictionaries are no longer needed, but similar collections need to be computed again from splitAxioms inside UpdateFunctionDependencies. Maybe additional members in Axiom, which are only used during monomorphization, are also undesirable. Overall I am tempted to just change the name for now. This can perhaps be considered again when adding used_by.

When I made the suggestion, I had something very simple in mind. You have the following lines of code in your PR:

var originalAxiomFc = new FunctionAndConstantCollector(); var uninstantiatedOriginalAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopy[originalAxiom]; originalAxiomFc.Visit(uninstantiatedOriginalAxiom);

If I understand this correctly, you retrieving the cloned axiom (prior to in-place updates) just so you can call the originalFc.Visit method. You could call this method up front and stash originalAxiomFc in the dictionary instead. Then you can look up the collected functions and constants later.

If you don't like this suggestion, go ahead and land your PR as is.

That makes sense, and axioms don't need to be cloned anymore. I just pushed a commit doing this, thanks for the suggestion!

zafer-esen · 2023-08-08T22:11:39Z

@keyboardDrummer

if f does not appear as a symbol in a, then edges from f_i (i = 0...m) to all a_0...a_n are added.

Does this occur in practice? I wonder whether we could disallow such uses/used-by clauses.

I do not know of any use cases, none in the DafnyPrelude I think.

Could you add tests to this PR?

I will add a few tomorrow.

zafer-esen · 2023-08-09T15:50:48Z

I added two tests. The tests will need to be updated if used is eventually removed, but this should be straightforward.

I also changed slightly how /printPruned works to be more consistent with /print:

Added .bpl suffix at the end.
Axioms that are part of definition axioms of some function or constant were double printed, now they are only printed inside uses clauses. This makes it consistent with print.

If the change to /printPruned is not okay or out of scope I can revert it.

shazqadeer · 2023-08-09T15:57:24Z

Test/pruning/MonomorphicSplit.bpl

+
+// The following checks are a bit simplistic, but this is
+// on purpose to reduce brittleness. We assume there would now be two uses clauses
+// with one axiom each, and those axioms should not be conjunctions


How can an axiom be a conjunction of monomorphized functions? The types do not match. Please rephrase.

The last sentence of this paragraph is equally mysterious.

shazqadeer · 2023-08-09T15:58:02Z

Test/pruning/MonomorphicSplit.bpl

+
+procedure monomorphicSplit()
+  ensures f1(true) == 42;
+	ensures f1(3) == 42;


Any particular reason to indent the second ensures past the first one?

Ah, this was not visible on my end in both Emacs and VS Code, apparently the second indentation was added as a tab (new laptop). Should be fixed now.

shazqadeer · 2023-08-09T15:59:53Z

Test/pruning/NonmonomorphicSplit.bpl

+// axiom f1(0) == 1 and axiom f2(0) == 2.
+// Current implementation ensures that f1(0) == 1 is kept as a dependency
+// of f1, and f2(0) is moved to be a dependency of f2. If there would be
+// other symbols in the axiom, the new split axioms would be added to those


I sort of understand what the last sentence is saying. But I am confident its meaning can be made more transparent. It is fine to define symbols and use them later to clarify what is being said.

Thanks for the feedback, they were written a bit hastily... I tried updating both explanations based on the comments.

zafer-esen · 2023-08-10T18:08:43Z

@keyboardDrummer About your question from earlier:

if f does not appear as a symbol in a, then edges from f_i (i = 0...m) to all a_0...a_n are added.

Does this occur in practice? I wonder whether we could disallow such uses/used-by clauses.

I was having a look at this paper, and I believe this is what the paper refers to as trigger sharing, and is sometimes useful.

Consider Example 3 from before (ignoring pruning for now):

function bar(x: int) : int;
function foo(x: int) : int;

axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42);
axiom (forall x: int :: {bar(x)} bar(x) == 0); // label: b

procedure p()
{
  assert foo(0) == 42;
}

This does not verify, because there are no terms that can trigger any of the axioms. However, if we add foo(x) as another trigger to the second axiom, i.e.,

axiom (forall x: int :: {bar(x)} {foo(x)} bar(x) == 0); // label: b

This verifies.

When we add pruning and monomorphization, If foo is polymorphic and if axiom b is in the uses clause of foo, the current implementation would add all instantiations of axiom b as dependencies to all instantiations of foo. I think this would be undesirable, if it ever happens. It should be possible to determine the correct instantiation of foo to match with some instantiation of b from its argument types. I can do this change in this PR for uses (might need to wait until next week), or it could be added in the proposed used_by PR.

keyboardDrummer · 2023-08-11T10:08:18Z

I was having a look at this paper, and I believe this is what the paper refers to as trigger sharing, and is sometimes useful.

Consider Example 3 from before (ignoring pruning for now):
function bar(x: int) : int;
function foo(x: int) : int;

axiom (forall x: int :: {foo(bar(x))} foo(bar(x)) == 42);
axiom (forall x: int :: {bar(x)} bar(x) == 0); // label: b

procedure p()
{
  assert foo(0) == 42;
}
This does not verify, because there are no terms that can trigger any of the axioms. However, if we add foo(x) as another trigger to the second axiom, i.e.,
axiom (forall x: int :: {bar(x)} {foo(x)} bar(x) == 0); // label: b
This verifies.

After thinking about this more, your initial suggestion (quoted below for clarity) seems perfect.

if f appears as a symbol anywhere in a, then an edge from f_i (i = 0...m) to a_j (j = 0...n) is only added if f_i appears as a symbol anywhere in a_j.

if f does not appear as a symbol in a, then edges from f_i (i = 0...m) to all a_0...a_n are added.

keyboardDrummer · 2023-08-11T10:09:49Z

@shazqadeer if you approve this, could you merge it?

@zafer-esen

(Note that this is @zafer-esen's work. I created the PR for permissions reasons.) Dafny uses the Boogie option `prune` by default. (Introduced in [Boogie PR #427](boogie-org/boogie#427), although the semantics explained there is [out of date](boogie-org/boogie#767 (comment)).). The `prune` option, when enabled, runs a reachability analysis in Boogie, and prunes away functions, constants and axioms that are not reachable from root nodes. This greatly reduces resource counts, and leads to less brittleness; which is why pruning is intentionally made as strong as possible. The semantics of pruning, at a high level, is as follows. If an axiom is inside a `uses` clause of some symbol `s`: * without quantifiers or without triggers: do not prune if `s` is reachable. * with both quantifiers and triggers: do not prune if (a) `s` is reachable _or_ (b) all symbols in one of its triggers are reachable. If an axiom is not inside a `uses` clause: * without quantifiers or without triggers: always pruned. * with both quantifiers and triggers: do not prune if (b) all symbols in one of its triggers are reachable. If (a) holds but (b) does not, this leads to a weaker pruning if an axiom with quantifiers and triggers is inside a `uses` clause. (b) matches the semantics of how axioms with triggers are instantiated (AFAIK), so axioms with both quantifiers and triggers should not be inside `uses` clauses (with the exception of purely polymorphic quantifiers, more on this at the end of this comment). Consider the [following lines](https://github.com/dafny-lang/dafny/blob/c31932b4b4f77a38e5da9c9f6a7689d8f57346bf/Source/DafnyCore/DafnyPrelude.bpl#L230-L290) from `DafnyPrelude.bpl`: ``` function $Is<T>(T,Ty): bool uses { // no heap for now axiom(forall v : int :: { $Is(v,TInt) } $Is(v,TInt)); axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal)); axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool)); axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar)); axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL)); [...] // more axioms for every type } ``` `$Is` is a function symbol and `TInt`, `TReal` etc. are constant symbols, i.e., the axioms shown are quantified and all have triggers with two function or constant symbols. Since they are inside the `uses` clause of `$Is`, none of these axioms can be pruned if `$Is` is reachable. However, if the second symbol inside the triggers, say `TReal` in the second axiom, is still unreachable, that axiom cannot be triggered despite being preserved (but will negatively affect resource counts). This PR moves all quantified axioms with triggers outside of their `uses` clauses. The one exception is purely polymorphic quantifiers ([example](https://github.com/dafny-lang/dafny/blob/2a2e1c41af9b89c10437abc71cca92eb818e02a8/Source/DafnyCore/DafnyPrelude.bpl#L970-L972)), which should remain inside a `uses` clause, as these quantifiers disappear if monomorphization is used in Boogie. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Zafer Esen <[email protected]> Co-authored-by: Remy Willems <[email protected]>

shazqadeer · 2023-09-13T14:24:14Z

@zafer-esen : There was discussion in this PR for dropping uses and include_dep in favor of used_by. Is that still the plan?

zafer-esen · 2023-09-13T15:02:21Z

There was a small discussion about this recently in a Dafny PR where I wrote the following in a comment:

I am starting to think it might be best if edge inference from triggers is preserved. The only correct way to use used_by might be to add exactly one tuple for each trigger of an axiom, which the current edge inference is already doing. Decoupling the semantics would make it possible to strengthen pruning, but I have difficulty seeing any cases where this would be useful.

It would be great to know what you all think @shazqadeer, @atomb and @keyboardDrummer about this.

If the edge inference from triggers infers exactly the set of axioms that can be instantiated, maybe it makes sense to keep edge inference around. With this PR merged, uses clauses are only needed in axioms without triggers.

Another small concern is, unlike uses and include_deps, used_by also requires specifying symbols whose names would need to be updated during monomorphization. There might be a simple way to avoid this that I am not seeing though, maybe by resolving the symbols after parsing. This would still require matching the axioms to the correct functions if those functions get monomorphized, something akin to what was done in this PR. Automatic edge inference side-steps this issue because it happens after monomorphization.

keyboardDrummer · 2023-09-14T09:40:23Z

If the edge inference from triggers infers exactly the set of axioms that can be instantiated, maybe it makes sense to keep edge inference around.

I think it does

With this PR merged, uses clauses are only needed in axioms without triggers.

Sounds good

) An axiom in DafnyPrelude was incorrectly being pruned away with the `monomorphic` type encoding, because it was losing its (polymorphic) quantifier and trigger. This meant automatic edge inference from triggers was no longer applicable. Moved the axiom in question into a uses clause to prevent it from being pruned. The change has no affect on other type encodings `arguments` (current default) and `predicates`. There is more discussion related to the fix here in [Boogie PR 767](boogie-org/boogie#767). 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).

An axiom in DafnyPrelude was incorrectly being pruned away with the `monomorphic` type encoding, because it was losing its (polymorphic) quantifier and trigger. This meant automatic edge inference from triggers was no longer applicable. Moved the axiom in question into a uses clause to prevent it from being pruned. The change has no affect on other type encodings `arguments` (current default) and `predicates`. There is more discussion related to the fix here in [Boogie PR 767](boogie-org/boogie#767). 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).

zafer-esen added 3 commits August 3, 2023 15:17

Attempts to fix the lost dependencies during monomoprhization.

41d2e86

The fix is a draft and not optimal, for instance it sometimes adds dependencies that were not part of the `uses` clauses of some functions.

Fixes too much pruning when using monomorphization.

2f21837

Update failing test output.

89643d8

keyboardDrummer reviewed Aug 4, 2023

View reviewed changes

Simplify Constant methods in Absy.cs.

e059d8e

Addresses review comments in PR boogie-org#767.

Remove automatic preservation of polymorphic quantifier dependencies.

d50af6f

zafer-esen mentioned this pull request Aug 7, 2023

Fix: incorrect pruning of axiom with monomorphization. dafny-lang/dafny#4396

Merged

shazqadeer requested changes Aug 7, 2023

View reviewed changes

Rename some variables as requested in boogie-org#767.

06e99f9

keyboardDrummer reviewed Aug 7, 2023

View reviewed changes

Source/Core/AST/Absy.cs Outdated Show resolved Hide resolved

Source/Core/Monomorphization.cs Outdated Show resolved Hide resolved

zafer-esen added 2 commits August 7, 2023 17:33

Expose OtherDefinitionAxioms and uppercase public member

8ac0139

Update failing grammar test file.

0024600

keyboardDrummer reviewed Aug 7, 2023

View reviewed changes

shazqadeer reviewed Aug 8, 2023

View reviewed changes

zafer-esen added 2 commits August 8, 2023 14:53

Address more comments from boogie-org#767 in monomorphization code.

c6b2762

Make some public members private / protected.

e4d5c99

Only store symbol collector instead of original axiom copies.

7b28f0e

shazqadeer approved these changes Aug 9, 2023

View reviewed changes

shazqadeer self-requested a review August 9, 2023 02:55

shazqadeer previously approved these changes Aug 9, 2023

View reviewed changes

Add tests and update how pruned files are printed.

d296215

zafer-esen dismissed shazqadeer’s stale review via d296215 August 9, 2023 15:45

shazqadeer reviewed Aug 9, 2023

View reviewed changes

zafer-esen added 2 commits August 9, 2023 12:03

Clarify test explanation and fix indentation.

9eb3ab9

Clarify comments in test.

1f14fac

keyboardDrummer approved these changes Aug 11, 2023

View reviewed changes

keyboardDrummer enabled auto-merge (squash) August 11, 2023 10:08

keyboardDrummer disabled auto-merge August 11, 2023 10:09

Merge branch 'master' into master

9d8c497

shazqadeer merged commit c243b86 into boogie-org:master Aug 11, 2023
4 checks passed

This was referenced Aug 15, 2023

Uses clauses are not printed to file #599

Closed

Prune is nondeterministic with -vcsCores:2 #560

Closed

zafer-esen mentioned this pull request Aug 18, 2023

Optimize uses clauses dafny-lang/dafny#4428

Merged


		private IList<Axiom> definitionAxioms = new List<Axiom>();

		public bool RemoveDefinitionAxiom(Axiom axiom)

Fixes lost dependencies for pruning during monomorphization. #767

Fixes lost dependencies for pruning during monomorphization. #767

Conversation

zafer-esen commented Aug 3, 2023 • edited by shazqadeer Loading

shazqadeer commented Aug 4, 2023

keyboardDrummer commented Aug 4, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zafer-esen commented Aug 4, 2023 • edited Loading

zafer-esen commented Aug 4, 2023 • edited Loading

shazqadeer commented Aug 4, 2023

zafer-esen commented Aug 5, 2023 • edited Loading

shazqadeer commented Aug 7, 2023

zafer-esen commented Aug 7, 2023

shazqadeer commented Aug 7, 2023 • edited Loading

zafer-esen commented Aug 7, 2023

zafer-esen commented Aug 7, 2023

keyboardDrummer commented Aug 7, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shazqadeer commented Aug 7, 2023 • edited Loading

keyboardDrummer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Aug 7, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shazqadeer Aug 8, 2023 • edited Loading

Choose a reason for hiding this comment

zafer-esen Aug 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shazqadeer Aug 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zafer-esen commented Aug 8, 2023

zafer-esen commented Aug 9, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zafer-esen Aug 9, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zafer-esen commented Aug 10, 2023 • edited Loading

keyboardDrummer commented Aug 11, 2023

keyboardDrummer commented Aug 11, 2023

shazqadeer commented Sep 13, 2023

zafer-esen commented Sep 13, 2023 • edited Loading

keyboardDrummer commented Sep 14, 2023

zafer-esen commented Aug 3, 2023 •

edited by shazqadeer

Loading

zafer-esen commented Aug 4, 2023 •

edited

Loading

zafer-esen commented Aug 4, 2023 •

edited

Loading

zafer-esen commented Aug 5, 2023 •

edited

Loading

shazqadeer commented Aug 7, 2023 •

edited

Loading

keyboardDrummer commented Aug 7, 2023 •

edited

Loading

shazqadeer commented Aug 7, 2023 •

edited

Loading

keyboardDrummer Aug 7, 2023 •

edited

Loading

shazqadeer Aug 8, 2023 •

edited

Loading

zafer-esen Aug 8, 2023 •

edited

Loading

shazqadeer Aug 8, 2023 •

edited

Loading

zafer-esen Aug 9, 2023 •

edited

Loading

zafer-esen commented Aug 10, 2023 •

edited

Loading

zafer-esen commented Sep 13, 2023 •

edited

Loading