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

Fixes lost dependencies for pruning during monomorphization. #767

Merged
merged 16 commits into from
Aug 11, 2023
Merged

Fixes lost dependencies for pruning during monomorphization. #767

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
41d2e86
Attempts to fix the lost dependencies during monomoprhization.
zafer-esen Aug 2, 2023
2f21837
Fixes too much pruning when using monomorphization.
zafer-esen Aug 3, 2023
89643d8
Update failing test output.
zafer-esen Aug 3, 2023
e059d8e
Simplify Constant methods in Absy.cs.
zafer-esen Aug 4, 2023
d50af6f
Remove automatic preservation of polymorphic quantifier dependencies.
zafer-esen Aug 7, 2023
06e99f9
Rename some variables as requested in #767.
zafer-esen Aug 7, 2023
8ac0139
Expose OtherDefinitionAxioms and uppercase public member
zafer-esen Aug 7, 2023
0024600
Update failing grammar test file.
zafer-esen Aug 7, 2023
c6b2762
Address more comments from #767 in monomorphization code.
zafer-esen Aug 8, 2023
e4d5c99
Make some public members private / protected.
zafer-esen Aug 8, 2023
b7c14eb
Fixes an issue where unnecessary dependencies were added.
zafer-esen Aug 8, 2023
7b28f0e
Only store symbol collector instead of original axiom copies.
zafer-esen Aug 8, 2023
d296215
Add tests and update how pruned files are printed.
zafer-esen Aug 9, 2023
9eb3ab9
Clarify test explanation and fix indentation.
zafer-esen Aug 9, 2023
1f14fac
Clarify comments in test.
zafer-esen Aug 9, 2023
9d8c497
Merge branch 'master' into master
keyboardDrummer Aug 11, 2023
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
15 changes: 3 additions & 12 deletions Source/Core/AST/Absy.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1429,7 +1429,7 @@ public class Constant : Variable
// from all other constants.
public readonly bool Unique;

public IList<Axiom> DefinitionAxioms { get; }
public IList<Axiom> DefinitionAxioms { get; set; }

public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent)
: this(tok, typedIdent, true)
Expand Down Expand Up @@ -2045,18 +2045,9 @@ public class Function : DeclWithFormals
public NAryExpr DefinitionBody; // Only set if the function is declared with {:define}
public Axiom DefinitionAxiom;

public IList<Axiom> otherDefinitionAxioms = new List<Axiom>();
public IList<Axiom> OtherDefinitionAxioms = new List<Axiom>();
public IEnumerable<Axiom> DefinitionAxioms =>
(DefinitionAxiom == null ? Enumerable.Empty<Axiom>() : new[]{ DefinitionAxiom }).Concat(otherDefinitionAxioms);

public IEnumerable<Axiom> OtherDefinitionAxioms => otherDefinitionAxioms;

public void AddOtherDefinitionAxiom(Axiom axiom)
{
Contract.Requires(axiom != null);

otherDefinitionAxioms.Add(axiom);
}
(DefinitionAxiom == null ? Enumerable.Empty<Axiom>() : new[]{ DefinitionAxiom }).Concat(OtherDefinitionAxioms);

private bool neverTrigger;
private bool neverTriggerComputed;
Expand Down
2 changes: 1 addition & 1 deletion Source/Core/BoogiePL.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,7 +477,7 @@ Function<.out List<Declaration>/*!*/ ds.>
new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
foreach(var axiom in axioms) {
ds.Add(axiom);
func.AddOtherDefinitionAxiom(axiom);
func.OtherDefinitionAxioms.Add(axiom);
}

Contract.Assert(func != null);
Expand Down
161 changes: 144 additions & 17 deletions Source/Core/Monomorphization.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ private bool IsFinitelyInstantiable()
}
return true;
}

public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is FunctionCall functionCall)
Expand Down Expand Up @@ -343,12 +343,12 @@ abstract class BinderExprMonomorphizer
*/

protected MonomorphizationVisitor monomorphizationVisitor;
protected Dictionary<List<Type>, Expr> instanceExprs;
public Dictionary<List<Type>, Expr> InstanceExprs { get; }

public BinderExprMonomorphizer(MonomorphizationVisitor monomorphizationVisitor)
{
this.monomorphizationVisitor = monomorphizationVisitor;
instanceExprs = new Dictionary<List<Type>, Expr>(new ListComparer<Type>());
InstanceExprs = new Dictionary<List<Type>, Expr>(new ListComparer<Type>());
}

