Builds the plugin using dune

wp/Makefile

@@ -18,10 +18,10 @@ all: install
 
 .PHONY: clean
 clean:
-	@printf $(FMT_STR) "CLEANING LIB"
-	$(MAKE) -C $(LIB) clean
 	@printf $(FMT_STR) "CLEANING PLUGIN"
 	$(MAKE) -C $(PLUGIN) clean
+	@printf $(FMT_STR) "CLEANING LIB"
+	$(MAKE) -C $(LIB) clean
 
 #####################################################
 # BUILD
@@ -46,10 +46,12 @@ build.plugin: build.lib install.lib
 #####################################################
 
 .PHONY: install
-install: uninstall.plugin install.plugin
+install: install.plugin
 
 .PHONY: uninstall
-uninstall: uninstall.lib uninstall.plugin
+uninstall:
+	$(MAKE) uninstall.plugin
+	$(MAKE) uninstall.lib
 
 .PHONY: uninstall.lib
 uninstall.lib:
@@ -71,7 +73,7 @@ install.plugin: install.lib
 
 # lib must be installed BEFORE building plugin
 .PHONY: install.lib
-install.lib:
+install.lib: uninstall.plugin
 	@printf $(FMT_STR) "INSTALLING LIB"
 	$(MAKE) -C $(LIB) install
 

wp/lib/bap_wp/Makefile

@@ -35,7 +35,7 @@ clean.local:
 #####################################################
 
 $(BUILD): $(SRC_FILES)
-	dune build -p $(PROJECT)
+	dune build -p $(PROJECT) @install
 	touch $(BUILD)
 
 .PHONY: build
@@ -71,11 +71,11 @@ test: test.unit test.performance
 
 .PHONY: test.unit
 test.unit:
-	dune runtest tests/unit
+	dune runtest --force tests/unit
 
 .PHONY: test.performance
 test.performance:
-	dune runtest tests/performance
+	dune runtest --force tests/performance
 
 #####################################################
 # DOCS

wp/lib/bap_wp/bap_wp.opam

@@ -1,25 +1,39 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "bap_wp"
 version: "0.1"
 synopsis: "A weakest-precondition analysis library"
-description: """
-A weakest-precondition analysis library for use with BAP.
-"""
-maintainer: "Draper Laboratory"
-authors: [
-  "Chloe Fortuna <[email protected]>"
-  "JT Paasch <[email protected]>"
+description: "A weakest-precondition analysis library for use with BAP."
+maintainer: [
+  "Chloe Fortuna <[email protected]"
+  "JT Paasch <[email protected]>"
   "Philip Zucker <[email protected]>"
   "Benjamin Mourad <[email protected]>"
 ]
+authors: ["Draper Laboratory"]
 license: "MIT"
 homepage: "https://github.com/draperlaboratory/cbat_tools"
-bug-reports: "https://github.com/draperlaboratory/cbat_tools"
-dev-repo: "git+https://github.com/draperlaboratory/cbat_tools"
+bug-reports: "https://github.com/draperlaboratory/cbat_tools/issues"
 depends: [
-  "bap" {>= "2.4.0"}
-  "core" {>= "v0.15.0"}
+  "dune" {>= "3.6"}
+  "bap" {>= "2.6.0"}
+  "core" {>= "v0.15"}
   "z3" {>= "4.8.14"}
   "ounit2" {>= "2.2.3"}
   "re" {>= "1.9.0"}
+  "odoc" {with-doc}
 ]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/draperlaboratory/cbat_tools.git"

wp/lib/bap_wp/dune-project

@@ -1,2 +1,26 @@
-(lang dune 1.7)
+(lang dune 3.6)
 (name bap_wp)
+(license MIT)
+(version 0.1)
+(source (github draperlaboratory/cbat_tools))
+
+(authors "Draper Laboratory")
+
+(maintainers
+ "Chloe Fortuna <[email protected]"
+ "JT Paasch <[email protected]>"
+ "Philip Zucker <[email protected]>"
+ "Benjamin Mourad <[email protected]>")
+
+(generate_opam_files true)
+
+(package
+ (name bap_wp)
+ (synopsis "A weakest-precondition analysis library")
+ (description "A weakest-precondition analysis library for use with BAP.")
+ (depends
+  (bap (>= 2.6.0))
+  (core (>= v0.15))
+  (z3 (>= 4.8.14))
+  (ounit2 (>= 2.2.3))
+  (re (>= 1.9.0))))

wp/lib/bap_wp/src/dune

@@ -1,5 +1,5 @@
 (library
    (name bap_wp)
    (public_name bap_wp)
-   (libraries bap bap-x86-cpu bap-arm z3 ounit2 re str)
+   (libraries bap-main bap-x86-cpu bap-arm z3 ounit2 re str)
    (preprocess (pps ppx_sexp_conv ppx_bin_prot)))

wp/lib/bap_wp/tests/performance/dune

@@ -1,3 +1,3 @@
 (test
   (name test)
-  (libraries bap z3 ounit2 bap_wp))
+  (libraries z3 ounit2 bap_wp))

