diff options
| author |  rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
| commit | ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 (patch) | |
| tree | 82944147dd136bf68b4cb2f8e40d440c6705d42e /Source/Forro/BoogiePrinter.fs | |
| parent | 8d1dd0f01a78bf29aa98832317d8fc951ed15075 (diff) | |
Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.
Diffstat (limited to 'Source/Forro/BoogiePrinter.fs')
| -rw-r--r-- | Source/Forro/BoogiePrinter.fs | 112 |
1 files changed, 112 insertions, 0 deletions
diff --git a/Source/Forro/BoogiePrinter.fs b/Source/Forro/BoogiePrinter.fs new file mode 100644 index 00000000..8f2b37ee --- /dev/null +++ b/Source/Forro/BoogiePrinter.fs @@ -0,0 +1,112 @@ +module BoogiePrinter
+
+open ForroPrinter // to get Indent
+open BoogieAst
+
+let PrintWithSep Pr sep list =
+ ignore (List.fold (fun sp e -> printf "%s" sp ; Pr e ; sep) "" list)
+
+let TypeName t =
+ match t with
+ | BInt -> "int"
+ | BBool -> "bool"
+
+let PrVarType v =
+ match v with
+ | BVar(name,t) ->
+ printf "%s: %s" name (TypeName t)
+
+let PrintOp op =
+ printf " "
+ match op with
+ | BEq -> printf "=="
+ | BNeq -> printf "!="
+ | BPlus -> printf "+"
+ | BMinus -> printf "-"
+ | BTimes -> printf "*"
+ | BLess -> printf "<"
+ | BAtMost -> printf "<="
+ | BAnd -> printf "&&"
+ | BOr -> printf "||"
+ printf " "
+
+let rec PrintExpr e =
+ match e with
+ | BConstant(x) -> printf "%d" x
+ | BFalse -> printf "false"
+ | BTrue -> printf "true"
+ | BNull -> printf "null"
+ | BIdentifier(id) -> printf "%s" id
+ | BNot(e) -> printf "!(" ; PrintExpr e ; printf ")"
+ | BBinary(op,e0,e1) -> printf "(" ; PrintExpr e0 ; PrintOp op ; PrintExpr e1 ; printf ")"
+ | BSelect(var,e) -> printf "%s[" var ; PrintExpr e ; printf "]"
+ | BToPred(e) -> printf "(" ; PrintExpr e ; printf " != 0)"
+ | BToTerm(e) -> printf "(if " ; PrintExpr e ; printf " then 1 else 0)"
+ | BOld(e) -> printf "old(" ; PrintExpr e ; printf ")"
+ | BFunc(id,args) -> printf "%s(" id ; PrintWithSep PrintExpr ", " args ; printf ")"
+
+let rec PrintStmt indent stmt =
+ Indent indent
+ let ind = indent + 2
+ match stmt with
+ | BAssign(id,e) -> printf "%s := " id ; PrintExpr e ; printfn ";"
+ | BUpdate(id,obj,rhs) -> printf "%s[" id ; PrintExpr obj ; printf "] := " ; PrintExpr rhs ; printfn ";"
+ | BHavoc(ids) -> printf "havoc " ; PrintWithSep (printf "%s") ", " ids ; printfn ";"
+ | BAssert(e) -> printf "assert " ; PrintExpr e ; printfn ";"
+ | BAssume(e) -> printf "assume " ; PrintExpr e ; printfn ";"
+ | BIfStmt(e,thn,els) ->
+ printf "if (" ; PrintExpr e ; printfn ") {"
+ PrintStmtList ind thn
+ Indent indent
+ printfn "} else {"
+ PrintStmtList ind els
+ Indent indent
+ printfn "}"
+ | BWhileStmt(e, invs, body) ->
+ printf "while (" ; PrintExpr e ; printfn ")"
+ List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv ; printfn ";") invs
+ Indent indent
+ printfn "{"
+ PrintStmtList ind body
+ Indent indent
+ printfn "}"
+ | BCallStmt(outs, id, ins) ->
+ printf "call "
+ if outs.IsEmpty then () else PrintWithSep (fun p -> printf "%s" p) ", " outs ; printf " := "
+ printf "%s(" id
+ PrintWithSep PrintExpr ", " ins
+ printfn ");"
+
+and PrintStmtList indent stmts =
+ match stmts with
+ | BBlock(slist) -> List.iter (fun s -> PrintStmt indent s) slist
+
+let BPrintProc proc =
+ match proc with
+ | BProc(name, ins, outs, req, frame, ens, locals, body) ->
+ printfn ""
+ printf "procedure %s(" name
+ PrintWithSep PrVarType ", " ins
+ printf ") returns ("
+ PrintWithSep PrVarType ", " outs
+ printfn ")"
+ printf " requires "
+ PrintExpr req
+ printfn ";"
+ printf " modifies "
+ PrintWithSep (printf "%s") ", " frame
+ printfn ";"
+ printf " ensures "
+ PrintExpr ens
+ printfn ";"
+ printfn "{"
+ List.iter (fun local -> printf " var " ; PrVarType local ; printfn ";") locals
+ if locals.IsEmpty then () else printfn ""
+ PrintStmtList 2 body
+ printfn "}"
+
+let BPrint (prog: BProgram) =
+ match prog with
+ | BProg(prelude, procs) ->
+ printfn "%s" prelude
+ List.iter BPrintProc procs
|