seahorn / crab Goto Github PK

View Code? Open in Web Editor NEW

227.0 12.0 32.0 6.93 MB

A library for building abstract interpretation-based analyses

License: Apache License 2.0

CMake 1.27% C++ 98.23% Shell 0.10% Dockerfile 0.27% Makefile 0.14%

static-analysis abstract-interpretation program-analysis invariants verification

crab's Introduction

About

SeaHorn is an automated analysis framework for LLVM-based languages. This version compiles against LLVM 14.

Some of the supported features are

Abstract Interpretation-based static analysis
Unification-based Context-Sensitive pointer analysis
SMT-based Bounded Model Checking (i.e., symbolic execution)
CHC-based Software Model Checking (i.e., invariant inference)
Executable counterexamples (i.e., no reports, just bugs!)

SeaHorn is developed primarily as a framework for conducting research in automated verification. The frameworks provides many components that can be put together in a variety of ways. However, it is not an "out-of-the-box" static analysis tool.

Many analysis tools and examples are provided with the framework. We are constantly looking for new applications and provide support to new users. For more information on what is happening, check our (infrequently updated) blog.

License

SeaHorn is distributed under a modified BSD license. See license.txt for details.

Introduction

SeaHorn provides a python script called sea to interact with users. Given a C program annotated with assertions, users just need to type: sea pf file.c

The result of sea-pf is unsat if all assertions hold, an sat if any of the assertions are violated.

The option pf tells SeaHorn to translate file.c into LLVM bitcode, generate a set of verification conditions (VCs), and finally, solve them. The main back-end solver is spacer.

The command pf provides, among others, the following options:

--show-invars: display computed invariants if answer was unsat.
--cex=FILE : stores a counter-example in FILE if answer was sat.
-g : compiles with debug information for more trackable counterexamples.
--step=large: large-step encoding. Each transition relation corresponds to a loop-free fragments.
--step=small: small-step encoding. Each transition relation corresponds to a basic block.
--track=reg : model (integer) registers only.
--track=ptr : model registers and pointers (but not memory content)
--track=mem: model both scalars, pointers, and memory contents
--inline : inlines the program before verification
--crab : inject invariants in spacer generated by the Crab abstract-interpretation-based tool. Read here for details about all Crab options (prefix --crab). You can see which invariants are inferred by Crab by typing option --log=crab.
--bmc: use BMC engine.

sea pf is a pipeline that runs multiple commands. Individual parts of the pipeline can be run separately as well:

sea fe file.c -o file.bc: SeaHorn frontend translates a C program into optimized LLVM bitcode including mixed-semantics transformation.
sea horn file.bc -o file.smt2: SeaHorn generates the verification conditions from file.bc and outputs them into SMT-LIB v2 format. Users can choose between different encoding styles with several levels of precision by adding:
- --step={small,large,fsmall,flarge} where small is small step encoding, large is block-large encoding, fsmall is small step encoding producing flat Horn clauses (i.e., it generates a transition system with only one predicate), and flarge: block-large encoding producing flat Horn clauses.
- --track={reg,ptr,mem} where reg only models integer scalars, ptr models reg and pointer addresses, and mem models ptr and memory contents.
sea smt file.c -o file.smt2: Generates CHC in SMT-LIB2 format. Is an alias for sea fe followed by sea horn. The command sea pf is an alias for sea smt --prove.
sea clp file.c -o file.clp: Generates CHC in CLP format.
sea lfe file.c -o file.ll : runs the legacy front-end

To see all the commands, type sea --help. To see options for each individual command CMD (e.g, horn), type sea CMD --help (e.g., sea horn --help).

Static Analysis with Abstract Interpretation

Inference of Inductive Invariants using Crab

SeaHorn does not use Crab by default. To enable Crab, add the option --crab to the sea command.

The abstract interpreter is by default intra-procedural and it uses the Zones domain as the numerical abstract domain. These default options should be enough for normal users. For developers, if you want to use other abstract domains you need to:

Compile with cmake options -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
Run sea with option --crab-dom=DOM where DOM can be:
- int for intervals
- term-int for intervals with uninterpreted functions
- boxes: for disjunctive intervals
- oct for octagons
- pk for polyhedra

To use the crab inter-procedural analysis you need to run sea with option --crab-inter

By default, the abstract interpreter only reasons about scalar variables (i.e., LLVM registers). Run sea with the options --crab-track=mem --crab-singleton-aliases=true to reason about memory contents.

How to use Invariants generated by Crab in Spacer

Crab is mostly path-insensitive while Spacer, our Horn clause solver, is path-sensitive. Although path-insensitive analyses are more efficient, path-sensitivity is typically required to prove the property of interest. This motivates our decision of running first Crab (if option --crab) and then pass the generated invariants to Spacer. There are currently two ways for Spacer to use the invariants generated by Crab. The sea option --horn-use-invs=VAL tells spacer how to use those invariants:

If VAL is equal to bg then invariants are only used to help spacer in proving a lemma is inductive.
If VAL is equal to always then the behavior is similar to bg but in addition invariants are also used to help spacer to block a counterexample.

The default value is bg. Of course, if Crab can prove the program is safe then Spacer does not incur in any extra cost.

Property Specification

Properties are assumed to be assertions. SeaHorn provides a static assertion command sassert, as illustrated in the following example

