Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improvements to the shape abstract domain and to memory safety analysis #120

Merged
merged 70 commits into from
Aug 13, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
70 commits
Select commit Hold shift + click to select a range
64daeeb
Set "record_malloc" and "record_may_leak" variables to true
viktormalik Feb 26, 2018
5f59a7d
Heap domain: handle incompatible pointer types in get_row_expr
viktormalik Feb 26, 2018
424cf5e
Heap domain: improve transitive row updating
viktormalik Mar 2, 2018
b624ec9
Track allocation sites of dynamic objects in assignmenst and SSA domain
viktormalik Mar 2, 2018
942511d
For dynamic objects allocated in a loop, add allocation guard to post…
viktormalik Mar 2, 2018
5e6503e
Add possibility to use object created in given SSA node at RHS of ass…
viktormalik Mar 2, 2018
66a12ca
Copy pointed info to member expression on symbolic dereference
viktormalik Mar 2, 2018
26684c8
Add new test to heap directory
viktormalik Mar 2, 2018
4af058e
For objects allocated in loops, create one concrete and one abstract …
viktormalik Mar 6, 2018
5859255
Collect allocation guards of concrete/abstract objects and use them i…
viktormalik Mar 6, 2018
7c5cada
Perform some pointer safety checks on concrete objects only
viktormalik Mar 6, 2018
b3eff2a
Heap domain: allow template row to contain a pair of variables as exp…
viktormalik Mar 6, 2018
cf4c5e3
Heap domain: track dependency between __CPROVER_deallocated and other…
viktormalik Mar 6, 2018
5ba86f4
Allow recording free
viktormalik Mar 6, 2018
1a282c0
Do not use pointer access paths in the heap domain
viktormalik Mar 6, 2018
7ade32c
Make unwinder to handle "object-select" guard
viktormalik Mar 6, 2018
8705014
Add tests for memory safety
viktormalik Mar 6, 2018
18b148b
Add another example to heap that uses domain combination
viktormalik Mar 6, 2018
0be684c
Split assignments having the same symbolic dereference object on both…
viktormalik Mar 6, 2018
06e0128
Update process_queue test
viktormalik Mar 6, 2018
0ce8606
Fix bug in splitting assignments having same symbolic deref on both s…
viktormalik Mar 7, 2018
42afc71
Symbolic paths: set loop-select guard to true only if the loop head i…
viktormalik Mar 15, 2018
ebb2d97
Remove dead GOTO instructions
viktormalik Mar 16, 2018
56210f3
Remove dead GOTO instruction only for backwards goto
viktormalik Mar 16, 2018
1fdd369
Better verification of free safety for multiple frees within a loop
viktormalik Mar 20, 2018
d04098e
Create new regression directory with benchmark for SAS 2018 paper
viktormalik Apr 5, 2018
d6428b5
Add combination of heap and zones domain
viktormalik Apr 9, 2018
4cb88ab
Modify SAS 2018 tests to use __VERIFIER_error instead of assert
viktormalik Apr 9, 2018
ff40be0
Add 2 more tests to SAS'18 benchmark
viktormalik Apr 9, 2018
2bfac82
Add new example to SAS'18 benchmark
viktormalik Apr 10, 2018
6524bf1
Add new example to SAS'18 benchmark
viktormalik Apr 10, 2018
4863739
Add combination of heap domain with multiple value domains
viktormalik Apr 10, 2018
99d6003
Update SAS;18 benchmark to use the new --heap-values-incremental switch
viktormalik Apr 10, 2018
0c8a3ab
Analysis of the required number of dynamic object instances
viktormalik May 15, 2018
6b2d154
Add test that reveals an unsoundness in treating of dynamic objects
viktormalik May 15, 2018
4b20b5d
Collect live pointers pointing to a dynamic object at the same time
viktormalik May 16, 2018
67bc0fc
Split dynamic objects into multiple instances based on results of the…
viktormalik May 18, 2018
328499c
rhs_concretisaztion
martinhruska May 18, 2018
df862c9
rhs_concretisaztion
martinhruska May 18, 2018
970b11b
adding case for assert
martinhruska May 18, 2018
f665fb1
Template polyhedra domain: do not generate template rows with 'false'…
viktormalik May 21, 2018
c3ab3f3
Update running example in sas18 directory
viktormalik May 25, 2018
7ae8727
updated running example to make it work
martinhruska May 27, 2018
154bb4c
renamed directory to fmcad
martinhruska May 27, 2018
cf39cd2
problematic version of running example
martinhruska May 27, 2018
0cbf7de
sas18 to fmcad18
martinhruska May 27, 2018
37d74d7
fmcad18 to heap-data
martinhruska May 28, 2018
735e5c4
Comments and refactoring of dynamic objects instances analysis.
viktormalik Jun 28, 2018
16ffaa1
Add missing function comments.
viktormalik Jun 28, 2018
6b67494
Adjust coding style.
viktormalik Jun 28, 2018
b414e3c
Heap-data tests: disable long test and move one from 'heap' directory
viktormalik Jun 28, 2018
14bad7b
Remove debugging output
viktormalik Jun 28, 2018
c75c8d4
Adjust creation of multiple dynamic objects at one allocation site
viktormalik Jun 29, 2018
bc085cd
Add one test to memsafety and disable failing tests.
viktormalik Jun 29, 2018
719684c
Splitting dynamic objects: do not fail on array-typed dynamic objects.
viktormalik Jun 29, 2018
4fe5103
Add memsafety and heap-data to main regression Makefile
viktormalik Jun 29, 2018
dd533c8
Fix bug in creating PHI nodes for dynamic objects in some 'if' branches
viktormalik Jun 29, 2018
54c9a2e
Disable competition mode that kills programs with pointer arithmetic
viktormalik Jun 29, 2018
d70047e
Fix bug in dynobj_instance_analysis.
viktormalik Jul 20, 2018
40facd1
Fix bug in dynobj_instance_analysis.
viktormalik Jul 20, 2018
9572ea2
Adjust code style for latest fix.
viktormalik Jul 20, 2018
c9a7d89
Remove fmcad18 directory, it has already been replaced by heap-data.
viktormalik Jul 20, 2018
c71334c
Remove spurious newlines from some tests in memory categories.
viktormalik Jul 23, 2018
d022890
Fix errors in command line options.
viktormalik Jul 23, 2018
ed80b24
Use has_prefix and CPROVER_PREFIX to check whether a symbol is CPROVE…
viktormalik Jul 23, 2018
556c9c7
Remove debugging output.
viktormalik Jul 26, 2018
9104bda
Rename heap-interval to heap-tpolyhedra including names of all relate…
viktormalik Aug 3, 2018
cbb660c
Refactor combination of heap domain with increasing strength of value…
viktormalik Aug 3, 2018
d938e3e
Code cleanup
viktormalik Aug 3, 2018
215ab5d
Help formatting.
viktormalik Aug 13, 2018
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions regression/Makefile
Original file line number Diff line number Diff line change
@@ -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;)
Expand Down
20 changes: 20 additions & 0 deletions regression/heap-data/Makefile
Original file line number Diff line number Diff line change
@@ -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;
40 changes: 40 additions & 0 deletions regression/heap-data/calendar/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
}

6 changes: 6 additions & 0 deletions regression/heap-data/calendar/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
--heap-values-refine --sympath --inline
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
46 changes: 46 additions & 0 deletions regression/heap-data/cart/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
}

6 changes: 6 additions & 0 deletions regression/heap-data/cart/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
--heap-values-refine --sympath --inline
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
42 changes: 42 additions & 0 deletions regression/heap-data/hash_fun/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
}
6 changes: 6 additions & 0 deletions regression/heap-data/hash_fun/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
--heap-values-refine --sympath --inline
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
40 changes: 40 additions & 0 deletions regression/heap-data/min_max/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
}
6 changes: 6 additions & 0 deletions regression/heap-data/min_max/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
--heap-values-refine --sympath --inline
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
81 changes: 81 additions & 0 deletions regression/heap-data/packet_filter/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
6 changes: 6 additions & 0 deletions regression/heap-data/packet_filter/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
THOROUGH
main.c
--heap-values-refine --sympath --inline
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
69 changes: 69 additions & 0 deletions regression/heap-data/process_queue/main.c
Original file line number Diff line number Diff line change
@@ -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);
}
}
Loading