[sledge] Fix Exp.map and garbage_collect

Summary:
:
* Fix non termination of garbage collection
* Fix implementation of Exp.map to handle recursive Exps (vtables)

Reviewed By: jberdine

Differential Revision: D16089676

fbshipit-source-id: 337c19f18

sledge/src/llair/exp.ml

@@ -1289,33 +1289,38 @@ let size_of t =
 (** Transform *)
 
 let map e ~f =
-  let map_bin mk ~f x y =
+  let map_ : (t -> t) -> t -> t =
-    let x' = f x in
+   fun map_ e ->
-    let y' = f y in
+    let map_bin mk ~f x y =
-    if x' == x && y' == y then e else mk x' y'
+      let x' = f x in
-  in
+      let y' = f y in
-  let map_vector mk ~f args =
+      if x' == x && y' == y then e else mk x' y'
-    let args' = Vector.map_preserving_phys_equal ~f args in
+    in
-    if args' == args then e else mk args'
+    let map_vector mk ~f args =
-  in
+      let args' = Vector.map_preserving_phys_equal ~f args in
-  let map_qset mk typ ~f args =
+      if args' == args then e else mk args'
-    let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
+    in
-    if args' == args then e else mk typ args'
+    let map_qset mk typ ~f args =
+      let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
+      if args' == args then e else mk typ args'
+    in
+    match e with
+    | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
+    | Add {args; typ} -> map_qset addN typ ~f args
+    | Mul {args; typ} -> map_qset mulN typ ~f args
+    | Splat {byt; siz} -> map_bin simp_splat ~f byt siz
+    | Memory {siz; arr} -> map_bin simp_memory ~f siz arr
+    | Concat {args} -> map_vector simp_concat ~f args
+    | Struct_rec {elts= args} -> Struct_rec {elts= Vector.map args ~f:map_}
+    | _ -> e
   in
-  match e with
+  fix map_ (fun e -> e) e
-  | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
-  | Add {args; typ} -> map_qset addN typ ~f args
-  | Mul {args; typ} -> map_qset mulN typ ~f args
-  | Splat {byt; siz} -> map_bin simp_splat ~f byt siz
-  | Memory {siz; arr} -> map_bin simp_memory ~f siz arr
-  | Concat {args} -> map_vector simp_concat ~f args
-  | _ -> e
 
 let rename e sub =
   let rec rename_ e sub =
     match e with
     | Var _ -> Var.Subst.apply sub e
-    | _ -> map e ~f:(fun f -> rename_ f sub)
+    | _ -> map ~f:(fun f -> rename_ f sub) e
   in
   rename_ e sub |> check (invariant ~partial:true)
 

sledge/src/symbheap/state_domain.ml

@@ -49,7 +49,7 @@ let garbage_collect (q : t) ~wrt =
   (* only support DNF for now *)
   assert (List.is_empty q.djns) ;
   let rec all_reachable_vars previous current (q : t) =
-    if previous == current then current
+    if Var.Set.equal previous current then current
     else
       let new_set =
         List.fold ~init:current q.heap ~f:(fun current seg ->