/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd();

int main(void) {
    int k = 1;
    int i = 1;
    int j = 0;
    int n = nd();
    while (i < n) {
        j = 0;
        while (j < i) {
            k += (i - j);
            j++;
        }
        i++;
    }
    sassert(k >= n);
}

Internally, SeaHorn follows SV-COMP convention of encoding error locations by a call to the designated error function __VERIFIER_error(). SeaHorn returns unsat when __VERIFIER_error() is unreachable, and the program is considered safe. SeaHorn returns sat when __VERIFIER_error() is reachable and the program is unsafe. sassert() method is defined in seahorn/seahorn.h.

Inspect Code

Apart from proving properties or producing counterexamples, it is sometimes useful to inspect the code under analysis to get an idea of its complexity. For this, SeaHorn provides a command sea inspect. For instance, given a C program ex.c type:

sea inspect ex.c --sea-dsa=cs+t --mem-dot

The option --sea-dsa=cs+t enables the new context-, type-sensitive sea-dsa analysis described in FMCAD19. This command generates a FUN.mem.dot file for each function FUN in the input program. To visualize the graph of the main function, use web graphivz interface, or the following commands:

$ dot -Tpdf main.mem.dot -o main.mem.pdf

More details on the memory graphs is in the SeaDsa repository: here.

Use sea inspect --help to see all options. Currently, the available options are:

sea inspect --profiler prints the number of functions, basic blocks, loops, etc.
sea inspect --mem-callgraph-dot prints to dot format the call graph constructed by SeaDsa.
sea inspect --mem-callgraph-stats prints to standard output some statstics about the call graph construction done by SeaDsa.
sea inspect --mem-smc-stats prints the number of memory accesses that can be proven safe by SeaDsa.

Installation

The easiest way to get started with SeaHorn is via a docker distribution.

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

Start with exploring what the sea command can do:

$ sea --help
$ sea pf --help

The nightly tag is automatically refreshed daily and contains the latest development version. We maintain all other tags (that require manual update) infrequently. Check the dates on DockerHub and log an issue on GitHub if they are too stale.

Additional examples and configuration options are on the blog. The blog is updated infrequently. In particular, options change, features are phased out, new things are added. If you find problems in the blog, let us know. We at least will update the blog post to indicate that it is not expected to work with the latest version of the code.

You can also manually install by:

Following the instructions in the Docker file Dockerfile: docker/seahorn-builder.Dockerfile.

If this does not work, run:

$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev*

The first 3 commands will install LLVM 14, the 4th will install libpolly which is wrongly omitted from LLVM 14 (but included in subsequent versions)

Next, follow the instruction in the Docker file above

Developer's Zone

The information from this point on is for developers only. If you would like to contribute to SeaHorn, build your own tools based on it, or just interested in how it works inside, keep reading.

Compilation Instructions

SeaHorn requires LLVM, Z3, and boost. The exact versions of the libraries keep changing, but cmake craft is used to check that right version is available.

To specify a specific version of any of the dependencies, use the usual <PackageName>_ROOT and/or <PackageName>_DIR (see find_package() for details) cmake variables.

SeaHorn is broken into multiple components that live in different repositories (under SeaHorn organization). The build process automatically checks out everything as necessary. For current build instructions, check the CI scripts.

These are the generic steps. Do NOT use them. Read on for a better way:

cd seahorn ; mkdir build ; cd build (The build directory can also be outside the source directory.)
cmake -DCMAKE_INSTALL_PREFIX=run ../ (Install is required!)
cmake --build . --target extra && cmake .. (clones components that live elsewhere)
cmake --build . --target crab && cmake .. (clones crab library)
cmake --build . --target install (build and install everything under run)
cmake --build . --target test-all (run tests)

Note: install target is required for tests to work!

Better Compilation Instructions

For an enhanced development experience:

Use clang
On Linux, use lld linker
Include debug symbols in Release builds
Use Ninja
Export compile_commands.json

On Linux, we suggest the following cmake configuration:

$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run \
      -DCMAKE_BUILD_TYPE=RelWithDebInfo \
      -DCMAKE_CXX_COMPILER="clang++-14" \
      -DCMAKE_C_COMPILER="clang-14" \
      -DSEA_ENABLE_LLD=ON  \
      -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \
      ../ \
      -DZ3_ROOT=<Z3_ROOT> \
      -DLLVM_DIR=<LLMV_CMAKE_DIR> \
      -GNinja
$ (cd .. && ln -sf build/compile_commands.json .)

where <Z3_ROOT is a directory containing Z3 binary distribution, and LLMV_CMAKE_DIR is directory containing LLVMConfig.cmake.

