CBMC additional profiling info: Count and report all array constraints added during postprocessing #5478

natasha-jeppu · 2020-08-26T19:04:06Z

Track constraints added for arrays in post processing as a potentially useful metric for performance evaluation.

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.

natasha-jeppu · 2020-08-26T19:07:32Z

src/solvers/flattening/arrays.h

+  enum class constraint_typet
+  {
+    ARRAY_ACKERMANN,
+    ARRAY_EQUALITY,
+    ARRAY_WITH,
+    ARRAY_WITH_OTHER,
+    ARRAY_IF_TRUE,
+    ARRAY_IF_FALSE,
+    ARRAY_OF,
+    ARRAY_TYPECAST,
+    ARRAY_CONSTANT,
+    ARRAY_NON_CONSTANT,
+    ARRAY_COMPREHENSION
+  };
+
+  typedef std::list<exprt> array_constraintst;
+  typedef std::map<constraint_typet, array_constraintst> array_constraints_mapt;
+  array_constraints_mapt array_constraints_map;
+  void display_constraints();
+  std::string enum_to_string(constraint_typet);


Is there a better way of doing this? Wanted to include more specific information regarding the type of constraint. For example split constraints added for array_with to constraints added for the specific index and for other indices.

peterschrammel

I thought this was about reporting metrics, but this PR stores copies of constraints and outputs them - what is the use case for this very detailed information?

peterschrammel · 2020-09-03T15:55:45Z

src/solvers/flattening/arrays.h

+
+  typedef std::list<exprt> array_constraintst;
+  typedef std::map<constraint_typet, array_constraintst> array_constraints_mapt;
+  array_constraints_mapt array_constraints_map;


❗Storing copies of these constraints is not ideal wrt memory consumption.

No longer applicable, changed to store only number of constraints, don't store the constraints themselves.

natasha-jeppu · 2020-09-03T16:12:37Z

I thought this was about reporting metrics, but this PR stores copies of constraints and outputs them - what is the use case for this very detailed information?

The intention was to investigate how array constraints added during post processing affects CBMC performance.

In order to see if the constraints themselves give any information, I tracked them here. But this is not very helpful indeed. I will be changing this to track just the number of constraints rather than the constraints themselves.

Let me know if you have any other metric in mind pertaining to this that could be useful.

natasha-jeppu · 2020-09-03T19:40:45Z

src/solvers/flattening/arrays.h

+  enum class constraint_typet
+  {
+    ARRAY_ACKERMANN,
+    ARRAY_EQUALITY,
+    ARRAY_WITH,
+    ARRAY_WITH_OTHER,
+    ARRAY_IF_TRUE,
+    ARRAY_IF_FALSE,
+    ARRAY_OF,
+    ARRAY_TYPECAST,
+    ARRAY_CONSTANT,
+    ARRAY_NON_CONSTANT,
+    ARRAY_COMPREHENSION
+  };


Is there a clean way of extending the existing lazy_typet enum class into a new enum class to include ARRAY_EQUALITY? Do not want to change the meaning of the lazy_typet by adding ARRAY_EQUALITY to the existing enum class.

@peterschrammel

src/solvers/flattening/arrays.cpp

codecov · 2020-09-11T15:53:35Z

Codecov Report

Merging #5478 (04341a8) into develop (46b3f01) will decrease coverage by 0.00%.
The diff coverage is 54.16%.

@@             Coverage Diff             @@
##           develop    #5478      +/-   ##
===========================================
- Coverage    69.34%   69.34%   -0.01%     
===========================================
  Files         1241     1241              
  Lines       100488   100530      +42     
===========================================
+ Hits         69688    69709      +21     
- Misses       30800    30821      +21

Flag	Coverage Δ
cproversmt2	`43.13% <35.41%> (-0.01%)`	⬇️
regression	`66.24% <54.16%> (-0.01%)`	⬇️
unit	`32.26% <20.83%> (-0.02%)`	⬇️

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

Impacted Files	Coverage Δ
src/cbmc/cbmc_parse_options.h	`100.00% <ø> (ø)`
src/solvers/flattening/bv_pointers.h	`100.00% <ø> (ø)`
src/solvers/flattening/arrays.cpp	`83.39% <40.00%> (-6.37%)`	⬇️
src/solvers/flattening/arrays.h	`91.66% <50.00%> (+1.66%)`	⬆️
src/cbmc/cbmc_parse_options.cpp	`77.62% <100.00%> (+0.30%)`	⬆️
src/goto-checker/solver_factory.cpp	`67.42% <100.00%> (+0.18%)`	⬆️
src/solvers/flattening/boolbv.h	`78.57% <100.00%> (ø)`
src/solvers/flattening/bv_pointers.cpp	`82.40% <100.00%> (ø)`

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 46b3f01...04341a8. Read the comment docs.

peterschrammel · 2020-09-23T16:13:14Z

regression/cbmc/array-constraint/test.desc

+^SIGNAL=0$
+--
+--
+To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.


⛏️ missing newline at end of file

peterschrammel · 2020-09-23T16:13:19Z

