Adding the possibility to enable checks per instruction using #pragma CPROVER enable "named-check"

Handling check enable/disable shadowing in the CPROVER pragma stack
Detect and error out on simultaneous enable and disable of a check at a same pragma stack level in the ansi-c parser and goto_check.cpp

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -131,22 +131,77 @@ The goto-instrument program supports these checks:
 | `--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. As of version 5.12, CBMC supports selectively
-disabling automatically generated properties.  To disable property generation,
-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.
+disable or enable 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. 
+As of version 5.12, CBMC supports selectively disabling or enabling
+automatically generated properties using pragmas.
+
+
+CPROVER pragmas are handled using a stack:
+- `#pragma CPROVER check push` pushes a new level on the pragma stack
+- `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma
+  at the top of the stack
+- `#pragma CPROVER check enable "<name_of_check>"` adds a enable pragma
+  at the top of the stack
+- an `enable` or `disable` pragma for a given check present at the top level
+  of the stack shadows other pragmas for the same in lower levels of the stack
+- adding both `enable` and `disable` pragmas for a same check in a same level
+  of the stack creates a PARSING_ERROR.
+- `#pragma CPROVER check pop` pops a level in the stack and restores the state
+  of pragmas at the sub level
+
 For example, for unsigned overflow checks, use
+
 ```
 unsigned foo(unsigned x)
 {
 #pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+  // unsigned overflow check apply here
+  x = x + 1;
+#pragma CPROVER check pop
+  // unsigned overflow checks do not apply here
+  x = x + 2;
+```
+
+```
+unsigned foo(unsigned x)
+{
+#pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "signed-overflow"
+  // unsigned and signed overflow check apply here
+  x = x + 1;
+#pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
-  x = x + 1; // immediately follows the pragma, no unsigned overflow check here
+  // only signed overflow check apply here
+  x = x + 2;
+#pragma CPROVER check pop
+  // unsigned and signed overflow check apply here
+  x = x + 3;
+#pragma CPROVER check pop
+  // unsigned overflow checks do not apply here
+  x = x + 2;
+```
+
+```
+unsigned foo(unsigned x)
+{
+#pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "signed-overflow"
+  // unsigned and signed overflow check apply here
+  x = x + 1;
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+#pragma CPROVER check enable "unsigned-overflow"
+  // PARSING_ERROR Found enable and disable pragmas for unsigned-overflow-check
+  x = x + 2;
+#pragma CPROVER check pop
+  x = x + 3;
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks are generated here
+  x = x + 2;
 ```
 
 #### Flag --nan-check limitations

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -705,7 +705,11 @@ void janalyzer_parse_optionst::process_goto_function(
 
   // add generic checks
   goto_check(
-    function.get_function_id(), function.get_goto_function(), ns, options);
+    function.get_function_id(),
+    function.get_goto_function(),
+    ns,
+    options,
+    ui_message_handler);
 }
 
 bool janalyzer_parse_optionst::can_generate_function_body(const irep_idt &name)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -812,7 +812,11 @@ void jbmc_parse_optionst::process_goto_function(
 
   // add generic checks
   goto_check(
-    function.get_function_id(), function.get_goto_function(), ns, options);
+    function.get_function_id(),
+    function.get_goto_function(),
+    ns,
+    options,
+    ui_message_handler);
 
   // Replace Java new side effects
   remove_java_new(

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -278,7 +278,7 @@ bool jdiff_parse_optionst::process_goto_program(
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
-    goto_check(options, goto_model);
+    goto_check(options, goto_model, ui_message_handler);
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);

regression/cbmc/pragma_cprover_enable1/main.c

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

regression/cbmc/pragma_cprover_enable1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\[main\.array_bounds\.1\] line \d+ array 'y' upper bound.*FAILURE$
+^\[main\.overflow\.1\] line \d+ arithmetic overflow on signed.*FAILURE$
+^\*\* 2 of 2 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that we can selectively activate checks using pragmas.

regression/cbmc/pragma_cprover_enable2/main.c

@@ -0,0 +1,23 @@
+int foo(int x)
+{
+  return x;
+}
+
+int main()
+{
+  int m, n;
+
+#pragma CPROVER check push
+#pragma CPROVER check enable "signed-overflow"
+  // generate assertions for the following statements
+  int x = m = n + n;
+  ++n;
+  n++;
+  n += 1;
+  foo(x + n);
+#pragma CPROVER check pop
+  // but do not generate assertions for these
+  x = n + n;
+  foo(x + n);
+  return x;
+}

regression/cbmc/pragma_cprover_enable2/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+
+^\[main\.overflow\.1\] line 13 arithmetic overflow on signed \+ in n \+ n: FAILURE$
+^\[main\.overflow\.2\] line 14 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
+^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
+^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
+^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$
+^\*\* 5 of 5 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/pragma_cprover_enable3/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(sizeof(*p));
+  char *q;
+
+#pragma CPROVER check push
+#pragma CPROVER check enable "pointer-primitive"
+  // generate checks for the following statements and fail
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check pop
+
+  // but do not generate checks on the following statements
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+}

