mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
broke dependency between components that need initialization and memory_manager
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
570147e326
commit
ed5d154f78
|
@ -378,6 +378,10 @@ class Component:
|
|||
def require_def_file(self):
|
||||
return False
|
||||
|
||||
# Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
|
||||
def require_mem_initializer(self):
|
||||
return False
|
||||
|
||||
def mk_install(self, out):
|
||||
return
|
||||
|
||||
|
@ -490,6 +494,9 @@ class ExeComponent(Component):
|
|||
def require_install_tactics(self):
|
||||
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
|
||||
|
||||
def require_mem_initializer(self):
|
||||
return True
|
||||
|
||||
# All executables are included in the all: rule
|
||||
def main_component(self):
|
||||
return True
|
||||
|
@ -601,6 +608,9 @@ class DLLComponent(Component):
|
|||
def require_install_tactics(self):
|
||||
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
|
||||
|
||||
def require_mem_initializer(self):
|
||||
return True
|
||||
|
||||
def require_def_file(self):
|
||||
return IS_WINDOWS and self.export_files
|
||||
|
||||
|
@ -927,6 +937,7 @@ def mk_auto_src():
|
|||
if not ONLY_MAKEFILES:
|
||||
mk_pat_db()
|
||||
mk_all_install_tactic_cpps()
|
||||
mk_all_mem_initializer_cpps()
|
||||
|
||||
# TODO: delete after src/ast/pattern/expr_pattern_match
|
||||
# database.smt ==> database.h
|
||||
|
@ -1099,6 +1110,60 @@ def mk_all_install_tactic_cpps():
|
|||
cnames.append(c.name)
|
||||
mk_install_tactic_cpp(cnames, c.src_dir)
|
||||
|
||||
# Generate an mem_initializer.cpp at path.
|
||||
# This file implements the procedures
|
||||
# void mem_initialize()
|
||||
# void mem_finalize()
|
||||
# This procedures are invoked by the Z3 memory_manager
|
||||
def mk_mem_initializer_cpp(cnames, path):
|
||||
initializer_cmds = []
|
||||
finalizer_cmds = []
|
||||
fullname = '%s/mem_initializer.cpp' % path
|
||||
fout = open(fullname, 'w')
|
||||
fout.write('// Automatically generated file.\n')
|
||||
initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
|
||||
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
|
||||
for h_file in h_files:
|
||||
added_include = False
|
||||
fin = open("%s/%s" % (c.src_dir, h_file), 'r')
|
||||
for line in fin:
|
||||
m = initializer_pat.match(line)
|
||||
if m:
|
||||
if not added_include:
|
||||
added_include = True
|
||||
fout.write('#include"%s"\n' % h_file)
|
||||
initializer_cmds.append(m.group(1))
|
||||
m = finalizer_pat.match(line)
|
||||
if m:
|
||||
if not added_include:
|
||||
added_include = True
|
||||
fout.write('#include"%s"\n' % h_file)
|
||||
finalizer_cmds.append(m.group(1))
|
||||
fout.write('void mem_initialize() {\n')
|
||||
for cmd in initializer_cmds:
|
||||
fout.write(cmd)
|
||||
fout.write('\n')
|
||||
fout.write('}\n')
|
||||
fout.write('void mem_finalize() {\n')
|
||||
for cmd in finalizer_cmds:
|
||||
fout.write(cmd)
|
||||
fout.write('\n')
|
||||
fout.write('}\n')
|
||||
if VERBOSE:
|
||||
print "Generated '%s'" % fullname
|
||||
|
||||
def mk_all_mem_initializer_cpps():
|
||||
if not ONLY_MAKEFILES:
|
||||
for c in get_components():
|
||||
if c.require_mem_initializer():
|
||||
cnames = []
|
||||
cnames.extend(c.deps)
|
||||
cnames.append(c.name)
|
||||
mk_mem_initializer_cpp(cnames, c.src_dir)
|
||||
|
||||
# Generate a .def based on the files at c.export_files slot.
|
||||
def mk_def_file(c):
|
||||
pat1 = re.compile(".*Z3_API.*")
|
||||
|
|
|
@ -98,6 +98,9 @@ private:
|
|||
};
|
||||
|
||||
void finalize_debug();
|
||||
/*
|
||||
ADD_FINALIZER('finalize_debug();')
|
||||
*/
|
||||
|
||||
#endif /* _DEBUG_H_ */
|
||||
|
||||
|
|
|
@ -1,13 +1,27 @@
|
|||
#include<iostream>
|
||||
#include<stdlib.h>
|
||||
#include"trace.h"
|
||||
#include"memory_manager.h"
|
||||
#include"rational.h"
|
||||
#include"prime_generator.h"
|
||||
#include"debug.h"
|
||||
#include"error_codes.h"
|
||||
|
||||
// The following two function are automatically generated by the mk_make.py script.
|
||||
// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
|
||||
// For example, rational.h contains
|
||||
// ADD_INITIALIZER('rational::initialize();')
|
||||
// ADD_FINALIZER('rational::finalize();')
|
||||
// Thus, any executable or shared object (DLL) that depends on rational.h
|
||||
// will have an automalically generated file mem_initializer.cpp containing
|
||||
// mem_initialize()
|
||||
// mem_finalize()
|
||||
// and these functions will include the statements:
|
||||
// rational::initialize();
|
||||
//
|
||||
// rational::finalize();
|
||||
void mem_initialize();
|
||||
void mem_finalize();
|
||||
|
||||
// If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
|
||||
// #define PROFILE_MEMORY
|
||||
void initialize_symbols();
|
||||
void finalize_symbols();
|
||||
|
||||
out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
|
||||
}
|
||||
|
@ -58,8 +72,7 @@ mem_usage_report g_info;
|
|||
void memory::initialize(size_t max_size) {
|
||||
g_memory_out_of_memory = false;
|
||||
g_memory_max_size = max_size;
|
||||
rational::initialize();
|
||||
initialize_symbols();
|
||||
mem_initialize();
|
||||
}
|
||||
|
||||
bool memory::is_out_of_memory() {
|
||||
|
@ -96,14 +109,9 @@ static bool g_finalizing = false;
|
|||
|
||||
void memory::finalize() {
|
||||
g_finalizing = true;
|
||||
finalize_debug();
|
||||
finalize_trace();
|
||||
finalize_symbols();
|
||||
rational::finalize();
|
||||
prime_iterator::finalize();
|
||||
mem_finalize();
|
||||
}
|
||||
|
||||
|
||||
unsigned long long memory::get_allocation_size() {
|
||||
long long r;
|
||||
#pragma omp critical (z3_memory_manager)
|
||||
|
|
|
@ -48,6 +48,9 @@ public:
|
|||
prime_iterator(prime_generator * g = 0);
|
||||
uint64 next();
|
||||
static void finalize();
|
||||
/*
|
||||
ADD_FINALIZER('prime_iterator::finalize();')
|
||||
*/
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -35,7 +35,10 @@ public:
|
|||
static void initialize();
|
||||
|
||||
static void finalize();
|
||||
|
||||
/*
|
||||
ADD_INITIALIZER('rational::initialize();')
|
||||
ADD_FINALIZER('rational::finalize();')
|
||||
*/
|
||||
rational() {}
|
||||
|
||||
rational(rational const & r) { m().set(m_val, r.m_val); }
|
||||
|
|
|
@ -141,6 +141,10 @@ struct symbol_eq_proc {
|
|||
|
||||
void initialize_symbols();
|
||||
void finalize_symbols();
|
||||
/*
|
||||
ADD_INITIALIZER('initialize_symbols();')
|
||||
ADD_FINALIZER('finalize_symbols();')
|
||||
*/
|
||||
|
||||
// total order on symbols... I did not overloaded '<' to avoid misunderstandings.
|
||||
// numerical symbols are smaller than non numerical symbols.
|
||||
|
|
|
@ -40,6 +40,9 @@ bool is_trace_enabled(const char * tag);
|
|||
void close_trace();
|
||||
void open_trace();
|
||||
void finalize_trace();
|
||||
/*
|
||||
ADD_FINALIZER('finalize_trace();')
|
||||
*/
|
||||
|
||||
#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
|
||||
|
||||
|
|
Loading…
Reference in a new issue