记录一下自己配置Doop环境的过程

环境

ARM架构（M2 Pro）
Ubuntu 22.04（Docker容器）

Souffle

在安装Doop之前，需要先编译Souffle（因为官方只有X86的包）。先安装必要的包

apt install \
  bison \
  build-essential \
  clang \
  cmake \
  doxygen \
  flex \
  g++ \
  git \
  libffi-dev \
  libncurses5-dev \
  libsqlite3-dev \
  make \
  mcpp \
  python3 \
  sqlite \
  zlib1g-dev

编译：

git clone https://github.com/souffle-lang/souffle.git
cd souffle
cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/usr/local/
cmake --build build -j8 --target install

Doop

安装JDK，并且把Doop给clone下来：

apt-get install openjdk-8-jdk
git clone https://bitbucket.org/yanniss/doop.git

进入Doop的目录，修改gradle/wrapper/gradle-wrapper.properties文件，把“services.gradle.org/distributions”改为“mirrors.cloud.tencent.com/gradle”（国内镜像），然后修改build.gradle文件，把jfrog.io那两行注释掉（因为现在失效了），同时取消centauri.di.uoa.gr那几行的注释。（后来我发现GitHub上的版本是有这样的修改的，不知道为啥bitbucket上没有）

运行./doop，开始编译。

在运行的时候可以加上指定的jre（–use-local-java-platform /usr/lib/jvm/java-8-openjdk-arm64/jre），这样可以节省不少下载的时间。

Doop运行新版Souffle的问题

参照https://bitbucket.org/yanniss/doop/src/master/docs/doop-101.md 的例子：

./doop -a micro -i docs/doop-101-examples/Example.jar \
--use-local-java-platform /usr/lib/jvm/java-8-openjdk-arm64/jre \
-L debug

发现会报错：

直接运行上面显示出错的souffle命令也是这样，这个问题发生在Doop的compile()方法里，后来发现需要加上-F指定fact的所在目录（out/xxx/database/）才能正常运行。

删除新版Souffle，编译2.1版本（需要apt install lsb-core，2.1编译会调用lsb_release命令），再次运行Doop，这次没有出错。

原因

抛出错误的位置是在生成的analysis-binary.cpp中：

if (op == "input") {
    out << "try {";
    out << "std::map<std::string, std::string> directiveMap(";
    printDirectives(directives);
    out << ");\n";
    out << R"_(if (!inputDirectory.empty()) {)_";
    out << R"_(directiveMap["fact-dir"] = inputDirectory;)_";
    out << "}\n";
    out << "IOSystem::getInstance().getReader(";
    out << "directiveMap, symTable, recordTable";
    out << ")->readAll(*" << synthesiser.getRelationName(synthesiser.lookup(io.getRelation()));
    out << ");\n";
    out << "} catch (std::exception& e) {std::cerr << \"Error loading " << io.getRelation()
        << " data: \" << e.what() "
        "<< "
        "'\\n';\nexit(1);\n}\n";
}

对比两个版本Souffle的运行，发现在2.1里，Doop是在run()里面才运行这个程序（这一阶段里面有加-F），compile()阶段只进行编译；而在2.4.1里，在Doop的compile()阶段，Souffle在编译好之后就直接自己运行这个程序了，而compile()阶段并没有传入-F，导致程序直接在当前目录（.）运行，找不到对应的fact。

代码区别

在2.1中，Souffle通过判断参数中是否包含dl-program和swig来决定是否运行程序，其中dl-program就是“-o”，也就是输出的程序文件名，这个参数是存在的，所以不会运行：

if (!Global::config().has("dl-program") && !Global::config().has("swig")) {
    executeBinary(baseFilename);
}

而在2.4.1中，Souffle直接判断是否包含compile参数（-c），这就导致了程序的运行：

const bool execute_mode = glb.config().has("compile") || glb.config().has("compile-many");
const bool compile_mode = glb.config().has("dl-program");
const bool generate_mode = glb.config().has("generate");
const bool generate_many_mode = glb.config().has("generate-many");
const bool must_interpret = !execute_mode && !compile_mode && !generate_mode && !generate_many_mode &&
                            !glb.config().has("swig");
const bool must_execute = execute_mode;
const bool must_compile = must_execute || compile_mode || glb.config().has("swig");
......
if (must_execute) {
    executeBinaryAndExit(glb, binaryFilename);
}

解决方法

1. 修改Doop的compile()，在原本的命令构建里加上-F参数：

String outputOpts = options.translateOnly ? outputCppOpts : "-F ${outDir}/database -c -o ${executablePath}"

2. 直接修改Souffle判断是否运行的条件。

至于是否还有其他兼容问题，暂时不确定。

参考

1. https://souffle-lang.github.io/build
2. https://bitbucket.org/yanniss/doop/src/master/