fix(CP): Make sure domains do not overflow the default domain

When reading domains through a non-canonical representative, we are
intersecting it with the default domain of the representative (i.e. the
range of the bit-vector type) in order to ensure that the resulting
domain is known to be within the range of the type.

This is useful for interval domains because we keep track of global
bounds, which we rely on in functions such as [bvshl], but are forgotten
by the call to [add_explanation].

We also need to perform the same intersection when modifying a domain
through a non-canonical representative, otherwise we might store a
domain that overflows the bounds of the type.

(It is unfortunate that we have to do this dance instead of storing type
information on the interval themselves, but that would be a bigger change).

This was found by fuzzing.

src/lib/reasoners/domains.ml

@@ -530,8 +530,12 @@ struct
             D.intersect (D.unknown (X.type_info repr)) @@
             D.add_explanation ~ex (Entry.domain entry)
 
-        let set_domain { entry ; explanation = ex ; _ } d =
-          Entry.set_domain entry (D.add_explanation ~ex d)
+        let set_domain { repr ; entry ; explanation = ex } d =
+          if Explanation.is_empty ex then Entry.set_domain entry d
+          else
+            Entry.set_domain entry @@
+            D.intersect (D.unknown (X.type_info repr)) @@
+            D.add_explanation ~ex d
       end
 
       type nonrec t =

tests/bitv/testfile-bvshl-001.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/bitv/testfile-bvshl-001.smt2

@@ -0,0 +1,9 @@
+(set-logic ALL)
+(declare-fun T4_306 () (_ BitVec 32))
+(declare-fun T1_306 () (_ BitVec 8))
+(declare-fun T1_307 () (_ BitVec 8))
+(declare-fun T1_308 () (_ BitVec 8))
+(declare-fun T1_309 () (_ BitVec 8))
+(assert (and (xor (or (bvule (_ bv0 32) T4_306) (= T4_306 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_309) (_ bv8 32)) ((_ zero_extend 24) T1_308)) (_ bv8 32)) ((_ zero_extend 24) T1_307)) T4_306) ((_ zero_extend 24) T1_306)))) (=> (bvult (_ bv8 32) T4_306) (and true (= (_ bv0 32) (bvor (bvshl ((_ zero_extend 24) T1_306) (_ bv8 32)) ((_ zero_extend 24) T1_306))) (bvult (_ bv0 32) T4_306) (bvule (_ bv0 32) (_ bv8 32))))) (bvult (_ bv0 32) T4_306)))
+(check-sat)
+(exit)

tests/bitv/testfile-bvshl-002.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/bitv/testfile-bvshl-002.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-fun T1_7389 () (_ BitVec 8))
+(declare-fun T1_7390 () (_ BitVec 8))
+(assert (=> (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (xor (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32))))))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (xor (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))))))))
+(check-sat)
+(exit)