Annotate loop unwinding bounds via pragma

Enable users to specify loop unwinding information directly in source code via `#pragma CPROVER unwind N` with some number `N`. This should be less susceptible to code changes than unwindsets that use loop numbers: those loop numbers may change when code outside the named loop is modified, e.g., when adding or removing other loops.
tautschnig · Aug 29, 2024 · ae74413 · ae74413
1 parent 6752c40
commit ae74413
Show file tree

Hide file tree

Showing 7 changed files with 110 additions and 20 deletions.
diff --git a/regression/cbmc/pragma_cprover_loop1/main.c b/regression/cbmc/pragma_cprover_loop1/main.c
@@ -0,0 +1,26 @@
+int main()
+{
+#pragma CPROVER unwind 2
+  for(int i = 0; i < 5; ++i)
+  {
+    if(i < 2)
+      continue;
+
+    for(int j = 0; j < 10; ++j)
+      ++j;
+  }
+
+#pragma CPROVER unwind 1
+  do
+  {
+    int x = 42;
+  } while(0);
+
+#pragma CPROVER unwind 10
+  while(1)
+  {
+    int x = 42;
+  }
+
+  __CPROVER_assert(0, "false");
+}
diff --git a/regression/cbmc/pragma_cprover_loop1/test.desc b/regression/cbmc/pragma_cprover_loop1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
@@ -188,21 +188,37 @@ void ansi_c_parsert::pragma_cprover_add_check(
   if(pragma_cprover_stack.empty())
     pragma_cprover_push();
 
-  pragma_cprover_stack.back()[name] = enabled;
+  pragma_cprover_stack.back()[name] = enabled ? 1 : 0;
+}
+
+void ansi_c_parsert::pragma_cprover_add_unwind(size_t bound)
+{
+  if(pragma_cprover_stack.empty())
+    pragma_cprover_push();
+
+  pragma_cprover_stack.back()["unwind"] = bound;
+}
+
+void ansi_c_parsert::pragma_cprover_consume_unwind()
+{
+  for(auto &map : pragma_cprover_stack)
+    map.erase("unwind");
+
+  set_pragma_cprover();
 }
 
 bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled)
 {
   auto top = pragma_cprover_stack.back();
   auto found = top.find(name);
-  return found != top.end() && found->second != enabled;
+  return found != top.end() && found->second != (enabled ? 1 : 0);
 }
 
 void ansi_c_parsert::set_pragma_cprover()
 {
   // handle enable/disable shadowing
   // by bottom-to-top flattening
-  std::map<irep_idt, bool> flattened;
+  std::map<irep_idt, size_t> flattened;
 
   for(const auto &pragma_set : pragma_cprover_stack)
     for(const auto &pragma : pragma_set)
@@ -212,9 +228,18 @@ void ansi_c_parsert::set_pragma_cprover()
 
   for(const auto &pragma : flattened)
   {
-    std::string check_name = id2string(pragma.first);
-    std::string full_name =
-      (pragma.second ? "enable:" : "disable:") + check_name;
-    source_location.add_pragma(full_name);
+    if(pragma.first == "unwind")
+    {
+      std::string unwind_info =
+        id2string(pragma.first) + ":" + std::to_string(pragma.second);
+      source_location.add_pragma(unwind_info);
+    }
+    else
+    {
+      std::string check_name = id2string(pragma.first);
+      std::string full_name =
+        (pragma.second == 1 ? "enable:" : "disable:") + check_name;
+      source_location.add_pragma(full_name);
+    }
   }
 }
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
@@ -153,12 +153,18 @@ class ansi_c_parsert:public parsert
   /// is already present at top of the stack
   bool pragma_cprover_clash(const irep_idt &name, bool enabled);
 
+  /// \brief Adds an unwinding bound to the CPROVER pragma stack
+  void pragma_cprover_add_unwind(size_t bound);
+
+  /// \brief Remove unwinding bounds from the CPROVER pragma stack
+  void pragma_cprover_consume_unwind();
+
   /// \brief Tags \ref source_location with
   /// the current CPROVER pragma stack
   void set_pragma_cprover();
 
 private:
