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

remi-delmas-3000 · 2021-12-11T00:46:46Z

This PR skips some unnecessary instrumentation when checking assigns clauses.

Skipping function parameters

Assignments to variables storing function parameters, as given by symbolt::is_parameter are always legal so we detect them and skip their instrumentation. We do however still add their CARs to the function's write set since they may be aliased and their addresses passed to sub-function calls.

Skipping auxiliary variables

Auxiliary variables, as given by symbolt::is_auxiliary are introduced by the goto compiler to decompose expressions in subexpressions, to store return values for function calls, etc. are only assigned once, cannot have aliases and are really just names for expressions. So we do not add them to the write set anymore, and we skip their assignments in the instrumentation.

Checking loop freeness

We add a check for loop-freeness of the goto-program before attempting a function's assigns clause instrumentation. The assigns clause instrumentation is not sound in the presence of loops, and we did not check this condition before.
To detect loops we compute strongly connected components of the function's control flow graph and detect components that have a cardinality strictly greater than 1.

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.

codecov · 2021-12-11T02:41:03Z

Codecov Report

Merging #6527 (bbe628b) into develop (5f33908) will increase coverage by 0.00%.
The diff coverage is 90.12%.

@@           Coverage Diff            @@
##           develop    #6527   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1578     1578           
  Lines       180910   180976   +66     
