analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Housekeeping relational analyses

Open DrMichaelPetter opened this issue 3 months ago • 8 comments

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:

  • [x] 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.

DrMichaelPetter avatar May 06 '24 14:05 DrMichaelPetter