Disjoint analysis and analysis filters

[N1ark]

Based on #207
Fixes #173

Long PR description because changes are a bit obscure maybe...

• Add a "disjoint" analysis, that tracks inequalities. Anytime it learns either !(a == b) or distinct(a, b, ...), it stores the inequalities. It can then reduce equalities to true/false when possible!
  To avoid its state being too large, it only stores inequalities for: values of type location, or simple variables, or concrete bitvectors; nothing else.

  Furthermore (and this should be discussed), it does a trick where if it absorbs information regarding a variable of type location, it does nos dirty those variables in the PC. In other words, it will learn e.g. |1| != |2|, and |1| and |2| won't be marked as dirty (meaning they become relevant for the next SAT check). This avoids sending a sat check everytime we create a new location to verify that all locations can in fact be distinct (since we "know" they can be).

• Add a filter : t -> Var.t -> Svalue.ty -> Svalue.t Iter.t -> Svalue.t Iter.t function to Analysis.S. It allows an analysis to filter the possible values for a variable of a given type, using its knowledge.

  This is used in the trivial model check in Bv_solver. We generate an infinite iterator of values for each type, and then filter that with the analyses. We then pick the first N possible values (currently 3), and do model checks with these values. This works a lot better than the previous method (using the variable's ID) and even just doing 2 attempts is usually a much better improvement.

  The filter of each analysis does:

  • Disjoint: if we know the variable is distinct to the iterated value, we filter it out.
  • Equality: if we know some equality for this variable, we substitute the entire iterator by a singleton iterator with that value. E.g. if we know V|1| == V|2| (and decide V|1| is cheaper than V|2|), for a filter on variable |2| we return singleton |1|. Bv_solver is then clever enough to resolve that to the same value as V|1| in the model check!
  • Interval: if we know some interval for the variable, we again substitute the entire iterator by a (non-shuffled) iterator over all valid values. The reason we override the iterator rather than filtering is because in cases where the interval is very narrow (e.g. [0; 10]), filtering means we will randomly generate numbers until we get N values that randomly fall in that range, which is insanely slow. I need to see if shuffling this iterator (requires some work) is a better heuristic!

• Re-add the AddOvf binary operator to check for overflows. We used to translate these into some comparison of the operand signs and it would just create an unnecessarily large expression, since analyses could usually not learn anything from it.

• Remove Declared_vars from Bv_solver; instead we learn the types of variables by using iter_var. Much nicer, in my opinion.

• The minimum value of a pointer in Rust is now its alignment; this helps the trivial model check a lot, since instead of starting at 1 for e.g. alignment 8, it starts at 8 and instantly finds a model :)

• Added some reductions

[giltho]

I think that one I can't just review in the car like the previous ones. I need to go a bit deeper and understand the implications of not dirtying variables.

I'm not sure that's valid because it is possible for two locations to be equal.

[N1ark]

I'm not sure that's valid because it is possible for two locations to be equal.

That's fine though? It will query whether L1 and L2 are equal, and the disjoint analysis will just add to the constraints all inequalities relating to L1 and L2.

Feel free to add a test if you want to check but I think it's sound (modulo when you reach 2^N locations and Z3 would tell u they can't all be distinct)