Stream: Coq devs & plugin devs

Topic: Validation bug?


view this post on Zulip Mario Carneiro (Dec 12 2023 at 15:35):

I'm reading the code in check.ml for my own understanding (I haven't done any tests), so this could be incorrect, but I noticed something odd:

The definition v_libraryobjs is used to validate the library_objects type in check.ml, but these types are significantly different. The one in check.ml uses Dyn while v_libraryobjs has a more precise type, but even before that it seems that check.ml thinks the list elements have type Id.t * obj while values.ml says the elements have type v_libobjt which is a sum type and would presumably not match the structure of a tuple in most situations.

view this post on Zulip Mario Carneiro (Dec 12 2023 at 16:19):

another bug: v_level says it has 3 constant constructors (SProp, Prop, Set) but the actual type only has one (Set) and the other two are missing for some reason

view this post on Zulip Mario Carneiro (Dec 12 2023 at 17:07):

v_retro_action has 3 constructors but Retroknowledge.action has 2

view this post on Zulip Gaëtan Gilbert (Dec 12 2023 at 20:17):

v_libraryobjs is correct and Check.library_objects is incorrect, but this doesn't lead to an observable bug because the checker doesn't actually use it (we could and probably should make Check.library_objects an abstract type)
the other 2 probably can lead to segfaults on crafted .vo files

we should probably figure out some way to generate values.ml from the types we check but no work has been done on this

view this post on Zulip Mario Carneiro (Dec 12 2023 at 20:23):

found another one, v_library_info has 2 variants but LibraryInfo.t has 1 (and the Deprecation variant has the wrong tag)

view this post on Zulip Gaëtan Gilbert (Dec 12 2023 at 20:28):

v_libsum has 4 fields but Check.summary_disk only has 3 (the last one is where libraryinfo should be) x_x

view this post on Zulip Gaëtan Gilbert (Dec 12 2023 at 20:31):

also v_library_info changed recently, it looks correct now


Last updated: Oct 13 2024 at 01:02 UTC