Bug 555162 - Review Request: blast - Berkeley Lazy Abstraction Software Verification Tool
Summary: Review Request: blast - Berkeley Lazy Abstraction Software Verification Tool
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
Target Milestone: ---
Assignee: David A. Wheeler
QA Contact: Fedora Extras Quality Assurance
Depends On: 555161
TreeView+ depends on / blocked
Reported: 2010-01-13 20:37 UTC by Jerry James
Modified: 2010-02-26 19:02 UTC (History)
3 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Last Closed: 2010-02-10 17:18:15 UTC
Type: ---
dwheeler: fedora-review?

Attachments (Terms of Use)

Description Jerry James 2010-01-13 20:37:59 UTC
Spec URL: http://jjames.fedorapeople.org/blast/blast.spec
SRPM URL: http://jjames.fedorapeople.org/blast/blast-2.5-1.fc12.src.rpm
BLAST is a software model checker for C programs.  The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses.  BLAST uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties.  The abstraction is constructed on-the-fly, and only to the required precision.

Comment 1 David A. Wheeler 2010-01-18 04:23:14 UTC
One thing that jumps out at me is the "ocaml-caddie" package it creates (CAml cuDD InterfacE).  It isn't named as a subpackage but is a completely separate package.  This "ocaml-caddie" package certainly looks useful, but is this really the right source for it?  Or is there a better upstream we should be trying to use instead?
(I presume this is different from MLCUDDIDL, which is also an OCaml binding to cuDD.)

This draft package includes "vampyre", which is NOT open source software.
This needs to be removed.  Its license says:
"Permission to use, copy, modify and distribute
 this software for research purposes only is hereby granted..."
Note that it's ONLY permitted for use for "research purposes"... you
are NOT allowed to use it for anything useful.  Thus,
it's not okay for Fedora to include it.  Vampyre needs to
be stripped out of this package.  I hope it can still be used
without it; if vampyre is 100% required,  then this package is done for.

Instead of:
 sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc/Makefile
 sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc2/Makefile
 sed -i -e "s|@libdir@|%{_libdir}|" blast/spec/Makefile
Why not (so we can see it's all the same change):
sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc/Makefile \
                     blast/psrc2/Makefile blast/spec/Makefile

Should the smp_mflags limitation be a "FIXME"?  It's more just a fact of life.

Looking over the installed files, I see all sorts of issues:

As I noted above, it installs "vampyre", which isn't allowed. Also,
a number of these other names are probably too generic to be
acceptable.  I bet there are a dozen "htmlize" programs.
Other bad names include mfilter, smt_solver, smtlibServer, spec.
Also, one weird thing... the package is named "blast", but the
program isn't named "blast"?  That's okay, but odd.

It did build on a 32-bit x86.

I can't easily use koji, since this depends on a package (csisat) not in the Fedora repository.

I ran rpmlint using rpmlint blast.spec ../RPMS/i586/blast-2.5-1.fc11.i586.rpm  ../RPMS/i586/ocaml-caddie-* ../SRPMS/blast-2.5-1.fc11.src.rpm
and got 2 warning messages:
blast.i586: W: devel-file-in-non-devel-package /usr/include/blast/assert.h
ocaml-caddie-devel.i586: W: no-documentation
4 packages and 1 specfiles checked; 0 errors, 2 warnings.
The first one is probably okay, and we can ignore the warning.
The second one doesn't look good.  ocaml-caddie should have SOME docs, yes?


Comment 2 David A. Wheeler 2010-01-18 04:33:50 UTC
I went through the "caddie" subdirectory, and in particular looked at caddieBdd.ml and caddie.c (the key source files).  This software library is *not* under the ASL, but under the modified (3-clause) BSD license.  That's not a *problem*... BSD is a well-known FLOSS license, and these licenses are legal to combine.  But it means that the license statements aren't right.  The ocaml-caddie package should have a "License" of "BSD" per http://fedoraproject.org/wiki/Licensing#Good_Licenses
and not ASL 2.0.

Comment 3 David A. Wheeler 2010-01-18 05:03:49 UTC
Why doesn't the package build the gui (blastgui), at least as a subpackage?  This would "BuildRequire: ocaml-lablgtk", then "make gui".  (You'd need to set up a desktop, and find a way to set BLASTGUI, but sounds useful.)

