diff options
Diffstat (limited to 'Source/Forro/Translator.fs')
-rw-r--r-- | Source/Forro/Translator.fs | 434 |
1 files changed, 217 insertions, 217 deletions
diff --git a/Source/Forro/Translator.fs b/Source/Forro/Translator.fs index 4e7be216..db771c96 100644 --- a/Source/Forro/Translator.fs +++ b/Source/Forro/Translator.fs @@ -1,217 +1,217 @@ -module Translator
-
-open Forro
-open BoogieAst
-open Resolver
-open System.Collections.Generic
-
-let rec Append a b =
- match a with
- | [] -> b
- | hd::tl -> hd::(Append tl b)
-
-let rec Flatten a =
- match a with
- | [] -> []
- | list::rest -> Append list (Flatten rest)
-
-// ---------- Prelude ----------
-
-let Prelude =
- @"// Forro
-
-var $head: [int]int; // int -> int
-var $tail: [int]int;
-var $valid: [int]bool; // array int of bool
-
-const null: int;
-
-function GoodState([int]int, [int]int, [int]bool): bool;
-
-axiom (forall hd, tl: [int]int, valid: [int]bool ::
- { GoodState(hd, tl, valid) }
- GoodState(hd, tl, valid) ==> !valid[null]);
-"
-
-// ---------- Translate Expressions ----------
-
-let TrField f =
- match f with
- | Head -> "$head"
- | Tail -> "$tail"
- | Valid -> "$valid"
-
-let AllFields = ["$head" ; "$tail" ; "$valid"]
-
-let MkPred term =
- match term with
- | BToTerm(p) -> p
- | _ -> BToPred(term)
-
-let MkTerm pred =
- match pred with
- | BToPred(e) -> e
- | _ -> BToTerm(pred)
-
-let rec TrExpr expr =
- match expr with
- | Constant(x) -> BConstant x
- | Null -> BNull
- | Identifier(Var(x)) -> BIdentifier(x)
- | Not(e) -> BNot(TrExpr e)
- | Binary(op,a,b) ->
- let a = TrExpr a
- let b = TrExpr b
- match op with
- | Eq -> MkTerm(BBinary(BEq,a,b))
- | Neq -> MkTerm(BBinary(BNeq,a,b))
- | Plus -> BBinary(BPlus,a,b)
- | Minus -> BBinary(BMinus,a,b)
- | Times -> BBinary(BTimes,a,b)
- | Less -> MkTerm(BBinary(BLess,a,b))
- | AtMost -> MkTerm(BBinary(BAtMost,a,b))
- | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b))
- | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b))
- | Select(e,f) ->
- let r = BSelect(TrField f, TrExpr e)
- if f = Field.Valid then MkTerm(r) else r
- | Old(e) -> BOld(TrExpr e)
-
-let rec ListToConjunction list =
- match list with
- | [] -> BTrue
- | [P] -> P
- | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl)
-
-let rec DefL expr =
- match expr with
- | Constant(x) -> []
- | Null -> []
- | Identifier(Var(x)) -> []
- | Not(e) -> DefL e
- | Binary(op,a,b) ->
- match op with
- | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a) // (Def a) && ((TrExpr a) ==> (Def b))
- | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a) // (Def a) && (!(TrExpr a) ==> (Def b))
- | _ -> Append (DefL b) (DefL a)
- | Select(e,f) ->
- let def = DefL e
- if f = Field.Valid then def // it is always okay to ask about .valid
- else BSelect("$valid", TrExpr e) :: def
- | Old(e) -> List.map BOld (DefL e)
-
-and Def expr =
- ListToConjunction (List.rev (DefL expr))
-
-let AssumeGoodState =
- BAssume (BFunc("GoodState", List.map BIdentifier AllFields))
-
-// ---------- Translate Statements ----------
-
-type LocalBookkeeping = LB of int * BVarDecl list
-
-let FreshLocal locals =
- match locals with
- | LB(n, vars) ->
- let name = "nw$" + n.ToString()
- (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars))
-
-let rec TrStmt stmt locals =
- match stmt with
- | Assign(v,e) ->
- let s = [ BAssert (Def e) ;
- BAssign(VarName v, TrExpr e) ]
- (s, locals)
- | Update(obj,f,rhs) ->
- let o = TrExpr obj
- let s = [ BAssert(Def obj) ; BAssert (Def rhs) ;
- BAssert(BSelect("$valid", o)) ;
- BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ;
- AssumeGoodState ]
- (s, locals)
- | Alloc(v,hd,tl) ->
- let nw, name, locals = FreshLocal locals
- let s = [ BAssert (Def hd) ; BAssert (Def tl) ;
- BHavoc [name] ;
- BAssume(BNot(BSelect("$valid", nw))) ;
- BAssume(BBinary(BEq, BSelect("$head", nw), TrExpr hd)) ;
- BAssume(BBinary(BEq, BSelect("$tail", nw), TrExpr tl)) ;
- BUpdate("$valid", nw, BTrue) ;
- AssumeGoodState ;
- BAssign(VarName v, nw) ]
- (s, locals)
- | IfStmt(guard,thn,els) ->
- let check = BAssert(Def guard)
- let thn, locals = TrStmtList thn locals
- let els, locals = TrStmtList els locals
- let s = BIfStmt(MkPred (TrExpr guard), thn, els)
- ([check ; s], locals)
- | WhileStmt(guard,invs,body) ->
- let ii = [Def guard]
- let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs
- let s, locals = TrStmtList body locals
- match s with
- | BBlock(slist) ->
- ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist)) ; AssumeGoodState], locals)
- | CallStmt(outs,id,ins) ->
- let check = List.map (fun e -> BAssert (Def e)) ins
- let ins = List.map (fun e -> TrExpr e) ins
- let outs = List.map (fun p -> VarName p) outs
- let s = BCallStmt(outs, id + "#Proc", ins)
- (Append check [s ; AssumeGoodState ], locals)
- | Assert(e) ->
- ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals)
-
-and TrStmtList slist locals =
- match slist with
- | Block([]) -> (BBlock [], locals)
- | Block(s::rest) ->
- let s,locals = TrStmt s locals
- let rest,locals = TrStmtList (Block rest) locals
- match rest with
- | BBlock(slist) -> (BBlock(Append s slist), locals)
-
-// ---------- Translate Procedure Body ----------
-
-let TrSignature ins outs =
- let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins
- let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs
- (bIns, bOuts)
-
-let LocalDecls (vars: Dictionary<string,VarKind>) =
- Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ]
-
-let TrProc proc vars =
- match proc with
- | Proc(id, ins, outs, req, ens, body) ->
- let bIns, bOuts = TrSignature ins outs
- let pre = MkPred (TrExpr req)
- let post = MkPred (TrExpr ens)
- let locals = LocalDecls vars
- let b, locals = TrStmtList body (LB(0,locals))
- match b, locals with
- | BBlock(slist), LB(n, vars) ->
- BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post,
- List.rev vars, BBlock(AssumeGoodState::slist))
-
-// --------------------
-
-let TrSpec proc vars =
- match proc with
- | Proc(id, ins, outs, req, ens, body) ->
- let bIns, bOuts = TrSignature ins outs
- let b = [ AssumeGoodState ;
- BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ;
- BHavoc AllFields ; AssumeGoodState ;
- BAssert (Def ens) ]
- BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b))
-
-let TrProcedure rproc =
- match rproc with
- | proc, (vars: Dictionary<string,VarKind>) ->
- let name = ProcedureName proc
- (TrSpec proc vars, TrProc proc vars)
-
-let Translate (rprog: (Procedure * Dictionary<string,VarKind>) list) =
- let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog)
- BProg(Prelude, procs)
+module Translator + +open Forro +open BoogieAst +open Resolver +open System.Collections.Generic + +let rec Append a b = + match a with + | [] -> b + | hd::tl -> hd::(Append tl b) + +let rec Flatten a = + match a with + | [] -> [] + | list::rest -> Append list (Flatten rest) + +// ---------- Prelude ---------- + +let Prelude = + @"// Forro + +var $head: [int]int; // int -> int +var $tail: [int]int; +var $valid: [int]bool; // array int of bool + +const null: int; + +function GoodState([int]int, [int]int, [int]bool): bool; + +axiom (forall hd, tl: [int]int, valid: [int]bool :: + { GoodState(hd, tl, valid) } + GoodState(hd, tl, valid) ==> !valid[null]); +" + +// ---------- Translate Expressions ---------- + +let TrField f = + match f with + | Head -> "$head" + | Tail -> "$tail" + | Valid -> "$valid" + +let AllFields = ["$head" ; "$tail" ; "$valid"] + +let MkPred term = + match term with + | BToTerm(p) -> p + | _ -> BToPred(term) + +let MkTerm pred = + match pred with + | BToPred(e) -> e + | _ -> BToTerm(pred) + +let rec TrExpr expr = + match expr with + | Constant(x) -> BConstant x + | Null -> BNull + | Identifier(Var(x)) -> BIdentifier(x) + | Not(e) -> BNot(TrExpr e) + | Binary(op,a,b) -> + let a = TrExpr a + let b = TrExpr b + match op with + | Eq -> MkTerm(BBinary(BEq,a,b)) + | Neq -> MkTerm(BBinary(BNeq,a,b)) + | Plus -> BBinary(BPlus,a,b) + | Minus -> BBinary(BMinus,a,b) + | Times -> BBinary(BTimes,a,b) + | Less -> MkTerm(BBinary(BLess,a,b)) + | AtMost -> MkTerm(BBinary(BAtMost,a,b)) + | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b)) + | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b)) + | Select(e,f) -> + let r = BSelect(TrField f, TrExpr e) + if f = Field.Valid then MkTerm(r) else r + | Old(e) -> BOld(TrExpr e) + +let rec ListToConjunction list = + match list with + | [] -> BTrue + | [P] -> P + | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl) + +let rec DefL expr = + match expr with + | Constant(x) -> [] + | Null -> [] + | Identifier(Var(x)) -> [] + | Not(e) -> DefL e + | Binary(op,a,b) -> + match op with + | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a) // (Def a) && ((TrExpr a) ==> (Def b)) + | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a) // (Def a) && (!(TrExpr a) ==> (Def b)) + | _ -> Append (DefL b) (DefL a) + | Select(e,f) -> + let def = DefL e + if f = Field.Valid then def // it is always okay to ask about .valid + else BSelect("$valid", TrExpr e) :: def + | Old(e) -> List.map BOld (DefL e) + +and Def expr = + ListToConjunction (List.rev (DefL expr)) + +let AssumeGoodState = + BAssume (BFunc("GoodState", List.map BIdentifier AllFields)) + +// ---------- Translate Statements ---------- + +type LocalBookkeeping = LB of int * BVarDecl list + +let FreshLocal locals = + match locals with + | LB(n, vars) -> + let name = "nw$" + n.ToString() + (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars)) + +let rec TrStmt stmt locals = + match stmt with + | Assign(v,e) -> + let s = [ BAssert (Def e) ; + BAssign(VarName v, TrExpr e) ] + (s, locals) + | Update(obj,f,rhs) -> + let o = TrExpr obj + let s = [ BAssert(Def obj) ; BAssert (Def rhs) ; + BAssert(BSelect("$valid", o)) ; + BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ; + AssumeGoodState ] + (s, locals) + | Alloc(v,hd,tl) -> + let nw, name, locals = FreshLocal locals + let s = [ BAssert (Def hd) ; BAssert (Def tl) ; + BHavoc [name] ; + BAssume(BNot(BSelect("$valid", nw))) ; + BAssume(BBinary(BEq, BSelect("$head", nw), TrExpr hd)) ; + BAssume(BBinary(BEq, BSelect("$tail", nw), TrExpr tl)) ; + BUpdate("$valid", nw, BTrue) ; + AssumeGoodState ; + BAssign(VarName v, nw) ] + (s, locals) + | IfStmt(guard,thn,els) -> + let check = BAssert(Def guard) + let thn, locals = TrStmtList thn locals + let els, locals = TrStmtList els locals + let s = BIfStmt(MkPred (TrExpr guard), thn, els) + ([check ; s], locals) + | WhileStmt(guard,invs,body) -> + let ii = [Def guard] + let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs + let s, locals = TrStmtList body locals + match s with + | BBlock(slist) -> + ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist)) ; AssumeGoodState], locals) + | CallStmt(outs,id,ins) -> + let check = List.map (fun e -> BAssert (Def e)) ins + let ins = List.map (fun e -> TrExpr e) ins + let outs = List.map (fun p -> VarName p) outs + let s = BCallStmt(outs, id + "#Proc", ins) + (Append check [s ; AssumeGoodState ], locals) + | Assert(e) -> + ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals) + +and TrStmtList slist locals = + match slist with + | Block([]) -> (BBlock [], locals) + | Block(s::rest) -> + let s,locals = TrStmt s locals + let rest,locals = TrStmtList (Block rest) locals + match rest with + | BBlock(slist) -> (BBlock(Append s slist), locals) + +// ---------- Translate Procedure Body ---------- + +let TrSignature ins outs = + let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins + let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs + (bIns, bOuts) + +let LocalDecls (vars: Dictionary<string,VarKind>) = + Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ] + +let TrProc proc vars = + match proc with + | Proc(id, ins, outs, req, ens, body) -> + let bIns, bOuts = TrSignature ins outs + let pre = MkPred (TrExpr req) + let post = MkPred (TrExpr ens) + let locals = LocalDecls vars + let b, locals = TrStmtList body (LB(0,locals)) + match b, locals with + | BBlock(slist), LB(n, vars) -> + BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post, + List.rev vars, BBlock(AssumeGoodState::slist)) + +// -------------------- + +let TrSpec proc vars = + match proc with + | Proc(id, ins, outs, req, ens, body) -> + let bIns, bOuts = TrSignature ins outs + let b = [ AssumeGoodState ; + BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ; + BHavoc AllFields ; AssumeGoodState ; + BAssert (Def ens) ] + BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b)) + +let TrProcedure rproc = + match rproc with + | proc, (vars: Dictionary<string,VarKind>) -> + let name = ProcedureName proc + (TrSpec proc vars, TrProc proc vars) + +let Translate (rprog: (Procedure * Dictionary<string,VarKind>) list) = + let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog) + BProg(Prelude, procs) |