Local configuration in scripts/Makefile.local

[Khoo Yit Phang]

Hi,

I noticed the recent check-ins that mistakenly modify Makefile.common; let me suggest a change to scripts/Makefile.common to optionally load scripts/Makefile.local for local configurations:

https://bitbucket.org/khooyp/stp-khooyp/src/f1972c763806/makefile-local

I'll check it in if that sounds good.

Yit
January 10, 2012

[Trevor Hansen]

Yes Yit, Please apply that. Are you working on other patches too?

Trev.

---

From: Khoo Yit Phang <kho...@cs.umd.edu>
To: stp-users <stp-...@googlegroups.com>
Cc: Khoo Yit Phang <kho...@cs.umd.edu>
Sent: Wednesday, 11 January 2012 2:53 PM
Subject: Local configuration in scripts/Makefile.local

[Khoo Yit Phang]

HI,

I do have a number of other patches on my Bitbucket page at <https://bitbucket.org/khooyp/stp-khooyp/qseries>; I can probably apply the first 6, which are fairly simple changes (though, I haven't checked the performance implications of fix-simplifyingnodefactory-creation):

conditional-march-native:

Conditionally enable -march=native, since it doesn't work in GCC on OS X.

fix-bitblaster-hash-set:

Fix BitBlaster to consistently use the hash_set macro defined in AST/UsefulDefs.h.

fix-bitblaster-vector-data:

Fix BitBlaster to not use the non-standard std::vector::data, for GCC-4.0 compatibility.

fix-simplifyingnodefactory-creation:

Fix creation of SimplifyingNodeFactory to use STPMgr's hashingNodeFactory, to satisfy various assertions.

local-svn-version:

Base version on local SVN change rather than the overall repository (if the STP source code is imported into another SVN project), so as not to trigger a relink and downstream rebuild.

push-pop-tests:

Add a C API test for the leak fixed in r1141 (when pushing/popping assertions), enabling valgrind on this test as well as another similar test.

The latter patches implements my Ocaml wrapper, but they affect performance significantly and I haven't updated them in a while (beyond maintenance).

Yit

January 11, 2012

[Khoo Yit Phang]

Hi Trevor,

I've checked compilation of STP under Clang 2.9 (without any of my STP patches). It fails to compile for a number of reasons, but there are no warnings about vector::data(). As far as I can tell, vector::data() isn't a standard method anyway, probably because vectors aren't necessarily backed by arrays.

BitBlaster.cpp:1461:32: error: variable length array of non-POD element type 'vector<BEEV::ASTNode>'
      vector<BBNode> t_products[bitWidth];
                               ^
BitBlaster.cpp:2634:18: note: in instantiation of member function 'BEEV::BitBlaster<BEEV::ASTNode,
      BEEV::BBNodeManagerASTNode>::mult_Booth' requested here
  template class BitBlaster<ASTNode, BBNodeManagerASTNode> ;
                 ^
BitBlaster.cpp:1461:32: error: variable length array of non-POD element type 'vector<BEEV::BBNodeAIG>'
      vector<BBNode> t_products[bitWidth];
                               ^
BitBlaster.cpp:2635:18: note: in instantiation of member function 'BEEV::BitBlaster<BEEV::BBNodeAIG,
      BEEV::BBNodeManagerAIG>::mult_Booth' requested here
  template class BitBlaster<BBNodeAIG, BBNodeManagerAIG> ;
                 ^
2 errors generated.

Changing the array to a vector reveals more errors:

BitBlaster.cpp:1467:11: error: no matching function for call to 'pushP'

          pushP(t_products, i, y, x[i], nf);

          ^~~~~

BitBlaster.cpp:2634:18: note: in instantiation of member function 'BEEV::BitBlaster<BEEV::ASTNode,

      BEEV::BBNodeManagerASTNode>::mult_Booth' requested here

  template class BitBlaster<ASTNode, BBNodeManagerASTNode> ;

                 ^

BitBlaster.cpp:1204:5: note: candidate template ignored: failed template argument deduction

    pushP(vector<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf)

    ^

BitBlaster.cpp:1473:11: error: no matching function for call to 'pushP'

          pushP(t_products, i, notY, BBTrue, nf);

          ^~~~~

BitBlaster.cpp:1204:5: note: candidate template ignored: failed template argument deduction

    pushP(vector<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf)

    ^

BitBlaster.cpp:1467:11: error: no matching function for call to 'pushP'

          pushP(t_products, i, y, x[i], nf);

          ^~~~~

BitBlaster.cpp:2635:18: note: in instantiation of member function 'BEEV::BitBlaster<BEEV::BBNodeAIG,

      BEEV::BBNodeManagerAIG>::mult_Booth' requested here

  template class BitBlaster<BBNodeAIG, BBNodeManagerAIG> ;

                 ^

BitBlaster.cpp:1204:5: note: candidate template ignored: failed template argument deduction

    pushP(vector<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf)

    ^

BitBlaster.cpp:1473:11: error: no matching function for call to 'pushP'

          pushP(t_products, i, notY, BBTrue, nf);

          ^~~~~

BitBlaster.cpp:1204:5: note: candidate template ignored: failed template argument deduction

    pushP(vector<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf)

    ^

4 errors generated.

Yit

January 11, 2012

On Jan 11, 2012, at 10:24 AM, Trevor Hansen wrote:

Hi Yit,

Thanks for working so hard! They look good to me except for the bitblaster-vector-data patch, see below.

conditional-march-native:  Yes.

fix-bitblaster-hash-set: Yes This was me being lazy. Thanks.
fix-bitblaster-vector-data: This was introduced by Peter Collingbourne to get STP compiling on clang. I don't remember why. We'd need to check if it still compiles on clang / whether this is required.

fix-simplifyingnodefactory-creation: Yes, thanks.
local-svn-version: thanks.

Trev.

---

From: Khoo Yit Phang <kho...@cs.umd.edu>

To: stp-...@googlegroups.com

Cc: Khoo Yit Phang <kho...@cs.umd.edu>

Sent: Thursday, 12 January 2012 1:54 AM
Subject: Re: Local configuration in scripts/Makefile.local

[Peter Collingbourne]

On Wed, Jan 11, 2012 at 10:46:41AM -0500, Khoo Yit Phang wrote:
> Hi Trevor,
>
> I've checked compilation of STP under Clang 2.9 (without any of my STP patches). It fails to compile for a number of reasons, but there are no warnings about vector::data(). As far as I can tell, vector::data() isn't a standard method anyway, probably because vectors aren't necessarily backed by arrays.

std::vector::data() was standardised in C++11, but the C++ standard has
always required vector elements to be stored contiguously (i.e. like
an array) -- see C++98 [lib.vector].

So we can either use &v[0] instead of v.data(), or pass vectors around
as in your patch. I don't really mind which.

I changed these to use vectors and &v[0], and made a few other
changes to fix Clang compilation in r1501.

Thanks,
--
Peter

[Khoo Yit Phang]

Hi,

On Jan 11, 2012, at 12:04 PM, Peter Collingbourne wrote:

On Wed, Jan 11, 2012 at 10:46:41AM -0500, Khoo Yit Phang wrote:

So we can either use &v[0] instead of v.data(), or pass vectors around
as in your patch.  I don't really mind which.

Alright, I'll check in my patch (which has the advantage of preventing NULL errors).

Yit

January 11, 2012