regression/cbmc/pragma_cprover_enable3/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+
+^main.c function main$
+^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^\[main.pointer_primitives.\d+\] line 17
+--

regression/cbmc/pragma_cprover_enable_all/main.c

@@ -0,0 +1,92 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+typedef enum ABC
+{
+  A = 0,
+  B = 1,
+  C = 2
+} ABC;
+
+int main()
+{
+#pragma CPROVER check push
+#pragma CPROVER check disable "bounds"
+#pragma CPROVER check disable "pointer"
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "enum-range"
+#pragma CPROVER check disable "signed-overflow"
+#pragma CPROVER check disable "unsigned-overflow"
+#pragma CPROVER check disable "pointer-overflow"
+#pragma CPROVER check disable "float-overflow"
+#pragma CPROVER check disable "conversion"
+#pragma CPROVER check disable "undefined-shift"
+#pragma CPROVER check disable "nan"
+#pragma CPROVER check disable "pointer-primitive"
+  {
+    int N = 10;
+    char *p = malloc(N * sizeof(*p));
+    char *q;
+    char *r;
+    float den;
+    float x;
+    float y;
+    ABC e;
+    bool same;
+    char i;
+    signed int j;
+    same = __CPROVER_same_object(p, q);
+    q = p + 2000000000000;
+    q = r;
+    if(nondet_bool())
+      den = 0.0;
+    else
+      den = 1.0;
+    y = x / den;
+    e = 10;
+    i += 1;
+    j += 1;
+  }
+#pragma CPROVER check push
+#pragma CPROVER check enable "bounds"
+#pragma CPROVER check enable "pointer"
+#pragma CPROVER check enable "div-by-zero"
+#pragma CPROVER check enable "enum-range"
+#pragma CPROVER check enable "signed-overflow"
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "pointer-overflow"
+#pragma CPROVER check enable "float-overflow"
+#pragma CPROVER check enable "conversion"
+#pragma CPROVER check enable "undefined-shift"
+#pragma CPROVER check enable "nan"
+#pragma CPROVER check enable "pointer-primitive"
+  {
+    int N = 10;
+    char *p = malloc(N * sizeof(*p));
+    char *q;
+    char *r;
+    float den;
+    float x;
+    float y;
+    ABC e;
+    bool same;
+    char i;
+    signed int j;
+    same = __CPROVER_same_object(p, q);
+    q = p + 2000000000000;
+    q = r;
+    if(nondet_bool())
+      den = 0.0;
+    else
+      den = 1.0;
+    y = x / den;
+    e = 10;
+    i += 1;
+    j += 1;
+  }
+#pragma CPROVER check pop
+#pragma CPROVER check pop
+  return 0;
+}

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -0,0 +1,27 @@
+CORE broken-smt-backend
+main.c
+--object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check
+^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
+^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000l: FAILURE
+^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in POINTER_OBJECT\(const void \*\)q\): FAILURE
+^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in POINTER_OBJECT\(const void \*\)q\): FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000l: FAILURE
+^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+--
+This test uses all possible named-checks to maximize coverage.

regression/cbmc/pragma_cprover_enable_disable_global_off/main.c

@@ -0,0 +1,42 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(sizeof(*p));
+  char *q;
+
+#pragma CPROVER check push
+#pragma CPROVER check enable "pointer-primitive"
+  // must generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check push
+#pragma CPROVER check disable "pointer-primitive"
+  // must not generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check push
+#pragma CPROVER check enable "pointer-primitive"
+  // must generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check pop
+  // must not generate generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check pop
+  // must generate generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check pop
+  // must not generate generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+  return 0;
+}