mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +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 e2f6b10e32
commit 7eb95bf6c2
2 changed files with 38 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

5
scripts/mk_util.py
View file

@ -1440,7 +1440,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)

51
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,8 +1375,7 @@ 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))))
@ -1381,13 +1383,24 @@ def mk_ml():
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