diff options
Diffstat (limited to 'Jennisys')
| -rw-r--r-- | Jennisys/Analyzer.fs | 200 | ||||
| -rw-r--r-- | Jennisys/Ast.fs | 1 | ||||
| -rw-r--r-- | Jennisys/AstUtils.fs | 91 | ||||
| -rw-r--r-- | Jennisys/CodeGen.fs | 162 | ||||
| -rw-r--r-- | Jennisys/DafnyModelUtils.fs | 19 | ||||
| -rw-r--r-- | Jennisys/DafnyPrinter.fs | 15 | ||||
| -rw-r--r-- | Jennisys/Jennisys.fsproj | 2 | ||||
| -rw-r--r-- | Jennisys/Options.fs | 32 | ||||
| -rw-r--r-- | Jennisys/Printer.fs | 284 | ||||
| -rw-r--r-- | Jennisys/Resolver.fs | 108 | ||||
| -rw-r--r-- | Jennisys/Utils.fs | 31 | ||||
| -rw-r--r-- | Jennisys/examples/List.jen | 6 | ||||
| -rw-r--r-- | Jennisys/examples/List2.jen | 4 | ||||
| -rw-r--r-- | Jennisys/examples/List3.jen | 4 | ||||
| -rw-r--r-- | Jennisys/examples/Set.jen | 9 |
15 files changed, 565 insertions, 403 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 9603dd6e..2bbd43cf 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -13,13 +13,7 @@ open Utils open Microsoft.Boogie
-type MethodSolution = {
- pathCond: Expr;
- heap : Map<Const * VarDecl, Const>;
- env : Map<Const, Const>;
- ctx : Set<Set<Const>>;
-}
-
+
let Rename suffix vars =
vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
@@ -92,7 +86,7 @@ let rec IsArgsOnly args expr = | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e
//TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"
-let GetUnifications indent expr args (heap,env,ctx) =
+let GetUnifications indent expr args heapInst =
let idt = Indent indent
// - first looks if the give expression talks only about method arguments (args)
// - then checks if it doesn't already exist in the unification map
@@ -103,8 +97,8 @@ let GetUnifications indent expr args (heap,env,ctx) = builder {
let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption
let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption
- let! v = try Some(Eval (heap,env,ctx) true e |> Expr2Const) with ex -> None
- Logger.DebugLine (idt + " - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));
+ let! v = try Some(Eval heapInst true e |> Expr2Const) with ex -> None
+ Logger.DebugLine (idt + " - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v))
return Map.add e v unifMap
}
// just recurses on all expressions
@@ -134,15 +128,15 @@ let GetUnifications indent expr args (heap,env,ctx) = /// Returns a map (Expr |--> Const) containing unifications
/// found for the given method and heap/env/ctx
// =======================================================
-let GetUnificationsForMethod indent comp m (heap,env,ctx) =
+let GetUnificationsForMethod indent comp m heapInst =
let idt = Indent indent
- let rec GetArgValueUnifications args env =
+ let rec GetArgValueUnifications args =
match args with
| Var(name,_) :: rest ->
- match Map.tryFind (Unresolved(name)) env with
+ match Map.tryFind name heapInst.methodArgs with
| Some(c) ->
- Logger.DebugLine (idt + " - adding unification " + (PrintConst c) + " <--> " + name);
- Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)
+ Logger.DebugLine (idt + " - adding unification " + name + " <--> " + (PrintConst c));
+ Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest)
| None -> failwith ("couldn't find value for argument " + name)
| [] -> Map.empty
(* --- function body starts here --- *)
@@ -151,8 +145,8 @@ let GetUnificationsForMethod indent comp m (heap,env,ctx) = let args = List.concat [ins; outs]
match args with
| [] -> Map.empty
- | _ -> GetUnifications indent (BinaryAnd pre post) args (heap,env,ctx)
- |> Utils.MapAddAll (GetArgValueUnifications args env)
+ | _ -> GetUnifications indent (BinaryAnd pre post) args heapInst
+ |> Utils.MapAddAll (GetArgValueUnifications args)
| _ -> failwith ("not a method: " + m.ToString())
// =========================================================================
@@ -163,33 +157,32 @@ let GetUnificationsForMethod indent comp m (heap,env,ctx) = /// path. It starts from the given object, and follows the backpointers
/// until it reaches the root ("this")
// =========================================================================
-let objRef2ExprCache = new System.Collections.Generic.Dictionary<Const, Expr>()
-let GetObjRefExpr o (heap,env,ctx) =
- let rec __GetObjRefExpr o (heap,env,ctx) visited =
- if Set.contains o visited then
+let objRef2ExprCache = new System.Collections.Generic.Dictionary<string, Expr>()
+let GetObjRefExpr objRefName (heapInst: HeapInstance) =
+ let rec __GetObjRefExpr objRefName visited =
+ if Set.contains objRefName visited then
None
else
- let newVisited = Set.add o visited
- let refName = PrintObjRefName o (env,ctx)
- match refName with
+ let newVisited = Set.add objRefName visited
+ match objRefName with
| "this" -> Some(ObjLiteral("this"))
| _ ->
let rec __fff lst =
match lst with
- | ((o,Var(fldName,_)),l) :: rest ->
- match __GetObjRefExpr o (heap,env,ctx) newVisited with
+ | ((o,Var(fldName,_)),_) :: rest ->
+ match __GetObjRefExpr o.name newVisited with
| Some(expr) -> Some(Dot(expr, fldName))
| None -> __fff rest
| [] -> None
- let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList
+ let backPointers = heapInst.assignments |> Map.filter (fun (_,_) l -> l = ObjLiteral(objRefName)) |> Map.toList
__fff backPointers
(* --- function body starts here --- *)
- if objRef2ExprCache.ContainsKey(o) then
- Some(objRef2ExprCache.[o])
+ if objRef2ExprCache.ContainsKey(objRefName) then
+ Some(objRef2ExprCache.[objRefName])
else
- let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)
+ let res = __GetObjRefExpr objRefName (Set.empty)
match res with
- | Some(e) -> objRef2ExprCache.Add(o, e)
+ | Some(e) -> objRef2ExprCache.Add(objRefName, e)
| None -> ()
res
@@ -199,13 +192,13 @@ let GetObjRefExpr o (heap,env,ctx) = /// If "conservative" is true, applies only those that
/// can be verified to hold, otherwise applies all of them
// =======================================================
-let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservative =
+let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
let idt = Indent indent
let __CheckUnif o f e idx =
if not conservative || not Options.CONFIG.checkUnifications then
true
else
- let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + (PrintObjRefName o (env,ctx)))
+ let objRefExpr = GetObjRefExpr o heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o)
let fldName = PrintVarName f
let lhs = Dot(objRefExpr, fldName)
let assertionExpr = match f with
@@ -213,7 +206,7 @@ let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservativ | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs
| _ -> BinaryEq lhs e
// check if the assertion follows and if so update the env
- let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)
+ let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) false
Logger.Debug (idt + " - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))
if ok then
@@ -224,50 +217,49 @@ let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservativ (* --- function body starts here --- *)
match unifs with
| (e,c) :: rest ->
- let restHeap,env,ctx = ApplyUnifications indent prog comp mthd rest (heap,env,ctx) conservative
- let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->
- let value = TryResolve (env,ctx) l
- if value = c then
- if __CheckUnif o f e -1 then
- // change the value to expression
- //Logger.TraceLine (sprintf "%s - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )
- acc |> Map.add (o,f) (ExprConst(e))
- else
- // don't change the value unless "conservative = false"
- acc |> Map.add (o,f) l
- else
- let rec __UnifyOverLst lst cnt =
- match lst with
- | lstElem :: rest when lstElem = c ->
- if __CheckUnif o f e cnt then
- //Logger.TraceLine (sprintf "%s - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )
- ExprConst(e) :: __UnifyOverLst rest (cnt+1)
- else
- lstElem :: __UnifyOverLst rest (cnt+1)
- | lstElem :: rest ->
- lstElem :: __UnifyOverLst rest (cnt+1)
- | [] -> []
- // see if it's a list, then try to match its elements, otherwise leave it as is
- match value with
- | SeqConst(clist) ->
- let newLstConst = __UnifyOverLst clist 0
- acc |> Map.add (o,f) (SeqConst(newLstConst))
- | SetConst(cset) ->
- let newLstConst = __UnifyOverLst (Set.toList cset) 0
- acc |> Map.add (o,f) (SetConst(newLstConst |> Set.ofList))
- | _ ->
- acc |> Map.add (o,f) l
- ) restHeap
- (newHeap,env,ctx)
- | [] -> (heap,env,ctx)
+ let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative
+ let newHeap = heapInst.assignments|> Map.fold (fun acc (o,f) value ->
+ if value = Const2Expr c then
+ if __CheckUnif o.name f e -1 then
+ // change the value to expression
+ //Logger.TraceLine (sprintf "%s - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )
+ acc |> Map.add (o,f) e
+ else
+ // don't change the value unless "conservative = false"
+ acc |> Map.add (o,f) value
+ else
+ let rec __UnifyOverLst lst cnt =
+ match lst with
+ | lstElem :: rest when lstElem = Const2Expr c ->
+ if __CheckUnif o.name f e cnt then
+ //Logger.TraceLine (sprintf "%s - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )
+ e :: __UnifyOverLst rest (cnt+1)
+ else
+ lstElem :: __UnifyOverLst rest (cnt+1)
+ | lstElem :: rest ->
+ lstElem :: __UnifyOverLst rest (cnt+1)
+ | [] -> []
+ // see if it's a list, then try to match its elements, otherwise leave it as is
+ match value with
+ | SequenceExpr(elist) ->
+ let newExprList = __UnifyOverLst elist 0
+ acc |> Map.add (o,f) (SequenceExpr(newExprList))
+ | SetExpr(elist) ->
+ let newExprList = __UnifyOverLst elist 0
+ acc |> Map.add (o,f) (SetExpr(newExprList))
+ | _ ->
+ acc |> Map.add (o,f) value
+ ) heapInst.assignments
+ {heapInst with assignments = newHeap }
+ | [] -> heapInst
// ====================================================================================
/// Returns whether the code synthesized for the given method can be verified with Dafny
// ====================================================================================
-let VerifySolution prog comp mthd sol =
+let VerifySolution prog comp mthd sol genRepr =
// print the solution to file and try to verify it with Dafny
let solutions = Map.empty |> Map.add (comp,mthd) sol
- let code = PrintImplCode prog solutions (fun p -> [comp,mthd])
+ let code = PrintImplCode prog solutions (fun p -> [comp,mthd]) genRepr
CheckDafnyProgram code dafnyVerifySuffix
// ============================================================================
@@ -280,7 +272,7 @@ let rec AnalyzeConstructor indent prog comp m = let methodName = GetMethodName m
let pre,post = GetMethodPrePost m
// generate Dafny code for analysis first
- let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral)
+ let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral) false
Logger.InfoLine (idt + "[*] Analyzing constructor")
Logger.InfoLine (idt + "------------------------------------------")
Logger.InfoLine (PrintMethodSignFull (indent + 4) m)
@@ -297,13 +289,14 @@ let rec AnalyzeConstructor indent prog comp m = failwith "internal error (more than one model for a single constructor analysis)"
Logger.InfoLine " OK "
let model = models.[0]
- let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
- let unifs = GetUnificationsForMethod indent comp m (heap,env,ctx) |> Map.toList
- let heap,env,ctx = ApplyUnifications indent prog comp m unifs (heap,env,ctx) true
+ let hModel = ReadFieldValuesFromModel model prog comp m
+ let heapInst = ResolveModel hModel
+ let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList
+ let heapInst = ApplyUnifications indent prog comp m unifs heapInst true
if Options.CONFIG.verifySolutions then
Logger.InfoLine (idt + " - verifying synthesized solution ... ")
- let sol = [TrueLiteral, (heap,env,ctx)]
- let verified = VerifySolution prog comp m sol
+ let sol = [TrueLiteral, heapInst]
+ let verified = VerifySolution prog comp m sol Options.CONFIG.genRepr
Logger.Info (idt + " ")
if verified then
Logger.InfoLine "~~~ VERIFIED ~~~"
@@ -311,50 +304,53 @@ let rec AnalyzeConstructor indent prog comp m = else
Logger.InfoLine "!!! NOT VERIFIED !!!"
Logger.InfoLine (idt + " Strengthening the pre-condition")
- TryInferConditionals (indent + 4) prog comp m unifs (heap,env,ctx)
+ TryInferConditionals (indent + 4) prog comp m unifs heapInst
else
- [TrueLiteral, (heap,env,ctx)]
-and TryInferConditionals indent prog comp m unifs (heap,env,ctx) =
+ [TrueLiteral, heapInst]
+and TryInferConditionals indent prog comp m unifs heapInst =
let idt = Indent indent
- let heap2,env2,ctx2 = ApplyUnifications indent prog comp m unifs (heap,env,ctx) false
+ let wrongSol = [TrueLiteral, heapInst]
+ let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false
// get expressions to evaluate:
- // - add pre and post conditions
- // - go through all objects on the heap and assert its invariant
+ // - add post (and pre?) conditions
+ // - go through all objects on the heap and assert their invariants
let pre,post = GetMethodPrePost m
let prepostExpr = post //TODO: do we need the "pre" here as well?
- let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty
+ let heapObjs = heapInst2.assignments |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty
let expr = heapObjs |> Set.fold (fun acc o ->
- let receiverOpt = GetObjRefExpr o (heap,env,ctx)
+ let receiverOpt = GetObjRefExpr o.name heapInst2
let receiver = Utils.ExtractOption receiverOpt
- match Resolve (env,ctx) o with
- | NewObj(_,tOpt) | ThisConst(_,tOpt) ->
- let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt
- let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption
- let objInvs = GetInvariantsAsList objComp
- let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)
- objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc
- | _ -> failwith "not supposed to happen"
+ let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption
+ let objInvs = GetInvariantsAsList objComp
+ let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)
+ objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc
) prepostExpr
- //expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")
// now evaluate and see what's left
- let newCond = Eval (heap2,env2,ctx2) false expr
+ let newCond = Eval heapInst2 false expr
try
if newCond = TrueLiteral then
Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt)
- []
+ wrongSol
else
Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 newCond))
let p2,c2,m2 = AddPrecondition prog comp m newCond
Logger.Info (idt + " - verifying partial solution ... ")
- let sol = [newCond, (heap2,env2,ctx2)]
- let verified = VerifySolution p2 c2 m2 sol
+ let sol = [newCond, heapInst2]
+ let verified =
+ if Options.CONFIG.verifyPartialSolutions then
+ VerifySolution p2 c2 m2 sol Options.CONFIG.genRepr
+ else
+ true
if verified then
- Logger.InfoLine "VERIFIED"
+ if Options.CONFIG.verifyPartialSolutions then
+ Logger.InfoLine "VERIFIED"
+ else
+ Logger.InfoLine "SKIPPED"
let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(newCond))
sol.[0] :: AnalyzeConstructor (indent + 2) p3 c3 m3
else
Logger.InfoLine "NOT VERIFIED"
- []
+ wrongSol
with
ex -> raise ex
@@ -410,7 +406,7 @@ let Analyze prog filename = use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName))
file.AutoFlush <- true
Logger.InfoLine "Printing synthesized code"
- let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze
+ let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr
fprintfn file "%s" synthCode
()
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 1ddf1f31..b9105254 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -56,7 +56,6 @@ type Const = | ThisConst of (* loc id *) string * Type option
| VarConst of string
| NewObj of (* loc id *) string * Type option
- | ExprConst of Expr
| Unresolved of (* loc id *) string
type Stmt =
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 25d2a129..ab86324b 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -9,6 +9,9 @@ module AstUtils open Ast
open Utils
+let PrintGenSym name =
+ sprintf "gensym%s" name
+
// =====================
/// Returns TRUE literal
// =====================
@@ -30,6 +33,12 @@ let UnaryNot sub = | _ -> UnaryExpr("!", sub)
// =======================================================================
+/// Returns a binary PLUS of the two given expressions
+// =======================================================================
+let BinaryPlus (lhs: Expr) (rhs: Expr) =
+ BinaryExpr(50, "+", lhs, rhs)
+
+// =======================================================================
/// Returns a binary AND of the two given expressions with short-circuiting
// =======================================================================
let BinaryAnd (lhs: Expr) (rhs: Expr) =
@@ -62,37 +71,6 @@ let BinaryImplies lhs rhs = | _, BoolLiteral(false) -> UnaryNot(lhs)
| _ -> BinaryExpr(20, "==>", lhs, rhs)
-
-//let TrueLiteral = IdLiteral("true")
-//let FalseLiteral = IdLiteral("false")
-//
-//// =======================================================================
-///// Returns a binary AND of the two given expressions with short-circuiting
-//// =======================================================================
-//let BinaryAnd (lhs: Expr) (rhs: Expr) =
-// match lhs, rhs with
-// | IdLiteral("true"), _ -> rhs
-// | IdLiteral("false"), _ -> IdLiteral("false")
-// | _, IdLiteral("true") -> lhs
-// | _, IdLiteral("false") -> IdLiteral("false")
-// | _, _ -> BinaryExpr(30, "&&", lhs, rhs)
-//
-//// =======================================================================
-///// Returns a binary OR of the two given expressions with short-circuiting
-//// =======================================================================
-//let BinaryOr (lhs: Expr) (rhs: Expr) =
-// match lhs, rhs with
-// | IdLiteral("true"), _ -> IdLiteral("true")
-// | IdLiteral("false"), _ -> rhs
-// | _, IdLiteral("true") -> IdLiteral("true")
-// | _, IdLiteral("false") -> lhs
-// | _, _ -> BinaryExpr(30, "||", lhs, rhs)
-//
-//// ===================================================================================
-///// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)
-//// ===================================================================================
-//let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)
-
// =======================================================
/// Constructors for binary EQ/NEQ of two given expressions
// =======================================================
@@ -100,6 +78,11 @@ let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs) let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)
// =======================================================
+/// Constructor for binary GETS
+// =======================================================
+let BinaryGets lhs rhs = Assign(lhs, rhs)
+
+// =======================================================
/// Constructors for binary IN/!IN of two given expressions
// =======================================================
let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs)
@@ -134,11 +117,10 @@ let rec Const2Expr c = let expSet = cset |> Set.fold (fun acc c -> Set.add (Const2Expr c) acc) Set.empty
SetExpr(Set.toList expSet)
| VarConst(id) -> VarLiteral(id)
- | ThisConst(name,_)
- | NewObj(name,_) -> ObjLiteral(name)
+ | ThisConst(_,_) -> ObjLiteral("this")
+ | NewObj(name,_) -> ObjLiteral(PrintGenSym name)
| NullConst -> ObjLiteral("null")
- | ExprConst(e) -> e
- | Unresolved(name) -> printf "What about unresolved stuff??"; failwith "don't want to convert unresolved to expr"
+ | Unresolved(name) -> failwithf "don't want to convert unresolved(%s) to expr" name // IdLiteral(name) //
| _ -> failwithf "not implemented or not supported: %O" c
let rec Expr2Const e =
@@ -147,7 +129,7 @@ let rec Expr2Const e = | BoolLiteral(b) -> BoolConst(b)
| ObjLiteral("this") -> ThisConst("this",None)
| ObjLiteral("null") -> NullConst
- | ObjLiteral(name) -> NewObj(name, None) //TODO: or Unresolved?
+ | ObjLiteral(name) -> Unresolved(name)
| IdLiteral(id) -> Unresolved(id)
| VarLiteral(id) -> VarConst(id)
| SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)
@@ -314,13 +296,36 @@ let FindMethod comp methodName = // ==============================================
/// Finds a field of a class that has a given name
// ==============================================
-let FindVar (prog: Program) clsName fldName =
- let copt = FindComponent prog clsName
- match copt with
- | Some(comp) ->
- GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
- |> Utils.ListToOption
- | None -> None
+//let FindCompVar prog clsName fldName =
+// let copt = FindComponent prog clsName
+// match copt with
+// | Some(comp) ->
+// GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
+// |> Utils.ListToOption
+// | None -> None
+
+let FindVar comp fldName =
+ GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
+ |> Utils.ListToOption
+
+// ======================================
+/// Returns the frame of a given component
+// ======================================
+let GetFrame comp =
+ match comp with
+ | Component(_, Model(_,_,_,frame,_), _) -> frame
+ | _ -> failwithf "not a valid component %O" comp
+
+let GetFrameFields comp =
+ let frame = GetFrame comp
+ frame |> List.choose (function IdLiteral(name) -> Some(name) | _ -> None) // TODO: is it really enough to handle only IdLiteral's
+ |> List.choose (fun varName ->
+ let v = FindVar comp varName
+ Utils.ExtractOptionMsg ("field not found: " + varName) v |> ignore
+ v
+ )
+
+////////////////////////
let AddPrecondition prog comp m e =
match prog, comp, m with
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index 5d7f8611..f2d5766c 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -7,9 +7,9 @@ open Printer open Resolver
open TypeChecker
open DafnyPrinter
+open DafnyModelUtils
-let numLoopUnrolls = 2
-
+// 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 =
if numUnrolls = 0 then
TrueLiteral
@@ -30,12 +30,12 @@ let GetFieldsValidExprList clsName allFields prog : Expr list = fields |> List.map (function Var(name, t) ->
let validFunName, numUnrolls =
match t with
- | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", numLoopUnrolls
+ | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls
| _ -> "Valid()", 1
GetFieldValidExpr name validFunName numUnrolls
)
-let PrintValidFunctionCode comp prog : string =
+let PrintValidFunctionCode comp prog genRepr: string =
let idt = " "
let __PrintInvs invs =
invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
@@ -45,16 +45,33 @@ let PrintValidFunctionCode comp prog : string = let vars = GetAllFields comp
let allInvs = GetInvariantsAsList comp |> DesugarLst
let fieldsValid = GetFieldsValidExprList clsName vars prog
-
+
+ let frameFldNames = GetFrameFields comp |> List.choose (function Var(name,_) -> Some(name))
+ let validReprBody =
+ " this in Repr &&" + newline +
+ " null !in Repr" +
+ (PrintSep "" (fun x -> " &&" + newline + " ($x != null ==> $x in Repr && $x.Repr <= Repr && this !in $x.Repr)".Replace("$x", x)) frameFldNames)
+
+ let vr =
+ if genRepr then
+ " function Valid_repr(): bool" + newline +
+ " reads *;" + newline +
+ " {" + newline +
+ validReprBody + newline +
+ " }" + newline + newline
+ else
+ ""
// 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) +
+ vr +
" function Valid_self(): bool" + newline +
" reads *;" + newline +
" {" + newline +
+ (Utils.Ite genRepr (" Valid_repr() &&" + newline) "") +
(__PrintInvs allInvs) + newline +
" }" + newline +
newline +
@@ -65,13 +82,12 @@ let PrintValidFunctionCode comp prog : string = (__PrintInvs fieldsValid) + newline +
" }" + newline
-let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
+let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =
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 aVars = FilterFieldMembers members |> List.append (Utils.Ite genRepr [Var("Repr", Some(SetType(NamedType("object", []))))] [])
let compMethods = FilterConstructorMembers members
// Now print it as a Dafny program
acc +
@@ -80,92 +96,118 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string = (sprintf "%s" (PrintFields aVars 2 true)) + newline +
(sprintf "%s" (PrintFields cVars 2 false)) + newline +
// generate the Valid function
- (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline +
+ (sprintf "%s" (PrintValidFunctionCode comp prog genRepr)) + 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)
- | _ -> failwithf "NewObj doesn't have a type: %O" newObjConst
- ) ""
-let PrintObjRefName o (env,ctx) =
- match Resolve (env,ctx) o with
- | ThisConst(_,_) -> "this";
- | NewObj(name, _) -> PrintGenSym name
- | _ -> failwith ("unresolved object ref: " + o.ToString())
-
-let CheckUnresolved c =
- match c with
- | Unresolved(_) -> Logger.WarnLine "!!! There are some unresolved constants in the output file !!!"; c
- | _ -> c
+let PrintAllocNewObjects heapInst indent =
+ let idt = Indent indent
+ heapInst.assignments |> Map.fold (fun acc (obj,fld) _ ->
+ if not (obj.name = "this") then
+ acc |> Set.add obj
+ else
+ acc
+ ) Set.empty
+ |> Set.fold (fun acc obj -> acc + (sprintf "%svar %s := new %s;%s" idt obj.name (PrintType obj.objType) newline)) ""
-let PrintVarAssignments (heap,env,ctx) indent =
+let PrintVarAssignments heapInst 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 = TryResolve (env,ctx) l |> CheckUnresolved |> PrintConst
- acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline
- ) ""
+ heapInst.assignments |> Map.fold (fun acc (o,f) e ->
+ let fldName = PrintVarName f
+ let value = PrintExpr 0 e
+ acc + (sprintf "%s%s.%s := %s;" idt o.name fldName value) + newline
+ ) ""
-let rec PrintHeapCreationCode sol indent =
+let PrintReprAssignments prog heapInst indent =
+ let __FollowsFunc o1 o2 =
+ heapInst.assignments |> Map.fold (fun acc (srcObj,fld) value ->
+ acc || (srcObj = o1 && value = ObjLiteral(o2.name))
+ ) false
+ let idt = Indent indent
+ let objs = heapInst.assignments |> Map.fold (fun acc (obj,fld) _ -> acc |> Set.add obj) Set.empty
+ |> Set.toList
+ |> Utils.TopSort __FollowsFunc
+ |> List.rev
+ let reprGetsList = objs |> List.fold (fun acc obj ->
+ let expr = SetExpr([ObjLiteral(obj.name)])
+ let builder = CascadingBuilder<_>(expr)
+ let fullRhs = builder {
+ let typeName = GetTypeShortName obj.objType
+ let! comp = FindComponent prog typeName
+ let vars = GetFrameFields comp
+ let nonNullVars = vars |> List.filter (fun v ->
+ match Map.tryFind (obj,v) heapInst.assignments with
+ | Some(ObjLiteral(n)) when not (n = "null") -> true
+ | _ -> false)
+ return nonNullVars |> List.fold (fun a v ->
+ BinaryPlus a (Dot(Dot(ObjLiteral(obj.name), (PrintVarName v)), "Repr"))
+ ) expr
+ }
+ let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs
+ fullReprExpr :: acc
+ ) []
+
+ idt + "// repr stuff" + newline +
+ (PrintStmtList reprGetsList indent)
+
+let rec PrintHeapCreationCode prog sol indent genRepr =
let idt = Indent indent
match sol with
- | (c, (heap,env,ctx)) :: rest ->
+ | (c, heapInst) :: rest ->
+ let __ReprAssignments ind =
+ if genRepr then
+ (PrintReprAssignments prog heapInst ind)
+ else
+ ""
if c = TrueLiteral then
- (PrintAllocNewObjects (heap,env,ctx) indent) +
- (PrintVarAssignments (heap,env,ctx) indent) +
- newline +
- (PrintHeapCreationCode rest indent)
+ (PrintAllocNewObjects heapInst indent) +
+ (PrintVarAssignments heapInst indent) +
+ (__ReprAssignments indent) +
+ (PrintHeapCreationCode prog rest indent genRepr)
else
if List.length rest > 0 then
idt + "if (" + (PrintExpr 0 c) + ") {" + newline +
- (PrintAllocNewObjects (heap,env,ctx) (indent+2)) +
- (PrintVarAssignments (heap,env,ctx) (indent+2)) +
+ (PrintAllocNewObjects heapInst (indent+2)) +
+ (PrintVarAssignments heapInst (indent+2)) +
+ (__ReprAssignments (indent+2)) +
idt + "} else {" + newline +
- (PrintHeapCreationCode rest (indent+2)) +
+ (PrintHeapCreationCode prog rest (indent+2) genRepr) +
idt + "}" + newline
else
- (PrintAllocNewObjects (heap,env,ctx) indent) +
- (PrintVarAssignments (heap,env,ctx) indent)
+ (PrintAllocNewObjects heapInst indent) +
+ (PrintVarAssignments heapInst indent) +
+ (__ReprAssignments indent)
| [] -> ""
-let GenConstructorCode mthd body =
+let GenConstructorCode mthd body genRepr =
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 __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep "" (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 +
+ " modifies this;" +
+ (__PrintPrePost (newline + " requires ") preExpr) +
+ Utils.Ite genRepr (newline + " ensures fresh(Repr - {this});") "" +
+ (__PrintPrePost (newline + " ensures ") postExpr) +
+ newline +
" {" + newline +
body +
" }" + newline
| _ -> ""
-// solutions: (comp, constructor) |--> (heap, env, ctx)
-let PrintImplCode prog solutions methodsToPrintFunc =
+// solutions: (comp, constructor) |--> condition * heapInst
+let PrintImplCode prog solutions methodsToPrintFunc genRepr =
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(sol) -> PrintHeapCreationCode sol 4
+ | Some(sol) -> PrintHeapCreationCode prog sol 4 genRepr
| _ -> " //unable to synthesize" + newline
- (GenConstructorCode mthd mthdBody) + newline
+ (GenConstructorCode mthd mthdBody genRepr) + newline
else
- "")
\ No newline at end of file + "") genRepr
\ No newline at end of file diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index 4b9b0c60..f04a0ca5 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -24,6 +24,15 @@ open AstUtils open Utils
open Microsoft.Boogie
+
+type HeapModel = {
+ heap : Map<Const * VarDecl, Const>;
+ env : Map<Const, Const>;
+ ctx : Set<Set<Const>>;
+}
+
+let MkHeapModel heap env ctx =
+ { heap = heap; env = env; ctx = ctx }
let GetElemFullName (elem: Model.Element) =
elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0)
@@ -140,7 +149,11 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog = 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
+ let nonebuilder = CascadingBuilder<_>(None)
+ let fldVarOpt = nonebuilder {
+ let! comp = FindComponent prog clsName
+ return FindVar comp fldName
+ }
match fldVarOpt with
| Some(fldVar) ->
let fldType = match fldVar with
@@ -165,7 +178,7 @@ let rec ReadArgValues (model: Microsoft.Boogie.Model) args = assert (Seq.length func.Apps = 1)
let ft = Seq.head func.Apps
let fldVal = ConvertValue model (ft.Result)
- ReadArgValues model rest |> Map.add (Unresolved(name)) fldVal
+ ReadArgValues model rest |> Map.add (VarConst(name)) fldVal
| None -> failwith ("cannot find corresponding function for parameter " + name)
| [] -> Map.empty
@@ -382,4 +395,4 @@ 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 + MkHeapModel heap env ctx
\ No newline at end of file diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index d1dc73fc..86974f20 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -1,6 +1,7 @@ module DafnyPrinter open Ast +open AstUtils open Printer let rec PrintType ty = @@ -56,7 +57,6 @@ let rec PrintConst cst = | NullConst -> "null" | NoneConst -> "<none>" | ThisConst(_,_) -> "this" - | ExprConst(e) -> PrintExpr 0 e | NewObj(name,_) -> PrintGenSym name | Unresolved(name) -> sprintf "Unresolved(%s)" name @@ -69,4 +69,15 @@ 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 "%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 + | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) "" + +let rec PrintStmt stmt indent =
+ let idt = (Indent indent)
+ match stmt with
+ | Block(stmts) ->
+ idt + "{" + newline +
+ (PrintStmtList stmts (indent + 2)) +
+ idt + "}" + newline
+ | Assign(lhs,rhs) -> sprintf "%s%s := %s;%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline
+and PrintStmtList stmts indent =
+ stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
\ No newline at end of file diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 5e1bea61..8642cb6b 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\Number.jen /method:Number.Abs /checkUnifs</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Triple /genRepr /noVerifyParSol</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index a03f7213..4bd59b11 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -11,19 +11,27 @@ open Utils type Config = {
inputFilename: string;
methodToSynth: string;
+ verifyPartialSolutions: bool;
verifySolutions: bool;
checkUnifications: bool;
+ genRepr: bool;
timeout: int;
+ numLoopUnrolls: int;
}
let defaultConfig: Config = {
inputFilename = "";
methodToSynth = "*";
+ verifyPartialSolutions = true;
verifySolutions = true;
checkUnifications = false;
+ genRepr = false;
timeout = 0;
+ numLoopUnrolls = 2;
}
+/// Should not be mutated outside the ParseCmdLineArgs method, which is
+/// typically called only once at the beginning of the program execution
let mutable CONFIG = defaultConfig
exception InvalidCmdLineArg of string
@@ -78,6 +86,12 @@ let ParseCmdLineArgs args = | "method" ->
__CheckNonEmpty value opt
__Parse rest { cfg with methodToSynth = value }
+ | "verifyParSol" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with verifyPartialSolutions = b }
+ | "noVerifyParSol" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with verifyPartialSolutions = not b }
| "verifySol" ->
let b = __CheckBool value opt
__Parse rest { cfg with verifySolutions = b }
@@ -90,24 +104,24 @@ let ParseCmdLineArgs args = | "noCheckUnifs" ->
let b = __CheckBool value opt
__Parse rest { cfg with checkUnifications = not b }
+ | "genRepr" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with genRepr = b }
+ | "noGenRepr" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with genRepr = not b }
| "timeout" ->
let t = __CheckInt value opt
__Parse rest { cfg with timeout = t }
+ | "unrolls" ->
+ let t = __CheckInt value opt
+ __Parse rest { cfg with numLoopUnrolls = t }
| "" ->
__Parse rest { cfg with inputFilename = value }
| _ ->
raise (InvalidCmdLineOption("Unknown option: " + opt))
| [] -> cfg
- let __CheckBool value optName =
- if value = "" then
- true
- else
- try
- System.Boolean.Parse value
- with
- | ex -> raise (InvalidCmdLineArg("Option " + optName " must be boolean"))
-
(* --- function body starts here --- *)
CONFIG <- __Parse args defaultConfig
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index e051492f..f8f2933b 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -1,138 +1,134 @@ -module Printer - -open Ast -open AstUtils - -let newline = System.Environment.NewLine // "\r\n" - -let PrintGenSym name = - sprintf "gensym%s" name - -let rec PrintSep sep f list = - match list with - | [] -> "" - | [a] -> f a - | a :: more -> (f a) + sep + (PrintSep sep f more) - -let rec PrintType ty = - match ty with - | 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 - | Var(id,None) -> id - | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty) - -let PrintVarName vd = - match vd with - | Var(id,_) -> id - -let rec PrintExpr ctx expr = - match expr with - | IntLiteral(d) -> sprintf "%d" d - | BoolLiteral(b) -> sprintf "%b" b - | ObjLiteral(id) - | VarLiteral(id) - | IdLiteral(id) -> id - | Star -> "*" - | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id - | UnaryExpr(op,UnaryExpr(op2, e2)) -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2))) - | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e) - | BinaryExpr(strength,op,e0,e1) -> - let needParens = strength <= ctx - let openParen = if needParens then "(" else "" - let closeParen = if needParens then ")" else "" - sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen - | IteExpr(c,e1,e2) -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2) - | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) - | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) - | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0)) - | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) - | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0)) - | ForallExpr(vv,e) -> - let needParens = ctx <> 0 - let openParen = if needParens then "(" else "" - let closeParen = if needParens then ")" else "" - sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen - -let rec PrintConst cst = - match cst with - | IntConst(v) -> sprintf "%d" v - | BoolConst(b) -> sprintf "%b" b - | VarConst(v) -> sprintf "%s" v - | SetConst(cset) -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset)) - | SeqConst(cseq) -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq) - | NullConst -> "null" - | NoneConst -> "<none>" - | ThisConst(_,_) -> "this" - | ExprConst(e) -> PrintExpr 0 e - | NewObj(name,_) -> PrintGenSym name - | Unresolved(name) -> sprintf "Unresolved(%s)" name - -let PrintSig signature = - match signature with - | Sig(ins, outs) -> - let returnClause = - if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl) - else "" - sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause - -let rec Indent i = - if i = 0 then "" else " " + (Indent (i-1)) - -let rec PrintStmt stmt indent = - let idt = (Indent indent) - match stmt with - | Block(stmts) -> - idt + "{" + newline + - (PrintStmtList stmts (indent + 2)) + - idt + "}" + newline - | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline -and PrintStmtList stmts indent = - stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) "" - -let PrintRoutine signature pre body = - let preStr = pre |> ForeachConjunct (fun e -> sprintf " requires %s%s" (PrintExpr 0 e) newline) - sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body) - -let PrintMember m = - match m with - | Field(vd) -> sprintf " var %s%s" (PrintVarDecl vd) newline - | Method(id,signature,pre,body,true) -> sprintf " constructor %s%s" id (PrintRoutine signature pre body) - | Method(id,signature,pre,body,false) -> sprintf " method %s%s" id (PrintRoutine signature pre body) - | Invariant(_) -> "" // invariants are handled separately - -let PrintTopLevelDeclHeader kind id typeParams = - let typeParamStr = - match typeParams with - | [] -> "" - | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp)) - sprintf "%s %s%s {%s" kind id typeParamStr newline - -let PrintDecl d = - match d with - | Class(id,typeParams,members) -> - sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams) - (List.fold (fun acc m -> acc + (PrintMember m)) "" members) - newline - | Model(id,typeParams,vars,frame,inv) -> - (PrintTopLevelDeclHeader "model" id typeParams) + - (vars |> List.fold (fun acc vd -> acc + " var " + (PrintVarDecl vd) + newline) "") + - " frame" + newline + - (frame |> List.fold (fun acc fr -> acc + " " + (PrintExpr 0 fr) + newline) "") + - " invariant" + newline + - (inv |> ForeachConjunct (fun e -> " " + (PrintExpr 0 e) + newline)) + - "}" + newline - | Code(id,typeParams) -> - (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline - -let PrintMethodSignFull indent m = - let idt = Indent indent +module Printer
+
+open Ast
+open AstUtils
+
+let newline = System.Environment.NewLine // "\r\n"
+
+let rec PrintSep sep f list =
+ match list with
+ | [] -> ""
+ | [a] -> f a
+ | a :: more -> (f a) + sep + (PrintSep sep f more)
+
+let rec PrintType ty =
+ match ty with
+ | 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
+ | Var(id,None) -> id
+ | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
+
+let PrintVarName vd =
+ match vd with
+ | Var(id,_) -> id
+
+let rec PrintExpr ctx expr =
+ match expr with
+ | IntLiteral(d) -> sprintf "%d" d
+ | BoolLiteral(b) -> sprintf "%b" b
+ | ObjLiteral(id)
+ | VarLiteral(id)
+ | IdLiteral(id) -> id
+ | Star -> "*"
+ | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
+ | UnaryExpr(op,UnaryExpr(op2, e2)) -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
+ | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)
+ | BinaryExpr(strength,op,e0,e1) ->
+ let needParens = strength <= ctx
+ let openParen = if needParens then "(" else ""
+ let closeParen = if needParens then ")" else ""
+ sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
+ | IteExpr(c,e1,e2) -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
+ | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)
+ | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
+ | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0))
+ | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e)
+ | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0))
+ | ForallExpr(vv,e) ->
+ let needParens = ctx <> 0
+ let openParen = if needParens then "(" else ""
+ let closeParen = if needParens then ")" else ""
+ sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
+
+let rec PrintConst cst =
+ match cst with
+ | IntConst(v) -> sprintf "%d" v
+ | BoolConst(b) -> sprintf "%b" b
+ | VarConst(v) -> sprintf "%s" v
+ | SetConst(cset) -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset))
+ | SeqConst(cseq) -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq)
+ | NullConst -> "null"
+ | NoneConst -> "<none>"
+ | ThisConst(_,_) -> "this"
+ | NewObj(name,_) -> PrintGenSym name
+ | Unresolved(name) -> sprintf "Unresolved(%s)" name
+
+let PrintSig signature =
+ match signature with
+ | Sig(ins, outs) ->
+ let returnClause =
+ if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)
+ else ""
+ sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
+
+let rec Indent i =
+ if i = 0 then "" else " " + (Indent (i-1))
+
+let rec PrintStmt stmt indent =
+ let idt = (Indent indent)
+ match stmt with
+ | Block(stmts) ->
+ idt + "{" + newline +
+ (PrintStmtList stmts (indent + 2)) +
+ idt + "}" + newline
+ | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline
+and PrintStmtList stmts indent =
+ stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
+
+let PrintRoutine signature pre body =
+ let preStr = pre |> ForeachConjunct (fun e -> sprintf " requires %s%s" (PrintExpr 0 e) newline)
+ sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body)
+
+let PrintMember m =
+ match m with
+ | Field(vd) -> sprintf " var %s%s" (PrintVarDecl vd) newline
+ | Method(id,signature,pre,body,true) -> sprintf " constructor %s%s" id (PrintRoutine signature pre body)
+ | Method(id,signature,pre,body,false) -> sprintf " method %s%s" id (PrintRoutine signature pre body)
+ | Invariant(_) -> "" // invariants are handled separately
+
+let PrintTopLevelDeclHeader kind id typeParams =
+ let typeParamStr =
+ match typeParams with
+ | [] -> ""
+ | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp))
+ sprintf "%s %s%s {%s" kind id typeParamStr newline
+
+let PrintDecl d =
+ match d with
+ | Class(id,typeParams,members) ->
+ sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams)
+ (List.fold (fun acc m -> acc + (PrintMember m)) "" members)
+ newline
+ | Model(id,typeParams,vars,frame,inv) ->
+ (PrintTopLevelDeclHeader "model" id typeParams) +
+ (vars |> List.fold (fun acc vd -> acc + " var " + (PrintVarDecl vd) + newline) "") +
+ " frame" + newline +
+ (frame |> List.fold (fun acc fr -> acc + " " + (PrintExpr 0 fr) + newline) "") +
+ " invariant" + newline +
+ (inv |> ForeachConjunct (fun e -> " " + (PrintExpr 0 e) + newline)) +
+ "}" + newline
+ | Code(id,typeParams) ->
+ (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
+
+let PrintMethodSignFull indent m =
+ let idt = Indent indent
let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")
match m with
| Method(methodName, sgn, pre, post, isConstr) ->
@@ -142,9 +138,15 @@ let PrintMethodSignFull indent m = idt + mc + " " + methodName + (PrintSig sgn) + newline +
preStr + (if preStr = "" then "" else newline) +
postStr
- - | _ -> failwithf "not a method: %O" m - -let Print prog = - match prog with - | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls +
+ | _ -> failwithf "not a method: %O" m
+
+let Print prog =
+ match prog with
+ | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls
+
+let PrintObjRefName o =
+ match o with
+ | ThisConst(_,_) -> "this";
+ | NewObj(name, _) -> PrintGenSym name
+ | _ -> failwith ("unresolved object ref: " + o.ToString())
\ No newline at end of file diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs index af49e51a..64f80584 100644 --- a/Jennisys/Resolver.fs +++ b/Jennisys/Resolver.fs @@ -11,6 +11,15 @@ open Ast open AstUtils
open Printer
open EnvUtils
+open DafnyModelUtils
+
+type Obj = { name: string; objType: Type }
+
+type HeapInstance = {
+ assignments: Map<Obj * VarDecl, Expr>; // the first string is the symbolic name of an object literal
+ methodArgs: Map<string, Const>;
+ globals: Map<string, Expr>;
+}
// resolving values
exception ConstResolveFailed of string
@@ -21,30 +30,35 @@ exception ConstResolveFailed of string /// If unable to resolve, it just delegates the task to the
/// failResolver function
// ================================================================
-let rec ResolveCont (env,ctx) failResolver cst =
+let rec ResolveCont hModel failResolver cst =
match cst with
| Unresolved(_) as u ->
// see if it is in the env map first
- let envVal = Map.tryFind cst env
+ let envVal = Map.tryFind cst hModel.env
match envVal with
- | Some(c) -> ResolveCont (env,ctx) failResolver c
+ | Some(c) -> ResolveCont hModel failResolver c
| None ->
// not found in the env map --> check the equality sets
- let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
- |> Utils.SetToOption
+ let eq = hModel.ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
+ |> Utils.SetToOption
match eq with
| Some(eqSet) ->
let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)
|> Utils.SetToOption
match cOpt with
| Some(c) -> c
- | _ -> failResolver cst (env,ctx)
- | _ -> failResolver cst (env,ctx)
+ | _ -> failResolver cst hModel
+ | None ->
+ // finally, see if it's a method argument
+ let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList
+ match m with
+ | (vc,_) :: [] -> vc
+ | _ -> failResolver cst hModel
| SeqConst(cseq) ->
- let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont (env,ctx) failResolver c :: acc) []
+ let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) []
SeqConst(resolvedLst)
| SetConst(cset) ->
- let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont (env,ctx) failResolver c)) Set.empty
+ let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont hModel failResolver c)) Set.empty
SetConst(resolvedSet)
| _ -> cst
@@ -53,39 +67,69 @@ let rec ResolveCont (env,ctx) failResolver cst = ///
/// If unable to resolve, just returns the original Unresolved const.
// =====================================================================
-let TryResolve (env,ctx) cst =
- ResolveCont (env,ctx) (fun c (e,x) -> c) cst
+let TryResolve hModel cst =
+ ResolveCont hModel (fun c _ -> c) cst
// ==============================================================
/// Resolves a given Const (cst) with respect to a given env/ctx.
///
/// If unable to resolve, raises a ConstResolveFailed exception
// ==============================================================
-let Resolve (env,ctx) cst =
- ResolveCont (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst
-
-// =================================================================
-/// Evaluates a given expression with respect to a given heap/env/ctx
-// =================================================================
-let Eval (heap,env,ctx) resolveVars expr =
+let Resolve hModel cst =
+ ResolveCont hModel (fun c _ -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst
+
+// ==================================================================
+/// Evaluates a given expression with respect to a given heap instance
+// ==================================================================
+let Eval heapInst resolveVars expr =
let rec __EvalResolver expr =
match expr with
- | VarLiteral(id) when not resolveVars -> VarConst(id)
- | ObjLiteral("this") -> GetThisLoc env
- | ObjLiteral("null") -> NullConst
- | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO
- | VarLiteral(id)
+ | VarLiteral(id) when not resolveVars -> expr
+ | ObjLiteral("this") | ObjLiteral("null") -> expr
+ | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO
+ | VarLiteral(id) ->
+ let argValue = heapInst.methodArgs |> Map.tryFind id |> Utils.ExtractOptionMsg ("cannot find value for method parameter " + id)
+ argValue |> Const2Expr
| IdLiteral(id) ->
- match TryResolve (env,ctx) (Unresolved(id)) with
- | Unresolved(_) -> __EvalResolver (Dot(ObjLiteral("this"), id))
- | _ as c -> c
+ let globalVal = heapInst.globals |> Map.tryFind id
+ match globalVal with
+ | Some(e) -> e
+ | None -> __EvalResolver (Dot(ObjLiteral("this"), id))
| Dot(e, str) ->
let discr = __EvalResolver e
- let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList
- match h2 with
- | ((_,_),x) :: [] -> x
- | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" (PrintConst discr) str))
- | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" (PrintConst discr) str))
+ match discr with
+ | ObjLiteral(objName) ->
+ let h2 = heapInst.assignments |> Map.filter (fun (o,Var(fldName,_)) v -> o.name = objName && fldName = str) |> Map.toList
+ match h2 with
+ | ((_,_),x) :: [] -> x
+ | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName str))
+ | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName str)) // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???
+ | _ -> raise (EvalFailed(sprintf "Dot expression discriminator does not resolve to an object literal but %O" discr))
| _ -> failwith ("NOT IMPLEMENTED YET: " + (PrintExpr 0 expr))
(* --- function body starts here --- *)
- EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx) |> Const2Expr) expr
+ EvalSym (fun e -> __EvalResolver e) expr
+
+// =====================================================================
+/// Takes an unresolved model of the heap (HeapModel), resolves all
+/// references in the model and returns an instance of the heap
+/// (HeapInstance), where all fields for all objects have explicit
+/// assignments.
+// =====================================================================
+let ResolveModel hModel =
+ let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->
+ let objName, objType = match Resolve hModel o with
+ | ThisConst(_,t) -> "this", t;
+ | NewObj(name, t) -> PrintGenSym name, t
+ | _ -> failwith ("unresolved object ref: " + o.ToString())
+ let objType = objType |> Utils.ExtractOptionMsg "unknown object type"
+ let value = TryResolve hModel l |> Const2Expr
+ acc |> Map.add ({name = objName; objType = objType}, f) value
+ ) Map.empty
+ let argmap = hModel.env |> Map.fold (fun acc k v ->
+ match k with
+ | VarConst(name) -> acc |> Map.add name (Resolve hModel v)
+ | _ -> acc
+ ) Map.empty
+ { assignments = hmap;
+ methodArgs = argmap;
+ globals = Map.empty }
\ No newline at end of file diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index 886d5868..8c25726a 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -135,6 +135,12 @@ let ListReplace oldElem newElem lst = let ListContains elem lst =
lst |> List.exists (fun e -> e = elem)
+// ====================================================
+/// Removes all elements in lst that are equal to "elem"
+// ====================================================
+let ListRemove elem lst =
+ lst |> List.choose (fun e -> if e = elem then None else Some(e))
+
// ===============================================================
/// ensures: |ret| = max(|lst| - cnt, 0)
/// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]
@@ -194,6 +200,25 @@ let rec ListSet idx v lst = // =======================================
let rec MapAddAll map1 map2 =
map2 |> Map.fold (fun acc k v -> acc |> Map.add k v) map1
+
+// -------------------------------------------
+// ------------ algorithms -------------------
+// -------------------------------------------
+
+// =======================================================================
+/// Topologically sorts a given list
+///
+/// ensures: |ret| = |lst|
+/// ensures: forall e in lst :: e in ret
+/// ensures: forall i,j :: 0 <= i < j < ==> not (followsFunc ret[j] ret[i])
+// =======================================================================
+let rec TopSort followsFunc lst =
+ match lst with
+ | [] -> []
+ | fs :: [] -> [fs]
+ | fs :: rest ->
+ let min = rest |> List.fold (fun acc elem -> if followsFunc acc elem then elem else acc) fs
+ min :: TopSort followsFunc (ListRemove min lst)
// -------------------------------------------
// ------ string active patterns -------------
@@ -221,6 +246,12 @@ let IfDo2 cond func2 (a1,a2) = else
a1,a2
+let Ite cond f1 f2 =
+ if cond then
+ f1
+ else
+ f2
+
type CascadingBuilder<'a>(failVal: 'a) =
member this.Bind(v, f) =
match v with
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index e7f42ddc..63535a20 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -15,10 +15,10 @@ model List[T] { var root: Node[T] frame - root * root.list[*] + root invariant - (root = null) ==> (|list| = 0) + root = null ==> |list| = 0 root != null ==> list = root.list } @@ -40,7 +40,7 @@ model Node[T] { var next: Node[T] frame - data * next + next invariant next = null <==> list = [data] diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen index e99cf342..61fad148 100644 --- a/Jennisys/examples/List2.jen +++ b/Jennisys/examples/List2.jen @@ -27,7 +27,7 @@ model IntList { var root: IntNode frame - root * root.list[*] + root invariant root = null <==> |list| = 0 @@ -49,7 +49,7 @@ model IntNode { var next: IntNode frame - data * next + next invariant next = null ==> list = [data] diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen index acb10ad5..776bd43d 100644 --- a/Jennisys/examples/List3.jen +++ b/Jennisys/examples/List3.jen @@ -27,7 +27,7 @@ model IntList { var root: IntNode frame - root * root.list[*] + root invariant root = null ==> |list| = 0 @@ -63,7 +63,7 @@ model IntNode { var next: IntNode frame - data * next + next invariant next = null ==> |succ| = 0 diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen index 6404bfd6..2142738e 100644 --- a/Jennisys/examples/Set.jen +++ b/Jennisys/examples/Set.jen @@ -13,13 +13,14 @@ class Set { constructor Double(p: int, q: int) requires p != q ensures elems = {p q} + } model Set { var root: SetNode frame - root * root.elems[*] + root invariant root = null ==> elems = {} @@ -35,6 +36,10 @@ class SetNode { constructor Double(p: int, q: int) 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 SetNode { @@ -43,7 +48,7 @@ model SetNode { var right: SetNode frame - data * left * right + left * right invariant elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) |