|
|
|
/*
|
|
|
|
* Copyright (c) 2018-present, Facebook, Inc.
|
|
|
|
*
|
|
|
|
* This source code is licensed under the MIT license found in the
|
|
|
|
* LICENSE file in the root directory of this source tree.
|
|
|
|
*/
|
|
|
|
|
|
|
|
#include <stdlib.h>
|
|
|
|
#include <vector>
|
|
|
|
|
|
|
|
void basic_loop_count_ok(int n) {
|
|
|
|
for (int i = 0; i < n; i++) {
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
struct foo {
|
|
|
|
int* val;
|
|
|
|
};
|
|
|
|
|
|
|
|
struct list {
|
|
|
|
struct list* next;
|
|
|
|
struct foo* foo;
|
|
|
|
};
|
|
|
|
|
|
|
|
int invalidate_node_alias_bad(struct list* head, int cond) {
|
|
|
|
int* result = 0;
|
|
|
|
struct list* x = head;
|
|
|
|
if (cond) {
|
|
|
|
result = x->next->foo->val;
|
|
|
|
delete result;
|
|
|
|
} else {
|
|
|
|
x = x->next;
|
|
|
|
struct list* y = x->next;
|
|
|
|
result = x->foo->val;
|
|
|
|
delete result;
|
|
|
|
}
|
|
|
|
return *result;
|
|
|
|
}
|
[pulse] record attributes inside memory cells instead of separately
Summary:
It turns out keeping attributes (such as invalidation facts) separate
from the memory is a bad idea and leads to loss of precision and false
positives, as seen in the new test (which previously generated a
report).
Allow me to illustrate on this example, which is a stylised version of
the issue in the added test: previously we'd have:
```
state1 = { x = 1; invalids={} }
state2 = { x = 2; invalids ={1} }
join(state1, state2) = { x = {1, 2}; invalids={{1, 2}} }
```
So even though none of the states said that `x` pointed to an invalid
location, the join state says it does because `1` and `2` have been
glommed together. The fact `x=1` from `state1` and the fact "1 is
invalid" from `state2` conspire together and `x` is now invalid even
though it shouldn't.
Instead, if we record attributes as part of the memory we get that `x`
is still valid after the join:
```
state1 = { x = (1, {}) }
state2 = { x = (2, {}) }
join(state1, state2) = { x = ({1, 2}, {}) }
```
Reviewed By: mbouaziz
Differential Revision: D12958130
fbshipit-source-id: 53dc81cc7
6 years ago
|
|
|
|
|
|
|
void list_delete_ok(struct list** l) {
|
|
|
|
auto head = *l;
|
|
|
|
*l = nullptr;
|
|
|
|
while (head) {
|
|
|
|
auto tmp = head;
|
|
|
|
head = head->next;
|
|
|
|
if (tmp->foo) {
|
|
|
|
free(tmp->foo);
|
|
|
|
tmp->foo = nullptr;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
[pulse] record attributes inside memory cells instead of separately
Summary:
It turns out keeping attributes (such as invalidation facts) separate
from the memory is a bad idea and leads to loss of precision and false
positives, as seen in the new test (which previously generated a
report).
Allow me to illustrate on this example, which is a stylised version of
the issue in the added test: previously we'd have:
```
state1 = { x = 1; invalids={} }
state2 = { x = 2; invalids ={1} }
join(state1, state2) = { x = {1, 2}; invalids={{1, 2}} }
```
So even though none of the states said that `x` pointed to an invalid
location, the join state says it does because `1` and `2` have been
glommed together. The fact `x=1` from `state1` and the fact "1 is
invalid" from `state2` conspire together and `x` is now invalid even
though it shouldn't.
Instead, if we record attributes as part of the memory we get that `x`
is still valid after the join:
```
state1 = { x = (1, {}) }
state2 = { x = (2, {}) }
join(state1, state2) = { x = ({1, 2}, {}) }
```
Reviewed By: mbouaziz
Differential Revision: D12958130
fbshipit-source-id: 53dc81cc7
6 years ago
|
|
|
struct BasicStruct {
|
|
|
|
void some_method() {}
|
|
|
|
BasicStruct();
|
|
|
|
~BasicStruct();
|
[pulse] record attributes inside memory cells instead of separately
Summary:
It turns out keeping attributes (such as invalidation facts) separate
from the memory is a bad idea and leads to loss of precision and false
positives, as seen in the new test (which previously generated a
report).
Allow me to illustrate on this example, which is a stylised version of
the issue in the added test: previously we'd have:
```
state1 = { x = 1; invalids={} }
state2 = { x = 2; invalids ={1} }
join(state1, state2) = { x = {1, 2}; invalids={{1, 2}} }
```
So even though none of the states said that `x` pointed to an invalid
location, the join state says it does because `1` and `2` have been
glommed together. The fact `x=1` from `state1` and the fact "1 is
invalid" from `state2` conspire together and `x` is now invalid even
though it shouldn't.
Instead, if we record attributes as part of the memory we get that `x`
is still valid after the join:
```
state1 = { x = (1, {}) }
state2 = { x = (2, {}) }
join(state1, state2) = { x = ({1, 2}, {}) }
```
Reviewed By: mbouaziz
Differential Revision: D12958130
fbshipit-source-id: 53dc81cc7
6 years ago
|
|
|
};
|
|
|
|
|
|
|
|
int nested_loops_ok() {
|
|
|
|
while (true) {
|
|
|
|
BasicStruct x;
|
|
|
|
for (;;) {
|
|
|
|
x.some_method();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
extern bool some_bool();
|
|
|
|
extern BasicStruct mk_basic_struct();
|
|
|
|
|
|
|
|
void cond_inside_loop_ok() {
|
|
|
|
while (true) {
|
|
|
|
BasicStruct x;
|
|
|
|
if (some_bool()) {
|
|
|
|
x = mk_basic_struct();
|
|
|
|
}
|
|
|
|
|
|
|
|
x.some_method();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
void nested_loops3_ok(std::vector<BasicStruct>* c) {
|
|
|
|
for (auto& b : *c) {
|
|
|
|
(&b)->~BasicStruct();
|
|
|
|
}
|
|
|
|
}
|