Other legal options for CMAKE_BUILD_TYPE are Debug and Coverage. Note that the CMAKE_BUILD_TYPE must be compatible with the one used to compile LLVM. In particular, you will need a Debug build of LLVM to compile SeaHorn in `Debug** mode. Make sure you have plenty of patience, disk space, and time if you decide to go this route.

Alternatively, the project can be configured using cmake presets. To do this, simply run the following command:

$ cmake --preset <BUILD_TYPE>-<PRESET_NAME>

to configure cmake, where <BUILD_TYPE> is one of: Debug, RelWithDebInfo or Coverage and <PRESET_NAME> is the preset you would like to use. The presets that are currently available are: jammy. These presets assume that you have Z3 installed in /opt/z3-4.8.9 and Yices installed in /opt/yices-2.6.1.

This will also allow the project to be configured and compiled within VS Code using the CMake Tools extension.

If you would like to use different compilation settings or if you have Z3 or Yices installed in any other directory, you will need to make your own CMakeUserPresets.json file with your own presets.

Compiling on a Mac

Do not include -DSEA_ENABLE_LLD=ON. The default compiler is clang, so you might not need to set it explicitly.

The EXTRA Target

SeaHorn provides several components that are automatically cloned and installed via the extra target. These components can be used by other projects outside of SeaHorn.

sea-dsa: git clone https://github.com/seahorn/sea-dsa.git

sea-dsa is a new DSA-based heap analysis. Unlike llvm-dsa, sea-dsa is context-sensitive and therefore, a finer-grained partition of the heap can be generated in presence of function calls.
clam: git clone https://github.com/seahorn/crab-llvm.git

clam provides inductive invariants using abstract interpretation techniques to the rest of SeaHorn's backends.
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git

llvm-seahorn provides tailored-to-verification versions of InstCombine and IndVarSimplify LLVM passes as well as a LLVM pass to convert undefined values into nondeterministic calls, among other things.

SeaHorn doesn't come with its own version of Clang and expects to find it either in the build directory (run/bin) or in PATH. Make sure that the version of Clang matches the version of LLVM that was used to compile SeaHorn (currently LLVM14). The easiest way to provide the right version of Clang is to download it from llvm.org, unpact it somewhere and create a symbolic link to clang and clang++ in run/bin.

$ cd seahorn/build/run/bin
$ ln -s <CLANG_ROOT>/bin/clang clang
$ ln -s <CLANG_ROOT>/bin/clang++ clang++

where <CLANG_ROOT> is the location at which Clang was unpacked.

Tests

Testing infrastructure depends on several Python packages. These have their own dependencies. If you cannot figure them out, use docker instead.

$ pip install lit OutputCheck networkx pygraphviz

Coverage

We can use gcov and lcov to generate test coverage information for SeaHorn. To build with coverage enabled, we need to run build under a different directory and set CMAKE_BUILD_TYPE to Coverage during cmake configuration.

Example steps for generating coverage report for the test-opsem target:

mkdir coverage; cd coverage create and enter coverage build directory
cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../
Complete the build as usual
cmake --build . --target test-opsem Run OpSem tests, now .gcda and .gcno files should be created in the corresponding CMakeFiles directories
lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info collect coverage data from desired module, if clang is used as the compiler instead of gcc, create a bash script llvm-gcov.sh:

#!/bin/bash
exec llvm-cov gcov "$@"

$ chmod +x llvm-gcov.sh

then append --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh to the lcov -c ... command. 6. extract data from desired directories and generate html report:

lcov --extract coverage.info "*/lib/seahorn/*" -o lib.info
lcov --extract coverage.info "*/include/seahorn/*" -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report

then open coverage_report/index.html in browser to view the coverage report

Also see scripts/coverage for scripts used by the CI. Coverage report for nightly builds is available at codecov

Code indexing

Compilation database for the seahorn project and all its sub-projects is generated using -DCMAKE_EXPORT_COMPILE_COMMANDS=ON option for cmake.

An easy way to get code indexing to work with with compilation database support is to link the compilation_database.json file into the main project directory and follow instructions specific to your editor.

Clion -- https://www.jetbrains.com/help/clion/compilation-database.html
Vim (YouCompleteMe) -- instructions
Emacs -- use lsp-ui with clangd which are available in spacemacs develop branch

Remote Configuration for CLion

For a detailed guide for a remote workflow with CLion check Clion-configuration.

Remote Configuration for Emacs (and other Editors)

Use our fork of mainframer. Don't miss the example configuration.

Contributors

crab's People

Contributors

Stargazers

Watchers

crab's Issues

Possibly stack overflow while computing WTO of a large CFG

Problem07_label52_true-unreach-call.pp.bc.zip

Command to reproduce the problem using crab-llvm:

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.

An instance of boxes domain can be in an inconsistent state due to global state

From @caballa on June 25, 2017 21:40

A crab variable can contain a pointer (e.g., crab-llvm stores Value* in a crab variable and seahorn stores Expr). This is very useful when we want to map back crab results to the client. The boxes domain keeps a global map from variables to internal ids. If the destructor of the factory that created the pointer to Value or Expr is called before than the global map is released then it leaves the instance of the boxes domain in an inconsistent state.

Copied from original issue: caballa/crab#17

More precise bitwise AND

x & K can at least be inferred to be <= K. This is not the case currently.

Question regarding "cyclic" encoding and propagation of analysis results

I want to analyze PLC programs which exhibit "cyclic" behavior using symbolic execution but sometimes the code is written poorly and there are unreachable branches. For this purpose I need some kind of value-set analysis, but I stumbled upon a few problems. Here is an example of a simple program as a crab cfg:

void declare main()
initialization:
  cycle = 0;
  x = 0;
  goto main_entry;
main_entry:
  assume(cycle <= 100);
  goto cycle_entry;
cycle_entry:
  cycle = cycle+1;
  goto main_body;
main_body:
  x_res:int32 = call increment(x:int32);
  goto cycle_exit;
cycle_exit:
  x = x_res;
  goto main_entry,main_exit;
main_exit:
  assume(-cycle < -100);

x_out:int32 declare increment(x_in:int32)
entry:
  goto body;
body:
  x_out = x_in+1;
  goto exit;
exit:

The program should simply increment the value of x by 1 through the use of a function call in each "iteration" for a couple of "cycles".

Using the top-down interprocedural analyzer with the boxes domain of the ldd library I get the following invariants:

Callgraph=
main--> increment
=================================
void declare main()
cycle_exit={-cycle <= -1; cycle <= 101; -x <= -1; -x_res <= -1}
main_exit={-cycle <= -101; cycle <= 101; -x <= -1; -x_res <= -1}
main_body={-cycle <= -2; cycle <= 101; -x <= -1; -x_res <= -1} or 
{-cycle <= -1; cycle <= 1; -x <= 0; x <= 0; -x_res <= -1}
cycle_entry={-cycle <= -2; cycle <= 101; -x <= -1; -x_res <= -1} or 
{-cycle <= -1; cycle <= 1; -x <= 0; x <= 0}
main_entry={-cycle <= -1; cycle <= 100; -x <= -1; -x_res <= -1} or 
{-cycle <= 0; cycle <= 0; -x <= 0; x <= 0}
initialization={-cycle <= 0; cycle <= 0; -x <= 0; x <= 0}
=================================
x_out:int32 declare increment(x_in:int32)
exit={-x_in <= 0; -x_out <= -1}
body={-x_in <= 0; -x_out <= -1}
entry={-x_in <= 0}
=================================

I would have expected that the value of x is propagated, e.g., main_exit={x>=1;x<=101,...} and that the generated function summary holds must summaries for each valuation of x_in, e.g., x_in = 0, x_in = 1, x_in = 2, ....

What is wrong with my encoding?

Make generic weights of adaptative sparse graph

adapt_sgraph.hpp assumes that the graph weights are basic types. The assumption for basic types is because we use memcpy and realloc for efficiency reasons. Thus, to use bignums as weights we should change the implementation which might affect performance. The changes are needed here:

domains/graphs/adapt_sgraph.hpp
domains/graphs/util/Vec.h

This is related to issue #21. Thanks to @elazarg to bring it in!

Adapt numerical domains for supporting reals

From @caballa on October 15, 2016 23:18

For intervals and zones, we need at least:

make sure rounding is correct (e.g., if upper bounds towards +oo, etc)
make sure division is correct
etc.

Copied from original issue: caballa/crab#4

Does crab support running on MacOS?

If so, is there any related installation document on MacOS? Thank you very much!

Improve precision of boxes when constraints that involve more than one variable

From @caballa on June 30, 2017 16:49

If we have x - y + z >= 5 we can translate into three interval constraints:

x >= Intervals(y-z) + 5
y <= Intervals(x+z) - 5
z >= Intervals(y-x) + 5

where Intervals evaluate each variable to an interval constraint.

Copied from original issue: caballa/crab#19

Extend linear_constraints to strict inequalities

Strict inequalities are needed for rationals. For integers we can always replace
x < y with x <= y-1. This issue is related to issue #10 .

Add new operations to abstract_domain virtual class

extend abstract_domain api with the operations from domain_traits_api:
- expand
- forget
- project
remove domain_traits_api

General question on "backward_assign_operations"

Two questions:

Is it possible to use crab's "backwards assignment"s to calculate inputs at the "beginning" of a program? For example:

void foo(int y)
{
    y++;
    if (y > 10); // <-- if this was SSA, it would be something like "y__0 > 9"
}

Are there any domains which support wrapped bit vectors and "work backwards"?

"compress" `powerset_domain` domain after projection

Current status

I have code that looks like this:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

using analysis_domain = powerset_of_z_wrapped_intervals;

int main(void) {
  variable_factory_t vfac;
  z_var y(vfac["y"], crab::INT_TYPE, 32);
  z_var x(vfac["x"], crab::INT_TYPE, 32);

  analysis_domain d1;
  d1 += (y > 10);
  d1.assign(x, 0);

  analysis_domain d2;
  d2 += (y > 20);
  d2.assign(x, 1);

  analysis_domain d3;
  d3 += (y > 30);
  d3.assign(x, 2);

  analysis_domain d4 = d1 | d2 | d3;
  crab::outs() << d4 << "\n\n\n";

  std::vector<z_var> vars;
  vars.push_back(x);

  analysis_domain proj = d4;
  proj.project(vars);
  crab::outs() << proj << "\n\n\n";

  return 0;
}

(the code is purposely brain-dead, but that's fine)

Which gives this:

{y -> [[11, 2147483647]]_32; x -> [[0, 0]]_32} or
{y -> [[21, 2147483647]]_32; x -> [[1, 1]]_32} or
{y -> [[31, 2147483647]]_32; x -> [[2, 2]]_32}


{x -> [[0, 0]]_32} or
{x -> [[1, 1]]_32} or
{x -> [[2, 2]]_32}

Question

After doing the projection, I get a powerset domain that has three elements (0, 1 and 2). Is it possible to ask crab to "compress" this domain into a single range of [0, 2]?

Python API

From @caballa on April 17, 2017 4:40

Copied from original issue: caballa/crab#16

none-optional dereference on array-expansion domain with elina-pk

The issue seem to come from array_expansion.hpp:1287 - missing if (!ignore_array_store) in the condition.

Valgrind traceback:

ebpf-verifier (post-submission)$ valgrind ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==31540== Memcheck, a memory error detector
==31540== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==31540== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==31540== Command: ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==31540== 
exception vector product
exception vector product
exception vector product
exception vector product
check: /usr/include/boost/optional/optional.hpp:1205: boost::optional<T>::reference_type boost::optional<T>::get() [with T = ikos::z_number; boost::optional<T>::reference_type = ikos::z_number&]: Assertion `this->is_initialized()' failed.
==31540== 
==31540== Process terminating with default action of signal 6 (SIGABRT)
==31540==    at 0x5967077: raise (raise.c:51)
==31540==    by 0x5948534: abort (abort.c:79)
==31540==    by 0x594840E: __assert_fail_base.cold.0 (assert.c:92)
==31540==    by 0x5958141: __assert_fail (assert.c:101)
==31540==    by 0x31666E: get (optional.hpp:1205)
==31540==    by 0x31666E: operator* (optional.hpp:1222)
==31540==    by 0x31666E: crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >::array_store_range(ikos::variable<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>) (array_expansion.hpp:1287)
==31540==    by 0x317107: crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::exec(crab::cfg::array_store_stmt<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>&) (abs_transformer.hpp:518)
==31540==    by 0x2ACA8E: crab::analyzer::fwd_analyzer<crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > > >::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >&) (fwd_analyzer.hpp:80)
==31540==    by 0x2B4E71: ikos::interleaved_fwd_fixpoint_iterator_impl::wto_iterator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::visit(ikos::wto_vertex<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >&) (fwd_fixpoint_iterators.hpp:419)
==31540==    by 0x201409: ikos::wto<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >::accept(ikos::wto_component_visitor<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >*) (wto.hpp:743)
==31540==    by 0x1D2C79: run (fwd_fixpoint_iterators.hpp:261)
==31540==    by 0x1D2C79: Run (fwd_analyzer.hpp:138)
==31540==    by 0x1D2C79: run (fwd_analyzer.hpp:285)
==31540==    by 0x1D2C79: crab::checker::checks_db analyze<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >(crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&) (crab_verifier.cpp:156)
==31540==    by 0x1DA725: std::_Function_handler<crab::checker::checks_db (crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&), crab::checker::checks_db (*)(crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&)>::_M_invoke(std::_Any_data const&, crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&) (std_function.h:283)
==31540==    by 0x1D14F5: operator() (std_function.h:687)
==31540==    by 0x1D14F5: analyze (crab_verifier.cpp:232)
==31540==    by 0x1D14F5: abs_validate(Cfg const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, program_info) (crab_verifier.cpp:72)
==31540== 
==31540== HEAP SUMMARY:
==31540==     in use at exit: 463,322,523 bytes in 4,653,262 blocks
==31540==   total heap usage: 48,232,624 allocs, 43,579,362 frees, 4,789,812,024 bytes allocated
==31540== 
==31540== LEAK SUMMARY:
==31540==    definitely lost: 2,784,843 bytes in 142,118 blocks
==31540==    indirectly lost: 326,439 bytes in 16,535 blocks
==31540==      possibly lost: 155,348,967 bytes in 1,107,462 blocks
==31540==    still reachable: 304,862,274 bytes in 3,387,147 blocks
==31540==         suppressed: 0 bytes in 0 blocks
==31540== Rerun with --leak-check=full to see details of leaked memory
==31540== 
==31540== For counts of detected and suppressed errors, rerun with: -v
==31540== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
Aborted (core dumped)