// Returns the BinderExpr for which this instance of BinderExprMonomorphizer was created.
Expand Down Expand Up @@ -377,20 +377,20 @@ public LambdaExprMonomorphizer(LambdaExpr lambdaExpr, MonomorphizationVisitor mo
public override bool Instantiate()
{
var polymorphicMapInfo = monomorphizationVisitor.RegisterPolymorphicMapType(lambdaExpr.Type);
Debug.Assert(instanceExprs.Count <= polymorphicMapInfo.Instances.Count);
if (instanceExprs.Count == polymorphicMapInfo.Instances.Count)
Debug.Assert(InstanceExprs.Count <= polymorphicMapInfo.Instances.Count);
if (InstanceExprs.Count == polymorphicMapInfo.Instances.Count)
{
return false;
}
polymorphicMapInfo.Instances.Skip(instanceExprs.Count).ForEach(x =>
instanceExprs[x] = monomorphizationVisitor.InstantiateBinderExpr(lambdaExpr, x));
polymorphicMapInfo.Instances.Skip(InstanceExprs.Count).ForEach(x =>
InstanceExprs[x] = monomorphizationVisitor.InstantiateBinderExpr(lambdaExpr, x));
return true;
}

public override Expr MonomorphicExpr(PolymorphicMapAndBinderSubstituter substituter)
{
return substituter.VisitExpr(monomorphizationVisitor.RegisterPolymorphicMapType(lambdaExpr.Type)
.GetLambdaConstructor(instanceExprs));
.GetLambdaConstructor(InstanceExprs));
}
}

Expand All @@ -410,7 +410,7 @@ protected QuantifierExprMonomorphizer(QuantifierExpr quantifierExpr, Monomorphiz

public override bool Instantiate()
{
var instanceExprsCount = instanceExprs.Count;
var instanceExprsCount = InstanceExprs.Count;
var typeParameterIndexToTypeHints = Enumerable.Range(0, quantifierExpr.TypeParameters.Count)
.Select(_ => new HashSet<Type>()).ToList();
for (int typeParameterIndex = 0; typeParameterIndex < quantifierExpr.TypeParameters.Count; typeParameterIndex++)
Expand All @@ -428,16 +428,16 @@ public override bool Instantiate()
}
}
InstantiateOne(typeParameterIndexToTypeHints, new List<Type>());
return instanceExprsCount < instanceExprs.Count;
return instanceExprsCount < InstanceExprs.Count;
}

private void InstantiateOne(List<HashSet<Type>> typeParameterIndexToTypeHints, List<Type> actualTypeParams)
{
if (typeParameterIndexToTypeHints.Count == actualTypeParams.Count)
{
if (!instanceExprs.ContainsKey(actualTypeParams))
if (!InstanceExprs.ContainsKey(actualTypeParams))
{
instanceExprs[new List<Type>(actualTypeParams)] =
InstanceExprs[new List<Type>(actualTypeParams)] =
monomorphizationVisitor.InstantiateBinderExpr(quantifierExpr, actualTypeParams);
}
return;
Expand All @@ -462,7 +462,7 @@ public ForallExprMonomorphizer(ForallExpr forallExpr, MonomorphizationVisitor mo

public override Expr MonomorphicExpr(PolymorphicMapAndBinderSubstituter substituter)
{
return Expr.And(instanceExprs.Values.Select(x => substituter.VisitExpr(x)));
return Expr.And(InstanceExprs.Values.Select(x => substituter.VisitExpr(x)));
}
}

Expand All @@ -475,7 +475,7 @@ public ExistsExprMonomorphizer(ExistsExpr existsExpr, MonomorphizationVisitor mo

public override Expr MonomorphicExpr(PolymorphicMapAndBinderSubstituter substituter)
{
return Expr.Or(instanceExprs.Values.Select(x => substituter.VisitExpr(x)));
return Expr.Or(InstanceExprs.Values.Select(x => substituter.VisitExpr(x)));
}
}

Expand Down Expand Up @@ -649,7 +649,11 @@ public override Axiom VisitAxiom(Axiom node)
}
else
{
splitAxioms.Add(new Axiom(Token.NoToken, expr));
var newAxiom = new Axiom(Token.NoToken, expr);
if (monomorphizationVisitor.originalAxiomToSplitAxioms.ContainsKey(axiom)) {
monomorphizationVisitor.originalAxiomToSplitAxioms[axiom].Add(newAxiom);
}
splitAxioms.Add(newAxiom);
}
}
return axiom;
Expand Down Expand Up @@ -1281,7 +1285,7 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor
private Dictionary<string, Procedure> nameToProcedure;
private Dictionary<string, Implementation> nameToImplementation;
private Dictionary<string, TypeCtorDecl> nameToTypeCtorDecl;
private Dictionary<Function, Dictionary<List<Type>, Function>> functionInstantiations;
public Dictionary<Function, Dictionary<List<Type>, Function>> functionInstantiations;
private Dictionary<Procedure, Dictionary<List<Type>, Procedure>> procInstantiations;
private Dictionary<Implementation, Dictionary<List<Type>, Implementation>> implInstantiations;
private Dictionary<TypeCtorDecl, Dictionary<List<Type>, TypeCtorDecl>> typeInstantiations;
Expand All @@ -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 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;
Copy link
Contributor

