Bug 555162 - Review Request: blast - Berkeley Lazy Abstraction Software Verification Tool
Review Request: blast - Berkeley Lazy Abstraction Software Verification Tool
Status: CLOSED CANTFIX
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
rawhide
All Linux
medium Severity medium
: ---
: ---
Assigned To: David A. Wheeler
Fedora Extras Quality Assurance
:
Depends On: 555161
Blocks:
  Show dependency treegraph
 
Reported: 2010-01-13 15:37 EST by Jerry James
Modified: 2010-02-26 14:02 EST (History)
3 users (show)

See Also:
Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Environment:
Last Closed: 2010-02-10 12:18:15 EST
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
CRM:
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
dwheeler: fedora‑review?


Attachments (Terms of Use)

  None (edit)
Description Jerry James 2010-01-13 15:37:59 EST
Spec URL: http://jjames.fedorapeople.org/blast/blast.spec
SRPM URL: http://jjames.fedorapeople.org/blast/blast-2.5-1.fc12.src.rpm
Description:
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-17 23:23:14 EST
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:
%{_bindir}/htmlize
%{_bindir}/mfilter
%{_bindir}/pblast
%{_bindir}/smt_solver
%{_bindir}/smtlibServer
%{_bindir}/spec
%{_bindir}/vampyre
%{_includedir}/blast


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?

Thoughts?
Comment 2 David A. Wheeler 2010-01-17 23:33:50 EST
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 00:03:49 EST
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 17:44:09 EST
Note to others: BLAST depends on two other applications, which have been packaged and approved for inclusion in the Fedora repository.  See:
https://bugzilla.redhat.com/show_bug.cgi?id=555160
https://bugzilla.redhat.com/show_bug.cgi?id=555161
Comment 5 Jerry James 2010-02-10 12:18:15 EST
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 17:18:44 EST
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
MOPS
Comment 7 David A. Wheeler 2010-02-12 13:50:15 EST
I looked briefly at CPAchecker. There's a paper about it here:
http://www.sosy-lab.org/~dbeyer/Publications/2009-SFU-TR002.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf

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 11:26:44 EST
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:

=============
David,
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
http://www.cs.ucla.edu/~rupak/b2/

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 12:31:08 EST
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 14:02:23 EST
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.