Function contracts: check loop freeness before instrumentation, skip assignments to locals and prune write set using CFG info. #6533

remi-delmas-3000 · 2021-12-16T23:18:04Z

The first two commits are from this draft PR #6525 which adds a maybe_alive bit to local_bitvector_analysist and is needed by this PR.

This PR adds:

In check_frame_conditions_function:

a pass that simplifies away GOTO instructions for which the guard is always false
a check that the program is loop-free before attempting instrumentation
manual loop unrolling in regression tests that still contained loops and are got rejected because of this new check

For assigns clause checking:

Assigning to local variables or function parameter variables is always legal so we skip instrumenting these assignments,
We avoid adding function parameters and local variables to the local write set, except when their address is taken at some point in the program and can later be assigned to indirectly via pointers.
When generating inclusion checks for assignments, we remove from the local write set targets which are not possibly alive at the ASSIGN instruction that gets instrumented.
Tests have been simplified by removing function parameters from assigns clauses, and removing function parameters and local variables from test specifications.

The net effect of these changes is a better proof performance because of a reduction in the number of generated assertions and of their size, but otherwise the contract checking functionality remains unchanged.

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.
[ x] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

How does this relate to #6527?

regression/contracts/assigns_enforce_04/test.desc

tautschnig · 2021-12-16T23:50:41Z

src/goto-instrument/contracts/assigns.cpp

@@ -20,6 +20,7 @@ Date: July 2021

 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/format_expr.h>


Debugging leftover?

tautschnig · 2021-12-16T23:51:58Z

src/goto-instrument/contracts/contracts.cpp

+    "Loops remain in function '" + id2string(function) +
+      "', assigns clause checking instrumentation cannot be applied.");
+
+  // Create a deep copy of the iriginal goto_function object


s/iriginal/original/

tautschnig · 2021-12-16T23:55:00Z

src/goto-instrument/contracts/contracts.cpp

+    if(can_cast_expr<symbol_exprt>(lhs))
+      return !cfg_info_opt.value().is_local(
+        to_symbol_expr(lhs).get_identifier());


With can_cast_expr you can use

if(auto lhs_symbol = can_cast_expr<symbol_exprt>(lhs)) return !cfg_info_opt->is_local(lhs_symbol->get_identifier());

lhs_symbol would be a boolean in that case, not the result of the cast ?

tautschnig · 2021-12-16T23:57:55Z

src/goto-instrument/contracts/utils.h

+      target(goto_function.body.instructions.begin()),
+      bitvector_analysis(goto_function, ns),
+      dirty_analysis(goto_function),
+      dirty_idents(dirty_analysis.get_dirty_ids()),


Why do you copy these instead of using dirty_analysis when needed?

codecov · 2021-12-17T00:27:44Z

Codecov Report

Merging #6533 (f7752cf) into develop (8834dc5) will decrease coverage by 0.00%.
The diff coverage is 93.45%.

@@             Coverage Diff             @@
##           develop    #6533      +/-   ##
===========================================
- Coverage    75.98%   75.98%   -0.01%     
===========================================
  Files         1578     1578              
  Lines       180919   181032     +113     
===========================================
+ Hits        137476   137551      +75     
- Misses       43443    43481      +38

