-
Notifications
You must be signed in to change notification settings - Fork 29
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge latest changes from rework (#488)
Add proper functions #470 Generic Registers #471 Rmw base classes #475 Type Safety #478 Parsing & thread creation #479 Unit tests for thread creation #481 Move memory initialization, inlining, and thread creation from the parser to processing passes #483 Inlining of nondet_int #485 Various fixes/cleanup #487 --------- Co-authored-by: Thomas Haas <[email protected]> Co-authored-by: René Pascal Maseli <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
- Loading branch information
1 parent
6e09d54
commit 70a496c
Showing
227 changed files
with
104,538 additions
and
5,328 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
#include <stdint.h> | ||
#include <assert.h> | ||
|
||
int main() | ||
{ | ||
int x = 0; | ||
while (x != 5) { | ||
if (__VERIFIER_nondet_int() == 0) { | ||
x += 2; | ||
} else { | ||
x += 3; | ||
} | ||
} | ||
assert (0); | ||
|
||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
#include <pthread.h> | ||
#include <stdatomic.h> | ||
|
||
/* | ||
The test shows chaining of thread creations + parameter passing, i.e, the spawned thread | ||
spawns another thread and passes its argument to that one. | ||
Expected result: PASS | ||
Current result: PASS | ||
*/ | ||
|
||
atomic_int data; | ||
|
||
void *thread2(void *arg) | ||
{ | ||
data = (int)arg; | ||
} | ||
|
||
void *thread1(void *arg) | ||
{ | ||
pthread_t t2; | ||
pthread_create(&t2, NULL, thread2, arg); | ||
pthread_join(t2, NULL); | ||
} | ||
|
||
int main() | ||
{ | ||
pthread_t t1; | ||
pthread_create(&t1, NULL, thread1, (void*)42); | ||
pthread_join(t1, NULL); | ||
|
||
assert(data == 42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
#include <pthread.h> | ||
#include <stdatomic.h> | ||
|
||
/* | ||
The test checks if inlining of thread-creating functions works properly. | ||
Expected result: PASS | ||
Current result: | ||
- development: FAIL | ||
- rework: Parsing error (matching between pthread_join and pthread_create fails) | ||
*/ | ||
|
||
atomic_int data; | ||
|
||
void *thread2(void *arg) | ||
{ | ||
data = 42; | ||
} | ||
|
||
void threadCreator(pthread_t *t) { | ||
pthread_create(t, NULL, thread2, NULL); | ||
} | ||
|
||
void *thread1(void *arg) | ||
{ | ||
pthread_t t; | ||
threadCreator(&t); | ||
pthread_join(t, NULL); | ||
} | ||
|
||
int main() | ||
{ | ||
pthread_t t1; | ||
pthread_create(&t1, NULL, thread1, NULL); | ||
pthread_join(t1, NULL); | ||
|
||
assert(data == 42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
#include <pthread.h> | ||
#include <stdatomic.h> | ||
|
||
/* | ||
The test checks if inlining of thread-creating functions + reassigning pthread_t variables works properly. | ||
Expected result: PASS | ||
Current result: | ||
- development: PASS | ||
- rework: Parsing error (matching between pthread_join and pthread_create fails) | ||
*/ | ||
|
||
atomic_int data; | ||
|
||
void *thread2(void *arg) | ||
{ | ||
data = 42; | ||
} | ||
|
||
pthread_t threadCreator() { | ||
pthread_t t; | ||
pthread_create(&t, NULL, thread2, NULL); | ||
return t; | ||
} | ||
|
||
void *thread1(void *arg) | ||
{ | ||
pthread_t t = threadCreator(); | ||
pthread_join(t, NULL); | ||
} | ||
|
||
int main() | ||
{ | ||
pthread_t t1; | ||
pthread_create(&t1, NULL, thread1, NULL); | ||
pthread_join(t1, NULL); | ||
|
||
assert(data == 42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
#include <pthread.h> | ||
#include <stdatomic.h> | ||
|
||
/* | ||
The test checks if inlining of thread-creating/joining functions + reassigning pthread_t variables works properly. | ||
Expected result: PASS | ||
Current result: | ||
- development: PASS | ||
- rework: Parsing error (matching between pthread_join and pthread_create fails) | ||
*/ | ||
|
||
atomic_int data; | ||
|
||
void *thread2(void *arg) | ||
{ | ||
data = 42; | ||
} | ||
|
||
pthread_t threadCreator() { | ||
pthread_t t; | ||
pthread_create(&t, NULL, thread2, NULL); | ||
return t; | ||
} | ||
|
||
void threadJoiner(pthread_t t) { | ||
pthread_join(t, NULL); | ||
} | ||
|
||
void *thread1(void *arg) | ||
{ | ||
threadJoiner(threadCreator()); | ||
} | ||
|
||
int main() | ||
{ | ||
pthread_t t1; | ||
pthread_create(&t1, NULL, thread1, NULL); | ||
pthread_join(t1, NULL); | ||
|
||
assert(data == 42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
#include <pthread.h> | ||
#include <stdatomic.h> | ||
|
||
/* | ||
The test shows thread-local storage + initialization. | ||
Expected result: PASS | ||
*/ | ||
|
||
__thread atomic_int data; | ||
__thread int val = 5; // All threads should see the same init value | ||
|
||
void check(int value) { | ||
// Extra indirection, so that if thread locals are (wrongly) created | ||
// per function rather than per thread, we get an error. | ||
assert (data == value); | ||
assert (val == 5); | ||
} | ||
|
||
void *thread2(void *arg) | ||
{ | ||
data = (int)arg; | ||
check(2); | ||
} | ||
|
||
void *thread1(void *arg) | ||
{ | ||
data = (int)arg; | ||
|
||
pthread_t t2; | ||
pthread_create(&t2, NULL, thread2, 2); | ||
pthread_join(t2, NULL); | ||
|
||
check(1); | ||
} | ||
|
||
int main() | ||
{ | ||
pthread_t t1; | ||
pthread_create(&t1, NULL, thread1, (void*)1); | ||
pthread_join(t1, NULL); | ||
|
||
check(0); | ||
} |
Oops, something went wrong.