goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

Replace JSON schema validation and add full options schema #476

Closed sim642 closed 2 years ago

sim642 commented 2 years ago

Our JSON schema validation for options is something custom, not the standard http://json-schema.org/. Moreover, our default schema is massively incomplete and fails to detect typos when merging entire JSON files in with --conf.

We should describe our entire options structure with the official JSON schema and use the only existing OCaml library to validate it: https://github.com/ocamlpro/ocplib-json-typed (supports Yojson conversion).

The complete schema could entirely replace our Defaults module, by also having the default values and descriptions inside the schema. This would also allow describing finite string choice options in the schema and detect invalid values already there.

sim642 commented 2 years ago

Apparently the library doesn't support arbitrary schema validation out-of-the-box, since it's more geared towards constructing static type-safe encodings: https://github.com/OCamlPro/ocplib-json-typed/issues/38. Also, it's successor is https://gitlab.com/nomadic-labs/json-data-encoding.

I think I'll still be able to abuse the library a bit to do what we need without writing everything from scratch.

vogler commented 2 years ago

This is just about runtime validation, in OCaml the options are still referenced by strings, right? Could define options by mutable records and ppx-generate the json (un)parsing. Gives you static checks for reading, autocomplete, and presumably better performance - the idea was to be able to bake a fixed configuration by making fields immutable and let the compiler hopefully optimize. I have a prototype somewhere.

sim642 commented 2 years ago

Yes, this doesn't change the internal structure that stores the runtime configuration or modifies it. Changing that would be a separate issue.

What nested record types don't give you is the ability to attach descriptions like the current Defaults has and like JSON schemas also do. Sure, you can put descriptions into ocamldoc comments, but that's completely static and not exposed in any way at runtime (e.g. --print_all_options or to Gobview, etc to show in some interface.

The json-data-encoding library actually is mostly designed around doing something statically typed: you define the whole structure as a GADT with JSON-schema-like constraint possibilities. It even allows exporting a JSON schema itself. But the massive downside is that it has no reasonable way to have those types be nice records, but objN and merge_objs constructors that it provides just construct a mess of nested tuples, which won't really work for the size of objects we would like to define.

vogler commented 2 years ago

What nested record types don't give you is the ability to attach descriptions like the current Defaults has and like JSON schemas also do.

Yes, that was the reason why I didn't continue with it. Would require some custom ppx or registering each option's default value together with a description string. There were some other issues with default values as well: https://github.com/ocaml-ppx/ppx_deriving_yojson/issues/created_by/vogler

sim642 commented 2 years ago

I managed to find ppx_deriving_encoding, which promises to be able to construct those json-data-encoding GADTs for record types by generating the necessary two-way conversions with the tuple encodings. The encodings and the ppx have the ability to attach default values and descriptions, so it might be possible to use it to replace our internal representaton from Yojson to nested records, which come with everything else built in as well, but I'd leave it for the future since it requires widespread changes to every option access. And we have some, where options are accesses by constructing the name strings (e.g. for warning options).