seahorn / clam Goto Github PK

Static Analyzer for LLVM bitcode based on Abstract Interpretation

License: Apache License 2.0

CMake 5.37% C++ 19.04% Python 2.23% C 73.24% Dockerfile 0.05% Emacs Lisp 0.07%

llvm program-analysis abstract-interpretation invariants static-analysis software-verification

clam's Introduction

Clam: LLVM front-end for Crab

Clam is an Abstract Interpretation-based static analyzer that computes inductive invariants for LLVM bitcode based on the Crab library. This branch supports LLVM 14.

The available documentation can be found in both Clam wiki and Crab wiki.

Docker

You can get Clam from Docker Hub (nightly built) using the command:

 docker pull seahorn/clam-llvm14:nightly

Requirements

Clam is written in C++ and uses heavily the Boost library. The main requirements are:

Modern C++ compiler supporting c++14
Boost >= 1.65
GMP
MPFR (only if -DCRAB_USE_APRON=ON or -DCRAB_USE_ELINA=ON)
FLINT (only if -DCRAB_USE_PPLITE=ON)
Python >= 3.6

In linux, you can install requirements typing the commands:

 sudo apt-get install libboost-all-dev libboost-program-options-dev
 sudo apt-get install libgmp-dev
 sudo apt-get install libmpfr-dev	
 sudo apt-get install libflint-dev

Tests

Testing infrastructure depends on several Python packages. To run tests you need to install lit and OutputCheck:

 pip3 install lit
 pip3 install OutputCheck

Compilation and installation

The basic compilation steps are:

1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..   
4. cmake --build . --target extra && cmake ..                  
5. cmake --build . --target install

The command at line 2 will try to find LLVM 14 from standard paths. If you installed LLVM 14 in a non-standard path, then add option -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm to line 2. The command at line 3 will download Crab and compile it from sources. Clam uses two external components that are installed via the extra target at line 4. These components are:

sea-dsa is the heap analysis used to translate LLVM memory instructions. Details can be found here and here.
llvm-seahorn provides specialized versions of LLVM components to make them more amenable for verification. llvm-seahorn is optional but hightly recommended.

The Boxes/Apron/Elina/PPLite domains require third-party libraries. To avoid the burden to users who are not interested in those domains, the installation of the libraries is optional.

If you want to use the Boxes domain then add -DCRAB_USE_LDD=ON option.
If you want to use the Apron library domains then add -DCRAB_USE_APRON=ON option.
If you want to use the Elina library domains then add -DCRAB_USE_ELINA=ON option.
If you want to use the PPLite library domains then add -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON options.

Important: Apron and Elina are currently not compatible so you cannot enable -DCRAB_USE_APRON=ON and -DCRAB_USE_ELINA=ON at the same time.

For instance, to install Clam with Boxes and Apron:

1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..                
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..             
7. cmake --build . --target install

For instance, lines 5 and 6 will download, compile and install the Boxes and Apron libraries, respectively. If you have already compiled and installed these libraries in your machine then skip commands at line 5 and 6 and add the following options at line 2.

For Apron: -DAPRON_ROOT=$APRON_INSTALL_DIR
For Elina: -DELINA_ROOT=$ELINA_INSTALL_DIR
For Boxes: -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
For PPLite: -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

Checking installation

To run some regression tests:

 cmake --build . --target test-simple

Usage

Clam provides a Python script called clam.py (located at $DIR/bin where $DIR is the directory where Clam was installed) to interact with users. The simplest command is clam.py test.c. Type clam.py --help for all options and read our wiki.

clam's People

Contributors

Stargazers

Watchers

clam's Issues

Possibly stack overflow while computing WTO of a large CFG

Problem07_label52_true-unreach-call.pp.bc.zip

Command:

crabllvm Problem07_label52_true-unreach-call.pp.bc  --crab-verbose=2 --crab-dom=int --crab-widening-delay=2 --crab-widening-jump-set=0 --crab-narrowing-iterations=2 --crab-track=arr --crab-singleton-aliases  --crab-check=assert --crab-stats --crab-disable-warnings

silently produces signal 11 (SEGFAULT).
I did some gdb and it seems that we run out of stack while computing WTO using recursion.

Wrong order of include directories when build from SeaHorn

When crab-llvm is include in SeaHorn as a sub-project it looks first inside the installed include directories as opposed to its source location. Every time the headers change, the build fails because it finds the old header files first.

Current work-around is to delete BUILD_DIR/crab_llvm and BUILD_DIR/crab manually.

It would be more convenient if the order of include directories is fixed.

Crab Error: CFG has no exit

Hi,

I'm running crab-llvm and trying to insert invariants in the bitcode and i'm getting an error: Crab Error: CFG has no exit but I'm not sure why.

Here is the llvm bitcode and i first run crabllvm-pp as follows

./crabllvm-pp -crab-devirt -devirt-resolver=dsa -crab-lower-select -o dd_pp.bc dd.bc

Afterwards I run:

./crabllvm -crab-inter -crab-print-invariants -crab-heap-analysis=cs-sea-dsa dd_pp.bc

This produces the following:

....
WARNING: 94603348149576 is allocating a new cell.
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: Skipped   %_6 = extractelement <2 x i64> %_5, i32 1
CRABLLVM WARNING: Skipped   %_7 = extractelement <2 x i64> %_5, i32 0
CRABLLVM WARNING: Skipped   %_9 = extractelement <2 x i64> %_8, i32 0
CRABLLVM WARNING: Skipped   %_63 = extractelement <2 x i64> %_60, i32 1
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: Skipped   %_9 = extractelement <2 x i64> %_8, i32 1
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRABLLVM WARNING: skipped indirect call. Enabling --devirt-functions might help.
CRAB ERROR: CFG has no exit

