diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 71e370470..b9eff070a 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1429,7 +1429,7 @@ public class Constant : Variable // from all other constants. public readonly bool Unique; - public IList DefinitionAxioms { get; } + public IList DefinitionAxioms { get; set; } public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent) : this(tok, typedIdent, true) @@ -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 otherDefinitionAxioms = new List(); + public IList OtherDefinitionAxioms = new List(); public IEnumerable DefinitionAxioms => - (DefinitionAxiom == null ? Enumerable.Empty() : new[]{ DefinitionAxiom }).Concat(otherDefinitionAxioms); - - public IEnumerable OtherDefinitionAxioms => otherDefinitionAxioms; - - public void AddOtherDefinitionAxiom(Axiom axiom) - { - Contract.Requires(axiom != null); - - otherDefinitionAxioms.Add(axiom); - } + (DefinitionAxiom == null ? Enumerable.Empty() : new[]{ DefinitionAxiom }).Concat(OtherDefinitionAxioms); private bool neverTrigger; private bool neverTriggerComputed; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index af59e22df..d0e35bac5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -477,7 +477,7 @@ Function<.out List/*!*/ 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); diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs index ffdfa2e2c..2914e9967 100644 --- a/Source/Core/Monomorphization.cs +++ b/Source/Core/Monomorphization.cs @@ -179,7 +179,7 @@ private bool IsFinitelyInstantiable() } return true; } - + public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall functionCall) @@ -343,9 +343,9 @@ abstract class BinderExprMonomorphizer */ protected MonomorphizationVisitor monomorphizationVisitor; - protected Dictionary, Expr> instanceExprs; + protected Dictionary, Expr> instanceExprs { get; } - public BinderExprMonomorphizer(MonomorphizationVisitor monomorphizationVisitor) + protected BinderExprMonomorphizer(MonomorphizationVisitor monomorphizationVisitor) { this.monomorphizationVisitor = monomorphizationVisitor; instanceExprs = new Dictionary, Expr>(new ListComparer()); @@ -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; @@ -1274,7 +1278,7 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor * children has been finalized. */ - public CoreOptions Options { get; } + private CoreOptions Options { get; } private Program program; private Dictionary nameToFunction; @@ -1293,11 +1297,20 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor private HashSet visitedTypeCtorDecls; private HashSet visitedFunctions; private Dictionary procToImpl; + private readonly HashSet originalFunctions; + private readonly HashSet originalConstants; + // Note that original axioms refer to axioms of the original program which might have been updated in-place during monomorphization. + public readonly Dictionary> originalAxiomToSplitAxioms; + private readonly Dictionary originalAxiomToOriginalSymbols; private MonomorphizationVisitor(CoreOptions options, Program program, HashSet polymorphicFunctionAxioms) { Options = options; this.program = program; + originalFunctions = program.Functions.ToHashSet(); + originalConstants = program.Constants.ToHashSet(); + originalAxiomToSplitAxioms = program.Axioms.ToDictionary(ax => ax, _ => new HashSet()); + originalAxiomToOriginalSymbols = program.Axioms.ToDictionary(ax => ax, ax => new FunctionAndConstantCollector(ax)); implInstantiations = new Dictionary, Implementation>>(); nameToImplementation = new Dictionary(); program.TopLevelDeclarations.OfType().Where(impl => impl.TypeParameters.Count > 0).ForEach( @@ -1351,7 +1364,8 @@ decl is TypeSynonymDecl typeSynonymDecl && typeSynonymDecl.TypeParameters.Count public static MonomorphizationVisitor Initialize(CoreOptions options, Program program, HashSet 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(); @@ -1378,6 +1392,7 @@ 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); @@ -1385,6 +1400,110 @@ public static MonomorphizationVisitor Initialize(CoreOptions options, Program pr return monomorphizationVisitor; } + /// + /// 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. + /// + private static void UpdateDependencies(MonomorphizationVisitor monomorphizationVisitor) + { + foreach (var (originalAxiom, newAxioms) in monomorphizationVisitor.originalAxiomToSplitAxioms) + { + var originalAxiomFc = monomorphizationVisitor.originalAxiomToOriginalSymbols[originalAxiom]; + var originalAxiomFunctions = originalAxiomFc.Functions; + + var newAxiomFunctions = new Dictionary>(); + var newAxiomConstants = new Dictionary>(); + + foreach (var newAxiom in newAxioms) + { + var newAxiomFc = new FunctionAndConstantCollector(newAxiom); + newAxiomFunctions.Add(newAxiom, newAxiomFc.Functions); + newAxiomConstants.Add(newAxiom, newAxiomFc.Constants); + } + + // Update function dependencies. + foreach (var function in monomorphizationVisitor.originalFunctions) + { + if (!function.DefinitionAxioms.Contains(originalAxiom)) + { + continue; + } + if (function.DefinitionAxiom == originalAxiom) + { + function.DefinitionAxiom = null; + } + foreach (var newAxiom in newAxioms) + { + if (function.TypeParameters.Any()) // Polymorphic function + { + var functionInstantiations = + monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet(); + var instancesToAddDependency = originalAxiomFunctions.Contains(function) + ? newAxiomFunctions[newAxiom].Intersect(functionInstantiations) + : functionInstantiations; + foreach (var inst in instancesToAddDependency) + { + inst.OtherDefinitionAxioms.Add(newAxiom); + } + } + else // Non-monomorphized function + { + if (!originalAxiomFunctions.Contains(function) || newAxiomFunctions[newAxiom].Contains(function)) + { + function.OtherDefinitionAxioms.Add(newAxiom); + } + } + } + function.OtherDefinitionAxioms.Remove(originalAxiom); + } + + // Update constant dependencies. + foreach (var constant in monomorphizationVisitor.originalConstants) + { + if (constant.DefinitionAxioms.Contains(originalAxiom)) + { + foreach (var newAxiom in newAxioms.Where(ax => newAxiomConstants[ax].Contains(constant))) + { + constant.DefinitionAxioms.Add(newAxiom); + } + constant.DefinitionAxioms.Remove(originalAxiom); + } + } + } + } + + private sealed class FunctionAndConstantCollector : ReadOnlyVisitor + { + public HashSet Functions { get; } + public HashSet Constants { get; } + + public FunctionAndConstantCollector(Axiom axiom) + { + Functions = new HashSet(); + Constants = new HashSet(); + VisitAxiom(axiom); + } + + 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 @@ -1492,6 +1611,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 (originalAxiomToSplitAxioms.ContainsKey(axiom)) { + originalAxiomToSplitAxioms[axiom].Add(instantiatedAxiom); + } newInstantiatedDeclarations.Add(instantiatedAxiom); return instantiatedAxiom; } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 4d5466075..d5b432cc6 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -451,7 +451,7 @@ void Function(out List/*!*/ 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); diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index d39da0185..f03417e2b 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -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); } } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 14db25dec..baca4e26d 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -151,9 +151,16 @@ private void PrintTopLevelDeclarationsForPruning(Program program, Implementation } using var writer = new TokenTextWriter( - $"{options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}", false, + $"{options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, options.PrettyPrint, options); - foreach (var declaration in TopLevelDeclarations ?? program.TopLevelDeclarations) { + + var functionAxioms = + program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); + var constantAxioms = + program.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); + + foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations). + Except(functionAxioms.Concat(constantAxioms)).ToList()) { declaration.Emit(writer, 0); } diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl new file mode 100644 index 000000000..956498d8c --- /dev/null +++ b/Test/pruning/MonomorphicSplit.bpl @@ -0,0 +1,39 @@ +// RUN: %parallel-boogie /prune /errorTrace:0 /printPruned:"%t" "%s" > "%t" +// RUN: %OutputCheck "%s" --file-to-check="%t-after-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 a conjunction of +// the instantiations of the original axiom. +// +// Last CHECK-NOT is for ensuring definition axioms are not printed outside +// uses clauses when using /printPruned. + +// CHECK-L: uses +// CHECK-NEXT-L: axiom +// CHECK-NOT-L: && +// CHECK-L: } +// CHECK-L: uses +// CHECK-NEXT-L: axiom +// CHECK-NOT-L: && +// CHECK-L: } +// CHECK-NOT: axiom + +// Related PR #767. + +function f1 (x: T) : int uses { + axiom (forall x: T :: {f1(x)} f1(x) == 42); +} + +// Both f1 and the axiom will be monomorphized into bool and int instances. +// Automatic edge inference would already ensure that only the monomorphized instances +// are incoming, however we want to test here how the new uses clauses are determined. +// +// After instantiation, each instance of f1 for some T should *only* have +// the T-instantiated axiom as outgoing. + +procedure monomorphicSplit() + ensures f1(true) == 42; + ensures f1(3) == 42; +{ +} diff --git a/Test/pruning/NonmonomorphicSplit.bpl b/Test/pruning/NonmonomorphicSplit.bpl new file mode 100644 index 000000000..17fbb7df6 --- /dev/null +++ b/Test/pruning/NonmonomorphicSplit.bpl @@ -0,0 +1,37 @@ +// RUN: %parallel-boogie /prune /trace /errorTrace:0 "%s" > "%t" +// RUN: %OutputCheck "%s" --file-to-check="%t" + +// Related PR #767. + +function f1 (x: int) : int; +function f2 (x: int) : int uses +{ + axiom f1(0) == 1 && f2(0) == 2; +} + +// Above axiom will be split into two during monomorphization into +// 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 s_0,...,s_n in the axiom, any split axiom containing some +// symbol s_i (with i = 0,...,n) would be added as a dependency to s_i. + +procedure nonMonomorphicSplitPass() + ensures f1(0) == 1 && f2(0) == 2; +{ +} +// CHECK-L: 1 proof obligation] verified + +function f3 (x: int) : int; +function f4 (x: int) : int; + +axiom f3(0) == 1 && f4(0) == 2; + +// This one is expected to fail. We do not want to preserve axioms not inside +// uses clauses automatically, as this weakens pruning. + +procedure nonMonomorphicSplitFail() + ensures f3(0) == 1 && f4(0) == 2; +{ +} +// CHECK-L: 1 proof obligation] error