Merge remote-tracking branch 'origin/main' into gussmith23/lr-egglog-…

…antiunify

.dockerignore

@@ -0,0 +1,18 @@
+*.dep
+*.zo
+
+.vscode/*
+.lit_test_times.txt
+**/Output
+
+**/.DS_Store
+**/.lit_test_times.txt
+**/Output/
+**/__pycache__
+
+target
+Cargo.lock
+.env
+
+**/*.so*
+**/*.d

.env.template

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+# User should set these variables.
+#
+# Optional environment variables which you opt not to set should be
+# deleted/commented out.
+#
+# OPTIONAL: Path to llvm-config binary. Only needed if LLVM's `llvm-config` and
+# `FileCheck` binaries are not in the PATH.
+export LLVM_CONFIG="/path/to/llvm-config"
+# OPTIONAL: Path to Yosys binary. Only needed if the `yosys` binary is not
+# available on your path, or if you want to use a specific version of Yosys.
+export YOSYS="/path/to/yosys"
+
+
+# Do not modify below this line.
+SCRIPTPATH="$( cd -- "$(dirname "$0")" >/dev/null 2>&1 ; pwd -P )"
+export CHURCHROAD_DIR=$SCRIPTPATH

.github/workflows/run-checks-github-runners.yml → .github/workflows/built-test-check-format.yml

@@ -1,4 +1,4 @@
-name: Build Docker image, format check, and run tests
+name: Build, Test, Check Format
 
 on:
   push:
@@ -48,10 +48,10 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
@@ -65,10 +65,10 @@ jobs:
       #     images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
 
       - name: Docker Setup Buildx
-        uses: docker/setup-buildx-action@v2
+        uses: docker/setup-buildx-action@v3
 
       - name: Build and push Docker image
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true
@@ -85,7 +85,7 @@ jobs:
            ]
     steps:
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
@@ -102,7 +102,7 @@ jobs:
     needs: build-and-push-image
     steps:
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
@@ -111,5 +111,7 @@ jobs:
       - name: Pull image
         run: docker pull ${{ env.IMAGE_TAG }}
 
-      - name: Rust format check
-        run: docker run ${{ env.IMAGE_TAG }} cargo fmt --manifest-path ./Cargo.toml -- --check
+      - name: Project-wide formatting check
+        run: |
+          docker run ${{ env.IMAGE_TAG }} \
+            bash -c './fmt.sh && git status && [ -z "$(git status --porcelain)" ]'

.gitignore

@@ -12,3 +12,7 @@
 
 target
 Cargo.lock
+.env
+
+**/*.so*
+**/*.d

Cargo.toml

@@ -1,10 +1,11 @@
 [package]
-name = "lakeroad-egglog"
+name = "churchroad"
 version = "0.1.0"
 edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
 egglog = { git = "https://github.com/egraphs-good/egglog", rev = "41562802315eccc9136c9d2ae6967d2df4071420" }
-log = "0.4.20"
+log = "0.4.20"
+lexpr = "0.2.6"

Dockerfile

@@ -51,20 +51,67 @@ RUN apt install -y \
 RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
 ENV PATH="/root/.cargo/bin:$PATH"
 
+# Build Rust package.
+WORKDIR /root/churchroad
+# ADD has weird behavior when it comes to directories. That's why we need so
+# many ADDs.
+ADD egglog_src egglog_src
+ADD src src
+ADD tests tests
+ADD Cargo.toml .
+RUN cargo build
+
+# Build Yosys.
+WORKDIR /root
+ARG MAKE_JOBS=2
+ADD dependencies.sh .
+RUN source /root/dependencies.sh \
+  && mkdir yosys && cd yosys \
+  && wget -qO- https://github.com/YosysHQ/yosys/archive/$YOSYS_COMMIT_HASH.tar.gz | tar xz --strip-components=1 \
+  && PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make config-gcc \
+  && PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make -j ${MAKE_JOBS} install \
+  && rm -rf /root/yosys
+
+# Add /root/.local/bin to PATH.
+ENV PATH="/root/.local/bin:$PATH"
+
+# Build Yosys plugin.
+WORKDIR /root/churchroad/yosys-plugin
+ADD yosys-plugin .
+RUN make -j ${MAKE_JOBS}
+
+# Make a binary for `lit`. If you're on Mac, you can install lit via Brew.
+# Ubuntu doesn't have a binary for it, but it is available on pip and is
+# installed later in this Dockerfile.
+WORKDIR /root
+RUN mkdir -p /root/.local/bin \
+  && echo "#!/usr/bin/env python3" >> /root/.local/bin/lit \
+  && echo "from lit.main import main" >> /root/.local/bin/lit \
+  && echo "if __name__ == '__main__': main()" >> /root/.local/bin/lit \
+  && chmod +x /root/.local/bin/lit
+
+# Point to llvm-config binary. Alternatively, make sure you have a binary called
+# `llvm-config` on your PATH.
+ENV LLVM_CONFIG=llvm-config-14
+
+# Python dependencies.
+WORKDIR /root/churchroad
+ADD requirements.txt .
+RUN pip install -r requirements.txt
+
+ENV CHURCHROAD_DIR=/root/churchroad
+
 # Add other Churchroad files. It's useful to put this as far down as possible.
 # In general, only ADD files just before they're needed. This maximizes the
 # ability to cache intermediate containers and minimizes rebuilding.
 #
-# In reality, we use the git functionality of ADD (enabled in our case via the
-# optional flag --keep-git-dir) to add all of the checked-in files of the
-# Churchroad repo (but not including the .git directory itself). We could cut
-# this down further if we wanted, but I think this is a clean approach for now.
+# We use the git functionality of ADD (enabled in our case via the optional flag
+# --keep-git-dir) to add all of the checked-in files of the Churchroad repo (but
+# not including the .git directory itself). We could cut this down further if we
+# wanted, but I think this is a clean approach for now.
 WORKDIR /root/churchroad
 ADD --keep-git-dir=false . .
 
-# Build Rust package.
-WORKDIR /root/churchroad
-RUN cargo build
-
 WORKDIR /root/churchroad
+ADD fmt.sh run-tests.sh ./
 CMD [ "/bin/bash", "run-tests.sh" ]

README.md

@@ -1,3 +1,15 @@
 # Churchroad
 
 :letsgo3:
+
+## Yosys Plugin
+
+[`./yosys-plugin/](./yosys-plugin/)
+
+We provide a Yosys plugin,
+  which can output Churchroad IR
+  from Yosys.
+Please see the README
+  in that directory
+  for information on building
+  and using the plugin.

dependencies.sh

@@ -0,0 +1,22 @@
+#!/bin/sh
+# This script exports a number of variables that help to pin the versions of
+# various Churchroad dependencies.
+#
+# To use, source this script before running relevant commands e.g. in a
+# Dockerfile.
+#
+# This is just one possible way to implement dependency tracking. Some of the
+# other options are:
+# - No tracking at all. E.g. in the Dockerfile, we could clone Yosys at a
+#   specific commit, using a "magic constant" commit hash. This isn't ideal,
+#   because if we use Yosys elsewhere (e.g. in the evaluation) we have to make
+#   sure we keep the commit hashes in sync.
+# - Git submodules. This is very similar to what we've chosen to do, but it's
+#   more directly supported by Git. However, it's a bit overkill to add a full
+#   repository as a submodule when we only need the resulting binary.
+#
+# This option is essentially a lighter-weight version of submodules. We track
+# the commit hashes of the dependencies we need, but nothing additional is
+# cloned on a `git clone --recursive`.
+
+export YOSYS_COMMIT_HASH="f8d4d7128cf72456cc03b0738a8651ac5dbe52e1"

egglog_src/lakeroad.egg

@@ -224,4 +224,4 @@
     (Op2 op 
      (Op1 (Extract (- n 1) 1) e1) (Op1 (Extract (- n 1) 1) e2))
     (Op2 op 
-     (Op1 (Extract 0 0) e1) (Op1 (Extract 0 0) e2))))))
+     (Op1 (Extract 0 0) e1) (Op1 (Extract 0 0) e2))))))

fmt.sh

@@ -2,6 +2,9 @@
 
 set -e
 SCRIPT_DIR=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &>/dev/null && pwd)
-raco fmt -i "$SCRIPT_DIR"/racket/*.rkt
-raco fmt -i "$SCRIPT_DIR"/bin/*.rkt
-cargo fmt --manifest-path "$SCRIPT_DIR"/rust/Cargo.toml
+
+# Rust formatting.
+cargo fmt --manifest-path "$SCRIPT_DIR"/Cargo.toml
+
+# Python formatting.
+black "$SCRIPT_DIR"/yosys-plugin/tests/lit.cfg

old_versions/churchroad_old/.gitignore

@@ -1,3 +1,2 @@
-target
-# For now, adding Cargo.lock to repo.
-# Cargo.lock
+/target
+Cargo.lock

requirements.txt

@@ -0,0 +1,2 @@
+black==24.2.0
+lit==15.0.0

run-tests.sh

@@ -2,4 +2,6 @@
 
 set -e
 
-cargo test
+cargo test
+
+./yosys-plugin/run_tests.sh

src/lib.rs

@@ -218,7 +218,6 @@ pub fn to_verilog(term_dag: &TermDag, id: usize) -> String {
 /// TODO(@gussmith23): Ideally, this would be done via an `import` statement.
 /// That's not currently possible because of the Rust-defined primitive
 /// `debruijnify` in Lakeroad.
-pub fn import_lakeroad(egraph: &mut EGraph) {
     egraph
         .parse_and_run_program(
             r#"
@@ -461,6 +460,4 @@ pub fn list_modules(egraph: &mut EGraph, num_variants: usize) {
 mod tests {
     // use super::*;
 
-    #[test]
-    fn it_works() {}
 }

yosys-plugin/Makefile

@@ -0,0 +1,7 @@
+churchroad.so: churchroad.cc
+	$(CXX) $(shell yosys-config --cxxflags --ldflags) -shared -o $@ churchroad.cc -lboost_filesystem
+
+clean:
+	rm -rfv *.d *.o churchroad.so*
+
+-include *.d

yosys-plugin/README.md

@@ -0,0 +1,30 @@
+# Churchroad Backend Plugin for Yosys
+
+We provide a plugin
+  for Yosys
+  which produces Churchroad code.
+
+## Note on Building
+
+Yosys plugins are simply shared libraries
+  that can be loaded into Yosys at runtime.
+As a result,
+  you are required to build
+  a Yosys plugin using the same
+  build environment
+  as your `yosys` binary.
+The easiest way to ensure this
+  is to simply build Yosys
+  from source.
+If you prefer to use
+  a prebuilt Yosys binary,
+  Yosys provides a Docker image
+  which sets up the appropriate
+  environment:
+  <https://github.com/YosysHQ-GmbH/tabby-cad-plugin-build>
+We don't yet support
+  using this option easily.
+If you would like this feature,
+  please open an issue.
+Until then, all plugin users should build Yosys
+  from source.