diff options
| -rw-r--r-- | Jennisys/Analyzer.fs | 25 | ||||
| -rw-r--r-- | Jennisys/Ast.fs | 8 | ||||
| -rw-r--r-- | Jennisys/AstUtils.fs | 323 | ||||
| -rw-r--r-- | Jennisys/CodeGen.fs | 3 | ||||
| -rw-r--r-- | Jennisys/DafnyPrinter.fs | 1 | ||||
| -rw-r--r-- | Jennisys/Jennisys.fsproj | 2 | ||||
| -rw-r--r-- | Jennisys/Options.fs | 19 | ||||
| -rw-r--r-- | Jennisys/Printer.fs | 1 | ||||
| -rw-r--r-- | Jennisys/Resolver.fs | 3 |
9 files changed, 258 insertions, 127 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index c02e290e..e14d2d06 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -75,6 +75,7 @@ let rec IsArgsOnly args expr = | IntLiteral(_) -> true
| BoolLiteral(_) -> true
| Star -> true
+ | VarLiteral(id)
| IdLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)
| UnaryExpr(_,e) -> IsArgsOnly args e
| BinaryExpr(_,_,e1,e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
@@ -106,6 +107,7 @@ let GetUnifications expr args (heap,env,ctx) = match expr with
| IntLiteral(_)
| BoolLiteral(_)
+ | VarLiteral(_)
| IdLiteral(_)
| Star -> unifs
| Dot(e, _)
@@ -191,7 +193,7 @@ let GetObjRefExpr o (heap,env,ctx) = // =======================================================
let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
let __CheckUnif o f e idx =
- if not conservative then
+ if not conservative || not Options.CONFIG.checkUnifications then
true
else
let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + (PrintObjRefName o (env,ctx)))
@@ -262,9 +264,26 @@ let VerifySolution prog comp mthd (heap,env,ctx) = let TryInferConditionals prog comp m unifs (heap,env,ctx) =
let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false
// get expressions to evaluate:
- // - go through all objects on the heap and assert its invariant
// - add pre and post conditions
-
+ // - go through all objects on the heap and assert its invariant
+ let pre,post = GetMethodPrePost m
+ let prepostExpr = post |> RewriteMethodArgs (GetMethodArgs m) //TODO: do we need the "pre" here as well?
+ let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty
+ let expr = heapObjs |> Set.fold (fun acc o ->
+ let receiverOpt = GetObjRefExpr o (heap,env,ctx)
+ let receiver = Utils.ExtractOption receiverOpt
+ match Resolve (env,ctx) o with
+ | NewObj(_,tOpt) | ThisConst(_,tOpt) ->
+ let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt
+ let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption
+ let objInvs = GetInvariantsAsList objComp
+ let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)
+ objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc
+ | _ -> failwith "not supposed to happen"
+ ) prepostExpr
+ expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")
+ // now evaluate and see what's left
+ let c = Eval (heap,env,ctx) expr
Some(heap2,env2,ctx2)
// ============================================================================
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 86f6861f..eeb34a8d 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -21,10 +21,15 @@ type Type = type VarDecl =
| Var of string * Type option
+(*
+ 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)
+ *)
type Expr =
| IntLiteral of int
| BoolLiteral of bool
- | IdLiteral of string
+ | VarLiteral of string
+ | IdLiteral of string
| Star
| Dot of Expr * string
| UnaryExpr of string * Expr
@@ -72,5 +77,6 @@ type Const = | NoneConst
| ThisConst of (* loc id *) string * Type option
| NewObj of (* loc id *) string * Type option
+ | VarConst of (* loc id *) string * Type option
| ExprConst of Expr
| Unresolved of (* loc id *) string
\ No newline at end of file diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 4f8b4099..b81fd807 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -15,17 +15,19 @@ let rec VisitExpr visitorFunc expr acc = match expr with
| IntLiteral(_)
| BoolLiteral(_)
- | IdLiteral(_)
+ | VarLiteral(_)
+ | IdLiteral(_)
| Star -> acc |> visitorFunc expr
- | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | SelectExpr(e1, e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
- | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
- | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
+ | Dot(e, _)
+ | ForallExpr(_,e)
+ | UnaryExpr(_,e)
| SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | ForallExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
- | UnaryExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+ | SelectExpr(e1, e2)
| BinaryExpr(_,_,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
- | IteExpr(c,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc c |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+ | IteExpr(e1,e2,e3)
+ | UpdateExpr(e1,e2,e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
+ | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
+
// ------------------------------- End Visitor Stuff -------------------------------------------
@@ -33,110 +35,155 @@ exception EvalFailed let DefaultResolver e = ExprConst(e)
-let rec EvalSym resolverFunc expr =
- match expr with
- | IntLiteral(n) -> IntConst(n)
- | IdLiteral(_) | Dot(_) -> resolverFunc expr
- | SeqLength(e) ->
- match EvalSym resolverFunc e with
- | SeqConst(clist) -> IntConst(List.length clist)
- | _ -> resolverFunc expr
- | SequenceExpr(elist) ->
- let clist = elist |> List.fold (fun acc e -> EvalSym resolverFunc e :: acc) [] |> List.rev
- SeqConst(clist)
- | SelectExpr(lst, idx) ->
- match EvalSym resolverFunc lst, EvalSym resolverFunc idx with
- | SeqConst(clist), IntConst(n) -> clist.[n]
- | _ -> resolverFunc expr
- | UpdateExpr(lst,idx,v) ->
- match EvalSym resolverFunc lst, EvalSym resolverFunc idx, EvalSym resolverFunc v with
- | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)
- | _ -> resolverFunc expr
- | BinaryExpr(_,op,e1,e2) ->
- match op with
- | "=" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2)
- | ExprConst(e1), ExprConst(e2) -> BoolConst(e1 = e2)
- | _ -> resolverFunc expr
- | "!=" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))
- | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2))
- | ExprConst(e1), ExprConst(e2) -> BoolConst(not (e1 = e2))
- | _ -> resolverFunc expr
- | "<" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2))
- | _ -> resolverFunc expr
- | "<=" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2))
- | _ -> resolverFunc expr
- | ">" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2))
- | _ -> resolverFunc expr
- | ">=" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2)
- | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2))
- | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2))
- | _ -> resolverFunc expr
- | "in" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | _ as c, SetConst(s) -> BoolConst(Set.contains c s)
- | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s)
- | _ -> resolverFunc expr
- | "!in" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s))
- | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s))
- | _ -> resolverFunc expr
- | "+" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
- | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
- | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
- | q,w -> resolverFunc expr
- | "-" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
- | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)
- | _ -> resolverFunc expr
- | "*" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)
- | _ -> resolverFunc expr
- | "div" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)
- | _ -> resolverFunc expr
- | "mod" ->
- match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with
- | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)
- | _ -> resolverFunc expr
- | _ -> resolverFunc expr
- | UnaryExpr(op, e) ->
- match op with
- | "!" ->
- match EvalSym resolverFunc e with
- | BoolConst(b) -> BoolConst(not b)
- | _ -> resolverFunc expr
- | "-" ->
- match EvalSym resolverFunc e with
- | IntConst(n) -> IntConst(-n)
- | _ -> resolverFunc expr
- | _ -> resolverFunc expr
- | _ -> resolverFunc expr
-
+let EvalSym resolverFunc expr =
+ let rec __EvalSym ctx expr =
+ match expr with
+ | IntLiteral(n) -> IntConst(n)
+ | IdLiteral(_) | Dot(_) -> resolverFunc expr
+ | SeqLength(e) ->
+ match __EvalSym ctx e with
+ | SeqConst(clist) -> IntConst(List.length clist)
+ | _ -> resolverFunc expr
+ | SequenceExpr(elist) ->
+ let clist = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev
+ SeqConst(clist)
+ | SetExpr(eset) ->
+ let cset = eset |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty
+ SetConst(cset)
+ | SelectExpr(lst, idx) ->
+ match __EvalSym ctx lst, __EvalSym ctx idx with
+ | SeqConst(clist), IntConst(n) -> clist.[n]
+ | _ -> resolverFunc expr
+ | UpdateExpr(lst,idx,v) ->
+ match __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v with
+ | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)
+ | _ -> resolverFunc expr
+ | IteExpr(c, e1, e2) ->
+ match __EvalSym ctx c with
+ | BoolConst(b) -> if b then __EvalSym ctx e1 else __EvalSym ctx e2
+ | _ -> resolverFunc expr
+ | BinaryExpr(_,op,e1,e2) ->
+ match op with
+ | "=" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2)
+ | ExprConst(e1), ExprConst(e2) -> BoolConst(e1 = e2)
+ | _ -> resolverFunc expr
+ | "!=" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))
+ | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2))
+ | ExprConst(e1), ExprConst(e2) -> BoolConst(not (e1 = e2))
+ | _ -> resolverFunc expr
+ | "<" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2))
+ | _ -> resolverFunc expr
+ | "<=" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2))
+ | _ -> resolverFunc expr
+ | ">" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2))
+ | _ -> resolverFunc expr
+ | ">=" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2)
+ | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2))
+ | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2))
+ | _ -> resolverFunc expr
+ | "in" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | _ as c, SetConst(s) -> BoolConst(Set.contains c s)
+ | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s)
+ | _ -> resolverFunc expr
+ | "!in" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s))
+ | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s))
+ | _ -> resolverFunc expr
+ | "+" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+ | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
+ | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
+ | q,w -> resolverFunc expr
+ | "-" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+ | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)
+ | _ -> resolverFunc expr
+ | "*" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)
+ | _ -> resolverFunc expr
+ | "div" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)
+ | _ -> resolverFunc expr
+ | "mod" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)
+ | _ -> resolverFunc expr
+ | "&&" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 && b2)
+ | _ -> resolverFunc expr
+ | "||" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 || b2)
+ | _ -> resolverFunc expr
+ | "==>" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst((not b1) || b2)
+ | _ -> resolverFunc expr
+ | "<==>" ->
+ match __EvalSym ctx e1, __EvalSym ctx e2 with
+ | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
+ | _ -> resolverFunc expr
+ | _ -> resolverFunc expr
+ | UnaryExpr(op, e) ->
+ match op with
+ | "!" ->
+ match __EvalSym ctx e with
+ | BoolConst(b) -> BoolConst(not b)
+ | _ -> resolverFunc expr
+ | "-" ->
+ match __EvalSym ctx e with
+ | IntConst(n) -> IntConst(-n)
+ | _ -> resolverFunc expr
+ | _ -> resolverFunc expr
+ | ForallExpr(vars, e) ->
+ let rec PrintSep sep f list = + match list with + | [] -> "" + | [a] -> f a + | a :: more -> (f a) + sep + (PrintSep sep f more)
+ let rec PrintType ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args) + | SeqType(t) -> sprintf "seq[%s]" (PrintType t) + | SetType(t) -> sprintf "set[%s]" (PrintType t) + | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)
+ let PrintVarDecl vd = + match vd with + | Var(id,None) -> id + | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
+ vars |> List.iter (fun v -> printfn "%s" (PrintVarDecl v))
+ resolverFunc expr
+ | _ -> resolverFunc expr
+ __EvalSym [] expr
+
// =======================================
/// Converts a given constant to expression
// =======================================
@@ -319,8 +366,7 @@ let rec GetTypeShortName ty = | BoolType -> "bool"
| SetType(_) -> "set"
| SeqType(_) -> "seq"
- | NamedType(n,_) -> n
- | InstantiatedType(n,_) -> n
+ | NamedType(n,_) | InstantiatedType(n,_) -> n
// ==============================================================
/// Returns all invariants of a component as a list of expressions
@@ -384,7 +430,8 @@ let rec Desugar expr = match expr with
| IntLiteral(_)
| BoolLiteral(_)
- | IdLiteral(_)
+ | IdLiteral(_)
+ | VarLiteral(_)
| Star
| Dot(_)
| SelectExpr(_)
@@ -425,3 +472,49 @@ let rec DesugarLst exprLst = | expr :: rest -> Desugar expr :: DesugarLst rest
| [] -> []
+let ChangeThisReceiver receiver expr =
+ let rec __ChangeThis locals expr =
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | Star
+ | VarLiteral(_)
+ | IdLiteral("null") -> expr
+ | IdLiteral("this") -> receiver
+ | IdLiteral(id) -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(IdLiteral("this"), id))
+ | Dot(e, id) -> Dot(__ChangeThis locals e, id)
+ | ForallExpr(vars,e) -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals
+ ForallExpr(vars, __ChangeThis newLocals 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))
+ (* function body starts here *)
+ __ChangeThis Set.empty expr
+
+let rec Rewrite rewriterFunc expr =
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | Star
+ | VarLiteral(_)
+ | IdLiteral(_) -> rewriterFunc expr
+ | Dot(e, id) -> Dot(rewriterFunc e, id)
+ | ForallExpr(vars,e) -> ForallExpr(vars, rewriterFunc e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, rewriterFunc e)
+ | SeqLength(e) -> SeqLength(rewriterFunc e)
+ | SelectExpr(e1, e2) -> SelectExpr(rewriterFunc e1, rewriterFunc e2)
+ | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, rewriterFunc e1, rewriterFunc e2)
+ | IteExpr(e1,e2,e3) -> IteExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3)
+ | UpdateExpr(e1,e2,e3) -> UpdateExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3)
+ | SequenceExpr(exs) -> SequenceExpr(exs |> List.map rewriterFunc)
+ | SetExpr(exs) -> SetExpr(exs |> List.map rewriterFunc)
+
+let RewriteMethodArgs args expr =
+ let __IdIsArg id = args |> List.exists (function Var(name,_) -> name = id)
+ Rewrite (function IdLiteral(id) when __IdIsArg id -> VarLiteral(id) | _ as e -> e) expr
+
\ No newline at end of file diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index c13b94d2..f0e59d3b 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -150,5 +150,4 @@ let PrintImplCode prog solutions methodsToPrintFunc = | _ -> " //unable to synthesize" + newline
(GenConstructorCode mthd mthdBody) + newline
else
- ""
- )
\ No newline at end of file + "")
\ No newline at end of file diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index 9ef9e74a..05f333d1 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -16,6 +16,7 @@ let rec PrintExpr ctx expr = match expr with | IntLiteral(n) -> sprintf "%d" n | BoolLiteral(b) -> sprintf "%b" b + | VarLiteral(id) | IdLiteral(id) -> id | Star -> assert false; "" // I hope this won't happen | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 17c74563..832176fd 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ <WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double</StartArguments>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double /noCheckUnifs</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 291bd678..4a1487ce 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -12,14 +12,16 @@ type Config = { inputFilename: string;
methodToSynth: string;
verifySolutions: bool;
+ checkUnifications: bool;
timeout: int;
}
let defaultConfig: Config = {
- inputFilename = "";
- methodToSynth = "*";
- verifySolutions = true;
- timeout = 0;
+ inputFilename = "";
+ methodToSynth = "*";
+ verifySolutions = true;
+ checkUnifications = true;
+ timeout = 0;
}
let mutable CONFIG = defaultConfig
@@ -79,6 +81,15 @@ let ParseCmdLineArgs args = | "verifySol" ->
let b = __CheckBool value opt
__Parse rest { cfg with verifySolutions = b }
+ | "noVerifySol" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with verifySolutions = not b }
+ | "checkUnifs" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with checkUnifications = b }
+ | "noCheckUnifs" ->
+ let b = __CheckBool value opt
+ __Parse rest { cfg with checkUnifications = not b }
| "timeout" ->
let t = __CheckInt value opt
__Parse rest { cfg with timeout = t }
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index 53bf6b6d..54d0dc43 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -36,6 +36,7 @@ let rec PrintExpr ctx expr = match expr with | IntLiteral(n) -> sprintf "%d" n | BoolLiteral(b) -> sprintf "%b" b + | VarLiteral(id) | IdLiteral(id) -> id | Star -> "*" | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs index 59c6904d..fac29fba 100644 --- a/Jennisys/Resolver.fs +++ b/Jennisys/Resolver.fs @@ -70,7 +70,8 @@ let Resolve (env,ctx) cst = let Eval (heap,env,ctx) expr =
let rec __EvalResolver expr =
match expr with
- | IdLiteral(id) when id = "this" -> GetThisLoc env
+ | VarLiteral(id) -> ExprConst(expr)
+ | IdLiteral("this") -> GetThisLoc env
| IdLiteral(id) ->
match TryResolve (env,ctx) (Unresolved(id)) with
| Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id))
|