Refactor/update refinement solver asserts

src/solvers/refinement/bv_refinement_loop.cpp

@@ -21,9 +21,9 @@ bv_refinementt::bv_refinementt(
   do_arithmetic_refinement(true)
 {
   // check features we need
-  assert(prop.has_set_assumptions());
-  assert(prop.has_set_to());
-  assert(prop.has_is_in_conflict());
+  PRECONDITION(prop.has_set_assumptions());
+  PRECONDITION(prop.has_set_to());
+  PRECONDITION(prop.has_is_in_conflict());
 }
 
 bv_refinementt::~bv_refinementt()

src/solvers/refinement/refine_arithmetic.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/floatbv/float_utils.h>
 
 #include "bv_refinement.h"
@@ -62,7 +63,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
 
   const typet &type=ns.follow(expr.type());
 
-  assert(operands.size()>=2);
+  PRECONDITION(operands.size()>=2);
 
   if(operands.size()>2)
     return convert_mult(make_binary(expr)); // make binary
@@ -106,7 +107,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
   // we catch any division
   // unless it's integer division by a constant
 
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
     return SUB::convert_div(expr);
@@ -124,7 +125,7 @@ bvt bv_refinementt::convert_mod(const mod_exprt &expr)
   // we catch any mod
   // unless it's integer + constant
 
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
     return SUB::convert_mod(expr);
@@ -152,7 +153,7 @@ void bv_refinementt::get_values(approximationt &a)
     a.op2_value=get_value(a.op2_bv);
   }
   else
-    assert(0);
+    UNREACHABLE;
 
   a.result_value=get_value(a.result_bv);
 }
@@ -170,8 +171,10 @@ void bv_refinementt::check_SAT(approximationt &a)
 
   if(type.id()==ID_floatbv)
   {
-    // these are all trinary
-    assert(a.expr.operands().size()==3);
+    // these are all ternary
+    INVARIANT(
+      a.expr.operands().size()==3,
+      string_refinement_invariantt("all floatbv typed exprs are ternary"));
 
     if(a.over_state==MAX_STATE)
       return;
@@ -203,7 +206,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     else if(a.expr.id()==ID_floatbv_div)
       result/=o1;
     else
-      assert(false);
+      UNREACHABLE;
 
     if(result.pack()==a.result_value) // ok
       return;
@@ -271,17 +274,19 @@ void bv_refinementt::check_SAT(approximationt &a)
       else if(a.expr.id()==ID_floatbv_div)
         r=float_utils.div(op0, op1);
       else
-        assert(0);
+        UNREACHABLE;
 
-      assert(r.size()==res.size());
+      CHECK_RETURN(r.size()==res.size());
       bv_utils.set_equal(r, res);
     }
   }
   else if(type.id()==ID_signedbv ||
           type.id()==ID_unsignedbv)
   {
     // these are all binary
-    assert(a.expr.operands().size()==2);
+    INVARIANT(
+      a.expr.operands().size()==2,
+      string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
 
     // already full interpretation?
     if(a.over_state>0)
@@ -305,7 +310,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     else if(a.expr.id()==ID_mod)
       o0%=o1;
     else
-      assert(false);
+      UNREACHABLE;
 
     if(o0.pack()==a.result_value) // ok
       return;
@@ -339,21 +344,21 @@ void bv_refinementt::check_SAT(approximationt &a)
             bv_utilst::representationt::UNSIGNED);
       }
       else
-        assert(0);
+        UNREACHABLE;
 
       bv_utils.set_equal(r, a.result_bv);
     }
     else
-      assert(0);
+      UNREACHABLE;
   }
   else if(type.id()==ID_fixedbv)
   {
     // TODO: not implemented
-    assert(0);
+    TODO;
   }
   else
   {
-    assert(0);
+    UNREACHABLE;
   }
 
   status() << "Found spurious `" << a.as_string()
@@ -375,7 +380,7 @@ void bv_refinementt::check_UNSAT(approximationt &a)
   status() << "Found assumption for `" << a.as_string()
            << "' in proof (state " << a.under_state << ")" << eom;
 
-  assert(!a.under_assumptions.empty());
+  PRECONDITION(!a.under_assumptions.empty());
 
   a.under_assumptions.clear();
 
