Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

remi-delmas-3000 · 2021-11-16T21:46:05Z

This PR fixes some performance issues with assigns clause checking for function and loop contracts.

The problem was that the goto variables and instructions generated to instrument the checks were themselves re-instrumented with automatic VCCs in subsequent passes, causing an explosion in the number of VCCs (with unwanted VCCs representing up to 85% of the total VCCs in some problems).

Instructions performing CAR inclusion checks are read-only logical expressions whose evaluation cannot fail so we can safely disable automatic checks on them.

CAR snapshotting instructions however perform some pointer arithmetic and need to be ultimately checked for pointer overflow.

In this PR:

we disable all pointer checks on CAR inclusion checking instructions
we enable pointer overflow checks on CAR snapshot instructions

The disable pragmas guard against reinstrumentation in later passes, and the enable pragmas make sure necessary checks will eventually be instantiated before analysis.

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.
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

jimgrundy · 2021-12-02T23:01:01Z

src/goto-instrument/contracts/utils.h

@@ -116,6 +116,8 @@ const symbolt &new_tmp_symbol(
  const typet &type,
  const source_locationt &location,
  const irep_idt &mode,
-  symbol_table_baset &symtab);
+  symbol_table_baset &symtab,
+  std::string suffix = "tmp_cc");


This new parameter needs a doxygen comment above

codecov · 2021-12-02T23:51:52Z

Codecov Report

Merging #6459 (e2f4fec) into develop (d8e5aac) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6459   +/-   ##
========================================
  Coverage    76.07%   76.08%           
========================================
  Files         1548     1548           
  Lines       166362   166387   +25     
========================================
+ Hits        126567   126591   +24     
- Misses       39795    39796    +1

Impacted Files	Coverage Δ
src/goto-instrument/contracts/assigns.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/assigns.cpp	`97.24% <100.00%> (+0.30%)`	⬆️
src/goto-instrument/contracts/contracts.cpp	`95.44% <100.00%> (+0.05%)`	⬆️
src/goto-instrument/contracts/utils.cpp	`93.54% <100.00%> (+0.69%)`	⬆️
src/solvers/flattening/bv_utils.cpp	`77.33% <0.00%> (-0.21%)`	⬇️

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 adfd71d...e2f4fec. Read the comment docs.

tautschnig

Generally ok with this, but the last commit introduces/modifies various tests and it is not obvious which tests are just additional tests, or which code changes these tests relate to.

tautschnig · 2021-12-03T09:15:33Z

src/goto-instrument/contracts/utils.cpp

  return get_fresh_aux_symbol(
    type,
-    id2string(location.get_function()) + "::tmp_cc",
-    "tmp_cc",
+    id2string(location.get_function()) + "::",
+    suffix,
    location,
    mode,
    symtab);


While at it: should this code also be modified to have those symbols show up in counterexample traces? I found myself having a hard time understanding counterexamples for none of the assignments to these variables show up, but failing assertions then refer to them. The change required to facilitate this:

symbolt &new_symbol = get_fresh_aux_symbol(...); new_symbol.is_auxiliary = false; return new_symbol;

Adding a new function argument 'is_auxiliary' to control that symbol per symbol.

tautschnig · 2021-12-03T09:17:24Z

src/goto-instrument/contracts/assigns.cpp

@@ -52,14 +52,16 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
 }

 const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
+  const std::string &prefix,


Random place for comment, and primarily for future reference: I would like to see commits like this be a pull request of their own. Changing the names of CAR instrumentation variables really has nothing to do with disabling selected checks.

tautschnig · 2021-12-03T09:27:12Z

src/goto-instrument/contracts/contracts.cpp

+    source_locationt &location_no_checks =
+      instruction_it->source_location_nonconst();


Do you really want or need to take a reference here? The reference will ensure (but is that desired?) that checks are disabled on the function call. Otherwise, I would have expected that you'd be taking a copy here, at which point you want to use source_location() instead of source_location_nonconst().

tautschnig · 2021-12-03T09:27:35Z

src/goto-instrument/contracts/contracts.cpp

