diff options
| author |  Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-06 19:56:38 -0700 |
|---|---|---|
| committer | Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-06 19:56:38 -0700 |
| commit | 0e4936c6b468b371c502cc5c7e7a311d7ae43bd6 (patch) | |
| tree | 45a02f5dc7885af87f39a2e1ed84720166cbf928 | |
| parent | 1b515b1aa3e92feceab97b3b65ce7f45bdccf274 (diff) | |
- fixed some bugs with applying unification over list elements
- fixed the List.jen example (generic list)
- changed SeqConst and SetConst to contain a list/set of "Const"
and not "Const option" like before
| -rw-r--r-- | Jennisys/Jennisys.sln | 21 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Analyzer.fs | 56 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Ast.fs | 9 | ||||
| -rw-r--r-- | Jennisys/Jennisys/AstUtils.fs | 501 | ||||
| -rw-r--r-- | Jennisys/Jennisys/CodeGen.fs | 272 | ||||
| -rw-r--r-- | Jennisys/Jennisys/DafnyModelUtils.fs | 87 | ||||
| -rw-r--r-- | Jennisys/Jennisys/DafnyPrinter.fs | 12 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Jennisys.fs | 10 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Jennisys.fsproj | 12 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Parser.fsy | 12 | ||||
| -rw-r--r-- | Jennisys/Jennisys/PipelineUtils.fs | 75 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Printer.fs | 19 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Resolver.fs | 33 | ||||
| -rw-r--r-- | Jennisys/Jennisys/TypeChecker.fs | 32 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Utils.fs | 26 | ||||
| -rw-r--r-- | Jennisys/Jennisys/examples/List.jen | 6 | ||||
| -rw-r--r-- | Jennisys/Jennisys/examples/List3.jen | 2 |
17 files changed, 619 insertions, 566 deletions
diff --git a/Jennisys/Jennisys.sln b/Jennisys/Jennisys.sln index bb45d27c..af8d8f4a 100644 --- a/Jennisys/Jennisys.sln +++ b/Jennisys/Jennisys.sln @@ -2,15 +2,9 @@ Microsoft Visual Studio Solution File, Format Version 11.00
# Visual Studio 2010
Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Jennisys", "Jennisys\Jennisys.fsproj", "{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}"
- ProjectSection(ProjectDependencies) = postProject
- {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} = {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C} = {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}
- EndProjectSection
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\Source\Model\Model.csproj", "{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ModelViewer", "..\Source\ModelViewer\ModelViewer.csproj", "{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}"
-EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|Any CPU = Checked|Any CPU
@@ -54,21 +48,6 @@ Global {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Mixed Platforms.Build.0 = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|x86.ActiveCfg = Release|Any CPU
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Any CPU.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index 244b50b4..24b8cbc7 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -37,7 +37,12 @@ let rec Substitute substMap = function | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) | expr -> expr -let GenMethodAnalysisCode comp methodName signature pre post assertion = +let GenMethodAnalysisCode comp m assertion = + let methodName = GetMethodName m + let signature = GetMethodSig m + let ppre,ppost = GetMethodPrePost m + let pre = Desugar ppre + let post = Desugar ppost " method " + methodName + "()" + newline + " modifies this;" + newline + " {" + newline + @@ -61,7 +66,7 @@ let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd = match onlyForThisCompMethod with | (c,m) when c = comp && m = mthd -> match m with - | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post assertion) + newline + | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp m assertion) + newline | _ -> "" | _ -> "" @@ -142,20 +147,23 @@ let GetObjRefExpr o (heap,env,ctx) = _GetObjRefExpr o (heap,env,ctx) (Set.empty) let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = + let __CheckUnif o f e idx = + let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx))) + let fldName = PrintVarName f + let lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) + let assertionExpr = BinaryEq lhs e + // check if the assertion follows and if so update the env + let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) + Logger.Debug(" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") + CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) + match unifs with | (c,e) :: rest -> let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx) let newHeap = restHeap |> Map.fold (fun acc (o,f) l -> - let value = Resolve l (env,ctx) + let value = TryResolve l (env,ctx) if value = c then - let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx))) - let fldName = PrintVarName f - let assertionExpr = BinaryEq (Dot(objRefExpr, fldName)) e - // check if the assertion follows and if so update the env - let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) - Logger.Debug(" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") - let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) - if ok then + if __CheckUnif o f e -1 then Logger.DebugLine " HOLDS" // change the value to expression acc |> Map.add (o,f) (ExprConst(e)) @@ -164,11 +172,24 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = // don't change the value acc |> Map.add (o,f) l else - // see if it's a list, then try to match its elements + // see if it's a list, then try to match its elements, otherwise leave it as is match value with - | SeqConst(clist) -> acc |> Map.add (o,f) l //TODO!! + | SeqConst(clist) -> + let rec __UnifyOverLst lst cnt = + match lst with + | lstElem :: rest when lstElem = c -> + if __CheckUnif o f e cnt then + Logger.DebugLine " HOLDS" + ExprConst(e) :: __UnifyOverLst rest (cnt+1) + else + Logger.DebugLine " DOESN'T HOLDS" + lstElem :: __UnifyOverLst rest (cnt+1) + | lstElem :: rest -> + lstElem :: __UnifyOverLst rest (cnt+1) + | [] -> [] + let newLstConst = __UnifyOverLst clist 0 + acc |> Map.add (o,f) (SeqConst(newLstConst)) | _ -> - // leave it as is acc |> Map.add (o,f) l ) restHeap (newHeap,env,ctx) @@ -181,7 +202,7 @@ let GeneralizeSolution prog comp mthd (heap,env,ctx) = match args with | [] -> (heap,env,ctx) | _ -> - let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx) + let unifs = GetUnifications (BinaryAnd pre post |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv |> Set.union (GetArgValueUnifications args env) UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx) | _ -> failwith ("not a method: " + mthd.ToString()) @@ -252,9 +273,10 @@ let rec AnalyzeMethods prog members = | _ -> AnalyzeMethods prog rest | [] -> Map.empty -let Analyze prog = +let Analyze prog filename = let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) - use file = System.IO.File.CreateText(dafnySynthFile) + let progName = System.IO.Path.GetFileNameWithoutExtension(filename) + use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName)) file.AutoFlush <- true Logger.InfoLine "Printing synthesized code" let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs index bd66e688..5c42dbec 100644 --- a/Jennisys/Jennisys/Ast.fs +++ b/Jennisys/Jennisys/Ast.fs @@ -13,8 +13,8 @@ type Type = | BoolType
| SetType of Type (* type parameter *)
| SeqType of Type (* type parameter *)
- | NamedType of string
- | InstantiatedType of string * Type (* type parameter *)
+ | NamedType of string * string list (* type parameters *)
+ | InstantiatedType of string * Type list (* type parameters *)
type VarDecl =
| Var of string * Type option
@@ -61,9 +61,10 @@ type Program = type Const =
| IntConst of int
| BoolConst of bool
- | SetConst of Set<Const option>
- | SeqConst of (Const option) list
+ | SetConst of Set<Const>
+ | SeqConst of Const list
| NullConst
+ | NoneConst
| ThisConst of (* loc id *) string * Type option
| NewObj of (* loc id *) string * Type option
| ExprConst of Expr
diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs index 442dfe57..af80fb65 100644 --- a/Jennisys/Jennisys/AstUtils.fs +++ b/Jennisys/Jennisys/AstUtils.fs @@ -10,17 +10,17 @@ open Utils // ------------------------------- Visitor Stuff -------------------------------------------
let rec VisitExpr visitorFunc expr acc =
- match expr with - | IntLiteral(_) - | IdLiteral(_) - | Star -> acc |> visitorFunc expr - | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e - | SelectExpr(e1, e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 - | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3 - | SequenceExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc) - | SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e - | ForallExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e - | UnaryExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e + match expr with
+ | IntLiteral(_)
+ | IdLiteral(_)
+ | Star -> acc |> visitorFunc expr
+ | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+ | SelectExpr(e1, e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+ | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
+ | SequenceExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
+ | SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+ | ForallExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+ | UnaryExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
| BinaryExpr(_,_,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
// ------------------------------- End Visitor Stuff -------------------------------------------
@@ -28,186 +28,186 @@ let rec VisitExpr visitorFunc expr acc = exception EvalFailed
let rec EvalSym expr =
- match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> VarConst(id) - | Dot(e, str) -> - match EvalSym e with - | VarConst(lhsName) -> VarConst(lhsName + "." + str) - | _ -> ExprConst(expr) - | SeqLength(e) -> - match EvalSym e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> ExprConst(expr) - | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev |> Utils.ConvertToOptionList - SeqConst(clist) - | SelectExpr(lst, idx) -> - match EvalSym lst, EvalSym idx with - | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption - | _ -> ExprConst(expr) - | UpdateExpr(lst,idx,v) -> - match EvalSym lst, EvalSym idx, EvalSym v with - | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) - | _ -> ExprConst(expr) - | BinaryExpr(_,op,e1,e2) -> - match op with - | Exact "=" _ -> - match EvalSym e1, EvalSym e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) - | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) - | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) - | _ -> ExprConst(expr) - | Exact "!=" _ -> - match EvalSym e1, EvalSym e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) - | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) - | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) - | _ -> ExprConst(expr) - | Exact "<" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) - | _ -> ExprConst(expr) - | Exact "<=" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) - | _ -> ExprConst(expr) - | Exact ">" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) - | _ -> ExprConst(expr) - | Exact ">=" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) - | _ -> ExprConst(expr) - | Exact "in" _ -> - match EvalSym e1, EvalSym e2 with - | _ as c, SetConst(s) -> BoolConst(Set.contains (Some(c)) s) - | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains (Some(c)) s) - | _ -> ExprConst(expr) - | Exact "!in" _ -> - match EvalSym e1, EvalSym e2 with - | _ as c, SetConst(s) -> BoolConst(not (Set.contains (Some(c)) s)) - | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains (Some(c)) s)) - | _ -> ExprConst(expr) - | Exact "+" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) - | _ -> ExprConst(expr) - | Exact "-" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) - | _ -> ExprConst(expr) - | Exact "*" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) - | _ -> ExprConst(expr) - | Exact "div" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) - | _ -> ExprConst(expr) - | Exact "mod" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) - | UnaryExpr(op, e) -> - match op with - | Exact "!" _ -> - match EvalSym e with - | BoolConst(b) -> BoolConst(not b) - | _ -> ExprConst(expr) - | Exact "-" _ -> - match EvalSym e with - | IntConst(n) -> IntConst(-n) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) + match expr with
+ | IntLiteral(n) -> IntConst(n)
+ | IdLiteral(id) -> VarConst(id)
+ | Dot(e, str) ->
+ match EvalSym e with
+ | VarConst(lhsName) -> VarConst(lhsName + "." + str)
+ | _ -> ExprConst(expr)
+ | SeqLength(e) ->
+ match EvalSym e with
+ | SeqConst(clist) -> IntConst(List.length clist)
+ | _ -> ExprConst(expr)
+ | SequenceExpr(elist) ->
+ let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev
+ SeqConst(clist)
+ | SelectExpr(lst, idx) ->
+ match EvalSym lst, EvalSym idx with
+ | SeqConst(clist), IntConst(n) -> clist.[n]
+ | _ -> ExprConst(expr)
+ | UpdateExpr(lst,idx,v) ->
+ match EvalSym lst, EvalSym idx, EvalSym v with
+ | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)
+ | _ -> ExprConst(expr)
+ | BinaryExpr(_,op,e1,e2) ->
+ match op with
+ | Exact "=" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2)
+ | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2)
+ | _ -> ExprConst(expr)
+ | Exact "!=" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))
+ | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2))
+ | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2))
+ | _ -> ExprConst(expr)
+ | Exact "<" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2))
+ | _ -> ExprConst(expr)
+ | Exact "<=" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2))
+ | _ -> ExprConst(expr)
+ | Exact ">" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2))
+ | _ -> ExprConst(expr)
+ | Exact ">=" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2))
+ | _ -> ExprConst(expr)
+ | Exact "in" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | _ as c, SetConst(s) -> BoolConst(Set.contains c s)
+ | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s)
+ | _ -> ExprConst(expr)
+ | Exact "!in" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s))
+ | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s))
+ | _ -> ExprConst(expr)
+ | Exact "+" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+ | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
+ | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
+ | _ -> ExprConst(expr)
+ | Exact "-" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+ | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)
+ | _ -> ExprConst(expr)
+ | Exact "*" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)
+ | _ -> ExprConst(expr)
+ | Exact "div" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)
+ | _ -> ExprConst(expr)
+ | Exact "mod" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)
+ | _ -> ExprConst(expr)
+ | _ -> ExprConst(expr)
+ | UnaryExpr(op, e) ->
+ match op with
+ | Exact "!" _ ->
+ match EvalSym e with
+ | BoolConst(b) -> BoolConst(not b)
+ | _ -> ExprConst(expr)
+ | Exact "-" _ ->
+ match EvalSym e with
+ | IntConst(n) -> IntConst(-n)
+ | _ -> ExprConst(expr)
+ | _ -> ExprConst(expr)
| _ -> ExprConst(expr)
//TODO: stuff might be missing
let rec EvalToConst expr =
- match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> raise EvalFailed //VarConst(id) - | Dot(e, str) -> raise EvalFailed - | SeqLength(e) -> - match EvalToConst e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> raise EvalFailed - | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev |> Utils.ConvertToOptionList - SeqConst(clist) - | SelectExpr(lst, idx) -> - match EvalToConst lst, EvalToConst idx with - | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption - | _ -> raise EvalFailed - | UpdateExpr(lst,idx,v) -> - match EvalToConst lst, EvalToConst idx, EvalToConst v with - | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) - | _ -> raise EvalFailed - | BinaryExpr(_,op,e1,e2) -> - match op with - | Exact "=" _ -> - try - BoolConst(EvalToBool(e1) = EvalToBool(e2)) - with - | EvalFailed -> BoolConst(EvalToInt(e1) = EvalToInt(e2)) - | Exact "!=" _ -> - try - BoolConst(not(EvalToBool(e1) = EvalToBool(e2))) - with - | EvalFailed -> BoolConst(not(EvalToInt e1 = EvalToInt e2)) - | Exact "<" _ -> BoolConst(EvalToInt e1 < EvalToInt e2) //TODO sets, seqs - | Exact "<=" _ -> BoolConst(EvalToInt e1 <= EvalToInt e2) //TODO sets, seqs - | Exact ">" _ -> BoolConst(EvalToInt e1 > EvalToInt e2) //TODO sets, seqs - | Exact ">=" _ -> BoolConst(EvalToInt e1 >= EvalToInt e2) //TODO sets, seqs - | Exact "in" _ -> raise EvalFailed //TODO - | Exact "!in" _ -> raise EvalFailed //TODO - | Exact "+" _ -> - match EvalToConst e1, EvalToConst e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) - | _ -> raise EvalFailed - | Exact "-" _ -> IntConst(EvalToInt e1 - EvalToInt e2) - | Exact "*" _ -> IntConst(EvalToInt e1 * EvalToInt e2) - | Exact "div" _ -> IntConst(EvalToInt e1 / EvalToInt e2) - | Exact "mod" _ -> IntConst(EvalToInt e1 % EvalToInt e2) - | _ -> raise EvalFailed - | UnaryExpr(op, e) -> - match op with - | Exact "!" _ -> BoolConst(not (EvalToBool e)) - | Exact "-" _ -> IntConst(-(EvalToInt e)) - | _ -> raise EvalFailed - | _ -> raise EvalFailed -and EvalToBool e = - let c = EvalToConst e - match c with - | BoolConst(b) -> b - | _ -> raise EvalFailed -and EvalToInt e = - let c = EvalToConst e - match c with - | IntConst(n) -> n - | _ -> raise EvalFailed - + match expr with
+ | IntLiteral(n) -> IntConst(n)
+ | IdLiteral(id) -> raise EvalFailed //VarConst(id)
+ | Dot(e, str) -> raise EvalFailed
+ | SeqLength(e) ->
+ match EvalToConst e with
+ | SeqConst(clist) -> IntConst(List.length clist)
+ | _ -> raise EvalFailed
+ | SequenceExpr(elist) ->
+ let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev
+ SeqConst(clist)
+ | SelectExpr(lst, idx) ->
+ match EvalToConst lst, EvalToConst idx with
+ | SeqConst(clist), IntConst(n) -> clist.[n]
+ | _ -> raise EvalFailed
+ | UpdateExpr(lst,idx,v) ->
+ match EvalToConst lst, EvalToConst idx, EvalToConst v with
+ | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n c clist)
+ | _ -> raise EvalFailed
+ | BinaryExpr(_,op,e1,e2) ->
+ match op with
+ | Exact "=" _ ->
+ try
+ BoolConst(EvalToBool(e1) = EvalToBool(e2))
+ with
+ | EvalFailed -> BoolConst(EvalToInt(e1) = EvalToInt(e2))
+ | Exact "!=" _ ->
+ try
+ BoolConst(not(EvalToBool(e1) = EvalToBool(e2)))
+ with
+ | EvalFailed -> BoolConst(not(EvalToInt e1 = EvalToInt e2))
+ | Exact "<" _ -> BoolConst(EvalToInt e1 < EvalToInt e2) //TODO sets, seqs
+ | Exact "<=" _ -> BoolConst(EvalToInt e1 <= EvalToInt e2) //TODO sets, seqs
+ | Exact ">" _ -> BoolConst(EvalToInt e1 > EvalToInt e2) //TODO sets, seqs
+ | Exact ">=" _ -> BoolConst(EvalToInt e1 >= EvalToInt e2) //TODO sets, seqs
+ | Exact "in" _ -> raise EvalFailed //TODO
+ | Exact "!in" _ -> raise EvalFailed //TODO
+ | Exact "+" _ ->
+ match EvalToConst e1, EvalToConst e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+ | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
+ | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
+ | _ -> raise EvalFailed
+ | Exact "-" _ -> IntConst(EvalToInt e1 - EvalToInt e2)
+ | Exact "*" _ -> IntConst(EvalToInt e1 * EvalToInt e2)
+ | Exact "div" _ -> IntConst(EvalToInt e1 / EvalToInt e2)
+ | Exact "mod" _ -> IntConst(EvalToInt e1 % EvalToInt e2)
+ | _ -> raise EvalFailed
+ | UnaryExpr(op, e) ->
+ match op with
+ | Exact "!" _ -> BoolConst(not (EvalToBool e))
+ | Exact "-" _ -> IntConst(-(EvalToInt e))
+ | _ -> raise EvalFailed
+ | _ -> raise EvalFailed
+and EvalToBool e =
+ let c = EvalToConst e
+ match c with
+ | BoolConst(b) -> b
+ | _ -> raise EvalFailed
+and EvalToInt e =
+ let c = EvalToConst e
+ match c with
+ | IntConst(n) -> n
+ | _ -> raise EvalFailed
+
let rec Const2Expr c =
match c with
| IntConst(n) -> IntLiteral(n)
| BoolConst(b) -> if b then IntLiteral(1) else IntLiteral(0) //?? BoolLiteral(b)
| SeqConst(clist) ->
- let expList = clist |> List.fold (fun acc c -> Const2Expr (Utils.ExtractOption c) :: acc) [] |> List.rev
+ let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev
SequenceExpr(expList)
| ThisConst(_) -> IdLiteral("this")
| VarConst(v) -> IdLiteral(v)
@@ -264,64 +264,64 @@ let FalseLiteral = IdLiteral("false") // ==========================================
/// Splits "expr" into a list of its conjuncts
-// ========================================== -let rec SplitIntoConjunts expr = - match expr with - | IdLiteral("true") -> [] - | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1] - | _ -> [expr] - -// ====================================== -/// Applies "f" to each conjunct of "expr" -// ====================================== -let rec ForeachConjunct f expr = +// ==========================================
+let rec SplitIntoConjunts expr =
+ match expr with
+ | IdLiteral("true") -> []
+ | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
+ | _ -> [expr]
+
+// ======================================
+/// Applies "f" to each conjunct of "expr"
+// ======================================
+let rec ForeachConjunct f expr =
SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""
// --- search functions ---
// =========================================================
/// Out of all "members" returns only those that are "Field"s
-// ========================================================= -let FilterFieldMembers members = - members |> List.choose (function Field(vd) -> Some(vd) | _ -> None) - -// ============================================================= -/// Out of all "members" returns only those that are constructors -// ============================================================= -let FilterConstructorMembers members = - members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None) - -// ============================================================= -/// Out of all "members" returns only those that are -/// constructors and have at least one input parameter -// ============================================================= -let FilterConstructorMembersWithParams members = - members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) - -// ========================================================== -/// Out of all "members" returns only those that are "Method"s -// ========================================================== -let FilterMethodMembers members = - members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None) - -// ======================================================================= -/// Returns all members of the program "prog" that pass the filter "filter" -// ======================================================================= -let FilterMembers prog filter = - match prog with - | Program(components) -> - components |> List.fold (fun acc comp -> - match comp with - | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))] +// =========================================================
+let FilterFieldMembers members =
+ members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
+
+// =============================================================
+/// Out of all "members" returns only those that are constructors
+// =============================================================
+let FilterConstructorMembers members =
+ members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)
+
+// =============================================================
+/// Out of all "members" returns only those that are
+/// constructors and have at least one input parameter
+// =============================================================
+let FilterConstructorMembersWithParams members =
+ members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None)
+
+// ==========================================================
+/// Out of all "members" returns only those that are "Method"s
+// ==========================================================
+let FilterMethodMembers members =
+ members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None)
+
+// =======================================================================
+/// Returns all members of the program "prog" that pass the filter "filter"
+// =======================================================================
+let FilterMembers prog filter =
+ match prog with
+ | Program(components) ->
+ components |> List.fold (fun acc comp ->
+ match comp with
+ | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]
| _ -> acc) []
// =================================
/// Returns all fields of a component
// =================================
let GetAllFields comp =
- match comp with - | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) -> - let aVars = FilterFieldMembers members + match comp with
+ | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
+ let aVars = FilterFieldMembers members
List.concat [aVars ; cVars]
| _ -> []
@@ -333,6 +333,11 @@ let GetClassName comp = | Component(Class(name,_,_),_,_) -> name
| _ -> failwith ("unrecognized component: " + comp.ToString())
+let GetClassType comp =
+ match comp with
+ | Component(Class(name,typeParams,_),_,_) -> NamedType(name, typeParams)
+ | _ -> failwith ("unrecognized component: " + comp.ToString())
+
// ========================
/// Returns name of a method
// ========================
@@ -355,6 +360,11 @@ let GetMethodSig mthd = | Method(_,sgn,_,_,_) -> sgn
| _ -> failwith ("not a method: " + mthd.ToString())
+let GetMethodPrePost mthd =
+ match mthd with
+ | Method(_,_,pre,post,_) -> pre,post
+ | _ -> failwith ("not a method: " + mthd.ToString())
+
// =========================================================
/// Returns all arguments of a method (both input and output)
// =========================================================
@@ -363,6 +373,15 @@ let GetMethodArgs mthd = | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs]
| _ -> failwith ("not a method: " + mthd.ToString())
+let rec GetTypeShortName ty =
+ match ty with
+ | IntType -> "int"
+ | BoolType -> "bool"
+ | SetType(_) -> "set"
+ | SeqType(_) -> "seq"
+ | NamedType(n,_) -> n
+ | InstantiatedType(n,_) -> n
+
// ==============================================================
/// Returns all invariants of a component as a list of expressions
// ==============================================================
@@ -415,17 +434,17 @@ let FindVar (prog: Program) clsName fldName = /// are expanded into explicit assignments to indexed elements
// ==========================================================
let rec Desugar expr =
- match expr with - | IntLiteral(_) - | IdLiteral(_) - | Star - | Dot(_) - | SelectExpr(_) - | SeqLength(_) -> expr - | UpdateExpr(_) -> expr //TODO - | SequenceExpr(exs) -> expr //TODO - | ForallExpr(v,e) -> ForallExpr(v, Desugar e) - | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e) + match expr with
+ | IntLiteral(_)
+ | IdLiteral(_)
+ | Star
+ | Dot(_)
+ | SelectExpr(_)
+ | SeqLength(_) -> expr
+ | UpdateExpr(_) -> expr //TODO
+ | SequenceExpr(exs) -> expr //TODO
+ | ForallExpr(v,e) -> ForallExpr(v, Desugar e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e)
| BinaryExpr(p,op,e1,e2) ->
let be = BinaryExpr(p, op, Desugar e1, Desugar e2)
try
@@ -436,13 +455,13 @@ let rec Desugar expr = | SeqConst(clist), VarConst(v) ->
let rec __fff lst cnt =
match lst with
- | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr (Utils.ExtractOption clist.[cnt])) :: __fff rest (cnt+1)
+ | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr clist.[cnt]) :: __fff rest (cnt+1)
| [] -> []
__fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
| SeqConst(cl1), SeqConst(cl2) ->
let rec __fff lst1 lst2 cnt =
match lst1, lst2 with
- | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr (Utils.ExtractOption cl1.[cnt])) (Const2Expr (Utils.ExtractOption cl2.[cnt])) :: __fff rest1 rest2 (cnt+1)
+ | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr cl1.[cnt]) (Const2Expr cl2.[cnt]) :: __fff rest1 rest2 (cnt+1)
| [], [] -> []
| _ -> failwith "Lists are of different sizes"
__fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs index 7e61ec7e..3c97b94f 100644 --- a/Jennisys/Jennisys/CodeGen.fs +++ b/Jennisys/Jennisys/CodeGen.fs @@ -2,7 +2,7 @@ open Ast
open AstUtils
-open Utils +open Utils
open Printer
open Resolver
open TypeChecker
@@ -18,143 +18,143 @@ let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr (BinaryAnd (Dot(fldExpr, validFunName))
(GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))
-let GetFieldValidExpr fldName validFunName numUnrolls : Expr = - GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls - //BinaryImplies (BinaryNeq (IdLiteral(fldName)) (IdLiteral("null"))) (Dot(IdLiteral(fldName), validFunName)) - -let GetFieldsForValidExpr allFields prog : VarDecl list = - allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true - | _ -> false) - -let GetFieldsValidExprList clsName allFields prog : Expr list = - let fields = GetFieldsForValidExpr allFields prog - fields |> List.map (function Var(name, t) -> - let validFunName, numUnrolls = - match t with - | Some(ty) when clsName = (PrintType ty) -> "Valid_self()", numLoopUnrolls - | _ -> "Valid()", 1 - GetFieldValidExpr name validFunName numUnrolls - ) - -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 = - invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) [] - |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e)) - |> fun s -> if s = "" then (idt + "true") else s - // TODO: don't hardcode decr vars!!! -// let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then -// ["list"] -// else -// [] -// (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) + - " function Valid_self(): bool" + newline + - " reads *;" + newline + - " {" + newline + - (PrintInvs allInvs) + newline + - " }" + newline + - newline + - " function Valid(): bool" + newline + - " reads *;" + newline + - " {" + newline + - " this.Valid_self() &&" + newline + - (PrintInvs fieldsValid) + newline + +let GetFieldValidExpr fldName validFunName numUnrolls : Expr =
+ GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls
+
+let GetFieldsForValidExpr allFields prog : VarDecl list =
+ allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
+ | _ -> false)
+
+let GetFieldsValidExprList clsName allFields prog : Expr list =
+ let fields = GetFieldsForValidExpr allFields prog
+ fields |> List.map (function Var(name, t) ->
+ let validFunName, numUnrolls =
+ match t with
+ | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", numLoopUnrolls
+ | _ -> "Valid()", 1
+ GetFieldValidExpr name validFunName numUnrolls
+ )
+
+let PrintValidFunctionCode comp prog : string =
+ let idt = " "
+ let __PrintInvs invs =
+ invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
+ |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e))
+ |> fun s -> if s = "" then (idt + "true") else s
+ let clsName = GetClassName comp
+ let vars = GetAllFields comp
+ let allInvs = GetInvariantsAsList comp |> DesugarLst
+ let fieldsValid = GetFieldsValidExprList clsName vars prog
+
+ // TODO: don't hardcode decr vars!!!
+// let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then
+// ["list"]
+// else
+// []
+// (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
+ " function Valid_self(): bool" + newline +
+ " reads *;" + newline +
+ " {" + newline +
+ (__PrintInvs allInvs) + newline +
+ " }" + newline +
+ newline +
+ " function Valid(): bool" + newline +
+ " reads *;" + newline +
+ " {" + newline +
+ " this.Valid_self() &&" + newline +
+ (__PrintInvs fieldsValid) + newline +
" }" + newline
-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) as comp -> - let aVars = FilterFieldMembers members - let allVars = List.concat [aVars ; cVars]; - let compMethods = FilterConstructorMembers members - // Now print it as a Dafny program - acc + - (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline + - // the fields: original abstract fields plus concrete fields - (sprintf "%s" (PrintFields aVars 2 true)) + newline + - (sprintf "%s" (PrintFields cVars 2 false)) + newline + - // generate the Valid function - (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 - "}" + newline + newline +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) as comp ->
+ let aVars = FilterFieldMembers members
+ let allVars = List.concat [aVars ; cVars];
+ let compMethods = FilterConstructorMembers members
+ // Now print it as a Dafny program
+ acc +
+ (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +
+ // the fields: original abstract fields plus concrete fields
+ (sprintf "%s" (PrintFields aVars 2 true)) + newline +
+ (sprintf "%s" (PrintFields cVars 2 false)) + newline +
+ // generate the Valid function
+ (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
+ "}" + newline + newline
| _ -> assert false; "") ""
-let PrintAllocNewObjects (heap,env,ctx) indent = - let idt = Indent indent - env |> Map.fold (fun acc l v -> - match v with - | NewObj(_,_) -> acc |> Set.add v - | _ -> acc - ) Set.empty - |> Set.fold (fun acc newObjConst -> - match newObjConst with - | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline) - | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString()) - ) "" - -let PrintObjRefName o (env,ctx) = - match Resolve o (env,ctx) with - | ThisConst(_,_) -> "this"; - | NewObj(name, _) -> PrintGenSym name - | _ -> failwith ("unresolved object ref: " + o.ToString()) - -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 = Resolve l (env,ctx) |> PrintConst - acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline - ) "" - -let PrintHeapCreationCode (heap,env,ctx) indent = - (PrintAllocNewObjects (heap,env,ctx) indent) + - (PrintVarAssignments (heap,env,ctx) indent) - -let GenConstructorCode mthd body = - let validExpr = IdLiteral("Valid()"); - match mthd with - | Method(methodName, sign, pre, post, _) -> - let preExpr = BinaryAnd validExpr pre - let postExpr = BinaryAnd validExpr post - let PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";") - " method " + methodName + (PrintSig sign) + newline + - " modifies this;" + newline + - (PrintPrePost " requires " preExpr) + newline + - (PrintPrePost " ensures " postExpr) + newline + - " {" + newline + - body + - " }" + newline - | _ -> "" - -// NOTE: insert here coto to say which methods to analyze -let GetMethodsToAnalyze prog = - (* exactly one *) -// let c = FindComponent prog "IntList" |> Utils.ExtractOption -// let m = FindMethod c "Sum" |> Utils.ExtractOption -// [c, m] - (* all *) - FilterMembers prog FilterConstructorMembers - (* only with parameters *) -// FilterMembers prog FilterConstructorMembersWithParams - -// solutions: (comp, constructor) |--> (heap, env, ctx) -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 - | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4 - | _ -> " //unable to synthesize" + newline - (GenConstructorCode mthd mthdBody) + newline - else - "" +let PrintAllocNewObjects (heap,env,ctx) indent =
+ let idt = Indent indent
+ env |> Map.fold (fun acc l v ->
+ match v with
+ | NewObj(_,_) -> acc |> Set.add v
+ | _ -> acc
+ ) Set.empty
+ |> Set.fold (fun acc newObjConst ->
+ match newObjConst with
+ | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline)
+ | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString())
+ ) ""
+
+let PrintObjRefName o (env,ctx) =
+ match Resolve o (env,ctx) with
+ | ThisConst(_,_) -> "this";
+ | NewObj(name, _) -> PrintGenSym name
+ | _ -> failwith ("unresolved object ref: " + o.ToString())
+
+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 = Resolve l (env,ctx) |> PrintConst
+ acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline
+ ) ""
+
+let PrintHeapCreationCode (heap,env,ctx) indent =
+ (PrintAllocNewObjects (heap,env,ctx) indent) +
+ (PrintVarAssignments (heap,env,ctx) indent)
+
+let GenConstructorCode mthd body =
+ let validExpr = IdLiteral("Valid()");
+ match mthd with
+ | Method(methodName, sign, pre, post, _) ->
+ let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")
+ let preExpr = pre
+ let postExpr = BinaryAnd validExpr post
+ " method " + methodName + (PrintSig sign) + newline +
+ " modifies this;" + newline +
+ (__PrintPrePost " requires " preExpr) + newline +
+ (__PrintPrePost " ensures " postExpr) + newline +
+ " {" + newline +
+ body +
+ " }" + newline
+ | _ -> ""
+
+// NOTE: insert here coto to say which methods to analyze
+let GetMethodsToAnalyze prog =
+ (* exactly one *)
+// let c = FindComponent prog "List" |> Utils.ExtractOption
+// let m = FindMethod c "Double" |> Utils.ExtractOption
+// [c, m]
+ (* all *)
+ FilterMembers prog FilterConstructorMembers
+ (* only with parameters *)
+// FilterMembers prog FilterConstructorMembersWithParams
+
+// solutions: (comp, constructor) |--> (heap, env, ctx)
+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
+ | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4
+ | _ -> " //unable to synthesize" + newline
+ (GenConstructorCode mthd mthdBody) + newline
+ else
+ ""
)
\ No newline at end of file diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs index 6e78dc33..597ac7c9 100644 --- a/Jennisys/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/Jennisys/DafnyModelUtils.fs @@ -23,16 +23,16 @@ open Microsoft.Boogie let argsObjRefConst = Unresolved("*0")
let GetElemFullName (elem: Model.Element) =
- elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0) - |> Seq.choose (fun ft -> Some(ft.Func.Name)) + elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0)
+ |> Seq.choose (fun ft -> Some(ft.Func.Name))
|> Utils.SeqToOption
let GetElemName (elem: Model.Element) =
- let fullNameOpt = GetElemFullName elem - match fullNameOpt with - | Some(fullName) -> - let dotIdx = fullName.LastIndexOf(".") - let fldName = fullName.Substring(dotIdx + 1) + let fullNameOpt = GetElemFullName elem
+ match fullNameOpt with
+ | Some(fullName) ->
+ let dotIdx = fullName.LastIndexOf(".")
+ let fldName = fullName.Substring(dotIdx + 1)
let clsName = if dotIdx = -1 then "" else fullName.Substring(0, dotIdx)
Some(clsName, fldName)
| None -> None
@@ -60,12 +60,15 @@ let GetBool (elem: Model.Element) = | :? Model.Boolean as bval -> bval.Value
| _ -> failwith ("not a bool element: " + elem.ToString())
-let GetType (e: Model.Element) =
+let GetType (e: Model.Element) prog =
let fNameOpt = GetElemFullName e
match fNameOpt with
| Some(fname) -> match fname with
| Exact "intType" _ -> Some(IntType)
- | Prefix "class." clsName -> Some(NamedType(clsName))
+ | Prefix "class." clsName ->
+ match FindComponent prog clsName with
+ | Some(comp) -> Some(GetClassType comp)
+ | None -> None
| _ -> None
| None -> None
@@ -100,8 +103,8 @@ let rec UpdateContext lst1 lst2 ctx = match lst1, lst2 with
| fs1 :: rest1, fs2 :: rest2 ->
match fs1, fs2 with
- | Some(c1), Some(c2) -> UpdateContext rest1 rest2 (AddConstr c1 c2 ctx)
- | _ -> UpdateContext rest1 rest2 ctx
+ | NoneConst,_ | _,NoneConst -> UpdateContext rest1 rest2 ctx
+ | _ -> UpdateContext rest1 rest2 (AddConstr fs1 fs2 ctx)
| [], [] -> ctx
| _ -> failwith "lists are not of the same length"
@@ -115,27 +118,27 @@ let UnboxIfNeeded (model: Microsoft.Boogie.Model) (e: Model.Element) = | None -> GetLoc e
let ReadHeap (model: Microsoft.Boogie.Model) prog =
- let f_heap_select = model.MkFunc("[3]", 3) - let values = f_heap_select.Apps - values |> Seq.fold (fun acc ft -> - assert (ft.Args.Length = 3) - let ref = ft.Args.[1] - let fld = ft.Args.[2] - assert (Seq.length fld.Names = 1) - let fldFullName = (Seq.nth 0 fld.Names).Func.Name - let dotIdx = fldFullName.LastIndexOf(".") - let fldName = fldFullName.Substring(dotIdx + 1) - let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx) - let refVal = ft.Result - let refObj = Unresolved(GetRefName ref) - let fldVarOpt = FindVar prog clsName fldName - match fldVarOpt with - | Some(fldVar) -> - let fldType = match fldVar with - | Var(_,t) -> t - let fldVal = ConvertValue model refVal - acc |> Map.add (refObj, fldVar) fldVal - | None -> acc + let f_heap_select = model.MkFunc("[3]", 3)
+ let values = f_heap_select.Apps
+ values |> Seq.fold (fun acc ft ->
+ assert (ft.Args.Length = 3)
+ let ref = ft.Args.[1]
+ let fld = ft.Args.[2]
+ assert (Seq.length fld.Names = 1)
+ let fldFullName = (Seq.nth 0 fld.Names).Func.Name
+ let dotIdx = fldFullName.LastIndexOf(".")
+ let fldName = fldFullName.Substring(dotIdx + 1)
+ let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx)
+ let refVal = ft.Result
+ let refObj = Unresolved(GetRefName ref)
+ let fldVarOpt = FindVar prog clsName fldName
+ match fldVarOpt with
+ | Some(fldVar) ->
+ let fldType = match fldVar with
+ | Var(_,t) -> t
+ let fldVal = ConvertValue model refVal
+ acc |> Map.add (refObj, fldVar) fldVal
+ | None -> acc
) Map.empty
let rec ReadArgValues (model: Microsoft.Boogie.Model) args =
@@ -157,7 +160,7 @@ let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple match len_tuples with
| ft :: rest ->
let len = GetInt ft.Result
- let emptyList = Utils.GenList len
+ let emptyList = Utils.GenList len NoneConst
let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList))
ReadSeqLen model rest (newMap,ctx)
| _ -> (envMap,ctx)
@@ -169,7 +172,7 @@ let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTupl let oldLst = GetSeqFromEnv envMap srcLstKey
let idx = GetInt ft.Args.[1]
let lstElem = UnboxIfNeeded model ft.Result
- let newLst = Utils.ListSet idx (Some(lstElem)) oldLst
+ let newLst = Utils.ListSet idx lstElem oldLst
let newCtx = UpdateContext oldLst newLst ctx
let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst))
ReadSeqIndex model rest (newEnv,newCtx)
@@ -184,7 +187,7 @@ let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTupl let idx = GetInt ft.Args.[1]
let lstElemVal = UnboxIfNeeded model ft.Args.[2]
let dstLst = GetSeqFromEnv envMap dstLstLoc
- let newLst = Utils.ListBuild oldLst idx (Some(lstElemVal)) dstLst
+ let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst
let newCtx = UpdateContext dstLst newLst ctx
let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
ReadSeqBuild model rest (newEnv,newCtx)
@@ -226,14 +229,14 @@ let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = let newEnv = envMap |> Map.add (GetLoc e) NullConst
(newEnv,ctx)
-let ReadEnv (model: Microsoft.Boogie.Model) =
- let f_dtype = model.MkFunc("dtype", 1) +let ReadEnv (model: Microsoft.Boogie.Model) prog =
+ let f_dtype = model.MkFunc("dtype", 1)
let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0]))
let envMap = f_dtype.Apps |> Seq.fold (fun acc ft ->
let locName = GetRefName ft.Args.[0]
let elemName = GetElemFullName ft.Args.[0]
let loc = Unresolved(locName)
- let locType = GetType ft.Result
+ let locType = GetType ft.Result prog
let value = match elemName with
| Some(n) when n.StartsWith("this") -> ThisConst(locName.Replace("*", ""), locType)
| _ -> NewObj(locName.Replace("*", ""), locType)
@@ -243,8 +246,8 @@ let ReadEnv (model: Microsoft.Boogie.Model) = |> ReadSeq model
|> ReadSet model
-let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth = - let heap = ReadHeap model prog - let env0,ctx = ReadEnv model - let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth)) +let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth =
+ let heap = ReadHeap model prog
+ let env0,ctx = ReadEnv model prog
+ let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth))
heap,env,ctx
\ No newline at end of file diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs index 87937850..fb9f3bf7 100644 --- a/Jennisys/Jennisys/DafnyPrinter.fs +++ b/Jennisys/Jennisys/DafnyPrinter.fs @@ -5,12 +5,12 @@ open Printer let rec PrintType ty = match ty with - | IntType -> "int" - | BoolType -> "bool" - | NamedType(id) -> id - | SeqType(t) -> sprintf "seq<%s>" (PrintType t) - | SetType(t) -> sprintf "set<%s>" (PrintType t) - | InstantiatedType(id,arg) -> sprintf "%s<%s>" id (PrintType arg) + | IntType -> "int" + | BoolType -> "bool" + | SeqType(t) -> sprintf "seq<%s>" (PrintType t) + | SetType(t) -> sprintf "set<%s>" (PrintType t) + | NamedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args) + | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args) let rec PrintExpr ctx expr = match expr with diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs index 0337c6a2..32827f39 100644 --- a/Jennisys/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys/Jennisys.fs @@ -38,18 +38,20 @@ let readAndProcess tracing analyzing (filename: string) = | Some(prog) -> if analyzing then // output a Dafny program with the constraints to be solved - Analyze prog + Analyze prog filename else () // that's it if tracing then printfn "----------" else () with - | ex -> - let pos = lexbuf.EndPos - printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + | ex -> + let pos = lexbuf.EndPos + printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + printfn "%s" (ex.StackTrace.ToString()) with | ex -> printfn "Unhandled Exception: %s" ex.Message + printfn "%s" (ex.StackTrace.ToString()) let rec start n (args: string []) tracing analyzing filename = if n < args.Length then diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index 39ed1aed..bbb15dc4 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ <WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List3.jen</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List.jen</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
@@ -83,17 +83,21 @@ <Reference Include="System.Numerics" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\..\Source\ModelViewer\ModelViewer.csproj">
- <Name>ModelViewer</Name>
- <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>
+ <ProjectReference Include="..\..\Source\Model\Model.csproj">
+ <Name>Model</Name>
+ <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
<Private>True</Private>
</ProjectReference>
+ </ItemGroup>
+ <!--
+ <ItemGroup>
<ProjectReference Include="..\..\Source\Model\Model.csproj">
<Name>Model</Name>
<Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
<Private>True</Private>
</ProjectReference>
</ItemGroup>
+ -->
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
<Target Name="BeforeBuild">
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index 21e2c83e..5053bd18 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -6,7 +6,7 @@ open AstUtils let rec MyFold ee acc =
match ee with
| [] -> acc
- | x::rest -> BinaryAnd (Desugar x) (MyFold rest acc)
+ | x::rest -> BinaryAnd x (MyFold rest acc)
%}
@@ -89,9 +89,9 @@ BlockStmt: Member:
| VAR VarDecl { Field($2) }
- | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, (Desugar $4), (Desugar $5), true) }
- | METHOD ID Signature Pre Post { Method($2, $3, (Desugar $4), (Desugar $5), false) }
- | INVARIANT ExprList { Invariant(DesugarLst $2) }
+ | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, $4, $5, true) }
+ | METHOD ID Signature Pre Post { Method($2, $3, $4, $5, false) }
+ | INVARIANT ExprList { Invariant($2) }
FrameMembers:
| { [], [], IdLiteral("true") }
@@ -116,10 +116,10 @@ VarDecl: Type:
| INTTYPE { IntType }
| BOOLTYPE { BoolType }
- | ID { NamedType($1) }
+ | ID { NamedType($1, []) }
| SEQTYPE LBRACKET Type RBRACKET { SeqType($3) }
| SETTYPE LBRACKET Type RBRACKET { SetType($3) }
- | ID LBRACKET Type RBRACKET { InstantiatedType($1, $3) }
+ | ID LBRACKET Type RBRACKET { InstantiatedType($1, [$3]) }
ExprList:
| { [] }
diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs index 686452b6..c17ebfa7 100644 --- a/Jennisys/Jennisys/PipelineUtils.fs +++ b/Jennisys/Jennisys/PipelineUtils.fs @@ -4,51 +4,52 @@ /// author: Aleksandar Milicevic (t-alekm@microsoft.com)
module PipelineUtils
- -let dafnyScratchSuffix = "scratch" -let dafnyVerifySuffix = "verify" -let dafnyUnifSuffix = "unif" -let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy" - -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 dafnyScratchSuffix = "scratch"
+let dafnyVerifySuffix = "verify"
+let dafnyUnifSuffix = "unif"
+let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy"
+
+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 =
CreateEmptyModelFile modelFile
async {
use proc = new System.Diagnostics.Process()
proc.StartInfo.FileName <- @"c:\tmp\StartDafny-jen.bat"
proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile
+ proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden
assert proc.Start()
proc.WaitForExit()
} |> 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 = - // 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 +// =======================================================
+/// 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 =
+ // 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
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index eb70acbd..e4f6e0a0 100644 --- a/Jennisys/Jennisys/Printer.fs +++ b/Jennisys/Jennisys/Printer.fs @@ -16,12 +16,12 @@ let rec PrintSep sep f list = let rec PrintType ty = match ty with - | IntType -> "int" - | BoolType -> "bool" - | NamedType(id) -> id - | SeqType(t) -> sprintf "seq[%s]" (PrintType t) - | SetType(t) -> sprintf "set[%s]" (PrintType t) - | InstantiatedType(id,arg) -> sprintf "%s[%s]" id (PrintType arg) + | IntType -> "int" + | BoolType -> "bool" + | NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args) + | SeqType(t) -> sprintf "seq[%s]" (PrintType t) + | SetType(t) -> sprintf "set[%s]" (PrintType t) + | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args) let PrintVarDecl vd = match vd with @@ -121,14 +121,13 @@ let rec PrintConst cst = | BoolConst(b) -> sprintf "%b" b | SetConst(cset) -> cset.ToString() //TODO: this won't work | SeqConst(cseq) -> - let seqCont = cseq |> List.fold (fun acc cOpt -> + let seqCont = cseq |> List.fold (fun acc c -> let sep = if acc = "" then "" else ", " - match cOpt with - | Some(c) -> acc + sep + (PrintConst c) - | None -> acc + sep + "null" + acc + sep + (PrintConst c) ) "" sprintf "[%s]" seqCont | NullConst -> "null" + | NoneConst -> "<none>" | ThisConst(_,_) -> "this" | NewObj(name,_) -> PrintGenSym name | ExprConst(e) -> PrintExpr 0 e diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs index f1a1f67f..c6bb1991 100644 --- a/Jennisys/Jennisys/Resolver.fs +++ b/Jennisys/Jennisys/Resolver.fs @@ -5,14 +5,15 @@ open Printer open EnvUtils
// resolving values
+exception ConstResolveFailed of string
-let rec Resolve cst (env,ctx) =
+let rec ResolveCont cst (env,ctx) failResolver =
match cst with
| Unresolved(_) as u ->
// see if it is in the env map first
let envVal = Map.tryFind cst env
match envVal with
- | Some(c) -> Resolve c (env,ctx)
+ | Some(c) -> ResolveCont c (env,ctx) failResolver
| None ->
// not found in the env map --> check the equality sets
let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
@@ -23,24 +24,24 @@ let rec Resolve cst (env,ctx) = |> Utils.SetToOption
match cOpt with
| Some(c) -> c
- | _ -> failwith ("failed to resolve " + cst.ToString())
- | _ -> failwith ("failed to resolve " + cst.ToString())
+ | _ -> failResolver cst (env,ctx)
+ | _ -> failResolver cst (env,ctx)
| SeqConst(cseq) ->
- let resolvedLst = cseq |> List.rev |> List.fold (fun acc cOpt ->
- match cOpt with
- | Some(c) -> Some(Resolve c (env,ctx)) :: acc
- | None -> cOpt :: acc
- ) []
+ let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont c (env,ctx) failResolver :: acc) []
SeqConst(resolvedLst)
| SetConst(cset) ->
- let resolvedSet = cset |> Set.fold (fun acc cOpt ->
- match cOpt with
- | Some(c) -> acc |> Set.add (Some(Resolve c (env,ctx)))
- | None -> acc |> Set.add(cOpt)
- ) Set.empty
+ let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont c (env,ctx) failResolver)) Set.empty
SetConst(resolvedSet)
| _ -> cst
+let TryResolve cst (env,ctx) =
+ ResolveCont cst (env,ctx) (fun c (e,x) -> c)
+
+let Resolve cst (env,ctx) =
+ ResolveCont cst (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString())))
+
+
+
let rec EvalUnresolved expr (heap,env,ctx) =
match expr with | IntLiteral(n) -> IntConst(n) @@ -57,7 +58,7 @@ let rec EvalUnresolved expr (heap,env,ctx) = let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) let idxC = EvalUnresolved idx (heap,env,ctx) match lstC, idxC with - | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | SeqConst(clist), IntConst(n) -> clist.[n] | _ -> failwith "can't eval SelectExpr" | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! // | Star @@ -73,6 +74,6 @@ let rec EvalUnresolved expr (heap,env,ctx) = let Eval expr (heap,env,ctx) =
try
let unresolvedConst = EvalUnresolved expr (heap,env,ctx)
- Some(Resolve unresolvedConst (env,ctx))
+ Some(TryResolve unresolvedConst (env,ctx))
with
ex -> None
\ No newline at end of file diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs index 7414f253..377082d9 100644 --- a/Jennisys/Jennisys/TypeChecker.fs +++ b/Jennisys/Jennisys/TypeChecker.fs @@ -6,34 +6,34 @@ open System.Collections.Generic let GetClass name decls =
match decls |> List.tryFind (function Class(n,_,_) when n = name -> true | _ -> false) with
- | Some(cl) -> cl
- | None -> Class(name,[],[])
+ | Some(cl) -> cl
+ | None -> Class(name,[],[])
let GetModel name decls =
match decls |> List.tryFind (function Model(n,_,_,_,_) when n = name -> true | _ -> false) with
- | Some(m) -> m
- | None -> Model(name,[],[],[],IdLiteral("true"))
+ | Some(m) -> m
+ | None -> Model(name,[],[],[],IdLiteral("true"))
let GetCode name decls =
match decls |> List.tryFind (function Code(n,_) when n = name -> true | _ -> false) with
- | Some(c) -> c
- | None -> Code(name,[])
+ | Some(c) -> c
+ | None -> Code(name,[])
let IsUserType prog tpo =
match tpo with
- | Some(tp) ->
- let tpname = match tp with
- | NamedType(tname) -> tname
- | InstantiatedType(tname, _) -> tname
- | _ -> ""
- match prog with
- | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true
- | _ -> false) |> List.isEmpty |> not
- | None -> false
+ | Some(tp) ->
+ let tpname = match tp with
+ | NamedType(tname,_) -> tname
+ | InstantiatedType(tname, _) -> tname
+ | _ -> ""
+ match prog with
+ | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true
+ | _ -> false) |> List.isEmpty |> not
+ | None -> false
let TypeCheck prog =
match prog with
- | SProgram(decls) ->
+ | SProgram(decls) ->
let componentNames = decls |> List.choose (function Class(name,_,_) -> Some(name) | _ -> None)
let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))
Some(Program(clist))
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs index 3cb8fee4..6540173c 100644 --- a/Jennisys/Jennisys/Utils.fs +++ b/Jennisys/Jennisys/Utils.fs @@ -77,17 +77,17 @@ let SetToOption set = else
Some(set |> Set.toList |> List.head)
-// ===============================================================
+// ============================================================
/// requires: n >= 0
-/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = None
-// ===============================================================
-let rec GenList n =
+/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = e
+// ============================================================
+let rec GenList n e =
if n < 0 then
failwith "n must be positive"
if n = 0 then
[]
else
- None :: (GenList (n-1))
+ e :: (GenList (n-1) e)
// ==========================
/// ensures: ret = elem in lst
@@ -171,3 +171,19 @@ let (|Exact|_|) (p:string) (s:string) = else
None
+// -------------------------------------------
+// ----------------- random ------------------
+// -------------------------------------------
+
+let IfDo1 cond func1 a =
+ if cond then
+ func1 a
+ else
+ a
+
+let IfDo2 cond func2 (a1,a2) =
+ if cond then
+ func2 a1 a2
+ else
+ a1,a2
+
diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen index 184f4947..e7f42ddc 100644 --- a/Jennisys/Jennisys/examples/List.jen +++ b/Jennisys/Jennisys/examples/List.jen @@ -6,6 +6,9 @@ class List[T] { constructor Singleton(t: T) ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] } model List[T] { @@ -27,6 +30,9 @@ class Node[T] { constructor Init(t: T) ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] } model Node[T] { diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen index 6bb49eb8..acb10ad5 100644 --- a/Jennisys/Jennisys/examples/List3.jen +++ b/Jennisys/Jennisys/examples/List3.jen @@ -33,7 +33,7 @@ model IntList { root = null ==> |list| = 0 root != null ==> (|list| = |root.succ| + 1 && list[0] = root.data && - (forall i:int :: (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-1] != null && list[i] = root.succ[i-1].data))) } class IntNode { |