Skip to content

Commit

Permalink
Merge pull request #583 from wintersteiger/new-ml-api
Browse files Browse the repository at this point in the history 
Lots of OCaml API bugfixes/improvements courtesy of @martin-neuhaeusser
  • Loading branch information
Christoph M. Wintersteiger committed May 3, 2016
2 parents 6895cc7 + 107f50d commit cf34a2b
Show file tree
Hide file tree
Showing 8 changed files with 2,949 additions and 3,482 deletions.
7 changes: 4 additions & 3 deletions examples/ml/ml_example.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,9 +190,10 @@ let basic_tests ( ctx : context ) =
(* Error handling test. *)
try (
let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException (numeral_to_string i)) (* unreachable *)
Printf.printf "%s\n" (Expr.to_string i) ;
raise (TestFailedException "check")
)
with Z3native.Exception(_) -> (
with Z3.Error(_) -> (
Printf.printf "Exception caught, OK.\n"
)

Expand Down Expand Up @@ -342,7 +343,7 @@ let _ =
);
Printf.printf "Exiting.\n" ;
exit 0
) with Z3native.Exception(msg) -> (
) with Error(msg) -> (
Printf.printf "Z3 EXCEPTION: %s\n" msg ;
exit 1
)
Expand Down
2 changes: 0 additions & 2 deletions scripts/mk_make.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,5 +19,3 @@
mk_vs_proj('z3', ['shell'])
mk_vs_proj_dll('libz3', ['api_dll'])
mk_makefile()


219 changes: 121 additions & 98 deletions scripts/mk_util.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ def getenv(name, default):
IS_OSX=False
IS_FREEBSD=False
IS_OPENBSD=False
IS_CYGWIN=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
Expand Down Expand Up @@ -139,6 +140,9 @@ def is_openbsd():
def is_osx():
return IS_OSX

def is_cygwin():
return IS_CYGWIN

def norm_path(p):
# We use '/' on mk_project for convenience
return os.path.join(*(p.split('/')))
Expand Down Expand Up @@ -591,6 +595,8 @@ def check_eol():
IS_FREEBSD=True
elif os.uname()[0] == 'OpenBSD':
IS_OPENBSD=True
elif os.uname()[0][:6] == 'CYGWIN':
IS_CYGWIN=True

def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
Expand Down Expand Up @@ -1691,6 +1697,8 @@ def mk_makefile(self, out):
t = t.replace('PLATFORM', 'freebsd')
elif IS_OPENBSD:
t = t.replace('PLATFORM', 'openbsd')
elif IS_CYGWIN:
t = t.replace('PLATFORM', 'cygwin')
else:
t = t.replace('PLATFORM', 'win32')
out.write(t)
Expand Down Expand Up @@ -1808,6 +1816,16 @@ def final_info(self):

def mk_makefile(self, out):
if is_ml_enabled():
CP_CMD = 'cp'
if IS_WINDOWS:
CP_CMD='copy'

OCAML_FLAGS = ''
if DEBUG_MODE:
OCAML_FLAGS += '-g'
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS

src_dir = self.to_src_dir
mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir
Expand All @@ -1824,51 +1842,52 @@ def mk_makefile(self, out):
os.path.join(BUILD_DIR, self.sub_dir, 'META'),
substitutions)

mlis = ''
for m in self.modules:
mlis = os.path.join(src_dir, m) + '.mli ' + mlis

stubsc = os.path.join(src_dir, self.stubs + '.c')
stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)'
out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso))
out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
(OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc))

cmis = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.mli')
ft = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s\n' % (ft, cmis))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmis = cmis + ' ' + ft
(OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))

cmos = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmo')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmos = cmos + ' ' + ft
ml = os.path.join(src_dir, m + '.ml')
cmo = os.path.join(self.sub_dir, m + '.cmo')
existing_mli = os.path.join(src_dir, m + '.mli')
mli = os.path.join(self.sub_dir, m + '.mli')
cmi = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (cmo, ml, cmos))
if (os.path.exists(existing_mli[3:])):
out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
else:
out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml))
cmos = cmos + cmo + ' '

cmxs = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmx')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPT, self.sub_dir, ft, ff))
out.write('%s: %s %s\n' % (ft, ff, cmos))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
cmxs = cmxs + ' ' + ft


