Permit selectively disabling generated assertions

Add support for `#pragma CPROVER check disable "<name_of_check>"` to
disable generating assertions for the statement(s) that follow the
pragma.

Author: tautschnig

doc/cprover-manual/properties.md

@@ -129,6 +129,24 @@ The goto-instrument program supports these checks:
 | `--uninitialized-check`      |  add checks for uninitialized locals (experimental)  |
 | `--error-label label`        |  check that given label is unreachable               |
 
+As all of these checks apply across the entire input program, we may wish to
+disable them for selected statements in the program. For example, unsigned
+overflows can be expected and acceptable in certain instructions even when
+elsewhere we do not expect them. To selectively disable automatically generated
+properties use `#pragma CPROVER check disable "<name_of_check>"`, which remains
+in effect until a `#pragma CPROVER check pop` (to re-enable all properties
+disabled before or since the last `#pragma CPROVER check push`) is provided.
+For example, for unsigned overflow checks, use
+```
+unsigned foo(unsigned x)
+{
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+  x = x + 1; // immediately follows the pragma, no unsigned overflow check here
+#pragma CPROVER check pop
+  x = x + 2; // unsigned overflow checks are generated here
+```
+
 #### Generating function bodies
 
 Sometimes implementations for called functions are not available in the goto

regression/cbmc/pragma_cprover1/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int x;
+  int y[1];
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "bounds"
+#pragma CPROVER check disable "signed-overflow"
+  // do not generate assertions for the following statement
+  x = x + y[1];
+  // pop all annotations
+#pragma CPROVER check pop
+  // but do generate assertions for this one
+  x = y[1];
+  return x;
+}

