caballa
commented
11 months ago The main difference in terms of functionality is that the implementation of the TOPLAS paper implemented bitwise operations and the Crab's one does not. However, porting the code should be pretty easy.
About the operations that you see as not implemented. That's not a limitation. In crab, different domains can implement different operations. The idea is that a combination of domains will implement all of the required operations. The wrapped interval domain is a numerical domain so it doesn't implement boolean, array, or pointer operations. These operations are implemented by other domains such as
All these operations should be sound on machine arithmetic because they can only call abstract domain's operations so if the abstract domain is sound then the boolean/array/pointer domains should be sound. You can look at Clam on how complex abstract domains are built from simpler ones. See for instance, how Clam builds an abstract domain based on intervals that can support boolean operations and pointers (https://github.com/seahorn/clam/blob/master/lib/Clam/crab/domains/intervals.hh).
Finally, let's talk about the issue you mentioned about comparisons. This is the actual weakness of the current implementation. The wrapped interval domain is, in general, unsound because it uses (as you pointed out) linear constraints that can be normalized and those transformations are not sound on machine arithmetic. In fact, there is an issue talking exactly about that and proposing the solution https://github.com/seahorn/crab/issues/40
What is your goal? Fixing this has been on my TODO list for long time but it never blocked me so that's why I have been postpone it. I could help with this but I want to know what you want to do with Crab first.
ghost
I noticed that these operations are not implemented in crab's wrapped_interval:
/// wrapped_interval_domain implements only standard abstract /// operations of a numerical domain so it is intended to be used as /// a leaf domain in the hierarchy of domains. BOOL_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t) ARRAY_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t) REGION_AND_REFERENCE_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t) DEFAULT_SELECT(wrapped_interval_domain_t)
Can this implementation retain the ideas of the TOPLAS15 paper?
For example, to handle branch condition like s < t, the paper update s and t respectively. But, in crab, we may transform this condition to a linear constraint s - t < 0, and solve this? Does this handling method safe in machine integer operation semantics?
I'm not very familiar with crab.