[sledge] Delay normalization of xor to equality

Summary:
Boolean and bitwise negation of `e` is represented using `-1 xor
e`. Since Equality can only maintain and propagate equality
constraints, Boolean negation `-1 xor b` is normalized to `b =
false`. This diff delays this normalization from being part of
expression construction to part of symbolic heap formula
construction. This makes the normalization done as part of expression
construction independent of the distinction between bitwise and
boolean operations.

Reviewed By: bennostein

Differential Revision: D17665254

fbshipit-source-id: 0a0722865

sledge/src/llair/exp.ml

@@ -894,8 +894,6 @@ let rec simp_not (typ : Typ.t) exp =
       simp_cond cnd (simp_not typ thn) (simp_not typ els)
   (* ¬false ==> true ¬true ==> false *)
   | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data)
-  (* ¬b ==> false = b *)
-  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
   (* ¬e ==> true xor e *)
   | e, _ ->
       App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}
@@ -938,11 +936,6 @@ let simp_xor x y =
   | Integer {data= i; typ}, Integer {data= j} ->
       let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
       integer (Z.blogxor ~bits i j) typ
-  (* true xor b ==> ¬b *)
-  | Integer {data; typ= Integer {bits= 1}}, b
-   |b, Integer {data; typ= Integer {bits= 1}}
-    when Z.is_true data ->
-      simp_not Typ.bool b
   | _ -> App {op= App {op= Xor; arg= x}; arg= y}
 
 let simp_shl x y =

sledge/src/symbheap/sh.ml

@@ -380,9 +380,20 @@ let rec pure (e : Term.t) =
   [%Trace.call fun {pf} -> pf "%a" Term.pp e]
   ;
   let us = Term.fv e in
+  let eq_false b =
+    let cong = Equality.and_eq b (Term.bool false) Equality.true_ in
+    {emp with us; cong; pure= [e]}
+  in
   ( match e with
   | Integer {data; typ= Integer {bits= 1}} ->
       if Z.is_false data then false_ us else emp
+  (* ¬b ==> false = b *)
+  | App {op= App {op= Xor; arg= Integer {data; typ= Integer {bits= 1}}}; arg}
+    when Z.is_true data ->
+      eq_false arg
+  | App {op= App {op= Xor; arg}; arg= Integer {data; typ= Integer {bits= 1}}}
+    when Z.is_true data ->
+      eq_false arg
   | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2)
   | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2)
   | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}

sledge/src/symbheap/term.ml

@@ -990,8 +990,6 @@ let rec simp_not (typ : Typ.t) term =
       simp_cond cnd (simp_not typ thn) (simp_not typ els)
   (* ¬false ==> true ¬true ==> false *)
   | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data)
-  (* ¬b ==> false = b *)
-  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
   (* ¬e ==> true xor e *)
   | e, _ ->
       App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}