From 8911e5c95d4715c2e2626aef67f19793d6f43201 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 4 Oct 2012 13:32:50 -0700 Subject: Put all sources under \Source directory --- Source/Jennisys/Analyzer.fs | 953 ++++++++++++++++++ Source/Jennisys/Ast.fs | 95 ++ Source/Jennisys/AstUtils.fs | 1033 ++++++++++++++++++++ Source/Jennisys/CodeGen.fs | 429 ++++++++ Source/Jennisys/DafnyModelUtils.fs | 455 +++++++++ Source/Jennisys/DafnyPrinter.fs | 135 +++ Source/Jennisys/EnvUtils.fs | 9 + Source/Jennisys/FixpointSolver.fs | 374 +++++++ Source/Jennisys/Getters.fs | 284 ++++++ Source/Jennisys/Jennisys.fs | 72 ++ Source/Jennisys/Jennisys.fsproj | 118 +++ Source/Jennisys/Lexer.fsl | 83 ++ Source/Jennisys/Logger.fs | 41 + Source/Jennisys/MethodUnifier.fs | 107 ++ Source/Jennisys/Modularizer.fs | 206 ++++ Source/Jennisys/Options.fs | 162 +++ Source/Jennisys/Parser.fsy | 214 ++++ Source/Jennisys/PipelineUtils.fs | 63 ++ Source/Jennisys/PrintUtils.fs | 12 + Source/Jennisys/Printer.fs | 156 +++ Source/Jennisys/README.txt | 28 + Source/Jennisys/Resolver.fs | 380 +++++++ Source/Jennisys/SymGen.fs | 9 + Source/Jennisys/TypeChecker.fs | 67 ++ Source/Jennisys/Utils.fs | 368 +++++++ Source/Jennisys/examples/BHeap.jen | 33 + Source/Jennisys/examples/DList.jen | 39 + Source/Jennisys/examples/List.jen | 77 ++ Source/Jennisys/examples/List2.jen | 68 ++ Source/Jennisys/examples/List3.jen | 71 ++ Source/Jennisys/examples/Number.jen | 44 + Source/Jennisys/examples/NumberMethods.jen | 40 + Source/Jennisys/examples/Set.jen | 72 ++ Source/Jennisys/examples/Set2.jen | 60 ++ Source/Jennisys/examples/Simple.jen | 31 + Source/Jennisys/examples/jennisys-synth_List.dfy | 147 +++ Source/Jennisys/examples/jennisys-synth_List2.dfy | 207 ++++ Source/Jennisys/examples/jennisys-synth_List3.dfy | 255 +++++ Source/Jennisys/examples/jennisys-synth_Number.dfy | 202 ++++ Source/Jennisys/examples/jennisys-synth_Set.dfy | 344 +++++++ .../Jennisys/examples/mod/jennisys-synth_List.dfy | 202 ++++ .../Jennisys/examples/mod/jennisys-synth_List2.dfy | 323 ++++++ .../Jennisys/examples/mod/jennisys-synth_List3.dfy | 393 ++++++++ .../examples/mod/jennisys-synth_Number.dfy | 233 +++++ .../Jennisys/examples/mod/jennisys-synth_Set.dfy | 388 ++++++++ .../examples/mod2/jennisys-synth_DList.dfy | 255 +++++ .../Jennisys/examples/mod2/jennisys-synth_List.dfy | 249 +++++ .../examples/mod2/jennisys-synth_List2.dfy | 225 +++++ .../examples/mod2/jennisys-synth_List3.dfy | 309 ++++++ .../examples/mod2/jennisys-synth_Number.dfy | 181 ++++ .../examples/mod2/jennisys-synth_NumberMethods.dfy | 167 ++++ .../Jennisys/examples/mod2/jennisys-synth_Set.dfy | 304 ++++++ Source/Jennisys/examples/oopsla12/BHeap.jen | 34 + Source/Jennisys/examples/oopsla12/BHeap_synth.dfy | 220 +++++ Source/Jennisys/examples/oopsla12/DList.jen | 40 + Source/Jennisys/examples/oopsla12/DList_synth.dfy | 154 +++ Source/Jennisys/examples/oopsla12/IntSet.jen | 30 + Source/Jennisys/examples/oopsla12/IntSet_synth.dfy | 130 +++ Source/Jennisys/examples/oopsla12/List.jen | 29 + Source/Jennisys/examples/oopsla12/List_synth.dfy | 146 +++ Source/Jennisys/examples/oopsla12/Math.jen | 20 + Source/Jennisys/examples/oopsla12/Math_synth.dfy | 105 ++ Source/Jennisys/examples/set.dfy | 246 +++++ Source/Jennisys/scripts/StartDafny-jen.bat | 2 + 64 files changed, 11928 insertions(+) create mode 100644 Source/Jennisys/Analyzer.fs create mode 100644 Source/Jennisys/Ast.fs create mode 100644 Source/Jennisys/AstUtils.fs create mode 100644 Source/Jennisys/CodeGen.fs create mode 100644 Source/Jennisys/DafnyModelUtils.fs create mode 100644 Source/Jennisys/DafnyPrinter.fs create mode 100644 Source/Jennisys/EnvUtils.fs create mode 100644 Source/Jennisys/FixpointSolver.fs create mode 100644 Source/Jennisys/Getters.fs create mode 100644 Source/Jennisys/Jennisys.fs create mode 100644 Source/Jennisys/Jennisys.fsproj create mode 100644 Source/Jennisys/Lexer.fsl create mode 100644 Source/Jennisys/Logger.fs create mode 100644 Source/Jennisys/MethodUnifier.fs create mode 100644 Source/Jennisys/Modularizer.fs create mode 100644 Source/Jennisys/Options.fs create mode 100644 Source/Jennisys/Parser.fsy create mode 100644 Source/Jennisys/PipelineUtils.fs create mode 100644 Source/Jennisys/PrintUtils.fs create mode 100644 Source/Jennisys/Printer.fs create mode 100644 Source/Jennisys/README.txt create mode 100644 Source/Jennisys/Resolver.fs create mode 100644 Source/Jennisys/SymGen.fs create mode 100644 Source/Jennisys/TypeChecker.fs create mode 100644 Source/Jennisys/Utils.fs create mode 100644 Source/Jennisys/examples/BHeap.jen create mode 100644 Source/Jennisys/examples/DList.jen create mode 100644 Source/Jennisys/examples/List.jen create mode 100644 Source/Jennisys/examples/List2.jen create mode 100644 Source/Jennisys/examples/List3.jen create mode 100644 Source/Jennisys/examples/Number.jen create mode 100644 Source/Jennisys/examples/NumberMethods.jen create mode 100644 Source/Jennisys/examples/Set.jen create mode 100644 Source/Jennisys/examples/Set2.jen create mode 100644 Source/Jennisys/examples/Simple.jen create mode 100644 Source/Jennisys/examples/jennisys-synth_List.dfy create mode 100644 Source/Jennisys/examples/jennisys-synth_List2.dfy create mode 100644 Source/Jennisys/examples/jennisys-synth_List3.dfy create mode 100644 Source/Jennisys/examples/jennisys-synth_Number.dfy create mode 100644 Source/Jennisys/examples/jennisys-synth_Set.dfy create mode 100644 Source/Jennisys/examples/mod/jennisys-synth_List.dfy create mode 100644 Source/Jennisys/examples/mod/jennisys-synth_List2.dfy create mode 100644 Source/Jennisys/examples/mod/jennisys-synth_List3.dfy create mode 100644 Source/Jennisys/examples/mod/jennisys-synth_Number.dfy create mode 100644 Source/Jennisys/examples/mod/jennisys-synth_Set.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_DList.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_List.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_List2.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_List3.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_Number.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy create mode 100644 Source/Jennisys/examples/mod2/jennisys-synth_Set.dfy create mode 100644 Source/Jennisys/examples/oopsla12/BHeap.jen create mode 100644 Source/Jennisys/examples/oopsla12/BHeap_synth.dfy create mode 100644 Source/Jennisys/examples/oopsla12/DList.jen create mode 100644 Source/Jennisys/examples/oopsla12/DList_synth.dfy create mode 100644 Source/Jennisys/examples/oopsla12/IntSet.jen create mode 100644 Source/Jennisys/examples/oopsla12/IntSet_synth.dfy create mode 100644 Source/Jennisys/examples/oopsla12/List.jen create mode 100644 Source/Jennisys/examples/oopsla12/List_synth.dfy create mode 100644 Source/Jennisys/examples/oopsla12/Math.jen create mode 100644 Source/Jennisys/examples/oopsla12/Math_synth.dfy create mode 100644 Source/Jennisys/examples/set.dfy create mode 100644 Source/Jennisys/scripts/StartDafny-jen.bat (limited to 'Source/Jennisys') diff --git a/Source/Jennisys/Analyzer.fs b/Source/Jennisys/Analyzer.fs new file mode 100644 index 00000000..db4887ed --- /dev/null +++ b/Source/Jennisys/Analyzer.fs @@ -0,0 +1,953 @@ +module Analyzer + +open Ast +open Getters +open AstUtils +open CodeGen +open DafnyModelUtils +open DafnyPrinter +open FixpointSolver +open MethodUnifier +open Modularizer +open Options +open PipelineUtils +open PrintUtils +open Resolver +open TypeChecker +open Utils + +open Microsoft.Boogie + +let Rename suffix vars = + vars |> List.map (function Var(nm,tp,old) -> nm, Var(nm + suffix, tp, old)) + +let ReplaceName substMap nm = + match Map.tryFind nm substMap with + | Some(Var(name,_,_)) -> name + | None -> nm + +let rec Substitute substMap = function + | IdLiteral(s) -> IdLiteral(ReplaceName substMap s) + | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f) + | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e) + | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1) + | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1) + | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2) + | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee) + | SeqLength(e) -> SeqLength(Substitute substMap e) + | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) + | expr -> expr + +let GenMethodAnalysisCode comp m assertion genOld = + let methodName = GetMethodName m + let signature = GetMethodSig m + let ppre,ppost = GetMethodPrePost m + let pre = Desugar ppre + let post = Desugar ppost |> RewriteOldExpr + let ghostPre = GetMethodGhostPrecondition m |> Desugar + //let sigStr = PrintSig signature + let sigVarsDecl = + match signature with + | Sig(ins,outs) -> ins @ outs |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "" + + " method " + methodName + "()" + newline + + " modifies this;" + newline + + " {" + newline + + // print signature as local variables + sigVarsDecl + + " // assume precondition" + newline + + " assume " + (PrintExpr 0 pre) + ";" + newline + + " // assume ghost precondition" + newline + + " assume " + (PrintExpr 0 ghostPre) + ";" + newline + + " // assume invariant and postcondition" + newline + + " assume Valid();" + newline + + (if genOld then " assume Valid_old();" + newline else "") + + " assume " + (PrintExpr 0 post) + ";" + newline + + " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + + (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline + + // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible + " // assert false to search for a model satisfying the assumed constraints" + newline + + " assert " + (PrintExpr 0 assertion) + ";" + newline + + " }" + newline + +let rec MethodAnalysisPrinter onlyForThese assertion genOld comp = + let cname = GetComponentName comp + match onlyForThese with + | (c,m) :: rest when GetComponentName c = cname -> + match m with + | Method(_) -> + (GenMethodAnalysisCode c m assertion genOld) + newline + + (MethodAnalysisPrinter rest assertion genOld comp) + | _ -> "" + | _ :: rest -> MethodAnalysisPrinter rest assertion genOld comp + | [] -> "" + +// ========================================================================= +/// For a given constant "objRefName" (which is an object, something like +/// "gensym32"), finds a path of field references from "this" (e.g. something +/// like "this.next.next"). +/// +/// Implements a backtracking search over the heap entries to find that +/// path. It starts from the given object, and follows the backpointers +/// until it reaches the root ("this") +// ========================================================================= +// let objRef2ExprCache = new System.Collections.Generic.Dictionary() +let GetObjRefExpr objRefName (heapInst: HeapInstance) = + let rec __GetObjRefExpr objRefName visited = + if Set.contains objRefName visited then + None + else + let newVisited = Set.add objRefName visited + match objRefName with + | "this" -> Some(ObjLiteral("this")) + | _ -> + let rec __fff lst = + match lst with + | ((o,var),_) :: rest -> + match __GetObjRefExpr o.name newVisited with + | Some(expr) -> Some(Dot(expr, GetExtVarName var)) + | None -> __fff rest + | [] -> None + let backPointers = heapInst.concreteValues |> List.choose (function + FieldAssignment (x,l) -> + if l = ObjLiteral(objRefName) then Some(x,l) else None + |_ -> None) + __fff backPointers + (* --- function body starts here --- *) + __GetObjRefExpr objRefName (Set.empty) +// THIS DOESN'T WORK BECAUSE THE CACHE HAS TO BE PURGED AFTER EVERY METHOD +// if objRef2ExprCache.ContainsKey(objRefName) then +// Some(objRef2ExprCache.[objRefName]) +// else +// let res = __GetObjRefExpr objRefName (Set.empty) +// match res with +// | Some(e) -> objRef2ExprCache.Add(objRefName, e) +// | None -> () +// res + +// ============================================================================= +/// Returns an expression that combines the post-condition of a given method with +/// invariants for all objects present on the heap +// ============================================================================= +let GetHeapExpr prog mthd heapInst includePreState = + // get expressions to evaluate: + // - add post (and pre?) conditions + // - go through all objects on the heap and assert their invariants + let pre,post = GetMethodPrePost mthd + let prepostExpr = post //TODO: do we need the "pre" here as well? + let heapObjs = heapInst.assignments |> List.fold (fun acc asgn -> + match asgn with + | FieldAssignment((o,_),_) -> acc |> Set.add o + | _ -> acc) Set.empty + heapObjs |> Set.fold (fun acc o -> + let receiverOpt = GetObjRefExpr o.name heapInst + let receiver = Utils.ExtractOption receiverOpt + let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption + let objInvs = GetInvariantsAsList objComp + let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver) + let objInvFinal = objInvsUpdated |> List.fold BinaryAnd TrueLiteral + let objAllInvs = + if includePreState then + let objInvPre = MakeOld objInvFinal + BinaryAnd objInvFinal objInvPre + else + objInvFinal + BinaryAnd prepostExpr objAllInvs + ) prepostExpr + +let IsUnmodConcrOnly prog (comp,meth) expr = + let isConstr = IsModifiableObj (ThisObj comp) (comp,meth) + let rec __IsUnmodOnly args expr = + let __IsUnmodOnlyLst elist = + elist |> List.fold (fun acc e -> acc && (__IsUnmodOnly args e)) true + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarDeclExpr(_) + | ObjLiteral(_) -> true + | VarLiteral(id) -> args |> List.exists (fun var -> GetExtVarName var = id) + | IdLiteral("null") | IdLiteral("this") -> true + | IdLiteral(id) -> + not (isConstr || IsAbstractField comp id) + | Dot(e, fldName) -> //if isConstr then false else __IsUnmodOnlyLst [e] + if isConstr then + false + else + // assume it is unmodifiable, because it is a method, so just check if it's concrete + let lhsType = InferType prog comp (MethodArgChecker prog meth) e |> Utils.ExtractOptionMsg (sprintf "Inference failed for %s" (PrintExpr 0 e)) + IsConcreteField lhsType fldName + | AssertExpr(e) + | AssumeExpr(e) + | SeqLength(e) + | LCIntervalExpr(e) + | MethodOutSelect(e,_) + | OldExpr(e) + | UnaryExpr(_,e) -> __IsUnmodOnlyLst [e] + | SelectExpr(e1, e2) + | BinaryExpr(_,_,e1,e2) -> __IsUnmodOnlyLst [e1; e2] + | IteExpr(e3, e1, e2) + | UpdateExpr(e1, e2, e3) -> __IsUnmodOnlyLst [e1; e2; e3] + | SequenceExpr(exprs) | SetExpr(exprs) -> __IsUnmodOnlyLst exprs + | MethodCall(rcv,_,_,aparams) -> __IsUnmodOnlyLst (rcv :: aparams) + | ForallExpr(vars,e) -> __IsUnmodOnly (args @ vars) e + (* --- function body starts here --- *) + __IsUnmodOnly (GetMethodInArgs meth) expr + +let AddUnif indent e v unifMap = + let idt = Indent indent + let builder = new CascadingBuilder<_>(unifMap) + builder { + let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption + Logger.DebugLine (idt + " - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v)) + return Map.add e v unifMap + } + +//TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const" +let rec GetUnifications prog indent (comp,meth) heapInst unifs expr = + let idt = Indent indent + // - first looks if the give expression talks only about method arguments (args) + // - then it tries to evaluate it to a constant + // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map + let __AddUnif e unifsAcc = + if IsConstExpr e then + unifsAcc + else + let builder = new CascadingBuilder<_>(unifsAcc) + builder { + let! argsOnly = IsUnmodConcrOnly prog (comp,meth) e |> Utils.BoolToOption + let! v = try Some(EvalFull heapInst e |> Expr2Const) with ex -> None + return AddUnif indent e v unifsAcc + } + (* --- function body starts here --- *) + AstUtils.DescendExpr2 __AddUnif expr unifs + +// ======================================================= +/// Returns a map (Expr |--> Const) containing unifications +/// found for the given method wrt to heapInst. +/// +/// The list of potential unifications include: +/// (1) arg-value pairs for all method arguments, +/// (2) field-value pairs for all unmodifiable fields, +/// (3) expr-value pairs where expr are unmodifiable +/// expressions found in the spec. +// ======================================================= +let GetUnificationsForMethod indent prog comp m heapInst = + let idt = Indent indent + let rec GetArgValueUnifications args = + match args with + | var :: rest -> + let name = GetExtVarName var + match Map.tryFind name heapInst.methodArgs with + | Some(c) -> + GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c + | None -> failwith ("couldn't find value for argument " + name) + | [] -> Map.empty + let rec GetFldValueUnifications unifs = + heapInst.assignments |> List.fold (fun acc asgn -> + match asgn with + | FieldAssignment((obj,var), fldVal) -> + try + let vname = GetExtVarName var + let comp = obj.objType |> FindComponentForType prog |> Utils.ExtractOption + if IsConcreteField comp vname then + let path = GetObjRefExpr obj.name heapInst |> Utils.ExtractOption + let c = Expr2Const fldVal + AddUnif indent (Dot(path, vname)) c acc + else + acc + with + | ex -> + Logger.WarnLine ("[WARN]: error during getting field value unifications: " + ex.Message) + acc + | _ -> acc + ) unifs + + (* --- function body starts here --- *) + let unifs = GetArgValueUnifications (GetMethodInArgs m) + let unifs = + //TODO: it should really read the "modifies" clause and figure out modifiable fields from there + if not (IsConstructor m) then + GetFldValueUnifications unifs + else + unifs + GetUnifications prog indent (comp,m) heapInst unifs (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x)) + +// ======================================================= +/// Applies given unifications onto a given heapInstance +/// +/// 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 heapInst conservative = + let idt = Indent indent + /// + let __CheckUnif o f e idx = + if not conservative || not Options.CONFIG.checkUnifications then + true + else + let lhs = if o = NoObj then + VarLiteral(GetVarName f) + else + let objRefExpr = GetObjRefExpr o.name heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o.name) + let fldName = GetVarName f + Dot(objRefExpr, fldName) + let assertionExpr = match GetVarType f with + | Some(SeqType(_)) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e + | Some(SetType(_)) when not (idx = -1) -> BinaryIn e lhs + | _ -> BinaryEq lhs e + // check if the assertion follows and if so update the env + let genOld = false + let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,mthd] assertionExpr genOld) true genOld + Logger.Debug (idt + " - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") + let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) + if ok then + Logger.DebugLine " HOLDS" + else + Logger.DebugLine " DOESN'T HOLD" + ok + /// + let __Apply (o,f) c e value= + if value = Const2Expr 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) ) + e + else + value + else + let rec __UnifyOverLst lst cnt = + match lst with + | lstElem :: rest when lstElem = Const2Expr 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) ) + 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 + SequenceExpr(newExprList) + | SetExpr(elist) -> + let newExprList = __UnifyOverLst elist 0 + SetExpr(newExprList) + | _ -> + value + + (* --- function body starts here --- *) + match unifs with + | (e,c) :: rest -> + let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative + let newHeap = heapInst.assignments|> List.fold (fun acc asgn -> + match asgn with + | FieldAssignment((o,f),value) when heapInst.modifiableObjs |> Set.contains o -> + let e2 = __Apply (o,f) c e value + acc @ [FieldAssignment((o,f),e2)] + | _ -> acc @ [asgn] + ) [] + let newRetVals = heapInst.methodRetVals |> Map.fold (fun acc key value -> + let e2 = __Apply (NoObj,Var(key, None, false)) c e value + acc |> Map.add key e2 + ) Map.empty + {heapInst with assignments = newHeap; methodRetVals = newRetVals} + | [] -> heapInst + +// ==================================================================================== +/// Returns whether the code synthesized for the given method can be verified with Dafny +// ==================================================================================== +let VerifySolution prog solutions genRepr = + // print the solution to file and try to verify it with Dafny + //let prog = Program(solutions |> Utils.MapKeys |> Map.ofList |> Utils.MapKeys) + let code = PrintImplCode prog solutions genRepr false + CheckDafnyProgram code dafnyVerifySuffix + +let rec DiscoverAliasing exprList heapInst = + match exprList with + | e1 :: rest -> + let eqExpr = rest |> List.fold (fun acc e -> + if EvalFull heapInst (BinaryEq e1 e) = TrueLiteral then + BinaryAnd acc (BinaryEq e1 e) + else + acc + ) TrueLiteral + BinaryAnd eqExpr (DiscoverAliasing rest heapInst) + | [] -> TrueLiteral + +// +let DontResolveUnmodifiableStuff prog comp meth expr = + let methodArgs = GetMethodInArgs meth + let __IsMethodArg argName = methodArgs |> List.exists (fun var -> GetExtVarName var = argName) + let isMod = IsModifiableObj (ThisObj comp) (comp,meth) + match expr with + | VarLiteral(id) when __IsMethodArg id -> false + | IdLiteral(id) when id = "this" || id = "null" -> true + | IdLiteral(id) | Dot(_, id) -> + // this must be a field, so resolve it only if modifiable + isMod + | _ -> true + +/// Descends down a given expression and returns bunch of sub-expressions that all evaluate to true +let FindClauses trueOnly resolverFunc heapInst expr = + let MyFun expr acc = + try + match expr with + // skip binary logical operators because we want to find smallest sub-expressions + | BinaryExpr(_,op,_,_) when IsLogicalOp op -> acc + | _ -> + let exprEval = Eval heapInst resolverFunc expr + match exprEval with + | _ when exprEval = TrueLiteral -> acc + | _ -> + let exprAllResolved = EvalFull heapInst expr + match exprAllResolved with + | BoolLiteral(true) -> acc @ (exprEval |> SplitIntoConjunts) + | BoolLiteral(false) -> acc //if trueOnly then acc else acc @ (UnaryNot exprEval |> SplitIntoConjunts) + | _ -> acc + with + | _ -> acc + (* --- function body starts here --- *) + DescendExpr2 MyFun expr [] + +/// Descends down a given expression and returns all sub-expressions that evaluate to TrueLiteral +let FindTrueClauses resolverFunc heapInst expr = + FindClauses true resolverFunc heapInst expr + +/// Returns a list of boolean expressions obtained by combining (in some way) +/// the two given list of conditions conditions +let GetAllPossibleConditions specConds argConds aliasingConds = + let __Conjoin lst = lst |> List.fold (fun acc e -> BinaryAnd acc e) TrueLiteral + let __Preproc lst = lst |> List.map SplitIntoConjunts |> List.concat |> Utils.ListDeduplicate + + // 0. aliasing conditions + // 1. conjunction of spec conditions + // 2. individual arg conditions + // 3. conjunction of arg conditions + // 4. individual spec conditions + let aliasing = aliasingConds |> __Preproc + let specIndi = specConds |> __Preproc + let specConj = [__Conjoin specIndi] + let argsIndi = argConds |> __Preproc + let argsConj = [__Conjoin argsIndi] + + let allConds = aliasing @ specConj @ argsIndi @ specIndi @ argsConj + allConds |> List.filter (fun e -> not (e = TrueLiteral)) + |> Utils.ListDeduplicate + +// check whther a given solution (in the form of heapInst) verifies assuming a given guard +let rec CheckGuard prog comp m candCond indent idt heapInst callGraph = + let rec __MinGuard guard idx m2 sol = + let conjs = SplitIntoConjunts guard + let len = List.length conjs + if idx >= 0 && idx < len && len > 1 then + let guard' = conjs |> Utils.ListRemoveIdx (len - idx - 1) |> List.fold BinaryAnd TrueLiteral + match CheckGuard prog comp m guard' indent idt heapInst callGraph with + | Some(x) -> x + | None -> __MinGuard guard (idx+1) m2 sol + else + guard, m2, sol + + let m2 = AddPrecondition m candCond + let sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph + Logger.Info (idt + " - verifying partial solution ... ") + let verified = + if Options.CONFIG.verifyPartialSolutions then + VerifySolution prog sol Options.CONFIG.genRepr + else + true + if verified then + if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" + if Options.CONFIG.minimizeGuards then + Logger.InfoLine(idt + " - minimizing guard ... " + (PrintExpr 0 candCond)) + Some(__MinGuard candCond 0 m2 sol) + else + Some(candCond,m2,sol) + else + Logger.InfoLine ("NOT VERIFIED") + None + +// iteratively tries to remove conjunts and check whether the solutions still verifies +//let MinimizeGuard guard prog comp m heapInst callGraph indent = + + +// ============================================================================ +/// Attempts to synthesize the initialization code for the given constructor "m" +/// +/// Returns a (heap,env,ctx) tuple +// ============================================================================ +let rec AnalyzeConstructor indent prog comp m callGraph = + let idt = Indent indent + let TryFindAndVerify m = + match TryFindExistingAndConvertToSolution indent comp m TrueLiteral callGraph with + | Some(sol) -> + if VerifySolution prog sol Options.CONFIG.genRepr then + Logger.InfoLine (idt + " ~~~ VERIFIED ~~~") + Some(sol) + else + Logger.InfoLine (idt + " !!! NOT VERIFIED !!!") + None + | None -> None + + (* --- function body starts here --- *) + Logger.InfoLine (idt + "[*] Analyzing constructor") + Logger.InfoLine (idt + "------------------------------------------") + Logger.InfoLine (Printer.PrintMethodSignFull (indent + 4) comp m) + Logger.InfoLine (idt + "------------------------------------------") + match TryFindAndVerify m with + | Some(sol) -> sol + | None -> + let methodName = GetMethodName m + let pre,post = GetMethodPrePost m + // generate Dafny code for analysis first + let genOld = true + let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral genOld) true genOld + 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 (idt + " !!! SPEC IS INCONSISTENT !!!") + Map.empty + else + if models.Count > 1 then + Logger.WarnLine " FAILED " + failwith "internal error (more than one model for a single constructor analysis)" + Logger.InfoLine " OK " + let model = models.[0] + let hModel = ReadFieldValuesFromModel model prog comp m + let heapInst = ResolveModel hModel (comp,m) + let unifs = GetUnificationsForMethod indent prog comp m heapInst |> Map.toList + let heapInst = ApplyUnifications indent prog comp m unifs heapInst true + + // split into method calls + let sol = MakeModular indent prog comp m TrueLiteral heapInst callGraph |> FixSolution comp m + + if Options.CONFIG.verifySolutions then + Logger.InfoLine (idt + " - verifying synthesized solution ... ") + let verified = VerifySolution prog sol Options.CONFIG.genRepr + Logger.Info (idt + " ") + if verified then + Logger.InfoLine "~~~ VERIFIED ~~~" + sol + else + Logger.InfoLine "!!! NOT VERIFIED !!!" + if Options.CONFIG.inferConditionals then + TryRecursion (indent + 4) prog comp m unifs heapInst callGraph + else + sol + else + sol +and TryRecursion indent prog comp m unifs heapInst callGraph = + let idt = Indent indent + + /// checks whether an expression is ok, meaning + /// - only immediate concrete fields of the "this" object are used, + /// - no recursion on the same object with the same parameters + let __IsOk hInst expr = + let compName = GetComponentName comp + let methName = GetMethodName m + let myVisitor = + fun expr acc -> + if not acc then + false + else + match expr with + | Dot(discr, fldName) -> + let obj = EvalFull heapInst discr + match obj with + | ObjLiteral(id) when id = "this" -> + try + let fname = RenameFromOld fldName + IsConcreteField (InferType prog comp (MethodArgChecker prog m) discr |> Utils.ExtractOption) fname + with + | _ -> false + | ObjLiteral(id) -> false + | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral" + | MethodCall(receiver, cn, mn, elst) when receiver = ThisLiteral && cn = compName && mn = methName -> + elst |> List.exists (function VarLiteral(_) -> false | _ -> true) + | _ -> true + DescendExpr2 myVisitor expr true + + /// Finds all modifiable fields in a given hInst, and checks if an "ok" + /// expression exists for each one of them. + /// + /// Returns all possible combinations of "ok" solutions (these are not verified yet). + let __GetAllAssignments hInst premises = + let rec __IterVars vars = + match vars with + | lhs :: [] -> + let lhsOptions = premises |> Set.toList + |> List.choose (function + | BinaryExpr(_,"=",l,r) -> if l = lhs then Some(r) elif r = lhs then Some(l) else None + | _ -> None) + |> List.filter (__IsOk hInst) + |> List.map (fun e -> [lhs,e]) + lhsOptions + | lhs :: rest -> + let lhsOptions = __IterVars [lhs] + if List.isEmpty lhsOptions then + List.empty + else + let restOptions = __IterVars rest + Utils.ListCombine (fun t1 t2 -> t1 @ t2) lhsOptions restOptions + | [] -> List.empty + + let stmts = ConvertToStatements hInst true + let modVars = stmts |> List.choose (function + | Assign(lhs,_) -> Some(lhs) + | _ -> None) + __IterVars modVars + + /// Print a given list of assignments + let rec __PrintSol indent s = + let idt = Indent indent + match s with + | (l,r) :: [] -> + sprintf "%s%s := %s" idt (PrintExpr 0 l) (PrintExpr 0 r) + | (l,r) :: rest -> + let str = __PrintSol indent [l,r] + str + newline + (__PrintSol indent rest) + | [] -> "" + + /// Returns a given method's postcondition where + /// - all input variables are renamed so that their names start with "$" and + /// (so that the unifier know that it's ok to try to unify those variables) + /// - all output variables are rewritten as $this.()[""] + /// (so that it is clear that they are results of a method call) + let __GetMethodPostTemplate comp m = + let compName = GetComponentName comp + let methName = GetMethodName m + let ins = GetMethodInArgs m + let outs = GetMethodOutArgs m + let post = GetMethodPrePost m |> snd + post |> RewriteWithCtx (fun ctx e -> + match e with + | VarLiteral(id) when not (IsInVarList ctx id) -> + if IsInVarList outs id then + let mcall = MethodCall(ThisLiteral, compName, methName, ins |> List.map (function var -> VarLiteral("$" + (GetExtVarName var)))) + let outSel = MethodOutSelect(mcall, id) + Some(outSel) + else + Some(VarLiteral("$" + id)) + | _ -> None) [] + |> ChangeThisReceiver (VarLiteral("$this")) + + /// Merges ... + let __MergeSolutions hInst s = + let __FindRhs lhs = s |> List.choose (fun (l,r) -> if l = lhs then Some(r) else None) |> Utils.ListToOption + let rec __FixAssignments asgs = + match asgs with + | asg :: rest -> + let newAsg = + match asg with + | FieldAssignment((obj,var) as discr,valExpr) -> + let objPath = GetObjRefExpr obj.name hInst |> Utils.ExtractOption + let lhs = Dot(objPath, GetExtVarName var) + match __FindRhs lhs with + | Some(rhs) -> FieldAssignment(discr,rhs) + | None -> asg + | _ -> asg + newAsg :: (__FixAssignments rest) + | [] -> [] + let rec __FixRetValues retVals = + match retVals with + | (varName,varExpr) :: rest -> + let lhs = VarLiteral(varName) + let newVarExpr = + match __FindRhs lhs with + | Some(rhs) -> rhs + | None -> varExpr + __FixRetValues rest |> Map.add varName newVarExpr + | [] -> Map.empty + if s = [] then + hInst + else + // fix assignments + let newAsgs = __FixAssignments hInst.assignments + // fix return values + let newRetVals = __FixRetValues (hInst.methodRetVals |> Map.toList) + {hInst with assignments = newAsgs; + methodRetVals = newRetVals} + + + /// For a given heap instance and a list of possible solutions, it iterates + /// trough all of them and returns whichever verifies first. + let rec __IterSolutions hInst premises wrongSol sList = + match sList with + | s :: rest -> + Logger.InfoLine (idt + "Candidate solution:") + Logger.InfoLine (__PrintSol (indent + 4) s) + let hInst' = __MergeSolutions hInst s + let sol = Utils.MapSingleton (comp,m) [TrueLiteral, hInst'] + if not (hInst' = hInst) && VerifySolution prog sol Options.CONFIG.genRepr then + Logger.InfoLine (idt + " ~~~ VERIFIED ~~~") + sol + else + Logger.InfoLine (idt + " !!! NOT VERIFIED !!!") + match TryInferConditionals indent prog comp m unifs hInst' callGraph premises with + | Some(candCond,solThis) -> + let m' = AddPrecondition m (UnaryNot(candCond)) + let solRest = AnalyzeConstructor (indent + 2) prog comp m' callGraph + MergeSolutions solThis solRest |> FixSolution comp m + | None -> + __IterSolutions hInst premises wrongSol rest + | [] -> wrongSol + + (* --- function body starts here --- *) + let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 e)) + + //TODO + let expandOnlyModVarsFunc = fun e -> + true +// let __CheckExpr l = +// //TODO: FIX THIS!!!!! +// match l with +// | VarLiteral(vname) -> GetMethodOutArgs m |> List.exists (fun var -> GetVarName var = vname) +// | IdLiteral(_) -> true +// | Dot(_,_) -> true +// | _ -> false +// match e with +// | BinaryExpr(_,"=",l,_) -> +// //TODO: it should really check both lhs and rhs +// __CheckExpr l +// | BinaryExpr(_,op,l,_) when IsRelationalOp op -> +// __CheckExpr l +// | _ -> __CheckExpr e + + let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst] + let heapInst = ApplyUnifications indent prog comp m unifs heapInst false + let methodArgs = GetMethodInArgs m + let heapExpr = GetHeapExpr prog m heapInst true + + //Logger.TraceLine (PrintExpr 0 heapExpr) + + // find set of premises (don't resolve anything) + let premises = heapExpr |> FindClauses false (fun e -> false) heapInst + + Logger.TraceLine (sprintf "%s Premises:" idt) + premises |> List.iter loggerFunc + + // add only recursive call for now + let post = __GetMethodPostTemplate comp m + + let premiseSet = premises |> Set.ofList |> Set.add post + let closedPremises = ComputeClosure heapInst expandOnlyModVarsFunc premiseSet + + Logger.TraceLine (idt + "Closed premises with methods") + closedPremises |> Set.iter loggerFunc + + let s = __GetAllAssignments heapInst closedPremises + if s = [] then + // have at least one empty sol so that the original heapInst is not missed + __IterSolutions heapInst closedPremises wrongSol [[]] + else + __IterSolutions heapInst closedPremises wrongSol s + +and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = + let idt = Indent indent + let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 e)) + let methodArgs = GetMethodInArgs m + + /// Iterates through a given list of boolean conditions and checks + /// which one suffices. If it finds such a condition, it returns + /// the following three things: + /// - the condition itself + /// - the method with this condition added to its preconditions + /// - a solution + /// Otherwise returns None. + let rec __TryOutConditions heapInst candidateConditions = + let idt = Indent indent + match candidateConditions with + | [] -> + Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) + None + | candCond :: rest -> + Logger.InfoLine (sprintf "%s ________________________" idt) + Logger.InfoLine (sprintf "%s candidate pre-condition: %s" idt (PrintExpr 0 candCond)) + Logger.InfoLine (sprintf "%s ------------------------" idt) + let idt = idt + " " + match CheckGuard prog comp m candCond indent idt heapInst callGraph with + | Some(guard, m2, sol) -> Some(guard, m2, sol) + | None -> __TryOutConditions heapInst rest + + if IsSolution1stLevelOnly heapInst then + // try to find a non-recursive solution + Logger.InfoLine (idt + "Strengthening the pre-condition") + let expr = GetHeapExpr prog m heapInst false + let specConds1 = expr |> FindTrueClauses (DontResolveUnmodifiableStuff prog comp m) heapInst + let specConds2 = premises |> Set.toList + + let isConstFunc = fun e -> try + EvalNone heapInst e |> Expr2Const |> ignore + true + with + | _ -> false + let unmodConcrFunc = IsUnmodConcrOnly prog (comp,m) + let is1stLevelFunc = __Is1stLevelExpr false heapInst + + let specConds = (specConds1 @ specConds2) + |> List.map SimplifyExpr + |> List.filter (fun e -> is1stLevelFunc e && unmodConcrFunc e && not (isConstFunc e)) + + let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function var -> VarLiteral(GetExtVarName var))) heapInst) + let argConds = heapInst.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) [] + let allConds = GetAllPossibleConditions specConds argConds [aliasingCond.Force()] + allConds |> List.iter loggerFunc + + match __TryOutConditions heapInst allConds with + | Some(candCond,m2,sol) -> + Logger.InfoLine (idt + " - guard found: " + (PrintExpr 0 candCond)) + let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with + | Some(sol2) -> sol2 + | None -> sol + let solThis = solThis |> FixSolution comp m + Some(candCond,solThis) + | None -> + Logger.InfoLine (idt + "!!! Giving up !!!") + None + else + // the solution is not immediate + None + + + +// =========================================================== +/// Reads CONFIG.methodToSynth to return a list of methods +/// that Jennisys should attempt to synthesize. +// =========================================================== +let GetMethodsToAnalyze prog = + let __ReadMethodsParam = + let mOpt = Options.CONFIG.methodToSynth; + if mOpt = "*" then + (* all *) + FilterMembers prog FilterMethodMembers + else + let allMethods,neg = + if mOpt.StartsWith("~") then + mOpt.Substring(1), true + else + mOpt, false + (* exact list *) + let methods = allMethods.Split([|','|]) + let lst = methods |> Array.fold (fun acc m -> + let idx = m.LastIndexOf(".") + if idx = -1 || idx = m.Length - 1 then + raise (InvalidCmdLineArg("Invalid method full name: " + m)) + let compName = m.Substring(0, idx) + let methName = m.Substring(idx + 1) + let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) + let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) + (c,mthd) :: acc + ) [] + if neg then + FilterMembers prog FilterMethodMembers |> List.filter (fun e -> not (Utils.ListContains e lst)) + else + lst + (* --- function body starts here --- *) + let meths = __ReadMethodsParam + if Options.CONFIG.constructorsOnly then + meths |> List.filter (fun (c,m) -> IsConstructor m) + else + meths + +// ============================================================================ +/// Goes through a given list of methods of the given program and attempts to +/// synthesize code for each one of them. +/// +/// Returns a map from (component * method) |--> Expr * HeapInstance +// ============================================================================ +let rec AnalyzeMethods prog members solutionsSoFar = + let __IsAlreadySolved c m solutionMap = + let existingKey = solutionMap |> Map.tryFindKey (fun (cc,mm) v -> CheckSameMethods (c,m) (cc,mm) && not (v = [])) + match existingKey with + | Some(_) -> true + | None -> false + + let rec __AnalyzeConstructorDeep prog mList solutionsSoFar = + let callGraph = GetCallGraph (solutionsSoFar |> Map.toList) Map.empty + match mList with + | (comp,mthd) :: rest -> + if not (__IsAlreadySolved comp mthd solutionsSoFar) then + let sol = AnalyzeConstructor 2 prog comp mthd callGraph + let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = [] && not(__IsAlreadySolved c m solutionsSoFar)) |> Utils.MapKeys + let newSols = solutionsSoFar |> MergeSolutions sol + __AnalyzeConstructorDeep prog (rest@unsolved) newSols + else + __AnalyzeConstructorDeep prog rest solutionsSoFar + | [] -> solutionsSoFar + + (* --- function body starts here --- *) + match members with + | (comp,m) :: rest -> + match m with + | Method(_,_,_,_,_) -> + let sol = __AnalyzeConstructorDeep prog [comp,m] solutionsSoFar + Logger.InfoLine "" + AnalyzeMethods prog rest sol + | _ -> AnalyzeMethods prog rest solutionsSoFar + | [] -> solutionsSoFar + +let Analyze prog filename = + let rec __AddMethodsFromProg methods solutions = + match methods with + | (c,m) :: rest -> + let exists = solutions |> Map.tryFindKey (fun (c1,m1) _ -> CheckSameMethods (c,m) (c1,m1)) + match exists with + | Some(_) -> __AddMethodsFromProg rest solutions + | None -> __AddMethodsFromProg rest (solutions |> Map.add (c,m) []) + | [] -> solutions + + /// Prints given solutions to a file + let __PrintSolution prog outFileName solutions = + use file = System.IO.File.CreateText(outFileName) + file.AutoFlush <- true + //let prog = Program(solutions |> Utils.MapKeys |> Map.ofList |> Utils.MapKeys) + // add all other methods (those for which we don't have synthesized solution) as well + let allMethods = FilterMembers prog FilterConstructorMembers + let extSolutions = solutions //__AddMethodsFromProg allMethods solutions + let synthCode = PrintImplCode prog extSolutions Options.CONFIG.genRepr false + fprintfn file "%s" synthCode + + (* --- function body starts here --- *) + let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) Map.empty + let progName = System.IO.Path.GetFileNameWithoutExtension(filename) + let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName) + Logger.InfoLine "Printing synthesized code" + __PrintSolution prog outFlatSolFileName solutions + () + +//let AnalyzeComponent_rustan c = +// match c with +// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) -> +// let aVars = Fields members +// let aVars0 = Rename "0" aVars +// let aVars1 = Rename "1" aVars +// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars] +// let inv0 = Substitute (Map.ofList aVars0) inv +// let inv1 = Substitute (Map.ofList aVars1) inv +// // Now print it as a Dafny program +// printf "class %s" name +// match typeParams with +// | [] -> () +// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) +// printfn " {" +// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields +// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp)) +// // the method +// printfn " method %s_checkInjective() {" name +// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";" +// printfn " assume %s;" (PrintExpr 0 inv0) +// printfn " assume %s;" (PrintExpr 0 inv1) +// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"} +// printfn " }" +// // generate code +// members |> List.iter (function +// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false) +// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true) +// | _ -> ()) +// // the end of the class +// printfn "}" +// | _ -> assert false // unexpected case \ No newline at end of file diff --git a/Source/Jennisys/Ast.fs b/Source/Jennisys/Ast.fs new file mode 100644 index 00000000..d355023a --- /dev/null +++ b/Source/Jennisys/Ast.fs @@ -0,0 +1,95 @@ +// #################################################################### +/// The AST of a Jennisy program +/// +/// author: Rustan Leino (leino@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### + +namespace Ast + +open System +open System.Numerics + +type Type = + | IntType + | BoolType + | SetType of Type (* type parameter *) + | SeqType of Type (* type parameter *) + | NamedType of string * string list (* type parameters *) + | InstantiatedType of string * Type list (* type parameters *) + +type VarDecl = + | Var of string * Type option * (* isOld *) bool + +(* + the difference between IdLiteral and VarLiteral is that the VarLiteral is more specific, + it always referes to a local variable (either method parameter or quantification variable) + + ObjLiteral is a concrete object, so if two ObjLiterals have different names, + they are different objects (as opposed to IdLiterals and VarLiterals, which can alias). + *) +type Expr = + | IntLiteral of int + | BoolLiteral of bool + | BoxLiteral of string + | VarLiteral of string + | IdLiteral of string + | ObjLiteral of string + | Star + | Dot of Expr * string + | UnaryExpr of string * Expr + | OldExpr of Expr + | LCIntervalExpr of Expr + | BinaryExpr of int * string * Expr * Expr + | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr + | SelectExpr of Expr * Expr + | UpdateExpr of Expr * Expr * Expr + | SequenceExpr of Expr list + | SeqLength of Expr + | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list + | ForallExpr of VarDecl list * Expr + | MethodCall of (* receiver *) Expr * (* component name *) string * (* method name *) string * (* actual parameters *) Expr list + | MethodOutSelect of (* method *) Expr * (* out param name *) string + | VarDeclExpr of (* var list *) VarDecl list * (* declareAlso *) bool + | AssertExpr of Expr + | AssumeExpr of Expr + +type Const = + | IntConst of int + | BoolConst of bool + | BoxConst of string + | SetConst of Set + | SeqConst of Const list + | NullConst + | NoneConst + | ThisConst of (* loc id *) string * Type option + | VarConst of string + | NewObj of (* loc id *) string * Type option + | Unresolved of (* loc id *) string + +type Stmt = + | Block of Stmt list + | ExprStmt of Expr + | Assign of Expr * Expr + +type Signature = + | Sig of (* ins *) VarDecl list * (* outs *) VarDecl list + +type Member = + | Field of VarDecl + | Method of (* name *) string * Signature * (* pre *) Expr * (* post *) Expr * (* isConstructor *) bool + | Invariant of Expr list + +type TopLevelDecl = + | Interface of string * string list * Member list + | DataModel of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr + | Code of string * string list + +type SyntacticProgram = + | SProgram of TopLevelDecl list + +type Component = + | Component of (*interface*)TopLevelDecl * (*datamodel*)TopLevelDecl * (*code*)TopLevelDecl + +type Program = + | Program of Component list diff --git a/Source/Jennisys/AstUtils.fs b/Source/Jennisys/AstUtils.fs new file mode 100644 index 00000000..6aac59e2 --- /dev/null +++ b/Source/Jennisys/AstUtils.fs @@ -0,0 +1,1033 @@ +// #################################################################### +/// Utility functions for manipulating AST elements +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### + +module AstUtils + +open Ast +open Getters +open Logger +open Utils + +let ThisLiteral = ObjLiteral("this") +let NullLiteral = ObjLiteral("null") + +let IsLogicalOp op = [ "&&"; "||"; "==>"; "<==>" ] |> Utils.ListContains op +let IsRelationalOp op = [ "="; "!="; "<"; "<="; ">"; ">="; "in"; "!in" ] |> Utils.ListContains op + +let AreInverseOps op1 op2 = match op1, op2 with "<" , ">" | ">" , "<" | "<=", ">=" | ">=", "<=" -> true | _ -> false + +let DoesImplyOp op1 op2 = + match op1, op2 with + | "<" , "!=" | ">" , "!=" -> true + | "=" , ">=" | "=" , "<=" -> true + | ">" , ">=" | "<" , "<=" -> true + | _ -> false +let IsCommutativeOp op = match op with "=" | "!=" -> true | _ -> false + +exception ExprConvFailed of string + +let Expr2Int e = + match e with + | IntLiteral(n) -> n + | _ -> raise (ExprConvFailed(sprintf "not an int but: %O" e)) + +let Expr2Bool e = + match e with + | BoolLiteral(b) -> b + | _ -> raise (ExprConvFailed(sprintf "not a bool but: %O" e)) + +let Expr2List e = + match e with + | SequenceExpr(elist) -> elist + | _ -> raise (ExprConvFailed(sprintf "not a Seq but: %O" e)) + +let rec MyRewrite rewriterFunc rewriteRecurseFunc expr = + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> match rewriterFunc expr with + | Some(e) -> e + | None -> expr + | Dot(e, id) -> Dot(rewriteRecurseFunc e, id) + | ForallExpr(vars,e) -> ForallExpr(vars, rewriteRecurseFunc e) + | UnaryExpr(op,e) -> UnaryExpr(op, rewriteRecurseFunc e) + | OldExpr(e) -> OldExpr(rewriteRecurseFunc e) + | LCIntervalExpr(e) -> LCIntervalExpr(rewriteRecurseFunc e) + | SeqLength(e) -> SeqLength(rewriteRecurseFunc e) + | SelectExpr(e1, e2) -> SelectExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2) + | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, rewriteRecurseFunc e1, rewriteRecurseFunc e2) + | IteExpr(e1,e2,e3) -> IteExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2, rewriteRecurseFunc e3) + | UpdateExpr(e1,e2,e3) -> UpdateExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2, rewriteRecurseFunc e3) + | SequenceExpr(exs) -> SequenceExpr(exs |> List.map rewriteRecurseFunc) + | SetExpr(exs) -> SetExpr(exs |> List.map rewriteRecurseFunc) + | MethodCall(rcv,cname,mname,ins) -> MethodCall(rewriteRecurseFunc rcv, cname, mname, ins |> List.map rewriteRecurseFunc) + | MethodOutSelect(mth,name) -> MethodOutSelect(rewriteRecurseFunc mth, name) + | AssertExpr(e) -> AssertExpr(rewriteRecurseFunc e) + | AssumeExpr(e) -> AssumeExpr(rewriteRecurseFunc e) + +let rec Rewrite rewriterFunc expr = + let __RewriteOrRecurse e = + match rewriterFunc e with + | Some(ee) -> ee + | None -> Rewrite rewriterFunc e + MyRewrite rewriterFunc __RewriteOrRecurse expr + +// TODO: double check this! +let rec RewriteBU rewriterFunc expr = + let rewriteRecurseFunc e = + RewriteBU rewriterFunc e +// let e' = Rewrite rewriterFunc e +// match rewriterFunc e' with +// | Some(ee) -> ee +// | None -> e' + let rewriteFunc e = + match rewriterFunc e with + | Some(ee) -> ee + | None -> e + let expr' = + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> expr + | Dot(e, id) -> Dot(rewriteRecurseFunc e, id) + | ForallExpr(vars,e) -> ForallExpr(vars, rewriteRecurseFunc e) + | UnaryExpr(op,e) -> UnaryExpr(op, rewriteRecurseFunc e) + | OldExpr(e) -> OldExpr(rewriteRecurseFunc e) + | LCIntervalExpr(e) -> LCIntervalExpr(rewriteRecurseFunc e) + | SeqLength(e) -> SeqLength(rewriteRecurseFunc e) + | SelectExpr(e1, e2) -> SelectExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2) + | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, rewriteRecurseFunc e1, rewriteRecurseFunc e2) + | IteExpr(e1,e2,e3) -> IteExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2, rewriteRecurseFunc e3) + | UpdateExpr(e1,e2,e3) -> UpdateExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2, rewriteRecurseFunc e3) + | SequenceExpr(exs) -> SequenceExpr(exs |> List.map rewriteRecurseFunc) + | SetExpr(exs) -> SetExpr(exs |> List.map rewriteRecurseFunc) + | MethodCall(rcv,cname,mname,ins) -> MethodCall(rewriteRecurseFunc rcv, cname, mname, ins |> List.map rewriteRecurseFunc) + | MethodOutSelect(mth,name) -> MethodOutSelect(rewriteRecurseFunc mth, name) + | AssertExpr(e) -> AssertExpr(rewriteRecurseFunc e) + | AssumeExpr(e) -> AssumeExpr(rewriteRecurseFunc e) + expr' |> rewriteFunc + +let rec RewriteWithCtx rewriterFunc ctx expr = + let __RewriteOrRecurse ctx e = + match rewriterFunc ctx e with + | Some(ee) -> ee + | None -> RewriteWithCtx rewriterFunc ctx e + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> match rewriterFunc ctx expr with + | Some(e) -> e + | None -> expr + | Dot(e, id) -> Dot(__RewriteOrRecurse ctx e, id) + | ForallExpr(vars,e) -> ForallExpr(vars, __RewriteOrRecurse (ctx @ vars) e) + | UnaryExpr(op,e) -> UnaryExpr(op, __RewriteOrRecurse ctx e) + | OldExpr(e) -> OldExpr(__RewriteOrRecurse ctx e) + | LCIntervalExpr(e) -> LCIntervalExpr(__RewriteOrRecurse ctx e) + | SeqLength(e) -> SeqLength(__RewriteOrRecurse ctx e) + | SelectExpr(e1, e2) -> SelectExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2) + | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2) + | IteExpr(e1,e2,e3) -> IteExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2, __RewriteOrRecurse ctx e3) + | UpdateExpr(e1,e2,e3) -> UpdateExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2, __RewriteOrRecurse ctx e3) + | SequenceExpr(exs) -> SequenceExpr(exs |> List.map (__RewriteOrRecurse ctx)) + | SetExpr(exs) -> SetExpr(exs |> List.map (__RewriteOrRecurse ctx)) + | MethodCall(rcv,cname,mname,ins) -> MethodCall(__RewriteOrRecurse ctx rcv, cname, mname, ins |> List.map (__RewriteOrRecurse ctx)) + | MethodOutSelect(mth,name) -> MethodOutSelect(__RewriteOrRecurse ctx mth, name) + | AssertExpr(e) -> AssertExpr(__RewriteOrRecurse ctx e) + | AssumeExpr(e) -> AssumeExpr(__RewriteOrRecurse ctx e) + +// ==================================================== +/// Substitutes all occurences of all IdLiterals having +/// the same name as one of the variables in "vars" with +/// VarLiterals, in "expr". +// ==================================================== +let RewriteVars vars expr = + let __IdIsArg id = vars |> List.exists (fun var -> GetVarName var = id) + Rewrite (fun e -> + match e with + | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id)) + | _ -> None) expr + +// ================================================ +/// Substitutes all occurences of e1 with e2 in expr +// ================================================ +let Substitute e1 e2 expr = + Rewrite (fun e -> + if e = e1 then + Some(e2) + else + None) expr + +// ================================================ +/// Distributes the negation operator over +/// arithmetic relations +// ================================================ +let rec DistributeNegation expr = + let __Neg op = + match op with + | "=" -> Some("!=") + | "!=" -> Some("=") + | "<" -> Some(">=") + | ">" -> Some("<=") + | ">=" -> Some("<") + | "<=" -> Some(">") + | _ -> None + Rewrite (fun e -> + match e with + | UnaryExpr("!", sub) -> + match sub with + | BinaryExpr(p,op,lhs,rhs) -> + match __Neg op with + | Some(op') -> Some(BinaryExpr(p, op', DistributeNegation lhs, DistributeNegation rhs)) + | None -> None + | _ -> None + | _ -> None) expr + +let rec DescendExpr visitorFunc composeFunc leafVal expr = + let __Compose elist = + match elist with + | [] -> leafVal + | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs) + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> leafVal + | AssertExpr(e) + | AssumeExpr(e) + | Dot(e, _) + | ForallExpr(_,e) + | LCIntervalExpr(e) + | OldExpr(e) + | UnaryExpr(_,e) + | MethodOutSelect(e,_) + | SeqLength(e) -> __Compose (e :: []) + | SelectExpr(e1, e2) + | BinaryExpr(_,_,e1,e2) -> __Compose (e1 :: e2 :: []) + | IteExpr(e1,e2,e3) + | UpdateExpr(e1,e2,e3) -> __Compose (e1 :: e2 :: e3 :: []) + | MethodCall(rcv,_,_,aparams) -> __Compose (rcv :: aparams) + | SequenceExpr(exs) + | SetExpr(exs) -> __Compose exs + +let rec DescendExpr2 visitorFunc expr acc = + let newAcc = acc |> visitorFunc expr + let __Pipe elist = elist |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> newAcc + | AssertExpr(e) + | AssumeExpr(e) + | Dot(e, _) + | ForallExpr(_,e) + | LCIntervalExpr(e) + | OldExpr(e) + | UnaryExpr(_,e) + | MethodOutSelect(e,_) + | SeqLength(e) -> __Pipe (e :: []) + | SelectExpr(e1, e2) + | BinaryExpr(_,_,e1,e2) -> __Pipe (e1 :: e2 :: []) + | IteExpr(e1,e2,e3) + | UpdateExpr(e1,e2,e3) -> __Pipe (e1 :: e2 :: e3 :: []) + | MethodCall(rcv,_,_,aparams) -> __Pipe (rcv :: aparams) + | SequenceExpr(exs) + | SetExpr(exs) -> __Pipe exs + +let rec DescendExpr2BU visitorFunc expr acc = + let __Pipe elist = + let newAcc = elist |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) acc + newAcc |> visitorFunc expr + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarLiteral(_) + | ObjLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) -> __Pipe [] + | AssertExpr(e) + | AssumeExpr(e) + | Dot(e, _) + | ForallExpr(_,e) + | LCIntervalExpr(e) + | OldExpr(e) + | UnaryExpr(_,e) + | MethodOutSelect(e,_) + | SeqLength(e) -> __Pipe (e :: []) + | SelectExpr(e1, e2) + | BinaryExpr(_,_,e1,e2) -> __Pipe (e1 :: e2 :: []) + | IteExpr(e1,e2,e3) + | UpdateExpr(e1,e2,e3) -> __Pipe (e1 :: e2 :: e3 :: []) + | MethodCall(rcv,_,_,aparams) -> __Pipe (rcv :: aparams) + | SequenceExpr(exs) + | SetExpr(exs) -> __Pipe exs + +//TODO: if names in dafny models contain funky characters, +// these gensym variables might not be valid identifiers +let PrintGenSym (name: string) = + if name.StartsWith("gensym") then + name + else + let idx = name.LastIndexOf("!") + if idx <> -1 then + sprintf "gensym%s" (name.Substring(idx+1)) + else + sprintf "gensym%s" name + +// ===================== +/// Returns TRUE literal +// ===================== +let TrueLiteral = BoolLiteral(true) + +// ===================== +/// Returns FALSE literal +// ===================== +let FalseLiteral = BoolLiteral(false) + +let UnaryNeg sub = + match sub with + | UnaryExpr("-", s) -> s + | _ -> UnaryExpr("-", sub) + +let UnaryNot sub = + match sub with + | UnaryExpr("!", s) -> s + | BoolLiteral(b) -> BoolLiteral(not b) + | BinaryExpr(p,"=",l,r) -> BinaryExpr(p,"!=",l,r) + | BinaryExpr(p,"!=",l,r) -> BinaryExpr(p,"=",l,r) + | BinaryExpr(p,"in",l,r) -> BinaryExpr(p,"!in",l,r) + | BinaryExpr(p,"!in=",l,r) -> BinaryExpr(p,"in",l,r) + | BinaryExpr(p,"<",l,r) -> BinaryExpr(p,">=",l,r) + | BinaryExpr(p,"<=",l,r) -> BinaryExpr(p,">",l,r) + | BinaryExpr(p,">",l,r) -> BinaryExpr(p,"<=",l,r) + | BinaryExpr(p,">=",l,r) -> BinaryExpr(p,"<",l,r) + | _ -> UnaryExpr("!", sub) + +// ======================================================================= +/// Returns a binary AND of the two given expressions with short-circuiting +// ======================================================================= +let BinaryAnd (lhs: Expr) (rhs: Expr) = + match lhs, rhs with + | BoolLiteral(true), _ -> rhs + | BoolLiteral(false), _ -> FalseLiteral + | _, BoolLiteral(true) -> lhs + | _, BoolLiteral(false) -> FalseLiteral + | _, _ -> 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 + | BoolLiteral(true), _ -> TrueLiteral + | BoolLiteral(false), _ -> rhs + | _, BoolLiteral(true) -> TrueLiteral + | _, BoolLiteral(false) -> lhs + | _, _ -> BinaryExpr(30, "||", lhs, rhs) + +// =================================================================================== +/// Returns a binary IMPLIES of the two given expressions +// =================================================================================== +let BinaryImplies lhs rhs = + match lhs, rhs with + | BoolLiteral(false), _ -> TrueLiteral + | BoolLiteral(true), _ -> rhs + | _, BoolLiteral(true) -> lhs + | _, BoolLiteral(false) -> UnaryNot(lhs) + | _ -> BinaryExpr(20, "==>", lhs, rhs) + +// ======================================================= +/// Constructors for binary EQ/NEQ of two given expressions +// ======================================================= +let BinaryNeq lhs rhs = + match lhs, rhs with + | BoolLiteral(true), x | x, BoolLiteral(true) -> UnaryNot x + | BoolLiteral(false), x | x, BoolLiteral(false) -> x + | _ -> BinaryExpr(40, "!=", lhs, rhs) + +let BinaryEq lhs rhs = + match lhs, rhs with + | BoolLiteral(true), x | x, BoolLiteral(true) -> x + | BoolLiteral(false), x | x, BoolLiteral(false) -> UnaryNot x + | _ when lhs = rhs -> TrueLiteral + | _ -> BinaryExpr(40, "=", lhs, rhs) + +// ======================================================= +/// Constructor for binary GETS +// ======================================================= +let BinaryGets lhs rhs = Assign(lhs, rhs) + +let BinaryAdd lhs rhs = BinaryExpr(55, "+", lhs, rhs) +let BinarySub lhs rhs = BinaryExpr(55, "-", lhs, rhs) + +// ======================================================= +/// Constructors for binary IN/!IN of two given expressions +// ======================================================= +let BinaryIn lhs rhs = + match lhs, rhs with + | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 0 -> FalseLiteral + | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 1 -> BinaryEq lhs (elist.[0]) + | _ -> BinaryExpr(40, "in", lhs, rhs) + +let BinaryNotIn lhs rhs = + match lhs, rhs with + | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 0 -> TrueLiteral + | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 1 -> BinaryNeq lhs (elist.[0]) + | _ -> BinaryExpr(40, "!in", lhs, rhs) + +// ========================================== +/// Splits "expr" into a list of its conjuncts +// ========================================== +let rec SplitIntoConjunts expr = + match expr with + | BoolLiteral(true) -> [] + | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1] + | _ -> [expr] + +// ====================================== +/// Applies "f" to each conjunct of "expr" +// ====================================== +let rec ForeachConjunct f expr = + SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) "" + +// ======================================= +/// Converts a given constant to expression +// ======================================= +let rec Const2Expr c = + match c with + | IntConst(n) -> IntLiteral(n) + | BoolConst(b) -> BoolLiteral(b) + | BoxConst(id) -> BoxLiteral(id) + | SeqConst(clist) -> + let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev + SequenceExpr(expList) + | SetConst(cset) -> + let expSet = cset |> Set.fold (fun acc c -> Set.add (Const2Expr c) acc) Set.empty + SetExpr(Set.toList expSet) + | VarConst(id) -> VarLiteral(id) + | ThisConst(_,_) -> ObjLiteral("this") + | NewObj(name,_) -> ObjLiteral(PrintGenSym name) + | NullConst -> ObjLiteral("null") + | Unresolved(id) -> BoxLiteral(id) // failwithf "don't want to convert Unresolved(%s) to expr" name // + | _ -> failwithf "not implemented or not supported: %O" c + +let rec Expr2Const e = + match e with + | IntLiteral(n) -> IntConst(n) + | BoolLiteral(b) -> BoolConst(b) + | BoxLiteral(id) -> BoxConst(id) + | ObjLiteral("this") -> ThisConst("this",None) + | ObjLiteral("null") -> NullConst + | ObjLiteral(name) -> NewObj(name, None) + | IdLiteral(id) -> Unresolved(id) + | VarLiteral(id) -> VarConst(id) + | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const) + | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList) + | _ -> failwithf "Not a constant: %O" e + +let rec Expr2ConstStrict e = + match e with + | IntLiteral(n) -> IntConst(n) + | BoolLiteral(b) -> BoolConst(b) + | BoxLiteral(id) -> BoxConst(id) + | ObjLiteral("this") -> ThisConst("this",None) + | ObjLiteral("null") -> NullConst + | ObjLiteral(name) -> NewObj(name, None) + | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2ConstStrict) + | SetExpr(elist) -> SetConst(elist |> List.map Expr2ConstStrict |> Set.ofList) + | _ -> failwithf "Not a constant: %O" e + +let TryExpr2Const e = + try + Some(Expr2Const e) + with + | ex -> None + +let IsConstExpr e = + try + Expr2Const e |> ignore + true + with + | _ -> false + +/////// + +let GetMethodPre mthd = + match mthd with + | Method(_,_,pre,_,_) -> pre + | _ -> failwith ("not a method" + mthd.ToString()) + +let GetMethodPrePost mthd = + let __FilterOutAssumes e = e |> SplitIntoConjunts |> List.filter (function AssumeExpr(_) -> false | _ -> true) |> List.fold BinaryAnd TrueLiteral + match mthd with + | Method(_,_,pre,post,_) -> __FilterOutAssumes pre,post + | _ -> failwith ("not a method: " + mthd.ToString()) + +let GetMethodGhostPrecondition mthd = + match mthd with + | Method(_,_,pre,_,_) -> + pre |> SplitIntoConjunts |> List.choose (function AssumeExpr(e) -> Some(e) | _ -> None) |> List.fold BinaryAnd TrueLiteral + | _ -> failwith ("not a method: " + mthd.ToString()) + +// ============================================================== +/// Returns all invariants of a component as a list of expressions +// ============================================================== +let GetInvariantsAsList comp = + match comp with + | Component(Interface(_,_,members), DataModel(_,_,_,_,inv), _) -> + let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat + List.append (SplitIntoConjunts inv) clsInvs + | _ -> failwithf "unexpected kind of component: %O" comp + +/// Replaces all Old nodes with IdLiteral with name = "old_" + +let RewriteOldExpr expr = + expr |> RewriteBU (fun e -> match e with + | OldExpr(IdLiteral(name)) -> Some(IdLiteral(RenameToOld name)) + | _ -> None) + +let MakeOldVar var = + match var with + | Var(name, ty, _) -> Var(name, ty, true) + +let MakeOldVars varLst = + varLst |> List.map MakeOldVar + +/// renames ALL variables to "old_"+ +let MakeOld expr = + expr |> RewriteBU (fun e -> match e with + | IdLiteral(name) when not (name="this") -> Some(IdLiteral(RenameToOld name)) + | Dot(e, name) -> Some(Dot(e, RenameToOld name)) + | _ -> None) + +let BringToPost expr = + expr |> RewriteBU (fun e -> match e with + | IdLiteral(name) -> Some(IdLiteral(RenameFromOld name)) + | Dot(e, name) -> Some(Dot(e, RenameFromOld name)) + | _ -> None) + +//////////////////////// + +let AddReplaceMethod prog comp newMthd oldMethod = + match prog, comp with + | Program(clist), Component(Interface(cname, ctypeParams, members), model, code) -> + let newMembers = + match oldMethod with + | None -> members @ [newMthd] + | Some(m) -> Utils.ListReplace m newMthd members + let newCls = Interface(cname, ctypeParams, newMembers) + let newComp = Component(newCls, model, code) + let newProg = Program(Utils.ListReplace comp newComp clist) + newProg, newComp + | _ -> failwithf "Invalid component: %O" comp + +let UnwrapAssumes e = e |> SplitIntoConjunts |> List.map (function AssumeExpr(e) -> e | x -> x) |> List.fold BinaryAnd TrueLiteral + +let AddPrecondition m e = + match m with + | Method(mn, sgn, pre, post, cstr) -> Method(mn, sgn, BinaryAnd pre (AssumeExpr(e |> UnwrapAssumes)), post, cstr) + | _ -> failwithf "Not a method: %O" m + +let SetPrecondition m e = + match m with + | Method(mn, sgn, pre, post, cstr) -> Method(mn, sgn, AssumeExpr(e |> UnwrapAssumes), post, cstr) + | _ -> failwithf "Not a method: %O" m + +//////////////////// + +exception EvalFailed of string +exception DomainNotInferred + +let DefaultResolver e fldOpt = + match fldOpt with + | None -> e + | Some(fldName) -> Dot(e, fldName) + +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 EvalSym2 fullResolverFunc otherResolverFunc returnFunc ctx expr = + let rec __EvalSym resolverFunc returnFunc ctx expr = + let expr' = + match expr with + | IntLiteral(_) -> expr + | BoolLiteral(_) -> expr + | BoxLiteral(_) -> expr + | ObjLiteral(_) -> expr + | Star -> expr //TODO: can we do better? + | VarDeclExpr(_) -> expr + | AssertExpr(e) -> AssertExpr(__EvalSym resolverFunc returnFunc ctx e) + | AssumeExpr(e) -> AssumeExpr(__EvalSym resolverFunc returnFunc ctx e) + | VarLiteral(id) -> + try + let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id) + e + with + | ex -> resolverFunc expr None + | IdLiteral(_) -> resolverFunc expr None + | Dot(e, str) -> + let discr = __EvalSym resolverFunc returnFunc ctx e + resolverFunc discr (Some(str)) + | SeqLength(e) -> + let e' = __EvalSym resolverFunc returnFunc ctx e + match e' with + | SequenceExpr(elist) -> IntLiteral(List.length elist) + | _ -> SeqLength(e') + | SequenceExpr(elist) -> + let elist' = elist |> List.map (__EvalSym resolverFunc returnFunc ctx) // List.fold (fun acc e -> (__EvalSym resolverFunc returnFunc ctx e) :: acc) [] |> List.rev + SequenceExpr(elist') + | SetExpr(elist) -> + let elist' = elist |> List.map (__EvalSym resolverFunc returnFunc ctx) //List.fold (fun acc e -> Set.add (__EvalSym resolverFunc returnFunc ctx e) acc) Set.empty + SetExpr(elist' |> Set.ofList |> Set.toList) + | MethodOutSelect(e,name) -> + MethodOutSelect(__EvalSym resolverFunc returnFunc ctx e, name) + | MethodCall(rcv,cname, mname,aparams) -> + let rcv' = __EvalSym resolverFunc returnFunc ctx rcv + let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc returnFunc ctx e :: acc) [] |> List.rev + MethodCall(rcv', cname, mname, aparams') + | LCIntervalExpr(_) -> expr + | SelectExpr(lst, idx) -> + let lst' = __EvalSym resolverFunc returnFunc ctx lst + let idx' = __EvalSym resolverFunc returnFunc ctx idx + match lst', idx' with + | SequenceExpr(elist), IntLiteral(n) -> elist.[n] + | SequenceExpr(elist), LCIntervalExpr(startIdx) -> + let startIdx' = __EvalSym resolverFunc returnFunc ctx startIdx + match startIdx' with + | IntLiteral(startIdxInt) -> + let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l) + SequenceExpr(__Skip startIdxInt elist) + | _ -> SelectExpr(lst', idx') + | _ -> SelectExpr(lst', idx') + | UpdateExpr(lst,idx,v) -> + let lst', idx', v' = __EvalSym resolverFunc returnFunc ctx lst, __EvalSym resolverFunc returnFunc ctx idx, __EvalSym resolverFunc returnFunc ctx v + match lst', idx', v' with + | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist) + | _ -> UpdateExpr(lst', idx', v') + | IteExpr(c, e1, e2) -> + let c' = __EvalSym fullResolverFunc returnFunc ctx c + match c' with + | BoolLiteral(b) -> if b then __EvalSym resolverFunc returnFunc ctx e1 else __EvalSym resolverFunc returnFunc ctx e2 + | _ -> IteExpr(c', __EvalSym resolverFunc returnFunc ctx e1, __EvalSym resolverFunc returnFunc ctx e2) + | BinaryExpr(p,op,e1,e2) -> + let e1' = lazy (__EvalSym resolverFunc returnFunc ctx e1) + let e2' = lazy (__EvalSym resolverFunc returnFunc ctx e2) + let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force())) + match op with + | "=" -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + let eq = __CheckEqual e1'' e2'' + match eq with + | Some(b) -> BoolLiteral(b) + | None -> 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) + | _ -> 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) + | _ -> recomposed.Force() + | ">" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2) + | _ -> 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) + | _ -> recomposed.Force() + | ".." -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + match e1'', e2'' with + | IntLiteral(lo), IntLiteral(hi) -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n))) + | _ -> recomposed.Force(); + | "in" -> + match e1'.Force(), e2'.Force() with + | _, SetExpr(s) + | _, SequenceExpr(s) -> //BoolLiteral(Utils.ListContains (e1'.Force()) s) + if Utils.ListContains (e1'.Force()) s then + TrueLiteral + else + try + let contains = s |> List.map Expr2ConstStrict |> Utils.ListContains (e1'.Force() |> Expr2ConstStrict) + BoolLiteral(contains) + with + | _ -> recomposed.Force() + | _ -> recomposed.Force() + | "!in" -> + match e1'.Force(), e2'.Force() with + | _, SetExpr(s) + | _, SequenceExpr(s) -> //BoolLiteral(not (Utils.ListContains (e1'.Force()) s)) + if Utils.ListContains (e1'.Force()) s then + FalseLiteral + else + try + let contains = s |> List.map Expr2ConstStrict |> Utils.ListContains (e1'.Force() |> Expr2ConstStrict) + BoolLiteral(not contains) + with + | _ -> recomposed.Force() + | _ -> recomposed.Force() + | "+" -> + let e1'' = e1'.Force(); + let e2'' = e2'.Force(); + match e1'', e2'' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2) + | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | _ -> recomposed.Force() + | "-" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | _ -> recomposed.Force() + | "*" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2) + | _ -> recomposed.Force() + | "div" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2) + | _ -> recomposed.Force() + | "mod" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2) + | _ -> recomposed.Force() + | "&&" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(false) -> BoolLiteral(false) + | _ -> + match e1'.Force(), e2'.Force() with + | _, BoolLiteral(false) -> BoolLiteral(false) + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2) + | _ -> BinaryAnd (e1'.Force()) (e2'.Force()) + | "||" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(true) -> BoolLiteral(true) + | _ -> + match e1'.Force(), e2'.Force() with + | _, BoolLiteral(true) -> BoolLiteral(true) + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2) + | _ -> BinaryOr (e1'.Force()) (e2'.Force()) + | "==>" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(false) -> BoolLiteral(true) + | _ -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + BinaryImplies e1'' e2'' + | "<==>" -> + 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() + | OldExpr(e) -> + let e' = __EvalSym resolverFunc returnFunc ctx e + let recomposed = OldExpr(e') + match e with + | IdLiteral(name) -> resolverFunc (IdLiteral(RenameToOld name)) None + | _ -> recomposed + | UnaryExpr(op, e) -> + let e' = __EvalSym resolverFunc returnFunc ctx e + let recomposed = UnaryExpr(op, e') + match op with + | "!" -> + match e' with + | BoolLiteral(b) -> BoolLiteral(not b) + | _ -> recomposed + | "-" -> + match e' with + | IntLiteral(n) -> IntLiteral(-n) + | _ -> recomposed + | _ -> recomposed + | ForallExpr(vars, e) -> + let rec __ExhaustVar v restV vDomain = + match vDomain with + | vv :: restD -> + let ctx' = (v,vv) :: ctx + let e' = __EvalSym resolverFunc returnFunc ctx' (ForallExpr(restV, e)) + let erest = __ExhaustVar v restV restD + BinaryAnd e' erest + | [] -> BoolLiteral(true) + let rec __TraverseVars vars = + match vars with + | v :: restV -> + try + let vDom = GetVarDomain resolverFunc returnFunc ctx v e + __ExhaustVar v restV vDom + with + | ex -> ForallExpr([v], __TraverseVars restV) + | [] -> __EvalSym resolverFunc returnFunc ctx e + (* --- function body starts here --- *) + __TraverseVars vars + if expr' = FalseLiteral then + Logger.Debug "" + expr' |> returnFunc + and GetVarDomain resolverFunc returnFunc ctx var expr = + match expr with + | BinaryExpr(_, "==>", lhs, rhs) -> + let conjs = SplitIntoConjunts lhs + conjs |> List.fold (fun acc e -> + match e with + | BinaryExpr(_, "in", VarLiteral(vn), rhs) when GetVarName var = vn -> + match __EvalSym resolverFunc returnFunc ctx rhs with + | SetExpr(elist) + | SequenceExpr(elist) -> elist |> List.append acc + | x -> raise DomainNotInferred + | BinaryExpr(_, op, VarLiteral(vn),oth) + | BinaryExpr(_, op, oth, VarLiteral(vn)) when GetVarName var = vn && Set.ofList ["<"; "<="; ">"; ">="] |> Set.contains op -> + failwith "Not implemented yet" + | _ -> raise DomainNotInferred) [] + | _ -> + Logger.WarnLine ("unknown pattern for a quantified expression; cannot infer domain of quantified variable \"" + (GetVarName var) + "\"") + raise DomainNotInferred + (* --- function body starts here --- *) + __EvalSym otherResolverFunc returnFunc ctx expr + +let EvalSym resolverFunc expr = + EvalSym2 resolverFunc resolverFunc (fun e -> e) [] expr + +let EvalSymRet fullResolverFunc resolverFunc returnFunc expr = + EvalSym2 fullResolverFunc resolverFunc returnFunc [] expr + +// ========================================================== +/// Desugars a given expression so that all list constructors +/// are expanded into explicit assignments to indexed elements +// ========================================================== +let MyDesugar expr removeOriginal = + let rec __Desugar expr = + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | VarDeclExpr(_) + | IdLiteral(_) + | VarLiteral(_) + | ObjLiteral(_) + | Star + | Dot(_) + | SelectExpr(_) + | SeqLength(_) + | UpdateExpr(_) + | SetExpr(_) + | MethodCall(_) + | MethodOutSelect(_) + | SequenceExpr(_) -> expr + // forall v :: v in {a1 a2 ... an} ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] + // forall v :: v in [a1 a2 ... an] ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] + | ForallExpr([Var(vn1,ty1,old1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 -> + match rhsCol with + | SetExpr(elist) + | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (__Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral + | _ -> ForallExpr(v, __Desugar ee) + | ForallExpr(v,e) -> ForallExpr(v, __Desugar e) + | LCIntervalExpr(e) -> LCIntervalExpr(__Desugar e) + | OldExpr(e) -> OldExpr(__Desugar e) + | UnaryExpr(op,e) -> UnaryExpr(op, __Desugar e) + | AssertExpr(e) -> AssertExpr(__Desugar e) + | AssumeExpr(e) -> AssumeExpr(__Desugar e) + | IteExpr(c,e1,e2) -> IteExpr(c, __Desugar e1, __Desugar e2) + // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an && |lst| = n + | BinaryExpr(p,op,e1,e2) -> + let be = BinaryExpr(p, op, __Desugar e1, __Desugar e2) + let fs = if removeOriginal then TrueLiteral else be + try + match op with + | "=" -> + match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with + | SequenceExpr(l1), SequenceExpr(l2) -> + let rec __fff lst1 lst2 cnt = + match lst1, lst2 with + | fs1 :: rest1, fs2 :: rest2 -> BinaryEq l1.[cnt] l2.[cnt] :: __fff rest1 rest2 (cnt+1) + | [], [] -> [] + | _ -> failwith "Lists are of different sizes" + __fff l1 l2 0 |> List.fold (fun acc e -> BinaryAnd acc e) fs + | e, SequenceExpr(elist) + | SequenceExpr(elist), e -> + let rec __fff lst cnt = + match lst with + | fs :: rest -> BinaryEq (SelectExpr(e, IntLiteral(cnt))) elist.[cnt] :: __fff rest (cnt+1) + | [] -> [BinaryEq (SeqLength(e)) (IntLiteral(cnt))] + __fff elist 0 |> List.fold (fun acc e -> BinaryAnd acc e) fs + | _ -> be + | _ -> be + with + | EvalFailed(_) as ex -> (* printfn "%O" (ex.StackTrace); *) be + __Desugar expr + +let Desugar expr = MyDesugar expr false +let DesugarAndRemove expr = MyDesugar expr true + +let rec DesugarLst exprLst = + match exprLst with + | expr :: rest -> Desugar expr :: DesugarLst rest + | [] -> [] + +let ChangeThisReceiver receiver expr = + let rec __ChangeThis locals expr = + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | BoxLiteral(_) + | Star + | VarDeclExpr(_) + | VarLiteral(_) -> expr + | ObjLiteral("this") -> receiver + | ObjLiteral(_) -> expr + | IdLiteral("null") -> failwith "should never happen anymore" //TODO + | IdLiteral("this") -> failwith "should never happen anymore" + | IdLiteral(id) -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(ObjLiteral("this"), id)) + | Dot(e, id) -> Dot(__ChangeThis locals e, id) + | AssertExpr(e) -> AssertExpr(__ChangeThis locals e) + | AssumeExpr(e) -> AssumeExpr(__ChangeThis locals e) + | ForallExpr(vars,e) -> let newLocals = vars |> List.map GetVarName |> Set.ofList |> Set.union locals + ForallExpr(vars, __ChangeThis newLocals e) + | LCIntervalExpr(e) -> LCIntervalExpr(__ChangeThis locals e) + | OldExpr(e) -> OldExpr(__ChangeThis locals e) + | UnaryExpr(op,e) -> UnaryExpr(op, __ChangeThis locals e) + | SeqLength(e) -> SeqLength(__ChangeThis locals e) + | SelectExpr(e1, e2) -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2) + | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __ChangeThis locals e1, __ChangeThis locals e2) + | IteExpr(e1,e2,e3) -> IteExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) + | 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)) + | MethodOutSelect(e, name) -> MethodOutSelect(__ChangeThis locals e, name) + | MethodCall(rcv,cname, mname,aparams) -> MethodCall(__ChangeThis locals rcv, cname, mname, aparams |> List.map (__ChangeThis locals)) + (* --- function body starts here --- *) + __ChangeThis Set.empty expr + +let rec SimplifyExpr expr = + let __Simplify expr = + match expr with + | UnaryExpr("!", sub) -> Some(UnaryNot sub) + | BinaryExpr(_, "&&", l, r) -> Some(BinaryAnd l r) + | BinaryExpr(_, "||", l, r) -> Some(BinaryOr l r) + | BinaryExpr(_, "in", l, r) -> Some(BinaryIn l r) + | BinaryExpr(_, "!in", l, r) -> Some(BinaryNotIn l r) + | BinaryExpr(_, "==>", l, r) -> Some(BinaryImplies l r) + | BinaryExpr(_, "=", l, r) -> Some(BinaryEq l r) + | BinaryExpr(_, "!=", l, r) -> Some(BinaryNeq l r) + | _ -> None + RewriteBU __Simplify expr + +let rec ExtractTopLevelExpressions stmt = + match stmt with + | ExprStmt(e) -> [e] + | Assign(e1, e2) -> [e1; e2] + | Block(slist) -> slist |> List.fold (fun acc s -> acc @ ExtractTopLevelExpressions s) [] + +let rec PullUpMethodCalls stmt = + let stmtList = new System.Collections.Generic.LinkedList<_>() + let rec __PullUpMethodCalls expr = + let newExpr = RewriteBU (fun expr -> + match expr with + | MethodOutSelect(_) -> + let vname = SymGen.NewSymFake expr + let e' = VarLiteral(vname) + let var = VarDeclExpr([Var(vname,None,false)], true) + let asgn = BinaryGets var expr + stmtList.AddLast asgn |> ignore + Some(e') + | _ -> None + ) expr + newExpr, (stmtList |> List.ofSeq) + stmtList.Clear() + match stmt with + | ExprStmt(e) -> + let e', slist = __PullUpMethodCalls e + slist @ [ExprStmt(e')] + | Assign(e1, e2) -> + let e2', slist = __PullUpMethodCalls e2 + slist @ [Assign(e1, e2')] + | Block(slist) -> slist |> List.fold (fun acc s -> acc @ PullUpMethodCalls s) [] + +// ========================================================== +/// Very simple for now: +/// - if "m" is a constructor, everything is modifiable +/// - if the method's post condition contains assignments to fields, everything is modifiable +/// - otherwise, all objects are immutable +/// +/// (TODO: instead it should read the "modifies" clause of a method and figure out what's modifiable from there) +// ========================================================== +let IsModifiableObj obj (c,m) = + let __IsFld name = FindVar c name |> Utils.OptionToBool + match m with + | Method(name,_,_,_,_) when name.EndsWith("__mod__") -> true + | Method(_,_,_,_,true) -> true + | Method(_,_,_,post,false) -> + DescendExpr2 (fun e acc -> + match e with + | BinaryExpr(_,"=",IdLiteral(name),r) when __IsFld name -> true + | Dot(_,name) when __IsFld name -> true + | _ -> acc + ) post false + | _ -> failwithf "expected a Method but got %O" m \ No newline at end of file diff --git a/Source/Jennisys/CodeGen.fs b/Source/Jennisys/CodeGen.fs new file mode 100644 index 00000000..8df4ca60 --- /dev/null +++ b/Source/Jennisys/CodeGen.fs @@ -0,0 +1,429 @@ +module CodeGen + +open Ast +open Getters +open AstUtils +open Utils +open Resolver +open TypeChecker +open PrintUtils +open DafnyPrinter +open DafnyModelUtils +open Options + +let validFuncName = "Valid()" +let validSelfFuncName = "Valid_self()" +let validReprFuncName = "Valid_repr()" + +/// requires: numUnrols >= 0 +/// requires: |fldExprs| = |fldNames| +let rec GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse 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] + else + let exprList = fldExprs |> List.map (fun e -> BinaryImplies (__NotNull e) (Dot(e, validFuncToUse))) + if numUnrolls = 1 then + exprList + else + let fldExprs = __Combine fldExprs fldNames + List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse (numUnrolls - 1)) + +let GetFieldValidExpr flds validFunName numUnrolls = + let fldExprs = flds |> List.map (fun var -> IdLiteral(GetExtVarName var)) + let fldNames = flds |> List.map GetExtVarName + let unrolledExprs = GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls + // add the recursive definition as well + let recExprs = + if not (validFunName = validFuncName) && Options.CONFIG.recursiveValid then + flds //|> List.filter (fun var -> not ((GetExtVarName var).StartsWith("_back_"))) //don't use back pointers + |> List.map (fun var -> + let name = GetExtVarName var + BinaryImplies (BinaryNeq (IdLiteral(name)) NullLiteral) (Dot(IdLiteral(name), validFuncName))) + else + [] + recExprs @ unrolledExprs + +let GetFieldsForValidExpr allFields prog comp : VarDecl list = + let frameVars = GetFrameFields comp + allFields |> List.filter (fun var -> IsUserType prog (GetVarType var)) + |> List.filter (fun var -> Utils.ListContains var frameVars) + +let GetFieldsValidExprList clsName allFields prog : Expr list = + let fields = GetFieldsForValidExpr allFields prog (FindComponent prog clsName |> ExtractOption) + let fieldsByType = GroupFieldsByType fields + fieldsByType |> Map.fold (fun acc t varSet -> + let validFunName, numUnrolls = + match t with + | Some(ty) when clsName = (GetTypeShortName ty) -> validSelfFuncName, Options.CONFIG.numLoopUnrolls + | _ -> validFuncName, 1 + acc |> List.append (GetFieldValidExpr (Set.toList varSet) validFunName numUnrolls) + ) [] + +let PrintValidFunctionCode comp prog vars allInvs genRepr nameSuffix: string = + let validFuncName = "Valid" + nameSuffix + "()" + let validReprFuncName = "Valid_repr" + nameSuffix + "()" + let validSelfFuncName = "Valid_self" + nameSuffix + "()" + let idt = " " + let __PrintInvs invs = + invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) [] + |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e)) + |> fun s -> if s = "" then (idt + "true") else s + let clsName = GetClassName comp + let compTypeName = GetClassType comp |> PrintType + let hasLoop = vars |> List.exists (fun var -> match GetVarType var with Some(ty) when compTypeName = PrintType ty -> true | _ -> false) + let fieldsValid = GetFieldsValidExprList clsName vars prog + + let frameFldNames = GetFrameFields comp |> List.map GetExtVarName + 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 " + validReprFuncName + ": bool" + newline + + " reads *;" + newline + + " {" + newline + + validReprBody + newline + + " }" + newline + newline + else + "" + + let decreasesStr = + if Options.CONFIG.recursiveValid then + if hasLoop then + if genRepr then + " decreases Repr;" + newline + else + // TODO: Dafny currently doesn't accept "decreases *" on methods + " decreases *;" + newline + else + "" + else "" + vr + + " function " + validSelfFuncName + ": bool" + newline + + " reads *;" + newline + + " {" + newline + + (if genRepr then " " + validReprFuncName + " &&" + newline else "") + + (__PrintInvs allInvs) + newline + + " }" + newline + + newline + + " function " + validFuncName + ": bool" + newline + + " reads *;" + newline + + decreasesStr + + " {" + newline + + " this." + validSelfFuncName + " &&" + newline + + (__PrintInvs fieldsValid) + newline + + " }" + newline + +let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr genOld = + match prog with + | Program(components) -> components |> List.fold (fun acc comp -> + match comp with + | Component(Interface(name,typeParams,members), DataModel(_,_,cVars,frame,inv), code) as comp -> + let aVars = FilterFieldMembers members + let aOldVars = MakeOldVars aVars + let cOldVars = MakeOldVars cVars + let allInvs = GetInvariantsAsList comp |> DesugarLst + let allOldInvs = MakeOld (allInvs |> List.fold BinaryAnd TrueLiteral) |> SplitIntoConjunts + let aVarsAndRepr = aVars |> List.append (Utils.Ite genRepr [Var("Repr", Some(SetType(NamedType("object", []))), false)] []) + let compMethods = FilterConstructorMembers members + // Now print it as a Dafny program + acc + + (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline + + // the fields: original abstract fields plus concrete fields + (sprintf "%s" (PrintFields aVarsAndRepr 2 true)) + newline + + (sprintf "%s" (PrintFields cVars 2 false)) + newline + + (if genOld then + (sprintf "%s" (PrintFields aOldVars 2 true)) + newline + + (sprintf "%s" (PrintFields cOldVars 2 false)) + newline + else + "") + + // generate the Valid function + (sprintf "%s" (PrintValidFunctionCode comp prog (aVars @ cVars) allInvs genRepr "")) + newline + + (if genOld then + (sprintf "%s" (PrintValidFunctionCode comp prog (aOldVars @ cOldVars) allOldInvs genRepr "_old")) + newline + else + "") + + // call the method printer function on all methods of this component + (methodPrinterFunc comp) + + // the end of the class + "}" + newline + newline + | _ -> assert false; "") "" + +let PrintPrePost pfix expr = + SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";") + +let GetPreconditionForMethod m = + let validExpr = IdLiteral(validFuncName); + if IsConstructor m then + GetMethodPrePost m |> fst + else + BinaryAnd validExpr (GetMethodPrePost m |> fst) + +let GetPostconditionForMethod prog m genRepr = + let validExpr = IdLiteral(validFuncName); + match m with + | Method(_,_,_,post,isConstr) -> + // this.Valid() and user-defined post-condition + let postExpr = BinaryAnd validExpr post + // method out args are valid + let postExpr = (GetMethodOutArgs m) |> List.fold (fun acc var -> + if IsUserType prog (GetVarType var) then + let varExpr = VarLiteral(GetExtVarName var) + let argValidExpr = BinaryImplies (BinaryNeq varExpr NullLiteral) (Dot(varExpr, validFuncName)) + BinaryAnd acc argValidExpr + else + acc + ) postExpr + // fresh Repr + if genRepr then + let freshExpr = if isConstr then "fresh(Repr - {this})" else "fresh(Repr - old(Repr))"; + BinaryAnd (IdLiteral(freshExpr)) postExpr + else + postExpr + | _ -> failwithf "expected a method, got %O" m + +let PrintAssumePostcondition prog m genRepr prefix = + PrintPrePost prefix (GetPostconditionForMethod prog m genRepr |> Desugar) + newline + +let GetAllocObjects heapInst = + heapInst.assignments |> List.fold (fun acc a -> + match a with + | FieldAssignment((obj,fld),_) when not (obj.name = "this") -> + acc |> Set.add obj + | FieldAssignment(_, ObjLiteral(name)) when not (name = "this" || name = "null") -> + acc |> Set.add (heapInst.objs |> Map.find name) + | _ -> acc + ) Set.empty + +let PrintAllocNewObjects heapInst indent = + let idt = Indent indent + GetAllocObjects heapInst |> Set.fold (fun acc obj -> acc + (sprintf "%svar %s := new %s;%s" idt obj.name (PrintType obj.objType) newline)) "" + +let PrintVarAssignments heapInst indent = + let idt = Indent indent + let stmts = ConvertToStatements heapInst true + let str = stmts |> PrintSep (newline) (fun s -> (PrintStmt s indent false)) + str + newline + +/// +let PrintReprAssignments prog heapInst indent = + let __FollowsFunc o1 o2 = + heapInst.assignments |> List.fold (fun acc assgn -> + match assgn with + | FieldAssignment ((srcObj,fld),value) -> acc || (srcObj = o1 && value = ObjLiteral(o2.name)) + | _ -> false + ) false + let idt = Indent indent + let objs = heapInst.assignments |> List.fold (fun acc assgn -> + match assgn with + | FieldAssignment((obj,var),_) -> if GetVarName var = "" then acc else acc |> Set.add obj + | _ -> acc + ) Set.empty + |> Set.toList + |> Utils.TopSort __FollowsFunc + |> List.rev + let rec __GetReprConcrete obj = + let expr = SetExpr([ObjLiteral(obj.name)]) + let builder = CascadingBuilder<_>(expr) + builder { + let typeName = GetTypeShortName obj.objType + let! comp = FindComponent prog typeName + let vars = GetFrameFields comp + let nonNullVars = vars |> List.choose (fun v -> + let lst = heapInst.assignments |> List.choose (function FieldAssignment(x,y) -> Some(x,y) | _ -> None) + match Utils.ListMapTryFind (obj,v) lst with + | Some(ObjLiteral(n)) when not (n = "null" || n = obj.name) -> Some(v,n) + | _ -> None) + return nonNullVars |> List.map (fun (var,objName) -> var,(Map.find objName heapInst.objs)) + |> List.fold (fun acc (var,varValObj) -> + if Options.CONFIG.genMod then + BinaryAdd acc (Dot(Dot(ObjLiteral(obj.name), (GetVarName var)), "Repr")) + else + BinaryAdd acc (__GetReprConcrete varValObj) + ) expr + } + + let reprGetsList = objs |> List.fold (fun acc obj -> + let objStmt = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) (__GetReprConcrete obj) + objStmt :: acc +// 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 -> +// let lst = heapInst.assignments |> List.choose (function FieldAssignment(x,y) -> Some(x,y) | _ -> None) +// match Utils.ListMapTryFind (obj,v) lst with +// | Some(ObjLiteral(n)) when not (n = "null") -> true +// | _ -> false) +// return nonNullVars |> List.fold (fun a v -> +// BinaryAdd a (Dot(Dot(ObjLiteral(obj.name), (GetVarName v)), "Repr")) +// ) expr +// } +// let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs +// fullReprExpr :: acc + ) [] + + let reprStr = if not (reprGetsList = []) then + idt + "// repr stuff" + newline + + (PrintStmtList reprGetsList indent true) + else + "" + + let reprValidExpr = GetAllocObjects heapInst |> Set.fold (fun acc obj -> BinaryAnd acc (Dot(ObjLiteral(obj.name), validFuncName))) TrueLiteral + + let assertValidStr = if not (reprValidExpr = TrueLiteral) then + idt + "// assert repr objects are valid (helps verification)" + newline + + (PrintStmt (ExprStmt(AssertExpr(reprValidExpr))) indent true) + else + "" + let outStr = reprStr + assertValidStr + if outStr = "" then + outStr + else + newline + outStr + +let rec PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr = + let rec __RewriteOldStmt stmt = + match stmt with + | Assign(l, r) -> Assign(l, BringToPost r) + | ExprStmt(e) -> ExprStmt(BringToPost e) + | Block(slist) -> Block(slist |> List.map __RewriteOldStmt) + + let __RewriteOldAsgn a = + match a with + | FieldAssignment((o,f),e) -> FieldAssignment((o,f), BringToPost e) + | ArbitraryStatement(stmt) -> ArbitraryStatement(__RewriteOldStmt stmt) + + /// inserts an assignments into a list of assignments such that the list remains + /// topologically sorted wrt field dependencies between different assignments + let rec __InsertSorted asgsLst asg = + let ___DependsOn dependentAsg asg = + match asg, dependentAsg with + | FieldAssignment((o,f),_), FieldAssignment(_,e) -> + let mf = fun e acc -> + match e with + | IdLiteral(name) when name = GetVarName f && o.name = "this" -> true + | Dot(discr, name) -> + let t1 = InferType prog comp (fun s -> None) discr + let t2 = FindComponentForType prog o.objType + acc || (name = GetVarName f && t1 = t2) + | _ -> acc + DescendExpr2 (mf + ) e false + | _ -> false + match asgsLst with + | [] -> [asg] + | a :: rest -> if ___DependsOn a asg then asg :: a :: rest else a :: __InsertSorted rest asg + + /// - removes all FieldAssignments to unmodifiable objects and old variables + /// - rewrites expressions not to use old fields + let __RemoveUnmodifiableStuff heapInst = + let newAsgs = heapInst.assignments |> List.fold (fun acc a -> + match a with + | FieldAssignment((obj,_),_) when not (Set.contains obj heapInst.modifiableObjs) -> acc + | FieldAssignment((_,var),_) when IsOldVar var -> acc + | _ -> __InsertSorted acc (__RewriteOldAsgn a) + ) [] + { heapInst with assignments = newAsgs } + + let idt = Indent indent + match sol with + | (c, hi) :: rest -> + let heapInstMod = __RemoveUnmodifiableStuff hi + let __ReprAssignments ind = + if genRepr then + (PrintReprAssignments prog heapInstMod ind) + else + "" + if c = TrueLiteral then + (PrintAllocNewObjects heapInstMod indent) + + (PrintVarAssignments heapInstMod indent) + + (__ReprAssignments indent) + + (PrintHeapCreationCodeOld prog (comp,meth) rest indent genRepr) + else + if List.length rest > 0 then + idt + "if (" + (PrintExpr 0 c) + ") {" + newline + + (PrintAllocNewObjects heapInstMod (indent+2)) + + (PrintVarAssignments heapInstMod (indent+2)) + + (__ReprAssignments (indent+2)) + + idt + "} else {" + newline + + (PrintHeapCreationCodeOld prog (comp,meth) rest (indent+2) genRepr) + + idt + "}" + newline + else + (PrintAllocNewObjects heapInstMod indent) + + (PrintVarAssignments heapInstMod indent) + + (__ReprAssignments indent) + | [] -> "" + +let PrintHeapCreationCode prog (comp,meth) sol indent genRepr = + let idt = Indent indent + let ghostPre = GetMethodGhostPrecondition meth + if ghostPre = TrueLiteral then + PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr + else + (ghostPre |> SplitIntoConjunts |> PrintSep newline (fun e -> idt + "assume " + (PrintExpr 0 e) + ";")) + newline + + (PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr) + +let GenConstructorCode prog comp mthd decreasesClause body genRepr = + let validExpr = IdLiteral(validFuncName); + match mthd with + | Method(methodName,sign,_,_,isConstr) -> + let preExpr = GetPreconditionForMethod mthd |> Desugar + let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar + let thisObj = ThisObj comp + " method " + methodName + (PrintSig sign) + + (if IsModifiableObj thisObj (comp,mthd) then newline + " modifies this;" else "") + + (PrintPrePost (newline + " requires ") preExpr) + + (PrintPrePost (newline + " ensures ") postExpr) + + newline + + decreasesClause + + " {" + newline + + body + + " }" + newline + | _ -> "" + +let GetDecreasesClause (c,m) sol = + if IsRecursiveSol (c,m) sol then + " decreases Repr;" + newline + else + "" + +// solutions: (comp, constructor) |--> condition * heapInst +let PrintImplCode prog solutions genRepr = + PrintDafnyCodeSkeleton prog (fun comp -> + let cname = GetComponentName comp + solutions |> Map.fold (fun acc (c,m) sol -> + if (GetComponentName c) = cname then + let mthdBody,decr = + match sol with + | [] -> + let body = " //unable to synthesize" + + (PrintAssumePostcondition prog m genRepr (newline + " assume ")) + let decr = "" + body,decr + | _ -> + let body = PrintHeapCreationCode prog (c,m) sol 4 genRepr + let decr = GetDecreasesClause (c,m) sol + body,decr + acc + newline + (GenConstructorCode prog comp m decr mthdBody genRepr) + newline + + else + acc) "") genRepr \ No newline at end of file diff --git a/Source/Jennisys/DafnyModelUtils.fs b/Source/Jennisys/DafnyModelUtils.fs new file mode 100644 index 00000000..e734f3bb --- /dev/null +++ b/Source/Jennisys/DafnyModelUtils.fs @@ -0,0 +1,455 @@ +// ######################################################################### +/// Utilities for reading/building models from Boogie Visual Debugger files +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// ######################################################################### + +module DafnyModelUtils + +(* + The heap maps objects and fields to locations. + heap: Const * VarDecl option |--> Const + + The environment maps locations to values (except that it can also + be locations to locations, because not all values are explicitly + present in the model. + envMap: Const |--> Const + + The context is just a list of equality constraints collected on the way + ctx: Set>, where the inner set contains exactly two constants +*) + +open Ast +open Getters +open AstUtils +open Utils + +open Microsoft.Boogie + +let HEAP_SELECT_FNAME = "MapType1Select" +let SEQ_BUILD_FNAME = "Seq#Build" +let SEQ_APPEND_FNAME = "Seq#Append" +let SEQ_LENGTH_FNAME = "Seq#Length" +let SEQ_INDEX_FNAME = "Seq#Index" +let SET_EMPTY_FNAME = "Set#Empty" +let SET_SELECT_FNAME = "MapType0Select" +let UNBOX_FNAME = "$Unbox" +let BOOL_2_U_FNAME = "bool_2_U" +let U_2_BOOL_FNAME = "U_2_bool" +let INT_2_U_FNAME = "int_2_U" +let U_2_INT_FNAME = "U_2_int" +let DTYPE_FNAME = "dtype" +let NULL_FNAME = "null" + +type HeapModel = { + heap : Map; + env : Map; + ctx : Set>; +} + +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) + |> Seq.choose (fun ft -> Some(ft.Func.Name)) + |> Utils.SeqToOption + +let GetRefName (ref: Model.Element) = + match ref with + | :? Model.Uninterpreted as uref -> uref.Name + | _ -> failwith ("not a ref (Uninterpreted) but: " + ref.GetType().Name) + +let GetInt (elem: Model.Element) = + let __NotIntFail e = failwith ("not an int element: " + elem.ToString()) + let rec __GetIntStrict (e: Model.Element) cont = + match e with + | :? Model.Number as ival -> ival.AsInt() + | _ -> cont e + __GetIntStrict elem (fun e -> + let f = e.Model.MkFunc(U_2_INT_FNAME, 1) + let matches = f.Apps |> Seq.filter (fun ft -> ft.Args.[0] = e) |> Seq.map (fun ft -> ft.Result) + if matches |> Seq.isEmpty then + __NotIntFail e + else + __GetIntStrict (matches |> Seq.nth 0) __NotIntFail) + +let GetBool (elem: Model.Element) = + let __NotBoolFail e = failwith ("not a bool element: " + elem.ToString()) + let rec __GetBoolStrict (e: Model.Element) cont = + match e with + | :? Model.Boolean as bval -> bval.Value + | _ -> cont e + __GetBoolStrict elem (fun e -> + let f = e.Model.MkFunc(U_2_BOOL_FNAME, 1) + let matches = f.Apps |> Seq.filter (fun ft -> ft.Args.[0] = e) |> Seq.map (fun ft -> ft.Result) + if matches |> Seq.isEmpty then + __NotBoolFail e + else + __GetBoolStrict (matches |> Seq.nth 0) __NotBoolFail) + +let ConvertValue (refVal: Model.Element) = + match refVal with + | :? Model.Number as ival -> IntConst(ival.AsInt()) + | :? Model.Boolean as bval -> BoolConst(bval.Value) + | :? Model.Array as aval -> failwith "reading array values from model not implemented" + | :? Model.Uninterpreted as uval -> + try BoolConst(GetBool refVal) + with _ -> try IntConst(GetInt refVal) + with _ -> Unresolved(uval.Name) (* just a symbolic name for now, which we'll hopefully resolve later*) + | _ -> failwith ("unexpected model element kind: " + refVal.ToString()) + +let LastDotSplit (str: string) = + let dotIdx = str.LastIndexOf(".") + let s1 = if dotIdx = -1 then "" else str.Substring(0, dotIdx) + let s2 = str.Substring(dotIdx + 1) + s1,s2 + +let GetType (e: Model.Element) prog = + let fNameOpt = GetElemFullName e + match fNameOpt with + | Some(fname) -> match fname with + | "intType" -> Some(IntType) + | Prefix "class." clsName -> + let _,shortClsName = LastDotSplit clsName + match FindComponent prog shortClsName with + | Some(comp) -> Some(GetClassType comp) + | None -> None + | _ -> None + | None -> None + +let GetLoc (e: Model.Element) = + Unresolved(GetRefName e) + +let FindOrCreateSeq env key len = + match Map.tryFind key env with + | Some(SeqConst(lst)) -> lst,env + | None -> + let emptyList = Utils.GenList len NoneConst + let newSeq = SeqConst(emptyList) + let newMap = env |> Map.add key newSeq + emptyList,newMap + | Some(_) as x-> failwith ("not a SeqConst but: " + x.ToString()) + +let FindSeqInEnv env key = + match Map.find key env with + | SeqConst(lst) -> lst + | _ as x-> failwith ("not a SeqConst but: " + x.ToString()) + +let TryFindSetInEnv env key = + match Map.tryFind key env with + | Some(SetConst(s)) -> Some(s) + | Some(x) -> failwith ("not a SetConst but: " + x.ToString()) + | None -> None + +let AddConstr c1 c2 ctx = + if c1 = c2 then + ctx + else + match c1, c2 with + | Unresolved(_), _ | _, Unresolved(_) -> + // find partitions + let s1Opt = ctx |> Set.filter (fun ss -> Set.contains c1 ss) |> Utils.SetToOption + let s2Opt = ctx |> Set.filter (fun ss -> Set.contains c2 ss) |> Utils.SetToOption + match s1Opt, s2Opt with + // both already exist --> so just merge them + | Some(s1), Some(s2) -> ctx |> Set.remove s1 |> Set.remove s2 |> Set.add (Set.union s1 s2) + // exactly one already exists --> add to existing + | Some(s1), None -> ctx |> Set.remove s1 |> Set.add (Set.add c2 s1) + | None, Some(s2) -> ctx |> Set.remove s2 |> Set.add (Set.add c1 s2) + // neither exists --> create a new one + | None, None -> ctx |> Set.add (Set.ofList [c1; c2]) + | _ -> failwith ("trying to add an equality constraint between two constants: " + c1.ToString() + ", and " + c2.ToString()) + +let rec UpdateContext lst1 lst2 ctx = + match lst1, lst2 with + | fs1 :: rest1, fs2 :: rest2 -> + match fs1, fs2 with + | NoneConst,_ | _,NoneConst -> UpdateContext rest1 rest2 ctx + | _ -> UpdateContext rest1 rest2 (AddConstr fs1 fs2 ctx) + | [], [] -> ctx + | _ -> failwith "lists are not of the same length" + +let UnboxIfNeeded (model: Microsoft.Boogie.Model) (e: Model.Element) = + let f_unbox = model.MkFunc(UNBOX_FNAME, 2) + let unboxed = f_unbox.Apps |> Seq.filter (fun ft -> if (GetLoc ft.Args.[1]) = (GetLoc e) then true else false) + |> Seq.choose (fun ft -> Some(ft.Result)) + |> Utils.SeqToOption + match unboxed with + | Some(e) -> ConvertValue e + | None -> GetLoc e + +let ReadHeap (model: Microsoft.Boogie.Model) prog = + let f_heap_select = model.MkFunc(HEAP_SELECT_FNAME, 3) + let values = f_heap_select.Apps + values |> Seq.fold (fun acc ft -> + assert (ft.Args.Length = 3) + let ref = ft.Args.[1] + let fld = ft.Args.[2] + assert (Seq.length fld.Names = 1) + let fldFullName = (Seq.nth 0 fld.Names).Func.Name + let pfix,fldName = LastDotSplit fldFullName + let _,clsName = LastDotSplit pfix + let refVal = ft.Result + let refObj = Unresolved(GetRefName ref) + let nonebuilder = CascadingBuilder<_>(None) + let fldVarOpt = nonebuilder { + let! comp = FindComponent prog clsName + if fldName.StartsWith("old_") then + let fn = RenameFromOld fldName + let! var = FindVar comp fn + return Some(MakeOldVar var) + else + return FindVar comp fldName + } + match fldVarOpt with + | Some(fldVar) -> + let fldType = GetVarType fldVar + let fldVal = ConvertValue refVal + acc |> Map.add (refObj, fldVar) fldVal + | None -> acc + ) Map.empty + +// ==================================================================== +/// Reads values that were assigned to given arguments. Those values +/// can be in functions with the same name as the argument name appended +/// with an "#" and some number after it. +// ==================================================================== +let rec ReadArgValues (model: Microsoft.Boogie.Model) args = + match args with + | v :: rest -> + let name = GetVarName v + let farg = model.Functions |> Seq.filter (fun f -> f.Arity = 0 && f.Name.StartsWith(name + "#")) |> Utils.SeqToOption + match farg with + | Some(func) -> + let fldVar = v + assert (Seq.length func.Apps = 1) + let ft = Seq.head func.Apps + let fldVal = ConvertValue (ft.Result) + ReadArgValues model rest |> Map.add (VarConst(name)) fldVal + | None -> failwith ("cannot find corresponding function for parameter " + name) + | [] -> Map.empty + +// ============================================================== +/// Reads stuff about sequences from a given model and ads it to +/// the given "envMap" map and a "ctx" set. The relevant stuff is +/// fetched from the following functions: +/// Seq#Length, Seq#Index, Seq#Build, Seq#Append +// ============================================================== +let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = + // reads stuff from Seq#Length + let rec __ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) = + match len_tuples with + | ft :: rest -> + let len = GetInt ft.Result + let emptyList = Utils.GenList len NoneConst + let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList)) + __ReadSeqLen model rest (newMap,ctx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Index + let rec __ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) = + match idx_tuples with + | ft :: rest -> + let srcLstKey = GetLoc ft.Args.[0] + let idx = GetInt ft.Args.[1] + let oldLst,envMap = FindOrCreateSeq envMap srcLstKey (idx+1) + let lstElem = UnboxIfNeeded model ft.Result + let newLst = Utils.ListSet idx lstElem oldLst + let newCtx = UpdateContext oldLst newLst ctx + let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst)) + __ReadSeqIndex model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Build + let rec __ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) = + match bld_tuples with + | ft :: rest -> + let srcLstLoc = GetLoc ft.Args.[0] + let lstElemVal = UnboxIfNeeded model ft.Args.[1] + let dstLstLoc = GetLoc ft.Result + let oldLst = FindSeqInEnv envMap srcLstLoc + let dstLst = FindSeqInEnv envMap dstLstLoc + let newLst = oldLst @ [lstElemVal] + let newCtx = UpdateContext dstLst newLst ctx + let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) + __ReadSeqBuild model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Append + let rec __ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) = + match app_tuples with + | ft :: rest -> + let srcLst1Loc = GetLoc ft.Args.[0] + let srcLst2Loc = GetLoc ft.Args.[1] + let dstLstLoc = GetLoc ft.Result + let oldLst1 = FindSeqInEnv envMap srcLst1Loc + let oldLst2 = FindSeqInEnv envMap srcLst2Loc + let dstLst = FindSeqInEnv envMap dstLstLoc + let newLst = oldLst1 @ oldLst2 + let newCtx = UpdateContext dstLst newLst ctx + let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) + __ReadSeqAppend model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + + // keeps reading from Seq#Build and Seq#Append until fixpoint + let rec __ReadUntilFixpoint hmodel = + let f_seq_bld = model.MkFunc(SEQ_BUILD_FNAME, 2) + let f_seq_app = model.MkFunc(SEQ_APPEND_FNAME, 2) + let hmodel' = hmodel |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps) + |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps) + if hmodel' = hmodel then + hmodel' + else + __ReadUntilFixpoint hmodel' + + let f_seq_len = model.MkFunc(SEQ_LENGTH_FNAME, 1) + let f_seq_idx = model.MkFunc(SEQ_INDEX_FNAME, 2) + let hmodel = (envMap,ctx) + let hmodel' = hmodel |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps) + |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps) + __ReadUntilFixpoint hmodel' + + + +// ===================================================== +/// Reads stuff about sets from a given model and adds it +/// to the given "envMap" map and "ctx" set. +// ===================================================== +let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = + // reads stuff from Set#Empty + let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) = + match empty_tuples with + | ft :: rest -> + let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty)) + __ReadSetEmpty rest (newMap,ctx) + | [] -> (envMap,ctx) + + // reads stuff from [2] + let rec __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = + match set_tuples with + | ft :: rest -> + if GetBool ft.Result then + let srcSetKey = GetLoc ft.Args.[0] + let srcSet = match TryFindSetInEnv env srcSetKey with + | Some(s) -> s + | None -> Set.empty + let elem = UnboxIfNeeded model ft.Args.[1] + let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) + __ReadSetMembership rest (newEnv,ctx) + else + __ReadSetMembership rest (env,ctx) + | [] -> (env,ctx) + + let t_set_empty = Seq.toList (model.MkFunc(SET_EMPTY_FNAME, 1).Apps) + let t_set = Seq.toList (model.MkFunc(SET_SELECT_FNAME, 2).Apps) + (envMap,ctx) |> __ReadSetEmpty t_set_empty + |> __ReadSetMembership t_set + +(* More complicated way which now doesn't seem to be necessary *) +//let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = +// // reads stuff from Set#Empty +// let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) = +// match empty_tuples with +// | ft :: rest -> +// let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty)) +// __ReadSetEmpty rest (newMap,ctx) +// | [] -> (envMap,ctx) +// +// // reads stuff from Set#UnionOne and Set#Union +// let rec __ReadSetUnions (envMap,ctx) = +// // this one goes through a given list of "UnionOne" tuples, updates +// // the env for those set that it was able to resolve, and returns a +// // list of tuples for which it wasn't able to resolve sets +// let rec ___RSU1 (tuples: Model.FuncTuple list) env unprocessed = +// match tuples with +// | ft :: rest -> +// let srcSetKey = GetLoc ft.Args.[0] +// match TryFindSetInEnv env srcSetKey with +// | Some(oldSet) -> +// let elem = UnboxIfNeeded model ft.Args.[1] +// let newSet = Set.add elem oldSet +// // update contex? +// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet)) +// ___RSU1 rest newEnv unprocessed +// | None -> ___RSU1 rest env (ft :: unprocessed) +// | [] -> (env,unprocessed) +// // this one goes through a given list of "Union" tuples, updates +// // the env for those set that it was able to resolve, and returns a +// // list of tuples for which it wasn't able to resolve sets +// let rec ___RSU (tuples: Model.FuncTuple list) env unprocessed = +// match tuples with +// | ft :: rest -> +// let set1Key = GetLoc ft.Args.[0] +// let set2Key = GetLoc ft.Args.[1] +// match TryFindSetInEnv env set1Key, TryFindSetInEnv env set2Key with +// | Some(oldSet1), Some(oldSet2) -> +// let newSet = Set.union oldSet1 oldSet2 +// // update contex? +// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet)) +// ___RSU rest newEnv unprocessed +// | _ -> ___RSU rest env (ft :: unprocessed) +// | [] -> (env,unprocessed) +// // this one keeps looping as loong as the list of unprocessed tuples +// // is decreasing, it ends when if falls down to 0, or fails if +// // the list stops decreasing +// let rec ___RSU_until_fixpoint u1tuples utuples env = +// let newEnv1,unprocessed1 = ___RSU1 u1tuples env [] +// let newEnv2,unprocessed2 = ___RSU utuples newEnv1 [] +// let oldLen = (List.length u1tuples) + (List.length utuples) +// let totalUnprocLen = (List.length unprocessed1) + (List.length unprocessed2) +// if totalUnprocLen = 0 then +// newEnv2 +// elif totalUnprocLen < oldLen then +// ___RSU_until_fixpoint unprocessed1 unprocessed2 newEnv2 +// else +// failwith "cannot resolve all sets in Set#UnionOne/Set#Union" +// // finally, just invoke the fixpoint function for UnionOne and Union tuples +// let t_union_one = Seq.toList (model.MkFunc("Set#UnionOne", 2).Apps) +// let t_union = Seq.toList (model.MkFunc("Set#Union", 2).Apps) +// let newEnv = ___RSU_until_fixpoint t_union_one t_union envMap +// (newEnv,ctx) +// +// let f_set_empty = model.MkFunc("Set#Empty", 1) +// (envMap,ctx) |> __ReadSetEmpty (List.ofSeq f_set_empty.Apps) +// |> __ReadSetUnions + +// ====================================================== +/// Reads staff about the null constant from a given model +/// and adds it to the given "envMap" map and "ctx" set. +// ====================================================== +let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = + let f_null = model.MkFunc(NULL_FNAME, 0) + assert (f_null.AppCount = 1) + let e = (f_null.Apps |> Seq.nth 0).Result + let newEnv = envMap |> Map.add (GetLoc e) NullConst + (newEnv,ctx) + +// ============================================================================================ +/// Reads the evinronment map and the context set. +/// +/// It starts by reading the model for the "dtype" function to discover all objects on the heap, +/// and then proceeds by reading stuff about the null constant, about sequences, and about sets. +// ============================================================================================ +let ReadEnv (model: Microsoft.Boogie.Model) prog = + let f_dtype = model.MkFunc(DTYPE_FNAME, 1) + let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0])) + let envMap = f_dtype.Apps |> Seq.fold (fun acc ft -> + let locName = GetRefName ft.Args.[0] + let elemName = GetElemFullName ft.Args.[0] + let loc = Unresolved(locName) + let locType = GetType ft.Result prog + let value = match elemName with + | Some(n) when n.StartsWith("this") -> ThisConst(locName.Replace("*", ""), locType) + | _ -> NewObj(locName.Replace("*", ""), locType) + acc |> Map.add loc value + ) Map.empty + (envMap, Set.ofList([])) |> ReadNull model + |> ReadSeq model + |> ReadSet model + +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)) + MkHeapModel heap env ctx \ No newline at end of file diff --git a/Source/Jennisys/DafnyPrinter.fs b/Source/Jennisys/DafnyPrinter.fs new file mode 100644 index 00000000..f2e71e8b --- /dev/null +++ b/Source/Jennisys/DafnyPrinter.fs @@ -0,0 +1,135 @@ +module DafnyPrinter + +open Ast +open Getters +open AstUtils +open PrintUtils + +let rec PrintType ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | SeqType(t) -> sprintf "seq<%s>" (PrintType t) + | SetType(t) -> sprintf "set<%s>" (PrintType t) + | NamedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args) + | InstantiatedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args) + +let PrintVarDecl vd = + let name = GetExtVarName vd + match GetVarType vd with + | None -> name + | Some(ty) -> sprintf "%s: %s" name (PrintType ty) + +let rec PrintExpr ctx expr = + match expr with + | IntLiteral(d) -> sprintf "%d" d + | BoolLiteral(b) -> sprintf "%b" b + | BoxLiteral(id) -> sprintf "box_%s" id + | ObjLiteral(id) + | VarLiteral(id) + | IdLiteral(id) -> id + | VarDeclExpr(vlist, declare) -> + let decl = if declare then "var " else "" + let vars = PrintSep ", " PrintVarDecl vlist + sprintf "%s%s" decl vars + | Star -> "*" + | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id + | LCIntervalExpr(e) -> sprintf "%s.." (PrintExpr 90 e) + | OldExpr(e) -> sprintf "old(%s)" (PrintExpr 90 e) + | 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,"in",lhs,BinaryExpr(_,"...",lo,hi)) -> + let needParens = strength <= ctx + let openParen = if needParens then "(" else "" + let closeParen = if needParens then ")" else "" + let loStr = PrintExpr strength lo + let hiStr = PrintExpr strength hi + let lhsStr = PrintExpr strength lhs + sprintf "%s%s <= %s && %s <= %s%s" openParen loStr lhsStr lhsStr hiStr closeParen + | BinaryExpr(strength,op,e0,e1) -> + let op = + match op with + | "=" -> "==" + | "div" -> "/" + | "mod" -> "%" + | _ -> op + 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 "(if %s then %s else %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)) + | AssertExpr(e) -> sprintf "assert %s" (PrintExpr 0 e) + | AssumeExpr(e) -> sprintf "assume %s" (PrintExpr 0 e) + | ForallExpr(vv,e) -> + let needParens = true + 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 + | MethodCall(rcv,_,name,aparams) -> + sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0)) + | MethodOutSelect(mth,name) -> + // TODO: this can only work if there is only 1 out parameter + sprintf "%s" (PrintExpr 0 mth) + +let rec PrintConst cst = + match cst with + | IntConst(v) -> sprintf "%d" v + | BoolConst(b) -> sprintf "%b" b + | BoxConst(id) -> sprintf "box_%s" id + | 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 -> "" + | 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 PrintTypeParams typeParams = + match typeParams with + | [] -> "" + | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) + +let PrintFields vars indent ghost = + let ghostStr = if ghost then "ghost " else "" + vars |> List.fold (fun acc v -> match GetVarType v with + | None -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr (GetExtVarName v) newline) + | Some(tp) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr (GetExtVarName v) (PrintType tp) newline)) "" + +let rec _PrintStmt stmt indent printNewline = + let idt = Indent indent + let nl = if printNewline then newline else "" + match stmt with + | Block(stmts) -> + idt + "{" + nl + + (_PrintStmtList stmts (indent + 2) true) + + idt + "}" + nl + | Assign(lhs,rhs) -> sprintf "%s%s := %s;%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) nl + | ExprStmt(expr) -> sprintf "%s%s;%s" idt (PrintExpr 0 expr) nl +and _PrintStmtList stmts indent printNewLine = + let idt = Indent indent + let str = stmts |> PrintSep newline (fun s -> _PrintStmt s indent false) + if printNewLine then + str + newline + else + str + +let PrintStmt stmt indent printNewline = + let stmts = PullUpMethodCalls stmt + _PrintStmtList stmts indent printNewline + +let PrintStmtList stmts indent printNewLine = + stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent printNewLine)) "" \ No newline at end of file diff --git a/Source/Jennisys/EnvUtils.fs b/Source/Jennisys/EnvUtils.fs new file mode 100644 index 00000000..0b840311 --- /dev/null +++ b/Source/Jennisys/EnvUtils.fs @@ -0,0 +1,9 @@ +module EnvUtils + +open Ast + +let GetThisLoc env = + Map.findKey (fun k v -> + match v with + | ThisConst(_) -> true + | _ -> false) env \ No newline at end of file diff --git a/Source/Jennisys/FixpointSolver.fs b/Source/Jennisys/FixpointSolver.fs new file mode 100644 index 00000000..1ca3b057 --- /dev/null +++ b/Source/Jennisys/FixpointSolver.fs @@ -0,0 +1,374 @@ +module FixpointSolver + +open Ast +open AstUtils +open Printer +open Resolver +open Utils + +///////////// + +type UnifDirection = LTR | RTL + +exception CannotUnify + +let rec SelectiveUnifyImplies okToUnifyFunc lhs rhs dir unifs = + /// + let __AddOrNone unifs name e = + if okToUnifyFunc name then + Some(unifs |> Utils.MapAddNew name e) + else + None + + /// + let __UnifLists lstL lstR = + if List.length lstL = List.length lstR then + try + let unifs2 = List.fold2 (fun acc elL elR -> match SelectiveUnifyImplies okToUnifyFunc elL elR dir acc with + | Some(u) -> u + | None -> raise CannotUnify) unifs lstL lstR + Some(unifs2) + with + | CannotUnify -> None + else + None + + /// + let __ApplyUnifs unifs exprList = + exprList |> List.fold (fun acc e -> + let e' = e |> Rewrite (fun e -> + match e with + | VarLiteral(id) when Map.containsKey id unifs -> Some(unifs |> Map.find id) + | _ -> None) + acc |> Set.add e' + ) Set.empty + + if lhs = FalseLiteral || rhs = TrueLiteral then + Some(unifs) + else + try + let l,r = match dir with + | LTR -> lhs,rhs + | RTL -> rhs,lhs + match l, r with + | VarLiteral(vname), rhs -> __AddOrNone unifs vname rhs + | IntLiteral(nL), IntLiteral(nR) when nL = nR -> + Some(unifs) + | BoolLiteral(bL), BoolLiteral(bR) when bL = bR -> + Some(unifs) + | SetExpr(elistL), SetExpr(elistR) -> + let s1 = elistL |> __ApplyUnifs unifs + let s2 = elistR |> Set.ofList + if (s1 = s2) then + Some(unifs) + else + __UnifLists elistL elistR + | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR -> + __UnifLists elistL elistR + | _ when l = r -> + Some(unifs) + | _ -> + let __TryUnifyPair x1 a1 x2 a2 unifs = + let builder = new Utils.CascadingBuilder<_>(None) + builder { + let! unifsLhs = SelectiveUnifyImplies okToUnifyFunc x1 a1 dir unifs + let! unifsRhs = SelectiveUnifyImplies okToUnifyFunc x2 a2 dir unifsLhs + return Some(unifsRhs) + } + + // target implies candidate! + let rec ___f2 consequence premise unifs = + match consequence, premise with + // same operators + commutative -> try both + | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC && IsCommutativeOp opT -> + match __TryUnifyPair lhsC lhsT rhsC rhsT unifs with + | Some(x) -> Some(x) + | None -> __TryUnifyPair lhsC rhsT rhsC lhsT unifs + // operators are the same + | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opC = opT -> + __TryUnifyPair lhsC lhsT rhsC rhsT unifs + // operators are exactly the invers of one another + | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when AreInverseOps opC opT -> + __TryUnifyPair lhsC rhsT rhsC lhsT unifs + // + | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when DoesImplyOp opC opT -> + __TryUnifyPair lhsC lhsT rhsC rhsT unifs + | UnaryExpr(opC, subC), UnaryExpr(opP, subP) when opC = opP -> + SelectiveUnifyImplies okToUnifyFunc subP subC dir unifs + | SelectExpr(lstC, idxC), SelectExpr(lstP, idxP) -> + __TryUnifyPair lstP lstC idxP idxC unifs + | SeqLength(lstC), SeqLength(lstP) -> + SelectiveUnifyImplies okToUnifyFunc lstP lstC dir unifs + | Dot(exprC, fldNameC), Dot(exprP, fldNameP) when fldNameC = fldNameP -> + SelectiveUnifyImplies okToUnifyFunc exprP exprC dir unifs + | _ -> None + + let rec ___f1 targetLst candidateLst unifs = + match targetLst, candidateLst with + | targetExpr :: targetRest, candExpr :: candRest -> + // trying to find a unification for "targetExpr" + let uOpt = match ___f2 targetExpr candExpr unifs with + // found -> just return + | Some(unifs2) -> Some(unifs2) + // not found -> keep looking in the rest of the candidate expressions + | None -> ___f1 [targetExpr] candRest unifs + match uOpt with + // found -> try find for the rest of the target expressions + | Some(unifs2) -> ___f1 targetRest candidateLst unifs2 + // not found -> fail + | None -> None + | targetExpr :: _, [] -> + // no more candidates for unification for this targetExpr -> fail + None + | [], _ -> + // we've found unifications for all target expressions -> return the current unifications map + Some(unifs) + + let __HasSetExpr e = DescendExpr2 (fun ex acc -> if acc then true else match ex with SetExpr(_) -> true | _ -> false) e false + let __PreprocSplitSort e = e |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts |> List.sortBy (fun e -> if __HasSetExpr e then 1 else 0) + let lhsConjs = lhs |> __PreprocSplitSort + let rhsConjs = rhs |> __PreprocSplitSort + ___f1 rhsConjs lhsConjs unifs + with + | CannotUnify + | KeyAlreadyExists -> None + +let UnifyImplies lhs rhs dir unifs = SelectiveUnifyImplies (fun e -> true) lhs rhs dir unifs + +//////////////////////////////////////////// + +let rec ComputeClosure heapInst expandExprFunc premises = + let bogusExpr = VarLiteral("!@#$%^&*()") + + let ApplyUnifs unifs expr = + Rewrite (function + | VarLiteral(id) when unifs |> Map.containsKey id -> + Some(unifs |> Map.find id) + | _ -> None + ) expr + + let FindMatches expr except premises = + //Logger.TraceLine ("finding matches for: " + (PrintExpr 0 expr) + "; #premises = " + (Set.count premises |> sprintf "%i")) + let okToUnifyFunc = fun (varName: string) -> varName.StartsWith("$") + if expr = TrueLiteral then + [] + else + let matches = + premises |> Set.toList + |> List.choose (function BinaryExpr(_,"=",lhs,rhs) -> + if lhs = expr && not (rhs = except) then + Some(rhs) + elif rhs = expr && not (lhs = except) then + Some(lhs) + else + match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with + | Some(unifs) -> Some(ApplyUnifs unifs rhs) + | None -> + match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with + | Some(unifs) -> Some(ApplyUnifs unifs lhs) + | None -> None + | _ -> None) + //Logger.TraceLine (sprintf "Number of matches for %s: %i" (PrintExpr 0 expr) (List.length matches)) + matches + + let MySetAdd expr set = + let x = Printer.PrintExpr 0 expr + if x.Contains("$") || not (expandExprFunc expr) then + set + else + match expr with + | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && Set.contains (BinaryExpr(p,op,rhs,lhs)) set -> set + | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && rhs = lhs -> set + | _ -> Set.add expr set + + let SelectExprCombinerFunc lst idx = + // distribute the indexing operation if possible + let rec __fff lst idx = + //Logger.TraceLine ("SelectExpr fff for " + (PrintExpr 0 lst)) + let selExpr = SelectExpr(lst, idx) + match lst with + | BinaryExpr(_,"+",lhs,rhs) -> + let idxVal = EvalFull heapInst idx |> Expr2Int + let lhsVal = EvalFull heapInst lhs |> Expr2List + let rhsVal = EvalFull heapInst rhs |> Expr2List + if idxVal < List.length lhsVal then + __fff lhs idx + else + __fff rhs (BinarySub idx (IntLiteral(List.length lhsVal))) + | SequenceExpr(elist) -> + let idxVal = EvalFull heapInst idx |> Expr2Int + [elist.[idxVal]] + | _ -> [selExpr] + __fff lst idx + + let SeqLenCombinerFunc lst = + // distribute the SeqLength operation if possible + let rec __fff lst = + //Logger.TraceLine ("SeqLen fff for " + (PrintExpr 0 lst)) + let lenExpr = SeqLength(lst) + match lst with + | BinaryExpr(_,"+",lhs,rhs) -> + BinaryAdd (__fff lhs) (__fff rhs) //TODO: this ought to be incorrect! + | SequenceExpr(elist) -> + IntLiteral(List.length elist) + | _ -> lenExpr + [__fff lst] + + let BinaryInCombiner lhs rhs = + // distribute the "in" operation if possible + let rec __fff lhs rhs = + //Logger.TraceLine ("In fff for " + (PrintExpr 0 lhs) + " and " + (PrintExpr 0 rhs)) + let binInExpr = BinaryIn lhs rhs +// match rhs with +// | BinaryExpr(_,"+",BinaryExpr(_,"+",SetExpr(_), Dot(_)), Dot(_)) -> Logger.Trace "" +// | _ -> ()//TODO: remove + + match rhs with + | BinaryExpr(_,"+",l,r) -> +// let lhsVal = EvalFull heapInst lhs +// let lVal = EvalFull heapInst l +// let rVal = EvalFull heapInst r +// match lVal,rVal with +// | SequenceExpr(elist), _ | _, SequenceExpr(elist) +// | SetExpr(elist), _ | _, SetExpr(elist) -> +// if elist |> Utils.ListContains lhsVal then +// __fff lhs l +// else +// __fff lhs r +// | _ -> [binInExpr] +/////////////////////////////// +// [BinaryOr (BinaryIn lhs l) (BinaryIn lhs r)] + let opt1 = BinaryIn lhs l + let opt2 = BinaryIn lhs r + match EvalFull heapInst opt1 with + | BoolLiteral(true) -> [opt1] + | _ -> match EvalFull heapInst opt2 with + | BoolLiteral(true) -> [opt2] + | _ -> Utils.ListCombine BinaryOr (__fff lhs l) (__fff lhs r) + //[BinaryOr (BinaryIn lhs l)(BinaryIn lhs r)] + | SequenceExpr(elist) -> + let len = elist |> List.length + if len = 0 then + [FalseLiteral] + elif len = 1 then + [BinaryEq lhs elist.[0]] + else + let lhsVal = EvalFull heapInst lhs + let lst0Val = EvalFull heapInst elist.[0] + if lhsVal = lst0Val then + [BinaryEq lhs elist.[0]] + else + __fff lhs (SequenceExpr(elist |> List.tail)) + //[BinaryIn lhs (SequenceExpr(elist |> List.tail))] + | SetExpr(elist) -> + let evalElist = elist |> List.map (EvalFull heapInst) + let evalLhs = EvalFull heapInst lhs + try + let idx = evalElist |> List.findIndex (fun e -> e = evalLhs) + [BinaryEq lhs elist.[idx]] + with + | _ -> [binInExpr] + | _ -> [binInExpr] + __fff lhs rhs + + let BinaryNotInCombiner lhs rhs = + // distribute the "!in" operation if possible + let rec __fff lhs rhs = + //Logger.TraceLine ("NotIn fff for " + (PrintExpr 0 lhs) + " and " + (PrintExpr 0 rhs)) + let binNotInExpr = BinaryNotIn lhs rhs + match rhs with + | BinaryExpr(_,"+",l,r) -> +// let lhsVal = EvalFull heapInst lhs +// let lVal = EvalFull heapInst l +// let rVal = EvalFull heapInst r +// match lVal,rVal with +// | SequenceExpr(elistL), SequenceExpr(elistR) +// | SetExpr(elistL), SetExpr(elistR) -> +// (__fff lhs l) @ +// (__fff lhs r) +// | _ -> [binNotInExpr] + __fff lhs l @ __fff lhs r + | SequenceExpr(elist) -> + let len = elist |> List.length + if len = 0 then + [TrueLiteral] + elif len = 1 then + [BinaryNeq lhs elist.[0]] + else + let lhsVal = EvalFull heapInst lhs + let lst0Val = EvalFull heapInst elist.[0] + [BinaryNeq lhs elist.[0]] @ + __fff lhs (SequenceExpr(elist |> List.tail)) + //[BinaryNotIn lhs (SequenceExpr(elist |> List.tail))] + | _ -> [binNotInExpr] + __fff lhs rhs + + let rec __CombineAllMatches expr premises = + //Logger.TraceLine ("Combining all matches for: " + (PrintExpr 0 expr)) + let lst0 = FindMatches expr bogusExpr premises + let lstCombined = + match expr with + | BinaryExpr(p,op,lhs,rhs) -> + let lhsMatches = __CombineAllMatches lhs premises + let rhsMatches = __CombineAllMatches rhs premises + let lst1 = Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches + let lst2 = + if op = "in" then + Utils.ListCombineMult BinaryInCombiner lhsMatches rhsMatches + elif op = "!in" then + Utils.ListCombineMult BinaryNotInCombiner lhsMatches rhsMatches + else + [] + lst1 @ lst2 + | UnaryExpr(op,sub) -> + __CombineAllMatches sub premises |> List.map (fun e -> UnaryExpr(op,e)) + | SelectExpr(lst,idx) -> + let lstMatches = __CombineAllMatches lst premises + let idxMatches = __CombineAllMatches idx premises + Utils.ListCombineMult SelectExprCombinerFunc lstMatches idxMatches + | SeqLength(lst) -> + __CombineAllMatches lst premises |> List.map SeqLenCombinerFunc |> List.concat + // TODO: other cases + | _ -> [] + expr :: (lst0 @ lstCombined) + + let rec __ExpandPremise expr premises = + let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd e acc) premises + let allMatches = lazy(__CombineAllMatches expr premises) + match expr with + | BinaryExpr(p,op,lhs,rhs) when IsRelationalOp op -> + let x = allMatches.Force() + __AddToPremisses x premises + | SelectExpr(lst, idx) -> + let x = allMatches.Force() + __AddToPremisses x premises + | _ -> premises + + let rec __Iter exprLst premises = + match exprLst with + | expr :: rest -> + let newPremises = + if expandExprFunc expr then + //Logger.TraceLine ("expanding " + (PrintExpr 0 expr)) + __ExpandPremise expr premises + else + premises + __Iter rest newPremises + | [] -> premises + + (* --- function body starts here --- *) + let iterOnceFunc p = __Iter (p |> Set.toList) p + // TODO: iterate only 3 times, instead of to full closure + let p1 = iterOnceFunc premises + let p2 = p1 |> iterOnceFunc + //let p3 = p2 |> iterOnceFunc + p2 +// let premises' = iterOnceFunc premises +// if premises' = premises then +// premises' +// else +// Logger.TraceLine "-------closure----------------" +// //premises' |> Set.iter (fun e -> Logger.TraceLine (Printer.PrintExpr 0 e)) +// ComputeClosure heapInst expandExprFunc premises' + + diff --git a/Source/Jennisys/Getters.fs b/Source/Jennisys/Getters.fs new file mode 100644 index 00000000..2e2732af --- /dev/null +++ b/Source/Jennisys/Getters.fs @@ -0,0 +1,284 @@ +module Getters + +open Ast + +let RenameToOld name = + "old_" + name + +let RenameFromOld (name: string) = + if name.StartsWith("old_") then + name.Substring(4) + else + name + +// --- search functions --- + +// ================================== +/// Returns variable name +// ================================== +let GetVarName var = + match var with + | Var(name,_,_) -> name + +let GetExtVarName var = + match var with + | Var(id, _, false) -> id + | Var(id, _, true) -> RenameToOld id + +let IsOldVar var = + match var with + | Var(_,_,isOld) -> isOld + +// ================================== +/// Returns variable type +// ================================== +let GetVarType var = + match var with + | Var(_,t,_) -> t + +// =============================================== +/// Returns whether there exists a variable +/// in a given VarDecl list with a given name (id) +// =============================================== +let IsInVarList varLst id = + varLst |> List.exists (fun var -> GetVarName var = id) + + +// ========================================================= +/// Out of all "members" returns only those that are "Field"s +// ========================================================= +let FilterFieldMembers members = + members |> List.choose (function Field(vd) -> Some(vd) | _ -> None) + +// ============================================================= +/// Out of all "members" returns only those that are constructors +// ============================================================= +let FilterConstructorMembers members = + members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None) + +// ============================================================= +/// Out of all "members" returns only those that are +/// constructors and have at least one input parameter +// ============================================================= +let FilterConstructorMembersWithParams members = + members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) + +// ========================================================== +/// Out of all "members" returns only those that are "Method"s +// ========================================================== +let FilterMethodMembers members = + members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None) + +// ======================================================================= +/// Returns all members of the program "prog" that pass the filter "filter" +// ======================================================================= +let FilterMembers prog filter = + match prog with + | Program(components) -> + components |> List.fold (fun acc comp -> + match comp with + | Component(Interface(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))] + | _ -> acc) [] + +let GetAbstractFields comp = + match comp with + | Component(Interface(_,_,members), _, _) -> FilterFieldMembers members + | _ -> failwithf "internal error: invalid component: %O" comp + +let GetConcreteFields comp = + match comp with + | Component(_, DataModel(_,_,cVars,_,_), _) -> cVars + | _ -> failwithf "internal error: invalid component: %O" comp + +// ================================= +/// Returns all fields of a component +// ================================= +let GetAllFields comp = + List.concat [GetAbstractFields comp; GetConcreteFields comp] + +// =========================================================== +/// Returns a map (Type |--> Set) 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, old) :: 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, old))) + | [] -> Map.empty + +let IsConcreteField comp fldName = GetConcreteFields comp |> List.exists (fun var -> GetVarName var = fldName) +let IsAbstractField comp fldName = GetAbstractFields comp |> List.exists (fun var -> GetVarName var = fldName) + +// ================================= +/// Returns class name of a component +// ================================= +let GetClassName comp = + match comp with + | Component(Interface(name,_,_),_,_) -> name + | _ -> failwith ("unrecognized component: " + comp.ToString()) + +let GetClassType comp = + match comp with + | Component(Interface(name,typeParams,_),_,_) -> NamedType(name, typeParams) + | _ -> failwith ("unrecognized component: " + comp.ToString()) + +// ======================== +/// Returns name of a method +// ======================== +let GetMethodName mthd = + match mthd with + | Method(name,_,_,_,_) -> name + | _ -> failwith ("not a method: " + mthd.ToString()) + +// =========================================================== +/// Returns full name of a method (= . +// =========================================================== +let GetMethodFullName comp mthd = + (GetClassName comp) + "." + (GetMethodName mthd) + +// ============================= +/// Returns signature of a method +// ============================= +let GetMethodSig mthd = + match mthd with + | Method(_,sgn,_,_,_) -> sgn + | _ -> failwith ("not a method: " + mthd.ToString()) + +// ========================================================= +/// Returns all arguments of a method (both input and output) +// ========================================================= +let GetSigVars sign = + match sign with + | Sig(ins, outs) -> List.concat [ins; outs] + +let GetMethodInArgs mthd = + match mthd with + | Method(_,Sig(ins, _),_,_,_) -> ins + | _ -> failwith ("not a method: " + mthd.ToString()) + +let GetMethodOutArgs mthd = + match mthd with + | Method(_,Sig(_, outs),_,_,_) -> outs + | _ -> failwith ("not a method: " + mthd.ToString()) + +let GetMethodArgs mthd = + let ins = GetMethodInArgs mthd + let outs = GetMethodOutArgs mthd + List.concat [ins; outs] + +let IsConstructor mthd = + match mthd with + | Method(_,_,_,_,isConstr) -> isConstr + | _ -> failwithf "expected a method but got %O" mthd + +let rec GetTypeShortName ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | SetType(_) -> "set" + | SeqType(_) -> "seq" + | NamedType(n,_) | InstantiatedType(n,_) -> n + +// ================================== +/// Returns component name +// ================================== +let GetComponentName comp = + match comp with + | Component(Interface(name,_,_),_,_) -> name + | _ -> failwithf "invalid component %O" comp + +let GetComponentTypeParameters comp = + match comp with + | Component(Interface(_,tp,_),_,_) -> tp + | _ -> failwithf "invalid component %O" comp + + +// ================================== +/// Returns all members of a component +// ================================== +let GetMembers comp = + match comp with + | Component(Interface(_,_,members),_,_) -> members + | _ -> failwith ("unrecognized component: " + comp.ToString()) + +// ==================================================== +/// Finds a component of a program that has a given name +// ==================================================== +let FindComponent (prog: Program) clsName = + match prog with + | Program(comps) -> comps |> List.filter (function Component(Interface(name,_,_),_,_) when name = clsName -> true | _ -> false) + |> Utils.ListToOption + +let FindComponentForType prog ty = + FindComponent prog (GetTypeShortName ty) + +let FindComponentForTypeOpt prog tyOpt = + match tyOpt with + | Some(ty) -> FindComponentForType prog ty + | None -> None + +let CheckSameCompType comp ty = + GetComponentName comp = GetTypeShortName ty + +let GetComponentType comp = + NamedType(GetComponentName comp, GetComponentTypeParameters comp) + +// =================================================== +/// Finds a method of a component that has a given name +// =================================================== +let FindMethod comp methodName = + let x = GetMembers comp + let y = x |> FilterMethodMembers + let z = y |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false) + GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false) + |> Utils.ListToOption + +// ============================================== +/// Finds a field of a class that has a given name +// ============================================== +//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 (fun var -> GetVarName var = fldName) + |> Utils.ListToOption + +// ====================================== +/// Returns the frame of a given component +// ====================================== +let GetFrame comp = + match comp with + | Component(_, DataModel(_,_,_,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 + ) + +// ============================================== +/// Checks whether two given methods are the same. +/// +/// Methods are the same if their names are the +/// same and their components have the same name. +// ============================================== +let CheckSameMethods (c1,m1) (c2,m2) = + GetComponentName c1 = GetComponentName c2 && GetMethodName m1 = GetMethodName m2 + +//////////////////////// \ No newline at end of file diff --git a/Source/Jennisys/Jennisys.fs b/Source/Jennisys/Jennisys.fs new file mode 100644 index 00000000..b10c9cfc --- /dev/null +++ b/Source/Jennisys/Jennisys.fs @@ -0,0 +1,72 @@ +// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases +// Learn more about F# at http://fsharp.net +// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio +// This posting is provided "AS IS" with no warranties, and confers no rights. +module Main + +open System +open System.IO +open Microsoft.FSharp.Text.Lexing + +open Ast +open AstUtils +open Lexer +open Options +open Parser +open Printer +open TypeChecker +open Analyzer + +let readAndProcess (filename: string) = + printfn "// Jennisys, Copyright (c) 2011, Microsoft." + // lex + let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader + let lexbuf = LexBuffer.FromTextReader(f) + lexbuf.EndPos <- { pos_bol = 0; + pos_fname=if filename = null then "stdin" else filename; + pos_cnum=0; + pos_lnum=1 } + + let sprog = + try + // parse + Parser.start Lexer.tokenize lexbuf + with + | ex -> + let pos = lexbuf.EndPos + printfn " [PARSE ERROR]: %s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + Environment.Exit(1) + failwith "" + match TypeCheck sprog with + | None -> () // errors have already been reported + | Some(prog) -> + Analyze prog filename + + +try + let args = Environment.GetCommandLineArgs() + ParseCmdLineArgs (List.ofArray args |> List.tail) + if CONFIG.breakIntoDebugger then ignore (System.Diagnostics.Debugger.Launch()) else () + if CONFIG.help then + printfn "%s" PrintHelpMsg + else + if CONFIG.inputFilename = "" then + printfn "*** Error: No input file was specified." + else + readAndProcess CONFIG.inputFilename +with + | InvalidCmdLineOption(msg) + | InvalidCmdLineArg(msg) as ex -> + printfn " [ERROR] %s" msg; + printfn "%s" PrintHelpMsg + | EvalFailed(msg) as ex -> + printfn " [EVALUATION ERROR] %s" msg + printfn "%O" ex.StackTrace + +//let mc = MethodOutSelect (MethodCall(IdLiteral("left"),"SetNode","Find",[VarLiteral("n")]), "ret") +//let expr = BinaryOr (BinaryOr (BinaryEq (VarLiteral("a")) (VarLiteral("b"))) mc) (mc) +//printfn "%s" (PrintExpr 0 expr) +//printfn "" +// +//let stmt = ExprStmt(expr) +//printfn "%s" (DafnyPrinter.PrintStmt stmt 0 false) \ No newline at end of file diff --git a/Source/Jennisys/Jennisys.fsproj b/Source/Jennisys/Jennisys.fsproj new file mode 100644 index 00000000..d3493749 --- /dev/null +++ b/Source/Jennisys/Jennisys.fsproj @@ -0,0 +1,118 @@ + + + + Debug + x86 + 8.0.30703 + 2.0 + {f2ff4b3a-2fe8-474a-88df-6950f7d78908} + Exe + Language + Jennisys + v4.0 + Client + Language + + + true + full + false + false + bin\Debug\ + DEBUG;TRACE + 3 + x86 + bin\Debug\Language.XML + examples/oopsla12/IntSet.jen /method:IntSet.Singleton + C:\boogie\Jennisys\Jennisys\ + + + pdbonly + true + true + bin\Release\ + TRACE + 3 + x86 + bin\Release\Language.XML + + + + + $(IntermediateOutputPath) + $(IntermediateOutputPath) + + + + + + + + + + + + false + Parser.fs + + + false + Lexer.fs + + + + + --module Parser + + + --unicode + + + + + + + + + + + + + + + + ..\..\Binaries\Boogie.exe + + + C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll + + + + + + + + + + Model + {acef88d5-dadd-46da-bae1-2144d63f4c83} + True + + + + + \ No newline at end of file diff --git a/Source/Jennisys/Lexer.fsl b/Source/Jennisys/Lexer.fsl new file mode 100644 index 00000000..e1d4795b --- /dev/null +++ b/Source/Jennisys/Lexer.fsl @@ -0,0 +1,83 @@ +{ +module Lexer +open System +open Parser +open Microsoft.FSharp.Text.Lexing + +let lexeme lexbuf = + LexBuffer.LexemeString lexbuf +} + +// These are some regular expression definitions +let digit = ['0'-'9'] +let nondigit = [ 'a'-'z' 'A'-'Z' '_' ] +let idchar = (nondigit | digit) +let whitespace = [' ' '\t' ] +let newline = ('\n' | '\r' '\n') + +rule tokenize = parse +| whitespace { tokenize lexbuf } +| newline { lexbuf.EndPos <- lexbuf.EndPos.NextLine; tokenize lexbuf } +// TODO: | "//"[-newline]* { tokenize lexbuf } +// keywords +| "interface" { INTERFACE } +| "datamodel" { DATAMODEL } +| "code" { CODE } +| "var" { VAR } +| "constructor" { CONSTRUCTOR } +| "method" { METHOD } +| "frame" { FRAME } +| "invariant" { INVARIANT } +| "returns" { RETURNS } +| "requires" { REQUIRES } +| "ensures" { ENSURES } +| "forall" { FORALL } +// Types +| "int" { INTTYPE } +| "bool" { BOOLTYPE } +| "seq" { SEQTYPE } +| "set" { SETTYPE } +// Operators +| "..." { DOTDOTDOT } +| ".." { DOTDOT } +| "." { DOT } +| "old" { OLD } +| "+" { PLUS } +| "-" { MINUS } +| "*" { STAR } +| "div" { DIV } +| "mod" { MOD } +| "&&" { AND } +| "||" { OR } +| "!" { NOT } +| "==>" { IMPLIES } +| "<==>" { IFF } +| "<" { LESS } +| "<=" { ATMOST } +| "=" { EQ } +| "!=" { NEQ } +| ">=" { ATLEAST } +| ">" { GREATER } +| "in" { IN } +| "!in" { NOTIN } +// Misc +| ":=" { GETS } +| "(" { LPAREN } +| ")" { RPAREN } +| "[" { LBRACKET } +| "]" { RBRACKET } +| "{" { LCURLY } +| "}" { RCURLY } +| "|" { VERTBAR } +| ":" { COLON } +| "::" { COLONCOLON } +| "," { COMMA } +| "?" { QMARK } +// Numberic constants +| digit+ { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) } +// identifiers +| idchar+ { ID (LexBuffer.LexemeString lexbuf) } +// EOF +| eof { EOF } +| _ { printfn "Unrecognized input character: %s" (lexeme lexbuf) ; EOF } + diff --git a/Source/Jennisys/Logger.fs b/Source/Jennisys/Logger.fs new file mode 100644 index 00000000..dbf762cd --- /dev/null +++ b/Source/Jennisys/Logger.fs @@ -0,0 +1,41 @@ +// ####################################################### +/// Simple logging facility +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// ####################################################### + +module Logger + +let newline = System.Environment.NewLine + +let _ALL = 100 +let _TRACE = 90 +let _DEBUG = 70 +let _INFO = 50 +let _WARN = 40 +let _ERROR = 20 +let _NONE = 0 + +let logLevel = _ALL + +let Log level msg = + if logLevel >= level then + printf "%s" msg + +let LogLine level msg = + Log level (msg + newline) + +let Trace msg = Log _TRACE msg +let TraceLine msg = LogLine _TRACE msg + +let Debug msg = Log _DEBUG msg +let DebugLine msg = LogLine _DEBUG msg + +let Info msg = Log _INFO msg +let InfoLine msg = LogLine _INFO msg + +let Warn msg = Log _WARN msg +let WarnLine msg = LogLine _WARN msg + +let Error msg = Log _ERROR msg +let ErrorLine msg = LogLine _ERROR msg \ No newline at end of file diff --git a/Source/Jennisys/MethodUnifier.fs b/Source/Jennisys/MethodUnifier.fs new file mode 100644 index 00000000..d2b1db68 --- /dev/null +++ b/Source/Jennisys/MethodUnifier.fs @@ -0,0 +1,107 @@ +module MethodUnifier + +open Ast +open Getters +open AstUtils +open FixpointSolver +open PrintUtils +open Resolver +open Utils + +let TryUnify targetMthd candMethod = + let targetPre,targetPost = GetMethodPrePost targetMthd + let targetPre = BinaryAnd targetPre (GetMethodGhostPrecondition targetMthd) + let candPre,candPost = GetMethodPrePost candMethod + let candPre = BinaryAnd candPre (GetMethodGhostPrecondition candMethod) + let builder = new CascadingBuilder<_>(None) + builder { + let! unifs1 = UnifyImplies targetPre candPre RTL Map.empty + let! unifs2 = UnifyImplies candPost targetPost LTR unifs1 + return Some(unifs2) + } + +let rec TryFindAMatch targetMthd candidateMethods = + let targetMthdName = GetMethodName targetMthd + match candidateMethods with + | candMthd :: rest -> + if GetMethodName candMthd = targetMthdName then + // skip if it is the same method + TryFindAMatch targetMthd rest + else + match TryUnify targetMthd candMthd with + | Some(unifs) -> Some(candMthd,unifs) + | None -> TryFindAMatch targetMthd rest + | [] -> None + +let TryFindExistingOpt comp targetMthd = + TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) + +let TryFindExisting comp targetMthd = + match TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with + | Some(m,unifs) -> m,unifs + | None -> targetMthd, Map.empty + +let ApplyMethodUnifs receiver (c,m) unifs = + let __Apply args = args |> List.map (fun var -> + let name = GetExtVarName var + match Map.tryFind name unifs with + | Some(e) -> e + | None -> VarLiteral(name)) + let ins = GetMethodInArgs m |> __Apply + let outs = GetMethodOutArgs m |> __Apply + + let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e -> + let vname = SymGen.NewSymFake e + let v = Var(vname, None, false) + let acc1' = acc1 @ [v] + let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))] + acc1', acc2' + ) ([],[]) + let mcallExpr = MethodCall(receiver, GetComponentName c, GetMethodName m, ins) + match retVars, outs with + | [], [] -> [ArbitraryStatement(ExprStmt(mcallExpr))] + | [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None, false)], false), mcallExpr))] + | _ -> + let mcall = ArbitraryStatement(Assign(VarDeclExpr(retVars, true), mcallExpr)) + mcall :: asgs + +// ==================================================== +/// +// ==================================================== +let TryFindExistingAndConvertToSolution indent comp m cond callGraph = + let __Calls caller callee = + let keyOpt = callGraph |> Map.tryFindKey (fun (cc,mm) mset -> CheckSameMethods (comp,caller) (cc,mm)) + match keyOpt with + | Some(k) -> callGraph |> Map.find k |> Set.contains ((GetComponentName comp),(GetMethodName callee)) + | None -> false + (* --- function body starts here --- *) + if not Options.CONFIG.genMod then + None + else + let idt = Indent indent + let candidateMethods = GetMembers comp |> List.filter (fun cm -> + match cm with + | Method(mname,_,_,_,_) when not (__Calls cm m) -> true + | _ -> false) + match TryFindAMatch m candidateMethods with + | Some(m',unifs) -> + Logger.InfoLine (idt + " - substitution method found:") + Logger.InfoLine (Printer.PrintMethodSignFull (indent+6) comp m') + Logger.DebugLine (idt + " Unifications: ") + let idtt = idt + " " + unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug + let obj = { name = "this"; objType = GetClassType comp } + let modObjs = if IsModifiableObj obj (comp,m) then Set.singleton obj else Set.empty + let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs + let hInst = { objs = Utils.MapSingleton obj.name obj; + modifiableObjs = modObjs; + assignments = body; + concreteValues = body; + methodArgs = Map.empty; + methodRetVals = Map.empty; + concreteMethodRetVals = Map.empty; + globals = Map.empty } + Some(Map.empty |> Map.add (comp,m) [cond, hInst] + |> Map.add (comp,m') []) + | None -> None + diff --git a/Source/Jennisys/Modularizer.fs b/Source/Jennisys/Modularizer.fs new file mode 100644 index 00000000..f5d7e7b7 --- /dev/null +++ b/Source/Jennisys/Modularizer.fs @@ -0,0 +1,206 @@ +module Modularizer + +open Ast +open Getters +open AstUtils +open MethodUnifier +open PrintUtils +open Resolver +open Utils + +// ======================================================================= +/// Merges two solution maps so that if there are multiple entries for a +/// single (comp,method) pair it concatenates them (corresponds to multiple +/// branches). +// ======================================================================= +let MergeSolutions sol1 sol2 = + let rec __Merge sol1map sol2lst res = + match sol2lst with + | ((c2,m2), lst2) :: rest -> + match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> CheckSameMethods (c1,m1) (c2,m2)) with + | Some(c1,m1) -> + let lst1 = sol1map |> Map.find(c1,m1) + let newRes = res |> Map.add (c1,m1) (lst1@lst2) + __Merge sol1map rest newRes + | None -> + let newRes = res |> Map.add (c2,m2) lst2 + __Merge sol1map rest newRes + | [] -> res + (* --- function body starts here --- *) + __Merge sol1 (sol2 |> Map.toList) sol1 + +// =========================================== +/// +// =========================================== +let rec MakeModular indent prog comp meth cond hInst callGraph = + let directChildren = lazy (GetDirectModifiableChildren hInst) + + let __IsAbstractField ty var = + let builder = CascadingBuilder<_>(false) + let varName = GetVarName var + builder { + let! comp = FindComponent prog (GetTypeShortName ty) + let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None + return true + } + + let __FindObj objName = + try + //hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst + hInst.assignments |> List.choose (function FieldAssignment((obj,_),_) -> + if (obj.name = objName) then Some(obj) else None + | _ -> None) + |> List.head + with + | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth) + + let __GetObjLitType objLitName = + (__FindObj objLitName).objType + + // =============================================================================== + /// Goes through the assignments of the heapInstance and returns only those + /// assignments that correspond to abstract fields of the given "objLitName" object + // =============================================================================== + let __GetAbsFldAssignments objLitName = + hInst.assignments |> List.choose (function + FieldAssignment ((obj,var),e) -> + if obj.name = objLitName && __IsAbstractField obj.objType var then + Some(var,e) + else + None + | _ -> None) + + // =============================================================================== + /// The given assignment is: + /// x := e + /// + /// If e is an object (e.g. gensym32) with e.g. two abstract fields "a" and "b", + /// with values 3 and 8 respectively, then the "x := e" spec is fixed as following: + /// x.a := 3 && x.b := 8 + /// + /// List values are handled similarly, e.g.: + /// x := [gensym32] + /// is translated into + /// |x| = 1 && x[0].a = 3 && x[0].b = 8 + // =============================================================================== + let rec __ExamineAndFix x e = + match e with + | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> //TODO: is it really only non-direct children? + let absFlds = __GetAbsFldAssignments id + absFlds |> List.fold (fun acc (var,vval) -> BinaryAnd acc (BinaryEq (Dot(x, GetVarName var)) vval)) TrueLiteral + | SequenceExpr(elist) -> + let rec __fff lst acc cnt = + match lst with + | fsExpr :: rest -> + let acc = BinaryAnd acc (__ExamineAndFix (SelectExpr(x, IntLiteral(cnt))) fsExpr) + __fff rest acc (cnt+1) + | [] -> + let lenExpr = BinaryEq (SeqLength(x)) (IntLiteral(cnt)) + BinaryAnd lenExpr acc + __fff elist TrueLiteral 0 + | _ -> BinaryEq x e + + // ================================================================================ + /// The spec for an object consists of assignments to its abstract fields with one + /// caveat: if some assignments include non-direct children objects of "this", then + /// those objects cannot be used directly in the spec; instead, their properties must + /// be expanded and embeded (that's what the "ExamineAndFix" function does) + // ================================================================================ + let __GetSpecFor objLitName = + let absFieldAssignments = __GetAbsFldAssignments objLitName + let absFldAssgnExpr = absFieldAssignments |> List.fold (fun acc (var,e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(GetVarName var)) e)) TrueLiteral + let retValExpr = hInst.methodRetVals |> Map.fold (fun acc varName varValueExpr -> BinaryAnd acc (BinaryEq (VarLiteral(varName)) varValueExpr)) TrueLiteral + BinaryAnd absFldAssgnExpr retValExpr + + // ================================================================================================ + /// Simply traverses a given expression and returns all arguments of the "meth" method that are used + // ================================================================================================ + let __GetArgsUsed expr = + let args = GetMethodArgs meth + let argSet = DescendExpr2 (fun e acc -> + match e with + | VarLiteral(vname) -> + match args |> List.tryFind (fun var -> GetVarName var = vname) with + | Some(var) -> acc |> Set.add var + | None -> acc + | _ -> acc + ) expr Set.empty + argSet |> Set.toList + + let rec __GetDelegateMethods objs acc = + match objs with + | ObjLiteral(name) as obj :: rest -> + let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name + let pre,_ = GetMethodPrePost meth //TrueLiteral + let post = __GetSpecFor name + let ins = __GetArgsUsed (BinaryAnd pre post) + let sgn = Sig(ins, []) + let m = Method(mName, sgn, pre, post, true) + let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption + let m',unifs = TryFindExisting c m + let args = ApplyMethodUnifs obj (c,m') unifs + __GetDelegateMethods rest (acc |> Map.add obj (c,m',args)) + | _ :: rest -> failwith "internal error: expected to see only ObjLiterals" + | [] -> acc + + // ======================================================================= + /// Tries to make a given solution for a given method into more modular, + /// by delegating some statements (initialization of inner objects) to + /// method calls. + // ======================================================================= + let __GetModularBranch = + let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty + let initChildrenExprList = delegateMethods |> Map.toList + |> List.map (fun (_, (_,_,asgs)) -> asgs) + |> List.concat + let newAssgns = hInst.assignments |> List.filter (function FieldAssignment((obj,_),_) -> obj.name = "this" | _ -> false) + let newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) -> + (c,newMthd) :: acc + ) [] + newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns } + + (* --- function body starts here --- *) + let idt = Indent indent + if Options.CONFIG.genMod then + Logger.InfoLine (idt + " - delegating to method calls ...") + // first try to find a match for the entire method (based on the given solution) + let postSpec = __GetSpecFor "this" + let meth' = match meth with + | Method (mname, msig, mpre, _, isConstr) -> Method(mname, msig, mpre, postSpec, isConstr) + | _ -> failwithf "internal error: expected a Method but got %O" meth + match TryFindExistingAndConvertToSolution indent comp meth' cond callGraph with + | Some(sol) -> sol |> FixSolution comp meth + | None -> + // if not found, try to split into parts + let newMthdLst, newHeapInst = __GetModularBranch + let msol = Utils.MapSingleton (comp,meth) [cond, newHeapInst] + newMthdLst |> List.fold (fun acc (c,m) -> + acc |> MergeSolutions (Utils.MapSingleton (c,m) []) + ) msol + else + Utils.MapSingleton (comp,meth) [cond, hInst] + +//let GetModularSol prog sol = +// let comp = fst (fst sol) +// let meth = snd (fst sol) +// let rec __xxx prog lst = +// match lst with +// | (cond, hInst) :: rest -> +// let newProg, newComp, newMthdLst, newhInst = GetModularBranch prog comp meth hInst +// let newProg, newRest = __xxx newProg rest +// newProg, ((cond, newhInst) :: newRest) +// | [] -> prog, [] +// let newProg, newSolutions = __xxx prog (snd sol) +// let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption +// newProg, ((newComp, meth), newSolutions) +// +//let Modularize prog solutions = +// let rec __Modularize prog sols acc = +// match sols with +// | sol :: rest -> +// let (newProg, newSol) = GetModularSol prog sol +// let newAcc = acc |> Map.add (fst newSol) (snd newSol) +// __Modularize newProg rest newAcc +// | [] -> (prog, acc) +// (* --- function body starts here --- *) +// __Modularize prog (Map.toList solutions) Map.empty diff --git a/Source/Jennisys/Options.fs b/Source/Jennisys/Options.fs new file mode 100644 index 00000000..fe640f48 --- /dev/null +++ b/Source/Jennisys/Options.fs @@ -0,0 +1,162 @@ +// #################################################################### +/// This module is intended to store and handle configuration options +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### + +module Options + +open Utils + +type Config = { + help : bool; + inputFilename : string; + methodToSynth : string; + constructorsOnly : bool; + inferConditionals : bool; + verifyPartialSolutions : bool; + verifySolutions : bool; + checkUnifications : bool; + genRepr : bool; + genMod : bool; + timeout : int; + numLoopUnrolls : int; + recursiveValid : bool; + breakIntoDebugger : bool; + minimizeGuards : bool; +} + +type CfgOption<'a> = { + optionName: string; + optionType: string; + optionSetter: 'a -> Config -> Config; + descr: string; +} + +exception InvalidCmdLineArg of string +exception InvalidCmdLineOption of string + +let CheckNonEmpty value optName = + if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty")) else value + +let CheckInt value optName = + try + System.Int32.Parse value + with + | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean")) + +let CheckBool value optName = + if value = "" then + true + else + try + System.Boolean.Parse value + with + | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer")) + +let cfgOptions = [ + { optionName = "help"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with help = CheckBool v "help"}); descr = "prints out the available switches"; } + { optionName = "method"; optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth = CheckNonEmpty v "method"}); descr = "select methods to synthesize; method names are in the form .; multiple methods can be given as a list of comma separated values"; } + { optionName = "constrOnly"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly = CheckBool v "constrOnly"}); descr = "synthesize constructors only"; } + { optionName = "inferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = CheckBool v "inferConds"}); descr = "try to infer conditions"; } + { optionName = "noInferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = not (CheckBool v "inferConds")}); descr = "don't try to infer conditions"; } + { optionName = "verifyParSol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = CheckBool v "verifyParSol"}); descr = "verify partial solutions"; } + { optionName = "noVerifyParSol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = not (CheckBool v "verifyParSol")}); descr = "don't verify partial solutions"; } + { optionName = "verifySol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions = CheckBool v "verifySol"}); descr = "verify final solution"; } + { optionName = "noVerifySol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions = not (CheckBool v "verifySol")}); descr = "don't verify final solution"; } + { optionName = "checkUnifs"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications = CheckBool v "checkUnifs"}); descr = "verify unifications"; } + { optionName = "noCheckUnifs"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications = not (CheckBool v "noCheckUnifs")}); descr = "don't verify unifications"; } + { optionName = "genRepr"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genRepr = CheckBool v "genRepr"}); descr = "generate Repr field"; } + { optionName = "noGenRepr"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genRepr = not (CheckBool v "noGenRepr")}); descr = "don't generate Repr field"; } + { optionName = "genMod"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genMod = CheckBool v "genMod"}); descr = "generate modular code (delegate to methods)"; } + { optionName = "noGenMod"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genMod = not (CheckBool v "noGenMod")}); descr = "dont generate modular code (delegate to methods)"; } + { optionName = "timeout"; optionType = "int"; optionSetter = (fun v (cfg: Config) -> {cfg with timeout = CheckInt v "timeout"}); descr = "timeout"; } + { optionName = "unrolls"; optionType = "int"; optionSetter = (fun v (cfg: Config) -> {cfg with numLoopUnrolls = CheckInt v "unrolls"}); descr = "number of unrolls of the Valid() function"; } + { optionName = "recValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = CheckBool v "recValid"}); descr = "generate recursive Valid() function"; } + { optionName = "noRecValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = not (CheckBool v "noRecValid")}); descr = "unroll Valid() function"; } + { optionName = "break"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with breakIntoDebugger = CheckBool v "break"}); descr = "launches debugger upon start-up"; } + { optionName = "minGuards"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with minimizeGuards = CheckBool v "minGuards"}); descr = "tries to remove unnecessary clauses from the inferred guards"; } + { optionName = "noMinGuards"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with minimizeGuards = not (CheckBool v "noMinGuards")}); descr = "don't minimize guards"; } +] + +let cfgOptMap = cfgOptions |> List.fold (fun acc o -> acc |> Map.add o.optionName o) Map.empty + +let newline = System.Environment.NewLine + +let PrintHelpMsg = + let maxw = cfgOptions |> List.fold (fun acc o -> if String.length o.optionName > acc then String.length o.optionName else acc) 0 + let maxwStr = sprintf "%d" (maxw + 2) + let strf = new Printf.StringFormat<_>(" %-" + maxwStr + "s: %-6s | %s") + let rec __PrintHelp optLst = + match optLst with + | fs :: [] -> (sprintf strf fs.optionName fs.optionType fs.descr) + | fs :: rest -> (sprintf strf fs.optionName fs.optionType fs.descr) + newline + (__PrintHelp rest) + | [] -> "" + (* --- function body starts here --- *) + newline + + "Jennisys usage: Jennisys [ option ... ] filename" + newline + + " where