[klee-dev] STP solver looping indefinitely
daniel at zuster.org
Thu Oct 15 17:52:32 PDT 2009
2009/10/15 Seungbeom Kim <sbkim at stanford.edu>:
> Daniel Dunbar wrote:
>> Well, it's certainly possible that you are getting a query that is
>> hard to solve. It's NP-hard, after all, so it doesn't take much work
>> to find queries that will take days to solve.
>> That said, if it only happens on one machine maybe something else is
>> going on. What versions of gcc do the machines have? Maybe MINISAT is
>> being miscompiled?
> cluestick has gcc (GCC) 4.3.0 20080428 (Red Hat 4.3.0-8),
> bohr has gcc (Debian 4.3.4-5) 4.3.4.
> I don't think any of these are outdated enough to be suspected,
Outdated isn't usually a good indication of brokenness. See
http://llvm.org/docs/GettingStarted.html#brokengcc for a nice litany
of versions that are known to miscompile LLVM (or did at some point).
As far as I know the above ones are ok, though.
> but how can I tell if one is causing the proble?
Generally the only option is to install another version and see if it
works, unless you can actually prove its a miscompile.
> By the way, the Makefile is certainly broken -- running make from
> $KLEE_ROOT doesn't recognize any changes in the source files in
> $KLEE_ROOT/stp/AST, nor does running make from $KLEE_ROOT/stp.
> Either you have to run "make clean" each time, or after changing
> any source file you have to do "make" first in $KLEE_ROOT/stp/AST,
> then in $KLEE_ROOT/stp, and then in $KLEE_ROOT.
I believe you, please submit a patch if you have one. The STP build
doesn't use the LLVM makefiles, its dependencies are pretty broken. I
fixed a few obvious ones (to make 'make -j' work), but haven't tried
to fix them all, since I don't have on STP much.
>> Otherwise it might be worth sending the query to Vijay, he may have a
>> better idea.
> I attached a query (printed from KLEE) that I saw more than once that
> caused the indefinite loop.
Note that the query has one remainder and two divides... these are not
"happy" operations for STP/SAT. It's really quite easy to make simple
queries that run for hours (days, years, lifetime-of-universe), so I'm
not sure I would call it an infinite loop. One way to see if its just
a complexity issue would be to take the query try reducing the
bitwidth of the remainder/division operations to, say, 16 bits, and
see if it terminates in a reasonable time.
> How can I feed this into the stand-alone
> STP solver ($KLEE_ROOT/stp/bin/stp, I guess)? It seems to expect a
> certain grammar that $KLEE_ROOT/stp/bin/stp doesn't accept directly.
There is code in klee to print the query in STP format, see:
I should add back the command line option to generate this, at some point.
> And how can I reach Vijay? (Are you on this list? :D)
He isn't on the list as far as I know, see
> Seungbeom Kim
> (Not (Eq 0
> (Add w8 (Select w8 (Ult N0:(URem w32 (UDiv w32 (UDiv w32 (Extract
> w32 0 (ZExt w64 (LShr w32 (Or w32 (Or w32 (Shl w32 N1:(Concat w32 (Read w8 7
> w24 (Read w8 6 arr7)
> (ReadLSB w16 4 arr7)))
> (And w32 (Shl w32 N1 8) 16711680))
> (Or w32 (And w32 (LShr w32 N1 8) 65280)
> (LShr w32 N1 24)))
> (Extract w8 0 N0))))
More information about the klee-dev