Do not add instance counter to predicate implementations

src/main/scala/gvc/benchmarking/BaselineChecks.scala

@@ -28,8 +28,13 @@ class BaselineChecks(
   val precision = new EquirecursivePrecision(program)
 
   def insert(): Unit = {
+    // Only inject instance counter into existing methods, not methods that are
+    // added to implement predicates
+    val programMethods = program.methods.toList
+
     program.methods.foreach(insertChecks)
-    InstanceCounter.inject(program, structIds)
+
+    InstanceCounter.inject(programMethods, structIds)
   }
 
   def insertChecks(

src/main/scala/gvc/weaver/Checker.scala

@@ -30,7 +30,11 @@ object Checker {
       insert(program, method, runtime, implementation)
     }
 
-    InstanceCounter.inject(program.program, structIdFields)
+    // Use the methods from the ProgramDependencies object, to avoid injecting
+    // instance counter into predicate implementations
+    InstanceCounter.inject(
+      program.methods.values.map(_.method).toSeq,
+      structIdFields)
   }
 
   // Assumes that there is a single return statement at the end of the method.

src/main/scala/gvc/weaver/InstanceCounter.scala

@@ -1,17 +1,26 @@
 package gvc.weaver
 
 import gvc.transformer.IR
+import scala.collection.mutable
 
 object InstanceCounter {
   private val counterRef = new IR.PointerType(IR.IntType)
   private val counterName = "_instanceCounter"
 
-  def inject(program: IR.Program, idFields: Map[String, IR.StructField]): Unit = {
-    program.methods.foreach(inject(_, idFields))
+  def inject(methods: Seq[IR.Method], idFields: Map[String, IR.StructField]): Unit = {
+    val names = mutable.HashSet[String]()
+    for (m <- methods) {
+      val name = m.name
+      if (name != "main")
+        names += name
+    }
+
+    methods.foreach(inject(_, names, idFields))
   }
 
   private def inject(
     method: IR.Method,
+    methods: mutable.HashSet[String],
     idFields: Map[String, IR.StructField]
   ): Unit = {
     val counter = method.name match {
@@ -23,23 +32,28 @@ object InstanceCounter {
       case _ => method.addParameter(counterRef, counterName)
     }
 
-    inject(method.body, counter, idFields)
+    inject(method.body, methods, counter, idFields)
   }
 
-  private def inject(block: IR.Block, counter: IR.Var, idFields: Map[String, IR.StructField]): Unit = {
+  private def inject(
+    block: IR.Block,
+    methods: mutable.HashSet[String],
+    counter: IR.Var,
+    idFields: Map[String, IR.StructField]
+  ): Unit = {
     block.foreach(_ match {
       case call: IR.Invoke => call.callee match {
-        case m: IR.Method if m.name != "main" =>
+        case m: IR.Method if methods.contains(m.name) =>
           call.arguments :+= counter
         case _ => ()
       }
 
       case cond: IR.If => {
-        inject(cond.ifTrue, counter, idFields)
-        inject(cond.ifFalse, counter, idFields)
+        inject(cond.ifTrue, methods, counter, idFields)
+        inject(cond.ifFalse, methods, counter, idFields)
       }
       case loop: IR.While => {
-        inject(loop.body, counter, idFields)
+        inject(loop.body, methods, counter, idFields)
       }
       case alloc: IR.AllocStruct => {
         idFields.get(alloc.struct.name).foreach(field => {

src/test/resources/baseline/predicate.baseline.c0

@@ -8,13 +8,13 @@ struct Node
   int _id;
 };
 
-void assert_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* add_perms, int* _instanceCounter);
-void assert_remove_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* remove_perms, struct OwnedFields* add_perms, int* _instanceCounter);
+void assert_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* add_perms);
+void assert_remove_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* remove_perms, struct OwnedFields* add_perms);
 struct Node* emptyList(struct OwnedFields* _ownedFields, int* _instanceCounter);
 int main();
 struct Node* prependList(int value, struct Node* node, struct OwnedFields* _ownedFields, int* _instanceCounter);
 
-void assert_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* add_perms, int* _instanceCounter)
+void assert_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* add_perms)
 {
   if (node == NULL)
   {
@@ -24,11 +24,11 @@ void assert_add_list(struct Node* node, struct OwnedFields* assert_perms, struct
   {
     runtime_assert(assert_perms, node == NULL ? -1 : node->_id, 0, "No permission to access 'node->value'");
     runtime_add(add_perms, node == NULL ? -1 : node->_id, 2, 0, "Invalid aliasing - 'node->value' overlaps with existing permission");
-    assert_add_list(node->next, assert_perms, add_perms, _instanceCounter);
+    assert_add_list(node->next, assert_perms, add_perms);
   }
 }
 
-void assert_remove_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* remove_perms, struct OwnedFields* add_perms, int* _instanceCounter)
+void assert_remove_add_list(struct Node* node, struct OwnedFields* assert_perms, struct OwnedFields* remove_perms, struct OwnedFields* add_perms)
 {
   if (node == NULL)
   {
@@ -39,7 +39,7 @@ void assert_remove_add_list(struct Node* node, struct OwnedFields* assert_perms,
     runtime_assert(assert_perms, node == NULL ? -1 : node->_id, 0, "No permission to access 'node->value'");
     runtime_remove(remove_perms, node == NULL ? -1 : node->_id, 0, "No permission to access 'node->value'");
     runtime_add(add_perms, node == NULL ? -1 : node->_id, 2, 0, "Invalid aliasing - 'node->value' overlaps with existing permission");
-    assert_remove_add_list(node->next, assert_perms, remove_perms, add_perms, _instanceCounter);
+    assert_remove_add_list(node->next, assert_perms, remove_perms, add_perms);
   }
 }
 
@@ -50,7 +50,7 @@ struct Node* emptyList(struct OwnedFields* _ownedFields, int* _instanceCounter)
   _tempFields = runtime_init();
   assert(true);
   nullList = NULL;
-  assert_add_list(nullList, _tempFields, _ownedFields, _instanceCounter);
+  assert_add_list(nullList, _tempFields, _ownedFields);
   return nullList;
 }
 
@@ -70,7 +70,7 @@ struct Node* prependList(int value, struct Node* node, struct OwnedFields* _owne
   struct Node* newNode = NULL;
   struct OwnedFields* _tempFields = NULL;
   _tempFields = runtime_init();
-  assert_remove_add_list(node, _ownedFields, _ownedFields, _tempFields, _instanceCounter);
+  assert_remove_add_list(node, _ownedFields, _ownedFields, _tempFields);
   newNode = alloc(struct Node);
   newNode->_id = *_instanceCounter;
   *_instanceCounter = *_instanceCounter + 1;
@@ -79,6 +79,6 @@ struct Node* prependList(int value, struct Node* node, struct OwnedFields* _owne
   newNode->next = node;
   runtime_assert(_tempFields, newNode == NULL ? -1 : newNode->_id, 0, "No permission to access 'newNode->value'");
   newNode->value = value;
-  assert_add_list(newNode, _tempFields, _ownedFields, _instanceCounter);
+  assert_add_list(newNode, _tempFields, _ownedFields);
   return newNode;
 }

src/test/resources/verifier/bare_pointers.output.c0

@@ -49,12 +49,12 @@ struct _ptr_struct_Test_
   int _id;
 };
 
-void add_accInt(struct _ptr_int* ptr, struct OwnedFields* add_perms, int* _instanceCounter);
+void add_accInt(struct _ptr_int* ptr, struct OwnedFields* add_perms);
 int main();
-void remove_accInt(struct _ptr_int* ptr, struct OwnedFields* remove_perms, int* _instanceCounter);
+void remove_accInt(struct _ptr_int* ptr, struct OwnedFields* remove_perms);
 void test(struct _ptr_int* input, int* _instanceCounter);
 
-void add_accInt(struct _ptr_int* ptr, struct OwnedFields* add_perms, int* _instanceCounter)
+void add_accInt(struct _ptr_int* ptr, struct OwnedFields* add_perms)
 {
   runtime_add(add_perms, ptr == NULL ? -1 : ptr->_id, 1, 0, "Invalid aliasing - 'ptr->value' overlaps with existing permission");
 }
@@ -110,12 +110,12 @@ int main()
   runtime_addAll(_ownedFields, ptr->_id, 1);
   if (_ownedFields != NULL)
   {
-    remove_accInt(ptr, _ownedFields, _instanceCounter);
+    remove_accInt(ptr, _ownedFields);
   }
   test(ptr, _instanceCounter);
   if (_ownedFields != NULL)
   {
-    add_accInt(ptr, _ownedFields, _instanceCounter);
+    add_accInt(ptr, _ownedFields);
   }
   wrapper = alloc(struct Wrapper);
   wrapper->_id = *_instanceCounter;
@@ -135,7 +135,7 @@ int main()
   return 0;
 }
 
-void remove_accInt(struct _ptr_int* ptr, struct OwnedFields* remove_perms, int* _instanceCounter)
+void remove_accInt(struct _ptr_int* ptr, struct OwnedFields* remove_perms)
 {
   runtime_remove(remove_perms, ptr->_id, 0, "No permission to access 'ptr->value'");
 }

src/test/resources/verifier/loop3.output.c0

@@ -7,28 +7,28 @@ struct _ptr_int
   int _id;
 };
 
-void add_nested(struct _ptr_int* value, struct OwnedFields* add_perms, int* _instanceCounter);
-void add_test(struct _ptr_int* value, struct OwnedFields* add_perms, int* _instanceCounter);
-void assert_nested(struct _ptr_int* value, struct OwnedFields* assert_perms, int* _instanceCounter);
-void assert_test(struct _ptr_int* value, struct OwnedFields* assert_perms, int* _instanceCounter);
+void add_nested(struct _ptr_int* value, struct OwnedFields* add_perms);
+void add_test(struct _ptr_int* value, struct OwnedFields* add_perms);
+void assert_nested(struct _ptr_int* value, struct OwnedFields* assert_perms);
+void assert_test(struct _ptr_int* value, struct OwnedFields* assert_perms);
 int main();
 
-void add_nested(struct _ptr_int* value, struct OwnedFields* add_perms, int* _instanceCounter)
+void add_nested(struct _ptr_int* value, struct OwnedFields* add_perms)
 {
 }
 
-void add_test(struct _ptr_int* value, struct OwnedFields* add_perms, int* _instanceCounter)
+void add_test(struct _ptr_int* value, struct OwnedFields* add_perms)
 {
 }
 
-void assert_nested(struct _ptr_int* value, struct OwnedFields* assert_perms, int* _instanceCounter)
+void assert_nested(struct _ptr_int* value, struct OwnedFields* assert_perms)
 {
   assert(true);
 }
 
-void assert_test(struct _ptr_int* value, struct OwnedFields* assert_perms, int* _instanceCounter)
+void assert_test(struct _ptr_int* value, struct OwnedFields* assert_perms)
 {
-  assert_nested(value, assert_perms, _instanceCounter);
+  assert_nested(value, assert_perms);
 }
 
 int main()
@@ -49,7 +49,7 @@ int main()
   _tempFields = runtime_init();
   if (_cond)
   {
-    assert_test(value, _ownedFields, _instanceCounter);
+    assert_test(value, _ownedFields);
   }
   _cond = i < 10;
   while (i < 10)

src/test/resources/verifier/predicates.output.c0

@@ -8,21 +8,21 @@ struct Node
   int _id;
 };
 
-void add_wrappedAcc(struct Node* node, struct OwnedFields* add_perms, int* _instanceCounter);
-void assert_wrappedAcc(struct Node* node, struct OwnedFields* assert_perms, int* _instanceCounter);
+void add_wrappedAcc(struct Node* node, struct OwnedFields* add_perms);
+void assert_wrappedAcc(struct Node* node, struct OwnedFields* assert_perms);
 int fullyImprecise(struct Node* a, struct OwnedFields* _ownedFields, int* _instanceCounter);
 int fullyPrecise(struct Node* a, int* _instanceCounter);
 int imprecisePostcondition(struct Node* a, int* _instanceCounter);
 int imprecisePrecondition(struct Node* a, struct OwnedFields* _ownedFields, int* _instanceCounter);
 int main();
 
-void add_wrappedAcc(struct Node* node, struct OwnedFields* add_perms, int* _instanceCounter)
+void add_wrappedAcc(struct Node* node, struct OwnedFields* add_perms)
 {
   runtime_add(add_perms, node == NULL ? -1 : node->_id, 2, 0, "Invalid aliasing - 'node->value' overlaps with existing permission");
   runtime_add(add_perms, node == NULL ? -1 : node->_id, 2, 1, "Invalid aliasing - 'node->next' overlaps with existing permission");
 }
 
-void assert_wrappedAcc(struct Node* node, struct OwnedFields* assert_perms, int* _instanceCounter)
+void assert_wrappedAcc(struct Node* node, struct OwnedFields* assert_perms)
 {
   runtime_assert(assert_perms, node == NULL ? -1 : node->_id, 0, "No permission to access 'node->value'");
   runtime_assert(assert_perms, node == NULL ? -1 : node->_id, 1, "No permission to access 'node->next'");
@@ -40,11 +40,11 @@ int fullyPrecise(struct Node* a, int* _instanceCounter)
   struct OwnedFields* _ownedFields = NULL;
   struct OwnedFields* _tempFields = NULL;
   _ownedFields = runtime_init();
-  add_wrappedAcc(a, _ownedFields, _instanceCounter);
+  add_wrappedAcc(a, _ownedFields);
   _ = imprecisePostcondition(a, _instanceCounter);
   _tempFields = runtime_init();
-  assert_wrappedAcc(a, _ownedFields, _instanceCounter);
-  add_wrappedAcc(a, _tempFields, _instanceCounter);
+  assert_wrappedAcc(a, _ownedFields);
+  add_wrappedAcc(a, _tempFields);
   return _;
 }