Remove deprecated Java and string options [TG-4282] #2907

peterschrammel · 2018-09-05T21:19:22Z

No description provided.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2df4f4f).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

tautschnig · 2018-09-06T07:53:36Z

src/cbmc/cbmc_parse_options.h

@@ -50,8 +50,6 @@ class optionst;
  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
  "(refine-strings)" \
  "(string-printable)" \
-  "(string-max-length):" \
-  "(string-max-input-length):" \


CBMC seems to be missing "--max-nondet-string-length"?!

This option is not required for CBMC at the moment as the string solver integration for C is incomplete.

That I am aware of, but we do have (refine-strings) etc. So really we should not have a half-consistent view. I believe the way to go about this is as we have done with several other option sets already: define the set of options and the help strings in a header file and just use the macro.

Fully agreed. Note, however, that refine-strings is default in JBMC and hence the options won't be the same for CBMC and JBMC.

Ok, so we might need two different sets, but it would still be nice to have all this encapsulated in some header file. It's fairly easy to fix now, but will be a lot more costly later on.

tautschnig · 2018-09-06T07:56:16Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

-  {
-    object_factory_parameters.max_nondet_array_length =
-      safe_string2size_t(cmd.get_value("java-max-input-array-length"));
-  }


The code below this one (if(cmd.isset("max-nondet-array-length"))) needs to be removed as well: it's the front-end that now does it, and it will provide the result in the parameters. This, in turn, would hopefully enable a larger cleanup in that cmd should no longer be necessary in here?

The code below this one (if(cmd.isset("max-nondet-array-length"))) needs to be removed as well: it's the front-end that now does it, and it will provide the result in the parameters.

No, this has been a long time hack. The front end is and has been doing that in addition to the language module. Avoiding that would require options to be fed into the language module, which is a separate refactoring (and will eventually become obsolete with Daniel's ambitions to get rid of languaget).

But why do we need to keep doing it in addition in here? I don't see how the options story applies here: it's all being passed via object_factory_parameters already?

The same options are both used by the languaget instance and in goto passes.
The object_factory_parameters in parse_options is only used in goto passes. The languaget instance does its own parsing.

One could either retrieve the object_factory_parameters from a (temporary) languaget instance or pass options into the languaget instance (preferred).

I don't have a sufficient grasp of the Java front-end to tell what the correct solution is, but surely parsing the same command-line option multiple times is not acceptable.

This will definitely require a solution as we will face the same issue when generalising/porting the object_factory to C. And we won't be able to wait until we got rid of languaget in this case. (I'm still remembering the incident with #2192, #2157 which still hasn't been resolved after 4 months).

I'm happy to dismiss my blocking review on this one if the problem cannot be solved right here. I just want to make sure it does get resolved eventually, with first steps defined. The large-scale refactorings surely aren't the solution...

Noted here: #2908

tautschnig · 2018-09-06T07:57:40Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

-  {
-    object_factory_parameters.max_nondet_tree_depth =
-      safe_string2size_t(cmd.get_value("java-max-input-tree-depth"));
-  }


Equally, if(cmd.isset("max-nondet-tree-depth")) needs to go away as well. The front-end does the command-line options parsing, not the language processing code.

tautschnig · 2018-09-06T08:00:26Z

jbmc/regression/jbmc/NondetInit/test_lazy.desc

 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods


There's some incomplete work here - it seems just -- has been removed in this line? Also, the test is explicitly named test_lazy.

jbmc/regression/jbmc/class-literals/test_lazy.desc

tautschnig · 2018-09-06T08:01:30Z

jbmc/regression/jbmc/lazyloading1/test.desc

 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with


Incompatible with ... what? (multiple occurrences)

allredj

This PR failed Diffblue compatibility checks (cbmc commit: d8e452d).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 997aa1e).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

smowton · 2018-09-12T17:04:41Z

Since you assign me, and I'm idle due to just having come back from holiday, created https://github.com/diffblue/test-gen/tree/bump/2907 removing use of deprecated parameters and #2942 fixing a silly exposed bug.

smowton · 2018-09-12T20:22:12Z

@peterschrammel needs a rebase

smowton · 2018-09-12T20:23:08Z

Actually @peterschrammel merge #2935 first since that causes test-gen test failures in any case

allredj

Passed Diffblue compatibility checks (cbmc commit: dc94b85).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84816090

allredj

