From e04fceb4e444cc0e1e96e1f909f13e784200d160 Mon Sep 17 00:00:00 2001 From: "Mark S. Baranowski" Date: Sat, 19 Oct 2024 16:54:02 -0600 Subject: [PATCH] Reformatting --- include/smack/Naming.h | 3 + lib/smack/Naming.cpp | 4 + lib/smack/SmackModuleGenerator.cpp | 5 + lib/smack/SmackRep.cpp | 4 + share/smack/include/smack.h | 84 +++++----- share/smack/lib/smack.c | 238 +++++++++++++++++------------ share/smack/lib/smack.rs | 180 +++++++++++----------- 7 files changed, 288 insertions(+), 230 deletions(-) diff --git a/include/smack/Naming.h b/include/smack/Naming.h index acfceb2f5..abeb01e35 100644 --- a/include/smack/Naming.h +++ b/include/smack/Naming.h @@ -56,6 +56,9 @@ class Naming { static const std::string STATIC_INIT_PROC; static const std::string LOOP_EXIT; + static const std::string EQUIV_STORE_COUNTER; + static const std::string EQUIV_LOAD_COUNTER; + static const std::string MEMORY; static const std::string ALLOC; static const std::string FREE; diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp index ce762cb64..29e1932a6 100644 --- a/lib/smack/Naming.cpp +++ b/lib/smack/Naming.cpp @@ -40,6 +40,10 @@ const std::string Naming::INITIALIZE_PROC = "$initialize"; const std::string Naming::STATIC_INIT_PROC = "__SMACK_static_init"; const std::string Naming::LOOP_EXIT = "__SMACK_loop_exit"; +const std::string Naming::EQUIV_STORE_COUNTER = "__SMACK_equiv_store_counter"; +const std::string Naming::EQUIV_LOAD_COUNTER = "__SMACK_equiv_load_counter"; + + const std::string Naming::MEMORY = "$M"; const std::string Naming::ALLOC = "$alloc"; const std::string Naming::FREE = "$free"; diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index 2c70404f4..9b75082b9 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -38,6 +38,11 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { SmackRep rep(&M.getDataLayout(), &naming, program, &getAnalysis()); std::list &decls = program->getDeclarations(); + decls.insert(decls.end(), {Decl::variable(Naming::EQUIV_STORE_COUNTER, "int"), + Decl::variable(Naming::EQUIV_LOAD_COUNTER, "int")}); + + decls.insert(decls.end(), {Decl::function("__SMACK_equiv_id", {{"id", "int"}}, "int")}); + SDEBUG(errs() << "Analyzing globals...\n"); for (auto &G : M.globals()) { diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 702322b0c..a46d9f35d 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -1244,6 +1244,10 @@ Decl *SmackRep::getInitFuncs() { b->addStmt( Stmt::assign(Expr::id(Naming::RMODE_VAR), Expr::lit(RModeKind::RNE))); } + b->addStmt( + Stmt::assign(Expr::id(Naming::EQUIV_STORE_COUNTER), Expr::lit((unsigned int) 0))); + b->addStmt( + Stmt::assign(Expr::id(Naming::EQUIV_LOAD_COUNTER), Expr::lit((unsigned int) 0))); b->addStmt(Stmt::return_()); proc->getBlocks().push_back(b); return proc; diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index 33b4fd26d..a36c4a065 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -171,60 +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_char(char val); +void __VERIFIER_equiv_check_char(char val); +void __VERIFIER_equiv_assume_char(char val); -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_unsigned_char(unsigned char val); +void __VERIFIER_equiv_check_unsigned_char(unsigned char val); +void __VERIFIER_equiv_assume_unsigned_char(unsigned char val); -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_signed_char(signed char val); +void __VERIFIER_equiv_check_signed_char(signed char val); +void __VERIFIER_equiv_assume_signed_char(signed char val); -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_short(short val); +void __VERIFIER_equiv_check_short(short val); +void __VERIFIER_equiv_assume_short(short val); -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_unsigned_short(unsigned short val); +void __VERIFIER_equiv_check_unsigned_short(unsigned short val); +void __VERIFIER_equiv_assume_unsigned_short(unsigned short val); -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_signed_short(signed short val); +void __VERIFIER_equiv_check_signed_short(signed short val); +void __VERIFIER_equiv_assume_signed_short(signed short val); -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_int(int val); +void __VERIFIER_equiv_check_int(int val); +void __VERIFIER_equiv_assume_int(int val); -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_unsigned_int(unsigned int val); +void __VERIFIER_equiv_check_unsigned_int(unsigned int val); +void __VERIFIER_equiv_assume_unsigned_int(unsigned int val); -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_signed_int(signed int val); +void __VERIFIER_equiv_check_signed_int(signed int val); +void __VERIFIER_equiv_assume_signed_int(signed int val); -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_long(long val); +void __VERIFIER_equiv_check_long(long val); +void __VERIFIER_equiv_assume_long(long val); -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_unsigned_long(unsigned long val); +void __VERIFIER_equiv_check_unsigned_long(unsigned long val); +void __VERIFIER_equiv_assume_unsigned_long(unsigned long val); -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_signed_long(signed long val); +void __VERIFIER_equiv_check_signed_long(signed long val); +void __VERIFIER_equiv_assume_signed_long(signed long val); -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_float(float val); +void __VERIFIER_equiv_check_float(float val); +void __VERIFIER_equiv_assume_float(float val); -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); +void __VERIFIER_equiv_store_double(double val); +void __VERIFIER_equiv_check_double(double val); +void __VERIFIER_equiv_assume_double(double val); #endif /*SMACK_H_*/ diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 588057824..c49f1edc6 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -1894,197 +1894,233 @@ 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) { +void __VERIFIER_equiv_store_char(char x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_char(x: bv32) returns (bv8);"); + __SMACK_top_decl("function equiv_store_char(x: int) returns (bv8);"); #else __SMACK_top_decl("function equiv_store_char(x: int) returns (int);"); #endif - __SMACK_code("assume equiv_store_char(@) == @;", id, x); + __SMACK_code("assume equiv_store_char(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_char(char x, int id) { - __SMACK_code("assert @ == equiv_store_char(@);", x, id); +void __VERIFIER_equiv_check_char(char x) { + __SMACK_code("assert @ == equiv_store_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_char(char x, int id) { - __SMACK_code("assume @ == equiv_store_char(@);", x, id); +void __VERIFIER_equiv_assume_char(char x) { + __SMACK_code("assume @ == equiv_store_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_unsigned_char(unsigned char x, int id) { +void __VERIFIER_equiv_store_unsigned_char(unsigned char x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_unsigned_char(x: bv32) returns (bv8);"); + __SMACK_top_decl("function equiv_store_unsigned_char(x: int) 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); + __SMACK_code("assume equiv_store_unsigned_char(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_unsigned_char(unsigned char x, int id) { - __SMACK_code("assert @ == equiv_store_unsigned_char(@);", x, id); +void __VERIFIER_equiv_check_unsigned_char(unsigned char x) { + __SMACK_code("assert @ == equiv_store_unsigned_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_unsigned_char(unsigned char x, int id) { - __SMACK_code("assume @ == equiv_store_unsigned_char(@);", x, id); +void __VERIFIER_equiv_assume_unsigned_char(unsigned char x) { + __SMACK_code("assume @ == equiv_store_unsigned_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_signed_char(signed char x, int id) { +void __VERIFIER_equiv_store_signed_char(signed char x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_signed_char(x: bv32) returns (bv8);"); + __SMACK_top_decl("function equiv_store_signed_char(x: int) 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); + __SMACK_code("assume equiv_store_signed_char(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_signed_char(signed char x, int id) { - __SMACK_code("assert @ == equiv_store_signed_char(@);", x, id); +void __VERIFIER_equiv_check_signed_char(signed char x) { + __SMACK_code("assert @ == equiv_store_signed_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_signed_char(signed char x, int id) { - __SMACK_code("assume @ == equiv_store_signed_char(@);", x, id); +void __VERIFIER_equiv_assume_signed_char(signed char x) { + __SMACK_code("assume @ == equiv_store_signed_char(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_short(short x, int id) { +void __VERIFIER_equiv_store_short(short x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_short(x: bv32) returns (bv16);"); + __SMACK_top_decl("function equiv_store_short(x: int) returns (bv16);"); #else __SMACK_top_decl("function equiv_store_short(x: int) returns (int);"); #endif - __SMACK_code("assume equiv_store_short(@) == @;", id, x); + __SMACK_code("assume equiv_store_short(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_short(short x, int id) { - __SMACK_code("assert @ == equiv_store_short(@);", x, id); +void __VERIFIER_equiv_check_short(short x) { + __SMACK_code("assert @ == equiv_store_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_short(short x, int id) { - __SMACK_code("assume @ == equiv_store_short(@);", x, id); +void __VERIFIER_equiv_assume_short(short x) { + __SMACK_code("assume @ == equiv_store_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_unsigned_short(unsigned short x, int id) { +void __VERIFIER_equiv_store_unsigned_short(unsigned short x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_unsigned_short(x: bv32) returns (bv16);"); + __SMACK_top_decl("function equiv_store_unsigned_short(x: int) 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); + __SMACK_code("assume equiv_store_unsigned_short(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_unsigned_short(unsigned short x, int id) { - __SMACK_code("assert @ == equiv_store_unsigned_short(@);", x, id); +void __VERIFIER_equiv_check_unsigned_short(unsigned short x) { + __SMACK_code("assert @ == equiv_store_unsigned_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_unsigned_short(unsigned short x, int id) { - __SMACK_code("assume @ == equiv_store_unsigned_short(@);", x, id); +void __VERIFIER_equiv_assume_unsigned_short(unsigned short x) { + __SMACK_code("assume @ == equiv_store_unsigned_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_signed_short(signed short x, int id) { +void __VERIFIER_equiv_store_signed_short(signed short x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_signed_short(x: bv32) returns (bv16);"); + __SMACK_top_decl("function equiv_store_signed_short(x: int) 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); + __SMACK_code("assume equiv_store_signed_short(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_signed_short(signed short x, int id) { - __SMACK_code("assert @ == equiv_store_signed_short(@);", x, id); +void __VERIFIER_equiv_check_signed_short(signed short x) { + __SMACK_code("assert @ == equiv_store_signed_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_signed_short(signed short x, int id) { - __SMACK_code("assume @ == equiv_store_signed_short(@);", x, id); +void __VERIFIER_equiv_assume_signed_short(signed short x) { + __SMACK_code("assume @ == equiv_store_signed_short(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_int(int x, int id) { +void __VERIFIER_equiv_store_int(int x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_int(x: bv32) returns (bv32);"); + __SMACK_top_decl("function equiv_store_int(x: int) returns (bv32);"); #else __SMACK_top_decl("function equiv_store_int(x: int) returns (int);"); #endif - __SMACK_code("assume equiv_store_int(@) == @;", id, x); + __SMACK_code("assume equiv_store_int(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_int(int x, int id) { - __SMACK_code("assert @ == equiv_store_int(@);", x, id); +void __VERIFIER_equiv_check_int(int x) { + __SMACK_code("assert @ == equiv_store_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_int(int x, int id) { - __SMACK_code("assume @ == equiv_store_int(@);", x, id); +void __VERIFIER_equiv_assume_int(int x) { + __SMACK_code("assume @ == equiv_store_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_unsigned_int(unsigned int x, int id) { +void __VERIFIER_equiv_store_unsigned_int(unsigned int x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_unsigned_int(x: bv32) returns (bv32);"); + __SMACK_top_decl("function equiv_store_unsigned_int(x: int) 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); + __SMACK_code("assume equiv_store_unsigned_int(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_unsigned_int(unsigned int x, int id) { - __SMACK_code("assert @ == equiv_store_unsigned_int(@);", x, id); +void __VERIFIER_equiv_check_unsigned_int(unsigned int x) { + __SMACK_code("assert @ == equiv_store_unsigned_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_unsigned_int(unsigned int x, int id) { - __SMACK_code("assume @ == equiv_store_unsigned_int(@);", x, id); +void __VERIFIER_equiv_assume_unsigned_int(unsigned int x) { + __SMACK_code("assume @ == equiv_store_unsigned_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_signed_int(signed int x, int id) { +void __VERIFIER_equiv_store_signed_int(signed int x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_signed_int(x: bv32) returns (bv32);"); + __SMACK_top_decl("function equiv_store_signed_int(x: int) 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); + __SMACK_code("assume equiv_store_signed_int(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_signed_int(signed int x, int id) { - __SMACK_code("assert @ == equiv_store_signed_int(@);", x, id); +void __VERIFIER_equiv_check_signed_int(signed int x) { + __SMACK_code("assert @ == equiv_store_signed_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_signed_int(signed int x, int id) { - __SMACK_code("assume @ == equiv_store_signed_int(@);", x, id); +void __VERIFIER_equiv_assume_signed_int(signed int x) { + __SMACK_code("assume @ == equiv_store_signed_int(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_long(long x, int id) { +void __VERIFIER_equiv_store_long(long x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_long(x: bv32) returns (bv64);"); + __SMACK_top_decl("function equiv_store_long(x: int) returns (bv64);"); #else __SMACK_top_decl("function equiv_store_long(x: int) returns (int);"); #endif - __SMACK_code("assume equiv_store_long(@) == @;", id, x); + __SMACK_code("assume equiv_store_long(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_long(long x, int id) { - __SMACK_code("assert @ == equiv_store_long(@);", x, id); +void __VERIFIER_equiv_check_long(long x) { + __SMACK_code("assert @ == equiv_store_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_long(long x, int id) { - __SMACK_code("assume @ == equiv_store_long(@);", x, id); +void __VERIFIER_equiv_assume_long(long x) { + __SMACK_code("assume @ == equiv_store_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_unsigned_long(unsigned long x, int id) { +void __VERIFIER_equiv_store_unsigned_long(unsigned long x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_unsigned_long(x: bv32) returns (bv64);"); + __SMACK_top_decl("function equiv_store_unsigned_long(x: int) 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); + __SMACK_code("assume equiv_store_unsigned_long(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_unsigned_long(unsigned long x, int id) { - __SMACK_code("assert @ == equiv_store_unsigned_long(@);", x, id); +void __VERIFIER_equiv_check_unsigned_long(unsigned long x) { + __SMACK_code("assert @ == equiv_store_unsigned_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_unsigned_long(unsigned long x, int id) { - __SMACK_code("assume @ == equiv_store_unsigned_long(@);", x, id); +void __VERIFIER_equiv_assume_unsigned_long(unsigned long x) { + __SMACK_code("assume @ == equiv_store_unsigned_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_signed_long(signed long x, int id) { +void __VERIFIER_equiv_store_signed_long(signed long x) { #ifdef BIT_PRECISE - __SMACK_top_decl("function equiv_store_signed_long(x: bv32) returns (bv64);"); + __SMACK_top_decl("function equiv_store_signed_long(x: int) 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); + __SMACK_code("assume equiv_store_signed_long(__SMACK_equiv_store_counter) == @;", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_signed_long(signed long x, int id) { - __SMACK_code("assert @ == equiv_store_signed_long(@);", x, id); +void __VERIFIER_equiv_check_signed_long(signed long x) { + __SMACK_code("assert @ == equiv_store_signed_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_signed_long(signed long x, int id) { - __SMACK_code("assume @ == equiv_store_signed_long(@);", x, id); +void __VERIFIER_equiv_assume_signed_long(signed long x) { + __SMACK_code("assume @ == equiv_store_signed_long(__SMACK_equiv_load_counter);", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } #ifdef BIT_PRECISE @@ -2100,28 +2136,34 @@ void __VERIFIER_equiv_assume_signed_long(signed long x, int id) { #define DOUBLET "double" #endif -void __VERIFIER_equiv_store_float(float x, int id) { - __SMACK_top_decl("function equiv_store_float(x: "INTT") returns ("FLOATT");"); - __SMACK_code("assume $foeq."FLOATT".bool(equiv_store_float(@), @f);", id, x); +void __VERIFIER_equiv_store_float(float x) { + __SMACK_top_decl("function equiv_store_float(x: int) returns ("FLOATT");"); + __SMACK_code("assume $foeq."FLOATT".bool(equiv_store_float(__SMACK_equiv_store_counter), @f);", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_float(float x, int id) { - __SMACK_code("assert $foeq."FLOATT".bool(@f, equiv_store_float(@));", x, id); +void __VERIFIER_equiv_check_float(float x) { + __SMACK_code("assert $foeq."FLOATT".bool(@f, equiv_store_float(__SMACK_equiv_load_counter));", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_float(float x, int id) { - __SMACK_code("assume $foeq."FLOATT".bool(@f, equiv_store_float(@));", x, id); +void __VERIFIER_equiv_assume_float(float x) { + __SMACK_code("assume $foeq."FLOATT".bool(@f, equiv_store_float(__SMACK_equiv_load_counter));", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_store_double(double x, int id) { - __SMACK_top_decl("function equiv_store_double(x: "INTT") returns ("DOUBLET");"); - __SMACK_code("assume $foeq."DOUBLET".bool(equiv_store_double(@), @);", id, x); +void __VERIFIER_equiv_store_double(double x) { + __SMACK_top_decl("function equiv_store_double(x: int) returns ("DOUBLET");"); + __SMACK_code("assume $foeq."DOUBLET".bool(equiv_store_double(__SMACK_equiv_store_counter), @);", x); + __SMACK_code("__SMACK_equiv_store_counter := __SMACK_equiv_store_counter + 1;"); } -void __VERIFIER_equiv_check_double(double x, int id) { - __SMACK_code("assert $foeq."DOUBLET".bool(@, equiv_store_double(@));", x, id); +void __VERIFIER_equiv_check_double(double x) { + __SMACK_code("assert $foeq."DOUBLET".bool(@, equiv_store_double(__SMACK_equiv_load_counter));", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } -void __VERIFIER_equiv_assume_double(double x, int id) { - __SMACK_code("assume $foeq."DOUBLET".bool(@, equiv_store_double(@));", x, id); +void __VERIFIER_equiv_assume_double(double x) { + __SMACK_code("assume $foeq."DOUBLET".bool(@, equiv_store_double(__SMACK_equiv_load_counter));", x); + __SMACK_code("__SMACK_equiv_load_counter := __SMACK_equiv_load_counter + 1;"); } diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs index a8e3f317d..15bf20cc1 100644 --- a/share/smack/lib/smack.rs +++ b/share/smack/lib/smack.rs @@ -22,45 +22,45 @@ extern "C" { 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_unsigned_char(val: u8); + pub fn __VERIFIER_equiv_check_unsigned_char(val: u8); + pub fn __VERIFIER_equiv_assume_unsigned_char(val: u8); - 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_signed_char(val: i8); + pub fn __VERIFIER_equiv_check_signed_char(val: i8); + pub fn __VERIFIER_equiv_assume_signed_char(val: i8); - 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_unsigned_short(val: u16); + pub fn __VERIFIER_equiv_check_unsigned_short(val: u16); + pub fn __VERIFIER_equiv_assume_unsigned_short(val: u16); - 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_signed_short(val: i16); + pub fn __VERIFIER_equiv_check_signed_short(val: i16); + pub fn __VERIFIER_equiv_assume_signed_short(val: i16); - 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_unsigned_int(val: u32); + pub fn __VERIFIER_equiv_check_unsigned_int(val: u32); + pub fn __VERIFIER_equiv_assume_unsigned_int(val: u32); - 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_signed_int(val: i32); + pub fn __VERIFIER_equiv_check_signed_int(val: i32); + pub fn __VERIFIER_equiv_assume_signed_int(val: 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_unsigned_long(val: u64); + pub fn __VERIFIER_equiv_check_unsigned_long(val: u64); + pub fn __VERIFIER_equiv_assume_unsigned_long(val: u64); - 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_signed_long(val: i64); + pub fn __VERIFIER_equiv_check_signed_long(val: i64); + pub fn __VERIFIER_equiv_assume_signed_long(val: i64); - 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_float(val: f32); + pub fn __VERIFIER_equiv_check_float(val: f32); + pub fn __VERIFIER_equiv_assume_float(val: f32); - 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); + pub fn __VERIFIER_equiv_store_double(val: f64); + pub fn __VERIFIER_equiv_check_double(val: f64); + pub fn __VERIFIER_equiv_assume_double(val: f64); } #[macro_export] @@ -134,117 +134,117 @@ 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_store_u8(val: u8) { + unsafe { __VERIFIER_equiv_store_unsigned_char(val) }; } -pub fn verifier_equiv_assume_u8(val: u8, id: i32) { - unsafe { __VERIFIER_equiv_assume_unsigned_char(val, id) }; +pub fn verifier_equiv_assume_u8(val: u8) { + unsafe { __VERIFIER_equiv_assume_unsigned_char(val) }; } -pub fn verifier_equiv_check_u8(val: u8, id: i32) { - unsafe { __VERIFIER_equiv_check_unsigned_char(val, id) }; +pub fn verifier_equiv_check_u8(val: u8) { + unsafe { __VERIFIER_equiv_check_unsigned_char(val) }; } -pub fn verifier_equiv_store_i8(val: i8, id: i32) { - unsafe { __VERIFIER_equiv_store_signed_char(val, id) }; +pub fn verifier_equiv_store_i8(val: i8) { + unsafe { __VERIFIER_equiv_store_signed_char(val) }; } -pub fn verifier_equiv_assume_i8(val: i8, id: i32) { - unsafe { __VERIFIER_equiv_assume_signed_char(val, id) }; +pub fn verifier_equiv_assume_i8(val: i8) { + unsafe { __VERIFIER_equiv_assume_signed_char(val) }; } -pub fn verifier_equiv_check_i8(val: i8, id: i32) { - unsafe { __VERIFIER_equiv_check_signed_char(val, id) }; +pub fn verifier_equiv_check_i8(val: i8) { + unsafe { __VERIFIER_equiv_check_signed_char(val) }; } -pub fn verifier_equiv_store_u16(val: u16, id: i32) { - unsafe { __VERIFIER_equiv_store_unsigned_short(val, id) }; +pub fn verifier_equiv_store_u16(val: u16) { + unsafe { __VERIFIER_equiv_store_unsigned_short(val) }; } -pub fn verifier_equiv_assume_u16(val: u16, id: i32) { - unsafe { __VERIFIER_equiv_assume_unsigned_short(val, id) }; +pub fn verifier_equiv_assume_u16(val: u16) { + unsafe { __VERIFIER_equiv_assume_unsigned_short(val) }; } -pub fn verifier_equiv_check_u16(val: u16, id: i32) { - unsafe { __VERIFIER_equiv_check_unsigned_short(val, id) }; +pub fn verifier_equiv_check_u16(val: u16) { + unsafe { __VERIFIER_equiv_check_unsigned_short(val) }; } -pub fn verifier_equiv_store_i16(val: i16, id: i32) { - unsafe { __VERIFIER_equiv_store_signed_short(val, id) }; +pub fn verifier_equiv_store_i16(val: i16) { + unsafe { __VERIFIER_equiv_store_signed_short(val) }; } -pub fn verifier_equiv_assume_i16(val: i16, id: i32) { - unsafe { __VERIFIER_equiv_assume_signed_short(val, id) }; +pub fn verifier_equiv_assume_i16(val: i16) { + unsafe { __VERIFIER_equiv_assume_signed_short(val) }; } -pub fn verifier_equiv_check_i16(val: i16, id: i32) { - unsafe { __VERIFIER_equiv_check_signed_short(val, id) }; +pub fn verifier_equiv_check_i16(val: i16) { + unsafe { __VERIFIER_equiv_check_signed_short(val) }; } -pub fn verifier_equiv_store_u32(val: u32, id: i32) { - unsafe { __VERIFIER_equiv_store_unsigned_int(val, id) }; +pub fn verifier_equiv_store_u32(val: u32) { + unsafe { __VERIFIER_equiv_store_unsigned_int(val) }; } -pub fn verifier_equiv_assume_u32(val: u32, id: i32) { - unsafe { __VERIFIER_equiv_assume_unsigned_int(val, id) }; +pub fn verifier_equiv_assume_u32(val: u32) { + unsafe { __VERIFIER_equiv_assume_unsigned_int(val) }; } -pub fn verifier_equiv_check_u32(val: u32, id: i32) { - unsafe { __VERIFIER_equiv_check_unsigned_int(val, id) }; +pub fn verifier_equiv_check_u32(val: u32) { + unsafe { __VERIFIER_equiv_check_unsigned_int(val) }; } -pub fn verifier_equiv_store_i32(val: i32, id: i32) { - unsafe { __VERIFIER_equiv_store_signed_int(val, id) }; +pub fn verifier_equiv_store_i32(val: i32) { + unsafe { __VERIFIER_equiv_store_signed_int(val) }; } -pub fn verifier_equiv_assume_i32(val: i32, id: i32) { - unsafe { __VERIFIER_equiv_assume_signed_int(val, id) }; +pub fn verifier_equiv_assume_i32(val: i32) { + unsafe { __VERIFIER_equiv_assume_signed_int(val) }; } -pub fn verifier_equiv_check_i32(val: i32, id: i32) { - unsafe { __VERIFIER_equiv_check_signed_int(val, id) }; +pub fn verifier_equiv_check_i32(val: i32) { + unsafe { __VERIFIER_equiv_check_signed_int(val) }; } -pub fn verifier_equiv_store_u64(val: u64, id: i32) { - unsafe { __VERIFIER_equiv_store_unsigned_long(val, id) }; +pub fn verifier_equiv_store_u64(val: u64) { + unsafe { __VERIFIER_equiv_store_unsigned_long(val) }; } -pub fn verifier_equiv_assume_u64(val: u64, id: i32) { - unsafe { __VERIFIER_equiv_assume_unsigned_long(val, id) }; +pub fn verifier_equiv_assume_u64(val: u64) { + unsafe { __VERIFIER_equiv_assume_unsigned_long(val) }; } -pub fn verifier_equiv_check_u64(val: u64, id: i32) { - unsafe { __VERIFIER_equiv_check_unsigned_long(val, id) }; +pub fn verifier_equiv_check_u64(val: u64) { + unsafe { __VERIFIER_equiv_check_unsigned_long(val) }; } -pub fn verifier_equiv_store_i64(val: i64, id: i32) { - unsafe { __VERIFIER_equiv_store_signed_long(val, id) }; +pub fn verifier_equiv_store_i64(val: i64) { + unsafe { __VERIFIER_equiv_store_signed_long(val) }; } -pub fn verifier_equiv_assume_i64(val: i64, id: i32) { - unsafe { __VERIFIER_equiv_assume_signed_long(val, id) }; +pub fn verifier_equiv_assume_i64(val: i64) { + unsafe { __VERIFIER_equiv_assume_signed_long(val) }; } -pub fn verifier_equiv_check_i64(val: i64, id: i32) { - unsafe { __VERIFIER_equiv_check_signed_long(val, id) }; +pub fn verifier_equiv_check_i64(val: i64) { + unsafe { __VERIFIER_equiv_check_signed_long(val) }; } -pub fn verifier_equiv_store_f32(val: f32, id: i32) { - unsafe { __VERIFIER_equiv_store_float(val, id) }; +pub fn verifier_equiv_store_f32(val: f32) { + unsafe { __VERIFIER_equiv_store_float(val) }; } -pub fn verifier_equiv_assume_f32(val: f32, id: i32) { - unsafe { __VERIFIER_equiv_assume_float(val, id) }; +pub fn verifier_equiv_assume_f32(val: f32) { + unsafe { __VERIFIER_equiv_assume_float(val) }; } -pub fn verifier_equiv_check_f32(val: f32, id: i32) { - unsafe { __VERIFIER_equiv_check_float(val, id) }; +pub fn verifier_equiv_check_f32(val: f32) { + unsafe { __VERIFIER_equiv_check_float(val) }; } -pub fn verifier_equiv_store_f64(val: f64, id: i32) { - unsafe { __VERIFIER_equiv_store_double(val, id) }; +pub fn verifier_equiv_store_f64(val: f64) { + unsafe { __VERIFIER_equiv_store_double(val) }; } -pub fn verifier_equiv_assume_f64(val: f64, id: i32) { - unsafe { __VERIFIER_equiv_assume_double(val, id) }; +pub fn verifier_equiv_assume_f64(val: f64) { + unsafe { __VERIFIER_equiv_assume_double(val) }; } -pub fn verifier_equiv_check_f64(val: f64, id: i32) { - unsafe { __VERIFIER_equiv_check_double(val, id) }; +pub fn verifier_equiv_check_f64(val: f64) { + unsafe { __VERIFIER_equiv_check_double(val) }; } #[macro_export]