Introduce expression enumerators #7080

qinheping · 2022-08-21T04:42:36Z

This PR include expression enumerator interface that allow us to specify regular tree grammars over exprt and enumerate expressions from the grammar. It will be used in the enumerative loop-invariant synthesizer.

We use a placeholder class to represent non-terminal symbols, enumerator classes to represent productions, and a factory class to represent grammars. A factory contain a map from placeholders to enumerators (non-terminal symbols to their productions). To enumerate expressions in the grammar with a given size, we repeatably expand placeholders with their productions until the expected size is reached. And then all productions without placeholders are instantiated to exprt objects.

enumerator_baset: base class of enumerators.
leaf_enumeratort: enumerators that enumerate leaf expressions---complete exprt without placeholder.
non_leaf_enumeratort: enumerators that enumerate tree expressions of form op(a_1, ..., a_n) where op is its operator symbol, n is the arity of op, and a_i are expressions enumerated by the i-th sub-enumerator.
binary_functional_enumeratort : non_leaf_enumeratort: enumerators that enumerate trees with two children. It is optimized for boolean operators, comparison operators, and the operator +.
alternatives_enumeratort: enumerators that enumerate expressions from the union of expressions enumerated by their sub-enumerators. For example, an enumerator for productions -> S + 1 | 1 in the grammar S -> S + 1 | 1 should enumerate the union of -> S + 1 and -> 1.
recursive_enumerator_placeholdert: placeholders that represent non-terminals in the grammar.
enumerator_factory_baset: factories that maintain enumerators, placeholders, and the map from placeholders to enumerators.

codecov · 2022-08-21T05:50:44Z

Codecov Report

Base: 77.87% // Head: 77.99% // Increases project coverage by +0.12% 🎉

Coverage data is based on head (f8e6230) compared to base (948994a).
Patch coverage: 85.85% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7080      +/-   ##
===========================================
+ Coverage    77.87%   77.99%   +0.12%     
===========================================
  Files         1574     1619      +45     
  Lines       181163   187185    +6022     
===========================================
+ Hits        141072   146000    +4928     
- Misses       40091    41185    +1094

Impacted Files	Coverage Δ
jbmc/src/jbmc/jbmc_parse_options.cpp	`75.88% <0.00%> (ø)`
...variable-sensitivity/variable_sensitivity_domain.h	`100.00% <ø> (ø)`
.../analyses/variable-sensitivity/write_stack_entry.h	`100.00% <ø> (ø)`
src/ansi-c/ansi_c_typecheck.cpp	`67.85% <0.00%> (ø)`
src/ansi-c/expr2c_class.h	`100.00% <ø> (ø)`
src/cpp/cpp_typecheck.cpp	`77.70% <0.00%> (ø)`
src/goto-analyzer/goto_analyzer_parse_options.cpp	`72.27% <ø> (ø)`
src/goto-cc/armcc_cmdline.cpp	`22.22% <ø> (ø)`
src/goto-cc/gcc_cmdline.cpp	`79.23% <ø> (ø)`
src/goto-cc/ms_cl_cmdline.cpp	`0.00% <ø> (ø)`
... and 373 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

jimgrundy · 2022-08-24T23:30:20Z

@SaswatPadhi, can you provide a first review of this so that we are making good use of the time of the DiffBlue reviewers.

tautschnig

I admit to not having read the entire PR, perhaps only the first half of it. As indicated in some comment, I would really appreciate some comments that explain the high-level idea. Various comments of mine hint at cleanup, which would make the code a lot more concise and thereby easier to read.

src/goto-instrument/synthesizer/expr_enumerator.cpp

src/goto-instrument/synthesizer/expr_enumerator.h

tautschnig · 2022-09-02T10:26:28Z

src/goto-instrument/synthesizer/expr_enumerator.h

+  void set_non_exchangable()
+  {
+    is_exchangable = false;
+  }


What is this method about?

Added a comment to explain exchangeable.

