Docker + write_(aig|cnf)_external -> abc: error while loading shared libraries: libreadline.so.7: cannot open shared object file: No such file or directory

[weaversa]

I'm unable to try write_aig_external etc. because I'm using Docker and abc seems to be installed incorrectly? Maybe?

$ docker pull galoisinc/saw:nightly
nightly: Pulling from galoisinc/saw
Digest: sha256:38c6ca19ccd5710166e1ca773372e79a63d4d0d774a09ed8b3b0a72143447610
Status: Image is up to date for galoisinc/saw:nightly
$ docker run --rm -it --mount type=bind,src=/Users,dst=/Users --workdir=$(pwd) --user=$(id -u):$(id -g) --env CRYPTOLPATH=$(pwd) galoisinc/saw:nightly $*

docker.io/galoisinc/saw:nightly
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.7.0.99 (<non-dev-build>)



sawscript> write_cnf_external "test.cnf" {{ \x -> x == 0b0001 }}

Stack trace:
"write_cnf_external" (<stdin>:1:1-1:19):
abc returned non-zero exit code: ExitFailure 127
Standard output:

Standard error:
abc: error while loading shared libraries: libreadline.so.7: cannot open shared object file: No such file or directory


sawscript> exec "which" ["abc"] ""
[18:13:37.295] "/usr/local/bin/abc\n"

[RyanGlScott]

I can reproduce this with the Docker invocation you're using (minus the filesystem-specific parts such as --mount type=bind,src=/Users,dst=/Users) but not if I use the saw binary from https://saw.galois.com/downloads.html, so this is likely related to the way the Docker image is built.

[RyanGlScott]

Some further digging reveals that saw's Dockerfile is to blame. It installs libreadline-dev (which comes with libreadline.so) in one stage:

saw-script/saw/Dockerfile

Lines 1 to 5 in 731bcd0

	FROM debian:buster AS solvers
	# Install needed packages for building
	RUN apt-get update \
	&& apt-get install -y curl cmake gcc g++ git libreadline-dev unzip

The result of that stage is copied over in a subsequent stage:

saw-script/saw/Dockerfile

Lines 61 to 65 in 731bcd0

	FROM debian:buster-slim
	RUN apt-get update \
	&& apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip
	COPY --from=build /home/saw/rootfs /
	COPY --from=solvers /solvers/rootfs /

However, that later stage doesn't install libreadline-dev, so it will fail at runtime if any code path involving libreadline.so is invoked. I can confirm that installing libreadline-dev in that last stage fixes the issue:

diff --git a/saw/Dockerfile b/saw/Dockerfile
index f7f13c46..345bd48e 100644
--- a/saw/Dockerfile
+++ b/saw/Dockerfile
@@ -60,7 +60,7 @@ RUN chown -R root:root /home/saw/rootfs
 
 FROM debian:buster-slim
 RUN apt-get update \
-    && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip
+    && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 libreadline-dev unzip
 COPY --from=build /home/saw/rootfs /
 COPY --from=solvers /solvers/rootfs /
 RUN useradd -m saw && chown -R saw:saw /home/saw

Patch incoming.