summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Jennisys/AstUtils.fs19
-rw-r--r--Jennisys/CodeGen.fs70
-rw-r--r--Jennisys/DafnyModelUtils.fs4
-rw-r--r--Jennisys/Utils.fs9
-rw-r--r--Jennisys/examples/Set.jen3
5 files changed, 88 insertions, 17 deletions
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index ab86324b..fa5a0a77 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -189,6 +189,23 @@ let GetAllFields comp =
let aVars = FilterFieldMembers members
List.concat [aVars ; cVars]
| _ -> []
+
+// ===========================================================
+/// Returns a map (Type |--> Set<Var>) where all
+/// the given fields are grouped by their type
+///
+/// ensures: forall v :: v in ret.values.elems ==> v in fields
+/// ensures: forall k :: k in ret.keys ==>
+/// forall v1, v2 :: v1, v2 in ret[k].elems ==>
+/// v1.type = v2.type
+// ===========================================================
+let rec GroupFieldsByType fields =
+ match fields with
+ | Var(name, ty) :: rest ->
+ let map = GroupFieldsByType rest
+ let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty
+ map |> Map.add ty (fldSet |> Set.add (Var(name, ty)))
+ | [] -> Map.empty
// =================================
/// Returns class name of a component
@@ -642,7 +659,7 @@ let ChangeThisReceiver receiver expr =
| UpdateExpr(e1,e2,e3) -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3)
| SequenceExpr(exs) -> SequenceExpr(exs |> List.map (__ChangeThis locals))
| SetExpr(exs) -> SetExpr(exs |> List.map (__ChangeThis locals))
- (* function body starts here *)
+ (* --- function body starts here --- *)
__ChangeThis Set.empty expr
let rec Rewrite rewriterFunc expr =
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index f2d5766c..6b53112e 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -10,16 +10,49 @@ open DafnyPrinter
open DafnyModelUtils
// TODO: this should take a list of fields and unroll all possibilities (instead of unrolling on branch only, following exactly one field)
-let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr =
+//let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr =
+// if numUnrolls = 0 then
+// TrueLiteral
+// else
+// BinaryImplies (BinaryNeq fldExpr (ObjLiteral("null")))
+// (BinaryAnd (Dot(fldExpr, validFunName))
+// (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))
+
+/// requires: numUnrols >= 0
+/// requires: |fldExprs| = |fldNames|
+let rec GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls =
+ let rec __Combine exprLst strLst =
+ match exprLst with
+ | e :: rest ->
+ let resLst1 = strLst |> List.map (fun s -> Dot(e, s))
+ List.concat [resLst1; __Combine rest strLst]
+ | [] -> []
+ let rec __NotNull e =
+ match e with
+ | IdLiteral(_)
+ | ObjLiteral(_) -> BinaryNeq e (ObjLiteral("null"))
+ | Dot(sub, str) -> BinaryAnd (__NotNull sub) (BinaryNeq e (ObjLiteral("null")))
+ | _ -> failwith "not supposed to happen"
+ (* --- function body starts here --- *)
+ assert (numUnrolls >= 0)
if numUnrolls = 0 then
- TrueLiteral
+ [TrueLiteral]
else
- BinaryImplies (BinaryNeq fldExpr (IdLiteral("null")))
- (BinaryAnd (Dot(fldExpr, validFunName))
- (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))
+ let exprList = fldExprs |> List.map (fun e -> BinaryImplies (__NotNull e) (Dot(e, validFunName)))
+ if numUnrolls = 1 then
+ exprList
+ else
+ let fldExprs = __Combine fldExprs fldNames
+ List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFunName (numUnrolls - 1))
+
+
+//let GetFieldValidExpr fldName validFunName numUnrolls : Expr =
+// GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls
-let GetFieldValidExpr fldName validFunName numUnrolls : Expr =
- GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls
+let GetFieldValidExpr flds validFunName numUnrolls =
+ let fldExprs = flds |> List.map (function Var(name, _) -> IdLiteral(name))
+ let fldNames = flds |> List.map (function Var(name, _) -> name)
+ GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls
let GetFieldsForValidExpr allFields prog : VarDecl list =
allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
@@ -27,13 +60,22 @@ let GetFieldsForValidExpr allFields prog : VarDecl list =
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()", Options.CONFIG.numLoopUnrolls
- | _ -> "Valid()", 1
- GetFieldValidExpr name validFunName numUnrolls
- )
+ let fieldsByType = GroupFieldsByType fields
+ fieldsByType |> Map.fold (fun acc t varSet ->
+ let validFunName, numUnrolls =
+ match t with
+ | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls
+ | _ -> "Valid()", 1
+ acc |> List.append (GetFieldValidExpr (Set.toList varSet) validFunName numUnrolls)
+ ) []
+
+// fields |> List.map (function Var(name, t) ->
+// let validFunName, numUnrolls =
+// match t with
+// | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls
+// | _ -> "Valid()", 1
+// GetFieldValidExpr name validFunName numUnrolls
+// )
let PrintValidFunctionCode comp prog genRepr: string =
let idt = " "
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index f04a0ca5..83de2292 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -247,11 +247,11 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
let f_seq_len = model.MkFunc("Seq#Length", 1)
let f_seq_idx = model.MkFunc("Seq#Index", 2)
- let f_seq_bld = model.MkFunc("Seq#Build", 4)
+ //let f_seq_bld = model.MkFunc("Seq#Build", 4)
let f_seq_app = model.MkFunc("Seq#Append", 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)
+ // |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
|> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index 8c25726a..c9f18e23 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -48,6 +48,15 @@ let ExtractOptionMsg msg x =
let ExtractOption x =
ExtractOptionMsg "can't extract anything from a None" x
+// ====================================
+/// ensures: res = Some(a) ==> ret = a
+/// ensures: res = None ==> ret = defVal
+// ====================================
+let ExtractOptionOr defVal opt =
+ match opt with
+ | Some(a) -> a
+ | None -> defVal
+
// ==========================================================
/// requres: List.length lst <= 1, otherwise fails with errMsg
/// ensures: if |lst| = 0 then
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index 2142738e..6006268e 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -14,6 +14,9 @@ class Set {
requires p != q
ensures elems = {p q}
+ constructor Triple(p: int, q: int, r: int)
+ requires p != q && q != r && r != p
+ ensures elems = {p q r}
}
model Set {
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 16:48:14 +0000