summaryrefslogtreecommitdiff
path: root/Jennisys/Resolver.fs
blob: bc3305203adc87d974c457be03d1b971864786e9 (plain)
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
//  ####################################################################
///   Utilities for resolving the "Unresolved" constants with respect to 
///   a given context (heap/env/ctx)
///
///   author: Aleksandar Milicevic (t-alekm@microsoft.com)
//  ####################################################################

module Resolver

open Ast
open Getters
open AstUtils 
open Printer
open EnvUtils
open DafnyModelUtils

type Obj = { name: string; objType: Type }

type AssignmentType = 
  | FieldAssignment of (Obj * VarDecl) * Expr // the first string is the symbolic name of an object literal
  | ArbitraryStatement of Stmt

type HeapInstance = {
   objs                       : Map<string, Obj>;
   modifiableObjs             : Set<Obj>;
   assignments                : AssignmentType list;
   concreteValues             : AssignmentType list;
   methodArgs                 : Map<string, Const>;
   methodRetVals              : Map<string, Expr>;
   concreteMethodRetVals      : Map<string, Expr>;
   globals                    : Map<string, Expr>;
}

let NoObj = { name = ""; objType = NamedType("", []) }
let ThisObj comp = {name = "this"; objType = GetComponentType comp}

let ExtractAllExpressions asg = 
  match asg with
  | FieldAssignment(_,e) -> [e]
  | ArbitraryStatement(s) -> ExtractTopLevelExpressions s

// use the orginal method, not the one with an extra precondition
let FixSolution origComp origMeth sol =
  sol |> Map.fold (fun acc (cc,mm) v -> 
                      if CheckSameMethods (cc,mm) (origComp,origMeth) then
                        acc |> Map.add (origComp,origMeth) v
                      else 
                        acc |> Map.add (cc,mm) v) Map.empty

let ConvertToStatements heapInst onModifiableObjsOnly = 
  let stmtLst1 = heapInst.assignments |> List.choose (fun asgn ->                                                        
                                                        match asgn with
                                                        | FieldAssignment((o,f),e) when (not onModifiableObjsOnly || Set.contains o heapInst.modifiableObjs) ->
                                                            if IsOldVar f then
                                                              None
                                                            else
                                                              let fldName = GetVarName f
                                                              if fldName = "" then
                                                                Some(ExprStmt(e))
                                                              else
                                                              Some(Assign(Dot(ObjLiteral(o.name), fldName), e))
                                                        | ArbitraryStatement(stmt) -> Some(stmt)
                                                        | _ -> None)
  let stmtLst2 = heapInst.methodRetVals |> Map.toList
                                        |> List.map (fun (retVarName, retVarVal) -> Assign(VarLiteral(retVarName), retVarVal))
  stmtLst1 @ stmtLst2
                            
// resolving values
exception ConstResolveFailed of string
 
//  ================================================================
/// Resolves a given Const (cst) with respect to a given env/ctx. 
///
/// If unable to resolve, it just delegates the task to the
/// failResolver function
//  ================================================================
let rec ResolveCont hModel failResolver cst =
  match cst with
  | Unresolved(_) as u -> 
      // see if it is in the env map first
      let envVal = Map.tryFind cst hModel.env
      match envVal with
      | Some(c) -> ResolveCont hModel failResolver c
      | None -> 
          // not found in the env map --> check the equality sets
          let eq = hModel.ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
                              |> Utils.SetToOption
          match eq with 
          | Some(eqSet) -> 
              let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)
                               |> Utils.SetToOption
              match cOpt with 
              | Some(c) -> c
              | _ -> failResolver cst hModel
          | None ->
              failResolver cst hModel
//              // finally, see if it's an *input* (have no way of telling input from output params here) method argument
//              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList
//              match m with 
//              | (vc,_) :: [] -> vc
//              | _ -> failResolver cst hModel
  | SeqConst(cseq) -> 
      let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) []
      SeqConst(resolvedLst)
  | SetConst(cset) ->
      let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont hModel failResolver c)) Set.empty
      SetConst(resolvedSet)
  | _ -> cst

//  =====================================================================
/// Tries to resolve a given Const (cst) with respect to a given env/ctx. 
///
/// If unable to resolve, just returns the original Unresolved const.
//  =====================================================================
let TryResolve hModel cst = 
  ResolveCont hModel (fun c _ -> c) cst

//  ==============================================================
/// Resolves a given Const (cst) with respect to a given env/ctx. 
///
/// If unable to resolve, raises a ConstResolveFailed exception
//  ==============================================================
let Resolve hModel cst =
  ResolveCont hModel (fun c _ -> 
                        match c with
                        | Unresolved(id) -> BoxConst(id)
                        | _ -> failwithf "internal error: expected Unresolved but got %O" c
                     ) cst //fun c _ -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))
 
//  ==================================================================
/// Evaluates a given expression with respect to a given heap instance       
//  ==================================================================

