mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	New native ML API layer.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
		
							parent
							
								
									dcd6f1f697
								
							
						
					
					
						commit
						c4f07c7fd1
					
				
					 2 changed files with 289 additions and 147 deletions
				
			
		| 
						 | 
					@ -1428,20 +1428,30 @@ class MLComponent(Component):
 | 
				
			||||||
                if IS_WINDOWS:
 | 
					                if IS_WINDOWS:
 | 
				
			||||||
                    out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
 | 
					                    out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
 | 
				
			||||||
                out.write('\n\n')
 | 
					                out.write('\n\n')
 | 
				
			||||||
 | 
					            deffile = open('%s.mllib' % os.path.join(self.src_dir, "z3"), 'w')
 | 
				
			||||||
 | 
					            for mlfile in get_ml_files(self.src_dir):
 | 
				
			||||||
 | 
					                deffile.write('%s\n' % (string.upper(mlfile[0]) + mlfile[1:-3]))
 | 
				
			||||||
 | 
					            deffile.close()
 | 
				
			||||||
            bld_dir = os.path.join(BUILD_DIR, 'api', 'ml')
 | 
					            bld_dir = os.path.join(BUILD_DIR, 'api', 'ml')
 | 
				
			||||||
            mk_dir(bld_dir)
 | 
					            mk_dir(bld_dir)
 | 
				
			||||||
            libfile = '%s$(LIB_EXT)' % self.lib_name
 | 
					            libfile = '%s$(SO_EXT)' % self.lib_name
 | 
				
			||||||
 | 
					            # for mlfile in get_ml_files(self.src_dir):
 | 
				
			||||||
 | 
					            #     out.write('%si: libz3$(SO_EXT) %s\n' % (os.path.join('api', 'ml', mlfile),os.path.join(self.to_src_dir, mlfile)))
 | 
				
			||||||
 | 
					            #     out.write('\tocamlopt -I %s -i %s > %si\n' % (os.path.join('api', 'ml'), os.path.join(self.to_src_dir, mlfile), os.path.join('api', 'ml', mlfile)))
 | 
				
			||||||
 | 
					            #     out.write('\tocamlopt -I %s -c %si \n' % (os.path.join('api', 'ml'), os.path.join('api','ml', mlfile)))
 | 
				
			||||||
 | 
					            out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'z3native.c')))
 | 
				
			||||||
            for mlfile in get_ml_files(self.src_dir):
 | 
					            for mlfile in get_ml_files(self.src_dir):
 | 
				
			||||||
                out.write('%si: %s\n' % (os.path.join('api', 'ml', mlfile),os.path.join(self.to_src_dir, mlfile)))
 | 
					                out.write(' %s' % os.path.join(self.to_src_dir, mlfile))
 | 
				
			||||||
                out.write('\tocamlopt -I %s -i %s > %si\n' % (os.path.join('api', 'ml'), os.path.join(self.to_src_dir, mlfile), os.path.join('api', 'ml', mlfile)))
 | 
					 | 
				
			||||||
                out.write('\tocamlopt -I %s -c %si \n' % (os.path.join('api', 'ml'), os.path.join('api','ml', mlfile)))
 | 
					 | 
				
			||||||
            out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
 | 
					 | 
				
			||||||
            for mlfile in get_ml_files(self.src_dir):
 | 
					 | 
				
			||||||
                out.write(' %si' % os.path.join('api','ml', mlfile))
 | 
					 | 
				
			||||||
            out.write('\n')
 | 
					            out.write('\n')
 | 
				
			||||||
            out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) -I%s %s/native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
 | 
					            out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT) -I%s %s/z3native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
 | 
				
			||||||
            out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %  os.path.join('api', 'ml', 'native'))
 | 
					            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('ml: %s\n' % libfile)
 | 
					            out.write('z3.cmxa: %s\n' % libfile)
 | 
				
			||||||
 | 
					            out.write('\tcd %s && ocamlbuild -lflags -cclib,../../../%s/libz3ml.so,-cclib,../../../%s/libz3.so -build-dir ../../../%s/api/ml z3.cmxa && cd -\n' % (self.to_src_dir,BUILD_DIR,BUILD_DIR,BUILD_DIR))
 | 
				
			||||||
 | 
					            out.write('\tcp api/ml/z3.cmxa .\n')
 | 
				
			||||||
 | 
					            out.write('z3.cma: %s\n' % libfile)
 | 
				
			||||||
 | 
					            out.write('\tcd %s && ocamlbuild -lflags -custom,-cclib,../../../%s/libz3ml.so,-cclib,../../../%s/libz3.so -build-dir ../../../%s/api/ml z3.cma && cd -\n' % (self.to_src_dir,BUILD_DIR,BUILD_DIR,BUILD_DIR))
 | 
				
			||||||
 | 
					            out.write('\tcp api/ml/z3.cma .\n')
 | 
				
			||||||
 | 
					            out.write('ml: z3.cmxa z3.cma\n')
 | 
				
			||||||
            out.write('\n')
 | 
					            out.write('\n')
 | 
				
			||||||
    
 | 
					    
 | 
				
			||||||
    def main_component(self):
 | 
					    def main_component(self):
 | 
				
			||||||
| 
						 | 
					@ -2728,6 +2738,7 @@ def mk_z3consts_ml(api_files):
 | 
				
			||||||
    if not os.path.exists(gendir):
 | 
					    if not os.path.exists(gendir):
 | 
				
			||||||
        os.mkdir(gendir)
 | 
					        os.mkdir(gendir)
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					<<<<<<< HEAD
 | 
				
			||||||
<<<<<<< HEAD
 | 
					<<<<<<< HEAD
 | 
				
			||||||
<<<<<<< HEAD
 | 
					<<<<<<< HEAD
 | 
				
			||||||
    efile  = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
 | 
					    efile  = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
 | 
				
			||||||
| 
						 | 
					@ -2823,6 +2834,11 @@ def mk_z3consts_ml(api_files):
 | 
				
			||||||
    efile.write('(* Automatically generated file *)\n\n')
 | 
					    efile.write('(* Automatically generated file *)\n\n')
 | 
				
			||||||
    efile.write('module Enumerations = struct\n')
 | 
					    efile.write('module Enumerations = struct\n')
 | 
				
			||||||
>>>>>>> More ML API
 | 
					>>>>>>> More ML API
 | 
				
			||||||
 | 
					=======
 | 
				
			||||||
 | 
					    efile  = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
 | 
				
			||||||
 | 
					    efile.write('(* Automatically generated file *)\n\n')
 | 
				
			||||||
 | 
					    efile.write('module Z3enums = struct\n')
 | 
				
			||||||
 | 
					>>>>>>> New native ML API layer.
 | 
				
			||||||
    for api_file in api_files:
 | 
					    for api_file in api_files:
 | 
				
			||||||
        api_file_c = ml.find_file(api_file, ml.name)
 | 
					        api_file_c = ml.find_file(api_file, ml.name)
 | 
				
			||||||
        api_file   = os.path.join(api_file_c.src_dir, api_file)
 | 
					        api_file   = os.path.join(api_file_c.src_dir, api_file)
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -1073,55 +1073,104 @@ def mk_bindings():
 | 
				
			||||||
def ml_method_name(name):
 | 
					def ml_method_name(name):
 | 
				
			||||||
    return name[3:] # Remove Z3_
 | 
					    return name[3:] # Remove Z3_
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					def is_out_param(p):
 | 
				
			||||||
 | 
					     if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
 | 
				
			||||||
 | 
					         return True
 | 
				
			||||||
 | 
					     else:
 | 
				
			||||||
 | 
					         return False
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					def outparams(params):
 | 
				
			||||||
 | 
					    op = []
 | 
				
			||||||
 | 
					    for param in params:
 | 
				
			||||||
 | 
					        if is_out_param(param):
 | 
				
			||||||
 | 
					            op.append(param)
 | 
				
			||||||
 | 
					    return op
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					def is_in_param(p):
 | 
				
			||||||
 | 
					    if param_kind(p) == IN or param_kind(p) == INOUT or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY:
 | 
				
			||||||
 | 
					        return True
 | 
				
			||||||
 | 
					    else:
 | 
				
			||||||
 | 
					        return False
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					def inparams(params):
 | 
				
			||||||
 | 
					    ip = []
 | 
				
			||||||
 | 
					    for param in params:
 | 
				
			||||||
 | 
					        if is_in_param(param):
 | 
				
			||||||
 | 
					            ip.append(param)
 | 
				
			||||||
 | 
					    return ip
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					def is_array_param(p):
 | 
				
			||||||
 | 
					    if param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_ARRAY:
 | 
				
			||||||
 | 
					        return True
 | 
				
			||||||
 | 
					    else:
 | 
				
			||||||
 | 
					        return False
 | 
				
			||||||
 | 
					
 | 
				
			||||||
def mk_ml():
 | 
					def mk_ml():
 | 
				
			||||||
    if not is_ml_enabled():
 | 
					    if not is_ml_enabled():
 | 
				
			||||||
        return
 | 
					        return
 | 
				
			||||||
    ml_dir      = get_component('ml').src_dir
 | 
					    ml_dir      = get_component('ml').src_dir
 | 
				
			||||||
    ml_nativef  = os.path.join(ml_dir, 'z3.ml')
 | 
					    ml_nativef  = os.path.join(ml_dir, 'z3native.ml')
 | 
				
			||||||
    ml_wrapperf = os.path.join(ml_dir, 'native.c')
 | 
					    ml_wrapperf = os.path.join(ml_dir, 'z3native.c')
 | 
				
			||||||
    ml_native   = open(ml_nativef, 'w')
 | 
					    ml_native   = open(ml_nativef, 'w')
 | 
				
			||||||
    ml_native.write('(* Automatically generated file *)\n\n')
 | 
					    ml_native.write('(* Automatically generated file *)\n\n')
 | 
				
			||||||
    ml_native.write('open Enumerations\n\n')
 | 
					    ml_native.write('open Z3enums\n\n')
 | 
				
			||||||
    ml_native.write('module Z3 = struct\n\n')
 | 
					    ml_native.write('module Z3native = struct\n\n')
 | 
				
			||||||
    ml_native.write('type context\n')
 | 
					    ml_native.write('  type context\n')
 | 
				
			||||||
    ml_native.write('and symbol\n')
 | 
					    ml_native.write('  and symbol\n')
 | 
				
			||||||
    ml_native.write('and ast\n')
 | 
					    ml_native.write('  and ast\n')
 | 
				
			||||||
    ml_native.write('and sort = private ast\n')
 | 
					    ml_native.write('  and sort = private ast\n')
 | 
				
			||||||
    ml_native.write('and func_decl = private ast\n')
 | 
					    ml_native.write('  and func_decl = private ast\n')
 | 
				
			||||||
    ml_native.write('and app = private ast\n')
 | 
					    ml_native.write('  and app = private ast\n')
 | 
				
			||||||
    ml_native.write('and pattern = private ast\n')
 | 
					    ml_native.write('  and pattern = private ast\n')
 | 
				
			||||||
    ml_native.write('and params\n')
 | 
					    ml_native.write('  and params\n')
 | 
				
			||||||
    ml_native.write('and param_descrs\n')
 | 
					    ml_native.write('  and param_descrs\n')
 | 
				
			||||||
    ml_native.write('and model\n')
 | 
					    ml_native.write('  and model\n')
 | 
				
			||||||
    ml_native.write('and func_interp\n')
 | 
					    ml_native.write('  and func_interp\n')
 | 
				
			||||||
    ml_native.write('and func_entry\n')
 | 
					    ml_native.write('  and func_entry\n')
 | 
				
			||||||
    ml_native.write('and fixedpoint\n')
 | 
					    ml_native.write('  and fixedpoint\n')
 | 
				
			||||||
    ml_native.write('and ast_vector\n')
 | 
					    ml_native.write('  and ast_vector\n')
 | 
				
			||||||
    ml_native.write('and ast_map\n')
 | 
					    ml_native.write('  and ast_map\n')
 | 
				
			||||||
    ml_native.write('and goal\n')
 | 
					    ml_native.write('  and goal\n')
 | 
				
			||||||
    ml_native.write('and tactic\n')
 | 
					    ml_native.write('  and tactic\n')
 | 
				
			||||||
    ml_native.write('and probe\n')
 | 
					    ml_native.write('  and probe\n')
 | 
				
			||||||
    ml_native.write('and apply_result\n')
 | 
					    ml_native.write('  and apply_result\n')
 | 
				
			||||||
    ml_native.write('and solver\n')
 | 
					    ml_native.write('  and solver\n')
 | 
				
			||||||
    ml_native.write('and stats\n')
 | 
					    ml_native.write('  and stats\n\n')
 | 
				
			||||||
    ml_native.write('\n')
 | 
					 | 
				
			||||||
    ml_native.write('  exception Exception of string\n\n')
 | 
					    ml_native.write('  exception Exception of string\n\n')
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    # ML declarations
 | 
				
			||||||
 | 
					    ml_native.write('  module ML2C = struct\n\n')
 | 
				
			||||||
    for name, result, params in _dotnet_decls:
 | 
					    for name, result, params in _dotnet_decls:
 | 
				
			||||||
        ml_native.write('    external n_%s : ' % ml_method_name(name))
 | 
					        ml_native.write('    external n_%s : ' % ml_method_name(name))
 | 
				
			||||||
        i = 0;
 | 
					        ip = inparams(params)
 | 
				
			||||||
        for param in params:
 | 
					        op = outparams(params)
 | 
				
			||||||
            ml_native.write('%s -> ' % param2ml(param))
 | 
					        if len(ip) == 0:
 | 
				
			||||||
            i = i + 1
 | 
					 | 
				
			||||||
        if len(params) == 0:
 | 
					 | 
				
			||||||
            ml_native.write(' unit -> ')
 | 
					            ml_native.write(' unit -> ')
 | 
				
			||||||
        ml_native.write('%s\n' % (type2ml(result)))
 | 
					        for p in ip:
 | 
				
			||||||
        ml_native.write('    = "n_%s"\n\n' % ml_method_name(name))
 | 
					            ml_native.write('%s -> ' % param2ml(p))
 | 
				
			||||||
 | 
					        if len(op) > 0:
 | 
				
			||||||
 | 
					            ml_native.write('(')
 | 
				
			||||||
 | 
					        ml_native.write('%s' % type2ml(result))
 | 
				
			||||||
 | 
					        for p in op:
 | 
				
			||||||
 | 
					            ml_native.write(' * %s' % param2ml(p))
 | 
				
			||||||
 | 
					        if len(op) > 0:
 | 
				
			||||||
 | 
					            ml_native.write(')')
 | 
				
			||||||
 | 
					        ml_native.write('\n')
 | 
				
			||||||
 | 
					        ml_native.write('      = "n_%s"\n' % ml_method_name(name))
 | 
				
			||||||
 | 
					        if len(ip) > 5:
 | 
				
			||||||
 | 
					            ml_native.write('        "n_%s_bytecode"\n' % ml_method_name(name))
 | 
				
			||||||
 | 
					        ml_native.write('\n')
 | 
				
			||||||
 | 
					    ml_native.write('  end\n\n')
 | 
				
			||||||
 | 
					
 | 
				
			||||||
    # Exception wrappers
 | 
					    # Exception wrappers
 | 
				
			||||||
    for name, result, params in _dotnet_decls:
 | 
					    for name, result, params in _dotnet_decls:
 | 
				
			||||||
 | 
					        ip = inparams(params)
 | 
				
			||||||
 | 
					        op = outparams(params)
 | 
				
			||||||
        ml_native.write('  let %s ' % ml_method_name(name))
 | 
					        ml_native.write('  let %s ' % ml_method_name(name))
 | 
				
			||||||
        first = True
 | 
					        first = True
 | 
				
			||||||
        i = 0;
 | 
					        i = 0;
 | 
				
			||||||
        for param in params:
 | 
					        for p in params:
 | 
				
			||||||
 | 
					            if is_in_param(p):
 | 
				
			||||||
                if first:
 | 
					                if first:
 | 
				
			||||||
                    first = False;
 | 
					                    first = False;
 | 
				
			||||||
                else:
 | 
					                else:
 | 
				
			||||||
| 
						 | 
					@ -1130,41 +1179,39 @@ def mk_ml():
 | 
				
			||||||
            i = i + 1
 | 
					            i = i + 1
 | 
				
			||||||
        ml_native.write(' = \n')
 | 
					        ml_native.write(' = \n')
 | 
				
			||||||
        ml_native.write('    ')
 | 
					        ml_native.write('    ')
 | 
				
			||||||
        if result != VOID:
 | 
					        if result == VOID:
 | 
				
			||||||
            ml_native.write('let res = ')
 | 
					            ml_native.write('let _ = ')
 | 
				
			||||||
        if len(params) == 0:
 | 
					 | 
				
			||||||
            ml_native.write('n_%s()' % (ml_method_name(name)))
 | 
					 | 
				
			||||||
        else:
 | 
					        else:
 | 
				
			||||||
            ml_native.write('(n_%s ' % (ml_method_name(name)))
 | 
					            ml_native.write('let res = ')
 | 
				
			||||||
 | 
					        ml_native.write('(ML2C.n_%s' % (ml_method_name(name)))
 | 
				
			||||||
        first = True
 | 
					        first = True
 | 
				
			||||||
        i = 0;
 | 
					        i = 0;
 | 
				
			||||||
            for param in params:
 | 
					        for p in params:
 | 
				
			||||||
                if first:
 | 
					            if is_in_param(p):
 | 
				
			||||||
                    first = False
 | 
					                ml_native.write(' a%d' % i)
 | 
				
			||||||
                else:
 | 
					 | 
				
			||||||
                    ml_native.write(' ')
 | 
					 | 
				
			||||||
                ml_native.write('a%d' % i)
 | 
					 | 
				
			||||||
            i = i + 1
 | 
					            i = i + 1
 | 
				
			||||||
            ml_native.write(')')
 | 
					        ml_native.write(') in\n')
 | 
				
			||||||
        if result != VOID:
 | 
					 | 
				
			||||||
            ml_native.write(' in\n')
 | 
					 | 
				
			||||||
        else:
 | 
					 | 
				
			||||||
            ml_native.write(';\n')
 | 
					 | 
				
			||||||
        if len(params) > 0 and param_type(params[0]) == CONTEXT:
 | 
					        if len(params) > 0 and param_type(params[0]) == CONTEXT:
 | 
				
			||||||
            ml_native.write('    let err = (Enumerations.int2error_code (n_get_error_code a0)) in \n')
 | 
					            ml_native.write('    let err = (Z3enums.int2error_code (ML2C.n_get_error_code a0)) in \n')
 | 
				
			||||||
            ml_native.write('      if err <> Enumerations.OK then\n')
 | 
					            ml_native.write('      if err <> Z3enums.OK then\n')
 | 
				
			||||||
            ml_native.write('        raise (Exception (n_get_error_msg_ex a0 (error_code2int err)))\n')
 | 
					            ml_native.write('        raise (Exception (ML2C.n_get_error_msg_ex a0 (Z3enums.error_code2int err)))\n')
 | 
				
			||||||
            ml_native.write('      else\n')
 | 
					            ml_native.write('      else\n')
 | 
				
			||||||
        if result == VOID:
 | 
					        if result == VOID:
 | 
				
			||||||
            ml_native.write('        ()\n')
 | 
					            ml_native.write('        ()\n')
 | 
				
			||||||
        else:
 | 
					        else:
 | 
				
			||||||
            ml_native.write('        res\n')
 | 
					            ml_native.write('        res\n')
 | 
				
			||||||
        ml_native.write('\n')
 | 
					        ml_native.write('\n')
 | 
				
			||||||
    ml_native.write('\nend\n')
 | 
					
 | 
				
			||||||
 | 
					    ml_native.write('end\n')
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    # C interface
 | 
				
			||||||
    ml_wrapper = open(ml_wrapperf, 'w')
 | 
					    ml_wrapper = open(ml_wrapperf, 'w')
 | 
				
			||||||
    ml_wrapper.write('// Automatically generated file\n\n')
 | 
					    ml_wrapper.write('// Automatically generated file\n\n')
 | 
				
			||||||
    ml_wrapper.write('#include <stddef.h>\n')
 | 
					    ml_wrapper.write('#include <stddef.h>\n')
 | 
				
			||||||
    ml_wrapper.write('#include <string.h>\n')
 | 
					    ml_wrapper.write('#include <string.h>\n\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#ifdef __cplusplus\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('extern "C" {\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#endif\n')
 | 
				
			||||||
    ml_wrapper.write('#include <caml/mlvalues.h>\n')
 | 
					    ml_wrapper.write('#include <caml/mlvalues.h>\n')
 | 
				
			||||||
    ml_wrapper.write('#include <caml/memory.h>\n')
 | 
					    ml_wrapper.write('#include <caml/memory.h>\n')
 | 
				
			||||||
    ml_wrapper.write('#include <caml/alloc.h>\n')
 | 
					    ml_wrapper.write('#include <caml/alloc.h>\n')
 | 
				
			||||||
| 
						 | 
					@ -1173,26 +1220,71 @@ def mk_ml():
 | 
				
			||||||
    ml_wrapper.write('#ifdef Custom_tag\n')
 | 
					    ml_wrapper.write('#ifdef Custom_tag\n')
 | 
				
			||||||
    ml_wrapper.write('#include <caml/custom.h>\n')
 | 
					    ml_wrapper.write('#include <caml/custom.h>\n')
 | 
				
			||||||
    ml_wrapper.write('#include <caml/bigarray.h>\n')
 | 
					    ml_wrapper.write('#include <caml/bigarray.h>\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#endif\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#ifdef __cplusplus\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('}\n')
 | 
				
			||||||
    ml_wrapper.write('#endif\n\n')
 | 
					    ml_wrapper.write('#endif\n\n')
 | 
				
			||||||
    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('  CAMLlocal5(X1,X2,X3,X4,X5);                                       \\\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('  CAMLlocal1(X6);                                                     \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('  CAMLlocal2(X6,X7);                                                  \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('  CAMLlocal3(X6,X7,X8);                                               \n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('\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('  CAMLxparam2(X6,X7);                                                 \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('  CAMLxparam3(X6,X7,X8);                                              \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('  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('  CAMLparam5(X1,X2,X3,X4,X5);                                       \\\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('  CAMLxparam5(X6,X7,X8,X9,X10);                                     \\\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('  CAMLparam5(X1,X2,X3,X4,X5);                                       \\\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('  CAMLxparam5(X6,X7,X8,X9,X10);                                     \\\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('  CAMLxparam3(X11,X12,X13);                                           \n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('\n\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#ifdef __cplusplus\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('extern "C" {\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#endif\n\n')
 | 
				
			||||||
    for name, result, params in _dotnet_decls:
 | 
					    for name, result, params in _dotnet_decls:
 | 
				
			||||||
        #return type = type2ml(result)
 | 
					        ip = inparams(params)
 | 
				
			||||||
 | 
					        op = outparams(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)) 
 | 
					        ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name)) 
 | 
				
			||||||
        first = True
 | 
					        first = True
 | 
				
			||||||
        i = 0
 | 
					        i = 0
 | 
				
			||||||
        for param in params:
 | 
					        for p in params:
 | 
				
			||||||
 | 
					            if is_in_param(p):
 | 
				
			||||||
                if first:
 | 
					                if first:
 | 
				
			||||||
                    first = False
 | 
					                    first = False
 | 
				
			||||||
                else:                
 | 
					                else:                
 | 
				
			||||||
                    ml_wrapper.write(', ')
 | 
					                    ml_wrapper.write(', ')
 | 
				
			||||||
                ml_wrapper.write('value a%d' % i)
 | 
					                ml_wrapper.write('value a%d' % i)
 | 
				
			||||||
            # param type = param2ml(param)
 | 
					 | 
				
			||||||
            i = i + 1
 | 
					            i = i + 1
 | 
				
			||||||
        ml_wrapper.write(') {\n')
 | 
					        ml_wrapper.write(') {\n')
 | 
				
			||||||
        ml_wrapper.write('  CAMLparam%d(' % len(params))
 | 
					        ml_wrapper.write('  CAMLparam%d(' % len(ip))
 | 
				
			||||||
        i = 0
 | 
					        i = 0
 | 
				
			||||||
        first = True
 | 
					        first = True
 | 
				
			||||||
        for param in params:
 | 
					        for p in params:
 | 
				
			||||||
 | 
					            if is_in_param(p):
 | 
				
			||||||
                if first:
 | 
					                if first:
 | 
				
			||||||
                    first = False
 | 
					                    first = False
 | 
				
			||||||
                else:
 | 
					                else:
 | 
				
			||||||
| 
						 | 
					@ -1200,34 +1292,47 @@ def mk_ml():
 | 
				
			||||||
                ml_wrapper.write('a%d' % i)
 | 
					                ml_wrapper.write('a%d' % i)
 | 
				
			||||||
            i = i + 1
 | 
					            i = i + 1
 | 
				
			||||||
        ml_wrapper.write(');\n')
 | 
					        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
 | 
				
			||||||
 | 
					            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)
 | 
				
			||||||
 | 
					                i = i + 1
 | 
				
			||||||
 | 
					            ml_wrapper.write(');\n')
 | 
				
			||||||
 | 
					
 | 
				
			||||||
        # preprocess arrays, strings, in/out arguments
 | 
					        # preprocess arrays, strings, in/out arguments
 | 
				
			||||||
        i = 0
 | 
					        i = 0
 | 
				
			||||||
        for param in params:
 | 
					        for param in params:
 | 
				
			||||||
            k = param_kind(param)
 | 
					            if param_kind(param) == OUT_ARRAY:
 | 
				
			||||||
            if k == OUT or k == INOUT:
 | 
					                ml_wrapper.write('  _a%s = (long) malloc(sizeof(%s) * ((long)a%s));\n' % (i, 
 | 
				
			||||||
                ml_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
 | 
					 | 
				
			||||||
            elif k == IN_ARRAY or k == INOUT_ARRAY:
 | 
					 | 
				
			||||||
                if param_type(param) == INT or param_type(param) == UINT:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
 | 
					 | 
				
			||||||
                else:                    
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
 | 
					 | 
				
			||||||
            elif k == OUT_ARRAY:
 | 
					 | 
				
			||||||
                ml_wrapper.write('  %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), 
 | 
					 | 
				
			||||||
                                                                                                     i, 
 | 
					 | 
				
			||||||
                                                                                          type2str(param_type(param)),
 | 
					                                                                                          type2str(param_type(param)),
 | 
				
			||||||
                                                                                                     param_array_capacity_pos(param), 
 | 
					                                                                                          param_array_capacity_pos(param)))
 | 
				
			||||||
                                                                                                     type2str(param_type(param))))
 | 
					            elif param_kind(param) == IN and param_type(param) == STRING:
 | 
				
			||||||
                if param_type(param) == INT or param_type(param) == UINT:
 | 
					                ml_wrapper.write('  _a%s = (value) String_val(a%s);\n' % (i, i))
 | 
				
			||||||
                    ml_wrapper.write('  jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
 | 
					 | 
				
			||||||
                else:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
 | 
					 | 
				
			||||||
            elif k == IN and param_type(param) == STRING:
 | 
					 | 
				
			||||||
                ml_wrapper.write('  Z3_string _a%s = (Z3_string) String_val(a%s);\n' % (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 result = ' % type2str(result))
 | 
					            ml_wrapper.write('result = (value) ')
 | 
				
			||||||
        ml_wrapper.write('%s(' % name)
 | 
					        ml_wrapper.write('%s(' % name)
 | 
				
			||||||
        i = 0
 | 
					        i = 0
 | 
				
			||||||
        first = True
 | 
					        first = True
 | 
				
			||||||
| 
						 | 
					@ -1238,53 +1343,74 @@ def mk_ml():
 | 
				
			||||||
                ml_wrapper.write(', ')
 | 
					                ml_wrapper.write(', ')
 | 
				
			||||||
            k = param_kind(param)
 | 
					            k = param_kind(param)
 | 
				
			||||||
            if k == OUT or k == INOUT:
 | 
					            if k == OUT or k == INOUT:
 | 
				
			||||||
                ml_wrapper.write('&_a%s' % i)
 | 
					                ml_wrapper.write('(%s)&_a%s' % (param2str(param), i))
 | 
				
			||||||
            elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
 | 
					            elif k == INOUT_ARRAY or k == IN_ARRAY:
 | 
				
			||||||
                ml_wrapper.write('_a%s' % i)
 | 
					                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:
 | 
					            elif k == IN and param_type(param) == STRING:
 | 
				
			||||||
                ml_wrapper.write('_a%s' % i)
 | 
					                ml_wrapper.write('(Z3_string) _a%s' % i)
 | 
				
			||||||
            else:
 | 
					            else:
 | 
				
			||||||
                ml_wrapper.write('(%s)a%i' % (param2str(param), i))
 | 
					                ml_wrapper.write('(%s)a%i' % (param2str(param), i))
 | 
				
			||||||
            i = i + 1
 | 
					            i = i + 1
 | 
				
			||||||
        ml_wrapper.write(');\n')
 | 
					        ml_wrapper.write(');\n')
 | 
				
			||||||
        # cleanup 
 | 
					 | 
				
			||||||
        i = 0
 | 
					 | 
				
			||||||
        for param in params:
 | 
					 | 
				
			||||||
            k = param_kind(param)
 | 
					 | 
				
			||||||
            if k == OUT_ARRAY:
 | 
					 | 
				
			||||||
                if param_type(param) == INT or param_type(param) == UINT:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
 | 
					 | 
				
			||||||
                else:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
 | 
					 | 
				
			||||||
                ml_wrapper.write('  free(_a%s);\n' % i)
 | 
					 | 
				
			||||||
            elif k == IN_ARRAY or k == OUT_ARRAY:
 | 
					 | 
				
			||||||
                if param_type(param) == INT or param_type(param) == UINT:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
 | 
					 | 
				
			||||||
                else:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
            elif k == OUT or k == INOUT:
 | 
					        # return tuples                
 | 
				
			||||||
                if param_type(param) == INT or param_type(param) == UINT:
 | 
					        if len(op) > 0:
 | 
				
			||||||
                    ml_wrapper.write('  {\n')
 | 
					            ml_wrapper.write('  result_tuple = caml_alloc(%s, 0);\n' % ret_size)
 | 
				
			||||||
                    ml_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
 | 
					            i = j = 0
 | 
				
			||||||
                    ml_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
 | 
					            if result != VOID:
 | 
				
			||||||
                    ml_wrapper.write('     jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  }\n')
 | 
					 | 
				
			||||||
                else:
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  {\n')
 | 
					 | 
				
			||||||
                    ml_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
 | 
					 | 
				
			||||||
                    ml_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
 | 
					 | 
				
			||||||
                    ml_wrapper.write('     jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
 | 
					 | 
				
			||||||
                    ml_wrapper.write('  }\n')
 | 
					 | 
				
			||||||
            i = i + 1
 | 
					 | 
				
			||||||
        # return
 | 
					 | 
				
			||||||
                if result == STRING:
 | 
					                if result == STRING:
 | 
				
			||||||
            ml_wrapper.write('  return caml_copy_string(result);\n')
 | 
					                    ml_wrapper.write('  Store_field(result_tuple, 0, caml_copy_string(result));\n')
 | 
				
			||||||
 | 
					                else:
 | 
				
			||||||
 | 
					                    ml_wrapper.write('  Store_field(result_tuple, 0, result);\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))
 | 
				
			||||||
 | 
					                    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)
 | 
				
			||||||
 | 
					            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:
 | 
					            elif result == VOID:
 | 
				
			||||||
                ml_wrapper.write('  CAMLreturn(Val_unit);\n')
 | 
					                ml_wrapper.write('  CAMLreturn(Val_unit);\n')
 | 
				
			||||||
            elif result != VOID:
 | 
					            elif result != VOID:
 | 
				
			||||||
            ml_wrapper.write('  return (value) result;\n')
 | 
					                ml_wrapper.write('  CAMLreturn(result);\n')
 | 
				
			||||||
 | 
					
 | 
				
			||||||
        ml_wrapper.write('}\n\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)) 
 | 
				
			||||||
 | 
					            ml_wrapper.write('  return n_%s(' % ml_method_name(name))
 | 
				
			||||||
 | 
					            i = 0
 | 
				
			||||||
 | 
					            while i < len(ip):
 | 
				
			||||||
 | 
					                if i == 0:
 | 
				
			||||||
 | 
					                    ml_wrapper.write('argv[0]')
 | 
				
			||||||
 | 
					                else:
 | 
				
			||||||
 | 
					                    ml_wrapper.write(', argv[%s]' % i)
 | 
				
			||||||
 | 
					                i = i + 1
 | 
				
			||||||
 | 
					            ml_wrapper.write(');\n}\n')
 | 
				
			||||||
 | 
					            ml_wrapper.write('\n\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#ifdef __cplusplus\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('}\n')
 | 
				
			||||||
 | 
					    ml_wrapper.write('#endif\n')
 | 
				
			||||||
    if is_verbose():
 | 
					    if is_verbose():
 | 
				
			||||||
        print "Generated '%s'" % ml_nativef
 | 
					        print "Generated '%s'" % ml_nativef
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue