diff --git a/examples/equivalence/trunc.c b/examples/equivalence/trunc.c new file mode 100644 index 000000000..2d1812ce2 --- /dev/null +++ b/examples/equivalence/trunc.c @@ -0,0 +1,24 @@ +#include "smack.h" + +double c_trunc(double x) +{ + union {double f; unsigned long i;} u = {x}; + __VERIFIER_equiv_store_unsigned_long(u.i, 0); + int e = (int)(u.i >> 52 & 0x7ff) - 0x3ff + 12; + unsigned long m; + + if (e >= 52 + 12) + return x; + if (e < 12) + e = 1; + m = -1ULL >> e; + __VERIFIER_equiv_store_unsigned_long(m, 1); + __VERIFIER_equiv_store_unsigned_long(u.i & m, 2); + if ((u.i & m) == 0) + return x; + __VERIFIER_equiv_store_unsigned_long(~m, 3); + __VERIFIER_equiv_store_unsigned_long(u.i & ~m, 4); + u.i &= ~m; + __VERIFIER_equiv_store_unsigned_long(u.i, 5); + return u.f; +} \ No newline at end of file diff --git a/examples/equivalence/trunc.rs b/examples/equivalence/trunc.rs new file mode 100644 index 000000000..e48dddc78 --- /dev/null +++ b/examples/equivalence/trunc.rs @@ -0,0 +1,49 @@ +// Modified version from https://github.com/rust-lang/libm/blob/master/src/math/trunc.rs + +#[macro_use] +extern crate smack; +use smack::*; + +extern crate core; +use core::f64; + +pub fn trunc(x: f64) -> f64 { + let x1p120 = f64::from_bits(0x4770000000000000); // 0x1p120f === 2 ^ 120 + + let mut i: u64 = x.to_bits(); + verifier_equiv_assume_u64(i, 0); + let mut e: i64 = (i >> 52 & 0x7ff) as i64 - 0x3ff + 12; + let m: u64; + + if e >= 52 + 12 { + return x; + } + if e < 12 { + e = 1; + } + m = -1i64 as u64 >> e; + verifier_equiv_assume_u64(m, 1); + verifier_equiv_assume_u64(i & m, 2); + + if (i & m) == 0 { + return x; + } + verifier_equiv_assume_u64(!m, 3); + verifier_equiv_assume_u64(i & !m, 4); + i &= !m; + verifier_equiv_assume_u64(i, 5); + f64::from_bits(i) +} + +extern "C" { + fn c_trunc(x: f64) -> f64; + fn __isnan(x: f64) -> i32; +} + +fn main() { + let x = 0.0.verifier_nondet(); + verifier_assume!(__isnan(x) == 0); + let c_res = unsafe { c_trunc(x) }; + let rust_res = trunc(x); + verifier_assert!(rust_res == c_res); +} \ No newline at end of file diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index e8136d17d..33b4fd26d 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -171,4 +171,60 @@ void __VERIFIER_atomic_end(); } #endif +void __VERIFIER_equiv_store_char(char val, int id); +void __VERIFIER_equiv_check_char(char val, int id); +void __VERIFIER_equiv_assume_char(char val, int id); + +void __VERIFIER_equiv_store_unsigned_char(unsigned char val, int id); +void __VERIFIER_equiv_check_unsigned_char(unsigned char val, int id); +void __VERIFIER_equiv_assume_unsigned_char(unsigned char val, int id); + +void __VERIFIER_equiv_store_signed_char(signed char val, int id); +void __VERIFIER_equiv_check_signed_char(signed char val, int id); +void __VERIFIER_equiv_assume_signed_char(signed char val, int id); + +void __VERIFIER_equiv_store_short(short val, int id); +void __VERIFIER_equiv_check_short(short val, int id); +void __VERIFIER_equiv_assume_short(short val, int id); + +void __VERIFIER_equiv_store_unsigned_short(unsigned short val, int id); +void __VERIFIER_equiv_check_unsigned_short(unsigned short val, int id); +void __VERIFIER_equiv_assume_unsigned_short(unsigned short val, int id); + +void __VERIFIER_equiv_store_signed_short(signed short val, int id); +void __VERIFIER_equiv_check_signed_short(signed short val, int id); +void __VERIFIER_equiv_assume_signed_short(signed short val, int id); + +void __VERIFIER_equiv_store_int(int val, int id); +void __VERIFIER_equiv_check_int(int val, int id); +void __VERIFIER_equiv_assume_int(int val, int id); + +void __VERIFIER_equiv_store_unsigned_int(unsigned int val, int id); +void __VERIFIER_equiv_check_unsigned_int(unsigned int val, int id); +void __VERIFIER_equiv_assume_unsigned_int(unsigned int val, int id); + +void __VERIFIER_equiv_store_signed_int(signed int val, int id); +void __VERIFIER_equiv_check_signed_int(signed int val, int id); +void __VERIFIER_equiv_assume_signed_int(signed int val, int id); + +void __VERIFIER_equiv_store_long(long val, int id); +void __VERIFIER_equiv_check_long(long val, int id); +void __VERIFIER_equiv_assume_long(long val, int id); + +void __VERIFIER_equiv_store_unsigned_long(unsigned long val, int id); +void __VERIFIER_equiv_check_unsigned_long(unsigned long val, int id); +void __VERIFIER_equiv_assume_unsigned_long(unsigned long val, int id); + +void __VERIFIER_equiv_store_signed_long(signed long val, int id); +void __VERIFIER_equiv_check_signed_long(signed long val, int id); +void __VERIFIER_equiv_assume_signed_long(signed long val, int id); + +void __VERIFIER_equiv_store_float(float val, int id); +void __VERIFIER_equiv_check_float(float val, int id); +void __VERIFIER_equiv_assume_float(float val, int id); + +void __VERIFIER_equiv_store_double(double val, int id); +void __VERIFIER_equiv_check_double(double val, int id); +void __VERIFIER_equiv_assume_double(double val, int id); + #endif /*SMACK_H_*/ diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 218fa0503..d10d0673a 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -1892,3 +1892,231 @@ void __SMACK_init_func_memory_model(void) { void __VERIFIER_atomic_begin() { __SMACK_code("call corral_atomic_begin();"); } void __VERIFIER_atomic_end() { __SMACK_code("call corral_atomic_end();"); } + + +void __VERIFIER_equiv_store_char(char x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_char(x: bv32) returns (bv8);"); + #else + __SMACK_top_decl("function equiv_store_char(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_char(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_char(char x, int id) { + __SMACK_code("assert @ == equiv_store_char(@);", x, id); +} + +void __VERIFIER_equiv_assume_char(char x, int id) { + __SMACK_code("assume @ == equiv_store_char(@);", x, id); +} +void __VERIFIER_equiv_store_unsigned_char(unsigned char x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_unsigned_char(x: bv32) returns (bv8);"); + #else + __SMACK_top_decl("function equiv_store_unsigned_char(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_unsigned_char(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_unsigned_char(unsigned char x, int id) { + __SMACK_code("assert @ == equiv_store_unsigned_char(@);", x, id); +} + +void __VERIFIER_equiv_assume_unsigned_char(unsigned char x, int id) { + __SMACK_code("assume @ == equiv_store_unsigned_char(@);", x, id); +} +void __VERIFIER_equiv_store_signed_char(signed char x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_signed_char(x: bv32) returns (bv8);"); + #else + __SMACK_top_decl("function equiv_store_signed_char(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_signed_char(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_signed_char(signed char x, int id) { + __SMACK_code("assert @ == equiv_store_signed_char(@);", x, id); +} + +void __VERIFIER_equiv_assume_signed_char(signed char x, int id) { + __SMACK_code("assume @ == equiv_store_signed_char(@);", x, id); +} +void __VERIFIER_equiv_store_short(short x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_short(x: bv32) returns (bv16);"); + #else + __SMACK_top_decl("function equiv_store_short(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_short(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_short(short x, int id) { + __SMACK_code("assert @ == equiv_store_short(@);", x, id); +} + +void __VERIFIER_equiv_assume_short(short x, int id) { + __SMACK_code("assume @ == equiv_store_short(@);", x, id); +} +void __VERIFIER_equiv_store_unsigned_short(unsigned short x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_unsigned_short(x: bv32) returns (bv16);"); + #else + __SMACK_top_decl("function equiv_store_unsigned_short(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_unsigned_short(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_unsigned_short(unsigned short x, int id) { + __SMACK_code("assert @ == equiv_store_unsigned_short(@);", x, id); +} + +void __VERIFIER_equiv_assume_unsigned_short(unsigned short x, int id) { + __SMACK_code("assume @ == equiv_store_unsigned_short(@);", x, id); +} +void __VERIFIER_equiv_store_signed_short(signed short x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_signed_short(x: bv32) returns (bv16);"); + #else + __SMACK_top_decl("function equiv_store_signed_short(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_signed_short(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_signed_short(signed short x, int id) { + __SMACK_code("assert @ == equiv_store_signed_short(@);", x, id); +} + +void __VERIFIER_equiv_assume_signed_short(signed short x, int id) { + __SMACK_code("assume @ == equiv_store_signed_short(@);", x, id); +} +void __VERIFIER_equiv_store_int(int x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_int(x: bv32) returns (bv32);"); + #else + __SMACK_top_decl("function equiv_store_int(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_int(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_int(int x, int id) { + __SMACK_code("assert @ == equiv_store_int(@);", x, id); +} + +void __VERIFIER_equiv_assume_int(int x, int id) { + __SMACK_code("assume @ == equiv_store_int(@);", x, id); +} +void __VERIFIER_equiv_store_unsigned_int(unsigned int x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_unsigned_int(x: bv32) returns (bv32);"); + #else + __SMACK_top_decl("function equiv_store_unsigned_int(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_unsigned_int(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_unsigned_int(unsigned int x, int id) { + __SMACK_code("assert @ == equiv_store_unsigned_int(@);", x, id); +} + +void __VERIFIER_equiv_assume_unsigned_int(unsigned int x, int id) { + __SMACK_code("assume @ == equiv_store_unsigned_int(@);", x, id); +} +void __VERIFIER_equiv_store_signed_int(signed int x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_signed_int(x: bv32) returns (bv32);"); + #else + __SMACK_top_decl("function equiv_store_signed_int(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_signed_int(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_signed_int(signed int x, int id) { + __SMACK_code("assert @ == equiv_store_signed_int(@);", x, id); +} + +void __VERIFIER_equiv_assume_signed_int(signed int x, int id) { + __SMACK_code("assume @ == equiv_store_signed_int(@);", x, id); +} +void __VERIFIER_equiv_store_long(long x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_long(x: bv32) returns (bv64);"); + #else + __SMACK_top_decl("function equiv_store_long(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_long(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_long(long x, int id) { + __SMACK_code("assert @ == equiv_store_long(@);", x, id); +} + +void __VERIFIER_equiv_assume_long(long x, int id) { + __SMACK_code("assume @ == equiv_store_long(@);", x, id); +} +void __VERIFIER_equiv_store_unsigned_long(unsigned long x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_unsigned_long(x: bv32) returns (bv64);"); + #else + __SMACK_top_decl("function equiv_store_unsigned_long(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_unsigned_long(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_unsigned_long(unsigned long x, int id) { + __SMACK_code("assert @ == equiv_store_unsigned_long(@);", x, id); +} + +void __VERIFIER_equiv_assume_unsigned_long(unsigned long x, int id) { + __SMACK_code("assume @ == equiv_store_unsigned_long(@);", x, id); +} +void __VERIFIER_equiv_store_signed_long(signed long x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_signed_long(x: bv32) returns (bv64);"); + #else + __SMACK_top_decl("function equiv_store_signed_long(x: int) returns (int);"); + #endif + __SMACK_code("assume equiv_store_signed_long(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_signed_long(signed long x, int id) { + __SMACK_code("assert @ == equiv_store_signed_long(@);", x, id); +} + +void __VERIFIER_equiv_assume_signed_long(signed long x, int id) { + __SMACK_code("assume @ == equiv_store_signed_long(@);", x, id); +} + +void __VERIFIER_equiv_store_float(float x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_float(x: bv32) returns (bvfloat);"); + #else + __SMACK_top_decl("function equiv_store_float(x: int) returns (bvfloat);"); + #endif + __SMACK_code("assume equiv_store_float(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_float(float x, int id) { + __SMACK_code("assert @ == equiv_store_float(@);", x, id); +} + +void __VERIFIER_equiv_assume_float(float x, int id) { + __SMACK_code("assume @ == equiv_store_float(@);", x, id); +} + +void __VERIFIER_equiv_store_double(double x, int id) { + #ifdef BIT_PRECISE + __SMACK_top_decl("function equiv_store_double(x: bv32) returns (bvdouble);"); + #else + __SMACK_top_decl("function equiv_store_double(x: int) returns (bvdouble);"); + #endif + __SMACK_code("assume equiv_store_double(@) == @;", id, x); +} + +void __VERIFIER_equiv_check_double(double x, int id) { + __SMACK_code("assert @ == equiv_store_double(@);", x, id); +} + +void __VERIFIER_equiv_assume_double(double x, int id) { + __SMACK_code("assume @ == equiv_store_double(@);", x, id); +} diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs index da6c71734..072af6df0 100644 --- a/share/smack/lib/smack.rs +++ b/share/smack/lib/smack.rs @@ -21,6 +21,46 @@ extern "C" { pub fn free(ptr: *mut u8); pub fn memset(ptr: *mut u8, ch: i32, count: usize); pub fn realloc(ptr: *mut u8, new_size: usize) -> *mut u8; + + pub fn __VERIFIER_equiv_store_unsigned_char(val: u8, id: i32); + pub fn __VERIFIER_equiv_check_unsigned_char(val: u8, id: i32); + pub fn __VERIFIER_equiv_assume_unsigned_char(val: u8, id: i32); + + pub fn __VERIFIER_equiv_store_signed_char(val: i8, id: i32); + pub fn __VERIFIER_equiv_check_signed_char(val: i8, id: i32); + pub fn __VERIFIER_equiv_assume_signed_char(val: i8, id: i32); + + pub fn __VERIFIER_equiv_store_unsigned_short(val: u16, id: i32); + pub fn __VERIFIER_equiv_check_unsigned_short(val: u16, id: i32); + pub fn __VERIFIER_equiv_assume_unsigned_short(val: u16, id: i32); + + pub fn __VERIFIER_equiv_store_signed_short(val: i16, id: i32); + pub fn __VERIFIER_equiv_check_signed_short(val: i16, id: i32); + pub fn __VERIFIER_equiv_assume_signed_short(val: i16, id: i32); + + pub fn __VERIFIER_equiv_store_unsigned_int(val: u32, id: i32); + pub fn __VERIFIER_equiv_check_unsigned_int(val: u32, id: i32); + pub fn __VERIFIER_equiv_assume_unsigned_int(val: u32, id: i32); + + pub fn __VERIFIER_equiv_store_signed_int(val: i32, id: i32); + pub fn __VERIFIER_equiv_check_signed_int(val: i32, id: i32); + pub fn __VERIFIER_equiv_assume_signed_int(val: i32, id: i32); + + pub fn __VERIFIER_equiv_store_unsigned_long(val: u64, id: i32); + pub fn __VERIFIER_equiv_check_unsigned_long(val: u64, id: i32); + pub fn __VERIFIER_equiv_assume_unsigned_long(val: u64, id: i32); + + pub fn __VERIFIER_equiv_store_signed_long(val: i64, id: i32); + pub fn __VERIFIER_equiv_check_signed_long(val: i64, id: i32); + pub fn __VERIFIER_equiv_assume_signed_long(val: i64, id: i32); + + pub fn __VERIFIER_equiv_store_float(val: f32, id: i32); + pub fn __VERIFIER_equiv_check_float(val: f32, id: i32); + pub fn __VERIFIER_equiv_assume_float(val: f32, id: i32); + + pub fn __VERIFIER_equiv_store_double(val: f64, id: i32); + pub fn __VERIFIER_equiv_check_double(val: f64, id: i32); + pub fn __VERIFIER_equiv_assume_double(val: f64, id: i32); } #[macro_export] @@ -94,6 +134,119 @@ macro_rules! verifier_assume { }; } +pub fn verifier_equiv_store_u8(val: u8, id: i32) { + unsafe { __VERIFIER_equiv_store_unsigned_char(val, id) }; +} + +pub fn verifier_equiv_assume_u8(val: u8, id: i32) { + unsafe { __VERIFIER_equiv_assume_unsigned_char(val, id) }; +} + +pub fn verifier_equiv_check_u8(val: u8, id: i32) { + unsafe { __VERIFIER_equiv_check_unsigned_char(val, id) }; +} +pub fn verifier_equiv_store_i8(val: i8, id: i32) { + unsafe { __VERIFIER_equiv_store_signed_char(val, id) }; +} + +pub fn verifier_equiv_assume_i8(val: i8, id: i32) { + unsafe { __VERIFIER_equiv_assume_signed_char(val, id) }; +} + +pub fn verifier_equiv_check_i8(val: i8, id: i32) { + unsafe { __VERIFIER_equiv_check_signed_char(val, id) }; +} +pub fn verifier_equiv_store_u16(val: u16, id: i32) { + unsafe { __VERIFIER_equiv_store_unsigned_short(val, id) }; +} + +pub fn verifier_equiv_assume_u16(val: u16, id: i32) { + unsafe { __VERIFIER_equiv_assume_unsigned_short(val, id) }; +} + +pub fn verifier_equiv_check_u16(val: u16, id: i32) { + unsafe { __VERIFIER_equiv_check_unsigned_short(val, id) }; +} +pub fn verifier_equiv_store_i16(val: i16, id: i32) { + unsafe { __VERIFIER_equiv_store_signed_short(val, id) }; +} + +pub fn verifier_equiv_assume_i16(val: i16, id: i32) { + unsafe { __VERIFIER_equiv_assume_signed_short(val, id) }; +} + +pub fn verifier_equiv_check_i16(val: i16, id: i32) { + unsafe { __VERIFIER_equiv_check_signed_short(val, id) }; +} +pub fn verifier_equiv_store_u32(val: u32, id: i32) { + unsafe { __VERIFIER_equiv_store_unsigned_int(val, id) }; +} + +pub fn verifier_equiv_assume_u32(val: u32, id: i32) { + unsafe { __VERIFIER_equiv_assume_unsigned_int(val, id) }; +} + +pub fn verifier_equiv_check_u32(val: u32, id: i32) { + unsafe { __VERIFIER_equiv_check_unsigned_int(val, id) }; +} +pub fn verifier_equiv_store_i32(val: i32, id: i32) { + unsafe { __VERIFIER_equiv_store_signed_int(val, id) }; +} + +pub fn verifier_equiv_assume_i32(val: i32, id: i32) { + unsafe { __VERIFIER_equiv_assume_signed_int(val, id) }; +} + +pub fn verifier_equiv_check_i32(val: i32, id: i32) { + unsafe { __VERIFIER_equiv_check_signed_int(val, id) }; +} +pub fn verifier_equiv_store_u64(val: u64, id: i32) { + unsafe { __VERIFIER_equiv_store_unsigned_long(val, id) }; +} + +pub fn verifier_equiv_assume_u64(val: u64, id: i32) { + unsafe { __VERIFIER_equiv_assume_unsigned_long(val, id) }; +} + +pub fn verifier_equiv_check_u64(val: u64, id: i32) { + unsafe { __VERIFIER_equiv_check_unsigned_long(val, id) }; +} +pub fn verifier_equiv_store_i64(val: i64, id: i32) { + unsafe { __VERIFIER_equiv_store_signed_long(val, id) }; +} + +pub fn verifier_equiv_assume_i64(val: i64, id: i32) { + unsafe { __VERIFIER_equiv_assume_signed_long(val, id) }; +} + +pub fn verifier_equiv_check_i64(val: i64, id: i32) { + unsafe { __VERIFIER_equiv_check_signed_long(val, id) }; +} + +pub fn verifier_equiv_store_f32(val: f32, id: i32) { + unsafe { __VERIFIER_equiv_store_float(val, id) }; +} + +pub fn verifier_equiv_assume_f32(val: f32, id: i32) { + unsafe { __VERIFIER_equiv_assume_float(val, id) }; +} + +pub fn verifier_equiv_check_f32(val: f32, id: i32) { + unsafe { __VERIFIER_equiv_check_float(val, id) }; +} + +pub fn verifier_equiv_store_f64(val: f64, id: i32) { + unsafe { __VERIFIER_equiv_store_double(val, id) }; +} + +pub fn verifier_equiv_assume_f64(val: f64, id: i32) { + unsafe { __VERIFIER_equiv_assume_double(val, id) }; +} + +pub fn verifier_equiv_check_f64(val: f64, id: i32) { + unsafe { __VERIFIER_equiv_check_double(val, id) }; +} + #[macro_export] macro_rules! assume { ( $cond:expr ) => {