Remove utilities that never got used #2019

tautschnig · 2018-04-08T11:56:07Z

Where possible, commits introducing them were reverted. Other utilities came into existence even before moving to SVN/git.

Some of this code may be used outside the code base - pinging @kroening and @mgudemann for EBMC, @thk123, @smowton, @peterschrammel as your commits got reverted.

peterschrammel · 2018-04-08T17:28:46Z

src/goto-programs/property_checker.h

-#include "goto_trace.h"
-#include "goto_model.h"
-
-class property_checkert:public messaget


This is used by Deltacheck and 2LS.

What is it good for? Would it be possible to contribute documentation? Why does CBMC/JBMC not use it?

Moved to #2212 for separate discussion.

peterschrammel · 2018-04-08T17:34:35Z

src/goto-analyzer/static_analyzer.cpp

-
-#include <analyses/interval_domain.h>
-
-class static_analyzert:public messaget


This class should really be removed. I think, however, that it is being used by @smowton?

No, we're using analysis/static_analysis.h, which is apparently unrelated.

peterschrammel · 2018-04-08T17:39:17Z

src/util/memory_limit.h

-\*******************************************************************/
-
-#ifndef CPROVER_UTIL_MEMORY_LIMIT_H
-#define CPROVER_UTIL_MEMORY_LIMIT_H


This is used by TG. We can move it there if you want to remove it from this repo.

The code isn't portable so it might make sense to move it? I don't have very strong feelings about it, but given that the code can't be tested in this repository I'd prefer to move it to a place where it is being tested.

Moved to #2214.

peterschrammel · 2018-04-08T17:51:47Z

src/solvers/prop/prop.h

@@ -17,11 +17,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/threeval.h>

-#include "prop_assignment.h"


literal.h needs to be included here

thk123 · 2018-04-09T09:40:14Z

unit/testing-utils/c_to_expr.cpp

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


This is OK to go

thk123 · 2018-04-09T09:41:44Z

unit/testing-utils/require_expr.cpp

-
-#include "require_expr.h"
-
-#include <testing-utils/catch.hpp>


These are used extensively in unit tests for the TG module. I'm happy to migrate these into TG, however for writing unit tests validating exprts, they are very useful for keeping tests succinct. If we want to expand unit tests in CBMC I suggest keeping them about.

Actually I had been looking at a not-up-to-date version of the tree: since 2348d10 require_expr.h is being used here as well, so we're good.

thk123 · 2018-04-09T09:45:35Z

Will create a TG pointer bump to verify the other reverts don't have an effect once you've lmk what you want to do re: require_expr

smowton · 2018-04-09T11:19:47Z

@tautschnig I can't see any of my commits reverted here, do you know which ones you were thinking of?

mgudemann · 2018-04-10T06:32:02Z

@tautschnig do you want to to test this with EBMC? I also didn't see one of my commits being reverted.

tautschnig · 2018-04-10T09:22:23Z

@smowton: It looks like infix.h was yours. Will do a proper revert in the next update of this PR.
@mgudemann: No, none of your commits were reverted, but I hoped you could commend on vcd_goto_tracet and get_modules.

smowton · 2018-04-10T09:29:15Z

@tautschnig aha, we do use has_infix in the security repo.

tautschnig · 2018-04-10T09:36:22Z

aha, we do use has_infix in the security repo.

Does that actually improve the code in some way (readability or some other sort of clarity)? Since I don't know your code, I need your guidance on this.

smowton · 2018-04-10T10:17:22Z

Sure, a little -- it's a shorthand for "string b occurs at offset i in string a", like has_prefix and has_suffix.

mgudemann · 2018-04-10T12:05:57Z

src/util/substitute.h

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


substitute is used in TG

Is there a reason not to use std::replace?

Edit: is TG actually using it for substring replacement?

Edit 2: if this is seriously being used, then at least a more efficient implementation should be built. Repeatedly searching from the beginning isn't optimal.

Yup 6 instances in TG that look like can be easily replaced to std::replace - will post here once that fix has been applied

Moved to #2214.

mgudemann · 2018-04-11T14:12:21Z

src/util/find_macros.h

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


find_macros.h is used in EBMC

Moved to #2213 to receive your separate approval/further discussion.

mgudemann · 2018-04-11T14:12:45Z

src/util/get_module.h

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


get_module is used in EBMC

mgudemann · 2018-04-11T14:13:13Z

src/util/preprocessor.h

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


preprocessor is used in EBMC

mgudemann · 2018-04-11T14:14:27Z

@tautschnig I searched in EBMC for occurrences of files deleted in your PR and found the above. I haven't yet put in the time / work to get EBMC to compile with current CBMC/develop though

tautschnig · 2018-04-11T15:58:27Z

@mgudemann Many thanks for checking. Are there reasons why moving them to EBMC would not be the right thing to do?

mgudemann · 2018-04-11T16:10:48Z

@tautschnig not from my side, could be moved to EBMC @kroening what is your opinion on this?

…

On 11 April 2018 at 17:58, Michael Tautschnig ***@***.***> wrote: @mgudemann <https://github.com/mgudemann> Many thanks for checking. Are there reasons why moving them to EBMC would not be the right thing to do? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#2019 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACeHTK8cHhiZmh3CPYsVhkqlaY_Xbekgks5tnigjgaJpZM4TLgrx> .

