Skip to content
Open
Show file tree
Hide file tree
Changes from 34 commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
35ca9fc
Alloc-free verification prototype
natgavrilenko Dec 10, 2024
3940bb8
Using stack pointer in alloc tests
natgavrilenko Jan 20, 2025
a4b8f1d
Support alloc-free dev (#794)
CapZTr Mar 11, 2025
20e84e4
Init setup
Apr 10, 2025
ddc0e11
Add Alloc and MemFree to witness for debugging
Apr 10, 2025
8631ddc
Modified some memory models and tests
Apr 30, 2025
44ead61
Fix event and relation extraction of alloc-free for witness
May 7, 2025
e5d6a28
Modify some relation and constraint definitions
May 13, 2025
8ff67e2
Merge development into this branch
May 13, 2025
5f7440f
Remove unnecessary definition
May 13, 2025
9803e52
Clean c11 and rc11
May 14, 2025
0659c5e
Modify as comments
May 14, 2025
616dfda
Clean code to prepare rebase
Jun 26, 2025
ec9717e
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Jun 26, 2025
4de382e
Fix merging
Jul 3, 2025
fd2593f
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Jul 3, 2025
d752cab
Fix CI tests: Attempt 1
Jul 11, 2025
89a4219
By Natalia: Add Termination event
Jul 17, 2025
5d21aee
Fix CI tests
Jul 17, 2025
cd4a5c1
Fix CI tests
Jul 18, 2025
702527a
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Jul 24, 2025
f21d510
Fix bugs from merge
Jul 24, 2025
02998bb
Add AllocPtrGraph & AllocMemGraph, modify as comments
Aug 1, 2025
9143013
Add Intrinsics pthread_detach (#905)
xeren Aug 7, 2025
1cdc4c3
Reverse vmm.cat
Aug 7, 2025
5f715e1
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Aug 7, 2025
01e6ac1
Fix bugs from merge
Aug 7, 2025
e602036
Remove vmm from AllocFreeTest
Aug 7, 2025
3a08b77
Add DI source location for frees
Aug 7, 2025
2b60b6c
Add MemAlloc & MemFree to witness
Aug 8, 2025
f4ca35d
Remove unused imports
Aug 8, 2025
8eebe94
Remove obsolete pthread mutex events. (#921)
xeren Aug 11, 2025
e48a53f
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Aug 14, 2025
8d8ca49
Make MemAlloc and MemFree extend GenericMemoryEvent
Aug 21, 2025
efa54cc
Remove M tag when copy alloc
Aug 21, 2025
4c531d7
Add HeapAlloc
Aug 22, 2025
944045f
Add HeapAlloc class
Aug 28, 2025
946bf92
Revert to efa54cc18
Aug 29, 2025
f1a05c6
Make MemAlloc & MemFree extend AbstractMemoryCoreEvent
Aug 29, 2025
1d49035
Use LazyEventGraph for loc and allocMem in LazyRelationAnalysis
Aug 29, 2025
2404a04
Fix EqualityAliasAnalysis
Aug 29, 2025
5d28e57
Fix EqualityAliasAnalysis
Aug 29, 2025
d7b7b4e
Small change to LazyRelationAnalysis
Aug 29, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions benchmarks/alloc/test_err_address.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

free(arr + sizeof(int));

return 0;
}
27 changes: 27 additions & 0 deletions benchmarks/alloc/test_err_double_free_1.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

free(arr);
free(arr);

return 0;
}
28 changes: 28 additions & 0 deletions benchmarks/alloc/test_err_double_free_2.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

free(arr);

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

free(arr);

return 0;
}
23 changes: 23 additions & 0 deletions benchmarks/alloc/test_err_no_alloc_1.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
free(arr);

return NULL;
}

int main()
{
pthread_t t1;
int *arr;

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

return 0;
}
26 changes: 26 additions & 0 deletions benchmarks/alloc/test_err_no_alloc_2.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr;

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

free(arr);

return 0;
}
24 changes: 24 additions & 0 deletions benchmarks/alloc/test_err_no_free.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

return 0;
}
26 changes: 26 additions & 0 deletions benchmarks/alloc/test_err_race.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
free(arr);

return NULL;
}

int main()
{
pthread_t t1;
int *arr;

pthread_create(&t1, NULL, thread_1, (void*)&arr);
arr = malloc(2 * sizeof(int));
pthread_join(t1, NULL);

free(arr);

return 0;
}
25 changes: 25 additions & 0 deletions benchmarks/alloc/test_err_use_after_free.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
free(arr);
pthread_join(t1, NULL);

return 0;
}
27 changes: 27 additions & 0 deletions benchmarks/alloc/test_err_use_before_alloc.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr;

pthread_create(&t1, NULL, thread_1, (void*)&arr);
arr = malloc(2 * sizeof(int));
pthread_join(t1, NULL);

free(arr);

return 0;
}
26 changes: 26 additions & 0 deletions benchmarks/alloc/test_ok_1.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

free(arr);

return 0;
}
26 changes: 26 additions & 0 deletions benchmarks/alloc/test_ok_2.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>
#include <stdatomic.h>

void *thread_1(void *arg)
{
int *arr = *((int**)arg);
arr[0] = 0;
arr[1] = 1;

free(arr);

return NULL;
}

int main()
{
pthread_t t1;
int *arr = malloc(2 * sizeof(int));

pthread_create(&t1, NULL, thread_1, (void*)&arr);
pthread_join(t1, NULL);

return 0;
}
8 changes: 4 additions & 4 deletions benchmarks/lfds/dglm.c
Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,13 @@ void *worker(void *arg)

intptr_t index = ((intptr_t) arg);

enqueue(index);
enqueue(index);
int r = dequeue();

assert(r != EMPTY);
data[r] = 1;
assert(r != EMPTY);
data[r] = 1;

return NULL;
return NULL;
}

int main()
Expand Down
Loading
Loading