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] 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 f8b49076cc..ee6edc0d7b 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 0000000000..a6e005255c --- /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 0000000000..159537e197 --- /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 0000000000..a6e005255c --- /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 0000000000..4d25fbb001 --- /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)