Merge pull request #120 from viktormalik/master

Improvements to the shape abstract domain and to memory safety analysis

Author: peterschrammel

regression/Makefile

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

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$

regression/heap-data/hash_fun/main.c

@@ -0,0 +1,42 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+#define INTERVAL_SIZE 100
+
+struct node {
+    int hash;
+    struct node *next;
+};
+
+int hash_fun();
+
+void append_to_list(struct node **list, int hash) {
+    struct node *node = malloc(sizeof(*node));
+    node->next = *list;
+    node->hash = hash;
+    *list = node;
+}
+
+int main() {
+    struct node *list = NULL;
+
+    int base = __VERIFIER_nondet_int();
+
+    while (__VERIFIER_nondet_int()) {
+        if (base >= 0 && base <= 1000000) {
+            base = base;
+            int hash = hash_fun();
+
+            if (hash > base && hash < base + INTERVAL_SIZE)
+                append_to_list(&list, hash);
+        }
+    }
+
+    while (list) {
+        if (!(list->hash >= base && list->hash < base + INTERVAL_SIZE))
+            __VERIFIER_error();
+        list = list->next;
+    }
+}

regression/heap-data/hash_fun/test.desc

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

regression/heap-data/min_max/main.c

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

regression/heap-data/min_max/test.desc

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