1 files changed, 63 insertions, 0 deletions
diff --git a/Source/Jennisys/PipelineUtils.fs b/Source/Jennisys/PipelineUtils.fs
new file mode 100644
index 00000000..a87d442f
--- /dev/null
+++ b/Source/Jennisys/PipelineUtils.fs
@@ -0,0 +1,63 @@
+//  ####################################################################
+///   Utility functions for executing shell commands and 
+///   running Dafny in particular
+///
+///   author: Aleksandar Milicevic (t-alekm@microsoft.com)
+//  ####################################################################
+
+module PipelineUtils
+  
+open Logger
+
+let dafnyScratchSuffix = "scratch"
+let dafnyVerifySuffix = "verify"
+let dafnyUnifSuffix = "unif"
+let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy"
+let dafnyModularSynthFileNameTemplate = @"c:\tmp\jennisys-synth_###_mod.dfy"
+
+let mutable lastDafnyExitCode = 0 //TODO: how to avoid this muttable state?
+
+let CreateEmptyModelFile modelFile = 
+  use mfile = System.IO.File.CreateText(modelFile)
+  fprintf mfile ""
+
+//  =======================================================
+/// Runs Dafny on the given "inputFile" and prints 
+/// the resulting model to the given "modelFile"
+//  =======================================================
+let RunDafny inputFile modelFile =
+  //TraceLine "\n@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Running Dafny @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@"
+  CreateEmptyModelFile modelFile
+  async {
+    use proc = new System.Diagnostics.Process()
+    proc.StartInfo.FileName  <- @"c:\tmp\StartDafny-jen.bat"
+    proc.StartInfo.Arguments <- (sprintf "/mv:%s /timeLimit:%d %s" modelFile Options.CONFIG.timeout inputFile)
+    proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden
+    assert proc.Start()
+    proc.WaitForExit() 
+    lastDafnyExitCode <- proc.ExitCode
+  } |> Async.RunSynchronously
+  
+//  =======================================================
+/// Runs Dafny on the given "dafnyCode" and returns models
+//  =======================================================
+let RunDafnyProgram dafnyProgram suffix =
+  let inFileName = @"c:\tmp\jennisys-" + suffix + ".dfy" 
+  let modelFileName = @"c:\tmp\jennisys-" + suffix + ".bvd" 
+  use file = System.IO.File.CreateText(inFileName)
+  file.AutoFlush <- true  
+  fprintfn file "%s" dafnyProgram
+  file.Close()
+  // run Dafny
+  RunDafny inFileName modelFileName
+  // read models from the model file
+  use modelFile = System.IO.File.OpenText(modelFileName)
+  Microsoft.Boogie.Model.ParseModels modelFile
+
+//  =======================================================
+/// Checks whether the given dafny program verifies
+//  =======================================================  
+let CheckDafnyProgram dafnyProgram suffix =
+  let models = RunDafnyProgram dafnyProgram suffix
+  // if there are no models, verification was successful
+  lastDafnyExitCode = 0 && models.Count = 0