CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions #6886

remi-delmas-3000 · 2022-05-26T12:52:57Z

Adds a new built-in type __CPROVER_assignable_t to represent sets of assignable memory locations and related built-in functions. This new specification format will be used in an upcoming update of assigns clause checking.

The built-in functions are:

// whole object pointed to by ptr is assignable
__CPROVER_assignable_t __CPROVER_whole_object(void *ptr);

// the range of bytes [ptr, ptr + object_size(ptr)-offset(ptr)] is assignable
__CPROVER_assignable_t __CPROVER_object_from(void *ptr);

// the range of bytes [ptr, ptr + size] is assignable
__CPROVER_assignable_t __CPROVER_object_upto(void *, size_t size);

// for all `expr_t` types and expressions, the range of bytes [&expr, &expr + sizeof(expr_t)] is assignable
__CPROVER_assignable_t __CPROVER_typed_target(exprt_t expr);

These built-ins can now be used as targets in assigns clauses.

In addition, users can define their own functions returning __CPROVER_assignable_t to model sets of assignable locations:

__CPROVER_assignable_t my_write_set(char *arr, size_t size)
{
  __CPROVER_assert(
    !arr || __CPROVER_rw_ok(arr, size), "target null or writable");

  if(arr && size > 0)
  { 
    // adds locations in the write set modeled by this function
    __CPROVER_whole_object(arr);
    __CPROVER_object_upto(arr, size);
    __CPROVER_object_from(arr);
    __CPROVER_typed_target(arr[0]);
  }
}

Internally, calls to the above built-ins are normalised during typechecking (for __CPROVER_typed_target) and goto conversion (for the rest) into calls to another built-in :

// the range of bytes [ptr, ptr + size] is assignable
// if is_pointer_to_pointer is true then will be havoced as a pointer during contract replacement
__CPROVER_assignable_t __CPROVER_assignable(void *, size_t size, bool is_pointer_to_pointer);

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.

function calls in assigns clauses.

codecov · 2022-05-26T14:09:44Z

Codecov Report

Merging #6886 (8131e13) into develop (b1f440a) will increase coverage by 0.00%.
The diff coverage is 78.04%.

❗ Current head 8131e13 differs from pull request most recent head 23b2b35. Consider uploading reports for the commit 23b2b35 to get more accurate results

@@            Coverage Diff            @@
##           develop    #6886    +/-   ##
=========================================
  Coverage    77.80%   77.80%            
=========================================
  Files         1567     1567            
  Lines       179920   180026   +106     
=========================================
+ Hits        139992   140076    +84     
- Misses       39928    39950    +22

Impacted Files	Coverage Δ
src/analyses/cfg_dominators.h	`100.00% <ø> (ø)`
src/analyses/flow_insensitive_analysis.cpp	`74.64% <0.00%> (ø)`
src/analyses/interval_analysis.cpp	`0.00% <0.00%> (ø)`
src/analyses/invariant_propagation.cpp	`0.00% <0.00%> (ø)`
src/analyses/invariant_set_domain.cpp	`0.00% <0.00%> (ø)`
src/analyses/static_analysis.cpp	`46.69% <0.00%> (ø)`
src/ansi-c/ansi_c_internal_additions.cpp	`90.12% <ø> (ø)`
src/ansi-c/ansi_c_language.h	`75.00% <ø> (ø)`
src/ansi-c/expr2c.cpp	`67.63% <ø> (ø)`
.../goto-instrument/accelerate/acceleration_utils.cpp	`2.23% <0.00%> (ø)`
... and 225 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 c6f83a2...23b2b35. Read the comment docs.

tautschnig · 2022-05-26T18:55:27Z

doc/cprover-manual/contracts-assigns.md

+__CPROVER_assignable_t __CPROVER_typed_target(expr_t expr);
+```
+
+Given a pointer `ptr` pointing into some object `o`, 
+`__CPROVER_whole_object(ptr)` specifies that all bytes of the object `o`
+are assignable:
+```c
+__CPROVER_assignable_t __CPROVER_whole_object(void *ptr);


Isn't __CPROVER_typed_target(x) expressible as __CPROVER_whole_object(&x)?

tautschnig · 2022-05-26T19:02:57Z

src/ansi-c/c_typecheck_code.cpp

+                   "assignable_t return type for function " +
+                     id2string(ident) + " called in assigns clause"


Nit picking: use << instead of + and then use ident instead of id2string(ident).

