Git Product home page Git Product logo

2ls's Introduction

Build Status

About

2LS ("tools") is a verification tool for C programs. It is built upon the CPROVER framework (cprover.org), which supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It allows verifying array bounds (buffer overflows), pointer safety, exceptions, user-specified assertions, and termination properties. The analysis is performed by template-based predicate synthesis and abstraction refinements techniques.

License

4-clause BSD license, see LICENSE file.

Overview

2LS reduces program analysis problems expressed in second order logic such as invariant or ranking function inference to synthesis problems over templates. Hence, it reduces (an existential fragment of) 2nd order Logic Solving to quantifier elimination in first order logic.

The current tool has following capabilities:

  • function-modular interprocedural analysis of C code based on summaries
  • summary and invariant inference using generic templates
  • combined k-induction and invariant inference
  • incremental bounded model checking
  • function-modular termination analysis
  • non-termination analysis

Releases

Download using git clone http://github.com/diffblue/2ls; cd 2ls; git checkout 2ls-x.y

Software Verification Competition Contributions

Installation

cd 2ls; ./install.sh

Run src/2ls/2ls

Command line options

The default abstract domain are intervals. If no options are given a context-insensitive interprocedural analysis is performed. For context-sensitivity, add --context-sensitive.

Other analyses include:

  • BMC: --inline --havoc --unwind n
  • Incremental BMC: --incremental-bmc
  • Incremental k-induction: --havoc --k-induction
  • Incremental k-induction and k-invariants (kIkI): --k-induction
  • Intraprocedural abstract interpretation with property checks: --inline
  • Necessary preconditions: --preconditions
  • Sufficient preconditions: --preconditions --sufficient

Currently the following abstract domains are available:

  • Intervals (default): --intervals
  • Zones: --zones
  • Octagons --octagons
  • Equalities/disequalities: --equalities
  • The abstract domain consisting of the Top element: --havoc

Since release 0.6:

  • Heap abstract domain: --heap

Since release 0.7:

  • Heap abstract domain with intervals or zones: --heap-[intervals|zones]
  • Heap abstract domain with intervals or zones and loop paths: --heap-[intervals|zones] --sympath

Interprocedural Termination Analysis

Is supported by release 0.1 and >=0.3.

  • Universal termination: --termination
  • Context-sensitive universal termination: --termination --context-sensitive
  • Sufficient preconditions for termination --termination --context-sensitive --preconditions

Since release 0.6:

  • Nontermination analysis: --non-termination

Features in development

Publications

Contributors

  • Björn Wachter
  • Cristina David
  • Daniel Kroening
  • Hongyi Chen
  • Madhukar Kumar
  • Martin Brain
  • Martin Hruska
  • Peter Schrammel
  • Rajdeep Mukherjee
  • Samuel Bücheli
  • Saurabh Joshi
  • Stefan Marticek
  • Viktor Malik

Contact

Peter Schrammel

2ls's People

Contributors

frnecas avatar martinhruska avatar marusak avatar peterschrammel avatar viktormalik avatar

Watchers

avatar avatar avatar

Forkers

martinhruska marusak

2ls's Issues

Checking validity of heap object concretisation (p'obj.next).

  • currently, we transform an assignment with memory access at right hand side into SSA as follows:
    a = p->next (original assignment in C/GOTO program)
    a#cur-loc == p'obj.next#last-loc (SSA equality where cur-loc is the current location and last-loc is the location of the last assignment of p'obj.next)

  • this transformation is done by method local_SSAt::build_transfer
    we check whether p'obj.next has been defined before (function all_symbolic_deref_called at line 469 in local_ssa.cpp)

  • but we also need to check whether p has not changed since last assignment of p'obj.next, because that would make p'obj.next invalid
    in that case, we would have to use actual abstract object on the heap (dynamic_object$0.next) instead - this can be obtained by calling the function local_SSAt::dereference on p->next

  • I'd suggest including this check into build_transfer function
    maybe it would be enough to check whether last definition of pointer p is before the last definition o p'obj.next - this information can be retrieved from ssa_analysis, for inspiration see all_symbolic_deref_defined (question is, is this really sound?)
    retrieving pointer p from object p'obj should be possible using functions from ssa_pointed_objects.h, particularly get_pointer

  • merge into heap branch

Unexpected assertion error

When trying to analyze the following example:

#include <stdlib.h>

extern int __VERIFIER_nondet_int(void);

struct list{
	struct list* next;
};

int main()
{
	struct list *p,*q;
	p = malloc(sizeof(struct list));
	q = malloc(sizeof(struct list));
	
	p->next = malloc(sizeof(struct list));
	p = q;

	while(__VERIFIER_nondet_int) {
		q = p->next;
		q->next = malloc(sizeof(struct list));
		p->next = q->next;
	}

	return 1;
}

2ls ends up with this assertion error:
2ls: strategy_solver_heap.cpp:141: virtual bool strategy_solver_heapt::iterate(strategy_solver_baset::invariantt&): Assertion `to_address_of_expr(ptr_value).object().id()==ID_symbol' failed.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.