I compiled it and tried to run it as it is.
It *did* work.  I put this in file "foo.c":
#include <assert.h>
int foo(int x, int y) {
 if (x > y) {
   x = x - y;
   L: assert(x > 0);

Then did:
 gcc -E -I /usr/include/blast/ foo.c > foo.tmp
 mfilter foo.tmp > foo.i
 pblast -main foo -smt foo.i

Which eventually produced:
 No error found.  The system is safe :-)

You have to give it the "-smt", or it tries to use the Simplify prover,
and since Simplify isn't there it fails.

Comment 4 David A. Wheeler 2010-01-20 22:44:09 UTC
Note to others: BLAST depends on two other applications, which have been packaged and approved for inclusion in the Fedora repository.  See:

Comment 5 Jerry James 2010-02-10 17:18:15 UTC
Sorry to take so long with this, but you raised some thorny issues.  I'm afraid that vampyre is, indeed, required.  At least, I can't find a way to untangle it from the main code (grep for "vampyre" in blast/psrc).  So I guess we're done: this package cannot be included in Fedora for licensing reasons.

We should perhaps look at http://code.google.com/p/cpachecker/ instead.  Its author, one of the BLAST maintainers, calls it a "better BLAST".  On the other hand, they haven't reached a 1.0 release yet.

Comment 6 David A. Wheeler 2010-02-11 22:18:44 UTC
Ugh.  Can you send an email to its developers?  Maybe vampyre can be untangled by them.

Packaging http://code.google.com/p/cpachecker/ is not a bad idea.  Other alternatives are:
Saturn http://saturn.stanford.edu/pages/overviewindex.html

Comment 7 David A. Wheeler 2010-02-12 18:50:15 UTC
I looked briefly at CPAchecker. There's a paper about it here:

The paper suggests that CPAchecker may depend on Simplify and MathSAT.  I know that Simplify is not FLOSS (it's not even clear it's legal to distribute at all), and I don't think that MathSAT is FLOSS either.  So CPAchecker may be unpackageable.

Comment 8 David A. Wheeler 2010-02-26 16:26:44 UTC
Good news!  On Thu, 25 Feb 2010 14:45:56 -0800, Rupak Majumdar ( rupak /at/  CS, dot, UCLA , dot, EDU send to me this email:

I am the original developer of Blast (the only other tool I know that used
Vampyre and is available) and we have gotten rid of vampyre dependencies.

The latest version of Blast (not depending on vampyre) is at

I will also relicense vampyre, but will only get to it next week.

This "latest version of BLAST" is really a follow-on project, with a new project name "B2".  It's released under the Apache 2.0 license, which is uncontroversially FLOSS.  If you package B2, I suggest opening a different review request... it's a different name, different developer, etc.

Once vampyre is released as FLOSS, you can continue with the BLAST packaging.
I still think it's great to get vampyre released as FLOSS, even if you decide to not package BLAST itself and just package B2 or something else instead.  As we package other stuff, I suspect we'll find other vampyre users :-).

Comment 9 David A. Wheeler 2010-02-26 17:31:08 UTC
Correction: It appears that B2 depends on Simplify.  Simplify isn't FLOSS, and I doubt it ever will be.  So if B2 really *requires* Simplify, then B2 cannot be packaged in the Fedora repository (or many others' either).

But if vampyre is released as FLOSS, then to the best of my understanding we can re-open this review request, since it would then be possible to package BLAST in the Fedora repository.

Comment 10 David A. Wheeler 2010-02-26 19:02:23 UTC
I got more information from Rupak about B2 (his replacement for BLAST);
B2 can work without Simplify.  Thus, it *appears* that we could package B2, but we'll need to package dpt (and hope that there aren't any MORE license problems).

Here is his Rupak's response:
> There is a compile time option to get rid of simplify. At the moment,
> there are backends to Simplify,
> Yices (also not FLOSS) and DPT (FLOSS, dpt.sourceforge.net).
> There is a component called Foci also not FLOSS, but an alternate
> CSISAT which is FLOSS. Again, there is a compile time way to take out Foci.

Note You need to log in before you can comment on or make changes to this bug.