From: Chao Wang (chaowang_at_nec-labs.com)
Date: Mon Oct 15 2007 - 07:45:55 MDT
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:01:59 MDT