========================================
+ Hits        137467   137522   +55     
- Misses       43443    43454   +11

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.cpp	`89.83% <84.31%> (-4.20%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`94.72% <100.00%> (-0.33%)`	⬇️

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 eeddb3f...bbe628b. Read the comment docs.

feliperodri · 2021-12-13T13:51:20Z

regression/contracts/function_check_02/main.c

+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;


Why remove this loop?

This PR adds a loop freeness check before running the instrumentation, so the loop needs to be eliminated to satisfy this loop-freeness check.
This manual unrolling of loops is just a quick and dirty fix. A better solution would be to modify chain.sh add a pass of loop unrolling or loop contracts instrumentation.

regression/contracts/history-pointer-enforce-10/test.desc

regression/contracts/loop-freeness-check/main.c

regression/contracts/quantifiers-forall-requires-enforce/main.c

src/goto-instrument/contracts/contracts.h

src/goto-instrument/contracts/contracts.cpp

feliperodri · 2021-12-13T14:00:44Z

src/goto-instrument/contracts/contracts.cpp

+  INVARIANT(
+    is_loop_free(goto_program),
+    "Loops remain in function '" + id2string(function) +
+      "', assigns clause checking instrumentation cannot be applied.");


src/goto-instrument/contracts/contracts.cpp

…rs and auxiliary variables

…ause instrumentation.

feliperodri

Only a couple of code suggestions.

feliperodri · 2021-12-14T18:50:11Z

src/goto-instrument/contracts/contracts.cpp

-  if(check_for_looped_mallocs(function_obj->second.body))
+  auto &function_body = function_obj->second.body;
+
+  if(check_for_looped_mallocs(function_body))


This check is no longer necessary, you can remove it. It checks whether there is malloc within loops, but we assume contract instrumentation happens after all loops have been unrolled.

feliperodri · 2021-12-14T19:00:44Z

src/goto-instrument/contracts/utils.cpp

+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_parameter;
+
+  return false;


Suggested change

optionalt<symbol_exprt> sym = {};

// extract symbol

if(instruction_it->is_assign())

{

const auto &lhs = instruction_it->assign_lhs();

if(can_cast_expr<symbol_exprt>(lhs))

sym = to_symbol_expr(lhs);

}

// check condition

if(sym.has_value())

return ns.lookup(sym.value().get_identifier()).is_parameter;

return false;

if(instruction_it->is_assign() && can_cast_expr<symbol_exprt>(instruction_it->assign_lhs()))

{

// Extract symbol from lhs

auto lhs_sym = to_symbol_expr(instruction_it->assign_lhs());

// Check whether is parameter

if(lhs_sym.has_value())

return ns.lookup(lhs_sym.value().get_identifier()).is_parameter;

}

return false;

On top of what Felipe suggested: there's no need for the optionalt anymore.

feliperodri · 2021-12-14T19:26:43Z

src/goto-instrument/contracts/utils.cpp

+bool is_auxiliary_decl_dead_or_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns)
+{
+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_decl())
+    sym = instruction_it->decl_symbol();
+  else if(instruction_it->is_dead())
+    sym = instruction_it->dead_symbol();
+  else if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_auxiliary;
+
+  return false;
+}


Suggested change

bool is_auxiliary_decl_dead_or_assign(

const goto_programt::targett &instruction_it,

namespacet &ns)

{

optionalt<symbol_exprt> sym = {};

// extract symbol

if(instruction_it->is_decl())

sym = instruction_it->decl_symbol();

else if(instruction_it->is_dead())

sym = instruction_it->dead_symbol();

else if(instruction_it->is_assign())

{

const auto &lhs = instruction_it->assign_lhs();

if(can_cast_expr<symbol_exprt>(lhs))

sym = to_symbol_expr(lhs);

}

// check condition

if(sym.has_value())

return ns.lookup(sym.value().get_identifier()).is_auxiliary;

return false;

}

bool is_auxiliary_decl_dead_or_assign(

const goto_programt::targett &instruction_it,

namespacet &ns)

{

// Extract symbol

optionalt<symbol_exprt> sym = {};

if(instruction_it->is_assign() && can_cast_expr<symbol_exprt>(instruction_it->assign_lhs()))

sym = to_symbol_expr(instruction_it->assign_lhs());

else if(instruction_it->is_decl())

sym = instruction_it->decl_symbol();

else if(instruction_it->is_dead())

sym = instruction_it->dead_symbol();

else

return false;

// Check whether is auxiliary

return ns.lookup(sym.value().get_identifier()).is_auxiliary;

}

feliperodri · 2021-12-14T19:27:18Z

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 &it : goto_program.instructions)

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

it.turn_into_skip();

}

feliperodri · 2021-12-14T19:28:35Z

src/goto-instrument/contracts/utils.cpp

+    auto size = scc_size[scc_id];
+    if(size > 1)
+    {
+      all_size_one = false;


We could add a regression test to explore these paths.

tautschnig · 2021-12-14T21:47:05Z

src/goto-instrument/contracts/contracts.cpp

+    // do not skip checks on function parameter assignments
+    false);


If we see a need to comment on the Boolean value then it may be better to introduce an enum that has informative values. If we always pass constant values, then it might be even better to use a template parameter.

tautschnig · 2021-12-14T21:49:58Z

src/goto-instrument/contracts/utils.h

+/// \param is_auxiliary: Do not print symbol in traces if true (default = true)
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
  const typet &type,
  const source_locationt &location,
  const irep_idt &mode,
  symbol_table_baset &symtab,
  std::string suffix = "tmp_cc",
-  bool is_auxiliary = false);
+  bool is_auxiliary = true);


Why is this being changed as part of this PR?

tautschnig · 2021-12-14T21:52:45Z

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);
+


You wouldn't have quite as elaborate error messages, but wouldn't a simple test of all instructions for is_backwards_goto() do the trick?

remi-delmas-3000 · 2021-12-17T14:58:27Z

superseded by #6533

remi-delmas-3000 requested review from tautschnig and feliperodri December 11, 2021 00:46

remi-delmas-3000 requested a review from SaswatPadhi as a code owner December 11, 2021 00:46

remi-delmas-3000 force-pushed the exclude-auxiliaries-from-assigns-clause-checking branch from 2c9c2aa to 7fa006e Compare December 11, 2021 01:26

feliperodri assigned remi-delmas-3000 Dec 13, 2021

feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Dec 13, 2021

feliperodri requested changes Dec 13, 2021

View reviewed changes

remi-delmas-3000 force-pushed the exclude-auxiliaries-from-assigns-clause-checking branch from f069a4c to f0f6dca Compare December 13, 2021 16:09

Function contracts: skip assigns clause checking on function paramete…

b847942

…rs and auxiliary variables

remi-delmas-3000 force-pushed the exclude-auxiliaries-from-assigns-clause-checking branch 2 times, most recently from ad4d9db to 08c7f2a Compare December 13, 2021 18:24

Function contracts: check for the presence of loops before assigns cl…

bbe628b

…ause instrumentation.

remi-delmas-3000 force-pushed the exclude-auxiliaries-from-assigns-clause-checking branch from 08c7f2a to bbe628b Compare December 13, 2021 21:43

feliperodri approved these changes Dec 14, 2021

View reviewed changes

tautschnig reviewed Dec 14, 2021

View reviewed changes

feliperodri added the enhancement label Dec 15, 2021

feliperodri mentioned this pull request Dec 17, 2021

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

Merged

6 tasks

remi-delmas-3000 closed this Dec 17, 2021

		// do not skip checks on function parameter assignments
		false);

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

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

Uh oh!

Conversation

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

Uh oh!

Skipping function parameters

Skipping auxiliary variables

Checking loop freeness

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 Dec 13, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

feliperodri Dec 14, 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!

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 17, 2021

Uh oh!

Uh oh!

remi-delmas-3000 commented Dec 11, 2021 •

edited by feliperodri

Loading

codecov bot commented Dec 11, 2021 •

edited

Loading

remi-delmas-3000 Dec 13, 2021 •

edited

Loading

feliperodri Dec 14, 2021 •

edited

Loading