Any assistance would be helpful and let me know if there is anything more I can provide. Thanks!

Segfault in crab-llvm-pp when LowerSwitch pass is executed

The zip file contains the file and the command to reproduce the segfault.

lower-switch-bug.zip

Unsoundness with recursive functions

Hi,
I was wondering whether crab-llvm handles recursive functions. Consider the following program:

extern int __VERIFIER_nondet_int();
extern void __VERIFIER_error();
void __VERIFIER_assert(int cond) {
  if (!cond) {
  ERROR: __VERIFIER_error();
  }
}

int fibo(int n) {
  // This does not hold
  __VERIFIER_assert(n != 0);
  if (n < 1) {
      return 0;
  } else if (n == 1) {
      return 1;
  } else {
      return fibo(n - 1) + fibo(n - 2);
  }
}

int main(void) {
  int x = 10;
  int result = fibo(x);
  return 0;
}

./crabllvm.py -m 32 --crab-inter --crab-check=assert --crab-dom=int /database/confrontation/crab/fibo.c yields

************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks
************** ANALYSIS RESULTS END*************

Another question, and only slightly related: Do crab-llvm and seahorn use the same frontend? Because as discussed in seahorn/seahorn#152, seahorn does not completely cover all potential program behavior if some part is implementation-specific (e.g. uninitialized variables). So, naturally I assumed that crab-llvm and seahorn would handle those cases similarly. Interestingly, sometimes there are still cases where crab-llvm and seahorn disagree because of undefined behavior, e.g.:

extern void __VERIFIER_error() __attribute__((__noreturn__));

void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
extern int __VERIFIER_nondet_int();
int main()
{
    int i, n = __VERIFIER_nondet_int();
    if (!(n < 1000 && n >= -1000))
    {
        return 0;
    }
    __VERIFIER_assert(i <= n );
}

(seahorn: Sat, crab-llvm: Unsat)

Precise translation of boolean operations

The solution is to translate all comparison instructions that do not feed branches and Boolean operations to crab Boolean operations. In that way, the abstract domain will decide what to do. Until now, we were assuming that the abstract domain does not have knowledge about Boolean operations so the translation tried to reduce all Boolean operations to expensive crab select statements.

LLVM-8.0 use sea-dsa to resolve indirect calls

Hi,

I was looking at #25 and I noticed you added dsa support to resolve indirect calls. However, dsa has not been ported to 8.0 but sea-dsa has. Would it be possible to use sea-dsa to resolve indirect calls?

question about --crab-bounds-check

Hi Seahorn Team,

Q1: is --crab-bounds-check for buffer overflow?
Q2: I don't find documentation regarding this option, is it deprecated?
Q3: I open this option but return -- Inserted 0 bound checks every time, Do I need to insert something to source code to enable it?

Thank you.

Tag analysis questions

Hey there!

I am trying to understand the tag analysis described here. I am hoping to implement a static taint analysis using this, but am a bit confused how to do this using the current __CRAB_intrinsic_check_does_not_have_tag assert.

If I want to understand what tags (i.e., taint) can reachable a given location, what is the best way to encode this given I only have the "does not have tag" function?

Thanks so much for all of your help!

Fail to build shared library

Hey Clam devs!

I am unable to build Clam as a shared library.

Here is my build:

cmake .. -DCLAM_BUILD_LIBS_SHARED=On -DCRAB_BUILD_LIBS_SHARED=On

Doing so gives me a whole bunch of

