[analyzer][solver] Track symbol equivalence
Summary: For the most cases, we try to reason about symbol either based on the information we know about that symbol in particular or about its composite parts. This is faster and eliminates costly brute force searches through existing constraints. However, we do want to support some cases that are widespread enough and involve reasoning about different existing constraints at once. These include: * resoning about 'a - b' based on what we know about 'b - a' * reasoning about 'a <= b' based on what we know about 'a > b' or 'a < b' This commit expands on that part by tracking symbols known to be equal while still avoiding brute force searches. It changes the way we track constraints for individual symbols. If we know for a fact that 'a == b' then there is no need in tracking constraints for both 'a' and 'b' especially if these constraints are different. This additional relationship makes dead/live logic for constraints harder as we want to maintain as much information on the equivalence class as possible, but we still won't carry the information that we don't need anymore. Differential Revision: https://reviews.llvm.org/D82445
Loading
Please sign in to comment