wp/lib/bap_wp/tests/unit/dune

@@ -1,3 +1,3 @@
 (test
   (name test)
-  (libraries bap z3 ounit2 bap_wp))
+  (libraries z3 ounit2 bap_wp))

wp/plugin/.gitignore

@@ -0,0 +1 @@
+*.install

wp/plugin/Makefile

@@ -1,29 +1,10 @@
-PASS_NAME := wp
 SHELL := /bin/bash
 
 SAMPLE_BIN_DIR := ../resources/sample_binaries
-API_PATH := $(shell bap --api-list-paths)
+API_PATH := $(shell bap config sysdatadir)/api
 VERIFIER_LOCAL := api/c/cbat.h
 VERIFIER_INSTALL_PATH := $(API_PATH)/c/cbat.h
 
-PKGS := 'z3,bap_wp,re,str'
-TAG := 'warn(A-48-44-70)'
-Is := 'lib'
-
-TEST_PKGS := 'bap,z3,bap_wp,ounit2,re,str,core_unix'
-TEST_TAG := 'warn(A-48-44-70),debug,thread'
-TEST_Is := 'lib,tests/test_libs'
-
-TEST_Is_UNIT := $(TEST_Is)',tests/unit'
-TEST_Is_INTEGRATION := $(TEST_Is)',tests/integration'
-
-BUILD := $(PASS_NAME).plugin
-SRC_FILES := $(wildcard **/*.ml) $(wildcard **/*.mli)
-
-LIB_SRC_FILES := $(wildcard ../lib/bap_wp/src/*.ml) $(wildcard ../lib/bap_wp/src/*.mli)
-
-TRACK_LIB:= _build/TRACK_LIB
-
 #####################################################
 # DEFAULT
 #####################################################
@@ -37,35 +18,23 @@ all: install
 # CLEAN
 #####################################################
 
+.PHONY: clean
 clean: uninstall
-	bapbuild -clean
-
-
-####################################################
-# REBUILD ON LIB CHANGE
-####################################################
-
-$(TRACK_LIB): $(LIB_SRC_FILES)
-	bapbuild -clean
-	mkdir _build
-	touch $(TRACK_LIB)
+	dune clean
 
 #####################################################
 # BUILD
 #####################################################
 
-build: $(BUILD)
-
-$(BUILD): $(SRC_FILES) $(TRACK_LIB)
-	bapbuild -use-ocamlfind -pkgs $(PKGS) -tag $(TAG) -I $(Is) $(PASS_NAME).plugin
+build:
+	dune build -p wp @install
 
 #####################################################
 # INSTALL
 #####################################################
 
-install: $(BUILD) $(VERIFIER_INSTALL_PATH)
-	bapbundle update -desc 'Computes the weakest precondition of a subroutine given a postcondition.' $(PASS_NAME).plugin
-	bapbundle install $(PASS_NAME).plugin
+install: build $(VERIFIER_INSTALL_PATH)
+	dune install
 
 $(VERIFIER_INSTALL_PATH): $(VERIFIER_LOCAL)
 	cp $(VERIFIER_LOCAL) $(VERIFIER_INSTALL_PATH)
@@ -76,7 +45,7 @@ uninstall.verifier:
 
 .PHONY: uninstall
 uninstall: uninstall.verifier
-	bapbundle remove $(PASS_NAME).plugin
+	dune uninstall
 
 .PHONY: reinstall
 reinstall: uninstall reinstall
@@ -97,15 +66,8 @@ test: test.unit
 
 .PHONY: test.unit
 test.unit: install
-	ocamlbuild -r -use-ocamlfind \
-		-pkgs $(TEST_PKGS) \
-		-tag $(TEST_TAG) -Is $(TEST_Is_UNIT) test.native
-	./test.native
+	dune runtest --force tests/unit
 
 .PHONY: test.integration
 test.integration: install
-	ocamlbuild -r -use-ocamlfind \
-		-pkgs $(TEST_PKGS) \
-		-tag $(TEST_TAG) \
-		-tag $(TEST_TAG) -Is $(TEST_Is_INTEGRATION) test.native
-	./test.native
+	dune runtest --force tests/integration

wp/plugin/dune-project

@@ -0,0 +1,27 @@
+(lang dune 3.6)
+(using dune_site 0.1)
+(name wp)
+(license MIT)
+(version 0.1)
+(source (github draperlaboratory/cbat_tools))
+
+(authors "Draper Laboratory")
+
+(maintainers
+ "Chloe Fortuna <[email protected]"
+ "JT Paasch <[email protected]>"
+ "Philip Zucker <[email protected]>"
+ "Benjamin Mourad <[email protected]>")
+
+(generate_opam_files true)
+
+(package
+ (name wp)
+ (synopsis "A weakest-precondition analysis plugin")
+ (description "A weakest-precondition analysis plugin for use with BAP.")
+ (depends
+  (bap (>= 2.6.0))
+  (core (>= v0.15))
+  (z3 (>= 4.8.14))
+  (ounit2 (>= 2.2.3))
+  (re (>= 1.9.0))))

wp/plugin/src/dune

@@ -0,0 +1,11 @@
+(library
+ (name wp_plugin)
+ (public_name wp.plugin)
+ (libraries z3 bap_wp re str)
+ (preprocess (pps ppx_bin_prot)))
+
+(plugin
+ (name wp)
+ (package wp)
+ (libraries wp.plugin)
+ (site (bap-common plugins)))

wp/plugin/wp.ml → wp/plugin/src/wp_main.ml

@@ -438,3 +438,9 @@ let callback
 
 let () =
   Cmd.declare name grammar callback ~doc
+
+let () =
+  let doc =
+    "Computes the weakest precondition of a \
+     subroutine given a postcondition." in
+  Extension.declare ~doc @@ fun _ -> Ok ()

wp/plugin/tests/integration/dune

@@ -0,0 +1,3 @@
+(test
+ (name test)
+ (libraries wp.test))

wp/plugin/tests/integration/test_wp_integration.ml

@@ -1,5 +1,5 @@
 open OUnitTest
-open Test_wp_utils
+open Test_lib.Test_wp_utils
 
 let integration_tests = List.append [
 

wp/plugin/tests/test_libs/dune

@@ -0,0 +1,4 @@
+(library
+ (name test_lib)
+ (public_name wp.test)
+ (libraries z3 ounit2 bap_wp re str core_unix))

wp/plugin/tests/test_libs/test_wp_utils.ml

@@ -24,7 +24,7 @@ module IntSet = Set.Make(Int)
 
 (* To run these tests: `make test` or `make test.integration` in wp directory *)
 
-let bin_dir = "../resources/sample_binaries"
+let bin_dir = "../../../../../resources/sample_binaries"
 
 let timeout_msg = "Test times out!"
 
@@ -292,7 +292,7 @@ let test_plugin
       ~foutput:(fun res -> check_result res reg_list checker)
       ~backtrace:true
       ~chdir:target
-      ~ctxt:ctxt
+      ~ctxt
   in
   test_case ~length test
 

wp/plugin/tests/unit/dune

@@ -0,0 +1,3 @@
+(test
+ (name test)
+ (libraries wp.test))

wp/plugin/tests/unit/test_wp_unit.ml

@@ -1,5 +1,5 @@
 open OUnitTest
-open Test_wp_utils
+open Test_lib.Test_wp_utils
 
 let unit_tests = [