undefined reference to `crab::domains::dis_interval<ikos::z_number>::bottom()'

Curiously, I don't see this error when building a static lib.

Question about assertion checking?

Hi, I run clam with the following command:

clam test.bc --crab-dom=int --crab-heap-analysis=none --crab-check=assert

I have already instrumented test.bc with some __CRAB_assert checks. When the analysis finishes, clam outputs:

************** ANALYSIS RESULTS ****************
 92   Number of total safe checks
  0    Number of total error checks
128  Number of total warning checks
************** ANALYSIS RESULTS END*************

It seems that there should be 128+92=220 checking statements in test.bc. However, I find out there are
more (around 700) inserted __CRAB_assert checks in test.bc.
Why is this happening? Does clam skip the verification for some __CRAB_assert statements?

PK domain is sometimes less precise than int?

Hi everyone,

I found a few interesting cases in which crab using the pk domain is less precise than when using the int domain. One example:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {   
    ERROR:
        __VERIFIER_error();
    }   
}
int main() {
    int i, j, k;
    i = 0;
    j = 0;
    while (i <= 100) {
        __VERIFIER_assert(i + 1 != 0); 
        i = i + 1;
        /* this part is relevant to the reachability of the assertion */
        while (j < 20) {
            j = i + j;
        }   
    }   
    return 0;
}

I invoked crab with the following parameters:
./crabllvm.py -m 32 --crab-inter --crab-check=assert --crab-dom=int
For which the output ends in

************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks

Now, if switch to the pk domain (--crab-dom=pk), the output changes to

************** ANALYSIS RESULTS ****************
0  Number of total safe checks
0  Number of total error checks
1  Number of total warning checks

Is there are a particular reason for this or this is a bug?

Thank you very much,
Chris

[llvm-dis] Invalid instruction with no BB

Hello,

I get the following error if I call llvm-dis after running crab-llvm on the c code below:
llvm-dis: error: Invalid instruction with no BB (Producer: 'LLVM5.0.2' Reader: 'LLVM 5.0.2')

Information to reproduce the bug:
Crab-llvm: Docker build (i.e. with apron)

$ crabllvm --version
LLVM (http://llvm.org/):
  LLVM version 5.0.2
  Optimized build.
  Default target: x86_64-unknown-linux-gnu
  Host CPU: sandybridge

example.c:

#include <stdio.h>

unsigned a;
unsigned x;

int main(int argc, char const* argv[])
{
    a = *(unsigned *) argv[1];
    unsigned b = a;
    unsigned c = 1;

    x = 32;
    x ^= a * 3;

    if (b == 0x55787855)
        printf("SUCCESS\n");
    else
        printf("FAILURE\n");

    printf("0x%x", x);
    return 0;
}

How to reproduce:

$ crabllvm.py example.c --crab-dom=pk --crab-track=arr --crab-add-invariants=all -o test.crab.bc
[omitted]
$ llvm-dis test.crab.bc
llvm-dis: error: Invalid instruction with no BB (Producer: 'LLVM5.0.2' Reader: 'LLVM 5.0.2')

The error occurred with the following domains:

pk
term-int
term-dis-int
rtz

Have a nice day :)

Precise translation of pointer instructions

From @caballa on October 15, 2016 23:40

The translation currently abstract pointers to their offsets.

Copied from original issue: caballa/crab-llvm#4

Is it possible to integrate crab-llvm at the library level?

Hi,

I play around with your crab-llvm tool and see that it can generate many interesting invariants, such as the Apron's polka or the reduced product of intervals and congruences domain.

I would like to integrate and test it further in my project, which also uses LLVM infrastructure (but version 3.2), could you advise me a starting point so that I can pass the CFG (llvm data structures) in my project to your crab-llvm library to compute the invariant of a specific basic block?

Another off-topic question I would like to ask is that crab-llvm uses Apache license, whereas the Apron library uses LGPL license. Are these two licenses compatible?

Thank you for your time when considering my question!

Docker Pull not Working

I was trying to install from docker using the suggested command:
docker pull seahorn/clam_5.0:latest
But I keep getting the following error
Error response from daemon: manifest for seahorn/clam_5.0:latest not found: manifest unknown: manifest unknown
I am using Docker version 19.03.4, build 9013bf583a on Debian GNU/Linux 9 (stretch)

Integrate new DSA from seahorn

From @caballa on April 9, 2017 3:20

The new DSA is available here https://github.com/seahorn/sea-dsa.

Copied from original issue: caballa/crab-llvm#11

Sea-DSA uses up a lot of memory

Hi,

This is more of a question but I'm running crab-llvm on a moderately sized llvm bitcode file here and it seems to use up 150GB of memory (don't know the upper limit as it always uses up too much). I tried to use valgrind but it was way too slow. Does what I say seem possible?

My command is:

./crabllvm -crab-inter -crab-track=arr -crab-dom=int -crab-heap-analysis=cs-sea-dsa [prog]

Regards,
Shankara

How to reproduce Elina paper results

This is from #66. I prefer to open a new issue to address it.

dengyuhui14 wrote:

I want to see if it is possible to make some improvement to the polyhedra abstract domain based on the ELINA library and Apron library. But first I need to reproduce the experiment in this paper. This paper uses crab-llvm analyzer, but it seems that I can't find crab-llvm. And I don't quite understand how analyzer and abstract domain work together to give invariants. Could you please give me some advice on how to conduct these experiment?

ICE error with the head of master tree

Hi ,
I've got this ICE error when compling the head master tree,
my gcc version is 5.5.0
[ 19%] Building CXX object lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/InsertInvariants.cc.o

c++: internal compiler error: Killed (program cc1plus)
Please submit a full bug report,
with preprocessed source if appropriate.
See file:///usr/share/doc/gcc-5/README.Bugs for instructions.
lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/build.make:62: recipe for target 'lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/InsertInvariants.cc.o' failed
make[2]: *** [lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/InsertInvariants.cc.o] Error 4
CMakeFiles/Makefile2:1367: recipe for target 'lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/all' failed
make[1]: *** [lib/CrabLlvm/CMakeFiles/CrabLlvmInstrumentation.dir/all] Error 2
Makefile:162: recipe for target 'all' failed
make: *** [all] Error 2

Specify entry point and auto generate nd values

Dear crab-llvm researchers,

I went through the possible options and the test files in the repo. They all start with the main function. I wonder if there a way to specify entry point and auto generate nd values against a testing function? For example, specify the entry point for "int get_sign(int test)" function, and auto generate a nd value for int test. If there is no way to do in current llvm-crab, my current plan is to write another llvm pass to the read the bc file for the function and read its signature.

Thank you very much.

Best,
Phil

Integrate master branch from crab

From @caballa on October 15, 2016 23:46

Crab master branch changes the CFG language so the class CfgBuilder needs to be updated accordingly.

Copied from original issue: caballa/crab-llvm#5

/usr/bin/ld: cannot find -lLLVMExtensions

When I tried to build the clam, in the last few steps: it shows the following.
[ 57%] Built target SeaInstCombine
[ 57%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/AnalysisWrappers.cpp.o
[ 59%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/CallGraphPrinterWrapper.cc.o
[ 61%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/GraphPrinters.cpp.o
[ 61%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/BreakpointPrinter.cpp.o
[ 61%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/NewPMDriver.cpp.o
[ 62%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/PassPrinters.cpp.o
[ 62%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/PrintSCC.cpp.o
[ 64%] Building CXX object llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/opt.cpp.o
[ 64%] Linking CXX executable ../../../bin/seaopt
/usr/bin/ld: cannot find -lLLVMExtensions
clang-10: error: linker command failed with exit code 1 (use -v to see invocation)
make[2]: *** [llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/build.make:319: bin/seaopt] Error 1
make[1]: *** [CMakeFiles/Makefile2:2383: llvm-seahorn/tools/opt/CMakeFiles/seaopt.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[ 64%] Linking CXX static library ../../../lib/libSeaDsaAnalysis.a
[ 64%] Built target SeaDsaAnalysis
make: *** [Makefile:152: all] Error 2

Which part of LLVM did I miss?

I used both from the " cmake --build . --target llvm && cmake .. " and also a local version. Both had the same ld error.

Thank you very much and any suggestions would be much appreciated.

System: ubuntu 20.04

LLVM 10.0.0 is buggy, which should not be used...

Devirtualization Error

Hi,

I'm running crabllvm-pp on this bitcode with the following commands:

./crabllvm-pp -crab-devirt -devirt-resolver=dsa -crab-lower-select -crab-lower-unsigned-icmp -o strings_pp.bc strings.bc

However, I get the following error:

#0 0x000056470871b13b llvm::sys::PrintStackTrace(llvm::raw_ostream&) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:495:0
 #1 0x000056470871b1ce PrintStackTraceSignalHandler(void*) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:559:0
 #2 0x0000564708718db2 llvm::sys::RunSignalHandlers() /home/shankara/llvm-project/llvm/lib/Support/Signals.cpp:69:0
 #3 0x000056470871ab5d SignalHandler(int) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:358:0
 #4 0x00007f3c68f51890 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12890)
 #5 0x00007f3c6824de97 gsignal /build/glibc-OTsEL5/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
 #6 0x00007f3c6824f801 abort /build/glibc-OTsEL5/glibc-2.27/stdlib/abort.c:81:0
 #7 0x00007f3c6823f39a __assert_fail_base /build/glibc-OTsEL5/glibc-2.27/assert/assert.c:89:0
 #8 0x00007f3c6823f412 (/lib/x86_64-linux-gnu/libc.so.6+0x30412)
 #9 0x000056470766707f llvm::CallInst::init(llvm::FunctionType*, llvm::Value*, llvm::ArrayRef<llvm::Value*>, llvm::ArrayRef<llvm::OperandBundleDefT<llvm::Value*> >, llvm::Twine const&) /home/shankara/llvm-project/llvm/lib/IR/Instructions.cpp:372:0
#10 0x0000564706ffe778 _ZN4llvm8CallInstC4EPNS_12FunctionTypeEPNS_5ValueENS_8ArrayRefIS4_EENS5_INS_17OperandBundleDefTIS4_EEEERKNS_5TwineEPNS_11InstructionE /usr/local/include/llvm/IR/Instructions.h:1725:0
#11 0x0000564706ffe778 llvm::CallInst::Create(llvm::FunctionType*, llvm::Value*, llvm::ArrayRef<llvm::Value*>, llvm::Twine const&, llvm::Instruction*) /usr/local/include/llvm/IR/Instructions.h:1490:0
#12 0x0000564706ffe778 llvm::CallInst::Create(llvm::Function*, llvm::ArrayRef<llvm::Value*>, llvm::Twine const&, llvm::Instruction*) /usr/local/include/llvm/IR/Instructions.h:1535:0
#13 0x0000564706ffe778 crab_llvm::DevirtualizeFunctions::mkDirectCall(llvm::CallSite, crab_llvm::CallSiteResolver*) /home/shankara/crab-llvm/lib/Transforms/DevirtFunctions.cc:527:0
#14 0x0000564706fffbd7 crab_llvm::DevirtualizeFunctions::resolveCallSites(llvm::Module&, crab_llvm::CallSiteResolver*) /home/shankara/crab-llvm/lib/Transforms/DevirtFunctions.cc:603:0
#15 0x0000564706ff9764 crab_llvm::DevirtualizeFunctionsPass::runOnModule(llvm::Module&) /home/shankara/crab-llvm/lib/Transforms/DevirtFunctionsPass.cc:82:0
#16 0x00005647076a5c54 (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /home/shankara/llvm-project/llvm/lib/IR/LegacyPassManager.cpp:1744:0

I observed that during the devirtualization that crabllvm is reusing the bounce function:

Reusing bounce function for  call void (i8*, ...) %152(i8* %call94, %struct.bfd* %153, %struct.bfd_section* %154, %struct.reloc_cache_entry* %156)
	seahorn.bounce.16::void (void (i8*, ...)*, i8*, %struct.bfd*, %struct.bfd_section*, %struct.reloc_cache_entry*, i32)*

It seems there is this additional i32 argument which shouldn't be there.

CRAB error because GMP z_number does not fit into a signed long integer

CRAB ERROR: mpz_class -9223372036854775809 does not fit into a signed long integer

This happens with split-dbm domain. This is a well known limitation since the domain uses for efficiency signed long integer as DBM weights rather than unlimited precision z_number.

Attached a zip file to reproduce the problem:

split-dbm-too-big-weight.zip

Add nullity analysis

From @caballa on October 15, 2016 23:55

Add a nullity analysis. This requires to resolve first Issues #4 and #5

Copied from original issue: caballa/crab-llvm#7

fatal: Could not find the clam executable

Hi,

I am using Mac OSX catalina and follow the installation instruction.
mkdir build && cd build cmake -DCMAKE_INSTALL_PREFIX=_DIR_ -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../ cmake --build . --target extra cmake --build . --target crab && cmake .. cmake --build . --target ldd && cmake .. cmake --build . --target apron && cmake .. cmake --build . --target llvm && cmake .. cmake --build . --target install

Things go smooth except I brew install svn before cmake --build . --target llvm && cmake .. .
I got installation succeed after running the above commands. However, when I run cmake --build . --target test-simple

I got
lit: [workspace]/crab-llvm/tests/lit.cfg:66: fatal: Could not find the clam executable make[3]: *** [tests/CMakeFiles/test-simple] Error 2 make[2]: *** [tests/CMakeFiles/test-simple.dir/all] Error 2 make[1]: *** [tests/CMakeFiles/test-simple.dir/rule] Error 2 make: *** [test-simple] Error 2

Thanks!

Port to LLVM 5.0

Ported code in branch dev-llvm-5.0
Pass all tests
Update .travis to download llvm/clang 5.0

Resolving indirect calls

So, my environment now is:

Ubuntu 18.04.
clang-5.0 (from apt).
crab-llvm on dev-llvm-5.0 branch.

Moreover, I compiled crab by issuing the following commands (by setting a proper value for _DIR_):

mkdir build && cd build
 cmake -DCMAKE_INSTALL_PREFIX=_DIR_ -DUSE_LDD=ON -DUSE_APRON=ON ../
 cmake --build . --target extra                 
 cmake --build . --target crab && cmake ..
 cmake --build . --target ldd && cmake ..
 cmake --build . --target apron && cmake ..
 cmake --build . --target llvm && cmake ..                
 cmake --build . --target install

I tried to analyze this example, namely test.c:

int a (void);
int b (void);

int main(int argc, char** argv) {
  int (*p) (void);
  if (argc == 1)
      p = a;
  else
      p = b;
  int x = p();
  return 0;
}

int a() {return 10;}
int b() {return 5;}

By running:
crabllvm.py test.c --devirt-functions --crab-track=ptr --lower-select

The output is:

function main
_3:
/**
  INVARIANTS: ({}, {})
**/
  goto __@bb_1,__@bb_2;
__@bb_1:
  assume ( = 1);
  goto TrueLowerSelect;
TrueLowerSelect:
/**
  INVARIANTS: ({}, { -> [1, 1]})
**/
  PHILowerSelect = &(a) + 0;
/**
  INVARIANTS: ({}, { -> [1, 1]})
**/
  goto LowerSelect;
LowerSelect:
/**
  INVARIANTS: ({}, {})
**/
  _ret = call seahorn.bounce(PHILowerSelect:ptr);
  @V_7 = 0;
  return @V_7;
/**
  INVARIANTS: ({}, {@V_7 -> [0, 0]})
**/

__@bb_2:
  assume ( != 1);
  goto FalseLowerSelect;
FalseLowerSelect:
/**
  INVARIANTS: ({}, {})
**/
  PHILowerSelect = &(b) + 0;
/**
  INVARIANTS: ({}, {})
**/
  goto LowerSelect;

function a
_ret:
/**
  INVARIANTS: ({}, {})
**/
  @V_9 = 10;
  return @V_9;
/**
  INVARIANTS: ({}, {@V_9 -> [10, 10]})
**/


function b
_ret:
/**
  INVARIANTS: ({}, {})
**/
  @V_10 = 5;
  return @V_10;
/**
  INVARIANTS: ({}, {@V_10 -> [5, 5]})
**/

CRABLLVM WARNING: skipped indirect call. Enable --devirt-functions

function seahorn.bounce
entry:
/**
  INVARIANTS: ({}, {})
**/
  goto __@bb_1,__@bb_2;
__@bb_1:
  assume_ptr(funcPtr == b);
  goto b;
b:
/**
  INVARIANTS: ({}, {})
**/
  _1 = call b();
  UnifiedRetVal = _1;
/**
  INVARIANTS: ({}, {_1-UnifiedRetVal<=0, UnifiedRetVal-_1<=0})
**/
  goto UnifiedReturnBlock;
UnifiedReturnBlock:
/**
  INVARIANTS: ({}, {})
**/
  return UnifiedRetVal;
/**
  INVARIANTS: ({}, {})
**/

__@bb_2:
  assume_ptr(funcPtr != b);
  goto test.a;
test.a:
/**
  INVARIANTS: ({}, {})
**/
  goto __@bb_3,__@bb_4;
__@bb_3:
  assume_ptr(funcPtr == a);
  goto a;
a:
/**
  INVARIANTS: ({}, {})
**/
  _0 = call a();
  UnifiedRetVal = _0;
/**
  INVARIANTS: ({}, {_0-UnifiedRetVal<=0, UnifiedRetVal-_0<=0})
**/
  goto UnifiedReturnBlock;
__@bb_4:
  assume_ptr(funcPtr != a);
  goto default;
default:
/**
  INVARIANTS: ({}, {})
**/
  havoc(_2);
  UnifiedRetVal = _2;
/**
  INVARIANTS: ({}, {_2-UnifiedRetVal<=0, UnifiedRetVal-_2<=0})
**/
  goto UnifiedReturnBlock;
----------------------------------------------------------------------
BRUNCH_STAT Clang 0.02
BRUNCH_STAT CrabLlvm 0.00
BRUNCH_STAT CrabLlvmPP 0.00
----------------------------------------------------------------------

My doubt is double:

How do I interpret the output?
Even if I set --devirt-functions I get CRABLLVM WARNING: skipped indirect call. Enable --devirt-functions in the output. Why?

More general, is there a kind of guide or documentation for crab?

Thanks in advance.

Originally posted by @tregua87 in #24 (comment)

Invariants aren't inserted into LLVM bitcode

Hello again :)

I think that some invariants aren't inserted into the bitcode any more since the last update.

Source file: ex.c
Crabllvm output: crabllvm_log.txt
llvm code - old version: old_main.crab.ll
llvm code - new version: new_main.crab.ll

Old version refers to f45870d
New version refers to bf9965b

Since the last update the invariant {_12-_11<=-91, _11-_12<=91} seems to be missing in the llvm (bit)code.

Thanks for your work

CMake Option Names

Unify all top-level option name. Options related to crab-llvm should start with CLAM, options related to crab should start with CRAB. Options in crab-llvm that relate on how clam configures crab should start with CLAM_CRAB_.

For example,
USE_COTIRE --> CLAM_USE_COTIRE
BUILD_CRABLLVM_LIBS_SHARED --> 'CLAM_SHARED_LIBS ALL_CRAB_DOMAINS-->CLAM_CRAB_ENABLE_ALL_DOMAINS ENABLE_CRAB_INTER-->CLAM_CRAB_ENABLE_INTERPROC CRABLLVM_STATIC_EXE-->CLAM_STATIC_EXE`

