Clean Const Function Pointer Removal #519

thk123 · 2017-02-09T15:40:06Z

A fairly naive approach to optimising function pointers in some specific common cases. If a function pointer is:

constant and assigned from one of:
directly from a function symbol
assigned to a constant FP
a component of a const struct
an element in a constant array *
A constant pointer pointing to something
Or some combination of the above

We replace it with either a direct function call, or generate the list of actually possible functions. This is opposed to generating a list of all functions with valid signatures.

There was a rough version of this in #434, this takes the same idea, splits it out in to a separate class. It also deals with more cases and should be more robust to chaining of weird things. I have also renamed the large body of tests from fp-removal1,...fp-removal45 to meaningful names describing what they test.

Issues: diffblue/cbmc-toyota#12 [private]
This also includes the improvments outlined in #476

thk123 · 2017-02-09T15:45:51Z

There are a bunch of commits relating to the old test names, I could just remove them, but there may be some useful notes in the commit messages, so I think I will just bulk squash them even though the files they relate to don't exist in the final commit. Particularly in light of the fact git has picked it up as a rename.

Other things I am aware of before this PR is ready for merge:

I also will go through the tests and make sure they are consistent with each other.
Make sure all structs have two components in it since that caused multiple bugs.
Splitting up the two big functions in remove_const_function_pointers.cpp (as done with the ID_index case)

There is also a reasonable amount of duplication between resolve_expression and resolve_function_call. In fact, the main difference is what it does with the results. I imagine there is a way of extracting the common stuff in to the resolve_expression and have the resolve_function_call use this.

thk123 · 2017-02-10T11:52:50Z

This currently isn't building due to a compile error in musketeer, investigating.

thk123 · 2017-02-10T17:30:58Z

@martin-cs raised an issue (#524) about dealing with null pointers. There is a flag called "--pointer-check" which will add an assertion after the IFs in case it didn't match any. To validate this works correctly with my tests I should:

Add the flag to all the tests
The tests with null having the correct handling
Adding some tests for the different ways the FP can be assigned null:
- Direct assignment to null pointer
- Assignment to array with null pointer but with literal
- Assignment to struct with null pointer
- Null pointer to FP
- Nul pointer to struct
- Indirect assignment to null pointer

tautschnig · 2017-02-11T07:08:18Z

src/goto-programs/Makefile

@@ -19,6 +19,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \
      slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \
      show_goto_functions_json.cpp \
+      remove_const_function_pointers.cpp \


Cf the discussion on coding guidelines: your insertion point is a random one (which is fine at present), but for the principle of least surprise there should be a canonical insertion point.

tautschnig · 2017-02-11T07:11:23Z

src/goto-programs/remove_const_function_pointers.h

+class remove_const_function_pointerst:public messaget
+{
+public:
+  typedef std::set<exprt> functionst;


Is there a reason for it not to be a std::unordered_set?

I didn't think there was but having changed it, I can think of a reason, though I don't know if it qualifies as good: the tests have to become a lot less precise as the ordering of the functions is no longer deterministic.

I'd suggestion one of two options here: 1) the tests really shouldn't be depending on ordering, thus try to adjust the tests; 2) or add a comment saying that using std::set simplifies testing.

Well I had thought it was required to make the tests actually test anything, but actually checking for the existence of the goto in the no-match and approx cases will test to the same precision so I will do that.

Ah no I realise where this will cause problems - in the approx tests as they will pass even if no match. They can however be fixed without ordering by adding the cases that shouldn't be generated to the exclude lines.

tautschnig · 2017-02-11T07:11:36Z

src/goto-programs/remove_const_function_pointers.h

+  bool try_resolve_typecast_function_call(
+    const typecast_exprt &typecast_expr, functionst &out_functions);
+
+  // recursive functions for dealing with the auxillary elements


Typo: "auxillary" -> auxiliary

tautschnig · 2017-02-11T07:12:12Z

src/goto-programs/remove_const_function_pointers.h

+    bool &out_is_const);
+
+  bool is_expression_const(const exprt &expression);
+  bool is_type_const(const typet &type);


Likely those two functions should be marked const? Also, is_const_expression, is_const_type would seem more consistent (e.g., replace_const_symbol).

tautschnig · 2017-02-11T07:12:16Z

src/goto-programs/remove_function_pointers.cpp


 #include <ansi-c/c_types.h>

 #include "remove_skip.h"
 #include "remove_function_pointers.h"
 #include "compute_called_functions.h"
