Add --expand-pointer-predicates to goto-instrument #4332

karkhaz · 2019-03-05T21:26:52Z

This patchset adds __CPROVER_points_to_valid_memory. It tells CBMC that an object of a particular size is pointed to by a pointer, and can be used in assertions and assumptions.

It also adds the --expand-pointer-predicates flag to goto-instrument, which expands the __CPROVER_points_to_valid_memory directive. This is in preparation for future commits that will introduce more pointer predicates having side effects, which will need to be expanded into multiple instructions.

src/ansi-c/c_typecheck_expr.cpp

The --expand-pointer-predicates pass resolves pointer predicates (util/pointer_predicates.{cpp, h}) which have side effects and so require expanding into multiple instructions. Currently, the only such predicate that needs to be expanded is __CPROVER_points_to_valid_memory (name subject to change). The __CPROVER_points_to_valid_memory predicates takes two parameters, a pointer and a size. Semantically, __CPROVER_points_to_valid_memory(p, size) should be true if and only if p points to a memory object which is valid to read/write for at least size bytes past p. When used in assertions, this will be checked in a similar manner to how --pointer-check checks validity of a dereference. When used in assumptions, this predicate creates (if none exists already) an object for p to refer to, using local_bitvector_analysis to make that determination, and then makes assumptions (again corresponding to the assertions made by --pointer-check) about that object.

This commit adds support for a one-argument form of __CPROVER_points_to_valid_memory, taking only a pointer, with no size. If ptr has type T*, then __CPROVER_points_to_valid_memory(ptr) is equivalent to __CPROVER_points_to_valid_memory(ptr, sizeof(T)).

tautschnig · 2019-03-07T08:25:26Z

@karkhaz This is still failing CI.

This commit ensures that the second argument to the __CPROVER_points_to_valid_memory directive can be coerced to a size_t, and adds a test to check for the failing case.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2ddb39b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104266680

karkhaz · 2019-03-13T17:17:15Z

@tautschnig do you know why the AWS CodeBuild build is failing? I tried re-pushing, it doesn't help.

Also, if I want to diagnose this problem in the future, what should I do? I can't currently see the results of that build.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f53b62b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104280806

tautschnig · 2019-03-14T14:19:13Z

regression/contracts/argument_sanity/test.desc

+CORE
+main.c
+--apply-code-contracts
+^EXIT=1$


This is the cause of the Windows failure: goto-cl exits with exit code 64 on errors (cf. other intentionally-failing tests, git grep -w 64 regression/ansi-c).

tautschnig · 2019-03-14T14:20:48Z

src/ansi-c/c_typecheck_expr.cpp

@@ -34,6 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "anonymous_member.h"
 #include "padding.h"

+bool is_lvalue(const exprt &expr);


This shouldn't be necessary, use #include <util/expr_util.h>

tautschnig · 2019-03-14T14:21:34Z

src/ansi-c/c_typecheck_expr.cpp

+    }
+
+    exprt same_object_expr;
+    if(expr.arguments().size() == 2)


This is established above, no need to check again.

tautschnig · 2019-03-14T14:22:32Z

src/ansi-c/c_typecheck_expr.cpp

+    {
+      UNREACHABLE;
+    }
+    same_object_expr.add_source_location() = source_location;


Maybe points_to_valid_memory should actually take a source_locationt as an additional argument?

tautschnig · 2019-03-14T14:23:31Z

src/goto-instrument/expand_pointer_predicates.cpp

+  new_tmp_symbol(const typet &type, const source_locationt &source_location);
+};
+
+bool is_lvalue(const exprt &expr);


This shouldn't be necessary, use #include <util/expr_util.h>

tautschnig · 2019-03-14T14:26:28Z

src/goto-instrument/expand_pointer_predicates.cpp

+        d->source_location = assume_expr.source_location();
+        const symbol_exprt obj =
+          new_tmp_symbol(object_type, d->source_location).symbol_expr();
+        d->code = code_declt(obj);


Please use the recently added API doing assume_code.add(goto_programt::make_decl(...)); to combine most of the above into a single instruction.

tautschnig · 2019-03-14T14:27:18Z