regression/cbmc/pragma_cprover1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--signed-overflow-check --bounds-check
+line 14 array `y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/string_utils.h>
 
 #include <langapi/language.h>
 #include <langapi/mode.h>
@@ -1690,6 +1691,32 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
     return {};
 }
 
+/// Set a Boolean flag to a new value (via `set_flag`) and restore the previous
+/// value when the entire object goes out of scope.
+class flag_resett
+{
+public:
+  /// Store the current value of \p flag and then set its value to \p new_value.
+  void set_flag(bool &flag, bool new_value)
+  {
+    if(flag != new_value)
+    {
+      flags_to_reset.emplace_back(&flag, flag);
+      flag = new_value;
+    }
+  }
+
+  /// Restore the values of all flags that have been modified via `set_flag`.
+  ~flag_resett()
+  {
+    for(const auto &flag_pair : flags_to_reset)
+      *flag_pair.first = flag_pair.second;
+  }
+
+private:
+  std::list<std::pair<bool *, bool>> flags_to_reset;
+};
+
 void goto_checkt::goto_check(
   const irep_idt &function_identifier,
   goto_functiont &goto_function)
@@ -1711,6 +1738,38 @@ void goto_checkt::goto_check(
     current_target = it;
     goto_programt::instructiont &i=*it;
 
+    flag_resett flag_resetter;
+    if(!i.source_location.get_comment().empty())
+    {
+      auto disabled_checks = split_string(
+        id2string(i.source_location.get_comment()), ',', true, true);
+      for(const auto &d : disabled_checks)
+      {
+        if(d == "disable:bounds-check")
+          flag_resetter.set_flag(enable_bounds_check, false);
+        else if(d == "disable:pointer-check")
+          flag_resetter.set_flag(enable_pointer_check, false);
+        else if(d == "disable:memory-leak-check")
+          flag_resetter.set_flag(enable_memory_leak_check, false);
+        else if(d == "disable:div-by-zero-check")
+          flag_resetter.set_flag(enable_div_by_zero_check, false);
+        else if(d == "disable:signed-overflow-check")
+          flag_resetter.set_flag(enable_signed_overflow_check, false);
+        else if(d == "disable:unsigned-overflow-check")
+          flag_resetter.set_flag(enable_unsigned_overflow_check, false);
+        else if(d == "disable:pointer-overflow-check")
+          flag_resetter.set_flag(enable_pointer_overflow_check, false);
+        else if(d == "disable:float-overflow-check")
+          flag_resetter.set_flag(enable_float_overflow_check, false);
+        else if(d == "disable:conversion-check")
+          flag_resetter.set_flag(enable_conversion_check, false);
+        else if(d == "disable:undefined-shift-check")
+          flag_resetter.set_flag(enable_undefined_shift_check, false);
+        else if(d == "disable:nan-check")
+          flag_resetter.set_flag(enable_nan_check, false);
+      }
+    }
+
     new_code.clear();
 
     // we clear all recorded assertions if

src/ansi-c/ansi_c_parser.h

@@ -57,6 +57,7 @@ class ansi_c_parsert:public parsert
     parenthesis_counter=0;
     string_literal.clear();
     pragma_pack.clear();
+    pragma_cprover.clear();
 
     // set up global scope
     scopes.clear();
@@ -69,6 +70,7 @@ class ansi_c_parsert:public parsert
   unsigned parenthesis_counter;
   std::string string_literal;
   std::list<exprt> pragma_pack;
+  std::list<irep_idt> pragma_cprover;
 
   typedef configt::ansi_ct::flavourt modet;
   modet mode;

src/ansi-c/parser.y

@@ -24,6 +24,10 @@ extern char *yyansi_ctext;
 
 #include "literals/convert_integer_literal.h"
 
+#include <util/string_utils.h>
+
+#include <sstream>
+
 #include "ansi_c_y.tab.h"
 
 #ifdef _MSC_VER
@@ -2306,10 +2310,38 @@ statement_list:
           statement
         {
           init($$);
+          if(!PARSER.pragma_cprover.empty())
+          {
+            std::ostringstream oss;
+            join_strings(
+              oss,
+              PARSER.pragma_cprover.begin(),
+              PARSER.pragma_cprover.end(),
+              ',');
+            parser_stack($1).add_source_location().set_comment(oss.str());
+            Forall_operands(it, parser_stack($1))
+            {
+              it->add_source_location().set_comment(oss.str());
+            }
+          }
           mto($$, $1);
         }
         | statement_list statement
         {
+          if(!PARSER.pragma_cprover.empty())
+          {
+            std::ostringstream oss;
+            join_strings(
+              oss,
+              PARSER.pragma_cprover.begin(),
+              PARSER.pragma_cprover.end(),
+              ',');
+            parser_stack($2).add_source_location().set_comment(oss.str());
+            Forall_operands(it, parser_stack($2))
+            {
+              it->add_source_location().set_comment(oss.str());
+            }
+          }
           mto($$, $2);
         }
         ;

src/ansi-c/scanner.l

@@ -27,7 +27,9 @@
 static int isatty(int) { return 0; }
 #endif
 
+#include <util/prefix.h>
 #include <util/string_constant.h>
+#include <util/suffix.h>
 #include <util/unicode.h>
 
 #include "preprocessor_line.h"
@@ -221,7 +223,7 @@ float_s         {float}{float_suffix}|{integer}[fF]
 gcc_ext_float_s {float}{gcc_ext_float_suffix}
 cppstart        {ws}"#"{ws}
 cpplineno       {cppstart}"line"*{ws}{integer}{ws}.*{newline}
-cppdirective    {cppstart}.*
+cppdirective    {cppstart}({newline}|[^p].*|"p"[^r].*|"pr"[^a].*|"pra"[^g].*|"prag"[^m].*|"pragm"[^a].*)
 
 escape_sequence [\\][^\n]
 c_char [^'\\\n]|{escape_sequence}
@@ -232,6 +234,11 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 
 CPROVER_PREFIX  "__CPROVER_"
 
+arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
+memory_check    ("bounds"|"pointer"|"memory_leak")
+overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
+named_check     ["]({arith_check}|{memory_check}|{overflow_check})["]
+
 %x GRAMMAR
 %x COMMENT1
 %x COMMENT2
@@ -251,6 +258,8 @@ CPROVER_PREFIX  "__CPROVER_"
 %x GCC_ASM
 %x GCC_ASM_PAREN
 %x CPROVER_ID
+%x CPROVER_PRAGMA
+%x OTHER_PRAGMA
 
 %{
 void ansi_c_scanner_init()
@@ -321,7 +330,7 @@ void ansi_c_scanner_init()
                   preprocessor_line(yytext, PARSER);
                   PARSER.set_line_no(PARSER.get_line_no()-1);
                 }
-<STRING_LITERAL>{cppdirective} { /* ignore */ }
+<STRING_LITERAL>{cppstart}.* { /* ignore */ }
 <STRING_LITERAL>"/*" { yy_push_state(STRING_LITERAL_COMMENT); /* C comment, ignore */ }
 <STRING_LITERAL>"//".*\n { /* C++ comment, ignore */ }
 <STRING_LITERAL>. { // anything else: back to normal
@@ -388,8 +397,46 @@ void ansi_c_scanner_init()
                   PARSER.pragma_pack.clear();
                 }
 
-<GRAMMAR>{cppstart}"pragma"{ws}.* {
-                  // silently ignore other pragmas
+<GRAMMAR>{cppstart}"pragma"{ws}"CPROVER" { BEGIN(CPROVER_PRAGMA); }
+<CPROVER_PRAGMA>{ws}{newline} { BEGIN(GRAMMAR); }
+
+                /* CProver specific pragmas: hint to disable named checks */
+<CPROVER_PRAGMA>{ws}"check"{ws}"push" {
+                  PARSER.pragma_cprover.push_back(irep_idt{});
+                }
+<CPROVER_PRAGMA>{ws}"check"{ws}"pop" {
+                  if(!PARSER.pragma_cprover.empty())
+                    PARSER.pragma_cprover.pop_back();
+                }
+<CPROVER_PRAGMA>{ws}"check"{ws}"disable"{ws}{named_check} {
+                  std::string tmp(yytext);
+                  std::string::size_type p = tmp.find('"') + 1;
+                  std::string value =
+                    std::string("disable:") +
+                    std::string(tmp, p, tmp.size() - p - 1) +
+                    std::string("-check");
+                  if(PARSER.pragma_cprover.empty())
+                    PARSER.pragma_cprover.push_back(value);
+                  else
+                  {
+                    if(!PARSER.pragma_cprover.back().empty())
+                    {
+                      value =
+                        id2string(PARSER.pragma_cprover.back()) + "," + value;
+                    }
+                    PARSER.pragma_cprover.back() = value;
+                  }
+                }
+
+<CPROVER_PRAGMA>. {
+                  yyansi_cerror("Unsupported #pragma CPROVER");
+                  return TOK_SCANNER_ERROR;
+                }
+
+<GRAMMAR>{cppstart}"pragma" { BEGIN(OTHER_PRAGMA); }
+<OTHER_PRAGMA>.*{newline} {
+                  /* silently ignore other pragmas */
+                  BEGIN(GRAMMAR);
                 }
 
 <GRAMMAR>{cppstart}"ident"{ws}.* { /* ignore */ }