[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

@@ -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

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' ->