Fix local static variables detection in assigns clauses #6447

remi-delmas-3000 · 2021-11-08T18:19:37Z

Function contracts instrumentation:

Use the call graph of the function to detect local static variables declared in the functions it calls.

Other changes:

subfunction call inlining was moved from code_contractst::check_frame_conditions to code_contractst::check_frame_conditions_function.
Recursive functions are now detected during inlining and cause an INVARIANT violation
Function pointers are now detected during call graph construction and cause a PRECONDITION violation

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.

SaswatPadhi · 2021-11-08T18:26:24Z

src/goto-instrument/contracts/contracts.cpp

@@ -861,7 +861,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
  for(const auto &sym_pair : symbol_table)
  {
    const auto &sym = sym_pair.second;
-    if(sym.is_static_lifetime && sym.location.get_function() == function)
+    if(sym.is_static_lifetime && !sym.location.get_function().empty())


Wouldn't this create CARs for ALL static local variables, like beyond the current function on which contracts are checked and its subfunction calls?

It might have a significant perf impact if lots of unrelated functions also introduce static local variables, because we'll add their CARs unnecessarily to the write set and check every assignment against them.

It might be worth fixing the inlining routine instead. Inlined static locals should just behave as static locals within the caller. It seems weird and inconsistent to have the function body inlined into a caller but be mutating a static local that's tagged with a different function name.

Indeed.
Since all sub-function calls are inlined for contract checking, a better solution would be to detect static locals used in the body of the function under analysis rather than at the symbol table level.

remi-delmas-3000 · 2021-11-08T19:32:15Z

Updated to a better solution is to detect static locals used in the body of the function under analysis rather than at the symbol table level.

codecov · 2021-11-08T22:32:49Z

Codecov Report

Merging #6447 (59d15d6) into develop (c13e416) will decrease coverage by 0.02%.
The diff coverage is 100.00%.

❗ Current head 59d15d6 differs from pull request most recent head 5fb8ee5. Consider uploading reports for the commit 5fb8ee5 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6447      +/-   ##
===========================================
- Coverage    76.04%   76.01%   -0.03%     
===========================================
  Files         1546     1527      -19     
  Lines       165543   164487    -1056     
===========================================
- Hits        125885   125035     -850     
+ Misses       39658    39452     -206

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/contracts.cpp	`96.27% <100.00%> (-0.83%)`	⬇️
...rc/solvers/smt2_incremental/smt_solver_process.cpp	`25.00% <0.00%> (-49.08%)`	⬇️
src/solvers/smt2_incremental/smt_solver_process.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/util/pointer_predicates.cpp	`71.60% <0.00%> (-21.95%)`	⬇️
unit/solvers/smt2/smt2irep.cpp	`83.09% <0.00%> (-16.91%)`	⬇️
...ncremental/smt2_incremental_decision_procedure.cpp	`78.43% <0.00%> (-11.26%)`	⬇️
src/util/piped_process.cpp	`76.92% <0.00%> (-3.85%)`	⬇️
src/goto-symex/symex_function_call.cpp	`93.18% <0.00%> (-2.28%)`	⬇️
src/goto-symex/ssa_step.cpp	`79.31% <0.00%> (-2.07%)`	⬇️
... and 69 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 40fd86b...5fb8ee5. Read the comment docs.

feliperodri

Only minor requests.

regression/contracts/assigns_enforce_statics_subfunctions/main.c

regression/contracts/assigns_enforce_statics_subfunctions/test.desc

feliperodri · 2021-11-10T20:16:24Z

regression/contracts/assigns_enforce_statics_subfunctions/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-contract bar _ --pointer-primitive-check


Why do we need --pointer-primitive-check here?

Why is there an underscore here (after bar)?

this underscore separates two groups of options , the first group is passed to goto-instrument to perform the contract instrumentation, and the second set is passed to cbmc to analyse the instrumented contracts.

src/goto-instrument/contracts/contracts.cpp

src/goto-instrument/contracts/contracts.h

src/goto-instrument/contracts/contracts.cpp

feliperodri

Almost there.

regression/contracts/assigns_enforce_statics/main.c

regression/contracts/assigns_enforce_statics_subfunctions/test1.c

regression/contracts/assigns_enforce_statics_subfunctions/test2.c

regression/contracts/assigns_enforce_statics_subfunctions/test2.desc

feliperodri

LGTM modulo a few minor comments.

regression/contracts/assigns_enforce_statics_subfunctions/main.c

feliperodri · 2021-11-16T22:10:18Z

regression/contracts/assigns_enforce_statics_subfunctions/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-contract bar _ --pointer-primitive-check


src/goto-instrument/contracts/contracts.cpp

feliperodri · 2021-11-16T22:13:03Z

src/goto-instrument/contracts/contracts.h

+  /// \brief Finds symbols declared with a static lifetime in the given
+  /// `root_function` or one of the functions it calls,
+  /// and adds them to the given `assigns`.
+  ///
+  /// @param functions all functions of the goto_model
+  /// @param root_function the root function under which to search statics
+  /// @param assigns assigns clause where search results are added
+  ///
+  /// A symbol is considered a static local symbol iff:
+  /// - it has a static lifetime annotation
+  /// - its source location has a non-empty function attribute
+  /// - this function attribute is found in the call graph of the root_function


Suggested change

/// \brief Finds symbols declared with a static lifetime in the given

/// `root_function` or one of the functions it calls,

/// and adds them to the given `assigns`.

///

/// @param functions all functions of the goto_model

/// @param root_function the root function under which to search statics

/// @param assigns assigns clause where search results are added

///

/// A symbol is considered a static local symbol iff:

/// - it has a static lifetime annotation

/// - its source location has a non-empty function attribute

/// - this function attribute is found in the call graph of the root_function

/// \brief Finds symbols declared with a static lifetime in the given

/// `root_function` or one of the functions it calls,

/// and adds them to the given `assigns`.

///

/// @param functions All functions of the `goto_model`.

/// @param root_function The root function under which to search statics.

/// @param assigns Assigns clause where search results are added.

///

/// A symbol is considered a static local symbol iff:

/// - it has a static lifetime annotation;

/// - its source location has a non-empty function attribute;

/// - this function attribute is found in the call graph of the `root_function`.

remi-delmas-3000 · 2021-11-17T16:41:59Z

We are now collecting symbols from the symbol table that have a static lifetime and are declare in functions occurring in the call graph of the function under analysis

tautschnig · 2021-11-19T16:01:59Z

regression/contracts/assigns_enforce_statics_subfunctions/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-contract bar _ --pointer-primitive-check


Why is there an underscore here (after bar)?

tautschnig · 2021-11-19T16:05:41Z

regression/contracts/assigns_enforce_statics/main.c

-#include <stdlib.h>
-
-static int x;
+static int x = 0;


Random place for comment: the commit message ...

Could make clear that this is about code contracts;

Should likely have the "A symbol is ..." all moved into the body of the message;

Should likely talk about "called functions" instead of "subfunctions."

src/goto-instrument/contracts/contracts.cpp

tautschnig · 2021-11-19T16:52:38Z

src/goto-instrument/contracts/contracts.cpp

@@ -853,18 +856,16 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
    function,
    symbol_table);

