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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
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
|