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
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
|
module Analyzer
open Ast
open AstUtils
open CodeGen
open DafnyModelUtils
open PipelineUtils
open Options
open Printer
open Resolver
open DafnyPrinter
open Utils
open Microsoft.Boogie
// =======================================================================
/// Merges two solution maps so that if there are multiple entries for a
/// single (comp,method) pair it concatenates them (corresponds to multiple
/// branches).
// =======================================================================
let MergeSolutions sol1 sol2 =
let rec __Merge sol1map sol2lst res =
match sol2lst with
| ((c2,m2), lst2) :: rest ->
match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> CheckSameMethods (c1,m1) (c2,m2)) with
| Some(c1,m1) ->
let lst1 = sol1map |> Map.find(c1,m1)
let newRes = res |> Map.add (c1,m1) (lst1@lst2)
__Merge sol1map rest newRes
| None ->
let newRes = res |> Map.add (c2,m2) lst2
__Merge sol1map rest newRes
| [] -> res
(* --- function body starts here --- *)
__Merge sol1 (sol2 |> Map.toList) sol1
let Rename suffix vars =
vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
let ReplaceName substMap nm =
match Map.tryFind nm substMap with
| Some(Var(name, tp)) -> name
| None -> nm
let rec Substitute substMap = function
| IdLiteral(s) -> IdLiteral(ReplaceName substMap s)
| Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f)
| UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e)
| BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1)
| SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1)
| UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2)
| SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee)
| SeqLength(e) -> SeqLength(Substitute substMap e)
| ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
| expr -> expr
let GenMethodAnalysisCode comp m assertion =
let methodName = GetMethodName m
let signature = GetMethodSig m
let ppre,ppost = GetMethodPrePost m
let pre = Desugar ppre
let post = Desugar ppost
" method " + methodName + "()" + newline +
" modifies this;" + newline +
" {" + newline +
// print signature as local variables
(match signature with
| Sig(ins,outs) ->
List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") +
" // assume precondition" + newline +
" assume " + (PrintExpr 0 pre) + ";" + newline +
" // assume invariant and postcondition" + newline +
" assume Valid();" + newline +
" assume " + (PrintExpr 0 post) + ";" + newline +
" // assume user defined invariant again because assuming Valid() doesn't always work" + newline +
(GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline +
// if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
" // assert false to search for a model satisfying the assumed constraints" + newline +
" assert " + (PrintExpr 0 assertion) + ";" + newline +
" }" + newline
let rec MethodAnalysisPrinter onlyForThese assertion comp =
let cname = GetComponentName comp
match onlyForThese with
| (c,m) :: rest when GetComponentName c = cname ->
match m with
| Method(methodName, sign, pre, post, true) ->
(GenMethodAnalysisCode c m assertion) + newline +
(MethodAnalysisPrinter rest assertion comp)
| _ -> ""
| _ :: rest -> MethodAnalysisPrinter rest assertion comp
| [] -> ""
let rec IsArgsOnly args expr =
match expr with
| IntLiteral(_) -> true
| BoolLiteral(_) -> true
| Star -> true
| ObjLiteral(id) -> 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)
| IteExpr(c,e1,e2) -> (IsArgsOnly args c) && (IsArgsOnly args e1) && (IsArgsOnly args e2)
| Dot(e,_) -> IsArgsOnly args e
| SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
| UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)
| SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
| SeqLength(e) -> IsArgsOnly args e
| ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e
| MethodCall(rcv,_,aparams) -> rcv :: aparams |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
let AddUnif indent e v unifMap =
let idt = Indent indent
let builder = new CascadingBuilder<_>(unifMap)
builder {
let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption
Logger.DebugLine (idt + " - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v))
return Map.add e v unifMap
}
//TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"
let rec GetUnifications indent args heapInst unifs expr =
let idt = Indent indent
// - first looks if the give expression talks only about method arguments (args)
// - then checks if it doesn't already exist in the unification map
// - then it tries to evaluate it to a constant
// - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map
let __AddUnif e unifsAcc =
let builder = new CascadingBuilder<_>(unifsAcc)
builder {
let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption
let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None
return AddUnif indent e v unifsAcc
}
(* --- function body starts here --- *)
AstUtils.DescendExpr2 __AddUnif expr unifs
// =======================================================
/// Returns a map (Expr |--> Const) containing unifications
/// found for the given method and heap/env/ctx
// =======================================================
let GetUnificationsForMethod indent comp m heapInst =
let idt = Indent indent
let rec GetArgValueUnifications args =
match args with
| Var(name,_) :: rest ->
match Map.tryFind name heapInst.methodArgs with
| Some(c) ->
GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c
| None -> failwith ("couldn't find value for argument " + name)
| [] -> Map.empty
(* --- function body starts here --- *)
match m with
| Method(mName,Sig(ins, outs),pre,post,_) ->
let args = List.concat [ins; outs]
match args with
| [] -> Map.empty
| _ -> let unifs = GetArgValueUnifications args
GetUnifications indent args heapInst unifs (BinaryAnd pre post)
| _ -> failwith ("not a method: " + m.ToString())
// =========================================================================
/// For a given constant "o" (which is an object, something like "gensym32"),
/// finds a path of field references from "this".
///
/// Implements a backtracking search over the heap entries to find that
/// path. It starts from the given object, and follows the backpointers
/// until it reaches the root ("this")
// =========================================================================
let objRef2ExprCache = new System.Collections.Generic.Dictionary<string, Expr>()
let GetObjRefExpr objRefName (heapInst: HeapInstance) =
let rec __GetObjRefExpr objRefName visited =
if Set.contains objRefName visited then
None
else
let newVisited = Set.add objRefName visited
match objRefName with
| "this" -> Some(ObjLiteral("this"))
| _ ->
let rec __fff lst =
match lst with
| ((o,Var(fldName,_)),_) :: rest ->
match __GetObjRefExpr o.name newVisited with
| Some(expr) -> Some(Dot(expr, fldName))
| None -> __fff rest
| [] -> None
let backPointers = heapInst.assignments |> List.filter (fun ((_,_),l) -> l = ObjLiteral(objRefName))
__fff backPointers
(* --- function body starts here --- *)
if objRef2ExprCache.ContainsKey(objRefName) then
Some(objRef2ExprCache.[objRefName])
else
let res = __GetObjRefExpr objRefName (Set.empty)
match res with
| Some(e) -> objRef2ExprCache.Add(objRefName, e)
| None -> ()
res
// =======================================================
/// Applies given unifications onto the given heap/env/ctx
///
/// If "conservative" is true, applies only those that
/// can be verified to hold, otherwise applies all of them
// =======================================================
let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
let idt = Indent indent
let __CheckUnif o f e idx =
if not conservative || not Options.CONFIG.checkUnifications then
true
else
let objRefExpr = GetObjRefExpr o heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o)
let fldName = PrintVarName f
let lhs = Dot(objRefExpr, fldName)
let assertionExpr = match f with
| Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e
| Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs
| _ -> BinaryEq lhs e
// check if the assertion follows and if so update the env
let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,mthd] assertionExpr) false
Logger.Debug (idt + " - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))
if ok then
Logger.DebugLine " HOLDS"
else
Logger.DebugLine " DOESN'T HOLD"
ok
(* --- function body starts here --- *)
match unifs with
| (e,c) :: rest ->
let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative
let newHeap = heapInst.assignments|> List.fold (fun acc ((o,f),value) ->
if value = Const2Expr c then
if __CheckUnif o.name f e -1 then
// change the value to expression
//Logger.TraceLine (sprintf "%s - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )
Utils.ListMapAdd (o,f) e acc
else
// don't change the value unless "conservative = false"
Utils.ListMapAdd (o,f) value acc
else
let rec __UnifyOverLst lst cnt =
match lst with
| lstElem :: rest when lstElem = Const2Expr c ->
if __CheckUnif o.name f e cnt then
//Logger.TraceLine (sprintf "%s - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )
e :: __UnifyOverLst rest (cnt+1)
else
lstElem :: __UnifyOverLst rest (cnt+1)
| lstElem :: rest ->
lstElem :: __UnifyOverLst rest (cnt+1)
| [] -> []
// see if it's a list, then try to match its elements, otherwise leave it as is
match value with
| SequenceExpr(elist) ->
let newExprList = __UnifyOverLst elist 0
Utils.ListMapAdd (o,f) (SequenceExpr(newExprList)) acc
| SetExpr(elist) ->
let newExprList = __UnifyOverLst elist 0
Utils.ListMapAdd (o,f) (SetExpr(newExprList)) acc
| _ ->
Utils.ListMapAdd (o,f) value acc
) heapInst.assignments
{heapInst with assignments = newHeap }
| [] -> heapInst
// ====================================================================================
/// Returns whether the code synthesized for the given method can be verified with Dafny
// ====================================================================================
let VerifySolution prog solutions genRepr =
// print the solution to file and try to verify it with Dafny
//let prog = Program(solutions |> Utils.MapKeys |> Map.ofList |> Utils.MapKeys)
let code = PrintImplCode prog solutions genRepr
CheckDafnyProgram code dafnyVerifySuffix
let rec DiscoverAliasing exprList heapInst =
match exprList with
| e1 :: rest ->
let eqExpr = rest |> List.fold (fun acc e ->
if Eval heapInst (fun _ -> true) (BinaryEq e1 e) = TrueLiteral then
BinaryAnd acc (BinaryEq e1 e)
else
acc
) TrueLiteral
BinaryAnd eqExpr (DiscoverAliasing rest heapInst)
| [] -> TrueLiteral
// =============================================================================
/// Returns an expression that combines the post-condition of a given method with
/// invariants for all objects present on the heap
// =============================================================================
let GetHeapExpr prog mthd heapInst =
// get expressions to evaluate:
// - add post (and pre?) conditions
// - go through all objects on the heap and assert their invariants
let pre,post = GetMethodPrePost mthd
let prepostExpr = post //TODO: do we need the "pre" here as well?
let heapObjs = heapInst.assignments |> List.fold (fun acc ((o,_),_) -> acc |> Set.add o) Set.empty
heapObjs |> Set.fold (fun acc o ->
let receiverOpt = GetObjRefExpr o.name heapInst
let receiver = Utils.ExtractOption receiverOpt
let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption
let objInvs = GetInvariantsAsList objComp
let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)
objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc
) prepostExpr
// ------------------------------- Modularization stuff ---------------------------------
exception CannotUnify
let GetModularBranch prog comp meth hInst =
let rec __AddDirectChildren e acc =
match e with
| ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e
| SequenceExpr(elist)
| SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc
| _ -> acc
let __GetDirectChildren =
let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)
thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty
|> Set.toList
let directChildren = lazy (__GetDirectChildren)
let __IsAbstractField ty var =
let builder = CascadingBuilder<_>(false)
let varName = GetVarName var
builder {
let! comp = FindComponent prog (GetTypeShortName ty)
let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None
return true
}
let __FindObj objName =
try
hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst
with
| ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)
let __GetObjLitType objLitName =
(__FindObj objLitName).objType
let __GetAbsFldAssignments objLitName =
hInst.assignments |> List.choose (fun ((obj,var),e) ->
if obj.name = objLitName && __IsAbstractField obj.objType var then
Some(var,e)
else
None)
let rec __ExamineAndFix x e =
match e with
| ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) ->
let absFlds = __GetAbsFldAssignments id
absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral
| SequenceExpr(elist) ->
let rec __fff lst acc cnt =
match lst with
| fsExpr :: rest ->
let acc = BinaryAnd acc (__ExamineAndFix (SelectExpr(x, IntLiteral(cnt))) fsExpr)
__fff rest acc (cnt+1)
| [] ->
let lenExpr = BinaryEq (SeqLength(x)) (IntLiteral(cnt))
BinaryAnd lenExpr acc
__fff elist TrueLiteral 0
| _ -> BinaryEq x e
let __GetSpecFor objLitName =
let absFieldAssignments = __GetAbsFldAssignments objLitName
absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral
let __GetArgsUsed expr =
let args = GetMethodArgs meth
let argSet = DescendExpr2 (fun e acc ->
match e with
| VarLiteral(vname) ->
match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with
| Some(var) -> acc |> Set.add var
| None -> acc
| _ -> acc
) expr Set.empty
argSet |> Set.toList
let rec __UnifyImplies lhs rhs unifs =
let ___AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)
if lhs = FalseLiteral || rhs = TrueLiteral then
Some(unifs)
else
try
match lhs, rhs with
| VarLiteral(vname), rhs -> ___AddOrNone unifs vname rhs
| IntLiteral(nL), IntLiteral(nR) when nL = nR ->
Some(unifs)
| BoolLiteral(bL), BoolLiteral(bR) when bL = bR ->
Some(unifs)
| SetExpr(elistL), SetExpr(elistR)
| SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->
let unifs2 = List.fold2 (fun acc elL elR -> match __UnifyImplies elL elR acc with
| Some(u) -> u
| None -> raise CannotUnify) unifs elistL elistR
Some(unifs2)
| _ when lhs = rhs ->
Some(unifs)
| _ ->
let rec ___f2 target candidate unifs =
match target, candidate with
| BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC ->
let builder = new CascadingBuilder<_>(None)
builder {
let! unifsLhs = __UnifyImplies lhsC lhsT unifs
let! unifsRhs = __UnifyImplies rhsC rhsT unifsLhs
return Some(unifsRhs)
}
| _ -> None
let rec ___f1 rhsLst lhsLst unifs =
match rhsLst, lhsLst with
| targetExpr :: rhsRest, candExpr :: lhsRest ->
// trying to find a unification for "targetExpr"
let uOpt = match ___f2 targetExpr candExpr unifs with
// found -> just return
| Some(unifs2) -> Some(unifs2)
// not found -> keep looking in the rest of the candidate expressions
| None -> ___f1 [targetExpr] lhsRest unifs
match uOpt with
// found -> try find for the rest of the target expressions
| Some(unifs2) -> ___f1 rhsRest lhsLst unifs2
// not found -> fail
| None -> None
| targetExpr :: _, [] ->
// no more candidates for unification for this targetExpr -> fail
None
| [], _ ->
// we've found unifications for all target expressions -> return the current unifications map
Some(unifs)
// let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) as e when cop = top -> Some(e) | _ -> None)
// candExprs |> List.fold (fun acc candExpr ->
// match candExpr with
// | BinaryExpr(_,_,cl,cr) ->
// let rec ___f1 lhsLst rhsLst unifs =
// match rhsLst with
// | targetExpr :: rhsRest ->
// match targetExpr with
// | BinaryExpr(_,"=",l,SequenceExpr(_)) ->
// // this one has already been desugared so it's ok to skip it
// ___f1 lhsLst rhsRest unifs
// | BinaryExpr(_,top,tl,tr) ->
// let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) when cop = top -> Some(cr) | _ -> None)
// match candExprs with
// | [] -> None
// | cand :: _ ->
// let unifs2Opt = __UnifyImplies cand tr unifs
// match unifs2Opt with
// | Some(unifs2) -> ___f1 lhsLst rhsRest unifs2
// | None -> None
// | _ -> None
// | [] -> Some(unifs)
//-----------
let lhsConjs = lhs |> DesugarRemove |> SplitIntoConjunts
let rhsConjs = rhs |> DesugarRemove |> SplitIntoConjunts
___f1 rhsConjs lhsConjs unifs
with
| KeyAlreadyExists
| CannotUnify -> None
let __TryUnify targetMthd candMethod =
let targetPre,targetPost = GetMethodPrePost targetMthd
let candPre,candPost = GetMethodPrePost candMethod
let builder = new CascadingBuilder<_>(None)
builder {
let! unifs1 = __UnifyImplies targetPre candPre Map.empty
let! unifs2 = __UnifyImplies candPost targetPost unifs1
return Some(unifs2)
}
let rec __TryFindAMatch targetMthd candidateMethods =
match candidateMethods with
| candMthd :: rest ->
match __TryUnify targetMthd candMthd with
| Some(unifs) -> Some(candMthd,unifs)
| None -> __TryFindAMatch targetMthd rest
| [] -> None
let __TryFindExisting comp targetMthd =
Logger.TraceLine "Trying"
match __TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with
| Some(m,unifs) -> m,unifs
| None ->
let argsExprs = GetMethodArgs targetMthd |> List.fold (fun acc (Var(name,_)) -> acc |> Map.add name (VarLiteral(name))) Map.empty
targetMthd,argsExprs
let rec __GetDelegateMethods objs acc =
match objs with
| ObjLiteral(name) as obj :: rest ->
let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name
let pre,_ = GetMethodPrePost meth //TrueLiteral
let post = __GetSpecFor name
let ins = __GetArgsUsed (BinaryAnd pre post)
let sgn = Sig(ins, [])
let m = Method(mName, sgn, pre, post, true)
let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption
let m',unifs = __TryFindExisting c m
let args = GetMethodArgs m' |> List.map (fun (Var(name,_)) -> Map.find name unifs)
__GetDelegateMethods rest (acc |> Map.add obj (c,m',args))
| _ :: rest -> failwith "internal error: expected to see only ObjLiterals"
| [] -> acc
(* --- function body starts here --- *)
let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty
let initChildrenExprList = delegateMethods |> Map.toList
|> List.map (fun (receiver, (cmp,mthd,args)) ->
let key = __FindObj (PrintExpr 0 receiver), Var("", None)
let e = MethodCall(receiver, GetMethodName mthd, args)
(key, e)
)
let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)
let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->
let obj = __FindObj (PrintExpr 0 receiver)
match acc with
| accProg, accComp, accmList ->
let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption
let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None
let mList' = (mcomp', newMthd) :: accmList
let comp' = if accComp = oldComp then mcomp' else accComp
prog', comp', mList'
) (prog, comp, [])
newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }
let rec MakeModular indent prog comp m cond heapInst =
let idt = Indent indent
if Options.CONFIG.genMod then
Logger.InfoLine (idt + " - delegating to method calls ...")
let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst
let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]
newMthdLst |> List.fold (fun acc (c,m) ->
acc |> MergeSolutions (Utils.MapSingleton (c,m) [])
) msol
else
Utils.MapSingleton (comp,m) [cond, heapInst]
//let GetModularSol prog sol =
// let comp = fst (fst sol)
// let meth = snd (fst sol)
// let rec __xxx prog lst =
// match lst with
// | (cond, hInst) :: rest ->
// let newProg, newComp, newMthdLst, newhInst = GetModularBranch prog comp meth hInst
// let newProg, newRest = __xxx newProg rest
// newProg, ((cond, newhInst) :: newRest)
// | [] -> prog, []
// let newProg, newSolutions = __xxx prog (snd sol)
// let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption
// newProg, ((newComp, meth), newSolutions)
//
//let Modularize prog solutions =
// let rec __Modularize prog sols acc =
// match sols with
// | sol :: rest ->
// let (newProg, newSol) = GetModularSol prog sol
// let newAcc = acc |> Map.add (fst newSol) (snd newSol)
// __Modularize newProg rest newAcc
// | [] -> (prog, acc)
// (* --- function body starts here --- *)
// __Modularize prog (Map.toList solutions) Map.empty
// --------------------------------------------------------------------------------------
// ============================================================================
/// Attempts to synthesize the initialization code for the given constructor "m"
///
/// Returns a (heap,env,ctx) tuple
// ============================================================================
let rec AnalyzeConstructor indent prog comp m =
// TODO: first check maybe there's already a method with this spec
let idt = Indent indent
let methodName = GetMethodName m
let pre,post = GetMethodPrePost m
// generate Dafny code for analysis first
let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false
Logger.InfoLine (idt + "[*] Analyzing constructor")
Logger.InfoLine (idt + "------------------------------------------")
Logger.InfoLine (PrintMethodSignFull (indent + 4) comp m)
Logger.InfoLine (idt + "------------------------------------------")
Logger.Info (idt + " - searching for an instance ...")
let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))
if models.Count = 0 then
// no models means that the "assert false" was verified, which means that the spec is inconsistent
Logger.WarnLine (idt + " !!! SPEC IS INCONSISTENT !!!")
Map.empty
else
if models.Count > 1 then
Logger.WarnLine " FAILED "
failwith "internal error (more than one model for a single constructor analysis)"
Logger.InfoLine " OK "
let model = models.[0]
let hModel = ReadFieldValuesFromModel model prog comp m
let heapInst = ResolveModel hModel
let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList
let heapInst = ApplyUnifications indent prog comp m unifs heapInst true
// split into method calls
let sol = MakeModular indent prog comp m TrueLiteral heapInst
if Options.CONFIG.verifySolutions then
Logger.InfoLine (idt + " - verifying synthesized solution ... ")
let verified = VerifySolution prog sol Options.CONFIG.genRepr
Logger.Info (idt + " ")
if verified then
Logger.InfoLine "~~~ VERIFIED ~~~"
sol
else
Logger.InfoLine "!!! NOT VERIFIED !!!"
if Options.CONFIG.inferConditionals then
Logger.InfoLine (idt + " Strengthening the pre-condition")
TryInferConditionals (indent + 4) prog comp m unifs heapInst
else
sol
else
sol
and TryInferConditionals indent prog comp m unifs heapInst =
let idt = Indent indent
let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]
let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false
let expr = GetHeapExpr prog m heapInst2
// now evaluate and see what's left
let newCond = Eval heapInst2 (function VarLiteral(_) -> false | _ -> true) expr
try
if newCond = TrueLiteral then
Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt)
wrongSol
else
let candCond =
if newCond = FalseLiteral then
// it must be because there is some aliasing going on between method arguments,
// so we should try that as a candidate pre-condition
let tmp = DiscoverAliasing (GetMethodArgs m |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2
if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered")
tmp
else
newCond
Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 candCond))
let p2,c2,m2 = AddPrecondition prog comp m candCond
let sol = MakeModular indent p2 c2 m2 candCond heapInst2
Logger.Info (idt + " - verifying partial solution ... ")
let verified =
if Options.CONFIG.verifyPartialSolutions then
VerifySolution p2 sol Options.CONFIG.genRepr
else
true
if verified then
if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"
let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(candCond))
let fixedSol = sol |> Map.fold (fun acc (cc,mm) v ->
if GetMethodName mm = GetMethodName m then
acc |> Map.add (cc,m) v
else
acc |> Map.add (cc,mm) v) Map.empty
MergeSolutions fixedSol (AnalyzeConstructor (indent + 2) p3 c3 m3)
else
Logger.InfoLine "NOT VERIFIED"
wrongSol
with
ex -> raise ex
let GetMethodsToAnalyze prog =
let mOpt = Options.CONFIG.methodToSynth;
if mOpt = "*" then
(* all *)
FilterMembers prog FilterConstructorMembers
elif mOpt = "paramsOnly" then
(* only with parameters *)
FilterMembers prog FilterConstructorMembersWithParams
else
let allMethods,neg =
if mOpt.StartsWith("~") then
mOpt.Substring(1), true
else
mOpt, false
(* exactly one *)
let methods = allMethods.Split([|','|])
let lst = methods |> Array.fold (fun acc m ->
let idx = m.LastIndexOf(".")
if idx = -1 || idx = m.Length - 1 then
raise (InvalidCmdLineArg("Invalid method full name: " + m))
let compName = m.Substring(0, idx)
let methName = m.Substring(idx + 1)
let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)
let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)
(c,mthd) :: acc
) []
if neg then
FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst))
else
lst
// ============================================================================
/// Goes through a given list of methods of the given program and attempts to
/// synthesize code for each one of them.
///
/// Returns a map from (component * method) |--> Expr * HeapInstance
// ============================================================================
let rec AnalyzeMethods prog members solutionsSoFar =
let __IsAlreadySolved c m solutionMap =
let existingKey = solutionMap |> Map.tryFindKey (fun (cc,mm) v -> CheckSameMethods (c,m) (cc,mm) && not (v = []))
match existingKey with
| Some(_) -> true
| None -> false
let rec __AnalyzeConstructorDeep prog mList solutionsSoFar =
match mList with
| (comp,mthd) :: rest ->
if not (__IsAlreadySolved comp mthd solutionsSoFar) then
let sol = AnalyzeConstructor 2 prog comp mthd
let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = [] && not(__IsAlreadySolved c m solutionsSoFar)) |> Utils.MapKeys
let newSols = solutionsSoFar |> MergeSolutions sol
__AnalyzeConstructorDeep prog (rest@unsolved) newSols
else
__AnalyzeConstructorDeep prog rest solutionsSoFar
| [] -> solutionsSoFar
(* --- function body starts here --- *)
match members with
| (comp,m) :: rest ->
match m with
| Method(_,_,_,_,true) ->
let sol = __AnalyzeConstructorDeep prog [comp,m] solutionsSoFar
Logger.InfoLine ""
AnalyzeMethods prog rest sol
| _ -> AnalyzeMethods prog rest solutionsSoFar
| [] -> solutionsSoFar
let Analyze prog filename =
let rec __AddMethodsFromProg methods solutions =
match methods with
| (c,m) :: rest ->
let exists = solutions |> Map.tryFindKey (fun (c1,m1) _ -> CheckSameMethods (c,m) (c1,m1))
match exists with
| Some(_) -> __AddMethodsFromProg rest solutions
| None -> __AddMethodsFromProg rest (solutions |> Map.add (c,m) [])
| [] -> solutions
/// Prints given solutions to a file
let __PrintSolution prog outFileName solutions =
use file = System.IO.File.CreateText(outFileName)
file.AutoFlush <- true
//let prog = Program(solutions |> Utils.MapKeys |> Map.ofList |> Utils.MapKeys)
// add all other methods (those for which we don't have synthesized solution) as well
let allMethods = FilterMembers prog FilterConstructorMembers
let extSolutions = solutions //__AddMethodsFromProg allMethods solutions
let synthCode = PrintImplCode prog extSolutions Options.CONFIG.genRepr
fprintfn file "%s" synthCode
(* --- function body starts here --- *)
let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) Map.empty
let progName = System.IO.Path.GetFileNameWithoutExtension(filename)
let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName)
Logger.InfoLine "Printing synthesized code"
__PrintSolution prog outFlatSolFileName solutions
()
//let AnalyzeComponent_rustan c =
// match c with
// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
// let aVars = Fields members
// let aVars0 = Rename "0" aVars
// let aVars1 = Rename "1" aVars
// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars]
// let inv0 = Substitute (Map.ofList aVars0) inv
// let inv1 = Substitute (Map.ofList aVars1) inv
// // Now print it as a Dafny program
// printf "class %s" name
// match typeParams with
// | [] -> ()
// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
// printfn " {"
// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields
// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp))
// // the method
// printfn " method %s_checkInjective() {" name
// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";"
// printfn " assume %s;" (PrintExpr 0 inv0)
// printfn " assume %s;" (PrintExpr 0 inv1)
// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"}
// printfn " }"
// // generate code
// members |> List.iter (function
// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false)
// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true)
// | _ -> ())
// // the end of the class
// printfn "}"
// | _ -> assert false // unexpected case
|