Rebuild ansi c when necessary #1503

reuk · 2017-10-20T10:33:11Z

@smowton noticed that in the CMake build, the ansi-c target wasn't being rebuilt when files in library/ansi-c were changed. This patch should ensure that changes to files in library/ansi-c cause a rebuild of the library.

reuk · 2017-10-20T10:34:03Z

Could @thk123 review this too please?

tautschnig · 2017-10-20T10:42:04Z

src/ansi-c/CMakeLists.txt

@@ -3,20 +3,57 @@ generic_flex(ansi_c)

 add_executable(converter library/converter.cpp)

+set(ansi_c_library_sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/library/cegis.c


Just curious: is the use of wildcards not possible here?

Raw wildcards aren't, because we need to evaluate the list of files at compile time, and wildcards are expanded in a shell at build time. We could use file(GLOB like elsewhere, I suppose

I think I'd prefer that so as to avoid some maintenance nightmare. All .c files are to be taken into account, so GLOB sounds about right.

tautschnig · 2017-10-20T10:43:00Z

src/ansi-c/CMakeLists.txt

 )

 add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
-    COMMAND converter < converter_input.txt > ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
+    COMMAND converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"


Any guidance on when to quote/when not to quote?

Much like a shell script, we quote when a path may contain spaces. The quotes around converter_input.txt aren't necessary, they're just for consistency

Ok, thanks! I was indeed wondering about the ones around converter_input.txt, but also the fact that quoting was only used after COMMAND but not after OUTPUT.

smowton

Looks sensible, though I don't precisely understand the cmake innards so some of this is guessing from macro names.

One thought: I'm guessing the GLOB logic will suffer from the standard pitfall where a modification results in a remake, but adding a new file goes unnoticed and requires a manual reconfigure? Is there an easy way to tell cmake that a change to the directory's mtime should spark a reconfigure?

reuk · 2017-10-20T12:14:28Z

Apparently you can do set_property(DIRECTORY APPEND PROPERTY CMAKE_CONFIGURE_DEPENDS] <dirname>) to tell CMake to reconfigure the project when some folder/file changes. Reconfiguration will then pick up any added or removed files.

I'm not sure how great of an idea this is though - if we do this here, then we should probably do it everywhere we use file globbing, and eventually we'll end up reconfiguring the project every time a globbed file changes, which will slow down the change -> build -> test cycle

smowton · 2017-10-20T12:17:10Z

It definitely shouldn't be reconfiguring on a file modification, but it definitely should be when a file is added or deleted if the globs can only be executed at configure time.

Ultimately I think we should heed the CMake manual's advice and not use glob (anywhere) because of these holes in its functionality.

reuk · 2017-10-20T12:22:44Z

Seems reasonable - I can put together a PR removing file-globbing from the CMakeLists. I'm concerned that we'll end up with files committed that aren't built, though.

smowton · 2017-10-20T12:50:20Z

I think the answer to that is to insist that at least one user for the new thing (perhaps a unit test) has to be PR'd side-by-side with the new thing, then any build system screwups will be obvious

thk123

Seems reasonable but I don't fully understand exactly what is going on. Though if the cmake build still builds I suppose it is fine

thk123 · 2017-10-23T11:21:25Z

src/ansi-c/CMakeLists.txt

-    DEPENDS converter_input.txt
+add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+    COMMAND converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+    DEPENDS "converter_input.txt"


Why are these now wrapped in quotes?

It's probably sensible to quote wrap some of those to handle path names with spaces - fairly common on OS X builds, for instance, I suspect.

thk123 · 2017-10-23T11:25:01Z

src/ansi-c/CMakeLists.txt