Passed Diffblue compatibility checks (cbmc commit: 56d01f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84820717

peterschrammel · 2018-09-14T15:58:08Z

@smowton, rebased.

peterschrammel requested review from cesaro, cristina-david, kroening, martin-cs, mgudemann, NathanJPhillips, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners September 5, 2018 21:19

peterschrammel force-pushed the remove-deprecated-options branch 2 times, most recently from 5a00bb8 to 2df4f4f Compare September 5, 2018 21:57

allredj reviewed Sep 5, 2018

View reviewed changes

tautschnig requested changes Sep 6, 2018

View reviewed changes

peterschrammel added the In progress label Sep 6, 2018

peterschrammel force-pushed the remove-deprecated-options branch from 2df4f4f to d8e452d Compare September 6, 2018 08:24

peterschrammel removed the In progress label Sep 6, 2018

allredj reviewed Sep 6, 2018

View reviewed changes

tautschnig approved these changes Sep 6, 2018

View reviewed changes

tautschnig mentioned this pull request Sep 6, 2018

Fix --string-non-empty option #2909

Merged

peterschrammel self-assigned this Sep 6, 2018

allredj reviewed Sep 6, 2018

View reviewed changes

tautschnig mentioned this pull request Sep 6, 2018

Separate parsing of language options from languaget #2911

Merged

peterschrammel assigned romainbrenguier, thk123 and mgudemann and unassigned peterschrammel Sep 10, 2018

romainbrenguier approved these changes Sep 11, 2018

View reviewed changes

peterschrammel changed the title ~~Remove deprecated Java and string options~~ Remove deprecated Java and string options [TG-4282] Sep 11, 2018

peterschrammel assigned smowton and unassigned romainbrenguier Sep 11, 2018

peterschrammel added 7 commits September 14, 2018 10:46

Remove --refine-strings from JBMC

44155b5

Remove --string-max-input-length from JBMC

95c6eef

Remove obsolete string options from CBMC

d3b8c01

Remove deprecated --java-throw-runtime-exceptions

92b642d

Remove deprecated --java-max-input-array-length

4d462b6

Remove deprecated --java-max-input-tree-depth

d76be60

Remove deprecated --lazy-methods

d527b68

peterschrammel force-pushed the remove-deprecated-options branch from 997aa1e to dc94b85 Compare September 14, 2018 09:47

allredj reviewed Sep 14, 2018

View reviewed changes

Use defines for string options and help text

56d01f4

peterschrammel force-pushed the remove-deprecated-options branch from dc94b85 to 56d01f4 Compare September 14, 2018 11:10

allredj reviewed Sep 14, 2018

View reviewed changes

peterschrammel merged commit d54d101 into diffblue:develop Sep 14, 2018

peterschrammel deleted the remove-deprecated-options branch September 14, 2018 21:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove deprecated Java and string options [TG-4282] #2907

Remove deprecated Java and string options [TG-4282] #2907

peterschrammel commented Sep 5, 2018

allredj left a comment

tautschnig Sep 6, 2018

peterschrammel Sep 6, 2018

tautschnig Sep 6, 2018

peterschrammel Sep 6, 2018

tautschnig Sep 6, 2018

tautschnig Sep 6, 2018

peterschrammel Sep 6, 2018 •

edited

Loading

tautschnig Sep 6, 2018 •

edited

Loading

peterschrammel Sep 6, 2018

peterschrammel Sep 6, 2018 •

edited

Loading

tautschnig Sep 6, 2018

peterschrammel Sep 6, 2018

tautschnig Sep 6, 2018

peterschrammel Sep 6, 2018

tautschnig Sep 6, 2018

tautschnig Sep 6, 2018

tautschnig Sep 6, 2018

allredj left a comment

allredj left a comment

smowton commented Sep 12, 2018

smowton commented Sep 12, 2018

smowton commented Sep 12, 2018

allredj left a comment

allredj left a comment

peterschrammel commented Sep 14, 2018

Remove deprecated Java and string options [TG-4282] #2907

Remove deprecated Java and string options [TG-4282] #2907

Conversation

peterschrammel commented Sep 5, 2018

allredj 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

peterschrammel Sep 6, 2018 • edited Loading

Choose a reason for hiding this comment

tautschnig Sep 6, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Sep 6, 2018 • edited Loading

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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

smowton commented Sep 12, 2018

smowton commented Sep 12, 2018

smowton commented Sep 12, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Sep 14, 2018

peterschrammel Sep 6, 2018 •

edited

Loading

tautschnig Sep 6, 2018 •

edited

Loading

peterschrammel Sep 6, 2018 •

edited

Loading