@@ -1175,6 +1175,10 @@ void code_contractst::check_frame_conditions(
    else if(instruction_it->is_dead())
    {
      const auto &symbol = instruction_it->dead_symbol();
+      source_locationt &location_no_checks =
+        instruction_it->source_location_nonconst();
+      disable_pointer_checks(location_no_checks);


As above: is the reference intentional?

We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

tautschnig · 2021-12-03T09:27:53Z

src/goto-instrument/contracts/contracts.cpp

-    assigns.generate_inclusion_check(car), instruction_it->source_location()));
-  assertion.instructions.back().source_location_nonconst().set_comment(
+  source_locationt location_no_checks =
+    instruction_it->source_location_nonconst();


Certainly source_location() instead of source_location_nonconst().

tautschnig · 2021-12-03T09:30:07Z

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -40,4 +42,4 @@ We also check (using positive regex matches above) that
 `**p` should be assignable in one case and should not be assignable in the other.

 Finally, we check that there should be no "internal" assertion failures
-on `tmp_cc` variables used to track CARs.
+on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs.


Changes in this file should be folded into the commit introducing the new names.

tautschnig · 2021-12-03T09:30:23Z

regression/contracts/assigns_enforce_havoc_object/functions.txt

@@ -0,0 +1 @@
+Reading GOTO program from '__CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset_with_contracts_harness.c.goto'


What is the meaning of this file?

this is a debugging session leftover, removing it

remi-delmas-3000 · 2021-12-03T16:34:43Z

All review comments were addressed

Issue has been addressed

…ter overflow checks on CAR upper bound computation.

feliperodri

I was a bit too late to the party, but I'll leave the comments here to be addressed on another PR.

feliperodri · 2021-12-03T19:33:24Z

regression/contracts/assigns_enforce_free_dead/test.desc

+^.*__car_valid.*: FAILURE$
+^.*__car_lb.*: FAILURE$
+^.*__car_ub.*: FAILURE$


nitpick: I'd prefer even more readable names for users: __car_valid, __car_lower_bound, and __car_upper_bound. However, the fact that these variables exist should be transparent to users. Why would this variables appear as failures? I guess you want to make sure here there are no memory safety errors in any operation using these variables, is that correct?

feliperodri · 2021-12-03T19:38:49Z

src/goto-instrument/contracts/assigns.h

+      const std::string &prefix,
+      const typet &,
+      const source_locationt &) const;


For consistency, add the name of the remaining parameters or remove prefix.

feliperodri · 2021-12-03T19:41:37Z

src/goto-instrument/contracts/utils.cpp

+  symbol_table_baset &symtab,
+  std::string suffix,


Suggested change

symbol_table_baset &symtab,

std::string suffix,

symbol_table_baset &symtab,

std::string &suffix,

feliperodri · 2021-12-03T19:43:28Z

src/goto-instrument/contracts/utils.h

+/// \param suffix: Suffix to use to generate the unique name
+/// \param is_auxiliary: Do not print symbol in traces if true (default = false) 


Suggested change

/// \param suffix: Suffix to use to generate the unique name

/// \param is_auxiliary: Do not print symbol in traces if true (default = false)

/// \param suffix: Suffix to use to generate the unique name.

/// \param is_auxiliary: Do not print symbol in traces if true (default = false).

feliperodri · 2021-12-03T19:45:48Z

src/goto-instrument/contracts/assigns.cpp

+  // adding pragmas to the location to selectively disable checks
+  // where it is sound to do so


I think a brief explanation of "why" is sound to disable checks here would be more helpful, since one can easily infer this comment from the code.

feliperodri · 2021-12-03T19:48:01Z

src/goto-instrument/contracts/assigns.cpp

+
+  // the computation of the CAR upper bound can overflow into the object ID bits
+  // of the pointer with very large allocation sizes.
+  // We enable pointer overflow checks to detect such cases.


Suggested change

// We enable pointer overflow checks to detect such cases.

// We always enable pointer overflow checks to detect such cases.

feliperodri · 2021-12-03T19:48:35Z

src/goto-instrument/contracts/assigns.cpp

+  // remark: both lb and ub are derived from the same object so checking
+  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
+  // is redundant


Nice!

Suggested change