-  std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
+  std::list<std::map<const irep_idt, size_t>> pragma_cprover_stack;
 };
 
 void ansi_c_scanner_init(ansi_c_parsert &);

diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -415,6 +415,7 @@ void c_typecheck_baset::typecheck_expression(codet &code)
 
 void c_typecheck_baset::typecheck_for(codet &code)
 {
+  warning() << code.pretty() << eom;
   if(code.operands().size()!=4)
   {
     error().source_location = code.source_location();
@@ -771,6 +772,7 @@ void c_typecheck_baset::typecheck_switch(codet &code)
 
 void c_typecheck_baset::typecheck_while(code_whilet &code)
 {
+  warning() << code.pretty() << eom;
   if(code.operands().size()!=2)
   {
     error().source_location = code.source_location();
@@ -817,6 +819,7 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
 
 void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
 {
+  warning() << code.pretty() << eom;
   if(code.operands().size()!=2)
   {
     error().source_location = code.source_location();

diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
@@ -2495,25 +2495,31 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
+        {
+          PARSER.pragma_cprover_consume_unwind();
+        }
           cprover_contract_assigns_opt
           cprover_contract_loop_invariant_list_opt 
           cprover_contract_decreases_opt
           statement
         {
           $$=$1;
           statement($$, ID_while);
-          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
-
-          if(!parser_stack($5).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($5).operands());
+          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($9)));
 
           if(!parser_stack($6).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($6).operands());
 
           if(!parser_stack($7).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
+
+          if(!parser_stack($8).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($8).operands());
         }
         | TOK_DO
+        {
+          PARSER.pragma_cprover_consume_unwind();
+        }
           cprover_contract_assigns_opt
           cprover_contract_loop_invariant_list_opt
           cprover_contract_decreases_opt
@@ -2522,16 +2528,16 @@ iteration_statement:
         {
           $$=$1;
           statement($$, ID_dowhile);
-          parser_stack($$).add_to_operands(std::move(parser_stack($8)), std::move(parser_stack($5)));
-
-          if(!parser_stack($2).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($2).operands());
+          parser_stack($$).add_to_operands(std::move(parser_stack($9)), std::move(parser_stack($6)));
 
           if(!parser_stack($3).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($3).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($3).operands());
 
           if(!parser_stack($4).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($4).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($4).operands());
+
+          if(!parser_stack($5).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($5).operands());
         }
         | TOK_FOR
           {
@@ -2541,6 +2547,7 @@ iteration_statement:
               unsigned prefix=++PARSER.current_scope().compound_counter;
               PARSER.new_scope(std::to_string(prefix)+"::");
             }
+            PARSER.pragma_cprover_consume_unwind();
           }
           '(' declaration_or_expression_statement
               comma_expression_opt ';'

diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
@@ -29,6 +29,7 @@ static int isatty(int) { return 0; }
 #endif
 
 #include <util/string_constant.h>
+#include <util/string2int.h>
 #include <util/unicode.h>
 
 #include "preprocessor_line.h"
@@ -443,6 +444,20 @@ enable_or_disable ("enable"|"disable")
                   PARSER.set_pragma_cprover();
                 }
 
+<CPROVER_PRAGMA>{ws}"unwind"{ws}{integer} {
+                  std::string tmp(yytext);
+                  std::string::size_type p = tmp.rfind('d') + 1;
+                  auto bound = string2optional_size_t(tmp.substr(p));
+                  if(!bound.has_value())
+                  {
+                    ansi_c_parser->parse_error(
+                      "Found invalid loop unwinding annotation " + tmp, "");
+                    return TOK_SCANNER_ERROR;
+                  }
+                  PARSER.pragma_cprover_add_unwind(*bound);
+                  PARSER.set_pragma_cprover();
+                }
+
 <CPROVER_PRAGMA>. {
                   yyansi_cerror("Unsupported #pragma CPROVER");
                   return TOK_SCANNER_ERROR;