Open DrMichaelPetter opened 1 month ago
The _with
suffixed versions are standard in Apron and those three are far from the only ones: https://github.com/goblint/analyzer/blob/2fa4f55e682da3ad937e394fe20449eeef4c9634/src/cdomains/apron/apronDomain.apron.ml#L133-L151
It looks like ApronDomain
was oddly split into RelationDomain
and SharedFunctions
.
Oh, ok. Discussions with @michael-schwarz lead me to believe, that the _with suffix would be loaded with the semantics of having a return value but possibly mutating the original parameter via side effect in the rest of the goblint code. Did I misunderstand something or is that possibly an unlucky clash in naming conventions?
Hmm, it seems I was confused. I was under the impression that these _with
functions are still used as described in https://github.com/goblint/analyzer/pull/592 and then implemented here https://github.com/goblint/analyzer/commit/236b3876260bc3b05e7e9891cf63bfceafab1eb1.
It seems that was removed in https://github.com/goblint/analyzer/pull/592/commits/54ff8257e450075be586868be9d64abc9b11b74c.
@sim642: Do you recall why this was necessary? It seem that unnecessarily ties us to only having imperative implementations whereas the old setting allowed us to have both pure and imperative things in the same framework...
val remove_vars_with : t -> var list -> unit
val remove_filter_with: t -> (var -> bool) -> unit
val assign_var_parallel_with : t -> (var * var) list -> unit
these are the only _with
functions exposed. If we replace them with their pt_with
equivalent, we could get rid of
type t = {
mutable d : RelDomain.t option;
mutable env : Environment.t
}
[@@deriving eq, ord, hash]
these being mutable in sharedFunctions.
@sim642: Do you recall why this was necessary? It seem that unnecessarily ties us to only having imperative implementations whereas the old setting allowed us to have both pure and imperative things in the same framework...
It really doesn't. It's just that existing relational domains were implemented with these imperative functions available, mainly because Apron exposes them to avoid unnecessary copying of C stuff that are inherently imperative under the hood and don't enjoy sharing like immutable OCaml values can.
Currently there's a functor to lift imperative versions of these domains to functional ones: that's what we do with Apron domains. But the converse lifting is also possible: that's what I did in #1339 to use immutable OCaml sets for the relation analysis domain. So it's perfectly possible to just implement an immutable relational domain and use it in the existing relation analysis. I don't know whether the non-Apron relational domains actually exploit mutability to reduce copying. The Apron ones do, so there's no reason not to benefit from that. If the others don't, then the lifting could be extracted from #1339 and reused generally. Mutability is just an implementation detail.
I think the pt_with
stuff was subtly flawed at the API consumer side. It was easy to fit both imperative and functional implementations to the API implementation side, but the abstraction doesn't fully hide the implementation. For example, there were definitions like let copy_pt t = t
, which are a bit dubious because what's the intended specification of copy
? If it's allowed to return the argument unchanged, then the consumer cannot really be sure what they are allowed to do with the "copy". To ensure a physically distinct value, you'd need to forcefully copy memory which you would expect to just share if nothing downstream modifies it.
In fact, to ensure that manipulating the returned value from copy_pt
cannot influence anything else, it's not just sufficient to return something physically distinct. Not only does the outermost value need to be unshared (shallow copy), but everything within must be unshared (deep copy).
I think a specific example where this didn't properly work might be this: https://github.com/goblint/analyzer/blob/2fa4f55e682da3ad937e394fe20449eeef4c9634/src/analyses/apron/relationAnalysis.apron.ml#L444-L457
Depending on the match
, unify_st'
may be already copied (from assign_to_global_wrapper
) or shared with something else. Or in the else
case, even unify_st
is not modified. Having to reason here about the may-or-may-not-mutate aspect of assign_to_global_wrapper
and remove_vars
is very error-prone.
The least confusing way is to use these domains through a proven interface that Apron has, where it's explicit in the operation name, what happens or doesn't happen. And lifting immutable domains to it is just as straightforward as the other way around, without the need for this extra complication at the analysis writing level. Everything is just fully abstracted away in a type-safe way.
If we replace them with their
pt_with
equivalent, we could get rid oftype t = { mutable d : RelDomain.t option; mutable env : Environment.t } [@@deriving eq, ord, hash]
these being mutable in sharedFunctions.
Those fields being mutable is not the whole story for affine equalities. Vectors and matrices within RelDomain
are still mutable because they're OCaml array
s, so that isn't enough. To make things really pure, those arrays would also have to get copied in a lot more places.
I added some documentation to the three _with
functions in 4762ced25427035e9b5a1a0bf172067905338169.
During #1412 we encountered several legacy problems in the current state of relational analysis, in
relationDomain.apron.ml
andsharedFunctions.apron.ml
to be taken care of in some PR:relationDomain.apron.ml
moduleS2
defines_with
suffixed functions withunit
return type. The semantics are undocumented and the_with
convention is not consistent with the rest of the project. -> clarified in commentsIn
sharedFunctions.apron.ml
we findVarManagementOps.change_d
, which is called whenever variable environment changes, maybe following apron specification? However, this function is again undocumented and~add
and~del
is neither documented nor clear what it doeschange_d
itself callsEnvironment.dimchange
, computing change records (in add_dimensions format) for both situations, whether an environment grows or shrinks. This leads to a violation in the apron API where there are different format specified for growing and shrinking cases. Further down the pipeline inaffineEqualityDomain.apron.ml
, this change structure is then postprocessed in both cases to now comply to remove_dimensions format indim_remove
as well asdim_add
. This is extremely confusing for future maintenance and extension of the framework. Since the change_d part of this is shared with linear-two-variables, linear-two-variables currently have to reformat these change records, which seems odd at best.A solution to this would be to rewrite the
change_d
confusion in one PR, and to sort out desired behaviour for the_with
functions.