@shazqadeer shazqadeer Aug 8, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

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.

Copy link
Contributor Author

@zafer-esen zafer-esen Aug 8, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.

Copy link
Contributor

@shazqadeer shazqadeer Aug 8, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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


private MonomorphizationVisitor(CoreOptions options, Program program, HashSet<Axiom> polymorphicFunctionAxioms)
{
Options = options;
this.program = program;
originalFunctions = program.Functions.ToHashSet();
originalConstants = program.Constants.ToHashSet();
originalAxiomToSplitAxioms = program.Axioms.ToDictionary(ax => ax, _ => new HashSet<Axiom>());
originalAxiomToUninstantiatedCopies = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() );
implInstantiations = new Dictionary<Implementation, Dictionary<List<Type>, Implementation>>();
nameToImplementation = new Dictionary<string, Implementation>();
program.TopLevelDeclarations.OfType<Implementation>().Where(impl => impl.TypeParameters.Count > 0).ForEach(
Expand Down Expand Up @@ -1351,7 +1364,8 @@ decl is TypeSynonymDecl typeSynonymDecl && typeSynonymDecl.TypeParameters.Count

public static MonomorphizationVisitor Initialize(CoreOptions options, Program program, HashSet<Axiom> polymorphicFunctionAxioms)
{
var monomorphizationVisitor = new MonomorphizationVisitor(options, program, polymorphicFunctionAxioms);
var monomorphizationVisitor =
new MonomorphizationVisitor(options, program, polymorphicFunctionAxioms);
// ctorTypes contains all the uninterpreted types created for monomorphizing top-level polymorphic implementations
// that must be verified. The types in ctorTypes are reused across different implementations.
var ctorTypes = new List<Type>();
Expand All @@ -1378,13 +1392,123 @@ public static MonomorphizationVisitor Initialize(CoreOptions options, Program pr
monomorphizationVisitor.polymorphicMapInfos.Values.Select(polymorphicMapInfo =>
polymorphicMapInfo.CreateDatatypeTypeCtorDecl(polymorphicMapAndBinderSubstituter)).ToList();
var splitAxioms = polymorphicMapAndBinderSubstituter.Substitute(program);
UpdateDependencies(monomorphizationVisitor);
program.RemoveTopLevelDeclarations(decl => decl is Axiom);
program.AddTopLevelDeclarations(splitAxioms);
program.AddTopLevelDeclarations(polymorphicMapDatatypeCtorDecls);
Contract.Assert(MonomorphismChecker.IsMonomorphic(program));
return monomorphizationVisitor;
}

private static void UpdateDependencies(MonomorphizationVisitor monomorphizationVisitor)
{
// Original program axioms were replaced with new splitAxioms. Program constants and functions that had
zafer-esen marked this conversation as resolved.
Show resolved Hide resolved
// those original axioms as dependencies need their references updated to the new axioms.
// Axioms / functions could both have been instantiated, which adds some complexity.

foreach (var (oldAxiom, newAxioms) in monomorphizationVisitor.originalAxiomToSplitAxioms)
{
var oldAxiomFC = new FunctionAndConstantCollector();
var unmodifiedOldAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopies[oldAxiom];
oldAxiomFC.Visit(unmodifiedOldAxiom);
var oldAxiomFunctions = oldAxiomFC.Functions;

Dictionary<Axiom, HashSet<Function>> newAxiomFunctions = new Dictionary<Axiom, HashSet<Function>>();
Copy link
Collaborator

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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

Dictionary<Axiom, HashSet<Constant>> newAxiomConstants = new Dictionary<Axiom, HashSet<Constant>>();

foreach (var newAxiom in newAxioms)
{
var newAxiomFC = new FunctionAndConstantCollector();
newAxiomFC.Visit(newAxiom);
newAxiomFunctions.Add(newAxiom, newAxiomFC.Functions);
newAxiomConstants.Add(newAxiom, newAxiomFC.Constants);
}

void UpdateFunctionDependencies(HashSet<Function> functions)
Copy link
Collaborator

Choose a reason for hiding this comment

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

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.

{
foreach (var function in functions)
Copy link
Collaborator

@keyboardDrummer keyboardDrummer Aug 7, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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

{
if (function.DefinitionAxioms.Contains(oldAxiom))
zafer-esen marked this conversation as resolved.
Show resolved Hide resolved
{
if (function.DefinitionAxiom == oldAxiom)
{
function.DefinitionAxiom = null;
}
foreach (var newAxiom in newAxioms)
{
if (function.TypeParameters.Any()) // Polymorphic function
{
var instancesToAddDependency = oldAxiomFunctions.Contains(function)
? newAxiomFunctions[newAxiom]
: monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet();
foreach (var inst in instancesToAddDependency)
{
inst.OtherDefinitionAxioms.Add(newAxiom);
}
}
else // Non-monomorphized function
{
if (!oldAxiomFunctions.Contains(function) || newAxiomFunctions[newAxiom].Contains(function))
{
function.OtherDefinitionAxioms.Add(newAxiom);
}
}
}
function.OtherDefinitionAxioms.Remove(oldAxiom);
}
}
}

void UpdateConstantDependencies(HashSet<Constant> constants)
{
foreach (var constant in constants)
{
if (constant.DefinitionAxioms.Contains(oldAxiom))
{
foreach (var newAxiom in newAxioms.Where(ax => newAxiomConstants[ax].Contains(constant)))
{
constant.DefinitionAxioms.Add(newAxiom);
}
constant.DefinitionAxioms.Remove(oldAxiom);
}
}
}

UpdateConstantDependencies(monomorphizationVisitor.originalConstants);
UpdateFunctionDependencies(monomorphizationVisitor.originalFunctions);
}
}

public class FunctionAndConstantCollector : ReadOnlyVisitor
{
public HashSet<Function> Functions { get; }
public HashSet<Constant> Constants { get; }

public FunctionAndConstantCollector()
{
Functions = new HashSet<Function>();
Constants = new HashSet<Constant>();
}

public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is FunctionCall functionCall)
{
Functions.Add(functionCall.Func);
}
return base.VisitNAryExpr(node);
}

public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
if (node.Decl is Constant c)
{
Constants.Add(c);
}
return base.VisitIdentifierExpr(node);
}
}

