diff --git a/regression/Makefile b/regression/Makefile index 0b4d2b0bd..7143b0ad8 100644 --- a/regression/Makefile +++ b/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;) diff --git a/regression/heap-data/Makefile b/regression/heap-data/Makefile new file mode 100644 index 000000000..34cd734b9 --- /dev/null +++ b/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; diff --git a/regression/heap-data/calendar/main.c b/regression/heap-data/calendar/main.c new file mode 100644 index 000000000..2ee9630e5 --- /dev/null +++ b/regression/heap-data/calendar/main.c @@ -0,0 +1,40 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +#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; + } +} + diff --git a/regression/heap-data/calendar/test.desc b/regression/heap-data/calendar/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/calendar/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/cart/main.c b/regression/heap-data/cart/main.c new file mode 100644 index 000000000..3144e411e --- /dev/null +++ b/regression/heap-data/cart/main.c @@ -0,0 +1,46 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +#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; + } +} + diff --git a/regression/heap-data/cart/test.desc b/regression/heap-data/cart/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/cart/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/hash_fun/main.c b/regression/heap-data/hash_fun/main.c new file mode 100644 index 000000000..08fd2104a --- /dev/null +++ b/regression/heap-data/hash_fun/main.c @@ -0,0 +1,42 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +#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; + } +} diff --git a/regression/heap-data/hash_fun/test.desc b/regression/heap-data/hash_fun/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/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$ diff --git a/regression/heap-data/min_max/main.c b/regression/heap-data/min_max/main.c new file mode 100644 index 000000000..76b129535 --- /dev/null +++ b/regression/heap-data/min_max/main.c @@ -0,0 +1,40 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include +#include + +#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; + } +} diff --git a/regression/heap-data/min_max/test.desc b/regression/heap-data/min_max/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/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$ diff --git a/regression/heap-data/packet_filter/main.c b/regression/heap-data/packet_filter/main.c new file mode 100644 index 000000000..b2a16f4b4 --- /dev/null +++ b/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 + +#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; +} diff --git a/regression/heap-data/packet_filter/test.desc b/regression/heap-data/packet_filter/test.desc new file mode 100644 index 000000000..2ed70fde0 --- /dev/null +++ b/regression/heap-data/packet_filter/test.desc @@ -0,0 +1,6 @@ +THOROUGH +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/process_queue/main.c b/regression/heap-data/process_queue/main.c new file mode 100644 index 000000000..1299105de --- /dev/null +++ b/regression/heap-data/process_queue/main.c @@ -0,0 +1,69 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +#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); + } +} diff --git a/regression/heap-data/process_queue/test.desc b/regression/heap-data/process_queue/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/process_queue/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/quick_sort_split/main.c b/regression/heap-data/quick_sort_split/main.c new file mode 100644 index 000000000..c286aa4e8 --- /dev/null +++ b/regression/heap-data/quick_sort_split/main.c @@ -0,0 +1,62 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +#define LOW -1 +#define HIGH 1 + +struct node { + int expected_list; + int value; + struct node *next; +}; + +void append_to_list(struct node **list, int val, int exp) { + struct node *node = malloc(sizeof(*node)); + node->next = *list; + node->value = val; + node->expected_list = exp; + *list = node; +} + +struct node *create_list() { + struct node *list = NULL; + while (__VERIFIER_nondet_int()) { + int v = __VERIFIER_nondet_int(); + if (v < 0) + append_to_list(&list, v, LOW); + else + append_to_list(&list, v, HIGH); + } + return list; +} + +int main() { + struct node *list = create_list(); + + struct node *low = NULL; + struct node *high = NULL; + + // Split list into low and high + struct node *p = list; + while (p) { + struct node *l = p->value >= 0 ? high : low; + struct node *next = p->next; + p->next = l; + l = p; + p = next; + } + + // Check that low and high contain expected elements + while (low) { + if (!low->expected_list == LOW) + __VERIFIER_error(); + low = low->next; + } + while (high) { + if (!high->expected_list == HIGH) + __VERIFIER_error(); + high = high->next; + } +} diff --git a/regression/heap-data/quick_sort_split/test.desc b/regression/heap-data/quick_sort_split/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/quick_sort_split/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example/main.c b/regression/heap-data/running_example/main.c new file mode 100644 index 000000000..378fa8348 --- /dev/null +++ b/regression/heap-data/running_example/main.c @@ -0,0 +1,35 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +typedef struct node { + int val; + struct node *next; +} Node; + +int main() { + Node *p, *list = malloc(sizeof(*list)); + Node *tail = list; + list->next = NULL; + list->val = 10; + while (__VERIFIER_nondet_int()) { + int x; + if (x < 10 || x > 20) continue; + p = malloc(sizeof(*p)); + tail->next = p; + p->next = NULL; + p->val = x; + tail = p; + } + + while (1) { + for (p = list; p!= NULL; p = p->next) { + if (!(p->val <= 20 && p->val >= 10)) + __VERIFIER_error(); + if (p->val < 20) p->val++; + else p->val /= 2; + } + } +} + diff --git a/regression/heap-data/running_example/test.desc b/regression/heap-data/running_example/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/running_example/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example_assume/main.c b/regression/heap-data/running_example_assume/main.c new file mode 100644 index 000000000..d64eed513 --- /dev/null +++ b/regression/heap-data/running_example_assume/main.c @@ -0,0 +1,35 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +typedef struct node { + int val; + struct node *next; +} Node; + +int main() { + Node *p, *list = malloc(sizeof(*list)); + Node *tail = list; + list->next = NULL; + list->val = 10; + while (__VERIFIER_nondet_int()) { + int x; + __CPROVER_assume(x >= 10 && x <= 20); + p = malloc(sizeof(*p)); + tail->next = p; + p->next = NULL; + p->val = x; + tail = p; + } + + while (1) { + for (p = list; p!= NULL; p = p->next) { + if (!(p->val <= 20 && p->val >= 10)) + __VERIFIER_error(); + if (p->val < 20) p->val++; + else p->val /= 2; + } + } +} + diff --git a/regression/heap-data/running_example_assume/test.desc b/regression/heap-data/running_example_assume/test.desc new file mode 100644 index 000000000..253d82f29 --- /dev/null +++ b/regression/heap-data/running_example_assume/test.desc @@ -0,0 +1,6 @@ +KNOWNBUG +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem1/main.c b/regression/heap-data/shared_mem1/main.c new file mode 100644 index 000000000..d80939e92 --- /dev/null +++ b/regression/heap-data/shared_mem1/main.c @@ -0,0 +1,49 @@ +extern int __VERIFIER_nondet_int(); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +#include + +struct mem { + int val; +}; + +struct list_node { + int x; + struct mem *mem; + struct list_node *next; +}; + +int main() { + struct mem *m = malloc(sizeof(*m)); + m->val = 100; + + struct list_node *head = malloc(sizeof(*head)); + head->x = 1; + head->mem = m; + head->next = head; + + struct list_node *list = head; + + while (__VERIFIER_nondet_int()) { + int x; + if (x > 0 && x < 10) { + struct list_node *n = malloc(sizeof(*n)); + n->x = x; + n->mem = m; + n->next = head; + list->next = n; + } + } + + list = head; + while (list) { + if (list->mem->val <= 100) + list->mem->val += list->x; + else + list->mem->val -= list->x; + list = list->next; + + if (!(m->val > 90 && m->val < 110)) + __VERIFIER_error(); + } +} diff --git a/regression/heap-data/shared_mem1/test.desc b/regression/heap-data/shared_mem1/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/shared_mem1/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem2/main.c b/regression/heap-data/shared_mem2/main.c new file mode 100644 index 000000000..dd4f6466d --- /dev/null +++ b/regression/heap-data/shared_mem2/main.c @@ -0,0 +1,45 @@ +extern int __VERIFIER_nondet_int(); + +#include + +struct mem { + int val; +}; + +struct list_node { + int x; + struct mem *mem; + struct list_node *next; +}; + +int main() { + struct mem *m = malloc(sizeof(*m)); + m->val = 0; + + struct list_node *head = malloc(sizeof(*head)); + head->x = 1; + head->mem = m; + head->next = head; + + struct list_node *list = head; + + while (__VERIFIER_nondet_int()) { + int x; + if (x > 0 && x < 10) { + struct list_node *n = malloc(sizeof(*n)); + n->x = x; + n->mem = m; + n->next = head; + list->next = n; + } + } + + list = head; + while (m->val < 100) { + if (list->mem->val + list->x <= 100) + list->mem->val += list->x; + list = list->next; + } + if (!m->val == 100) + __VERIFIER_nondet_int(); +} diff --git a/regression/heap-data/shared_mem2/test.desc b/regression/heap-data/shared_mem2/test.desc new file mode 100644 index 000000000..b48b4027a --- /dev/null +++ b/regression/heap-data/shared_mem2/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-values-refine --sympath --inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/built_from_end/main.c b/regression/heap/built_from_end/main.c index a25f56363..47fe17aed 100644 --- a/regression/heap/built_from_end/main.c +++ b/regression/heap/built_from_end/main.c @@ -34,6 +34,5 @@ int main() { } p = p->n; } - } diff --git a/regression/heap/dll1_simple/test.desc b/regression/heap/dll1_simple/test.desc index ed14b476a..92784083a 100644 --- a/regression/heap/dll1_simple/test.desc +++ b/regression/heap/dll1_simple/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --heap --inline --no-propagation ^EXIT=0$ diff --git a/regression/heap/dynobj_concret/main.c b/regression/heap/dynobj_concret/main.c new file mode 100644 index 000000000..d59aae01b --- /dev/null +++ b/regression/heap/dynobj_concret/main.c @@ -0,0 +1,30 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +extern int __VERIFIER_nondet_int(); + +#include + +void exit(int s) { + _EXIT: goto _EXIT; +} + +typedef struct node { + struct node *n; +} *List; + +int main() { + /* Build a list of the form 1->...->1->0 */ + List t; + List p = NULL; + while (__VERIFIER_nondet_int()) { + t = (List) malloc(sizeof(struct node)); + t->n = p; + p = t; + } + + if (p && p->n) { + List n = p->n; + List nn = n->n; + assert(n==nn); + } +} diff --git a/regression/heap/list_true/test.desc b/regression/heap/list_true/test.desc index c03cf0e85..e2ef350dc 100644 --- a/regression/heap/list_true/test.desc +++ b/regression/heap/list_true/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --heap-interval --sympath --inline --no-propagation ^EXIT=0$ diff --git a/regression/heap/simple_true/test.desc b/regression/heap/simple_true/test.desc index e086f8559..405084afc 100644 --- a/regression/heap/simple_true/test.desc +++ b/regression/heap/simple_true/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --heap-interval --inline --no-propagation --sympath ^EXIT=0$ diff --git a/regression/memsafety/Makefile b/regression/memsafety/Makefile new file mode 100644 index 000000000..34cd734b9 --- /dev/null +++ b/regression/memsafety/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; diff --git a/regression/memsafety/built_from_end/main.c b/regression/memsafety/built_from_end/main.c new file mode 100644 index 000000000..dcac19706 --- /dev/null +++ b/regression/memsafety/built_from_end/main.c @@ -0,0 +1,37 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +extern int __VERIFIER_nondet_int(); +/* + * Simple example: build a list with only 1s and finally a 0 (arbitrary length); + * afterwards, go through it and check if the list does have the correct form, and in particular + * finishes by a 0. + */ +#include + +void exit(int s) { + _EXIT: goto _EXIT; +} + +typedef struct node { + int h; + struct node *n; +} *List; + +int main() { + /* Build a list of the form 1->...->1->0 */ + List t; + List p = 0; + while (__VERIFIER_nondet_int()) { + t = (List) malloc(sizeof(struct node)); + if (t == 0) exit(1); + t->h = 1; + t->n = p; + p = t; + } + while (p!=0) { + t = p->n; + free(p); + p = t; + } +} + diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc new file mode 100644 index 000000000..02a269a04 --- /dev/null +++ b/regression/memsafety/built_from_end/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--heap-interval --inline --sympath --pointer-check --no-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/memsafety/built_from_end_false/main.c b/regression/memsafety/built_from_end_false/main.c new file mode 100644 index 000000000..153ccea0e --- /dev/null +++ b/regression/memsafety/built_from_end_false/main.c @@ -0,0 +1,37 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +extern int __VERIFIER_nondet_int(); +/* + * Simple example: build a list with only 1s and finally a 0 (arbitrary length); + * afterwards, go through it and check if the list does have the correct form, and in particular + * finishes by a 0. + */ +#include + +void exit(int s) { + _EXIT: goto _EXIT; +} + +typedef struct node { + int h; + struct node *n; +} *List; + +int main() { + /* Build a list of the form 1->...->1->0 */ + List t; + List p = 0; + while (__VERIFIER_nondet_int()) { + t = (List) malloc(sizeof(struct node)); + if (t == 0) exit(1); + t->h = 1; + t->n = p ? p : t; + p = t; + } + while (p!=0) { + t = p->n; + free(p); + p = t; + } +} + diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc new file mode 100644 index 000000000..f93d3925c --- /dev/null +++ b/regression/memsafety/built_from_end_false/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--heap-interval --sympath --inline --pointer-check --no-assertions --k-induction +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[main.pointer_dereference.11\] dereference failure: deallocated dynamic object in \*p: FAILURE diff --git a/regression/memsafety/simple_false/main.c b/regression/memsafety/simple_false/main.c new file mode 100644 index 000000000..ee661872a --- /dev/null +++ b/regression/memsafety/simple_false/main.c @@ -0,0 +1,39 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +extern int __VERIFIER_nondet_int(); + +#include + +void exit(int s) { + _EXIT: goto _EXIT; +} + +typedef struct node { + int h; + struct node *n; +} *List; + +int main() { + /* Build a list of the form 1->...->1->0 */ + List a = (List) malloc(sizeof(struct node)); + if (a == 0) exit(1); + a->n = 0; + List t; + List p = a; + while (__VERIFIER_nondet_int()) { + t = (List) malloc(sizeof(struct node)); + if (t == 0) exit(1); + t->n = 0; + p->n = t; + p = p->n; + } + p->n = a; + p = a; + while (p!=0) { + t = p->n; + free(p); + p = t; + } + return 0; +} + diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc new file mode 100644 index 000000000..fdea46680 --- /dev/null +++ b/regression/memsafety/simple_false/test.desc @@ -0,0 +1,7 @@ +KNOWNBUG +main.c +--heap-interval --sympath --inline --pointer-check --k-induction +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[main.pointer_dereference.23\] dereference failure: deallocated dynamic object in \*p: FAILURE diff --git a/regression/memsafety/simple_true/main.c b/regression/memsafety/simple_true/main.c new file mode 100644 index 000000000..79d7b5e74 --- /dev/null +++ b/regression/memsafety/simple_true/main.c @@ -0,0 +1,38 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); + +extern int __VERIFIER_nondet_int(); + +#include + +void exit(int s) { + _EXIT: goto _EXIT; +} + +typedef struct node { + int h; + struct node *n; +} *List; + +int main() { + /* Build a list of the form 1->...->1->0 */ + List a = (List) malloc(sizeof(struct node)); + if (a == 0) exit(1); + a->n = 0; + List t; + List p = a; + while (__VERIFIER_nondet_int()) { + t = (List) malloc(sizeof(struct node)); + if (t == 0) exit(1); + t->n = 0; + p->n = t; + p = p->n; + } + p = a; + while (p!=0) { + t = p->n; + free(p); + p = t; + } + return 0; +} + diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc new file mode 100644 index 000000000..3b416f2a8 --- /dev/null +++ b/regression/memsafety/simple_true/test.desc @@ -0,0 +1,6 @@ +KNOWNBUG +main.c +--heap-interval --inline --sympath --pointer-check --no-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index a78b4c0b1..a9e8a3f76 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -46,6 +46,7 @@ Author: Daniel Kroening, Peter Schrammel #include "graphml_witness_ext.h" #include +#include #include "2ls_parse_options.h" #include "summary_checker_ai.h" @@ -209,6 +210,19 @@ void twols_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("sympath")) options.set_option("sympath", true); } + else if(cmdline.isset("heap-zones")) + { + options.set_option("heap-zones", true); + if(cmdline.isset("sympath")) + options.set_option("sympath", true); + } + else if(cmdline.isset("heap-values-refine")) + { + options.set_option("heap-values-refine", true); + options.set_option("heap-interval", true); + if(cmdline.isset("sympath")) + options.set_option("sympath", true); + } else { if(cmdline.isset("zones")) @@ -518,6 +532,8 @@ int twols_parse_optionst::doit() status() << "Using heap domain" << eom; else if(options.get_bool_option("heap-interval")) status() << "Using heap domain with interval domain for values" << eom; + else if(options.get_bool_option("heap-zones")) + status() << "Using heap domain with zones domain for values" << eom; else { if(options.get_bool_option("intervals")) @@ -577,8 +593,8 @@ int twols_parse_optionst::doit() checker=std::unique_ptr( new summary_checker_bmct(options, heap_analysis)); if(options.get_bool_option("nontermination")) - checker=std::unique_ptr( - new summary_checker_nontermt(options, heap_analysis)); + checker=std::unique_ptr( + new summary_checker_nontermt(options, heap_analysis)); checker->set_message_handler(get_message_handler()); checker->simplify=!cmdline.isset("no-simplify"); @@ -1232,7 +1248,18 @@ bool twols_parse_optionst::process_goto_program( goto_model.goto_functions.compute_loop_numbers(); // Replace malloc - dynamic_memory_detected=replace_malloc(goto_model, ""); + dynamic_memory_detected=replace_malloc( + goto_model, "", options.get_bool_option("pointer-check")); + + // Allow recording of mallocs and memory leaks + if(options.get_bool_option("pointer-check")) + { + allow_record_malloc(goto_model); + } + if(options.get_bool_option("memory-leak-check")) + allow_record_memleak(goto_model); + + split_same_symbolic_object_assignments(goto_model); // remove loop heads from function entries remove_loops_in_entry(goto_model); @@ -1243,6 +1270,8 @@ bool twols_parse_optionst::process_goto_program( inline_main(goto_model); } + auto dynobj_instances=split_dynamic_objects(goto_model); + if(!cmdline.isset("independent-properties")) { add_assumptions_after_assertions(goto_model); @@ -1252,14 +1281,14 @@ bool twols_parse_optionst::process_goto_program( filter_assertions(goto_model); #endif - if(options.get_bool_option("constant-propagation") && - !(options.get_bool_option("competition-mode") && - dynamic_memory_detected)) + if(options.get_bool_option("constant-propagation")) { status() << "Constant Propagation" << eom; propagate_constants(goto_model); } + remove_dead_goto(goto_model); + // if we aim to cover, replace // all assertions by false to prevent simplification if(cmdline.isset("cover-assertions")) @@ -1744,8 +1773,13 @@ void twols_parse_optionst::help() " --heap use heap domain\n" " --zones use zone domain\n" " --octagons use octagon domain\n" - " --heap-interval use heap domain with interval domain for values\n" // NOLINT(*) - " --sympath compute invariant for each symbolic path (only usable with --heap-interval switch)" // NOLINT(*) + " --heap-interval use heap domain with interval domain for\n" + " values\n" + " --heap-zones use heap domain with zones domain for values\n" // NOLINT(*) + " --heap-values-refine use heap domain with a dynamic refinement\n" + " of strength of the value domain\n" + " --sympath compute invariant for each symbolic path\n" + " (only usable with --heap-* switches)\n" " --enum-solver use solver based on model enumeration\n" " --binsearch-solver use solver based on binary search\n" " --arrays do not ignore array contents\n" diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 612e35f5c..2199b95d3 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -16,6 +16,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include class goto_modelt; class optionst; @@ -37,7 +38,15 @@ class optionst; "(version)" \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ "(ppc-macos)(unsigned-char)" \ - "(havoc)(intervals)(zones)(octagons)(equalities)(heap)(heap-interval)"\ + "(havoc)" \ + "(intervals)" \ + "(zones)" \ + "(octagons)" \ + "(equalities)" \ + "(heap)" \ + "(heap-interval)" \ + "(heap-zones)" \ + "(heap-values-refine)" \ "(sympath)" \ "(enum-solver)(binsearch-solver)(arrays)"\ "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ @@ -183,6 +192,18 @@ class twols_parse_optionst: void add_dynamic_object_symbols( const ssa_heap_analysist &heap_analysis, goto_modelt &goto_model); + void split_same_symbolic_object_assignments(goto_modelt &goto_model); + void remove_dead_goto(goto_modelt &goto_model); + void compute_dynobj_instances( + const goto_programt &goto_program, + const dynobj_instance_analysist &analysis, + std::map &instance_counts, + const namespacet &ns); + void create_dynobj_instances( + goto_programt &goto_program, + const std::map &instance_counts, + symbol_tablet &symbol_table); + std::map split_dynamic_objects(goto_modelt &goto_model); }; #endif diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index b31229afb..f69cc78db 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -12,6 +12,7 @@ Author: Peter Schrammel #include #include +#include #include "2ls_parse_options.h" @@ -626,3 +627,242 @@ void twols_parse_optionst::add_dynamic_object_symbols( } } } + +/*******************************************************************\ + +Function: twols_parse_optionst::split_same_symbolic_object_assignments + + Inputs: + + Outputs: + + Purpose: Split assignments that have same symbolic dereference object + on both sides into two separate assignments. + +\*******************************************************************/ + +void twols_parse_optionst::split_same_symbolic_object_assignments( + goto_modelt &goto_model) +{ + const namespacet ns(goto_model.symbol_table); + unsigned counter=0; + Forall_goto_functions(f_it, goto_model.goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if(i_it->is_assign()) + { + code_assignt &assign=to_code_assign(i_it->code); + auto lhs_sym_deref=symbolic_dereference(assign.lhs(), ns); + if((lhs_sym_deref.id()==ID_symbol || lhs_sym_deref.id()==ID_member) + && has_symbolic_deref(lhs_sym_deref)) + { + while(lhs_sym_deref.id()==ID_member) + lhs_sym_deref=to_member_expr(lhs_sym_deref).compound(); + + auto rhs_sym_deref=symbolic_dereference(assign.rhs(), ns); + + std::set rhs_symbols; + find_symbols(rhs_sym_deref, rhs_symbols); + + if(rhs_symbols.find(to_symbol_expr(lhs_sym_deref))!=rhs_symbols.end()) + { + symbolt tmp_symbol; + tmp_symbol.type=assign.lhs().type(); + tmp_symbol.name="$symderef_tmp"+i2string(counter++); + tmp_symbol.base_name=tmp_symbol.name; + tmp_symbol.pretty_name=tmp_symbol.name; + + goto_model.symbol_table.add(tmp_symbol); + + auto new_assign=f_it->second.body.insert_after(i_it); + new_assign->make_assignment(); + new_assign->code=code_assignt( + assign.lhs(), tmp_symbol.symbol_expr()); + + assign.lhs()=tmp_symbol.symbol_expr(); + } + } + } + } + } +} + +/*******************************************************************\ + +Function: twols_parse_optionst::remove_dead_goto + + Inputs: + + Outputs: + + Purpose: Remove dead backwards GOTO instructions (having false as guard) + +\*******************************************************************/ +void twols_parse_optionst::remove_dead_goto(goto_modelt &goto_model) +{ + Forall_goto_functions(f_it, goto_model.goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if(i_it->is_backwards_goto()) + { + if(i_it->guard.is_false()) + i_it->make_skip(); + } + } + } +} + +/*******************************************************************\ + +Function: twols_parse_optionst::compute_dynobj_instances + + Inputs: + + Outputs: + + Purpose: For each allocation site, compute the number of objects + that must be used to soundly represent all objects allocated + at the given site. + +\*******************************************************************/ +void twols_parse_optionst::compute_dynobj_instances( + const goto_programt &goto_program, + const dynobj_instance_analysist &analysis, + std::map &instance_counts, + const namespacet &ns) +{ + forall_goto_program_instructions(it, goto_program) + { + auto &analysis_value=analysis[it]; + for(auto &obj : analysis_value.live_pointers) + { + auto must_alias=analysis_value.must_alias_relations.find(obj.first); + if(must_alias==analysis_value.must_alias_relations.end()) + continue; + + std::set alias_classes; + for(auto &expr : obj.second) + { + size_t n; + must_alias->second.get_number(expr, n); + alias_classes.insert(must_alias->second.find_number(n)); + } + + if(instance_counts.find(obj.first)==instance_counts.end() || + instance_counts.at(obj.first) &instance_counts, + symbol_tablet &symbol_table) +{ + Forall_goto_program_instructions(it, goto_program) + { + if(it->is_assign()) + { + auto &assign=to_code_assign(it->code); + if(assign.rhs().get_bool("#malloc_result")) + { + exprt &rhs=assign.rhs(); + exprt &abstract_obj=rhs.id()==ID_if ? to_if_expr(rhs).false_case() + : rhs; + exprt &address=abstract_obj.id()==ID_typecast ? + to_typecast_expr(abstract_obj).op() : abstract_obj; + if(address.id()!=ID_address_of) + continue; + exprt &obj=to_address_of_expr(address).object(); + if(obj.id()!=ID_symbol) + continue; + + if(instance_counts.find(to_symbol_expr(obj))==instance_counts.end()) + continue; + + size_t count=instance_counts.at(to_symbol_expr(obj)); + if(count<=1) + continue; + + symbolt obj_symbol= + symbol_table.lookup(to_symbol_expr(obj).get_identifier()); + + const std::string name=id2string(obj_symbol.name); + const std::string base_name=id2string(obj_symbol.base_name); + std::string suffix="#"+std::to_string(0); + + obj_symbol.name=name+suffix; + obj_symbol.base_name=base_name+suffix; + symbol_table.add(obj_symbol); + + exprt new_rhs=address_of_exprt(obj_symbol.symbol_expr()); + if(abstract_obj.id()==ID_typecast) + new_rhs=typecast_exprt(new_rhs, rhs.type()); + new_rhs.set("#malloc_result", true); + + for(size_t i=1; ilocation_number)+"#"+ + std::to_string(i); + nondet.base_name=nondet.name; + nondet.pretty_name=nondet.name; + symbol_table.add(nondet); + + suffix="#"+std::to_string(i); + obj_symbol.name=name+suffix; + obj_symbol.base_name=base_name+suffix; + + exprt new_obj=address_of_exprt(obj_symbol.symbol_expr()); + if(abstract_obj.id()==ID_typecast) + new_obj=typecast_exprt(new_obj, rhs.type()); + new_rhs=if_exprt( + nondet.symbol_expr(), new_obj, new_rhs); + new_rhs.set("#malloc_result", true); + } + + abstract_obj=new_rhs; + abstract_obj.set("#malloc_result", true); + } + } + } +} + +std::map twols_parse_optionst::split_dynamic_objects( + goto_modelt &goto_model) +{ + std::map dynobj_instances; + Forall_goto_functions(f_it, goto_model.goto_functions) + { + if(!f_it->second.body_available()) + continue; + namespacet ns(goto_model.symbol_table); + ssa_value_ait value_analysis(f_it->second, ns, ssa_heap_analysist(ns)); + dynobj_instance_analysist do_inst(f_it->second, ns, value_analysis); + + compute_dynobj_instances( + f_it->second.body, do_inst, dynobj_instances, ns); + create_dynobj_instances( + f_it->second.body, dynobj_instances, goto_model.symbol_table); + } + return dynobj_instances; +} diff --git a/src/2ls/summary_checker_ai.cpp b/src/2ls/summary_checker_ai.cpp index 6f36857ab..8e60a8739 100644 --- a/src/2ls/summary_checker_ai.cpp +++ b/src/2ls/summary_checker_ai.cpp @@ -43,40 +43,58 @@ property_checkert::resultt summary_checker_ait::operator()( // properties initialize_property_map(goto_model.goto_functions); - bool preconditions=options.get_bool_option("preconditions"); - bool termination=options.get_bool_option("termination"); - bool trivial_domain=options.get_bool_option("havoc"); - if(!trivial_domain || termination) + property_checkert::resultt result=property_checkert::UNKNOWN; + bool finished=false; + while(!finished) { - // forward analysis - summarize(goto_model, true, termination); - } - if(!trivial_domain && preconditions) - { - // backward analysis - summarize(goto_model, false, termination); - } + bool preconditions=options.get_bool_option("preconditions"); + bool termination=options.get_bool_option("termination"); + bool trivial_domain=options.get_bool_option("havoc"); + if(!trivial_domain || termination) + { + // forward analysis + summarize(goto_model, true, termination); + } + if(!trivial_domain && preconditions) + { + // backward analysis + summarize(goto_model, false, termination); + } - if(preconditions) - { - report_statistics(); - report_preconditions(); - return property_checkert::UNKNOWN; - } + if(preconditions) + { + report_statistics(); + report_preconditions(); + return property_checkert::UNKNOWN; + } - if(termination) - { - report_statistics(); - return report_termination(); - } + if(termination) + { + report_statistics(); + return report_termination(); + } #ifdef SHOW_CALLINGCONTEXTS - if(options.get_bool_option("show-calling-contexts")) - return property_checkert::UNKNOWN; + if(options.get_bool_option("show-calling-contexts")) + return property_checkert::UNKNOWN; #endif - property_checkert::resultt result=check_properties(); - report_statistics(); + result=check_properties(); + report_statistics(); + + if(result==property_checkert::UNKNOWN && + options.get_bool_option("heap-values-refine") && + options.get_bool_option("heap-interval")) + { + summary_db.clear(); + options.set_option("heap-interval", false); + options.set_option("heap-zones", true); + } + else + { + finished=true; + } + } return result; } diff --git a/src/2ls/summary_checker_kind.cpp b/src/2ls/summary_checker_kind.cpp index 0fe1c9110..47092b8a7 100644 --- a/src/2ls/summary_checker_kind.cpp +++ b/src/2ls/summary_checker_kind.cpp @@ -6,7 +6,7 @@ Author: Peter Schrammel \*******************************************************************/ -#include +#include #include "summary_checker_kind.h" /*******************************************************************\ diff --git a/src/domains/Makefile b/src/domains/Makefile index 28f310666..e293aee2f 100644 --- a/src/domains/Makefile +++ b/src/domains/Makefile @@ -1,6 +1,7 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ predabs_domain.cpp heap_domain.cpp list_iterator.cpp \ - heap_interval_domain.cpp heap_interval_sympath_domain.cpp symbolic_path.cpp\ + heap_tpolyhedra_domain.cpp heap_tpolyhedra_sympath_domain.cpp \ + symbolic_path.cpp\ ssa_analyzer.cpp util.cpp incremental_solver.cpp \ strategy_solver_base.cpp strategy_solver_equality.cpp \ linrank_domain.cpp lexlinrank_domain.cpp\ @@ -10,7 +11,8 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ template_generator_callingcontext.cpp template_generator_ranking.cpp \ strategy_solver_binsearch2.cpp strategy_solver_binsearch3.cpp \ strategy_solver_predabs.cpp strategy_solver_heap.cpp \ - strategy_solver_heap_interval.cpp strategy_solver_heap_interval_sympath.cpp \ + strategy_solver_heap_tpolyhedra.cpp \ + strategy_solver_heap_tpolyhedra_sympath.cpp \ #solver_enumeration.cpp include ../config.inc diff --git a/src/domains/heap_domain.cpp b/src/domains/heap_domain.cpp index 25a421c03..6c4576dea 100644 --- a/src/domains/heap_domain.cpp +++ b/src/domains/heap_domain.cpp @@ -30,10 +30,11 @@ void heap_domaint::initialize(domaint::valuet &value) for(const template_rowt &templ_row : templ) { if(templ_row.mem_kind==STACK) - val.emplace_back(new stack_row_valuet()); + val.emplace_back(new stack_row_valuet(ns)); else if(templ_row.mem_kind==HEAP) val.emplace_back( new heap_row_valuet( + ns, std::make_pair( templ_row.dyn_obj, templ_row.expr))); @@ -75,6 +76,29 @@ void heap_domaint::make_template( { const typet &pointed_type=ns.follow(var.type().subtype()); add_template_row(v, pointed_type); + + if(var.id()==ID_symbol && + id2string(to_symbol_expr(var).get_identifier()).find( + "__CPROVER_deallocated")!=std::string::npos) + { + for(const var_spect &v_other : var_specs) + { + if(!(v_other.var.type().id()==ID_pointer && v_other.kind==LOOP && + v_other.pre_guard==v.pre_guard)) + { + continue; + } + + if(v_other.var.id()==ID_symbol && + id2string(to_symbol_expr(v_other.var).get_identifier()).find( + "__CPROVER_")!=std::string::npos) + { + continue; + } + + add_template_row_pair(v, v_other, pointed_type); + } + } } } } @@ -116,7 +140,12 @@ void heap_domaint::add_template_row( if(identifier.find("."+id2string(component.get_name()))!= std::string::npos) { +#if 0 + // It has shown that using stack rows only is sufficient to prove all + // tested programs and it seems that pointer access paths are not + // necessary. Therefore, we currently disable this code. templ_row.mem_kind=HEAP; +#endif templ_row.member=component.get_name(); std::string var_id=id2string(to_symbol_expr(var).get_identifier()); @@ -129,6 +158,36 @@ void heap_domaint::add_template_row( /*******************************************************************\ +Function: heap_domaint::add_template_row_pair + + Inputs: var_spec Variable specification + + Outputs: + + Purpose: Add a template row with a pair of variables as expression. + +\*******************************************************************/ + +void heap_domaint::add_template_row_pair( + const domaint::var_spect &var_spec1, + const domaint::var_spect &var_spec2, + const typet &pointed_type) +{ + const exprt var_pair=and_exprt(var_spec1.var, var_spec2.var); + + templ.push_back(template_rowt()); + template_rowt &templ_row=templ.back(); + templ_row.expr=var_pair; + templ_row.pre_guard=var_spec1.pre_guard; + templ_row.post_guard=var_spec1.post_guard; + templ_row.aux_expr=var_spec1.aux_expr; + templ_row.kind=var_spec1.kind; + + templ_row.mem_kind=STACK; +} + +/*******************************************************************\ + Function: heap_domaint::to_pre_constraints Inputs: @@ -459,8 +518,17 @@ void heap_domaint::project_on_vars( { const template_rowt &templ_row=templ[row]; - if(!vars.empty() && vars.find(templ_row.expr)==vars.end()) - continue; + if(!vars.empty()) + { + if(templ_row.expr.id()==ID_and) + { + if(vars.find(templ_row.expr.op0())==vars.end() && + vars.find(templ_row.expr.op1())==vars.end()) + continue; + } + else if(vars.find(templ_row.expr)==vars.end()) + continue; + } const row_valuet &row_val=val[row]; if(templ_row.kind==LOOP) @@ -551,6 +619,38 @@ int heap_domaint::get_symbol_loc(const exprt &expr) /*******************************************************************\ +Function: ptr_equality + + Inputs: Pointer expression (variable) + Value (object or address) of the pointer + + Outputs: Equality between pointer and its value with correct types + + Purpose: + +\*******************************************************************/ + +const exprt ptr_equality( + const exprt &ptr_expr, + const exprt &ptr_value, + const namespacet &ns) +{ + exprt value; + if(ptr_expr.type()==ptr_value.type()) + value=ptr_value; + else if(ns.follow(ptr_expr.type().subtype())==ns.follow(ptr_value.type())) + value=address_of_exprt(ptr_value); + else + { + value=typecast_exprt( + address_of_exprt(ptr_value), + ns.follow(ptr_expr.type())); + } + return equal_exprt(ptr_expr, value); +} + +/*******************************************************************\ + Function: heap_domaint::stack_row_valuet::get_row_expr Inputs: templ_expr Template expression @@ -577,10 +677,15 @@ exprt heap_domaint::stack_row_valuet::get_row_expr( exprt::operandst result; for(const exprt &pt : points_to) { - result.push_back( - equal_exprt( - templ_expr, - templ_expr.type()==pt.type() ? pt : address_of_exprt(pt))); + if(templ_expr.id()==ID_and) + { + result.push_back( + and_exprt( + ptr_equality(templ_expr.op0(), pt.op0(), ns), + ptr_equality(templ_expr.op1(), pt.op1(), ns))); + } + else + result.push_back(ptr_equality(templ_expr, pt, ns)); } return disjunction(result); } @@ -796,8 +901,11 @@ bool heap_domaint::heap_row_valuet::add_all_paths( bool result=false; for(auto &path : other_val.paths) { + bool new_dest=(paths.find(path.destination)==paths.end()); if(add_path(path.destination, dyn_obj)) { + if(!new_dest) + paths.erase(dyn_obj.first); result=true; for(auto &o : path.dyn_objects) { diff --git a/src/domains/heap_domain.h b/src/domains/heap_domain.h index 73ff01a9b..72d0f3167 100644 --- a/src/domains/heap_domain.h +++ b/src/domains/heap_domain.h @@ -60,6 +60,10 @@ class heap_domaint:public domaint // Row is nondeterministic - row expression is TRUE bool nondet=false; + const namespacet &ns; + + explicit row_valuet(const namespacet &ns):ns(ns) {} + virtual exprt get_row_expr( const vart &templ_expr, bool rename_templ_expr) const=0; @@ -82,6 +86,8 @@ class heap_domaint:public domaint // Set of objects (or NULL) the row variable can point to std::set points_to; + explicit stack_row_valuet(const namespacet &ns):row_valuet(ns) {} + virtual exprt get_row_expr( const vart &templ_expr, bool rename_templ_expr) const override; @@ -143,7 +149,8 @@ class heap_domaint:public domaint // Self link on an abstract dynamic object bool self_linkage=false; - explicit heap_row_valuet(const dyn_objt &dyn_obj_):dyn_obj(dyn_obj_) {} + heap_row_valuet(const namespacet &ns, const dyn_objt &dyn_obj_): + row_valuet(ns), dyn_obj(dyn_obj_) {} virtual exprt get_row_expr( const vart &templ_expr_, @@ -300,6 +307,10 @@ class heap_domaint:public domaint void make_template(const var_specst &var_specs, const namespacet &ns); void add_template_row(const var_spect &var_spec, const typet &pointed_type); + void add_template_row_pair( + const var_spect &var_spec1, + const var_spect &var_spec2, + const typet &pointed_type); // Initializing functions void bind_iterators( diff --git a/src/domains/heap_interval_domain.cpp b/src/domains/heap_tpolyhedra_domain.cpp similarity index 60% rename from src/domains/heap_interval_domain.cpp rename to src/domains/heap_tpolyhedra_domain.cpp index e38d89332..c5bd4a636 100644 --- a/src/domains/heap_interval_domain.cpp +++ b/src/domains/heap_tpolyhedra_domain.cpp @@ -1,16 +1,16 @@ /*******************************************************************\ -Module: Combination of heap and interval abstract domains +Module: Combination of heap and template polyhedra abstract domains Author: Viktor Malik \*******************************************************************/ -#include "heap_interval_domain.h" +#include "heap_tpolyhedra_domain.h" /*******************************************************************\ -Function: heap_interval_domaint::initialize +Function: heap_tpolyhedra_domaint::initialize Inputs: @@ -20,17 +20,17 @@ Function: heap_interval_domaint::initialize \*******************************************************************/ -void heap_interval_domaint::initialize(domaint::valuet &value) +void heap_tpolyhedra_domaint::initialize(domaint::valuet &value) { - heap_interval_valuet &v=static_cast(value); + heap_tpolyhedra_valuet &v=static_cast(value); heap_domain.initialize(v.heap_value); - interval_domain.initialize(v.interval_value); + polyhedra_domain.initialize(v.tpolyhedra_value); } /*******************************************************************\ -Function: heap_interval_domaint::output_value +Function: heap_tpolyhedra_domaint::output_value Inputs: @@ -40,21 +40,21 @@ Function: heap_interval_domaint::output_value \*******************************************************************/ -void heap_interval_domaint::output_value( +void heap_tpolyhedra_domaint::output_value( std::ostream &out, const domaint::valuet &value, const namespacet &ns) const { - const heap_interval_valuet &v= - static_cast(value); + const heap_tpolyhedra_valuet &v= + static_cast(value); heap_domain.output_value(out, v.heap_value, ns); - interval_domain.output_value(out, v.interval_value, ns); + polyhedra_domain.output_value(out, v.tpolyhedra_value, ns); } /*******************************************************************\ -Function: heap_interval_domaint::output_domain +Function: heap_tpolyhedra_domaint::output_domain Inputs: @@ -64,17 +64,17 @@ Function: heap_interval_domaint::output_domain \*******************************************************************/ -void heap_interval_domaint::output_domain( +void heap_tpolyhedra_domaint::output_domain( std::ostream &out, const namespacet &ns) const { heap_domain.output_domain(out, ns); - interval_domain.output_domain(out, ns); + polyhedra_domain.output_domain(out, ns); } /*******************************************************************\ -Function: heap_interval_domaint::project_on_vars +Function: heap_tpolyhedra_domaint::project_on_vars Inputs: @@ -84,26 +84,26 @@ Function: heap_interval_domaint::project_on_vars \*******************************************************************/ -void heap_interval_domaint::project_on_vars( +void heap_tpolyhedra_domaint::project_on_vars( domaint::valuet &value, const domaint::var_sett &vars, exprt &result) { - heap_interval_valuet &v=static_cast(value); + heap_tpolyhedra_valuet &v=static_cast(value); exprt heap_result; heap_domain.project_on_vars(v.heap_value, vars, heap_result); - exprt interval_result; - interval_domain.project_on_vars(v.interval_value, vars, interval_result); + exprt tpolyhedra_result; + polyhedra_domain.project_on_vars(v.tpolyhedra_value, vars, tpolyhedra_result); result=heap_result; - if(interval_result!=true_exprt()) - result=and_exprt(result, interval_result); + if(tpolyhedra_result!=true_exprt()) + result=and_exprt(result, tpolyhedra_result); } /*******************************************************************\ -Function: heap_interval_domaint::restrict_to_sympath +Function: heap_tpolyhedra_domaint::restrict_to_sympath Inputs: Symbolic path @@ -112,16 +112,16 @@ Function: heap_interval_domaint::restrict_to_sympath Purpose: Restrict template to a given symbolic path. \*******************************************************************/ -void heap_interval_domaint::restrict_to_sympath( +void heap_tpolyhedra_domaint::restrict_to_sympath( const symbolic_patht &sympath) { heap_domain.restrict_to_sympath(sympath); - interval_domain.restrict_to_sympath(sympath); + polyhedra_domain.restrict_to_sympath(sympath); } /*******************************************************************\ -Function: heap_interval_domaint::clear_aux_symbols +Function: heap_tpolyhedra_domaint::clear_aux_symbols Inputs: @@ -130,15 +130,15 @@ Function: heap_interval_domaint::clear_aux_symbols Purpose: Reset aux symbols to true (remove all restricitions). \*******************************************************************/ -void heap_interval_domaint::clear_aux_symbols() +void heap_tpolyhedra_domaint::clear_aux_symbols() { heap_domain.clear_aux_symbols(); - interval_domain.clear_aux_symbols(); + polyhedra_domain.clear_aux_symbols(); } /*******************************************************************\ -Function: heap_interval_domaint::eliminate_sympaths +Function: heap_tpolyhedra_domaint::eliminate_sympaths Inputs: Vector of symbolic paths @@ -147,16 +147,16 @@ Function: heap_interval_domaint::eliminate_sympaths Purpose: Restrict template to other paths than those specified. \*******************************************************************/ -void heap_interval_domaint::eliminate_sympaths( +void heap_tpolyhedra_domaint::eliminate_sympaths( const std::vector &sympaths) { heap_domain.eliminate_sympaths(sympaths); - interval_domain.eliminate_sympaths(sympaths); + polyhedra_domain.eliminate_sympaths(sympaths); } /*******************************************************************\ -Function: heap_interval_domaint::undo_restriction +Function: heap_tpolyhedra_domaint::undo_restriction Inputs: @@ -165,8 +165,8 @@ Function: heap_interval_domaint::undo_restriction Purpose: Undo last restriction. \*******************************************************************/ -void heap_interval_domaint::undo_restriction() +void heap_tpolyhedra_domaint::undo_restriction() { heap_domain.undo_restriction(); - interval_domain.undo_restriction(); + polyhedra_domain.undo_restriction(); } diff --git a/src/domains/heap_interval_domain.h b/src/domains/heap_tpolyhedra_domain.h similarity index 56% rename from src/domains/heap_interval_domain.h rename to src/domains/heap_tpolyhedra_domain.h index cf6179f6f..5c2cb9d68 100644 --- a/src/domains/heap_interval_domain.h +++ b/src/domains/heap_tpolyhedra_domain.h @@ -1,41 +1,53 @@ /*******************************************************************\ -Module: Combination of heap and interval abstract domains +Module: Combination of heap and template polyhedra abstract domains Author: Viktor Malik \*******************************************************************/ -#ifndef CPROVER_2LS_DOMAINS_HEAP_INTERVAL_DOMAIN_H -#define CPROVER_2LS_DOMAINS_HEAP_INTERVAL_DOMAIN_H +#ifndef CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H +#define CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H #include "domain.h" #include "tpolyhedra_domain.h" #include "heap_domain.h" -class heap_interval_domaint:public domaint +class heap_tpolyhedra_domaint:public domaint { public: + enum polyhedra_kindt + { + INTERVAL, ZONES, OCTAGONS + }; + heap_domaint heap_domain; - tpolyhedra_domaint interval_domain; + tpolyhedra_domaint polyhedra_domain; - heap_interval_domaint( + heap_tpolyhedra_domaint( unsigned int _domain_number, replace_mapt &_renaming_map, const var_specst &var_specs, - const namespacet &ns): + const namespacet &ns, + const polyhedra_kindt polyhedra_kind): domaint(_domain_number, _renaming_map, ns), heap_domain(_domain_number, _renaming_map, var_specs, ns), - interval_domain(_domain_number, _renaming_map, ns) + polyhedra_domain(_domain_number, _renaming_map, ns) { - interval_domain.add_interval_template(var_specs, ns); + if(polyhedra_kind==INTERVAL) + polyhedra_domain.add_interval_template(var_specs, ns); + else if(polyhedra_kind==ZONES) + { + polyhedra_domain.add_difference_template(var_specs, ns); + polyhedra_domain.add_interval_template(var_specs, ns); + } } - class heap_interval_valuet:public valuet + class heap_tpolyhedra_valuet:public valuet { public: heap_domaint::heap_valuet heap_value; - tpolyhedra_domaint::templ_valuet interval_value; + tpolyhedra_domaint::templ_valuet tpolyhedra_value; }; virtual void initialize(valuet &value) override; @@ -61,4 +73,4 @@ class heap_interval_domaint:public domaint void clear_aux_symbols(); }; -#endif // CPROVER_2LS_DOMAINS_HEAP_INTERVAL_DOMAIN_H +#endif // CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H diff --git a/src/domains/heap_interval_sympath_domain.cpp b/src/domains/heap_tpolyhedra_sympath_domain.cpp similarity index 60% rename from src/domains/heap_interval_sympath_domain.cpp rename to src/domains/heap_tpolyhedra_sympath_domain.cpp index 8fc09f9c4..c13d3bb9c 100644 --- a/src/domains/heap_interval_sympath_domain.cpp +++ b/src/domains/heap_tpolyhedra_sympath_domain.cpp @@ -1,17 +1,17 @@ /*******************************************************************\ -Module: Abstract domain for computing invariants in heap-interval +Module: Abstract domain for computing invariants in heap-tpolyhedra domain for different symbolic paths in program. Author: Viktor Malik \*******************************************************************/ -#include "heap_interval_sympath_domain.h" +#include "heap_tpolyhedra_sympath_domain.h" /*******************************************************************\ -Function: heap_interval_sympath_domaint::output_value +Function: heap_tpolyhedra_sympath_domaint::output_value Inputs: @@ -20,23 +20,23 @@ Function: heap_interval_sympath_domaint::output_value Purpose: \*******************************************************************/ -void heap_interval_sympath_domaint::output_value( +void heap_tpolyhedra_sympath_domaint::output_value( std::ostream &out, const domaint::valuet &value, const namespacet &ns) const { - const heap_interval_sympath_valuet &v= - static_cast(value); + const heap_tpolyhedra_sympath_valuet &v= + static_cast(value); for(auto &config : v) { out << from_expr(ns, "", config.first) << "==>\n"; - heap_interval_domain.output_value(out, config.second, ns); + heap_tpolyhedra_domain.output_value(out, config.second, ns); } } /*******************************************************************\ -Function: heap_interval_sympath_domaint::output_domain +Function: heap_tpolyhedra_sympath_domaint::output_domain Inputs: @@ -45,16 +45,16 @@ Function: heap_interval_sympath_domaint::output_domain Purpose: \*******************************************************************/ -void heap_interval_sympath_domaint::output_domain( +void heap_tpolyhedra_sympath_domaint::output_domain( std::ostream &out, const namespacet &ns) const { - heap_interval_domain.output_domain(out, ns); + heap_tpolyhedra_domain.output_domain(out, ns); } /*******************************************************************\ -Function: heap_interval_sympath_domaint::project_on_vars +Function: heap_tpolyhedra_sympath_domaint::project_on_vars Inputs: @@ -63,18 +63,18 @@ Function: heap_interval_sympath_domaint::project_on_vars Purpose: \*******************************************************************/ -void heap_interval_sympath_domaint::project_on_vars( +void heap_tpolyhedra_sympath_domaint::project_on_vars( domaint::valuet &value, const domaint::var_sett &vars, exprt &result) { - heap_interval_sympath_valuet &v= - static_cast(value); + heap_tpolyhedra_sympath_valuet &v= + static_cast(value); exprt::operandst c; for(auto &config : v) { exprt config_result; - heap_interval_domain.project_on_vars(config.second, vars, config_result); + heap_tpolyhedra_domain.project_on_vars(config.second, vars, config_result); c.push_back(and_exprt(config.first, config_result)); } c.push_back(no_loops_path); diff --git a/src/domains/heap_interval_sympath_domain.h b/src/domains/heap_tpolyhedra_sympath_domain.h similarity index 57% rename from src/domains/heap_interval_sympath_domain.h rename to src/domains/heap_tpolyhedra_sympath_domain.h index 5a3fee8fc..3e2ddadb1 100644 --- a/src/domains/heap_interval_sympath_domain.h +++ b/src/domains/heap_tpolyhedra_sympath_domain.h @@ -1,43 +1,45 @@ /*******************************************************************\ -Module: Abstract domain for computing invariants in heap-interval +Module: Abstract domain for computing invariants in heap-tpolyhedra domain for different symbolic paths in program. Author: Viktor Malik \*******************************************************************/ -#ifndef CPROVER_2LS_DOMAINS_HEAP_INTERVAL_SYMPATH_DOMAIN_H -#define CPROVER_2LS_DOMAINS_HEAP_INTERVAL_SYMPATH_DOMAIN_H +#ifndef CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H +#define CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H #include "domain.h" -#include "heap_interval_domain.h" +#include "heap_tpolyhedra_domain.h" -class heap_interval_sympath_domaint:public domaint +class heap_tpolyhedra_sympath_domaint:public domaint { public: - heap_interval_domaint heap_interval_domain; + heap_tpolyhedra_domaint heap_tpolyhedra_domain; - heap_interval_sympath_domaint( + heap_tpolyhedra_sympath_domaint( unsigned int _domain_number, replace_mapt &_renaming_map, const var_specst &var_specs, - const local_SSAt &SSA): + const local_SSAt &SSA, + const heap_tpolyhedra_domaint::polyhedra_kindt polyhedra_kind): domaint(_domain_number, _renaming_map, SSA.ns), - heap_interval_domain(_domain_number, _renaming_map, var_specs, SSA.ns) + heap_tpolyhedra_domain( + _domain_number, _renaming_map, var_specs, SSA.ns, polyhedra_kind) { exprt::operandst false_loop_guards; for(auto &g : SSA.loop_guards) - false_loop_guards.push_back(not_exprt(g)); + false_loop_guards.push_back(not_exprt(g.first)); no_loops_path=conjunction(false_loop_guards); } // Value is a map from expression (symbolic path) to an invariant in heap - // interval domain - class heap_interval_sympath_valuet: + // tpolyhedra domain + class heap_tpolyhedra_sympath_valuet: public valuet, - public std::map + public std::map { }; @@ -61,8 +63,8 @@ class heap_interval_sympath_domaint:public domaint // path even though it can be feasible exprt no_loops_path; - friend class strategy_solver_heap_interval_sympatht; + friend class strategy_solver_heap_tpolyhedra_sympatht; }; -#endif // CPROVER_2LS_DOMAINS_HEAP_INTERVAL_SYMPATH_DOMAIN_H +#endif // CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 5b048f561..72ad03b52 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -32,8 +32,8 @@ Author: Peter Schrammel #include "strategy_solver_predabs.h" #include "ssa_analyzer.h" #include "strategy_solver_heap.h" -#include "strategy_solver_heap_interval.h" -#include "strategy_solver_heap_interval_sympath.h" +#include "strategy_solver_heap_tpolyhedra.h" +#include "strategy_solver_heap_tpolyhedra_sympath.h" // NOLINTNEXTLINE(*) #define BINSEARCH_SOLVER strategy_solver_binsearcht(\ @@ -120,29 +120,31 @@ void ssa_analyzert::operator()( template_generator); result=new heap_domaint::heap_valuet(); } - else if(template_generator.options.get_bool_option("heap-interval")) + else if(template_generator.options.get_bool_option("heap-interval") + || template_generator.options.get_bool_option("heap-zones")) { if(template_generator.options.get_bool_option("sympath")) { - strategy_solver=new strategy_solver_heap_interval_sympatht( - *static_cast(domain), + strategy_solver=new strategy_solver_heap_tpolyhedra_sympatht( + *static_cast(domain), solver, SSA, precondition, get_message_handler(), template_generator); - result=new heap_interval_sympath_domaint::heap_interval_sympath_valuet(); + result= + new heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet(); } else { - strategy_solver=new strategy_solver_heap_intervalt( - *static_cast(domain), + strategy_solver=new strategy_solver_heap_tpolyhedrat( + *static_cast(domain), solver, SSA, precondition, get_message_handler(), template_generator); - result=new heap_interval_domaint::heap_interval_valuet(); + result=new heap_tpolyhedra_domaint::heap_tpolyhedra_valuet(); } } else diff --git a/src/domains/strategy_solver_base.cpp b/src/domains/strategy_solver_base.cpp index f82dbb7e8..c43d17b86 100644 --- a/src/domains/strategy_solver_base.cpp +++ b/src/domains/strategy_solver_base.cpp @@ -22,20 +22,21 @@ Function: strategy_solver_baset::find_symbolic_path \*******************************************************************/ void strategy_solver_baset::find_symbolic_path( - std::set &loop_guards, + std::set> &loop_guards, const exprt ¤t_guard) { - for(const symbol_exprt &guard : loop_guards) + for(const auto &guard : loop_guards) { - if(guard==current_guard) + if(guard.first==current_guard) { - symbolic_path[guard]=true; + symbolic_path[guard.first]=true; continue; } - exprt guard_value=solver.get(guard); - if(guard_value.is_true()) - symbolic_path[guard]=true; - else if(guard_value.is_false()) - symbolic_path[guard]=false; + exprt ls_guard_value=solver.get(guard.first); + exprt lh_guard_value=solver.get(guard.second); + if(ls_guard_value.is_true() && lh_guard_value.is_true()) + symbolic_path[guard.first]=true; + else if(ls_guard_value.is_false()) + symbolic_path[guard.first]=false; } } diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h index 375e8a19b..7915b5ef9 100644 --- a/src/domains/strategy_solver_base.h +++ b/src/domains/strategy_solver_base.h @@ -50,7 +50,7 @@ class strategy_solver_baset:public messaget unsigned solver_calls; void find_symbolic_path( - std::set &loop_guards, + std::set> &loop_guards, const exprt ¤t_guard=nil_exprt()); }; diff --git a/src/domains/strategy_solver_heap.cpp b/src/domains/strategy_solver_heap.cpp index 5eadf165e..faf3c1a5f 100644 --- a/src/domains/strategy_solver_heap.cpp +++ b/src/domains/strategy_solver_heap.cpp @@ -116,114 +116,103 @@ bool strategy_solver_heapt::iterate(invariantt &_inv) const heap_domaint::template_rowt &templ_row=heap_domain.templ[row]; - int actual_loc=heap_domain.get_symbol_loc(templ_row.expr); - - exprt pointer=strategy_value_exprs[row]; - exprt value=solver.get(pointer); - // Value from the solver must be converted into an expression - exprt ptr_value=heap_domain.value_to_ptr_exprt(value); - const exprt loop_guard=to_and_expr( heap_domain.templ[row].pre_guard).op1(); find_symbolic_path(loop_guards, loop_guard); - if((ptr_value.id()==ID_constant && - to_constant_expr(ptr_value).get_value()==ID_NULL) || - ptr_value.id()==ID_symbol) - { - // Add equality p == NULL or p == symbol - if(heap_domain.add_points_to(row, inv, ptr_value)) - { - improved=true; - const std::string info= - templ_row.mem_kind==heap_domaint::STACK ? "points to " - : "path to "; - debug() << "Add " << info << from_expr(ns, "", ptr_value) << eom; - } - } - else if(ptr_value.id()==ID_address_of) + if(templ_row.expr.id()==ID_and) { - // Template row pointer points to the heap (p = &obj) - debug() << from_expr(ns, "", ptr_value) << eom; - assert(ptr_value.id()==ID_address_of); - if(to_address_of_expr(ptr_value).object().id()!=ID_symbol) + // Handle template row with a pair of variables in the expression + exprt points_to1=get_points_to_dest( + strategy_value_exprs[row].op0(), templ_row.expr.op0()); + exprt points_to2=get_points_to_dest( + strategy_value_exprs[row].op1(), templ_row.expr.op1()); + + if(points_to1.is_nil() || points_to2.is_nil()) { - // If solver did not return address of a symbol, it is considered - // as nondet value. if(heap_domain.set_nondet(row, inv)) { improved=true; debug() << "Set nondet" << eom; } - continue; } - - symbol_exprt obj=to_symbol_expr( - to_address_of_expr(ptr_value).object()); - - if(obj.type()!=templ_row.expr.type() && - ns.follow(templ_row.expr.type().subtype())!=ns.follow(obj.type())) + else { - // If types disagree, it's a nondet (solver assigned random value) - if(heap_domain.set_nondet(row, inv)) + if(heap_domain.add_points_to( + row, inv, and_exprt(points_to1, points_to2))) { improved=true; - debug() << "Set nondet" << eom; + const std::string info= + templ_row.mem_kind==heap_domaint::STACK ? "points to " + : "path to "; + debug() << "Add " << info + << from_expr(ns, "", and_exprt(points_to1, points_to2)) + << eom; } - continue; } + continue; + } + + int actual_loc=heap_domain.get_symbol_loc(templ_row.expr); + + exprt points_to=get_points_to_dest( + strategy_value_exprs[row], templ_row.expr); - // Add equality p == &obj - if(heap_domain.add_points_to(row, inv, obj)) + if(points_to.is_nil()) + { + if(heap_domain.set_nondet(row, inv)) + { + improved=true; + debug() << "Set nondet" << eom; + } + continue; + } + else + { + if(heap_domain.add_points_to(row, inv, points_to)) { improved=true; const std::string info= templ_row.mem_kind==heap_domaint::STACK ? "points to " : "path to "; - debug() << "Add " << info << from_expr(ns, "", obj) << eom; + debug() << "Add " << info << from_expr(ns, "", points_to) << eom; } + } - // If the template row is of heap kind, we need to ensure the - // transitive closure over the set of all paths - if(templ_row.mem_kind==heap_domaint::HEAP && - obj.type().get_bool("#dynamic") && - id2string(obj.get_identifier()).find("$unknown")== - std::string::npos) + // If the template row is of heap kind, we need to ensure the + // transitive closure over the set of all paths + if(templ_row.mem_kind==heap_domaint::HEAP && + points_to.type().get_bool("#dynamic") && + points_to.id()==ID_symbol && + id2string(to_symbol_expr(points_to).get_identifier()).find( + "$unknown")== + std::string::npos) + { + // Find row with corresponding member field of the pointed object + // (obj.member) + int member_val_index; + member_val_index= + find_member_row( + points_to, + templ_row.member, + actual_loc, + templ_row.kind); + if(member_val_index>=0 && !inv[member_val_index].nondet) { - // Find row with corresponding member field of the pointed object - // (obj.member) - int member_val_index; - member_val_index= - find_member_row( - obj, - templ_row.member, - actual_loc, - templ_row.kind); - if(member_val_index>=0 && !inv[member_val_index].nondet) + // Add all paths from obj.next to p + if(heap_domain.add_transitivity( + row, + static_cast(member_val_index), + inv)) { - // Add all paths from obj.next to p - if(heap_domain.add_transitivity( - row, - static_cast(member_val_index), - inv)) - { - improved=true; - const std::string expr_str= - from_expr(ns, "", heap_domain.templ[member_val_index].expr); - debug() << "Add all paths: " << expr_str - << ", through: " << from_expr(ns, "", obj) << eom; - } + improved=true; + const std::string expr_str= + from_expr(ns, "", heap_domain.templ[member_val_index].expr); + debug() << "Add all paths: " << expr_str + << ", through: " << from_expr(ns, "", points_to) << eom; } } } - else - { - if(heap_domain.set_nondet(row, inv)) - { - improved=true; - debug() << "Set nondet" << eom; - } - } // Recursively update all rows that are dependent on this row if(templ_row.mem_kind==heap_domaint::HEAP) @@ -310,7 +299,8 @@ int strategy_solver_heapt::find_member_row( templ_row.mem_kind==heap_domaint::HEAP) { std::string id=id2string(to_symbol_expr(templ_row.expr).get_identifier()); - if(id.find(obj_id)!=std::string::npos) + if(id.find(obj_id)!=std::string::npos && + id.find_first_of(".")==obj_id.length()) { int loc=heap_domain.get_symbol_loc(templ_row.expr); if(loc>max_loc && @@ -420,6 +410,18 @@ void strategy_solver_heapt::initialize( } } +/*******************************************************************\ + +Function: strategy_solver_heapt::clear_pointing_rows + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + void strategy_solver_heapt::clear_pointing_rows( const heap_domaint::rowt &row, heap_domaint::heap_valuet &value) @@ -427,9 +429,77 @@ void strategy_solver_heapt::clear_pointing_rows( heap_domaint::heap_row_valuet &row_value= static_cast(value[row]); + std::vector to_remove; for(auto &ptr : row_value.pointed_by) { - debug() << "Clearing row: " << ptr << eom; - value[ptr].clear(); + if(ptr!=row) + { + debug() << "Clearing row: " << ptr << eom; + value[ptr].clear(); + to_remove.push_back(ptr); + } } + for(auto &r : to_remove) + row_value.pointed_by.erase(r); +} + +/*******************************************************************\ + +Function: strategy_solver_heapt::get_points_to_dest + + Inputs: + + Outputs: + + Purpose: Get an address where the given pointer points to in the current + solver iteration. Returns nil_exprt if the value of the pointer + is nondet. + +\*******************************************************************/ + +const exprt strategy_solver_heapt::get_points_to_dest( + const exprt &pointer, + const exprt &templ_row_expr) +{ + exprt value=solver.get(pointer); + // Value from the solver must be converted into an expression + exprt ptr_value=heap_domain.value_to_ptr_exprt(value); + + if((ptr_value.id()==ID_constant && + to_constant_expr(ptr_value).get_value()==ID_NULL) || + ptr_value.id()==ID_symbol) + { + // Add equality p == NULL or p == symbol + return ptr_value; + } + else if(ptr_value.id()==ID_address_of) + { + // Template row pointer points to the heap (p = &obj) + debug() << from_expr(ns, "", ptr_value) << eom; + assert(ptr_value.id()==ID_address_of); + if(to_address_of_expr(ptr_value).object().id()!=ID_symbol) + { + // If solver did not return address of a symbol, it is considered + // as nondet value. + return nil_exprt(); + } + + symbol_exprt obj=to_symbol_expr( + to_address_of_expr(ptr_value).object()); + + if(obj.type()!=templ_row_expr.type() && + ns.follow(templ_row_expr.type().subtype())!=ns.follow(obj.type())) + { + if(!is_cprover_symbol(templ_row_expr)) + { + // If types disagree, it's a nondet (solver assigned random value) + return nil_exprt(); + } + } + + // Add equality p == &obj + return obj; + } + else + return nil_exprt(); } diff --git a/src/domains/strategy_solver_heap.h b/src/domains/strategy_solver_heap.h index f7a0859a8..757da4d86 100644 --- a/src/domains/strategy_solver_heap.h +++ b/src/domains/strategy_solver_heap.h @@ -40,9 +40,13 @@ class strategy_solver_heapt:public strategy_solver_baset protected: heap_domaint &heap_domain; - std::set loop_guards; + std::set> loop_guards; std::set updated_rows; + const exprt get_points_to_dest( + const exprt &pointer, + const exprt &templ_row_expr); + int find_member_row( const exprt &obj, const irep_idt &member, diff --git a/src/domains/strategy_solver_heap_interval.cpp b/src/domains/strategy_solver_heap_interval.cpp deleted file mode 100644 index 1932f3852..000000000 --- a/src/domains/strategy_solver_heap_interval.cpp +++ /dev/null @@ -1,83 +0,0 @@ -/*******************************************************************\ - -Module: Strategy solver for combination of shape and interval domains. - -Author: Viktor Malik - -\*******************************************************************/ - -#include "strategy_solver_heap_interval.h" - -/*******************************************************************\ - -Function: strategy_solver_heap_intervalt::iterate - - Inputs: - - Outputs: - - Purpose: Run iteration of each solver separately, but every time - in the context of the current invariant found by the other - solver. The interval solving is also restricted to - a symbolic path found by the heap solver. - -\*******************************************************************/ - -bool strategy_solver_heap_intervalt::iterate( - strategy_solver_baset::invariantt &_inv) -{ - heap_interval_domaint::heap_interval_valuet &inv= - static_cast(_inv); - - // Run one iteration of heap solver in the context of invariant from - // the interval solver - solver.new_context(); - solver << heap_interval_domain.interval_domain.to_pre_constraints( - inv.interval_value); - bool heap_improved=heap_solver.iterate(inv.heap_value); - solver.pop_context(); - - if(heap_improved) - { - // If heap part was improved, restrict interval part to found symbolic path - symbolic_path=heap_solver.symbolic_path; - heap_interval_domain.interval_domain.restrict_to_sympath(symbolic_path); - } - - // Run one interation of interval solver in the context of invariant from - // the heap solver - solver.new_context(); - solver << heap_interval_domain.heap_domain.to_pre_constraints(inv.heap_value); - bool interval_improved=interval_solver.iterate(inv.interval_value); - solver.pop_context(); - - if(heap_improved) - heap_interval_domain.interval_domain.undo_restriction(); - - return heap_improved || interval_improved; -} - -/*******************************************************************\ - -Function: strategy_solver_heap_intervalt::set_message_handler - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void strategy_solver_heap_intervalt::set_message_handler( - message_handlert &_message_handler) -{ - heap_solver.set_message_handler(_message_handler); - interval_solver.set_message_handler(_message_handler); -} - -void strategy_solver_heap_intervalt::clear_symbolic_path() -{ - heap_solver.symbolic_path.clear(); - interval_solver.symbolic_path.clear(); -} diff --git a/src/domains/strategy_solver_heap_tpolyhedra.cpp b/src/domains/strategy_solver_heap_tpolyhedra.cpp new file mode 100644 index 000000000..53625a76c --- /dev/null +++ b/src/domains/strategy_solver_heap_tpolyhedra.cpp @@ -0,0 +1,86 @@ +/*******************************************************************\ + +Module: Strategy solver for combination of shape and template + polyhedra domains. + +Author: Viktor Malik + +\*******************************************************************/ + +#include "strategy_solver_heap_tpolyhedra.h" + +/*******************************************************************\ + +Function: strategy_solver_heap_tpolyhedrat::iterate + + Inputs: + + Outputs: + + Purpose: Run iteration of each solver separately, but every time + in the context of the current invariant found by the other + solver. The template polyhedra solving is also restricted to + a symbolic path found by the heap solver. + +\*******************************************************************/ + +bool strategy_solver_heap_tpolyhedrat::iterate( + strategy_solver_baset::invariantt &_inv) +{ + heap_tpolyhedra_domaint::heap_tpolyhedra_valuet &inv= + static_cast(_inv); + + // Run one iteration of heap solver in the context of invariant from + // the template polyhedra solver + solver.new_context(); + solver << heap_tpolyhedra_domain.polyhedra_domain.to_pre_constraints( + inv.tpolyhedra_value); + bool heap_improved=heap_solver.iterate(inv.heap_value); + solver.pop_context(); + + if(heap_improved) + { + // If heap part was improved, restrict template polyhedra part to the found + // symbolic path + symbolic_path=heap_solver.symbolic_path; + heap_tpolyhedra_domain.polyhedra_domain.restrict_to_sympath(symbolic_path); + } + + // Run one interation of the template polyhedra solver in the context of + // invariant from the heap solver + solver.new_context(); + solver << heap_tpolyhedra_domain.heap_domain.to_pre_constraints( + inv.heap_value); + bool tpolyhedra_improved=tpolyhedra_solver.iterate(inv.tpolyhedra_value); + solver.pop_context(); + + if(heap_improved) + heap_tpolyhedra_domain.polyhedra_domain.undo_restriction(); + + return heap_improved || tpolyhedra_improved; +} + +/*******************************************************************\ + +Function: strategy_solver_heap_tpolyhedrat::set_message_handler + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void strategy_solver_heap_tpolyhedrat::set_message_handler( + message_handlert &_message_handler) +{ + heap_solver.set_message_handler(_message_handler); + tpolyhedra_solver.set_message_handler(_message_handler); +} + +void strategy_solver_heap_tpolyhedrat::clear_symbolic_path() +{ + heap_solver.symbolic_path.clear(); + tpolyhedra_solver.symbolic_path.clear(); +} diff --git a/src/domains/strategy_solver_heap_interval.h b/src/domains/strategy_solver_heap_tpolyhedra.h similarity index 53% rename from src/domains/strategy_solver_heap_interval.h rename to src/domains/strategy_solver_heap_tpolyhedra.h index bb6c1baca..967f53aa8 100644 --- a/src/domains/strategy_solver_heap_interval.h +++ b/src/domains/strategy_solver_heap_tpolyhedra.h @@ -1,40 +1,41 @@ /*******************************************************************\ -Module: Strategy solver for combination of shape and interval domains. +Module: Strategy solver for combination of shape and template + polyhedra domains. Author: Viktor Malik \*******************************************************************/ -#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_H -#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_H +#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H +#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H #include "strategy_solver_base.h" -#include "heap_interval_domain.h" +#include "heap_tpolyhedra_domain.h" #include "strategy_solver_heap.h" #include "strategy_solver_binsearch.h" -class strategy_solver_heap_intervalt:public strategy_solver_baset +class strategy_solver_heap_tpolyhedrat:public strategy_solver_baset { public: - strategy_solver_heap_intervalt( - heap_interval_domaint &_heap_interval_domain, + strategy_solver_heap_tpolyhedrat( + heap_tpolyhedra_domaint &_heap_tpolyhedra_domain, incremental_solvert &_solver, const local_SSAt &SSA, const exprt &precondition, message_handlert &message_handler, template_generator_baset &template_generator): strategy_solver_baset(_solver, SSA.ns), - heap_interval_domain(_heap_interval_domain), + heap_tpolyhedra_domain(_heap_tpolyhedra_domain), heap_solver( - heap_interval_domain.heap_domain, + heap_tpolyhedra_domain.heap_domain, _solver, SSA, precondition, message_handler, template_generator), - interval_solver(heap_interval_domain.interval_domain, _solver, SSA.ns) + tpolyhedra_solver(heap_tpolyhedra_domain.polyhedra_domain, _solver, SSA.ns) { } @@ -44,11 +45,11 @@ class strategy_solver_heap_intervalt:public strategy_solver_baset void clear_symbolic_path(); protected: - heap_interval_domaint &heap_interval_domain; + heap_tpolyhedra_domaint &heap_tpolyhedra_domain; strategy_solver_heapt heap_solver; - strategy_solver_binsearcht interval_solver; + strategy_solver_binsearcht tpolyhedra_solver; }; -#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_H +#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H diff --git a/src/domains/strategy_solver_heap_interval_sympath.cpp b/src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp similarity index 66% rename from src/domains/strategy_solver_heap_interval_sympath.cpp rename to src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp index f940883fd..53fcb1546 100644 --- a/src/domains/strategy_solver_heap_interval_sympath.cpp +++ b/src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Strategy solver for heap-interval domain using symbolic paths +Module: Strategy solver for heap-tpolyhedra domain using symbolic paths Author: Viktor Malik @@ -8,11 +8,11 @@ Author: Viktor Malik // #define DEBUG -#include "strategy_solver_heap_interval_sympath.h" +#include "strategy_solver_heap_tpolyhedra_sympath.h" /*******************************************************************\ -Function: strategy_solver_heap_interval_sympatht::set_message_handler +Function: strategy_solver_heap_tpolyhedra_sympatht::set_message_handler Inputs: @@ -21,7 +21,7 @@ Function: strategy_solver_heap_interval_sympatht::set_message_handler Purpose: \*******************************************************************/ -void strategy_solver_heap_interval_sympatht::set_message_handler( +void strategy_solver_heap_tpolyhedra_sympatht::set_message_handler( message_handlert &_message_handler) { solver.set_message_handler(_message_handler); @@ -29,7 +29,7 @@ void strategy_solver_heap_interval_sympatht::set_message_handler( /*******************************************************************\ -Function: strategy_solver_heap_interval_sympatht::iterate +Function: strategy_solver_heap_tpolyhedra_sympatht::iterate Inputs: @@ -38,12 +38,11 @@ Function: strategy_solver_heap_interval_sympatht::iterate Purpose: \*******************************************************************/ -bool strategy_solver_heap_interval_sympatht::iterate( +bool strategy_solver_heap_tpolyhedra_sympatht::iterate( strategy_solver_baset::invariantt &_inv) { - heap_interval_sympath_domaint::heap_interval_sympath_valuet &inv= - static_cast - (_inv); + auto &inv=static_cast + (_inv); bool improved; if(!new_path) @@ -53,13 +52,13 @@ bool strategy_solver_heap_interval_sympatht::iterate( #ifdef DEBUG std::cerr << "------------------------------------------\n"; std::cerr << "Same path\n"; - std::cerr << from_expr(ns, "", sympath) << "\n"; + std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n"; #endif const exprt sympath=symbolic_path.get_expr(); - domain.heap_interval_domain.restrict_to_sympath(symbolic_path); - improved=heap_interval_solver.iterate(inv.at(sympath)); + domain.heap_tpolyhedra_domain.restrict_to_sympath(symbolic_path); + improved=heap_tpolyhedra_solver.iterate(inv.at(sympath)); if(!improved) { // Invariant for the current symbolic path cannot be improved @@ -74,43 +73,42 @@ bool strategy_solver_heap_interval_sympatht::iterate( inv.erase(sympath); visited_paths.push_back(symbolic_path); - domain.heap_interval_domain.clear_aux_symbols(); - domain.heap_interval_domain.eliminate_sympaths(visited_paths); + domain.heap_tpolyhedra_domain.clear_aux_symbols(); + domain.heap_tpolyhedra_domain.eliminate_sympaths(visited_paths); clear_symbolic_path(); improved=true; new_path=true; } - else if(heap_interval_solver.symbolic_path.get_expr()!=sympath) + else if(heap_tpolyhedra_solver.symbolic_path.get_expr()!=sympath) { // The path has been altered during computation (solver has found another // loop-select guard that can be true - + auto new_sympath=heap_tpolyhedra_solver.symbolic_path.get_expr(); + inv.emplace(new_sympath, std::move(inv.at(sympath))); + inv.erase(sympath); + symbolic_path=heap_tpolyhedra_solver.symbolic_path; #ifdef DEBUG std::cerr << "Path altered\n"; + std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n"; #endif - - auto new_sympath=heap_interval_solver.symbolic_path.get_expr(); - inv.emplace(new_sympath, std::move(inv.at(sympath))); - inv.erase(sympath); - symbolic_path=heap_interval_solver.symbolic_path; } - domain.heap_interval_domain.undo_restriction(); + domain.heap_tpolyhedra_domain.undo_restriction(); } else { // Computing invariant for a new path - heap_interval_domaint::heap_interval_valuet new_value; - domain.heap_interval_domain.initialize(new_value); - improved=heap_interval_solver.iterate(new_value); + heap_tpolyhedra_domaint::heap_tpolyhedra_valuet new_value; + domain.heap_tpolyhedra_domain.initialize(new_value); + improved=heap_tpolyhedra_solver.iterate(new_value); if(improved) { + symbolic_path=heap_tpolyhedra_solver.symbolic_path; #ifdef DEBUG std::cerr << "Symbolic path:\n"; - std::cerr << from_expr(ns, "", sympath) << "\n"; + std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n"; #endif - symbolic_path=heap_interval_solver.symbolic_path; - const exprt sympath=heap_interval_solver.symbolic_path.get_expr(); + const exprt sympath=heap_tpolyhedra_solver.symbolic_path.get_expr(); inv.emplace(sympath, std::move(new_value)); new_path=false; } @@ -120,7 +118,7 @@ bool strategy_solver_heap_interval_sympatht::iterate( /*******************************************************************\ -Function: strategy_solver_heap_interval_sympatht::clear_symbolic_path +Function: strategy_solver_heap_tpolyhedra_sympatht::clear_symbolic_path Inputs: @@ -129,15 +127,15 @@ Function: strategy_solver_heap_interval_sympatht::clear_symbolic_path Purpose: \*******************************************************************/ -void strategy_solver_heap_interval_sympatht::clear_symbolic_path() +void strategy_solver_heap_tpolyhedra_sympatht::clear_symbolic_path() { symbolic_path.clear(); - heap_interval_solver.clear_symbolic_path(); + heap_tpolyhedra_solver.clear_symbolic_path(); } /*******************************************************************\ -Function: strategy_solver_heap_interval_sympatht::is_current_path_feasible +Function: strategy_solver_heap_tpolyhedra_sympatht::is_current_path_feasible Inputs: @@ -154,8 +152,8 @@ Function: strategy_solver_heap_interval_sympatht::is_current_path_feasible (g#lb => !g#le must be SAT) \*******************************************************************/ -bool strategy_solver_heap_interval_sympatht::is_current_path_feasible( - heap_interval_sympath_domaint::heap_interval_sympath_valuet &value) +bool strategy_solver_heap_tpolyhedra_sympatht::is_current_path_feasible( + heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet &value) { bool result=true; auto sympath=symbolic_path.get_expr(); @@ -163,7 +161,8 @@ bool strategy_solver_heap_interval_sympatht::is_current_path_feasible( // Path invariant exprt invariant; - domain.heap_interval_domain.project_on_vars(value.at(sympath), {}, invariant); + domain.heap_tpolyhedra_domain.project_on_vars( + value.at(sympath), {}, invariant); solver << invariant; for(auto &guard : symbolic_path.path_map) @@ -195,7 +194,7 @@ bool strategy_solver_heap_interval_sympatht::is_current_path_feasible( /*******************************************************************\ -Function: strategy_solver_heap_interval_sympatht::build_loop_conds_map +Function: strategy_solver_heap_tpolyhedra_sympatht::build_loop_conds_map Inputs: @@ -204,7 +203,7 @@ Function: strategy_solver_heap_interval_sympatht::build_loop_conds_map Purpose: \*******************************************************************/ -void strategy_solver_heap_interval_sympatht::build_loop_conds_map( +void strategy_solver_heap_tpolyhedra_sympatht::build_loop_conds_map( const local_SSAt &SSA) { for(auto &node : SSA.nodes) diff --git a/src/domains/strategy_solver_heap_interval_sympath.h b/src/domains/strategy_solver_heap_tpolyhedra_sympath.h similarity index 59% rename from src/domains/strategy_solver_heap_interval_sympath.h rename to src/domains/strategy_solver_heap_tpolyhedra_sympath.h index 6fb7fc17b..6bca710e3 100644 --- a/src/domains/strategy_solver_heap_interval_sympath.h +++ b/src/domains/strategy_solver_heap_tpolyhedra_sympath.h @@ -1,24 +1,24 @@ /*******************************************************************\ -Module: Strategy solver for heap-interval domain using symbolic paths +Module: Strategy solver for heap-tpolyhedra domain using symbolic paths Author: Viktor Malik \*******************************************************************/ -#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_SYMPATH_H -#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_SYMPATH_H +#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H +#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H #include "strategy_solver_base.h" -#include "heap_interval_sympath_domain.h" -#include "strategy_solver_heap_interval.h" +#include "heap_tpolyhedra_sympath_domain.h" +#include "strategy_solver_heap_tpolyhedra.h" -class strategy_solver_heap_interval_sympatht:public strategy_solver_baset +class strategy_solver_heap_tpolyhedra_sympatht:public strategy_solver_baset { public: - strategy_solver_heap_interval_sympatht( - heap_interval_sympath_domaint &_domain, + strategy_solver_heap_tpolyhedra_sympatht( + heap_tpolyhedra_sympath_domaint &_domain, incremental_solvert &_solver, const local_SSAt &SSA, const exprt &precondition, @@ -26,8 +26,8 @@ class strategy_solver_heap_interval_sympatht:public strategy_solver_baset template_generator_baset &template_generator): strategy_solver_baset(_solver, SSA.ns), domain(_domain), - heap_interval_solver( - domain.heap_interval_domain, + heap_tpolyhedra_solver( + domain.heap_tpolyhedra_domain, _solver, SSA, precondition, @@ -44,8 +44,8 @@ class strategy_solver_heap_interval_sympatht:public strategy_solver_baset void clear_symbolic_path(); protected: - heap_interval_sympath_domaint &domain; - strategy_solver_heap_intervalt heap_interval_solver; + heap_tpolyhedra_sympath_domaint &domain; + strategy_solver_heap_tpolyhedrat heap_tpolyhedra_solver; std::vector visited_paths; bool new_path=true; @@ -58,8 +58,8 @@ class strategy_solver_heap_interval_sympatht:public strategy_solver_baset void build_loop_conds_map(const local_SSAt &SSA); bool is_current_path_feasible( - heap_interval_sympath_domaint::heap_interval_sympath_valuet &value); + heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet &value); }; -#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_INTERVAL_SYMPATH_ +#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index 0f03b6722..f9a56e7bd 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -19,8 +19,8 @@ Author: Peter Schrammel #include "tpolyhedra_domain.h" #include "predabs_domain.h" #include "heap_domain.h" -#include "heap_interval_domain.h" -#include "heap_interval_sympath_domain.h" +#include "heap_tpolyhedra_domain.h" +#include "heap_tpolyhedra_sympath_domain.h" #ifdef DEBUG #include @@ -171,17 +171,46 @@ void template_generator_baset::collect_variables_loop( o_it!=SSA.ssa_objects.objects.end(); o_it++) { - ssa_domaint::phi_nodest::const_iterator p_it= - phi_nodes.find(o_it->get_identifier()); + const std::string id=id2string(o_it->get_identifier()); + ssa_domaint::phi_nodest::const_iterator p_it=phi_nodes.find(id); if(p_it==phi_nodes.end()) // object not modified in this loop continue; + exprt obj_post_guard=post_guard; + // For dynamic objects allocated within the given loop, we need to add + // guard of their allocation + if(id.find("ssa::dynamic_object$")!=std::string::npos) + { + std::string obj_id=id.substr(0, id.find_first_of(".")); + auto obj_def=SSA.ssa_analysis[n_it->location].def_map.find(obj_id); + if(obj_def!=SSA.ssa_analysis[n_it->location].def_map.end() && + obj_def->second.def.kind==ssa_domaint::deft::ALLOCATION) + { + obj_post_guard=and_exprt( + SSA.guard_symbol(obj_def->second.def.loc), + post_guard); + auto alloc_guard=SSA.allocation_guards.find(obj_id); + if(alloc_guard!=SSA.allocation_guards.end()) + obj_post_guard=and_exprt(obj_post_guard, alloc_guard->second); + } + } + + if(id.find("__CPROVER_deallocated")!=std::string::npos) + { + auto record_frees=collect_record_frees(SSA, n_it->loophead, n_it); + exprt::operandst d; + for(auto &r : record_frees) + d.push_back(equal_exprt(r, true_exprt())); + if(!d.empty()) + obj_post_guard=and_exprt(obj_post_guard, disjunction(d)); + } + symbol_exprt pre_var; get_pre_var(SSA, o_it, n_it, pre_var); exprt init_expr; get_init_expr(SSA, o_it, n_it, init_expr); - add_var(pre_var, pre_guard, post_guard, domaint::LOOP, var_specs); + add_var(pre_var, pre_guard, obj_post_guard, domaint::LOOP, var_specs); #ifdef DEBUG std::cout << "Adding " << from_expr(ns, "", in) << " " << @@ -767,15 +796,19 @@ void template_generator_baset::instantiate_standard_domains( static_cast(domain_ptr) ->add_quadratic_template(var_specs, SSA.ns); } - else if(options.get_bool_option("heap-interval")) + else if(options.get_bool_option("heap-interval") || + options.get_bool_option("heap-zones")) { filter_heap_interval_domain(); + auto polyhedra_kind=options.get_bool_option("heap-interval") + ? heap_tpolyhedra_domaint::INTERVAL + : heap_tpolyhedra_domaint::ZONES; if(options.get_bool_option("sympath")) - domain_ptr=new heap_interval_sympath_domaint( - domain_number, renaming_map, var_specs, SSA); + domain_ptr=new heap_tpolyhedra_sympath_domaint( + domain_number, renaming_map, var_specs, SSA, polyhedra_kind); else - domain_ptr=new heap_interval_domaint( - domain_number, renaming_map, var_specs, SSA.ns); + domain_ptr=new heap_tpolyhedra_domaint( + domain_number, renaming_map, var_specs, SSA.ns, polyhedra_kind); } } @@ -814,3 +847,21 @@ void template_generator_baset::filter_heap_interval_domain() } } } + +std::vector template_generator_baset::collect_record_frees( + const local_SSAt &SSA, + local_SSAt::nodest::const_iterator loop_begin, + local_SSAt::nodest::const_iterator loop_end) +{ + std::vector result; + for(auto &node : SSA.nodes) + { + if(node.location->location_number>loop_begin->location->location_number && + node.location->location_numberlocation->location_number && + node.record_free.is_not_nil()) + { + result.push_back(SSA.read_lhs(node.record_free, node.location)); + } + } + return result; +} diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index 50b3fff03..1c42a6c0c 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -71,6 +71,11 @@ class template_generator_baset:public messaget const local_SSAt &SSA, bool forward); + std::vector collect_record_frees( + const local_SSAt &SSA, + local_SSAt::nodest::const_iterator loop_begin, + local_SSAt::nodest::const_iterator loop_end); + void filter_template_domain(); void filter_equality_domain(); void filter_heap_domain(); diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index 1c6e1be44..dbbecde6e 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -17,6 +17,7 @@ Author: Peter Schrammel #include "tpolyhedra_domain.h" #include "util.h" +#include "domain.h" #define SYMB_BOUND_VAR "symb_bound#" @@ -1051,7 +1052,10 @@ void tpolyhedra_domaint::add_difference_template( for(var_specst::const_iterator v1=var_specs.begin(); v1!=var_specs.end(); ++v1) { - var_specst::const_iterator v2=v1; ++v2; + if(v1->var.type().id()==ID_pointer) + continue; + var_specst::const_iterator v2=v1; + ++v2; for(; v2!=var_specs.end(); ++v2) { kindt k=domaint::merge_kinds(v1->kind, v2->kind); @@ -1059,11 +1063,15 @@ void tpolyhedra_domaint::add_difference_template( continue; if(k==LOOP && v1->pre_guard!=v2->pre_guard) continue; // TEST: we need better heuristics + if(v2->var.type().id()==ID_pointer) + continue; exprt pre_g, post_g, aux_expr; merge_and(pre_g, v1->pre_guard, v2->pre_guard, ns); merge_and(post_g, v1->post_guard, v2->post_guard, ns); merge_and(aux_expr, v1->aux_expr, v2->aux_expr, ns); + if(post_g.is_false()) + continue; // x1-x2 add_template_row( diff --git a/src/domains/util.cpp b/src/domains/util.cpp index 4833531e6..826495123 100644 --- a/src/domains/util.cpp +++ b/src/domains/util.cpp @@ -7,6 +7,8 @@ Author: Peter Schrammel \*******************************************************************/ #include +#include +#include #include "util.h" @@ -688,3 +690,23 @@ void clean_expr(exprt &expr) } } } + +/*******************************************************************\ + +Function: is_cprover_symbol + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool is_cprover_symbol(const exprt &expr) +{ + return expr.id()==ID_symbol && + has_prefix( + id2string(to_symbol_expr(expr).get_identifier()), + CPROVER_PREFIX); +} diff --git a/src/domains/util.h b/src/domains/util.h index 790473db4..d21601a18 100644 --- a/src/domains/util.h +++ b/src/domains/util.h @@ -36,4 +36,6 @@ constant_exprt make_minusone(const typet &type); irep_idt get_original_name(const symbol_exprt &); void clean_expr(exprt &expr); +bool is_cprover_symbol(const exprt &expr); + #endif diff --git a/src/ssa/Makefile b/src/ssa/Makefile index 81460b00c..55c63720d 100644 --- a/src/ssa/Makefile +++ b/src/ssa/Makefile @@ -5,7 +5,8 @@ SRC = local_ssa.cpp ssa_var_collector.cpp \ ssa_value_set.cpp address_canonizer.cpp simplify_ssa.cpp \ ssa_build_goto_trace.cpp ssa_inliner.cpp ssa_unwinder.cpp \ unwindable_local_ssa.cpp ssa_db.cpp \ - ssa_pointed_objects.cpp ssa_heap_domain.cpp may_alias_analysis.cpp + ssa_pointed_objects.cpp ssa_heap_domain.cpp may_alias_analysis.cpp \ + dynobj_instance_analysis.cpp include ../config.inc include $(CBMC)/src/config.inc diff --git a/src/ssa/assignments.cpp b/src/ssa/assignments.cpp index 556d0d037..0820333ee 100644 --- a/src/ssa/assignments.cpp +++ b/src/ssa/assignments.cpp @@ -33,6 +33,7 @@ void assignmentst::build_assignment_map( { // make sure we have the location in the map assignment_map[it]; + allocation_map[it]; // now fill it if(it->is_assign()) @@ -44,6 +45,12 @@ void assignmentst::build_assignment_map( assign(lhs_symbolic_deref, it, ns); assign_symbolic_rhs(code_assign.rhs(), it, ns); + + // At allocations site, save newly allocated object(s) + if(code_assign.rhs().get_bool("#malloc_result")) + { + allocate(code_assign.rhs(), it, ns); + } } else if(it->is_assert()) { @@ -306,3 +313,34 @@ void assignmentst::output( out << "\n"; } } + +/*******************************************************************\ + +Function: assignmentst::allocate + + Inputs: + + Outputs: + + Purpose: Record allocation + +\*******************************************************************/ +void assignmentst::allocate( + const exprt &expr, + const assignmentst::locationt loc, + const namespacet &ns) +{ + if(expr.id()==ID_symbol && expr.type().get_bool("#dynamic")) + { + allocation_map[loc].insert(ssa_objectt(expr, ns)); + } + else if(expr.id()==ID_if) + { + allocate(to_if_expr(expr).true_case(), loc, ns); + allocate(to_if_expr(expr).false_case(), loc, ns); + } + else if(expr.id()==ID_address_of) + allocate(to_address_of_expr(expr).object(), loc, ns); + else if(expr.id()==ID_typecast) + allocate(to_typecast_expr(expr).op(), loc, ns); +} diff --git a/src/ssa/assignments.h b/src/ssa/assignments.h index f316e158f..1e4807b33 100644 --- a/src/ssa/assignments.h +++ b/src/ssa/assignments.h @@ -28,6 +28,8 @@ class assignmentst typedef std::map assignment_mapt; assignment_mapt assignment_map; + assignment_mapt allocation_map; + bool assigns(locationt loc, const ssa_objectt &object) const { assignment_mapt::const_iterator it=assignment_map.find(loc); @@ -43,6 +45,13 @@ class assignmentst return it->second; } + inline const objectst &get_allocations(locationt loc) const + { + auto it=allocation_map.find(loc); + assert(it!=allocation_map.end()); + return it->second; + } + assignmentst( const goto_programt &_goto_program, const namespacet &_ns, @@ -78,6 +87,11 @@ class assignmentst const exprt &expr, const locationt &loc, const namespacet &ns); + + void allocate( + const exprt &expr, + const locationt loc, + const namespacet &ns); }; #endif diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp new file mode 100644 index 000000000..32d1454ad --- /dev/null +++ b/src/ssa/dynobj_instance_analysis.cpp @@ -0,0 +1,321 @@ +/*******************************************************************\ + +Module: Analysis of the number of instances of abstract dynamic objects. + In some cases, multiple instances must be used so that the + analysis is sound. + +Author: Viktor Malik, viktor.malik@gmail.com + +\*******************************************************************/ + +#include +#include +#include +#include "dynobj_instance_analysis.h" +#include "ssa_dereference.h" + +/*******************************************************************\ + +Function: has_deref_of + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +bool has_deref_of(const exprt &expr, const exprt &pointer) +{ + if(expr.id()==ID_dereference && to_dereference_expr(expr).pointer()==pointer) + return true; + forall_operands(it, expr) + { + if(has_deref_of(*it, pointer)) + return true; + } + return false; +} + +/*******************************************************************\ + +Function: remove_dereferences + + Inputs: + + Outputs: + + Purpose: Isolate all dereferences of some pointer in must-alias + paritioning. + +\*******************************************************************/ +void remove_dereferences(const exprt &pointer, must_alias_setst &instances) +{ + for(auto &i : instances) + { + if(has_deref_of(i, pointer)) + instances.isolate(i); + } +} + +/*******************************************************************\ + +Function: replace_pointer_in_deref + + Inputs: + + Outputs: + + Purpose: Replace pointer in derefence expression by another pointer. + +\*******************************************************************/ +void replace_pointer_in_deref(exprt &deref, const exprt &src, const exprt &dest) +{ + if(deref.id()==ID_dereference && to_dereference_expr(deref).pointer()==src) + deref=dereference_exprt(dest, deref.type()); + + Forall_operands(it, deref)replace_pointer_in_deref(*it, src, dest); +} + +/*******************************************************************\ + +Function: add_aliased_dereferences + + Inputs: + + Outputs: + + Purpose: Add dereferences of all aliased pointers to instances. + When dereference of a pointer is put to some must-alias + equivalence class, dereferences of aliased pointers must + be added to the same class as well. + +\*******************************************************************/ +void add_aliased_dereferences(const exprt &pointer, must_alias_setst &instances) +{ + // We must copy instances so that we can alter them while iterating + auto inst_copy=instances; + for(auto &i : inst_copy) + { + if(i.id()==ID_symbol && pointer.id()==ID_symbol && i!=pointer && + instances.same_set(i, pointer)) + { + for(auto &deref_i : inst_copy) + { + if(has_deref_of(deref_i, i)) + { + exprt deref_copy=deref_i; + replace_pointer_in_deref(deref_copy, i, pointer); + instances.make_union(deref_i, deref_copy); + } + } + } + } +} + +/*******************************************************************\ + +Function: dynobj_instance_domaint::rhs_concretisation + + Inputs: + + Outputs: + + Purpose: Concretise pointer expressions that occur at some RHS and + did not occur before (assume they do not alias with anything). + +\*******************************************************************/ +void dynobj_instance_domaint::rhs_concretisation( + const exprt &guard, + ai_domain_baset::locationt loc, + ai_baset &ai, + const namespacet &ns) +{ + forall_operands(it, guard) + { + if(it->id()==ID_symbol || it->id()==ID_member) + { + bool found=false; + for(const auto &i : must_alias_relations) + { + size_t n; + found|=!i.second.get_number(*it, n); + } + if(!found) + { + // 1) now make dereference + const auto &values= + static_cast(ai).value_analysis[loc]; + const auto guard_deref=dereference(guard, values, "", ns); + auto value_set=values(guard_deref, ns).value_set; + // 2) then isolate for all values in value set of dereferences + for(auto &v : value_set) + { + auto &instances=must_alias_relations[v.symbol_expr()]; + instances.isolate(*it); + } + } + } + else + { + rhs_concretisation(*it, loc, ai, ns); + } + } +} + +/*******************************************************************\ + +Function: dynobj_instance_domaint::transform + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void dynobj_instance_domaint::transform( + ai_domain_baset::locationt from, + ai_domain_baset::locationt to, + ai_baset &ai, + const namespacet &ns) +{ + if(from->is_assign()) + { + const code_assignt &assignment=to_code_assign(from->code); + const exprt lhs=symbolic_dereference(assignment.lhs(), ns); + + // Do not include CPROVER symbols + if(lhs.id()==ID_symbol && + has_prefix( + id2string(to_symbol_expr(lhs).get_identifier()), + CPROVER_PREFIX)) + return; + + if(assignment.rhs().get_bool("#malloc_result")) + { + // For allocation site, the assigned pointer has no aliases + const auto &values= + static_cast(ai).value_analysis[to]; + const auto lhs_deref=dereference(assignment.lhs(), values, "", ns); + auto value_set=values(lhs_deref, ns).value_set; + for(auto &v : value_set) + must_alias_relations[v.symbol_expr()].isolate(lhs); + } + else + { + // For other assignments, use value analysis to get all pointers pointing + // to a dynamic object and then update must-alias sets. + exprt rhs=assignment.rhs(); + if(rhs.id()==ID_typecast) + rhs=to_typecast_expr(rhs).op(); + + const auto &values= + static_cast(ai).value_analysis[from]; + const auto rhs_deref=dereference(rhs, values, "", ns); + auto value_set=values(rhs_deref, ns).value_set; + for(auto &v : value_set) + { + auto &instances=must_alias_relations[v.symbol_expr()]; + instances.isolate(assignment.lhs()); + instances.make_union(assignment.lhs(), rhs); + + remove_dereferences(assignment.lhs(), instances); + add_aliased_dereferences(assignment.lhs(), instances); + + live_pointers[v.symbol_expr()].insert(rhs); + } + } + } + else if(from->is_goto() || from->is_assume() || from->is_assert()) + rhs_concretisation(from->guard, from, ai, ns); + else if(from->is_dead()) + { + const exprt &symbol=to_code_dead(from->code).symbol(); + const auto &values= + static_cast(ai).value_analysis[from]; + auto value_set=values(symbol, ns).value_set; + for(auto &v : value_set) + { + live_pointers[v.symbol_expr()].erase(symbol); + } + } +} + +/*******************************************************************\ + +Function: dynobj_instance_domaint::merge + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +bool dynobj_instance_domaint::merge( + const dynobj_instance_domaint &other, + ai_domain_baset::locationt from, + ai_domain_baset::locationt to) +{ + bool result=false; + for(auto &obj : other.must_alias_relations) + { + if(must_alias_relations.find(obj.first)==must_alias_relations.end()) + { + must_alias_relations.insert(obj); + result=true; + } + else + { + if(must_alias_relations.at(obj.first).join(obj.second)) + result=true; + } + + if(other.live_pointers.find(obj.first)!=other.live_pointers.end()) + { + auto &other_pointers=other.live_pointers.at(obj.first); + live_pointers[obj.first].insert( + other_pointers.begin(), other_pointers.end()); + } + } + return result; +} + +/*******************************************************************\ + +Function: dynobj_instance_domaint::output + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void dynobj_instance_domaint::output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const +{ + for(const auto &o : must_alias_relations) + { + out << o.first.get_identifier() << ":\n"; + for(const exprt &p : o.second) + { + size_t n; + o.second.get_number(p, n); + out << " " << o.second.find_number(n) << ": " << from_expr(ns, "", p) + << "\n"; + } + + if(live_pointers.find(o.first)==live_pointers.end()) + continue; + out << "Live: "; + for(const auto &v : live_pointers.at(o.first)) + { + out << from_expr(ns, "", v) << " "; + } + out << "\n"; + } +} diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h new file mode 100644 index 000000000..2dd170a21 --- /dev/null +++ b/src/ssa/dynobj_instance_analysis.h @@ -0,0 +1,191 @@ +/*******************************************************************\ + +Module: Analysis of the number of instances of abstract dynamic objects. + +Author: Viktor Malik, viktor.malik@gmail.com + +Description: In some cases, multiple instances must be used so that the + analysis is sound. The analysis computes for each allocation + site 'a' and each program location 'i' a set of pointer + expressions that may point to some object allocated at 'a' + in the location 'i'. Then, a must-alias relation is computed + over these sets and the maximum number of equivalence classes + gives the number of required objects for the given allocation + site. + +\*******************************************************************/ + +#ifndef CPROVER_2LS_SSA_DYNOBJ_INSTANCE_ANALYSIS_H +#define CPROVER_2LS_SSA_DYNOBJ_INSTANCE_ANALYSIS_H + + +#include +#include +#include "ssa_object.h" +#include "ssa_value_set.h" + +/*******************************************************************\ + + Set partitioning by must-alias relation (it is an equivalence). + It extends the standard union find structure, particularly using + a custom join and equality. + +\*******************************************************************/ +class must_alias_setst:public union_find +{ +public: + bool join(const must_alias_setst &other) + { + if(!equal(other)) + { + // Find new elements (those that are unique to one of the sets) + auto new_elements=sym_diff_elements(other); + // Copy *this + auto original=*this; + + // Make intersection (into *this) which contains all common elements + // (after retyping to vector) + clear(); + std::set common_elements; + for(auto &e1 : original) + { + if(new_elements.find(e1)!=new_elements.end()) + continue; + + isolate(e1); + for(auto &e2 : common_elements) + if(original.same_set(e1, e2) && other.same_set(e1, e2)) + make_union(e1, e2); + common_elements.insert(e1); + } + + for(auto &e_new : new_elements) + { + bool added=false; + // First, try to find some new element that is already in *this and that + // is in the same class as e_new in one of the sets + auto this_copy(*this); + for(auto &e : this_copy) + { + if(new_elements.find(e)!=new_elements.end() && + (original.same_set(e, e_new) || other.same_set(e, e_new))) + { + make_union(e, e_new); + added=true; + } + } + if(!added) + { + // Find all sets to which e_new should be added by comparing with + // common elements + // The map will contain: set_number(in *this) -> set_representative + std::map dest_sets; + for(auto &e : common_elements) + { + if(original.same_set(e_new, e) || other.same_set(e_new, e)) + { + size_t n; + get_number(e, n); + if(dest_sets.find(n)==dest_sets.end()) + dest_sets.emplace(n, e); + } + } + + // If there is just one set to add e_new to, add it there, otherwise + // isolate it + if(dest_sets.size()==1) + make_union(e_new, dest_sets.begin()->second); + else + isolate(e_new); + } + } + return true; + } + return false; + } + +protected: + // Two partitionings are equal if they contain same elements partitioned + // in same sets (not necessarily having same numbers). + bool equal(const must_alias_setst &other) + { + if(size()!=other.size()) + return false; + + for(auto &e1 : *this) + { + size_t n; + if(other.get_number(e1, n)) + return false; + for(auto &e2 : *this) + if(same_set(e1, e2)!=other.same_set(e1, e2)) + return false; + } + return true; + } + + // Symmetric difference of elements + std::set sym_diff_elements(const must_alias_setst &other) + { + std::set result; + size_t n; + for(auto &e : *this) + if(get_number(e, n)) + result.insert(e); + for(auto &e : other) + if(get_number(e, n)) + result.insert(e); + return result; + } +}; + +class dynobj_instance_domaint:public ai_domain_baset +{ +public: + // Must-alias relation for each dynamic object (corresponding to allocation + // site). + std::map must_alias_relations; + // Set of live pointers pointing to dynamic object. + std::map> live_pointers; + + void transform( + locationt from, + locationt to, + ai_baset &ai, + const namespacet &ns) override; + void output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const override; + bool merge( + const dynobj_instance_domaint &other, + locationt from, + locationt to); + +private: + void rhs_concretisation( + const exprt &guard, + ai_domain_baset::locationt loc, + ai_baset &ai, + const namespacet &ns); +}; + +class dynobj_instance_analysist:public ait +{ +public: + dynobj_instance_analysist( + const goto_functionst::goto_functiont &goto_function, + const namespacet &ns, + ssa_value_ait &_value_ai): + value_analysis(_value_ai) + { + operator()(goto_function, ns); + } + +protected: + ssa_value_ait &value_analysis; + + friend class dynobj_instance_domaint; +}; + +#endif // CPROVER_2LS_SSA_DYNOBJ_INSTANCE_ANALYSIS_H diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 0422ef8a9..6ca775df8 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -57,7 +57,8 @@ void local_SSAt::build_SSA() build_guard(i_it); build_assertions(i_it); build_function_call(i_it); - build_unknown_objs(i_it); +// build_unknown_objs(i_it); + collect_record_frees(i_it); } // collect custom templates in loop heads @@ -390,7 +391,10 @@ void local_SSAt::build_phi_nodes(locationt loc) const locationt &iloc=get_location(incoming_it->first); exprt incoming_value=name(*o_it, LOOP_BACK, iloc); exprt incoming_select=name(guard_symbol(), LOOP_SELECT, iloc); - loop_guards.insert(to_symbol_expr(incoming_select)); + loop_guards.insert( + std::make_pair( + to_symbol_expr(incoming_select), + to_symbol_expr(guard_symbol(loc)))); if(rhs.is_nil()) // first rhs=incoming_value; @@ -460,6 +464,9 @@ void local_SSAt::build_transfer(locationt loc) id2string(code_assign.rhs().get(ID_identifier)). find(TEMPLATE_PREFIX)!=std::string::npos) return; + // build allocation guards map + collect_allocation_guards(code_assign, loc); + exprt deref_lhs=dereference(code_assign.lhs(), loc); exprt deref_rhs=dereference(code_assign.rhs(), loc); @@ -474,9 +481,10 @@ void local_SSAt::build_transfer(locationt loc) assign_rec(symbolic_deref_lhs, rhs, true_exprt(), loc); assign_rec( deref_lhs, - name(ssa_objectt(symbolic_deref_lhs, ns), OUT, loc), + symbolic_deref_lhs, true_exprt(), - loc); + loc, + true); } else { @@ -711,10 +719,37 @@ void local_SSAt::build_assertions(locationt loc) { if(loc->is_assert()) { - const exprt deref_rhs=dereference(loc->guard, loc); + exprt assert=loc->guard; + if(assert.id()==ID_not && assert.op0().id()==ID_equal && + assert.op0().op1().id()==ID_pointer_object && + assert.op0().op1().op0().id()==ID_symbol) + { + std::string id=id2string( + to_symbol_expr(assert.op0().op1().op0()).get_identifier()); + if(id.find("__CPROVER_deallocated")!=std::string::npos) + { + const exprt &dealloc_symbol=assert.op0().op1().op0(); + exprt::operandst d; + for(auto &global : assignments.ssa_objects.globals) + { + if(global.get_expr().get_bool("#concrete")) + { + d.push_back( + equal_exprt( + dealloc_symbol, + typecast_exprt( + address_of_exprt(global.symbol_expr()), + dealloc_symbol.type()))); + } + } + assert=implies_exprt(disjunction(d), assert); + } + } + + const exprt deref_rhs=dereference(assert, loc); collect_iterators_rhs(deref_rhs, loc); - const exprt rhs=concretise_symbolic_deref_rhs(loc->guard, ns, loc); + const exprt rhs=concretise_symbolic_deref_rhs(assert, ns, loc); exprt c=read_rhs(rhs, loc); exprt g=guard_symbol(loc); (--nodes.end())->assertions.push_back(implies_exprt(g, c)); @@ -1310,7 +1345,8 @@ void local_SSAt::assign_rec( const exprt &lhs, const exprt &rhs, const exprt &guard, - locationt loc) + locationt loc, + bool fresh_rhs) { const typet &type=ns.follow(lhs.type()); @@ -1330,7 +1366,7 @@ void local_SSAt::assign_rec( { member_exprt new_lhs(lhs, it->get_name(), it->type()); member_exprt new_rhs(rhs, it->get_name(), it->type()); - assign_rec(new_lhs, new_rhs, guard, loc); + assign_rec(new_lhs, new_rhs, guard, loc, fresh_rhs); } return; @@ -1346,7 +1382,8 @@ void local_SSAt::assign_rec( collect_iterators_lhs(lhs_object, loc); collect_iterators_rhs(rhs, loc); - exprt ssa_rhs=read_rhs(rhs, loc); + exprt ssa_rhs=fresh_rhs ? name(ssa_objectt(rhs, ns), OUT, loc) + : read_rhs(rhs, loc); const symbol_exprt ssa_symbol=name(lhs_object, OUT, loc); @@ -1359,7 +1396,7 @@ void local_SSAt::assign_rec( const index_exprt &index_expr=to_index_expr(lhs); exprt ssa_array=index_expr.array(); exprt new_rhs=with_exprt(ssa_array, index_expr.index(), rhs); - assign_rec(index_expr.array(), new_rhs, guard, loc); + assign_rec(index_expr.array(), new_rhs, guard, loc, fresh_rhs); } else if(lhs.id()==ID_member) { @@ -1372,14 +1409,14 @@ void local_SSAt::assign_rec( { union_exprt new_rhs( member_expr.get_component_name(), rhs, compound.type()); - assign_rec(member_expr.struct_op(), new_rhs, guard, loc); + assign_rec(member_expr.struct_op(), new_rhs, guard, loc, fresh_rhs); } else if(compound_type.id()==ID_struct) { exprt member_name(ID_member_name); member_name.set(ID_component_name, member_expr.get_component_name()); with_exprt new_rhs(compound, member_name, rhs); - assign_rec(compound, new_rhs, guard, loc); + assign_rec(compound, new_rhs, guard, loc, fresh_rhs); } } else if(lhs.id()==ID_complex_real) @@ -1389,7 +1426,7 @@ void local_SSAt::assign_rec( const complex_typet &complex_type=to_complex_type(op.type()); exprt imag_op=unary_exprt(ID_complex_imag, op, complex_type.subtype()); complex_exprt new_rhs(rhs, imag_op, complex_type); - assign_rec(op, new_rhs, guard, loc); + assign_rec(op, new_rhs, guard, loc, fresh_rhs); } else if(lhs.id()==ID_complex_imag) { @@ -1398,7 +1435,7 @@ void local_SSAt::assign_rec( const complex_typet &complex_type=to_complex_type(op.type()); exprt real_op=unary_exprt(ID_complex_real, op, complex_type.subtype()); complex_exprt new_rhs(real_op, rhs, complex_type); - assign_rec(op, new_rhs, guard, loc); + assign_rec(op, new_rhs, guard, loc, fresh_rhs); } else if(lhs.id()==ID_if) { @@ -1436,7 +1473,8 @@ void local_SSAt::assign_rec( name(guard_symbol(), OBJECT_SELECT, loc)); cond=and_exprt(cond, other_cond); } - exprt new_rhs=if_exprt(cond, rhs, if_expr.true_case()); + exprt orig_rhs=fresh_rhs ? name(ssa_objectt(rhs, ns), OUT, loc) : rhs; + exprt new_rhs=if_exprt(cond, orig_rhs, if_expr.true_case()); assign_rec( if_expr.true_case(), new_rhs, @@ -1447,7 +1485,8 @@ void local_SSAt::assign_rec( if_expr.false_case(), rhs, and_exprt(guard, not_exprt(if_expr.cond())), - loc); + loc, + fresh_rhs); } else if(lhs.id()==ID_byte_extract_little_endian || lhs.id()==ID_byte_extract_big_endian) @@ -1459,7 +1498,7 @@ void local_SSAt::assign_rec( exprt new_rhs=byte_extract_exprt( byte_extract_expr.id(), rhs, byte_extract_expr.offset(), new_lhs.type()); - assign_rec(new_lhs, new_rhs, guard, loc); + assign_rec(new_lhs, new_rhs, guard, loc, fresh_rhs); } else throw "UNKNOWN LHS: "+lhs.id_string(); // NOLINT(*) @@ -1856,8 +1895,11 @@ void local_SSAt::build_unknown_objs(locationt loc) const exprt &rhs=code_assign.rhs(); if(rhs.get_bool("#malloc_result")) { - const exprt &addr_of_do= + const exprt &malloc_res= rhs.id()==ID_typecast ? to_typecast_expr(rhs).op() : rhs; + const exprt &addr_of_do= + malloc_res.id()==ID_if ? to_if_expr(malloc_res).true_case() + : malloc_res; const exprt &dyn_obj=to_address_of_expr(addr_of_do).object(); const typet &dyn_type=ns.follow(dyn_obj.type()); @@ -2080,3 +2122,94 @@ exprt local_SSAt::concretise_symbolic_deref_rhs( all_symbolic_deref_defined(symbolic_deref_rhs, ns, loc)? symbolic_deref_rhs:deref_rhs; } + +/********************************************************************\ + +Function: local_SSAt::collect_allocation_guards + + Inputs: + + Outputs: + + Purpose: Collect allocation guards for the given location + +\*******************************************************************/ + +void local_SSAt::collect_allocation_guards( + const code_assignt &assign, + locationt loc) +{ + if(!assign.rhs().get_bool("#malloc_result")) + return; + + exprt rhs=assign.rhs(); + if(rhs.id()==ID_typecast) + rhs=to_typecast_expr(rhs).op(); + if(rhs.id()==ID_if) + { + get_alloc_guard_rec( + to_if_expr(rhs).true_case(), read_rhs(to_if_expr(rhs).cond(), loc)); + get_alloc_guard_rec( + to_if_expr(rhs).false_case(), + read_rhs(not_exprt(to_if_expr(rhs).cond()), loc)); + } +} + +/********************************************************************\ + +Function: local_SSAt::collect_record_frees + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void local_SSAt::collect_record_frees(local_SSAt::locationt loc) +{ + if(loc->is_decl()) + { + const exprt &symbol=to_code_decl(loc->code).symbol(); + if(symbol.id()!=ID_symbol) + return; + + std::string id=id2string(to_symbol_expr(symbol).get_identifier()); + if(id.find("free::")!=std::string::npos && + id.find("::record")!=std::string::npos) + { + (--nodes.end())->record_free=symbol; + } + } +} + +/********************************************************************\ + +Function: local_SSAt::get_alloc_guard_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void local_SSAt::get_alloc_guard_rec(const exprt &expr, exprt guard) +{ + if(expr.id()==ID_symbol && expr.type().get_bool("#dynamic")) + { + allocation_guards.emplace(to_symbol_expr(expr).get_identifier(), guard); + } + else if(expr.id()==ID_if) + { + get_alloc_guard_rec( + to_if_expr(expr).true_case(), and_exprt(guard, to_if_expr(expr).cond())); + get_alloc_guard_rec( + to_if_expr(expr).false_case(), + and_exprt(guard, not_exprt(to_if_expr(expr).cond()))); + } + else if(expr.id()==ID_typecast) + get_alloc_guard_rec(to_typecast_expr(expr).op(), guard); + else if(expr.id()==ID_address_of) + get_alloc_guard_rec(to_address_of_expr(expr).object(), guard); +} diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 087fbe32e..0dbc6bdc0 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -96,6 +96,8 @@ class local_SSAt std::list::iterator loophead; // link to loop head node // otherwise points to nodes.end() + exprt record_free=nil_exprt(); + void output(std::ostream &, const namespacet &) const; inline bool empty() const @@ -154,6 +156,9 @@ class local_SSAt typedef std::list dyn_obj_assignst; std::map dyn_obj_assigns; + // Map dynamic object names to guards of their allocation + std::map allocation_guards; + bool has_function_calls() const; const namespacet &ns; @@ -193,7 +198,8 @@ class local_SSAt const exprt &lhs, const exprt &rhs, const exprt &guard, - locationt loc); + locationt loc, + bool fresh_rhs=false); void collect_iterators_rhs(const exprt &expr, locationt loc); void collect_iterators_lhs(const ssa_objectt &object, locationt loc); @@ -240,7 +246,7 @@ class local_SSAt // Collect all loop_guards that will represent symbolic paths used in heap // domain - var_sett loop_guards; + std::set> loop_guards; void get_globals( locationt loc, @@ -277,6 +283,10 @@ class local_SSAt void build_assertions(locationt loc); void build_unknown_objs(locationt loc); + void collect_allocation_guards(const code_assignt &assign, locationt loc); + void get_alloc_guard_rec(const exprt &expr, exprt old_guard); + void collect_record_frees(locationt loc); + // custom templates void collect_custom_templates(); replace_mapt template_newvars; diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index 8c4a1003f..b392faa98 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "malloc_ssa.h" /*******************************************************************\ @@ -54,6 +56,105 @@ inline static typet c_sizeof_type_rec(const exprt &expr) /*******************************************************************\ +Function: create_dynamic_object + + Inputs: + + Outputs: + + Purpose: Create new dynamic object, insert it into the symbol table + and return its address. + +\*******************************************************************/ + +exprt create_dynamic_object( + const std::string &suffix, + const typet &type, + symbol_tablet &symbol_table, + bool concrete) +{ + symbolt value_symbol; + + value_symbol.base_name="dynamic_object"+suffix; + value_symbol.name="ssa::"+id2string(value_symbol.base_name); + value_symbol.is_lvalue=true; + value_symbol.type=type; + value_symbol.type.set("#dynamic", true); + value_symbol.mode=ID_C; + symbol_table.add(value_symbol); + + address_of_exprt address_of_object; + + if(type.id()==ID_array) + { + address_of_object.type()=pointer_typet(value_symbol.type.subtype()); + index_exprt index_expr(value_symbol.type.subtype()); + index_expr.array()=value_symbol.symbol_expr(); + index_expr.index()=gen_zero(index_type()); + address_of_object.op0()=index_expr; + } + else + { + address_of_object.op0()=value_symbol.symbol_expr(); + if(concrete) + address_of_object.op0().set("#concrete", true); + address_of_object.type()=pointer_typet(value_symbol.type); + } + + return address_of_object; +} + +/*******************************************************************\ + +Function: collect_pointer_vars + + Inputs: + + Outputs: + + Purpose: Collect all variables (symbols and their members) of pointer + type with given pointed type. + +\*******************************************************************/ + +std::vector collect_pointer_vars( + const symbol_tablet &symbol_table, + const typet &pointed_type) +{ + namespacet ns(symbol_table); + std::vector pointers; + forall_symbols(it, symbol_table.symbols) + { + if(ns.follow(it->second.type).id()==ID_struct) + { + for(auto &component : to_struct_type( + ns.follow(it->second.type)).components()) + { + if(component.type().id()==ID_pointer) + { + if(ns.follow(component.type().subtype())==ns.follow(pointed_type)) + { + pointers.push_back( + member_exprt( + it->second.symbol_expr(), component.get_name(), + component.type())); + } + } + } + } + if(it->second.type.id()==ID_pointer) + { + if(ns.follow(it->second.type.subtype())==ns.follow(pointed_type)) + { + pointers.push_back(it->second.symbol_expr()); + } + } + } + return pointers; +} + +/*******************************************************************\ + Function: malloc_ssa Inputs: @@ -67,7 +168,8 @@ Function: malloc_ssa exprt malloc_ssa( const side_effect_exprt &code, const std::string &suffix, - symbol_tablet &symbol_table) + symbol_tablet &symbol_table, + bool alloc_concrete) { if(code.operands().size()!=1) throw "malloc expected to have one operand"; @@ -132,37 +234,42 @@ exprt malloc_ssa( std::cout << "OBJECT_TYPE: " << from_type(ns, "", object_type) << std::endl; #endif - // value - symbolt value_symbol; + auto pointers=collect_pointer_vars(symbol_table, object_type); - value_symbol.base_name="dynamic_object"+suffix; - value_symbol.name="ssa::"+id2string(value_symbol.base_name); - value_symbol.is_lvalue=true; - value_symbol.type=object_type; - value_symbol.type.set("#dynamic", true); - value_symbol.mode=ID_C; - symbol_table.add(value_symbol); - - address_of_exprt address_of; - - if(object_type.id()==ID_array) + exprt object=create_dynamic_object( + suffix, object_type, symbol_table, !alloc_concrete); + if(object.type()!=code.type()) + object=typecast_exprt(object, code.type()); + exprt result; + if(alloc_concrete) { - address_of.type()=pointer_typet(value_symbol.type.subtype()); - index_exprt index_expr(value_symbol.type.subtype()); - index_expr.array()=value_symbol.symbol_expr(); - index_expr.index()=gen_zero(index_type()); - address_of.op0()=index_expr; + exprt concrete_object=create_dynamic_object( + suffix+"$co", object_type, symbol_table, true); + + // Create nondet symbol + symbolt nondet_symbol; + nondet_symbol.base_name="nondet"+suffix; + nondet_symbol.name="ssa::"+id2string(nondet_symbol.base_name); + nondet_symbol.is_lvalue=true; + nondet_symbol.type=bool_typet(); + nondet_symbol.mode=ID_C; + symbol_table.add(nondet_symbol); + + exprt::operandst pointer_equs; + for(auto &ptr : pointers) + { + pointer_equs.push_back(equal_exprt(ptr, concrete_object)); + } + exprt cond=and_exprt( + nondet_symbol.symbol_expr(), + not_exprt(disjunction(pointer_equs))); + + if(concrete_object.type()!=code.type()) + concrete_object=typecast_exprt(concrete_object, code.type()); + result=if_exprt(cond, concrete_object, object); } else - { - address_of.op0()=value_symbol.symbol_expr(); - address_of.type()=pointer_typet(value_symbol.type); - } - - exprt result=address_of; - - if(result.type()!=code.type()) - result=typecast_exprt(result, code.type()); + result=object; result.set("#malloc_result", true); @@ -187,7 +294,8 @@ static bool replace_malloc_rec( const std::string &suffix, symbol_tablet &symbol_table, const exprt &malloc_size, - unsigned loc_number) + unsigned loc_number, + bool alloc_concrete) { if(expr.id()==ID_side_effect && to_side_effect_expr(expr).get_statement()==ID_malloc) @@ -196,9 +304,8 @@ static bool replace_malloc_rec( expr.op0()=malloc_size; expr=malloc_ssa( - to_side_effect_expr(expr), - "$"+i2string(loc_number)+suffix, - symbol_table); + to_side_effect_expr(expr), "$"+i2string(loc_number)+suffix, symbol_table, + alloc_concrete); return true; } else @@ -206,7 +313,8 @@ static bool replace_malloc_rec( bool result=false; Forall_operands(it, expr) { - if(replace_malloc_rec(*it, suffix, symbol_table, malloc_size, loc_number)) + if(replace_malloc_rec( + *it, suffix, symbol_table, malloc_size, loc_number, alloc_concrete)) result=true; } return result; @@ -227,7 +335,8 @@ Function: replace_malloc bool replace_malloc( goto_modelt &goto_model, - const std::string &suffix) + const std::string &suffix, + bool alloc_concrete) { bool result=false; Forall_goto_functions(f_it, goto_model.goto_functions) @@ -280,11 +389,9 @@ bool replace_malloc( } } if(replace_malloc_rec( - code_assign.rhs(), - suffix, - goto_model.symbol_table, - malloc_size, - i_it->location_number)) + code_assign.rhs(), suffix, goto_model.symbol_table, malloc_size, + i_it->location_number, + alloc_concrete && loop_end!=f_it->second.body.instructions.end())) { result=(loop_end!=f_it->second.body.instructions.end()); } @@ -293,3 +400,96 @@ bool replace_malloc( } return result; } + +/*******************************************************************\ + +Function: set_var_always_to_true + + Inputs: goto_model + name_cond Function returning true for names of variables + to be set. + + Outputs: + + Purpose: Set undefined boolean variable to true. + Finds declaration of a variable whose name matches the given + condition and adds an instruction var = TRUE after + the declaration. + +\*******************************************************************/ + +void set_var_always_to_true( + goto_modelt &goto_model, + std::functionname_cond) +{ + Forall_goto_functions(f_it, goto_model.goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if(i_it->is_decl()) + { + code_declt &code_decl=to_code_decl(i_it->code); + if(code_decl.symbol().id()==ID_symbol) + { + std::string decl_id= + id2string(to_symbol_expr(code_decl.symbol()).get_identifier()); + if(name_cond(decl_id)) + { + auto assign=f_it->second.body.insert_after(i_it); + assign->make_assignment(); + assign->code=code_assignt(code_decl.symbol(), true_exprt()); + } + } + } + } + f_it->second.body.compute_location_numbers(); + f_it->second.body.compute_target_numbers(); + f_it->second.body.compute_incoming_edges(); + } +} + +/*******************************************************************\ + +Function: allow_record_malloc + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void allow_record_malloc(goto_modelt &goto_model) +{ + set_var_always_to_true( + goto_model, + [](std::string &name) + { + return name.find("malloc::")!=std::string::npos && + name.find("::record_malloc")!=std::string::npos; + }); +} + +/*******************************************************************\ + +Function: allow_record_memleak + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void allow_record_memleak(goto_modelt &goto_model) +{ + set_var_always_to_true( + goto_model, + [](std::string &name) + { + return name.find("malloc::")!=std::string::npos && + name.find("::record_may_leak")!=std::string::npos; + }); +} diff --git a/src/ssa/malloc_ssa.h b/src/ssa/malloc_ssa.h index bd6c2ec5c..753dc6e57 100644 --- a/src/ssa/malloc_ssa.h +++ b/src/ssa/malloc_ssa.h @@ -15,10 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com exprt malloc_ssa( const side_effect_exprt &, const std::string &suffix, - symbol_tablet &); + symbol_tablet &, + bool alloc_concrete); bool replace_malloc( goto_modelt &goto_model, - const std::string &suffix); + const std::string &suffix, + bool alloc_concrete); + +void allow_record_malloc(goto_modelt &goto_model); +void allow_record_memleak(goto_modelt &goto_model); #endif diff --git a/src/ssa/ssa_domain.cpp b/src/ssa/ssa_domain.cpp index 3e2d2bb65..610f85be1 100644 --- a/src/ssa/ssa_domain.cpp +++ b/src/ssa/ssa_domain.cpp @@ -121,6 +121,17 @@ void ssa_domaint::transform( def_entry.def.kind=deft::ASSIGNMENT; def_entry.source=from; } + + auto allocations= + static_cast(ai).assignments.get_allocations(from); + for(auto &alloc : allocations) + { + irep_idt identifier=alloc.get_identifier(); + def_entryt &def_entry=def_map[identifier]; + def_entry.def.loc=from; + def_entry.def.kind=deft::ALLOCATION; + def_entry.source=from; + } } else if(from->is_dead()) { @@ -210,6 +221,43 @@ bool ssa_domaint::merge( } else { + // Do not create PHIs for allocations + if(d_it_a->second.def.kind==deft::ALLOCATION || + d_it_b->second.def.kind==deft::ALLOCATION) + continue; + + // Do not create PHIs for join of PHI and allocation with assignment + auto alloc_def=get_object_allocation_def(id, def_map); + if(alloc_def!=def_map.end()) + { + if(d_it_b->second.def.kind!=deft::ASSIGNMENT && + to->location_number>alloc_def->second.def.loc->location_number && + to->location_number>d_it_a->second.def.loc->location_number && + to->location_number>d_it_b->second.def.loc->location_number) + { + def_map[id]=d_it_a->second; + def_map[id2string(id).substr(0, id2string(id).find_first_of("."))]= + alloc_def->second; + result=true; + continue; + } + } + alloc_def=get_object_allocation_def(id, b.def_map); + if(alloc_def!=b.def_map.end()) + { + if(d_it_a->second.def.kind!=deft::ASSIGNMENT && + to->location_number>alloc_def->second.def.loc->location_number && + to->location_number>d_it_b->second.def.loc->location_number && + to->location_number>d_it_a->second.def.loc->location_number) + { + def_map[id]=d_it_b->second; + def_map[id2string(id).substr(0, id2string(id).find_first_of("."))]= + alloc_def->second; + result=true; + continue; + } + } + // Arg! Data coming from two sources from two different definitions! // We produce a new phi node. loc_def_mapt &phi_node=phi_nodes[id]; @@ -235,6 +283,37 @@ bool ssa_domaint::merge( /*******************************************************************\ +Function: ssa_domaint::get_object_allocation_def + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +ssa_domaint::def_mapt::const_iterator ssa_domaint::get_object_allocation_def( + const irep_idt &id, + const ssa_domaint::def_mapt &def_map) +{ + auto def=def_map.find(id); + std::string id_str=id2string(id); + if(def!=def_map.end() && + def->second.def.kind==deft::ASSIGNMENT && + id_str.find("ssa::dynamic_object$")!=std::string::npos) + { + // Check if corresponding dynamic object has been allocated in that branch + std::string dyn_obj_id=id_str.substr(0, id_str.find_first_of(".")); + auto dyn_obj_def=def_map.find(dyn_obj_id); + if(dyn_obj_def!=def_map.end() && + dyn_obj_def->second.def.kind==deft::ALLOCATION) + return dyn_obj_def; + } + return def_map.end(); +} + +/*******************************************************************\ + Function: ssa_ait::initialize Inputs: diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h index 679fdbc59..c6767973b 100644 --- a/src/ssa/ssa_domain.h +++ b/src/ssa/ssa_domain.h @@ -20,7 +20,7 @@ class ssa_domaint:public ai_domain_baset struct deft { deft():kind(ASSIGNMENT) { } - typedef enum { INPUT, ASSIGNMENT, PHI } kindt; + typedef enum { INPUT, ASSIGNMENT, PHI, ALLOCATION } kindt; kindt kind; locationt loc; @@ -42,6 +42,7 @@ class ssa_domaint:public ai_domain_baset case deft::INPUT: out << "INPUT"; break; case deft::ASSIGNMENT: out << d.loc->location_number; break; case deft::PHI: out << "PHI" << d.loc->location_number; break; + case deft::ALLOCATION: out << "ALLOC" << d.loc->location_number; break; } return out; } @@ -84,6 +85,12 @@ class ssa_domaint:public ai_domain_baset const ssa_domaint &b, locationt from, locationt to); + +private: + static std::map::const_iterator + get_object_allocation_def( + const irep_idt &id, + const def_mapt &def_map); }; class ssa_ait:public ait diff --git a/src/ssa/ssa_pointed_objects.cpp b/src/ssa/ssa_pointed_objects.cpp index b48671827..b5c51fad1 100644 --- a/src/ssa/ssa_pointed_objects.cpp +++ b/src/ssa/ssa_pointed_objects.cpp @@ -386,6 +386,7 @@ const exprt symbolic_dereference(const exprt &expr, const namespacet &ns) { member_exprt member=to_member_expr(expr); member.compound()=symbolic_dereference(member.compound(), ns); + copy_pointed_info(member, member.compound()); member.set( "#has_symbolic_deref", diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp index d8e6bffb0..20ba39d47 100644 --- a/src/ssa/ssa_value_set.cpp +++ b/src/ssa/ssa_value_set.cpp @@ -7,7 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ // #define DEBUG -#define COMPETITION +// #define COMPETITION #ifdef DEBUG #include diff --git a/src/ssa/unwindable_local_ssa.cpp b/src/ssa/unwindable_local_ssa.cpp index e53155c7f..da31f1b7a 100644 --- a/src/ssa/unwindable_local_ssa.cpp +++ b/src/ssa/unwindable_local_ssa.cpp @@ -350,6 +350,8 @@ irep_idt unwindable_local_SSAt::get_ssa_name( pos1+=2; else if(s.substr(pos1+1, 2)=="ls") pos1+=2; + else if(s.substr(pos1+1, 2)=="os") + pos1+=2; else if(s.substr(pos1+1, 3)=="phi") pos1+=3; else if((pos2==pos1+13) && (s.substr(pos1+1, 12)=="return_value"))