Constraint-Based Thread-Modular Abstract Interpretation