From 87ebbbd95d350554266324230abd761e50580c08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 29 Aug 2024 10:23:53 +0200 Subject: [PATCH 1/2] 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 | 8 ++++++-- tests/bitv/testfile-bvshl-001.expected | 2 ++ tests/bitv/testfile-bvshl-001.smt2 | 9 +++++++++ tests/bitv/testfile-bvshl-002.expected | 2 ++ tests/bitv/testfile-bvshl-002.smt2 | 6 ++++++ 5 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 tests/bitv/testfile-bvshl-001.expected create mode 100644 tests/bitv/testfile-bvshl-001.smt2 create mode 100644 tests/bitv/testfile-bvshl-002.expected create mode 100644 tests/bitv/testfile-bvshl-002.smt2 diff --git a/src/lib/reasoners/domains.ml b/src/lib/reasoners/domains.ml index f8b49076c..ee6edc0d7 100644 --- a/src/lib/reasoners/domains.ml +++ b/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 = diff --git a/tests/bitv/testfile-bvshl-001.expected b/tests/bitv/testfile-bvshl-001.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/bitv/testfile-bvshl-001.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/bitv/testfile-bvshl-001.smt2 b/tests/bitv/testfile-bvshl-001.smt2 new file mode 100644 index 000000000..159537e19 --- /dev/null +++ b/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) diff --git a/tests/bitv/testfile-bvshl-002.expected b/tests/bitv/testfile-bvshl-002.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/bitv/testfile-bvshl-002.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/bitv/testfile-bvshl-002.smt2 b/tests/bitv/testfile-bvshl-002.smt2 new file mode 100644 index 000000000..4d25fbb00 --- /dev/null +++ b/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) From fda508967620a864a9dc834a76d71ae26bd440fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 29 Aug 2024 11:13:39 +0200 Subject: [PATCH 2/2] Clarify doc --- src/lib/reasoners/domains_intf.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/domains_intf.ml b/src/lib/reasoners/domains_intf.ml index a60b42414..f6954545d 100644 --- a/src/lib/reasoners/domains_intf.ml +++ b/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