Restrict API of CFG array_assume method

From @caballa on June 25, 2017 23:18

it takes two parameters that delimits a symbolic interval: lower and upper bounds, which can only be number or variables but the current type is a linear expression. So it's more general than it should be.

Copied from original issue: caballa/crab#18

Compiler warning with `dev`

I tried playing with the dev branch today (71fea99), but got this warning:

In file included from /home/avj/clones/crab/dev/build/_INSTALL_DIR_/../../tests/./crab_dom.hpp:6,
                 from /home/avj/clones/crab/dev/build/_INSTALL_DIR_/../../tests/common.hpp:6,
                 from 01_simple_crab.cpp:1:
/home/avj/clones/crab/dev/build/_INSTALL_DIR_/crab/include/crab/domains/array_adaptive.hpp:64:35: warning: comparison between ‘enum crab::domains::array_adaptive_impl::DefaultParams::<unnamed>’ and ‘enum crab::domains::array_adaptive_impl::DefaultParams::<unnamed>’ [-Wenum-compare]
   static_assert(max_array_size <= max_smashable_cells,
                                   ^~~~~~~~~~~~~~~~~~~
/home/avj/clones/crab/dev/build/_INSTALL_DIR_/crab/include/crab/domains/array_adaptive.hpp:77:35: warning: comparison between ‘enum crab::domains::array_adaptive_impl::NoSmashableParams::<unnamed>’ and ‘enum crab::domains::array_adaptive_impl::NoSmashableParams::<unnamed>’ [-Wenum-compare]
   static_assert(max_array_size <= max_smashable_cells,

It seems that this is a legitimate issue, as max_array_size and max_smashable_cells come from different enums.

GCC version

g++ (GCC) 8.3.1 20191121 (Red Hat 8.3.1-5)
Copyright (C) 2018 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Bug in flat_boolean_domain

This line looks very suspicious. Shouldn't the inequation be the other way around? I didn't try to create an example that triggers the bug (if it is one), I just stumbled across this line when I was looking at the code to understand how Booleans are handled.

Enhance top-down inter-procedural analysis

analysis of recursive functions in a precise way
backward analysis

Optimize/cleanup array graph domain

From @caballa on April 9, 2017 8:34

The current implementation works for toy programs but two main things
must to be done for being able to analyze real programs:

landmarks must be kept as local state as part of each abstract
state.
reduction between scalar and weight domains must be done
incrementally. For that, we need some assumptions about the
underlying scalar domain. For instance, if we assume zones then
after each operation we know which are the indexes affected by
the operation. We can use that information for doing reduction
only on those indexes. This would remove the need of having
methods such as array_sgraph_domain_traits::is_unsat and
array_sgraph_domain_traits::active_variables which are anyway
domain dependent.

Copied from original issue: caballa/crab#15

Bug with apron-domains and rationals

From @caballa on February 16, 2017 21:22

Added test case in branch crab2 (commit 9a21877) that triggers the bug.
The test is actually quite simple. If we just add two constraints x >= 1/2 and x <= 1/2 we get bottom rather than x = 1/2.

If we use integers we get the expected result so something is wrong with how we handle rationals.

Copied from original issue: caballa/crab#12

Reduce compilation time

Elina does not compile on mac: `'stdlib.h' file not found`

(seems like an issue in elina, but I thought it might be helpful to open it here)

ebpf-verifier$ make crab_install
[...]
[ 75%] Performing build step for 'elina'
CMake Error at [...]/workspace/ebpf-verifier/external/crab/build/elina-prefix/src/elina-stamp/elina-build-RelWithDebInfo.cmake:16 (message):
  Command failed: 2

   'make' 'CC=/Library/Developer/CommandLineTools/usr/bin/cc' 'CXX=/Library/Developer/CommandLineTools/usr/bin/c++' 'IS_VECTOR=-DVECTOR' 'ELINA_PREFIX=[...]/workspace/ebpf-verifier/external/crab/build/run/elina' 'GMP_PREFIX=/usr/local' 'MPFR_PREFIX=/usr/local'

  See also

    [...]/workspace/ebpf-verifier/external/crab/build/elina-prefix/src/elina-stamp/elina-build-*.log

make[4]: *** [elina-prefix/src/elina-stamp/elina-build] Error 1
make[3]: *** [CMakeFiles/elina.dir/all] Error 2
make[2]: *** [CMakeFiles/elina.dir/rule] Error 2
make[1]: *** [elina] Error 2
make: *** [crab_install] Error 2

Error:

$ cat elina-build-err.log
clang: warning: -lmpfr: 'linker' input unused [-Wunused-command-line-argument]
clang: warning: -lgmp: 'linker' input unused [-Wunused-command-line-argument]
clang: warning: -lm: 'linker' input unused [-Wunused-command-line-argument]
clang: warning: argument unused during compilation: '-L../elina_linearize' [-Wunused-command-line-argument]
elina_scalar.c:27:10: fatal error: 'stdlib.h' file not found
#include <stdlib.h>
         ^~~~~~~~~~
1 error generated.
make[6]: *** [elina_scalar.o] Error 1
make[5]: *** [c] Error 2

Add widening with thresholds in apron domains

It requires to implement make_thresholds in apron_domains.hpp.

There are at least two examples:

tests/domains/test2-rat.cc
tests/domains/test3-rat.cc

that would be benefit.

Copy-on-write optimization in apron_domains, split_dbm, and sparse_dbm seems flaky

I noticed some cases with split_dbm and sparse_dbm where the analysis does not converge because one of the widening operands is wrong due to COW. For now, I decide to disable COW but with some time I should revisit it and fix it.

For future debugging (it requires to use crab-llvm)

crabllvm ./simple_array_index_value_true-unreach-call4_true-termination.pp.bc --crab-turn-undef-nondet --crab-lower-select --crab-dom=zones --crab-inter-sum-dom=zones --crab-widening-delay=2 --crab-widening-jump-set=0 --crab-narrowing-iterations=2 --crab-relational-threshold=10000 --crab-track=arr --crab-singleton-aliases --crab-add-invariants=none --crab-check=assert --crab-stats

cow_bug_program.zip

Valgrind warnings

Running valgrind when using the sdbm domain I get a warning about "use of uninitialized value of size 8" and "Conditional jump depends on uninitialized value" in this line.

I'm not sure which of the variables triggers this error; I would guess it's the dense field since it is of size 8.

(I used the file samples/self/accept_DIV32_overflow_check_1.3 in the bpf verifier)

g++-8:

g++-8 now warns about "writing to an object of non-trivially copyable type" using memcpy:

crab/install/include/crab/domains/graphs/adapt_sgraph.hpp:59:15: 
   error: ‘void* memcpy(void*, const void*, size_t)’
   writing to an object of non-trivially copyable type ‘class crab::AdaptSMap<long unsigned int>::elt_t’; 
   use copy-assignment or copy-initialization instead [-Werror=class-memaccess]
         memcpy(dense, o.dense, sizeof(elt_t)*sz);
         ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The warning is enabled automatically on -Wall.

Add a logico-numerical abstract domain

From @caballa on October 15, 2016 23:32

One simple option is to integrate BDDApron but it is implemented in OCaml so it will add more dependencies to Crab and it would still require changes for supporting Crab domains.

Instead, I prefer to re-implement BDDApron by combining the ADD library (MTBDD) provided by CUDD with the existing Crab domains.

Copied from original issue: caballa/crab#6

Should we add the bitwise complement (~) operation in Crab?

I noticed that this bitwise operation type is not included in Crab, and there is no need to add specialized abstraction design of this operation for each abstract domain in Crab. So, should we add the bitwise complement (~) operation in Crab? Or perhaps we have already implemented this operation in some other way, since -x = ~x +1 ?

Integrate new ELINA

What is the difference between the wrapped_interval implemented in crab and the one implemented in TOPLAS15 paper?

I noticed that these operations are not implemented in crab's wrapped_interval:

/// wrapped_interval_domain implements only standard abstract
/// operations of a numerical domain so it is intended to be used as
/// a leaf domain in the hierarchy of domains.
BOOL_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t)
ARRAY_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t)
REGION_AND_REFERENCE_OPERATIONS_NOT_IMPLEMENTED(wrapped_interval_domain_t)
DEFAULT_SELECT(wrapped_interval_domain_t)

