Skip to content

Commit d460854

Browse files
mistzztmistzzt
authored
Add AutoLifter, Parsynt, and Synduce (#6)
* add autolifter * fixes * requires x86_64-linux * update reduce-algebra * add parsynt * Add Synduce * correct ci nixpkgs channel
1 parent 3eeebdf commit d460854

File tree

10 files changed

+1016
-9
lines changed

10 files changed

+1016
-9
lines changed

‎.github/workflows/build.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,7 @@ jobs:
1919
cachixName:
2020
- mistzzt
2121
nixPath:
22-
- nixpkgs=channel:nixos-unstable
23-
- nixpkgs=channel:nixpkgs-unstable
24-
- nixpkgs=channel:nixos-23.11
22+
- nixpkgs=channel:nixos-24.05
2523
runs-on: ubuntu-latest
2624
steps:
2725
- name: Checkout repository

‎default.nix

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,7 @@ in {
1212

1313
sketch = pkgs.callPackage ./pkgs/sketch {stdenv = darwinStdenv;};
1414
reduce-algebra = pkgs.callPackage ./pkgs/reduce-algebra {stdenv = darwinStdenv;};
15+
AutoLifter = pkgs.callPackage ./pkgs/AutoLifter {};
16+
parsynt = pkgs.callPackage ./pkgs/parsynt {};
17+
Synduce = pkgs.callPackage ./pkgs/Synduce {};
1518
}

‎flake.lock

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎pkgs/AutoLifter/default.nix

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
{
2+
fetchFromGitHub,
3+
lib,
4+
makeWrapper,
5+
stdenv,
6+
cmake,
7+
pkg-config,
8+
wget,
9+
jsoncpp,
10+
glog,
11+
cbmc,
12+
gurobi,
13+
}:
14+
stdenv.mkDerivation rec {
15+
name = "AutoLifter";
16+
version = "1.0.0";
17+
src =
18+
fetchFromGitHub
19+
{
20+
owner = "jiry17";
21+
repo = "AutoLifter";
22+
rev = "4eef4cba765c6ee3687106b25c167bcd79441332";
23+
sha256 = "bEAWVa0xYxtaPHGrpGNRBWey4rnJfRdpeYAaSKaoIPc=";
24+
};
25+
patches = [./diff.patch];
26+
27+
nativeBuildInputs = [
28+
cmake
29+
pkg-config
30+
wget
31+
jsoncpp
32+
glog
33+
cbmc
34+
makeWrapper
35+
gurobi
36+
];
37+
38+
preConfigure = ''
39+
substituteInPlace basic/config.cpp run/run run/run_exp \
40+
--replace 'SOURCEPATH' $out
41+
42+
substituteInPlace exp/paradigms/paradigm_util.cpp \
43+
--replace 'command = "cbmc "' 'command = "${cbmc}/bin/cbmc "'
44+
45+
substituteInPlace run/run run/run_exp \
46+
--replace 'build/main' 'bin/autolifter_main'
47+
'';
48+
cmakeBuildType = " ";
49+
50+
installPhase = ''
51+
mkdir -p $out/bin
52+
cp main $out/bin/autolifter_main
53+
cp -r ../run $out
54+
cp -r ../resource $out
55+
56+
makeWrapper $out/run/run $out/bin/autolifter_run --argv0 "run"
57+
makeWrapper $out/run/run_exp $out/bin/autolifter_run_exp --argv0 "run"
58+
'';
59+
60+
meta = with lib; {
61+
description = "Artifact for TOPLAS24: Decomposition-Based Synthesis for Applying D&C-Like Algorithmic Paradigms";
62+
homepage = "https://github.com/jiry17/AutoLifter";
63+
license = licenses.unfreeRedistributable;
64+
platforms = ["x86_64-linux"];
65+
};
66+
}

‎pkgs/AutoLifter/diff.patch

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
diff --git a/CMakeLists.txt b/CMakeLists.txt
2+
index c1e551f..fef80df 100644
3+
--- a/CMakeLists.txt
4+
+++ b/CMakeLists.txt
5+
@@ -1,4 +1,4 @@
6+
-cmake_minimum_required(VERSION 3.5.1)
7+
+cmake_minimum_required(VERSION 3.25)
8+
project(cpp)
9+
10+
set(CMAKE_CXX_STANDARD 17)
11+
@@ -7,18 +7,7 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/")
12+
13+
include_directories(include)
14+
15+
-#jsoncpp
16+
-INCLUDE(FindPkgConfig)
17+
-find_package(Jsoncpp)
18+
-include_directories(${Jsoncpp_INCLUDE_DIR})
19+
-
20+
-#gurobi
21+
-set(GUROBI_PATH ${CMAKE_SOURCE_DIR}/resource/gurobi912/linux64)
22+
-INCLUDE_DIRECTORIES(${GUROBI_PATH}/include/)
23+
-link_directories(${GUROBI_PATH}/lib)
24+
-set(GUROBI_FILE libgurobi_g++5.2.a libgurobi91.so)
25+
-
26+
-set(THIRDPARTY_LIBS glog gflags ${Jsoncpp_LIBRARY} ${Z3_FILE} ${GUROBI_FILE})
27+
+set(THIRDPARTY_LIBS glog gflags jsoncpp gurobi110 gurobi_g++8.5 ${Jsoncpp_LIBRARY} ${Z3_FILE})
28+
29+
add_subdirectory(basic)
30+
add_subdirectory(autolifter)
31+
diff --git a/basic/grammar.cpp b/basic/grammar.cpp
32+
index ae2523d..7d43eb3 100644
33+
--- a/basic/grammar.cpp
34+
+++ b/basic/grammar.cpp
35+
@@ -12,7 +12,7 @@
36+
37+
namespace {
38+
Json::Value loadFromFile(std::string file_name) {
39+
- std::ifstream inp(file_name, std::ios::out);
40+
+ std::ifstream inp(file_name);
41+
std::stringstream buf;
42+
Json::Reader reader;
43+
Json::Value root;

‎pkgs/Synduce/default.nix

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
{
2+
fetchFromGitHub,
3+
lib,
4+
makeWrapper,
5+
ocamlPackages,
6+
z3,
7+
cvc4,
8+
cvc5,
9+
}: let
10+
parsexp_io = ocamlPackages.buildDunePackage rec {
11+
pname = "parsexp_io";
12+
version = "v0.17.0";
13+
duneVersion = "3";
14+
src =
15+
fetchFromGitHub
16+
{
17+
owner = "janestreet";
18+
repo = "parsexp_io";
19+
rev = version;
20+
sha256 = "r1HXO3VJ167QUgz4UIQuB5sY6p10FLE3Jrp9NmoDKoE=";
21+
};
22+
buildInputs = with ocamlPackages; [
23+
ppx_js_style
24+
parsexp
25+
];
26+
strictDeps = true;
27+
preBuild = ''
28+
dune build parsexp_io.opam
29+
'';
30+
};
31+
in
32+
ocamlPackages.buildDunePackage rec {
33+
pname = "Synduce";
34+
version = "0.2";
35+
duneVersion = "3";
36+
src =
37+
fetchFromGitHub
38+
{
39+
owner = "synduce";
40+
repo = "Synduce";
41+
rev = "b5c1d1611d3fbf5d8cdf9a23fde52c2cbba95a89";
42+
sha256 = "hgdN9IK1cv/IepaqGDzXXgKHqN2jtYWqWu9N4ejEYI4=";
43+
};
44+
patches = [./deps.patch];
45+
preConfigure = ''
46+
mkdir -p $out
47+
cp -r $src/src $out
48+
49+
bin_path_src_path=$PWD/src/utils/DepPath.ml
50+
rm $bin_path_src_path || true
51+
touch $bin_path_src_path
52+
53+
echo "let cvc4_binary_path = Some(\"${cvc4}/bin/cvc4\")" >> $bin_path_src_path
54+
echo "let cvc5_binary_path = Some(\"${cvc5}/bin/cvc5\")" >> $bin_path_src_path
55+
echo "let z3_binary_path = \"${z3}/bin/z3\"" >> $bin_path_src_path
56+
'';
57+
58+
nativeBuildInputs = with ocamlPackages; [menhir];
59+
60+
buildInputs = with ocamlPackages; [
61+
getopt
62+
sexplib
63+
fmt
64+
stdio
65+
ppx_sexp_conv
66+
ppx_let
67+
fileutils
68+
core
69+
core_unix
70+
lwt
71+
lwt_ppx
72+
camlp-streams
73+
menhir
74+
yojson
75+
ppx_deriving
76+
ocamlgraph
77+
menhirLib
78+
parsexp_io
79+
];
80+
strictDeps = true;
81+
preBuild = ''
82+
dune build Synduce.opam
83+
'';
84+
85+
meta = with lib; {
86+
description = "An automatic recursive function transformer";
87+
homepage = "https://github.com/synduce/Synduce";
88+
license = licenses.mit;
89+
platforms = platforms.unix;
90+
};
91+
}

‎pkgs/Synduce/deps.patch

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
diff --git a/src/utils/Config.ml b/src/utils/Config.ml
2+
index 25bc344..cb06e25 100644
3+
--- a/src/utils/Config.ml
4+
+++ b/src/utils/Config.ml
5+
@@ -163,15 +163,9 @@ let using_cvc4_tuples = ref false
6+
(** Don't generate a special grammar for constants if true. *)
7+
let no_grammar_for_constants = ref true
8+
9+
-let cvc4_binary_path =
10+
- try Some (FileUtil.which "cvc4") with
11+
- | _ -> None
12+
-;;
13+
+let cvc4_binary_path = DepPath.cvc4_binary_path
14+
15+
-let cvc5_binary_path =
16+
- try Some (FileUtil.which "cvc5") with
17+
- | _ -> None
18+
-;;
19+
+let cvc5_binary_path = DepPath.cvc5_binary_path
20+
21+
let using_cvc5 () =
22+
(Option.is_some cvc5_binary_path && not !use_cvc4) || Option.is_none cvc4_binary_path
23+
@@ -195,10 +189,7 @@ let cvc_binary_path () =
24+
| None -> failwith "CVC5 and CVC4 not found."))
25+
;;
26+
27+
-let z3_binary_path =
28+
- try FileUtil.which "z3" with
29+
- | _ -> failwith "Z3 not found (using 'which z3')."
30+
-;;
31+
+let z3_binary_path = DepPath.z3_binary_path
32+
33+
let yices_binary_path =
34+
try Some (FileUtil.which "yices-smt2") with
35+
diff --git a/src/utils/DepPath.ml b/src/utils/DepPath.ml
36+
new file mode 100644
37+
index 0000000..5ac2491
38+
--- /dev/null
39+
+++ b/src/utils/DepPath.ml
40+
@@ -0,0 +1,14 @@
41+
+let cvc4_binary_path =
42+
+ try Some (FileUtil.which "cvc4") with
43+
+ | _ -> None
44+
+;;
45+
+
46+
+let cvc5_binary_path =
47+
+ try Some (FileUtil.which "cvc5") with
48+
+ | _ -> None
49+
+;;
50+
+
51+
+let z3_binary_path =
52+
+ try FileUtil.which "z3" with
53+
+ | _ -> failwith "Z3 not found (using 'which z3')."
54+
+;;
55+
\ No newline at end of file

‎pkgs/parsynt/default.nix

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
{
2+
fetchFromGitHub,
3+
lib,
4+
makeWrapper,
5+
ocamlPackages,
6+
z3,
7+
racket,
8+
}:
9+
ocamlPackages.buildDunePackage rec {
10+
pname = "Parsynt";
11+
version = "0.3";
12+
duneVersion = "3";
13+
src =
14+
fetchFromGitHub
15+
{
16+
owner = "victornicolet";
17+
repo = "parsynt";
18+
rev = "b70635d199dfc47378b19d4140093b7d261d753e";
19+
sha256 = "cJnCGDFe7scnvlHN0G31Oi156iY0+DJnkZvgoQG3VRQ=";
20+
};
21+
patches = [./diff.patch];
22+
preConfigure = ''
23+
mkdir -p $out
24+
cp -r $src/src $out
25+
26+
project_dir_src_path=$PWD/src/utils/Project_dir.ml
27+
rm $project_dir_src_path || true
28+
touch $project_dir_src_path
29+
echo "let base = \"$out\"" >> $project_dir_src_path
30+
echo "let src = \"$out/src/\"" >> $project_dir_src_path
31+
echo "let templates = \"$out/src/templates/\"" >> $project_dir_src_path
32+
echo "let racket = \"${racket}/bin/racket\"" >> $project_dir_src_path
33+
echo "let z3 = \"${z3}/bin/z3\"" >> $project_dir_src_path
34+
'';
35+
36+
nativeBuildInputs = with ocamlPackages; [menhir];
37+
38+
buildInputs = with ocamlPackages; [
39+
getopt
40+
sexplib
41+
fmt
42+
stdio
43+
ppx_sexp_conv
44+
ppx_let
45+
fileutils
46+
core
47+
lwt
48+
camlp-streams
49+
];
50+
strictDeps = true;
51+
preBuild = ''
52+
dune build Parsynt.opam
53+
'';
54+
55+
meta = with lib; {
56+
description = "Automatic parallel divide-and-conquer programs synthesizer";
57+
homepage = "https://github.com/victornicolet/parsynt";
58+
license = licenses.gpl2;
59+
platforms = platforms.unix;
60+
};
61+
}

0 commit comments

Comments
 (0)