Merge pull request #911 from martin-cs/feature/internal-invariant

Feature/internal invariant

Author: Daniel Kroening

CODING_STANDARD

@@ -158,6 +158,9 @@ C++ features:
 - Use the auto keyword if and only if one of the following
   - The type is explictly repeated on the RHS (e.g. a constructor call)
   - Adding the type will increase confusion (e.g. iterators, function pointers)
+- Avoid assert, if the condition is an actual invariant, use INVARIANT,
+  PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT.
+  If there are possible reasons why it might fail, throw an exception.
 
 Architecture-specific code:
 - Avoid if possible.

regression/cbmc/invariant-failure/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/cbmc/invariant-failure/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--test-invariant-failure
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/cpp-linter/assert/main.cpp

@@ -0,0 +1,10 @@
+// Author: Martin Brain, [email protected]
+
+#include <cassert>
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  assert(0);
+  return 0;
+}

regression/cpp-linter/assert/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.cpp
+
+^main\.cpp:8:  assert is deprecated, use INVARIANT instead  \[build/deprecated\] \[4\]
+^Total errors found: 1$
+^SIGNAL=0$

regression/test.pl

@@ -35,7 +35,6 @@ ($$$$$)
   print LOG "  Core: $dumped_core\n";
 
   if($signal_num != 0) {
-    $failed = 1;
     print "Killed by signal $signal_num";
     if($dumped_core) {
       print " (code dumped)";

scripts/cpplint.py

@@ -4629,6 +4629,27 @@ def CheckAltTokens(filename, clean_lines, linenum, error):
               _ALT_TOKEN_REPLACEMENT[match.group(1)], match.group(1)))
 
 
