[racerd] rationalize test suite

Summary:
The C++ tests were a bit of a mess. This diff tries to enforce the following principles:
- mark every function with `_ok` or `_bad` so that when a function appears in `issues.exp` it's easy to figure out the intention;
- mark every false negative and positive with `FP_` and `FN_` to document expectations;
- make every function access one field and participate in at most one issue report so that it's easier to assess changes.

Reviewed By: jvillard

Differential Revision: D21278627

fbshipit-source-id: 9698f716f
master
Nikos Gorogiannis 5 years ago committed by Facebook GitHub Bot
parent 2d8debc562
commit f207b3dfda

@ -13,16 +13,17 @@ class Basic {
public:
Basic() {}
void set(int new_value) {
not_guarded = new_value;
void set_not_guarded_ok(int new_value) { not_guarded = new_value; }
int get_not_guarded_ok() { return not_guarded; }
void set_well_guarded_ok(int new_value) {
mutex_.lock();
well_guarded = new_value;
suspiciously_read = new_value;
mutex_.unlock();
suspiciously_written = new_value;
}
int get1() {
int get_well_guarded_ok() {
int result;
mutex_.lock();
result = well_guarded;
@ -30,19 +31,28 @@ class Basic {
return result;
}
int get2() {
int result;
void set_suspiciously_read_bad(int new_value) {
mutex_.lock();
result = suspiciously_written;
suspiciously_read = new_value;
mutex_.unlock();
return result;
}
int get3() { return not_guarded; }
int get_suspiciously_read_bad() { return suspiciously_read; }
int get4() { return suspiciously_read; }
void set_suspiciously_written_bad(int new_value) {
// the only reason we report here is because of the use of a mutex
mutex_.lock();
mutex_.unlock();
suspiciously_written = new_value;
}
int get5() { return get_private_suspiciously_read(); }
int get_suspiciously_written_bad() {
int result;
mutex_.lock();
result = suspiciously_written;
mutex_.unlock();
return result;
}
void write_array_under_lock_ok(char* arr1) {
mutex_.lock();
@ -52,17 +62,15 @@ class Basic {
int read_array_outside_lock_ok(char* arr2, int i) { return arr2[i]; }
void set_double(int new_value) {
void set_double_lock_guarded_ok(int new_value) {
mutex_.lock();
mutex_2.lock();
double_lock_guarded = new_value;
mutex_2.unlock();
single_lock_guarded = new_value;
single_lock_suspiciously_read = new_value;
mutex_.unlock();
}
int test_double_lock_1_ok() {
int read_double_lock_guarded_ok() {
int result;
mutex_2.lock();
result = double_lock_guarded;
@ -70,15 +78,17 @@ class Basic {
return result;
}
int test_double_lock_2_ok() {
int result;
void set_double_suspiciously_read_bad(int new_value) {
mutex_.lock();
result = single_lock_guarded;
mutex_2.lock();
single_lock_suspiciously_read = new_value;
mutex_2.unlock();
mutex_.unlock();
return result;
}
int test_double_lock_bad() { return single_lock_suspiciously_read; }
int read_double_suspiciously_read_bad() {
return single_lock_suspiciously_read;
}
private:
int well_guarded;
@ -86,11 +96,10 @@ class Basic {
int suspiciously_written;
int not_guarded;
int double_lock_guarded;
int single_lock_guarded;
int single_lock_suspiciously_read;
std::mutex mutex_;
std::mutex mutex_2;
int get_private_suspiciously_read() { return suspiciously_read; }
int get_private_suspiciously_read_ok() { return suspiciously_read; }
};
} // namespace basics

@ -11,19 +11,15 @@ class BasicsNoMutex {
public:
BasicsNoMutex() {}
void set(int new_value) {
void set_ok(int new_value) {
field_1 = new_value;
field_2 = new_value;
field_3 = new_value;
}
int get1() { return field_1; }
int get2() { return field_2; }
int get_field1_ok() { return field_1; }
private:
int field_1;
int field_2;
int field_3;
};
} // namespace basics

@ -8,46 +8,20 @@
#include <mutex>
namespace constructor_formals {
struct Y {
Y() : rawStatus_(-3) {}
Y(const Y& p) = default;
Y& operator=(const Y& p) = default;
Y(Y&& p) noexcept : rawStatus_(p.rawStatus_) { p.rawStatus_ = -3; }
int rawStatus_;
};
struct S {
Y w() { return returnCode; }
Y returnCode;
};
struct SU {
void p() {
S s;
auto result = s.w();
}
};
class Basic {
public:
Basic() {}
// there can be a race here between the initializer read and the set function
// below
Basic(Basic& other) : field_(other.field_) {}
int test_locked() {
SU su;
void FN_set_under_lock_bad(int value) {
mutex_.lock();
su.p();
}
int test_not_locked() {
SU su;
su.p(); // FP fixed after adding ownership to formal parameters of
// constructors
field_ = value;
mutex_.unlock();
}
private:
std::mutex mutex_;
int field_;
};
} // namespace constructor_formals

@ -1,88 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <mutex>
#include <string>
#include <unordered_map>
namespace constructors {
struct dynamic {
enum T {
NULLT,
};
private:
struct ObjectMaker;
public:
template <class T>
dynamic(T t);
static ObjectMaker object();
dynamic(dynamic&&) noexcept;
dynamic& operator=(dynamic&&) noexcept;
dynamic& operator[](dynamic const&) &;
dynamic&& operator[](dynamic const&) &&;
template <class K, class V>
void insert(K&&, V&& val);
private:
T type_;
};
dynamic& dynamic::operator=(dynamic&& o) noexcept {
if (&o != this) {
if (type_ == o.type_) {
} else {
type_ = o.type_;
}
}
return *this;
}
struct dynamic::ObjectMaker {
friend struct dynamic;
explicit ObjectMaker() {}
ObjectMaker(ObjectMaker&&) = default;
};
inline dynamic::ObjectMaker dynamic::object() { return ObjectMaker(); }
struct BSS {
dynamic toJson_ok() const noexcept {
dynamic ret = dynamic::object();
ret["key"] = dynamic::object();
return ret;
}
dynamic& toJson_race(dynamic& ret) const noexcept {
ret["key"] = dynamic::object();
return ret;
}
};
struct TSL {
std::mutex mutex_;
void not_locked_ok(dynamic& ret) { BSS().toJson_ok(); }
void locked_ok(dynamic& ret) {
std::lock_guard<std::mutex> lock(mutex_);
BSS().toJson_ok();
}
void FN_not_locked_race(dynamic& ret) { BSS().toJson_race(ret); }
void locked_race(dynamic& ret) {
std::lock_guard<std::mutex> lock(mutex_);
BSS().toJson_race(ret);
}
};
} // namespace constructors

@ -16,12 +16,16 @@ struct A {
struct B {
void access_container_and_contents_ok(int key, int value) {
int s = map.size();
void FN_write_container_bad(int key, int value) {
mutex_.lock();
map[key].value = value;
mutex_.unlock();
}
int FN_get_bad(int key) { return map[key].value; }
int FN_size_bad() { return map.size(); }
private:
std::map<int, A> map;
std::mutex mutex_;

@ -29,36 +29,97 @@ class Basic {
public:
Basic() {}
void pointer_deref_race(int* v1) { (*v1)++; } // HIL: *(v1) := *(v1) + 1
void pointer_arith_ok(int* v2) { v2++; } // HIL: v2 := v2 + 1
void FN_pointer_deref_bad(int b) {
if (b) {
pointer_deref(&p);
} else {
mutex_.lock();
pointer_deref(&p);
mutex_.unlock();
}
}
void value_ok(int v3) { v3++; } // HIL: v3 := v3 + 1
void pointer_arith_ok(int b) {
if (b) {
pointer_arith(&q);
} else {
mutex_.lock();
pointer_arith(&q);
mutex_.unlock();
}
}
void field_race(int& f) { f++; } // HIL: *(f) := *(f) + 1
void value_ok(int b) {
if (b) {
value(h);
} else {
mutex_.lock();
value(h);
mutex_.unlock();
}
}
void mixed_deref_race(X& xparam) {
xparam.x1->w++; // HIL: xparam->x1->w := xparam->x1->w + 1
(*xparam.x1).u++; // HIL: xparam->x1->u := xparam->x1->u + 1
(**xparam.x2).a.b.c++; // HIL:*(xparam->x2)->a.b.c:= *(xparam->x2)->a.b.c+1
void FN_field_bad(int b) {
if (b) {
field(g);
} else {
mutex_.lock();
field(g);
mutex_.unlock();
}
}
void call1() {
pointer_deref_race(&p); // race - FalseNegative
pointer_arith_ok(&q); // no race
value_ok(h); // no race
field_race(g); // race - FalseNegative
mixed_deref_race(x); // race
void deref_w_bad(int b) {
if (b) {
deref_w(x);
} else {
mutex_.lock();
deref_w(x);
mutex_.unlock();
}
}
int test_lock() {
mutex_.lock();
call1();
void deref_u_bad(int b) {
if (b) {
deref_u(x);
} else {
mutex_.lock();
deref_u(x);
mutex_.unlock();
}
}
int test_unlock() { call1(); }
void deref_abc_bad(int b) {
if (b) {
deref_abc(x);
} else {
mutex_.lock();
deref_abc(x);
mutex_.unlock();
}
}
private:
void pointer_deref(int* v1) { (*v1)++; } // HIL: *(v1) := *(v1) + 1
void pointer_arith(int* v2) { v2++; } // HIL: v2 := v2 + 1
void value(int v3) { v3++; } // HIL: v3 := v3 + 1
void field(int& f) { f++; } // HIL: *(f) := *(f) + 1
void deref_w(X& xparam) {
xparam.x1->w++; // HIL: xparam->x1->w := xparam->x1->w + 1
}
void deref_u(X& xparam) {
(*xparam.x1).u++; // HIL: xparam->x1->u := xparam->x1->u + 1
}
void deref_abc(X& xparam) {
(**xparam.x2).a.b.c++; // HIL:*(xparam->x2)->a.b.c:= *(xparam->x2)->a.b.c+1
}
int g;
int h;
int p;

@ -1,25 +1,17 @@
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::get2, 36, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::get4, 43, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to basics::Basic::get_private_suspiciously_read,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->single_lock_suspiciously_read`,<Write trace>,access to `this->single_lock_suspiciously_read`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`]
codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get2, 34, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get4, 40, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::test1, 44, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/lock_guard_with_scope.cpp, basics::LockGuardWithScope::get2, 37, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/lock_guard_with_scope.cpp, basics::LockGuardWithScope::get4, 43, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/reporting.cpp, reporting::Basic::call1, 24, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to reporting::Basic::test,access to `this->x.x1->w`,<Write trace>,call to reporting::Basic::call1,call to reporting::Basic::test,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/reporting.cpp, reporting::Basic::test_unlock, 32, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to reporting::Basic::call1,call to reporting::Basic::test,access to `this->x.x1->w`,<Write trace>,call to reporting::Basic::call1,call to reporting::Basic::test,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::get_suspiciously_read_bad, 40, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::get_suspiciously_written_bad, 52, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic::read_double_suspiciously_read_bad, 90, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->single_lock_suspiciously_read`,<Write trace>,access to `this->single_lock_suspiciously_read`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_abc_bad, 94, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_abc,access to `*(this->x.x2)->a.b.c`,<Write trace>,call to dereferencing::Basic::deref_abc,access to `*(this->x.x2)->a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_abc_bad, 97, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_abc,access to `*(this->x.x2)->a.b.c`,<Write trace>,call to dereferencing::Basic::deref_abc,access to `*(this->x.x2)->a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_u_bad, 84, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_u,access to `this->x.x1->u`,<Write trace>,call to dereferencing::Basic::deref_u,access to `this->x.x1->u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_u_bad, 87, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_u,access to `this->x.x1->u`,<Write trace>,call to dereferencing::Basic::deref_u,access to `this->x.x1->u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_w_bad, 74, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_w,access to `this->x.x1->w`,<Write trace>,call to dereferencing::Basic::deref_w,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::deref_w_bad, 77, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::deref_w,access to `this->x.x1->w`,<Write trace>,call to dereferencing::Basic::deref_w,access to `this->x.x1->w`]
codetoanalyze/cpp/racerd/lock_guard_with_scope.cpp, basics::LockGuardWithScope::FP_suspiciously_written_ok, 47, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/lock_guard_with_scope.cpp, basics::LockGuardWithScope::suspiciously_read_bad, 38, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
codetoanalyze/cpp/racerd/std_lock.cpp, basics::StdLock::get_bad, 31, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->not_guarded`,<Write trace>,access to `this->not_guarded`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get2, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written1`,<Write trace>,access to `this->suspiciously_written1`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get2, 46, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written2`,<Write trace>,access to `this->suspiciously_written2`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get4, 55, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read1`,<Write trace>,access to `this->suspiciously_read1`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get4, 56, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read2`,<Write trace>,access to `this->suspiciously_read2`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get5, 64, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read1`,<Write trace>,access to `this->suspiciously_read1`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::get6, 73, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read1`,<Write trace>,access to `this->suspiciously_read1`]
codetoanalyze/cpp/racerd/without_mutex.cpp, without_mutex::WithoutMutex::get, 15, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->field_1`,<Write trace>,access to `this->field_1`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::suspiciously_read1_bad, 68, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read1`,<Write trace>,access to `this->suspiciously_read1`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::suspiciously_read2_trylock_bad, 92, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read2`,<Write trace>,access to `this->suspiciously_read2`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::suspiciously_read3_deferlock_bad, 107, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read3`,<Write trace>,access to `this->suspiciously_read3`]
codetoanalyze/cpp/racerd/unique_lock.cpp, basics::UniqueLock::suspiciously_written_ok, 78, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
codetoanalyze/cpp/racerd/without_mutex.cpp, without_mutex::WithoutMutex::get_bad, 15, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->field`,<Write trace>,access to `this->field`]

@ -11,16 +11,22 @@ namespace locals_char_array {
void f() {
char line[1024];
int x;
line[0] = line[1];
x = 0;
}
struct A {
void not_locked() { f(); }
bool locked() {
mutex_.lock();
f();
void locals_ok(int b) {
if (b) {
f();
} else {
mutex_.lock();
f();
mutex_.unlock();
}
}
std::mutex mutex_;
};

@ -17,7 +17,7 @@ class Ownership {
public:
Ownership() {}
int test0_ok() {
int struct_ok() {
X x;
mutex_.lock();
x.f = 7;
@ -25,7 +25,7 @@ class Ownership {
return x.f;
}
int test1_ok() {
int ptr_to_struct_ok() {
X* x = new X();
mutex_.lock();
x->f = 7;
@ -33,7 +33,7 @@ class Ownership {
return x->f;
}
int test2_ok() {
int copy_constructor_ok() {
X x = current; // copy constructor
mutex_.lock();
x.f = 7;
@ -41,7 +41,7 @@ class Ownership {
return x.f;
}
int FN_test2_bad() {
int FN_ptr_to_field_struct_bad() {
X* x = &current;
mutex_.lock();
x->f = 7;
@ -49,7 +49,7 @@ class Ownership {
return x->f;
}
int test3_ok(X xformal) {
int copy_formal_ok(X xformal) {
X x = xformal; // copy constructor
mutex_.lock();
x.f = 7;
@ -57,7 +57,7 @@ class Ownership {
return x.f;
}
int FN_test3_bad(X* xformal) {
int FN_ptr_to_formal_bad(X* xformal) {
X* x = xformal;
mutex_.lock();
x->f = 7;

@ -1,56 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <mutex>
namespace basics {
class LockGuard {
public:
LockGuard() {}
void set(int new_value) {
not_guarded = new_value;
suspiciously_written = new_value;
std::lock_guard<std::mutex> lock(mutex_);
well_guarded = new_value;
suspiciously_read = new_value;
}
int get1() {
int result;
std::lock_guard<std::mutex> lock(mutex_);
result = well_guarded;
return result;
}
int get2() {
int result;
std::lock_guard<std::mutex> lock(mutex_);
result = suspiciously_written;
return result;
}
int get3() { return not_guarded; }
int get4() { return suspiciously_read; }
int test1() {
int result = get1();
return suspiciously_read + result;
}
private:
int well_guarded;
int suspiciously_read;
int suspiciously_written;
int not_guarded;
std::mutex mutex_;
int test2() { return suspiciously_read; }
};
} // namespace basics

@ -13,34 +13,40 @@ class LockGuardWithScope {
public:
LockGuardWithScope() {}
void set(int new_value) {
{
std::lock_guard<std::mutex> lock(mutex_);
well_guarded = new_value;
suspiciously_read = new_value;
void not_guarded_ok(int b, int new_value) {
if (b) {
not_guarded = new_value;
} else {
return not_guarded;
}
not_guarded = new_value;
suspiciously_written = new_value;
}
int get1() {
int result;
void well_guarded_ok(int b, int new_value) {
std::lock_guard<std::mutex> lock(mutex_);
result = well_guarded;
return result;
if (b) {
well_guarded = new_value;
} else {
return well_guarded;
}
}
int get2() {
int result;
std::lock_guard<std::mutex> lock(mutex_);
result = suspiciously_written;
return result;
void suspiciously_read_bad(int b, int new_value) {
if (b) {
std::lock_guard<std::mutex> lock(mutex_);
suspiciously_read = new_value;
} else {
return suspiciously_read;
}
}
int get3() { return not_guarded; }
int get4() { return suspiciously_read; }
void FP_suspiciously_written_ok(int b, int new_value) {
if (b) {
suspiciously_written = new_value;
} else {
std::lock_guard<std::mutex> lock(mutex_);
return suspiciously_written;
}
}
private:
int well_guarded;

@ -1,38 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <mutex>
namespace reporting {
struct X {
int w;
X* x1;
};
class Basic {
public:
Basic() {}
void test(X& xparam) { xparam.x1->w++; }
void call1() {
test(x); // race
}
int test_lock() {
mutex_.lock();
call1();
}
int test_unlock() { call1(); }
private:
X x;
std::mutex mutex_;
};
} // namespace reporting

@ -1,17 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
extern int nondet_int();
extern char* nondet_string();
void loop() {
int i = 0;
char* s = nondet_string();
while (nondet_int()) {
s[i++] = "0123456789ABCDEF"[nondet_int() % 16];
}
}

@ -13,75 +13,110 @@ class UniqueLock {
public:
UniqueLock() {}
void set(int new_value) {
std::unique_lock<std::mutex> g(mutex_);
well_guarded1 = new_value;
suspiciously_read1 = new_value;
g.unlock();
not_guarded1 = new_value;
suspiciously_written1 = new_value;
int well_guarded1_ok(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_);
well_guarded1 = new_value;
return 0;
} else {
std::lock_guard<std::mutex> lock(mutex_);
return well_guarded1;
}
}
void set2(int new_value) {
std::unique_lock<std::mutex> g(mutex_, std::defer_lock);
not_guarded2 = new_value;
suspiciously_written2 = new_value;
g.lock();
well_guarded2 = new_value;
suspiciously_read2 = new_value;
g.unlock();
int well_guarded2_deferred_ok(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_, std::defer_lock);
g.lock();
well_guarded2 = new_value;
g.unlock();
return 0;
} else {
std::unique_lock<std::mutex> g(mutex_);
return well_guarded2;
}
}
int get1() {
int result;
std::lock_guard<std::mutex> lock(mutex_);
result = well_guarded1;
return result + well_guarded2;
int not_guarded1_ok(int b, int new_value) {
if (b) {
not_guarded1 = new_value;
return 0;
} else {
return not_guarded1;
}
}
int get2() {
int result;
std::lock_guard<std::mutex> lock(mutex_);
result = suspiciously_written1;
return result + suspiciously_written2;
int not_guarded2_ok(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_);
g.unlock();
not_guarded2 = new_value;
return 0;
} else {
std::unique_lock<std::mutex> g(mutex_);
g.unlock();
return not_guarded2;
}
}
int get3() {
int result = not_guarded1;
return result + not_guarded2;
int suspiciously_read1_bad(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_);
suspiciously_read1 = new_value;
return 0;
} else {
return suspiciously_read1;
}
}
int get4() {
int result = suspiciously_read1;
return result + suspiciously_read2;
int suspiciously_written_ok(int b, int new_value) {
if (b) {
suspiciously_written = new_value;
return 0;
} else {
std::unique_lock<std::mutex> g(mutex_);
return suspiciously_written;
}
}
int get5() {
std::unique_lock<std::mutex> lock(mutex_, std::try_to_lock);
if (lock.owns_lock()) {
return well_guarded1;
int suspiciously_read2_trylock_bad(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_);
suspiciously_read2 = new_value;
return 0;
} else {
return suspiciously_read1;
std::unique_lock<std::mutex> lock(mutex_, std::try_to_lock);
if (lock.owns_lock()) {
return 0;
} else {
return suspiciously_read2;
}
}
}
int get6() {
std::unique_lock<std::mutex> lock(mutex_, std::defer_lock);
if (lock.try_lock()) {
return well_guarded1;
int suspiciously_read3_deferlock_bad(int b, int new_value) {
if (b) {
std::unique_lock<std::mutex> g(mutex_);
suspiciously_read3 = new_value;
return 0;
} else {
return suspiciously_read1;
std::unique_lock<std::mutex> lock(mutex_, std::defer_lock);
if (lock.try_lock()) {
return 0;
} else {
return suspiciously_read3;
}
}
}
private:
int well_guarded1;
int suspiciously_read1;
int suspiciously_written1;
int not_guarded1;
int well_guarded2;
int suspiciously_read1;
int suspiciously_read2;
int suspiciously_written2;
int suspiciously_read3;
int suspiciously_written;
int not_guarded1;
int not_guarded2;
std::mutex mutex_;
};

@ -1,28 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <cstdarg>
#include <cstdio>
double average(int count, ...) {
va_list ap;
int j;
double sum = 0;
va_start(ap,
count); /* Requires the last fixed parameter (to get the address) */
for (j = 0; j < count; j++) {
sum += va_arg(ap, int); /* Increments ap to the next argument. */
}
va_end(ap);
return sum / count;
}
int main(int argc, char const* argv[]) {
printf("%f\n", average(3, 1, 2, 3));
return 0;
}

@ -12,14 +12,14 @@ class WithoutMutex {
public:
WithoutMutex() {}
int get() { return field_1; }
int get_bad() { return field; }
int set(std::mutex& mutex, int data) {
int set_bad(std::mutex& mutex, int data) {
std::lock_guard<std::mutex> lock(mutex);
field_1 = data;
field = data;
}
private:
int field_1;
int field;
};
} // namespace without_mutex

@ -9,7 +9,7 @@
@interface Ctor : NSObject
- (instancetype)init;
- (void)write:(int)data;
- (void)write_ok:(int)data;
@end
@implementation Ctor {
@ -27,7 +27,7 @@
return self;
}
- (void)write:(int)data {
- (void)write_ok:(int)data {
_mutex.lock();
_data = data;
_mutex.unlock();

@ -21,7 +21,7 @@
return self;
}
- (void)writeZero {
- (void)write_zero_ok {
[self write:0];
}
@end

Loading…
Cancel
Save