Compute triggers for automatic induction

Source/DafnyCore/Rewriters/InductionRewriter.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
@@ -183,6 +184,23 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
  }
 
  if (inductionVariables.Count != 0) {
+ if (lemma != null) {
+ var triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
+ if (triggers.Count == 0) {
+ var msg = "omitting automatic induction because of lack of triggers";
+ if (args != null) {
+ Reporter.Warning(MessageSource.Rewriter, GenericErrors.ErrorId.none, tok, msg);
+ } else {
+ Reporter.Info(MessageSource.Rewriter, tok, msg);
+ }
+ return;
+ }
+
+ foreach (var trigger in triggers) {
+ attributes = new Attributes("_inductionPattern", trigger, attributes);
+ }
+ }
+
  // We found something usable, so let's record that in an attribute
  attributes = new Attributes("_induction", inductionVariables, attributes);
  // And since we're inferring something, let's also report that in a hover text.
@@ -195,6 +213,49 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
  }
  }
 
+ /// <summary>
+ /// Obtain and return matching patterns for
+ /// (forall inductionVariables :: body)
+ /// If there aren't any, then return null.
+ /// </summary>
+ List<List<Expression>> ComputeInductionTriggers(List<Expression> inductionVariables, Expression body, ModuleDefinition moduleDefinition) {
+ Contract.Requires(inductionVariables.Count != 0);
+
+ // Construct a quantifier, because that's what the trigger-generating machinery expects.
+ // We start by creating a new BoundVar for each ThisExpr-or-IdentifierExpr in "inductionVariables".
+ var boundVars = new List<BoundVar>();
+ var substMap = new Dictionary<IVariable, Expression>();
+ var reverseSubstMap = new Dictionary<IVariable, Expression>();
+ Expression receiverReplacement = null;
+ foreach (var inductionVariableExpr in inductionVariables) {
+ var tok = inductionVariableExpr.tok;
+ BoundVar boundVar;
+ if (inductionVariableExpr is IdentifierExpr identifierExpr) {
+ boundVar = new BoundVar(tok, identifierExpr.Var.Name, identifierExpr.Var.Type);
+ substMap.Add(identifierExpr.Var, new IdentifierExpr(tok, boundVar));
+ } else {
+ Contract.Assert(inductionVariableExpr is ThisExpr);
+ boundVar = new BoundVar(tok, "this", inductionVariableExpr.Type);
+ receiverReplacement = new IdentifierExpr(tok, boundVar);
+ }
+ boundVars.Add(boundVar);
+ reverseSubstMap.Add(boundVar, inductionVariableExpr);
+ }
+
+ var substituter = new Substituter(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>());
+ var quantifier = new ForallExpr(body.tok, body.RangeToken, boundVars, null, substituter.Substitute(body), null) {
+ Type = Type.Bool
+ };
+
+ var finder = new Triggers.QuantifierCollector(Reporter);
+ var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, moduleDefinition);
+ var quantifierCollection = new Triggers.ComprehensionTriggerGenerator(quantifier, Enumerable.Repeat(quantifier, 1), Reporter);
+ quantifierCollection.ComputeTriggers(triggersCollector);
+ var triggers = quantifierCollection.GetTriggers();
+ var reverseSubstituter = new Substituter(null, reverseSubstMap, new Dictionary<TypeParameter, Type>());
+ return triggers.ConvertAll(trigger => trigger.ConvertAll(reverseSubstituter.Substitute));
+ }
+
  class InductionVisitor : BottomUpVisitor {
  readonly InductionRewriter IndRewriter;
 

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

@@ -230,5 +230,19 @@ internal void CommitTriggers(SystemModuleManager systemModuleManager) {
  triggerWriter.CommitTrigger(reporter, partWriters.Count > 1 ? index : null, systemModuleManager);
  }
  }
+
+ public List<List<Expression>> GetTriggers() {
+ var triggers = new List<List<Expression>>();
+ foreach (var triggerWriter in partWriters) {
+ foreach (var triggerTerms in triggerWriter.Candidates) {
+ var trigger = new List<Expression>();
+ foreach (var triggerTerm in triggerTerms.Terms) {
+ trigger.Add(triggerTerm.Expr);
+ }
+ triggers.Add(trigger);
+ }
+ }
+ return triggers;
+ }
  }
 }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -789,14 +789,17 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List<Vari
  DecreasesCheck(decrToks, null, decrCalleeDafny, decrCallerDafny, decrCallee, decrCaller, null, null, false, true));
  };
 
+ var triggers = Attributes.FindAllExpressions(m.Attributes, "_inductionPattern");
 #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
- var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
- var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
- TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
- // All done, so put the two pieces together
- builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+ var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
+ var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
+ TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, definedness,
+ exporter, localVariables, etran);
+ // All done, so put the two pieces together
+ builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
 #else
- TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, null,
+ builder, localVariables, etran);
 #endif
  }
  // translate the body of the method

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

@@ -40,12 +40,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, List<Variable> locals,
  } else {
  var s0 = (CallStmt)forallStmt.S0;
  if (Attributes.Contains(forallStmt.Attributes, "_trustWellformed")) {
- TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, null, builder, locals, etran);
+ TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+ forallStmt.EffectiveEnsuresClauses, null, s0, null, builder, locals, etran);
  } else {
  var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
  DefineFuelConstant(forallStmt.Tok, forallStmt.Attributes, definedness, etran);
  var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
- TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, definedness, exporter, locals, etran);
+ TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+ forallStmt.EffectiveEnsuresClauses, null, s0, definedness, exporter, locals, etran);
  // All done, so put the two pieces together
  builder.Add(new Bpl.IfCmd(forallStmt.Tok, null, definedness.Collect(forallStmt.Tok), null, exporter.Collect(forallStmt.Tok)));
  }
@@ -71,13 +73,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, List<Variable> locals,
 
 
  void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bounds,
- Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, CallStmt s0,
+ Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, List<List<Expression>> triggers, CallStmt s0,
  BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, List<Variable> locals, ExpressionTranslator etran) {
  Contract.Requires(tok != null);
  Contract.Requires(boundVars != null);
  Contract.Requires(bounds != null);
  Contract.Requires(range != null);
  // additionalRange is allowed to be null
+ Contract.Requires(forallExpressions == null || triggers == null || triggers.Count == 0);
  Contract.Requires(s0 != null);
  // definedness is allowed to be null
  Contract.Requires(exporter != null);
@@ -209,7 +212,18 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
  post = BplAnd(post, callEtran.CanCallAssumption(p));
  post = BplAnd(post, callEtran.TrExpr(p));
  }
+
  tr = null;
+ if (triggers != null) {
+ foreach (var trigger in triggers) {
+ Contract.Assert(trigger.Count != 0);
+ var terms = trigger.ConvertAll(expr => {
+ expr = Substitute(expr, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
+ return callEtran.TrExpr(expr);
+ });
+ tr = new Trigger(trigger[0].tok, true, terms, tr);
+ }
+ }
  }
 
  // 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)))