Add new builtin __CPROVER_havoc_slice #6430

remi-delmas-3000 · 2021-11-02T18:07:04Z

Resolves #6351.

This PR adds a new builtin function :

void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);

Which lets you update size consecutive bytes to nondet values in the object underlying a given pointer p. It requires that __CPROVER_w_ok(p, size) holds.
It is rewritten at goto level to an array_replace(p, q) operation where q is declared a nondet array of size size.

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.

danielsn · 2021-11-04T22:44:12Z

doc/cprover-manual/api.md

+
+This function requires a valid pointer and updates all the bytes of the underlying object with nondeterministic values.
+```C
+void __CPROVER_havoc_object(void *p);


When you say "object", what do you mean?
For example, should this assertion pass or fail?

struct foo { int x; int y; }; struct foo thefoo = {.x = 1; .y = 12}; int* p = &thefoo.y; __CPROVER_havoc_object(p); assert(thefoo.x == 1);

the object in that case is the blob of memory that holds the whole struct thefoo so this assertion should fail.
on the other it passes when using __CPROVER_havoc_object_slice(p, sizeof(*p))

This seems like it could lead to a foot gun:

int foo_stub(int* p) { __CPROVER_havoc_object(p); return *p; } struct foo { int x; int y; }; int main() [ struct foo thefoo = {.x = 1; .y = 12}; int v = foo_stub(&thefoo.y); assert(thefoo.x == 1); assert(thefoo.y == v); }

I think the user would expect that foo_stub wouldn't modify memory which it doesn't have a valid pointer to. Maybe we need a different name:

__CPROVER_havoc_entire_allocation()

Agreed, we could name __CPROVER_havoc_object differently but it was introduced some time ago so this could be a breaking change for existing users of the primitive.

Can we just add a more explicit warning to the document about havoc_object that it will havoc enclosing structs.

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

src/goto-programs/builtin_functions.cpp

+    throw 0;
+  }
+
+  if(arguments[1].type().id() != ID_unsignedbv)


To improve readability, could we rewrite this as:

Suggested change

if(arguments[1].type().id() != ID_unsignedbv)

if(arguments[1].type().id() != size_type().id())

The idea with this check was to allow users that use the primitive directly from GOTO to use any unsignedbv type and not just size_t to specify sizes. This makes it more general than its C interface.

Hmm, thinking more, I think it could actually be:

Suggested change

if(arguments[1].type().id() != ID_unsignedbv)

if(arguments[1].type() != size_type())

We define the signature of __CPROVER_havoc_slice as:

void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);

for the frontend.

So, shouldn't the check here match the this signature?

Yes it should be an unsignedbv type, but I think it shouldn't be any unsignedbv type. It should match the size_t semantics on the machine, which is computed by size_type():

cbmc/src/util/c_types.cpp

Lines 58 to 72 in 4889328

unsignedbv_typet size_type()

{

// The size type varies. This is unsigned int on some systems,

// and unsigned long int on others,

// and unsigned long long on say Windows 64.

if(config.ansi_c.pointer_width==config.ansi_c.int_width)

return unsigned_int_type();

else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)

return unsigned_long_int_type();

else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)

return unsigned_long_long_int_type();

else

INVARIANT(false, "width of size type"); // aaah!

}

Or am I missing something here?

regression/cbmc/havoc_object_slice/test.desc

src/goto-programs/builtin_functions.cpp

regression/cbmc/havoc_object_slice/main.c

codecov · 2021-11-10T20:42:43Z

Codecov Report

Merging #6430 (8ee6305) into develop (bfa4c2c) will increase coverage by 0.01%.
The diff coverage is 70.83%.

@@             Coverage Diff             @@
##           develop    #6430      +/-   ##
===========================================
+ Coverage    76.01%   76.02%   +0.01%     
===========================================
  Files         1527     1527              
  Lines       164465   164510      +45     
===========================================
+ Hits        125013   125068      +55     
+ Misses       39452    39442      -10

Impacted Files	Coverage Δ
src/goto-programs/goto_convert_class.h	`87.30% <ø> (ø)`
src/goto-programs/goto_instruction_code.cpp	`100.00% <ø> (ø)`
src/goto-programs/goto_instruction_code.h	`100.00% <ø> (ø)`
src/goto-programs/builtin_functions.cpp	`56.17% <70.21%> (+0.85%)`	⬆️
src/goto-programs/goto_convert_function_call.cpp	`47.27% <100.00%> (ø)`
src/solvers/lowering/byte_operators.cpp	`92.18% <0.00%> (+0.09%)`	⬆️
src/analyses/goto_check.cpp	`88.98% <0.00%> (+0.20%)`	⬆️
src/solvers/flattening/boolbv_shift.cpp	`84.37% <0.00%> (+9.37%)`	⬆️
src/solvers/flattening/boolbv_member.cpp	`97.56% <0.00%> (+43.90%)`	⬆️

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 e27dba6...8ee6305. Read the comment docs.

feliperodri

Only minor changes. Almost ready to go 😄

regression/cbmc/havoc_object_slice/declarations.h

regression/cbmc/havoc_object_slice/test_array_slice_1.c

regression/cbmc/havoc_object_slice/test_array_slice_1.desc

regression/cbmc/havoc_object_slice/test_array_slice_2.desc

regression/cbmc/havoc_object_slice/test_struct_b.desc

src/goto-programs/builtin_functions.cpp

src/goto-programs/goto_convert_class.h

tautschnig

Approving, but please address the comments before merging.

src/goto-programs/builtin_functions.cpp

tautschnig · 2021-11-11T17:28:30Z

src/goto-programs/builtin_functions.cpp

+  t->source_location_nonconst().set("user-provided", false);
+  t->source_location_nonconst().set_property_class(ID_assertion);
+  t->source_location_nonconst().set_comment(
+    "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));


Rather than fixing up the location after the fact, make these changes to a source location beforehand, like:

source_locationt annotated_location = source_location; annotated_location.set("user-provided", ...); ...

and then use annotated_location when constructing the goto-program instruction.

Did you perhaps end up going back and forth on this? It doesn't seem to have been addressed.

src/goto-programs/builtin_functions.cpp

tautschnig · 2021-11-11T20:01:52Z

src/goto-programs/goto_instruction_code.h

+  symbol_exprt havoc_slice_function =
+    symbol_exprt{CPROVER_PREFIX "havoc_slice", empty_typet()};


This needs to be of a code_typet type, and then makes me wonder whether you should rather fetch this symbol from the symbol table. And that, in turn, makes me wonder whether such a function should make sure it is present in the symbol table.

The symbol's signature is only declared in src/ansi-c/cprover_builtin_headers.h.
If someone were to build a goto model programatically without using the C front-end, is there a guarantee that this signature will be present in the symbol table ?

No, there is no such guarantee. Hence, it would be necessary to check, and add the symbol if it isn't present just yet.

src/ansi-c/scanner.l

feliperodri

LGTM module a few more tests updates and Michael's comments.

doc/cprover-manual/api.md

regression/cbmc/havoc_slice/declarations.h

regression/cbmc/havoc_slice_checks/main.c

feliperodri · 2021-11-16T01:04:14Z

regression/cbmc/havoc_slice/test_whole_array_with_offset.desc

+CORE
+test_whole_array_with_offset.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^.*expecting FAILURE: SUCCESS$
+^.*expecting SUCCESS: FAILURE$
+^.*dereference .*: FAILURE$


I see that you have a different name for each test case (i.e., a .c file and a test description). The usual pattern across the regression tests is to create a folder with a descriptive name (like the ones you're using for each test case) and add a main.c file and a test.desc file inside that folder. At the end of each test description, we add a small explanation of what behavior the test is covering. Not a blocker, but I suggest you to update this test to follow the same pattern.

feliperodri · 2021-11-16T01:05:08Z

src/goto-programs/builtin_functions.cpp

+    throw 0;
+  }


We probably don't have any cases where we try to pass more than 2 parameters, thus, we don't hit this case.

Since tests are expressed in C and uses of havoc_slice are checked by the front end these would be impossible to reach using a test expressed in C.
Covering them would require build and load a goto model directly or create them in C++ directly.

feliperodri · 2021-11-16T01:05:35Z

src/goto-programs/builtin_functions.cpp

+    throw 0;
+  }


Same as above for non-pointer parameters.

feliperodri · 2021-11-16T01:06:15Z

src/goto-programs/builtin_functions.cpp

+    throw 0;
+  }


Same as above. We can create one test to cover these error cases.

feliperodri · 2021-11-16T01:06:52Z

src/goto-programs/builtin_functions.cpp

+  // check nil lhs
+  if(lhs.is_not_nil())
+  {
+    error().source_location = source_location;
+    error() << "'" << identifier << "' not expected to have a LHS" << eom;
+    throw 0;
+  }


Same as above.

src/goto-programs/goto_instruction_code.h

tautschnig · 2021-11-17T12:08:07Z

doc/cprover-manual/api.md

 optional size; when the size argument is not given, the size of the subtype
 (which must not be **void**) of the pointer type is used.

+#### \_\_CPROVER\_havoc\_object


Random place for comment: it would be great if the commit message also answered the "Why?" question. See https://chris.beams.io/posts/git-commit/ as linked from the pull-request template. On this occasion, it would be good to answer the "why did __CPROVER_havoc_object not suffice" question.

tautschnig · 2021-11-17T12:10:53Z

src/goto-programs/builtin_functions.cpp

+  t->source_location_nonconst().set("user-provided", false);
+  t->source_location_nonconst().set_property_class(ID_assertion);
+  t->source_location_nonconst().set_comment(
+    "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));


Did you perhaps end up going back and forth on this? It doesn't seem to have been addressed.

tautschnig · 2021-11-17T12:13:02Z

src/goto-programs/goto_instruction_code.cpp

    vm, code.operands().size() >= 2, "output must have at least two operands");
 }
+
+inline code_function_callt


Remove inline

tautschnig · 2021-11-17T12:13:11Z

src/goto-programs/goto_instruction_code.h

+///
+/// \return A \ref code_function_callt expression
+///         `nil_exprt() := __CPROVER_havoc_slice(p, size)`.
+inline code_function_callt


Remove inline

tautschnig · 2021-11-17T12:13:34Z

src/goto-programs/goto_instruction_code.h

 #ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
 #define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H

+#include <util/cprover_prefix.h>


You don't actually need this in the header file anymore.

remi-delmas-3000 requested review from chrisr-diffblue, kroening, martin-cs and peterschrammel as code owners November 2, 2021 18:07

remi-delmas-3000 assigned tautschnig Nov 2, 2021

remi-delmas-3000 requested a review from tautschnig as a code owner November 2, 2021 18:07

remi-delmas-3000 assigned SaswatPadhi, kroening and jimgrundy Nov 2, 2021

SaswatPadhi added aws Bugs or features of importance to AWS CBMC users aws-high enhancement labels Nov 2, 2021

remi-delmas-3000 force-pushed the havoc-object-slice branch from c1b6b23 to 2698970 Compare November 2, 2021 19:53

NlightNFotis mentioned this pull request Nov 3, 2021

Create new __CPROVER_havoc_slice & __CPROVER_havoc_from primitives #6351

Closed

remi-delmas-3000 force-pushed the havoc-object-slice branch from 2698970 to 4589c6d Compare November 4, 2021 13:42

danielsn reviewed Nov 4, 2021

View reviewed changes

jimgrundy approved these changes Nov 4, 2021

View reviewed changes

SaswatPadhi reviewed Nov 5, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-object-slice branch 3 times, most recently from 341baa6 to 5671a81 Compare November 10, 2021 19:44

SaswatPadhi requested a review from feliperodri November 10, 2021 21:01

feliperodri requested changes Nov 10, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-object-slice branch from 5671a81 to a16bdb2 Compare November 11, 2021 17:19

remi-delmas-3000 changed the title ~~Add new builtin __CPROVER_havoc_object_slice~~ Add new builtin __CPROVER_havoc_slice Nov 11, 2021

tautschnig approved these changes Nov 11, 2021

View reviewed changes

tautschnig reviewed Nov 11, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-object-slice branch from 99e757d to ab9c505 Compare November 11, 2021 20:05

feliperodri approved these changes Nov 16, 2021

View reviewed changes

feliperodri requested a review from SaswatPadhi November 16, 2021 01:10

remi-delmas-3000 force-pushed the havoc-object-slice branch 2 times, most recently from 413c583 to b9b984f Compare November 16, 2021 17:31

havoc_slice documentation, implementation and regression tests

8ee6305

remi-delmas-3000 force-pushed the havoc-object-slice branch from b9b984f to 8ee6305 Compare November 16, 2021 18:46

tautschnig approved these changes Nov 17, 2021

View reviewed changes

TGWDB merged commit f562bcf into diffblue:develop Nov 18, 2021

	if(arguments[1].type().id() != ID_unsignedbv)
	if(arguments[1].type().id() != size_type().id())

	if(arguments[1].type().id() != ID_unsignedbv)
	if(arguments[1].type() != size_type())

	unsignedbv_typet size_type()
	{
	// The size type varies. This is unsigned int on some systems,
	// and unsigned long int on others,
	// and unsigned long long on say Windows 64.

	if(config.ansi_c.pointer_width==config.ansi_c.int_width)
	return unsigned_int_type();
	else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
	return unsigned_long_int_type();
	else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
	return unsigned_long_long_int_type();
	else
	INVARIANT(false, "width of size type"); // aaah!
	}

		symbol_exprt havoc_slice_function =
		symbol_exprt{CPROVER_PREFIX "havoc_slice", empty_typet()};

Add new builtin __CPROVER_havoc_slice #6430

Add new builtin __CPROVER_havoc_slice #6430

Uh oh!

Conversation

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

Uh oh!

Uh oh!

danielsn Nov 4, 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!

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Nov 10, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

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!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

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

remi-delmas-3000 commented Nov 2, 2021 •

edited

Loading

danielsn Nov 4, 2021 •

edited

Loading

codecov bot commented Nov 10, 2021 •

edited

Loading