Can this implementation retain the ideas of the TOPLAS15 paper?

For example, to handle branch condition like s < t, the paper update s and t respectively. But, in crab, we may transform this condition to a linear constraint s - t < 0, and solve this? Does this handling method safe in machine integer operation semantics?

I'm not very familiar with crab.

How to correctly represent "else" when manually working with `powerset_domain`

Current situation

Following on from #34, I am able to successfully represent something like:

void foo(int y) {
  int w = 0;
  if (y > 10) {
    w = 1;
  } else {
    w = 2;
  }
}

which I can correctly encode and obtain:

{y -> [[11, 2147483647]]_32; w -> [[2, 2]]_32} or
{y -> [[-2147483648, 10]]_32; w -> [[3, 3]]_32}

My code looks like this like:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

using analysis_domain = powerset_of_z_wrapped_intervals;

int main(void) {
  variable_factory_t vfac;
  z_var y(vfac["y"], crab::INT_TYPE, 32);
  z_var w(vfac["w"], crab::INT_TYPE, 32);

  analysis_domain start;
  start.assign(w, 0);

  analysis_domain tt_1 = start;
  tt_1 += (y > 10);
  tt_1.assign(w, 1);

  analysis_domain ff_1 = start;
  ff_1 += (y <= 10);
  ff_1.assign(w, 2);

  analysis_domain after1 = tt_1 | ff_1;
  crab::outs() << after1 << "\n\n\n";
 
  return 0;
}

