Merge pull request #1281 from tautschnig/interpreter-assert-cleanup

Interpreter: replace assert by invariants

Author: Daniel Kroening

src/goto-programs/interpreter.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <string.h>
 
+#include <util/invariant.h>
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 #include <util/ieee_float.h>
@@ -380,7 +381,9 @@ void interpretert::execute_other()
   const irep_idt &statement=pc->code.get_statement();
   if(statement==ID_expression)
   {
-    assert(pc->code.operands().size()==1);
+    DATA_INVARIANT(
+      pc->code.operands().size()==1,
+      "expression statement expected to have one operand");
     mp_vectort rhs;
     evaluate(pc->code.op0(), rhs);
   }
@@ -409,7 +412,7 @@ void interpretert::execute_other()
 
 void interpretert::execute_decl()
 {
-  assert(pc->code.get_statement()==ID_decl);
+  PRECONDITION(pc->code.get_statement()==ID_decl);
 }
 
 /// retrieves the member at offset
@@ -515,7 +518,7 @@ exprt interpretert::get_value(
   std::size_t offset)
 {
   const typet real_type=ns.follow(type);
-  assert(!rhs.empty());
+  PRECONDITION(!rhs.empty());
 
   if(real_type.id()==ID_struct)
   {
@@ -807,7 +810,6 @@ void interpretert::execute_function_call()
       const code_typet::parametert &a=parameters[i];
       exprt symbol_expr(ID_symbol, a.type());
       symbol_expr.set(ID_identifier, a.get_identifier());
-      assert(i<argument_values.size());
       assign(evaluate_address(symbol_expr), argument_values[i]);
     }
 
@@ -822,8 +824,8 @@ void interpretert::execute_function_call()
     if(it!=function_input_vars.end())
     {
       mp_vectort value;
-      assert(!it->second.empty());
-      assert(!it->second.front().return_assignments.empty());
+      PRECONDITION(!it->second.empty());
+      PRECONDITION(!it->second.front().return_assignments.empty());
       evaluate(it->second.front().return_assignments.back().value, value);
       if(return_value_address>0)
       {
@@ -1013,7 +1015,8 @@ size_t interpretert::get_size(const typet &type)
       // overflow behaviour.
       exprt size_const=from_integer(i[0], size_expr.type());
       mp_integer size_mp;
-      assert(!to_integer(size_const, size_mp));
+      bool ret=to_integer(size_const, size_mp);
+      CHECK_RETURN(!ret);
       return subtype_size*integer2unsigned(size_mp);
     }
     return subtype_size;

src/goto-programs/interpreter_class.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <stack>
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/sparse_vector.h>
 
 #include "goto_functions.h"
@@ -113,7 +114,7 @@ class interpretert:public messaget
     auto lower_bound=inverse_memory_map.lower_bound(address);
     if(lower_bound->first!=address)
     {
-      assert(lower_bound!=inverse_memory_map.begin());
+      CHECK_RETURN(lower_bound!=inverse_memory_map.begin());
       --lower_bound;
     }
     return *lower_bound;
@@ -131,7 +132,7 @@ class interpretert:public messaget
 
   std::size_t base_address_to_alloc_size(std::size_t address) const
   {
-    assert(address_to_offset(address)==0);
+    PRECONDITION(address_to_offset(address)==0);
     auto upper_bound=inverse_memory_map.upper_bound(address);
     std::size_t next_alloc_address=
       upper_bound==inverse_memory_map.end() ?

src/goto-programs/interpreter_evaluate.cpp

@@ -11,11 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "interpreter_class.h"
 
-#include <cassert>
 #include <iostream>
 #include <sstream>
 
 #include <util/ieee_float.h>
+#include <util/invariant.h>
 #include <util/fixedbv.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
@@ -911,7 +911,7 @@ void interpretert::evaluate(
         if(expr.op0().id()==ID_array)
         {
           const auto &ops=expr.op0().operands();
-          assert(read_from_index.is_long());
+          DATA_INVARIANT(read_from_index.is_long(), "index is too large");
           if(read_from_index>=0 && read_from_index<ops.size())
           {
             evaluate(ops[read_from_index.to_long()], dest);
@@ -924,12 +924,14 @@ void interpretert::evaluate(
           // This sort of construct comes from boolbv_get, but doesn't seem
           // to have an exprt yet. Its operands are a list of key-value pairs.
           const auto &ops=expr.op0().operands();
-          assert(ops.size()%2==0);
+          DATA_INVARIANT(
+            ops.size()%2==0,
+            "array-list has odd number of operands");
           for(size_t listidx=0; listidx!=ops.size(); listidx+=2)
           {
             mp_vectort elem_idx;
             evaluate(ops[listidx], elem_idx);
-            assert(elem_idx.size()==1);
+            CHECK_RETURN(elem_idx.size()==1);
             if(elem_idx[0]==read_from_index)
             {
               evaluate(ops[listidx+1], dest);
@@ -1177,7 +1179,7 @@ mp_integer interpretert::evaluate_address(
     if(expr.operands().size()!=1)
       throw "typecast expects one operand";
 
-    assert(expr.type().id()==ID_pointer);
+    PRECONDITION(expr.type().id()==ID_pointer);
 
     return evaluate_address(expr.op0(), fail_quietly);
   }

src/util/sparse_vector.h

@@ -12,9 +12,10 @@ Author: Romain Brenguier
 #ifndef CPROVER_UTIL_SPARSE_VECTOR_H
 #define CPROVER_UTIL_SPARSE_VECTOR_H
 
+#include "invariant.h"
+
 #include <cstdint>
 #include <map>
-#include <assert.h>
 
 template<class T> class sparse_vectort
 {
@@ -29,13 +30,13 @@ template<class T> class sparse_vectort
 
   const T &operator[](uint64_t idx) const
   {
-    assert(idx<_size && "index out of range");
+    INVARIANT(idx<_size, "index out of range");
     return underlying[idx];
   }
 
   T &operator[](uint64_t idx)
   {
-    assert(idx<_size && "index out of range");
+    INVARIANT(idx<_size, "index out of range");
     return underlying[idx];
   }
 
@@ -46,7 +47,7 @@ template<class T> class sparse_vectort
 
   void resize(uint64_t new_size)
   {
-    assert(new_size>=_size && "sparse vector can't be shrunk (yet)");
+    INVARIANT(new_size>=_size, "sparse vector can't be shrunk (yet)");
     _size=new_size;
   }