-  // Adds formal parameters to write set
+  // fetch local statics of all subfunctions in the symbol_table


Much like the commit message: I don't think "subfunctions" is the right terminology.

tautschnig · 2021-11-19T16:53:17Z

src/goto-instrument/contracts/contracts.cpp

+  // Full inlining of the function body
+  goto_function_inline(goto_functions, function, ns, log.get_message_handler());


I think the comment could be more useful if it explained why full inlining was necessary. (Also, will this work with recursive functions?)

the reason behind inlining is that in the function f we are instrumenting , a same function g can be called in several locations under different write sets.
Without inlining, for each call site we would have to create a copy of g and instrument for the write set specific to this call site.
Inlining allows us to avoid having to duplicate g and instrument it specifically.

As for inlining recursive functions, I'll implement a check to detect them and error out during inlining

tautschnig · 2021-11-19T16:54:23Z

src/goto-instrument/contracts/contracts.cpp

+        // - this function appears in the call graph of the function
+        assigns.add_to_write_set(sym.symbol_expr());


What about function pointers?

we suppose function pointers have been removed/restricted before this instrumentation phase so that all possible target functions would appear explicitly in the call graph

Hmm, we should really include a PRECONDITION in call_graph.cpp's forall_callsites to replace if(function_expr.id()==ID_symbol) by PRECONDITION_WITH_DIAGNOSTICS(function_expr.id() == ID_symbol, "call graph computation requires function pointer removal");.

