From 776eb757b0e4b7b98ea9c7ca9bcee002eaf6bee2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 13:52:58 -0700 Subject: - added Set.jen example - fixed implementation for sets - generalized unification rules - added command line options - removed the "Exact" active pattern for strings (the same thing is already supported by F#) - added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST --- Jennisys/examples/Set.jen | 53 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 Jennisys/examples/Set.jen (limited to 'Jennisys/examples/Set.jen') diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen new file mode 100644 index 00000000..5626babb --- /dev/null +++ b/Jennisys/examples/Set.jen @@ -0,0 +1,53 @@ +class Set { + var elems: set[int] + + constructor Empty() + ensures elems = {} + + constructor Singleton(t: int) + ensures elems = {t} + + constructor Sum(p: int, q: int) + ensures elems = {p + q} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model Set { + var root: SetNode + + frame + root * root.elems[*] + + invariant + root = null ==> elems = {} + root != null ==> elems = root.elems +} + +class SetNode { + var elems: set[int] + + constructor Init(t: int) + ensures elems = {t} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model SetNode { + var data: int + var left: SetNode + var right: SetNode + + frame + data * left * right + + invariant + left = null && right = null ==> elems = {data} + elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) + left != null ==> forall e :: e in left.elems ==> e < data + right != null ==> forall e :: e in right.elems ==> e > data +} -- cgit v1.2.3 From d9a484aaaee37d4192b6abe67328f9cc875e9294 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 17:03:18 -0700 Subject: - fixed a bug in DafnyModelUtils.fs (reading set values from models) - changed Dafny so that it returns an exit code - changed CheckDafnyProgram so that it checks Dafny exit code as well --- DafnyDriver/DafnyDriver.cs | 22 +++++++++++++++++----- Jennisys/CodeGen.fs | 37 ++++++++++++++++++++++++++----------- Jennisys/DafnyModelUtils.fs | 23 +++++++++++++---------- Jennisys/Jennisys.fsproj | 2 +- Jennisys/PipelineUtils.fs | 6 ++++-- Jennisys/examples/Set.jen | 1 - 6 files changed, 61 insertions(+), 30 deletions(-) (limited to 'Jennisys/examples/Set.jen') diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 73f7fc71..afd36aa8 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -34,23 +34,27 @@ namespace Microsoft.Boogie // ------------------------------------------------------------------------ // Main - public static void Main (string[] args) + public static int Main (string[] args) {Contract.Requires(cce.NonNullElements(args)); //assert forall{int i in (0:args.Length); args[i] != null}; + ExitValue exitValue = ExitValue.VERIFIED; CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; if (CommandLineOptions.Clo.Parse(args) != 1) { + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } if (CommandLineOptions.Clo.Files.Count == 0) { ErrorWriteLine("*** Error: No input files were specified."); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } if (CommandLineOptions.Clo.XmlSink != null) { string errMsg = CommandLineOptions.Clo.XmlSink.Open(); if (errMsg != null) { ErrorWriteLine("*** Error: " + errMsg); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } } @@ -76,11 +80,12 @@ namespace Microsoft.Boogie { ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file, extension == null ? "" : extension); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } } CommandLineOptions.Clo.RunningBoogieOnSsc = false; - ProcessFiles(CommandLineOptions.Clo.Files); + exitValue = ProcessFiles(CommandLineOptions.Clo.Files); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -91,6 +96,7 @@ namespace Microsoft.Boogie Console.WriteLine("Press Enter to exit."); Console.ReadLine(); } + return (int)exitValue; } public static void ErrorWriteLine(string s) {Contract.Requires(s != null); @@ -136,14 +142,16 @@ namespace Microsoft.Boogie enum FileType { Unknown, Cil, Bpl, Dafny }; - static void ProcessFiles (List/*!*/ fileNames) + static ExitValue ProcessFiles (List/*!*/ fileNames) { Contract.Requires(cce.NonNullElements(fileNames)); + ExitValue exitValue = ExitValue.VERIFIED; using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram); if (err != null) { + exitValue = ExitValue.DAFNY_ERROR; ErrorWriteLine(err); } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) { Dafny.Translator translator = new Dafny.Translator(); @@ -164,10 +172,11 @@ namespace Microsoft.Boogie int errorCount, verified, inconclusives, timeOuts, outOfMemories; PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); + bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0; switch (oc) { case PipelineOutcome.VerificationCompleted: WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories); - if ((CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) || CommandLineOptions.Clo.ForceCompile) + if ((CommandLineOptions.Clo.Compile && allOk) || CommandLineOptions.Clo.ForceCompile) CompileDafnyProgram(dafnyProgram); break; case PipelineOutcome.Done: @@ -179,8 +188,10 @@ namespace Microsoft.Boogie // error has already been reported to user break; } + exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED; } } + return exitValue; } private static void CompileDafnyProgram(Dafny.Program dafnyProgram) @@ -373,7 +384,8 @@ namespace Microsoft.Boogie enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted } - + enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED } + /// /// Resolves and type checks the given Boogie program. Any errors are reported to the /// console. Returns: diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index f59215ed..1a2d207a 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -106,12 +106,17 @@ let PrintObjRefName o (env,ctx) = | NewObj(name, _) -> PrintGenSym name | _ -> failwith ("unresolved object ref: " + o.ToString()) +let CheckUnresolved c = + match c with + | Unresolved(_) -> Logger.WarnLine "!!! There are some unresolved constants in the output file !!!"; c + | _ -> c + let PrintVarAssignments (heap,env,ctx) indent = let idt = Indent indent heap |> Map.fold (fun acc (o,f) l -> let objRef = PrintObjRefName o (env,ctx) let fldName = PrintVarName f - let value = TryResolve (env,ctx) l |> PrintConst + let value = TryResolve (env,ctx) l |> CheckUnresolved |> PrintConst acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline ) "" @@ -135,23 +140,33 @@ let GenConstructorCode mthd body = " }" + newline | _ -> "" -// NOTE: insert here coto to say which methods to analyze let GetMethodsToAnalyze prog = - let m = Options.CONFIG.methodToSynth; - if m = "*" then + let mOpt = Options.CONFIG.methodToSynth; + if mOpt = "*" then (* all *) FilterMembers prog FilterConstructorMembers - elif m = "paramsOnly" then + elif mOpt = "paramsOnly" then (* only with parameters *) FilterMembers prog FilterConstructorMembersWithParams else + let allMethods,neg = + if mOpt.StartsWith("~") then + mOpt.Substring(1), true + else + mOpt, false (* exactly one *) - let compName = m.Substring(0, m.LastIndexOf(".")) - let methName = m.Substring(m.LastIndexOf(".") + 1) - let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) - let m = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) - [c, m] - + let methods = allMethods.Split([|','|]) + let lst = methods |> Array.fold (fun acc m -> + let compName = m.Substring(0, m.LastIndexOf(".")) + let methName = m.Substring(m.LastIndexOf(".") + 1) + let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) + let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) + (c,mthd) :: acc + ) [] + if neg then + FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst)) + else + lst // solutions: (comp, constructor) |--> (heap, env, ctx) let PrintImplCode prog solutions methodsToPrintFunc = diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index 4cc517f2..4b9b0c60 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -256,17 +256,20 @@ let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = | [] -> (envMap,ctx) // reads stuff from [2] - let __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = + let rec __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = match set_tuples with - | ft :: rest when GetBool ft.Result -> - let srcSetKey = GetLoc ft.Args.[0] - let srcSet = match TryFindSetInEnv env srcSetKey with - | Some(s) -> s - | None -> Set.empty - let elem = UnboxIfNeeded model ft.Args.[1] - let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) - (newEnv,ctx) - | _ -> (env,ctx) + | ft :: rest -> + if GetBool ft.Result then + let srcSetKey = GetLoc ft.Args.[0] + let srcSet = match TryFindSetInEnv env srcSetKey with + | Some(s) -> s + | None -> Set.empty + let elem = UnboxIfNeeded model ft.Args.[1] + let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) + __ReadSetMembership rest (newEnv,ctx) + else + __ReadSetMembership rest (env,ctx) + | [] -> (env,ctx) let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps) let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps) diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 1c87ba4d..17c74563 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.sum + C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double pdbonly diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs index d24391f1..f4c0177c 100644 --- a/Jennisys/PipelineUtils.fs +++ b/Jennisys/PipelineUtils.fs @@ -12,6 +12,8 @@ let dafnyVerifySuffix = "verify" let dafnyUnifSuffix = "unif" let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy" +let mutable lastDafnyExitCode = 0 //TODO: how to avoid this muttable state? + let CreateEmptyModelFile modelFile = use mfile = System.IO.File.CreateText(modelFile) fprintf mfile "" @@ -29,6 +31,7 @@ let RunDafny inputFile modelFile = proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden assert proc.Start() proc.WaitForExit() + lastDafnyExitCode <- proc.ExitCode } |> Async.RunSynchronously // ======================================================= @@ -51,7 +54,6 @@ let RunDafnyProgram dafnyProgram suffix = /// Checks whether the given dafny program verifies // ======================================================= let CheckDafnyProgram dafnyProgram suffix = - // TODO: also check whether Dafny produced any other errors (e.g. compilation errors, etc.) let models = RunDafnyProgram dafnyProgram suffix // if there are no models, verification was successful - models.Count = 0 + lastDafnyExitCode = 0 && models.Count = 0 diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen index 5626babb..6404bfd6 100644 --- a/Jennisys/examples/Set.jen +++ b/Jennisys/examples/Set.jen @@ -46,7 +46,6 @@ model SetNode { data * left * right invariant - left = null && right = null ==> elems = {data} elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) left != null ==> forall e :: e in left.elems ==> e < data right != null ==> forall e :: e in right.elems ==> e > data -- cgit v1.2.3