+def CheckAssert(filename, clean_lines, linenum, error):
+  """Check for uses of assert.
+
+  Args:
+    filename: The name of the current file.
+    clean_lines: A CleansedLines instance containing the file.
+    linenum: The number of the line to check.
+    error: The function to call with any errors found.
+  """
+  line = clean_lines.elided[linenum]
+  match = Match(r'.*\s+assert\(.*\).*', line)
+  if match:
+    if Match(r'.*\s+assert\((0|false)\).*', line):
+      error(filename, linenum, 'build/deprecated', 4,
+            'assert is deprecated, use UNREACHABLE instead')
+    else:
+      error(filename, linenum, 'build/deprecated', 4,
+            'assert is deprecated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead')
+
+
+
 def GetLineWidth(line):
   """Determines the width of the line in column positions.
 
@@ -4853,6 +4874,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state,
   CheckSpacingForFunctionCall(filename, clean_lines, linenum, error)
   CheckCheck(filename, clean_lines, linenum, error)
   CheckAltTokens(filename, clean_lines, linenum, error)
+  CheckAssert(filename, clean_lines, linenum, error)
   classinfo = nesting_state.InnermostClass()
   if classinfo:
     CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error)

src/cbmc/cbmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/language.h>
 #include <util/unicode.h>
 #include <util/memory_info.h>
+#include <util/invariant.h>
 
 #include <ansi-c/c_preprocess.h>
 
@@ -104,6 +105,27 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(1); // should contemplate EX_USAGE from sysexits.h
   }
 
+  // Test only; do not use for input validation
+  if(cmdline.isset("test-invariant-failure"))
+  {
+    // Have to catch this as the default handling of uncaught exceptions
+    // on windows appears to be silent termination.
+    try
+    {
+      INVARIANT(0, "Test invariant failure");
+    }
+    catch (const invariant_failedt &e)
+    {
+      std::cerr << e.what();
+      exit(0); // should contemplate EX_OK from sysexits.h
+    }
+    catch (...)
+    {
+      error() << "Unexpected exception type\n";
+    }
+    exit(1);
+  }
+
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 

src/cbmc/cbmc_parse_options.h

@@ -63,6 +63,7 @@ class optionst;
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
+  "(test-invariant-failure)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:

src/solvers/smt2/smt2_conv.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/base_type.h>
 #include <util/string2int.h>
+#include <util/invariant.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -34,7 +35,6 @@ Author: Daniel Kroening, [email protected]
 
 // Mark different kinds of error condition
 // General
-#define UNREACHABLE throw "Supposidly unreachable location reached"
 #define PARSERERROR(S) throw S
 
 // Error checking the expression type
@@ -45,7 +45,7 @@ Author: Daniel Kroening, [email protected]
 #define UNEXPECTEDCASE(S) throw "Unexpected case: " S
 
 // General todos
-#define TODO(S) throw "TODO: " S
+#define SMT2_TODO(S) throw "TODO: " S
 
 void smt2_convt::print_assignment(std::ostream &out) const
 {
@@ -952,7 +952,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("bitnot for vectors");
+        SMT2_TODO("bitnot for vectors");
     }
     else
     {
@@ -1017,7 +1017,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("unary minus for vector");
+        SMT2_TODO("unary minus for vector");
     }
     else
     {
@@ -1363,7 +1363,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     assert(expr.operands().size()==1);
 
     out << "false"; // TODO
-    TODO("pointer_object_has_type not implemented");
+    SMT2_TODO("pointer_object_has_type not implemented");
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -1432,7 +1432,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       convert_expr(tmp);
       out << ")) bin1)"; // bvlshr, extract, =
       #endif
-      TODO("smt2: extractbits with non-constant index");
+      SMT2_TODO("smt2: extractbits with non-constant index");
     }
   }
   else if(expr.id()==ID_replication)
@@ -1944,7 +1944,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
           // This conversion is non-trivial as it requires creating a
           // new bit-vector variable and then asserting that it converts
           // to the required floating-point number.
-          TODO("bit-wise floatbv to bv");
+          SMT2_TODO("bit-wise floatbv to bv");
         }
         else
         {
@@ -2017,7 +2017,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         out << "(_ bv" << i << " " << to_width << ")";
       }
       else
-        TODO("can't convert non-constant integer to bitvector");
+        SMT2_TODO("can't convert non-constant integer to bitvector");
     }
     else if(src_type.id()==ID_struct) // flatten a struct to a bit-vector
     {
@@ -2207,7 +2207,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
   }
   else if(dest_type.id()==ID_range)
   {
-    TODO("range typecast");
+    SMT2_TODO("range typecast");
   }
   else if(dest_type.id()==ID_floatbv)
   {
@@ -3031,11 +3031,11 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr)
     }
     else if(type.id()==ID_complex)
     {
-      TODO("+ for floatbv complex");
+      SMT2_TODO("+ for floatbv complex");
     }
     else if(type.id()==ID_vector)
     {
-      TODO("+ for floatbv vector");
+      SMT2_TODO("+ for floatbv vector");
     }
     else
       UNEXPECTEDCASE("unsupported type for +: "+type.id_string());
@@ -3093,7 +3093,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
   }
   else if(expr.type().id()==ID_pointer)
   {
-    TODO("pointer subtraction");
+    SMT2_TODO("pointer subtraction");
   }
   else if(expr.type().id()==ID_vector)
   {
@@ -3527,7 +3527,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
     typecast_exprt index_tc(index, expr_type);
 
     // TODO: SMT2-ify
-    TODO("SMT2-ify");
+    SMT2_TODO("SMT2-ify");
     out << "(bvor ";
     out << "(band ";
 
@@ -3565,7 +3565,7 @@ void smt2_convt::convert_update(const exprt &expr)
 {
   assert(expr.operands().size()==3);
 
-  TODO("smt2_convt::convert_update to be implemented");
+  SMT2_TODO("smt2_convt::convert_update to be implemented");
 }
 
 void smt2_convt::convert_index(const index_exprt &expr)
@@ -3651,7 +3651,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
       mp_integer index_int;
       if(to_integer(expr.index(), index_int))
       {
-        TODO("non-constant index on vectors");
+        SMT2_TODO("non-constant index on vectors");
       }
       else
       {
@@ -3662,7 +3662,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
     }
     else
     {
-      TODO("index on vectors");
+      SMT2_TODO("index on vectors");
     }
   }
   else

src/util/Makefile

@@ -24,6 +24,7 @@ SRC = arith_tools.cpp \
       guard.cpp \
       identifier.cpp \
       ieee_float.cpp \
+      invariant.cpp \
       irep.cpp \
       irep_hash.cpp \
       irep_hash_container.cpp \

src/util/expr.cpp

@@ -9,14 +9,13 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Expression Representation
 
-#include <cassert>
-
 #include <stack>
 
 #include "string2int.h"
 #include "mp_arith.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
+#include "invariant.h"
 #include "expr.h"
 #include "rational.h"
 #include "rational_tools.h"
@@ -203,15 +202,16 @@ void exprt::negate()
       else
       {
         make_nil();
-        assert(false);
+        UNREACHABLE;
       }
     }
     else
     {
       if(id()==ID_unary_minus)
       {
         exprt tmp;
-        assert(operands().size()==1);
+        DATA_INVARIANT(operands().size()==1,
+                       "Unary minus must have one operand");
         tmp.swap(op0());
         swap(tmp);
       }
@@ -245,7 +245,7 @@ bool exprt::is_zero() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_zero();
     }
     else if(type_id==ID_unsignedbv ||
@@ -291,7 +291,7 @@ bool exprt::is_one() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_one();
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)

src/util/expr_util.cpp

@@ -36,14 +36,14 @@ exprt make_binary(const exprt &expr)
   const typet &type=expr.type();
 
   exprt previous=operands.front();
-  assert(previous.type()==type);
+  PRECONDITION(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
-    assert(it->type()==type);
+    PRECONDITION(it->type()==type);
 
     exprt tmp=expr;
     tmp.operands().clear();
@@ -59,7 +59,7 @@ exprt make_binary(const exprt &expr)
 with_exprt make_with_expr(const update_exprt &src)
 {
   const exprt::operandst &designator=src.designator();
-  assert(!designator.empty());
+  PRECONDITION(!designator.empty());
 
   with_exprt result;
   exprt *dest=&result;
@@ -78,7 +78,7 @@ with_exprt make_with_expr(const update_exprt &src)
       //  to_member_designator(*it).get_component_name();
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     *dest=tmp;
     dest=&to_with_expr(*dest).new_value();
@@ -108,7 +108,7 @@ exprt is_not_zero(
     src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
 
   exprt zero=from_integer(0, src_type);
-  assert(zero.is_not_nil());
+  CHECK_RETURN(zero.is_not_nil());
 
   binary_exprt comparison(src, id, zero, bool_typet());
   comparison.add_source_location()=src.source_location();
@@ -142,8 +142,8 @@ bool has_subexpr(const exprt &src, const irep_idt &id)
 
 if_exprt lift_if(const exprt &src, std::size_t operand_number)
 {
-  assert(operand_number<src.operands().size());
-  assert(src.operands()[operand_number].id()==ID_if);
+  PRECONDITION(operand_number<src.operands().size());
+  PRECONDITION(src.operands()[operand_number].id()==ID_if);
 
   const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
   const exprt true_case=if_expr.true_case();