mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
100 lines
3.2 KiB
Python
Executable File
100 lines
3.2 KiB
Python
Executable File
#!/usr/bin/env python3
|
|
# ------------------------------------------------------------------------------
|
|
# This file is part of solidity.
|
|
#
|
|
# solidity is free software: you can redistribute it and/or modify
|
|
# it under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation, either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# solidity is distributed in the hope that it will be useful,
|
|
# but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
# GNU General Public License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with solidity. If not, see <http://www.gnu.org/licenses/>
|
|
#------------------------------------------------------------------------------
|
|
#
|
|
# Script that generates a dlsym-wrapper for Z3 from the header files.
|
|
# Expects all Z3 headers as arguments and outputs the wrapper code to stdout.
|
|
|
|
import sys
|
|
import re
|
|
|
|
# Patterns to match Z3 API entry point definitions.
|
|
def_pat = re.compile(" *def_API(.*)")
|
|
extradef_pat = re.compile(" *extra_API(.*)")
|
|
# Pattern to extract name and arguments from the above.
|
|
def_args_pat = re.compile("\('([^']*)'[^\(\)]*\((.*)\)\s*\)")
|
|
# Pattern to extract a list of arguments from the above.
|
|
arg_list_pat = re.compile("[^\(]*\([^\)]*\)[, ]*")
|
|
|
|
def generateEntryPoint(line, args):
|
|
m = def_args_pat.match(args)
|
|
if not m:
|
|
raise Exception('Could not parse entry point definition: ' + line)
|
|
name = m.group(1)
|
|
num_args = len(arg_list_pat.findall(m.group(2)))
|
|
arglist = ', '.join(f"_{i}" for i in range(num_args))
|
|
paramlist = ', '.join(f"ArgType<&{name}, {i}> _{i}" for i in range(num_args))
|
|
print(f'ResultType<&{name}> Z3_API {name}({paramlist})')
|
|
print('{')
|
|
print(f'\tstatic auto sym = reinterpret_cast<decltype(&{name})>(Z3Loader::get().loadSymbol(\"{name}\"));')
|
|
print(f'\treturn sym({arglist});')
|
|
print('}')
|
|
|
|
|
|
print(r"""// This file is auto-generated from genz3wrapper.py
|
|
#include <libsmtutil/Z3Loader.h>
|
|
#include <tuple>
|
|
#include <z3.h>
|
|
|
|
namespace
|
|
{
|
|
|
|
template<typename T>
|
|
struct FunctionTrait;
|
|
|
|
template<typename R, typename... Args>
|
|
struct FunctionTrait<R(*)(Args...)>
|
|
{
|
|
using ResultType = R;
|
|
template<unsigned N>
|
|
using ArgType = std::tuple_element_t<N, std::tuple<Args...>>;
|
|
};
|
|
|
|
template<auto F>
|
|
using ResultType = typename FunctionTrait<decltype(F)>::ResultType;
|
|
|
|
template<auto F, unsigned N>
|
|
using ArgType = typename FunctionTrait<decltype(F)>::template ArgType<N>;
|
|
|
|
}
|
|
|
|
using namespace solidity;
|
|
using namespace solidity::smtutil;
|
|
|
|
extern "C"
|
|
{
|
|
|
|
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
|
|
{
|
|
static auto sym = reinterpret_cast<decltype(&Z3_set_error_handler)>(Z3Loader::get().loadSymbol("Z3_set_error_handler"));
|
|
sym(c, h);
|
|
}
|
|
""")
|
|
|
|
for header in sys.argv[1:]:
|
|
with open(header, 'r') as f:
|
|
for line in f:
|
|
line = line.strip('\r\n\t ')
|
|
m = def_pat.match(line)
|
|
if m:
|
|
generateEntryPoint(line, m.group(1).strip('\r\n\t '))
|
|
m = extradef_pat.match(line)
|
|
if m:
|
|
generateEntryPoint(line, m.group(1).strip('\r\n\t '))
|
|
|
|
print('}')
|