summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Jennisys/Analyzer.fs71
-rw-r--r--Jennisys/Ast.fs2
-rw-r--r--Jennisys/AstUtils.fs26
-rw-r--r--Jennisys/CodeGen.fs17
-rw-r--r--Jennisys/Jennisys.fsproj1
-rw-r--r--Jennisys/PipelineUtils.fs4
-rw-r--r--Jennisys/Printer.fs10
-rw-r--r--Jennisys/examples/List2.jen4
-rw-r--r--Jennisys/examples/List3.jen8
9 files changed, 93 insertions, 50 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index e3135cff..fab61ff4 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -5,6 +5,7 @@ open AstUtils
open CodeGen
open DafnyModelUtils
open PipelineUtils
+open Options
open Printer
open DafnyPrinter
@@ -34,11 +35,10 @@ let rec Substitute substMap = function
| ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
| expr -> expr
-let GenMethodAnalysisCode methodName signature pre post assumeInvInitially =
+let GenMethodAnalysisCode comp methodName signature pre post =
" method " + methodName + "()" + newline +
" modifies this;" + newline +
" {" + newline +
- (if assumeInvInitially then " assume Valid();" else "") +
// print signature as local variables
(match signature with
| Sig(ins,outs) ->
@@ -50,45 +50,81 @@ let GenMethodAnalysisCode methodName signature pre post assumeInvInitially =
" // assume invariant and postcondition" + newline +
" assume Valid();" + newline +
" assume " + (PrintExpr 0 post) + ";" + newline +
+ // inline the user defined invariant because assuming Valid() doesn't always work
+ " // assume user defined invariant again because assuming Valid() doesn't always work" +
+ (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline +
// if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
" // assert false to search for a model satisfying the assumed constraints" + newline +
" assert false;" + newline +
- " }" + newline
+ " }" + newline
let MethodAnalysisPrinter onlyForThisCompMethod comp mthd =
match onlyForThisCompMethod with
| (c,m) when c = comp && m = mthd ->
match m with
- | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
+ | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post) + newline
| _ -> ""
| _ -> ""
+
+let VerifySolution (heap,env,ctx) prog comp mthd =
+ // print the solution to file and try to verify it with Dafny
+ let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)
+ let code = PrintImplCode prog solution (fun p -> [comp,mthd])
+ use file = System.IO.File.CreateText(dafnyVerifyFile)
+ file.AutoFlush <- true
+ fprintfn file "%s" code
+ file.Close()
+ // run Dafny
+ RunDafny dafnyVerifyFile dafnyVerifyModelFile
+ // read models from the model file
+ use modelFile = System.IO.File.OpenText(dafnyVerifyModelFile)
+ let models = Microsoft.Boogie.Model.ParseModels modelFile
+ // if there are no models, verification was successful
+ models.Count = 0
-let AnalyzeConstructor prog comp methodName signature pre post =
- let m = Method(methodName, signature, pre, post, true)
+let AnalyzeConstructor prog comp m =
+ let methodName = GetMethodName m
+ // generate Dafny code for analysis first
+ let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
+ printfn " [*] analyzing constructor %s" methodName
+ printf " - searching for a solution ..."
use file = System.IO.File.CreateText(dafnyScratchFile)
file.AutoFlush <- true
- let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
- printfn "analyzing constructor %s" methodName
fprintf file "%s" code
file.Close()
+ // run Dafny
RunDafny dafnyScratchFile dafnyModelFile
- use modelFile = System.IO.File.OpenText(dafnyModelFile)
-
+ // read models
+ use modelFile = System.IO.File.OpenText(dafnyModelFile)
let models = Microsoft.Boogie.Model.ParseModels modelFile
if models.Count = 0 then
- printfn "spec for method %s.%s is inconsistent (no valid solution exists)" (GetClassName comp) methodName
- None //failwith "inconsistent spec" // TODO: instead of failing, just continue
+ // no models means that the "assert false" was verified, which means that the spec is inconsistent
+ printfn " !!! SPEC IS INCONSISTENT !!!"
+ None
else
- if models.Count > 1 then failwith "why did we get more than one model for a single constructor analysis???"
+ if models.Count > 1 then
+ printfn " FAILED "
+ failwith "internal error (more than one model for a single constructor analysis)"
+ printfn " OK "
let model = models.[0]
- Some(ReadFieldValuesFromModel model prog comp m)
+ let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
+ if _opt_verifySolutions then
+ printf " - verifying synthesized solution ..."
+ if VerifySolution (heap,env,ctx) prog comp m then
+ printfn " OK"
+ Some(heap,env,ctx)
+ else
+ printfn " NOT VERIFIED"
+ Some(heap,env,ctx)
+ else
+ Some(heap,env,ctx)
let rec AnalyzeMethods prog members =
match members with
| (comp,m) :: rest ->
match m with
- | Method(methodName,signature,pre,post,true) ->
- let solOpt = AnalyzeConstructor prog comp methodName signature pre post
+ | Method(_,_,_,_,true) ->
+ let solOpt = AnalyzeConstructor prog comp m
match solOpt with
| Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
| None -> AnalyzeMethods prog rest
@@ -99,7 +135,8 @@ let Analyze prog =
let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
use file = System.IO.File.CreateText(dafnySynthFile)
file.AutoFlush <- true
- let synthCode = PrintImplCode prog solutions
+ printfn "Printing synthesized code"
+ let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze
fprintfn file "%s" synthCode
()
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index 45fd2aff..26d27fef 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -51,7 +51,7 @@ type Member =
type TopLevelDecl =
| Class of string * string list * Member list
- | Model of string * string list * VarDecl list * Expr list * Expr
+ | Model of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr
| Code of string * string list
type SyntacticProgram =
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 23e802ab..47ee49b7 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -25,6 +25,15 @@ let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
let TrueLiteral = IdLiteral("true")
let FalseLiteral = IdLiteral("false")
+let rec SplitIntoConjunts expr =
+ match expr with
+ | IdLiteral("true") -> []
+ | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
+ | _ -> [expr]
+
+let rec ForeachConjunct f expr =
+ SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""
+
// --- search functions ---
let FilterFieldMembers members =
@@ -44,13 +53,13 @@ let FilterMembers prog filter =
| Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]
| _ -> acc) []
-let AllFields c =
- match c with
+let GetAllFields comp =
+ match comp with
| Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
let aVars = FilterFieldMembers members
List.concat [aVars ; cVars]
| _ -> []
-
+
let GetClassName comp =
match comp with
| Component(Class(name,_,_),_,_) -> name
@@ -61,6 +70,13 @@ let GetMethodName mthd =
| Method(name,_,_,_,_) -> name
| _ -> failwith ("not a method: " + mthd.ToString())
+let GetInvariantsAsList comp =
+ match comp with
+ | Component(Class(_,_,members), Model(_,_,_,_,inv), _) ->
+ let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
+ List.append (SplitIntoConjunts inv) clsInvs
+ | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())
+
let GetMembers comp =
match comp with
| Component(Class(_,_,members),_,_) -> members
@@ -79,6 +95,6 @@ let FindVar (prog: Program) clsName fldName =
let copt = FindComponent prog clsName
match copt with
| Some(comp) ->
- AllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
- |> Utils.ListToOption
+ GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
+ |> Utils.ListToOption
| None -> None \ No newline at end of file
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 6b08bf58..75422de7 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -35,10 +35,10 @@ let GetFieldsValidExprList clsName allFields prog : Expr list =
GetFieldValidExpr name validFunName numUnrolls
)
-let PrintValidFunctionCode clsName clsMembers modelInv vars prog : string =
- let invMembers = clsMembers |> List.filter (function Invariant(_) -> true | _ -> false)
- let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
- let allInvs = modelInv :: clsInvs
+let PrintValidFunctionCode comp prog : string =
+ let clsName = GetClassName comp
+ let vars = GetAllFields comp
+ let allInvs = GetInvariantsAsList comp
let fieldsValid = GetFieldsValidExprList clsName vars prog
let idt = " "
let PrintInvs invs =
@@ -68,7 +68,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
match prog with
| Program(components) -> components |> List.fold (fun acc comp ->
match comp with
- | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+ | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp ->
let aVars = FilterFieldMembers members
let allVars = List.concat [aVars ; cVars];
let compMethods = FilterConstructorMembers members
@@ -79,7 +79,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
(sprintf "%s" (PrintFields aVars 2 true)) + newline +
(sprintf "%s" (PrintFields cVars 2 false)) + newline +
// generate the Valid function
- (sprintf "%s" (PrintValidFunctionCode name members inv allVars prog)) + newline +
+ (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline +
// call the method printer function on all methods of this component
(compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") +
// the end of the class
@@ -119,7 +119,6 @@ let PrintHeapCreationCode (heap,env,ctx) indent =
(PrintVarAssignments (heap,env,ctx) indent)
let GenConstructorCode mthd body =
- printfn "Printing code for method %s." (GetMethodName mthd)
let validExpr = IdLiteral("Valid()");
match mthd with
| Method(methodName, sign, pre, post, _) ->
@@ -143,8 +142,8 @@ let GetMethodsToAnalyze prog =
FilterMembers prog FilterConstructorMembers
// solutions: (comp, constructor) |--> (heap, env, ctx)
-let PrintImplCode prog solutions =
- let methods = GetMethodsToAnalyze prog
+let PrintImplCode prog solutions methodsToPrintFunc =
+ let methods = methodsToPrintFunc prog
PrintDafnyCodeSkeleton prog (fun comp mthd ->
if Utils.ListContains (comp,mthd) methods then
let mthdBody = match Map.tryFind (comp,mthd) solutions with
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 9d776796..4341dfcf 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -42,6 +42,7 @@
<FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
</PropertyGroup>
<ItemGroup>
+ <Compile Include="Options.fs" />
<Compile Include="Utils.fs" />
<Compile Include="PipelineUtils.fs" />
<Compile Include="Ast.fs" />
diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs
index 2363995d..35507d1e 100644
--- a/Jennisys/PipelineUtils.fs
+++ b/Jennisys/PipelineUtils.fs
@@ -1,7 +1,9 @@
module PipelineUtils
let dafnyScratchFile = @"c:\tmp\jennisys-scratch.dfy"
-let dafnyModelFile = @"c:\tmp\jennisys-scratch.model"
+let dafnyVerifyFile = @"c:\tmp\jennisys-verify.dfy"
+let dafnyModelFile = @"c:\tmp\jennisys-scratch.bvd"
+let dafnyVerifyModelFile = @"c:\tmp\jennisys-verify.bvd"
let dafnyOutFile = @"c:\tmp\jennisys-scratch.out"
let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy"
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index 97b537db..5410db31 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -1,6 +1,7 @@
module Printer
open Ast
+open AstUtils
let newline = System.Environment.NewLine // "\r\n"
@@ -79,15 +80,6 @@ let PrintSig signature =
else ""
sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
-let rec SplitIntoConjunts expr =
- match expr with
- | IdLiteral("true") -> []
- | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
- | _ -> [expr]
-
-let rec ForeachConjunct f expr =
- SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""
-
let rec Indent i =
if i = 0 then "" else " " + (Indent (i-1))
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index 5c95e20f..771fe680 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -8,9 +8,7 @@ class IntList {
ensures list = [2]
constructor OneTwo()
- ensures |list| = 2
- ensures list[0] = 1
- ensures list[1] = 2
+ ensures list = [1] + [2]
}
model IntList {
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index 1b6cef80..13ed2878 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -8,9 +8,7 @@ class IntList {
ensures list = [2]
constructor OneTwo()
- ensures |list| = 2
- ensures list[0] = 1
- ensures list[1] = 2
+ ensures list = [1] + [2]
}
model IntList {
@@ -23,7 +21,7 @@ model IntList {
root = null ==> |list| = 0
root != null ==> (|list| = |root.succ| + 1 &&
list[0] = root.data &&
- (forall i :: (0 < i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data)))
+ (forall i:int :: (0 <= i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data)))
}
class IntNode {
@@ -36,7 +34,7 @@ class IntNode {
constructor OneTwo()
ensures data = 1
- ensures |succ| = 1 && succ[0] != null && succ[0].data = 1
+ ensures |succ| = 1 && succ[0] != null && succ[0].data = 2
invariant
!(null in succ)
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-05 14:03:21 +0000