+#include <goto-programs/remove_const_function_pointers.h>


Use #include "remove_const_function_pointers.h" for consistency with the preceding ones.

tautschnig · 2017-02-11T07:12:22Z

src/goto-programs/remove_function_pointers.cpp

+  bool found_functions=fpr(functions);
+
+  // Consistency checks
+  if(found_functions && functions.size()==0)


functions.empty() (.size() is linear time, even in C++11 I believe)

For std::set/std::unordered_set (which is was functions is) size() is constant time. None the less, I think empty() expresses the check clearer so I will do this.

tautschnig · 2017-02-11T07:12:26Z

src/goto-programs/remove_function_pointers.cpp


-  bool return_value_used=code.lhs().is_not_nil();
+  if(functions.size()==1)


Hmm, ok, if you need the actual size: maybe just compute it once.

tautschnig

See comments plus the remaining quest for test cases.

thk123 · 2017-02-13T14:43:16Z

@tautschnig Addressed your feedback (including the unordered set)
@martin-cs I've adjusted and added tests for dealing with null pointers through the use of --pointer-check but the code hasn't changed (well apart from adding support in goto-analyze for --pointer-check), so for this to fix your problem you'll need to run goto-analyze with --pointer-check.

thk123 · 2017-02-13T14:44:56Z

Before merging, there is an issue diffblue/cbmc-toyota#27 to add a flag to activate this FP removal mode only, which is probably small enough to just be part of this PR.

thk123 · 2017-02-13T15:47:45Z

Note: before merging fix the approx-* tests: #519 (comment)

tautschnig · 2017-02-13T16:22:16Z

I'm going to take a look at the entire PR, but would then wonder whether some squashing should be applied.

thk123 · 2017-02-13T16:48:04Z

Resolved the extra flag, fixed the approx tests to work without the ordering so I think this is good for a final review.

@tautschnig I've tried to squash as much as I can. However, all the further squashing I could think of became very fiddly and time consuming to apply. As such I abandoned it as I didn't think it was worth the time it would take. For example, renaming the is_expr_const -> is_const_expr, new calls get added in multiple commits so each would have to be edited.

I've just spotted master is building again so will rebase to check this branch builds.

tautschnig

Almost all about typos (in comments), except the concern that there is no check whether a const expression has genuinely never been changed.

