From a3e7107969431eb3e6b688cfeed65a3eabcbe468 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 23 May 2019 15:38:31 -0700
Subject: [PATCH] [sledge] Optimize variable renaming in symbolic heaps

Summary:
Add shortcut code paths to return early in some cases guaranteed to be
the identity function.

Reviewed By: ngorogiannis

Differential Revision: D15468704

fbshipit-source-id: f137049c6
---
 sledge/src/llair/exp.ml   |  3 +++
 sledge/src/llair/exp.mli  |  1 +
 sledge/src/symbheap/sh.ml | 19 ++++++++++++-------
 3 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 0615e4064..70b58feb1 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -596,6 +596,9 @@ module Var = struct
     let exclude sub vs =
       Set.fold vs ~init:sub ~f:Map.remove |> check invariant
 
+    let restrict sub vs =
+      Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
+
     let domain sub =
       Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
           Set.add domain key )
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index c82866c11..2ce055b02 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -121,6 +121,7 @@ module Var : sig
     val extend : t -> replace:var -> with_:var -> t
     val invert : t -> t
     val exclude : t -> Set.t -> t
+    val restrict : t -> Set.t -> t
     val is_empty : t -> bool
     val domain : t -> Set.t
     val range : t -> Set.t
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 9c09abeb2..9ecb0d73e 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -195,10 +195,13 @@ let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
 and rename sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;
-  let sub = Var.Subst.exclude sub q.xs in
-  let us = Var.Subst.apply_set sub q.us in
-  let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Subst.range sub)) in
-  (if us == q.us && q' == q then q else {q' with us})
+  let sub = Var.Subst.restrict sub q.us in
+  ( if Var.Subst.is_empty sub then q
+  else
+    let us = Var.Subst.apply_set sub q.us in
+    assert (not (Set.equal us q.us)) ;
+    let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Subst.range sub)) in
+    {q' with us} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -210,9 +213,11 @@ and freshen_xs q ~wrt =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
   ;
   let sub = Var.Subst.freshen q.xs ~wrt in
-  let xs = Var.Subst.apply_set sub q.xs in
-  let q' = apply_subst sub q in
-  (if xs == q.xs && q' == q then q else {q' with xs})
+  ( if Var.Subst.is_empty sub then q
+  else
+    let xs = Var.Subst.apply_set sub q.xs in
+    let q' = apply_subst sub q in
+    if xs == q.xs && q' == q then q else {q' with xs} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;