From 6fad07e6e1f16c0c662092132e2141f690176d34 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 4 Dec 2012 03:31:08 +0000 Subject: [PATCH] Update build system for ml api --- src/api/ml/Makefile | 14 +++++ src/api/ml/Makefile.build | 69 ++++++++++++++++++++++++ src/api/ml/generate_mlapi.sh | 53 ++++++++++++++++++ src/api/ml/postprocess.sed | 8 +++ src/api/ml/{build.sed => preprocess.sed} | 0 src/api/ml/reverse.sed | 3 ++ src/api/ml/{z3.idl => z3.0.idl} | 5 -- 7 files changed, 147 insertions(+), 5 deletions(-) create mode 100644 src/api/ml/Makefile create mode 100644 src/api/ml/Makefile.build create mode 100755 src/api/ml/generate_mlapi.sh create mode 100644 src/api/ml/postprocess.sed rename src/api/ml/{build.sed => preprocess.sed} (100%) create mode 100644 src/api/ml/reverse.sed rename src/api/ml/{z3.idl => z3.0.idl} (98%) diff --git a/src/api/ml/Makefile b/src/api/ml/Makefile new file mode 100644 index 000000000..55f89fe1c --- /dev/null +++ b/src/api/ml/Makefile @@ -0,0 +1,14 @@ +# to set ARGS, invoke as e.g.: $ make ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS' +ARGS= + + +default: z3.ml z3.mli z3_stubs.c + + +%.ml %.mli %_stubs.c: ../%_api.h %.0.idl x3.ml x3V3.ml x3V3.mli \ + error_handling.idl mlx_get_app_args.idl mlx_get_array_sort.idl mlx_get_datatype_sort.idl mlx_get_domains.idl mlx_get_error_msg.idl mlx_get_pattern_terms.idl mlx_get_tuple_sort.idl mlx_mk_context_x.idl mlx_mk_datatypes.idl mlx_mk_numeral.idl mlx_mk_sort.idl mlx_mk_symbol.idl mlx_model.idl mlx_numeral_refine.idl mlx_parse_smtlib.idl mlx_sort_refine.idl mlx_statistics.idl mlx_symbol_refine.idl mlx_term_refine.idl \ + generate_mlapi.sh add_error_checking.V3.sed add_error_checking.sed preprocess.sed postprocess.sed reverse.sed + ./generate_mlapi.sh $(ARGS) + +clean: + rm -f z3.ml z3.mli z3_stubs.c diff --git a/src/api/ml/Makefile.build b/src/api/ml/Makefile.build new file mode 100644 index 000000000..27c798bbf --- /dev/null +++ b/src/api/ml/Makefile.build @@ -0,0 +1,69 @@ +# Makefile to compile OCaml interface to Z3 +# +# Parameters: ARGS and DEPS environment variables +# ARGS is passed through to the Makefile that generates the OCaml interface +# DEPS is a sequence of files that are deleted when the OCaml interface changes + +SRC_ML=../../../src/api/ml +ifeq (${OS}, Windows_NT) +# the BLD_ML path ends up stored in z3.cm{,x}a, so it must be in windows format +BLD_ML=$(shell cygpath -m $(CURDIR)) +CFLAGS=-ccopt -wd4090 -ccopt -I$(SRC_ML)/.. +XCDBG=-g $(CFLAGS) +XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS) +# ole32 is needed by camlidl (COM support) +XLIB=-cclib ole32.lib +AR=lib /nologo /LIBPATH:../../build ../../z3.lib /out: +O=obj +A=lib +else +BLD_ML=$(CURDIR) +CFLAGS=-ccopt -Wno-discard-qual -ccopt -Wno-unused-variable -ccopt -I$(SRC_ML)/.. +XCDBG=-g -ccopt -g $(CFLAGS) +XCOPT=-ccopt -O3 -ccopt -fomit-frame-pointer $(CFLAGS) +XLIB= +AR=ar rcs # note trailing space is significant +O=o +A=a +endif + + +all: z3.cma z3.cmxa ocamlz3 + + +# keep these files to avoid repeatedly rebuilding them +.PRECIOUS: $(SRC_ML)/z3.ml $(SRC_ML)/z3.mli $(SRC_ML)/z3_stubs.c z3.ml z3.mli z3_stubs.c z3_theory_stubs.c + +# regenerate OCaml API if needed +$(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c: $(SRC_ML)/Makefile + make -C $(SRC_ML) z3.mli z3.ml z3_stubs.c + +# copy OCaml API from src to build directories +%.mli %.ml %_stubs.c %_theory_stubs.c: $(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c Makefile + cp $(SRC_ML)/z3.mli $(SRC_ML)/z3.ml $(SRC_ML)/z3_stubs.c $(SRC_ML)/z3_theory_stubs.c . + +# OCaml library module for native code clients +%.cmxa %.cmi lib%stubs.a %.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile + rm -f $(DEPS) + ocamlopt.opt -c $(XCOPT) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c + $(AR)libz3stubs.$(A) z3.$(O) z3_stubs.$(O) z3_theory_stubs.$(O) + ocamlopt.opt -a -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs z3.cmx -o z3.cmxa + rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.$(O) z3.cmx + +# OCaml library module for byte code clients +%.cma %.cmi lib%stubs_dbg.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile + rm -f $(DEPS) + ocamlc.opt -c $(XCDBG) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c + $(AR)libz3stubs_dbg.$(A) z3_stubs.$(O) z3_theory_stubs.$(O) + ocamlc.opt -custom -a $(CXDBG) -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs_dbg z3.cmo -o z3.cma + rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.cmo + + +# OCaml custom toplevel system pre-linked with Z3 +ocamlz3: z3.cma Makefile + ocamlmktop -o ocamlz3 z3.cma -cclib -L. + + +clean: Makefile + make -C $(SRC_ML) clean + rm -rf Makefile libz3stubs.$(A) libz3stubs_dbg.$(A) ocamlz3 ocamlz3.dSYM z3.$(O) z3.$(A) z3.cma z3.cmi z3.cmo z3.cmx z3.cmxa z3.ml z3.mli z3_stubs.$(O) z3_stubs.c z3_theory_stubs.$(O) z3_theory_stubs.c diff --git a/src/api/ml/generate_mlapi.sh b/src/api/ml/generate_mlapi.sh new file mode 100755 index 000000000..dd8692833 --- /dev/null +++ b/src/api/ml/generate_mlapi.sh @@ -0,0 +1,53 @@ +#!/bin/bash + +# Script to generate the Z3 OCaml API +# +# Assumes that environment variables are set to provide access to the following commands: camlidl, gcc, grep, sed +# +# This script uses 'gcc -E' as the C preprocessor, other C preprocessors may work but have not been tested. +# +# Invoke with "-DUNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead. +# Invoke with "-DLEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead. + + +# add calls to error checking routine +# convert from doxygen to ocamldoc markup and other syntactic munging +# ../z3_api.h -> z3V3_api.idl +sed -f add_error_checking.V3.sed -f preprocess.sed ../z3_api.h > z3V3_api.idl + +# z3.idl (z3V3_api.idl x3V3.mli x3V3.ml) -> z3V3_stubs.c, z3V3.mli, z3V3.ml +gcc -E -w -P -CC -xc -DCAMLIDL -DMLAPIV3 $@ z3.0.idl > z3V3.idl +camlidl -nocpp z3V3.idl + +# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10 +grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$" z3V3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/renameV3.sed +grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3V3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g" >> /tmp/renameV3.sed + +# rename.sed to substitute out type equations for enums and options, then postprocess +cp -f z3V3.mli z3V3.ml /tmp +sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.mli > z3V3.mli +sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.ml > z3V3.ml + +# ../z3_api.h -> z3_api.idl +sed -f add_error_checking.sed -f preprocess.sed ../z3_api.h > z3_api.idl + +# z3.idl (z3_api.idl x3.ml) -> z3_stubs.c, z3.mli, z3.ml +gcc -E -w -P -CC -xc -I. -DCAMLIDL $@ z3.0.idl > z3.idl +camlidl -nocpp z3.idl + +# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10 +grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$" z3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/rename.sed +grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g" >> /tmp/rename.sed + +# rename.sed to substitute out type equations for enums and options, then postprocess +cp z3.mli z3.ml /tmp +sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.mli > z3.mli +sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.ml > z3.ml + + +# append Z3.V3 module onto Z3 module +cat z3V3.mli >> z3.mli +cat z3V3.ml >> z3.ml +sed "1,22d" z3V3_stubs.c >> z3_stubs.c + +rm -f z3V3_api.idl z3V3.idl z3V3.ml z3V3.mli z3V3_stubs.c z3_api.idl z3.idl diff --git a/src/api/ml/postprocess.sed b/src/api/ml/postprocess.sed new file mode 100644 index 000000000..f25f70cb7 --- /dev/null +++ b/src/api/ml/postprocess.sed @@ -0,0 +1,8 @@ +# remove 'z3_' and 'Z3_' prefixes on names + +s/{\!Z3\./{\!/g +s/\([^_]\)[zZ]3_/\1/g + +# remove cyclic definitions introduced by substituting type equations + +s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g diff --git a/src/api/ml/build.sed b/src/api/ml/preprocess.sed similarity index 100% rename from src/api/ml/build.sed rename to src/api/ml/preprocess.sed diff --git a/src/api/ml/reverse.sed b/src/api/ml/reverse.sed new file mode 100644 index 000000000..31ac563d2 --- /dev/null +++ b/src/api/ml/reverse.sed @@ -0,0 +1,3 @@ +# output lines of input in reverse order + +1!G;h;$!d diff --git a/src/api/ml/z3.idl b/src/api/ml/z3.0.idl similarity index 98% rename from src/api/ml/z3.idl rename to src/api/ml/z3.0.idl index 555835c88..3773a28e3 100644 --- a/src/api/ml/z3.idl +++ b/src/api/ml/z3.0.idl @@ -91,11 +91,6 @@ quote(c,"#define xstr(s) str(s)"); quote(c,"#define str(s) #s"); -// Suppress "warning C4090: 'function' : different 'const' qualifiers" as -// CamlIDL does not seem to get this right. -quote(c,"#pragma warning(disable:4090)"); - - #ifndef MLAPIV3 #define DEFINE_TYPE(T) typedef [abstract] void* T