crangler loop invariants

Author: qinheping

regression/crangler/loop-invariant-01/main.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/crangler/loop-invariant-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+while\(i \< 2\) \_\_CPROVER
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER
+--
+Annotate loop invariant only to the for-loop.

regression/crangler/loop-invariant-01/test.json

@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "while 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/loop-invariant-02/main.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/crangler/loop-invariant-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+while\(i \< 2\) \_\_CPROVER
+--
+Annotate loop invariant only to the while-loop.

regression/crangler/loop-invariant-02/test.json

@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "for 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/loop-invariant-03/main.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/crangler/loop-invariant-03/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+while\(i \< 2\) \_\_CPROVER
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER
+--
+Annotate loop invariant only to the second loop.

regression/crangler/loop-invariant-03/test.json

@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "loop 2 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

src/crangler/c_wrangler.cpp

@@ -213,8 +213,8 @@ void c_wranglert::configure_functions(const jsont &config)
           function_config.assertions.emplace_back(split[1], rest.str());
         }
         else if(
-          (split[0] == "for" && split.size() >= 3 && split[2] == "invariant") ||
-          (split[0] == "while" && split.size() >= 3 && split[2] == "invariant"))
+          (split[0] == "for" || split[0] == "while" || split[0] == "loop") &&
+          split.size() >= 3 && split[2] == "invariant")
         {
           std::ostringstream rest;
           join_strings(rest, split.begin() + 3, split.end(), ' ');
@@ -434,7 +434,10 @@ static void mangle_function(
         {
           while_count++;
           const auto &invariant =
-            loop_invariants["while" + std::to_string(while_count)];
+            loop_invariants.count("while" + std::to_string(while_count))
+              ? loop_invariants["while" + std::to_string(while_count)]
+              : loop_invariants
+                  ["loop" + std::to_string(while_count + for_count)];
 
           if(!invariant.empty())
           {
@@ -449,7 +452,10 @@ static void mangle_function(
         {
           for_count++;
           const auto &invariant =
-            loop_invariants["for" + std::to_string(for_count)];
+            loop_invariants.count("for" + std::to_string(for_count))
+              ? loop_invariants["for" + std::to_string(for_count)]
+              : loop_invariants
+                  ["loop" + std::to_string(while_count + for_count)];
 
           if(!invariant.empty())
           {