Skip to content

Commit

Permalink
Implement functioning test
Browse files Browse the repository at this point in the history
  • Loading branch information
AdrianJendo committed Apr 9, 2024
1 parent 37604b0 commit 3b7e6c0
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 50 deletions.
2 changes: 1 addition & 1 deletion scripts/rust-jobs.json
Original file line number Diff line number Diff line change
Expand Up @@ -56,4 +56,4 @@
"vec-filter",
"vec-sort-reverse"
]
}
}
43 changes: 23 additions & 20 deletions src/rust-jobs/mock-test1/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,36 +3,39 @@
use verifier;
use seamock::seamock;

// TODO: move this enum into the library
enum WithVal<T> {
Gt(T),
Gte(T),
Lt(T),
Lte(T),
Eq(T),
}

#[seamock]
pub trait Test {
fn a(&self, z: bool, a: i32) -> i32;
fn a(&self, x: i32, y: bool) -> i32;
fn b(&self) -> u8;
fn c(&self) -> i32;
}

fn test<T: Test>(mock_test: &T, x: i32, y: bool) -> i32 {
let ans = mock_test.a(x, y);
mock_test.b();
mock_test.c();
return ans;
}

#[no_mangle]
pub extern "C" fn entrypt() {
let mut x: MockTest = MockTest::new();
let mut y: i32 = verifier::any!();
let mut z: bool = verifier::any!();
let mut mock: MockTest = MockTest::new();
let mut x: i32 = verifier::any!();
let mut y: bool = verifier::any!();

verifier::assume!(y < 10);
verifier::assume!(x < 10);

x
mock
.times_a(2)
.returning_a(|z, a| a + 6)
.returning_b(|| 4)
.times_b(2);
.times_b(2)
.times_c(1)
.returning_a(|x, y| x + 5)
.returning_b(|| 4);

// verifier::vassert!(y == x.c());
verifier::vassert!(x.a(z, y) < 15);
verifier::vassert!(mock.a(x, y) < 15);
verifier::vassert!(mock.b() == 4);
verifier::vassert!(test(&mock, x, y) < 15);
verifier::vassert!(mock.expect_times_a(2));
verifier::vassert!(mock.expect_times_b(2));
verifier::vassert!(mock.expect_times_c(1));
}
46 changes: 17 additions & 29 deletions src/seamock-lib/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -152,37 +152,10 @@ pub fn seamock(_args: TokenStream, input: TokenStream) -> TokenStream {
let ret_func = Ident::new(&format!("val_returning_{}", &method.sig.ident), method.sig.ident.span());
let method_name_string = &method.sig.ident.to_string();

// TODO: generate code to check parameter values are correct
// let x = if !method_inputs.is_empty() {
// Some(quote! {
// match self.#val_attr {
// Some(x) => {
//
// assert!(val > z);
// }
// Some(WithVal::Gte(val)) {
// assert!(val >= z);
// }
// Some(WithVal::Eq(val)) => {
// assert_eq!(val, z);
// }
// None => {}
// _ => {}
// }
// })
// } else {
// None
// };

Some (quote! {
fn #method_name(#method_inputs) #method_output {
self.#times_attr.replace_with(|&mut old| old + 1);
// sassert
// verifier error
if *self.#times_attr.borrow() > self.#max_times_attr {
// panic!("{} called more than {} times", #method_name_string, self.#max_times_attr);
}
// #x
// verifier::vassert!(*self.#times_attr.borrow() <= self.#max_times_attr)
(self.#ret_func)(#(#params)*)
}
})
Expand Down Expand Up @@ -210,6 +183,7 @@ pub fn seamock(_args: TokenStream, input: TokenStream) -> TokenStream {
let max_times_clone = max_times.clone();

// Implement the trait for MockContext
let trait_original = &input.ident;
let mock_impl = quote! {
impl #mock_struct_name {
pub fn new() -> Self {
Expand All @@ -232,18 +206,32 @@ pub fn seamock(_args: TokenStream, input: TokenStream) -> TokenStream {
#(#with_methods)*
#(#times_methods)*
#(#expect_times_methods)*
// #(#methods_impl)*
}
};

let trait_impl = quote! {
impl #trait_original for #mock_struct_name {
#(#methods_impl)*
}
};

// Combine the generated tokens
let expanded = quote! {
use core::cell::RefCell;
enum WithVal<T> {
Gt(T),
Gte(T),
Lt(T),
Lte(T),
Eq(T),
}
#input
#mock_struct
#mock_impl
#trait_impl
};


TokenStream::from(expanded)
}
}

0 comments on commit 3b7e6c0

Please sign in to comment.