Implement --watch to rerun Leon on file changes

src/main/scala/leon/Main.scala

@@ -36,6 +36,7 @@ object Main {
       LeonFlagOptionDef ("repair",      "--repair",             "Repair selected functions"),
       LeonFlagOptionDef ("synthesis",   "--synthesis",          "Partial synthesis of choose() constructs"),
       LeonFlagOptionDef ("xlang",       "--xlang",              "Support for extra program constructs (imperative,...)"),
+      LeonFlagOptionDef ("watch",       "--watch",              "Rerun pipeline when file changes"),
       LeonValueOptionDef("solvers",     "--solvers=s1,s2",      "Use solvers s1 and s2 (fairz3,enum,smt)"),
       LeonValueOptionDef("debug",       "--debug=<sections..>", "Enables specific messages"),
       LeonFlagOptionDef ("noop",        "--noop",               "No operation performed, just output program"),
@@ -241,6 +242,8 @@ object Main {
     pipeProcess
   }
 
+  private var hasFatal = false;
+
   def main(args: Array[String]) {
     val argsl = args.toList
 
@@ -263,10 +266,31 @@ object Main {
         sys.exit(1)
     }
 
+    ctx.interruptManager.registerSignalHandler()
 
-    try {
-      ctx.interruptManager.registerSignalHandler()
+    val doWatch = ctx.options.exists {
+      case LeonFlagOption("watch", value) => value
+      case _ => false
+    }
 
+    if (doWatch) {
+      val watcher = new FilesWatcher(ctx, ctx.files)
+      watcher.onChange {
+        execute(args, ctx)
+      }
+    } else {
+      execute(args, ctx)
+    }
+
+    if (hasFatal) {
+      sys.exit(1)
+    } else {
+      sys.exit(0)
+    }
+  }
+
+  def execute(args: Seq[String], ctx: LeonContext): Unit = {
+    try {
       // Compute leon pipeline
       val pipeline = computePipeline(ctx.settings)
 
@@ -290,7 +314,7 @@ object Main {
       }
     } catch {
       case LeonFatalError(None) =>
-        sys.exit(1)
+        hasFatal = true
 
       case LeonFatalError(Some(msg)) =>
         // For the special case of fatal errors not sent though Reporter, we
@@ -301,7 +325,8 @@ object Main {
           case _: LeonFatalError =>
         }
 
-        sys.exit(1)
+        hasFatal = true
     }
   }
+
 }

src/main/scala/leon/utils/FilesWatcher.scala

+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+
+import leon.utils._
+import solvers.SolverFactory
+import java.io.File
+import java.nio.file._
+import scala.collection.JavaConversions._
+import java.security.MessageDigest
+import java.math.BigInteger
+
+case class FilesWatcher(ctx: LeonContext, files: Seq[File]) {
+  val toWatch = files.map(_.getAbsoluteFile).toSet
+  val dirs    = toWatch.map(_.getParentFile)
+
+  def onChange(body: => Unit): Unit = {
+    val watcher = FileSystems.getDefault().newWatchService()
+    val paths = dirs.map(_.toPath.register(watcher, StandardWatchEventKinds.ENTRY_MODIFY))
+
+    var lastHashes = toWatch.map(md5file)
+
+    body
+    ctx.reporter.info("Waiting for source changes...")
+
+    while (true) {
+      var key = watcher.take()
+
+      val events = key.pollEvents()
+
+      if (events.exists{_.context match {
+        case (p: Path) => toWatch(p.toFile.getAbsoluteFile)
+        case e => false
+      }}) {
+        val currentHashes = toWatch.map(md5file)
+        if (currentHashes != lastHashes) {
+          lastHashes = currentHashes
+
+          ctx.reporter.info("Detected new version!")
+          body
+          ctx.reporter.info("Waiting for source changes...")
+        }
+      }
+
+      key.reset()
+    }
+  }
+
+  def md5file(f: File): String = {
+    var buffer = new Array[Byte](1024)
+    val md = MessageDigest.getInstance("MD5");
+    try {
+      val is = Files.newInputStream(f.toPath)
+      var read = 0;
+      do {
+        read = is.read(buffer);
+        if (read > 0) {
+          md.update(buffer, 0, read)
+        }
+      } while (read != -1);
+      is.close()
+
+      val bytes = md.digest();
+      ("%0" + (bytes.length << 1) + "X").format(new BigInteger(1, bytes));
+    } catch {
+      case _: RuntimeException =>
+        ""
+    }
+  }
+}