Ensure labels (even __CPROVER_ASYNC_*) are unique per function

An upcoming change will enforce per-function unique labels, as mandated
by the C standard. We were sometimes sloppy about this with
__CPROVER_ASYNC_* pseudo-labels as they don't actually indicate jump
targets.

Author: tautschnig

regression/cbmc-concurrency/atomic_section_sc3/main.c

@@ -85,8 +85,8 @@ unsigned dec() {
 
 int main(){
 __CPROVER_ASYNC_1: inc();
-__CPROVER_ASYNC_1: dec();
-__CPROVER_ASYNC_1: dec();
+__CPROVER_ASYNC_2: dec();
+__CPROVER_ASYNC_3: dec();
 
   return 0;
 }

regression/cbmc-concurrency/conditional_spawn2/main.c

@@ -16,8 +16,8 @@ int main()
 __CPROVER_ASYNC_1: thread();
   }
 
-__CPROVER_ASYNC_1: thread();
-__CPROVER_ASYNC_1: thread();
+__CPROVER_ASYNC_2: thread();
+__CPROVER_ASYNC_3: thread();
 
   __CPROVER_assert(n<4, "3 threads spawned");
 

regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c

@@ -8,7 +8,7 @@
 
 #ifdef _ENABLE_CBMC_
 
-#define ASYNC(c) __CPROVER_ASYNC_1: (c)
+#define ASYNC(n, c) __CPROVER_ASYNC_ ## n: (c)
 #define ATOMIC_BEGIN  __CPROVER_atomic_begin()
 #define ATOMIC_END  __CPROVER_atomic_end()
 
@@ -233,7 +233,7 @@ void* write_data_register(struct Hardware *hw, RegisterId reg_id, Register value
     pthread_create(&interrupt_thread, NULL, hw->interrupt_handler, (void *) hw->fw);
   }
 #else
-    ASYNC(hw->interrupt_handler((void *) hw->fw));
+    ASYNC(1, hw->interrupt_handler((void *) hw->fw));
 #endif
 
 SKIP:
@@ -346,7 +346,7 @@ int main(void)
   pthread_t firmware_thread;
   pthread_create(&firmware_thread, NULL, poll, (void *) fw);
 #else
-  ASYNC(poll((void *) fw));
+  ASYNC(1, poll((void *) fw));
 #endif
 
 #ifdef _EXPOSE_BUG_
@@ -358,7 +358,7 @@ int main(void)
   pthread_t stimulus_thread;
   pthread_create(&stimulus_thread, NULL, stimulus, (void *) hw);
 #else
-  ASYNC(stimulus((void *) hw));
+  ASYNC(2, stimulus((void *) hw));
 #endif
 
 #ifdef _EXPOSE_BUG_

regression/cbmc-concurrency/invalid_object1/main.c

@@ -283,7 +283,7 @@ static signed int ethoc_reset(struct ethoc *dev)
 __CPROVER_ASYNC_1:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
 
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
   return 0;
 }

regression/cbmc-concurrency/recursion1/main.c

@@ -13,7 +13,7 @@ int main()
 
 start2:
   (void)0;
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   goto start2;
 
   rec_spawn();

regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c

@@ -118,7 +118,7 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2: qrcu_reader2();
+__CPROVER_ASYNC_3: qrcu_updater();
   return 0;
 }

regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c

@@ -118,7 +118,7 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2: qrcu_reader2();
+__CPROVER_ASYNC_3: qrcu_updater();
   return 0;
 }

regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c

@@ -39,8 +39,8 @@ void *reader() { //reader
 
 int main() {
 __CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
-__CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
+__CPROVER_ASYNC_2: reader();
+__CPROVER_ASYNC_3: writer();
+__CPROVER_ASYNC_4: reader();
   return 0;
 }