Current issue

However, I am not sure how to encode things when the condition in the false branch is "more complicated":

void foo(int y) {
  int w = 0;
  if (y > 10 && y < 20) {
    w = 1;
  } else {
    w = 2;
  }
}

(notice the if now contains a conjunction)

While encoding the true branch is fine:

  analysis_domain tt_1 = start;
  tt_1 += (y > 10);
  tt_1 += (y < 20);
  tt_1.assign(w, 1);

the false branch is more complicated:

  analysis_domain ff_1 = start;
  ff_1 += (y <= 10);
  ff_1 += (y >= 20);
  ff_1.assign(w, 2);

because it seems that crab says that this is bottom.

Question

What is the best way to represent the negation of a conditional that contains Booleans when working with crab?

Is there a simple way to build up a Boolean expression, and then use that both positively and then negate it (to represent an else)? It is fine if I need to manually build-up the else, but I'm really unsure about how to encode it.

Adaptative domain between a relational and non-relational domain

From @caballa on October 15, 2016 23:37

Create a combined domain between e.g., (zones x terms) and intervals such that the domain is zones x terms if the number of variables does not exceed a threshold, otherwise it degrades to intervals.

Copied from original issue: caballa/crab#8

Question: "range of intervals"

Hi,

I just started playing around with crab (so I am very inexperienced here!) and I wanted to model something like this:

void foo(int x) {
  int y = 0;
  if (x >= 10 && x <= 20) {
    y = x;
  } else if (x >= -20 && x <= -10) {
    y = x;
  } else {
    y = 0;
  }

  // y = ([-20, -10], [0], [10, 20])

  ++y;

  // y = ([-10, -9], [1], [11, 21])
}

Using one of the examples, I got this far:

#include <crab/common/types.hpp>
#include <crab/config.h>
#include <crab/domains/wrapped_interval_domain.hpp>
#include <crab/numbers/wrapint.hpp>
#include <iostream>

using namespace std;
using namespace crab::domains;

typedef wrapped_interval<ikos::z_number> wrapped_interval_t;

int main(void) {
  wrapped_interval_t i1(crab::wrapint(10, 32), crab::wrapint(20, 32));
  wrapped_interval_t i2(crab::wrapint(-10, 32), crab::wrapint(-20, 32));
  crab::outs() << "i1 & i2: " << (i1 & i2) << "\n";
  return 0;
}

but this just seems to expand the domain to be [-20, 20], rather than join the "disjointly" (apologies for wrong terminology) -- that is, what I want is ([-20, -10], [10, 20]).

Is this something I can do with crab or are these just "disjoint intervals" not possible with the library?

Thanks!

Zones domains (sparse_dbm and split_dbm): implement narrowing, widening w/thresholds, strict inequalities, and disequations

