Skip to content

Commit

Permalink
Add tests for the DOIT checker.
Browse files Browse the repository at this point in the history
Adds a CCT-DOIT test group that contains the normal CCT tests
in the success condition and the failure condition as well as
DOIT-specific tests in the failure condition. The DOIT-specific
tests use the two non-DOIT instructions ROL and XCHG.

Reusing the CCT tests required making their main functions
"export" to make sure they are kept at the later compiler passes
where DOIT checking needs to be done.
  • Loading branch information
J08nY committed May 14, 2024
1 parent 11cde9a commit d37bd9b
Show file tree
Hide file tree
Showing 11 changed files with 26 additions and 7 deletions.
3 changes: 2 additions & 1 deletion compiler/CCT/fail/H_L_L.jazz
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {
export fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {

reg u64 t;

t = x + ya;
t = t;

return t;
}
5 changes: 5 additions & 0 deletions compiler/CCT/fail/doit/rol.jazz
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// This is CT in the ordinary sense, but not DOIT as ROL is not DOIT.
export fn rol(#secret reg u32 x) -> #secret reg u32 {
_, _, x = #ROL_32(x, 5);
return x;
}
5 changes: 5 additions & 0 deletions compiler/CCT/fail/doit/xchg.jazz
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// This is CT in the ordinary sense, but not DOIT as XCHG is not DOIT.
export fn xchange(#secret reg u32 a, #secret reg u32 b) -> #secret reg u32, #secret reg u32 {
a, b = #XCHG_32(a, b);
return a, b;
}
2 changes: 1 addition & 1 deletion compiler/CCT/fail/flex_on_ret.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn foo(#public reg u64 r) -> #flex reg u64 {
export fn foo(#public reg u64 r) -> #flex reg u64 {
return r;
}

2 changes: 1 addition & 1 deletion compiler/CCT/fail/load_on_poly.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn load(#poly=l1 reg u64 x) -> reg u64 {
export fn load(#poly=l1 reg u64 x) -> reg u64 {

reg u64 t;

Expand Down
2 changes: 1 addition & 1 deletion compiler/CCT/fail/load_on_secret.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn mem3(#secret reg u64 p, reg u64 x) {
export fn mem3(#secret reg u64 p, reg u64 x) {
reg u64 r;

[p] = x;
Expand Down
2 changes: 1 addition & 1 deletion compiler/CCT/fail/strict.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn add(#public reg u64 p, #secret reg u64 s) -> reg u64 {
export fn add(#public reg u64 p, #secret reg u64 s) -> reg u64 {
p += s;
return p;
}
2 changes: 1 addition & 1 deletion compiler/CCT/fail/strict_local.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn add(#public reg u64 p, #secret reg u64 s) -> reg u64 {
export fn add(#public reg u64 p, #secret reg u64 s) -> reg u64 {
#public reg u64 p1;
p1 = p + s;
return p1;
Expand Down
2 changes: 1 addition & 1 deletion compiler/CCT/fail/strict_on_ret.jazz
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn foo(#public reg u64 r) -> #strict reg u64 {
export fn foo(#public reg u64 r) -> #strict reg u64 {
return r;
}

1 change: 1 addition & 0 deletions compiler/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ CHECK += config/tests.config
CHECKCATS ?= \
safety \
CCT \
CCT-DOIT \
x86-64-ATT \
x86-64-Intel \
x86-64-print \
Expand Down
7 changes: 7 additions & 0 deletions compiler/config/tests.config
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,13 @@ kodirs = !safety/fail
bin = ./scripts/check-cct
okdirs = !CCT/success
kodirs = !CCT/fail
exclude = !CCT/fail/doit

[test-CCT-DOIT]
bin = ./scripts/check-cct
args = --doit --after=propagate
okdirs = !CCT/success
kodirs = !CCT/fail !CCT/fail/doit

[test-SCT]
bin = ./scripts/check-cct
Expand Down

0 comments on commit d37bd9b

Please sign in to comment.