Add term simplification to Python bindings #897

Baltoli · 2023-11-21T12:06:31Z

This PR exposes the concrete term simplification routines already used by the booster to the Python bindings so that they can be called from Pyk. Specifically, it adds two free functions to the runtime module:

simplify_pattern(Pattern, Sort) -> Pattern
simplify_bool_pattern(Pattern) -> bool

These are exposed as free functions because they depend on the runtime library and so can't be automatically bound to the Pattern class as methods; I suggest Pyk probably wants to monkey-patch them into its Pattern class along with some kind of dynamic check for whether the runtime module has been loaded or not.

Previously, the C and Python bindings didn't share a great deal of code; the simplification routine is the first bit of non-trivial behaviour that they need to share. I have therefore started a reorganisation of the bindings code to extract as much functionality to a common library, which has the additional benefit of reducing the amount of memory-leak prone handling of C wrapper structures. To keep the diff in this PR reasonable I have not completed this migration, but this is future work that I will complete in a future PR.

A summary of the changes in this PR is as follows:

Build a common bindings library that the C and Python bindings link against.
Extract the minimal set of features from the existing C bindings that the Python bindings require to perform term simplification, and port the C bindings over to calling the extracted common features.
Add a test case to the Python bindings test suite that performs a few small simplifications of sort Int and Bool; these are really just smoke tests and Pyk should test the feature more thoroughly.

Baltoli · 2023-11-22T12:45:29Z

I have also tested the booster's integration tests with this change applied and there is no breakage to the C bindings.

tothtamas28

Looks good in terms of functionality.

Python tests: runtimeverification/pyk#736

dwightguth

It's very difficult to follow these changes because they are a mix of a refactoring that moves a lot of code around, and new features. I'm concerned that despite my best efforts, I still wasn't really able to determine what code was "new" and review it effectively.

I think you need to refactor the history of this PR to more obviously break it into two components: the moving around of existing code, and the addition of new code.

This commit sets up an empty library that will be used to extract features currently implemented in _either_ the Python or C bindings, such that the two bindings can share code.

This commit reorganises the existing C bindings for the LLVM backend by extracting some of their AST manipulation code to the newly-created core bindings library. It does not change the set of features offered by the bindings; the diff does not look quite like a straight reorganisation because the implementation changes from "pure C" style to direct usage of the underlying C++ data structures, but the intent of the code remains identical.

Builds on the refactoring performed in the previous commits by adding a new binding to the Python module that exposes the core library's term simplifier. A small amount of build system code is required to do so as well.

This test mimics existing Python bindings tests; it performs a few small smoke tests of the exposed features from the previous commits in this PR but leaves the bulk of the testing responsibility to Pyk.

Baltoli · 2023-11-28T15:41:55Z

bindings/c/lib.cpp

-
-  kore_symbol_free(inj_sym);
+  auto inj = new kore_pattern;
+  inj->ptr_ = kllvm::bindings::make_injection(term->ptr_, from->ptr_, to->ptr_);


@dwightguth As an example of how to look at the changes in this diff, the kllvm::bindings::make_injection function contains code that is equivalent to the C on the LHS here, but using the underlying C++ structures directly. All the changes in this commit are of that form.

Baltoli · 2023-11-28T15:42:26Z

bindings/core/src/core.cpp

+  auto inj_sym = KORESymbol::Create("inj");
+
+  inj_sym->addFormalArgument(from);
+  inj_sym->addFormalArgument(to);
+
+  auto inj = KORECompositePattern::Create(std::move(inj_sym));
+  inj->addArgument(term);
+
+  return inj;


The restated C++ code from my other comment is here.

This function got missed out when I rebased some commit history in #897

~Blocked on runtimeverification/llvm-backend#897 ~Blocked on runtimeverification/llvm-backend#910 Adds runtime methods `simplify` and `simplify_bool`. --------- Co-authored-by: devops <devops@runtimeverification.com>

…n/pyk#736) ~Blocked on runtimeverification/llvm-backend#897 ~Blocked on runtimeverification/llvm-backend#910 Adds runtime methods `simplify` and `simplify_bool`. --------- Co-authored-by: devops <devops@runtimeverification.com>

Baltoli force-pushed the term-simplifier branch 2 times, most recently from e4c3531 to 9d93cb5 Compare November 22, 2023 10:29

Baltoli marked this pull request as ready for review November 22, 2023 11:00

Baltoli requested review from dwightguth, gtrepta, theo25 and tothtamas28 November 22, 2023 11:21

tothtamas28 mentioned this pull request Nov 22, 2023

Expose pattern simplification from KLLVM bindings runtimeverification/pyk#736

Merged

tothtamas28 reviewed Nov 22, 2023

View reviewed changes

This was referenced Nov 22, 2023

Finish migrating C bindings to core bindings library #900

Open

Expose function evaluation to bindings #903

Closed

dwightguth requested changes Nov 27, 2023

View reviewed changes

Baltoli added 2 commits November 28, 2023 15:20

Set up empty core bindings library

2c26aff

This commit sets up an empty library that will be used to extract features currently implemented in _either_ the Python or C bindings, such that the two bindings can share code.

Baltoli force-pushed the term-simplifier branch from 33b638e to d422878 Compare November 28, 2023 15:31

Baltoli added 2 commits November 28, 2023 15:37

Expose reorganised term simplifier to Python

4706524

Builds on the refactoring performed in the previous commits by adding a new binding to the Python module that exposes the core library's term simplifier. A small amount of build system code is required to do so as well.

Add python simplifier test

707de47

This test mimics existing Python bindings tests; it performs a few small smoke tests of the exposed features from the previous commits in this PR but leaves the bulk of the testing responsibility to Pyk.

Baltoli force-pushed the term-simplifier branch from d422878 to 707de47 Compare November 28, 2023 15:38

Baltoli commented Nov 28, 2023

View reviewed changes

Baltoli requested a review from dwightguth November 28, 2023 16:23

dwightguth approved these changes Nov 28, 2023

View reviewed changes

Baltoli added the automerge label Nov 28, 2023

Merge branch 'master' into term-simplifier

a50b953

rv-jenkins merged commit 236a777 into master Nov 28, 2023
5 checks passed

rv-jenkins deleted the term-simplifier branch November 28, 2023 20:42

Baltoli mentioned this pull request Nov 30, 2023

Reinstate missing simplify_bool_pattern binding #910

Merged

rv-jenkins pushed a commit that referenced this pull request Nov 30, 2023

Reinstate missing simplify_bool_pattern binding (#910)

4cbbb3a

This function got missed out when I rebased some commit history in #897

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add term simplification to Python bindings #897

Add term simplification to Python bindings #897

Baltoli commented Nov 21, 2023 •

edited

Loading

Baltoli commented Nov 22, 2023

tothtamas28 left a comment

dwightguth left a comment

Baltoli Nov 28, 2023

Baltoli Nov 28, 2023

Add term simplification to Python bindings #897

Add term simplification to Python bindings #897

Conversation

Baltoli commented Nov 21, 2023 • edited Loading

Baltoli commented Nov 22, 2023

tothtamas28 left a comment

Choose a reason for hiding this comment

dwightguth left a comment

Choose a reason for hiding this comment

Baltoli Nov 28, 2023

Choose a reason for hiding this comment

Baltoli Nov 28, 2023

Choose a reason for hiding this comment

Baltoli commented Nov 21, 2023 •

edited

Loading