Skip to content

Commit

Permalink
Update Bitwuzla to 0.4.0
Browse files Browse the repository at this point in the history
  • Loading branch information
khang06 committed Mar 18, 2024
1 parent 924bcbb commit 550c8e4
Show file tree
Hide file tree
Showing 9 changed files with 81 additions and 76 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/codecov.yml
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ jobs:
run: |
git clone https://github.com/bitwuzla/bitwuzla.git
cd bitwuzla
git checkout -b 0.2.0 0.2.0
git checkout -b 0.4.0 0.4.0
python ./configure.py --shared
cd build
sudo ninja install
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/linux.yml
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ jobs:
run: |
git clone https://github.com/bitwuzla/bitwuzla.git
cd bitwuzla
git checkout -b 0.2.0 0.2.0
git checkout -b 0.4.0 0.4.0
python ./configure.py --shared
cd build
sudo ninja install
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/osx.yml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ jobs:
run: |
git clone https://github.com/bitwuzla/bitwuzla.git
cd bitwuzla
git checkout -b 0.2.0 0.2.0
git checkout -b 0.4.0 0.4.0
python ./configure.py --shared --prefix $(pwd)/install
cd build
sudo ninja install
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/python.yml
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ jobs:
run: |
git clone https://github.com/bitwuzla/bitwuzla.git
cd bitwuzla
git checkout -b 0.2.0 0.2.0
git checkout -b 0.4.0 0.4.0
python ./configure.py --shared --prefix $(pwd)/install
cd build
sudo ninja install
Expand Down
4 changes: 2 additions & 2 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@ RUN cd /tmp && \
tar xvf cap.tgz && cd capstone-4.0.2/ && ./make.sh && make install && rm -rf /tmp/cap* \
&& ln -s /usr/lib/libcapstone.so.4 /usr/lib/x86_64-linux-gnu/libcapstone.so

