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

…ro#1225)

* 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.

* Clarify doc

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 =

src/lib/reasoners/domains_intf.ml

@@ -140,9 +140,11 @@ module type EphemeralDomainMap = sig
     (** [set_domain e d] sets the domain of entry [e] to [d]. This overwrites
         any pre-existing domain associated with [e].
 
-        {b Note}: if you need to tighten an existing domain, this must be done
-        explicitely by accessing the current domain through [domain] before
-        calling [set_domain].  See {!MakEntryNotation}. *)
+        {b Note}: the caller is responsible for ensuring that the domain is
+        a subset of the possible domains for the entry (e.g. due to type
+        constraints). The recommended way to do so is by first intersecting
+        with the existing [domain]. See also the {!EntryNotation} functor
+        which does this for you. *)
   end
 
   val entry : t -> key -> Entry.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)