From: William Hung (william_hung_at_alumni.utexas.net)
Date: Mon Oct 15 2007 - 08:42:48 MDT
Thanks for your prompt clarification.
Yes, I must have misunderstood the array package documentation in the middle
of the night.
William
On 10/15/07, Chao Wang <chaowang_at_nec-labs.com> wrote:
>
> Dear William,
>
> Thanks for your email on a potential problem of GRAB source code. I am
> the author of the original GRAB package. According to my understanding,
> the code segment you've highlighted, in particular the function
> "array_insert()", is not a bug. Note that "array_insert(int, clause, 0,
> ...)" is similar to "clause[0]=..."; in other words each time we are
> overwriting the first (and only) element of the array. If one wants to
> append an element to the array, then "array_insert_last()" can be used
> instead. Having said that, I think your modification is also correct
> (and perhaps is more readable), although inside the loop it keeps doing
> malloc/free of the array (which could be improved).
>
> Chao
>
>
> William Hung wrote:
>
> > ---------- Forwarded message ----------
> > From: *William Hung* <william_hung_at_alumni.utexas.net
> > <mailto:william_hung_at_alumni.utexas.net>>
> > Date: Oct 14, 2007 10:08 PM
> > Subject: Logic bug in the VIS GRAB package?
> > To: chaowang_at_nec-labs.com <mailto:chaowang_at_nec-labs.com>
> >
> > Hi,
> >
> > I am reviewing the source code of VIS, in particular the GRAB package,
> > which seem to report good verification results for some cases.
> >
> > However, it seems there may be a logic bug in the SAT-based
> > counter-example generation routine for the GRAB package.
> >
> > In the file grabBMC.c lines 135-165, you have:
> >
> > 135 /* Generate the constraints from the abstract paths
> > 136 * (1) build a bAigEdge_t (graph) for each ring
> > 137 * (2) add all the cnf clauses that describe this graph
> > 138 * (3) make the output bAigEdge_t equals to 1
> > 139 */
> > 140 {
> > 141 bAigEdge_t bAigState;
> > 142 mdd_manager *mddManager =
> Ntk_NetworkReadMddManager(network);
> > * 143 array_t *clause = array_alloc(int, 1);
> > * 144 mdd_t *ring;
> > 145
> > 146 arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
> > 147 st_table *bddidTobAigNames;
> > 148 bddidTobAigNames =
> > GrabBddGetSupportBaigNames(mddManager, ring);
> > 149 bAigState = GrabConvertBddToBaig(maigManager, ring,
> > bddidTobAigNames);
> > 150 {
> > 151 st_generator *stgen;
> > 152 long tmpId;
> > 153 char *tmpStr;
> > 154 st_foreach_item(bddidTobAigNames, stgen, &tmpId,
> > &tmpStr) {
> > 155 FREE(tmpStr);
> > 156 }
> > 157 st_free_table(bddidTobAigNames);
> > 158 }
> > * 159 array_insert(int, clause, 0,
> > BmcGenerateCnfFormulaForAigFunction(
> > 160 maigManager, bAigState, i,
> > cnfClauses));
> > 161 BmcCnfInsertClause(cnfClauses, clause);
> > * 162 }
> > 163
> > * 164 array_free(clause);
> > * 165 }
> >
> > I have highlighted the problematic lines in red color above.
> >
> > It seems that for each ring, you want to use the "bAigState" of the
> > ring to generate a "clause", and insert this "clause" into your
> > collection of "cnfClauses". However, you did not cleanup the clause
> > (integer array) after the insertion. So for the next ring, you seem to
> > append (or prepend) the bAigState of the next ring to the same
> > "clause", which seems to be the logical disjunction "OR" of both
> > rings. You will then insert this disjunction clause into your
> > collection of "cnfClauses". This scenario will go on for the rest of
> > the rings.
> >
> > Would you please take a look at the code and see if my analysis is
> > correct or not?
> >
> > If my analysis is correct, a simple fix for the above code would be:
> >
> > /* Generate the constraints from the abstract paths
> > * (1) build a bAigEdge_t (graph) for each ring
> > * (2) add all the cnf clauses that describe this graph
> > * (3) make the output bAigEdge_t equals to 1
> > */
> > {
> > bAigEdge_t bAigState;
> > mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
> > * array_t *clause;
> > * mdd_t *ring;
> >
> > arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
> > st_table *bddidTobAigNames;
> > bddidTobAigNames = GrabBddGetSupportBaigNames(mddManager, ring);
> > bAigState = GrabConvertBddToBaig(maigManager, ring,
> > bddidTobAigNames);
> > {
> > st_generator *stgen;
> > long tmpId;
> > char *tmpStr;
> > st_foreach_item(bddidTobAigNames, stgen, &tmpId, &tmpStr) {
> > FREE(tmpStr);
> > }
> > st_free_table(bddidTobAigNames);
> > }
> > * clause = array_alloc(int, 1);
> > * array_insert(int, clause, 0, BmcGenerateCnfFormulaForAigFunction(
> > maigManager, bAigState, i,
> > cnfClauses));
> > BmcCnfInsertClause(cnfClauses, clause);
> > * array_free(clause);
> > * }
> > }
> >
> > I have highlighted my changes in red color in the above listing.
> >
> > Please let me know whether my analysis is correct or not, and if so,
> > what do you think about the code fix.
> >
> > Thanks
> >
> > William Hung
> >
> > E-mail: william_hung_at_alumni.utexas.net
> > <mailto:william_hung_at_alumni.utexas.net>
> >
> >
> >
>
>
> --
> Chao Wang, Ph.D. Email: chaowang_at_nec-labs.com
> Research Staff Member
> NEC Laboratories America
> 4 Independence Way, Suite 200 Phone: +1 609 951-2814
> Princeton, NJ 08540, U.S.A. Fax: +1 609 951-2499
>
>
This archive was generated by hypermail 2.1.7 : Mon Oct 15 2007 - 08:50:09 MDT