1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
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
|