ELINA(--crab-dom=opt) uses octagon instead of opt_octagon

Given the description of crab options, I expected crab-llvm to use optimized octagon. This seems to be not the case in the current implementation.

Question: Out of memory when running on a large bitcode file

Hi, I run the following command for clam:

clam php.bc --crab-dom=int --crab-heap-analysis=none --sea-dsa=ci --sea-dsa-devirt=false --crab-check=assert

clam runs out of 200GB of memory and throws out std::bad_alloc exception:

terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
clam(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x1ed804f]
clam(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x1ed62e2]
clam[0x1ed8595]
/lib/x86_64-linux-gnu/libpthread.so.0(+0x12980)[0x7f00769e1980]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xc7)[0x7f007548afb7]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x141)[0x7f007548c921]
/usr/lib/x86_64-linux-gnu/libstdc++.so.6(+0x8c957)[0x7f0075ae1957]
/usr/lib/x86_64-linux-gnu/libstdc++.so.6(+0x92ae6)[0x7f0075ae7ae6]
/usr/lib/x86_64-linux-gnu/libstdc++.so.6(+0x92b21)[0x7f0075ae7b21]
/usr/lib/x86_64-linux-gnu/libstdc++.so.6(+0x92d54)[0x7f0075ae7d54]
/usr/lib/x86_64-linux-gnu/libstdc++.so.6(+0x932dc)[0x7f0075ae82dc]
clam(_ZN6seadsa5Graph6mkNodeEv+0x26)[0x186e546]
clam(_ZN6seadsa5Graph6mkCellERKN4llvm5ValueERKNS_4CellE+0xcb)[0x18702ab]
clam(_ZN6seadsa25CompleteCallGraphAnalysis36cloneAndResolveArgumentsAndCallSitesERKNS_11DsaCallSiteERNS_5GraphES5_b+0x141)[0x18b6a11]
clam[0x18bad7d]
clam(_ZN6seadsa25CompleteCallGraphAnalysis11runOnModuleERN4llvm6ModuleE+0x1273)[0x18b92b3]
clam(_ZN6seadsa17CompleteCallGraph11runOnModuleERN4llvm6ModuleE+0x282)[0x18bb492]
clam(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x3c0)[0xba65b0]
clam(main+0xba4)[0x773644]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7)[0x7f007546dbf7]
clam(_start+0x2a)[0x77274a]
Stack dump:
0.      Program arguments: clam transed.bc --crab-dom=int --crab-heap-analysis=none --sea-dsa=ci --sea-dsa-devirt=false --crab-check=assert 
1.      Running pass 'Complete Call Graph SeaDsa pass' on module 'transed.bc'.
Aborted (core dumped)

