Add AutoLifter, Parsynt, and Synduce

commit 3469e8d Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 21:40:16 2024 -0500 Add Synduce commit c9b6717 Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 21:16:46 2024 -0500 add parsynt commit c1c42e1 Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 20:23:05 2024 -0500 update reduce-algebra commit ce897f3 Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 19:56:31 2024 -0500 requires x86_64-linux commit 794a98b Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 19:52:28 2024 -0500 fixes commit 2173a8b Author: Ziteng Wang <z@wzt.me> Date: Sun Oct 27 19:44:51 2024 -0500 add autolifter
mistzzt · Oct 28, 2024 · ecacc0c · ecacc0c
1 parent 3eeebdf
commit ecacc0c
Showing 9 changed files with 1,015 additions and 6 deletions.
diff --git a/default.nix b/default.nix
@@ -12,4 +12,7 @@ in {
 
   sketch = pkgs.callPackage ./pkgs/sketch {stdenv = darwinStdenv;};
   reduce-algebra = pkgs.callPackage ./pkgs/reduce-algebra {stdenv = darwinStdenv;};
+  AutoLifter = pkgs.callPackage ./pkgs/AutoLifter {};
+  parsynt = pkgs.callPackage ./pkgs/parsynt {};
+  Synduce = pkgs.callPackage ./pkgs/Synduce {};
 }
diff --git a/flake.lock b/flake.lock
diff --git a/pkgs/AutoLifter/default.nix b/pkgs/AutoLifter/default.nix
@@ -0,0 +1,66 @@
+{
+  fetchFromGitHub,
+  lib,
+  makeWrapper,
+  stdenv,
+  cmake,
+  pkg-config,
+  wget,
+  jsoncpp,
+  glog,
+  cbmc,
+  gurobi,
+}:
+stdenv.mkDerivation rec {
+  name = "AutoLifter";
+  version = "1.0.0";
+  src =
+    fetchFromGitHub
+    {
+      owner = "jiry17";
+      repo = "AutoLifter";
+      rev = "4eef4cba765c6ee3687106b25c167bcd79441332";
+      sha256 = "bEAWVa0xYxtaPHGrpGNRBWey4rnJfRdpeYAaSKaoIPc=";
+    };
+  patches = [./diff.patch];
+
+  nativeBuildInputs = [
+    cmake
+    pkg-config
+    wget
+    jsoncpp
+    glog
+    cbmc
+    makeWrapper
+    gurobi
+  ];
+
+  preConfigure = ''
+    substituteInPlace basic/config.cpp run/run run/run_exp \
+      --replace 'SOURCEPATH' $out
+
+    substituteInPlace exp/paradigms/paradigm_util.cpp \
+      --replace 'command = "cbmc "' 'command = "${cbmc}/bin/cbmc "'
+
+    substituteInPlace run/run run/run_exp \
+      --replace 'build/main' 'bin/autolifter_main'
+  '';
+  cmakeBuildType = " ";
+
+  installPhase = ''
+    mkdir -p $out/bin
+    cp main $out/bin/autolifter_main
+    cp -r ../run $out
+    cp -r ../resource $out
+
+    makeWrapper $out/run/run $out/bin/autolifter_run --argv0 "run"
+    makeWrapper $out/run/run_exp $out/bin/autolifter_run_exp --argv0 "run"
+  '';
+
+  meta = with lib; {
+    description = "Artifact for TOPLAS24: Decomposition-Based Synthesis for Applying D&C-Like Algorithmic Paradigms";
+    homepage = "https://github.com/jiry17/AutoLifter";
+    license = licenses.mit;
+    platforms = ["x86_64-linux"];
+  };
+}
diff --git a/pkgs/AutoLifter/diff.patch b/pkgs/AutoLifter/diff.patch
@@ -0,0 +1,43 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index c1e551f..fef80df 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -1,4 +1,4 @@
+-cmake_minimum_required(VERSION 3.5.1)
++cmake_minimum_required(VERSION 3.25)
+ project(cpp)
+
+ set(CMAKE_CXX_STANDARD 17)
+@@ -7,18 +7,7 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/")
+
+ include_directories(include)
+
+-#jsoncpp
+-INCLUDE(FindPkgConfig)
+-find_package(Jsoncpp)
+-include_directories(${Jsoncpp_INCLUDE_DIR})
+-
+-#gurobi
+-set(GUROBI_PATH ${CMAKE_SOURCE_DIR}/resource/gurobi912/linux64)
+-INCLUDE_DIRECTORIES(${GUROBI_PATH}/include/)
+-link_directories(${GUROBI_PATH}/lib)
+-set(GUROBI_FILE libgurobi_g++5.2.a libgurobi91.so)
+-
+-set(THIRDPARTY_LIBS glog gflags ${Jsoncpp_LIBRARY} ${Z3_FILE} ${GUROBI_FILE})
++set(THIRDPARTY_LIBS glog gflags jsoncpp gurobi110 gurobi_g++8.5 ${Jsoncpp_LIBRARY} ${Z3_FILE})
+
+ add_subdirectory(basic)
+ add_subdirectory(autolifter)
+diff --git a/basic/grammar.cpp b/basic/grammar.cpp
+index ae2523d..7d43eb3 100644
+--- a/basic/grammar.cpp
++++ b/basic/grammar.cpp
+@@ -12,7 +12,7 @@
+
+ namespace {
+     Json::Value loadFromFile(std::string file_name) {
+-        std::ifstream inp(file_name, std::ios::out);
++        std::ifstream inp(file_name);
+         std::stringstream buf;
+         Json::Reader reader;
+         Json::Value root;
diff --git a/pkgs/Synduce/default.nix b/pkgs/Synduce/default.nix
@@ -0,0 +1,91 @@
+{
+  fetchFromGitHub,
+  lib,
+  makeWrapper,
+  ocamlPackages,
+  z3,
+  cvc4,
+  cvc5,
+}: let
+  parsexp_io = ocamlPackages.buildDunePackage rec {
+    pname = "parsexp_io";
+    version = "v0.17.0";
+    duneVersion = "3";
+    src =
+      fetchFromGitHub
+      {
+        owner = "janestreet";
+        repo = "parsexp_io";
+        rev = version;
+        sha256 = "r1HXO3VJ167QUgz4UIQuB5sY6p10FLE3Jrp9NmoDKoE=";
+      };
+    buildInputs = with ocamlPackages; [
+      ppx_js_style
+      parsexp
+    ];
+    strictDeps = true;
+    preBuild = ''
+      dune build parsexp_io.opam
+    '';
+  };
+in
+  ocamlPackages.buildDunePackage rec {
+    pname = "Synduce";
+    version = "0.2";
+    duneVersion = "3";
+    src =
+      fetchFromGitHub
+      {
+        owner = "synduce";
+        repo = "Synduce";
+        rev = "b5c1d1611d3fbf5d8cdf9a23fde52c2cbba95a89";
+        sha256 = "hgdN9IK1cv/IepaqGDzXXgKHqN2jtYWqWu9N4ejEYI4=";
+      };
+    patches = [./deps.patch];
+    preConfigure = ''
+      mkdir -p $out
+      cp -r $src/src $out
+
+      bin_path_src_path=$PWD/src/utils/DepPath.ml
+      rm $bin_path_src_path || true
+      touch $bin_path_src_path
+
+      echo "let cvc4_binary_path = Some(\"${cvc4}/bin/cvc4\")" >> $bin_path_src_path
+      echo "let cvc5_binary_path = Some(\"${cvc5}/bin/cvc5\")" >> $bin_path_src_path
+      echo "let z3_binary_path = \"${z3}/bin/z3\"" >> $bin_path_src_path
+    '';
+
+    nativeBuildInputs = with ocamlPackages; [menhir];
+
+    buildInputs = with ocamlPackages; [
+      getopt
+      sexplib
+      fmt
+      stdio
+      ppx_sexp_conv
+      ppx_let
+      fileutils
+      core
+      core_unix
+      lwt
+      lwt_ppx
+      camlp-streams
+      menhir
+      yojson
+      ppx_deriving
+      ocamlgraph
+      menhirLib
+      parsexp_io
+    ];
+    strictDeps = true;
+    preBuild = ''
+      dune build Synduce.opam
+    '';
+
+    meta = with lib; {
+      description = "An automatic recursive function transformer";
+      homepage = "https://github.com/synduce/Synduce";
+      license = licenses.mit;
+      platforms = platforms.unix;
+    };
+  }
diff --git a/pkgs/Synduce/deps.patch b/pkgs/Synduce/deps.patch
@@ -0,0 +1,55 @@
+diff --git a/src/utils/Config.ml b/src/utils/Config.ml
+index 25bc344..cb06e25 100644
+--- a/src/utils/Config.ml
++++ b/src/utils/Config.ml
+@@ -163,15 +163,9 @@ let using_cvc4_tuples = ref false
+ (** Don't generate a special grammar for constants if true. *)
+ let no_grammar_for_constants = ref true
+
+-let cvc4_binary_path =
+-  try Some (FileUtil.which "cvc4") with
+-  | _ -> None
+-;;
++let cvc4_binary_path = DepPath.cvc4_binary_path
+
+-let cvc5_binary_path =
+-  try Some (FileUtil.which "cvc5") with
+-  | _ -> None
+-;;
++let cvc5_binary_path = DepPath.cvc5_binary_path
+
+ let using_cvc5 () =
+   (Option.is_some cvc5_binary_path && not !use_cvc4) || Option.is_none cvc4_binary_path
+@@ -195,10 +189,7 @@ let cvc_binary_path () =
+       | None -> failwith "CVC5 and CVC4 not found."))
+ ;;
+
+-let z3_binary_path =
+-  try FileUtil.which "z3" with
+-  | _ -> failwith "Z3 not found (using 'which z3')."
+-;;
++let z3_binary_path = DepPath.z3_binary_path
+
+ let yices_binary_path =
+   try Some (FileUtil.which "yices-smt2") with
+diff --git a/src/utils/DepPath.ml b/src/utils/DepPath.ml
+new file mode 100644
+index 0000000..5ac2491
+--- /dev/null
++++ b/src/utils/DepPath.ml
+@@ -0,0 +1,14 @@
++let cvc4_binary_path =
++  try Some (FileUtil.which "cvc4") with
++  | _ -> None
++;;
++
++let cvc5_binary_path =
++  try Some (FileUtil.which "cvc5") with
++  | _ -> None
++;;
++
++let z3_binary_path =
++  try FileUtil.which "z3" with
++  | _ -> failwith "Z3 not found (using 'which z3')."
++;;
+\ No newline at end of file
diff --git a/pkgs/parsynt/default.nix b/pkgs/parsynt/default.nix
@@ -0,0 +1,61 @@
+{
+  fetchFromGitHub,
+  lib,
+  makeWrapper,
+  ocamlPackages,
+  z3,
+  racket,
+}:
+ocamlPackages.buildDunePackage rec {
+  pname = "Parsynt";
+  version = "0.3";
+  duneVersion = "3";
+  src =
+    fetchFromGitHub
+    {
+      owner = "victornicolet";
+      repo = "parsynt";
+      rev = "b70635d199dfc47378b19d4140093b7d261d753e";
+      sha256 = "cJnCGDFe7scnvlHN0G31Oi156iY0+DJnkZvgoQG3VRQ=";
+    };
+  patches = [./diff.patch];
+  preConfigure = ''
+    mkdir -p $out
+    cp -r $src/src $out
+
+    project_dir_src_path=$PWD/src/utils/Project_dir.ml
+    rm $project_dir_src_path || true
+    touch $project_dir_src_path
+    echo "let base = \"$out\"" >> $project_dir_src_path
+    echo "let src = \"$out/src/\"" >> $project_dir_src_path
+    echo "let templates = \"$out/src/templates/\"" >> $project_dir_src_path
+    echo "let racket = \"${racket}/bin/racket\"" >> $project_dir_src_path
+    echo "let z3 = \"${z3}/bin/z3\"" >> $project_dir_src_path
+  '';
+
+  nativeBuildInputs = with ocamlPackages; [menhir];
+
+  buildInputs = with ocamlPackages; [
+    getopt
+    sexplib
+    fmt
+    stdio
+    ppx_sexp_conv
+    ppx_let
+    fileutils
+    core
+    lwt
+    camlp-streams
+  ];
+  strictDeps = true;
+  preBuild = ''
+    dune build Parsynt.opam
+  '';
+
+  meta = with lib; {
+    description = "Automatic parallel divide-and-conquer programs synthesizer";
+    homepage = "https://github.com/victornicolet/parsynt";
+    license = licenses.gpl2;
+    platforms = platforms.unix;
+  };
+}