Housekeeping relational analyses

[DrMichaelPetter]

During #1412 we encountered several legacy problems in the current state of relational analysis, in relationDomain.apron.ml and sharedFunctions.apron.ml to be taken care of in some PR:

• relationDomain.apron.ml module S2 defines _with suffixed functions with unit return type. The semantics are undocumented and the _with convention is not consistent with the rest of the project. -> clarified in comments

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

In sharedFunctions.apron.ml we find VarManagementOps.change_d , which is called whenever variable environment changes, maybe following apron specification? However, this function is again undocumented and

• the purpose of named parameters ~add and ~del is neither documented nor clear what it does
• change_d itself calls Environment.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 in affineEqualityDomain.apron.ml, this change structure is then postprocessed in both cases to now comply to remove_dimensions format in dim_remove as well as dim_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.

[sim642]

The _with suffixed versions are standard in Apron and those three are far from the only ones:

analyzer/src/cdomains/apron/apronDomain.apron.ml

Lines 133 to 151 in 2fa4f55

	(** Imperative in-place environment and transfer functions. *)
	module type AOpsImperative =
	sig
	type t
	val add_vars_with : t -> Var.t list -> unit
	val remove_vars_with : t -> Var.t list -> unit
	val remove_filter_with : t -> (Var.t -> bool) -> unit
	val keep_vars_with : t -> Var.t list -> unit
	val keep_filter_with : t -> (Var.t -> bool) -> unit
	val forget_vars_with : t -> Var.t list -> unit
	val assign_exp_with : Queries.ask -> t -> Var.t -> exp -> bool Lazy.t -> unit
	val assign_exp_parallel_with : Queries.ask -> t -> (Var.t * exp) list -> bool -> unit (* TODO: why this one isn't lazy? *)
	val assign_var_with : t -> Var.t -> Var.t -> unit
	val assign_var_parallel_with : t -> (Var.t * Var.t) list -> unit
	val substitute_exp_with : Queries.ask -> t -> Var.t -> exp -> bool Lazy.t-> unit
	val substitute_exp_parallel_with :
	Queries.ask -> t -> (Var.t * exp) list -> bool Lazy.t -> unit
	val substitute_var_with : t -> Var.t -> Var.t -> unit
	end

It looks like ApronDomain was oddly split into RelationDomain and SharedFunctions.

[DrMichaelPetter]

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?

[michael-schwarz]

Hmm, it seems I was confused. I was under the impression that these _with functions are still used as described in #592 and then implemented here 236b387.

[michael-schwarz]

It seems that was removed in 54ff825.

@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...

[michael-schwarz]

  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]

@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:

analyzer/src/analyses/apron/relationAnalysis.apron.ml

Lines 444 to 457 in 2fa4f55

	if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
	let unify_st' = match r with
	| Some lv ->
	assign_to_global_wrapper (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg unify_st lv (fun st v ->
	RD.assign_var st.rel (RV.local v) RV.return
	)
	| None ->
	unify_st
	in
	RD.remove_vars_with unify_st'.rel [RV.return]; (* mutates! *)
	unify_st'
	)
	else
	unify_st

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.

[sim642]

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.

Those fields being mutable is not the whole story for affine equalities. Vectors and matrices within RelDomain are still mutable because they're OCaml arrays, so that isn't enough. To make things really pure, those arrays would also have to get copied in a lot more places.

[sim642]

I added some documentation to the three _with functions in 4762ced.

[DrMichaelPetter]

This has been adressed in #1754