Fix and uncomment failing domain property tests #99
Description
This is a follow-up issue to PR #86. Before merging I commented out all the property testing of all the (integer) domains where something failed, so it doesn't cause CI to massively fail on the master branch but still brings the property testing infrastructure up to date to a usable place.
Usage
- Compiling:
make domaintest - Running:
./goblint.domaintest.
See--helpfor other useful flags provided by qcheck, e.g.-vor--long.
Current situation
That special standalone binary runs property tests on the domains listed in maindomaintest.ml. The first list domains just tests lattice properties (see DomainProperties) and the second list intDomains is also intended to additionally check things like whether the integer domain is a valid abstraction of finite sets of integers (see IntDomainProperties).
TODO
As you can see, most of them are currently commented out and possibly even in the wrong list. What needs to be done is commenting them out and seeing what fails and hopefully fixing the issue. For example for DefExc 9 lattice properties apparently fail:
--- Failure --------------------------------------------------------------------
Test def_exc: join assoc failed (187 shrink steps):
(Not {1}([-63,63]), 0, -1)
--- Failure --------------------------------------------------------------------
Test def_exc: join abs failed (61 shrink steps):
(Not {109}([-63,63]), Unknown int([-63,63]))
--- Failure --------------------------------------------------------------------
Test def_exc: meet leq failed (62 shrink steps):
(Unknown int([-63,63]), Not {-98}([-63,63]))
--- Failure --------------------------------------------------------------------
Test def_exc: meet idem failed (61 shrink steps):
Not {126}([-63,63])
--- Failure --------------------------------------------------------------------
Test def_exc: meet abs failed (61 shrink steps):
(Not {-118}([-63,63]), Unknown int([-63,63]))
--- Failure --------------------------------------------------------------------
Test def_exc: top meet failed (60 shrink steps):
Not {118}([-63,63])
--- Failure --------------------------------------------------------------------
Test def_exc: connect join failed (33 shrink steps):
(7144723426, Unknown int([-63,63]))
--- Failure --------------------------------------------------------------------
Test def_exc: connect meet failed (57 shrink steps):
(Unknown int([-63,63]), Not {100}([-63,63]))
--- Failure --------------------------------------------------------------------
Test def_exc: narrow fst failed (63 shrink steps):
(Not {110}([-63,63]), Unknown int([-63,63]))
Since the integer domains have been actively worked on, it might also be a good time to investigate these now. The arbitrary instaces for those domains should also be looked over to make sure they don't generate anything semantically invalid or generalized to generate values with differing ranges.
Also from what I've noticed in some of the integer domain fixes is changing how their operations handle bot, some of the integer domain properties might have to be changed to exclude such cases.