mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

ML API: made native layer ANSI-C compliant to avoid compilation issues.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-01-07 15:32:25 +00:00
parent 597409c8ac
commit d0591334a2
2 changed files with 41 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

12
scripts/mk_util.py
View file

@ -345,21 +345,20 @@ def check_ml():
t.commit() t.commit()
if is_verbose(): if is_verbose():
print "Testing %s..." % OCAMLC print "Testing %s..." % OCAMLC
r = exec_cmd([OCAMLC, 'hello.ml']) r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
if r != 0: if r != 0:
raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler') raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
if is_verbose(): if is_verbose():
print "Testing %s..." % OCAMLOPT print "Testing %s..." % OCAMLOPT
r = exec_cmd([OCAMLC, 'hello.ml']) r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
if r != 0: if r != 0:
raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler') raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler')
os.remove('hello.cmi') os.remove('hello.cmi')
os.remove('hello.cmo') os.remove('hello.cmo')
os.remove('a.out') os.remove('a.out')
r = exec_cmd([OCAMLBUILD]) r = exec_cmd([OCAMLBUILD, '-version'])
if r != 0: if r != 0:
raise MKException('Failed testing ocamlbuild. Set environment variable OCAMLBUILD with the path to ocamlbuild') raise MKException('Failed testing ocamlbuild. Set environment variable OCAMLBUILD with the path to ocamlbuild')
shutil.rmtree('_build')
find_ml_lib() find_ml_lib()
def find_ml_lib(): def find_ml_lib():
@ -1350,7 +1349,10 @@ class MLComponent(Component):
out.write(' %s' % os.path.join(self.to_src_dir, mlfile)) out.write(' %s' % os.path.join(self.to_src_dir, mlfile))
out.write('\n') out.write('\n')
out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT) -I%s -I%s %s/z3native.c\n' % (get_component(API_COMPONENT).to_src_dir, OCAML_LIB, self.to_src_dir)) out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT) -I%s -I%s %s/z3native.c\n' % (get_component(API_COMPONENT).to_src_dir, OCAML_LIB, self.to_src_dir))
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % (libfile, os.path.join('api', 'ml', 'z3native'))) if WINDOWS:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % (libfile, os.path.join('api', 'ml', 'z3native')))
else:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % (libfile, os.path.join('api', 'ml', 'z3native')))
out.write('z3.cmxa: %s\n' % libfile) out.write('z3.cmxa: %s\n' % libfile)
out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3.cmxa z3native$(OBJ_EXT) && cd -\n' % (self.to_src_dir,BUILD_DIR)) out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3.cmxa z3native$(OBJ_EXT) && cd -\n' % (self.to_src_dir,BUILD_DIR))
out.write('z3.cma: %s\n' % libfile) out.write('z3.cma: %s\n' % libfile)

55
scripts/update_api.py
View file

@ -1262,39 +1262,39 @@ def mk_ml():
ml_wrapper.write('#include <z3.h>\n\n') ml_wrapper.write('#include <z3.h>\n\n')
ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n') ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal1(X6); \n') ml_wrapper.write(' CAMLlocal1(X6) \n')
ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n') ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal2(X6,X7); \n') ml_wrapper.write(' CAMLlocal2(X6,X7) \n')
ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal3(X6,X7,X8); \n') ml_wrapper.write(' CAMLlocal3(X6,X7,X8) \n')
ml_wrapper.write('\n') ml_wrapper.write('\n')
ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n') ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam2(X6,X7); \n') ml_wrapper.write(' CAMLxparam2(X6,X7) \n')
ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam3(X6,X7,X8); \n') ml_wrapper.write(' CAMLxparam3(X6,X7,X8) \n')
ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n') ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9); \n') ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9) \n')
ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n') ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam2(X11,X12); \n') ml_wrapper.write(' CAMLxparam2(X11,X12) \n')
ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n') ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam3(X11,X12,X13); \n') ml_wrapper.write(' CAMLxparam3(X11,X12,X13) \n')
ml_wrapper.write('\n\n') ml_wrapper.write('\n\n')
ml_wrapper.write('static struct custom_operations default_custom_ops = {\n') ml_wrapper.write('static struct custom_operations default_custom_ops = {\n')
ml_wrapper.write(' identifier: (char*) "default handling",\n') ml_wrapper.write(' (char*) "default handling",\n')
ml_wrapper.write(' finalize: custom_finalize_default,\n') ml_wrapper.write(' custom_finalize_default,\n')
ml_wrapper.write(' compare: custom_compare_default,\n') ml_wrapper.write(' custom_compare_default,\n')
ml_wrapper.write(' hash: custom_hash_default,\n') ml_wrapper.write(' custom_hash_default,\n')
ml_wrapper.write(' serialize: custom_serialize_default,\n') ml_wrapper.write(' custom_serialize_default,\n')
ml_wrapper.write(' deserialize: custom_deserialize_default\n') ml_wrapper.write(' custom_deserialize_default\n')
ml_wrapper.write('};\n\n') ml_wrapper.write('};\n\n')
ml_wrapper.write('#ifdef __cplusplus\n') ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n') ml_wrapper.write('extern "C" {\n')
@ -1358,7 +1358,10 @@ def mk_ml():
i = i + 1 i = i + 1
ml_wrapper.write(');\n') ml_wrapper.write(');\n')
# preprocess arrays, strings, in/out arguments if len(ap) != 0:
ml_wrapper.write(' unsigned _i;\n')
# declare locals, preprocess arrays, strings, in/out arguments
i = 0 i = 0
for param in params: for param in params:
k = param_kind(param) k = param_kind(param)
@ -1372,22 +1375,32 @@ def mk_ml():
elif k == IN_ARRAY or k == INOUT_ARRAY: elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param) t = param_type(param)
ts = type2str(t) ts = type2str(t)
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param))) ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
ml_wrapper.write(' for (unsigned i = 0; i < _a%s; i++) _a%s[i] = %s;\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', i)')))
elif k == IN: elif k == IN:
t = param_type(param) t = param_type(param)
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i)))) ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
elif k == OUT: elif k == OUT:
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == INOUT: elif k == INOUT:
ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i)) ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
i = i + 1
if result != VOID:
ml_wrapper.write(' %s z3_result;\n' % type2str(result))
i = 0
for param in params:
k = param_kind(param)
if k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { _a%s[_i] = %s; }\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)')))
i = i + 1 i = i + 1
# invoke procedure # invoke procedure
ml_wrapper.write(' ') ml_wrapper.write(' ')
if result != VOID: if result != VOID:
ml_wrapper.write('%s z3_result = ' % type2str(result)) ml_wrapper.write('z3_result = ')
ml_wrapper.write('%s(' % name) ml_wrapper.write('%s(' % name)
i = 0 i = 0
first = True first = True
@ -1412,7 +1425,7 @@ def mk_ml():
for p in params: for p in params:
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY: if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p))) ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
ml_wrapper.write(' for (unsigned i = 0; i < _a%s; i++) { value t; %s Store_field(_a%s, i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[i]'), i)) ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i))
elif is_out_param(p): elif is_out_param(p):
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) )) ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
i = i + 1 i = i + 1