PRECONDITION added in call_graph.cpp.

Should we also modify goto_function_inline to warn on unresolved function pointers ?

Yes, we should either warn or fail with a PRECONDITION.

SaswatPadhi

Some minor comments:

src/goto-instrument/contracts/contracts.cpp

src/goto-instrument/contracts/contracts.h

src/goto-instrument/contracts/contracts.cpp

SaswatPadhi

LGTM 🎉

SaswatPadhi · 2021-11-22T19:43:13Z

regression/contracts/function-calls-recursive-01/main.c

+  int result = sum(10);
+  __CPROVER_assert(result == 55, "result == 55");
+  return 0;
+}


[nit] missing newline

feliperodri · 2021-11-22T22:36:20Z

@chrisr-diffblue @martin-cs @peterschrammel could you review this PR? It's missing code owner approval.

SaswatPadhi

Couple of minor nitpicks but nothing that would block the merge.

SaswatPadhi · 2021-11-22T23:32:01Z

src/goto-instrument/contracts/assigns.cpp

@@ -15,6 +15,8 @@ Date: July 2021

 #include <langapi/language_util.h>

+#include <analyses/call_graph.h>


[nit] this should go above langapi include(s).

SaswatPadhi · 2021-11-22T23:32:29Z

src/goto-instrument/contracts/assigns.cpp

+      }
+    }
+  }
+  return;


Redundant return

…call graph add INVARIANT for recursive functions and PRECONDITION for function pointers. - Static local variables declared in functions called by the function under analysis are now added the write set (same for loops) - `code_contractst::check_frame_conditions_function` now errors out on recursive functions - `call_grapht::forall_callsites` now errors out on function pointers

peterschrammel

Nothing blocking, just a few remarks for future work:
That's quite a lot in a single commit. It could have been split into a series of commits:

introduce decorator
add new tests
add static local detection
other changes 1
other changes 2
other changes 3
activate/modify tests (separately or with the corresponding commit that makes the test pass)

each of which with a 'why' description in the commit body to make the intent of the PR clearer and easier and faster to review.

peterschrammel · 2021-12-01T15:23:02Z

src/goto-instrument/contracts/contracts.cpp

@@ -29,6 +29,7 @@ Date: February 2016



This is file is getting way to large. Consider refactoring/splitting in future.

remi-delmas-3000 requested review from feliperodri, SaswatPadhi and tautschnig as code owners November 8, 2021 18:19

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high labels Nov 8, 2021

remi-delmas-3000 changed the title ~~Fixes local static variables detection.~~ Fix local static variables detection in assigns clause checking instrumentation Nov 8, 2021

SaswatPadhi reviewed Nov 8, 2021

View reviewed changes

remi-delmas-3000 closed this Nov 8, 2021

remi-delmas-3000 reopened this Nov 8, 2021

feliperodri requested changes Nov 10, 2021

View reviewed changes

feliperodri assigned remi-delmas-3000 Nov 10, 2021

feliperodri added the Code Contracts Function and loop contracts label Nov 10, 2021

feliperodri reviewed Nov 10, 2021

View reviewed changes

