From 88c193d71cac69d501c8f55e65b6b3628edcb684 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 31 Aug 2024 00:30:03 +0200 Subject: [PATCH] fix: out of bounds access when the CNF is too small (#5220) As reported by @alexkeizer to me. --- src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean | 12 +++++++++++- tests/lean/run/bv_unused.lean | 11 +++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/bv_unused.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index bcd31a4eb0..71d872307f 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -45,8 +45,18 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar 2. The actual BitVec bitwise variables Hence we access the assignment array offset by the AIG size to obtain the value for a BitVec bit. We assume that a variable can be found at its index as CaDiCal prints them in order. + + Note that cadical will report an assignment for all literals up to the maximum literal from the + CNF. So even if variable or AIG bits below the maximum literal did not occur in the CNF they + will still occur in the assignment that cadical reports. + + There is one crucial thing to consider in addition: If the highest literal that ended up in the + CNF does not represent the highest variable bit not all variable bits show up in the assignment. + For this situation we do the same as cadical for literals that did not show up in the CNF: + set them to true. -/ - let (varSet, _) := assignment[cnfVar + aigSize]! + let idx := cnfVar + aigSize + let varSet := if h : idx < assignment.size then assignment[idx].fst else true let mut bitMap := sparseMap.getD bitVar.var {} bitMap := bitMap.insert bitVar.idx varSet sparseMap := sparseMap.insert bitVar.var bitMap diff --git a/tests/lean/run/bv_unused.lean b/tests/lean/run/bv_unused.lean new file mode 100644 index 0000000000..15755881b5 --- /dev/null +++ b/tests/lean/run/bv_unused.lean @@ -0,0 +1,11 @@ +import Std.Tactic.BVDecide + +open BitVec + +/-- +error: The prover found a potential counterexample, consider the following assignment: +y = 0xffffffffffffffff#64 +-/ +#guard_msgs in +example {y : BitVec 64} : zeroExtend 32 y = 0 := by + bv_decide