CONTRACTS: New class `instrument_spec_assignst` encapsulating assigns clause checking logic. #6575

remi-delmas-3000 · 2022-01-13T04:38:37Z

The previous assigns_clauset class leaked its internal representations to the outside world and important control logic was spread between assigns.cpp and contracts.cpp.

New classes:

New class conditional_target_exprt deriving exprt: represents a single conditional target from the source program
New classconditional_address_range_exprt deriving exprt: represents a CAR derived from a conditional target
New class instrument_spec_assignst encapsulating assigns clause checking algos:
- 3 methods to track targets by origin (from an assigns clause , from a DECL, from a malloc)
- 1 method to detect local static variables used directly or indirectly by the function
- 1 method to check assignments
- 1 method to invalidate DEAD objects
- 1 method to check freed objects and invalidate aliased CARs
The generated assertions now have property class "assigns" for better console output

Changes:

The function havoc_assigns_clause_targets is now a class havoc_assigns_clause_targetst that inherits from instrument_spec_assignst and reuses all the snapshotting and target validity checking conditions
Removed code from contracts.cpp that now lives in instrument_spec_assignst
Function and loop contracts instrumentations now use the new classes

No performance changes expected.

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.

tautschnig

Just some preliminary comments below. Overall, this is really hard to review as it's hard to tell what is a change in behaviour (if any?) and what is just refactoring. It it truly were refactoring-only then surely no tests should change. Having this split up in several commits would have helped a lot.

tautschnig · 2022-01-13T16:50:20Z

src/goto-instrument/contracts/contracts.cpp

+  // ^^^ FIXME ^^^ we should only allow assignments to static locals
+  // declared in functions that are called in the loop body, not from the whole
+  // function...


Are we tracking this task somewhere?

tautschnig · 2022-01-13T16:51:55Z

src/goto-instrument/contracts/contracts.cpp

+        auto payload = instrument_spec_assigns.track_spec_target(target);
+        snapshot_instructions.destructive_append(payload);


Would it perhaps make for a better interface if snapshot_instructions were passed as an argument?

I refactored the API to use destination passing style, but since sometimes we have to append instructions, or to insert them before a target, or after a target, with or without swapping, we often end up having to declare a temporary goto_programt destination anyway.

tautschnig · 2022-01-13T16:52:32Z

src/goto-instrument/contracts/contracts.cpp

-    insert_before_swap_and_advance(
-      goto_function.body, loop_head, snapshot_instructions);
-  };
+  // ^^^ FIXME this is not true ^^^


Can we just fix this now?

this actually depends on wether

a loop assigns clause is meant to represent the whole set of locations ever touched by the loop until completion, and hence

no target expression should depend on other expressions also touched by the loop (i.e. we do not allow array slice expressions a[0..i]),

it can be snapshotted before havoc+invariants

or

it should summarize an arbitrary execution prefix of the loop, in which case:

a target expressions could depend on each other like (i, a[0..i])

targets should be snapshotted after havocking and assuming the invariant.

the whole clause should be proved to be included in itself post loop-step

and we have not really decided on the semantics yet.

tautschnig · 2022-01-13T16:54:33Z

src/goto-instrument/contracts/contracts.cpp

  }
 }

+#if 0


At least a comment would be really helpful here.

this was leftover from refactoring, now removed

tautschnig · 2022-01-13T16:54:51Z

src/goto-instrument/contracts/contracts.h

 #include <util/pointer_expr.h>

-#include "assigns.h"
+// #include "assigns.h"


Just remove it. It's very easy to re-add if needed...

tautschnig · 2022-01-13T16:55:01Z

src/goto-instrument/contracts/contracts.h

    skipt skip_parameter_assigns,
    optionalt<cfg_infot> &cfg_info_opt);

+#if 0


Comment, please.

codecov · 2022-01-14T04:42:38Z

Codecov Report

Merging #6575 (63d03bc) into develop (57e7b2c) will decrease coverage by 0.00%.
The diff coverage is 81.42%.

@@             Coverage Diff             @@
##           develop    #6575      +/-   ##
===========================================
- Coverage    76.65%   76.64%   -0.01%     
===========================================
  Files         1579     1580       +1     
  Lines       181294   181542     +248     