src/goto-instrument/contracts/contracts.cpp Outdated Show resolved Hide resolved

feliperodri requested changes Nov 16, 2021

View reviewed changes

remi-delmas-3000 force-pushed the fix-local-statics-detection branch 2 times, most recently from 1b03a35 to 0531588 Compare November 16, 2021 18:24

This was referenced Nov 16, 2021

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

Closed

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

Merged

feliperodri requested review from feliperodri and SaswatPadhi November 16, 2021 22:09

feliperodri approved these changes Nov 16, 2021

View reviewed changes

feliperodri added the bugfix label Nov 16, 2021

feliperodri changed the title ~~Fix local static variables detection in assigns clause checking instrumentation~~ Fix local static variables detection in assigns clauses Nov 16, 2021

tautschnig reviewed Nov 19, 2021

View reviewed changes

SaswatPadhi reviewed Nov 19, 2021

View reviewed changes

src/goto-instrument/contracts/contracts.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/contracts.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/contracts.h Outdated Show resolved Hide resolved

remi-delmas-3000 force-pushed the fix-local-statics-detection branch from 0531588 to f89fcd4 Compare November 19, 2021 22:18

tautschnig reviewed Nov 20, 2021

View reviewed changes

remi-delmas-3000 force-pushed the fix-local-statics-detection branch from f89fcd4 to 09e7bcb Compare November 22, 2021 17:34

remi-delmas-3000 requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners November 22, 2021 17:34

remi-delmas-3000 force-pushed the fix-local-statics-detection branch 2 times, most recently from b64d75b to 3023ccb Compare November 22, 2021 18:42

SaswatPadhi approved these changes Nov 22, 2021

View reviewed changes

remi-delmas-3000 force-pushed the fix-local-statics-detection branch from 3023ccb to 3dfdd56 Compare November 22, 2021 22:24

feliperodri requested a review from tautschnig November 22, 2021 22:35

SaswatPadhi reviewed Nov 23, 2021

View reviewed changes

remi-delmas-3000 force-pushed the fix-local-statics-detection branch 2 times, most recently from 455425e to 200246c Compare November 23, 2021 15:01

remi-delmas-3000 force-pushed the fix-local-statics-detection branch from 200246c to df40139 Compare November 30, 2021 21:56

tautschnig approved these changes Nov 30, 2021

View reviewed changes

remi-delmas-3000 force-pushed the fix-local-statics-detection branch from df40139 to 5fb8ee5 Compare November 30, 2021 23:58

tautschnig assigned peterschrammel and martin-cs and unassigned remi-delmas-3000 Dec 1, 2021

peterschrammel approved these changes Dec 1, 2021

View reviewed changes

tautschnig merged commit 5750c68 into diffblue:develop Dec 1, 2021

		// Full inlining of the function body
		goto_function_inline(goto_functions, function, ns, log.get_message_handler());

		// - this function appears in the call graph of the function
		assigns.add_to_write_set(sym.symbol_expr());

		@@ -15,6 +15,8 @@ Date: July 2021

		#include <langapi/language_util.h>

		#include <analyses/call_graph.h>

Fix local static variables detection in assigns clauses #6447

Fix local static variables detection in assigns clauses #6447

Uh oh!

Conversation

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

Uh oh!

Uh oh!

SaswatPadhi Nov 8, 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!

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

Uh oh!

Uh oh!

codecov bot commented Nov 8, 2021 • 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!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Nov 17, 2021

Uh oh!

Choose a reason for hiding this comment

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!

remi-delmas-3000 Nov 19, 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!

remi-delmas-3000 commented Nov 8, 2021 •

edited

Loading

SaswatPadhi Nov 8, 2021 •

edited

Loading

remi-delmas-3000 commented Nov 8, 2021 •

edited

Loading

codecov bot commented Nov 8, 2021 •

edited

Loading

remi-delmas-3000 Nov 19, 2021 •

edited

Loading

peterschrammel left a comment •

edited

Loading