Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007822OCamltypingpublic2018-07-16 13:592018-08-01 07:32
Reporteroctachron 
Assigned Togarrigue 
PrioritylowSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product Version4.07.0 
Target Version4.08.0+devFixed in Version 
Summary0007822: Refuting a pathological but reachable pattern with chess
DescriptionWhen typing overly complex refutation clauses, it is possible to exploit the lack of backtracking for ident binding time in the counter-example search to go beyond the authorized number of existential variables during the search and then refute the pattern even if counter-examples exist further down in the search tree.

As an illustration, the attached file construct a type level encoding of
of a piece moving on a 4×4 board and then proceed to simultaneously
refute the existence of hamiltonian paths and produce a hamiltonian path
as a counter-example (by pruning the search path and avoiding the issue above).

Does this count as a bug?
TagsNo tags attached.
Attached Files? file icon minichess.ml [^] (3,811 bytes) 2018-07-16 13:59 [Show Content]

- Relationships

-  Notes
(0019249)
gasche (administrator)
2018-07-16 14:02

Clearly the most beautiful bug this month -- for now.
(0019281)
garrigue (manager)
2018-07-30 09:52

Using ocaml 4.06.1, the search seems to go on forever.
What version did you use?
(0019282)
octachron (developer)
2018-07-30 10:04

I tested on 4.07.0, where it only takes few seconds to fail on the second refutation clause.
(0019285)
garrigue (manager)
2018-07-31 12:13

For the second clause, it indeed produces a counter example.
My question was for the first clause. How long does it take to be accepted without warning?
For me on MacOS, it just goes on forever, so the bug does not appear.
(0019286)
garrigue (manager)
2018-07-31 12:19

Sorry. Indeed on 4.07.0, and on the 4.07 branch the first clause succeeds pretty fast too.
However on 4.06.0 it goes on forever, whereas the allowed number of existentials is supposed to be lower.
Mystery in the search.
(0019287)
octachron (developer)
2018-07-31 12:27
edited on: 2018-07-31 12:27

On 4.06.1, it takes me ~ 10 minutes to find a counter-example for the first refutable clause. I have another example with a 3×4 board where it only takes ~ 30 seconds to find a counter-example with 4.06.1 (whereas 4.07 still fail to find it). Should I upload it?

(0019289)
garrigue (manager)
2018-08-01 07:32

For there record:

there_are_no_wazir_tours (Right::Right::Up::Up::Left::Down::Left::Up::Left::Down::Down::Down:: Right::Right::Right::[]);;
Exception: Match_failure ("//toplevel//", 1, 59).

Turning it into a segfault should be easy (using the result type).
(0019290)
garrigue (manager)
2018-08-01 07:32

There is now a GPR fixing that.
Please review :)

https://github.com/ocaml/ocaml/pull/1951 [^]

- Issue History
Date Modified Username Field Change
2018-07-16 13:59 octachron New Issue
2018-07-16 13:59 octachron File Added: minichess.ml
2018-07-16 14:02 gasche Note Added: 0019249
2018-07-30 09:17 garrigue Assigned To => garrigue
2018-07-30 09:17 garrigue Status new => assigned
2018-07-30 09:52 garrigue Note Added: 0019281
2018-07-30 09:52 garrigue Status assigned => feedback
2018-07-30 10:04 octachron Note Added: 0019282
2018-07-30 10:04 octachron Status feedback => assigned
2018-07-31 12:13 garrigue Note Added: 0019285
2018-07-31 12:13 garrigue Status assigned => feedback
2018-07-31 12:19 garrigue Note Added: 0019286
2018-07-31 12:19 garrigue Status feedback => confirmed
2018-07-31 12:21 garrigue Product Version => 4.07.0
2018-07-31 12:21 garrigue Target Version => 4.08.0+dev
2018-07-31 12:27 octachron Note Added: 0019287
2018-07-31 12:27 octachron Note Edited: 0019287 View Revisions
2018-08-01 07:32 garrigue Note Added: 0019289
2018-08-01 07:32 garrigue Note Added: 0019290


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker