Allow incremental octagon Apron analysis

[jerhard]

Support for incremental runs with the octagon Apron analysis should be added.

Currently, when incremental.save is activated, the serialization of Apron analyses results fails, with the following error:
Fatal error: exception Invalid_argument("output_value: abstract value (Custom)")
This is due too the fact that the serialization is not natively supported in Apron for Abstract1.t values.

#433 already allowed serializing these results for comparison, but it did not solve the serialization for the incremental analysis: because in the latter, the marshaling is directly triggered by the solver, without delegating to the analyses domains to allow for special handling.

Since the octagon domain is the only domain that is serializable in Apron, we can only hope to serialize relational domains that are expressible as octagons.

[sim642]

If I remember correctly, then indeed octagon implements some serialization/deserialization for its custom OCaml memory blocks, but if that's the case, why do we still get the exception with it?

I'm not sure anymore, but maybe Environment.t or Var.t is missing serialization/deserialization in Apron? Because if that's the case, then there's not much we can do about it except patch Apron to support that. Shouldn't be that controversial though.

[jerhard]

I'm not sure anymore, but maybe Environment.t or Var.t is missing serialization/deserialization in Apron

Yes. What I did in #433 was to write marshal/unmarshal functions in OCaml that converts the Environment back and forth to serializable data structures.

A difficulty with patching this directly into the C level Apron is that the var type ap_var_t is generic in the sense that it is void *. While the default implementation uses char*, from what I get an Apron user can actually replace the actually used type and the operations on it (in some ap_var_operations_t). If we were to introduce new serialize/deserialize functions to this struct, I fear that might break compatibility.

[sim642]

Yes. What I did in #433 was to write marshal/unmarshal functions in OCaml that converts the Environment back and forth to serializable data structures.

Right, but there isn't really any way to hook into the standard marshal/unmarshal to do that other than implementing the custom operations in C.
The other alternative would be to implement such marshal/unmarshal functions for all Printable.S, but that's an insane amount of work for little gain. It's equivalent to adding yet another output format. So one might just as well marshal everything as JSON instead.

If we were to introduce new serialize/deserialize functions to this struct, I fear that might break compatibility.

I don't see any other simple way of doing that though. If the new fields are added to the end of the struct, then it should still be compatible as long as those functions aren't called (any non-default var implementations would have those pointers uninitialized). But given that so far it has been impossible to serialize vars anyway, there's no existing code that would possibly do that and break.

[jerhard]

If the new fields are added to the end of the struct, then it should still be compatible as long as those functions aren't called (any non-default var implementations would have those pointers uninitialized).

Good point!

[jerhard]

@michael-schwarz and I discussed this before – for the server mode, the marshalling is not inherently necessary, so the Apron analysis should work in the incremental server mode.

[sim642]

I think with some of the changes from #545, it should be possible to make this work quite easily in server mode, because that PR exposes solver data handling functions such that server mode can do things differently.

[sim642]

rlwrap ./regtest.sh 36 01 --enable server.enabled --enable server.reparse

now works in server mode, so this can be considered reasonably done for the time being. If there's ever interest in implementing more marshaling in C inside Apron, then that can be done for non-server-mode incremental analysis, but that's not something on our agenda I think.

Anyway, #909 and a00e2aa are probably what made it work.