refactor query system with GADTs

[vogler]

The query system uses a variant type for the question and a polymorphic variant type for the result.

Problem Every query has only a subset of valid return variants. This information is not encoded in the type, i.e., every question might return any result.

Idea Use GADTs. Problem Subtyping (r can't be covariant): code, issue.

Idea Get rid of need for subtyping (the result type seems partially redundant anyway):

type 'd r = Result of 'd | Top | Bot
let rec query : type d. d t -> d r = ...

[sim642]

I don't think we have any queries that may return results from different lattices. Also it wouldn't be very sensible, because if two analyses responded with results from different lattices, then their meet would go to the result lattice bottom anyway, which isn't meaningful. Therefore I think we should be perfectly fine having one result lattice per query. I guess this would avoid all the polymorphic variant and subtyping issues?

But if that's the case, then we don't need the query return type to have its own Top and Bot when the result lattice should have its own anyway. That Bot could never occur, because there would be no meet between different result lattices. And that Top is redundant because how would it be different from the result lattice's own top? We have cases where we need to explicitly make them the same if the responding analysis is deactivated, but that should be the same as an activated analysis that doesn't know anything. For example:

analyzer/src/analyses/threadFlag.ml

Lines 9 to 14 in 4feae9f

	let is_multi (ask: Queries.ask): bool =
	if !GU.global_initialization then false else
	match ask Queries.MustBeSingleThreaded with
	| `MustBool x -> not x
	| `Top -> true
	| _ -> failwith "ThreadFlag.is_multi"

Currently the possible query results are these:

analyzer/src/domains/queries.ml

Lines 72 to 84 in 4feae9f

	type result = [
	| `Top
	| `Int of ID.t
	| `Str of string
	| `LvalSet of LS.t
	| `ExprSet of ES.t
	| `ExpTriples of PS.t
	| `TypeSet of TS.t
	| `Varinfo of VI.t
	| `MustBool of bool (* true \leq false *)
	| `MayBool of bool (* false \leq true *)
	| `PartAccessResult of PartAccessResult.t
	| `Bot

Most of them should be complete lattices already. I think only the Str case would need to be changed to be a flat lattice of strings.

[sim642]

Fueled by my thoughts on the topic, I tried to start doing this on query-gadt branch but it's not as beautiful as one would hope. I tried the simplest possible thing: making Queries.t a GADT that contains the intended result type, but without making actual use of it.

Currently the type Queries.ask is:

analyzer/src/domains/queries.ml

Line 87 in 11dcafd

type ask = t -> result

The (initially) desired type would be:

type ask = type a. a t -> result

Unfortunately this isn't allowed in OCaml because it's second-order polymorphism: https://ocaml.org/releases/4.12/htmlman/polymorphism.html#s%3Ahigher-rank-poly. The suggested workaround suggested there is the following:

analyzer/src/domains/queries.ml

Line 89 in c05e792

type ask = { f: 'a. 'a t -> result }

It technically works but is extremely inconvenient to use, because you must always access the single record field to make a query and define a record with a single field as the transfer function query. (It's the same kind of workaround used by IntDomTuple.)

---

I'm starting to think this extra type safety isn't worth it if it makes the code much uglier. It'd be much easier to just add a comment for each query about which result it returns.

[vogler]

Can't you move it into the existing ctx record?

analyzer/src/framework/analyses.ml

Lines 379 to 380 in 148ddba

	type ('d,'g,'c) ctx =
	{ ask : Queries.ask

From

ask : Queries.t -> Queries.Result.t

to

ask : 'a. 'a Queries.t -> Queries.Result.t

[sim642]

I considered it and that should be workable, but we have lots of helper functions that are based on taking Queries.ask as argument instead of the entire ctx. Of course that can be changed to match but the existing practice has been to avoid relying on ctx if just ask suffices.

It doesn't solve the other side though: implementations of query would still need to return such a singleton record, so it would still need to exist (and we don't want query having to return a ctx...) and have extra conversion between the two.

[vogler]

I just tried to change it, but then gave up at some point since there were so many type annotations to remove.
Noticed the following:

File "src/cdomains/arrayDomain.ml", line 269, characters 32-106:
269 |                       match ask (Q.MayBeLess (exp, Cil.kinteger64 Cil.IInt (IntOps.BigIntOps.to_int64 i))) with
                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type bool Q.t
       but an expression was expected of type int64 Q.t
       Type bool is not compatible with type int64

I considered it and that should be workable, but we have lots of helper functions that are based on taking Queries.ask as argument instead of the entire ctx. Of course that can be changed to match but the existing practice has been to avoid relying on ctx if just ask suffices.

Yea, not that great. However, a lot of them don't even use the ask argument (annotated 'a Queries.ask) or only use it for one type of query (annotated the type they use).

It doesn't solve the other side though: implementations of query would still need to return such a singleton record, so it would still need to exist (and we don't want query having to return a ctx...) and have extra conversion between the two.

Why? The only problem should be passing ask and using it polymorphically.
query has has no second-order polymorphism (besides ctx.ask), so you just do:

let query ctx = function ...

and once the result type depends on the query

let query ctx (type a) (q: a Queries.t) : a = ...

[sim642]

Noticed the following:

File "src/cdomains/arrayDomain.ml", line 269, characters 32-106:
269 |                       match ask (Q.MayBeLess (exp, Cil.kinteger64 Cil.IInt (IntOps.BigIntOps.to_int64 i))) with
                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type bool Q.t
       but an expression was expected of type int64 Q.t
       Type bool is not compatible with type int64

This is exactly what happens when ask is left unannotated and type inference infers the type of ask based on its first use, which is for one type, but a following use has a different type.

Why? The only problem should be passing ask and using it polymorphically.
query has has no second-order polymorphism (besides ctx.ask)

I'll have to try at some point to be sure because there's also some difference between (type a) and an explicitly polymorphic type type a. … just for GADTs, unrelated to the second order: https://ocaml.org/releases/4.12/htmlman/gadts.html. At one point I had to change a bunch of things to use the latter to get everything to typecheck.

Also, I'm not then sure what the type of query should be in the Spec signature. By not going into second order, it would be

val query : (D.t, G.t, C.t) ctx -> 'a Queries.t -> 'a

I think the problem would be using this query, which is just first order polymorphic, to define ctx.ask, which needs to be second order polymorphic. It would be like taking the more limited ask function of type 'a Queries.t -> 'a and turning it into something of type type a. a Queries.t -> a, which would magically allow it to be used with different types, although the ask function we got from the argument would not allow that.