===========================================
+ Hits        138973   139148     +175     
- Misses       42321    42394      +73

Impacted Files	Coverage Δ
src/analyses/goto_rw.cpp	`52.30% <0.00%> (-0.13%)`	⬇️
src/analyses/uncaught_exceptions_analysis.h	`100.00% <ø> (ø)`
src/ansi-c/ansi_c_parser.cpp	`88.39% <0.00%> (ø)`
src/cpp/cpp_declarator_converter.h	`100.00% <ø> (ø)`
src/cpp/cpp_exception_id.cpp	`0.00% <0.00%> (ø)`
src/cpp/cpp_template_type.h	`64.28% <0.00%> (-17.54%)`	⬇️
src/cpp/cpp_typecheck.cpp	`79.22% <0.00%> (ø)`
src/cpp/cpp_typecheck_initializer.cpp	`29.09% <0.00%> (-0.36%)`	⬇️
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-programs/interpreter.cpp	`52.29% <0.00%> (ø)`
... and 102 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 637f138...63d03bc. Read the comment docs.

SaswatPadhi

Below are some minor initial comments based on a quick look at the changes.

I share the same concern as @tautschnig, that the change is huge (even ignoring the regression tests) and so is kind of hard to review. The new assigns clause code is MUCH larger than the previous assigns.cpp code and to me it seems quite complex (but I am also looking at it after a long time, and after the conditional assigns clause stuff was added).

My requests are to split the PR to multiple smaller commits if possible, and also add some description to the PR and/or the commit message as to why having these exprt subclasses is desirable.

SaswatPadhi · 2022-01-14T14:02:12Z

src/goto-instrument/contracts/instrument_spec_assigns.h

+  // set of tracked conditional targets that come from heap-allocated objects
+  conditional_target_sett from_heap_alloc;
+
+  using car_mapt = std::map<const conditional_target_exprt, const car_exprt>;


Why not:

Suggested change

using car_mapt = std::map<const conditional_target_exprt, const car_exprt>;

using car_mapt = std::unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;

SaswatPadhi · 2022-01-14T14:02:39Z

src/goto-instrument/contracts/instrument_spec_assigns.h

+  void
+  invalidate_aliases(const car_exprt &freed_car, goto_programt &dest) const;
+
+  using conditional_target_sett = std::set<conditional_target_exprt>;


Why not:

Suggested change

using conditional_target_sett = std::set<conditional_target_exprt>;

using conditional_target_sett = std::unorederd_set<conditional_target_exprt, irep_hash>;

SaswatPadhi · 2022-01-14T14:07:38Z

src/goto-instrument/contracts/utils.cpp

+    add_pragma_disable_assigns_check(*it);
+  return prog;
+}
+


Am I missing something or have these two functions (this one + the one above) just been moved to a different location in the same file? If so, can we move those back to reduce the diff?

This change was made so that the order of definitions in the cpp file follows the order of declarations in the header file, after moving havoc_assigns_targett from the now defunct assigns to utils.

tautschnig

Looks ok in general, but a whole bunch of comments on individual bits of code.

tautschnig · 2022-01-25T13:10:09Z

src/ansi-c/c_typecheck_code.cpp

+  // now each target is either a simple side-effect-free unconditional lvalue
+  // expression conditional target group expression with a non-trivial condition


Missing "or?"

tautschnig · 2022-01-25T13:12:34Z

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+#include "utils.h"
+
+#include <analyses/call_graph.h>
+
+#include <langapi/language_util.h>
+
+#include "havoc_assigns_clause_targets.h"
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/expr_util.h>
+#include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>


Nit pick for consistency with other places: use the following order

Include the header file corresponding to the implementation (as done here)

Includes from util

Includes from other directories

Includes from the current directory

tautschnig · 2022-01-25T13:13:43Z

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+  if(can_cast_expr<conditional_target_group_exprt>(expr))
+    track_spec_target_group(to_conditional_target_group_expr(expr), dest);


How about

if(auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr)) track_spec_target_group(*target, dest);