The coredump suggests that it is related to the call graph analysis of dsa. However, I think I have already disabled dsa analysis in the above command line. How can I obtain the cheapest (maybe imprecise) command line configuration
for running clam? Thanks for your help.

cannot build crab-llvm due to an ocaml-llvm binding issue

Hi,

When building crab-llvm, I encountered an error at the step:

cmake --build . --target llvm && cmake ..

The reason is due to the compilation of ocaml-llvm binding. Here is the detailed log produced in the file crab-llvm/build/llvm-prefix/src/llvm-stamp/llvm-build-err.log.

File "llvm_executionengine.ml", line 54, characters 28-77:
Error: This expression has type nativeint
       but an expression was expected of type int64
make[6]: *** [bindings/ocaml/executionengine/llvm_executionengine.cma] Error 2
make[5]: *** [bindings/ocaml/executionengine/CMakeFiles/ocaml_llvm_executionengine.dir/all] Error 2
make[4]: *** [all] Error 2

This issue occurs with both OCaml 4.02.3 and OCaml 4.04.0 I googled for the solution of this issue but there is not much information, except the bug report: http://lists.llvm.org/pipermail/llvm-bugs/2015-June/040629.html

Do you know how to overcome this issue?

Thank you!

Question: Why doesn't Clam use SeaDSA's butd-cs analysis?

Potentially silly question, but it will greatly assist in my understanding.

Thanks folks!

Cannot build with shared libraries

From @caballa on April 9, 2017 8:40

Copied from original issue: caballa/crab-llvm#12

Support for multiple input files

use llvm-link to produce a single bc file.

Interprocedural Invariants

Hi,

I have a simple C program like the following:

#include <unistd.h>

int add (int a) {
	if (a > 2)
		a += 4;
	else
		a += 2;
	write(1, "Hello", a);
	return a;
}

int main(int argc, char **argv) {
	int x = 4;
	add(x);
	return 0;
}

I generated the IR for this program and ran crabllvm with the following arguments:

./crabllvm -crab-inter -crab-print-invariants -crab-track=arr -crab-heap-analysis=cs-sea-dsa input.bc

I expected crab to say that a = [4, 4] holds at the entry to add but it says that no invariants hold. Am I correct in this expectation? Thanks!

EDIT: It seems if we change the program to do just add(4) instead of add(x) I see the invariant but I'm not sure if that is to be expected.

Crab CFG has no exit

Hi!

Thanks for your help on previous issues. I'm on llvm-8.0 branch and I'm getting the error CRAB ERROR: CFG has no exit when running crabllvm on this file.

My specific commands are:

./crabllvm -crab-inter -crab-heap-analysis=ci-sea-dsa sshd_pp.bc

