Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) by yvizel · Pull Request #8465 · diffblue/cbmc

yvizel · 2024-09-22T12:19:17Z

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.

tautschnig

A bunch of comments that each apply in several more places. More generally, however, it would be great to have comments. At bare minimum there should be high-level design comments in some place that explain how the various pieces fit together. Also, we need tests that demonstrate the new feature.

src/cprover/cprover_parse_options.h

src/cprover/chc_db.cpp

tautschnig · 2024-09-23T12:49:25Z

src/cprover/chc_db.cpp

+    m_head_idx[func].insert(&r);
+
+    std::vector<symbol_exprt> use;
+    r.used_relations(*this,std::back_inserter(use));


I'd suggest that used_relations just return a std::vector<symbol_exprt> (which is cheap with copy elision).

src/cprover/cutpoint_graph.h

tautschnig

clang-format fixes are strictly required.
A bunch of suggestions below. Would be great to see them addressed, but we can do this in parallel with reviewing/working on the solver changes.

tautschnig · 2025-01-08T11:54:37Z

regression/cprover/large_step/trace/trace_pointer3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG


Applies to this one as well as all other KNOWNBUG tests that you added: could you please add at the bottom:

-- Brief explanation as to what the bug is.

That is, add another -- and then an explanatory text.

tautschnig · 2025-01-08T11:55:57Z

src/cprover/chc_db.cpp

+chc_dbt::chc_sett chc_dbt::m_empty_set;
+std::unordered_set<exprt, irep_hash> chc_grapht::m_expr_empty_set;
+
+void horn_clauset::used_relations(chc_dbt &db, std::vector<symbol_exprt> & out) const


You'll want to run clang-format (or, rather, git-clang-format) to ensure all use of whitespace is in line with the repository rules.

tautschnig · 2025-01-08T12:00:25Z

src/cprover/chc_db.cpp

+    std::vector<symbol_exprt> use;
+    r.used_relations(*this, use);


Please change the signature of used_relations such that this becomes std::vector<symbol_exprt> use = r.used_relations(*this);. That is, return by value.

tautschnig · 2025-01-08T12:03:03Z

src/cprover/chc_db.cpp

+                    if (can_cast_expr<function_application_exprt>(expr))
+                    {
+                      const function_application_exprt & f = to_function_application_expr(expr);
+                      funcs.insert(f);
+                    }


Suggested change

if (can_cast_expr<function_application_exprt>(expr))

{

const function_application_exprt & f = to_function_application_expr(expr);

funcs.insert(f);

}

if (auto f = expr_try_dynamic_cast<function_application_exprt>(expr))

{

funcs.insert(*f);

}

tautschnig · 2025-01-08T12:06:24Z

src/cprover/chc_db.h

+  forall_exprt m_chc;
+
+public:
+  horn_clauset(forall_exprt f) : m_chc(f) {}


Qualify this with explicit

tautschnig · 2025-01-08T12:19:58Z

src/cprover/cprover_parse_options.cpp

@@ -277,6 +277,7 @@ int cprover_parse_optionst::main()

    solver_options.trace = cmdline.isset("trace");
    solver_options.verbose = cmdline.isset("verbose");
+    solver_options.large_step = cmdline.isset("large-step");


Please add a help entry (in cprover_parse_optionst::help at the bottom of this file).

tautschnig · 2025-01-08T12:20:32Z

src/cprover/cutpoint_graph.cpp

+#include <iostream>
+#include <fstream>


Are either of those really required?

tautschnig · 2025-01-08T12:22:38Z

src/cprover/cutpoint_graph.cpp

+cutpoint_grapht::~cutpoint_grapht() {
+  m_edges.clear();
+  m_cps.clear();
+  m_insts.clear();
+}


Why is the explicit deconstruction required?

tautschnig · 2025-01-08T12:24:16Z

src/cprover/state_encoding.cpp

+  container_encoding_targett container2;
+  std::vector<horn_clauset> all2;


What are those good for?

tautschnig · 2025-01-08T12:25:09Z

src/cprover/state_encoding.cpp

+    if (!can_cast_expr<forall_exprt>(clause))
+    {
+      throw incorrect_goto_program_exceptiont("Not forall");
+    }
+    const forall_exprt& forall = to_forall_expr(clause);
+    db.add_clause(forall);


I'd rewrite this using expr_try_dynamic_cast instead of can_cast_expr.

tautschnig · 2025-01-08T12:28:00Z

Also, once done with the changes, please rebase/combine all commits into a single one. (Or perhaps one for the source changes and one for the tests.)

…step encoding

… in CHC db

yvizel requested review from kroening, peterschrammel and tautschnig as code owners September 22, 2024 12:19

tautschnig self-assigned this Sep 23, 2024

tautschnig reviewed Sep 23, 2024

View reviewed changes

qinheping self-assigned this Oct 28, 2024

yvizel requested a review from tautschnig October 29, 2024 12:01

tautschnig approved these changes Jan 8, 2025

View reviewed changes

tautschnig assigned yvizel and unassigned tautschnig and qinheping Jan 8, 2025

Yakir Vizel and others added 18 commits February 24, 2025 15:24

Adding CHCs data structures and utilities for resolution-based large …

d6ba7cf

…step encoding

Enabling large step encoding using a flag

d390670

Comparison operators for chcs

fc597d6

Clean up old code

26f982d

Small fix

e8bb4e7

Extracting new chcs after transformation

5a02d55

Moving from std::set to std::unordered_set

f01cbe9

Naming conventions, unsigned -> size_t

7672856

Renaming types and function names, and adjusments to changes in API

7ae6ef2

Adjusting API changes

c5fffbd

Equivalent query clauses may represent different properties. Allow it…

be0662b

… in CHC db

Adding regression tests for large step encoding of CHCs

7638533

Some comments and minor modifications

8df40d1

Removed whitespace

d4d3835

Removed include

d75ddaf

Missing commit

193da7a

Removing redundant include, and fixing function arguments

aa6df74

Changing user_relations function declaration

0f6a42a

yvizel added 2 commits February 24, 2025 15:24

clang format, and minor fixes to is_query, is_fact

ad717ba

Small fix

fbb2194

yvizel force-pushed the develop branch from 66d6fa8 to fbb2194 Compare March 2, 2025 12:19

yvizel added 2 commits April 5, 2025 12:02

Merge branch 'diffblue:develop' into develop

7a48436

Merge branch 'diffblue:develop' into develop

d559b6f

		container_encoding_targett container2;
		std::vector<horn_clauset> all2;

		#include <iostream>
		#include <fstream>

Comments

Conversation

yvizel commented Sep 22, 2024

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!

Uh oh!

Uh oh!

Uh oh!

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

tautschnig commented Jan 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants