Make re-building __CPROVER_initialize safe #6576

tautschnig · 2022-01-13T11:55:37Z

We auto-generate __CPROVER_initialize, but also have/had several places that tweak the generated function. Such tweaking could be lost when rebuilding __CPROVER_initialize. The commits in this PR make sure that rebuilding __CPROVER_initialize is safe by making the prior tweaks permanent through updates to the symbol table.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-01-13T13:15:27Z

Codecov Report

Merging #6576 (e631369) into develop (4f84963) will increase coverage by 0.01%.
The diff coverage is 99.54%.

@@             Coverage Diff             @@
##           develop    #6576      +/-   ##
===========================================
+ Coverage    76.20%   76.21%   +0.01%     
===========================================
  Files         1579     1578       -1     
  Lines       181291   181378      +87     
===========================================
+ Hits        138144   138237      +93     
+ Misses       43147    43141       -6

Impacted Files	Coverage Δ
jbmc/src/jbmc/jbmc_parse_options.cpp	`72.31% <ø> (ø)`
src/cbmc/cbmc_parse_options.cpp	`77.39% <ø> (-0.05%)`	⬇️
src/goto-analyzer/goto_analyzer_parse_options.cpp	`71.94% <ø> (-0.09%)`	⬇️
src/goto-cc/linker_script_merge.h	`100.00% <ø> (ø)`
src/goto-diff/goto_diff_parse_options.cpp	`58.33% <ø> (-0.50%)`	⬇️
...rc/goto-instrument/goto_instrument_parse_options.h	`100.00% <ø> (ø)`
src/goto-programs/slice_global_inits.h	`0.00% <ø> (ø)`
src/goto-cc/linker_script_merge.cpp	`79.12% <98.33%> (+0.97%)`	⬆️
src/ansi-c/ansi_c_internal_additions.cpp	`90.12% <100.00%> (-0.47%)`	⬇️
src/ansi-c/cprover_library.cpp	`97.61% <100.00%> (+0.32%)`	⬆️
... and 13 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bd1b8c2...e631369. Read the comment docs.

feliperodri

Approving changes in our contract module.

feliperodri · 2022-01-15T05:13:47Z

src/goto-instrument/contracts/memory_predicates.cpp

+  if(parent.get_goto_functions().function_map.erase(INITIALIZE_FUNCTION) != 0)
+  {
+    static_lifetime_init(
+      parent.get_symbol_table(),
+      parent.get_symbol_table().lookup_ref(INITIALIZE_FUNCTION).location);
+    goto_convert(
+      INITIALIZE_FUNCTION,
+      parent.get_symbol_table(),
+      parent.get_goto_functions(),
+      log.get_message_handler());
+    parent.get_goto_functions().update();
+  }


Nice! It'll remove unnecessary warnings from our proofs with contracts.

chrisr-diffblue

Looks good :-)

chrisr-diffblue · 2022-01-15T11:03:56Z

src/cpp/cpp_internal_additions.cpp