regression/cbmc/array-constraint/test_xml.desc

+^SIGNAL=0$
+--
+--
+To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.


⛏️ missing newline at end of file

src/solvers/flattening/arrays.cpp

…added during post processing Array theory constraints added during post processing might be useful to reason about proof runtimes. This commit adds a new parse option --show-array-constraints that tracks constraints pertaining to arrays added during post processing.

… format This commit adds utilities to track array constraints and also the type of constraint being added, eg: ackermann constraint, array_of etc. Added a new enum class constraint_typet which is an extension of lazy_typet. This enum class includes a separate value for constraints added for other indices array_with, constraints added for the 'true' and 'false branches of if etc in addition to those available in lazy_typet. Also define a new member of type std::map that tracks mapping between type of constraint and the constraint itself. Currently support json output.

…boolean option used in arrayst class Add an additional boolean argument to the class constrcutor to propagate the setting of parse option --show-array-constraints to true to the arrayst class. The entry point for this is in the default invocation of solver factory.

… format This commit adds utilities to track array constraints and also the type of constraint being added, eg: ackermann constraint, array_of etc. Added a new enum class constraint_typet which is an extension of lazy_typet. This enum class includes a separate value for constraints added for other indices array_with, constraints added for the 'true' and 'false branches of if etc in addition to those available in lazy_typet. Also define a new member of type std::map that tracks mapping between type of constraint and the constraint itself. Currently support json output. clang format arrays.cpp

…boolean option used in arrayst class Add an additional boolean argument to the class constrcutor to propagate the setting of parse option --show-array-constraints to true to the arrayst class. The entry point for this is in the default invocation of solver factory. clang format solver_factory and bv_pointers

clang format regression test Adding KNOWNBUG flag to ignore failed test The --smt2 option does not go over arrayst class so no output is generated. The current test thus fails on test-cprover-smt2.

…added during post processing Array theory constraints added during post processing might be useful to reason about proof runtimes. This commit adds a new parse option --show-array-constraints that tracks constraints pertaining to arrays added during post processing. fix command line argument to display error message of xml or plain format is used

… constraints

add newline to test.desc

natasha-jeppu commented Aug 26, 2020

View reviewed changes

danielsn added the aws Bugs or features of importance to AWS CBMC users label Aug 26, 2020

peterschrammel reviewed Sep 3, 2020

View reviewed changes

natasha-jeppu commented Sep 3, 2020

View reviewed changes

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

natasha-jeppu marked this pull request as ready for review September 23, 2020 16:18

natasha-jeppu requested review from chrisr-diffblue, kroening, martin-cs and smowton as code owners September 23, 2020 16:18

peterschrammel reviewed Sep 23, 2020

View reviewed changes

peterschrammel approved these changes Sep 23, 2020

View reviewed changes

danielsn force-pushed the array_theory branch 2 times, most recently from 1c8aa27 to c88821c Compare November 19, 2020 15:39

Natasha Yogananda Jeppu added 12 commits November 19, 2020 12:47

Regression test for --show-array-constraints --json-ui

30dc217

Regression test for --show-array-constraints --json-ui

bbac08f

clang format regression test Adding KNOWNBUG flag to ignore failed test The --smt2 option does not go over arrayst class so no output is generated. The current test thus fails on test-cprover-smt2.

track number of constraints of different types rather than the actual…

56158fe

… constraints

Regression tests for --xml-ui and plain

ecb0a5d

Regression tests for --xml-ui and plain

fbe0406

Regression tests for --xml-ui and plain

04341a8

add newline to test.desc

danielsn force-pushed the array_theory branch from c88821c to 04341a8 Compare November 19, 2020 17:49

tautschnig merged commit 6648620 into diffblue:develop Nov 19, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CBMC additional profiling info: Count and report all array constraints added during postprocessing #5478

CBMC additional profiling info: Count and report all array constraints added during postprocessing #5478

natasha-jeppu commented Aug 26, 2020

natasha-jeppu Aug 26, 2020

peterschrammel left a comment

peterschrammel Sep 3, 2020 •

edited

Loading

natasha-jeppu Sep 23, 2020

natasha-jeppu commented Sep 3, 2020 •

edited

Loading

natasha-jeppu Sep 3, 2020

natasha-jeppu Sep 23, 2020

codecov bot commented Sep 11, 2020 •

edited

Loading

peterschrammel Sep 23, 2020

natasha-jeppu Sep 24, 2020

peterschrammel Sep 23, 2020

natasha-jeppu Sep 24, 2020

CBMC additional profiling info: Count and report all array constraints added during postprocessing #5478

CBMC additional profiling info: Count and report all array constraints added during postprocessing #5478

Conversation

natasha-jeppu commented Aug 26, 2020

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

peterschrammel Sep 3, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

natasha-jeppu commented Sep 3, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov bot commented Sep 11, 2020 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Sep 3, 2020 •

edited

Loading

natasha-jeppu commented Sep 3, 2020 •

edited

Loading

codecov bot commented Sep 11, 2020 •

edited

Loading