Disable unnecessary pointer checks, enable necessary pointer checks in the instrumentation for assigns clause

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -134,19 +134,73 @@ 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.
+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_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;
+}

regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc

@@ -0,0 +1,36 @@
+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$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^\[main.pointer_primitives.\d+\] line 17
+^\[main.pointer_primitives.\d+\] line 28
+^\[main.pointer_primitives.\d+\] line 38
+--

regression/cbmc/pragma_cprover_enable_disable_global_on/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 generate generate checks
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+  return 0;
+}

regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc

@@ -0,0 +1,43 @@
+CORE
+main.c
+--pointer-primitive-check
+^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$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^\[main.pointer_primitives.\d+\] line 17
+^\[main.pointer_primitives.\d+\] line 28
+--