tautschnig · 2022-01-25T13:15:55Z

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+  conditional_target_exprt target{
+    true_exprt{}, symbol_expr, symbol_expr.source_location()};
+
+  return from_stack_alloc.find(target) != from_stack_alloc.end();


Is it really necessary to construct an expression this complicated just for the sake of a lookup? I'd expect the keys to be much more succinct (I'm particularly worried about the source location seemingly being required).

I specialized the lookup tables to have more specific key types depending on context, which caused some code inflation.

tautschnig · 2022-01-25T13:17:24Z

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+  // ensure it is tracked
+  PRECONDITION_WITH_DIAGNOSTICS(
+    stack_allocated_is_tracked(symbol_expr),
+    "symbol is not tracked :" + from_expr(ns, "", symbol_expr));


I'd prefer the use of format (from util/format_expr.h) over from_expr. Ideally, we'd restrict from_expr to output that has to be language-specific.

All I see in format_expr.h is std::ostream & format_rec(std::ostream &os, const expr &src) which is barely used in the whole codebase (28 uses), however I see a lot more uses of from_expr() (139 occurences).

Also format_rec renders directly to ostreams so from_expr seems necessary when rendering expressions to irep_ids to generate comments, or precondition/invariant message strings. What should I use to render to a string in a language agnostic way ?

Ah, my apologies for the lack of clarity. It's: stream << format(expr); or string = format_to_string(expr);

tautschnig · 2022-01-25T14:09:39Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+    side_effect_expr_nondett nondet(target_type, source_location);
    const auto &inst = dest.add(goto_programt::make_assignment(
-      dereference_exprt{target_snapshot_var}, nondet, source_location));
+      dereference_exprt{typecast_exprt::conditional_cast(
+        car.lower_bound_var(), pointer_type(target_type))},
+      nondet,
+      source_location));


I think we might be better off using nondet_initializer here for that would produce nondets for individual fields (based on the type). goto-symex could then take each of these in its field-sensitive encoding.

What is the relation between side_effect_expr_nondett (which also carries type information) and this nondet_initializer class ? It seemed to me that the latter was used to lower the former to basic GOTO before symex.

The latter will use side_effect_expr_nondett by either returning exactly such (for all basic types), or by creating a compound object that in turn contains side_effect_expr_nondett (for example a struct expression with a nondet for each member).

tautschnig · 2022-01-25T14:10:18Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

-}
+  dest.add(
+    goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks));
+}


Github says there's no newline at end-of-file.

tautschnig · 2022-01-25T14:11:09Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

+    namespacet &_ns,
+    symbol_tablet &_st,


As said in another comment: don't take both a namespacet and a symbol_tablet (and essentially never take a non-const namespacet).

tautschnig · 2022-01-25T14:14:37Z

src/goto-instrument/contracts/contracts.cpp

-        havoc_argument,
-        allow_null_lhst::NO,
-        cfg_info_opt);
+      auto havoc_argument = instruction_it->get_other().operands().front();


You probably want to_unary_expr(instruction_it->get_other()).op()

tautschnig · 2022-01-25T14:15:25Z

src/goto-instrument/Makefile

      call_sequences.cpp \
-      contracts/assigns.cpp \
      contracts/contracts.cpp \
      contracts/havoc_assigns_clause_targets.cpp \
+      contracts/instrument_spec_assigns.cpp \


This should be part of the commit that removed the old file so as not to break git bisect applications.

remi-delmas-3000

I addressed all comments except the one regarding from_expr and the use of nondet_initializer.

remi-delmas-3000 · 2022-01-13T20:08:36Z

src/goto-instrument/contracts/contracts.cpp

-    insert_before_swap_and_advance(
-      goto_function.body, loop_head, snapshot_instructions);
-  };
+  // ^^^ FIXME this is not true ^^^


this actually depends on wether

a loop assigns clause is meant to represent the whole set of locations ever touched by the loop until completion, and hence

no target expression should depend on other expressions also touched by the loop (i.e. we do not allow array slice expressions a[0..i]),

it can be snapshotted before havoc+invariants

or

it should summarize an arbitrary execution prefix of the loop, in which case:

a target expressions could depend on each other like (i, a[0..i])

targets should be snapshotted after havocking and assuming the invariant.

the whole clause should be proved to be included in itself post loop-step

and we have not really decided on the semantics yet.

remi-delmas-3000 · 2022-01-13T20:10:18Z

src/goto-instrument/contracts/contracts.cpp

+        auto payload = instrument_spec_assigns.track_spec_target(target);
+        snapshot_instructions.destructive_append(payload);


I refactored the API to use destination passing style, but since sometimes we have to append instructions, or to insert them before a target, or after a target, with or without swapping, we often end up having to declare a temporary goto_programt destination anyway.

remi-delmas-3000 · 2022-01-13T21:10:16Z

src/goto-instrument/contracts/contracts.cpp

  }
 }

+#if 0


this was leftover from refactoring, now removed

remi-delmas-3000 · 2022-01-13T21:10:25Z

src/goto-instrument/contracts/contracts.h

 #include <util/pointer_expr.h>

-#include "assigns.h"
+// #include "assigns.h"


remi-delmas-3000 · 2022-01-13T21:10:40Z

src/goto-instrument/contracts/contracts.h

    skipt skip_parameter_assigns,
    optionalt<cfg_infot> &cfg_info_opt);

+#if 0


remi-delmas-3000 · 2022-01-25T18:56:09Z

src/goto-instrument/contracts/instrument_spec_assigns.h

+    const namespacet &_ns,
+    symbol_tablet &_st,


Good point.

remi-delmas-3000 · 2022-01-25T18:57:30Z

src/goto-instrument/contracts/instrument_spec_assigns.h

+  /// Message handler
+  message_handlert &message_handler;
+
+  /// Logger
+  messaget log;


I did not realise the message_handler was not used elsewhere.

remi-delmas-3000 · 2022-01-25T18:58:58Z

src/goto-instrument/contracts/instrument_spec_assigns.h

+  conditional_target_sett from_heap_alloc;
+
+  using car_mapt = std::
+    unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;


I need to make sure that things stored in this map will never get modified.

remi-delmas-3000 · 2022-01-25T19:08:31Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+    side_effect_expr_nondett nondet(target_type, source_location);
    const auto &inst = dest.add(goto_programt::make_assignment(
-      dereference_exprt{target_snapshot_var}, nondet, source_location));
+      dereference_exprt{typecast_exprt::conditional_cast(
+        car.lower_bound_var(), pointer_type(target_type))},
+      nondet,
+      source_location));


What is the relation between side_effect_expr_nondett (which also carries type information) and this nondet_initializer class ? It seemed to me that the latter was used to lower the former to basic GOTO before symex.

remi-delmas-3000 · 2022-01-25T19:08:39Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

-}
+  dest.add(
+    goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks));
+}


tautschnig · 2022-01-27T14:50:42Z

The change to the Makefile requires approval from one of { @peterschrammel, @martin-cs, @chrisr-diffblue }.

chrisr-diffblue

I've only reviewed the Makefile changes - so consider my approval as mainly for that.

…the front-end (defer to actual instrumentation).

- new class conditional_target_exprt derived from exprt representing conditional targets - new class car_exprt derived from exprt representing normalised conditional targets extended with their conditional address ranges and snapshot variables - new class instrument_assigns_clauset encapsulating assigns clause checking logic - simplified interface with 5 main methods to generate CARs snapshots for different types of targets, generate inclusion checks, invalidate CARs - Add the new intrument_spec_assigns.cpp to the Makefile

from instrument_assigns_clauset. Eliminate code duplication for CAR calculation, target validity assertions properly handle condition cleaning, local statics when havocking assigns clauses.

- Move havoc_assigns_clauset from contract/assigns to utils - Moving functions for tracking assigns clause replacement to utils to break circular dependency - Unified interface for adding "disable:check" pragmas on locations, instructions and programs

- Remove the old assigns clause checking implementation - Remove assigns.cpp from the Makefile.

…ment_assigns_clauset.

remi-delmas-3000 added enhancement In progress aws Bugs or features of importance to AWS CBMC users aws-high labels Jan 13, 2022

remi-delmas-3000 requested review from SaswatPadhi and tautschnig January 13, 2022 04:38

remi-delmas-3000 self-assigned this Jan 13, 2022

