analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Clean up existing must-equality analyses

Open sim642 opened this issue 3 years ago • 0 comments

In https://github.com/goblint/analyzer/pull/737#discussion_r878862538 it became even more apparent that we have multiple must-equality analyses, some of which are not in regular use:

  1. var_eq analysis is the one we regularly use, particularly together with symb_locks. Nevertheless, it contains multiple dead functions, which have been copied around. Its whole logic is messy and incomprehensible.
  2. condvars analysis describes itself as "Must equality between variables and logical expressions". We have no tests for it nor activate it in benchmarking, so it's not apparent how well it works or what it does compared to var_eq. (Is it just a more specialized and cheaper version of var_eq specifically for logical expressions?)
  3. MusteqDomain is separate from var_eq and completely unused (there's no corresponding analysis even). At some point I deduced from something, that it might have been intended (and maybe at some earlier time even used) to be used together with region analysis. At least the region analysis paper speaks about a must-equality analysis, but our region implementation makes no use of MusteqDomain nor var_eq analysis. Figuring out whether it should be used would also be part of #107.

An easy thing would be to just get rid of condvars and MusteqDomain, but without having investigated further, it's unclear if they maybe contain logic that var_eq does not. Hence, at some point it might be useful to clean up var_eq and see how the other two could integrate into it, instead of potentially duplicating something.

sim642 avatar May 23 '22 07:05 sim642