Skip to content

Commit

Permalink
Added equivalence checking extensions
Browse files Browse the repository at this point in the history
  • Loading branch information
@keram88
keram88 committed Aug 23, 2023
1 parent a321447 commit b1bae13
Show file tree
Hide file tree
Showing 5 changed files with 510 additions and 0 deletions.
24 changes: 24 additions & 0 deletions examples/equivalence/trunc.c
View file
Original file line number Diff line number Diff line change
@@ -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;
}
49 changes: 49 additions & 0 deletions examples/equivalence/trunc.rs
View file
Original file line number Diff line number Diff line change
@@ -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);
}
56 changes: 56 additions & 0 deletions share/smack/include/smack.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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_*/
228 changes: 228 additions & 0 deletions share/smack/lib/smack.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Loading

0 comments on commit b1bae13

Please sign in to comment.