Cprover enum is in range #5808

TGWDB · 2021-02-09T10:35:06Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

regression/cbmc/enum_is_in_range/enum_test3.c

peterschrammel · 2021-02-09T11:05:27Z

src/ansi-c/c_typecheck_expr.cpp

+                    << expr.arguments().size() << " were provided";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+    // Replace expr with giant boolean that checks all the values


I don't think the translation into a condition should be done here, but rather later as a pass on the goto program.

@peterschrammel Could you elaborate where exactly you'd like this to happen?

I think it would fit well into the goto_check pass. Then you can even reuse the logic for generating the conditons that is already there.

@peterschrammel This should work without enum-range-check being enabled as it's more generally useful though. Or do you mean just have it as something that happens during goto check? Because I feel that'd be slightly confusing as it's not a check.

@peterschrammel It would be nice to be able to reuse the same check logic for both kinds of check. However we don't think it fits into goto_check because it is replacing an existing expression rather than adding new checks. Would you be OK with us adding it in src/goto-programs/builtin_functions.cpp, function goto_convertt::do_function_call_symbol? This seems to be the place where the other built in functions are implemented / replaced.

builtin_functions is certainly a better place than c_typecheck_expr.

@peterschrammel This is addressed now.

codecov · 2021-02-09T11:17:28Z

Codecov Report

Merging #5808 (baab734) into develop (4cc9611) will increase coverage by 4.05%.
The diff coverage is 97.72%.

@@             Coverage Diff             @@
##           develop    #5808      +/-   ##
===========================================
+ Coverage    69.54%   73.60%   +4.05%     
===========================================
  Files         1243     1491     +248     
  Lines       100701   179270   +78569     
===========================================
+ Hits         70037   131958   +61921     
- Misses       30664    47312   +16648