// remark: both lb and ub are derived from the same object so checking

// same_object(upper_bound_address_var, lhs.upper_bound_address_var)

// is redundant

// Both lb and ub are derived from the same object so checking

// same_object(upper_bound_address_var, lhs.upper_bound_address_var)

// is redundant

feliperodri · 2021-12-03T19:49:39Z

src/goto-instrument/contracts/contracts.cpp

@@ -911,6 +911,8 @@ void code_contractst::instrument_call_statement(
  }
  else if(callee_name == "free")
  {
+    source_locationt location_no_checks = instruction_it->source_location();
+    disable_pointer_checks(location_no_checks);


We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

feliperodri · 2021-12-03T19:50:26Z

src/goto-instrument/contracts/contracts.cpp

@@ -1175,6 +1175,10 @@ void code_contractst::check_frame_conditions(
    else if(instruction_it->is_dead())
    {
      const auto &symbol = instruction_it->dead_symbol();
+      source_locationt &location_no_checks =
+        instruction_it->source_location_nonconst();
+      disable_pointer_checks(location_no_checks);


We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

feliperodri · 2021-12-03T19:51:19Z

src/goto-instrument/contracts/contracts.cpp

-  assertion.instructions.back().source_location_nonconst().set_comment(
+  source_locationt location_no_checks =
+    instruction_it->source_location_nonconst();
+  disable_pointer_checks(location_no_checks);


We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

remi-delmas-3000 added dependent - do not merge aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Nov 16, 2021

remi-delmas-3000 requested review from tautschnig, SaswatPadhi and feliperodri November 16, 2021 21:46

remi-delmas-3000 self-assigned this Nov 16, 2021

remi-delmas-3000 requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and romainbrenguier as code owners November 16, 2021 21:46

remi-delmas-3000 mentioned this pull request Nov 16, 2021

Disable redundant automatic checks on assigns clause checking instrumentation [depends-on: #6450] #6455

Closed

7 tasks

remi-delmas-3000 added dependent - do not merge and removed dependent - do not merge labels Dec 2, 2021

remi-delmas-3000 force-pushed the assigns-clause-perf-optim branch from bf54161 to 7c37804 Compare December 2, 2021 22:47

jimgrundy previously requested changes Dec 2, 2021

View reviewed changes

tautschnig approved these changes Dec 3, 2021

View reviewed changes

remi-delmas-3000 force-pushed the assigns-clause-perf-optim branch from 7c37804 to 0b7535c Compare December 3, 2021 16:26

remi-delmas-3000 force-pushed the assigns-clause-perf-optim branch from 0b7535c to 3aee2f7 Compare December 3, 2021 18:09

Remi Delmas added 3 commits December 3, 2021 18:45

Adding readable names for CAR instrumentation variables.

850578b

Disabling pointer checks on CAR inclusion instructions. Enabling poin…

26dc976

…ter overflow checks on CAR upper bound computation.

Fixed test that triggers the newly added pointer overflow checks

e2f4fec

remi-delmas-3000 force-pushed the assigns-clause-perf-optim branch from 3aee2f7 to e2f4fec Compare December 3, 2021 18:45

tautschnig removed the dependent - do not merge label Dec 3, 2021

tautschnig merged commit 1e8e495 into diffblue:develop Dec 3, 2021

feliperodri reviewed Dec 3, 2021

View reviewed changes

		source_locationt &location_no_checks =
		instruction_it->source_location_nonconst();

		@@ -0,0 +1 @@
		Reading GOTO program from '__CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset_with_contracts_harness.c.goto'

		/// \param suffix: Suffix to use to generate the unique name
		/// \param is_auxiliary: Do not print symbol in traces if true (default = false)

		// adding pragmas to the location to selectively disable checks
		// where it is sound to do so

	// We enable pointer overflow checks to detect such cases.
	// We always enable pointer overflow checks to detect such cases.

Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

Uh oh!

Conversation

remi-delmas-3000 commented Nov 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Dec 2, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Dec 3, 2021

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

remi-delmas-3000 commented Nov 16, 2021 •

edited

Loading

codecov bot commented Dec 2, 2021 •

edited

Loading