Add array graph domain

Replace adapt-rtz domain with a more precise version

From @caballa on October 15, 2016 23:53

It should be replaced by this domain described in Issue #8.

Currenty, adapt-rtz (adaptive reduced product of terms with zones) is really rough. For a given program we determine (via liveness analysis) the maximum number of live variables and fix for the whole program whether running with rtz or intervals. We would like to change from one domain to another at the level of basic block.

Copied from original issue: caballa/crab-llvm#6

Function @verifier.assume has invalid attributes

When using clam to insert invariants, it declares a function @verifier.assume:

; Function Attrs: inaccessiblememonly norecurse nounwind optnone
declare void @verifier.assume(i1) #1

However, attempting to disassemble the bitcode to LLVM IR generates an error as the function should also have the noinline attribute:

Attribute 'optnone' requires 'noinline'!
void (i1)* @verifier.assume
LLVM ERROR: Broken module found, compilation aborted!

I had to patch LLVM to get the .ll file and see what's going on by removing the following line: https://github.com/llvm/llvm-project/blob/97d00b72a2b0a7aca631e1402a647f32c4e8bafb/llvm/lib/IR/Verifier.cpp#L2051-L2052

Analyzing FP programs questions

Hi there!

I'm trying to implement static analysis of floating-point programs. So far when I try to use clam.py float_test.c I don't get any invariant (which makes sense since it only works on integers). I was wondering if I can get some pointers on what would be required to support FP variables in clam so I can try to implement it if possible.

Thank you for all the help!

Not Handled Expression

Hi,

I'm running crab-llvm on llvm-8.0. I am running the anlaysis on the following file and I get this error:

