blob: a87d442fd8857297c0cb8d43e8634c26e0a04acb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
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
|
