diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 71e370470..3446ab80f 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1429,7 +1429,23 @@ public class Constant : Variable // from all other constants. public readonly bool Unique; - public IList DefinitionAxioms { get; } + public IList DefinitionAxioms => definitionAxioms; + + private IList definitionAxioms = new List(); + + public bool RemoveDefinitionAxiom(Axiom axiom) + { + Contract.Requires(axiom != null); + + return definitionAxioms.Remove(axiom); + } + + public void AddDefinitionAxiom(Axiom axiom) + { + Contract.Requires(axiom != null); + + DefinitionAxioms.Add(axiom); + } public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent) : this(tok, typedIdent, true) @@ -1452,7 +1468,7 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0); Contract.Requires(typedIdent.WhereExpr == null); this.Unique = unique; - this.DefinitionAxioms = definitionAxioms ?? new List(); + this.definitionAxioms = definitionAxioms ?? new List(); } public override bool IsMutable => false; @@ -2058,6 +2074,13 @@ public void AddOtherDefinitionAxiom(Axiom axiom) otherDefinitionAxioms.Add(axiom); } + public bool RemoveOtherDefinitionAxiom(Axiom axiom) + { + Contract.Requires(axiom != null); + + return otherDefinitionAxioms.Remove(axiom); + } + private bool neverTrigger; private bool neverTriggerComputed; diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs index dbba7eb5f..4baf03243 100644 --- a/Source/Core/Monomorphization.cs +++ b/Source/Core/Monomorphization.cs @@ -7,7 +7,7 @@ namespace Microsoft.Boogie { - public class MonomorphismChecker : ReadOnlyVisitor + sealed public class MonomorphismChecker : ReadOnlyVisitor { // This visitor checks if the program is already monomorphic. @@ -131,11 +131,13 @@ class MonomorphizableChecker : ReadOnlyVisitor * This visitor checks if the program is monomorphizable. It calculates one status value from * the enum MonomorphizableStatus for the program. */ - public static MonomorphizableStatus IsMonomorphizable(Program program, out HashSet polymorphicFunctionAxioms) + public static MonomorphizableStatus IsMonomorphizable(Program program, out HashSet polymorphicFunctionAxioms, + out Dictionary, HashSet)> axiomsThatWillLoseQuantifiers) { var checker = new MonomorphizableChecker(program); checker.VisitProgram(program); polymorphicFunctionAxioms = checker.polymorphicFunctionAxioms; + axiomsThatWillLoseQuantifiers = checker.axiomsThatWillLoseQuantifiers; if (!checker.isMonomorphizable) { return MonomorphizableStatus.UnhandledPolymorphism; @@ -148,7 +150,9 @@ public static MonomorphizableStatus IsMonomorphizable(Program program, out HashS } private bool isMonomorphizable; + private Axiom curAxiom; private HashSet polymorphicFunctionAxioms; + private Dictionary, HashSet)> axiomsThatWillLoseQuantifiers; private Graph typeVariableDependencyGraph; // (T,U) in this graph iff T flows to U private HashSet> strongDependencyEdges; // (T,U) in this set iff a type constructed from T flows into U @@ -158,6 +162,8 @@ private MonomorphizableChecker(Program program) polymorphicFunctionAxioms = program.TopLevelDeclarations.OfType() .Where(f => f.TypeParameters.Count > 0 && f.DefinitionAxiom != null) .Select(f => f.DefinitionAxiom).ToHashSet(); + axiomsThatWillLoseQuantifiers = new Dictionary, HashSet)>(); + curAxiom = null; typeVariableDependencyGraph = new Graph(); strongDependencyEdges = new HashSet>(); } @@ -179,7 +185,51 @@ private bool IsFinitelyInstantiable() } return true; } - + + public override Axiom VisitAxiom(Axiom node) + { + curAxiom = node; + var res = base.VisitAxiom(node); + curAxiom = null; + return res; + } + + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) + { + if (curAxiom != null && node.TypeParameters.Any() && !node.Dummies.Any() && + node.Triggers != null && node.Triggers.Tr.Any()) + { + // This expression will be instantiated into non-quantified expressions. + // Since pruning (currently) depends on triggers and `uses` clauses, + // if the enclosing axiom is not already inside a uses clause, it can + // be incorrectly pruned away. + if (!axiomsThatWillLoseQuantifiers.ContainsKey(curAxiom)) + { + axiomsThatWillLoseQuantifiers[curAxiom] = (new HashSet(), new HashSet()); + } + + var fc = new MonomorphizationVisitor.FunctionAndConstantCollector(); + node.Triggers.Tr.ForEach(expr => fc.VisitExpr(expr)); + var triggerConstants = fc.GetConstants(); + var triggerFunctions = fc.GetFunctions(); + + var functionsAndConstants = axiomsThatWillLoseQuantifiers[curAxiom]; + + if (triggerConstants.Any()) + { + triggerConstants.ForEach(c => functionsAndConstants.Item2.Add(c)); + } + + if (triggerFunctions.Any()) + { + triggerFunctions.ForEach(f => functionsAndConstants.Item1.Add(f)); + } + + axiomsThatWillLoseQuantifiers[curAxiom] = functionsAndConstants; + } + return base.VisitQuantifierExpr(node); + } + public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall functionCall) @@ -615,23 +665,6 @@ class PolymorphicMapAndBinderSubstituter : VarDeclOnceStandardVisitor // be applied. private List splitAxioms; - private Dictionary> binderExprToTypes = null; - public List lookupTypeForBinderExpr(Expr binderExpr) - { - if (binderExprToTypes == null) - { - binderExprToTypes = new Dictionary>(); - foreach (var binderMonomorphizer in binderExprMonomorphizers.Values) - { - foreach ((var types, var expr) in binderMonomorphizer.instanceExprs) - { - binderExprToTypes.TryAdd(expr, types); - } - } - } - return binderExprToTypes.TryGetValue(binderExpr, out var res) ? res : new List(); - } - public PolymorphicMapAndBinderSubstituter(MonomorphizationVisitor monomorphizationVisitor) { this.monomorphizationVisitor = monomorphizationVisitor; @@ -664,13 +697,13 @@ public override Axiom VisitAxiom(Axiom node) stack.Push(nAryExpr.Args[0]); stack.Push(nAryExpr.Args[1]); } - else if (expr == axiom.Expr) - { - splitAxioms.Add(axiom); - } else { - splitAxioms.Add(new Axiom(Token.NoToken, expr)); + var newAxiom = new Axiom(Token.NoToken, expr); + if(monomorphizationVisitor.oldToNewAxioms.ContainsKey(axiom)) { + monomorphizationVisitor.oldToNewAxioms[axiom].Add(newAxiom); + } + splitAxioms.Add(newAxiom); } } return axiom; @@ -1302,7 +1335,7 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor private Dictionary nameToProcedure; private Dictionary nameToImplementation; private Dictionary nameToTypeCtorDecl; - private Dictionary, Function>> functionInstantiations; + public Dictionary, Function>> functionInstantiations; private Dictionary, Procedure>> procInstantiations; private Dictionary, Implementation>> implInstantiations; private Dictionary, TypeCtorDecl>> typeInstantiations; @@ -1314,11 +1347,19 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor private HashSet visitedTypeCtorDecls; private HashSet visitedFunctions; private Dictionary procToImpl; + public readonly HashSet originalFunctions; + public readonly HashSet originalConstants; + public readonly Dictionary> oldToNewAxioms; // TODO: optimize using this + public readonly Dictionary oldAxiomToOriginalAxioms; // private MonomorphizationVisitor(CoreOptions options, Program program, HashSet polymorphicFunctionAxioms) { Options = options; this.program = program; + originalFunctions = program.Functions.ToHashSet(); + originalConstants = program.Constants.ToHashSet(); + oldToNewAxioms = program.Axioms.ToDictionary(ax => ax, _ => new HashSet()); + oldAxiomToOriginalAxioms = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() ); implInstantiations = new Dictionary, Implementation>>(); nameToImplementation = new Dictionary(); program.TopLevelDeclarations.OfType().Where(impl => impl.TypeParameters.Count > 0).ForEach( @@ -1370,9 +1411,11 @@ decl is TypeSynonymDecl typeSynonymDecl && typeSynonymDecl.TypeParameters.Count decl is Axiom axiom && polymorphicFunctionAxioms.Contains(axiom)); } - public static MonomorphizationVisitor Initialize(CoreOptions options, Program program, HashSet polymorphicFunctionAxioms) + public static MonomorphizationVisitor Initialize(CoreOptions options, Program program, HashSet polymorphicFunctionAxioms, + Dictionary, HashSet)> axiomsThatWillLoseQuantifiers) { - 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(); @@ -1399,33 +1442,137 @@ public static MonomorphizationVisitor Initialize(CoreOptions options, Program pr monomorphizationVisitor.polymorphicMapInfos.Values.Select(polymorphicMapInfo => polymorphicMapInfo.CreateDatatypeTypeCtorDecl(polymorphicMapAndBinderSubstituter)).ToList(); var splitAxioms = polymorphicMapAndBinderSubstituter.Substitute(program); + UpdateDependencies(splitAxioms, monomorphizationVisitor, axiomsThatWillLoseQuantifiers); program.RemoveTopLevelDeclarations(decl => decl is Axiom); - foreach (var axiom in splitAxioms) + program.AddTopLevelDeclarations(splitAxioms); + program.AddTopLevelDeclarations(polymorphicMapDatatypeCtorDecls); + Contract.Assert(MonomorphismChecker.IsMonomorphic(program)); + return monomorphizationVisitor; + } + + private static void UpdateDependencies(List splitAxioms, MonomorphizationVisitor monomorphizationVisitor, + Dictionary, HashSet)> axiomsThatWillLoseQuantifiers) + { + // Original program axioms were replaced with new splitAxioms. Program constants and functions that had + // those original axioms as dependencies need their references updated to the new axioms. + // Axioms / functions could both have been instantiated, which adds some complexity. + // Furthermore, current pruning depends on symbols in triggers in quantified axioms to compute dependencies, + // which might have been lost during instantiation (i.e., axiom [forall | exists] :: ...). These are tracked + // separately and added as dependencies to corresponding constants and functions + + foreach (var (oldAxiom, newAxioms) in monomorphizationVisitor.oldToNewAxioms) { - if (axiom.FunctionDependencies != null) + var oldAxiomFC = new FunctionAndConstantCollector(); + var unmodifiedOldAxiom = monomorphizationVisitor.oldAxiomToOriginalAxioms[oldAxiom]; + oldAxiomFC.Visit(unmodifiedOldAxiom); + var oldAxiomFunctions = oldAxiomFC.GetFunctions(); + + Dictionary> newAxiomFunctions = new Dictionary>(); + Dictionary> newAxiomConstants = new Dictionary>(); + + foreach (var newAxiom in newAxioms) + { + var newAxiomFC = new FunctionAndConstantCollector(); + newAxiomFC.Visit(newAxiom); + newAxiomFunctions.Add(newAxiom, newAxiomFC.GetFunctions()); + newAxiomConstants.Add(newAxiom, newAxiomFC.GetConstants()); + } + + void UpdateFunctionDependencies(HashSet functions, bool forceDependency = false) { - var functionDependenciesCopy = new List(axiom.FunctionDependencies); - foreach (var function in functionDependenciesCopy) + foreach (var function in functions) { - if (monomorphizationVisitor.functionInstantiations.TryGetValue(function, out var instFuncsMap)) + if (function.DefinitionAxioms.Contains(oldAxiom) || forceDependency) { - var types = polymorphicMapAndBinderSubstituter.lookupTypeForBinderExpr(axiom.Expr); - if (types.Any() && instFuncsMap.ContainsKey(types)) + if (function.DefinitionAxiom == oldAxiom) + { + function.DefinitionAxiom = null; // is moving DefinitionAxiom to OtherDefinitionAxioms OK? + } + foreach (var newAxiom in newAxioms) { - var newFunction = instFuncsMap[types]; - if (!newFunction.DefinitionAxioms.Contains(axiom)) + if (function.TypeParameters.Any()) // Polymorphic function { - newFunction.AddOtherDefinitionAxiom(axiom); + var instancesToAddDependency = oldAxiomFunctions.Contains(function) + ? newAxiomFunctions[newAxiom] + : monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet(); + foreach (var inst in instancesToAddDependency) + { + inst.AddOtherDefinitionAxiom(newAxiom); + } } + else + { + // Non-monomorphized function + if (!oldAxiomFunctions.Contains(function) || newAxiomFunctions[newAxiom].Contains(function)) + { + function.AddOtherDefinitionAxiom(newAxiom); + } + } + } + function.RemoveOtherDefinitionAxiom(oldAxiom); + } + } + } + + void UpdateConstantDependencies(HashSet constants) + { + foreach (var constant in constants) + { + if (constant.DefinitionAxioms.Contains(oldAxiom)) + { + foreach (var newAxiom in newAxioms.Where(ax => newAxiomConstants[ax].Contains(constant))) + { + constant.AddDefinitionAxiom(newAxiom); } + constant.RemoveDefinitionAxiom(oldAxiom); } } } + + UpdateConstantDependencies(monomorphizationVisitor.originalConstants); + UpdateFunctionDependencies(monomorphizationVisitor.originalFunctions); + + if (axiomsThatWillLoseQuantifiers.TryGetValue(oldAxiom, out var pair)) + { + UpdateFunctionDependencies(pair.Item1, true); + UpdateConstantDependencies(pair.Item2); + } } - program.AddTopLevelDeclarations(splitAxioms); - program.AddTopLevelDeclarations(polymorphicMapDatatypeCtorDecls); - Contract.Assert(MonomorphismChecker.IsMonomorphic(program)); - return monomorphizationVisitor; + } + + public class FunctionAndConstantCollector : ReadOnlyVisitor + { + private readonly HashSet functions = new HashSet(); + private readonly HashSet constants = new HashSet(); + private bool hasTriggers = false; + + public override Expr VisitNAryExpr(NAryExpr node) + { + if (node.Fun is FunctionCall functionCall) + { + functions.Add(functionCall.Func); + } + return base.VisitNAryExpr(node); + } + + public override Trigger VisitTrigger(Trigger node) + { + hasTriggers = true; + return base.VisitTrigger(node); + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + if (node.Decl is Constant c) + { + constants.Add(c); + } + return base.VisitIdentifierExpr(node); + } + + public HashSet GetFunctions() => functions; + public HashSet GetConstants() => constants; + public bool HasTriggers() => hasTriggers; } /* @@ -1535,6 +1682,9 @@ private Axiom InstantiateAxiom(Axiom axiom, List actualTypeParams) { var axiomExpr = InstantiateBinderExpr((BinderExpr)axiom.Expr, actualTypeParams); var instantiatedAxiom = new Axiom(axiom.tok, axiomExpr, axiom.Comment, axiom.Attributes); + if(oldToNewAxioms.ContainsKey(axiom)) { + oldToNewAxioms[axiom].Add(instantiatedAxiom); + } newInstantiatedDeclarations.Add(instantiatedAxiom); return instantiatedAxiom; } @@ -1931,11 +2081,13 @@ public class Monomorphizer public static MonomorphizableStatus Monomorphize(CoreOptions options, Program program) { - var monomorphizableStatus = MonomorphizableChecker.IsMonomorphizable(program, out var polymorphicFunctionAxioms); + var monomorphizableStatus = MonomorphizableChecker.IsMonomorphizable(program, + out var polymorphicFunctionAxioms, out var axiomsThatWillLoseQuantifiers); if (monomorphizableStatus == MonomorphizableStatus.Monomorphizable) { - var monomorphizationVisitor = MonomorphizationVisitor.Initialize(options, program, polymorphicFunctionAxioms); - program.monomorphizer = new Monomorphizer(monomorphizationVisitor); + var monomorphizationVisitor = + MonomorphizationVisitor.Initialize(options, program, polymorphicFunctionAxioms, axiomsThatWillLoseQuantifiers); + program.monomorphizer = new Monomorphizer(monomorphizationVisitor, axiomsThatWillLoseQuantifiers); } return monomorphizableStatus; } @@ -1979,9 +2131,12 @@ public List GetTypeInstantiation(TypeCtorDecl decl) } private MonomorphizationVisitor monomorphizationVisitor; - private Monomorphizer(MonomorphizationVisitor monomorphizationVisitor) + private Dictionary, HashSet)> axiomsThatWillLoseQuantifiers; + private Monomorphizer(MonomorphizationVisitor monomorphizationVisitor, + Dictionary, HashSet)> axiomsThatWillLoseQuantifiers) { this.monomorphizationVisitor = monomorphizationVisitor; + this.axiomsThatWillLoseQuantifiers = axiomsThatWillLoseQuantifiers; } } } \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 74bd1301b..78d20b958 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -412,7 +412,6 @@ public PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, } else if (Options.TypeEncodingMethod == CoreOptions.TypeEncoding.Monomorphic) { - DependencyCollector.Collect(Options, program); var monomorphizableStatus = Monomorphizer.Monomorphize(Options, program); if (monomorphizableStatus == MonomorphizableStatus.Monomorphizable) {