Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Split the entry-point-generation phase into two parts #1394

Merged

Conversation

smowton
Copy link
Contributor

@smowton smowton commented Sep 15, 2017

The new generate_support_functions phase creates __CPROVER_start and __CPROVER_initialize and runs before lazy loading; the final phase will run after lazy loading, and is therefore used to patch up changes that require functions' bodies to have been loaded already.

In subsequent PRs, lazy loading will take advantage of this to read __CPROVER_start and use it to guide its work; CI-lazy-loading will use it to replace its current hackish logic to guess how globals and parameters will be initialised.

Copy link
Contributor

@reuk reuk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Virtual methods used to customize behavior should generally be private.

/// complete. Functions introduced here are visible to lazy loading and
/// can influence its decisions (e.g. picking the types of input parameters
/// and globals), whereas anything introduced during `final` cannot.
virtual bool generate_support_functions(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should probably be private.

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems reasonable - some suggestions if you agree with them. One thing to bare in mind is that the language appears to get thrown away and recreated (meaning the cmdline isn't parsed to the new instance). I'm going to create a PR that basically asserts that this is called before calling any of the methods. You might want to rebase this ontop of that and add the assert to generate_support_functions if it gets in first...

@@ -117,6 +117,21 @@ bool ansi_c_languaget::parse(
return result;
}

bool ansi_c_languaget::generate_support_functions(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider adding doxygen documentation for what supporting functions this generates (opaque functions, entry point)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have this in languaget, is that enough or does it have to be duplicated in derived classes?

{
msg.error() << "CONVERSION ERROR" << messaget::eom;
msg.error() << "ENTRY-POINT GENERATION ERROR" << messaget::eom;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Though most of generate_support_functions is related to the entry point, in might be worth calling this SUPPORT FUNCTION ERROR. Alternatively, could have the generate_support_functions throw structured exceptions for error states?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Structured exception will come, but let's do that separately.

max_nondet_array_length,
max_nondet_tree_depth,
get_pointer_type_selector());
return false;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would you mind adding a comment to this?
Sometime later it might not be obvious why this cannot fail.

@smowton
Copy link
Contributor Author

smowton commented Sep 18, 2017

@thk123 suggest checking https://github.com/diffblue/security-scanner/pull/192/files for the latest version of this (will update that one once this passes)--

Changes since this version:

  • Removed generate_entry_point, replaced with a call to generate_support_functions (which must work correctly if run more than once; amended the Java version to match the Ansi-C version in this respect)
  • Only use rebuild_goto_start_function when the binaries provided one and we're directed to overwrite it; otherwise run the language_filest version which searches for a frontend that can provide an entry-point.
  • Move declaration of the --function option into language.h, which is I think its proper owner

@thk123
Copy link
Contributor

thk123 commented Sep 19, 2017

@smowton Sorry your last message confused me - which PR should I be reviewing, this on diffblue/security-scanner#192?

@smowton
Copy link
Contributor Author

smowton commented Sep 19, 2017

@thk123 please review diffblue/security-scanner#192 then I once that's in I will clone it into this one for submission to develop

@@ -629,20 +629,6 @@ int cbmc_parse_optionst::get_goto_program(
// are already compiled
return 6;

if(cmdline.isset("function"))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this removed? What replaces this functionality?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was a duplicate of functionality already in initialize_goto_model -- it was previously overwriting the start function twice.

{
msg.error() << "CONVERSION ERROR" << messaget::eom;
msg.error() << "ENTRY-POINT GENERATION ERROR" << messaget::eom;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Structured exception will come, but let's do that separately.

{
std::set<std::string> languages;

for(file_mapt::iterator it=file_map.begin();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ranged for?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok

@thk123
Copy link
Contributor

thk123 commented Sep 20, 2017

I've reviewed 192 - once you've updated this PR to mirror could you ping me so I can create a TG bump since this will probably require some changes (I overhead you mention about the TG specific version of the language)

@smowton smowton force-pushed the smowton/feature/split_frontend_final_stage branch from 55c4bc3 to 8b2f871 Compare September 20, 2017 15:18
@smowton
Copy link
Contributor Author

smowton commented Sep 20, 2017

@thk123 @peterschrammel this has been updated; Peter your suggested C++11 loops have been added as a separate commit.

@smowton smowton force-pushed the smowton/feature/split_frontend_final_stage branch from 8b2f871 to 72c865e Compare September 21, 2017 10:08
@thk123
Copy link
Contributor

thk123 commented Sep 22, 2017

I am creating a TG bump for this to verify it - but then can be merged

@smowton
Copy link
Contributor Author

smowton commented Sep 22, 2017

@thk123 please press the button when you're happy

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For those out of ear shot of me and @smowton - there was a problem merging in to TG which @smowton is looking at at the moment.

The new generate_support_functions phase creates __CPROVER_start and
__CPROVER_initialize and runs before lazy loading; the final phase will run
*after* lazy loading, and is therefore used to patch up changes that require
functions' bodies to have been loaded already.
@smowton smowton force-pushed the smowton/feature/split_frontend_final_stage branch from 72c865e to 901d745 Compare October 4, 2017 09:50
@smowton
Copy link
Contributor Author

smowton commented Oct 4, 2017

Updated; created companion test-gen PR https://github.com/diffblue/test-gen/pull/1085 to verify this doesn't break it

@thk123
Copy link
Contributor

thk123 commented Oct 4, 2017

TG bump passes so have set approval.

@smowton smowton merged commit 6be5fd5 into diffblue:develop Oct 4, 2017
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
64d81f1 Merge remote-tracking branch 'upstream/develop' into pull-support-20171019
9e05177 Merge pull request diffblue#1474 from diffblue/jbmc
e847137 Merge pull request diffblue#1493 from reuk/reuk/output-instruction-const-ref
e74e1d8 Merge pull request diffblue#1489 from svorenova/tg-865
09431fd Adding unit tests for the signature/descripture mismatch
9a59fb9 Renamed DiffBlue -> Diffblue
185206c cbmc cleanup
d542f7e cbmc: clean out java
320eeaf use jbmc in regression tests
4286b86 added jbmc executable
b61cb56 Resolving signature/descriptor mismatch for methods
62675bb Merge pull request diffblue#1494 from thk123/tests/adding-generic-unit-tests
69d67ab Modified unit test to compile
9e68466 Replace loop_id parameter with const instructiont&
dbff05b Replace iterator with const value_type& in output_instruction signature
5191170 Merge pull request diffblue#1485 from diffblue/std_expr_typing
210a2f4 Merge pull request diffblue#1491 from andreast271/cbmc_parse_options_fix
fbc54ad guard against spurious pointers in taint analysis
5d6ebfd Revert "test isn't ready yet"
de668e6 upgrade uses of deprecated member_exprt constructor
9da3f4f elaborate typing of std_expr expression classes
36ac8c9 Merge pull request diffblue#1482 from reuk/reuk/more-cmake-errors
47c2a51 Merge pull request diffblue#1447 from NathanJPhillips/bugfix/calculate_max_string_length-unit-test
b2b4ca5 Align options string with help function and options parser
dfb11c2 Merge pull request diffblue#1480 from diffblue/java-types-cleanup
11c8aba Fixed calculate_max_string_length unit test to work in CLion
8f4f2ec Merge pull request diffblue#1473 from reuk/reuk/simplify-expr-fixup
1ad89a0 Merge pull request diffblue#1475 from martin-cs/goto-analyzer-6-part1
3c5df61 Merge pull request diffblue#1486 from diffblue/revert-1413-smowton/feature/prepare_vsa_for_subclasses
24f9867 Simplify a broader range of java primitive types
a18d7ec Revert "Value-set analysis: templatise and virtualise to facilitate customisation"
88acdfd Merge pull request diffblue#1355 from diffblue/cleanout-config-dependency
7df77e8 Add the overrides that clang wants.
e96e09b Regression test for constant propagator merge bug
ba55a2f constant propagator fix
350aa96 Addressing constant domain review comments by Daniel Poetzl.
5e9b2f4 Fail CMake build if make-generated files are found
32dcad8 test approx-const-fp-array-variable-invalid-cast-const-fp now more generous
12d45c6 Remove config dependency from CVC and DPLIB solvers
00d25a2 Pointers now come with a width
f4bc0ec cleanup of java_types.h
08b2332 disable two-way propagation for now
76abe8a Fix constant propagator.
c0ce9de Merge pull request diffblue#1413 from smowton/smowton/feature/prepare_vsa_for_subclasses
0bf2ce8 Merge pull request diffblue#1478 from smowton/smowton/fix/doxygen_fixes
0e0b501 Merge pull request diffblue#1463 from diffblue/mem-safety-check
04aff7c Remove residual doc template
fc02354 Fix docstyle in dump_c.cpp
a99b254 Indirect value_set_domaint -> value_sett operations via non-member functions
f94807d Merge pull request diffblue#1428 from romainbrenguier/refactor/find_index
433fdbf Merge pull request diffblue#1472 from reuk/reuk/label-tests
df6a0b3 Merge pull request diffblue#1406 from NlightNFotis/fotis/generics_support
123162b Merge pull request diffblue#1476 from diffblue/remove_ID_reference
e669c12 Add unit tests for value-set-analysis customisation
9465771 Value-set analysis: ignore DEAD statements
a2c1685 Templatize and virtualize value-set analysis
8ea9dcb Use std::find_if instead of expr visitor
5e1eede Merge pull request diffblue#1454 from martin-cs/feature/string-solver-performance
c73b758 Merge pull request diffblue#1452 from diffblue/call-seq-fix
d735cc5 Added support for concretising a generic and adding it into the symbol table.
f131b34 Remove ID_reference as front-ends use ID_pointer+ID_C_reference
d67bc87 Merge pull request diffblue#1471 from reuk/reuk/more-expr-cast-updates
5777062 check that memory for memcpy, memset and memmove is accessible
808a6ad Created basic class for creating new java instantiations of classes
57c2c1f Label tests with CBMC
bf4a103 Make a few changes suggested by @smowton
b63eb99 Merge pull request diffblue#1418 from diffblue/address_of_unions
e82701a Merge pull request diffblue#1456 from diffblue/preserve-hidden
3ff8448 Merge pull request diffblue#1468 from smowton/smowton/fix/unit_test_makefile_dependencies
1a81b3f Merge pull request diffblue#1341 from reuk/reuk/big-int-fixes
1d9eace Merge pull request diffblue#1465 from mgudemann/feature/string-solver-performance
987d384 Switch (!a | b) for (a => b) to clarrify the intent of the code.
40ff71b Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs.
d8b25f3 Merge pull request diffblue#1470 from reuk/reuk/fix-null-dereferences
5fa7b9a Merge pull request diffblue#1466 from reuk/reuk/return-ptr-from-expr-cast
0832454 Fix a couple of places where a null pointer may be dereferenced
47e426f Merge pull request diffblue#1442 from andreast271/compilation-NDEBUG-enable
869043a Merge pull request diffblue#1464 from smowton/smowton/fix/messaget_copy_and_assign_operators
9f53e90 Return pointer from expr_try_dynamic_cast
838c8a1 Fix testing-utils Makefile dependency
691e9fb Merge pull request diffblue#1449 from diffblue/havoc_object
78cd286 Fix messaget's copy-constructor and operator=
1614c2c Merge pull request diffblue#1462 from reuk/reuk/symbol-table-pointer
a9ba0f9 Modify/add symbol table lookup and get_writeable
d19e737 Merge pull request diffblue#1461 from thk123/bugfix/correcting-includes-in-new-unit-tests
3b69fe1 Missing source file from Makefile
d70a08a Util files were moved into a util library
0681219 Merge branch 'develop' of github.com:diffblue/cbmc into develop
8891466 test isn't ready yet (cmake variant)
b8057d3 Merge pull request diffblue#1448 from diffblue/goto-analalyzer-taint-test
beac327 added __CPROVER_havoc(...)
8118efa test isn't ready yet
19858f9 Fix zeroing of arrays in value set analysis
12fd5fe Fix identifying arrays in value set analysis
e618169 Merge pull request diffblue#1434 from svorenova/generics_support
68e4d6b Merge pull request diffblue#1457 from reuk/reuk/testing-utils
7c545c8 Switch (!a | b) for (a => b) to clarrify the intent of the code.
438ba8d Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs.
aacd436 Add new testing-utils library
b7aaad0 Removing signature parsing for local variables
8d54be1 Adding exception and tests for missing closing delimiter
608c6b6 Disabling part of the unit test for generic classes
e140bb7 Updating the calls of lookup method to reflect the new return type
cfb5212 Resolving name shadowing
97e1b9a Adding a warning and a commentary for unsupported generics, cleaning
4f305de Handling wild card generics with exception
8f527f8 Cleaning java files
3a1962f Turning back on regression tests
a9dc64d Disabling part of the unit test for generic classes
04e55be Reverting method descriptor loading
2f7925d Adding unit test for recursive generic class
764c651 Enable compilation with NDEBUG defined
e8c75ac Adding unit test for generic array
de5c040 Adding tests for generic functions
85c1574 Applied use of utility function for loading a class file
8c7f4e4 Adding unit test for java class that inherits from a generic class
1dd221d Correct handling of the java generic class signature
33afe48 Adding unit tests for parsing wild card functions
a2344f8 Extending the tests for the generic class
35cd160 Deal with generic methods
7320c46 Correcting a typo
2f7f695 Adding some useful debug info
79f743b Adding conversions for wild cards
a60ead4 Correctly handle nested generic types
b59c659 When dealing with generic arrays we should treat them like ref arrays too
1bd95c0 Classes that aren't generic but inherit from a generic type have a signature
b2f57e8 Fixing handling the case of *
31faaa6 Revert "Revert "TG-374 Feature/java support generics""
89341da Merge pull request diffblue#227 from diffblue/feature/adding_goto_statistics_to_goto-instrument
99eb662 Merge pull request diffblue#1450 from reuk/reuk/join-strings
9cf47a2 Updates requested in the PR.
4c4a267 Adding computation and save of goto program statistics.
7fcfd30 Merge pull request diffblue#1453 from diffblue/integer-addressees
639d1aa Merge pull request diffblue#1451 from diffblue/time-stopping
7e42fd2 preserve hidden flag for functions
0346f87 Add a join function for strings
2b17564 integer dereferences are now re-written to a custom expression
202b509 fix for call-sequences and call-graph
f159bd5 more time stopping functionality
ba96dde Merge pull request diffblue#1441 from reuk/reuk/expr-cast-for-code-types
086d6da moved taint-related tests for goto-analyzer into separate subdirectory
c25e56f Respond to @NathanJPhillips' review feedback
3a4d364 Add checked_cast signatures
47a13c7 Remove unnecessary explicit typelists
bc3d79b Use decay instead of remove_const(remove_reference)
f9c1c70 Reorder and hide functions in expr_cast
800adbe Allow dynamic expr cast with code types
3ce8f11 Fix comparison in expr_cast.h
48b154a Bugfix: Exclude functions without bodies from GOTO statistics.
22a68fe Merge pull request diffblue#1444 from smowton/upstream/restrict-symbol-table
d577d40 Merge pull request diffblue#1445 from smowton/smowton/feature/test-pl-interrupt
b01ff65 Test.pl: exit if a test is interrupted
6794191 Improve symbol table documentation
d320187 Linter fixes
53e1ca2 Made move constructor strong exception safe
9f4e933 Changed interface to symbol_tablet::insert
e35f2fc Misc review requests
a9d802b Made lookup return optional
d1d502f Restricted interface of current symbol_tablet
478dc8a Merge pull request diffblue#1371 from NathanJPhillips/feature/unhide-error
b790095 Merge pull request diffblue#1443 from tautschnig/fix-library-check
ab2f3c3 Merge pull request diffblue#1438 from reuk/reuk/simplify-expr-improvement
e865729 Updated comment
1def64c Added INVARIANT to symbol_tablet::remove
7798daa Add move insert to symbol_table
b14a495 Tidy up symbol_tablet::move
6be5fd5 Merge pull request diffblue#1394 from smowton/smowton/feature/split_frontend_final_stage
14eecf6 library_check: use the build-system configured C compiler
3197045 library_check: rename _mm_*fence functions
6bc86e1 Merge pull request diffblue#222 from diffblue/feature/lexicographical_ordered_dump_of_functions_and_symbols
a73ee46 Merge pull request diffblue#224 from diffblue/feature/file_utils_add_parsing_of_file_extension
421f4eb Merge pull request diffblue#226 from diffblue/feature/goto_statistics
1d87928 Add unit test for new behavior
9ea7414 Set up config in unit tests
0e2b13f Remove tautological typecasts
901d745 Switch to C++11 for-loops in language_file.cpp
c7c8022 Add tests for mixed GOTO and C input
05f2f3c Split the entry-point-generation phase into two parts
268d196 Display error in catch(...)
6888dd2 Merge pull request diffblue#1436 from smowton/smowton/initialize-goto-model-opaque-stub-generation
6d9f029 Updates requested in the PR.
6f8ebe4 Updates requested in the PR.
d4a04ac Added support of Windows platform to parsing file extension.
1884d67 Merge pull request diffblue#221 from diffblue/bugfix/INVARIANT_while(0)_to_while(false)
39a774f Introducing GOTO program statistics.
821ba1c Updates requested in the PR.
9266de0 Add parsing of file extension from file path-name.
a9fa893 Merge pull request diffblue#1437 from smowton/smowton/fix-object-factory-globals
632ae4b Updates to recording_symbol_tablet
7545fc5 Merge pull request diffblue#1409 from thk123/bugfix/lang-args-missing
7fb835c Merge pull request diffblue#1433 from thk123/bugfix/doxy-script-documentation
56b0b26 Added lexicographical order to textual dump of functions and symbols.
58ef65b Object factory: initialise global symbols in place
c41acce Set opaque stub generation in initialize-goto-model
ef76441 Corrected error in the run_diff script
897aaf6 Merge pull request diffblue#1431 from thk123/feature/java-load-class-utility
79324b3 INVARIANT: while(0) -> while(false)
774bfdb Correcting type in the extendor class
46cbec6 Created utility function for loading a class file
8151e91 Merge pull request diffblue#1429 from janmroczkowski/janmroczkowski/unified_difft-remove-unused-identifier
3ceb89b Merge pull request diffblue#1390 from diffblue/fix_pointer_type
733f7b2 Added is_success and is_error helpers
5e7f3f7 Added implicit constructors to main_function_resultt to make code in get_main_symbol even briefer
3317a3a Tidied up code in get_main_symbol
47fe36f Changed main_function_resultt to use an enum instead of a collection of bools
8bb39ca Merge pull request diffblue#1427 from LAJW/feature/string-replace-single-character-strings
a084a6a Reverting indentation in order to make the compiler silent.
f948c2f Readability improvement
fc7c615 Remove unused function identifier
c063d01 Merge pull request diffblue#1259 from romainbrenguier/cleaning/factor-assign-java-string
c24e6c9 Update regression test that can randomly fail
df88b49 Rename operand_to_process into expr_to_process
e0441cb Add example where the solver potentially runing out of memory
52a08d8 Setting string-max-length on strings test
02e42da Adding unit test for convert exprt to string exprt
870814e Make code_assign_java_string_to_string_expr append to a code argument
e8491a6 Factoring assign_java_string_to_string_expr with process_operands
00af153 Add comment on implementation status of String.replace
f2fab1a String.replace for single-character strings
fade69f Move expr_cast to a separate file
e4b5e12 Merge pull request diffblue#218 from diffblue/cleanup/typo
5fecceb Added recording_symbol_tablet
4d65951 Split storage for symbol_tablet into a concrete derived type
7b254e2 Made move constructor strong exception safe
d66c0bc Changed interface to symbol_tablet::insert
6dc1213 Typo in reachable
51e493e Merge pull request diffblue#1422 from reuk/reuk/library-check-dep
27e1f2a Merge pull request diffblue#1423 from janmroczkowski/janmroczkowski/fresh_symbol-reset_temporary_counter
15af645 Merge pull request diffblue#1426 from reuk/reuk/download-project
db9a0a7 Updates requested in the PR.
d00c03d Introducing "enable_ccache" switch (default on) into our build system.
88c2f9c Use DownloadProject method for integrating sat libraries
bc593c5 Add DownloadProject cmake script
0cc696b introduced ID_frontend_pointer
cc63551 revert bits of a9806c0; the width of these pointers is done during the conversion phase
8fdb06f preserve location of pointer types
de493ae Merge pull request diffblue#1412 from diffblue/java-object-factory-bug
7c3239b Merge pull request diffblue#1417 from diffblue/builtin_memset
368bb27 Merge pull request diffblue#1421 from jasigal/refactor/string-refinement-decision-procedure#TG-672
f079156 Merge pull request diffblue#205 from diffblue/feature/restrict-symbol-table
2462077 Misc review requests
98d0082 Made lookup return optional
db69023 Restricted interface of current symbol_tablet
ea74c6d Updated comment
909b557 Added INVARIANT to symbol_tablet::remove
bd3ee6e Add move insert to symbol_table
e67f326 TG-672 Added universal constraint counter-examples, assumed fix-point with no not contains constraints is equi-SAT
72a537a TG-672 Remove some unused concretizing code
95efc6f TG-672 Grouped string axioms together
a65407e TG-672 Grouped index sets together
503c49d TG-672 Removed unneeded code (current index set display, extra invariant check)
45af45d TG-672 Uniformity in algorithm for treatement of universal and not contains constraints
dd03003 TG-672 Fixed correctness issue in main loop of algorithm and added first UNSAT return
dfa3ffd TG-672 Replaced `push_back` with `emplace_back`
ac1b620 TG-672 Fixed `expr_cast` to be unambiguous and added `const` and `const` references throughout
eb5726e Add reset_temporary_counter to fresh_symbol
b5fe7e3 TG-672 Initial refactoring (renaming, code removal)
438d9f0 Merge pull request diffblue#1401 from janmroczkowski/janmroczkowski/java_bytecode_convert_classt-add_array_types-fix
18aacc0 Add full JSON-structured output for value-set analysis
0cdd9c6 Improve structure of JSON static-analysis dump
7df9f15 Add LVSA summary dump-to-JSON
83ee7d4 Only re-run library-check when ansi-c changes
2adc013 symex: fix address_of unions
cd8d494 added __builtin_memset
fcd470a only attempt to translate nondet sideeffects for Java code
b9dfda9 Fix to java_bytecode_convert_classt.add_array_types
61c6489 Verify that language options have been initialized
e3ad6c0 Update Big-Int with copy, move, swap

git-subtree-dir: cbmc
git-subtree-split: 64d81f1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants