Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure #7313

thomasspriggs · 2022-11-09T19:37:51Z

This PR adds support for __CPROVER_DYNAMIC_OBJECT to incremental SMT decision procedure. Note that it is currently based on top of #7311 . So the first commit titled "Add unit test of object size tracking" should be reviewed as part of that separate PR, rather than this one.

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.

TGWDB · 2022-11-10T09:38:14Z

src/solvers/smt2_incremental/object_tracking.cpp

+  bool dynamic_type = object.type().get_bool(ID_C_dynamic);
+  const auto symbol = expr_try_dynamic_cast<symbol_exprt>(object);
+  bool symbol_is_dynamic =
+    symbol &&
+    has_prefix(id2string(symbol->get_identifier()), SYMEX_DYNAMIC_PREFIX);
+  return dynamic_type || symbol_is_dynamic;


This seems like it is overly inefficient, can't we return on the dynamic_type immediately and then only progress to the casting and string prefix check if necessary?

Yes, we could. I was thinking about readability rather than optimisation when I wrote this.

🤔 has_prefix, id2string and get_identifier are all header defined functions. An optimising compiler may potentially be able to work out that these functions are all side-effect free and add in the early return...

I've added the suggested optimisation for the moment.

codecov · 2022-11-10T13:41:13Z

Codecov Report

Base: 78.28% // Head: 78.30% // Increases project coverage by +0.01% 🎉

Coverage data is based on head (f398ace) compared to base (a295651).
Patch coverage: 94.05% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7313      +/-   ##
===========================================
+ Coverage    78.28%   78.30%   +0.01%     
===========================================
  Files         1642     1644       +2     
  Lines       190004   190141     +137     
===========================================
+ Hits        148744   148889     +145     
+ Misses       41260    41252       -8

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-programs/graphml_witness.cpp	`52.94% <0.00%> (-0.15%)`	⬇️
src/goto-programs/interpreter.cpp	`52.38% <0.00%> (+0.17%)`	⬆️
src/solvers/smt2_incremental/object_tracking.h	`100.00% <ø> (ø)`
..._incremental/smt2_incremental_decision_procedure.h	`75.00% <ø> (ø)`
src/util/expr_initializer.cpp	`85.10% <80.00%> (+1.77%)`	⬆️
jbmc/src/java_bytecode/expr2java.cpp	`86.25% <93.75%> (ø)`
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	`99.60% <94.73%> (-0.10%)`	⬇️
src/ansi-c/c_typecheck_initializer.cpp	`76.57% <100.00%> (+0.04%)`	⬆️
src/ansi-c/expr2c.cpp	`67.33% <100.00%> (-0.02%)`	⬇️
... and 33 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

esteffin

Looks good to me (with few minor suggestions)

esteffin · 2022-11-11T11:54:07Z

src/solvers/smt2_incremental/smt_is_dynamic_object.h

+  /// Makes the command to define the resulting \p size of calling the is
+  /// dynamic object function with \p unique_id.


⛏️ Change is dynamic object to is_dynamic_object as that's the function name

esteffin · 2022-11-11T11:55:11Z

src/solvers/smt2_incremental/smt_is_dynamic_object.h

+#include <solvers/smt2_incremental/ast/smt_commands.h>
+#include <solvers/smt2_incremental/ast/smt_terms.h>
+
+struct smt_is_dynamic_objectt final


💡 Documentation inside looks very good, why not dropping a line to document the class itself?

esteffin · 2022-11-11T12:02:23Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -159,6 +160,7 @@ class smt2_incremental_decision_proceduret final
  /// stateful because it depends on the configuration of the number of object
  /// bits and how many bits wide the size type is configured to be.
  smt_object_sizet object_size_function;
+  smt_is_dynamic_objectt is_dynamic_object_function;


⛏️ Add documentation

esteffin · 2022-11-11T12:07:41Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -255,6 +255,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
    smt_set_option_commandt{smt_option_produce_modelst{true}});
  solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
  solver_process->send(object_size_function.declaration);
+  solver_process->send(is_dynamic_object_function.declaration);


⛏️ Personal opinion: I know smt_is_dynamic_objectt is default-constructed, but readability would benefit if we explicitly construct it 5 lines above as in object_map{initial_smt_object_map()}.

esteffin · 2022-11-11T12:10:55Z

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

+  const auto null_object_dynamic_definition =
+    test.is_dynamic_object_function.make_definition(0, false);


❓ Where do we handle the null_object_dynamic_definition case?

It is currently defaulted to false in the definition of decision_procedure_objectt. I should set it explicitly in the make_null_object function.

esteffin · 2022-11-11T12:38:48Z

regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c

@@ -0,0 +1,17 @@
+#include <assert.h>


⛏️ As we have a test checking that the object is not dynamic, should we avoid the nondeterministic boolean so that one verification leads to FAILURE and one to SUCCESS?
Otherwise we never check for SUCCESS (UNSAT on the SMT level).

So that the information is available in subsequent conversions.

The resolves a potential issue which clang-tidy warns about.

The SMT function which this commit implements declaration / application / definition will be used in follow up commits in order to convert dynamic_object expressions to smt terms.

In preparation for calling the new function in the conversion of is_dynamic_object expressions to SMT terms.

Because this now covers both the size and the definition of whether the object is dynamic or not.

This is the final step required to complete the implementation of the support for this kind of expression.

thomasspriggs requested review from kroening, tautschnig, peterschrammel, chris-ryder, NlightNFotis and TGWDB as code owners November 9, 2022 19:37

TGWDB reviewed Nov 10, 2022

View reviewed changes

thomasspriggs force-pushed the tas/dynamic_object branch 2 times, most recently from 8855491 to 4d64be8 Compare November 10, 2022 12:22

esteffin approved these changes Nov 11, 2022

View reviewed changes

thomasspriggs added 6 commits November 14, 2022 14:02

Add is_dynamic to object map

9e2f74a

So that the information is available in subsequent conversions.

Fix un-initialised fields in decision_procedure_objectt

5e29858

The resolves a potential issue which clang-tidy warns about.

Add smt_is_dynamic_objectt function

1deb0ca

The SMT function which this commit implements declaration / application / definition will be used in follow up commits in order to convert dynamic_object expressions to smt terms.

Send is_dynamic object declaration and defintion to solver

49a5eae

In preparation for calling the new function in the conversion of is_dynamic_object expressions to SMT terms.

Rename define_object_sizes to define_object_properties

e35a5a6

Because this now covers both the size and the definition of whether the object is dynamic or not.

Add conversion of is_dynamic_object_exprt to SMT

4d7381e

This is the final step required to complete the implementation of the support for this kind of expression.

thomasspriggs force-pushed the tas/dynamic_object branch from 4d64be8 to 5b55ebc Compare November 14, 2022 14:24

Add regression test of __CPROVER_DYNAMIC_OBJECT

f398ace

thomasspriggs force-pushed the tas/dynamic_object branch from 5b55ebc to f398ace Compare November 14, 2022 16:54

NlightNFotis approved these changes Nov 14, 2022

View reviewed changes

thomasspriggs merged commit b47a7b2 into diffblue:develop Nov 14, 2022

thomasspriggs deleted the tas/dynamic_object branch November 14, 2022 19:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure #7313

Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure #7313

Uh oh!

thomasspriggs commented Nov 9, 2022

Uh oh!

TGWDB Nov 10, 2022

Uh oh!

thomasspriggs Nov 10, 2022

Uh oh!

thomasspriggs Nov 14, 2022

Uh oh!

codecov bot commented Nov 10, 2022 •

edited

Loading

Uh oh!

esteffin left a comment

Uh oh!

esteffin Nov 11, 2022

Uh oh!

esteffin Nov 11, 2022

Uh oh!

thomasspriggs Nov 14, 2022

Uh oh!

esteffin Nov 11, 2022

Uh oh!

thomasspriggs Nov 14, 2022

Uh oh!

esteffin Nov 11, 2022

Uh oh!

esteffin Nov 11, 2022

Uh oh!

thomasspriggs Nov 11, 2022

Uh oh!

thomasspriggs Nov 14, 2022

Uh oh!

esteffin Nov 11, 2022

Uh oh!

Uh oh!

		/// Makes the command to define the resulting \p size of calling the is
		/// dynamic object function with \p unique_id.

		const auto null_object_dynamic_definition =
		test.is_dynamic_object_function.make_definition(0, false);

Add support for __CPROVER_DYNAMIC_OBJECT to incremental SMT decision procedure #7313

Add support for __CPROVER_DYNAMIC_OBJECT to incremental SMT decision procedure #7313

Uh oh!

Conversation

thomasspriggs commented Nov 9, 2022

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

Uh oh!

Codecov Report

Uh oh!

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

Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure #7313

Add support for `__CPROVER_DYNAMIC_OBJECT` to incremental SMT decision procedure #7313

codecov bot commented Nov 10, 2022 •

edited

Loading