From 23b557102910cf921b8011f8390b6d6cc81125a4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:39:21 -0800
Subject: [PATCH] [sledge] Normalize Splat 0 to 0

Summary:
0 and Splat 0 need to be treated the same since code relies on knowing
that 0 consists of all-0 bytes, and extracting a subsequence of a
Splat 0 yields 0. For example, initializing a struct to all-zeros and
then reading a member of pointer type out of it needs to produce the
null pointer. Therefore 0 and Splat 0 are redundant representations,
and all uses of Splat need to be updated to also handle 0.

This unfortunately leads to some near code duplication that seems to
be necessary. The issue is that 0 and Splat 0 are, from the backend's
perspective, constants in two distinct theories. Since 0 is chosen
over Splat 0 as the representation, the sequence theory solver needs
to treat 0 as if it was Splat 0, which duplicates some code handling
the general Splat cases.

Reviewed By: jvillard

Differential Revision: D24920758

fbshipit-source-id: 7c02be62b
---
 sledge/src/fol/context.ml |  3 +++
 sledge/src/fol/trm.ml     | 11 ++++++++++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index ae8fe5a93..29d23d39d 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -305,6 +305,9 @@ and solve_ ?f d e s =
   (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
   | Some (Sized {siz= n; seq= a}, Sized {siz= m; seq= b}) ->
       s |> solve_ ?f n m >>= solve_ ?f a b
+  (* ⟨n,0⟩ = α₀^…^αᵥ ==> *)
+  | Some ((Sized {siz= n; seq} as b), Concat a0V) when seq == Trm.zero ->
+      solve_concat ?f a0V b n s
   (* ⟨n,e^⟩ = α₀^…^αᵥ ==> *)
   | Some ((Sized {siz= n; seq= Splat _} as b), Concat a0V) ->
       solve_concat ?f a0V b n s
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index e28787280..3336387b0 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -208,7 +208,10 @@ end = struct
 
   let add x y = _Arith Arith.(add (trm x) (trm y))
   let sub x y = _Arith Arith.(sub (trm x) (trm y))
-  let _Splat x = Splat x |> check invariant
+
+  let _Splat x =
+    (* 0^ ==> 0 *)
+    (if x == zero then x else Splat x) |> check invariant
 
   let seq_size_exn =
     let invalid = Invalid_argument "seq_size_exn" in
@@ -254,6 +257,8 @@ end = struct
       (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *)
       | Extract {seq= a; off= m; len= k} when partial_ge k o_l ->
           _Extract a (add m off) len
+      (* ⟨_,0⟩[_,_) ==> 0 *)
+      | Sized {seq} when seq == zero -> seq
       (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *)
       | Sized {siz= n; seq= Splat _ as e} when partial_ge n o_l ->
           _Sized e len
@@ -321,6 +326,10 @@ end = struct
         when equal na na' && equal o_k (add o k) && partial_ge n (add o_k l)
         ->
           Some (_Extract na o (add k l))
+      (* ⟨m,0⟩^⟨n,0⟩ ==> ⟨m+n,0⟩ *)
+      | Sized {siz= m; seq= a}, Sized {siz= n; seq= a'}
+        when a == zero && a' == zero ->
+          Some (_Sized a (add m n))
       (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
       | Sized {siz= m; seq= Splat _ as a}, Sized {siz= n; seq= a'}
         when equal a a' ->