Rewrite smt2_conv to build a syntax tree TG-5825 #4100

romainbrenguier · 2019-02-05T19:06:46Z

This defines an AST class for smt2 instances, and modify convert_expr to return one of this instances.

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.

tautschnig · 2019-02-05T19:25:08Z

Why not use irept instead of introducing this new AST class?

romainbrenguier · 2019-02-06T06:40:27Z

Why not use irept instead of introducing this new AST class?

The original reason was type safety, so that we couldn't mix ASTs and exprt.
A harder constraints is that we want to print without using a recursive function (or a stack), which I'm not sure we can do with irept. I think this has caused problems in the past.

tautschnig · 2019-02-06T06:55:31Z

I had expected some collection of classes that would do actual typed AST nodes, but it seems this is just another string-based approach so I’m not particularly convinced there is added type safety?

For printing, I have not yet understood what makes this new AST class so fundamentally different- irept can happily be used without recursion, as is done in the depth iterator.

romainbrenguier · 2019-02-06T14:20:30Z

I had expected some collection of classes that would do actual typed AST nodes, but it seems this is just another string-based approach so I’m not particularly convinced there is added type safety?

Yes for now there are only strings and mp_integer and we don't do many checks, but we can slowly transition to stricter type checking. The idea would be to avoid direct calls to smt2_node and instead used typed functions like smt2_extract, smt2_bv, etc

For printing, I have not yet understood what makes this new AST class so fundamentally different- irept can happily be used without recursion, as is done in the depth iterator.

I thought depth iterator were using a stack, but apparently it's a deque, so yes it could work.
But it seems wrong to use irept for something much more specific. It would be like using a tree to encode a list, or a vector to encode a pair; it's inefficient and confusing.

tautschnig · 2019-02-06T15:53:10Z

It would be like using a tree to encode a list, or a vector to encode a pair; it's inefficient and confusing.

Well, there are different approaches to building ASTs. One school of thought is to use dedicated classes/data types for each kind, and another approach is to have a generic representation with information held in strings (or some other sufficiently general data type). Of course the latter doesn't give you compiler-supported type checking, but it makes it much easier to extend a language.

If you would like to pursue the first approach with dedicated data types that's fine, but I just don't see how the PR achieves this at the moment. As far as I understand (and I might be wrong) the PR introduces just a new generic data type to hold AST nodes. Maybe it's in some way more efficient than irept, but again I don't understand where exactly that's the case.

So I'll keep fighting what currently feels like not-invented-here-syndrome until sufficient documentation, commit messages, etc. is provided to clearly describe why a new AST base class is needed, and what its characteristics/limitations are.

kroening · 2019-02-06T21:19:43Z

BTW, for type safety, simply derive from irept.
Also, is there any benefit in building that AST? If the only purpose is to output it to the SMT2 solver, that could be done instead of building.

romainbrenguier · 2019-02-08T15:42:58Z

@kroening

Also, is there any benefit in building that AST? If the only purpose is to output it to the SMT2 solver, that could be done instead of building.

The goal is to separate conversion from printing. The immediate benefit is the syntax correctness is easier to check (in particular we don't have to worry about unmatched parenthesis) and the code should be clearer. Ultimately we could pass the AST directly to the smt solver without having to print it and then parse it back.

@tautschnig
I get your point about not having two data structures for the same thing. I see a couple of issues with irept but it can be worked around. I will try something in that direction.

romainbrenguier · 2019-05-17T08:57:50Z

src/solvers/smt2/smt2_ast.h

+  {
+  }
+
+  smt2_sortt(smt2_symbolt symbol, std::vector<smt2_astt> &&parameters)


The parameters should be smt2_sortts and symbol should be smt2_identifiert

romainbrenguier · 2019-05-17T08:59:32Z

src/solvers/smt2/smt2_ast.h

+private:
+  /// Indexed sort, only used for BitVec at the moment
+  smt2_sortt(irep_idt symbol, std::vector<smt2_constantt> &&parameters)
+    : smt2_astt(smt2_identifiert{smt2_symbolt(symbol), std::move(parameters)})


there shouldn't be a need for this constructor if the one above is made to take a smt2_identifiert

romainbrenguier · 2019-05-17T10:06:27Z

src/solvers/smt2/smt2_command.h

+  return stream;
+}
+
+class smt2_commandt final : public smt2_command_or_commentt


Reference the SMT-LIB standard http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 9dd2ff4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112202263

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 4ddd58f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114702452

This reflects the inheritance from exprt and will avoid collision with a type that will be introduced for smt2 ASTs.

This is to represent the structure of the smt2 instance generated by smt2_conv. This will allow separation between the structure and the printing of these instances. The structure is not used in this commit but will ultimately be used by convert_expr. The class inherits from non_sharing_treet to reuse the structure of trees. Sharing does not seem to be useful for the usage we will make of these ASTs. We don't inherit from irept so that we can get some type safety: in particular we can't add a irept child to a smt2_astt by mistake.

This allows to separate the creation of the structure of the AST from its printing. Unfortunately all the functions we modify here are mutualy recursive so they have to be modified all at once. That's why this commit is so big. The correctness of this change is checked by the regression test that are run using: scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2 which is done by travis.

This reflects the structure of SMT2 commands, making commands constructed using this framework will be syntatically correct by construction.

Allow better structure of the code and avoids syntaxic mistakes.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 84b0a90).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/116629722

TGWDB · 2021-09-15T09:07:43Z

Closing as this is now out of date and being done in another series of PRs, for details see #6134

romainbrenguier added the In progress label Feb 5, 2019

romainbrenguier requested review from allredj, kroening, martin-cs, peterschrammel and tautschnig as code owners February 5, 2019 19:06

romainbrenguier force-pushed the clean-up/smt-backend branch from 0ecb1e3 to fef9a22 Compare February 6, 2019 15:48

romainbrenguier requested review from chrisr-diffblue and smowton as code owners February 6, 2019 15:48

peterschrammel assigned romainbrenguier Feb 9, 2019

romainbrenguier force-pushed the clean-up/smt-backend branch from fef9a22 to 842ae2a Compare February 20, 2019 10:57

romainbrenguier changed the title ~~Big rewrite of smt2_conv~~ Rewrite of smt2_conv to build a syntax tree Feb 22, 2019

romainbrenguier force-pushed the clean-up/smt-backend branch 4 times, most recently from 0193bf4 to 89d558e Compare February 22, 2019 09:08

romainbrenguier changed the title ~~Rewrite of smt2_conv to build a syntax tree~~ Rewrite smt2_conv to build a syntax tree Feb 22, 2019

romainbrenguier force-pushed the clean-up/smt-backend branch 6 times, most recently from bd6ecec to 37aa9cb Compare March 1, 2019 15:44

romainbrenguier requested review from pkesseli and thk123 as code owners May 10, 2019 09:42

romainbrenguier force-pushed the clean-up/smt-backend branch from feea012 to 750acf3 Compare May 10, 2019 12:04

romainbrenguier closed this May 10, 2019

romainbrenguier force-pushed the clean-up/smt-backend branch from 750acf3 to fc65eae Compare May 10, 2019 13:10

romainbrenguier reopened this May 10, 2019

romainbrenguier force-pushed the clean-up/smt-backend branch 6 times, most recently from fe3f5ba to 9dd2ff4 Compare May 17, 2019 08:15

romainbrenguier commented May 17, 2019

View reviewed changes

allredj reviewed May 17, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/smt-backend branch 3 times, most recently from f36bb2a to af2eedf Compare May 21, 2019 12:09

romainbrenguier force-pushed the clean-up/smt-backend branch from af2eedf to 4ddd58f Compare June 7, 2019 07:03

allredj reviewed Jun 7, 2019

View reviewed changes

romainbrenguier added 5 commits June 24, 2019 10:44

Rename class to smt2_symbol_exprt

d498bc1

This reflects the inheritance from exprt and will avoid collision with a type that will be introduced for smt2 ASTs.

Add a class for SMT2 commands

40a2b51

This reflects the structure of SMT2 commands, making commands constructed using this framework will be syntatically correct by construction.

Use smt2_commandt in smt2_conv

84b0a90

Allow better structure of the code and avoids syntaxic mistakes.

romainbrenguier force-pushed the clean-up/smt-backend branch from 4ddd58f to 84b0a90 Compare June 24, 2019 09:45

allredj reviewed Jun 24, 2019

View reviewed changes

TGWDB closed this Sep 15, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Rewrite smt2_conv to build a syntax tree TG-5825 #4100

Rewrite smt2_conv to build a syntax tree TG-5825 #4100

Uh oh!

romainbrenguier commented Feb 5, 2019 •

edited

Loading

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

romainbrenguier commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

romainbrenguier commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019 •

edited

Loading

Uh oh!

kroening commented Feb 6, 2019

Uh oh!

romainbrenguier commented Feb 8, 2019

Uh oh!

romainbrenguier May 17, 2019

Uh oh!

romainbrenguier May 17, 2019

Uh oh!

romainbrenguier May 17, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

TGWDB commented Sep 15, 2021

Uh oh!

Uh oh!

Rewrite smt2_conv to build a syntax tree TG-5825 #4100

Rewrite smt2_conv to build a syntax tree TG-5825 #4100

Uh oh!

Conversation

romainbrenguier commented Feb 5, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

romainbrenguier commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

romainbrenguier commented Feb 6, 2019

Uh oh!

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

Uh oh!

Uh oh!

kroening commented Feb 6, 2019

Uh oh!

romainbrenguier commented Feb 8, 2019

Uh oh!

romainbrenguier May 17, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier May 17, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier May 17, 2019

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!

TGWDB commented Sep 15, 2021

Uh oh!

Uh oh!

romainbrenguier commented Feb 5, 2019 •

edited

Loading

tautschnig commented Feb 6, 2019 •

edited

Loading