+    ${FLEX_scanner_OUTPUTS}
+)
+
+set_source_files_properties(


What is this doing?

Yes, I'm a bit confused here too - this is removing converter and file_converter sources from the dependencies for ansi-c, which in someways makes sense. But should there be some sort of transitive dependency on the converter/file_converter tools so that if those tools get modified, anything that depends on them also gets rebuilt? (possibly adding the dependencies on the tools in the earlier custom_commands?)

I've updated this so that the custom commands depend on the executables they run.

I was confused about this, but it turns out CMake only adds a target-level dependency for commands which reference executables built in the project (i.e. the executable is built before the files it generates). CMake doesn't add a file-level dependency for files built by the executable. By adding an explicit DEPENDS to the custom command, we can force CMake to re-generate files that are created by the generator executables whenever the executables are changed.

chrisr-diffblue

Mostly looks good, but I wonder if there should be some extra dependencies on the tools used in the custom_commands?

reuk · 2017-10-23T13:21:51Z

I've fixed this up based on your comments @thk123 and @chrisr-diffblue, please re-review when you get an opportunity

chrisr-diffblue

Thanks for making the changes - looks good to me.

739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table 429c13f Merge pull request diffblue#1520 from smowton/smowton/fix/symbol_table_writer_erase d9f3a2f Revert "Disable OSX builds" 81bb39c Symbol-table writer: fix use of map key after erasure 021fe8f Merge pull request diffblue#1492 from tautschnig/perf-test 0729e3d Merge pull request diffblue#1517 from NathanJPhillips/bugfix/journaling-symbol-table-constructor 93ae9f3 Merge pull request diffblue#1527 from diffblue/revert-1510-always-inline c4ed1ae Revert security-scanner version of recording symbol table e83e307 Fixed scope of moved symbol 535f1df Revert "Fully process always_inline" 0096451 Replace broken copy constructor with move constructor a6adb19 Fix more catch std::string occurances 22a876f Merge pull request diffblue#1523 from reuk/reuk/update-compiling-instructions 8fe258b Update COMPILING with cmake setup instructions 99592b3 Merge pull request diffblue#1504 from andreast271/update-windows-build dff22b8 Make Windows compilation instructions more prescriptive bc3bc8f Merge pull request diffblue#1511 from tautschnig/fix-graphml 358829c Merge pull request diffblue#1510 from tautschnig/always-inline 3e77dd6 Merge pull request diffblue#1496 from smowton/smowton/feature/symbol_table_writer d115b4e catch by const ref instead of by value or non-const ref 444d824 Fix graphml output of concurrency witnesses 08c512d Make Windows compilation instructions more prescriptive bcf8ff3 Update documentation for building cbmc on windows. Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line. 728dbb5 Merge pull request diffblue#1508 from smowton/smowton/1420-fragments/value_set_debugging 9d9e50d Merge pull request diffblue#1507 from smowton/smowton/1420-fragments/factor_java_object_init b2104b0 Merge pull request diffblue#1506 from smowton/smowton/1420-fragments/typecheck_expr_cleanup 7175efe Merge pull request diffblue#1505 from smowton/smowton/1420-fragments/invariants 7537302 Adding a java_lang_object_init function 86513ee Merge pull request diffblue#1324 from reuk/reuk/clang-format ea4a777 Merge pull request diffblue#1503 from reuk/reuk/rebuild-ansi-c-when-necessary d9c0598 [pointer-analysis] Better debugging information in pointer analysis 3146336 Remove unnecessary includes in java-typecheck 10b5c8e [java-bytecode/typecheck] Style: Changing assertions in preconditions 2afe377 Fully interpret __attribute__((always_inline)) 8eaf89e Apply symbol replacement in type_arg members 13a7553 Rebuild ansi-c library if non-source dependencies change b97a766 Merge pull request diffblue#1403 from karkhaz/kk-regenerate-arch-flags-binaries a4dc986 Merge pull request diffblue#1484 from diffblue/interpreter_size_t 9d4e0ca Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs c3e6726 Script to automate performance evaluation of CBMC on AWS 912ee38 Improve symbol table style 6b1a49d Add missing goto-statistics file to Makefile d512204 Add cbmc and jbmc as install targets bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019 c5c77ac Merge pull request diffblue#1495 from diffblue/codeowners2 f154d16 Merge pull request diffblue#1487 from martin-cs/goto-analyzer-6-part2 4955417 initialize_goto_model now returns a goto_model 56f924c Merge pull request diffblue#1483 from diffblue/signature_initialize_goto_model eef32db Methods for ai_baset to allow access to the ai_base_domaint for a location. aae984a Disable the regression test for now as it depends on the variable sensitivity domain. 3050c53 Don't stop when recursion found 93f2e1f Use is_bottom() to catch unreachable functions. 5b604ae Update the mock domain with the new ai_domain_baset interface. f9ca353 Add is_bottom() and is_top() to ai_domain_baset and derived domains. 88d8673 Rename the XML output to something a bit more meaningful. 2110cd1 Make formatting stage non-blocking on Travis a24ac3d Fixup compiling.md with more clang-format install instructions c3c24e2 Add symbol table writer 98643d7 initialize_goto_model now returns a goto_model fd6acc5 initial proposal for owners of code f39ae5c use mp_integer for addresses f6ae635 use std::size_t in interpreter 55e6594 Fixup cpplint.py 9d4b827 Update coding standard 8482b35 Add information about using clang-format 1dcc82c Convert COMPILING to markdown format 554cb54 Adjust cpplint to disable whitespace checks by default 6ce0dba Add travis style check f18979a Add clang-format config 622e2e3 Merge branch 'develop' into show_functions_dfs bea696a Regenerated cross-compiled arch flag test binaries 1fab1c1 Fixed show-call-sequences deature of goto instrument; added test suite git-subtree-dir: cbmc git-subtree-split: 739c7f5

tautschnig reviewed Oct 20, 2017

View reviewed changes

reuk force-pushed the reuk/rebuild-ansi-c-when-necessary branch from 1450f8f to 771186f Compare October 20, 2017 10:52

smowton approved these changes Oct 20, 2017

View reviewed changes

thk123 reviewed Oct 23, 2017

View reviewed changes

thk123 requested a review from chrisr-diffblue October 23, 2017 11:31

chrisr-diffblue approved these changes Oct 23, 2017

View reviewed changes

Rebuild ansi-c library if non-source dependencies change

13a7553

reuk force-pushed the reuk/rebuild-ansi-c-when-necessary branch from 771186f to 13a7553 Compare October 23, 2017 13:17

chrisr-diffblue approved these changes Oct 23, 2017

View reviewed changes

thk123 approved these changes Oct 24, 2017

View reviewed changes

thk123 merged commit ea4a777 into diffblue:develop Oct 24, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rebuild ansi c when necessary #1503

Rebuild ansi c when necessary #1503

reuk commented Oct 20, 2017

reuk commented Oct 20, 2017

tautschnig Oct 20, 2017

reuk Oct 20, 2017

tautschnig Oct 20, 2017

tautschnig Oct 20, 2017

reuk Oct 20, 2017

tautschnig Oct 20, 2017

smowton left a comment

reuk commented Oct 20, 2017 •

edited

Loading

smowton commented Oct 20, 2017

reuk commented Oct 20, 2017

smowton commented Oct 20, 2017

thk123 left a comment

thk123 Oct 23, 2017

chrisr-diffblue Oct 23, 2017

thk123 Oct 23, 2017

chrisr-diffblue Oct 23, 2017 •

edited

Loading

reuk Oct 23, 2017

chrisr-diffblue left a comment

reuk commented Oct 23, 2017

chrisr-diffblue left a comment

Rebuild ansi c when necessary #1503

Rebuild ansi c when necessary #1503

Conversation

reuk commented Oct 20, 2017

reuk commented Oct 20, 2017

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

smowton left a comment

Choose a reason for hiding this comment

reuk commented Oct 20, 2017 • edited Loading

smowton commented Oct 20, 2017

reuk commented Oct 20, 2017

smowton commented Oct 20, 2017

thk123 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

chrisr-diffblue Oct 23, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisr-diffblue left a comment

Choose a reason for hiding this comment

reuk commented Oct 23, 2017

chrisr-diffblue left a comment

Choose a reason for hiding this comment

reuk commented Oct 20, 2017 •

edited

Loading

chrisr-diffblue Oct 23, 2017 •

edited

Loading