From d8ed9be98e9224b9abfc37d90b1ea7879b35a3f0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Dec 2012 03:02:12 +0000 Subject: [PATCH] ML native layer bugfixes Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 2 +- scripts/update_api.py | 165 +++++++++++++++++++++++++----------------- src/api/ml/z3.ml | 120 +++++++++++++++++------------- 3 files changed, 171 insertions(+), 116 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a0f123609..e44c120cb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2888,7 +2888,7 @@ def mk_z3consts_ml(api_files): linenum = linenum + 1 efile.write('end\n') if VERBOSE: - print "Generated '%s/enumerations.ml'" % ('%s' % gendir) + print "Generated '%s/z3enums.ml'" % ('%s' % gendir) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index 25adce2af..d0ef2ec86 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,3 +1,4 @@ + ############################################ # Copyright (c) 2012 Microsoft Corporation # @@ -1097,6 +1098,45 @@ def is_array_param(p): else: return False +def arrayparams(params): + op = [] + for param in params: + if is_array_param(param): + op.append(param) + return op + + +def ml_unwrap(t): + if t == STRING: + return 'String_val' + elif t == BOOL or t == INT or PRINT_MODE or ERROR_CODE: + return 'Int_val' + elif t == UINT: + return 'Unsigned_int_val' + elif t == INT64: + return 'Long_val' + elif t == UINT64: + return 'Unsigned_long_val' + elif t == DOUBLE: + return 'Double_val' + else: + return 'Data_custom_val' + +def ml_set_wrap(t, d, n): + if t == VOID: + return d + ' = Val_unit;' + elif t == BOOL or t == INT or t == UINT or PRINT_MODE or ERROR_CODE: + return d + ' = Val_int(' + n + ');' + elif t == INT64 or t == UINT64: + return d + ' = Val_long(' + n + ');' + elif t == DOUBLE: + return 'Store_double_val(' + d + ', ' + n + ');' + elif t == STRING: + return d + ' = caml_copy_string((const char*) ' + n + ');' + else: + ts = type2str(t) + return d + ' = caml_alloc_custom(0, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));' + def mk_ml(): global Type2Str if not is_ml_enabled(): @@ -1242,15 +1282,12 @@ def mk_ml(): for name, result, params in _dotnet_decls: ip = inparams(params) op = outparams(params) + ap = arrayparams(params) ret_size = len(op) if result != VOID: ret_size = ret_size + 1 # Setup frame - n_locals = 0 - for p in params: - if is_out_param(p) or (is_in_param(p) and param_type(p) == STRING): - n_locals = n_locals + 1 ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name)) first = True i = 0 @@ -1276,46 +1313,50 @@ def mk_ml(): i = i + 1 ml_wrapper.write(');\n') i = 0 - first = True - if result != VOID: - n_locals = n_locals + 1 - if ret_size > 1: - n_locals = n_locals + 1 - if n_locals > 0: - ml_wrapper.write(' CAMLlocal%s(' % (n_locals)) - if ret_size > 1: - if result != VOID: - ml_wrapper.write('result, ') - ml_wrapper.write('result_tuple') - first = False - elif result != VOID: - ml_wrapper.write('result') - first = False + if len(op) + len(ap) == 0: + ml_wrapper.write(' CAMLlocal1(result);\n') + else: + c = 0 for p in params: - if is_out_param(p) or (is_in_param(p) and param_type(p) == STRING): - if first: - first = False - else: - ml_wrapper.write(', ') - ml_wrapper.write('_a%s' % i) + if is_out_param(p) or is_array_param(p): + c = c + 1 + ml_wrapper.write(' CAMLlocal%s(result, res_val' % (c+2)) + for p in params: + if is_out_param(p) or is_array_param(p): + ml_wrapper.write(', _a%s_val' % i) i = i + 1 ml_wrapper.write(');\n') # preprocess arrays, strings, in/out arguments i = 0 for param in params: - if param_kind(param) == OUT_ARRAY: - ml_wrapper.write(' _a%s = (long) malloc(sizeof(%s) * ((long)a%s));\n' % (i, - type2str(param_type(param)), - param_array_capacity_pos(param))) - elif param_kind(param) == IN and param_type(param) == STRING: - ml_wrapper.write(' _a%s = (value) String_val(a%s);\n' % (i, i)) + k = param_kind(param) + if k == OUT_ARRAY: + ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( + type2str(param_type(param)), + i, + type2str(param_type(param)), + type2str(param_type(param)), + param_array_capacity_pos(param))) + elif k == IN_ARRAY or k == INOUT_ARRAY: + t = param_type(param) + 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(' for (unsigned i = 0; i < a%s; i++) _a%s[i] = (%s) %s(Field(a%s, i));\n' % (param_array_capacity_pos(param), i, ts, ml_unwrap(t), i)) + elif k == IN: + t = param_type(param) + ml_wrapper.write(' %s _a%s = (%s) %s(a%s);\n' % (type2str(t), i, type2str(t), ml_unwrap(t), i)) + elif k == OUT: + ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) + elif k == INOUT: + ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i)) + i = i + 1 # invoke procedure ml_wrapper.write(' ') if result != VOID: - ml_wrapper.write('result = (value) ') + ml_wrapper.write('%s z3_result = ' % type2str(result)) ml_wrapper.write('%s(' % name) i = 0 first = True @@ -1326,58 +1367,50 @@ def mk_ml(): ml_wrapper.write(', ') k = param_kind(param) if k == OUT or k == INOUT: - ml_wrapper.write('(%s)&_a%s' % (param2str(param), i)) - elif k == INOUT_ARRAY or k == IN_ARRAY: - ml_wrapper.write('(%s*)a%s' % (type2str(param_type(param)), i)) - elif k == OUT_ARRAY: - ml_wrapper.write('(%s*)_a%s' % (type2str(param_type(param)), i)) - elif k == IN and param_type(param) == STRING: - ml_wrapper.write('(Z3_string) _a%s' % i) + ml_wrapper.write('&_a%s' % i) else: - ml_wrapper.write('(%s)a%i' % (param2str(param), i)) + ml_wrapper.write('_a%i' % i) i = i + 1 ml_wrapper.write(');\n') - # return tuples + # convert output params if len(op) > 0: - ml_wrapper.write(' result_tuple = caml_alloc(%s, 0);\n' % ret_size) + if result != VOID: + ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result")) + i = 0; + for p in params: + 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(' 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)) + elif is_out_param(p): + ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) )) + i = i + 1 + + # return tuples + if len(op) == 0: + ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3_result")) + else: + ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size) i = j = 0 if result != VOID: - if result == STRING: - ml_wrapper.write(' Store_field(result_tuple, 0, caml_copy_string(result));\n') - else: - ml_wrapper.write(' Store_field(result_tuple, 0, result);\n') + ml_wrapper.write(' Store_field(result, 0, res_val);\n') j = j + 1 for p in params: - if param_kind(p) == OUT_ARRAY or param_kind(p) == OUT: - ml_wrapper.write(' Store_field(result_tuple, %s, _a%s);\n' % (j, i)) - j = j + 1; - elif is_out_param(p): - if param_type(p) == STRING: - ml_wrapper.write(' Store_field(result_tuple, %s, caml_copy_string((const char *)_a%s));\n' % (j, i)) - else: - ml_wrapper.write(' Store_field(result_tuple, %s, a%s);\n' % (j, i)) + if is_out_param(p): + ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i)) j = j + 1; i = i + 1 # local array cleanup i = 0 for p in params: - if param_kind(p) == OUT_ARRAY: - ml_wrapper.write(' free((long*)_a%s);\n' % i) + k = param_kind(p) + if k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: + ml_wrapper.write(' free(_a%s);\n' % i) i = i + 1 # return - if len(op) > 0: - ml_wrapper.write(' CAMLreturn(result_tuple);\n') - else: - if result == STRING: - ml_wrapper.write(' CAMLreturn(caml_copy_string((const char*) result));\n') - elif result == VOID: - ml_wrapper.write(' CAMLreturn(Val_unit);\n') - elif result != VOID: - ml_wrapper.write(' CAMLreturn(result);\n') - + ml_wrapper.write(' CAMLreturn(result);\n') ml_wrapper.write('}\n\n') if len(ip) > 5: ml_wrapper.write('CAMLprim value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name)) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 4f847bc48..d1ba2b746 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -10,11 +10,25 @@ module Log = struct let m_is_open = false (* CMW: "open" seems to be an invalid function name*) - let open_ fn = int2lbool(open_log fn) == L_TRUE - let close = (close_log) - let append s = (append_log s) + let open_ fn = ((int2lbool (open_log fn)) == L_TRUE) + let close = close_log + let append s = append_log s end - + +module Version = +struct + let major = let (x, _, _, _) = get_version in x + let minor = let (_, x, _, _) = get_version in x + let build = let (_, _, x, _) = get_version in x + let revision = let (_, _, _, x) = get_version in x + let to_string = + let (mj, mn, bld, rev) = get_version in + string_of_int mj ^ "." ^ + string_of_int mn ^ "." ^ + string_of_int bld ^ "." ^ + string_of_int rev ^ "." +end + class virtual idisposable = object method virtual dispose : unit @@ -25,7 +39,7 @@ object (self) inherit idisposable val mutable m_n_ctx : Z3native.z3_context = - let cfg = mk_config() in + let cfg = mk_config in let f e = (set_param_value cfg (fst e) (snd e)) in (List.iter f settings) ; let v = mk_context_rc cfg in @@ -34,14 +48,15 @@ object (self) val mutable m_refCount : int = 0 - initializer Gc.finalise (fun self -> self#dispose) self + initializer + Gc.finalise (fun self -> self#dispose) self method dispose : unit = if m_refCount == 0 then ( - Printf.printf "Disposing %d \n" (Oo.id self) ; + Printf.printf "Disposing context %d \n" (Oo.id self) ; (del_context m_n_ctx) ) else ( - (* re-queue for finalization? *) + (* re-queue for finalization? *) ) method sub_one_ctx_obj = m_refCount <- m_refCount - 1 @@ -66,9 +81,9 @@ object (self) method virtual incref : Z3native.ptr -> unit method virtual decref : Z3native.ptr -> unit - (* - Disposes of the underlying native Z3 object. - *) + (* + Disposes of the underlying native Z3 object. + *) method dispose = Printf.printf "Disposing z3object %d \n" (Oo.id self) ; (match m_n_obj with @@ -92,16 +107,17 @@ object (self) method get_context = m_ctx method get_native_context = m_ctx#get_native - (* - method array_to_native a = +(* + method array_to_native a = let f e = e#get_native_object in (Array.map f a) - method array_length a = + method array_length a = match a with - | Some(x) -> (Array.length x) - | None -> 0 - *) + | Some(x) -> (Array.length x) + | None -> 0 +*) + end class symbol ctx_init obj_init = @@ -110,49 +126,55 @@ object (self) method incref o = () method decref o = () +end - method kind = match m_n_obj with - | Some(x) -> (int2symbol_kind (get_symbol_kind self#get_native_context x)) - | _ -> raise (Exception "Underlying object lost") +class int_symbol ctx_init obj_init = +object(self) + inherit symbol ctx_init obj_init +end - method is_int_symbol = match m_n_obj with - | Some(x) -> self#kind == INT_SYMBOL - | _ -> false +class string_symbol ctx_init obj_init = +object(self) + inherit symbol ctx_init obj_init +end - method is_string_symbol = match m_n_obj with - | Some(x) -> self#kind == STRING_SYMBOL - | _ -> false - - method to_string = match m_n_obj with - | Some(x) -> - ( - match self#kind with - | INT_SYMBOL -> (string_of_int (get_symbol_int self#get_native_context x)) - | STRING_SYMBOL -> (get_symbol_string self#get_native_context x) - ) - | None -> "" - - method create ctx obj = +module Symbol = +struct + let create ctx obj = match obj with | Some(x) -> ( match (int2symbol_kind (get_symbol_kind ctx#get_native x)) with - | INT_SYMBOL -> (new intsymbol ctx obj :> symbol) - | STRING_SYMBOL -> (new stringsymbol ctx obj :> symbol) + | INT_SYMBOL -> (new int_symbol ctx obj :> symbol) + | STRING_SYMBOL -> (new string_symbol ctx obj :> symbol) ) | None -> raise (Exception "Can't create null objects") -end + let kind o = match o#m_n_obj with + | Some(x) -> (int2symbol_kind (get_symbol_kind o#get_native_context x)) + | _ -> raise (Exception "Underlying object lost") -and intsymbol ctx_init obj_init = -object(self) - inherit symbol ctx_init obj_init + let is_int_symbol o = match o#m_n_obj with + | Some(x) -> x#kind == INT_SYMBOL + | _ -> false - method get_int = match m_n_obj with - | Some(x) -> (get_symbol_int m_ctx#get_native x) + let is_string_symbol o = match o#m_n_obj with + | Some(x) -> x#kind == STRING_SYMBOL + | _ -> false + + let get_int o = match o#m_n_obj with + | Some(x) -> (get_symbol_int o#get_native_context x) | None -> 0 -end -and stringsymbol ctx_init obj_init = -object(self) - inherit symbol ctx_init obj_init + let get_string o = match o#m_n_obj with + | Some(x) -> (get_symbol_string o#get_native_context x) + | None -> "" + + let to_string o = match o#m_n_obj with + | Some(x) -> + ( + match (kind o) with + | INT_SYMBOL -> (string_of_int (get_symbol_int o#get_native_context x)) + | STRING_SYMBOL -> (get_symbol_string o#get_native_context x) + ) + | None -> "" end