Merge

21 files changed, 339 insertions, 105 deletions

diff --git a/Binaries/z3 b/Binaries/z3
deleted file mode 100755
index 7c60feb4..00000000
--- a/Binaries/z3
+++ /dev/null
diff --git a/INSTALL b/INSTALL
index dbc63410..488060f6 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,7 +1,9 @@
 Building on Linux

 =================

 

-(Tested on a fresh Linux Mint 17.2)

+Tested on a fresh Linux Mint 17.2. Note that we now have official releases for

+Linux, so these instructions mostly apply to people interested in looking at

+Dafny's sources.

 

 0. Dependencies

 

@@ -28,25 +30,20 @@ Building on Linux
    cd dafny/Sources/

    xbuild Dafny.sln

 

-4. Download and build Z3

+4. Download and unpack z3 (Dafny looks for `z3` in Binaries/z3/bin/)

 

-   git clone https://github.com/Z3Prover/z3.git

-   cd z3

-   git checkout z3-4.4.0

-   ./configure

-   cd build

-   make -j4

-   cd ../..

+   cd BASE-DIRECTORY

+   wget https://github.com/Z3Prover/z3/releases/download/z3-4.4.0/z3-4.4.0-x64-ubuntu-14.04.zip

+   unzip z3-4.4.0-x64-ubuntu-14.04.zip

+   mv z3-4.4.0-x64-ubuntu-14.04 dafny/Binaries/z3

 

-5. Copy (or symlink) the z3 binary so that Dafny can find it:

+5. (Optional) If you plan to use Boogie directly, copy (or symlink) the z3 binary so that Boogie, too, can find it:

 

    cd BASE-DIRECTORY

-   rm -f dafny/Binaries/z3

    rm -f boogie/Binaries/z3.exe

-   ln -s /usr/bin/z3 dafny/Binaries/z3

-   ln -s /usr/bin/z3 boogie/Binaries/z3.exe

+   cp dafny/Binaries/z3/bin/z3 boogie/Binaries/z3.exe

 

-6. Run Dafny using the `dafny` shell script in the Binaries directory.

+6. Run Dafny using the `dafny` shell script in the Binaries directory (it calls mono as appropriate)

 

 Editing in Emacs

 ================

@@ -55,6 +52,6 @@ The README at https://github.com/boogie-org/boogie-friends has plenty of
 information on how to set-up Emacs to work with Dafny. In short, it boils down

 to running [M-x package-install RET boogie-friends RET] and adding the following

 to your .emacs:

-  (setq flycheck-dafny-executable "BASE-DIRECTORy/dafny/")

+  (setq flycheck-dafny-executable "BASE-DIRECTORY/dafny/Binaries/dafny")

 

 Do look at the README, though! It's full of useful tips.

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c7aae173..9bff2038 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2965,6 +2965,7 @@ namespace Microsoft.Dafny {
     }

   }

 

+  [DebuggerDisplay("Bound<{name}>")]

   public class BoundVar : NonglobalVariable {

     public override bool IsMutable {

       get {

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 1986ea6d..08e53d5c 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -9,8 +9,11 @@ namespace Microsoft.Dafny
 {

   public class DafnyOptions : Bpl.CommandLineOptions

   {

-    public DafnyOptions()

+    private ErrorReporter errorReporter;

+

+    public DafnyOptions(ErrorReporter errorReporter = null)

       : base("Dafny", "Dafny program verifier") {

+        this.errorReporter = errorReporter;

         SetZ3ExecutableName();

     }

 

@@ -257,13 +260,37 @@ namespace Microsoft.Dafny
       // TODO: provide attribute help here

     }

 

+    

+    /// <summary>

+    /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. 

+    /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.

+    /// For developers though (and people getting this from source), it's convenient to be able to run right away, 

+    /// so we vendor a Windows version.

+    /// </summary>

     private void SetZ3ExecutableName() {

       var platform = (int)System.Environment.OSVersion.Platform;

-      var isLinux = platform == 4 || platform ==  128; // http://www.mono-project.com/docs/faq/technical/

 

-      //TODO should we also vendor an OSX build?

-      var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

-      Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe");

+      // http://www.mono-project.com/docs/faq/technical/

+      var isUnix = platform == 4 || platform == 128;

+      

+      var z3binName = isUnix ? "z3" : "z3.exe";

+      var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

+      var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");

+      var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);

+

+      if (!System.IO.File.Exists(z3BinPath) && !isUnix) {

+        // This is most likely a Windows user running from source without downloading z3 

+        // separately; this is ok, since we vendor z3.exe.

+        z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);

+      }

+      

+      if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {

+        var tok = new Bpl.Token(1, 1) { filename = "*** " };

+        errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", 

+          z3binName, z3BinDir, System.Environment.NewLine);

+      } else {

+        Z3ExecutablePath = z3BinPath;

+      }

     }

 

     public override void Usage() {

diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
index 4cfbf20e..760392ca 100644
--- a/Source/Dafny/Reporting.cs
+++ b/Source/Dafny/Reporting.cs
@@ -143,7 +143,7 @@ namespace Microsoft.Dafny {
     }

 

     public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

-      if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) {

+      if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) {

         // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI

         msg = msg.Replace(Environment.NewLine, Environment.NewLine + " ");

 

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 6555b52a..50458ab7 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -47,15 +47,9 @@ namespace Microsoft.Dafny.Triggers {
       SelectTriggers();

     }

     

-    private bool SubsetGenerationPredicate(List<TriggerTerm> terms, TriggerTerm additionalTerm) {

-      // Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very

-      // large numbers of multi-triggers, most of which are useless. This filter

-      // restricts subsets of terms so that we only generate sets of terms where each

-      // element contributes at least one variable. In the example above, we'll only

-      // get 5 triggers.

-      // Note that this may still be an over-approximation, as in the following example:

-      // forall a, b :: forall x :: a[x] || b[x] > 0.

-      return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();

+    private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) {

+      return true; // FIXME Remove this

+      //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();

     }

 

     /// <summary>

@@ -68,11 +62,10 @@ namespace Microsoft.Dafny.Triggers {
     void CollectAndShareTriggers(TriggersCollector triggersCollector) {

       var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));

       var distinctPool = pool.Deduplicate(TriggerTerm.Eq);

-      var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList();

 

       foreach (var q in quantifiers) {

-        q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed

-        q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList();

+        q.CandidateTerms = distinctPool; // The list of candidate terms is immutable

+        q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList();

       }

     }

 

@@ -107,7 +100,12 @@ namespace Microsoft.Dafny.Triggers {
       // quantifier that matches one of the terms of the trigger (this ensures that

       // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even

       // ignore terms that almost match a trigger term, modulo a single variable

-      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop).

+      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). 

+      // 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

+      // triggers/literals-do-not-cause-loops.

       // This ignoring logic is implemented by the CouldCauseLoops method.

 

       foreach (var q in quantifiers) {

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index 71414eee..d4a822a8 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -31,9 +31,15 @@ namespace Microsoft.Dafny.Triggers {
       return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);

     }

 

-    internal bool CouldCauseLoops(List<TriggerTerm> terms) {

+    /// <summary>

+    ///  This method checks whether this match could actually cause a loop, given a set of terms participating in a trigger; 

+    ///  to compute an answer, we match the Expr of this match against the Exprs of each of these term, allowing for harmless 

+    ///  variations. If any of these tests does match, this term likely won't cause a loop.

+    ///  The boundVars list is useful to determine that forall x :: P(x) == P(y+z) does not loop.

+    /// </summary>

+    internal bool CouldCauseLoops(List<TriggerTerm> terms, ISet<BoundVar> boundVars) {

       var expr = Expr;

-      return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr));

+      return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars));

     }

   }

 

@@ -79,15 +85,22 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2));

     }

 

-    internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) {

+    internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet<BoundVar> boundVars) {

       expr1 = expr1.Resolved;

       expr2 = expr2.Resolved;

 

       if (expr1 is IdentifierExpr) {

-        return expr2 is IdentifierExpr;

+        if (expr2 is IdentifierExpr) {

+          return true;

+        } else {

+          var freeInE2 = Translator.ComputeFreeVariables(expr2);

+          freeInE2.IntersectWith(boundVars);

+          return !freeInE2.Any();

+        }

       }

 

-      return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2));

+      return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, 

+        expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars));

     }

 

     internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 4fd139e2..efa1f167 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -15,29 +15,109 @@ namespace Microsoft.Dafny.Triggers {
       return copy;

     }

 

-    internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, Func<List<T>, T, bool> predicate, int offset) {

+    internal class SetOfTerms {

+      internal bool IsRedundant { get; private set; }

+      internal List<TriggerTerm> Terms { get; set; }

+

+      private ISet<BoundVar> variables;

+      private Dictionary<BoundVar, TriggerTerm> termOwningAUniqueVar;

+      private Dictionary<TriggerTerm, ISet<BoundVar>> uniqueVarsOwnedByATerm;

+

+      public int Count { get { return Terms.Count; } }

+

+      private SetOfTerms() { }

+

+      internal TriggerCandidate ToTriggerCandidate() {

+        return new TriggerCandidate(Terms);

+      }

+      

+      internal static SetOfTerms Empty() {

+        var newSet = new SetOfTerms();

+        newSet.IsRedundant = false;

+        newSet.Terms = new List<TriggerTerm>();

+        newSet.variables = new HashSet<BoundVar>();

+        newSet.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>();

+        newSet.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>();

+        return newSet;

+      }

+

+      /// <summary>

+      /// Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very

+      /// large numbers of multi-triggers, most of which are useless. As it copies its

+      /// argument, this method updates various datastructures that allow it to

+      /// efficiently track ownership relations between formulae and bound variables,

+      /// and sets the IsRedundant flag of the returned set, allowing the caller to

+      /// discard that set of terms, and the ones that would have been built on top of

+      /// it, thus ensuring that the only sets of terms produced in the end are sets

+      /// of terms in which each element contributes (owns) at least one variable.

+      ///

+      /// Note that this is trickier than just checking every term for new variables;

+      /// indeed, a new term that does bring new variables in can make an existing

+      /// term redundant (see redundancy-detection-does-its-job-properly.dfy).

+      /// </summary>

+      internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet<BoundVar> relevantVariables) {

+        var copy = new SetOfTerms();

+        copy.Terms = new List<TriggerTerm>(Terms);

+        copy.variables = new HashSet<BoundVar>(variables);

+        copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);

+        copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);

+

+        copy.Terms.Add(term);

+

+        var varsInNewTerm = new HashSet<BoundVar>(term.BoundVars);

+        varsInNewTerm.IntersectWith(relevantVariables);

+

+        var ownedByNewTerm = new HashSet<BoundVar>();

+

+        // Check #0: does this term bring anything new?

+        copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv));

+        copy.variables.UnionWith(varsInNewTerm);

+        

+        // Check #1: does this term claiming ownership of all its variables cause another term to become useless?

+        foreach (var v in varsInNewTerm) {

+          TriggerTerm originalOwner;

+          if (copy.termOwningAUniqueVar.TryGetValue(v, out originalOwner)) {

+            var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner];

+            alsoOwnedByOriginalOwner.Remove(v);

+            if (!alsoOwnedByOriginalOwner.Any()) {

+              copy.IsRedundant = true;

+            }

+          } else {

+            ownedByNewTerm.Add(v);

+            copy.termOwningAUniqueVar[v] = term;

+          }

+        }

+

+        // Actually claim ownership

+        copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm;

+

+        return copy;

+      }

+    }

+

+    internal static IEnumerable<SetOfTerms> AllSubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, int offset, ISet<BoundVar> relevantVariables) {

       if (offset >= source.Count) {

-        yield return new List<T>();

+        yield return SetOfTerms.Empty();

         yield break;

       }

 

-      foreach (var subset in AllSubsets<T>(source, predicate, offset + 1)) {

-        if (predicate(subset, source[offset])) {

-          yield return CopyAndAdd(subset, source[offset]);

+      foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) {

+        var newSet = subset.CopyWithAdd(source[offset], relevantVariables);

+        if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate?

+          yield return newSet;

         }

-        yield return new List<T>(subset);

+        yield return subset;

       }

     }

 

-    internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source, Func<List<T>, T, bool> predicate) {

-      List<T> all = new List<T>(source);

-      foreach (var subset in AllSubsets(all, predicate, 0)) {

+    internal static IEnumerable<SetOfTerms> AllNonEmptySubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, IEnumerable<BoundVar> relevantVariables) {

+      foreach (var subset in AllSubsets(source, predicate, 0, new HashSet<BoundVar>(relevantVariables))) {

         if (subset.Count > 0) {

           yield return subset;

         }

       }

     }

-

+    

     internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 69c47d90..c25f65b9 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers {
     internal Expression Expr { get; set; }

     internal Expression OriginalExpr { get; set; }

     internal ISet<IVariable> Variables { get; set; }

+    internal IEnumerable<BoundVar> BoundVars {

+      get {

+        return Variables.Select(v => v as BoundVar).Where(v => v != null);

+      }

+    }

 

     public override string ToString() {

       return Printer.ExprToString(Expr); 

@@ -64,7 +69,8 @@ namespace Microsoft.Dafny.Triggers {
     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       var matchingSubterms = this.MatchingSubterms(quantifier);

-      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

+      var boundVars = new HashSet<BoundVar>(quantifier.BoundVars);

+      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars));

     }

 

     internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {

@@ -185,8 +191,13 @@ namespace Microsoft.Dafny.Triggers {
       expr.SubExpressions.Iter(e => Annotate(e));

 

       TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort

-      if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MultiSelectExpr || expr is MemberSelectExpr || 

-          expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression ||

+      if (expr is FunctionCallExpr || 

+          expr is SeqSelectExpr || 

+          expr is MultiSelectExpr || 

+          expr is MemberSelectExpr || 

+          expr is OldExpr || 

+          expr is ApplyExpr || 

+          expr is DisplayExpression ||

           (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944

           (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {

         annotation = AnnotatePotentialCandidate(expr);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4b5ae8d8..c45d66fc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -40,10 +40,11 @@ namespace Microsoft.Dafny
     public static int ThreadMain(string[] args)

     {

       Contract.Requires(cce.NonNullElements(args));

-         

+

+      ErrorReporter reporter = new ConsoleErrorReporter();

       ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors

 

-      DafnyOptions.Install(new DafnyOptions());

+      DafnyOptions.Install(new DafnyOptions(reporter));

 

       ExitValue exitValue = ExitValue.VERIFIED;

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

@@ -92,7 +93,7 @@ namespace Microsoft.Dafny
           goto END;

         }

       }

-      exitValue = ProcessFiles(CommandLineOptions.Clo.Files);

+      exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter);

 

       END:

         if (CommandLineOptions.Clo.XmlSink != null) {

@@ -112,7 +113,7 @@ namespace Microsoft.Dafny
     }

 

 

-    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)

+    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

 

@@ -128,7 +129,7 @@ namespace Microsoft.Dafny
         {

           Console.WriteLine();

           Console.WriteLine("-------------------- {0} --------------------", f);

-          var ev = ProcessFiles(new List<string> { f }, lookForSnapshots, f);

+          var ev = ProcessFiles(new List<string> { f }, reporter, lookForSnapshots, f);

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -142,7 +143,7 @@ namespace Microsoft.Dafny
         var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);

         foreach (var s in snapshotsByVersion)

         {

-          var ev = ProcessFiles(new List<string>(s), false, programId);

+          var ev = ProcessFiles(new List<string>(s), reporter, false, programId);

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -153,7 +154,6 @@ namespace Microsoft.Dafny
       

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {

         Dafny.Program dafnyProgram;

-        ErrorReporter reporter = new ConsoleErrorReporter();

         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";

         string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram);

         if (err != null) {

diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
index 3204fdb3..e54e2b48 100644
--- a/Source/DafnyServer/DafnyHelper.cs
+++ b/Source/DafnyServer/DafnyHelper.cs
@@ -29,18 +29,21 @@ namespace Microsoft.Dafny {
   class DafnyHelper {

     private string fname;

     private string source;

+    private string[] args;

 

     private readonly Dafny.ErrorReporter reporter;

     private Dafny.Program dafnyProgram;

     private Bpl.Program boogieProgram;

 

-    public DafnyHelper(string fname, string source) {

+    public DafnyHelper(string[] args, string fname, string source) {

+      this.args = args;

       this.fname = fname;

       this.source = source;

       this.reporter = new Dafny.ConsoleErrorReporter();

     }

 

     public bool Verify() {

+      ServerUtils.ApplyArgs(args, reporter);

       return Parse() && Resolve() && Translate() && Boogie();

     }

 

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 59b3abb9..5e2c6f96 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -43,8 +43,8 @@ namespace Microsoft.Dafny {
       }

     }

 

-    internal static void ApplyArgs(string[] args) {

-      Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

+    internal static void ApplyArgs(string[] args, ErrorReporter reporter) {

+      Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter));

       Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden

 

       if (CommandLineOptions.Clo.Parse(args)) {

diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index a00688b1..eb740e70 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -52,8 +52,7 @@ namespace Microsoft.Dafny {
     }

 

     internal void Run() {

-      ServerUtils.ApplyArgs(args);

-      new DafnyHelper(filename, ProgramSource).Verify();

+      new DafnyHelper(args, filename, ProgramSource).Verify();

     }

   }

 }

diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
new file mode 100644
index 00000000..09032453
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This example was listed in IronClad's notebook as one place were z3 picked

+// much too liberal triggers. THe Boogie code for this is shown below:

+//

+// forall k#2: Seq Box :: $Is(k#2, TSeq(TInt)) && $IsAlloc(k#2, TSeq(TInt), $Heap)

+//                   ==> Seq#Equal(_module.__default.HashtableLookup($Heap, h1#0, k#2),

+//                                 _module.__default.HashtableLookup($Heap, h2#0, k#2))

+//

+// and z3 would pick $Is(k#2, TSeq(TInt)) or $IsAlloc(k#2, TSeq(TInt), $Heap) as

+// triggers.

+

+type Key = seq<int>

+type Value = seq<int>

+

+type Hashtable = map<Key, Value>

+function HashtableLookup(h: Hashtable, k: Key): Value

+

+lemma HashtableAgreement(h1:Hashtable, h2:Hashtable, k:Key)

+  requires forall k :: HashtableLookup(h1,k) == HashtableLookup(h2,k) {

+    assert true || (k in h1) == (k in h2);

+}

diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
new file mode 100644
index 00000000..46ec143e
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
@@ -0,0 +1,4 @@
+auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy(21,11): Info: Selected triggers:

+   {HashtableLookup(h2, k)}, {HashtableLookup(h1, k)}

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 7922e88d..501cfa51 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1
 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:

    {f(10)}, {f.requires(10)}

 function-applications-are-triggers.dfy(12,5): Info: Selected triggers:

-   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}

+   {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}

 

 Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
index a5a30c81..81f764ad 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -7,8 +7,9 @@
 // equal to that trigger, as long as the only differences are variable

 

 predicate P(x: int, y: int)

+predicate Q(x: int)

 

-method Test() {

+method Test(z: int) {

   // P(x, y) and P(y, x) might look like they would cause a loop. Since they

   // only differ by their variables, though, they won't raise flags.

   assume forall x: int, y: int :: P(x, y) == P(y, x);

@@ -18,4 +19,22 @@ method Test() {
 

   // Contrast with the following:

   assume forall x: int, y: int :: P(x, y) == P(x, y+1);

+

+  // The following examples were made legal after an exchange where Chris

+  // pointed examples in the IronClad sources where things like this were

+  // incorrectly flagged.

+  assert forall x :: true || Q(x) || Q(0);

+  assert forall x :: true || Q(x) || Q(z);

+  assert forall x :: true || P(x, 1) || P(x, z);

+

+  // Support for the following was added following a discussion with Rustan; in

+  // the second one the expression `if z > 1 then z else 3 * z + 1` is not

+  // directly a constant expression, but it does not involve x, so it's ok:

+  assert forall x :: true || Q(x) || Q(0+1);

+  assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1);

+  // Sanity check:

+  assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1);

+

+  // WISH: It might also be good to zeta-reduce before loop detection.

+  assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));

 }

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 6f5ed3d7..705c2a8c 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -1,8 +1,17 @@
-loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers:

+loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers:

    {P(y, x)}, {P(x, y)}

-loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:

+loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers:

    {P(y, x)}, {P(x, y)}

-loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})

+loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})

  (!) Suppressing loops would leave this expression without triggers.

+loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)}

+loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)}

+loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers:

+   {P(x, z)}, {P(x, 1)}

+loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)}

+loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)}

+loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)}

 

-Dafny program verifier finished with 3 verified, 0 errors

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
new file mode 100644
index 00000000..06541b70
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test checks for tricky cases of redundancy suppression when building

+// triggers.

+

+predicate P(x: int, y: int)

+predicate Q(x: int)

+predicate R(x: int)

+

+method M() {

+  // For this term, it is enough to order the terms by number of variables

+  assert forall x, y :: true || P(x, y) || Q(y) || R(x);

+  assert forall x, y :: true || Q(y) || P(x, y) || R(x);

+  assert forall x, y :: true || Q(y) || R(x) || P(x, y);

+}

+

+predicate PP(x: int, y: int, z: int)

+predicate QQ(x: int, y: int)

+predicate RR(x: int, y: int)

+predicate SS(x: int, y: int)

+

+method MM() {

+  // Not for this one, though

+  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);

+}

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
new file mode 100644
index 00000000..78c9e7ca
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
@@ -0,0 +1,12 @@
+redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:

+   {P(x, y)}, {R(x), Q(y)}

+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+

+Dafny program verifier finished with 11 verified, 0 errors

diff --git a/package.py b/package.py
index 22ed232c..fa111ec5 100644
--- a/package.py
+++ b/package.py
@@ -1,25 +1,39 @@
+from fnmatch import fnmatch
+from os import path
 import argparse
 import json
 import os
-from os import path
 import re
-import urllib.request
+import shutil
+import subprocess
 import sys
+import urllib.request
 import zipfile
-import subprocess
-import shutil
 
 # Configuration
 
+## Where do we fetch the list of releases from?
 RELEASES_URL = "https://api.github.com/repos/Z3Prover/z3/releases/latest"
-RELEASE_REGEXP = r"^(?P<directory>z3-[0-9\.]+-(?P<platform>x86|x64)-(?P<os>[a-z0-9\.\-]+)).zip$"
+## How do we extract info from the name of a release file?
+RELEASE_REGEXP = re.compile(r"^(?P<directory>z3-[0-9\.]+-(?P<platform>x86|x64)-(?P<os>[a-z0-9\.\-]+)).zip$", re.IGNORECASE)
 
+## Where are the sources?
 SOURCE_DIRECTORY = "Source"
+## Where do the binaries get put?
 BINARIES_DIRECTORY = "Binaries"
+## Where do we store the built packages and cache files?
 DESTINATION_DIRECTORY = "Package"
 
-Z3_ARCHIVE_PREFIX = path.join("z3", "bin")
+## What sub-folder of the packages does z3 go into?
+Z3_PACKAGE_PREFIX = path.join("z3")
+
+## What do we take from the z3 archive? (Glob syntax)
+Z3_INTERESTING_FILES = ["LICENSE.txt", "bin/*"]
 
+## On unix system, which Dafny files should be marked as executable? (Glob syntax; Z3's permissions are preserved)
+UNIX_EXECUTABLES = ["dafny"]
+
+## What do we take from Dafny's Binaries folder?
 DLLs = ["AbsInt",
         "Basetypes",
         "CodeContractsExtender",
@@ -48,8 +62,6 @@ BINARIES_DIRECTORY = path.join(ROOT_DIRECTORY, BINARIES_DIRECTORY)
 DESTINATION_DIRECTORY = path.join(ROOT_DIRECTORY, DESTINATION_DIRECTORY)
 CACHE_DIRECTORY = path.join(DESTINATION_DIRECTORY, "cache")
 
-RELEASE_REGEXP = re.compile(RELEASE_REGEXP, re.IGNORECASE)
-
 MONO = sys.platform not in ("win32", "cygwin")
 DLL_PDB_EXT = ".dll.mdb" if MONO else ".pdb"
 EXE_PDB_EXT = ".exe.mdb" if MONO else ".pdb"
@@ -77,8 +89,6 @@ class Release:
         self.url = js["browser_download_url"]
         self.platform, self.os, self.directory = Release.parse_zip_name(js["name"])
         self.z3_zip = path.join(CACHE_DIRECTORY, self.z3_name)
-        self.z3_directory = path.join(CACHE_DIRECTORY, self.directory)
-        self.z3_bin_directory = path.join(self.z3_directory, "bin")
         self.dafny_name = "dafny-{}-{}-{}.zip".format(version, self.platform, self.os)
         self.dafny_zip = path.join(DESTINATION_DIRECTORY, self.dafny_name)
 
@@ -100,12 +110,6 @@ class Release:
                     writer.write(reader.read())
             flush("done!")
 
-    def unpack(self):
-        shutil.rmtree(self.z3_directory)
-        with zipfile.ZipFile(self.z3_zip) as archive:
-            archive.extractall(CACHE_DIRECTORY)
-            flush("done!")
-
     def pack(self):
         try:
             os.remove(self.dafny_zip)
@@ -113,24 +117,32 @@ class Release:
             pass
         missing = []
         with zipfile.ZipFile(self.dafny_zip, 'w',  zipfile.ZIP_DEFLATED) as archive:
-            for root, _, files in os.walk(self.z3_bin_directory):
-                for f in files:
-                    fpath = path.join(root, f)
-                    arcpath = path.join(Z3_ARCHIVE_PREFIX, path.relpath(fpath, self.z3_bin_directory))
-                    archive.write(fpath, arcpath)
+            with zipfile.ZipFile(self.z3_zip) as Z3_archive:
+                z3_files_count = 0
+                for fileinfo in Z3_archive.infolist():
+                    fname = path.relpath(fileinfo.filename, self.directory)
+                    if any(fnmatch(fname, pattern) for pattern in Z3_INTERESTING_FILES):
+                        z3_files_count += 1
+                        contents = Z3_archive.read(fileinfo)
+                        fileinfo.filename = path.join(Z3_PACKAGE_PREFIX, fname)
+                        archive.writestr(fileinfo, contents)
             for fname in ARCHIVE_FNAMES:
                 fpath = path.join(BINARIES_DIRECTORY, fname)
                 if path.exists(fpath):
+                    fileinfo = zipfile.ZipInfo(fname)
+                    if any(fnmatch(fname, pattern) for pattern in UNIX_EXECUTABLES):
+                        # http://stackoverflow.com/questions/434641/
+                        fileinfo.external_attr = 0o777 << 16
                     archive.write(fpath, fname)
                 else:
                     missing.append(fname)
-        flush("done!")
+        flush("done! (imported {} files from z3's sources)".format(z3_files_count))
         if missing:
             flush("      WARNING: Not all files were found: {} were missing".format(", ".join(missing)))
 
 def discover(version):
     flush("  - Getting information about latest release")
-    with urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest") as reader:
+    with urllib.request.urlopen(RELEASES_URL) as reader:
         js = json.loads(reader.read().decode("utf-8"))
 
         for release_js in js["assets"]:
@@ -147,17 +159,11 @@ def download(releases):
         flush("    + {}:".format(release.z3_name), end=' ')
         release.download()
 
-def unpack(releases):
-    flush("  - Unpacking {} z3 archives".format(len(releases)))
-    for release in releases:
-        flush("    + {}:".format(release.z3_name), end=' ')
-        release.unpack()
-
 def run(cmd):
     flush("    + {}...".format(" ".join(cmd)), end=' ')
     retv = subprocess.call(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
     if retv != 0:
-        flush("failed!")
+        flush("failed! (Is Dafny or the Dafny server running?)")
         sys.exit(1)
     else:
         flush("done!")
@@ -165,9 +171,13 @@ def run(cmd):
 def build():
     os.chdir(ROOT_DIRECTORY)
     flush("  - Building")
-    builder = "xbuild" if MONO else "xbuild"
-    run([builder, "Source/Dafny.sln", "/t:Clean"])
-    run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/t:Rebuild"])
+    builder = "xbuild" if MONO else "msbuild"
+    try:
+        run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/p:Platform=Any CPU", "/t:Clean"])
+        run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/p:Platform=Any CPU", "/t:Rebuild"])
+    except FileNotFoundError:
+        flush("Could not find '{}'! On Windows, you need to run this from the VS native tools command prompt.".format(builder))
+        sys.exit(1)
 
 def pack(releases):
     flush("  - Packaging {} Dafny archives".format(len(releases)))
@@ -185,10 +195,9 @@ def main():
     os.makedirs(CACHE_DIRECTORY, exist_ok=True)
 
     # Z3
-    flush("* Finding, downloading, and unpacking Z3 releases")
+    flush("* Finding and downloading Z3 releases")
     releases = list(discover(args.version))
     download(releases)
-    unpack(releases)
 
     flush("* Building and packaging Dafny")
     build()