tautschnig · 2022-05-26T19:05:58Z

src/ansi-c/c_typecheck_expr.cpp

+        auto arg0 = expr.arguments().at(0);
+        typecheck_expr(arg0);


Check that there is exactly one argument and else report back via error() and throw. It should not be possible for a user to trigger a system exception (.at(0)).

tautschnig · 2022-05-26T19:09:57Z

src/goto-programs/builtin_functions.cpp

+void goto_convertt::do_whole_object(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  source_location.add_pragma("enable:pointer-check");
+  source_location.add_pragma("enable:pointer-overflow-check");
+  source_location.add_pragma("enable:signed-overflow-check");
+  source_location.add_pragma("enable:unsigned-overflow-check");
+  const auto &arg0 = arguments[0];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // pointer
+  new_arguments.emplace_back(typecast_exprt::conditional_cast(
+    minus_exprt{
+      typecast_exprt::conditional_cast(arg0, pointer_type(char_type())),
+      pointer_offset_exprt{arg0, size_type()}},
+    pointer_type(empty_typet())));
+  // size
+  new_arguments.emplace_back(object_size_exprt{arg0, size_type()});
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}


Why can't we do this in the C front-end (during type checking) already?

tautschnig · 2022-05-26T19:10:21Z

src/goto-programs/builtin_functions.cpp

+void goto_convertt::do_object_from(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  source_location.add_pragma("enable:pointer-check");
+  source_location.add_pragma("enable:pointer-overflow-check");
+  source_location.add_pragma("enable:signed-overflow-check");
+  source_location.add_pragma("enable:unsigned-overflow-check");
+  const auto &arg0 = arguments[0];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // ptr
+  new_arguments.emplace_back(arg0);
+  // size
+  new_arguments.emplace_back(minus_exprt{
+    object_size_exprt{arg0, size_type()},
+    pointer_offset_exprt{arg0, size_type()}});
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}


As above: can't we do this in the C front-end?

tautschnig · 2022-05-26T19:10:39Z

src/goto-programs/builtin_functions.cpp

+void goto_convertt::do_object_upto(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  const auto &arg0 = arguments[0];
+  const auto &arg1 = arguments[1];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // pointer
+  new_arguments.emplace_back(arg0);
+  // size
+  new_arguments.emplace_back(arg1);
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}


As above: can't we do this in the C front-end already?

tautschnig · 2022-05-26T19:11:13Z

src/ansi-c/ansi_c_internal_additions.cpp

+    // frame specifications for contracts
+    // Type that describes assignable memory locations
+    "typedef void " CPROVER_PREFIX "assignable_t;\n"


Why do we need this typedef?

feliperodri · 2022-08-16T17:28:53Z

#6887 supersedes this PR.

remi-delmas-3000 requested review from tautschnig, feliperodri, SaswatPadhi, kroening, peterschrammel and chris-ryder as code owners May 26, 2022 12:52

remi-delmas-3000 self-assigned this May 26, 2022

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels May 26, 2022

CONTRACTS: introduce __CPROVER_assignable_t built-ins and allow

23b2b35

function calls in assigns clauses.

remi-delmas-3000 force-pushed the cprover-assignable-builtin branch from 8131e13 to 23b2b35 Compare May 26, 2022 12:59

remi-delmas-3000 mentioned this pull request May 26, 2022

CONTRACTS: Dynamic frame condition checking #6887

Closed

tautschnig reviewed May 26, 2022

View reviewed changes

feliperodri closed this Aug 16, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions #6886

CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions #6886

remi-delmas-3000 commented May 26, 2022 •

edited

Loading

codecov bot commented May 26, 2022 •

edited

Loading

tautschnig May 26, 2022

tautschnig May 26, 2022

tautschnig May 26, 2022

tautschnig May 26, 2022

tautschnig May 26, 2022

tautschnig May 26, 2022

tautschnig May 26, 2022

feliperodri commented Aug 16, 2022

		"assignable_t return type for function " +
		id2string(ident) + " called in assigns clause"

CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions #6886

CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions #6886

Conversation

remi-delmas-3000 commented May 26, 2022 • edited Loading

codecov bot commented May 26, 2022 • edited Loading

Codecov Report

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

tautschnig May 26, 2022

Choose a reason for hiding this comment

feliperodri commented Aug 16, 2022

remi-delmas-3000 commented May 26, 2022 •

edited

Loading

codecov bot commented May 26, 2022 •

edited

Loading