tautschnig · 2017-02-13T17:48:13Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -790,6 +791,39 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(

 /*******************************************************************\

+Function: goto_instrument_parse_optionst::do_remove_const_fps_only


Comment name does not coincide with the action function name.

tautschnig · 2017-02-13T17:50:51Z

src/goto-programs/remove_const_function_pointers.cpp

+Function: remove_const_function_pointerst::operator()
+
+  Inputs:
+   out_functions - The functions that (symbols of type ID_code)


The functions that ... what?

tautschnig · 2017-02-13T17:51:31Z

src/goto-programs/remove_const_function_pointers.cpp

+
+ Outputs: Returns true if it was able to resolve the call, false if not.
+          If it returns true, out_functions will be populated by all the
+          possible values the funciton pointer could be.


Typo: funciton -> function

tautschnig · 2017-02-13T17:52:11Z

src/goto-programs/remove_const_function_pointers.cpp

+bool remove_const_function_pointerst::operator()(
+  functionst &out_functions)
+{
+  // Replace all const symbols with there values


Typo: there -> their

tautschnig · 2017-02-13T17:52:50Z

src/goto-programs/remove_const_function_pointers.cpp

+  Inputs:
+   expression - The expression to resolve symbols in
+
+ Outputs: Returns the a modified version of the expression, with all


"the" or "a", but not "the a"

tautschnig · 2017-02-13T17:57:36Z

src/goto-programs/remove_const_function_pointers.cpp

+        symbol_table.lookup(expression.get(ID_identifier));
+      if(symbol.type.id()!=ID_code)
+      {
+        const exprt &symbol_value=symbol.value;


So how do we catch cases where the value has been overwritten (consider a const casted away)?

So the answer here is we don't. No attempt is made to validate that const-ness has been respected.

I initially believed that we didn't need to worry at all about UB and that if the code was doing something illegal, it was acceptable to not worry about it. However, since discussion about null pointers (#524), I am less certain.

Ultimately, I don't have enough knowledge to make a judgement on this. I was under the impression that we can't easily validate the const-ness before first resolving the FPs resulting in a chicken/egg problem. Unfortunately @martin-cs is away this week, perhaps @danpoe knows more?

@tautschnig @danpoe has suggested as a simple fix for getting this done without introducing a gap we scan the GOTO program for any casts of FPs that remove const-ness and if any are found, we abandon removing FPs in this way. That way for the majority of code that doesn't cast away const-ness we can still make the improvement without having todo anything too arduous but we are still correct if there is such a cast and it matters.

That certainly is a good option. There might be gaps, but it would yield a defined point for inserting additional sanity checks.

tautschnig · 2017-02-13T17:58:34Z

src/goto-programs/remove_const_function_pointers.cpp

+
+  Inputs:
+   expr - The expression to get the possible function calls
+   out_functions - The functions this expression could be


is there a "calling" missing at the end?

I don't think so - the expression is what is being called rather than doing the calling. I've replaced it with

the functions this expression could be resolved to

Is that clearer?

tautschnig · 2017-02-13T17:58:54Z

src/goto-programs/remove_const_function_pointers.cpp

+   out_functions - The functions this expression could be
+
+ Outputs: Returns true if it was able to resolve the expression to some
+          specific functions. If this is the case, out_functinos will contain


Typo: out_functinos -> out_functions

tautschnig · 2017-02-13T18:03:42Z

src/goto-programs/remove_const_function_pointers.cpp

+Function: remove_const_function_pointerst::try_resolve_index_of_function_call
+
+  Inputs:
+   index_expr - The index expression to  to resolve to possible function calls


tautschnig · 2017-02-13T18:16:54Z

src/goto-programs/remove_function_pointers.cpp

+  // subset of possible functions and just leave the function pointer
+  // as it is.
+  // This can be activated in goto-instrument using --remove-const-fps
+  // instead of remove--function-pointers


That's the "--" in the wrong place.

thk123 · 2017-02-14T11:34:26Z

@tautschnig Apart from the question re: modifying const variables I believe I have addressed all of your feedback. We may have to wait till next week to resolve the const problem unfortunately.

Apologies for all the typos and spelling mistakes, I am investigating how I can turn on a spell checker in my IDE since these are just as annoying for reviewers as linting errors!

tautschnig · 2017-02-14T14:57:03Z

@thk123 Thanks a lot for the incredibly quick turnarounds on all change requests! I do agree that all questions are addressed, with the exception of the const-ness check. It would be great to have that included.

thk123 · 2017-02-16T14:14:19Z

@tautschnig I have added a check for when the code contains a cast away from const and some tests to verify it. It could probably do with a more experienced eye in case I've missed a case as I wasn't sure about the way of checking the expression tree. Commit: 97668a4

thk123 · 2017-02-16T18:11:04Z

Tests are failing again for some reason, I'm sure they passed locally. It looks to be something to do with the test.pl change - the output looks fine.

forejtv · 2017-02-17T11:21:27Z

https://github.com/diffblue/cbmc/blob/150e353ab00bca829404a38de8a5f107e7decbaa/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc has unescaped ( and ). I guess the other failing tests will have similar problems.

thk123 · 2017-02-17T12:48:23Z

Rebased to fix the linting issues.
@forejtv Fixed the build issues (they were in a different folder to the one I had fixed) so should pass this time, just waiting on that and a review from @tautschnig on the new changes (97668a4)

resolve_index_of and resolve_index_of_function_call both involved squashing down an array, the function call just made a different recurssive call at the end. Therefore it is equivalent to squash the entry and call the resolve function call on the final result.

Rather than sometimes using the array directly, other times checking it, use and having lots of exit points to the function, all steps use same interface and work in the same way with arrays.

To handle the cases where the function pointer is null, we enable the pointer--check flag. This asserts that one of the branches is taken (e.g. a valid function pointer). This wasn't supported by goto-analyze so added the option to it.

Modified the tests to not assume the order of the functions. For precise tests no further changes are required since if the removal failed, there will be a label before the call to be jumped to. For the no-match tests, no further changes are required since the goto statements are being verified to be all the there. For the approx tests, we need to verify that the other case statements aren't present in the GOTO program to be sure that the FP removal has been successful. As such, the other case statements are added to the exclude section.

Added a flag --remove-const-function-pointers for goto-instrument that can be used instead of --remove-function-pointers to only remove function pointers where we can resolve to something more precise that all functions with a matching signature.

Before removing const function pointers using remove_const_function_pointerst we check each instruction in the goto program for assigns where the RHS is more const than the LHS. This includes both implicit and explicit casting away of const. If this has happened to something relating to a function pointer, then our optimization is not sound, so if we find any we just abandon this optimization. This is acceptable since it is undefined behavior anyway to be modifying a const variable.

Added test for run time const arrays. Adding test case for pointer to struct

The new test.pl script requrires breaks to be escaped.

Created a standalone class to check whether a prgram contains a cast that loses the const-ness of something that would allow modifying a constant value (i.e. undefinied behaviour).

When we are checking for loss of const qualifiers, we need to check all children that are the same basic type to see if their qualification is lost in their parent.

Simplifying assert Simplify and reducing indentation by changing if branches with trivial else clauses into checking them first and bailing if condition not met. Corrected use of reference

To avoid unnecessary temporary objects, use a pointer when checking for const preservation. Note we now need to compare the ID against NIL rather than the empty string since the non-const version of subtype returns a new irept with no id, but the const version returns the nil data structure.

thk123 · 2017-03-24T10:34:42Z

@tautschnig Fixed whitespace as requested - this I believe is good to go.

tautschnig · 2017-03-24T14:53:53Z

Assigned to @kroening for final review and merging.

SEC-562: Smowton/merge/20180730

…6357 240236357 Merge pull request diffblue#581 from diffblue/forejtv/simpler-file 8ef53a50a simplified constructor for java.io.File d1c08d982 Put non-simple File.java into simple models 13c22a856 Merge pull request diffblue#578 from diffblue/jeannie/UpdateDTUversion 39202a4e5 Merge pull request diffblue#577 from diffblue/allredj/complete-linked-list-documentation 2d94c7b47 Update deeptest-utils version. ab300bbe2 Complete documentation of LinkedList 4f77b90dd Merge pull request diffblue#544 from diffblue/collections-reverse e78b7f02c Tests for Collections model 137622bcf Model for java/util/Collections 422197c51 Added java/util/Collections 33c1410b9 Merge pull request diffblue#576 from diffblue/smowton/admin/increase-to-depth-1600 85000a8ac Bump depth to 1600 927fef36d Merge pull request diffblue#571 from diffblue/zgoriely/linked-list-basic 8621e0d71 Addressing reviewer comments 46376144c Add tests for LinkedList methods e4782ab96 Implement model for remaining basic LinkedList methods 0a32c4de5 Merge pull request diffblue#566 from diffblue/zgoriely/linked-list 7cc397a82 Add tests for new methods e86ade7cb Implement methods for LinkedList 6fe84d51a Merge pull request diffblue#569 from diffblue/allredj/update-dtu-131 7bf5a1a80 Update DeepTestUtils to 1.3.1 9df72dd93 Merge pull request diffblue#560 from diffblue/zgoriely/arrays-simple-equals 78228133b Re-enable tests depending on Arrays.equals b011e0cf5 Add Tests for Simple Arrays.equals 1a76bd166 Implement Simple Model for Arrays.equals 4d14a9a57 Merge pull request diffblue#543 from diffblue/linked-list-add-all 27c9f5da6 Merge pull request diffblue#562 from diffblue/zgoriely/arrays-equals-fix b19e50c71 Tests for LinkedList init(c)|addAll(c) 394db6890 Modelled java/util/LinkedList.(<init>(Collection)|addAll) 950aae85c Merge pull request diffblue#565 from diffblue/zgoriely/hashset-fix 534a85708 Arrays Equals Model fix - Double and Float 74fa617b8 Fixing HashSet.addAll method dac4774ce Merge pull request diffblue#542 from diffblue/java-util-optional 396f52c45 Tests for Optional model d11e8faed Tidying Optional Model 3f8e7e19f Modelled java/util/Optional and java/util/function/(Supplier|Consumer) 8db4ad90e Emptied java/util/Optional and java/util/function/(Supplier|Consumer) 4c3781871 Added java/util/Optional and java/util/function/(Supplier|Consumer) a6cbe0c51 Merge pull request diffblue#564 from diffblue/zgoriely/arrays-comparator-fix ab7638920 Fix for Comparator sort test-gen failure 13218fec0 Merge pull request diffblue#545 from diffblue/arrays-sort bd27eeac1 Fixing up tags in Base64 Models 14f7cda29 Tests for Arrays.sort 8c4c1c524 Model java/util/Arrays.sort edefabb77 Empty java/util/Comparator 5c39ba9e2 Add java/util/Comparator 941eefa80 Merge pull request diffblue#563 from diffblue/allredj/travis-housekeeping 996c4aab8 Travis: Don't save html report 37640904c Travis: install gauge html-report 72330e6ce Linting 3a97f9fa5 Travis: Remove unneeded addon installs c6d77308b Merge pull request diffblue#556 from diffblue/allredj/update-modeltests-gitignore 11409e1aa Merge pull request diffblue#375 from diffblue/jeannie/setTimeZoneAndOthers 6b4808330 Update .class files 7deac9024 Tag all failing tests with appropriate ticket no. c832fba9b Mock Calendar and fix some things in the model 726558344 Re-enable fastTime field in Date model e5f994525 Updates CProver.nondet methods for not modelled functions. d43a366cf Updates documentation in javadocs for java.util.Date e65c0f6aa Tests java.text.SimpleDateFormat 798fd0b5e Models java.text.SimpleDateFormat 0499abc91 Models java.text.DateFormat getTimeZone() and setTimeZone() 6d96405f7 Marks all methods as notModelled() in Format classes 477fcc92d Initial commit for java.text.Format, DateFormat and SimpleDateFormat models. efd6fe8e3 Tests java.util.GregorianCalendar e4e0d40ff Tests java.util.Calendar b87c250f8 Models java.util.GregorianCalendar() e03f25170 Marks all methods as notModelled() for java.util.GregorianCalendar ce2549199 Initial commit for java.util.GregorianCalendar 9d85399fa Models java.util.Calendar d0d31e9ed Marks all methods as notModelled() in java.util.Calendar 71d877078 Initial commit for java.util.Calendar 149aa4da6 Models ZoneInfo getRawOffset() and uses it for getOffset() 8d9a9ac67 Merge pull request diffblue#561 from diffblue/zgoriely/model-test-generator-improvement 0a7e92e0d Fixing a couple bugs in model test generator 7ce6d62a9 Merge pull request diffblue#558 from diffblue/antonia/appendable-annotation 562ffb424 Merge pull request diffblue#559 from diffblue/antonia/enable-TG-3905-tests e32331aa9 Merge pull request diffblue#555 from diffblue/zgoriely/arrays-fill 4d1111fa6 Enable tests for TG-3905 fb5308932 Move Appendable test to appropriate folder 2149e3ad8 Pick StringBuilder as an Appendable implementation 9b2a4a30a Arrays fill model 1fcddca3f Merge pull request diffblue#557 from diffblue/zgoriely/arrays-equals 0ef93d6dd Updated test class names and test method names c037628e6 Re-Enabling tests that rely on Arrays.equals 8329b761d Merge pull request diffblue#541 from diffblue/emptier-script bc31d0bdf Merge pull request diffblue#551 from diffblue/zgoriely/arrays-equals f9f914b8f Update modelTests .gitignore 8469f6c28 Tests for Arrays.equals methods 2eef3d595 Model for Arrays.equals methods bf7b6f191 Merge pull request diffblue#550 from diffblue/cesaro/java-sync-fix 1a93b39d5 Re-enable tests in PushbackReader.spec, see e21b471 dd8689737 Merge pull request diffblue#547 from diffblue/svorenova/enable_tests_tg3514 5fd67cde8 Use Gauge tear-down steps e1b2b5241 Update ticket number for disabled tests for mocking with inheritance 9ee355cd5 Merge pull request diffblue#554 from diffblue/allredj/travis-use-obfuscated-build 5fee9930a Use obfuscated test-gen build in models-library 7502e471d Merge pull request diffblue#540 from diffblue/java-concurrency-synchronization-models e21b471ab Temporary disabled a number of tests in 'PushbackReader.spec' 7f1eb804d Emptier script d0b941b83 Changes to support PR cbmc#2280 5915ce44d Merge pull request diffblue#536 from diffblue/antonia/unnecessary-gauge-steps e8b4888f9 Merge pull request diffblue#538 from diffblue/bugfix/TG-1888/put-tests-in-appropriate-packages 8fd5af6eb Tidy up Verify steps in spec files da8b4ac38 Don't use java or javax packages 4ec167eec Adding test for checking getPackageFromMethod 91ea20ce3 Put tests in to the package that the function under test is in 6e6b59698 Merge pull request diffblue#533 from diffblue/allredj/testrunner-start-with-unwind-2 57b73a8b0 Merge pull request diffblue#504 from diffblue/forejtv/simple-base64 8907ffd20 Simplified model for Base64 8d521d65d Skip some tests that fail due to TG-3981 35621a7e9 Merge pull request diffblue#530 from diffblue/romain/string-init-charset efebf5cec Use CProverString.substring d929a005f Use a reversible version of getBytes c1e020c3d Add test for constructor from byte[] and charset 07004ec1b Model for String constructor from byte[], charset 136326682 Use equality on name for charsets e45df98d0 Use CProverString.equals instead of == 61c713714 Define a CProverString.equals function c0ef4fe7d Merge pull request diffblue#519 from diffblue/allredj/linkedhashset 338a1cdfc Merge pull request diffblue#528 from diffblue/allredj/simple-linkedhashset cf1f27e96 Added original model for Base64 8676ea6b5 Merge pull request diffblue#535 from diffblue/antonia/stringreader-optimisations 0f051858c Tests for LinkedHashSet (simple model) d964fa763 Make HashSet fields package-private (simple model) beaf7d1bf Simple model for LinkedHashSet 01e2b787c Import LinkedHashSet.java from JDK 400db2ba0 Add missing Diffblue Javadoc tags f50914877 Use more efficient charAt in StringReader 6a60301b0 Clarify differences from JDK StringReader c95f30f27 Load a StringReader when loading PushbackReader 8290e5b13 Start generating tests with unwind 2 8861b24f1 Tests for LinkedHashSet 81ca53b05 Model for LinkedHashSet 5d9420c1d Import LinkedHashSet.java from JDK 4e22d539b TestRunner: Factor out debug output 9616e1769 Merge pull request diffblue#531 from diffblue/romain/nondet-initialize-file 8553bf0e5 Activate cproverNondetInitialize for file c0d1c05dc Merge pull request diffblue#532 from diffblue/allredj/fix-stringbuffer-append 71e3b0788 Merge pull request diffblue#534 from diffblue/allredj/use-fornotmodelled-in-simple-models-2 c0f10640b Merge pull request #529 from diffblue/jeannie/TestRunnerImportsUpdate 65b68beeb Merge pull request diffblue#516 from diffblue/allredj/exhibit-mocking-bug-with-inheritance 2588b96c0 Use appropriate header for tests. fc3f1c53a Use short name for annotation in TestRunner. 0e9da3a50 Avoid using nondet statements where possible a20e778b4 Build modelling utils with "package" 753eea477 Copy over cprover package from standard models 67199cdb2 Fix StringBuffer.append 3f2ac3406 Disable tests that suffer from TG-3514 d2dabe327 Make tests sensitive to mocking problems 532d146f3 Merge pull request diffblue#515 from diffblue/antonia/implement-annotation 0048a020c Add tests for classes given in annotations 2e6182b10 Annotate common abstract classes 39f6d72f4 Add java.lang.Appendable interface bc383f3b2 Add java.io.Flushable interface 83dffab13 Add java.lang.AutoCloseable interface 18bd2e55b Add java.io.Closeable interface f37ca90df Add java.lang.Readable interface a8369c332 Add implementation annotation to simple models d06449814 Show "Preferred..." annotations in Javadoc git-subtree-dir: benchmarks/LIBRARIES/models git-subtree-split: 240236357fc9fb1cb87bf5adacaa1b27786ff84b

thk123 force-pushed the feature/clean-fp-removal branch from e271353 to a602fd4 Compare February 9, 2017 17:49

thk123 mentioned this pull request Feb 9, 2017

Optimisations in generated code with function pointers #434

Closed

thk123 force-pushed the feature/clean-fp-removal branch from daeaed9 to 9be7020 Compare February 10, 2017 18:02

tautschnig reviewed Feb 11, 2017

View reviewed changes

tautschnig requested changes Feb 13, 2017

View reviewed changes

tautschnig assigned thk123 Feb 13, 2017

thk123 force-pushed the feature/clean-fp-removal branch from 380ddf0 to c796211 Compare February 13, 2017 14:40

thk123 force-pushed the feature/clean-fp-removal branch 2 times, most recently from 82bea9b to cbd8454 Compare February 13, 2017 16:43

thk123 force-pushed the feature/clean-fp-removal branch from cbd8454 to eb7a4b5 Compare February 13, 2017 16:51

tautschnig requested changes Feb 13, 2017

View reviewed changes

thk123 force-pushed the feature/clean-fp-removal branch from eb7a4b5 to cae911c Compare February 14, 2017 11:33

thk123 force-pushed the feature/clean-fp-removal branch from cae911c to 150e353 Compare February 16, 2017 14:10

thk123 force-pushed the feature/clean-fp-removal branch 2 times, most recently from 26375b4 to 4730afb Compare February 17, 2017 12:46

forejtv unassigned thk123 Feb 17, 2017

thk123 and others added 19 commits March 24, 2017 10:33

Split out functions from try_resolve_function_call

6298fea

Made the behaviour of try_resolve_function_call clearer

5d33d4d

Rather than sometimes using the array directly, other times checking it, use and having lots of exit points to the function, all steps use same interface and work in the same way with arrays.

Split up try_resolve_expression into functions

a75957b

Made other try_resolve*_function_call use the normal method

37660b1

Extracted element dealing with calling resolve on each result

8362233

Adding the pointer check flag

e57677e

To handle the cases where the function pointer is null, we enable the pointer--check flag. This asserts that one of the branches is taken (e.g. a valid function pointer). This wasn't supported by goto-analyze so added the option to it.

Adding checks for NULL function pointers

0de6b17

Renaming functions to more consistent name

10a08ef

Added a couple of missed test cases.

6ba0469

Added test for run time const arrays. Adding test case for pointer to struct

Fixing tests to work with new test.pl

18b5907

The new test.pl script requrires breaks to be escaped.

Fixing missing new lines

2538f4f

Split out the const check into own analysis

29e7e0d

Created a standalone class to check whether a prgram contains a cast that loses the const-ness of something that would allow modifying a constant value (i.e. undefinied behaviour).

Descend all children of the same base type

649e0bf

When we are checking for loss of const qualifiers, we need to check all children that are the same basic type to see if their qualification is lost in their parent.

PR Feedback implementation

4607e73

Simplifying assert Simplify and reducing indentation by changing if branches with trivial else clauses into checking them first and bailing if condition not met. Corrected use of reference

thk123 force-pushed the feature/clean-fp-removal branch from a7f9c97 to d7c15ae Compare March 24, 2017 10:33

tautschnig assigned kroening and unassigned thk123 Mar 24, 2017

kroening merged commit fae3cd8 into diffblue:master Apr 4, 2017

thk123 deleted the feature/clean-fp-removal branch April 4, 2017 15:42

thk123 mentioned this pull request May 12, 2017

[depends: #708] Adding tests that check that simplify removes statements generated by FP removal #915

Closed

NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Aug 22, 2018

Merge pull request diffblue#519 from diffblue/smowton/merge/20180730

30dc0d0

SEC-562: Smowton/merge/20180730


		bool return_value_used=code.lhs().is_not_nil();
		if(functions.size()==1)

		@@ -790,6 +791,39 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(

		/*******************************************************************\

		Function: goto_instrument_parse_optionst::do_remove_const_fps_only

Clean Const Function Pointer Removal #519

Clean Const Function Pointer Removal #519

Conversation

thk123 commented Feb 9, 2017 • edited Loading

thk123 commented Feb 9, 2017 • edited Loading

thk123 commented Feb 10, 2017

thk123 commented Feb 10, 2017 • 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

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

tautschnig left a comment

Choose a reason for hiding this comment

thk123 commented Feb 13, 2017

thk123 commented Feb 13, 2017

thk123 commented Feb 13, 2017

tautschnig commented Feb 13, 2017

thk123 commented Feb 13, 2017 • edited Loading

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Feb 14, 2017

tautschnig commented Feb 14, 2017

thk123 commented Feb 16, 2017 • edited Loading

thk123 commented Feb 16, 2017

forejtv commented Feb 17, 2017

thk123 commented Feb 17, 2017 • edited Loading

thk123 commented Mar 24, 2017

tautschnig commented Mar 24, 2017

thk123 commented Feb 9, 2017 •

edited

Loading

thk123 commented Feb 9, 2017 •

edited

Loading

thk123 commented Feb 10, 2017 •

edited

Loading

thk123 commented Feb 13, 2017 •

edited

Loading

thk123 commented Feb 16, 2017 •

edited

Loading

thk123 commented Feb 17, 2017 •

edited

Loading