# libbitwuzla >= 0.2.0
# libbitwuzla >= 0.4.0
RUN cd /tmp && \
git clone https://github.com/bitwuzla/bitwuzla.git && \
cd bitwuzla && \
git checkout -b 0.2.0 0.2.0 && \
git checkout -b 0.4.0 0.4.0 && \
python3 ./configure.py --shared && \
cd build && \
ninja install && \
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ Triton relies on the following dependencies:
* libboost (optional) >= 1.68
* libpython (optional) >= 3.6
* libz3 (optional) >= 4.6.0 https://github.com/Z3Prover/z3
* libbitwuzla (optional) >= 0.2.x https://github.com/bitwuzla/bitwuzla
* libbitwuzla (optional) >= 0.4.x https://github.com/bitwuzla/bitwuzla
* llvm (optional) >= 12
```

Expand Down
125 changes: 63 additions & 62 deletions src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -61,174 +61,175 @@ namespace triton {
children.emplace_back(this->translatedNodes.at(n));
}

BitwuzlaTermManager* tm = bitwuzla_get_term_mgr(bzla);
switch (node->getType()) {

case ARRAY_NODE: {
auto size = triton::ast::getInteger<triton::uint32>(node->getChildren()[0]);
auto isort = bitwuzla_mk_bv_sort(size); // index sort
auto vsort = bitwuzla_mk_bv_sort(8); // value sort
auto asort = bitwuzla_mk_array_sort(isort, vsort); // array sort
auto value = bitwuzla_mk_bv_value_uint64(vsort, 0); // const value
return bitwuzla_mk_const_array(asort, value);
auto isort = bitwuzla_mk_bv_sort(tm, size); // index sort
auto vsort = bitwuzla_mk_bv_sort(tm, 8); // value sort
auto asort = bitwuzla_mk_array_sort(tm, isort, vsort); // array sort
auto value = bitwuzla_mk_bv_value_uint64(tm, vsort, 0); // const value
return bitwuzla_mk_const_array(tm, asort, value);
}

case BSWAP_NODE: {
auto bvsize = node->getBitvectorSize();
auto bvsort = bitwuzla_mk_bv_sort(bvsize);
auto retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND, children[0], bitwuzla_mk_bv_value_uint64(bvsort, 0xff));
auto bvsort = bitwuzla_mk_bv_sort(tm, bvsize);
auto retval = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_AND, children[0], bitwuzla_mk_bv_value_uint64(tm, bvsort, 0xff));
for (triton::uint32 index = 8 ; index != bvsize ; index += triton::bitsize::byte) {
retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHL, retval, bitwuzla_mk_bv_value_uint64(bvsort, 8));
retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_OR, retval,
bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND,
bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHR, children[0], bitwuzla_mk_bv_value_uint64(bvsort, index)),
bitwuzla_mk_bv_value_uint64(bvsort, 0xff)
retval = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SHL, retval, bitwuzla_mk_bv_value_uint64(tm, bvsort, 8));
retval = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_OR, retval,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_AND,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SHR, children[0], bitwuzla_mk_bv_value_uint64(tm, bvsort, index)),
bitwuzla_mk_bv_value_uint64(tm, bvsort, 0xff)
)
);
}
return retval;
}

case BVADD_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ADD, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, children[0], children[1]);

case BVAND_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_AND, children[0], children[1]);

case BVASHR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ASHR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ASHR, children[0], children[1]);

case BVLSHR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SHR, children[0], children[1]);

case BVMUL_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_MUL, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, children[0], children[1]);

case BVNAND_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_NAND, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_NAND, children[0], children[1]);

case BVNEG_NODE:
return bitwuzla_mk_term1(BITWUZLA_KIND_BV_NEG, children[0]);
return bitwuzla_mk_term1(tm, BITWUZLA_KIND_BV_NEG, children[0]);

case BVNOR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_NOR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_NOR, children[0], children[1]);

case BVNOT_NODE:
return bitwuzla_mk_term1(BITWUZLA_KIND_BV_NOT, children[0]);
return bitwuzla_mk_term1(tm, BITWUZLA_KIND_BV_NOT, children[0]);

case BVOR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_OR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_OR, children[0], children[1]);

case BVROL_NODE: {
auto childNodes = node->getChildren();
auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_ROLI, children[0], idx);
return bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_ROLI, children[0], idx);
}

case BVROR_NODE: {
auto childNodes = node->getChildren();
auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_RORI, children[0], idx);
return bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_RORI, children[0], idx);
}

case BVSDIV_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SDIV, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SDIV, children[0], children[1]);

case BVSGE_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SGE, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SGE, children[0], children[1]);

case BVSGT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SGT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SGT, children[0], children[1]);

case BVSHL_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHL, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SHL, children[0], children[1]);

case BVSLE_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SLE, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SLE, children[0], children[1]);

case BVSLT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SLT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SLT, children[0], children[1]);

case BVSMOD_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SMOD, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SMOD, children[0], children[1]);

case BVSREM_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SREM, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SREM, children[0], children[1]);

case BVSUB_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SUB, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SUB, children[0], children[1]);

case BVUDIV_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UDIV, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_UDIV, children[0], children[1]);

case BVUGE_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UGE, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_UGE, children[0], children[1]);

case BVUGT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UGT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_UGT, children[0], children[1]);

case BVULE_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ULE, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ULE, children[0], children[1]);

case BVULT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ULT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ULT, children[0], children[1]);

case BVUREM_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UREM, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_UREM, children[0], children[1]);

case BVXNOR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_XNOR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_XNOR, children[0], children[1]);

case BVXOR_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_BV_XOR, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_XOR, children[0], children[1]);

case BV_NODE: {
auto childNodes = node->getChildren();
auto bv_size = triton::ast::getInteger<triton::usize>(childNodes[1]);
auto sort = this->bvSorts.find(bv_size);
if (sort == this->bvSorts.end()) {
sort = this->bvSorts.insert({bv_size, bitwuzla_mk_bv_sort(bv_size)}).first;
sort = this->bvSorts.insert({bv_size, bitwuzla_mk_bv_sort(tm, bv_size)}).first;
}

// Handle bitvector value as integer if it small enough.
if (bv_size <= sizeof(uint64_t) * 8) {
auto bv_value = triton::ast::getInteger<triton::uint64>(childNodes[0]);
return bitwuzla_mk_bv_value_uint64(sort->second, bv_value);
return bitwuzla_mk_bv_value_uint64(tm, sort->second, bv_value);
}

auto bv_value = triton::ast::getInteger<std::string>(childNodes[0]);
return bitwuzla_mk_bv_value(sort->second, bv_value.c_str(), 10);
return bitwuzla_mk_bv_value(tm, sort->second, bv_value.c_str(), 10);
}

case CONCAT_NODE:
return bitwuzla_mk_term(BITWUZLA_KIND_BV_CONCAT, children.size(), children.data());
return bitwuzla_mk_term(tm, BITWUZLA_KIND_BV_CONCAT, children.size(), children.data());

case DISTINCT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_DISTINCT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_DISTINCT, children[0], children[1]);

case EQUAL_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_EQUAL, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, children[0], children[1]);

case EXTRACT_NODE: {
auto childNodes = node->getChildren();
auto high = triton::ast::getInteger<triton::usize>(childNodes[0]);
auto low = triton::ast::getInteger<triton::usize>(childNodes[1]);
return bitwuzla_mk_term1_indexed2(BITWUZLA_KIND_BV_EXTRACT, children[2], high, low);
return bitwuzla_mk_term1_indexed2(tm, BITWUZLA_KIND_BV_EXTRACT, children[2], high, low);
}

case FORALL_NODE:
throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062).");

case IFF_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_IFF, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_IFF, children[0], children[1]);

case INTEGER_NODE:
return (BitwuzlaTerm) 0;

case ITE_NODE:
return bitwuzla_mk_term3(BITWUZLA_KIND_ITE, children[0], children[1], children[2]);
return bitwuzla_mk_term3(tm, BITWUZLA_KIND_ITE, children[0], children[1], children[2]);

case LAND_NODE:
return bitwuzla_mk_term(BITWUZLA_KIND_AND, children.size(), children.data());
return bitwuzla_mk_term(tm, BITWUZLA_KIND_AND, children.size(), children.data());

case LET_NODE: {
auto childNodes = node->getChildren();
Expand All @@ -237,24 +238,24 @@ namespace triton {
}

case LNOT_NODE:
return bitwuzla_mk_term1(BITWUZLA_KIND_NOT, children[0]);
return bitwuzla_mk_term1(tm, BITWUZLA_KIND_NOT, children[0]);

case LOR_NODE:
return bitwuzla_mk_term(BITWUZLA_KIND_OR, children.size(), children.data());
return bitwuzla_mk_term(tm, BITWUZLA_KIND_OR, children.size(), children.data());

case LXOR_NODE:
return bitwuzla_mk_term(BITWUZLA_KIND_XOR, children.size(), children.data());
return bitwuzla_mk_term(tm, BITWUZLA_KIND_XOR, children.size(), children.data());

case REFERENCE_NODE: {
auto ref = reinterpret_cast<ReferenceNode*>(node.get())->getSymbolicExpression()->getAst();
return this->translatedNodes.at(ref);
}

case SELECT_NODE:
return bitwuzla_mk_term2(BITWUZLA_KIND_ARRAY_SELECT, children[0], children[1]);
return bitwuzla_mk_term2(tm, BITWUZLA_KIND_ARRAY_SELECT, children[0], children[1]);

case STORE_NODE:
return bitwuzla_mk_term3(BITWUZLA_KIND_ARRAY_STORE, children[0], children[1], children[2]);
return bitwuzla_mk_term3(tm, BITWUZLA_KIND_ARRAY_STORE, children[0], children[1], children[2]);

case STRING_NODE: {
std::string value = reinterpret_cast<triton::ast::StringNode*>(node.get())->getString();
Expand All @@ -269,24 +270,24 @@ namespace triton {
case SX_NODE: {
auto childNodes = node->getChildren();
auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_SIGN_EXTEND, children[1], ext);
return bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_SIGN_EXTEND, children[1], ext);
}

case VARIABLE_NODE: {
const auto& symVar = reinterpret_cast<VariableNode*>(node.get())->getSymbolicVariable();
auto size = symVar->getSize();
auto sort = this->bvSorts.find(size);
if (sort == this->bvSorts.end()) {
sort = this->bvSorts.insert({size, bitwuzla_mk_bv_sort(size)}).first;
sort = this->bvSorts.insert({size, bitwuzla_mk_bv_sort(tm, size)}).first;
}

// If the conversion is used to evaluate a node, we concretize symbolic variables.
if (this->isEval) {
triton::uint512 value = reinterpret_cast<triton::ast::VariableNode*>(node.get())->evaluate();
if (size <= sizeof(uint64_t) * 8) {
return bitwuzla_mk_bv_value_uint64(sort->second, static_cast<uint64_t>(value));
return bitwuzla_mk_bv_value_uint64(tm, sort->second, static_cast<uint64_t>(value));
}
return bitwuzla_mk_bv_value(sort->second, triton::utils::toString(value).c_str(), 10);
return bitwuzla_mk_bv_value(tm, sort->second, triton::utils::toString(value).c_str(), 10);
}

auto n = (BitwuzlaTerm) 0;
Expand All @@ -299,7 +300,7 @@ namespace triton {
}

if (n == 0) {
n = bitwuzla_mk_const(sort->second, symVar->getName().c_str());
n = bitwuzla_mk_const(tm, sort->second, symVar->getName().c_str());
variables[n] = symVar;
}

Expand All @@ -309,7 +310,7 @@ namespace triton {
case ZX_NODE: {
auto childNodes = node->getChildren();
auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_ZERO_EXTEND,children[1], ext);
return bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_ZERO_EXTEND,children[1], ext);
}

default:
Expand Down
Loading

0 comments on commit 550c8e4

Please sign in to comment.