Impacted Files	Coverage Δ
src/goto-instrument/contracts/assigns.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.cpp	`89.47% <78.57%> (-4.56%)`	⬇️
src/goto-instrument/contracts/assigns.cpp	`95.83% <90.00%> (-0.60%)`	⬇️
src/analyses/goto_check_c.cpp	`90.29% <92.30%> (-0.10%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`91.13% <98.46%> (-3.99%)`	⬇️
src/goto-instrument/contracts/utils.h	`100.00% <100.00%> (ø)`
src/goto-programs/goto_convert.cpp	`92.03% <100.00%> (+0.07%)`	⬆️
src/analyses/dirty.h	`100.00% <0.00%> (ø)`
... and 2 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 4ec7d9b...f7752cf. Read the comment docs.

src/goto-instrument/contracts/assigns.cpp

src/goto-instrument/contracts/contracts.cpp

feliperodri · 2021-12-17T13:41:44Z

src/goto-instrument/contracts/contracts.cpp

+    // skip checks on function parameter assignments
+    true,


This should really be an enum.

An enum with TRUE and FALSE values ?

A 2-value enum, where the "true" and "false" values carry meaningful names.

Fixed.
Following that logic we should change all bool return types to SUCCESS/FAILURE for

replace_calls,
-enforce_contracts,

enforce_contract,

check_frame_conditions_function,

apply_function_contract,

src/goto-instrument/contracts/contracts.cpp

feliperodri · 2021-12-17T13:46:55Z

src/goto-instrument/contracts/contracts.cpp

+  // Unless proved non-dirty by the CFG analysis we assume it is dirty.
+  if(!cfg_info_opt.has_value())
+    return true;
+
+  return cfg_info_opt.value().is_not_local_or_dirty_local(
+    target->dead_symbol().get_identifier());


Suggested change

// Unless proved non-dirty by the CFG analysis we assume it is dirty.

if(!cfg_info_opt.has_value())

return true;

return cfg_info_opt.value().is_not_local_or_dirty_local(

target->dead_symbol().get_identifier());

// Unless proved non-dirty by the CFG analysis we assume it is dirty.

if(cfg_info_opt.has_value())

return cfg_info_opt.value().is_not_local_or_dirty_local(

target->dead_symbol().get_identifier());

return true;

feliperodri · 2021-12-17T13:47:16Z

src/goto-instrument/contracts/contracts.cpp

  {
-    const auto &pragmas = instruction_it->source_location().get_pragmas();
-    if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end())
+    // skip instructions marked as disabled for assigns clause checking


Suggested change

// skip instructions marked as disabled for assigns clause checking

// Skip instructions marked as disabled for assigns clause checking.

src/goto-instrument/contracts/contracts.cpp

src/goto-instrument/contracts/contracts.h

src/goto-instrument/contracts/utils.cpp

remi-delmas-3000 · 2021-12-17T15:30:05Z

The dependency on local_bitvector_analysist and #6533 was removed

feliperodri

Only minor comments left.

feliperodri · 2021-12-17T18:02:03Z

src/goto-instrument/contracts/utils.cpp

+void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_goto())
+    {
+      const auto &condition = instruction.get_condition();
+      const auto &simplified = simplify_expr(condition, ns);
+      if(simplified.is_false())
+        instruction.turn_into_skip();
+    }
+  }
+}


Suggested change

void simplify_gotos(goto_programt &goto_program, namespacet &ns)

{

for(auto &instruction : goto_program.instructions)

{

if(instruction.is_goto())

{

const auto &condition = instruction.get_condition();

const auto &simplified = simplify_expr(condition, ns);

if(simplified.is_false())

instruction.turn_into_skip();

}

}

}

void simplify_gotos(goto_programt &goto_program, namespacet &ns)

{

for(auto &instruction : goto_program.instructions)

if(instruction.is_goto() && simplify_expr(instruction.get_condition(), ns).is_false())

instruction.turn_into_skip();

}

tautschnig · 2021-12-17T21:56:57Z

src/goto-instrument/contracts/assigns.cpp

+bool assigns_clauset::conditional_address_ranget::maybe_alive(
+  cfg_infot &cfg_info) const
+{
+  if(can_cast_expr<symbol_exprt>(source_expr))


As discussed earlier today: could be implemented using if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(source_expr))

tautschnig · 2021-12-17T21:59:08Z

src/goto-instrument/contracts/assigns.cpp

+    auto &cfg_info = cfg_info_opt.value();
+    for(const auto &target : write_set)
+      if(target.maybe_alive(cfg_info))
+        conditions.push_back(target.generate_unsafe_inclusion_check(lhs));


Will this actually introduce the same check in multiple places? Wouldn't it be sufficient to check this once?

it generates an inclusion check for each possible target of the write set, and each check is specify to the lhs of the instrumented assignment, so no doublons are created here.

tautschnig · 2021-12-17T22:00:50Z

src/goto-instrument/contracts/contracts.cpp

+    // skip checks on function parameter assignments
+    true,


A 2-value enum, where the "true" and "false" values carry meaningful names.

tautschnig · 2021-12-17T22:02:19Z

src/goto-instrument/contracts/contracts.cpp


  return false;
 }

+/// Returns true iff the target instruction is tagged with a
+/// 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma.
+bool has_disable_assigns_check_pragma(const goto_programt::targett &target)


Do you really want an iterator that cannot change (const goto_programt::targett&) or an iterator so that whatever it points to cannot change (goto_programt::const_targett)?

Both! Thanks for the tip

tautschnig · 2021-12-17T22:04:10Z

src/goto-instrument/contracts/utils.cpp

+bool is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log)
+{
+  // create cfg from instruction list
+  cfg_baset<empty_cfg_nodet> cfg;
+  cfg(goto_program);


Comment from the earlier PR: do you really need such an elaborate analysis, or would looking at is_backwards_goto() for all instructions in goto_program also do the trick?

Hmm, that indeed does not imply the existence of a loop. But then, would natural_loopst do the trick here and relieve you of some of the heavy lifting?

…ing. - don't instrument assignments to locals and function parameters, - don't add function parameters and non-dirty locals to the write set, - remove from the local write set CARs that are provably not alive, - remove function parameters and locals from assigns clauses in tests. Sanity checks: - change GOTO instruction with false guards into SKIP instructions (removes artificial loops), - check loop-freeness before assigns clause instrumentation (required for soundness of assigns clause checking). The net effect of these changes is a better proof performance because of a reduction in the number of generated assertions and of their size, but otherwise the contract checking functionality remains unchanged. Rationale: Assigning to local variables or function parameter is always legal so we skip instrumenting these assignments. We avoid adding function parameters and local variables to the local write set, except when their address is taken at some point in the program and can later be assigned to indirectly via pointers. When generating inclusion checks for assignments, we remove from the local write set targets which are not possibly alive at the ASSIGN instruction that gets instrumented.

remi-delmas-3000 requested review from chrisr-diffblue, feliperodri, martin-cs, peterschrammel, SaswatPadhi and tautschnig as code owners December 16, 2021 23:18

remi-delmas-3000 assigned tautschnig and remi-delmas-3000 Dec 16, 2021

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts enhancement labels Dec 16, 2021

tautschnig reviewed Dec 16, 2021

View reviewed changes

feliperodri requested changes Dec 17, 2021

View reviewed changes

remi-delmas-3000 mentioned this pull request Dec 17, 2021

Skip function parameters and auxiliary variables when checking assigns clauses and check loop-freeness #6527

Closed

7 tasks

remi-delmas-3000 force-pushed the function-contracts-prune-write-set branch from 40409fa to d2ba49f Compare December 17, 2021 16:15

feliperodri approved these changes Dec 17, 2021

View reviewed changes

feliperodri requested a review from tautschnig December 17, 2021 18:03

tautschnig reviewed Dec 17, 2021

View reviewed changes

tautschnig removed their assignment Dec 17, 2021

remi-delmas-3000 force-pushed the function-contracts-prune-write-set branch from d2ba49f to d05ed7c Compare December 17, 2021 23:03

remi-delmas-3000 force-pushed the function-contracts-prune-write-set branch from d05ed7c to f7752cf Compare December 17, 2021 23:37

remi-delmas-3000 merged commit f351d5e into diffblue:develop Dec 18, 2021

	// skip instructions marked as disabled for assigns clause checking
	// Skip instructions marked as disabled for assigns clause checking.

Function contracts: check loop freeness before instrumentation, skip assignments to locals and prune write set using CFG info. #6533

Function contracts: check loop freeness before instrumentation, skip assignments to locals and prune write set using CFG info. #6533

Conversation

remi-delmas-3000 commented Dec 16, 2021

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

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!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

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 Dec 17, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

Uh oh!

Uh oh!

remi-delmas-3000 commented Dec 17, 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

codecov bot commented Dec 17, 2021 •

edited

Loading

remi-delmas-3000 Dec 17, 2021 •

edited

Loading