diff options
Diffstat (limited to 'Jennisys')
| -rw-r--r-- | Jennisys/Analyzer.fs | 145 | ||||
| -rw-r--r-- | Jennisys/AstUtils.fs | 100 | ||||
| -rw-r--r-- | Jennisys/CodeGen.fs | 26 | ||||
| -rw-r--r-- | Jennisys/DafnyPrinter.fs | 1 | ||||
| -rw-r--r-- | Jennisys/Jennisys.fsproj | 2 | ||||
| -rw-r--r-- | Jennisys/Logger.fs | 2 | ||||
| -rw-r--r-- | Jennisys/Options.fs | 2 | ||||
| -rw-r--r-- | Jennisys/Printer.fs | 15 | ||||
| -rw-r--r-- | Jennisys/Utils.fs | 10 | ||||
| -rw-r--r-- | Jennisys/examples/Number.jen | 40 |
10 files changed, 251 insertions, 92 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index fa388b99..9603dd6e 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -12,6 +12,13 @@ open DafnyPrinter 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))
@@ -85,7 +92,8 @@ 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 expr args (heap,env,ctx) =
+let GetUnifications indent expr args (heap,env,ctx) =
+ 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
// - then it tries to evaluate it to a constant
@@ -96,7 +104,7 @@ let GetUnifications expr args (heap,env,ctx) = 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 (" - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));
+ Logger.DebugLine (idt + " - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));
return Map.add e v unifMap
}
// just recurses on all expressions
@@ -126,13 +134,14 @@ let GetUnifications expr args (heap,env,ctx) = /// Returns a map (Expr |--> Const) containing unifications
/// found for the given method and heap/env/ctx
// =======================================================
-let GetUnificationsForMethod comp m (heap,env,ctx) =
+let GetUnificationsForMethod indent comp m (heap,env,ctx) =
+ let idt = Indent indent
let rec GetArgValueUnifications args env =
match args with
| Var(name,_) :: rest ->
match Map.tryFind (Unresolved(name)) env with
| Some(c) ->
- Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name);
+ Logger.DebugLine (idt + " - adding unification " + (PrintConst c) + " <--> " + name);
Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)
| None -> failwith ("couldn't find value for argument " + name)
| [] -> Map.empty
@@ -142,7 +151,7 @@ let GetUnificationsForMethod comp m (heap,env,ctx) = let args = List.concat [ins; outs]
match args with
| [] -> Map.empty
- | _ -> GetUnifications (BinaryAnd pre post) args (heap,env,ctx)
+ | _ -> GetUnifications indent (BinaryAnd pre post) args (heap,env,ctx)
|> Utils.MapAddAll (GetArgValueUnifications args env)
| _ -> failwith ("not a method: " + m.ToString())
@@ -190,7 +199,8 @@ 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 prog comp mthd unifs (heap,env,ctx) conservative =
+let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservative =
+ let idt = Indent indent
let __CheckUnif o f e idx =
if not conservative || not Options.CONFIG.checkUnifications then
true
@@ -204,7 +214,7 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = | _ -> BinaryEq lhs e
// check if the assertion follows and if so update the env
let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)
- Logger.Debug (" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
+ Logger.Debug (idt + " - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))
if ok then
Logger.DebugLine " HOLDS"
@@ -214,13 +224,13 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = (* --- function body starts here --- *)
match unifs with
| (e,c) :: rest ->
- let restHeap,env,ctx = ApplyUnifications prog comp mthd rest (heap,env,ctx) conservative
+ 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 " - applied: %s.%s --> %s" (PrintConst o) (GetVarName f) (PrintExpr 0 e) )
+ //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"
@@ -230,7 +240,7 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = match lst with
| lstElem :: rest when lstElem = c ->
if __CheckUnif o f e cnt then
- Logger.TraceLine (sprintf " - applied: %s.%s[%d] --> %s" (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )
+ //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)
@@ -254,54 +264,33 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = // ====================================================================================
/// Returns whether the code synthesized for the given method can be verified with Dafny
// ====================================================================================
-let VerifySolution prog comp mthd (heap,env,ctx) =
+let VerifySolution prog comp mthd sol =
// print the solution to file and try to verify it with Dafny
- let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)
- let code = PrintImplCode prog solution (fun p -> [comp,mthd])
+ let solutions = Map.empty |> Map.add (comp,mthd) sol
+ let code = PrintImplCode prog solutions (fun p -> [comp,mthd])
CheckDafnyProgram code dafnyVerifySuffix
-let TryInferConditionals prog comp m unifs (heap,env,ctx) =
- let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false
- // get expressions to evaluate:
- // - add pre and post conditions
- // - go through all objects on the heap and assert its invariant
- 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 expr = heapObjs |> Set.fold (fun acc o ->
- let receiverOpt = GetObjRefExpr o (heap,env,ctx)
- 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"
- ) prepostExpr
- expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")
- // now evaluate and see what's left
- let c = Eval (heap2,env2,ctx2) false expr
- printfn "%s" (PrintExpr 0 c)
- Some(heap2,env2,ctx2)
-
// ============================================================================
/// Attempts to synthesize the initialization code for the given constructor "m"
///
/// Returns a (heap,env,ctx) tuple
// ============================================================================
-let AnalyzeConstructor prog comp m =
+let rec AnalyzeConstructor indent prog comp m =
+ let idt = Indent indent
let methodName = GetMethodName m
+ let pre,post = GetMethodPrePost m
// generate Dafny code for analysis first
let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral)
- Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m)))
- Logger.Info " - searching for an instance ..."
+ Logger.InfoLine (idt + "[*] Analyzing constructor")
+ Logger.InfoLine (idt + "------------------------------------------")
+ Logger.InfoLine (PrintMethodSignFull (indent + 4) m)
+ Logger.InfoLine (idt + "------------------------------------------")
+ Logger.Info (idt + " - searching for an instance ...")
let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))
if models.Count = 0 then
// no models means that the "assert false" was verified, which means that the spec is inconsistent
- Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!"
- None
+ Logger.WarnLine (idt + " !!! SPEC IS INCONSISTENT !!!")
+ []
else
if models.Count > 1 then
Logger.WarnLine " FAILED "
@@ -309,21 +298,65 @@ let AnalyzeConstructor prog comp m = Logger.InfoLine " OK "
let model = models.[0]
let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
- let unifs = GetUnificationsForMethod comp m (heap,env,ctx) |> Map.toList
- let heap,env,ctx = ApplyUnifications prog comp m unifs (heap,env,ctx) true
+ 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
if Options.CONFIG.verifySolutions then
- Logger.InfoLine " - verifying synthesized solution ... "
- let verified = VerifySolution prog comp m (heap,env,ctx)
- Logger.Info " "
+ Logger.InfoLine (idt + " - verifying synthesized solution ... ")
+ let sol = [TrueLiteral, (heap,env,ctx)]
+ let verified = VerifySolution prog comp m sol
+ Logger.Info (idt + " ")
if verified then
Logger.InfoLine "~~~ VERIFIED ~~~"
- Some(heap,env,ctx)
+ sol
else
Logger.InfoLine "!!! NOT VERIFIED !!!"
- Logger.InfoLine "Trying to infer conditionals"
- TryInferConditionals prog comp m unifs (heap,env,ctx)
+ Logger.InfoLine (idt + " Strengthening the pre-condition")
+ TryInferConditionals (indent + 4) prog comp m unifs (heap,env,ctx)
else
- Some(heap,env,ctx)
+ [TrueLiteral, (heap,env,ctx)]
+and TryInferConditionals indent prog comp m unifs (heap,env,ctx) =
+ let idt = Indent indent
+ let heap2,env2,ctx2 = ApplyUnifications indent prog comp m unifs (heap,env,ctx) false
+ // get expressions to evaluate:
+ // - add pre and post conditions
+ // - go through all objects on the heap and assert its invariant
+ 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 expr = heapObjs |> Set.fold (fun acc o ->
+ let receiverOpt = GetObjRefExpr o (heap,env,ctx)
+ 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"
+ ) 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
+ try
+ if newCond = TrueLiteral then
+ Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt)
+ []
+ 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
+ if verified then
+ Logger.InfoLine "VERIFIED"
+ let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(newCond))
+ sol.[0] :: AnalyzeConstructor (indent + 2) p3 c3 m3
+ else
+ Logger.InfoLine "NOT VERIFIED"
+ []
+ with
+ ex -> raise ex
let GetMethodsToAnalyze prog =
let mOpt = Options.CONFIG.methodToSynth;
@@ -365,11 +398,9 @@ let rec AnalyzeMethods prog members = | (comp,m) :: rest ->
match m with
| Method(_,_,_,_,true) ->
- let solOpt = AnalyzeConstructor prog comp m
+ let solOpt = AnalyzeConstructor 2 prog comp m
Logger.InfoLine ""
- match solOpt with
- | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
- | None -> AnalyzeMethods prog rest
+ AnalyzeMethods prog rest |> Map.add (comp,m) solOpt
| _ -> AnalyzeMethods prog rest
| [] -> Map.empty
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 2cfd38a1..25d2a129 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -19,6 +19,16 @@ let TrueLiteral = BoolLiteral(true) // =====================
let FalseLiteral = BoolLiteral(false)
+let UnaryNeg sub =
+ match sub with
+ | UnaryExpr("-", s) -> s
+ | _ -> UnaryExpr("-", sub)
+
+let UnaryNot sub =
+ match sub with
+ | UnaryExpr("!", s) -> s
+ | _ -> UnaryExpr("!", sub)
+
// =======================================================================
/// Returns a binary AND of the two given expressions with short-circuiting
// =======================================================================
@@ -49,7 +59,7 @@ let BinaryImplies lhs rhs = | BoolLiteral(false), _ -> FalseLiteral
| BoolLiteral(true), _ -> rhs
| _, BoolLiteral(true) -> lhs
- | _, BoolLiteral(false) -> UnaryExpr("!", lhs)
+ | _, BoolLiteral(false) -> UnaryNot(lhs)
| _ -> BinaryExpr(20, "==>", lhs, rhs)
@@ -312,6 +322,16 @@ let FindVar (prog: Program) clsName fldName = |> Utils.ListToOption
| None -> None
+let AddPrecondition prog comp m e =
+ match prog, comp, m with
+ | Program(clist), Component(Class(cname, ctypeParams, members), model, code), Method(mn, sgn, pre, post, cstr) ->
+ let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)
+ let newCls = Class(cname, ctypeParams, Utils.ListReplace m newMthd members)
+ let newComp = Component(newCls, model, code)
+ let newProg = Program(Utils.ListReplace comp newComp clist)
+ newProg, newComp, newMthd
+ | _ -> failwithf "Not a method: %O" m
+
////////////////////
exception EvalFailed of string
@@ -322,7 +342,23 @@ let DefaultFallbackResolver resolverFunc e = match resolverFunc e with
| Some(e') -> e'
| None -> e
-
+
+let __CheckEqual e1 e2 =
+ match e1, e2 with
+ | BoolLiteral(b1), BoolLiteral(b2) -> Some(b1 = b2)
+ | IntLiteral(n1), IntLiteral(n2) -> Some(n1 = n2)
+ | ObjLiteral(o1), ObjLiteral(o2) -> Some(o1 = o2)
+ | SetExpr(elist1), SetExpr(elist2) -> Some(Set.ofList elist1 = Set.ofList elist2)
+ | SequenceExpr(elist1), SequenceExpr(elist2) -> Some(elist1 = elist2)
+ | UnaryExpr("-", sub1), sub2
+ | sub1, UnaryExpr("-", sub2) when sub1 = sub2 -> Some(false)
+ | UnaryExpr("-", sub1), UnaryExpr("-", sub2) when sub1 = sub2 -> Some(true)
+ | UnaryExpr("!", sub1), sub2
+ | sub1, UnaryExpr("!", sub2) when sub1 = sub2 -> Some(false)
+ | UnaryExpr("!", sub1), UnaryExpr("-", sub2) when sub1 = sub2 -> Some(true)
+ | _ when e1 = e2 -> Some(true)
+ | _ -> None
+
let rec __EvalSym resolverFunc ctx expr =
match expr with
| IntLiteral(_) -> expr
@@ -369,23 +405,19 @@ let rec __EvalSym resolverFunc ctx expr = let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force()))
match op with
| "=" ->
- match e1'.Force(), e2'.Force() with
- | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)
- | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 = n2)
- | ObjLiteral(o1), ObjLiteral(o2) -> BoolLiteral(o1 = o2)
- | SetExpr(elist1), SetExpr(elist2) -> BoolLiteral(Set.ofList elist1 = Set.ofList elist2)
- | SequenceExpr(elist1), SequenceExpr(elist2) -> BoolLiteral(elist1 = elist2)
- | _ when e1'.Force() = e2'.Force() -> BoolLiteral(true)
- | _ -> recomposed.Force()
+ let e1'' = e1'.Force()
+ let e2'' = e2'.Force()
+ let eq = __CheckEqual e1'' e2''
+ match eq with
+ | Some(b) -> BoolLiteral(b)
+ | None -> recomposed.Force()
| "!=" ->
- match e1'.Force(), e2'.Force() with
- | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(not (b1 = b2))
- | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(not (n1 = n2))
- | ObjLiteral(o1), ObjLiteral(o2) -> BoolLiteral(not (o1 = o2))
- | SetExpr(elist1), SetExpr(elist2) -> BoolLiteral(not (Set.ofList elist1 = Set.ofList elist2))
- | SequenceExpr(elist1), SequenceExpr(elist2) -> BoolLiteral(not (elist1 = elist2))
- | _ when e1'.Force() = e2'.Force() -> BoolLiteral(false)
- | _ -> recomposed.Force()
+ let e1'' = e1'.Force()
+ let e2'' = e2'.Force()
+ let eq = __CheckEqual e1'' e2''
+ match eq with
+ | Some(b) -> BoolLiteral(not b)
+ | None -> recomposed.Force()
| "<" ->
match e1'.Force(), e2'.Force() with
| IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 < n2)
@@ -393,11 +425,16 @@ let rec __EvalSym resolverFunc ctx expr = | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))
| _ -> recomposed.Force()
| "<=" ->
- match e1'.Force(), e2'.Force() with
- | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2)
- | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
- | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
- | _ -> recomposed.Force()
+ let e1'' = e1'.Force()
+ let e2'' = e2'.Force()
+ let eq = __CheckEqual e1'' e2''
+ match eq with
+ | Some(true) -> TrueLiteral
+ | _ -> match e1'', e2'' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))
+ | _ -> recomposed.Force()
| ">" ->
match e1'.Force(), e2'.Force() with
| IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2)
@@ -405,11 +442,16 @@ let rec __EvalSym resolverFunc ctx expr = | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))
| _ -> recomposed.Force()
| ">=" ->
- match e1'.Force(), e2'.Force() with
- | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2)
- | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
- | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
- | _ -> recomposed.Force()
+ let e1'' = e1'.Force()
+ let e2'' = e2'.Force()
+ let eq = __CheckEqual e1'' e2''
+ match eq with
+ | Some(true) -> TrueLiteral
+ | _ -> match e1'', e2'' with
+ | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2)
+ | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
+ | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))
+ | _ -> recomposed.Force()
| "in" ->
match e1'.Force(), e2'.Force() with
| _, SetExpr(s)
@@ -480,6 +522,8 @@ let rec __EvalSym resolverFunc ctx expr = | "<==>" ->
match e1'.Force(), e2'.Force() with
| BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)
+ | x, BoolLiteral(b)
+ | BoolLiteral(b), x -> if b then x else UnaryNot(x)
| _ -> recomposed.Force()
| _ -> recomposed.Force()
| UnaryExpr(op, e) ->
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index f0e59d3b..5d7f8611 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -120,9 +120,27 @@ let PrintVarAssignments (heap,env,ctx) indent = acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline
) ""
-let PrintHeapCreationCode (heap,env,ctx) indent =
- (PrintAllocNewObjects (heap,env,ctx) indent) +
- (PrintVarAssignments (heap,env,ctx) indent)
+let rec PrintHeapCreationCode sol indent =
+ let idt = Indent indent
+ match sol with
+ | (c, (heap,env,ctx)) :: rest ->
+ if c = TrueLiteral then
+ (PrintAllocNewObjects (heap,env,ctx) indent) +
+ (PrintVarAssignments (heap,env,ctx) indent) +
+ newline +
+ (PrintHeapCreationCode rest indent)
+ 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)) +
+ idt + "} else {" + newline +
+ (PrintHeapCreationCode rest (indent+2)) +
+ idt + "}" + newline
+ else
+ (PrintAllocNewObjects (heap,env,ctx) indent) +
+ (PrintVarAssignments (heap,env,ctx) indent)
+ | [] -> ""
let GenConstructorCode mthd body =
let validExpr = IdLiteral("Valid()");
@@ -146,7 +164,7 @@ let PrintImplCode prog solutions methodsToPrintFunc = PrintDafnyCodeSkeleton prog (fun comp mthd ->
if Utils.ListContains (comp,mthd) methods then
let mthdBody = match Map.tryFind (comp,mthd) solutions with
- | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4
+ | Some(sol) -> PrintHeapCreationCode sol 4
| _ -> " //unable to synthesize" + newline
(GenConstructorCode mthd mthdBody) + newline
else
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index a467330b..d1dc73fc 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -21,6 +21,7 @@ let rec PrintExpr ctx expr = | IdLiteral(id) -> id | Star -> assert false; "" // I hope this won't happen | 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 op = diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 832176fd..5e1bea61 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\Set.jen /method:Set.Double /noCheckUnifs</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Number.jen /method:Number.Abs /checkUnifs</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs index 2801354d..09b576fd 100644 --- a/Jennisys/Logger.fs +++ b/Jennisys/Logger.fs @@ -16,7 +16,7 @@ let _WARN = 40 let _ERROR = 20
let _NONE = 0
-let logLevel = _ALL
+let logLevel = _DEBUG
let Log level msg =
if logLevel >= level then
diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 4a1487ce..a03f7213 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -20,7 +20,7 @@ let defaultConfig: Config = { inputFilename = "";
methodToSynth = "*";
verifySolutions = true;
- checkUnifications = true;
+ checkUnifications = false;
timeout = 0;
}
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index 81fde2cd..e051492f 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -41,6 +41,7 @@ let rec PrintExpr ctx expr = | 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 @@ -130,6 +131,20 @@ let PrintDecl d = | 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) ->
+ let mc = if isConstr then "constructor" else "method"
+ let preStr = (__PrintPrePost (idt + " requires ") pre)
+ let postStr = (__PrintPrePost (idt + " ensures ") post)
+ 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 diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index b7db5706..886d5868 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -119,6 +119,16 @@ let rec GenList n e = else
e :: (GenList (n-1) e)
+// =======================================
+/// ensures: forall i :: 0 <= i < |lst| ==>
+/// if lst[i] = oldElem then
+/// ret[i] = newElem
+/// else
+/// ret[i] = lst[i]
+// =======================================
+let ListReplace oldElem newElem lst =
+ lst |> List.choose (fun e -> if e = oldElem then Some(newElem) else Some(e))
+
// ==========================
/// ensures: ret = elem in lst
// ==========================
diff --git a/Jennisys/examples/Number.jen b/Jennisys/examples/Number.jen new file mode 100644 index 00000000..75417168 --- /dev/null +++ b/Jennisys/examples/Number.jen @@ -0,0 +1,40 @@ +class Number { + var num: int + + constructor Init(p: int) + ensures num = p + + constructor Double(p: int) + ensures num = 2*p + + constructor Sum(a: int, b: int) + ensures num = a + b + + constructor Min2(a: int, b: int) + ensures a < b ==> num = a + ensures a >= b ==> num = b + + constructor Min22(a: int, b: int) + ensures num in {a b} + ensures num <= a && num <= b + + constructor Min3(a: int, b: int, c: int) + ensures num in {a b c} + ensures num <= a && num <= b && num <= c + + constructor MinSum(a: int, b: int, c: int) + ensures num in {a+b a+c b+c} + ensures num <= a+b && num <= b+c && num <= a+c + + constructor Min4(a: int, b: int, c: int, d: int) + ensures num in {a b c d} + ensures num <= a && num <= b && num <= c && num <= d + + constructor Abs(a: int) + ensures a < 0 ==> num = -a + ensures a >= 0 ==> num = a +} + +model Number { + +}
\ No newline at end of file |