CHC encoder #6717

kroening · 2022-03-09T13:21:17Z

This adds a major new feature, a state-based CHC encoder and solver. It is delivered as a separate binary.

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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-03-09T17:48:02Z

Codecov Report

Base: 77.87% // Head: 77.79% // Decreases project coverage by -0.08% ⚠️

Coverage data is based on head (14da6d6) compared to base (524aa79).
Patch has no changes to coverable lines.

❗ Current head 14da6d6 differs from pull request most recent head e54a0ee. Consider uploading reports for the commit e54a0ee to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #6717      +/-   ##
===========================================
- Coverage    77.87%   77.79%   -0.09%     
===========================================
  Files         1576     1578       +2     
  Lines       181829   182079     +250     
===========================================
+ Hits        141605   141653      +48     
- Misses       40224    40426     +202

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	`65.15% <0.00%> (-3.54%)`	⬇️
src/util/pointer_expr.cpp	`78.44% <0.00%> (-3.11%)`	⬇️
src/util/std_types.cpp	`87.36% <0.00%> (-1.75%)`	⬇️
src/ansi-c/c_typecast.cpp	`80.65% <0.00%> (-0.55%)`	⬇️
src/ansi-c/parser.y	`80.47% <0.00%> (-0.46%)`	⬇️
src/crangler/c_wrangler.cpp	`75.10% <0.00%> (-0.41%)`	⬇️
src/util/graph.h	`96.83% <0.00%> (-0.32%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`73.92% <0.00%> (-0.28%)`	⬇️
src/ansi-c/c_expr.cpp	`96.66% <0.00%> (-0.11%)`	⬇️
src/goto-instrument/goto_program2code.cpp	`68.75% <0.00%> (-0.10%)`	⬇️
... and 16 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.

tautschnig

We need some form of documentation as to what this new tool can/cannot do. A man-page would also be nice (and might be a place to host that documentation).

src/util/format_expr.h

src/ansi-c/cprover_builtin_headers.h

tautschnig · 2022-09-19T11:08:08Z

regression/cbmc/pointer-predicates/in_range1.c

@@ -0,0 +1,13 @@
+int x;


Random place for comment: isn't this commit also a PR of its own?

tautschnig · 2022-09-19T11:13:05Z

src/util/simplify_expr_pointer.cpp

-    exprt pointer_offset_expr = simplify_pointer_offset(
-      to_pointer_offset_expr(pointer_offset(ptr_expr.front())));
+    exprt pointer_offset_expr = simplify_pointer_offset(to_pointer_offset_expr(
+      pointer_offset_exprt(ptr_expr.front(), expr.type())));


I don't understand this change: why do we do to_pointer_offset_expr when the argument (now) is a pointer_offset_exprt? And when we're now constructing the expression with expr.type(), does the comment still apply? If the comment no longer applies, why was it previously ok to change the type, and why is it now the right thing not to change the type?

Removed the comment, this is indeed no longer the case.

Removed the cast.

tautschnig · 2022-09-19T11:15:16Z

src/cprover/help_formatter.h

+/*******************************************************************\
+
+Module: Help Formatter
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Help Formatter
+
+#ifndef CPROVER_CPROVER_HELP_FORMATTER_H
+#define CPROVER_CPROVER_HELP_FORMATTER_H


How does this differ from help_entry, and why is it part of the cprover tool (only)? I can see that the implementation does handle help strings with some markup, but can't we please instead have this for everyone rather than having it buried in some commit? I had put together #6931, which perhaps could be done in a more human-readable fashion using this facility.

tautschnig · 2022-09-19T11:16:56Z

src/cprover/find_variables.cpp

+
+#include <util/pointer_expr.h>
+
+#include "state.h"


Does this code actually use anything from that include, and should the entire code not be part of find_symbols.{h,cpp} instead?

I am adding a comment -- note that this is materially different to any variant of find_symbols.

I understand, yet this is a concern of mine for several pieces of code being added here: they are different from existing functionality, but the absence of documentation makes it impossible for a potential user to tell what exactly the difference is without putting the code side-by-side.

src/cprover/Makefile

peterschrammel

Is there some documentation that describes the encoding and its implementation on a conceptual level?

kroening · 2022-09-21T09:11:52Z

Will email to you

This commit adds a function to extend the expression formatter at runtime.

The Makefile is extended to compile plain C code.

substitute_symbols is useful beyond the specific use case in std_expr.cpp (instantiating binding_exprt). This commit makes it available outside.

Instead of building a completely new binding_exprt, make a copy of the previous one, and then change the operand. The key benefit is that comments (source locations and the like) are preserved.

object_address expressions have pointer type, and hence, the conversion must happen in bv_pointerst::convert_pointer_type.

The SMT2 backend constructs strings to disambiguate overloaded operations using types, and now supports generating strings for array types.

The SMT2 backend constructs strings to disambiguate overloaded operations using types, and now supports generating strings for union_tag types.

This introduces C syntax for a multi-ary predicate that implies that the given pointers point to pairwise different objects.

This adds the predicate __CPROVER_pointer_in_range to the C frontend. The expression __CPROVER_pointer_in_range(a, b, c) evaluates to true iff the following conditions are met: 1) The three pointers a, b, c point to the same object. 2) The object is readable from a to (but not including) c, i.e., c may point just beyond the end of the sequence. 3) a <= b 4) b <= c This predicate is an invariant for the standard loop pattern in which a pointer is used to iterate over an object, stopping when the pointer points one beyond the end of the sequence. The benefit over using a<=b && b<=c is that ANSI-C's <= operator is undefined when the two pointers related by <= do not point into the same object.

This adds a CHC encoding that uses the concept of an abstract "program state", in contrast to the usual explicit enumeration of the variables that the state comprises.

tautschnig

Approving so as not to block experimenting, but documenting my remaining concerns:

There is a bunch of code that is similar-but-not-quite-the-same and not documented.
There is no documentation at all, as also noted by @peterschrammel .

So, really, this code is only usable by a very small group of people. It would be great to learn about a path towards fixing this.

peterschrammel

I have only looked at the changes to existing code, which look ok.
Reviewing the new code will take longer than reasonable. It's preferable to get it merged right away and review the new code gradually when documentation is added.

kroening added the new feature label Mar 9, 2022

kroening force-pushed the set_encoding branch from 0e54364 to c4416c0 Compare March 9, 2022 16:17

kroening force-pushed the set_encoding branch 3 times, most recently from be4d4e0 to f207870 Compare March 21, 2022 10:11

kroening force-pushed the set_encoding branch from c634148 to e0801da Compare April 5, 2022 09:03

kroening force-pushed the set_encoding branch from 1e88e70 to fb5e2dd Compare April 25, 2022 15:17

kroening force-pushed the set_encoding branch from b80403d to d85b674 Compare May 8, 2022 22:13

kroening force-pushed the set_encoding branch 2 times, most recently from 2b7ff7d to 00bf87c Compare May 25, 2022 16:59

kroening force-pushed the set_encoding branch from 4802245 to 8c0e263 Compare July 1, 2022 07:01

kroening force-pushed the set_encoding branch 3 times, most recently from 08f5250 to 0b0d8dd Compare September 9, 2022 16:26

kroening force-pushed the set_encoding branch 15 times, most recently from f9c9bfb to e8dedf1 Compare September 17, 2022 09:33

kroening force-pushed the set_encoding branch from bc9e9ff to 1392c76 Compare September 18, 2022 17:23

tautschnig reviewed Sep 19, 2022

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Sep 19, 2022

kroening force-pushed the set_encoding branch 2 times, most recently from 46195d3 to 9f97a49 Compare September 19, 2022 18:13

kroening requested a review from a team as a code owner September 19, 2022 18:18

kroening force-pushed the set_encoding branch from 14da6d6 to 523dcb7 Compare September 20, 2022 06:30

kroening assigned tautschnig and unassigned kroening Sep 20, 2022

peterschrammel reviewed Sep 21, 2022

View reviewed changes

kroening added 10 commits September 23, 2022 13:31

introduce add_format_hook(...)

1a9a55a

This commit adds a function to extend the expression formatter at runtime.

changes to 'common' Makefile include to compile plain C

06ecbf2

The Makefile is extended to compile plain C code.

make substitute_symbols available outside of std_expr.cpp

d0f3312

substitute_symbols is useful beyond the specific use case in std_expr.cpp (instantiating binding_exprt). This commit makes it available outside.

substitute_symbols now preserves comments in binding expressions

608b2c2

Instead of building a completely new binding_exprt, make a copy of the previous one, and then change the operand. The key benefit is that comments (source locations and the like) are preserved.

correctly convert object_address

5de5a66

object_address expressions have pointer type, and hence, the conversion must happen in bv_pointerst::convert_pointer_type.

SMT2 backend: type2id can now do arrays

766a986

The SMT2 backend constructs strings to disambiguate overloaded operations using types, and now supports generating strings for array types.

SMT2 backend: type2id can now do union_tag

4e425e7

The SMT2 backend constructs strings to disambiguate overloaded operations using types, and now supports generating strings for union_tag types.

introduce __CPROVER_separate

d1c201b

This introduces C syntax for a multi-ary predicate that implies that the given pointers point to pairwise different objects.

add the CHC state encoding

e54a0ee

This adds a CHC encoding that uses the concept of an abstract "program state", in contrast to the usual explicit enumeration of the variables that the state comprises.

kroening force-pushed the set_encoding branch from 523dcb7 to e54a0ee Compare September 23, 2022 12:38

tautschnig approved these changes Sep 27, 2022

View reviewed changes

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Sep 27, 2022

peterschrammel approved these changes Sep 29, 2022

View reviewed changes

kroening merged commit 6c6a4d4 into develop Sep 29, 2022

kroening deleted the set_encoding branch September 29, 2022 18:49


		#include <util/pointer_expr.h>

		#include "state.h"

CHC encoder #6717

CHC encoder #6717

Uh oh!

Conversation

kroening commented Mar 9, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

kroening Sep 19, 2022 • 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!

tautschnig Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

kroening Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

kroening Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Sep 19, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Sep 21, 2022

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kroening commented Mar 9, 2022 •

edited

Loading

codecov bot commented Mar 9, 2022 •

edited

Loading

kroening Sep 19, 2022 •

edited

Loading