Disjunctive domains

.travis.yml

@@ -36,6 +36,7 @@ matrix:
       compiler: clang
       env: COMPILER=clang++
     - env: NAME="CPP-LINT"
+      before_script: git fetch origin master:master
       script: scripts/run_lint.sh master HEAD
 
 script:

README.md

@@ -3,19 +3,154 @@
 About
 =====
 
-2LS is a verification tool for C programs. It is built upon the
+2LS ("tools") is a verification tool for C programs. It is built upon the
 CPROVER framework ([cprover.org](http://www.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.
 
-For more information see [cprover.org](http://www.cprover.org/2LS).
 
 License
 =======
 4-clause BSD license, see `LICENSE` file.
 
 [build_img]: https://travis-ci.org/diffblue/2ls.svg?branch=master
 [travis]: https://travis-ci.org/diffblue/2ls
+
+
+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`
+
+* [2LS 0.7](http://github.com/diffblue/2ls/releases/tag/2ls-0.7) (08/2018)
+* [2LS 0.6](http://github.com/diffblue/2ls/releases/tag/2ls-0.6) (12/2017)
+* [2LS 0.5](http://github.com/diffblue/2ls/releases/tag/2ls-0.5) (01/2017)
+* [2LS 0.4](http://github.com/diffblue/2ls/releases/tag/2ls-0.4) (08/2016)
+* [2LS 0.3](http://svn.cprover.org/svn/deltacheck/releases/2ls-0.3) (08/2015)
+* [2LS 0.2](http://svn.cprover.org/svn/deltacheck/releases/2ls-0.2) (06/2015)
+* [2LS 0.1](http://svn.cprover.org/svn/deltacheck/releases/2ls-0.1) (11/2014)
+
+Software Verification Competition Contributions
+
+* [SV-COMP 2018](http://github.com/diffblue/2ls/releases/tag/2ls-0.6) (12/2017)
+* [SV-COMP 2017](http://github.com/diffblue/2ls/releases/tag/2ls-0.5-sv-comp-2017) (01/2017)
+* [SV-COMP 2016](http://svn.cprover.org/svn/deltacheck/releases/2ls-0.3-sv-comp-2016) (11/2015) [Follow these instructions](http://www.cprover.org/2LS/2ls-sv-comp-2016.pdf)
+
+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
+=======================
+
+* ACDL solver (ATVA'17 [Lifting CDCL to Template-Based Abstract Domains for Program Verification](https://doi.org/10.1007/978-3-319-68167-2_2))
+* array domain
+* disjunctive domains
+* custom template specifications
+* modular refinement
+* template refinement
+* thread-modular analysis
+
+Publications
+============
+
+* FMCAD'18 Template-Based Verification of Heap-Manipulating Programs
+* TACAS'18 [2LS: Memory Safety and Non-Termination](https://link.springer.com/chapter/10.1007%2F978-3-319-89963-3_24)
+* TOPLAS 40(1) 2018 [Bit-Precise Procedure-Modular Termination Analysis](https://dl.acm.org/citation.cfm?doid=3121136)
+* ATVA'17 [Compositional Refutation Techniques](https://link.springer.com/chapter/10.1007%2F978-3-319-68167-2_12)
+* ATVA'17 [Lifting CDCL to Template-Based Abstract Domains for Program Verification](https://doi.org/10.1007/978-3-319-68167-2_2)
+* TACAS'16 [2LS for Program Analysis](http://dl.acm.org/citation.cfm?id=2945506)
+* SAS'15 [Safety Verification and Refutation by k-Invariants and k-Induction](http://link.springer.com/chapter/10.1007%2F978-3-662-48288-9_9)
+* ASE'15 [Synthesising Interprocedural Bit-Precise Termination Proofs](http://dl.acm.org/citation.cfm?id=2916211) [Experimental log](http://www.cs.ox.ac.uk/people/peter.schrammel/2ls/ase15-experimental_results_log.txt) [Additional material](http://www.cs.ox.ac.uk/people/peter.schrammel/2ls/ase15-additional-material.tgz) [Website](http://www.cprover.org/termination/modular)
+
+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](http://www.schrammel.it)
+
+

install.sh

@@ -1,7 +1,7 @@
 #!/bin/bash
 
 CBMC_REPO=https://github.com/peterschrammel/cbmc
-CBMC_VERSION=d95e7da28018fd315b04a1201d5b7cfe8195cbc6
+CBMC_VERSION=2ls-prerequisites-0.7
 
 if [ "$1" != "" ]
 then
@@ -12,7 +12,16 @@ git clone $CBMC_REPO
 cd cbmc
 CBMC=`pwd`
 git checkout $CBMC_VERSION
-make -C src minisat2-download
+if grep '^MINISAT2' src/config.inc > /dev/null
+then
+  make -C src minisat2-download > /dev/null
+elif grep '^GLUCOSE' src/config.inc
+then
+  make -C src glucose-download
+else
+  echo "SAT solver not supported"
+  exit 1
+fi
 if [ "$COMPILER" != "" ]
 then
   make -C src CXX=$COMPILER

regression/Makefile

@@ -1,7 +1,15 @@
-DIRS = termination kiki preconditions interprocedural invariants
+DIRS = nontermination \
+	   termination \
+	   kiki \
+       preconditions \
+	   interprocedural \
+	   invariants \
+	   heap \
+	   heap-data \
+	   memsafety
 
 test:
-	$(foreach var,$(DIRS), make -C $(var) test;)
+	$(foreach var,$(DIRS), make -C $(var) test || exit 1;)
 
 clean:
 	$(foreach var,$(DIRS), make -C $(var) clean;)

regression/graphml/Makefile

@@ -1,6 +1,6 @@
 #FLAGS = --k-induction --competition-mode --32
 FLAGS = --unwind 11 --no-unwinding-assertions
-#2LS = ../../../src/summarizer/2ls 
+#2LS = ../../../src/summarizer/2ls
 2LS = $W/svncprover/branches/peter-incremental-unwinding/src/cbmc/cbmc
 CPACHECKER = $W/svncpachecker
 ULTIMATE = $W/UltimateAutomizer

regression/graphml/loop23/main.c

@@ -6,10 +6,10 @@ int main()
 int y;
  if(x) { return x;}
 
- for(x=0;x<2;x++) 
+ for(x=0;x<2;x++)
  {
    if(x==y) { return x;}
- 
+
 }
   __VERIFIER_assert(0);
   return 0;

regression/graphml/loop29/main.c

@@ -7,6 +7,6 @@ void main() {
     int y;
     if(-3>y || y>-1) return;
     x += y;
-  }        
-  __VERIFIER_assert(x==0 || x==-2);                           
-} 
+  }
+  __VERIFIER_assert(x==0 || x==-2);
+}

regression/graphml/malloc1/main.c

@@ -1029,7 +1029,7 @@ int ssl3_connect(SSL *s )
 
   {
     blastFlag = 0;
-    s->state = 12292; 
+    s->state = 12292;
     while (1) {
       if (s->state == 12292) {
 	goto switch_1_12292;
@@ -1047,15 +1047,15 @@ int ssl3_connect(SSL *s )
 	      switch_1_4368: ;
 		if (blastFlag == 0) {
 		  blastFlag = 1;
-		} 
+		}
 		s->state = 4384;
 		goto switch_1_break;
 	      switch_1_4384: ;
 		if (blastFlag == 1) {
 		  blastFlag = 2;
 		  goto ERROR;
-		} 
-									
+		}
+
 		goto end;
 	      switch_1_default:
 		goto end;

regression/heap-data/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+FLAGS = --verbosity 10
+
+test:
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+tests.log: ../test.pl
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@rm -f *.log
+	@for dir in *; do rm -f $$dir/*.out; done;

regression/heap-data/calendar/main.c

@@ -0,0 +1,40 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+#define APPEND(l,i) {i->next=l; l=i;}
+
+typedef struct node {
+    struct node *next;
+    int event1;
+    int event2;
+} Node;
+
+int main() {
+    Node *l = NULL;
+
+    while (__VERIFIER_nondet_int()) {
+        int ev1 = __VERIFIER_nondet_int();
+        int ev2 = __VERIFIER_nondet_int();
+        if (ev1 < 0 || ev1 > 3 || ev2 < 0 || ev2 > 3)
+            continue;
+
+        if (((ev1 == 0) && (ev2 == 2)) || ((ev1 == 1) && (ev2 == 3)) || ((ev1 == 0) && (ev2 == 3)))
+            continue;
+
+        Node *p = malloc(sizeof(*p));
+        p->event1 = ev1;
+        p->event2 = ev2;
+        APPEND(l,p)
+    }
+
+    Node *i = l;
+
+    while (i != NULL) {
+        if (((i->event1 == 1) && (i->event2 == 3)) || ((i->event1 == 0) && (i->event2 == 2)))
+            __VERIFIER_error();
+        i = i->next;
+    }
+}
+

regression/heap-data/calendar/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap-values-refine --sympath --inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/heap-data/cart/main.c

@@ -0,0 +1,46 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+#define APPEND(l,i) {i->next=l; l=i;}
+
+typedef struct node {
+    struct node *next;
+    int stock;
+    int order;
+} Node;
+
+int main() {
+    Node *l = NULL;
+
+    while (__VERIFIER_nondet_int()) {
+        int stock = __VERIFIER_nondet_int();
+        if (stock < 0)
+            continue;
+
+        Node *p = malloc(sizeof(*p));
+        p->stock = stock;
+        p->order = 0;
+        APPEND(l,p)
+    }
+
+    Node *i = l;
+    while (i != NULL) {
+        int order = __VERIFIER_nondet_int();
+        if (order < 0 || i->stock < order)
+            continue;
+        i->order = order;
+        i->stock = i->stock;
+        i = i->next;
+    }
+
+
+    i = l;
+    while (i != NULL) {
+        if (i->order > i->stock)
+            __VERIFIER_error();
+        i = i->next;
+    }
+}
+

regression/heap-data/cart/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap-values-refine --sympath --inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$