OCAMLMKLIB = 'ocamlmklib'
LIBZ3 = '-L. -lz3'
if is_cygwin():
# Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
LIBZ3 = 'libz3.dll'
elif DEBUG_MODE:
OCAMLMKLIB += ' -g'
z3mls = os.path.join(self.sub_dir, 'z3ml')
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmos))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmxs))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPT, z3mls, self.sub_dir, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))

out.write('\n')
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
Expand Down Expand Up @@ -1911,7 +1930,11 @@ def mk_install(self, out):
metafile=os.path.join(self.sub_dir, 'META')))

for m in self.modules:
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
mli = os.path.join(self.src_dir, m) + '.mli'
if os.path.exists(mli):
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
else:
out.write(' ' + os.path.join(self.sub_dir, m) + '.mli')
out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx')
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
Expand Down Expand Up @@ -2863,78 +2886,78 @@ def mk_z3consts_ml(api_files):
efile.close()
if VERBOSE:
print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n')
for api_file in api_files:
api_file_c = ml.find_file(api_file, ml.name)
api_file = os.path.join(api_file_c.src_dir, api_file)

api = open(api_file, 'r')

SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2

mode = SEARCHING
decls = {}
idx = 0

linenum = 1
for line in api:
m1 = blank_pat.match(line)
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
mode = FOUND_ENUM
m = typedef2_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
elif mode == FOUND_ENUM:
m = openbrace_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
else:
assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
assert mode == IN_ENUM
words = re.split('[^\-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line)
if m:
name = words[1]
if name not in DeprecatedEnums:
efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.items():
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])
efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
efile.write('(** Convert int to %s*)\n' % name[3:])
efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
efile.write('\n')
mode = SEARCHING
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
idx = int(words[2], 16)
else:
idx = int(words[2])
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
api.close()
efile.close()
if VERBOSE:
print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
# efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
# efile.write('(* Automatically generated file *)\n\n')
# efile.write('(** The enumeration types of Z3. *)\n\n')
# for api_file in api_files:
# api_file_c = ml.find_file(api_file, ml.name)
# api_file = os.path.join(api_file_c.src_dir, api_file)

# api = open(api_file, 'r')

# SEARCHING = 0
# FOUND_ENUM = 1
# IN_ENUM = 2

# mode = SEARCHING
# decls = {}
# idx = 0

# linenum = 1
# for line in api:
# m1 = blank_pat.match(line)
# m2 = comment_pat.match(line)
# if m1 or m2:
# # skip blank lines and comments
# linenum = linenum + 1
# elif mode == SEARCHING:
# m = typedef_pat.match(line)
# if m:
# mode = FOUND_ENUM
# m = typedef2_pat.match(line)
# if m:
# mode = IN_ENUM
# decls = {}
# idx = 0
# elif mode == FOUND_ENUM:
# m = openbrace_pat.match(line)
# if m:
# mode = IN_ENUM
# decls = {}
# idx = 0
# else:
# assert False, "Invalid %s, line: %s" % (api_file, linenum)
# else:
# assert mode == IN_ENUM
# words = re.split('[^\-a-zA-Z0-9_]+', line)
# m = closebrace_pat.match(line)
# if m:
# name = words[1]
# if name not in DeprecatedEnums:
# efile.write('(** %s *)\n' % name[3:])
# efile.write('type %s =\n' % name[3:]) # strip Z3_
# for k, i in decls.items():
# efile.write(' | %s \n' % k[3:]) # strip Z3_
# efile.write('\n')
# efile.write('(** Convert %s to int*)\n' % name[3:])
# efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
# efile.write('(** Convert int to %s*)\n' % name[3:])
# efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
# efile.write('\n')
# mode = SEARCHING
# else:
# if words[2] != '':
# if len(words[2]) > 1 and words[2][1] == 'x':
# idx = int(words[2], 16)
# else:
# idx = int(words[2])
# decls[words[1]] = idx
# idx = idx + 1
# linenum = linenum + 1
# api.close()
# efile.close()
# if VERBOSE:
# print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))

def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id
Expand Down
Loading

0 comments on commit cf34a2b

Please sign in to comment.