Alive2 version bump and misc (#879)

CMakeLists.txt

@@ -16,6 +16,10 @@ if(NOT EXISTS ${LLVM_CONFIG_EXECUTABLE})
   message(FATAL_ERROR "llvm-config could not be found!")
 endif()
 
+find_path(ZSTD_LIBRARY_DIR
+          NAMES libzstd.a libzstd.dylib libzstd.so
+          HINTS /usr/local/lib /opt/homebrew/lib)
+
 execute_process(
   COMMAND ${LLVM_CONFIG_EXECUTABLE} --includedir
   OUTPUT_VARIABLE LLVM_INCLUDEDIR
@@ -51,6 +55,7 @@ execute_process(
 )
 
 set(PASS_LDFLAGS "${LLVM_LDFLAGS}")
+set(LLVM_LDFLAGS "${LLVM_LDFLAGS} -L ${ZSTD_LIBRARY_DIR}")
 
 execute_process(
   COMMAND ${LLVM_CONFIG_EXECUTABLE} --bindir

README.md

@@ -11,7 +11,8 @@ You will need a reasonably modern compiler toolchain. LLVM has instructions
 on how to get one for Linux:
 http://llvm.org/docs/GettingStarted.html#getting-a-modern-host-c-toolchain
 
-You will also need CMake to build Souper and its dependencies.
+You will also need CMake to build Souper and its dependencies, and the zstd
+library from your package manager or from Homebrew.
 
 # Building Souper
 

build_deps.sh

@@ -28,7 +28,7 @@ llvm_repo=https://github.com/regehr/llvm-project.git
 llvm_commit=disable-peepholes-llvmorg-17.0.3-1
 klee_repo=https://github.com/regehr/klee
 klee_branch=klee-for-souper-17-2
-alive_commit=v4
+alive_commit=v7
 alive_repo=https://github.com/manasij7479/alive2.git
 z3_repo=https://github.com/Z3Prover/z3.git
 z3_commit=z3-4.12.2

lib/Infer/AliveDriver.cpp

@@ -129,7 +129,7 @@ class FunctionBuilder {
   template <typename T>
   void assume(T &&V) {
     auto AI =
-      std::make_unique<IR::Assume>(*std::move(V), IR::Assume::Kind::IfNonPoison);
+      std::make_unique<IR::Assume>(*std::move(V), IR::Assume::Kind::AndNonPoison);
     F.getBB("").addInstr(std::move(AI));
   }
 
@@ -229,50 +229,13 @@ std::map<souper::Inst *, llvm::APInt>
 performCegisFirstQuery(tools::Transform &t,
                        std::map<std::string, souper::Inst *> &SouperConsts,
                        smt::expr &TriedExpr) {
-  IR::State SrcState(t.src, true);
-  IR::State TgtState(t.tgt, false);
-  util::sym_exec(SrcState);
-  util::sym_exec(TgtState);
-
-  auto &&Sv = SrcState.returnVal();
-  auto &&Tv = TgtState.returnVal();
-
-  std::map<souper::Inst *, llvm::APInt> SynthesisResult;
-  SynthesisResult.clear();
-
-  std::set<smt::expr> Vars;
-  std::map<std::string, smt::expr> SMTConsts;
-  for (auto &[Var, Val] : TgtState.getValues()) {
-    auto &Name = Var->getName();
-    if (startsWith("%reservedconst", Name)) {
-      SMTConsts[Name] = Val.val.value;
-    }
-  }
-
-  if (SkipAliveSolver)
-    return SynthesisResult;
-
-  auto R = smt::check_expr((Sv.val.value == Tv.val.value) && (TriedExpr));
-  // no more guesses, stop immediately
-  if (R.isUnsat()) {
-    if (DebugLevel > 3)
-      llvm::errs()<<"No more new possible guesses\n";
-    return {};
-  } else if (R.isSat()) {
-    auto &&Model = R.getModel();
-    smt::expr TriedAnte(false);
-
-    for (auto &[name, expr] : SMTConsts) {
-      TriedAnte |= (expr != smt::expr::mkUInt(Model.getInt(expr), expr.bits()));
-    }
-    TriedExpr &= TriedAnte;
-
-    for (auto &[name, expr] : SMTConsts) {
-      auto *I = SouperConsts[name];
-      SynthesisResult[I] = llvm::APInt(I->Width, Model.getInt(expr));
-    }
-  }
-  return SynthesisResult;
+  // Removed because implementation was bit-rotting.
+  // The combination of the options requiring this is
+  // not currently used.
+  // TODO implement either this or the solver based synthesis
+  // before removing KLEE backend
+  llvm::errs() << "CEGIS constant synthesis through alive unimplemented.";
+  return {};
 }
 
 std::map<souper::Inst *, llvm::APInt>