%.pre1 = load i8*, i8** null, align 8, !tbaa !14
main: /home/shankara/crab-llvm/sea-dsa/src/DsaLocal.cc:278: sea_dsa::Cell {anonymous}::BlockBuilderBase::valueCell(const llvm::Value&): Assertion `false && "Not handled expression"' failed.
 #0 0x0000563b7b08b915 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:495:0
 #1 0x0000563b7b08b9a8 PrintStackTraceSignalHandler(void*) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:559:0
 #2 0x0000563b7b08958c llvm::sys::RunSignalHandlers() /home/shankara/llvm-project/llvm/lib/Support/Signals.cpp:69:0
 #3 0x0000563b7b08b337 SignalHandler(int) /home/shankara/llvm-project/llvm/lib/Support/Unix/Signals.inc:358:0
 #4 0x00007f86d0443890 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12890)
 #5 0x00007f86cf73fe97 gsignal /build/glibc-OTsEL5/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
 #6 0x00007f86cf741801 abort /build/glibc-OTsEL5/glibc-2.27/stdlib/abort.c:81:0
 #7 0x00007f86cf73139a __assert_fail_base /build/glibc-OTsEL5/glibc-2.27/assert/assert.c:89:0
 #8 0x00007f86cf731412 (/lib/x86_64-linux-gnu/libc.so.6+0x30412)
 #9 0x0000563b799e0853 (anonymous namespace)::BlockBuilderBase::valueCell(llvm::Value const&) /home/shankara/crab-llvm/sea-dsa/src/DsaLocal.cc:278:0
#10 0x0000563b799e46f5 visitPHINode /home/shankara/crab-llvm/sea-dsa/src/DsaLocal.cc:177:0
#11 0x0000563b799e46f5 visitPHI /usr/local/include/llvm/IR/Instruction.def:208:0
#12 0x0000563b799e46f5 visit /usr/local/include/llvm/IR/Instruction.def:208:0
#13 0x0000563b799e46f5 visit<llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::Instruction, true, false, void>, false, false> > /usr/local/include/llvm/IR/InstVisitor.h:92:0
#14 0x0000563b799e46f5 visit /usr/local/include/llvm/IR/InstVisitor.h:107:0
#15 0x0000563b799e46f5 sea_dsa::LocalAnalysis::runOnFunction(llvm::Function&, sea_dsa::Graph&) /home/shankara/crab-llvm/sea-dsa/src/DsaLocal.cc:1040:0
#16 0x0000563b799c4c2d boost::container::vector<llvm::Function const*, boost::container::new_allocator<llvm::Function const*> >::cend() const /usr/include/boost/container/vector.hpp:1403:0
#17 0x0000563b799c4c2d boost::container::vector<llvm::Function const*, boost::container::new_allocator<llvm::Function const*> >::end() const /usr/include/boost/container/vector.hpp:1351:0
#18 0x0000563b799c4c2d boost::container::container_detail::flat_tree<llvm::Function const*, boost::move_detail::identity<llvm::Function const*>, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::cend() const /usr/include/boost/container/detail/flat_tree.hpp:393:0
#19 0x0000563b799c4c2d boost::container::container_detail::flat_tree<llvm::Function const*, boost::move_detail::identity<llvm::Function const*>, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::priv_insert_unique_prepare(llvm::Function const* const&, boost::container::container_detail::flat_tree<llvm::Function const*, boost::move_detail::identity<llvm::Function const*>, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::insert_commit_data&) /usr/include/boost/container/detail/flat_tree.hpp:1041:0
#20 0x0000563b799c4c2d boost::container::container_detail::flat_tree<llvm::Function const*, boost::move_detail::identity<llvm::Function const*>, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::insert_unique(llvm::Function const*&&) /usr/include/boost/container/detail/flat_tree.hpp:443:0
#21 0x0000563b799c4c2d std::pair<boost::container::container_detail::vec_iterator<llvm::Function const**, false>, bool> boost::container::flat_set<llvm::Function const*, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::priv_insert<llvm::Function const*>(llvm::Function const*&&) /usr/include/boost/container/flat_set.hpp:992:0
#22 0x0000563b799c4c2d boost::container::flat_set<llvm::Function const*, std::less<llvm::Function const*>, boost::container::new_allocator<llvm::Function const*> >::insert(llvm::Function const*&&) /usr/include/boost/container/flat_set.hpp:646:0
#23 0x0000563b799c4c2d sea_dsa::ContextInsensitiveGlobalAnalysis::runOnModule(llvm::Module&) /home/shankara/crab-llvm/sea-dsa/src/DsaGlobal.cc:108:0
#24 0x0000563b7995c084 crab_llvm::SeaDsaHeapAbstraction::SeaDsaHeapAbstraction(llvm::Module&, llvm::CallGraph&, llvm::DataLayout const&, llvm::TargetLibraryInfo const&, sea_dsa::AllocWrapInfo const&, bool, bool, bool, bool) /home/shankara/crab-llvm/lib/CrabLlvm/SeaDsaHeapAbstraction.cc:563:0
#25 0x0000563b79753762 crab_llvm::CrabLlvmPass::runOnModule(llvm::Module&) /home/shankara/crab-llvm/lib/CrabLlvm/CrabLlvm.cc:1419:0
#26 0x0000563b7a06f8d4 (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /home/shankara/llvm-project/llvm/lib/IR/LegacyPassManager.cpp:1744:0
#27 0x0000563b7a0700f7 llvm::legacy::PassManagerImpl::run(llvm::Module&) /home/shankara/llvm-project/llvm/lib/IR/LegacyPassManager.cpp:1857:0
#28 0x0000563b7a070327 llvm::legacy::PassManager::run(llvm::Module&) /home/shankara/llvm-project/llvm/lib/IR/LegacyPassManager.cpp:1889:0
#29 0x0000563b794935ea run_abhaya(llvm::Module&) /home/shankara/abhaya/src/main/main.cpp:65:0
#30 0x0000563b7949390e main /home/shankara/abhaya/src/main/main.cpp:141:0
#31 0x00007f86cf722b97 __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:344:0
#32 0x0000563b794929ea _start (./main+0x11f9ea)
Stack dump:
0.      Program arguments: ./main -crab-heap-analysis=ci-sea-dsa -crab-inter merged_vsftpd_pp.bc

My command is:

./crabllvm -crab-heap-analysis=ci-sea-dsa -crab-inter merged_vsftpd_pp.bc

Thanks!

Seemingly Spurious Bot Invariants Generated

Hi!

I'm seeing a lot of bottom invariants generated when running crab-llvm from the following file. This seems unsound as the program can reach a lot of functions on legitimate inputs in particular function do_authentication2. Any assistance would be great!

./crabllvm -crab-inter -crab-print-invariants -crab-heap-analysis=llvm-dsa sshd_pp.bc

Cannot build crab-llvm due to error: could not find svn for checkout of llvm

Hi,

I follow your tutorial at https://github.com/seahorn/crab-llvm to build crab-llvm but always encounter an issue at the command: cmake --build . --target crab && cmake ...

In brief, the error is: error: could not find svn for checkout of llvm. Below is the detailed log:

-- All crabllvm libraries will be built statically
-- Boost version: 1.58.0
-- All crab libraries will be built dynamically
-- Boost version: 1.58.0
-- The boxes domain will not be available
-- The apron domains will not be available
-- Analysis statistics is enabled
-- Analysis logging for debugging is enabled
CMake Error at /usr/share/cmake-3.5/Modules/ExternalProject.cmake:1720 (message):
  error: could not find svn for checkout of llvm
Call Stack (most recent call first):
  /usr/share/cmake-3.5/Modules/ExternalProject.cmake:2459 (_ep_add_download_command)
  CMakeLists.txt:153 (ExternalProject_Add)


-- Configuring incomplete, errors occurred!
See also "/home/trungtq/workspace/tools/crab-llvm/crab-llvm/build/CMakeFiles/CMakeOutput.log".
Makefile:606: recipe for target 'cmake_check

The commands that I run successful is:

 sudo apt-get install libboost-all-dev libboost-program-options-dev
 sudo apt-get install libgmp-dev
 sudo apt-get install libmpfr-dev	
 mkdir build && cd build
 cmake -DCMAKE_INSTALL_PREFIX=_DIR_ ../

Could you advise whether I do something incorrectly?

Thank you!

install clang-3.8

I am experimenting with crab-llvm.

I installed crab llvm by following the guide in the repo, everything worked well.

However, I have some trouble with clang 3.8.

It is not clear whether I should install clang 3.8 from scratch (and also a parallel llvm installation), or else I should refer to the custom clang repo here (https://github.com/seahorn/clang).

Currently, I am working with Ubuntu 18.04 and the oldest clang in apt is 3.9.

May you give me a clue about this issue, please?

Segmentation Fault During Analysis

Hi!

I'm running crab-llvm with the following commands on this llvm-bitcode and it gives me the crash: