Configurable expr2c #2713

thk123 · 2018-08-10T14:22:50Z

Subsumes #2704

Commit by commit probably makes the most sense for reviewing, the "extended interface" I alluded to in discussions in #2704 is the method added in the last commit. If memory serves, it is useful for when you have an array of a struct Foo, with variable name "var_name" and you want to print something like:

struct Foo var_name[]

then you can call type2c(type, "var_name", ns) and get what you want, otherwise you have to split apart struct Foo [] to insert your identifier.

thk123 · 2018-08-10T14:24:18Z

@mmuesly hopefully isn't too hard to adapt your commit to use this, now can just use the regular expr2 methods with a expr2c_configurationt::clean_configuration

kroening · 2018-08-10T14:24:33Z

Is this really needed? I strongly recommend instead divoring expr2java from expr2c.

thk123 · 2018-08-10T14:46:18Z

@kroening not needed by expr2java (& TG [almost] doesn't use expr2java anymore) - was requested by @peterschrammel in #2704

mmuesly · 2018-08-10T16:59:21Z

@thk123 Don't be afraid, about having me to readapt code to one of these versions. As soon as, there is a decision, which of these versions around makes it into develop, I will pick it up and make my changes work using it.

But seems, like the underlying need of getting some clean and compilable c code, is around in various sub-projects. Therefore I appreciate any solution that does this in one central place.

peterschrammel · 2018-08-10T17:29:44Z

But seems, like the underlying need of getting some clean and compilable c code, is around in various sub-projects. Therefore I appreciate any solution that does this in one central place.

Yes, this was the idea of upstreaming this code, since the current expr2ct in the CBMC repo doesn't always output compileable C, and we had some of the necessary fixes already in a subproject in a form that might satisfy your needs, @mmuesly.

smowton · 2018-08-11T08:33:02Z

src/ansi-c/expr2c.h

@@ -16,7 +16,50 @@ class exprt;
 class namespacet;
 class typet;

+struct expr2c_configurationt final


Good place to document what the options do?

tautschnig

Mostly good to go, except I don't understand the back&forth on expr2cleanc

tautschnig · 2018-08-11T08:41:11Z

jbmc/src/java_bytecode/expr2java.h

@@ -19,7 +19,10 @@ Author: Daniel Kroening, [email protected]
 class expr2javat:public expr2ct
 {
 public:
-  explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
+  explicit expr2javat(const namespacet &_ns)
+    : expr2ct(_ns, expr2c_configurationt::default_configuration)


I would suggest to maintain a 1-argument constructor that just picks the default configuration rather than forcing various places to change the code.

tautschnig · 2018-08-11T08:43:43Z

src/ansi-c/expr2c.cpp

@@ -1998,16 +2010,17 @@ std::string expr2ct::convert_constant_bool(bool boolean_value)
 {
  // C doesn't really have these


This comment should now be removed.

tautschnig · 2018-08-11T08:46:16Z

src/ansi-c/expr2c.h

+    const bool include_struct_padding_components,
+    const bool print_struct_body_in_type,
+    const bool inc_size_if_possible,
+    const std::string true_string,


Pass as reference

So clang-tidy warns me about this, preferring pass by value and using std::move - would you be happy with this?

No concern (and overall nit-picky of me anyway).

tautschnig · 2018-08-11T08:46:54Z

src/ansi-c/expr2c.h

+  expr2c_configurationt(
+    const bool include_struct_padding_components,
+    const bool print_struct_body_in_type,
+    const bool inc_size_if_possible,


That's the one option the meaning of which is not immediately clear to me from the name

Renamed to include_array_size and added docs

tautschnig · 2018-08-11T08:47:47Z

src/ansi-c/expr2c_class.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_map>
 #include <unordered_set>

+#include <ansi-c/expr2c.h>


I think we usually use #include "expr2c.h" when including a file from the same directory.

tautschnig · 2018-08-11T08:48:51Z

src/ansi-c/expr2c_class.h

-  explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
+  explicit expr2ct(
+    const namespacet &_ns,
+    const expr2c_configurationt &configuration)


As said above, leave the previous constructor in place and add an additional one. While at it, and in order to simplify code: use C++-11 initialisation of sizeof_nesting at the point of its declaration.

tautschnig · 2018-08-11T08:50:44Z

src/ansi-c/expr2cleanc.cpp

@@ -0,0 +1,76 @@
+/*******************************************************************\


GitHub confuses me: does the same PR both introduce and remove expr2cleanc.{h,cpp}?

tautschnig · 2018-08-11T08:55:18Z

src/ansi-c/expr2c.cpp

@@ -3966,6 +3966,18 @@ std::string expr2ct::convert(const exprt &src)
  return convert_with_precedence(src, precedence);
 }

+/// To convert a type in to ANSI-C but with the identifier in place.
+/// This is useful for array types where the identifier is inside the type


Nit picking: the wording doesn't quite work for me ("in to ANSI-C" and "inside the type"). How about: "Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position." Caveat: English is not my first language.

tautschnig · 2018-08-11T09:04:49Z

src/ansi-c/expr2c.cpp

+{
+  expr2ct expr2c(ns, configuration);
+  return expr2c.convert_with_identifier(type, identifier);
+}


Nice! I have filed #2715 as follow-up action for myself.

thk123 · 2018-08-13T10:42:41Z

@tautschnig I guess I was "moving" it from a private repo here and then removing it. I can just never introduce it if that is clearer for you?

thk123 · 2018-08-13T11:32:40Z

@tautschnig @smowton comments addressed

tautschnig · 2018-08-13T11:39:26Z

src/ansi-c/expr2c.h

@@ -53,6 +53,10 @@ struct expr2c_configurationt final
  /// This prints a human readable C like syntax that closely mirrors the
  /// internals of the GOTO program
  static expr2c_configurationt default_configuration;
+
+  /// This prints compilable C that is loses some of the internal details of the


Remove "is"

thk123 · 2018-08-13T11:41:29Z

TG bump: diffblue/test-gen#2162

peterschrammel · 2018-08-13T14:11:12Z

src/ansi-c/expr2c.cpp

@@ -30,6 +30,12 @@ Author: Daniel Kroening, [email protected]
 #include "c_qualifiers.h"
 #include "expr2c_class.h"

+expr2c_configurationt expr2c_configurationt::default_configuration{true,


Is this really what clang-format is doing? :/

Yes I know 😢

A case for // clang-format off, // clang-format on?

Done - hope you're happy with my choice of alternate formatting

This makes the subclassing of it redundant and should instead be customsied via the configuration.

This configuration can be used in place of expr2cleanc

thk123 · 2018-08-14T14:15:47Z

TG bump failing somehow, not yet investigated

It's linting 🤦‍♂️

4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration 01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor 9c3fd45 Add AWS CodeBuild badges 4261fd8 Remove appveyor badge fe23db7 Remove appveyor.yml 21857a7 Add support for getting components by name to `struct_exprt` 05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug 0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants 159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type 5ca6cd2 Restrict new clinit_wrapper calls to enum types 6e04213 Reformatting the structs to aid readability 0cfacb8 Add type2c conversion for specifying a type name c3fef70 Add a clean configuration for expr2c 3a40db1 Make expr2ct configurable in a number of ways 097cf71 Merge pull request diffblue#2731 from diffblue/increase-version 170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant c9e46ae Temporarily remove new UNREACHABLE statements 03e3877 Add tests for nondet initialization of enums 3e32140 CI lazy methods: load clinit for all param types 5542c54 Move nondet enum initialization to new function 6ecf4f9 Nondet-init enums by assigning them to a constant 6c84caa Refactor logic for generating a nondet int 07d1e44 Always run clinit_wrapper before nondet object init 3be826f Add some documentation to java_object_factory 5e80310 add invariant on parent-child class relationship 2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType c6acc9c increased version number in preparation for release 5.10 0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls 89048e6 Function-pointer remvoval: print human-friendly debug messages 1fc3118 Use pointer difference type when adding to pointer 072b592 Merge pull request diffblue#2726 from tautschnig/java-loc 4dca215 Goto program should not use java_method_typet 273fff4 Add can_cast_type and precondition. 6cb7e5d Reinstate require_code and add require_java_method 78f7cb7 Refactor constructors for java_method_typet 6cefc61 Unit tests conversion from code_typet to java_method_typet c3b8b5a Update tag in to_java_method_type 972315a Update docs on java_method_typet constructor 211931c Add tag for java_method_type 551df9c Update unit tests to use java_method_typet da18c9f Change variables named code_type to method_type f1bd41e Change code_typet to java_method_typet in jbmc be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id 03fa885 Replace function calls c4d79ab Java string preprocessing: use provided source location fb0c552 Java string preprocessing: use and document parameter function_id c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type 2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2 8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest 30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h 8c8801c List source files in goto-programs/Makefile in lexicographic order 40d28ae replace_symbolt: report replacements in code_typet::return_type 4b9df3b Revert "Ignore return value" e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe 424ab4f --stop-on-fail now stops on failed path 545bff8 Add clear() to path exploration worklist 95d8d0f Generalise option setting from strategy unit tests e85fb77 Cleanup constant_propagator_domaint::valuest 18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests 30d557a Constant propagation: Check type consistency before adding to replacement map a5ce621 Make unit tests quiet 61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names 7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm 3785941 Remove names of unused parameters af79cb9 add support for Visual Studio style inline assembler 254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix 26009a3 remove_asm now guarantees that functions called exist 9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue e247a29 CodeBuild: Remove empty artifact stanza 756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang 355fbd2 avoid assert() 6178908 bump goto binary version f93deec type symbols now use ID_symbol_type 22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation 5c06786 set mode for functions added by remove_asm ef53b65 Update description of regression test framework 312ca1d Add section to documentation about running tests d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location 119e88b Pass location around for nondet initialization 50660db Specify source location for nondet expressions d1f2ad9 Replace -> with → e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments 519370d State that identifiers should be good 30d29b9 Replace unicode arrows → with ascii ones -> 611374f Document classes and member variables unless obvious adb7ef0 Minor fixes to documentation outline fd4f563 Add side_effect_exprt constructor with location 98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions 6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide 61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes c0bcce7 use clang as native compiler for goto-clang 1f19e23 goto-cc: use result of our native compiler detection d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags f94d5e2 follow union, struct and enum tags 99e33bd fix typo in comments for struct_tag_typet 1f53246 expose remove_preconditions f212505 Avoids using expr.op0 when type is known 7b36ca2 Moves is_lvalue to expr_util.c 4782b48 Fix invariant regression tests efb1c40 Refactor invariant_failedt definition. 515f050 Pass the condition to the invariant_failedt constructor. bf6dd9e Added extra use-case hints to the already present invariant definitions. 612b4f8 Address review comments 7233f92 Rearrange everything into separate pages 1cb3cdd Move other tools into a separate file 82eefb7 Fix links between files d9e690b Move folder walkthrough to a separate file 2939db4 Address review comments 8d5cbcb Create CBMC developer guide documentation git-subtree-dir: cbmc git-subtree-split: 4f5e148

thk123 requested review from cesaro, chrisr-diffblue, cristina-david, kroening, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton and tautschnig as code owners August 10, 2018 14:22

thk123 mentioned this pull request Aug 10, 2018

Upstreaming expr2cleanct #2704

Closed

smowton reviewed Aug 11, 2018

View reviewed changes

tautschnig mentioned this pull request Aug 11, 2018

Replace dump_ct::make_decl once #2713 is merged #2715

Closed

tautschnig reviewed Aug 11, 2018

View reviewed changes

tautschnig assigned thk123 Aug 11, 2018

thk123 force-pushed the dump/expr2c-configuration branch from 87d0586 to 1212839 Compare August 13, 2018 11:32

tautschnig approved these changes Aug 13, 2018

View reviewed changes

thk123 force-pushed the dump/expr2c-configuration branch from 1212839 to 147cf09 Compare August 13, 2018 12:32

peterschrammel approved these changes Aug 13, 2018

View reviewed changes

thk123 force-pushed the dump/expr2c-configuration branch from 147cf09 to 34bf1ee Compare August 13, 2018 14:27

smowton approved these changes Aug 13, 2018

View reviewed changes

Make expr2ct configurable in a number of ways

3a40db1

This makes the subclassing of it redundant and should instead be customsied via the configuration.

thk123 added 3 commits August 14, 2018 11:17

Add a clean configuration for expr2c

c3fef70

This configuration can be used in place of expr2cleanc

Add type2c conversion for specifying a type name

0cfacb8

Reformatting the structs to aid readability

6e04213

thk123 force-pushed the dump/expr2c-configuration branch from 34bf1ee to 6e04213 Compare August 14, 2018 10:18

thk123 added the do not merge label Aug 14, 2018

thk123 removed the do not merge label Aug 15, 2018

thk123 merged commit 4f5e148 into diffblue:develop Aug 15, 2018

thk123 deleted the dump/expr2c-configuration branch August 15, 2018 12:45

mmuesly added a commit to mmuesly/cbmc that referenced this pull request Aug 16, 2018

Update to work with diffblue#2713 for clean c code output

cad848d

mmuesly added a commit to mmuesly/cbmc that referenced this pull request Aug 17, 2018

Update to work with diffblue#2713 for clean c code output

9e5d730

mmuesly mentioned this pull request Aug 21, 2018

Feature memory-analyzer [depends-on: #2680, #4261] #2649

Closed

mmuesly added a commit to mmuesly/cbmc that referenced this pull request Aug 30, 2018

Update to work with diffblue#2713 for clean c code output

9c15079

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Feb 15, 2019

Update to work with diffblue#2713 for clean c code output

afa8e35

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Feb 22, 2019

Update to work with diffblue#2713 for clean c code output

6a13987

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 1, 2019

Update to work with diffblue#2713 for clean c code output

31fbd5f

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 4, 2019

Update to work with diffblue#2713 for clean c code output

900f39d

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 4, 2019

Update to work with diffblue#2713 for clean c code output

8706a18

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Mar 19, 2019

Update to work with diffblue#2713 for clean c code output

656b38f

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 20, 2019

Update to work with diffblue#2713 for clean c code output

1f34cf5

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Mar 20, 2019

Update to work with diffblue#2713 for clean c code output

55b109d

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Mar 20, 2019

Update to work with diffblue#2713 for clean c code output

f71c1ca

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Mar 20, 2019

Update to work with diffblue#2713 for clean c code output

acab138

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Mar 20, 2019

Update to work with diffblue#2713 for clean c code output

2845d71

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Apr 15, 2019

Update to work with diffblue#2713 for clean c code output

7f3ba6f

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Apr 18, 2019

Update to work with diffblue#2713 for clean c code output

431bb29

danpoe pushed a commit to danpoe/cbmc that referenced this pull request Apr 23, 2019

Update to work with diffblue#2713 for clean c code output

0aae6a8

danpoe pushed a commit to danpoe/cbmc that referenced this pull request May 15, 2019

Update to work with diffblue#2713 for clean c code output

2fa97e8

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Configurable expr2c #2713

Configurable expr2c #2713

thk123 commented Aug 10, 2018

thk123 commented Aug 10, 2018

kroening commented Aug 10, 2018

thk123 commented Aug 10, 2018

mmuesly commented Aug 10, 2018

peterschrammel commented Aug 10, 2018 •

edited

Loading

smowton Aug 11, 2018

tautschnig left a comment

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

thk123 Aug 13, 2018

tautschnig Aug 13, 2018

tautschnig Aug 11, 2018

thk123 Aug 13, 2018

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

tautschnig Aug 11, 2018

thk123 commented Aug 13, 2018

thk123 commented Aug 13, 2018

tautschnig Aug 13, 2018

thk123 commented Aug 13, 2018

peterschrammel Aug 13, 2018

thk123 Aug 13, 2018

tautschnig Aug 13, 2018

thk123 Aug 14, 2018

thk123 commented Aug 14, 2018 •

edited

Loading

		@@ -1998,16 +2010,17 @@ std::string expr2ct::convert_constant_bool(bool boolean_value)
		{
		// C doesn't really have these

		@@ -0,0 +1,76 @@
		/*******************************************************************\

Configurable expr2c #2713

Configurable expr2c #2713

Conversation

thk123 commented Aug 10, 2018

thk123 commented Aug 10, 2018

kroening commented Aug 10, 2018

thk123 commented Aug 10, 2018

mmuesly commented Aug 10, 2018

peterschrammel commented Aug 10, 2018 • edited Loading

Choose a reason for hiding this comment

tautschnig left a comment

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

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

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

Choose a reason for hiding this comment

thk123 commented Aug 13, 2018

thk123 commented Aug 13, 2018

Choose a reason for hiding this comment

thk123 commented Aug 13, 2018

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

thk123 commented Aug 14, 2018 • edited Loading

peterschrammel commented Aug 10, 2018 •

edited

Loading

thk123 commented Aug 14, 2018 •

edited

Loading