let rec _EvalResolver heapInst useConcrete resolveExprFunc expr fldNameOpt = 
  let rec __FurtherResolve expr = 
    match expr with
    | SetExpr(elist)      -> SetExpr(elist |> List.map __FurtherResolve)
    | SequenceExpr(elist) -> SequenceExpr(elist |> List.map __FurtherResolve)
    | VarLiteral(_) ->
        try 
          _EvalResolver heapInst useConcrete resolveExprFunc expr None
        with 
        | _ -> expr
    | IdLiteral(id) when not (id = "this" || id = "null") ->
        try 
          _EvalResolver heapInst useConcrete resolveExprFunc expr None
        with 
        | _ -> expr
    | _ -> expr

  (* --- function body starts here --- *)
  let ex = match fldNameOpt with
            | None -> expr
            | Some(n) -> Dot(expr, n)
  if not (resolveExprFunc ex) then
    ex
  else
    match fldNameOpt with
    | None -> 
        match expr with
        | ObjLiteral("this") | ObjLiteral("null") -> expr
        | IdLiteral("this")  | IdLiteral("null") -> failwith "should never happen anymore" //TODO
        | VarLiteral(id) -> 
            match heapInst.methodArgs |> Map.tryFind id with
            | Some(argValue) -> argValue |> Const2Expr
            | None -> 
                let retVals = if useConcrete then heapInst.concreteMethodRetVals else heapInst.methodRetVals
                match retVals |> Map.tryFind id with
                | Some(e) -> e |> __FurtherResolve
                | None -> raise (EvalFailed("cannot find value for method parameter " + id))              
        | IdLiteral(id) ->
            let globalVal = heapInst.globals |> Map.tryFind id
            match globalVal with
            | Some(e) -> e
            | None -> _EvalResolver heapInst useConcrete resolveExprFunc ThisLiteral (Some(id))      
        | _ -> raise (EvalFailed(sprintf "I'm not supposed to resolve %O" expr))
    | Some(fldName) -> 
        match expr with
        | ObjLiteral(objName) -> 
            let asgs = if useConcrete then heapInst.concreteValues else heapInst.assignments
            let h2 = asgs |> List.filter (function FieldAssignment((o, var), v) -> o.name = objName && GetExtVarName var = fldName | _ -> false)
            match h2 with
            | FieldAssignment((_,_),x) :: [] -> __FurtherResolve x
            | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName))
            | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???
        | _ -> Dot(expr, fldName)

let _Eval heapInst resolveExprFunc returnFunc expr = 
  (* --- function body starts here --- *)
  //EvalSym  (__EvalResolver resolveExprFunc) expr
  EvalSymRet  (_EvalResolver heapInst false resolveExprFunc) returnFunc expr

/// Resolves nothing
let EvalNone heapInst expr = 
  EvalSym (_EvalResolver heapInst false (fun e -> false)) expr

let fullResolver heapInst = _EvalResolver heapInst true (fun e -> true)

/// Resolves everything
let EvalFull heapInst expr = 
  EvalSym (fullResolver heapInst) expr
  //_Eval heapInst (fun _ -> true) (fun e -> e) expr 

let Eval heapInst resolveExprFunc expr = 
  let returnFunc = fun expr -> match expr with IdLiteral(id) -> Dot(ThisLiteral, id) | _ -> expr
  EvalSymRet (fullResolver heapInst) (_EvalResolver heapInst false resolveExprFunc) returnFunc expr

let EvalAndCheckTrue heapInst resolveExprFunc expr = 
  let returnFunc = fun expr -> 
                     let expr =
                       match expr with
                       //| IteExpr(c,t,e) -> 
                       //    let cond = c |> EvalFull heapInst |> Expr2Bool
                       //    if cond then t else e
                       //| ForallExpr(vars, sub) -> expr
                       // TODO: this is just to ensure that all field accesses to this object are prefixed with "this."
                       //       this is not the best place to do it, though
                       | IdLiteral(id) -> Dot(ThisLiteral, id) 
                       | _ -> expr  
                     
                     // TODO: infer type of expr and then re-execute only if its type is Bool
                     let e1 = EvalFull heapInst expr //EvalSym (_EvalResolver heapInst true (fun _ -> true)) expr
                     match e1 with
                     | BoolLiteral(b) -> 
                         if b then
                           expr
                         else 
                           FalseLiteral
                           //UnaryNot expr
                     | _ -> expr
  EvalSymRet (fullResolver heapInst) (_EvalResolver heapInst false resolveExprFunc) returnFunc expr
  //_Eval heapInst resolveExprFunc returnFunc expr 

