summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Jennisys.sln56
-rw-r--r--Jennisys/Analyzer.fs83
-rw-r--r--Jennisys/Ast.fs17
-rw-r--r--Jennisys/AstUtils.fs40
-rw-r--r--Jennisys/DafnyModelUtils.fs192
-rw-r--r--Jennisys/DafnyPrinter.fs13
-rw-r--r--Jennisys/Jennisys.fs5
-rw-r--r--Jennisys/Jennisys.fsproj17
-rw-r--r--Jennisys/Lexer.fsl5
-rw-r--r--Jennisys/Parser.fsy13
-rw-r--r--Jennisys/PipelineUtils.fs14
-rw-r--r--Jennisys/Printer.fs17
-rw-r--r--Jennisys/TypeChecker.fs1
-rw-r--r--Jennisys/Utils.fs71
-rw-r--r--Jennisys/examples/List.jen10
15 files changed, 501 insertions, 53 deletions
diff --git a/Jennisys.sln b/Jennisys.sln
index 77ebb8e2..bb45d27c 100644
--- a/Jennisys.sln
+++ b/Jennisys.sln
@@ -2,17 +2,73 @@
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
+ Checked|Mixed Platforms = Checked|Mixed Platforms
+ Checked|x86 = Checked|x86
+ Debug|Any CPU = Debug|Any CPU
+ Debug|Mixed Platforms = Debug|Mixed Platforms
Debug|x86 = Debug|x86
+ Release|Any CPU = Release|Any CPU
+ Release|Mixed Platforms = Release|Mixed Platforms
Release|x86 = Release|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Any CPU.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Mixed Platforms.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Mixed Platforms.Build.0 = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|x86.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|x86.Build.0 = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Any CPU.ActiveCfg = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Mixed Platforms.Build.0 = Debug|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|x86.ActiveCfg = Debug|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|x86.Build.0 = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Any CPU.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Mixed Platforms.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Mixed Platforms.Build.0 = Release|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|x86.ActiveCfg = Release|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|x86.Build.0 = Release|x86
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.Build.0 = Release|Any CPU
+ {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/Analyzer.fs b/Jennisys/Analyzer.fs
index 806a6ab5..9a57ae64 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -2,25 +2,18 @@
open Ast
open AstUtils
+open DafnyModelUtils
+open PipelineUtils
open Printer
open DafnyPrinter
open TypeChecker
+open Microsoft.Boogie
+
let VarsAreDifferent aa bb =
printf "false"
List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb
-let Fields members =
- members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
-
-let Methods prog =
- match prog with
- | Program(components) ->
- components |> List.fold (fun acc comp ->
- match comp with
- | Component(Class(_,_,members), Model(_,_,_,_,_), _) -> List.concat [acc ; members]
- | _ -> acc) []
-
let Rename suffix vars =
vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
@@ -79,18 +72,31 @@ let GenValidFunctionCode clsMembers modelInv vars prog : string =
let allInvs = modelInv :: clsInvs
let fieldsValid = GetFieldsValidExprList vars prog
let idt = " "
- let invsStr = List.concat [fieldsValid ; allInvs] |> List.fold (fun acc (e: Expr) ->
- if acc = "" then
- sprintf "%s%s" idt (PrintExpr 0 e)
- else
- acc + " &&" + newline + sprintf "%s%s" idt (PrintExpr 0 e)) ""
+ let invsStr = List.concat [allInvs ; fieldsValid] |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
+ |> List.fold (fun acc (e: Expr) ->
+ if acc = "" then
+ sprintf "%s(%s)" idt (PrintExpr 0 e)
+ else
+ acc + " &&" + newline + sprintf "%s(%s)" idt (PrintExpr 0 e)) ""
+ // 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
+ []
" function Valid(): bool" + newline +
" reads *;" + newline +
+ (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
" {" + newline +
invsStr + newline +
" }" + newline
-let AnalyzeMethod prog mthd : string =
+let GetAnalyzeConstrCode mthd =
+ match mthd with
+ | Constructor(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post false) + newline
+ | Method(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post true) + newline
+ | _ -> ""
+
+let AnalyzeMethod prog mthd mthdCodeFunc: string =
match prog with
| Program(components) -> components |> List.fold (fun acc comp ->
match comp with
@@ -101,35 +107,52 @@ let AnalyzeMethod prog mthd : string =
acc +
(sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +
// the fields: original abstract fields plus concrete fields
- (sprintf "%s" (PrintFields allVars 2)) + newline +
+ (sprintf "%s" (PrintFields aVars 2 true)) + newline +
+ (sprintf "%s" (PrintFields cVars 2 false)) + newline +
// generate the Valid function
(sprintf "%s" (GenValidFunctionCode members inv allVars prog)) + newline +
// generate code for the given method
(if List.exists (fun a -> a = mthd) members then
- match mthd with
- | Constructor(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post false) + newline
- | Method(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post true) + newline
- | _ -> ""
+ mthdCodeFunc mthd
else
"") +
// the end of the class
"}" + newline + newline
| _ -> assert false; "") ""
-let scratchFileName = "scratch.dfy"
+let PrintImplCode (heap, env, ctx) =
+
+ ()
let Analyze prog =
- let methods = Methods prog
-
+ let models = ref null
+ let methods = Methods prog
// synthesize constructors
- methods |> List.iter (fun m ->
+ methods |> List.iter (fun (comp, m) ->
match m with
| Constructor(methodName,signature,pre,post) ->
- use file = System.IO.File.CreateText(scratchFileName)
- let code = AnalyzeMethod prog m
- printfn "printing code for method %s:\r\n%s" methodName code
- printfn "-------------------------"
+ use file = System.IO.File.CreateText(dafnyScratchFile)
+ file.AutoFlush <- true
+ let code = AnalyzeMethod prog m GetAnalyzeConstrCode
+ printfn "analyzing constructor %s" methodName
+// printfn "%s" code
+// printfn "-------------------------"
fprintf file "%s" code
+ file.Close()
+ RunDafny dafnyScratchFile dafnyModelFile
+ 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
+ else
+ assert (models.Count = 1) // TODO
+ let model = models.[0]
+
+ let (heap,env,ctx) = ReadFieldValuesFromModel model prog comp m
+ PrintImplCode (heap, env, ctx) |> ignore
+ printfn "done with %s" methodName
+ System.Environment.Exit(1)
| _ -> ())
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index b6e04d3f..eeb2f753 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -3,10 +3,22 @@
open System
open System.Numerics
-
type Type =
+ | IntType
+ | BoolType
+ | SetType of Type (* type parameter *)
+ | SeqType of Type (* type parameter *)
| NamedType of string
- | InstantiatedType of string * Type
+ | InstantiatedType of string * Type (* type parameter *)
+
+type Const =
+ | IntConst of int
+ | BoolConst of bool
+ | SetConst of Set<Const>
+ | SeqConst of (Const option) list
+ | ThisConst of (* loc id *) string * Type option
+ | NewObj of (* loc id *) string * Type option
+ | Unresolved of (* loc id *) string
type VarDecl =
| Var of string * Type option
@@ -50,3 +62,4 @@ type Component =
type Program =
| Program of Component list
+
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 83104f5d..794a89dc 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -23,4 +23,42 @@ let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)
let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
let TrueLiteral = IdLiteral("true")
-let FalseLiteral = IdLiteral("false") \ No newline at end of file
+let FalseLiteral = IdLiteral("false")
+
+// --- search functions ---
+
+let Fields members =
+ members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
+
+let Methods prog =
+ match prog with
+ | Program(components) ->
+ components |> List.fold (fun acc comp ->
+ match comp with
+ | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> List.choose (fun m -> Some(comp, m))]
+ | _ -> acc) []
+
+let AllFields c =
+ match c with
+ | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
+ let aVars = Fields members
+ List.concat [aVars ; cVars]
+ | _ -> []
+
+let GetClassName comp =
+ match comp with
+ | Component(Class(name,_,_),_,_) -> name
+ | _ -> failwith ("unrecognized component: " + comp.ToString())
+
+let FindComponent (prog: Program) clsName =
+ match prog with
+ | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)
+ |> Utils.ListToOption
+
+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
+ | None -> None \ No newline at end of file
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
new file mode 100644
index 00000000..c3db8e83
--- /dev/null
+++ b/Jennisys/DafnyModelUtils.fs
@@ -0,0 +1,192 @@
+module DafnyModelUtils
+
+(*
+ The heap maps objects and fields to locations.
+ heap: Const * VarDecl option |--> Const
+
+ The environment maps locations to values (except that it can also
+ be locations to locations, because not all values are explicitly
+ present in the model.
+ envMap: Const |--> Const
+
+ The context is just a list of equality constraints collected on the way
+ ctx: Set<Set<Const>>, where the inner set contains exactly two constants
+*)
+
+open Ast
+open AstUtils
+open Utils
+
+open Microsoft.Boogie
+
+let GetElemFullName (elem: Model.Element) =
+ 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 clsName = if dotIdx = -1 then "" else fullName.Substring(0, dotIdx)
+ Some(clsName, fldName)
+ | None -> None
+
+let GetRefName (ref: Model.Element) =
+ match ref with
+ | :? Model.Uninterpreted as uref -> uref.Name
+ | _ -> failwith ("not a ref (Uninterpreted) but: " + ref.GetType().Name)
+
+let ConvertValue (model: Model) (refVal: Model.Element) =
+ match refVal with
+ | :? Model.Number as ival -> IntConst(ival.AsInt())
+ | :? Model.Boolean as bval -> BoolConst(bval.Value)
+ | :? Model.Array as aval -> failwith "reading array values from model not implemented"
+ | :? Model.Uninterpreted as uval -> Unresolved(uval.Name) (* just a symbolic name for now, which we'll hopefully resolve later*)
+ | _ -> failwith ("unexpected model element kind: " + refVal.ToString())
+
+let GetInt (elem: Model.Element) =
+ match elem with
+ | :? Model.Number as ival -> ival.AsInt()
+ | _ -> failwith ("not an int element: " + elem.ToString())
+
+let GetBool (elem: Model.Element) =
+ match elem with
+ | :? Model.Boolean as bval -> bval.Value
+ | _ -> failwith ("not a bool element: " + elem.ToString())
+
+let GetType (e: Model.Element) =
+ let fNameOpt = GetElemFullName e
+ match fNameOpt with
+ | Some(fname) -> match fname with
+ | Exact "intType" _ -> Some(IntType)
+ | Prefix "class." clsName -> Some(NamedType(clsName))
+ | _ -> None
+ | None -> None
+
+let GetLoc (e: Model.Element) =
+ Unresolved(GetRefName e)
+
+let GetSeqFromEnv env key =
+ match Map.find key env with
+ | SeqConst(lst) -> lst
+ | _ as x-> failwith ("not a SeqConst but: " + x.ToString())
+
+let AddConstr c1 c2 ctx =
+ if c1 = c2 then
+ ctx
+ else
+ match c1, c2 with
+ | Unresolved(_), _ | _, Unresolved(_) -> Set.add (Set.ofList [c1; c2]) ctx
+ | _ -> failwith ("trying to add an equality constraint between two constants: " + c1.ToString() + ", and " + c2.ToString())
+
+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
+ | [], [] -> ctx
+ | _ -> failwith "lists are not of the same length"
+
+let UnboxIfNeeded (model: Microsoft.Boogie.Model) (e: Model.Element) =
+ let f_unbox = model.MkFunc("$Unbox", 2)
+ let unboxed = f_unbox.Apps |> Seq.filter (fun ft -> if (GetLoc ft.Args.[1]) = (GetLoc e) then true else false)
+ |> Seq.choose (fun ft -> Some(ft.Result))
+ |> Utils.SeqToOption
+ match unboxed with
+ | Some(e) -> ConvertValue model e
+ | 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 fldVar = FindVar prog clsName fldName
+ let fldType = match fldVar with
+ | Some(Var(_,t)) -> t
+ | _ -> None
+ let fldVal = ConvertValue model refVal
+ acc |> Map.add (refObj, fldVar) fldVal
+ ) Map.empty
+
+let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match len_tuples with
+ | ft :: rest ->
+ let len = GetInt ft.Result
+ let emptyList = Utils.GenList len
+ let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList))
+ ReadSeqLen model rest (newMap,ctx)
+ | _ -> (envMap,ctx)
+
+let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match idx_tuples with
+ | ft :: rest ->
+ let srcLstKey = GetLoc ft.Args.[0]
+ 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 newCtx = UpdateContext oldLst newLst ctx
+ let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst))
+ ReadSeqIndex model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match bld_tuples with
+ | ft :: rest ->
+ let srcLstKey = GetLoc ft.Args.[0]
+ let dstLstKey = GetLoc ft.Result
+ let oldLst = GetSeqFromEnv envMap srcLstKey
+ let idx = GetInt ft.Args.[1]
+ let lstElemVal = UnboxIfNeeded model ft.Args.[2]
+ let dstLst = GetSeqFromEnv envMap dstLstKey
+ let newLst = Utils.ListBuild oldLst idx (Some(lstElemVal)) dstLst
+ let newCtx = UpdateContext dstLst newLst ctx
+ let newEnv = envMap |> Map.add dstLstKey (SeqConst(newLst))
+ ReadSeqBuild model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
+ let f_seq_len = model.MkFunc("Seq#Length", 1)
+ let f_seq_bld = model.MkFunc("Seq#Build", 4)
+ let f_seq_idx = model.MkFunc("Seq#Index", 2)
+ (envMap,ctx) |> ReadSeqLen model (List.ofSeq f_seq_len.Apps)
+ |> ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)
+ |> ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
+
+let ReadSet (model: Microsoft.Boogie.Model) envMap =
+ envMap
+
+let ReadEnv (model: Microsoft.Boogie.Model) =
+ 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 value = match elemName with
+ | Some(n) when n.StartsWith("this") -> ThisConst(locName, locType)
+ | _ -> NewObj(locName, locType)
+ acc |> Map.add loc value
+ ) Map.empty
+ (envMap, Set.ofList([])) |> ReadSeq model
+ |> ReadSet model
+
+let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth =
+ let heap = ReadHeap model prog
+ let env,ctx = ReadEnv model
+ heap,env,ctx \ No newline at end of file
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index d5fa6086..87937850 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -5,7 +5,11 @@ open Printer
let rec PrintType ty =
match ty with
- | NamedType(id) -> id
+ | 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)
let rec PrintExpr ctx expr =
@@ -41,7 +45,8 @@ let PrintTypeParams typeParams =
| [] -> ""
| _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
-let PrintFields vars indent =
+let PrintFields vars indent ghost =
+ let ghostStr = if ghost then "ghost " else ""
vars |> List.fold (fun acc v -> match v with
- | Var(nm,None) -> acc + (sprintf "%svar %s;%s" (Indent indent) nm newline)
- | Var(nm,Some(tp)) -> acc + (sprintf "%svar %s: %s;%s" (Indent indent) nm (PrintType tp) newline)) "" \ No newline at end of file
+ | Var(nm,None) -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)
+ | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) "" \ No newline at end of file
diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs
index d58af665..0c69f797 100644
--- a/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys.fs
@@ -61,4 +61,7 @@ let rec start n (args: string []) tracing analyzing filename =
readAndProcess tracing analyzing filename
let args = Environment.GetCommandLineArgs()
-start 1 args false true null
+try
+ start 1 args false true null
+with
+| _ as e -> printfn "%s" e.StackTrace \ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 68369571..1ec66a98 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/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\List.jen</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List2.jen</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
@@ -42,6 +42,8 @@
<FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
</PropertyGroup>
<ItemGroup>
+ <Compile Include="Utils.fs" />
+ <Compile Include="PipelineUtils.fs" />
<Compile Include="Ast.fs" />
<Compile Include="AstUtils.fs" />
<Compile Include="$(IntermediateOutputPath)\Parser.fs">
@@ -52,6 +54,7 @@
<Visible>false</Visible>
<Link>Lexer.fs</Link>
</Compile>
+ <Compile Include="DafnyModelUtils.fs" />
<FsYacc Include="Parser.fsy">
<OtherFlags>--module Parser</OtherFlags>
</FsYacc>
@@ -74,6 +77,18 @@
<Reference Include="System.Core" />
<Reference Include="System.Numerics" />
</ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\Source\ModelViewer\ModelViewer.csproj">
+ <Name>ModelViewer</Name>
+ <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>
+ <Private>True</Private>
+ </ProjectReference>
+ <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/Lexer.fsl b/Jennisys/Lexer.fsl
index 26195484..a0e62109 100644
--- a/Jennisys/Lexer.fsl
+++ b/Jennisys/Lexer.fsl
@@ -32,6 +32,11 @@ rule tokenize = parse
| "requires" { REQUIRES }
| "ensures" { ENSURES }
| "forall" { FORALL }
+// Types
+| "int" { INTTYPE }
+| "bool" { BOOLTYPE }
+| "seq" { SEQTYPE }
+| "set" { SETTYPE }
// Operators
| "." { DOT }
| "+" { PLUS }
diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 0b5c2fc8..71ca4de0 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -29,6 +29,7 @@ let rec MyFold ee acc =
%token GETS COLON COLONCOLON COMMA
%token CLASS MODEL CODE
%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL
+%token INTTYPE BOOLTYPE SEQTYPE SETTYPE
%token EOF
// This is the type of the data produced by a successful reduction of the 'start'
@@ -89,8 +90,8 @@ BlockStmt:
Member:
| VAR VarDecl { Field($2) }
| CONSTRUCTOR ID Signature Pre Post { Constructor($2, $3, $4, $5) }
- | METHOD ID Signature Pre Post { Method($2, $3, $4, $5) }
- | INVARIANT ExprList { Invariant($2) }
+ | METHOD ID Signature Pre Post { Method($2, $3, $4, $5) }
+ | INVARIANT ExprList { Invariant($2) }
FrameMembers:
| { [], [], IdLiteral("true") }
@@ -113,8 +114,12 @@ VarDecl:
| ID COLON Type { Var($1,Some($3)) }
Type:
- | ID { NamedType($1) }
- | ID LBRACKET Type RBRACKET { InstantiatedType($1, $3) }
+ | INTTYPE { IntType }
+ | BOOLTYPE { BoolType }
+ | ID { NamedType($1) }
+ | SEQTYPE LBRACKET Type RBRACKET { SeqType($3) }
+ | SETTYPE LBRACKET Type RBRACKET { SetType($3) }
+ | ID LBRACKET Type RBRACKET { InstantiatedType($1, $3) }
ExprList:
| { [] }
diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs
new file mode 100644
index 00000000..0f7eb847
--- /dev/null
+++ b/Jennisys/PipelineUtils.fs
@@ -0,0 +1,14 @@
+module PipelineUtils
+
+let dafnyScratchFile = @"c:\tmp\jennisys-scratch.dfy"
+let dafnyModelFile = @"c:\tmp\jennisys-scratch.model"
+let dafnyOutFile = @"c:\tmp\jennisys-scratch.out"
+
+let RunDafny inputFile modelFile =
+ async {
+ use proc = new System.Diagnostics.Process()
+ proc.StartInfo.FileName <- @"c:\tmp\StartDafny-jen.bat"
+ proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile
+ assert proc.Start()
+ proc.WaitForExit()
+ } |> Async.RunSynchronously
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index 77e462f3..2c6315a3 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -12,7 +12,11 @@ let rec PrintSep sep f list =
let rec PrintType ty =
match ty with
- | NamedType(id) -> id
+ | 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)
let PrintVarDecl vd =
@@ -50,11 +54,14 @@ let PrintSig signature =
else ""
sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
-let rec ForeachConjunct f expr =
+let rec SplitIntoConjunts expr =
match expr with
- | IdLiteral("true") -> ""
- | BinaryExpr(_,"&&",e0,e1) -> (ForeachConjunct f e0) + (ForeachConjunct f e1)
- | _ -> f expr
+ | 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/TypeChecker.fs b/Jennisys/TypeChecker.fs
index 41ffbb5d..6ca13453 100644
--- a/Jennisys/TypeChecker.fs
+++ b/Jennisys/TypeChecker.fs
@@ -24,6 +24,7 @@ let IsUserType prog tpo =
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
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
new file mode 100644
index 00000000..8a2e107e
--- /dev/null
+++ b/Jennisys/Utils.fs
@@ -0,0 +1,71 @@
+module Utils
+
+// -------------------------------------------
+// ----------- collection util funcs ---------
+// -------------------------------------------
+
+let ListToOption lst =
+ assert (List.length lst <= 1)
+ if List.isEmpty lst then
+ None
+ else
+ Some(lst.[0])
+
+let SeqToOption seq =
+ assert (Seq.length seq <= 1)
+ if Seq.isEmpty seq then
+ None
+ else
+ Some(Seq.nth 0 seq)
+
+let rec GenList n =
+ if n = 0 then
+ []
+ else
+ None :: (GenList (n-1))
+
+let rec ListSkip cnt lst =
+ if cnt = 0 then
+ lst
+ else
+ match lst with
+ | fs :: rest -> ListSkip (cnt-1) rest
+ | [] -> []
+
+let rec ListBuild srcList idx v dstList =
+ match srcList, dstList with
+ | fs1 :: rest1, fs2 :: rest2 -> if idx = 0 then
+ v :: List.concat [rest1 ; ListSkip (List.length rest1) rest2]
+ else
+ fs1 :: ListBuild rest1 (idx-1) v rest2
+ | [], fs2 :: rest2 -> if idx = 0 then
+ v :: rest2
+ else
+ fs2 :: ListBuild [] (idx-1) v rest2
+ | _, [] -> failwith "index out of range"
+
+
+let rec ListSet idx v lst =
+ match lst with
+ | fs :: rest -> if idx = 0 then
+ v :: rest
+ else
+ fs :: ListSet (idx-1) v rest
+ | [] -> failwith "index out of range"
+
+// -------------------------------------------
+// ------ string active patterns -------------
+// -------------------------------------------
+
+let (|Prefix|_|) (p:string) (s:string) =
+ if s.StartsWith(p) then
+ Some(s.Substring(p.Length))
+ else
+ None
+
+let (|Exact|_|) (p:string) (s:string) =
+ if s = p then
+ Some(s)
+ else
+ None
+
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index 89716f8b..184f4947 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -1,10 +1,10 @@
class List[T] {
var list: seq[T]
- constructor Init()
+ constructor Empty()
ensures list = []
- constructor Singleton(t)
+ constructor Singleton(t: T)
ensures list = [t]
}
@@ -25,7 +25,7 @@ class Node[T] {
invariant
|list| > 0
- constructor Init(t)
+ constructor Init(t: T)
ensures list = [t]
}
@@ -37,6 +37,6 @@ model Node[T] {
data * next
invariant
- next = null ==> list = [data]
- next != null ==> list = [data] + next.list
+ next = null <==> list = [data]
+ next != null ==> list = [data] + next.list
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-18 04:28:37 +0000