summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Jennisys/AstUtils.fs10
-rw-r--r--Jennisys/DafnyModelUtils.fs88
-rw-r--r--Jennisys/Jennisys.fsproj2
-rw-r--r--Jennisys/README.txt24
-rw-r--r--Jennisys/examples/BHeap.jen33
5 files changed, 121 insertions, 36 deletions
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 11189ebb..6aac59e2 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -290,11 +290,17 @@ let rec DescendExpr2BU visitorFunc expr acc =
| SequenceExpr(exs)
| SetExpr(exs) -> __Pipe exs
+//TODO: if names in dafny models contain funky characters,
+// these gensym variables might not be valid identifiers
let PrintGenSym (name: string) =
if name.StartsWith("gensym") then
name
- else
- sprintf "gensym%s" name
+ else
+ let idx = name.LastIndexOf("!")
+ if idx <> -1 then
+ sprintf "gensym%s" (name.Substring(idx+1))
+ else
+ sprintf "gensym%s" name
// =====================
/// Returns TRUE literal
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index 50d5f2c5..e734f3bb 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -26,6 +26,21 @@ open Utils
open Microsoft.Boogie
+let HEAP_SELECT_FNAME = "MapType1Select"
+let SEQ_BUILD_FNAME = "Seq#Build"
+let SEQ_APPEND_FNAME = "Seq#Append"
+let SEQ_LENGTH_FNAME = "Seq#Length"
+let SEQ_INDEX_FNAME = "Seq#Index"
+let SET_EMPTY_FNAME = "Set#Empty"
+let SET_SELECT_FNAME = "MapType0Select"
+let UNBOX_FNAME = "$Unbox"
+let BOOL_2_U_FNAME = "bool_2_U"
+let U_2_BOOL_FNAME = "U_2_bool"
+let INT_2_U_FNAME = "int_2_U"
+let U_2_INT_FNAME = "U_2_int"
+let DTYPE_FNAME = "dtype"
+let NULL_FNAME = "null"
+
type HeapModel = {
heap : Map<Const * VarDecl, Const>;
env : Map<Const, Const>;
@@ -44,25 +59,46 @@ 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) =
+
+let GetInt (elem: Model.Element) =
+ let __NotIntFail e = failwith ("not an int element: " + elem.ToString())
+ let rec __GetIntStrict (e: Model.Element) cont =
+ match e with
+ | :? Model.Number as ival -> ival.AsInt()
+ | _ -> cont e
+ __GetIntStrict elem (fun e ->
+ let f = e.Model.MkFunc(U_2_INT_FNAME, 1)
+ let matches = f.Apps |> Seq.filter (fun ft -> ft.Args.[0] = e) |> Seq.map (fun ft -> ft.Result)
+ if matches |> Seq.isEmpty then
+ __NotIntFail e
+ else
+ __GetIntStrict (matches |> Seq.nth 0) __NotIntFail)
+
+let GetBool (elem: Model.Element) =
+ let __NotBoolFail e = failwith ("not a bool element: " + elem.ToString())
+ let rec __GetBoolStrict (e: Model.Element) cont =
+ match e with
+ | :? Model.Boolean as bval -> bval.Value
+ | _ -> cont e
+ __GetBoolStrict elem (fun e ->
+ let f = e.Model.MkFunc(U_2_BOOL_FNAME, 1)
+ let matches = f.Apps |> Seq.filter (fun ft -> ft.Args.[0] = e) |> Seq.map (fun ft -> ft.Result)
+ if matches |> Seq.isEmpty then
+ __NotBoolFail e
+ else
+ __GetBoolStrict (matches |> Seq.nth 0) __NotBoolFail)
+
+let ConvertValue (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*)
+ | :? Model.Uninterpreted as uval ->
+ try BoolConst(GetBool refVal)
+ with _ -> try IntConst(GetInt refVal)
+ with _ -> 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 LastDotSplit (str: string) =
let dotIdx = str.LastIndexOf(".")
let s1 = if dotIdx = -1 then "" else str.Substring(0, dotIdx)
@@ -135,16 +171,16 @@ let rec UpdateContext lst1 lst2 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 f_unbox = model.MkFunc(UNBOX_FNAME, 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
+ | Some(e) -> ConvertValue e
| None -> GetLoc e
let ReadHeap (model: Microsoft.Boogie.Model) prog =
- let f_heap_select = model.MkFunc("[3]", 3)
+ let f_heap_select = model.MkFunc(HEAP_SELECT_FNAME, 3)
let values = f_heap_select.Apps
values |> Seq.fold (fun acc ft ->
assert (ft.Args.Length = 3)
@@ -169,7 +205,7 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
match fldVarOpt with
| Some(fldVar) ->
let fldType = GetVarType fldVar
- let fldVal = ConvertValue model refVal
+ let fldVal = ConvertValue refVal
acc |> Map.add (refObj, fldVar) fldVal
| None -> acc
) Map.empty
@@ -189,7 +225,7 @@ let rec ReadArgValues (model: Microsoft.Boogie.Model) args =
let fldVar = v
assert (Seq.length func.Apps = 1)
let ft = Seq.head func.Apps
- let fldVal = ConvertValue model (ft.Result)
+ let fldVal = ConvertValue (ft.Result)
ReadArgValues model rest |> Map.add (VarConst(name)) fldVal
| None -> failwith ("cannot find corresponding function for parameter " + name)
| [] -> Map.empty
@@ -258,8 +294,8 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
// keeps reading from Seq#Build and Seq#Append until fixpoint
let rec __ReadUntilFixpoint hmodel =
- let f_seq_bld = model.MkFunc("Seq#Build", 2)
- let f_seq_app = model.MkFunc("Seq#Append", 2)
+ let f_seq_bld = model.MkFunc(SEQ_BUILD_FNAME, 2)
+ let f_seq_app = model.MkFunc(SEQ_APPEND_FNAME, 2)
let hmodel' = hmodel |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
|> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)
if hmodel' = hmodel then
@@ -267,8 +303,8 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
else
__ReadUntilFixpoint hmodel'
- let f_seq_len = model.MkFunc("Seq#Length", 1)
- let f_seq_idx = model.MkFunc("Seq#Index", 2)
+ let f_seq_len = model.MkFunc(SEQ_LENGTH_FNAME, 1)
+ let f_seq_idx = model.MkFunc(SEQ_INDEX_FNAME, 2)
let hmodel = (envMap,ctx)
let hmodel' = hmodel |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)
|> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)
@@ -305,8 +341,8 @@ let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =
__ReadSetMembership rest (env,ctx)
| [] -> (env,ctx)
- let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps)
- let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps)
+ let t_set_empty = Seq.toList (model.MkFunc(SET_EMPTY_FNAME, 1).Apps)
+ let t_set = Seq.toList (model.MkFunc(SET_SELECT_FNAME, 2).Apps)
(envMap,ctx) |> __ReadSetEmpty t_set_empty
|> __ReadSetMembership t_set
@@ -383,7 +419,7 @@ let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =
/// and adds it to the given "envMap" map and "ctx" set.
// ======================================================
let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) =
- let f_null = model.MkFunc("null", 0)
+ let f_null = model.MkFunc(NULL_FNAME, 0)
assert (f_null.AppCount = 1)
let e = (f_null.Apps |> Seq.nth 0).Result
let newEnv = envMap |> Map.add (GetLoc e) NullConst
@@ -396,7 +432,7 @@ let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) =
/// and then proceeds by reading stuff about the null constant, about sequences, and about sets.
// ============================================================================================
let ReadEnv (model: Microsoft.Boogie.Model) prog =
- let f_dtype = model.MkFunc("dtype", 1)
+ let f_dtype = model.MkFunc(DTYPE_FNAME, 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]
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index f9bbc289..d3493749 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>examples/DList.jen /method:DNode.Init /noGenMod</StartArguments>
+ <StartArguments>examples/oopsla12/IntSet.jen /method:IntSet.Singleton</StartArguments>
<StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
diff --git a/Jennisys/README.txt b/Jennisys/README.txt
index 41bb9964..30f91b2e 100644
--- a/Jennisys/README.txt
+++ b/Jennisys/README.txt
@@ -1,18 +1,28 @@
1. Installation instructions
----------------------------
+ - download the entire boogie source distribution and place it in c:\boogie
- create c:\tmp folder
- copy the Jennisys\scripts\StartDafny-jen.bat script into c:\tmp
2. Running the examples
----------------------------
- $ cd Jennisys
- $ bin/Debug/Jennisys.exe examples/<name>.jen /genRepr /genMod
+ $ cd Jennisys
+ $ bin/Debug/Jennisys.exe examples/<name>.jen
- /genRepr - generate Repr field
- /genMod - generate modular code (delegate to methods)
+ The most current and complete set of examples is in the
+ "examples/oopsla12" folder. No additional Jennisys switches need be
+ passed for either of them.
- Currenty, in the List.jen example, methods SkipFew and Index cannot
- be synthesized. All other methods in List.jen, List2.jen, List3.jen,
- Set.jen, Number.jen, and NumberMethods.jen should be synthesizable.
+ Synthesized programs will be generated in "c:\tmp", and their file
+ names will follow the following pattern:
+
+ "jennisys-synth_<example-name>.dfy"
+
+ To verify the correctness of the synthesized programs, run
+
+ $ Dafny /compile:0 jennisys-synth_<example-name>.dfy
+
+ Expected outputs (i.e., synthesized Dafny programs) for the examples
+ in "examples/oopsla12" can be found in the same folder.
diff --git a/Jennisys/examples/BHeap.jen b/Jennisys/examples/BHeap.jen
new file mode 100644
index 00000000..55258bde
--- /dev/null
+++ b/Jennisys/examples/BHeap.jen
@@ -0,0 +1,33 @@
+interface BHeap {
+ var elems: set[int]
+
+ constructor Singleton(x: int)
+ ensures elems = {x}
+
+ constructor Dupleton(a: int, b: int)
+ requires a != b
+ ensures elems = {a b}
+
+ constructor Tripleton(x: int, y: int, z: int)
+ requires x != y && y != z && z != x
+ ensures elems = {x y z}
+
+ method Find(n: int) returns (ret: bool)
+ ensures ret = (n in elems)
+}
+
+datamodel BHeap {
+ var data: int
+ var left: BHeap
+ var right: BHeap
+
+ frame
+ left * right
+
+ invariant
+ elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})
+ left != null ==> forall e :: e in left.elems ==> e < data
+ right != null ==> forall e :: e in right.elems ==> e < data
+ left = null ==> right = null
+ (left != null && right = null) ==> left.elems = {left.data}
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 16:17:43 +0000