Flag	Coverage Δ
cproversmt2	`43.35% <62.96%> (+0.02%)`	⬆️
regression	`66.46% <96.29%> (+0.01%)`	⬆️
unit	`32.24% <7.40%> (-0.01%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/goto-programs/goto_convert_class.h	`87.50% <ø> (-4.17%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`80.60% <95.00%> (+4.68%)`	⬆️
src/goto-programs/builtin_functions.cpp	`56.06% <100.00%> (+4.64%)`	⬆️
src/cpp/cpp_storage_spec.cpp	`65.00% <0.00%> (-35.00%)`	⬇️
src/solvers/strings/array_pool.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/util/mathematical_types.h	`78.94% <0.00%> (-21.06%)`	⬇️
src/util/mathematical_expr.cpp	`82.35% <0.00%> (-17.65%)`	⬇️
src/goto-programs/name_mangler.cpp	`50.00% <0.00%> (-14.71%)`	⬇️
src/solvers/flattening/boolbv_union.cpp	`69.69% <0.00%> (-14.52%)`	⬇️
src/cpp/cpp_typecheck_static_assert.cpp	`46.15% <0.00%> (-13.85%)`	⬇️
... and 1281 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 4cc9611...baab734. Read the comment docs.

tautschnig · 2021-02-09T12:07:58Z

src/ansi-c/c_typecheck_expr.cpp

+                    << expr.arguments().size() << " were provided";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+    // Replace expr with giant boolean that checks all the values


src/ansi-c/c_typecheck_expr.cpp

tautschnig

I think this is great work, and would just ask for

@peterschrammel's comment to be addressed and
the commit pile to be cleaned up.

tautschnig · 2021-02-09T18:53:50Z

src/ansi-c/c_typecheck_expr.cpp

+      std::vector<exprt> disjuncts;
+      for(const auto &enum_value : enum_values)
+      {
+        const constant_exprt val{enum_value.get_value(), *c_enum_tag_type};


Rather than making this const I'd even opt to std::move it in the construction of the equal_exprt below.

tautschnig · 2021-02-09T18:54:57Z

src/ansi-c/c_typecheck_expr.cpp

+      error().source_location = expr.source_location();
+      error() << identifier << " expects one argument, "
+              << expr.arguments().size() << " were provided" << eom;
+      throw 0;


Is it worth adding a test also covering this error condition? You've got a bunch of tests already, adding one more would help tick another box :-)

src/ansi-c/c_typecheck_expr.cpp

hannes-steffenhagen-diffblue · 2021-02-09T10:59:17Z

doc/cprover-manual/api.md

+
+The function **\_\_CPROVER\_enum\_is\_in\_range** returns true
+if their one argument (an `enum`) is one of the defined values for
+the enumeration. For example


I would probably rewrite that as

in this example, __CPROVER_enum_is_in_range(ev1) would return true, while in that example...

Because otherwise we have a block of code and it's a bit unclear 'what' returns true/false. Otherwise, maybe just say something like

In this example the assertion will pass

while in this example it will fail.

Improved this.

hannes-steffenhagen-diffblue

I think the code is mostly OK, withholding approval for commit / error handling cleanup.

src/ansi-c/c_typecheck_expr.cpp

hannes-steffenhagen-diffblue · 2021-02-10T10:20:54Z

src/ansi-c/c_typecheck_expr.cpp

+                    << expr.arguments().size() << " were provided";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+    // Replace expr with giant boolean that checks all the values


@peterschrammel Could you elaborate where exactly you'd like this to happen?

hannes-steffenhagen-diffblue · 2021-02-10T10:21:49Z

src/ansi-c/c_typecheck_expr.cpp

+    {
+      // Can't enum range check a non-enum
+      error().source_location = expr.source_location();
+      error() << identifier << " expects enum argument type" << eom;


Again, would be better if the error message also stated what we got instead of what it expected.

hannes-steffenhagen-diffblue · 2021-02-10T10:52:53Z

@tautschnig We seem to be disagreeing on the error handling. To avoid us giving conflicting advice in the future, we should probably come to an agreement on what we do with error handling. My view was that we should avoid adding additional unstructured exceptions/remove unstructured exceptions when we come across them. Do you disagree with that on principle, or do you only have a problem with it in this particular case?

tautschnig · 2021-02-10T16:20:03Z

@tautschnig We seem to be disagreeing on the error handling. To avoid us giving conflicting advice in the future, we should probably come to an agreement on what we do with error handling. My view was that we should avoid adding additional unstructured exceptions/remove unstructured exceptions when we come across them. Do you disagree with that on principle, or do you only have a problem with it in this particular case?

My apologies if I caused confusion here. I'm all for structured exceptions in general, except the C front-end does things differently (but is consistent in doing it in such a way). I'd thus ask for this to remain consistent, not ruling out that we change this at a later point - but then we should make a wholesale change.

Edit: to be very explicit: my comment is just about this particular case.

tautschnig · 2021-02-10T16:48:29Z

To also explain at a more technical level why the C front-end (rightly) does throw 0, though only for handling type checking errors that can be triggered by syntactically valid input files: the message handler will ensure that the error message is formatted in a style matching the compiler (GCC or Visual Studio). That throw 0 will be caught by https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/ansi_c_typecheck.cpp#L53. If we were to use structured exceptions here, we would need to make sure the behaviour of printing a well-formatted message is preserved.

peterschrammel · 2021-02-15T16:30:31Z

src/goto-programs/builtin_functions.cpp

+  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
+  const c_enum_typet::memberst enum_values = c_enum_type.members();
+
+  std::vector<exprt> disjuncts;


⛏️

Suggested change

std::vector<exprt> disjuncts;

exprt::operandst disjuncts;

peterschrammel · 2021-02-15T16:31:52Z

src/goto-programs/goto_convert_class.h

@@ -589,6 +589,11 @@ class goto_convertt:public messaget
  exprt get_constant(const exprt &expr);

  // some built-in functions
+  void do_enum_is_in_range(


⛏️ Some docs would be appreciated.

TGWDB · 2021-02-15T18:10:36Z

@hannes-steffenhagen-diffblue Can you please (re)review this PR now it's been redone taking into account above comments (and also tidied up).

tautschnig

I would ask for the changes I've suggested to be addressed, but no longer have blocking concerns. Also, please add Fixes: #5473 to one of the commit messages.

tautschnig · 2021-02-16T13:46:17Z

src/goto-programs/builtin_functions.cpp

+  const auto disjunction = ::disjunction(disjuncts);
+
+  code_assignt assignment(lhs, disjunction);


Nit picking: I'd do code_assignt assignment{lhs, disjunction(disjuncts)}; to avoid constructing (and then deleting) a temporary.

tautschnig · 2021-02-16T13:46:56Z

src/goto-programs/goto_convert_class.h

+  ///
+  /// Note that the check for the range of values is done by creating a
+  /// disjunction comparing the expression with each possible valid value.
+  /// \param lhs The destination for the generated assignment.


Nit picking: I believe the coding guidelines suggest to use a colon after the parameter's name.

tautschnig · 2021-02-16T13:48:12Z

regression/cbmc/enum_is_in_range/enum_test10.desc

+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_num_is_in_range


s/_num_/_enum_/

tautschnig · 2021-02-16T13:48:44Z

regression/cbmc/enum_is_in_range/enum_test12.desc

+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_num_is_in_range


s/_num_/_enum_

tautschnig · 2021-02-16T13:50:00Z

regression/cbmc/enum_is_in_range/enum_test10.desc

+
+^EXIT=6$
+^SIGNAL=0$
+^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$


This test ought to live in the regression/ansi-c/ folder, I'd say. This will require modifying EXIT=6 to EXIT=(1|64)

tautschnig · 2021-02-16T13:50:19Z

regression/cbmc/enum_is_in_range/enum_test12.desc

+
+^EXIT=6$
+^SIGNAL=0$
+^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$


Should also go in regression/ansi-c/.

This adds a new builtin function that allows user to explicitly check that an enum has a valid value (and also this function in an assert).

Adds regression tests for enum_is_in_range to test positive, negative and error outcomes on both named and typedef'd enumerations.

Adds documentation of how to use the CPROVER_enum_is_in_range function to explain to a user how to use this function.

regression/ansi-c/enum_is_in_range/enum_test10.desc

TGWDB requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners February 9, 2021 10:35

TGWDB mentioned this pull request Feb 9, 2021

Cprover should have an __enum_in_range primitive #5473

Closed

peterschrammel reviewed Feb 9, 2021

View reviewed changes

tautschnig reviewed Feb 9, 2021

View reviewed changes

hannes-steffenhagen-diffblue reviewed Feb 10, 2021

View reviewed changes

TGWDB force-pushed the CPROVER-enum-is-in-range branch from 1f8f445 to 8412bdf Compare February 15, 2021 16:24

peterschrammel approved these changes Feb 15, 2021

View reviewed changes

TGWDB force-pushed the CPROVER-enum-is-in-range branch from 64124d7 to 955fd76 Compare February 15, 2021 18:09

tautschnig approved these changes Feb 16, 2021

View reviewed changes

tautschnig assigned TGWDB Feb 16, 2021

Implement enum_is_in_range builtin function

a0f1236

This adds a new builtin function that allows user to explicitly check that an enum has a valid value (and also this function in an assert).

TGWDB force-pushed the CPROVER-enum-is-in-range branch from 955fd76 to b953457 Compare February 17, 2021 14:22

TGWDB added 2 commits February 17, 2021 14:49

Add regression tests for enum_is_in_range

de02783

Adds regression tests for enum_is_in_range to test positive, negative and error outcomes on both named and typedef'd enumerations.

Add documentation for CPROVER_enum_is_in_range

baab734

Adds documentation of how to use the CPROVER_enum_is_in_range function to explain to a user how to use this function.

TGWDB force-pushed the CPROVER-enum-is-in-range branch from b953457 to baab734 Compare February 17, 2021 14:49

TGWDB merged commit bfad11a into diffblue:develop Feb 17, 2021

tautschnig reviewed Feb 18, 2021

View reviewed changes

regression/ansi-c/enum_is_in_range/enum_test10.desc Show resolved Hide resolved

		const auto disjunction = ::disjunction(disjuncts);

		code_assignt assignment(lhs, disjunction);

Cprover enum is in range #5808

Cprover enum is in range #5808

Uh oh!

Conversation

TGWDB commented Feb 9, 2021

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!

hannes-steffenhagen-diffblue Feb 10, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

codecov bot commented Feb 9, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig left a comment

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!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

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!

hannes-steffenhagen-diffblue commented Feb 10, 2021

Uh oh!

tautschnig commented Feb 10, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Feb 10, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

TGWDB commented Feb 15, 2021

Uh oh!

tautschnig left a comment

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

hannes-steffenhagen-diffblue Feb 10, 2021 •

edited

Loading

codecov bot commented Feb 9, 2021 •

edited

Loading

tautschnig commented Feb 10, 2021 •

edited

Loading