forked from esbmc/esbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[regression] added CHERI-C++ test suite
- Loading branch information
1 parent
64e0ad7
commit c007c8e
Showing
12 changed files
with
270 additions
and
0 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,34 @@ | ||
// TC description : | ||
// This is a modified version of 01_cheri_clear_tag_failed with trivial class ctor | ||
#include <cheri/cheric.h> | ||
#include <assert.h> | ||
|
||
char *buffer = "hello"; | ||
char *secret = "secret"; | ||
|
||
class t1 | ||
{ | ||
public: | ||
t1() { } | ||
|
||
int foo(); | ||
}; | ||
|
||
int t1::foo() { | ||
/* create valid capability: */ | ||
char *__capability valid_cap = cheri_ptr(buffer, 6); | ||
/* create a copy with tag cleared: */ | ||
char *__capability cleared_cap = cheri_cleartag(valid_cap); | ||
|
||
/* now try to dereference the capability with cleared tag */ | ||
assert(cleared_cap[0]); // this fails with tag violation exception | ||
|
||
return 0; | ||
} | ||
|
||
int main(int argc, char **argv) { | ||
t1 instance1; | ||
instance1.foo(); | ||
|
||
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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION FAILED$ |
45 changes: 45 additions & 0 deletions
45
regression/cheri-cpp/01_cheri_clear_tag_leak_failed/main.c
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,45 @@ | ||
// TC description: | ||
// This is a modified version of 01_cheri_clear_tag_leak_failed with non-trivial class ctor | ||
|
||
#include <cheri/cheric.h> | ||
#include <assert.h> | ||
|
||
char *buffer = "hello"; | ||
|
||
class t1 | ||
{ | ||
public: | ||
int i; | ||
|
||
t1() | ||
{ | ||
i = 1; | ||
} | ||
|
||
int foo(); | ||
}; | ||
|
||
|
||
|
||
int t1::foo() { | ||
/* create valid capability: */ | ||
char *__capability valid_cap = cheri_ptr(buffer, 6); | ||
/* create a copy with tag cleared: */ | ||
char *__capability cleared_cap = cheri_cleartag(valid_cap); | ||
|
||
/* this does not fail, leaking the capability base */ | ||
assert(cheri_getbase(cleared_cap)); | ||
|
||
return 0; | ||
} | ||
|
||
int main(int argc, char **argv) { | ||
|
||
t1 instance1; | ||
/* test data member in object */ | ||
assert(instance1.i == 1); | ||
|
||
instance1.foo(); | ||
|
||
return 0; | ||
} |
4 changes: 4 additions & 0 deletions
4
regression/cheri-cpp/01_cheri_clear_tag_leak_failed/test.desc
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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION FAILED$ |
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,40 @@ | ||
// TC description: | ||
// This is a modified version of 01_cheri_ptr10_successful mixed with ctor initialization list | ||
|
||
#include <stdint.h> | ||
#include <cheri/cheric.h> | ||
|
||
int nondet_int(); | ||
|
||
void* foo(void *a) { | ||
return ((void *)((intptr_t)a & (intptr_t)~1)); | ||
} | ||
|
||
class t2 | ||
{ | ||
public: | ||
int i; | ||
|
||
t2() : i(2) /*init list*/ | ||
{ | ||
} | ||
|
||
int bar(); | ||
}; | ||
|
||
|
||
int t2::bar() { | ||
int a = nondet_int() % 10; | ||
int *__capability cap_ptr = cheri_ptr(&a, sizeof(a)); | ||
assert(*cap_ptr >= 10 || *cap_ptr < 10); | ||
return 0; | ||
} | ||
|
||
int main() { | ||
t2 instance2; | ||
assert(instance2.i == 2); | ||
|
||
instance2.bar(); | ||
|
||
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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION SUCCESSFUL$ |
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,39 @@ | ||
// TC description: | ||
// This is a modified version of 01_cheri_ptr11_failed with constructor array initializer | ||
|
||
#include <stdint.h> | ||
#include <cheri/cheric.h> | ||
|
||
int nondet_int(); | ||
|
||
class t2 | ||
{ | ||
public: | ||
int a[5]; | ||
|
||
t2() : a{0,1,2,3,4} | ||
{ | ||
} | ||
|
||
int bar(); | ||
}; | ||
|
||
void* foo(void *a) { | ||
return ((void *)((intptr_t)a & (intptr_t)~1)); | ||
} | ||
|
||
int bar() { | ||
int a = nondet_int() % 10; | ||
int *__capability cap_ptr = cheri_ptr(&a, sizeof(a)); | ||
assert(*cap_ptr < 9); | ||
return 0; | ||
} | ||
|
||
int main() { | ||
t2 t; | ||
assert(t.a[0] == 0); | ||
|
||
t.bar(); | ||
|
||
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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION FAILED$ |
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,46 @@ | ||
// TC description: | ||
// This is a modified version of 01_cheri_ptr12_successful with a non-trivial destructor | ||
|
||
#include <stdio.h> | ||
#include <string.h> | ||
#include <cheri/cheric.h> | ||
|
||
char *buffer = "hello"; | ||
char *secret = "secret"; | ||
|
||
int ii = 1; | ||
|
||
class t2 | ||
{ | ||
public: | ||
int i; | ||
|
||
t2() : i(2) | ||
{ | ||
} | ||
|
||
~t2() { ii = 0; } | ||
|
||
int foo(); | ||
}; | ||
|
||
int t2::foo() | ||
{ | ||
// zero-length capability is allowed | ||
char *__capability cap_ptr = cheri_ptr(buffer, 3); | ||
assert(cap_ptr[2] == 'l'); | ||
return 0; | ||
} | ||
|
||
int main(int argc, char **argv) | ||
{ | ||
t2 *p = new t2; | ||
assert(p->i == 2); | ||
|
||
t2.foo(); | ||
|
||
delete p; | ||
assert(ii == 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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION SUCCESSFUL$ |
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,42 @@ | ||
#include <stdio.h> | ||
#include <string.h> | ||
#include <cheri/cheric.h> | ||
|
||
char *buffer = "hello"; | ||
char *secret = "secret"; | ||
|
||
class t1 { | ||
public: | ||
int i; | ||
|
||
t1(): i(0) | ||
{ | ||
} | ||
|
||
int foo(); | ||
}; | ||
|
||
int t1::foo() | ||
{ | ||
char *__capability cap_ptr = cheri_ptr(buffer, 6); | ||
/* Overflow buffer, leaking the secret in a traditional system */ | ||
for(int i = 0; i < strlen(buffer) + 7; i++) | ||
{ | ||
printf("ptr[%d] = '%c'\n", i, cap_ptr[i]); | ||
} | ||
return 0; | ||
} | ||
|
||
int main(int argc, char **argv) | ||
{ | ||
t1 instance1; | ||
t1 &r = instance1; | ||
assert(r.i == 0); // pass | ||
|
||
r.foo(); // access the CHERI API function from a lvalue reference | ||
|
||
r.i = 1; | ||
assert(r.i == 1); // fail | ||
|
||
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,4 @@ | ||
CORE | ||
main.c | ||
--cheri hybrid | ||
^VERIFICATION FAILED$ |