@@ -486,7 +491,7 @@ bv_refinementt::add_approximation(
   approximationt &a=approximations.back(); // stable!
 
   std::size_t width=boolbv_width(expr.type());
-  assert(width!=0);
+  PRECONDITION(width!=0);
 
   a.expr=expr;
   a.result_bv=prop.new_variables(width);
@@ -515,7 +520,7 @@ bv_refinementt::add_approximation(
     set_frozen(a.op2_bv);
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   bv=a.result_bv;
 

src/solvers/refinement/refine_arrays.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/find_symbols.h>
 
 #include "bv_refinement.h"
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/sat/satcheck.h>
 
 /// generate array constraints
@@ -55,7 +56,9 @@ void bv_refinementt::arrays_overapproximated()
     if(current.id()==ID_implies)
     {
       implies_exprt imp=to_implies_expr(current);
-      assert(imp.operands().size()==2);
+      DATA_INVARIANT(
+        imp.operands().size()==2,
+        string_refinement_invariantt("implies must have two operands"));
       exprt implies_simplified=get(imp.op0());
       if(implies_simplified==false_exprt())
       {
@@ -67,7 +70,9 @@ void bv_refinementt::arrays_overapproximated()
     if(current.id()==ID_or)
     {
       or_exprt orexp=to_or_expr(current);
-      assert(orexp.operands().size()==2);
+      INVARIANT(
+        orexp.operands().size()==2,
+        string_refinement_invariantt("only treats the case of a binary or"));
       exprt o1=get(orexp.op0());
       exprt o2=get(orexp.op1());
       if(o1==true_exprt() || o2 == true_exprt())
@@ -91,7 +96,13 @@ void bv_refinementt::arrays_overapproximated()
       lazy_array_constraints.erase(it++);
       break;
     default:
-      assert(false);
+      error() << "error in array over approximation check" << eom;
+      INVARIANT(
+        false,
+        string_refinement_invariantt("error in array over approximation "
+          "check"));
+      // Placeholder to tell the compiler we bail
+      throw 0;
     }
   }
 

src/solvers/refinement/string_constraint.h

@@ -22,6 +22,7 @@ Author: Romain Brenguier, [email protected]
 
 #include <langapi/language_ui.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>
 
 class string_constraintt: public exprt
@@ -103,13 +104,13 @@ class string_constraintt: public exprt
 
 extern inline const string_constraintt &to_string_constraint(const exprt &expr)
 {
-  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
+  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
   return static_cast<const string_constraintt &>(expr);
 }
 
 extern inline string_constraintt &to_string_constraint(exprt &expr)
 {
-  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
+  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
   return static_cast<string_constraintt &>(expr);
 }
 
@@ -173,16 +174,22 @@ class string_not_contains_constraintt: public exprt
 inline const string_not_contains_constraintt
 &to_string_not_contains_constraint(const exprt &expr)
 {
-  assert(expr.id()==ID_string_not_contains_constraint);
-  assert(expr.operands().size()==7);
+  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size()==7,
+    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
+      "operands"));
   return static_cast<const string_not_contains_constraintt &>(expr);
 }
 
 inline string_not_contains_constraintt
 &to_string_not_contains_constraint(exprt &expr)
 {
-  assert(expr.id()==ID_string_not_contains_constraint);
-  assert(expr.operands().size()==7);
+  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size()==7,
+    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
+      "operands"));
   return static_cast<string_not_contains_constraintt &>(expr);
 }
 

src/solvers/refinement/string_constraint_generator.h

@@ -317,7 +317,7 @@ class string_constraint_generatort
     const function_application_exprt &expr, size_t nb)
   {
     const function_application_exprt::argumentst &args=expr.arguments();
-    assert(args.size()==nb);
+    PRECONDITION(args.size()==nb);
     return args;
   }
 

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -30,7 +30,7 @@ string_exprt string_constraint_generatort::add_axioms_for_code_point(
 {
   string_exprt res=fresh_string(ref_type);
   const typet &type=code_point.type();
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
 
   // We add axioms:
   // a1 : code_point<0x010000 => |res|=1
@@ -126,7 +126,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
   const function_application_exprt &f)
 {
   typet return_type=f.type();
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
   string_exprt str=get_string_expr(args(f, 2)[0]);
   const exprt &pos=args(f, 2)[1];
 
@@ -155,9 +155,9 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==2);
+  PRECONDITION(args.size()==2);
   typet return_type=f.type();
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
   symbol_exprt result=fresh_symbol("char", return_type);
   string_exprt str=get_string_expr(args[0]);
 

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -22,7 +22,7 @@ Author: Romain Brenguier, [email protected]
 exprt string_constraint_generatort::add_axioms_for_equals(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
   symbol_exprt eq=fresh_boolean("equal");
   typecast_exprt tc_eq(eq, f.type());
 
@@ -98,7 +98,7 @@ exprt string_constraint_generatort::character_equals_ignore_case(
 exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
 
   symbol_exprt eq=fresh_boolean("equal_ignore_case");
   typecast_exprt tc_eq(eq, f.type());
@@ -207,7 +207,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   //       (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|)
   // a4 : forall i'<x. res!=0 => s1[i]=s2[i]
 
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
 
   equal_exprt res_null=equal_exprt(res, from_integer(0, return_type));
   implies_exprt a1(res_null, s1.axiom_for_has_same_length_as(s2));

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -54,8 +54,8 @@ string_exprt string_constraint_generatort::add_axioms_for_constant(
 string_exprt string_constraint_generatort::add_axioms_for_empty_string(
   const function_application_exprt &f)
 {
-  assert(f.arguments().empty());
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(f.arguments().empty());
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   const refined_string_typet &ref_type=to_refined_string_type(f.type());
   exprt size=from_integer(0, ref_type.get_index_type());
   const array_typet &content_type=ref_type.get_content_type();
@@ -74,7 +74,7 @@ string_exprt string_constraint_generatort::add_axioms_from_literal(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==1); // Bad args to string literal?
+  PRECONDITION(args.size()==1); // Bad args to string literal?
 
   const exprt &arg=args[0];
   irep_idt sval=to_constant_expr(arg).get_value();