Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465

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.

…step encoding

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

… in CHC db

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.)

Yakir Vizel and others added 8 commits September 16, 2024 09:55

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

22e48ff

…step encoding

Enabling large step encoding using a flag

ffca3f2

Comparison operators for chcs

e2b3727

Merge branch 'diffblue:develop' into develop

6c88418

Merge branch 'develop' of github.com:yvizel/cbmc into develop

a2c42b6

Clean up old code

d1ffe55

Small fix

05277f4

Extracting new chcs after transformation

710f96f

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

tautschnig self-assigned this Sep 23, 2024

tautschnig reviewed Sep 23, 2024

View reviewed changes

Yakir Vizel and others added 9 commits October 13, 2024 14:38

Moving from std::set to std::unordered_set

618730c

Naming conventions, unsigned -> size_t

bb675e1

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

349830b

Adjusting API changes

9f18c1b

Merge branch 'diffblue:develop' into develop

f274914

Merge branch 'develop' of github.com:yvizel/cbmc into develop

4673ae3

Merge branch 'diffblue:develop' into develop

a586173

Equivalent query clauses may represent different properties. Allow it…

4d6728c

… in CHC db

Adding regression tests for large step encoding of CHCs

c68df5b

qinheping self-assigned this Oct 28, 2024

Yakir Vizel and others added 5 commits October 29, 2024 13:56

Some comments and minor modifications

8970b81

Merge branch 'diffblue:develop' into develop

c5f6d65

Removed whitespace

1af0494

Removed include

d618cf3

Merge branch 'develop' of github.com:yvizel/cbmc into develop

e84fe43

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

Missing commit

3f73e52

Yakir Vizel and others added 3 commits November 10, 2024 14:48

Removing redundant include, and fixing function arguments

13d1779

Merge branch 'diffblue:develop' into develop

540b219

Merge branch 'diffblue:develop' into develop

ed10809

tautschnig approved these changes Jan 8, 2025

View reviewed changes

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465

Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465

yvizel commented Sep 22, 2024

tautschnig left a comment

tautschnig Sep 23, 2024

tautschnig left a comment

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig Jan 8, 2025

tautschnig commented Jan 8, 2025

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

		#include <iostream>
		#include <fstream>

Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465

Are you sure you want to change the base?

Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465

Conversation

yvizel commented Sep 22, 2024

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Jan 8, 2025