Reformatting

smackers · Oct 19, 2024 · e04fceb · e04fceb
1 parent 8c77e35
commit e04fceb
Show file tree

Hide file tree

Showing 7 changed files with 288 additions and 230 deletions.
diff --git 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
@@ -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
@@ -38,6 +38,11 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) {
   SmackRep rep(&M.getDataLayout(), &naming, program, &getAnalysis<Regions>());
   std::list<Decl *> &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
@@ -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
@@ -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_*/