Skip to content

Conversation

@jmid
Copy link
Contributor

@jmid jmid commented Jul 9, 2025

The forthcoming QCheck 0.26 release ocaml/opam-repository#28148 changes the distribution of the float generator to avoid blind spots: c-cube/qcheck#350. As a consequence, an existing goblint analyzer test now fails to hold, resulting in:

File "src/core/QCheck2.ml", line 2005, characters 1-1:
Error: :1:floatDomainTest:1:float_interval_qcheck32:2:test_FI_div_zero_result_top (in the code).


test `test_FI_div_zero_result_top` failed on ≥ 1 cases: <instance>

This PR first patches the arbitrary generator to use the existing show function to print counterexamples:

File "src/core/QCheck2.ml", line 2005, characters 1-1:
Error: :1:floatDomainTest:1:float_interval_qcheck32:2:test_FI_div_zero_result_top (in the code).


test `test_FI_div_zero_result_top` failed on ≥ 1 cases: [0.,0.]

Second, it patches the property of the mentioned QCheck test to account for the [0.;0.] / [0.;0.] case.
Here, I was guided by the unit test above already exercising this corner case:

let test_FI_div_specific _ =
let (/) = FI.div in
let (=) a b = assert_equal b a in
begin
fi_zero / fi_one = fi_zero;
(FI.of_const 2.) / fi_zero = FI.top ();
fi_zero / fi_zero = FI.nan ();

In retrospect, I can see the arbitrary () generator produces random intervals by mapping convert_arb over a pair of random floats. The chance of producing a unit (const) interval with that strategy is close to zero. 🤔
I believe the change of distribution (and the ability of emitting nan) is the reason why the failure started to trigger with QCheck 0.26:

# min nan 0.;;
- : float = 0.
# max nan 0.;;
- : float = 0.

I therefore encourage you to investigate the distribution of the generator. I just adjusted the output of collect stats in QCheck 0.26 c-cube/qcheck#351 which lends itself to a nice "top", "bot", "const", "non-const" classification... 🤓 😅

Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for looking so deep into our tests!

@sim642 sim642 merged commit 1278886 into goblint:master Jul 11, 2025
11 checks passed
@jmid jmid deleted the adjust-div-zero-result-top-test branch July 11, 2025 07:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants