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: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Solver/Solver.cpp?view=diff&r1=73132&r2=73133 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 http://people.csail.mit.edu/vganesh/ though. - Daniel > -- > 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 > arr7) > > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? (Concat > w24 (Read w8 6 arr7) > > > ? (ReadLSB w16 4 arr7))) > > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?24) > > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? (And w32 (Shl w32 N1 8) 16711680)) > > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? (Or w32 (And w32 (LShr w32 N1 8) 65280) > > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? (LShr w32 N1 24))) > > ? ? ? ? ? ? ? ? ? ? ? ? ? 24))) > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?10) > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?10) > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?10) > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? 10) > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?48 > ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?0) > ? ? ? ? ? ? ? ? ? (Extract w8 0 N0)))) > >
