CAR inclusion checking optimisation:

- Readable names for instrumentation variables
- Use pointer offsets in CAR bounds checking instead of whole pointers
- Disable pointer, pointer-overflow and pointer-primitive checks on CAR inclusion checks
- Enable pointer-overflow checks on CAR upperbound computation

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -134,21 +134,64 @@ 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"
+  x = x + 1; // immediately follows the pragma, unsigned overflow check apply here
+#pragma CPROVER check pop
+  x = x + 2; // unsigned overflow checks do not apply here
+```
+
+```
+unsigned foo(unsigned x)
+{
+#pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "signed-overflow"
+  x = x + 1; // unsigned and signed overflow check apply here
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+  x = x + 2; // only signed overflow check apply here
+#pragma CPROVER check pop
+  x = x + 3; // unsigned and signed overflow check apply here
+#pragma CPROVER check pop
+  x = x + 2; // unsigned overflow checks do not apply here
+```
+
 ```
 unsigned foo(unsigned x)
 {
 #pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "signed-overflow"
+  x = x + 1; // unsigned and signed overflow check apply here
+#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 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
 
 Please note that `--nan-check` flag is adding not-a-number checks only for

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,
+    log.get_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,
+    log.get_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, log.get_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,16 @@
+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];
+  // pop all annotations
+#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,24 @@
+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);
+  // pop all annotations
+#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 
+--