Improvements to the shape abstract domain and to memory safety analysis

regression/Makefile

@@ -1,5 +1,6 @@
-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-incremental --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-incremental --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-incremental --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-incremental --sympath --inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/heap-data/packet_filter/main.c

@@ -0,0 +1,81 @@
+extern unsigned __VERIFIER_nondet_uint();
+extern int __VERIFIER_nondet_int();
+extern char *__VERIFIER_nondet_charp();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+#define LOW 0
+#define HIGH 1
+
+typedef struct packet {
+    unsigned size;
+    unsigned prio;
+    char *payload;
+} Packet;
+
+typedef struct packet_list_node {
+    struct packet packet;
+    struct packet_list_node *next;
+} *Node;
+
+struct packet_queue {
+    struct packet_list_node *front;
+};
+
+
+Packet receive() {
+    Packet packet;
+    packet.size = __VERIFIER_nondet_uint();
+    packet.prio = __VERIFIER_nondet_int() ? LOW : HIGH;
+    packet.payload = __VERIFIER_nondet_charp();
+    return packet;
+}
+
+extern void send(struct packet p);
+
+void append_to_queue(Packet p, Node *q) {
+    Node node = malloc(sizeof(*node));
+    node->packet = p;
+    node->next = *q;
+    *q = node;
+}
+
+void process_prio_queue(Node q) {
+    for (Node node = q; node != NULL; node = node->next) {
+        if (!(node->packet.prio == HIGH || node->packet.size < 500))
+            __VERIFIER_error();
+        send(node->packet);
+    }
+}
+
+void process_normal_queue(Node q) {
+    for (Node node = q; node != NULL; node = node->next) {
+        if (!(node->packet.prio == LOW && node->packet.size >= 500))
+            __VERIFIER_error();
+        send(node->packet);
+    }
+}
+
+int main() {
+    Node prio_queue = NULL;
+    Node normal_queue = NULL;
+
+    while (__VERIFIER_nondet_int()) {
+        Packet new_packet = receive();
+        if (new_packet.size > 0) {
+            if (new_packet.prio == HIGH) {
+                append_to_queue(new_packet, &prio_queue);
+            } else if (new_packet.size < 500) {
+                append_to_queue(new_packet, &prio_queue);
+            } else {
+                append_to_queue(new_packet, &normal_queue);
+            }
+        }
+    }
+
+    process_prio_queue(prio_queue);
+    process_normal_queue(normal_queue);
+
+    return 0;
+}

regression/heap-data/packet_filter/test.desc

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

regression/heap-data/process_queue/main.c

@@ -0,0 +1,69 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+#define MAX_PROC 1000
+
+struct process_node {
+    int process_id;
+    int time_to_wait;
+
+    struct process_node *next;
+};
+
+extern void run_process(int id);
+
+void append_to_queue(struct process_node *n, struct process_node **q) {
+    n->next = *q;
+    *q = n;
+}
+
+struct process_node *choose_next(struct process_node **q) {
+    struct process_node *node = *q;
+    struct process_node *prev = NULL;
+    struct process_node *result = NULL;
+    while (node != NULL) {
+        if (node->time_to_wait == 1) {
+            result = node;
+            if (prev == NULL)
+                *q = node->next;
+            else
+                prev->next = node->next;
+        } else {
+            node->time_to_wait--;
+        }
+        prev = node;
+        node = node->next;
+    }
+    return result;
+}
+
+void check_queue(struct process_node *q) {
+    for (struct process_node *n = q; n != NULL; n = n->next)
+        if (!n->time_to_wait >= 1)
+            __VERIFIER_error();
+}
+
+
+int main() {
+    struct process_node *queue = NULL;
+    int next_time = 1;
+
+    while (__VERIFIER_nondet_int()) {
+        if (next_time < MAX_PROC && __VERIFIER_nondet_int()) {
+            int new_id = __VERIFIER_nondet_int();
+
+            struct process_node *new_process = malloc(sizeof(*new_process));
+            new_process->process_id = __VERIFIER_nondet_int();
+            new_process->time_to_wait = next_time++;
+            append_to_queue(new_process, &queue);
+        } else if (next_time > 1){
+            struct process_node *p = choose_next(&queue);
+            next_time--;
+            run_process(p->process_id);
+        }
+
+        check_queue(queue);
+    } 
+}

regression/heap-data/process_queue/test.desc

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