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,7 +46,7 @@ build.plugin: build.lib install.lib
 #####################################################
 
 .PHONY: install
-install: uninstall.plugin install.plugin
+install: install.plugin
 
 .PHONY: uninstall
 uninstall: uninstall.lib uninstall.plugin

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

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,22 @@ all: install
 # CLEAN
 #####################################################
 
-clean: uninstall
-	bapbuild -clean
-
-
-####################################################
-# REBUILD ON LIB CHANGE
-####################################################
-
-$(TRACK_LIB): $(LIB_SRC_FILES)
-	bapbuild -clean
-	mkdir _build
-	touch $(TRACK_LIB)
+clean:
+	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 +44,7 @@ uninstall.verifier:
 
 .PHONY: uninstall
 uninstall: uninstall.verifier
-	bapbundle remove $(PASS_NAME).plugin
+	dune uninstall
 
 .PHONY: reinstall
 reinstall: uninstall reinstall
@@ -97,15 +65,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 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 tests/integration

wp/plugin/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.6)
+(using dune_site 0.1)
+(name wp)

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 = [
 

wp/plugin/wp.opam

@@ -0,0 +1,25 @@
+opam-version: "2.0"
+name: "wp"
+version: "0.1"
+synopsis: "A weakest-precondition analysis plugin"
+description: """
+A weakest-precondition analysis plugin for use with BAP.
+"""
+maintainer: "Draper Laboratory"
+authors: [
+  "Chloe Fortuna <[email protected]>"
+  "JT Paasch <[email protected]>"
+  "Philip Zucker <[email protected]>"
+  "Benjamin Mourad <[email protected]>"
+]
+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"
+depends: [
+  "bap" {>= "2.4.0"}
+  "core" {>= "v0.15.0"}
+  "z3" {>= "4.8.14"}
+  "ounit2" {>= "2.2.3"}
+  "re" {>= "1.9.0"}
+]