diff --git a/cvlr-asserts/src/core.rs b/cvlr-asserts/src/core.rs index d532f19..6768e3b 100644 --- a/cvlr-asserts/src/core.rs +++ b/cvlr-asserts/src/core.rs @@ -1,4 +1,8 @@ mod rt_decls { + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] extern "C" { pub fn CVT_assume(_c: bool); pub fn CVT_assert(_c: bool); diff --git a/cvlr-asserts/src/log.rs b/cvlr-asserts/src/log.rs index 040c0cc..e1d0e96 100644 --- a/cvlr-asserts/src/log.rs +++ b/cvlr-asserts/src/log.rs @@ -1,4 +1,8 @@ mod rt_decls { + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] extern "C" { #![allow(improper_ctypes)] // duplicated to avoid cvlr-assert depend on any other cvlr crate diff --git a/cvlr-hook/tests/expand/test_hook_combined.expanded.rs b/cvlr-hook/tests/expand/test_hook_combined.expanded.rs index 9b3ba08..14693c1 100644 --- a/cvlr-hook/tests/expand/test_hook_combined.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_combined.expanded.rs @@ -5,68 +5,45 @@ fn hook_start() { fn hook_end() { (); } +fn check_eq(_a: i32, _b: i32) { + (); +} +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} +fn log(_msg: &str) { + (); +} fn tmp() -> Result<()> { hook_start(); hook_end(); Ok(()) } fn t3() { - match (&tmp(), &Ok(())) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_res(tmp(), Ok(())); } fn t4() { hook_start(); - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); hook_end(); } fn abs(x: i32) -> i32 { hook_start(); if x >= 0 { - { - ::std::io::_print(format_args!("x is positive\n")); - }; + log("x is positive"); x } else { - { - ::std::io::_print(format_args!("x is negative\n")); - }; + log("x is negative"); -x } } fn abs2(x: i32) -> i32 { hook_end(); if x >= 0 { - { - ::std::io::_print(format_args!("x is positive\n")); - }; + log("x is positive"); x } else { - { - ::std::io::_print(format_args!("x is negative\n")); - }; + log("x is negative"); -x } } diff --git a/cvlr-hook/tests/expand/test_hook_combined.rs b/cvlr-hook/tests/expand/test_hook_combined.rs index e0a3bc7..41aead5 100644 --- a/cvlr-hook/tests/expand/test_hook_combined.rs +++ b/cvlr-hook/tests/expand/test_hook_combined.rs @@ -8,6 +8,20 @@ fn hook_end() { (); } +// plain functions instead of assert_eq!/println! so the expanded output +// does not depend on the compiler's builtin macro lowering, which +// changes between rustc versions +fn check_eq(_a: i32, _b: i32) { + (); +} + +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} + +fn log(_msg: &str) { + (); +} #[cvlr_hook_on_entry(hook_start())] #[cvlr_hook_on_exit(hook_end())] @@ -18,37 +32,37 @@ fn tmp() -> Result<()> { } fn t3() { - assert_eq!(tmp(), Ok(())); + check_res(tmp(), Ok(())); } #[cvlr_hook_on_entry(hook_start())] #[cvlr_hook_on_exit(hook_end())] fn t4() { // hook start inserted here - assert_eq!(1, 1); + check_eq(1, 1); // hook end inserted here } #[cvlr_hook_on_entry(hook_start())] fn abs(x : i32) -> i32 { // hook start inserted here - if x >= 0 { - println!("x is positive"); - x - } else { - println!("x is negative"); - -x + if x >= 0 { + log("x is positive"); + x + } else { + log("x is negative"); + -x } } #[cvlr_hook_on_exit(hook_end())] fn abs2(x : i32) -> i32 { // hook end inserted here - if x >= 0 { - println!("x is positive"); - x - } else { - println!("x is negative"); - -x + if x >= 0 { + log("x is positive"); + x + } else { + log("x is negative"); + -x } -} \ No newline at end of file +} diff --git a/cvlr-hook/tests/expand/test_hook_end.expanded.rs b/cvlr-hook/tests/expand/test_hook_end.expanded.rs index ee07c08..304434b 100644 --- a/cvlr-hook/tests/expand/test_hook_end.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_end.expanded.rs @@ -2,49 +2,19 @@ use cvlr_hook::cvlr_hook_on_exit; fn hook() { (); } +fn check_eq(_a: i32, _b: i32) { + (); +} +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} fn t1() { - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; - match (&2, &2) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); + check_eq(2, 2); hook(); } fn t2() { - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); hook(); } fn tmp() -> Result<()> { @@ -52,17 +22,5 @@ fn tmp() -> Result<()> { Ok(()) } fn t3() { - match (&tmp(), &Ok(())) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_res(tmp(), Ok(())); } diff --git a/cvlr-hook/tests/expand/test_hook_end.rs b/cvlr-hook/tests/expand/test_hook_end.rs index 715701f..15824b8 100644 --- a/cvlr-hook/tests/expand/test_hook_end.rs +++ b/cvlr-hook/tests/expand/test_hook_end.rs @@ -4,17 +4,28 @@ fn hook() { (); } +// plain functions instead of assert_eq! so the expanded output does not +// depend on the compiler's builtin macro lowering, which changes +// between rustc versions +fn check_eq(_a: i32, _b: i32) { + (); +} + +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} + #[cvlr_hook_on_exit(hook())] fn t1() { - assert_eq!(1, 1); + check_eq(1, 1); // hook inserted here - assert_eq!(2, 2); + check_eq(2, 2); } #[cvlr_hook_on_exit(hook())] fn t2() { // hook inserted here - assert_eq!(1, 1); + check_eq(1, 1); } #[cvlr_hook_on_exit(hook())] @@ -24,5 +35,5 @@ fn tmp() -> Result<()> { } fn t3() { - assert_eq!(tmp(), Ok(())); -} \ No newline at end of file + check_res(tmp(), Ok(())); +} diff --git a/cvlr-hook/tests/expand/test_hook_start.expanded.rs b/cvlr-hook/tests/expand/test_hook_start.expanded.rs index e3b6c5f..404f684 100644 --- a/cvlr-hook/tests/expand/test_hook_start.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_start.expanded.rs @@ -2,9 +2,10 @@ use cvlr_hook::cvlr_hook_on_entry; fn hook() { (); } +fn work(_msg: &str) { + (); +} fn t1() { hook(); - { - ::std::io::_print(format_args!("t1\n")); - }; + work("t1"); } diff --git a/cvlr-hook/tests/expand/test_hook_start.rs b/cvlr-hook/tests/expand/test_hook_start.rs index 2ad2b03..3e34e5c 100644 --- a/cvlr-hook/tests/expand/test_hook_start.rs +++ b/cvlr-hook/tests/expand/test_hook_start.rs @@ -4,8 +4,15 @@ fn hook() { (); } +// plain function instead of println! so the expanded output does not +// depend on the compiler's builtin macro lowering, which changes +// between rustc versions +fn work(_msg: &str) { + (); +} + #[cvlr_hook_on_entry(hook())] fn t1() { // hook inserted here - println!("t1"); -} \ No newline at end of file + work("t1"); +} diff --git a/cvlr-log/src/core.rs b/cvlr-log/src/core.rs index f30f92a..cd9da63 100644 --- a/cvlr-log/src/core.rs +++ b/cvlr-log/src/core.rs @@ -1,4 +1,8 @@ pub mod rt_decls { + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] #[allow(improper_ctypes)] extern "C" { pub fn CVT_calltrace_print_tag(tag: &str); diff --git a/cvlr-mathint/src/nativeint_u64.rs b/cvlr-mathint/src/nativeint_u64.rs index b6d6994..61dff4b 100644 --- a/cvlr-mathint/src/nativeint_u64.rs +++ b/cvlr-mathint/src/nativeint_u64.rs @@ -12,6 +12,10 @@ pub struct NativeIntU64(u64); mod rt_decls { type BoolU64 = u64; + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] extern "C" { pub fn CVT_nativeint_u64_eq(_: u64, _: u64) -> BoolU64; pub fn CVT_nativeint_u64_lt(_: u64, _: u64) -> BoolU64; diff --git a/cvlr-nondet/src/lib.rs b/cvlr-nondet/src/lib.rs index b386c9a..36d6f14 100644 --- a/cvlr-nondet/src/lib.rs +++ b/cvlr-nondet/src/lib.rs @@ -13,4 +13,6 @@ pub mod havoc; pub use core::{nondet, nondet_with, Nondet}; pub use option::nondet_option; -pub use scalars::{cvlr_nondet_small_i128, cvlr_nondet_small_u128}; +pub use scalars::{ + cvlr_nondet_small_i128, cvlr_nondet_small_u128, cvlr_nondet_u32, cvlr_nondet_u64, +}; diff --git a/cvlr-nondet/src/scalars.rs b/cvlr-nondet/src/scalars.rs index 4250db3..a435621 100644 --- a/cvlr-nondet/src/scalars.rs +++ b/cvlr-nondet/src/scalars.rs @@ -1,6 +1,10 @@ use crate::Nondet; mod rt_decls { + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] #[allow(improper_ctypes)] extern "C" { // Definition of external functions that represent getting arbitrary values diff --git a/cvlr/src/u128_arith.rs b/cvlr/src/u128_arith.rs index 63de700..5331da0 100644 --- a/cvlr/src/u128_arith.rs +++ b/cvlr/src/u128_arith.rs @@ -1,4 +1,8 @@ mod rt_decls { + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "env") + )] #[allow(improper_ctypes)] extern "C" { pub fn CVT_u128_leq(x: u128, y: u128) -> bool;