src/goto-instrument/expand_pointer_predicates.cpp

+        goto_programt::targett a = assume_code.add_instruction(ASSIGN);
+        a->source_location = assume_expr.source_location();
+        a->code = code_assignt(pointer_expr, rhs);
+        a->code.add_source_location() = assume_expr.source_location();


Use assume_code.add(goto_programt::make_assign(...));

tautschnig · 2019-03-14T14:28:34Z

src/goto-instrument/expand_pointer_predicates.cpp

+{
+  return get_fresh_aux_symbol(
+    type,
+    id2string(source_location.get_function()),


If possible, please use the actual function identifier as found in the function map instead of this user-level name. This will require passing in such an additional irep_idt to new_tmp_symbol.

tautschnig · 2019-03-14T14:30:49Z

src/util/expr_util.cpp

-#include "namespace.h"
-#include "arith_tools.h"
+#include <algorithm>
+#include <unordered_set>


Leave the STL includes where they were, separated by a blank line.

tautschnig · 2019-03-14T14:33:15Z

src/ansi-c/c_typecheck_expr.cpp

      {
-        err_location(f_op);
+        error().source_location = f_op.source_location();


I'd prefer for those changes to be squashed into the earlier commit as otherwise that code wouldn't compile (which makes bisecting hard).

TGWDB · 2021-05-11T09:40:28Z

Closing as this has been untouched for a couple of years. Please feel free to re-open/update if you believe this closure is erroneous.

karkhaz added Instrumentations new feature labels Mar 5, 2019

karkhaz requested review from tautschnig, kroening and romainbrenguier March 5, 2019 21:26

karkhaz requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, martin-cs, peterschrammel, pkesseli and smowton as code owners March 5, 2019 21:26

karkhaz commented Mar 5, 2019

View reviewed changes

src/ansi-c/c_typecheck_expr.cpp Outdated Show resolved Hide resolved

tautschnig assigned karkhaz Mar 6, 2019

karkhaz force-pushed the kk-expand-pointer-predicates branch 2 times, most recently from 9deb9dd to 8cf8e62 Compare March 6, 2019 14:59

karkhaz assigned tautschnig and romainbrenguier and unassigned karkhaz Mar 6, 2019

karkhaz force-pushed the kk-expand-pointer-predicates branch 2 times, most recently from e5222d7 to c844655 Compare March 6, 2019 15:46

karkhaz and others added 3 commits March 6, 2019 10:51

Whitespace fix

563ba56

karkhaz force-pushed the kk-expand-pointer-predicates branch from c844655 to bc07b78 Compare March 6, 2019 15:51

tautschnig assigned karkhaz and unassigned romainbrenguier Mar 7, 2019

Adds tests for --expand-pointer-predicates

026a611

karkhaz force-pushed the kk-expand-pointer-predicates branch from bc07b78 to 2ddb39b Compare March 13, 2019 14:25

Check 2nd arg to points_to_valid_memory is size_t

f53b62b

This commit ensures that the second argument to the __CPROVER_points_to_valid_memory directive can be coerced to a size_t, and adds a test to check for the failing case.

karkhaz force-pushed the kk-expand-pointer-predicates branch from 2ddb39b to f53b62b Compare March 13, 2019 16:20

allredj reviewed Mar 13, 2019

View reviewed changes

tautschnig approved these changes Mar 14, 2019

View reviewed changes

tautschnig assigned peterschrammel and chrisr-diffblue and unassigned tautschnig Mar 14, 2019

tautschnig added the blocker label Mar 21, 2019

tautschnig mentioned this pull request Apr 3, 2019

disambiguate two exprts with same ID #4479

Merged

7 tasks

TGWDB closed this May 11, 2021

Add --expand-pointer-predicates to goto-instrument #4332

Add --expand-pointer-predicates to goto-instrument #4332

Uh oh!

Conversation

karkhaz commented Mar 5, 2019

Uh oh!

Uh oh!

tautschnig commented Mar 7, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

karkhaz commented Mar 13, 2019

Uh oh!

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

TGWDB commented May 11, 2021

Uh oh!

Uh oh!