widening with thresholds
narrowing
strict inequalities for integers
disequations (similar precision as intervals)

From @caballa on October 15, 2016 23:33

Copied from original issue: caballa/crab#7

zones with bignum seems to be imprecise for computing summaries

The tests

simple/test-arr-4.c
simple/test-arr-4.unsafe.c
simple/fntest-1.c
simple/fntest-1.unsafe.c

from crab-llvm do not pass if we use:

  typedef SDBM_impl::BigNumDefaultParams<number_t> SplitDBMGraph;
  typedef SplitDBM<number_t, varname_t, SplitDBMGraph> BASE(split_dbm_domain_t);

in include/crab_llvm/crab_domains.hh

Question regarding the CFG input encoding for the analysis

Hello, this might be a silly question but I can not wrap my head around on how to encode my cfg representation to the crab cfg representation properly. Consider given the following program P:

As I can not express statements such as NOT(activate) AND b I converted my input to SSA and three-address code as follows:

where SEQ is simply my representation of a basic block. The marshaling to crab looks as follows:

entry:
  havoc(P.activate_1003);
  goto bb_1;
bb_1:
  P.v_bool_1001 = true;
  P.b_1002 = P.v_bool_1001;
  goto bb_2;
bb_2:
  P.temp_0 = not(P.activate_1003);
  P.temp_1 = P.temp_0&P.b_1002;
  goto bb_3,bb_4;
bb_3:
  assume(P.temp_1);
  P.v_int_1004 = 0;
  P.y_1005 = P.v_int_1004;
  goto exit;
exit:

bb_4:
  assume(not(P.temp_1));
  P.temp_2 = not(P.b_1002);
  P.temp_3 = P.activate_1003|P.temp_2;
  goto bb_5,bb_6;
bb_5:
  assume(P.temp_3);
  P.v_int_1006 = 1;
  P.y_1007 = P.v_int_1006;
  goto exit;
bb_6:
  assume(not(P.temp_3));
  P.v_int_1008 = 2;
  P.y_1009 = P.v_int_1008;
  goto exit;

and running a forward analysis using a flat boolean numerical domain with intervals results in the following output:

bb_6:({P.b_1002 -> true; P.temp_1 -> false; P.temp_2 -> false; P.v_bool_1001 -> true}, {})
bb_5:({P.b_1002 -> true; P.temp_1 -> false; P.temp_2 -> false; P.v_bool_1001 -> true}, {})
bb_3:({P.b_1002 -> true; P.v_bool_1001 -> true}, {})
bb_4:({P.b_1002 -> true; P.v_bool_1001 -> true}, {})
bb_2:({P.b_1002 -> true; P.v_bool_1001 -> true}, {})
bb_1:({}, {})
exit:({P.b_1002 -> true; P.v_bool_1001 -> true}, {})
entry:({}, {})

which, sadly, is not helpful to me. I was hoping to detect the unreachability of bb_6, but the information of the value P.activate_1003 is dropped somewhere in between. Any hints on how to encode my problem instance properly such that information is not dropped?

Reaching Definitions Analysis

Hello, is it possible to add a reaching definitions analysis to this framework to obtain a data dependence graph?
I am interested in obtaining a program dependence graph of a control flow graph, however, currently only the control dependence graph is obtainable.

Improve precision and performance of backward operations

Create tree expressions and adapt abstract domains to use them

Abstract domains only support arithmetic operations in three-address form (e.g., +,-,*,/) and addition of linear constraints.

Abstract domains do not support addition of non-linear constraints. Moreover, linear constraints are simplified on-the-fly to keep a normalized form. This does not work well if linear constraints are defined over machine arithmetic because those simplifications are not sound. To address these issues, we should have tree expressions (similar to those defined by Apron) which can be converted to linear constraints (if possible/wanted) by each abstract domain.

Implement a sound domain for machine integer arithmetic

The wrapped interval domain is a good candidate:
https://jorgenavas.github.io/papers/wrapped-intervals-aplas12.pdf

CMake Options

CMake top-level options should be prefixed with CRAB. For example,

USE_LDD --> CRAB_ENABLE_LDD
USE_APRON --> CRAB_ENABLE_APRON

etc.

seahorn / crab Goto Github PK

crab's Introduction

About

License

Introduction

Static Analysis with Abstract Interpretation

Inference of Inductive Invariants using Crab

How to use Invariants generated by Crab in Spacer

Property Specification

Inspect Code

Installation

Developer's Zone

Compilation Instructions

Better Compilation Instructions

Compiling on a Mac

The EXTRA Target

Tests

Coverage

Code indexing

Remote Configuration for CLion

Remote Configuration for Emacs (and other Editors)

Contributors

crab's People

Contributors

Stargazers

Watchers

Forkers

crab's Issues

Current status

Question

Current situation

Current issue

Question

Recommend Projects

Recommend Topics

Recommend Org