chore: Improve trigger/induction code

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -174,7 +174,7 @@ public void ComputeIsRecursiveBit(CompilationData compilation, ModuleDefinition
  }
 
  foreach (var rewriter in rewriters) {
- rewriter.PostCyclicityResolve(module, Reporter);
+ rewriter.PostCyclicityResolve(module);
  }
  }
 

Source/DafnyCore/Rewriters/IRewriter.cs

@@ -76,7 +76,7 @@ internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition)
  /// <param name="moduleDefinition">A module definition after it
  /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
  /// <param name="errorReporter"></param>
- internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition, ErrorReporter errorReporter) {
+ internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) {
  Contract.Requires(moduleDefinition != null);
  }
 

Source/DafnyCore/Rewriters/InductionRewriter.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
@@ -40,20 +41,17 @@ internal override void PostDecreasesResolve(ModuleDefinition m) {
  }
  }
 
- if (decl is NewtypeDecl) {
- var nt = (NewtypeDecl)decl;
- if (nt.Constraint != null) {
- var visitor = new Induction_Visitor(this);
- visitor.Visit(nt.Constraint);
- }
+ if (decl is NewtypeDecl { Constraint: { } constraint }) {
+ var visitor = new InductionVisitor(this);
+ visitor.Visit(constraint);
  }
  }
  }
  }
 
  void ProcessMethodExpressions(Method method) {
  Contract.Requires(method != null);
- var visitor = new Induction_Visitor(this);
+ var visitor = new InductionVisitor(this);
  method.Req.ForEach(mfe => visitor.Visit(mfe.E));
  method.Ens.ForEach(mfe => visitor.Visit(mfe.E));
  if (method.Body != null) {
@@ -63,7 +61,7 @@ void ProcessMethodExpressions(Method method) {
 
  void ProcessFunctionExpressions(Function function) {
  Contract.Requires(function != null);
- var visitor = new Induction_Visitor(this);
+ var visitor = new InductionVisitor(this);
  function.Req.ForEach(visitor.Visit);
  function.Ens.ForEach(visitor.Visit);
  if (function.Body != null) {
@@ -73,20 +71,29 @@ void ProcessFunctionExpressions(Function function) {
 
  void ComputeLemmaInduction(Method method) {
  Contract.Requires(method != null);
- if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 &&
- !(method is ExtremeLemma)) {
- var specs = new List<Expression>();
- method.Req.ForEach(mfe => specs.Add(mfe.E));
- method.Ens.ForEach(mfe => specs.Add(mfe.E));
- ComputeInductionVariables(method.tok, method.Ins, specs, method, ref method.Attributes);
+ if (method is Lemma or PrefixLemma && method is { Body: not null, Outs: { Count: 0 } }) {
+ Expression pre = Expression.CreateBoolLiteral(method.tok, true);
+ foreach (var req in method.Req) {
+ pre = Expression.CreateAnd(pre, req.E);
+ }
+ Expression post = Expression.CreateBoolLiteral(method.tok, true);
+ foreach (var ens in method.Ens) {
+ post = Expression.CreateAnd(post, ens.E);
+ }
+ ComputeInductionVariables(method.tok, method.Ins, Expression.CreateImplies(pre, post), method, ref method.Attributes);
  }
  }
 
- void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs,
- Method lemma, ref Attributes attributes) where VarType : class, IVariable {
+ /// <summary>
+ /// Look at the command-line options and any {:induction} attribute to determine a good list of induction
+ /// variables. If there are any, then record them in an attribute {:_induction ...} added to "attributes".
+ /// "body" is the condition that the induction would support.
+ /// </summary>
+ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, Expression body,
+ [CanBeNull] Method lemma, ref Attributes attributes) where TVarType : class, IVariable {
  Contract.Requires(tok != null);
  Contract.Requires(boundVars != null);
- Contract.Requires(searchExprs != null);
+ Contract.Requires(body != null);
  Contract.Requires(Reporter.Options.Induction != 0);
 
  var args = Attributes.FindExpressions(attributes,
@@ -106,9 +113,9 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
  } else if (args.Count == 0) {
  // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables
  // GO INFER below (all boundVars)
- } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {
+ } else if (args.Count == 1 && args[0] is LiteralExpr { Value: bool and var boolValue }) {
  // {:induction false} or {:induction true}
- if (!(bool)((LiteralExpr)args[0]).Value) {
+ if (!boolValue) {
  // we're told not to infer anything
  return;
  }
@@ -117,12 +124,11 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
  // Here, we're expecting the arguments to {:induction args} to be a sublist of "this;boundVars", where "this" is allowed only
  // if "lemma" denotes an instance lemma.
  var goodArguments = new List<Expression>();
- var i = lemma != null && !lemma.IsStatic
+ var i = lemma is { IsStatic: false }
  ? -1
  : 0; // -1 says it's okay to see "this" or any other parameter; 0 <= i says it's okay to see parameter i or higher
  foreach (var arg in args) {
- var ie = arg.Resolved as IdentifierExpr;
- if (ie != null) {
+ if (arg.Resolved is IdentifierExpr ie) {
  var j = boundVars.FindIndex(v => v == ie.Var);
  if (0 <= j && i <= j) {
  goodArguments.Add(ie);
@@ -163,15 +169,15 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
 
  // Okay, here we go, coming up with good induction setting for the given situation
  var inductionVariables = new List<Expression>();
- if (lemma != null && !lemma.IsStatic) {
- if (args != null || searchExprs.Exists(expr => FreeVariablesUtil.ContainsFreeVariable(expr, true, null))) {
+ if (lemma is { IsStatic: false }) {
+ if (args != null || FreeVariablesUtil.ContainsFreeVariable(body, true, null)) {
  inductionVariables.Add(new ThisExpr(lemma));
  }
  }
 
  foreach (IVariable n in boundVars) {
- if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) && (args != null ||
-  searchExprs.Exists(expr => InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, expr, n)))) {
+ if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) &&
+ (args != null || InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, body, n))) {
  inductionVariables.Add(new IdentifierExpr(n.Tok, n));
  }
  }
@@ -189,19 +195,17 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
  }
  }
 
- class Induction_Visitor : BottomUpVisitor {
+ class InductionVisitor : BottomUpVisitor {
  readonly InductionRewriter IndRewriter;
 
- public Induction_Visitor(InductionRewriter inductionRewriter) {
+ public InductionVisitor(InductionRewriter inductionRewriter) {
  Contract.Requires(inductionRewriter != null);
  IndRewriter = inductionRewriter;
  }
 
  protected override void VisitOneExpr(Expression expr) {
- var q = expr as QuantifierExpr;
- if (q != null && q.SplitQuantifier == null) {
- IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null,
- ref q.Attributes);
+ if (expr is QuantifierExpr { SplitQuantifier: null } q) {
+ IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, q.LogicalBody(), null, ref q.Attributes);
  }
  }
  }

Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs

@@ -9,8 +9,8 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter, SystemModuleManager s
  this.systemModuleManager = systemModuleManager;
  }
 
- internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorReporter reporter) {
- var finder = new Triggers.QuantifierCollector(reporter);
+ internal override void PostCyclicityResolve(ModuleDefinition definition) {
+ var finder = new Triggers.QuantifierCollector(Reporter);
 
  foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(definition.TopLevelDecls)) {
  finder.Visit(decl, null);

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

@@ -122,7 +122,7 @@ bool DetectAndFilterLoopingCandidates() {
  // In addition, we ignore cases where the only differences between a trigger
  // and a trigger match are places where a variable is replaced with an
  // expression whose free variables do not intersect that of the quantifier
- // in which that expression is found. For examples of this behavious, see
+ // in which that expression is found. For examples of this behavior, see
  // triggers/literals-do-not-cause-loops.
  // This ignoring logic is implemented by the CouldCauseLoops method.
  bool foundLoop = false;

Source/DafnyCore/Triggers/QuantifiersCollector.cs

@@ -7,6 +7,7 @@
 using System.Text;
 using System.Collections.ObjectModel;
 using System.Diagnostics.Contracts;
+using JetBrains.Annotations;
 
 namespace Microsoft.Dafny.Triggers {
  internal class QuantifierCollector : TopDownVisitor<OldExpr/*?*/> {
@@ -20,21 +21,24 @@ public QuantifierCollector(ErrorReporter reporter) {
  this.reporter = reporter;
  }
 
+ public void AddComprehension(ComprehensionExpr comprehensionExpr, [CanBeNull] List<Expression> splitQuantifier) {
+ quantifiers.Add(comprehensionExpr);
+ if (splitQuantifier != null) {
+ var collection = splitQuantifier.OfType<ComprehensionExpr>();
+ quantifierCollections.Add(new ComprehensionTriggerGenerator(comprehensionExpr, collection, reporter));
+ quantifiers.UnionWith(splitQuantifier);
+ } else {
+ quantifierCollections.Add(new ComprehensionTriggerGenerator(comprehensionExpr, Enumerable.Repeat(comprehensionExpr, 1), reporter));
+ }
+ }
+
  protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosingOldContext) {
  // only consider quantifiers that are not empty (Bound.Vars.Count > 0)
  if (expr is ComprehensionExpr e && e.BoundVars.Count > 0 && !quantifiers.Contains(e)) {
  if (e is SetComprehension or MapComprehension) {
- quantifiers.Add(e);
- quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(e, 1), reporter));
+ AddComprehension(e, null);
  } else if (e is QuantifierExpr quantifier) {
- quantifiers.Add(quantifier);
- if (quantifier.SplitQuantifier != null) {
- var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null);
- quantifierCollections.Add(new ComprehensionTriggerGenerator(e, collection, reporter));
- quantifiers.UnionWith(quantifier.SplitQuantifier);
- } else {
- quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(quantifier, 1), reporter));
- }
+ AddComprehension(quantifier, quantifier.SplitQuantifier);
  }
  }
 

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1678,17 +1678,18 @@ public Boogie.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, List<Variable
  return varsAndAntecedents;
  }
 
- public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variable> bvars, out Dictionary<IVariable, Expression> substMap, out Boogie.Trigger antitriggers) {
+ public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variable> bvars, out Dictionary<IVariable, Expression> substMap) {
  Contract.Requires(boundVars != null);
  Contract.Requires(bvars != null);
 
  substMap = new Dictionary<IVariable, Expression>();
- antitriggers = null;
  Boogie.Expr typeAntecedent = Boogie.Expr.True;
  foreach (BoundVar bv in boundVars) {
  var newBoundVar = new BoundVar(bv.tok, bv.Name, bv.Type);
- IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator));
- ie.Var = newBoundVar; ie.Type = ie.Var.Type; // resolve ie here
+ IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator)) {
+ Var = newBoundVar,
+ Type = newBoundVar.Type
+ };
  substMap.Add(bv, ie);
  Boogie.Variable bvar = new Boogie.BoundVariable(newBoundVar.tok, new Boogie.TypedIdent(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(newBoundVar.Type)));
  bvars.Add(bvar);

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -763,6 +763,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List<Vari
  foreach (var pre in m.Req) {
  parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverSubst, substMap));
  }
+
  // construct an expression (generator) for: VF' << VF
  ExpressionConverter decrCheck = delegate (Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
  var decrToks = new List<IToken>();

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

@@ -158,11 +158,10 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
 
  // Note, in the following, we need to do a bit of a song and dance. The actual arguments of the
  // call should be translated using "initEtran", whereas the method postcondition should be translated
- // using "callEtran". To accomplish this, we translate the argument and then tuck the resulting
+ // using "callEtran". To accomplish this, we translate the arguments and then tuck the resulting
  // Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution.
  var bvars = new List<Variable>();
  Dictionary<IVariable, Expression> substMap;
- Bpl.Trigger antitriggerBoundVarTypes;
  var argsSubstMap = new Dictionary<IVariable, Expression>(); // maps formal arguments to actuals
  Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
  var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap, etran.scope);
@@ -176,7 +175,7 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
  expr = (QuantifierExpr)expr.SplitQuantifierExpression;
  }
  boundVars = expr.BoundVars;
- ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap, out antitriggerBoundVarTypes);
+ ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
  tr = TrTrigger(callEtran, expr.Attributes, expr.tok, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
 
  var p = Substitute(expr.Range, null, substMap);
@@ -190,11 +189,7 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
  post = BplAnd(post, callEtran.TrExpr(p));
 
  } else {
- ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap, out antitriggerBoundVarTypes);
- for (int i = 0; i < s0.Method.Ins.Count; i++) {
- var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); // substitute the renamed bound variables for the declared ones
- argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
- }
+ ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
 
  var p = Substitute(range, null, substMap);
  anteCanCalls = initEtran.CanCallAssumption(p);
@@ -203,13 +198,18 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
  // additionalRange produces something of the form canCallAssumptions ==> TrExpr
  ante = BplAnd(ante, additionalRange(substMap, initEtran));
  }
+
  var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents())), s0.Receiver.Type);
+ for (int i = 0; i < s0.Method.Ins.Count; i++) {
+ var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); // substitute the renamed bound variables for the declared ones
+ argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
+ }
  foreach (var ens in ConjunctsOf(s0.Method.Ens)) {
  p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); // substitute the call's actuals for the method's formals
  post = BplAnd(post, callEtran.CanCallAssumption(p));
  post = BplAnd(post, callEtran.TrExpr(p));
  }
- tr = antitriggerBoundVarTypes;
+ tr = null;
  }
 
  // TRIG (forall $ih#s0#0: Seq :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))