//  =====================================================================
/// Takes an unresolved model of the heap (HeapModel), resolves all 
/// references in the model and returns an instance of the heap 
/// (HeapInstance), where all fields for all objects have explicit 
/// assignments.
//  =====================================================================
let ResolveModel hModel (comp,meth) = 
  let outArgs = GetMethodOutArgs meth
  let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->
                                        let objName, objTypeOpt = match Resolve hModel o with
                                                                  | ThisConst(_,t) -> "this", t;
                                                                  | NewObj(name, t) -> PrintGenSym name, t
                                                                  | _ -> failwith ("unresolved object ref: " + o.ToString())
                                        let objType = objTypeOpt |> Utils.ExtractOptionMsg "unknown object type"
                                        let obj = {name = objName; objType = objType}
                                        let value = TryResolve hModel l |> Const2Expr
                                        Utils.ListMapAdd (obj, f) value acc 
                                     ) []
                         |> List.map (fun el -> FieldAssignment(el))
  let objs, modObjs = hmap |> List.fold (fun (acc1,acc2) asgn -> 
                                           match asgn with
                                           | FieldAssignment((obj,_),_) -> 
                                               let acc1' = acc1 |> Map.add obj.name obj
                                               let acc2' = 
                                                 if IsModifiableObj obj (comp,meth) then
                                                   acc2 |> Set.add obj
                                                 else
                                                   acc2
                                               acc1',acc2'
                                           | _ -> acc1,acc2
                                        ) (Map.empty, Set.empty)
  let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> 
                                                  match k with
                                                  | VarConst(name) -> 
                                                      let resolvedValExpr = Resolve hModel v
                                                      if outArgs |> List.exists (fun var -> GetVarName var = name) then
                                                        acc1, acc2 |> Map.add name (resolvedValExpr |> Const2Expr)
                                                      else
                                                        acc1 |> Map.add name resolvedValExpr, acc2
                                                  | _ -> acc1, acc2
                                               ) (Map.empty, Map.empty)
  { objs                   = objs;
    modifiableObjs         = modObjs;
    assignments            = hmap; 
    concreteValues         = hmap;
    methodArgs             = argmap; 
    methodRetVals          = retvals;
    concreteMethodRetVals  = retvals;
    globals                = Map.empty }

let rec GetCallGraph solutions graph = 
  let rec __SearchExprsForMethodCalls elist acc = 
    match elist with
    | e :: rest ->
        match e with 
        // no need to descend for, just check if the top-level one is MEthodCall
        | MethodCall(_,cname,mname,_) -> __SearchExprsForMethodCalls rest (acc |> Set.add (cname,mname))
        | _ -> __SearchExprsForMethodCalls rest acc 
    | [] -> acc
  match solutions with
  | ((comp,m), sol) :: rest -> 
        let callees = sol |> List.fold (fun acc (cond, hInst) ->
                                          hInst.assignments |> List.fold (fun acc asgn -> 
                                                                            match asgn with
                                                                            | FieldAssignment(_,e) ->
                                                                                __SearchExprsForMethodCalls [e] acc
                                                                            | ArbitraryStatement(stmt) -> 
                                                                                let exprs = ExtractTopLevelExpressions stmt
                                                                                __SearchExprsForMethodCalls exprs acc
                                                                         ) acc
                                       ) Set.empty
        let graph' = graph |> Map.add (comp,m) callees
        GetCallGraph rest graph'
  | [] -> graph

//////////////////////////////

//TODO: below here should really go to a different module

let __Is1stLevelExpr methodsOk heapInst expr = 
  DescendExpr2 (fun expr acc ->
                  if not acc then
                    false
                  else
                    match expr with
                    | Dot(discr, fldName) -> 
                        try
                          let obj = EvalFull heapInst discr
                          match obj with 
                          | ObjLiteral(id) -> id = "this"
                          | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"
                        with
                        | _ -> false
                    | MethodCall(_) -> methodsOk
                    | _ -> true                          
               ) expr true

let Is1stLevelExpr = __Is1stLevelExpr true

let IsSolution1stLevelOnly heapInst = 
  let rec __IsSol1stLevel stmts = 
    match stmts with
    | stmt :: rest -> 
        match stmt with
        | Assign(_, e)
        | ExprStmt(e) -> 
            let ok = Is1stLevelExpr heapInst e
            ok && __IsSol1stLevel rest
        | Block(stmts) -> __IsSol1stLevel (stmts @ rest)
    | [] -> true
  (* --- function body starts here --- *)
  __IsSol1stLevel (ConvertToStatements heapInst true)

let IsRecursiveSol (c,m) sol = 
  let compName = GetComponentName c
  let methName = GetMethodName m
  let allAssignments = sol |> List.map (fun (_,hInst) -> hInst.assignments) |> List.concat
  let allExprs = (allAssignments |> List.map ExtractAllExpressions |> List.concat) @
                 (sol |> List.map (fun (_,hInst) -> hInst.methodRetVals |> Map.toList |> List.map snd) |> List.concat)
  let singleExpr = allExprs |> List.fold BinaryAnd TrueLiteral
  DescendExpr2 (fun expr acc ->
                  if acc then
                    true
                  else
                    match expr with
                    | MethodCall(_, cn, mn, elst) when cn = compName && mn = methName -> 
                        true
                    | _ -> false
                ) singleExpr false

/// Returns a list of direct modifiable children objects with respect to "this" object
///
/// All returned expressions are of type ObjLiteral
///
/// ensures: forall e :: e in ret ==> e is ObjInstance
let GetDirectModifiableChildren 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

  (* --- function body starts here --- *)
  let thisRhsExprs = hInst.assignments |> List.choose (function FieldAssignment((obj,_),e) when obj.name = "this" && Set.contains obj hInst.modifiableObjs  -> Some(e) | _ -> None)
  thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty 
               |> Set.toList