tautschnig · 2022-09-02T10:27:22Z

src/goto-instrument/synthesizer/expr_enumerator.h

+  bool is_commutative(const irep_idt op)
+  {
+    return op_id == ID_equal || op_id == ID_plus;
+  }


What about multiplication, not-equal, and, or, bitand, bitor, bitxor? You might want to look at, or perhaps even call the functions from src/util/simplify_utils.cpp.

Thanks for the reminder. simplify_expr() is now used to rule out more expressions. However, the optimization introduced in this class is still needed to avoid to enumerate redundant expressions.

martin-cs · 2022-09-02T13:37:52Z

Maybe I am getting mixed up but I remember @polgreen having some SyGuS / expression synthesis code built with CPROVER. Maybe with was @pkesseli ? Am hoping that @peterschrammel remembers...

polgreen · 2022-09-02T13:45:44Z

Maybe I am getting mixed up but I remember @polgreen having some SyGuS / expression synthesis code built with CPROVER. Maybe with was @pkesseli ? Am hoping that @peterschrammel remembers...

We did, but it wasn't enumerating: it was a symbolic encoding using selector variables in a fixed grammar and asking a decision procedure to find assignments to those selector variables that made the expression satisfy some spec.
The synthesis encoding is here: https://github.com/kroening/fastsynth/blob/master/src/fastsynth/synth_encoding.cpp

martin-cs · 2022-09-02T15:32:58Z

Thanks for the super-swift response @polgreen

NlightNFotis

Sorry, didn't spend a lot of time reviewing - please ping me when you want to re-review it.

src/config.inc

qinheping · 2022-09-26T14:17:24Z

I admit to not having read the entire PR, perhaps only the first half of it. As indicated in some comment, I would really appreciate some comments that explain the high-level idea. Various comments of mine hint at cleanup, which would make the code a lot more concise and thereby easier to read.

Thanks for the comments. I addressed most of the comments and added more explanation and examples.

Issue has been addressed

tautschnig

A few more comments. This time I have managed to read all the code, and what I find the hardest to comprehend is the business of setting the size (is that the arity?). Why is the current approach the right one?

src/goto-instrument/synthesizer/expr_enumerator.cpp

src/goto-instrument/synthesizer/expr_enumerator.h

tautschnig · 2022-09-28T20:34:23Z

src/goto-instrument/synthesizer/expr_enumerator.cpp

+}
+
+std::list<partitiont>
+non_leaf_enumeratort::get_partitions(std::size_t n, std::size_t k)


So as to avoid having to convince myself that your algorithm is correct: how about using https://graphics.stanford.edu/~seander/bithacks.html#NextBitPermutation instead?

Seconded. This took quite a bit of time to understand.

Yes, I added an implementation that use the bithacks to enumerate bit permutation. However, such method only works for n <= 64 due to the length of size_t. I rewrote the old implementation using a similar idea of next-bit-permutation to handle n > 64

You could use mp_integer, but is it actually realistic to ever want n > 64? Depending on the value of k this might get very expensive...

src/goto-instrument/synthesizer/expr_enumerator.cpp

src/goto-instrument/synthesizer/expr_enumerator.h

nwetzler · 2022-09-29T23:00:15Z

src/goto-instrument/synthesizer/expr_enumerator.cpp

+}
+
+std::list<partitiont>
+non_leaf_enumeratort::get_partitions(std::size_t n, std::size_t k)


Seconded. This took quite a bit of time to understand.

qinheping · 2022-10-06T05:15:51Z

I pushed an update including the following changes:

A walkthrough example to illustrate how the enumeration works and why do we need to compute the Cartesian products.
Removing all clone functions and unnecessary pointers.
Removing set_size functions and expected_size. Now the function enumerate(std::size_t size) explicitly take the size of expressions we want to enumerate as argument.
Implementing a new get_partition(n, k) function using the bithack you suggested. However, it works for only n no larger than 64. So I rewrote the old implementation using the same idea of computing next bit permutation to handle case of n > 64.

src/goto-instrument/synthesizer/expr_enumerator.cpp

qinheping requested review from martin-cs, chris-ryder and peterschrammel as code owners August 21, 2022 04:42

qinheping force-pushed the loop_invariant_synthesis branch from 9a8b1bc to 12b7ad8 Compare August 21, 2022 05:25

qinheping force-pushed the loop_invariant_synthesis branch from 12b7ad8 to 114b145 Compare August 21, 2022 06:13

jimgrundy requested a review from SaswatPadhi August 24, 2022 23:29

jimgrundy assigned SaswatPadhi Aug 25, 2022

jimgrundy added aws Bugs or features of importance to AWS CBMC users aws-medium labels Aug 25, 2022

feliperodri added the Synthesis Invariant synthesis label Aug 31, 2022

tautschnig self-assigned this Sep 2, 2022

tautschnig requested changes Sep 2, 2022

View reviewed changes

tautschnig assigned qinheping and unassigned tautschnig Sep 2, 2022

qinheping force-pushed the loop_invariant_synthesis branch from 114b145 to 210246b Compare September 8, 2022 05:02

qinheping requested a review from a team as a code owner September 8, 2022 05:02

NlightNFotis previously requested changes Sep 8, 2022

View reviewed changes

src/config.inc Outdated Show resolved Hide resolved

qinheping force-pushed the loop_invariant_synthesis branch 2 times, most recently from ea47a16 to fd2bac4 Compare September 8, 2022 14:49

qinheping changed the title ~~Expression enumerators~~ Introduce expression enumerators Sep 8, 2022

SaswatPadhi removed their request for review September 17, 2022 23:59

qinheping force-pushed the loop_invariant_synthesis branch 3 times, most recently from 3530345 to 822fcbf Compare September 26, 2022 06:29

SaswatPadhi removed their assignment Sep 26, 2022

qinheping force-pushed the loop_invariant_synthesis branch from f93db8f to 393c5e4 Compare September 26, 2022 15:06

qinheping requested review from NlightNFotis and removed request for tautschnig September 26, 2022 15:53

tautschnig self-assigned this Sep 28, 2022

nwetzler self-requested a review September 28, 2022 13:42

tautschnig reviewed Sep 28, 2022

View reviewed changes

nwetzler approved these changes Sep 29, 2022

View reviewed changes

tautschnig removed their assignment Oct 4, 2022

qinheping force-pushed the loop_invariant_synthesis branch 6 times, most recently from 579c55a to 6cd5d8e Compare October 6, 2022 05:15

qinheping requested a review from tautschnig October 10, 2022 15:57

tautschnig approved these changes Oct 11, 2022

View reviewed changes

tautschnig assigned peterschrammel and martin-cs Oct 11, 2022

qinheping force-pushed the loop_invariant_synthesis branch 3 times, most recently from 13571cb to a75e2d6 Compare October 12, 2022 03:17

qinheping requested a review from kroening as a code owner October 12, 2022 03:17

Introduce grammar-based expression enumerators

f8e6230

qinheping force-pushed the loop_invariant_synthesis branch from a75e2d6 to f8e6230 Compare October 12, 2022 04:26

kroening unassigned peterschrammel and martin-cs Oct 12, 2022

kroening merged commit b0744ea into diffblue:develop Oct 12, 2022

Introduce expression enumerators #7080

Introduce expression enumerators #7080

Uh oh!

Conversation

qinheping commented Aug 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Aug 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

jimgrundy commented Aug 24, 2022

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Sep 2, 2022

Uh oh!

polgreen commented Sep 2, 2022

Uh oh!

martin-cs commented Sep 2, 2022

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

qinheping commented Sep 26, 2022

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

qinheping commented Oct 6, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

qinheping commented Aug 21, 2022 •

edited

Loading

codecov bot commented Aug 21, 2022 •

edited

Loading