Merge pull request #5845 from tautschnig/keep-redundant-checks

goto_checkt: keep same-assertion for different expressions

Author: tautschnig

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 14 failed
+\*\* 1 of \d+ failed
 --
 ^warning: ignoring
 --

regression/cbmc/Undefined_Shift1/test.desc

@@ -4,11 +4,12 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] line 4 shift operand is negative in .*: SUCCESS$
+^\[.*\] line 5 shift operand is negative in .*: SUCCESS$
 ^\[.*\] line 7 shift distance too large in .*: FAILURE$
 ^\[.*\] line 15 shift distance is negative in .*: FAILURE$
 ^\[.*\] line 15 shift distance too large in .*: SUCCESS$
 ^\[.*\] line 20 shift operand is negative in .*: FAILURE$
-^\*\* 3 of 5 failed
+^\*\* 3 of 6 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/bounds_check2/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int A[2];
+  int x = A[1];
+}

regression/cbmc/bounds_check2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--bounds-check --retain-trivial-checks
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^\[main.array_bounds.1\] line 4 array 'A' lower bound in A\[\(signed (long (long )?)?int\)1\]: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Generated 0 VCC\(s\), 0 remaining after simplification$

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -0,0 +1,16 @@
+CORE broken-smt-backend
+main.c
+--pointer-overflow-check --no-simplify
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed
+--
+Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.

regression/cbmc/pointer-overflow3/test.desc

@@ -1,6 +1,6 @@
-CORE broken-smt-backend
+CORE
 main.c
---pointer-overflow-check --no-simplify
+--pointer-overflow-check
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
@@ -12,5 +12,3 @@ main.c
 --
 ^warning: ignoring
 Invariant check failed
---
-Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.

src/analyses/goto_check.cpp

@@ -70,7 +70,7 @@ class goto_checkt
       _options.get_bool_option("float-overflow-check");
     enable_simplify=_options.get_bool_option("simplify");
     enable_nan_check=_options.get_bool_option("nan-check");
-    retain_trivial=_options.get_bool_option("retain-trivial");
+    retain_trivial = _options.get_bool_option("retain-trivial-checks");
     enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
     enable_assertions=_options.get_bool_option("assertions");
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
@@ -242,7 +242,7 @@ class goto_checkt
     const guardt &guard);
 
   goto_programt new_code;
-  typedef std::set<exprt> assertionst;
+  typedef std::set<std::pair<exprt, exprt>> assertionst;
   assertionst assertions;
 
   /// Remove all assertions containing the symbol in \p lhs as well as all
@@ -333,8 +333,12 @@ void goto_checkt::invalidate(const exprt &lhs)
 
     for(auto it = assertions.begin(); it != assertions.end();)
     {
-      if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
+      if(
+        has_symbol(it->second, find_symbols_set) ||
+        has_subexpr(it->second, ID_dereference))
+      {
         it = assertions.erase(it);
+      }
       else
         ++it;
     }
@@ -1545,7 +1549,7 @@ void goto_checkt::add_guarded_property(
       ? std::move(simplified_expr)
       : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
 
-  if(assertions.insert(guarded_expr).second)
+  if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
   {
     auto t = new_code.add(
       enable_assert_to_assume ? goto_programt::make_assumption(

src/analyses/goto_check.h

@@ -39,7 +39,8 @@ void goto_check(
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
-  "(pointer-primitive-check)"
+  "(pointer-primitive-check)"                                                  \
+  "(retain-trivial-checks)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -54,9 +55,10 @@ void goto_check(
   " --undefined-shift-check      check shift greater than bit-width\n" \
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
-  " --no-built-in-assertions     ignore assertions in built-in library\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
-  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */
+  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
+  " --no-built-in-assertions     ignore assertions in built-in library\n" \
+  " --retain-trivial-checks      include checks that are trivially true\n" \
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -72,7 +74,10 @@ void goto_check(
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
   options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */
+  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("retain-trivial-checks", \
+                     cmdline.isset("retain-trivial-checks")); \
+  (void)0
 // clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H