Allow serialization and deserialization of Apron Analysis results for precision comparison

[jerhard]

The serialization of results of the Apron analysis currently fails with execption: Fatal error: exception Invalid_argument("output_value: abstract value (Custom)").

This needs to be fixed for the incremental analysis and for comparing different runs with the Apron analysis.

Edit: For now we only need to focus on allowing a comparison.

[sim642]

I'm doubtful about how fixable this really is because Apron defines custom OCaml runtime object types in C, where the (de)serialization functions must also be defined. And that for all Apron's data structures, probably including its own GMP and MPFR bindings. This would be an Apron fork...

For just comparison it would be a lot simpler to export the constraints textually and implement their comparison in a separate program, a la privPrecCompare. Apron also includes a parser for the expressions/constraints it prints: https://antoinemine.github.io/Apron/doc/api/ocaml/Parser.html.

[jerhard]

In the Apron documentation some Funid_serialize_raw and Funid_deserialize_raw constructor values are mentioned. It's not really clear what behavior is already implemented and how to use the corresponding functions.

[michael-schwarz]

This might also be relevant, it allows for the serialization of an Abstract1:
http://apron.cri.ensmp.fr/library/0.9.10/apron/apron_91.html#SEC127

[sim642]

Serialization is implemented for some data structures:
https://github.com/antoinemine/apron/blob/c852ebcc89e5cf4a5a3318e7c13c73e1756abb11/mlapronidl/apron_caml.c#L348-L349
But not others: https://github.com/antoinemine/apron/blob/c852ebcc89e5cf4a5a3318e7c13c73e1756abb11/mlapronidl/apron_caml.c#L406-L407.

The functions you have linked are probably ones that need to be manually called, but that would be separate from OCaml's marshaling.

[sim642]

But there's this set_deserialize function: https://antoinemine.github.io/Apron/doc/api/ocaml/Manager.html#VALset_deserialize. Maybe that does something, although there isn't one for serialization.

There seem to be fdump functions in modules, so maybe that's the dual.

[jerhard]

There seem to be fdump functions in modules, so maybe that's the dual.

This fdump for Abstract0 and Abstract1 dumps the internal representation to standard out. So it doesn't seem to be something that we could use for serialization.

Looking at the C-implementation of Abtract1, the deserialize also seems to be only a dummy implementation yieliding top. For Abstract0, there seems to be a more meaningful implementation. But this serialization and deserialization are not exposed in the OCaml API.

@sim642 Would the serialization / deserialization of this Abstract0 already suffice for our purposes? If so, the best thing might be to ask the Apron maintainers why serilazation/deserialization is not exposed to the OCaml API. If there are bigger problems with it, we would have to think about some alternative way to compare these Apron domains, as suggested #423 (comment).

[jerhard]

But there's this set_deserialize function: https://antoinemine.github.io/Apron/doc/api/ocaml/Manager.html#VALset_deserialize. Maybe that does something, although there isn't one for serialization.

This set_deserialize sets some manager for deserialization, but this is only a prerequesite for the deserialization to work.

[sim642]

But doesn't marshalling work directly on Abstract0.t then? It would already be of great benefit because Abstract1.t is just that and an Environment.t, which would also need to be (de)serialized.

If we're going to use a special-purpose (de)serialization for the comparison, then it shouldn't be too difficult to have custom logic for environments. If we want marshaling to work in entirety, it'd have to be implemented in C for environments (and then it should also be easy for Abstract1).

[jerhard]

I tested serialization of Abstract0.t, and it indeed works for octagons, albeit not for polyhedra and intervals.
For the latter two, it gives the following error:

Fatal error: exception Apron.Manager.Error
 {  exn = Exc_not_implemented; funid = Funid_serialize_raw; msg = ; }

But serializing octagons should suffice -- we would translate the intervals to octagons before serialization.

[jerhard]

Marshalling/Unmarshalling now also works for Man.mt A.t, i.e. Abstract0.t together with an environment, where for the environment a string based representation is used, and as long the Octagons are used as the Apron domain. See here.

Now one would have to serialize all abstract values using this mechanism. One option would be to add a marshal function to the analyses, which then could used by Analyses.FromSpec and ultimately Control. Any other ideas?

[sim642]

Now one would have to serialize all abstract values using this mechanism. One option would be to add a marshal function to the analyses, which then could used by Analyses.FromSpec and ultimately Control. Any other ideas?

Adding new transfer function for everything just to have some Apron-specific marshaling is quite ugly.

I think it'd be easier to add a hack into sync of apron analysis, which during postsolving just puts things into its own hashtable and in finalize writes it to a file. Kind of like how privPrecCompare does it.

This would only do locals though. For globals it might be necessary to extract a part of the WarnGlobal query from #397, which makes it possible to do postprocessing (add to hashtable) on the final values of globals as well.

The other question is what will actually get compared: only box vs oct of a fixed privatization or also between privatizations? Because the latter would have different domains.

I'm not sure if it's possible to do anything in read_global like for base priv. Maybe one could record the resulting local relations after all read_global calls? Those still return relations which should contain everything else as well. And it'd be a privatization-independent mechanism. Unless the local states end up differing somehow else.

[jerhard]

I think it'd be easier to add a hack into sync of apron analysis, which during postsolving just puts things into its own hashtable and in finalize writes it to a file. Kind of like how privPrecCompare does it.

If one were to create a hashmap node * C.t -> D.t the results would not be split with regards to the contexts of the other analyses, right? But probably the comparison has to be performed in join-over-all-contexts manner, anyway.

[sim642]

If one were to create a hashmap node * C.t -> D.t the results would not be split with regards to the contexts of the other analyses, right? But probably the comparison has to be performed in join-over-all contexts manner, anyway.

That's true. The contexts, which might contain relations themselves, would be different and possibly incomparable anyway.
PrivPrecCompare for base also joined all contexts.

[jerhard]

I am working on creating a version of privPrecCompare that works for the Apron analysis, with as much code reuse of privPrecCompare as possible. @sim642 Is there a specific reason why privPrecCompare is using CilType.Location instead of Node?

[sim642]

I'm not exactly sure anymore. I guess we just wanted it to be as independent from our internal structures as possible. I suppose it could happen that CIL does its transformations and creates auxiliary nodes that all correspond to the same statement in the program (e.g. ternary operator, short-circuiting logic).