@@ -44,7 +44,7 @@ std::string c2cpp(const std::string &s)

 void cpp_internal_additions(std::ostream &out)
 {
-  out << "# 1 \"<built-in-additions>\"" << '\n';
+  out << "#line 1 \"<built-in-additions>\"" << '\n';


Good catch!

chrisr-diffblue · 2022-01-15T11:07:05Z

src/goto-cc/linker_script_merge.cpp

+    CHECK_RETURN(zi.has_value());
+
+    // Add the array to the symbol table.
+    symbolt array_sym;


Mildly a shame there isn't a constructor/utility function for creating a suitably initialised symbolt

Thank you for calling this out! I'll try to address this in a separate PR.

Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes.

Do not fix up the value by tweaking __CPROVER_initialize. This simplifies the code and allows us to regenerate __CPROVER_initialize at any time (at least as far as __CPROVER_malloc_may_fail and __CPROVER_malloc_failure_mode are concerned). This change also avoids any cost of variables to be processed by program analysis when they are compile-time constants. This, in turn, entails updates to various goto-analyzer tests. These updates include removal of redundant patterns.

We sometimes used # 1 instead of #line 1, which GCC accepts, but Visual Studio might not actually do, or perhaps sometimes does. It certainly failed when used with the code in cprover_library.cpp.

src/goto-instrument/goto_instrument_parse_options.h

Remove deprecated calls to initiallize malloc_may_fail variables. This feature is now handled differently in CBMC, see: diffblue/cbmc#6576 Signed-off-by: František Nečas <[email protected]>

Add missing symbolt include Remove usage of deprecated goto_instructiont::get_assign() Remove usage of deprecated goto_instructiont::get_function_call() Add missing include for side_effect_exprt Fix usage of goto_instructiont::source_location Fix usage of goto_instructiontt:type Update usage of goto_checkt Remove deprecated calls to initiallize malloc_may_fail variables. This feature is now handled differently in CBMC, see: diffblue/cbmc#6576 Make tests containing argc less strict, the C standard does not guarantee that it is >= 1, just that it is non-negative. For more information, refer to the CBMC commit: 788cb496ee573cc4182273d1513c5a5eb68a383a Make use of refactored update_assumptions_assertions of goto_check Adjust heap domain to newly returned annotated_pointer_constant type. For more information about this constant, see CBMC commit: 112f1d0aaa5a4606aa0e6a06a9e1ee853ebc20ab Update goto_check includes Add removed make_assertions_false to preprocessing Fix goto_check usage Remove direct access to goto_instructiont::guard Do not use soon-to-be-deprecated goto_instructiont::get_code Fix collection of record free variables Remove usage of base_type, it's deprecated Signed-off-by: František Nečas <[email protected]>

tautschnig self-assigned this Jan 13, 2022

tautschnig force-pushed the cleanup/init-function-updates branch 2 times, most recently from 24a68ed to eaa6568 Compare January 13, 2022 14:56

tautschnig added the dependent - do not merge label Jan 13, 2022

peterschrammel approved these changes Jan 13, 2022

View reviewed changes

tautschnig force-pushed the cleanup/init-function-updates branch from eaa6568 to e7c87e9 Compare January 14, 2022 16:04

tautschnig removed the dependent - do not merge label Jan 14, 2022

tautschnig force-pushed the cleanup/init-function-updates branch from eb58e07 to 907a214 Compare January 14, 2022 22:10

tautschnig marked this pull request as ready for review January 14, 2022 22:11

tautschnig requested review from chrisr-diffblue, feliperodri, kroening, martin-cs, romainbrenguier and SaswatPadhi as code owners January 14, 2022 22:11

tautschnig assigned kroening and unassigned tautschnig Jan 14, 2022

feliperodri approved these changes Jan 15, 2022

View reviewed changes

chrisr-diffblue approved these changes Jan 15, 2022

View reviewed changes

tautschnig and others added 7 commits January 17, 2022 16:40

Stack-depth instrumentation: update the symbol table

fe6db02

Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes.

Nondet static: update the symbol table

9a64fc3

Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes.

Slice global inits: update the symbol table

4910998

Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes.

Linker scripts processing updates symbol tables

98bb43d

Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes.

C/C++ internal additions: consistently use #line

4e32058

We sometimes used # 1 instead of #line 1, which GCC accepts, but Visual Studio might not actually do, or perhaps sometimes does. It certainly failed when used with the code in cprover_library.cpp.

Clang-format builtin header declarations

e631369

tautschnig force-pushed the cleanup/init-function-updates branch from 907a214 to e631369 Compare January 17, 2022 16:40

tautschnig assigned tautschnig and unassigned kroening Jan 17, 2022

tautschnig merged commit 49fb197 into diffblue:develop Jan 17, 2022

tautschnig deleted the cleanup/init-function-updates branch January 17, 2022 18:15

martin-cs reviewed Feb 11, 2022

View reviewed changes

src/goto-instrument/goto_instrument_parse_options.h Show resolved Hide resolved

martin-cs mentioned this pull request Feb 11, 2022

Warn when --malloc-may-fail has no effect #6657

Draft

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Make re-building __CPROVER_initialize safe #6576

Make re-building __CPROVER_initialize safe #6576

Uh oh!

tautschnig commented Jan 13, 2022 •

edited

Loading

Uh oh!

codecov bot commented Jan 13, 2022 •

edited

Loading

Uh oh!

feliperodri left a comment

Uh oh!

feliperodri Jan 15, 2022

Uh oh!

chrisr-diffblue left a comment

Uh oh!

chrisr-diffblue Jan 15, 2022

Uh oh!

chrisr-diffblue Jan 15, 2022

Uh oh!

tautschnig Jan 17, 2022

Uh oh!

Uh oh!

Uh oh!

Make re-building __CPROVER_initialize safe #6576

Make re-building __CPROVER_initialize safe #6576

Uh oh!

Conversation

tautschnig commented Jan 13, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jan 13, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

feliperodri Jan 15, 2022

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jan 15, 2022

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jan 15, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 17, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Jan 13, 2022 •

edited

Loading

codecov bot commented Jan 13, 2022 •

edited

Loading