From 1afd4f55ba858223abf8d060182d6f1a061ffc5e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 15 Jan 2020 13:17:56 -0800
Subject: [PATCH] [sledge] Classify Memory and Concat terms as Simplified

Summary:
It is necessary to normalize subterms of Memory and Concat terms or
else Equality.entails_eq is incomplete. They ought to be Interpreted,
but the solver for the byte-array theory is not yet ready for that.

Reviewed By: ngorogiannis

Differential Revision: D19282635

fbshipit-source-id: c06b6ca6d
---
 sledge/src/symbheap/equality.ml      |  7 ++++---
 sledge/src/symbheap/equality_test.ml | 10 +++++++---
 sledge/src/symbheap/solver_test.ml   |  3 +--
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 4241ffaf7..50c04388b 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -15,7 +15,8 @@ type kind = Interpreted | Simplified | Atomic | Uninterpreted
 let classify e =
   match (e : Term.t) with
   | Add _ | Mul _ -> Interpreted
-  | Ap2 ((Eq | Dq), _, _) -> Simplified
+  | Ap2 ((Eq | Dq), _, _) | Ap2 (Memory, _, _) | ApN (Concat, _) ->
+      Simplified
   | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted
   | RecN _ | Var _ | Integer _ | Float _ | Nondet _ | Label _ -> Atomic
 
@@ -266,8 +267,8 @@ let rec canon r a =
 (** add a term to the carrier *)
 let rec extend a r =
   match classify a with
-  | Interpreted | Simplified -> Term.fold ~f:extend a ~init:r
-  | Uninterpreted -> (
+  | Interpreted -> Term.fold ~f:extend a ~init:r
+  | Simplified | Uninterpreted -> (
     match Subst.extend a r.rep with
     | Some rep -> Term.fold ~f:extend a ~init:{r with rep}
     | None -> r )
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 18f74a4e6..cd6d5c60f 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -320,7 +320,9 @@ let%test_module _ =
     let r14 = of_eqs [(a, a); (x, !1)]
 
     let%expect_test _ =
-      pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r14 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
 
@@ -331,7 +333,7 @@ let%test_module _ =
       pp r14 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
     let%test _ = entails_eq r14 b Term.true_
@@ -340,7 +342,9 @@ let%test_module _ =
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
-      pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r15 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r15 b (Term.signed 1 !1)
     let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index 01338f2f9..948b17923 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -185,8 +185,7 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
-          ∧ ⟨%n_9,%a0_10⟩ = ⟨16,%a_2⟩
-          ∧ ⟨32,%a_1⟩ = ⟨%n_9,%a0_10⟩^⟨16,%a1_11⟩
+          ∧ ⟨32,%a_1⟩ = ⟨16,%a_2⟩^⟨16,%a1_11⟩
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]