remi-delmas-3000 requested review from chrisr-diffblue, feliperodri, martin-cs and peterschrammel as code owners January 13, 2022 04:38

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch 8 times, most recently from b2384c8 to f8b5c50 Compare January 13, 2022 07:42

tautschnig reviewed Jan 13, 2022

View reviewed changes

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch 3 times, most recently from dfe63b9 to 62cca11 Compare January 14, 2022 03:16

SaswatPadhi reviewed Jan 14, 2022

View reviewed changes

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch 3 times, most recently from 355d3e4 to b6dfda0 Compare January 14, 2022 22:17

remi-delmas-3000 requested a review from kroening as a code owner January 14, 2022 22:17

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch from b6dfda0 to ced8795 Compare January 25, 2022 02:26

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch 2 times, most recently from 07ba00a to 22893ba Compare January 25, 2022 02:51

tautschnig approved these changes Jan 25, 2022

View reviewed changes

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch from 22893ba to 1d326d8 Compare January 25, 2022 20:13

remi-delmas-3000 commented Jan 25, 2022

View reviewed changes

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch from 1d326d8 to da0b0dc Compare January 25, 2022 20:22

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue Jan 27, 2022

chrisr-diffblue approved these changes Jan 27, 2022

View reviewed changes

tautschnig unassigned peterschrammel, martin-cs and chrisr-diffblue Jan 27, 2022

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch from da0b0dc to 19fe124 Compare January 29, 2022 00:07

Remi Delmas added 7 commits January 31, 2022 17:46

CONTRACTS: Do not distribute conditions on assigns clause targets in …

db9131a

…the front-end (defer to actual instrumentation).

CONTRACTS: Make havoc_assigns_clause_targets a class that inherits

a61b669

from instrument_assigns_clauset. Eliminate code duplication for CAR calculation, target validity assertions properly handle condition cleaning, local statics when havocking assigns clauses.

CONTRACTS: Move code to utils

f28f7ba

- Move havoc_assigns_clauset from contract/assigns to utils - Moving functions for tracking assigns clause replacement to utils to break circular dependency - Unified interface for adding "disable:check" pragmas on locations, instructions and programs

CONTRACTS: Remove assigns.cpp

cc143a0

- Remove the old assigns clause checking implementation - Remove assigns.cpp from the Makefile.

CONTRACTS: Remove assigns clause checking logic that is now in instru…

b18fb50

…ment_assigns_clauset.

CONTRACS: Update test descriptions following assigns clause refactoring

63d03bc

remi-delmas-3000 force-pushed the assigns-clause-checking-cleanup branch from 19fe124 to 63d03bc Compare January 31, 2022 17:47

remi-delmas-3000 merged commit 3bbd3ab into diffblue:develop Feb 1, 2022

		auto payload = instrument_spec_assigns.track_spec_target(target);
		snapshot_instructions.destructive_append(payload);

                 }
               }
+              #if 0

	using car_mapt = std::map<const conditional_target_exprt, const car_exprt>;
	using car_mapt = std::unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;

	using conditional_target_sett = std::set<conditional_target_exprt>;
	using conditional_target_sett = std::unorederd_set<conditional_target_exprt, irep_hash>;

		// now each target is either a simple side-effect-free unconditional lvalue
		// expression conditional target group expression with a non-trivial condition

		if(can_cast_expr<conditional_target_group_exprt>(expr))
		track_spec_target_group(to_conditional_target_group_expr(expr), dest);

CONTRACTS: New class instrument_spec_assignst encapsulating assigns clause checking logic. #6575

CONTRACTS: New class instrument_spec_assignst encapsulating assigns clause checking logic. #6575

Uh oh!

Conversation

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

Uh oh!

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!

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

Uh oh!

Codecov Report

Uh oh!

SaswatPadhi 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!

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!

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!

CONTRACTS: New class `instrument_spec_assignst` encapsulating assigns clause checking logic. #6575

CONTRACTS: New class `instrument_spec_assignst` encapsulating assigns clause checking logic. #6575

remi-delmas-3000 commented Jan 13, 2022 •

edited

Loading

codecov bot commented Jan 14, 2022 •

edited

Loading