tautschnig · 2018-04-27T10:01:49Z

I've found some more unused code, but that requires merging #2128 first (hence this won't build for the moment).

tautschnig · 2018-05-21T11:57:11Z

I have moved all those parts that have raised concerns to separate PRs as indicated.
I have split up commits so that each of the remaining ones will only remove one module at a time, and should thus be reverted rather easily if a previously unknown use case arises.

mgudemann · 2018-06-01T10:50:21Z

@tautschnig I'd say go with removing, we can move the required modules to EBMC

This reverts commit 3185028. Removing a class that was never used; unit/analyses/ai/ai_simplify_lhs.cpp shows how to do the parsing without any helper.

This reverts commit f29ca0c.

This reverts commit 38642cd.

Partly reverts 055f515.

This interface only has a single implementation.

It has been deprecated (and was no longer being built) in e936c50.

This interface was just used once.

allredj

Passed Diffblue compatibility checks (cbmc commit: 471b20f).

peterschrammel

No objections

e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and smowton as code owners April 8, 2018 11:56

tautschnig assigned smowton, thk123, kroening, mgudemann and peterschrammel Apr 8, 2018

peterschrammel reviewed Apr 8, 2018

View reviewed changes

thk123 reviewed Apr 9, 2018

View reviewed changes

tautschnig force-pushed the remove-unused branch from 8f05ee7 to bfd7920 Compare April 9, 2018 18:27

tautschnig force-pushed the remove-unused branch from bfd7920 to 4296099 Compare April 10, 2018 09:26

tautschnig force-pushed the remove-unused branch from 4296099 to 41d1de1 Compare April 10, 2018 11:34

tautschnig unassigned smowton and thk123 Apr 10, 2018

mgudemann suggested changes Apr 10, 2018

View reviewed changes

mgudemann suggested changes Apr 11, 2018

View reviewed changes

tautschnig mentioned this pull request Apr 13, 2018

Memory regression test [blocks: #2035] #1971

Closed

tautschnig force-pushed the remove-unused branch from 41d1de1 to bb2794b Compare April 27, 2018 09:59

tautschnig self-assigned this Apr 27, 2018

tautschnig force-pushed the remove-unused branch from bb2794b to 70da03f Compare April 29, 2018 18:11

tautschnig removed their assignment Apr 29, 2018

kroening mentioned this pull request May 19, 2018

remove basic_blocks and goto_program_irep #2208

Merged

tautschnig force-pushed the remove-unused branch from 70da03f to 56823a4 Compare May 21, 2018 11:54

mgudemann approved these changes Jun 1, 2018

View reviewed changes

tautschnig unassigned mgudemann Jun 13, 2018

tautschnig force-pushed the remove-unused branch from 56823a4 to 48ad4a7 Compare June 13, 2018 23:18

tautschnig and others added 11 commits June 14, 2018 07:57

Revert "Added utility class to convert strings into expressions"

3fb06ba

This reverts commit 3185028. Removing a class that was never used; unit/analyses/ai/ai_simplify_lhs.cpp shows how to do the parsing without any helper.

Revert "new exception class"

2696420

This reverts commit f29ca0c.

Revert "added pipe_stream class"

4d4c9c6

This reverts commit 38642cd.

Remove unused sorted_vector.h

71cfbbd

Remove unused cpp/recursion_counter.h

a4936f8

Remove unused nondet_ifthenelse.{h,cpp}

d350e5c

Partly reverts 055f515.

Remove path_accelerationt interface

2260f82

This interface only has a single implementation.

Remove unused goto-analyzer/static_analyzer.{h,cpp}

ae56978

It has been deprecated (and was no longer being built) in e936c50.

Remove unused solver/prop/prop_wrapper.h

502687e

Remove unused solvers/prop/prop_conv_store.{h,cpp}

2639cf1

Remove prop_assignmentt interface

471b20f

This interface was just used once.

tautschnig force-pushed the remove-unused branch from 48ad4a7 to 471b20f Compare June 14, 2018 07:57

allredj reviewed Jun 14, 2018

View reviewed changes

peterschrammel approved these changes Jun 14, 2018

View reviewed changes

tautschnig merged commit b71efaf into diffblue:develop Jun 14, 2018

tautschnig deleted the remove-unused branch June 14, 2018 11:39


		#include <analyses/interval_domain.h>

		class static_analyzert:public messaget

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

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

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

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

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

Remove utilities that never got used #2019

Remove utilities that never got used #2019

Conversation

tautschnig commented Apr 8, 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

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 Apr 9, 2018

smowton commented Apr 9, 2018

mgudemann commented Apr 10, 2018

tautschnig commented Apr 10, 2018

smowton commented Apr 10, 2018

tautschnig commented Apr 10, 2018

smowton commented Apr 10, 2018

Choose a reason for hiding this comment

tautschnig Apr 10, 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

mgudemann commented Apr 11, 2018

tautschnig commented Apr 11, 2018

mgudemann commented Apr 11, 2018 via email

tautschnig commented Apr 27, 2018

tautschnig commented May 21, 2018

mgudemann commented Jun 1, 2018

allredj left a comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

tautschnig Apr 10, 2018 •

edited

Loading