tclbdd

Check-in [56cfd0fd3f]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fix problem where a bead pointer was kept across a possible realloc leading to a read of freed memory
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:56cfd0fd3fb5deeb5cee64f6f4064fa4ac018df9
User & Date: kbk 2013-12-21 00:47:24
Context
2013-12-21
01:21
Made example code quieter. check-in: 28643a8e70 user: kbk tags: trunk
00:47
Fix problem where a bead pointer was kept across a possible realloc leading to a read of freed memory check-in: 56cfd0fd3f user: kbk tags: trunk
2013-12-20
21:45
Add test case for projecting away a nowhere-used variable. check-in: e4346a7b93 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1676
1677
1678
1679
1680
1681
1682



1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694



1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
    BDD_BeadIndex h;		/* High transition of the result */
    BDD_BeadIndex r;		/* Return value */
    int newFlag;		/* Flag == 1 iff the result was not cached */
    BDD_Quantifier q = sysPtr->quantifier;
				/* Quantifier to apply */
    Tcl_HashEntry* entryPtr;	/* Pointer to the hash entry for
				 * a cached result */




    /* Check for a cached result */
    entryPtr = Tcl_CreateHashEntry(&(sysPtr->quantifyCache),
				   (ClientData) u, &newFlag);
    if (!newFlag) {
	r = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
	++sysPtr->beads[r].refCount;
	return r;
    }

    for (;;) {
	Bead* beadPtr = sysPtr->beads + u;



	if (n == 0 || *v >= sysPtr->beads[0].level) {
	    /*
	     * No variables remain to quantify. Simply return the expression
	     * itself.
	     */
	    ++beadPtr->refCount;
	    r = u;
	    break;
	} else if (beadPtr->level < *v) {
	    /*
	     * The current variable in the expression is unquantified.
	     * Quantify the two subexpressions and make the result
	     */
	    l = Quantify(sysPtr, n, v, beadPtr->low);
	    h = Quantify(sysPtr, n, v, beadPtr->high);
	    r = BDD_MakeBead(sysPtr, beadPtr->level, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else if (beadPtr->level == *v) {
	    /*
	     * The current variable in the expression is quantified.
	     * Quantify the two subexpressions with respect to the
	     * remaining variables and then apply the combining operation.
	     */
	    l = Quantify(sysPtr, n-1, v+1, beadPtr->low);
	    h = Quantify(sysPtr, n-1, v+1, beadPtr->high);
	    sysPtr->applyOp = q;
	    r = Apply(sysPtr, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else {
	    /* 







>
>
>












>
>
>








|




|
|
|



|





|
|







1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
    BDD_BeadIndex h;		/* High transition of the result */
    BDD_BeadIndex r;		/* Return value */
    int newFlag;		/* Flag == 1 iff the result was not cached */
    BDD_Quantifier q = sysPtr->quantifier;
				/* Quantifier to apply */
    Tcl_HashEntry* entryPtr;	/* Pointer to the hash entry for
				 * a cached result */
    BDD_VariableIndex level;	/* Level from current bead */
    BDD_BeadIndex low;		/* Low branch from current bead */
    BDD_BeadIndex high;		/* High branch from current bead */

    /* Check for a cached result */
    entryPtr = Tcl_CreateHashEntry(&(sysPtr->quantifyCache),
				   (ClientData) u, &newFlag);
    if (!newFlag) {
	r = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
	++sysPtr->beads[r].refCount;
	return r;
    }

    for (;;) {
	Bead* beadPtr = sysPtr->beads + u;
	level = beadPtr->level;
	low = beadPtr->low;
	high = beadPtr->high;
	if (n == 0 || *v >= sysPtr->beads[0].level) {
	    /*
	     * No variables remain to quantify. Simply return the expression
	     * itself.
	     */
	    ++beadPtr->refCount;
	    r = u;
	    break;
	} else if (level < *v) {
	    /*
	     * The current variable in the expression is unquantified.
	     * Quantify the two subexpressions and make the result
	     */
	    l = Quantify(sysPtr, n, v, low);
	    h = Quantify(sysPtr, n, v, high);
	    r = BDD_MakeBead(sysPtr, level, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else if (level == *v) {
	    /*
	     * The current variable in the expression is quantified.
	     * Quantify the two subexpressions with respect to the
	     * remaining variables and then apply the combining operation.
	     */
	    l = Quantify(sysPtr, n-1, v+1, low);
	    h = Quantify(sysPtr, n-1, v+1, high);
	    sysPtr->applyOp = q;
	    r = Apply(sysPtr, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else {
	    /*