/*
* Binder expressions may be nested inside other binder expressions. The instantiation of known binder
* expressions using known type and function instantiations may discover more binder expressions and
Expand Down Expand Up @@ -1492,6 +1616,9 @@ private Axiom InstantiateAxiom(Axiom axiom, List<Type> actualTypeParams)
{
var axiomExpr = InstantiateBinderExpr((BinderExpr)axiom.Expr, actualTypeParams);
var instantiatedAxiom = new Axiom(axiom.tok, axiomExpr, axiom.Comment, axiom.Attributes);
if (originalAxiomToSplitAxioms.ContainsKey(axiom)) {
originalAxiomToSplitAxioms[axiom].Add(instantiatedAxiom);
}
newInstantiatedDeclarations.Add(instantiatedAxiom);
return instantiatedAxiom;
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Core/Parser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -451,7 +451,7 @@ void Function(out List<Declaration>/*!*/ ds) {
new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
foreach(var axiom in axioms) {
ds.Add(axiom);
func.AddOtherDefinitionAxiom(axiom);
func.OtherDefinitionAxioms.Add(axiom);
}

Contract.Assert(func != null);
Expand Down
2 changes: 1 addition & 1 deletion Source/ExecutionEngine/VerificationResultCache.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -507,7 +507,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
{
// We found a function call within a trigger of a quantifier expression, or the function does not take any
// arguments so we don't expect it ever to sit inside a quantifier.
funCall.Func.AddOtherDefinitionAxiom(currentAxiom);
funCall.Func.OtherDefinitionAxioms.Add(currentAxiom);
}
}

Expand Down
Loading