Error handling cleanup in solvers/flattening 2 #2932

danpoe · 2018-09-10T15:50:38Z

No description provided.

danpoe · 2018-09-10T15:56:56Z

src/solvers/flattening/boolbv.cpp

@@ -302,7 +312,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
  else if(expr.id()==ID_float_debug1 ||
          expr.id()==ID_float_debug2)
  {
-    assert(expr.operands().size()==2);
+    DATA_INVARIANT(expr.operands().size() == 2, "");


There are no expression types corresponding to ID_float_debug1 and ID_float_debug2 as it seems they have been added quickly for debugging purposes. Should there be actual expression types for these?

I think this can be removed.

danpoe · 2018-09-10T16:05:08Z

src/solvers/flattening/boolbv.cpp

-  if(expr.operands().size()!=2)
-    throw "lambda takes two operands";
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "lambda expression should have two operands");


There currently exists a lambda expression type in a non-public repo. @peterschrammel: Should this be pulled out from there and added to std_expr.h?

That's used in cegis. @pkesseli will remove this as soon as the cegis code has been cleaned up.

I've raised an issue for that as well now: #3039

peterschrammel · 2018-09-10T16:00:40Z

src/solvers/flattening/boolbv.cpp

@@ -126,18 +126,28 @@ const bvt &boolbvt::convert_bv(const exprt &expr)
  // Iterators into hash_maps supposedly stay stable
  // even though we are inserting more elements recursively.

-  cache_result.first->second=convert_bitvector(expr);
+  const bvt &bv = convert_bitvector(expr);
+  CHECK_RETURN(!expected_width || bv.size() == *expected_width);


I think you have to remove this, otherwise the invariant with diagnostics will never be triggered.

There is a CHECK_RETURN_WITH_DIAGNOSTICS, but I'm not sure if CHECK_RETURN is even the right invariant type to use here

peterschrammel · 2018-09-10T16:09:11Z

src/solvers/flattening/boolbv.cpp

@@ -183,8 +183,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)

  if(expr.id()==ID_index)
    return convert_index(to_index_expr(expr));
-  else if(expr.id()==ID_constraint_select_one)


Isn't this used by EBMC?

Ah, I didn't know that. Where can I find the source code of EBMC?

hannes-steffenhagen-diffblue · 2018-09-10T16:26:37Z

src/solvers/flattening/boolbv.cpp

-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "unary plus expressions should have one operand");


@tautschnig Is likely going to suggest to add a to_unary_plus_expr and call it here...

See PR #2931 ;)

AFAIK that has been merged?

src/solvers/flattening/boolbv.cpp

peterschrammel · 2018-09-17T15:22:46Z

src/util/irep_ids.def

@@ -298,7 +298,6 @@ IREP_ID_ONE(predecrement)
 IREP_ID_ONE(integer_bits)
 IREP_ID_ONE(KnR)
 IREP_ID_TWO(C_KnR, #KnR)
-IREP_ID_ONE(constraint_select_one)


This is used in ebmc.

peterschrammel · 2018-09-17T15:26:20Z

src/solvers/flattening/boolbv.cpp

-  if(expr.operands().size()!=2)
-    throw "lambda takes two operands";
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "lambda expression should have two operands");


That's used in cegis. @pkesseli will remove this as soon as the cegis code has been cleaned up.

peterschrammel · 2018-09-17T15:28:52Z

src/solvers/flattening/boolbv.cpp

@@ -302,7 +312,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
  else if(expr.id()==ID_float_debug1 ||
          expr.id()==ID_float_debug2)
  {
-    assert(expr.operands().size()==2);
+    DATA_INVARIANT(expr.operands().size() == 2, "");


I think this can be removed.

tautschnig · 2018-09-18T10:14:48Z

src/solvers/flattening/boolbv.cpp

-      if(to_integer(index_expr.index(), index))
-        throw "literal expects constant index";
+      bool error = to_integer(index_expr.index(), index);
+      CHECK_RETURN(!error);


How about using numeric_cast_v, which would do the error checking?

tautschnig · 2018-09-18T10:16:10Z

src/solvers/flattening/boolbv.cpp

-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "unary plus expressions should have one operand");


AFAIK that has been merged?

tautschnig · 2018-09-18T10:17:47Z

src/solvers/flattening/boolbv.cpp


-    if(size*tmp.size()!=width)
-      throw "convert_lambda: unexpected operand width";
+    std::size_t offset = integer2unsigned(i * tmp.size());


Please replace by numeric_cast_v

allredj

Passed Diffblue compatibility checks (cbmc commit: a721b1b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85286739

allredj

Passed Diffblue compatibility checks (cbmc commit: e8f2e21).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85554847

Files boolbv_constant.cpp, boolbv.cpp

allredj

Passed Diffblue compatibility checks (cbmc commit: ce19636).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85857128

danpoe · 2018-09-28T10:02:34Z

@peterschrammel I think this is ready to be merged now.

danpoe requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners September 10, 2018 15:50

danpoe commented Sep 10, 2018

View reviewed changes

peterschrammel reviewed Sep 10, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Sep 10, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-constant branch from cedaaad to 0c6ed43 Compare September 10, 2018 16:30

hannes-steffenhagen-diffblue approved these changes Sep 12, 2018

View reviewed changes

src/solvers/flattening/boolbv.cpp Show resolved Hide resolved

peterschrammel requested changes Sep 17, 2018

View reviewed changes

peterschrammel assigned danpoe Sep 17, 2018

tautschnig reviewed Sep 18, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-constant branch from 0c6ed43 to a721b1b Compare September 19, 2018 12:05

allredj reviewed Sep 19, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-constant branch 2 times, most recently from b2ae89a to e8f2e21 Compare September 21, 2018 10:24

allredj reviewed Sep 21, 2018

View reviewed changes

danpoe added 2 commits September 25, 2018 12:12

Error handling cleanup in solvers/flattening

18fbc60

Files boolbv_constant.cpp, boolbv.cpp

Remove ID_float_debug1 and ID_float_debug2 expressions

ce19636

danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-constant branch from e8f2e21 to ce19636 Compare September 25, 2018 11:18

allredj reviewed Sep 25, 2018

View reviewed changes

tautschnig assigned peterschrammel Sep 25, 2018

peterschrammel approved these changes Sep 28, 2018

View reviewed changes

peterschrammel removed their assignment Sep 28, 2018

tautschnig approved these changes Sep 28, 2018

View reviewed changes

tautschnig merged commit d37341e into diffblue:develop Sep 28, 2018

danpoe deleted the refactor/error-handling-solvers-flattening-from-boolbv-constant branch June 2, 2020 17:13

Error handling cleanup in solvers/flattening 2 #2932

Error handling cleanup in solvers/flattening 2 #2932

Uh oh!

Conversation

danpoe commented Sep 10, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe commented Sep 28, 2018

Uh oh!

Uh oh!

danpoe commented Sep 10, 2018 •

edited

Loading