Introduce aggressive pruning and the related 'uses' keyword for constants and functions

Source/Core/Absy.cs

@@ -1779,6 +1779,11 @@ public override void Emit(TokenTextWriter stream, int level)
 
  public class Axiom : Declaration
  {
+ public override string ToString()
+ {
+ return "Axiom: " + expression.ToString();
+ }
+
  private Expr /*!*/
  expression;
 
@@ -2472,6 +2477,8 @@ public class Constant : Variable
  // that the parental situation is unconstrained.
  public readonly ReadOnlyCollection<ConstantParent /*!*/> Parents;
 
+ public IEnumerable<Axiom> DefinitionAxioms { get; }
+
  [ContractInvariantMethod]
  void ObjectInvariant()
  {
@@ -2483,33 +2490,20 @@ void ObjectInvariant()
  public readonly bool ChildrenComplete;
 
  public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent)
- : base(tok, typedIdent)
+ : this(tok, typedIdent, true)
  {
- Contract.Requires(tok != null);
- Contract.Requires(typedIdent != null);
- Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0));
- Contract.Requires(typedIdent.WhereExpr == null);
- this.Unique = true;
- this.Parents = null;
- this.ChildrenComplete = false;
  }
 
  public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, bool unique)
- : base(tok, typedIdent)
+ : this(tok, typedIdent, unique, null, false, null, new List<Axiom>())
  {
- Contract.Requires(tok != null);
- Contract.Requires(typedIdent != null);
- Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
- Contract.Requires(typedIdent.WhereExpr == null);
- this.Unique = unique;
- this.Parents = null;
- this.ChildrenComplete = false;
  }
 
  public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent,
  bool unique,
- IEnumerable<ConstantParent /*!*/> parents, bool childrenComplete,
- QKeyValue kv)
+ IEnumerable<ConstantParent /*!*/> parents = null, bool childrenComplete = false,
+ QKeyValue kv = null,
+ IEnumerable<Axiom> definitionAxioms = null)
  : base(tok, typedIdent, kv)
  {
  Contract.Requires(tok != null);
@@ -2520,12 +2514,10 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent,
  this.Unique = unique;
  this.Parents = parents == null ? null : new ReadOnlyCollection<ConstantParent>(parents.ToList());
  this.ChildrenComplete = childrenComplete;
+ this.DefinitionAxioms = definitionAxioms ?? Enumerable.Empty<Axiom>();
  }
 
- public override bool IsMutable
- {
- get { return false; }
- }
+ public override bool IsMutable => false;
 
  public override void Emit(TokenTextWriter stream, int level)
  {
@@ -3301,22 +3293,16 @@ public class Function : DeclWithFormals
  public NAryExpr DefinitionBody; // Only set if the function is declared with {:define}
  public Axiom DefinitionAxiom;
 
- public IList<Axiom> otherDefinitionAxioms;
+ public IList<Axiom> otherDefinitionAxioms = new List<Axiom>();
+ public IEnumerable<Axiom> DefinitionAxioms => 
+ (DefinitionAxiom == null ? Enumerable.Empty<Axiom>() : new[]{ DefinitionAxiom }).Concat(otherDefinitionAxioms);
 
- public IEnumerable<Axiom> OtherDefinitionAxioms
- {
- get { return otherDefinitionAxioms; }
- }
+ public IEnumerable<Axiom> OtherDefinitionAxioms => otherDefinitionAxioms;
 
  public void AddOtherDefinitionAxiom(Axiom axiom)
  {
  Contract.Requires(axiom != null);
 
- if (otherDefinitionAxioms == null)
- {
- otherDefinitionAxioms = new List<Axiom>();
- }
-
  otherDefinitionAxioms.Add(axiom);
  }
 

Source/Core/AbsyQuant.cs

@@ -51,7 +51,7 @@ public List<Variable> /*!*/
 
  public Expr /*!*/ Body
  {
- get { return _Body; }
+ get => _Body;
  set
  {
  if (Immutable)

Source/Core/BoogiePL.atg

@@ -185,7 +185,7 @@ BoogiePL
  Implementation im;
  Implementation/*!*/ nnim;
  .)
- { Consts<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
+ { Consts<out ds> (. foreach(Bpl.Declaration/*!*/ v in ds){
  Contract.Assert(v != null);
  Pgm.AddTopLevelDeclaration(v);
  }
@@ -395,9 +395,11 @@ Types<.List<Bpl.Type>/*!*/ ts.>
 
 
 /*------------------------------------------------------------------------*/
-Consts<.out List<Variable>/*!*/ ds.>
+Consts<.out List<Declaration>/*!*/ ds.>
 = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;
- ds = new List<Variable>();
+ ds = new List<Declaration>();
+ var axioms = new List<Axiom>();
+ Axiom ax;
  bool u = false; QKeyValue kv = null;
  bool ChildrenComplete = false;
  List<ConstantParent/*!*/> Parents = null; .)
@@ -407,6 +409,7 @@ Consts<.out List<Variable>/*!*/ ds.>
  ]
  IdsType<out xs>
  [ OrderSpec<out ChildrenComplete, out Parents> ]
+ ( ";" | "uses" "{" { Axiom<out ax>(. axioms.Add(ax); .) } "}")
  (. bool makeClone = false;
  foreach(TypedIdent/*!*/ x in xs){
  Contract.Assert(x != null);
@@ -424,11 +427,14 @@ Consts<.out List<Variable>/*!*/ ds.>
  ParentsClone = Parents;
  }
  makeClone = true;
-
- ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
+
+ var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms);
+ ds.Add(constant);
+ }
+ foreach(var axiom in axioms) {
+ ds.Add(axiom);
  }
  .)
- ";"
  .
 
 OrderSpec<.out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents.>
@@ -462,13 +468,15 @@ Function<.out List<Declaration>/*!*/ ds.>
  IToken/*!*/ typeParamTok;
  var typeParams = new List<TypeVariable>();
  var arguments = new List<Variable>();
+ var axioms = new List<Axiom>();
  TypedIdent/*!*/ tyd;
  TypedIdent retTyd = null;
  Bpl.Type/*!*/ retTy;
  QKeyValue argKv = null;
  QKeyValue kv = null;
  Expr definition = null;
  Expr/*!*/ tmp;
+ Axiom ax;
  .)
  "function" { Attribute<ref kv> } Ident<out z>
  [ TypeParams<out typeParamTok, out typeParams> ]
@@ -482,18 +490,26 @@ Function<.out List<Declaration>/*!*/ ds.>
  |
  ":" Type<out retTy> (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .)
  )
- ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
+ ( "{" Expression<out tmp> (. definition = tmp; .) "}" [ "uses" "{" { Axiom<out ax>(. axioms.Add(ax); .) } "}" ] 
+ | "uses" "{" { Axiom<out ax>(. axioms.Add(ax); .) } "}" 
+ | ";"
+ )
  (.
  if (retTyd == null) {
  // construct a dummy type for the case of syntax error
  retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
  }
  Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
  new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
+ foreach(var axiom in axioms) {
+ ds.Add(axiom);
+ func.AddOtherDefinitionAxiom(axiom);
+ }
+
  Contract.Assert(func != null);
  ds.Add(func);
  bool allUnnamed = true;
- foreach(Formal/*!*/ f in arguments){
+ foreach(Formal/*!*/ f in arguments) {
  Contract.Assert(f != null);
  if (f.TypedIdent.HasName) {
  allUnnamed = false;

Source/Core/CommandLineOptions.cs

@@ -523,10 +523,7 @@ protected CommandLineOptions(string toolName, string descriptiveName)
 
  private static CommandLineOptions clo;
 
- public static CommandLineOptions /*!*/ Clo
- {
- get { return clo; }
- }
+ public static CommandLineOptions /*!*/ Clo => clo;
 
  public static void Install(CommandLineOptions options)
  {
@@ -592,7 +589,80 @@ public bool PrintInstrumented {
  public bool InstrumentWithAsserts = false;
  public string ProverPreamble { get; set; }= null;
  public bool WarnNotEliminatedVars = false;
- public bool PruneFunctionsAndAxioms = false;
+
+ public enum PruneMode { 
+ None, 
+
+ /**
+ * Automatic pruning will remove any declarations that do not reference,
+ * directly or indirectly, and are not referenced by, the implementation being verified,
+ * and declarations which cannot be used for verifying the current implementation,
+ * such as axioms with triggers that can not be satisfied.
+ * 
+ * Automatic pruning detects incoming edges in axioms, for example:
+ *
+ * function A(int): int;
+ * axiom A(3) == 2;
+ *
+ * Will detect edges in both directions between the declaration of A and the axiom declaration.
+ * So if either declaration is live, both declarations are live.
+ */
+ Automatic, 
+
+ /**
+ * UsesDecls pruning will not automatically detect incoming edges in axioms.
+ * Instead it depends on uses clauses in the input program to determine the outgoing edges of functions and constants.
+ * Outgoing edges in axioms are still detected automatically.
+ * 
+ * The reason to use UsesDecls over Automatic pruning is that the latter can miss pruning opportunities.
+ * Consider the following program:
+ *
+ * ```
+ * function F(int): int;
+ * function G(int): int;
+ *
+ * // declaration axiom for F
+ * axiom forall x: int :: F(x) == x * 2
+ * 
+ * // declaration axiom for G
+ * axiom forall x: int :: G(x) == F(x) + 1
+ *
+ * procedure FMultipliesByTwo(x: int)
+ * ensures F(x) - x == x
+ * { }
+ * ```
+ * 
+ * Automatic pruning will not remove any declarations when verifying the procedure FMultipliesByTwo,
+ * since it refers to F, which refers to the declaration axiom of G through an incoming edge in the axiom,
+ * which also has an outgoing edge to G.
+ *
+ * If we rewrite the previous program to
+ * 
+ * ```
+ * function F(int) returns (int) uses {
+ * axiom forall x: int :: F(x) == x * 2
+ * }
+ * function G(int) returns (int) uses {
+ * axiom forall x: int :: G(x) == F(x) + 1
+ * }
+ *
+ * procedure FMultipliesByTwo(x: int)
+ * ensures F(x) - x == x
+ * { }
+ * ```
+ *
+ * And apply UsesDecls pruning, then G and its axiom will be removed when verifying FMultipliesByTwo.
+ *
+ * An alternative to using UsesDecls pruning, is to add an {:exclude_dep} attribute to a function or constant,
+ * which prevents axioms from detecting incoming edges from that declaration.
+ * To add outgoing edges to the function or constant, uses clauses should be used.
+ *
+ * Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning,
+ * or to migrate from None to UsesDecls pruning.
+ */
+ UsesDecls 
+ }
+ public PruneMode Prune = PruneMode.None;
 
  public enum InstrumentationPlaces
  {
@@ -1681,6 +1751,12 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
  ps.GetNumericArgument(ref KInductionDepth);
  return true;
 
+ case "prune":
+ int number = 0;
+ ps.GetNumericArgument(ref number);
+ Prune = (PruneMode)number;
+ return true;
+
  case "emitDebugInformation":
  ps.GetNumericArgument(ref emitDebugInformation);
  return true;
@@ -1738,7 +1814,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
  ps.CheckBooleanFlag("trustInductiveSequentialization", ref trustInductiveSequentialization) ||
  ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName) ||
  ps.CheckBooleanFlag("freeVarLambdaLifting", ref FreeVarLambdaLifting) ||
- ps.CheckBooleanFlag("pruneFunctionsAndAxioms", ref PruneFunctionsAndAxioms) ||
  ps.CheckBooleanFlag("warnNotEliminatedVars", ref WarnNotEliminatedVars)
  )
  {
@@ -2323,8 +2398,10 @@ Use the SMT theory of arrays (as opposed to axioms). Supported
  only for monomorphic programs.
  /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined
  to be +, instead of +.
- /pruneFunctionsAndAxioms
- Prune declarations for each implementation
+ /prune:<n>
+ 0 (default) - none
+ 1 - automatic pruning
+ 2 - aggressive pruning. Requires binding axioms to functions and constants using 'uses'
  /relaxFocus Process foci in a bottom-up fashion. This way only generates
  a linear number of splits. The default way (top-down) is more
  aggressive and it may create an exponential number of splits.

Source/Core/LambdaHelper.cs

@@ -109,7 +109,7 @@ void ObjectInvariant()
 
  string FreshLambdaFunctionName()
  {
- return string.Format("lambda#{0}", lambdaid++);
+ return $"lambda#{lambdaid++}";
  }
 
  public override Expr VisitLambdaExpr(LambdaExpr lambda)