@@ -1391,6 +1391,113 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
1391
1391
return {RangeFactory, ValueFactory.getValue (Min), ValueFactory.getValue (Max)};
1392
1392
}
1393
1393
1394
+ // ===----------------------------------------------------------------------===//
1395
+ // Constraint manager implementation details
1396
+ // ===----------------------------------------------------------------------===//
1397
+
1398
+ class RangeConstraintManager : public RangedConstraintManager {
1399
+ public:
1400
+ RangeConstraintManager (ExprEngine *EE, SValBuilder &SVB)
1401
+ : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
1402
+
1403
+ // ===------------------------------------------------------------------===//
1404
+ // Implementation for interface from ConstraintManager.
1405
+ // ===------------------------------------------------------------------===//
1406
+
1407
+ bool haveEqualConstraints (ProgramStateRef S1,
1408
+ ProgramStateRef S2) const override {
1409
+ // NOTE: ClassMembers are as simple as back pointers for ClassMap,
1410
+ // so comparing constraint ranges and class maps should be
1411
+ // sufficient.
1412
+ return S1->get <ConstraintRange>() == S2->get <ConstraintRange>() &&
1413
+ S1->get <ClassMap>() == S2->get <ClassMap>();
1414
+ }
1415
+
1416
+ bool canReasonAbout (SVal X) const override ;
1417
+
1418
+ ConditionTruthVal checkNull (ProgramStateRef State, SymbolRef Sym) override ;
1419
+
1420
+ const llvm::APSInt *getSymVal (ProgramStateRef State,
1421
+ SymbolRef Sym) const override ;
1422
+
1423
+ ProgramStateRef removeDeadBindings (ProgramStateRef State,
1424
+ SymbolReaper &SymReaper) override ;
1425
+
1426
+ void printJson (raw_ostream &Out, ProgramStateRef State, const char *NL = " \n " ,
1427
+ unsigned int Space = 0 , bool IsDot = false ) const override ;
1428
+ void printConstraints (raw_ostream &Out, ProgramStateRef State,
1429
+ const char *NL = " \n " , unsigned int Space = 0 ,
1430
+ bool IsDot = false ) const ;
1431
+ void printEquivalenceClasses (raw_ostream &Out, ProgramStateRef State,
1432
+ const char *NL = " \n " , unsigned int Space = 0 ,
1433
+ bool IsDot = false ) const ;
1434
+ void printDisequalities (raw_ostream &Out, ProgramStateRef State,
1435
+ const char *NL = " \n " , unsigned int Space = 0 ,
1436
+ bool IsDot = false ) const ;
1437
+
1438
+ // ===------------------------------------------------------------------===//
1439
+ // Implementation for interface from RangedConstraintManager.
1440
+ // ===------------------------------------------------------------------===//
1441
+
1442
+ ProgramStateRef assumeSymNE (ProgramStateRef State, SymbolRef Sym,
1443
+ const llvm::APSInt &V,
1444
+ const llvm::APSInt &Adjustment) override ;
1445
+
1446
+ ProgramStateRef assumeSymEQ (ProgramStateRef State, SymbolRef Sym,
1447
+ const llvm::APSInt &V,
1448
+ const llvm::APSInt &Adjustment) override ;
1449
+
1450
+ ProgramStateRef assumeSymLT (ProgramStateRef State, SymbolRef Sym,
1451
+ const llvm::APSInt &V,
1452
+ const llvm::APSInt &Adjustment) override ;
1453
+
1454
+ ProgramStateRef assumeSymGT (ProgramStateRef State, SymbolRef Sym,
1455
+ const llvm::APSInt &V,
1456
+ const llvm::APSInt &Adjustment) override ;
1457
+
1458
+ ProgramStateRef assumeSymLE (ProgramStateRef State, SymbolRef Sym,
1459
+ const llvm::APSInt &V,
1460
+ const llvm::APSInt &Adjustment) override ;
1461
+
1462
+ ProgramStateRef assumeSymGE (ProgramStateRef State, SymbolRef Sym,
1463
+ const llvm::APSInt &V,
1464
+ const llvm::APSInt &Adjustment) override ;
1465
+
1466
+ ProgramStateRef assumeSymWithinInclusiveRange (
1467
+ ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1468
+ const llvm::APSInt &To, const llvm::APSInt &Adjustment) override ;
1469
+
1470
+ ProgramStateRef assumeSymOutsideInclusiveRange (
1471
+ ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1472
+ const llvm::APSInt &To, const llvm::APSInt &Adjustment) override ;
1473
+
1474
+ private:
1475
+ RangeSet::Factory F;
1476
+
1477
+ RangeSet getRange (ProgramStateRef State, SymbolRef Sym);
1478
+ RangeSet getRange (ProgramStateRef State, EquivalenceClass Class);
1479
+ ProgramStateRef setRange (ProgramStateRef State, SymbolRef Sym,
1480
+ RangeSet Range);
1481
+ ProgramStateRef setRange (ProgramStateRef State, EquivalenceClass Class,
1482
+ RangeSet Range);
1483
+
1484
+ RangeSet getSymLTRange (ProgramStateRef St, SymbolRef Sym,
1485
+ const llvm::APSInt &Int,
1486
+ const llvm::APSInt &Adjustment);
1487
+ RangeSet getSymGTRange (ProgramStateRef St, SymbolRef Sym,
1488
+ const llvm::APSInt &Int,
1489
+ const llvm::APSInt &Adjustment);
1490
+ RangeSet getSymLERange (ProgramStateRef St, SymbolRef Sym,
1491
+ const llvm::APSInt &Int,
1492
+ const llvm::APSInt &Adjustment);
1493
+ RangeSet getSymLERange (llvm::function_ref<RangeSet()> RS,
1494
+ const llvm::APSInt &Int,
1495
+ const llvm::APSInt &Adjustment);
1496
+ RangeSet getSymGERange (ProgramStateRef St, SymbolRef Sym,
1497
+ const llvm::APSInt &Int,
1498
+ const llvm::APSInt &Adjustment);
1499
+ };
1500
+
1394
1501
// ===----------------------------------------------------------------------===//
1395
1502
// Constraint assignment logic
1396
1503
// ===----------------------------------------------------------------------===//
@@ -1593,112 +1700,6 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
1593
1700
RangeSet::Factory &RangeFactory;
1594
1701
};
1595
1702
1596
- // ===----------------------------------------------------------------------===//
1597
- // Constraint manager implementation details
1598
- // ===----------------------------------------------------------------------===//
1599
-
1600
- class RangeConstraintManager : public RangedConstraintManager {
1601
- public:
1602
- RangeConstraintManager (ExprEngine *EE, SValBuilder &SVB)
1603
- : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
1604
-
1605
- // ===------------------------------------------------------------------===//
1606
- // Implementation for interface from ConstraintManager.
1607
- // ===------------------------------------------------------------------===//
1608
-
1609
- bool haveEqualConstraints (ProgramStateRef S1,
1610
- ProgramStateRef S2) const override {
1611
- // NOTE: ClassMembers are as simple as back pointers for ClassMap,
1612
- // so comparing constraint ranges and class maps should be
1613
- // sufficient.
1614
- return S1->get <ConstraintRange>() == S2->get <ConstraintRange>() &&
1615
- S1->get <ClassMap>() == S2->get <ClassMap>();
1616
- }
1617
-
1618
- bool canReasonAbout (SVal X) const override ;
1619
-
1620
- ConditionTruthVal checkNull (ProgramStateRef State, SymbolRef Sym) override ;
1621
-
1622
- const llvm::APSInt *getSymVal (ProgramStateRef State,
1623
- SymbolRef Sym) const override ;
1624
-
1625
- ProgramStateRef removeDeadBindings (ProgramStateRef State,
1626
- SymbolReaper &SymReaper) override ;
1627
-
1628
- void printJson (raw_ostream &Out, ProgramStateRef State, const char *NL = " \n " ,
1629
- unsigned int Space = 0 , bool IsDot = false ) const override ;
1630
- void printConstraints (raw_ostream &Out, ProgramStateRef State,
1631
- const char *NL = " \n " , unsigned int Space = 0 ,
1632
- bool IsDot = false ) const ;
1633
- void printEquivalenceClasses (raw_ostream &Out, ProgramStateRef State,
1634
- const char *NL = " \n " , unsigned int Space = 0 ,
1635
- bool IsDot = false ) const ;
1636
- void printDisequalities (raw_ostream &Out, ProgramStateRef State,
1637
- const char *NL = " \n " , unsigned int Space = 0 ,
1638
- bool IsDot = false ) const ;
1639
-
1640
- // ===------------------------------------------------------------------===//
1641
- // Implementation for interface from RangedConstraintManager.
1642
- // ===------------------------------------------------------------------===//
1643
-
1644
- ProgramStateRef assumeSymNE (ProgramStateRef State, SymbolRef Sym,
1645
- const llvm::APSInt &V,
1646
- const llvm::APSInt &Adjustment) override ;
1647
-
1648
- ProgramStateRef assumeSymEQ (ProgramStateRef State, SymbolRef Sym,
1649
- const llvm::APSInt &V,
1650
- const llvm::APSInt &Adjustment) override ;
1651
-
1652
- ProgramStateRef assumeSymLT (ProgramStateRef State, SymbolRef Sym,
1653
- const llvm::APSInt &V,
1654
- const llvm::APSInt &Adjustment) override ;
1655
-
1656
- ProgramStateRef assumeSymGT (ProgramStateRef State, SymbolRef Sym,
1657
- const llvm::APSInt &V,
1658
- const llvm::APSInt &Adjustment) override ;
1659
-
1660
- ProgramStateRef assumeSymLE (ProgramStateRef State, SymbolRef Sym,
1661
- const llvm::APSInt &V,
1662
- const llvm::APSInt &Adjustment) override ;
1663
-
1664
- ProgramStateRef assumeSymGE (ProgramStateRef State, SymbolRef Sym,
1665
- const llvm::APSInt &V,
1666
- const llvm::APSInt &Adjustment) override ;
1667
-
1668
- ProgramStateRef assumeSymWithinInclusiveRange (
1669
- ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1670
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) override ;
1671
-
1672
- ProgramStateRef assumeSymOutsideInclusiveRange (
1673
- ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1674
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) override ;
1675
-
1676
- private:
1677
- RangeSet::Factory F;
1678
-
1679
- RangeSet getRange (ProgramStateRef State, SymbolRef Sym);
1680
- RangeSet getRange (ProgramStateRef State, EquivalenceClass Class);
1681
- ProgramStateRef setRange (ProgramStateRef State, SymbolRef Sym,
1682
- RangeSet Range);
1683
- ProgramStateRef setRange (ProgramStateRef State, EquivalenceClass Class,
1684
- RangeSet Range);
1685
-
1686
- RangeSet getSymLTRange (ProgramStateRef St, SymbolRef Sym,
1687
- const llvm::APSInt &Int,
1688
- const llvm::APSInt &Adjustment);
1689
- RangeSet getSymGTRange (ProgramStateRef St, SymbolRef Sym,
1690
- const llvm::APSInt &Int,
1691
- const llvm::APSInt &Adjustment);
1692
- RangeSet getSymLERange (ProgramStateRef St, SymbolRef Sym,
1693
- const llvm::APSInt &Int,
1694
- const llvm::APSInt &Adjustment);
1695
- RangeSet getSymLERange (llvm::function_ref<RangeSet()> RS,
1696
- const llvm::APSInt &Int,
1697
- const llvm::APSInt &Adjustment);
1698
- RangeSet getSymGERange (ProgramStateRef St, SymbolRef Sym,
1699
- const llvm::APSInt &Int,
1700
- const llvm::APSInt &Adjustment);
1701
- };
1702
1703
1703
1704
bool ConstraintAssignor::assignSymExprToConst (const SymExpr *Sym,
1704
1705
const llvm::APSInt &Constraint) {
0 commit comments