From 4e42a987f9b8fde1e4e98e4ae2a43bf6ee73f27a Mon Sep 17 00:00:00 2001 From: Igor Skochinsky Date: Tue, 24 Jan 2023 16:22:09 +0100 Subject: [PATCH] Initial commit Initial public release --- BUILDING.md | 40 +++++ README.md | 52 ++++++ bitwise_expr_lookup_tbl.cpp | 168 ++++++++++++++++++ bitwise_expr_lookup_tbl.hpp | 43 +++++ consts.hpp | 27 +++ equiv_class.cpp | 104 +++++++++++ equiv_class.hpp | 303 ++++++++++++++++++++++++++++++++ file.cpp | 212 +++++++++++++++++++++++ file.hpp | 18 ++ generate_oracle.bat | 25 +++ generate_oracle.sh | 13 ++ goomba.cfg | 17 ++ goomba.cpp | 260 ++++++++++++++++++++++++++++ heuristics.cpp | 130 ++++++++++++++ heuristics.hpp | 83 +++++++++ images/mba1_after.png | Bin 0 -> 7636 bytes images/mba1_before.png | Bin 0 -> 17511 bytes lin_conj_exprs.hpp | 297 +++++++++++++++++++++++++++++++ linear_exprs.cpp | 149 ++++++++++++++++ linear_exprs.hpp | 81 +++++++++ makefile | 139 +++++++++++++++ mba.cfg | 17 ++ mcode_emu.hpp | 337 ++++++++++++++++++++++++++++++++++++ minsn_template.hpp | 163 +++++++++++++++++ msynth_parser.cpp | 128 ++++++++++++++ msynth_parser.hpp | 99 +++++++++++ optimizer.cpp | 174 +++++++++++++++++++ optimizer.hpp | 35 ++++ simp_lin_conj_exprs.hpp | 311 +++++++++++++++++++++++++++++++++ smt_convert.cpp | 167 ++++++++++++++++++ smt_convert.hpp | 83 +++++++++ tests/idb/mba_challenge.i64 | Bin 0 -> 19642 bytes tests/idb/nonlinear.o.i64 | Bin 0 -> 9434 bytes z3++_no_warn.h | 10 ++ z3/readme.txt | 5 + 35 files changed, 3690 insertions(+) create mode 100644 BUILDING.md create mode 100644 README.md create mode 100644 bitwise_expr_lookup_tbl.cpp create mode 100644 bitwise_expr_lookup_tbl.hpp create mode 100644 consts.hpp create mode 100644 equiv_class.cpp create mode 100644 equiv_class.hpp create mode 100644 file.cpp create mode 100644 file.hpp create mode 100644 generate_oracle.bat create mode 100644 generate_oracle.sh create mode 100644 goomba.cfg create mode 100644 goomba.cpp create mode 100644 heuristics.cpp create mode 100644 heuristics.hpp create mode 100644 images/mba1_after.png create mode 100644 images/mba1_before.png create mode 100644 lin_conj_exprs.hpp create mode 100644 linear_exprs.cpp create mode 100644 linear_exprs.hpp create mode 100644 makefile create mode 100644 mba.cfg create mode 100644 mcode_emu.hpp create mode 100644 minsn_template.hpp create mode 100644 msynth_parser.cpp create mode 100644 msynth_parser.hpp create mode 100644 optimizer.cpp create mode 100644 optimizer.hpp create mode 100644 simp_lin_conj_exprs.hpp create mode 100644 smt_convert.cpp create mode 100644 smt_convert.hpp create mode 100644 tests/idb/mba_challenge.i64 create mode 100644 tests/idb/nonlinear.o.i64 create mode 100644 z3++_no_warn.h create mode 100644 z3/readme.txt diff --git a/BUILDING.md b/BUILDING.md new file mode 100644 index 0000000..4c561bb --- /dev/null +++ b/BUILDING.md @@ -0,0 +1,40 @@ + +# Bulding gooMBA + +## dependencies + +gooMBA requires IDA SDK (8.2 or later) and the [z3 library](https://github.com/Z3Prover/z3). + +## Building + +1. After unpacking and setting up the SDK, copy goomba source tree under SDK's `plugins` directory, +for example `C:\idasdk_pro82\plugins\goomba`. + +2. Download and extract [z3 build for your OS](https://github.com/Z3Prover/z3/releases) into the `z3` subdirectory, for example: + +`z3/z3-4.11.2-x64-win` + + Under it, you should have `bin` and `include` directories + + Alternatively, set `Z3_BIN` and `Z3_INCLUDE` to point to the directories elsewhere. + +3. If using another `z3` version than 4.11.2, open `makefile` and adjust + + * `Z3VER` with the correct version number + * possibly, `Z3BIN` with the correct glibc version number (on Linux), + or osx version number (on macOS) + +4. build the necessary version of gooMBA, for example: + +```make -j``` for 32-bit IDA +```make __EA64__=1 -j``` for IDA64 + +5. Copy generated files from SDK's bin directory to your IDA install (or [user directory](https://hex-rays.com/blog/igors-tip-of-the-week-33-idas-user-directory-idausr/)): + + * `C:\idasdk_pro82\bin\plugins\goomba*` -> `C:\Program Files\IDA Pro 8.2\plugins\` + * `C:\idasdk_pro82\bin\cfg\goomba.cfg` -> `C:\Program Files\IDA Pro 8.2\cfg\` + * `C:\idasdk_pro82\bin\libz3.*` -> `C:\Program Files\IDA Pro 8.2\` + + + + diff --git a/README.md b/README.md new file mode 100644 index 0000000..e869152 --- /dev/null +++ b/README.md @@ -0,0 +1,52 @@ +# gooMBA + +gooMBA is a Hex-Rays Decompiler plugin that simplifies Mixed Boolean-Arithmetic +(MBA) expressions. It achieves this using several heuristics and algorithms to +achieve orders-of-magnitude better performance than existing state-of-the-art +solutions. + +More information on the inner workings of this tool is available in our [blog +post](https://hex-rays.com/blog/deobfuscation-with-goomba/). + +## Core Features +- Full integration with the Hex-Rays Decompiler +- Simplifies linear MBAs, including opaque predicates +- Handles sign extension for linear functions +- Verifies soundness of simplifications using the z3 SMT solver +- Simplifies non-linear MBAs with the use of a function fingerprint oracle + +## Usage + +By default, the plugin does not run automatically. You can invoke the plugin +by right clicking in the pseudocode view and selecting "Run gooMBA Optimizer". +In addition, you can set up a keyboard shortcut in IDA by opening Options -> +Shortcuts... and adding a shortcut for the `goomba:run` action. + +Several options for usage are available within `goomba.cfg`. You can set up a +fingerprint oracle, configure the z3 proof timeout time, choose the desired behavior when +timeouts occur, and choose to make the plugin run automatically without needing +to be invoked from the right-click menu. + +## Demo + +The sample database `tests/idb/mba_challenge.i64` was created from the `mba_challenge` binary. The functions +`mba1`, `mba2`, `mba3`, `mba`, `solve_me` contain MBA expressions of varying complexity. + +For example, the `mba1` function's initial pseudocode: +![mba1 initial pseudocode](./images/mba1_before.png) + +And after running gooMBA optimization: +![mba1 pseudocode optimized](./images/mba1_after.png) + + +## Fingerprint oracle + +The oracle can be used for simplifying non-linear MBAs. +The input for generaring it is a list of candidate expressions in [msynth](https://github.com/mrphrazer/msynth) syntax. +You can use `generate_oracle.sh` or `generate_oracle.bat` to generate a binary +oracle file which can then be used by the plugin by specifying the path to it +in `goomba.cfg` (parameter `MBA_ORACLE_PATH`). + +A large pre-computed oracle is available [here](https://hex-rays.com/products/ida/support/freefiles/goomba-oracle.7z) + +NOTE: oracle files generated with IDA 8.2 can only be used with 64-bit binaries, otherwise you may hit internal error 30661. diff --git a/bitwise_expr_lookup_tbl.cpp b/bitwise_expr_lookup_tbl.cpp new file mode 100644 index 0000000..0361b7d --- /dev/null +++ b/bitwise_expr_lookup_tbl.cpp @@ -0,0 +1,168 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "bitwise_expr_lookup_tbl.hpp" + +bw_expr_tbl_t bw_expr_tbl_t::instance; + +bw_expr_tbl_t::bw_expr_tbl_t() +{ + minsn_templates_t X; + X.push_back(std::make_shared(0)); + X.push_back(std::make_shared(1)); + X.push_back(std::make_shared(2)); + + minsn_template_ptr_t zero = std::make_shared(0ull); + + // note that all expressions are ordered by the numeric value of the instruction trace + // see lin_conj_exprs.hpp for more info on ordering. + auto &onevar = tbl.push_back(); + onevar.push_back(zero); // [0 0] + onevar.push_back(X[0]); // [0 1] + + auto &twovar = tbl.push_back(); + twovar.push_back(zero); // [0 0 0 0] + twovar.push_back(X[0]&~X[1]); // [0 1 0 0] + twovar.push_back(~(X[0]|~X[1])); // [0 0 1 0] + twovar.push_back(X[0]^X[1]); // [0 1 1 0] + twovar.push_back(X[0]&X[1]); // [0 0 0 1] + twovar.push_back(X[0]); // [0 1 0 1] + twovar.push_back(X[1]); // [0 0 1 1] + twovar.push_back(X[0]|X[1]); // [0 1 1 1] + + auto &threevar = tbl.push_back(); + threevar.push_back(zero); // [0 0 0 0 0 0 0 0] + threevar.push_back(~(~X[0]|(X[1]|X[2]))); // [0 1 0 0 0 0 0 0] + threevar.push_back(~(X[0]|(~X[1]|X[2]))); // [0 0 1 0 0 0 0 0] + threevar.push_back(~X[2]&(X[0]^X[1])); // [0 1 1 0 0 0 0 0] + threevar.push_back(~(~X[0]|(~X[1]|X[2]))); // [0 0 0 1 0 0 0 0] + threevar.push_back(X[0]&~X[2]); // [0 1 0 1 0 0 0 0] + threevar.push_back(X[1]&~X[2]); // [0 0 1 1 0 0 0 0] + threevar.push_back(X[2]^(X[0]|(X[1]|X[2]))); // [0 1 1 1 0 0 0 0] + threevar.push_back(~X[0]&(~X[1]&X[2])); // [0 0 0 0 1 0 0 0] + threevar.push_back(~X[1]&(X[0]^X[2])); // [0 1 0 0 1 0 0 0] + threevar.push_back(~X[0]&(X[1]^X[2])); // [0 0 1 0 1 0 0 0] + threevar.push_back(~(X[0]&X[1])&(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 0 0 0] + threevar.push_back(~(X[0]^X[1])&(X[0]^X[2])); // [0 0 0 1 1 0 0 0] + threevar.push_back(X[2]^(X[0]|(X[1]&X[2]))); // [0 1 0 1 1 0 0 0] + threevar.push_back(~(X[0]&~X[1])&(X[1]^X[2])); // [0 0 1 1 1 0 0 0] + threevar.push_back(X[2]^(X[0]|X[1])); // [0 1 1 1 1 0 0 0] + threevar.push_back(X[0]&(~X[1]&X[2])); // [0 0 0 0 0 1 0 0] + threevar.push_back(X[0]&~X[1]); // [0 1 0 0 0 1 0 0] + threevar.push_back((X[0]^X[1])&~(X[0]^X[2])); // [0 0 1 0 0 1 0 0] + threevar.push_back(X[1]^(X[0]|(X[1]&X[2]))); // [0 1 1 0 0 1 0 0] + threevar.push_back(X[0]&(X[1]^X[2])); // [0 0 0 1 0 1 0 0] + threevar.push_back(~(~X[0]|(X[1]&X[2]))); // [0 1 0 1 0 1 0 0] + threevar.push_back((X[0]|X[1])&(X[1]^X[2])); // [0 0 1 1 0 1 0 0] + threevar.push_back((X[0]&X[1])^~(X[0]^(~X[1]|X[2]))); // [0 1 1 1 0 1 0 0] + threevar.push_back(~(X[1]|~X[2])); // [0 0 0 0 1 1 0 0] + threevar.push_back(X[1]^(X[0]|(X[1]|X[2]))); // [0 1 0 0 1 1 0 0] + threevar.push_back(~(X[0]&X[1])&(X[1]^X[2])); // [0 0 1 0 1 1 0 0] + threevar.push_back(X[1]^(X[0]|X[2])); // [0 1 1 0 1 1 0 0] + threevar.push_back((X[0]|~X[1])&(X[1]^X[2])); // [0 0 0 1 1 1 0 0] + threevar.push_back((X[0]&X[2])^(X[0]^(~X[1]&X[2]))); // [0 1 0 1 1 1 0 0] + threevar.push_back(X[1]^X[2]); // [0 0 1 1 1 1 0 0] + threevar.push_back((X[0]&~X[1])|(X[1]^X[2])); // [0 1 1 1 1 1 0 0] + threevar.push_back(~X[0]&(X[1]&X[2])); // [0 0 0 0 0 0 1 0] + threevar.push_back((X[0]^X[1])&(X[0]^X[2])); // [0 1 0 0 0 0 1 0] + threevar.push_back(~(X[0]|~X[1])); // [0 0 1 0 0 0 1 0] + threevar.push_back(X[1]^~(~X[0]|(~X[1]&X[2]))); // [0 1 1 0 0 0 1 0] + threevar.push_back(X[1]&(X[0]^X[2])); // [0 0 0 1 0 0 1 0] + threevar.push_back(X[2]^(X[0]|(~X[1]&X[2]))); // [0 1 0 1 0 0 1 0] + threevar.push_back(X[1]&~(X[0]&X[2])); // [0 0 1 1 0 0 1 0] + threevar.push_back(X[1]^~(~X[0]|(X[1]^X[2]))); // [0 1 1 1 0 0 1 0] + threevar.push_back(~(X[0]|~X[2])); // [0 0 0 0 1 0 1 0] + threevar.push_back(X[2]^(X[0]&(~X[1]|X[2]))); // [0 1 0 0 1 0 1 0] + threevar.push_back(~X[0]&(X[1]|X[2])); // [0 0 1 0 1 0 1 0] + threevar.push_back(X[0]^(X[1]|X[2])); // [0 1 1 0 1 0 1 0] + threevar.push_back(X[2]^(X[0]&(X[1]|X[2]))); // [0 0 0 1 1 0 1 0] + threevar.push_back(X[0]^X[2]); // [0 1 0 1 1 0 1 0] + threevar.push_back((X[0]&X[2])^(X[1]|X[2])); // [0 0 1 1 1 0 1 0] + threevar.push_back(X[2]^~(~X[0]&(~X[1]|X[2]))); // [0 1 1 1 1 0 1 0] + threevar.push_back(X[2]&(X[0]^X[1])); // [0 0 0 0 0 1 1 0] + threevar.push_back(X[1]^~(~X[0]&(~X[1]|X[2]))); // [0 1 0 0 0 1 1 0] + threevar.push_back(X[1]^(X[0]&(X[1]|X[2]))); // [0 0 1 0 0 1 1 0] + threevar.push_back(X[0]^X[1]); // [0 1 1 0 0 1 1 0] + threevar.push_back((X[0]|X[1])&~(X[0]^(X[1]^X[2]))); // [0 0 0 1 0 1 1 0] + threevar.push_back(X[0]^(X[1]&X[2])); // [0 1 0 1 0 1 1 0] + threevar.push_back(X[1]^(X[0]&X[2])); // [0 0 1 1 0 1 1 0] + threevar.push_back(X[1]^(X[0]&(~X[1]|X[2]))); // [0 1 1 1 0 1 1 0] + threevar.push_back(X[2]&~(X[0]&X[1])); // [0 0 0 0 1 1 1 0] + threevar.push_back(X[1]^(X[0]|(X[1]^X[2]))); // [0 1 0 0 1 1 1 0] + threevar.push_back((X[0]&X[1])^(X[1]|X[2])); // [0 0 1 0 1 1 1 0] + threevar.push_back(X[1]^(X[0]|(~X[1]&X[2]))); // [0 1 1 0 1 1 1 0] + threevar.push_back(X[2]^(X[0]&X[1])); // [0 0 0 1 1 1 1 0] + threevar.push_back(X[2]^~(~X[0]|(~X[1]&X[2]))); // [0 1 0 1 1 1 1 0] + threevar.push_back(~(X[0]|~X[1])|(X[1]^X[2])); // [0 0 1 1 1 1 1 0] + threevar.push_back((X[0]^X[1])|(X[0]^X[2])); // [0 1 1 1 1 1 1 0] + threevar.push_back(X[0]&(X[1]&X[2])); // [0 0 0 0 0 0 0 1] + threevar.push_back(~(~X[0]|(X[1]^X[2]))); // [0 1 0 0 0 0 0 1] + threevar.push_back(X[1]&~(X[0]^X[2])); // [0 0 1 0 0 0 0 1] + threevar.push_back((X[0]|X[1])&(X[0]^(X[1]^X[2]))); // [0 1 1 0 0 0 0 1] + threevar.push_back(X[0]&X[1]); // [0 0 0 1 0 0 0 1] + threevar.push_back(~(~X[0]|(~X[1]&X[2]))); // [0 1 0 1 0 0 0 1] + threevar.push_back(X[1]&(X[0]|~X[2])); // [0 0 1 1 0 0 0 1] + threevar.push_back((X[1]&~X[2])|~(~X[0]|(~X[1]&X[2]))); // [0 1 1 1 0 0 0 1] + threevar.push_back(X[2]&~(X[0]^X[1])); // [0 0 0 0 1 0 0 1] + threevar.push_back((X[0]|~X[1])&(X[0]^(X[1]^X[2]))); // [0 1 0 0 1 0 0 1] + threevar.push_back(~(X[0]&~X[1])&(X[0]^(X[1]^X[2]))); // [0 0 1 0 1 0 0 1] + threevar.push_back(X[0]^(X[1]^X[2])); // [0 1 1 0 1 0 0 1] + threevar.push_back(X[1]^(~X[0]&(X[1]|X[2]))); // [0 0 0 1 1 0 0 1] + threevar.push_back(X[0]^(~X[1]&X[2])); // [0 1 0 1 1 0 0 1] + threevar.push_back(X[1]^~(X[0]|~X[2])); // [0 0 1 1 1 0 0 1] + threevar.push_back((X[0]&X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 1 1 0 0 1] + threevar.push_back(X[0]&X[2]); // [0 0 0 0 0 1 0 1] + threevar.push_back(X[0]&(~X[1]|X[2])); // [0 1 0 0 0 1 0 1] + threevar.push_back(X[2]^(~X[0]&(X[1]|X[2]))); // [0 0 1 0 0 1 0 1] + threevar.push_back(~(X[0]^(~X[1]|X[2]))); // [0 1 1 0 0 1 0 1] + threevar.push_back(X[0]&(X[1]|X[2])); // [0 0 0 1 0 1 0 1] + threevar.push_back(X[0]); // [0 1 0 1 0 1 0 1] + threevar.push_back((X[0]&X[2])|(X[1]&~X[2])); // [0 0 1 1 0 1 0 1] + threevar.push_back(~(~X[0]&(~X[1]|X[2]))); // [0 1 1 1 0 1 0 1] + threevar.push_back(X[2]&(X[0]|~X[1])); // [0 0 0 0 1 1 0 1] + threevar.push_back((X[1]&~X[2])^(X[0]|(X[1]^X[2]))); // [0 1 0 0 1 1 0 1] + threevar.push_back(X[2]^~(X[0]|~X[1])); // [0 0 1 0 1 1 0 1] + threevar.push_back((X[0]&~X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 1 0 1] + threevar.push_back((X[0]&X[1])|~(X[1]|~X[2])); // [0 0 0 1 1 1 0 1] + threevar.push_back(X[0]|(~X[1]&X[2])); // [0 1 0 1 1 1 0 1] + threevar.push_back((X[0]&X[1])|(X[1]^X[2])); // [0 0 1 1 1 1 0 1] + threevar.push_back(X[0]|(X[1]^X[2])); // [0 1 1 1 1 1 0 1] + threevar.push_back(X[1]&X[2]); // [0 0 0 0 0 0 1 1] + threevar.push_back((X[0]|X[1])&~(X[1]^X[2])); // [0 1 0 0 0 0 1 1] + threevar.push_back(X[1]&~(X[0]&~X[2])); // [0 0 1 0 0 0 1 1] + threevar.push_back(X[1]^(X[0]&~X[2])); // [0 1 1 0 0 0 1 1] + threevar.push_back(X[1]&(X[0]|X[2])); // [0 0 0 1 0 0 1 1] + threevar.push_back((X[0]&X[2])^(X[0]^(X[1]&X[2]))); // [0 1 0 1 0 0 1 1] + threevar.push_back(X[1]); // [0 0 1 1 0 0 1 1] + threevar.push_back(X[1]|(X[0]&~X[2])); // [0 1 1 1 0 0 1 1] + threevar.push_back(X[2]&~(X[0]&~X[1])); // [0 0 0 0 1 0 1 1] + threevar.push_back(X[2]^(X[0]&~X[1])); // [0 1 0 0 1 0 1 1] + threevar.push_back((X[1]&X[2])|(~X[0]&(X[1]|X[2]))); // [0 0 1 0 1 0 1 1] + threevar.push_back(~(X[0]|~X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 0 1 1] + threevar.push_back(X[1]^(~X[0]&(X[1]^X[2]))); // [0 0 0 1 1 0 1 1] + threevar.push_back(X[2]^~(~X[0]|(X[1]&X[2]))); // [0 1 0 1 1 0 1 1] + threevar.push_back(X[1]|~(X[0]|~X[2])); // [0 0 1 1 1 0 1 1] + threevar.push_back(X[1]|(X[0]^X[2])); // [0 1 1 1 1 0 1 1] + threevar.push_back(X[2]&(X[0]|X[1])); // [0 0 0 0 0 1 1 1] + threevar.push_back((X[0]&X[1])^(X[0]^(X[1]&X[2]))); // [0 1 0 0 0 1 1 1] + threevar.push_back(X[1]^(X[0]&(X[1]^X[2]))); // [0 0 1 0 0 1 1 1] + threevar.push_back(X[1]^~(~X[0]|(X[1]&X[2]))); // [0 1 1 0 0 1 1 1] + threevar.push_back((X[1]&X[2])|(X[0]&(X[1]|X[2]))); // [0 0 0 1 0 1 1 1] + threevar.push_back(X[0]|(X[1]&X[2])); // [0 1 0 1 0 1 1 1] + threevar.push_back(X[1]|(X[0]&X[2])); // [0 0 1 1 0 1 1 1] + threevar.push_back(X[0]|X[1]); // [0 1 1 1 0 1 1 1] + threevar.push_back(X[2]); // [0 0 0 0 1 1 1 1] + threevar.push_back(X[2]|(X[0]&~X[1])); // [0 1 0 0 1 1 1 1] + threevar.push_back(X[2]|~(X[0]|~X[1])); // [0 0 1 0 1 1 1 1] + threevar.push_back(X[2]|(X[0]^X[1])); // [0 1 1 0 1 1 1 1] + threevar.push_back(X[2]|(X[0]&X[1])); // [0 0 0 1 1 1 1 1] + threevar.push_back(X[0]|X[2]); // [0 1 0 1 1 1 1 1] + threevar.push_back(X[1]|X[2]); // [0 0 1 1 1 1 1 1] + threevar.push_back(X[0]|(X[1]|X[2])); // [0 1 1 1 1 1 1 1] +} diff --git a/bitwise_expr_lookup_tbl.hpp b/bitwise_expr_lookup_tbl.hpp new file mode 100644 index 0000000..1c3044c --- /dev/null +++ b/bitwise_expr_lookup_tbl.hpp @@ -0,0 +1,43 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include "minsn_template.hpp" + +// bw_expr_tbl_t is a singleton class that maintains a lookup table mapping +// boolean function evaluation traces (i.e. I/O behavior) to the shortest +// representation of each boolean function. +// for instance, if you found a boolean function f(x, y) with the following +// behavior: f(0, 0) = 0, f(0, 1) = 0, f(1, 0) = 0, f(1, 1) = 1, then you +// can query this object to find that f(x, y) = x & y. +// note that we do not consider any functions that return 1 on the all-zeros +// input. +class bw_expr_tbl_t +{ + qvector tbl; + +public: + static bw_expr_tbl_t instance; + + // do not call directly, use instance instead + bw_expr_tbl_t(); + + // eval_trace is a bitmap whose i'th bit contains the + // boolean function's evaluation on the i'th conjunction, + // where conjunctions are ordered in the same way as in lin_conj_exprs.hpp + minsn_template_ptr_t lookup(int nvars, uint64_t bit_trace) + { + QASSERT(30698, (bit_trace & 1) == 0); + QASSERT(30699, nvars <= 3); + QASSERT(30700, nvars >= 1); + QASSERT(30701, bit_trace < (1ull << (1ull << (nvars)))); + return tbl[nvars-1][bit_trace >> 1]; + // since the 0th conjunction is never considered, all vector indices are + // divided by 2. See the corresponding .cpp file for more info. + } +}; diff --git a/consts.hpp b/consts.hpp new file mode 100644 index 0000000..3aefcae --- /dev/null +++ b/consts.hpp @@ -0,0 +1,27 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#define ACTION_NAME "goomba:run" +// Z3_TIMEOUT_MS defines the amount of time we allow the z3 theorem prover to +// take to prove any given statement +#define Z3_TIMEOUT_MS 1000 + +// Only used for *generating* oracles: how many test cases to run against each +// function to generate fingerprints. Note that an existing oracle will report +// its own number, and the below constant will not be used +#define TCS_PER_EQUIV_CLASS 128 +// The number of inputs used when evaluating functions for fingerprinting +#define CANDIDATE_EXPR_NUMINPUTS 5 +// The maximum number of candidates to consider which have the same fingerprint +// as the expression being simplified +#define EQUIV_CLASS_MAX_CANDIDATES 10 +// The maximum number of fingerprints to consider for each expression being +// simplified -- this number is greater than one since we consider every +// possible assignment of input variables +#define EQUIV_CLASS_MAX_FINGERPRINTS 50 \ No newline at end of file diff --git a/equiv_class.cpp b/equiv_class.cpp new file mode 100644 index 0000000..573b082 --- /dev/null +++ b/equiv_class.cpp @@ -0,0 +1,104 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "equiv_class.hpp" +#include "optimizer.hpp" + + +//------------------------------------------------------------------------- +// replaces all references to abstract mop_l's with variables from new_vars +minsn_t *make_concrete_minsn(ea_t ea, const minsn_t &minsn, const mopvec_t &new_vars, int newsz) +{ + struct mop_reassigner_t : public mop_visitor_t + { + const mopvec_t &new_vars; + ea_t ea; + mop_reassigner_t(ea_t e, const mopvec_t &nm) + : new_vars(nm), ea(e) {} + int idaapi visit_mop(mop_t *op, const tinfo_t *, bool) + { + if ( op->t == mop_l ) + { + int idx = op->l->idx; + if ( idx >= new_vars.size() ) + return -1; + op->t = mop_d; + op->d = resize_mop(ea, new_vars.at(idx), op->size, false); + } + return 0; + } + }; + + minsn_t *res = nullptr; + minsn_t *copy = new minsn_t(minsn); + + mop_reassigner_t mr(ea, new_vars); + int code = copy->for_all_ops(mr); + if ( code >= 0 ) + { + copy->setaddr(ea); + + // resize res to the correct output size + mop_t res_mop; + res_mop.create_from_insn(copy); + res = resize_mop(ea, res_mop, newsz, false); + } + delete copy; + return res; +} + +//------------------------------------------------------------------------- +static void create_var_mapping(var_mapping_t &dest, const mopvec_t &mops) +{ + for ( size_t i = 0; i < mops.size(); i++ ) + dest.insert( { mops[i], i } ); +} + +//------------------------------------------------------------------------- +void equiv_class_finder_t::find_candidates(minsn_set_t &dest, const minsn_t &insn) +{ + std::set seen; + int num_fingerprints = 0; // includes duplicate fingerprints + int num_candidates = 0; + + mopvec_t input_mops = get_input_mops(insn); + do + { + var_mapping_t mapping; + create_var_mapping(mapping, input_mops); + + func_fingerprint_t fingerprint = compute_fingerprint(insn, &mapping); + msg("Computed fingerprint %" FMT_64 "x\n", fingerprint); + + num_fingerprints++; + if ( num_fingerprints > EQUIV_CLASS_MAX_FINGERPRINTS ) + break; + + if ( !seen.insert(fingerprint).second ) + continue; // already seen + + const minsn_set_t *equiv_class = find_equiv_class(fingerprint); + if ( equiv_class != nullptr ) + { + for ( const auto &mi : *equiv_class ) + { + num_candidates++; +// msg("Fingerprint matches: %s\n", mi->dstr()); + minsn_t *concrete = make_concrete_minsn(insn.ea, *mi, input_mops, insn.d.size); + + if ( concrete != nullptr ) + dest.insert(concrete); + + if ( num_candidates >= EQUIV_CLASS_MAX_CANDIDATES ) + break; + } + } + + } while ( std::next_permutation(input_mops.begin(), input_mops.end()) ); +} diff --git a/equiv_class.hpp b/equiv_class.hpp new file mode 100644 index 0000000..75d14ff --- /dev/null +++ b/equiv_class.hpp @@ -0,0 +1,303 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include +#include "msynth_parser.hpp" +#include "heuristics.hpp" +#include "linear_exprs.hpp" +#include "consts.hpp" + +struct minsn_with_mapping_t; + +typedef std::set minsn_set_t; + +typedef qvector output_behavior_t; +typedef qvector testcase_t; +typedef std::map var_mapping_t; +typedef uint64 func_fingerprint_t; +typedef std::map equiv_class_map_t; + +#define CHECK_SERIALIZATION_CONSISTENCY true + +//------------------------------------------------------------------------- +// output behavior is summarized as a list of uint64's, each corresponding to a test case +inline func_fingerprint_t compute_fingerprint_from_outputs(const output_behavior_t &outputs) +{ + // FNV-1a, as per Wikipedia + const uint64 FNV_BASIS = 0xcbf29ce484222325; + const uint64 FNV_PRIME = 0x100000001b3; + uint64 sum = FNV_BASIS; + for ( uint64 c : outputs ) + { + sum ^= c; + sum *= FNV_PRIME; + } + return sum; +} + +//------------------------------------------------------------------------- +inline void gen_testcase(testcase_t *tc) +{ + tc->resize(CANDIDATE_EXPR_NUMINPUTS); + for ( auto &v : *tc ) + v = gen_rand_mcode_val(8).val; +} + +//------------------------------------------------------------------------- +class equiv_class_finder_t +{ +public: + equiv_class_map_t equiv_classes; + qvector testcases; + + //------------------------------------------------------------------------- + // helper_emu_t evaluates expressions for a given test case and variable mapping + struct helper_emu_t : public mcode_emulator_t + { + const testcase_t &tc; + const var_mapping_t *var_mapping; // maps variables to input index + // assigning a nullptr var_mapping indicates that the indexing should be done + // according to the abstract mop's self-declared index + + helper_emu_t (const testcase_t &t, const var_mapping_t *vm) + : tc(t), var_mapping(vm) {} + + virtual mcode_val_t get_var_val(const mop_t &mop) override + { + if ( var_mapping == nullptr ) + { + // the instruction must be abstract, get the index from the mop itself + QASSERT(30706, mop.t == mop_l); + return mcode_val_t(tc[mop.l->idx], mop.size); + } + return mcode_val_t(tc.at(var_mapping->at(mop)), mop.size); + } + }; + + virtual ~equiv_class_finder_t() {} + + //------------------------------------------------------------------------- + equiv_class_finder_t() + { + testcases.resize(TCS_PER_EQUIV_CLASS); + for ( auto &tc : testcases ) + gen_testcase(&tc); + } + + //------------------------------------------------------------------------- + // mapping = nullptr means the instruction is abstract (all terminal mops + // have type mop_l), and mop indices will be retrieved by querying mop.l->idx + func_fingerprint_t compute_fingerprint( + const minsn_t &ins, + const var_mapping_t *mapping = nullptr) + { + output_behavior_t res; + res.reserve(testcases.size()); + for ( const auto &tc : testcases ) + { + helper_emu_t emu(tc, mapping); + res.push_back(emu.minsn_value(ins).val); + } + return compute_fingerprint_from_outputs(res); + } + + //------------------------------------------------------------------------- + func_fingerprint_t compute_fingerprint_from_serialization( + uchar *buf, uint32 sz, + int version = -1, + const var_mapping_t *mapping = nullptr) + { + if ( version == -1 ) // use current serialization version + { + bytevec_t bv; + version = minsn_t(0).serialize(&bv); + } + minsn_t minsn(0); + minsn.deserialize(buf, sz, version); + + return compute_fingerprint(minsn, mapping); + } + + //------------------------------------------------------------------------- + // computes the fingerprint of the abstract minsn and adds it to the index + void add_abstract_minsn(minsn_t *ins) + { + auto fingerprint = compute_fingerprint(*ins); + auto it = equiv_classes.find(fingerprint); + if ( it != equiv_classes.end() ) + { + // check if semantically equivalent expression already exists + for ( const auto &o : it->second ) + if ( probably_equivalent(*o, *ins) ) + return; + it->second.insert(ins); + } + else + { + minsn_set_t new_entry; + new_entry.insert(ins); + equiv_classes.insert( { fingerprint, new_entry } ); + } + } + + //------------------------------------------------------------------------- + virtual const minsn_set_t *find_equiv_class(func_fingerprint_t fingerprint) + { + auto p = equiv_classes.find(fingerprint); + if ( p != equiv_classes.end() ) + return &p->second; + return nullptr; + } + + //------------------------------------------------------------------------- + // find candidate minsns that match the fingerprint of the given minsn + // before being added, these are made concrete -- the abstract mop_l's are + // replaced by real mops from the input insn + void find_candidates(minsn_set_t &dest, const minsn_t &insn); +}; + +//------------------------------------------------------------------------- +struct equiv_class_idx_entry_t +{ + func_fingerprint_t fingerprint; + uint64_t offset; + // offset relative to the beginning of where minsns are stored within the oracle file + + bool operator<(const equiv_class_idx_entry_t &o) const + { + return fingerprint < o.fingerprint; + } +}; + +//------------------------------------------------------------------------- +struct equiv_class_idx_t +{ + qvector index; + + //------------------------------------------------------------------------- + void read_from_file(FILE *file) + { + uint32 idx_sz; + if ( qfread(file, &idx_sz, sizeof(idx_sz)) != sizeof(idx_sz) ) + INTERR(30719); + CASSERT(sizeof(equiv_class_idx_entry_t) == 16); + + index.resize_noinit(idx_sz); + size_t nbytes = idx_sz * sizeof(equiv_class_idx_entry_t); + if ( qfread(file, index.begin(), nbytes) != nbytes ) + INTERR(0); + } + + //------------------------------------------------------------------------- + size_t find(func_fingerprint_t fp) + { + equiv_class_idx_entry_t key; + key.fingerprint = fp; + auto p = std::lower_bound(index.begin(), index.end(), key); + if ( p == index.end() || p->fingerprint != fp ) + return -1; + return p->offset; + } +}; + +//------------------------------------------------------------------------- +// lazy-loading collection of equivalence classes +struct equiv_class_finder_lazy_t : public equiv_class_finder_t +{ + FILE *file; + qoff64_t fsize; + uint32 format_version; // format version used to serialize minsn_t's + equiv_class_idx_t index; + uint64 minsns_offset; // offset at which the minsns table begins + + virtual ~equiv_class_finder_lazy_t() { qfclose(file); } + + //------------------------------------------------------------------------- + //lint -sem(equiv_class_finder_lazy_t::equiv_class_finder_lazy_t, custodial(1)) + equiv_class_finder_lazy_t(FILE *f) : file(f) + { + fsize = qfsize(file); + + // read in the format version + if ( qfread(file, &format_version, sizeof(format_version)) != sizeof(format_version) ) + INTERR(30716); + + // read and validate the number of the test cases + uint32 n_tcs; + if ( qfread(file, &n_tcs, sizeof(n_tcs)) != sizeof(n_tcs) ) + INTERR(30717); + if ( n_tcs > fsize ) + INTERR(0); + + // read in the test cases + testcases.resize(n_tcs); + for ( auto &new_tc : testcases ) + { + new_tc.resize(CANDIDATE_EXPR_NUMINPUTS); + for ( uint64 &new_inp : new_tc ) + if ( qfread(file, &new_inp, sizeof(new_inp)) != sizeof(new_inp) ) + INTERR(30718); + } + + // read in the index + index.read_from_file(file); + + minsns_offset = qftell(file); +// msg("minsns offset %llu", minsns_offset); + } + + //------------------------------------------------------------------------- + // populates the equiv_classes map with the minsn set included in the file + // for the given fingerprint + void read_minsn_set_from_file(func_fingerprint_t fp) + { + int64 idx_lookup = index.find(fp); + if ( idx_lookup < 0 ) + return; // fingerprint doesn't exist in oracle + if ( equiv_classes.count(fp) != 0 ) + return; // we already loaded in the equiv class + + uint64 minsn_offset = minsns_offset + idx_lookup; + if ( qfseek(file, minsn_offset, SEEK_SET) != 0 ) + INTERR(30722); + + uint32 n_minsns; + if ( qfread(file, &n_minsns, sizeof(n_minsns)) != sizeof(n_minsns) ) + INTERR(30723); + if ( n_minsns > fsize ) // sanity check + INTERR(0); + + bytevec_t bv; + minsn_set_t &set = equiv_classes[fp]; + for ( uint32 i = 0; i < n_minsns; i++ ) + { + uint32 minsn_sz; + if ( qfread(file, &minsn_sz, sizeof(minsn_sz)) != sizeof(minsn_sz) ) + INTERR(30724); + if ( minsn_sz > fsize ) // sanity check + INTERR(0); + bv.resize(minsn_sz); + if ( qfread(file, bv.begin(), minsn_sz) != minsn_sz ) + INTERR(30725); + minsn_t *minsn = new minsn_t(0); + minsn->deserialize(bv.begin(), minsn_sz, format_version); + set.insert(minsn); + } + } + + //------------------------------------------------------------------------- + const minsn_set_t *find_equiv_class(func_fingerprint_t fingerprint) override + { + read_minsn_set_from_file(fingerprint); + return equiv_class_finder_t::find_equiv_class(fingerprint); + } + + //------------------------------------------------------------------------- + bool optimize(minsn_t &insn); +}; diff --git a/file.cpp b/file.cpp new file mode 100644 index 0000000..48a38c7 --- /dev/null +++ b/file.cpp @@ -0,0 +1,212 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include +#include +#include "file.hpp" +#include "msynth_parser.hpp" +#include "simp_lin_conj_exprs.hpp" +#include "heuristics.hpp" +#include "equiv_class.hpp" + +//------------------------------------------------------------------------- +// In fact this function is not really needed. The user can simply turn on +// the timestamp display in the output window. +static qstring curtime() +{ + char buf[64]; + char *ptr = buf; + char *end = buf + sizeof(buf); + qtime64_t ts = qtime64(); + ptr += qstrftime64(ptr, end-ptr, "%H:%M:%S", ts); + uint32 msecs = get_usecs(ts) / 1000; + qsnprintf(ptr, end-ptr, ".%03d", msecs); + return qstring(buf); +} + +//------------------------------------------------------------------------- +void create_minsns_file(FILE *msynth_in, FILE *minsns_out) +{ + qstring line; + int n_proc = 0; + int n_written = 0; + while ( qgetline(&line, msynth_in) >= 0 ) + { + n_proc++; + if ( line.size() == 0 ) + continue; + if ( n_proc % REPORT_FREQ == 0 ) + msg("%s: Processed %d, Wrote %d\n", curtime().c_str(), n_proc, n_written); + mopvec_t default_vars; + //------------------------------------------------------------------------- + // an *abstract* mop is a mop_l that does not refer to anything within a + // specific program, it is a placeholder for minsn templates + for ( int i = 0; i < CANDIDATE_EXPR_NUMINPUTS; i++ ) + { + mop_t new_var; + new_var.t = mop_l; + new_var.l = new lvar_ref_t(nullptr, i); + new_var.size = 8; + default_vars.push_back(new_var); + } + + msynth_expr_parser_t mep(line.c_str(), default_vars); + minsn_t *insn = mep.parse_next_expr(); + + bytevec_t bv; + insn->serialize(&bv); + uint32 bv_sz = bv.size(); + qfwrite(minsns_out, &bv_sz, sizeof(bv_sz)); + qfwrite(minsns_out, bv.begin(), bv_sz); + n_written++; + + delete insn; + } + + msg("%s: Processed %d, Wrote %d\n", curtime().c_str(), n_proc, n_written); +} + +//------------------------------------------------------------------------- +// bytevec comparison based on length +struct bv_len_cmptr_t +{ + inline bool operator()(const bytevec_t &a, const bytevec_t &b) const + { + auto asz = a.size(); + auto bsz = b.size(); + return std::tie(asz, a) < std::tie(bsz, b); + } +}; +typedef std::set bvset_t; + +//------------------------------------------------------------------------- +inline size_t bv_sz_on_disk(const bytevec_t &bv) +{ + return sizeof(uint32) + bv.size(); +} + +//------------------------------------------------------------------------- +static void write_bv_to_disk(FILE *fout, const bytevec_t &bv) +{ + uint32 bv_sz = bv.size(); + qfwrite(fout, &bv_sz, sizeof(bv_sz)); + qfwrite(fout, bv.begin(), bv_sz); +} + +//------------------------------------------------------------------------- +static size_t bvset_sz_on_disk(const bvset_t &bvset) +{ + size_t res = sizeof(uint32); + for ( const auto &bv : bvset ) + res += bv_sz_on_disk(bv); + return res; +} + +//------------------------------------------------------------------------- +static void write_bvset_to_disk(FILE *fout, const bvset_t &bvset) +{ + uint32 bvset_sz = bvset.size(); + qfwrite(fout, &bvset_sz, sizeof(bvset_sz)); + for ( const auto &bv : bvset ) + write_bv_to_disk(fout, bv); +} + +//------------------------------------------------------------------------- +bool create_oracle_file(FILE *minsns_in, FILE *oracle_out) +{ + // begin by loading the minsns from the file and generating fingerprints + // keeping full minsns in memory would take too much space, so we store them as strings + // and use string length as a proxy for complexity + std::map oracle; + equiv_class_finder_t ecf; + + int n_proc = 0; + while ( true ) + { + if ( n_proc % REPORT_FREQ == 0 ) + msg("%s: Processed %d, #Fingerprints %" FMT_Z "\n", curtime().c_str(), n_proc, oracle.size()); + n_proc++; + uint32 minsn_sz; + if ( qfread(minsns_in, &minsn_sz, sizeof(minsn_sz)) != sizeof(minsn_sz) ) + break; + if ( minsn_sz > qfsize(minsns_in) ) // sanity check on minsn_sz + { + msg("Wrong instruction size %d in the oracle file, stopped reading it\n", minsn_sz); + return false; + } + bytevec_t buf; + buf.resize(minsn_sz); + if ( qfread(minsns_in, buf.begin(), minsn_sz) != minsn_sz ) + break; + + func_fingerprint_t fp = ecf.compute_fingerprint_from_serialization(buf.begin(), minsn_sz); + + if ( oracle.count(fp) == 0 ) + oracle.insert( { fp, std::set() } ); + + oracle[fp].insert(buf); + } + + msg("%s: Processed %d, #Fingerprints %" FMT_Z "\n", curtime().c_str(), n_proc, oracle.size()); + + // write the resulting oracle to the file + // begin by writing the format version + { + bytevec_t bv; + uint32 format_version = minsn_t(0).serialize(&bv); + qfwrite(oracle_out, &format_version, sizeof(format_version)); + } + + // write the ecf's test cases to file + uint32 n_tcs = ecf.testcases.size(); + qfwrite(oracle_out, &n_tcs, sizeof(n_tcs)); + for ( const testcase_t &tc : ecf.testcases ) + for ( const uint64 input : tc ) + qfwrite(oracle_out, &input, sizeof(input)); + + msg("Wrote test cases to file\n"); + + // write the index to file + // the index is a list of entries, each consisting of a uint64 (fingerprint) and a uint64 (offset) + uint32 index_sz = oracle.size(); + qfwrite(oracle_out, &index_sz, sizeof(index_sz)); + qoff64_t current_offset = 0; + int n_written = 0; + for ( const auto &entry : oracle ) + { + if ( n_written % REPORT_FREQ == 0 ) + msg("%s: Wrote %d index entries\n", curtime().c_str(), n_written); + n_written++; + + auto fingerprint = entry.first; + auto bvset = entry.second; + qfwrite(oracle_out, &fingerprint, sizeof(fingerprint)); + qfwrite(oracle_out, ¤t_offset, sizeof(current_offset)); + + current_offset += bvset_sz_on_disk(bvset); + } + + msg("Size of oracle on disk: %llu\n", current_offset); + msg("Current file position: %llu\n", qftell(oracle_out)); + + // write the actual microinstructions to disk + n_written = 0; + for ( const auto &entry : oracle ) + { + if ( n_written % REPORT_FREQ == 0 ) + msg("%s: Wrote %d microinstruction vectors\n", curtime().c_str(), n_written); + n_written++; + + write_bvset_to_disk(oracle_out, entry.second); + } + + msg("%s: Wrote %d microinstruction vectors\n", curtime().c_str(), n_written); + msg("Current file position: %" FMT_64 "u\n", qftell(oracle_out)); + return true; +} diff --git a/file.hpp b/file.hpp new file mode 100644 index 0000000..5c21e0f --- /dev/null +++ b/file.hpp @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include + +// functions that convert huge files in a streaming fashion without using too much memory + +const int REPORT_FREQ = 10000; // how often we should report progress in the log +// generates a file that is just a list of minsns +void create_minsns_file(FILE *msynth_in, FILE *minsns_out); +// given a minsns file, fingerprints each minsn and serializes it into the oracle +bool create_oracle_file(FILE *minsns_in, FILE *oracle_out); \ No newline at end of file diff --git a/generate_oracle.bat b/generate_oracle.bat new file mode 100644 index 0000000..76ce330 --- /dev/null +++ b/generate_oracle.bat @@ -0,0 +1,25 @@ +@if "%DEBUG%" == "" @echo off +@rem ########################################################################## +@rem +@rem gooMBA oracle file generation script +@rem +@rem ########################################################################## +@rem Set local scope for the variables with windows NT shell +if "%OS%"=="Windows_NT" setlocal + +if .%1 == . goto usage +set VD_MSYNTH_PATH=%~f1 +echo generating minsns file (step 1/2)... +idat64 -A -Llog.txt tests/idb/mba_challenge.i64 +set VD_MSYNTH_PATH= +set VD_MBA_MINSNS_PATH=%~dpnx1.b +echo generating oracle file (step 2/2)... +idat64 -A -Llog.txt tests/idb/mba_challenge.i64 +echo. >> log.txt +echo finished! +move %~dpnx1.b.c %~dpn1.oracle +echo finished! Result is in %~dpn1.oracle +tail log.txt +exit /b +:usage +echo "Usage: generate_oracle.bat all_combined.txt" diff --git a/generate_oracle.sh b/generate_oracle.sh new file mode 100644 index 0000000..0712c05 --- /dev/null +++ b/generate_oracle.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +# usage: ./generate_oracle.sh all_combined.txt +# after the script finishes running, the oracle file will be available in all_combined.txt.oracle + +( + VD_MSYNTH_PATH=`realpath $1` ida64 -A -S`realpath script.py` -Llog.txt tests/idb/mba_challenge.i64 + VD_MBA_MINSNS_PATH=`realpath $1.b` ida64 -A -S`realpath script.py` -Llog.txt tests/idb/mba_challenge.i64 + mv $1.b.c $1.oracle + echo -e "\nfinished! Result is in $1.oracle" >> log.txt +) & + +tail -F log.txt \ No newline at end of file diff --git a/goomba.cfg b/goomba.cfg new file mode 100644 index 0000000..8d00f3d --- /dev/null +++ b/goomba.cfg @@ -0,0 +1,17 @@ + +// This configuration file is used by the mixed_bool_arith plugin, which +// provides deobfuscation functionality for expressions obfuscated with +// mixed boolean arithmetic expressions. + +// By default, the plugin only engages through a right-click menu option. +// Set the below option to YES to make the plugin engage automatically +// when the decompiler is invoked. +MBA_RUN_AUTOMATICALLY = NO +// The timeout in ms for z3 proofs. Set this to 0 to disable z3 proofs +// entirely and assume simplifications are correct after heuristic checks. +MBA_Z3_TIMEOUT = 1000 +// When z3 times out, should the simplification be assumed correct? +MBA_Z3_ASSUME_TIMEOUTS_CORRECT = YES +// Path to an MBA oracle. Leave this empty to disable the function +// fingerprinting algorithm and use only linear methods. +MBA_ORACLE_PATH = ""; diff --git a/goomba.cpp b/goomba.cpp new file mode 100644 index 0000000..af274e2 --- /dev/null +++ b/goomba.cpp @@ -0,0 +1,260 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * It deobfuscates the MBA (mixed boolean arithmetic) epxressions. + * + */ + +#include + +#include "z3++_no_warn.h" +#include "consts.hpp" +#include "optimizer.hpp" +#include "equiv_class.hpp" +#include "file.hpp" +#include +#include + +struct plugin_ctx_t; + +//-------------------------------------------------------------------------- +// returns true if the environment variables indicate the plugin should +// always be enabled (i.e. in testing environments) +inline bool always_on(void) +{ + return qgetenv("VD_MBA_AUTO"); +} + +//-------------------------------------------------------------------------- +struct action_handler : public action_handler_t +{ + plugin_ctx_t *plugmod; + + action_handler(plugin_ctx_t *_plugmod) : plugmod(_plugmod) {} + + virtual int idaapi activate(action_activation_ctx_t *ctx) override; + virtual action_state_t idaapi update(action_update_ctx_t *) override + { + return AST_ENABLE; + }; +}; + +//-------------------------------------------------------------------------- +//lint -e{958} padding of 7 bytes needed to align member on a 8 byte boundary +struct plugin_ctx_t : public plugmod_t +{ + bool run_automatically = false; + qstring oracle_path; + + action_handler ah; + optimizer_t optimizer; + bool plugmod_active = false; + plugin_ctx_t(); + ~plugin_ctx_t() { term_hexrays_plugin(); } + virtual bool idaapi run(size_t) override; +}; + +//-------------------------------------------------------------------------- +static plugmod_t *idaapi init() +{ + if ( !init_hexrays_plugin() ) + return nullptr; // no decompiler + + const char *hxver = get_hexrays_version(); + msg("Hex-rays version %s has been detected, %s ready to use\n", + hxver, PLUGIN.wanted_name); + + plugin_ctx_t *plugmod = new plugin_ctx_t; + + const cfgopt_t cfgopts[] = + { + cfgopt_t("MBA_RUN_AUTOMATICALLY", &plugmod->run_automatically, 1), + cfgopt_t("MBA_Z3_TIMEOUT", &plugmod->optimizer.z3_timeout), + cfgopt_t("MBA_ORACLE_PATH", &plugmod->oracle_path), + cfgopt_t("MBA_Z3_ASSUME_TIMEOUTS_CORRECT", &plugmod->optimizer.z3_assume_timeouts_correct, 1) + }; + + read_config_file("goomba", cfgopts, qnumber(cfgopts), nullptr); + + if ( plugmod->oracle_path.empty() ) + qgetenv("VD_MBA_ORACLE_PATH", &plugmod->oracle_path); + + if ( !plugmod->oracle_path.empty() ) + { + const char *path = plugmod->oracle_path.c_str(); + FILE *fin = qfopen(path, "rb"); + if ( fin != nullptr ) + { + plugmod->optimizer.equiv_classes = new equiv_class_finder_lazy_t(fin); + msg("%s: loaded MBA oracle\n", path); + } + else + { + msg("%s: %s\n", path, qstrerror(-1)); + } + } + + qstring ifpath; + if ( qgetenv("VD_MSYNTH_PATH", &ifpath) ) + { + qstring ofpath = ifpath + ".b"; + FILE *fin = qfopen(ifpath.c_str(), "r"); + if ( fin == nullptr ) + error("%s: failed to open for reading", ifpath.c_str()); + FILE *fout = qfopen(ofpath.c_str(), "wb"); + if ( fout == nullptr ) + error("%s: failed to open for writing", ofpath.c_str()); + create_minsns_file(fin, fout); + qfclose(fin); + qfclose(fout); + // do not save the IDB + set_database_flag(DBFL_KILL); + qexit(0); + } + + if ( qgetenv("VD_MBA_MINSNS_PATH", &ifpath) ) + { + qstring ofpath = ifpath + ".c"; + FILE *fin = qfopen(ifpath.c_str(), "rb"); + if ( fin == nullptr ) + error("%s: failed to open for reading", ifpath.c_str()); + FILE *fout = qfopen(ofpath.c_str(), "wb"); + if ( fout == nullptr ) + error("%s: failed to open for writing", ofpath.c_str()); + bool ok = create_oracle_file(fin, fout); + qfclose(fin); + qfclose(fout); + if ( !ok ) + error("%s: failed to process", ifpath.c_str()); + // do not save the IDB + set_database_flag(DBFL_KILL); + qexit(0); + } + + return plugmod; +} + +//-------------------------------------------------------------------------- +int idaapi action_handler::activate(action_activation_ctx_t *ctx) +{ + vdui_t *vu = get_widget_vdui(ctx->widget); + if ( vu != nullptr ) + { + plugmod->plugmod_active = true; + vu->refresh_view(true); + return 1; + } + return 0; +} + +//-------------------------------------------------------------------------- +// This callback handles various hexrays events. +static ssize_t idaapi callback(void *ud, hexrays_event_t event, va_list va) +{ + plugin_ctx_t *plugmod = (plugin_ctx_t *) ud; + switch ( event ) + { + case hxe_microcode: // microcode has been generated + { + mba_t *mba = va_arg(va, mba_t *); + if ( always_on() || plugmod->run_automatically ) + plugmod->plugmod_active = true; + if ( plugmod->plugmod_active ) + mba->set_mba_flags2(MBA2_PROP_COMPLEX); // increase acceptable complexity + } + break; + + case hxe_populating_popup: + { + TWidget *widget = va_arg(va, TWidget *); + TPopupMenu *popup = va_arg(va, TPopupMenu *); + attach_action_to_popup(widget, popup, ACTION_NAME); + } + break; + + case hxe_glbopt: + if ( plugmod->plugmod_active ) + { + mba_t *mba = va_arg(va, mba_t *); + + struct ida_local insn_optimize_t : public minsn_visitor_t + { + optimizer_t &optimizer; + int cnt = 0; + insn_optimize_t ( optimizer_t &o ) : optimizer(o) {} + int idaapi visit_minsn() override + { +// msg("Optimizing %s\n", curins->dstr()); + if ( optimizer.optimize_insn_recurse(curins) ) + { + cnt++; + blk->mark_lists_dirty(); + mba->dump_mba(true, "vd_mba success %a", curins->ea); + } + return 0; + } + }; + + insn_optimize_t visitor(plugmod->optimizer); + mba->for_all_topinsns(visitor); + + if ( visitor.cnt != 0 ) + { + mba->verify(true); + msg("Completed mba optimization pass, improved %d expressions\n", visitor.cnt); + } + plugmod->plugmod_active = false; + mba->clr_mba_flags2(MBA2_PROP_COMPLEX); + return MERR_LOOP; // restart optimization + } + break; + + default: + break; + } + return 0; +} + +//-------------------------------------------------------------------------- +plugin_ctx_t::plugin_ctx_t() : ah(this) +{ + install_hexrays_callback(callback, this); + register_action(ACTION_DESC_LITERAL_PLUGMOD( + ACTION_NAME, + "Run gooMBA Optimizer", + &ah, + this, + nullptr, + nullptr, + -1)); +} + +//-------------------------------------------------------------------------- +bool idaapi plugin_ctx_t::run(size_t) +{ + return true; +} + +//-------------------------------------------------------------------------- +static char comment[] = "gooMBA plugin for Hex-Rays decompiler"; + +//-------------------------------------------------------------------------- +// +// PLUGIN DESCRIPTION BLOCK +// +//-------------------------------------------------------------------------- +plugin_t PLUGIN = +{ + IDP_INTERFACE_VERSION, + PLUGIN_MULTI // The plugin can work with multiple idbs in parallel +| PLUGIN_HIDE, // no menu items in Edit, Plugins + init, // initialize + nullptr, + nullptr, + comment, // long comment about the plugin + nullptr, // multiline help about the plugin + "gooMBA plugin", // the preferred short name of the plugin + nullptr, // the preferred hotkey to run the plugin +}; diff --git a/heuristics.cpp b/heuristics.cpp new file mode 100644 index 0000000..d5fbeb6 --- /dev/null +++ b/heuristics.cpp @@ -0,0 +1,130 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "heuristics.hpp" + +//------------------------------------------------------------------------- +inline uint64 rand64() +{ + uint32 r1 = rand(); + uint32 r2 = rand(); + return uint64(r1) << 32 | uint64(r2); +} + +//------------------------------------------------------------------------- +mcode_val_t gen_rand_mcode_val(int size) +{ + if ( rand() > SPECIAL_PROBABILITY * RAND_MAX ) + { + // select from uniform random distribution + return mcode_val_t(rand64(), size); + } + else + { + // select from special cases + return mcode_val_t(SPECIAL[rand() % NUM_SPECIAL], size); + } +} + +//------------------------------------------------------------------------- +// guesses whether or not the instruction is MBA +bool is_mba(const minsn_t &insn) +{ + struct mba_opc_counter_t : public minsn_visitor_t + { + int bool_cnt = 0; + int arith_cnt = 0; + int idaapi visit_minsn(void) override + { + switch ( curins->opcode ) + { + case m_neg: + case m_add: + case m_sub: + case m_mul: + case m_udiv: + case m_sdiv: + case m_umod: + case m_smod: + case m_shl: + case m_shr: + arith_cnt++; + break; + case m_bnot: + case m_or: + case m_and: + case m_xor: + case m_sar: + bool_cnt++; + break; + default: + return 0; + } + return bool_cnt >= MIN_MBA_BOOL_OPS && arith_cnt >= MIN_MBA_ARITH_OPS; + } + }; + + if ( is_mcode_xdsu(insn.opcode) ) + return false; // exclude xdsu, it is better to optimize its operand + + mba_opc_counter_t cntr; + return CONST_CAST(minsn_t*)(&insn)->for_all_insns(cntr) != 0; +} + +//------------------------------------------------------------------------- +// runs a battery of random test cases against both expressions to see if they are equivalent +bool probably_equivalent(const minsn_t &insn, const candidate_expr_t &expr) +{ + for ( int i = 0; i < NUM_TEST_CASES; i++ ) + { + mcode_emu_rand_vals_t emu; + mcode_val_t insn_eval = emu.minsn_value(insn); + mcode_val_t expr_eval = expr.evaluate(emu); + + if ( insn_eval != expr_eval ) + return false; + } + + return true; +} + +//------------------------------------------------------------------------- +// runs a battery of random test cases against both expressions to see if they are equivalent +bool probably_equivalent(const minsn_t &a, const minsn_t &b) +{ + for ( int i = 0; i < NUM_TEST_CASES; i++ ) + { + mcode_emu_rand_vals_t emu; + mcode_val_t insn_eval = emu.minsn_value(a); + mcode_val_t expr_eval = emu.minsn_value(b); + + if ( insn_eval != expr_eval ) + return false; + } + + return true; +} + +//------------------------------------------------------------------------- +// estimates the "complexity" of a given instruction +int score_complexity(const minsn_t &insn) +{ + struct ida_local complexity_counter_t : public minsn_visitor_t + { + int cnt = 0; + int idaapi visit_minsn() override + { + cnt++; + return 0; + } + }; + complexity_counter_t cc; + CONST_CAST(minsn_t&)(insn).for_all_insns(cc); + return cc.cnt; +} diff --git a/heuristics.hpp b/heuristics.hpp new file mode 100644 index 0000000..23f3265 --- /dev/null +++ b/heuristics.hpp @@ -0,0 +1,83 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include "mcode_emu.hpp" +#include "linear_exprs.hpp" + +const uint64 SPECIAL[] = { 0, 1, 0xffffffffffffffff }; +const int NUM_SPECIAL = qnumber(SPECIAL); +const double SPECIAL_PROBABILITY = 0.2; // probability of selecting a special number when sampling + +// an expression must have at least this many subinstructions of each type to count as an MBA +const int MIN_MBA_BOOL_OPS = 1; +const int MIN_MBA_ARITH_OPS = 1; + +// number of test cases to run when checking if an instruction matches the candidate expression's behavior +const int NUM_TEST_CASES = 256; + +//------------------------------------------------------------------------- +mcode_val_t gen_rand_mcode_val(int size); + +//------------------------------------------------------------------------- +// emulates the microcode, assigning random values to unknown variables +// (but keeping them consistent across executions) +struct mcode_emu_rand_vals_t : public mcode_emulator_t +{ + std::map assigned_vals; + + mcode_val_t get_var_val(const mop_t &mop) override + { + // check that the mop is indeed a variable + mopt_t t = mop.t; + QASSERT(30672, t == mop_r || t == mop_S || t == mop_v || t == mop_l); + + auto assignment = assigned_vals.find(mop); + if ( assignment != assigned_vals.end() ) + return assignment->second; + + mcode_val_t new_val = gen_rand_mcode_val(mop.size); + assigned_vals.insert( { mop, new_val } ); + return new_val; + } +}; + +//------------------------------------------------------------------------- +bool is_mba(const minsn_t &insn); + +//------------------------------------------------------------------------- +bool probably_equivalent(const minsn_t &insn, const candidate_expr_t &expr); +bool probably_equivalent(const minsn_t &a, const minsn_t &b); + +//------------------------------------------------------------------------- +// estimates the "complexity" of a given instruction +int score_complexity(const minsn_t &insn); + +struct minsn_complexity_cmptr_t +{ + bool operator()(const minsn_t *a, const minsn_t *b) const + { + auto score_a = score_complexity(*a); + auto score_b = score_complexity(*b); + return score_a < score_b; + } +}; + +inline mopvec_t get_input_mops(const minsn_t &insn) +{ + default_zero_mcode_emu_t emu; + emu.minsn_value(insn); // populate emu.assigned_vals + + mopvec_t res; + res.reserve(emu.assigned_vals.size()); + for ( auto const &entry : emu.assigned_vals ) + res.push_back(entry.first); + + std::sort(res.begin(), res.end()); + return res; +} \ No newline at end of file diff --git a/images/mba1_after.png b/images/mba1_after.png new file mode 100644 index 0000000000000000000000000000000000000000..8242ca0b9c5f8767e1a4bf0a24fef0bc1c08aaaa GIT binary patch literal 7636 zcmY*eRahKNu*Dab1%kUJxVyW%1qkkL!6mpuaQ8q6?(P~OXmFRHL3VLj;BNkVU+%+9 zclA_v*VI>C=hRG$x~d!oDlsYy3=D>XytF0^4D21WZ-op8y|bh1HbNU%4^25qnA&O5 z6R3b-BcUPz1JjU%1~Ef~$|$b#A3b1TFo*tKuwyP2mM}16b_&uG+CIkT`DjL@i#=m+ zlU!KxC6es24)NHCt+yH!EOx9Jx-a56Iov2O3$4o=fALeW7C{Z=IqUjGDy1AtXfJrU z^=*r46b6zx`Xm*yCv=3>IX*3)ym(A+S`(6^4qss2-M!9aH#IeNaWyqfo^f`)_7y(% z`%dL?*-Sr91yASYTL^ib5n_j@A75UY)SHHYu*0qReL$wFs)?Xsln`K2k5W6b`4wdh z12eK>x9bQNBap(o?F01yyYome_{-6s9~%5|xg^saW`u1VguCnSo%eUF4XrEBXIk`P z1CgmUfy1%O0#WOJTx$7VQD+)NA3$e41ToMj%JE8&&-pZZCWXR&=6HPfC~dL(4;41E z@YnPAV)g{j*wWv^(;n8J)Tzd@Bqy$-gXKo?Q3Xb2=2Mf2X_C>^_WEuPwZlYC%K&UR zQ01&}DsZsiC!f#mGnc}yhv<1ifT1CFPB>@2_=JH6eji~+4>+U3&bNk{=)h<-q__6K z@gLsLj=V{r=Y8-BC+kelpSBs4J`PDmNaj|K*X?J8QUZy1{yBt}~26v@3qn05|XYNGOC?=N8T^a68-O%Q$qL-K4< zuZ^{}YBndGfWSwDM~|nQlil6j zt|U=1+rE3ZPTn!<)WvR_S;1RmCSv{|9eE{*5F3dP!h=(9exqi?`R)VXRbSj(UaMHi zEu&|FZ(^-4ZBv9}x>4Ch-EgMC4&h1gCX}WgG-)=Gc&gr zgPm0182N40sf^n8{m9a7+nHaz<2{y(!yEWYOayXE&>HY}Wt_{Lje1VvnT+mrI0pBa zp9le|q+P90^wajQq;NC7R#V5=6_5G(l)3u;`rw+*d!fI<4~4nJ;9;!j2t@g4q2>FHt;AqY1+FdiFNw^4*R=YQ`70N$Vc}a_{(CbPt&6X^?f;S z_JkJ>u^b4u{_2I2XC%XZ60)&}mZ5FjZf|k*>)KTc;KzYoTHh0!M$Z|~lKk<)#oaBq z9?7}W7c!!HpXowY^#fe}1K|iZi?wX{ju>|^{h|F_qmp#ZZ<0CYR78}o)GtYXaM!KP zQG~YJn0sw1an;0LxLcJcS4m}Vd&pHu(nj*nH`=-o85xVL+R`WU;cT`7 zd_8wu?Uy#t`g(Bw^JR8|(>2CyE>hbbxII1Hbx37jrH}Y|k7eH(Ya^iQDEs`v(3xz= z)$GKl+HPd*a}uicYYxGd&v7IPx!=D2%ha(I<}?YGfF7gv>+H3V*&^f0W5Ab->Aug| zq(A4GyIOpv(AcW8XW*%&ndOigzderOR95$So%h8Uyc&6RU;Ms9xSKkQ$McDibq zGPLJi(AEpS-@d4RFnHu+AMWIpJDHDlwyB$M%)}GxuOpR7-gM9DK6MsQLOUNZBE8+cY?hYpES(kW4~F$qYJrXQt?J+iT-C;NVC6b|F*&y0+>nSl=VPxJS#p zAUnPa*50u_!Uq)PC#vi%>Y2!VEF6`91^_!Fy)b8`l}CTieO=YMzMjcjs>!SO^`&9K z=$PW<8fhQ~Np2kK)f4eWMQfXabq^VSUk~R@M~J^j&jE{f1tUv2_~N&r$sdY&!^`)$ zvBpT6#7Wdr0vdG!qjKKhs2sdKhx6MgV7RIfJ z_<;;5kR}34Zx6Rbj>tU7dBEYad(tQ+Q1tC^q)MB6E7yMJf&tCl>N-&Ew&k)K7Ykw1 zt9HxpXD()vPCcp@m))5EAbzIOc;N8?K0#61_p$~%d(PwZ8xclEF~LND&KfB+<__;c z<#H7ICS8XYms`D+jb{#R7DWe+i5I8B&J0H_Y4;a~xw&2am{V38jjT@gjORkfrp6y+ zKJ)Qi!w+!F-2PRJNGe7i|72vm&|Q`Pqk%d>5w0Z+!HOmK_E#kVDw{~K{#v5iH2>wG z5MP<~3=tWBD2d=~TnP1=r)(fFX^*`6O0=304BjZEma1U=Qh8y%lUlJ7^^{ljuBm|> z^J!;1Jq0KD{AoF>-9pf2n`+@UbmZP>H|=ic9$|IEMz=S}7%cAR_r$YoM3XQ>`CnAn z{@(RUcJwd}8;pK zvZVs?=1O?o5NcfSvI(*6+66-g%!Og-i9$=;A<0TlsC-^?_*-X1-F>B?zUX7KP0l?X zh&uB%>Xyi{=)*PcBUa*p1GChAqH6S6c~PT|twvUz`54ViAN3pTV*cp%_v>ztZf zRv(v@RzLRt8%GK-3+d_diz8&d-)lL@{<$Z{4e5caLdNlL_!?VQW?L1u$IpmzgIR*K zJtK6rZ`V{$c1a}GaE~R$k`(;#`!eBs;SdJd@rXD*c&!-y;HvK;Lp2EQ< zv+P^3TMAp7p*zD?{_KS5ye@A5*6;A?$-ScJx0lOcZ+_CczSmB?Q0Qx$YTuAiaxJz( zM8_Ka-#R_d4NZEURZbd!xfBM3JXl-zCP@nr_rIlmZ?~<9Vi0;v$HWc99g+@Tdnac* zToUFZ*q?)uy&ElRzVH{WYmY^~c3Qcg*2W3;HsdhrmG0WQN&E$oRg1i_W&6?ew0#bK zCee-A3zO#_-3X*H8djeF2{{@|on9#~+l$1!X(UQ@mRD39vor@Z^^XEvk&1Sj>RV8F zUyw=J)-R0A*SGD~AEbP`QCQ!Y1DMO=@y&uF&l<2+-1<@+%$U&#CL;2>Yb|J`QAp#teR zi|<^1cJ_&TM+S@GsMqYsL!BXfd(bT|8HP8w^@GaR!TG}9_mByZqq`SvS~_4(@J6qt zqipAS_rka9?@e~6yt!GDVWV9DL->`^dAY41vCp*Qf3OH0Urpc219rjge~^D=(`;}q z>yZ1L;E0M6SPiB=!1M+L#|0&wx;!V#E7Ee4k&&I8oY>jfX_YG{OU^zF^*xZX`6idj zC6$mlT>#MG9y0xdz+kXe7MiF8(%V#4j^NFnnzSbMTz1;b*T;C%1?kp?yoX54_#;f! z(S>g|f6dK$Rpj^j8jEj_V}2Wm*gvJEN%hs?D8xwHXo^b7VmHu!8#erkq980G4WHsO zm@`~D9QD|lPKg{EO(DOB5=setw=F(Z`>Bf-Afe1!_y#$$D~hbA1YnT|9Hi@oGpK?T zAiuJ?=;YAVdoy!yK{&hA$f1^k zw|nSBt*>Tz7?H^1snr3GgYL#K^8T6joY;ZuIO|Tt#A8Jh0QCi{5*Hum>`K;;ax?Cr z(g<{P^Q1FnC4ukY7Z)3y)zXYT?DVGj=h~|=u!KyWebq^7At|%pPw;JC$OUp-WmQY! zfOh30euHEWYCbh6o@MQxqYd^|QAtqX)2Z$kbmm5da~dnIUBZl>a>)V!o(7Du5!Y{V zC8OW17_ZJ7Xhws{-O`x8*9SXAm}n7Iuj`%T$v{ii{*f#3(( zj?Fosr*YZHtxO{4CCH+gcB>^!r%tBO%G33;m$*XuVG)eW7doa`l@78fQ(Ig0_Go0} zMYvC0ImPBfCHeu=JOO(x&*8L@FL4URe1+AJLDFLi`EJZ~6H`5by6P5^v)Qw>CC`{U zePLo6mc$~QkH1Iv9(U<%#OVot3v^Zb6md|JU!EtBy=Z=o7jC3KFI#MR=w0<8?RRWI zv*%erDdGQs7<;Wn52C=k5fhU7{tK+MM^Khe5GCWV5U#3?&HNTJm@uoIFrwym z*Jp*z2E`w!AFg+Lf9(=r^rsB-Z!@o0NiS92UzZDXNi~bmU@K+&N}zLhN}$BG^hT-Z zc?CSS{9!^I{Lsgpxvkr~=n&SvWYz#LS$}&;-7g<@uD{n|pLIjr_=oaf`4<+)4*?Yg`qACL z=)PMt&>g0=kAfKY3-y z?k`U}q!5t;8EjU8#8kCt6javtb?TqrV|cGjVk9K!BU?DpILx8C;M+?8>uCMG64itW zmEQg1-aKkx7B53wKeo0KcM>2XiW@qAG{2rQ-U z#p^&SsJgXV@6G()P<5gRXKptgOvcd6nlUhNon}`t?hu(DQW?S34Twp0^%7rR6Lnp> z%qiskZH~$$r>f9UHz}(- zI3J4YdX{oXniVR08%a5T>QqdMbrRq2N9(JVaKHR zYOo+9#QcMbcs_u@_<8|yeTe=BTr;@#%D)M90Tm^;- z_Y6}J;j0ZTp}qc!z7yL$cLU*57CSg5LWS95LGN7a~nA@J^`&Y+1+OrW)JP=#~_dy3RCariAy;0F9-sK z(|_M`pM*H1)Pz#wCc^S5duN!6j~!Mrj+isZ?e-Cz{UsA8mVYl4dl4$Pe)?0F7 z2Klp>g%F2QMu$fr*+anu_%6lgKZ&-05}DeJD&{{lVP*gaVyrv13g$W)N);kgK^3WK zV!7<`JX+vvOzoyC<_wflp)iJAX!{W?g;P_x=Y>DHqJlag^9$C+WkW`swbd}qYlf-`czlO((vN4 zBy^BjC5_HFN5{fcr)It!TDDZ0TIAPoZm=Cex4=G?*4kUG&Z*a3oG>sdfKQ~#!B)dY zFhkWy^|4z_VZX_T8podf{^drYgE>83?Xo54X;^e?Q&S#o6&q?{XiG1F8t~r?>V_&{CjaU;0AiI*`u{B!O!^1n2xf52^%N4=(u3w4Oi(9Ij8t)eO>A_Ab2T+?ebb!TqH8c8xhto z5JGpT_(8|~Ne^x@A^m)?Ds-IZva`P|Spc|hLw{}p41Ie8Z(SD$?tm$^EqKl_ahCuA8-mF0+PKgKB_^0N& zsV$@O&&7)l#!ts~`e?}aJdU_`j&o7TKTRvl%q&`Zgdb=YD|u#uOwO4zfLz`@goX-)=l2Q86$>+9xvJM`x9LA*1iytb-`7Z{8re)Ujle zP5@Pq-2ON2C*KcAL_X?Pc)&a>_BFZ%#>msQ3->g&I5=zbutqaVS@Qj-&Uc5OSKz(0 zqez-|TJ{D&7DR2chyv;@#Bi~R=$|DllKj%_!Wog)u84JoOLTj-66x=m&F95qGC>I7 zHH{gpEpWA;mWTh%rMU1jT4(0nitva9MFfCUKVjr6=RVzct&a zvumRkY0k__ff_8@{1I4YLK6+5YmAVTN8grf^Ko{?Z=Sm1P8vOLC=UIYn$4LMGgvkb zPEJ*Igog zN;G?r>qJV)LZZq2;CX(hn3Z4fKl}b*PI&h*PIp;e8~=`5)`eOwQP^Ojuo{5XsAnnF zWjGu9{*L&awTNov;RsliZpY(x9`)Eu_PS%u<^TyRL?F+sH;07u7~mhmo^u_iOZ9WM;Ov8)o0cjGf_Xu7q0H8+pA`x}DWleeyE)uOnI)dJoGIi|lYc6`LAHHYhc* zV7Ral>AGAZR>cQiUMbX9D|;e}-eE5GAA`{I86PXV-dFJLDIi;69q-NR1iuBlrVq=PF!!%+kIj| zNUl~$%s<)b!6~$a>X;rsY_+((TeF{lztA7XQnNR0h_6bubWl9GiG$qTqn{KXF)C|JIhZu_PuouRLkCv>B?#1X6G;!DayCR@0WQC0RWILX-$LA z{>ZF&nIFpEA_g#__qcXNH(qVdfTLIT4ei6=qwAPaRw}Ec>pC0^UC*cn%g%(@37A zES0}oR>fmWwL07CP2{9E8E^d2HA?^EBCu`V2|1a@4PJ64+lY;>UCmQAT zyXU+MHb15Hrjx3#!RbDTyppsf!fw(v5`uhd?M9N+-j<$aMaumZ_O3Uj|B-j?dao?k z>c&2aJ#y}HBq@F<+s!pesxskaNx|XE7UfNk58_$*URHC5l|<`%0OB$lqR6W(b2wwHo3wXwz7o0Szkp09_s(lA&1uE$&UT2zoXm3 z{+IVaLHvI~J`X6lXVG52{d_+YXnwK5;QZX-!zT{q49eIdF@-+|gE-Il&g75F#t)rD z1D1C)>%wx*?*Wja#D7ISvPg`a&`V9~>}>-G31lSJ9f&#|k5VTn^{IyJtHrU!hrCHv zLwB<7z-V;eP)cOn+0+LVwzDzBUP~D_bBJ~dl!0wQF}!(Jj2y>VCo!?#uFVxNgwVTf zEc_u3^&jtf0w#HNzRExIQ`9X}HZBHRPxS%s#O}BJ2bG{UN<(vknx&c8UCcvthBwnH z)Ih(Ag6H9l=WPNB=xk}}V}*b}XwNdtAehUSfUynx3Nfh8)U`CW1U3Q=j^B0#5y0mS z9dcUeIBLmWm<`KxRKfQAy|Ei!&bU_MnS^I7C}{oeD5E;yPRu$6#zAVkf(m(XBK!e; zwIWI-Kj0AFHQ!t;EJa=|^smi8BkA3_Pkuz9WoYKff5b8x7MgeEQR}V5XAMlauzCdu zCXV{a2&5K;^@Z0f{&7d_R2k%$w$&AV$i@eCcCy;sk@$NDYw;i?qb%~s-Xk`?&QmU^ zsb literal 0 HcmV?d00001 diff --git a/images/mba1_before.png b/images/mba1_before.png new file mode 100644 index 0000000000000000000000000000000000000000..120993d67247184a63989747cbbaf431024c6e18 GIT binary patch literal 17511 zcmbunbxwJi#@%L-61bg1b8eC%C%=5AKrS?(TY#;1=B7xm@^~%zJNs zuWG)Ts+m8iQ{8>~Sf9Q2+Ux8~sDhjX%ImkUK_C!{YI} z;=|g_l1*iz^VXlrXvmM7F0ZdqV%Jv^^AHnPzQ4r@w4f0AhUiS7Nsb=a({je*@C0_q zaM&IhNyeje2ufbNfkxb>?X>XkY^Loz?0m~eu8fF`WcH!{z{i)CoJ>On$`RMq)s>P8 zO9T1f$J)UupAE5f&IwecK4WnqMP^DtKkuX7+;8mE3=>p%2cEm(u{m9^_mR6d#jJ1R+DOug=hLN6?|S^y zahlw4EDpZ8;A3DKs$2)x2CFT7+eKNxAX1zXUcs*Mj~~RD+X+T+w2}zg-|fU}w7+-u z;xmo@?fp7>z)8=>%+iv8gd_<|+@@hI=;6VGdu7CG%bBEZU@mQsWwf+_se+;dVQm1{c$`wXd1Cw4#z>ddtlbQW;>~gO6 z8y=+zw#BO`R-KIY?XdtQLBqpyWANKp9Vryaa+^K@UnzSVL_-uwzerY{2SCDH<5$jM%%Jt@jqImdnY=ymELyN;-Bs*y#N< zDO*!yFC=h%SPZsq(;QQpFf>llL9M%9Gu18i{B8pz6w+=5cFUJAf~EMHcJ@SH?)m5jukBQW^-CE)7qXU4cHQ}fqjN4V z#rvgpQ-bY-+m5w8dx*6`HcnkI)LIaM8OBZb<>?x9-2 zyO}~X6&!)5^hkzP=tGQm)01j*n`_CoZ9k({tff#(E?4?-&czN`Y26QRC=WtKLo?{j zMG{u5lBg`SXhR;)4sCs^^WjK%?m_t033S<8SI#Mj6E#p|$d=&mM2* z9KihUaGRnswI`JZW7BWWPRBUyoZ7k`M z&^qBFKD_hJ{`pg7X~3^;Bi66D9jy0;C$LeNeU=1g$~###Xr~t-#g>V0rF>y*JbAiM zlJ_dKSezL}n{UghF_PhBxKwS_%7x{hU`VNY&%zlL@-k#Q%jl7B*kgFIIozhH{?NaU z3e)x$)JiQB7cW`8>y{uLG@;yt`Hi6O;9b}4nDh0|7yU^6g#yi9ZV+cvG5l(mDsp4V zCLR4KMT;(k+3%MUh?Kim;;W09kl*Pi?RDNq{jA=rH+6|%u}wc@ma&j|i{)`WZT+g8 zs_BGnTFtF@em_*zIH{?WUT>>Vq!Z~ImHw_n z8j&;B)R#g!)%Q?kM((D!dnpeqO6-dyt2*j;qfd`lvbxkz%q>ydKh0}xvQ$UVdk$2J z!_yx#E*56y*2xJ8RJH0-QN_udpOQx~)K`#h7enk`^>jx}THhFFM(ls=j{V?i>`~;r zxH&NXK%lfMhM1Bk!)^BdkkTk$_V^AtGbODqBpRiPCfFDXH@h?!!djM&n2_g6r!q-e zXdu&L`N?aLrt=jP>UpvleBvO!$6yM`}pp$Vs^k)eThgj ztc2+CMdVbgBYeJPXLAG2E9Rrb@>d_??QPjGJWlA~6!_$ldg#hqgk8oAd@lTj)l(2m@Qkt{N zv&x6sG4CBRSwEz#ZDb@W&hC|uI)L}ek5;I=!y;wW`}UUFJKbTrBX3u05m>`mTz#-d zec@oSW=E^FPG$&4smihZMPzq5)^w$_ns}_UNxR?w{(kX^+`?(f^|x(F?Ptq?t!kss z2;LNu)2yvHBMC~CMz|KA?1X4Ld*%YA+fR7o(!bH=3#wi-*v{T^scZAMaQNk+>lSqoGK)y{yRnm%3XPdBe7|aZe9Nzld;FZ?}`I zjS1RMjfWzdI&O@%q$Uh1sw!)qdQ0)~ljjdR#3%YH^q(G4UV1Kjd{)mn&oetc6&>E3 zwpk=CZ2=P(Ksdm0Nozj=zN85Y`t%#YIx&T`D)TU^}ZhySWYA=I~$|efz6ru z(YBx`bhz|d4X1`AkROw8K0U)6jcIVYYjBZP4`kt0Rdg^Vzu7r$<&n=-E^D zU5l5C8nxj53tejuI9PlSw{9;1yVZ*ab4E9|8rTNt{ihB`o#wH*`y3Xb!2AyzdC0LG z#CnQ^W?V$!tj8Jc4~d~JE04od370tlj8Q(B72_v$=atk9+Uown2om_sR0u(4sKT8X?R!6+i!5ru~F6U7+U#Jo%YFUr! zu(7Tz*NACr`*BR>#d^l>N|5!@7Usnf9o&-Rl&s@UnxOY1#a~Nf8(#aW+^Nsn`%<@Q zY!^3K;^y}zd0>nDqta-79TYk{Ow9PWu9{FB^Ef${%MaL{QXelh^}=rX=)tjJ@;nut zo)9(pqYyjdsC8VF!VM3| z6Or}9Bd%Nb654UFwpw#eHQVv)>>5@+>1cppZ6J!N*={fE~DP)^sE6-RvDqcvmmr6Dc^!KG8YqFInQz+ZGpxc5rtwY>elBx>& z#x&_%tMYrBg+83N88p1@$TuTEu>vA%(sK{eOx2YXRiu&Lttz92pfHOzeYB) zg8HVMvAfs3`BbU@v}R>Yp&HeMOX8SaBWhNB=8Sm)EM36G8$>Dnptkpvw9Rs9a^V;2 zIKO_;UohbDMDt)Ws^fzHG7s+}r!Wd~`n=xF*K5LfB!)?Es=d;tk4)ts-yb}dZXMic z=yuK<2}ut6dT(43iY0eFr0$Gi)cE#+jFm5+fPZ1vss0w>$)3#S|7V^tW23?=%(*u^C+Za6DcVe zw5yEF2a_JJqabZ}*WM5QTC6-MGdM%U5}Hc0zuqQOVw;DLC*x9^UX@Wd)v`32B)FgC z4p`BA_H(oTHk()*xi`bUB%=Tc`#d^2N~c=Z;&I24zZWEl9$&*ExtA}UbbWb=jfZ!E z^YHo+@{#|+>8{$^ofvbr;QY?QF8x<1d*-73R&T4lVu+<_o5#uJ6%qrAG zAvH;oxhR^6U96*4T*pgHDJ~m8`fcA|JT| z>VwFI1b*fo`5{w`-7amwukw0NsMcoGn63N)*AD{?1fHq-2}iMlWN*Tse1k+IAh>pf&n5`86U2fKrv!qZWc1Z6cOxt0dOr$C?$H}{r$a; z+a3is42ace0?mUx)r(8!yo@Xvh=F~$*i-F-s@-bSfLDE71J3Y)QV+N1pT!3%B5os^ zgBWw4H!gWrJN)kATdzLGhi;wW^9MU~I2Uf(GU_(VZ1*798L<#)!xz!1JMUdXu2!>7 zOjSPJUaN6&Y)1M;M82U5?4b!sDSw~?5K4Ci9Q!t;>aA}SL%}!LNf#nkC{`0s5 zZHoxbA<@%HiFc`iwRJBETIH9!epRnw&5#dp&;t;aST0oo#V8h)<9feBrnu z(e@bX@Z@9&rgBzO9isO!!?^asYN~f8HnObR%1f>~UTyPq|FNPouHB;4;+e>|Di)o= zHP`p7emw&YbgU! zG9%jwXopj*ziJKF31p0-&P5MM`k3iY-Xgnc&deQ6OOw={;Tv2?O&U_M?c9#0&ZaN# zFlVl89a<8oRIzE;7FQ*f-)omNr`2_v)n5{xDr@SzUl!WijgoKoahIrsOu#w~_$|J( zsrERL{!{IlhA3Fwath7VjuV^|56o&E@a9nWG8Rd-6)3}0WZM^O8rRH3!y@XkWNhMb4jwWk=SU#)VCSosMaRvAZbRR1^(gogK( z`pkA@Ii7zvV$5W@T0jrZJ#|ueU;B;s+@jl|1GI)2ooVURy7$3G=dw#e)RA+cwCZB2 z^rm_T-P`n=>`8E!!Tf@~D%q`F<3Sy`Leu%O$40Q**Uds%2B=9S3n$;IG?qZ>ZO2H={}8Ad9sg}B56X2t7+?Qes&LJ zBUf{K;wLJZf7a{plrX%hglfS8%&~H`SFSG$Tc?sI5ZvnxXI?GLT77<(J1+errZFv@ zZ;`3cM2sy{CoTZ`_}UTGybXcncVdtlv%h6`KO_JHBAJ+uubGY0)6R`+dioaJ9PV2` zh*nSZg^qJ2KZ|WW99-3Sx|l&*K7a3;s#1FD;wv>2{zm_#@AiAbO?;W*HTFo`yRfA9 z6yE6vjTjn;oNAnv$2;9z?^gTwP)L7Ix#w9G_G0#~KD-%(49{|7qaEn43W;xyWq+Fu znq4L(swB~yztKmh7ES)(y&~G!zZD?NX~d(I$vF`{koemo5Il*Ze)EI;9&=y90Wvgu zv66x)D%27@(4186IQp}%`XJtzZ>-T}&679#3}{tm&7nWkL_imLGD~ zRGq|lb#7l$_T!&1%7L@X!B#IvI3mD4jg*#8Ylm?OkRgLpNCez9p zFV>CK;fmuMAvn?8c`Gni!>%duQOxHdBD&yJHsTVzFB=<&EM}$&29SpJp^l9Egli|} z=`Q+}z-ny&OmEhpgYiWfu>J_w=ei3-%LtAMp$Cz6M8Ny}fQ3^2yA%3djK zYtr*FB;NDCWPt~s8E6B5o&(`Z-wEFI@LCD*?jHH{;5mm3II<`t2lu|+P`Ag?X5mx8 zJ@#?VuJajevH{?&5GMU7*4vYyU#rbbUXzx$haoJ_dana&pYO9@RF{ch6?d0Isg6%g z8kQ8iKkBA;$8VAaYOF_?+lhm-J*~TG?$BZ>@`p9?R|E9V{o+yf;6JcZ@ePc_1;AC66tM+5MX!gmKDR8>uz~!V z<+>IHO!_=Tp9X+q?0wEb=FYZM zB9z7qkDS&3|56w9qAUG{-iu7Tpzgsj9pm(kL(be1rvM_selO0kl~kh`f>CBXLT)yR zwy)4n^JDJU5krU{ts~M?^^`)`yZmSi0EV!*-Gf(XGnWXay-6U7iPH-U(NcWrzR!UB zcoCfFE*Ef--k#Yd@sy5PiFr-9(CARFK%a<0c?WqxJ`< zj$e-BTo+?FuWKjg-rS*8)pAx5>@bImZSQ{bAS>#>i3UIJ$htappz@xqk`|gO$|vVn zHalO0YrcH=on~LX*Vq22rfUptu|CJSdUqomaw36&xz28T0}i5<8vm`@o8h1MRlF{TU-#v$K+vOa zC1o5v>7yN;L}N|Pk1qW}$s0C#9JcU_MoCK5mIXUs`wmm*qFNT5?+KDcqDF9fZ*qvE z1Uw@jum$c<;w@?Q>Hpx|39**1fp`&2TQQ(cU$QWR6gzl^!1F)mLs@n?@sstSc*YB< z-Ge((GDDKyRVDLQfE}g1NYB_otB{QjzUMzs$KIK{psC7hx^0`WAi}TcR^nuolrYov2w#vN5e8X?Fz4Z?{5x;ba@T%8?aRpbp zWbo<_Na(WAUz3RKd?z{aO}rp9t8Ef@qZMLT+JldvNQpx%k2m?N1v}zb)gd>Gt#^#swKkv=wByBs-0dKyu>#kcdJwKaQ4F`3|U zQI-Vqj*9N)EF{3T)Di2z>s^Cl!%NTi^e5X1_EM(t(~I-hN9PIrBiD+q#W_+AJ93Yh zR2;j%9JZ;wFkeDz#$5qp*asQ5Qy_QQTM{1}vpQgFI;M3agfHPFR9?f^0{Sfhow}Fz zxKL0#-H`lR?xP%;*Xxu1uZsf2&R_HAOCSv#7F9drZFO5i$U-+2V@qFCPbTzS#SX9c8^h%F!4ytPR^Ba@X7y9?*2Od7~+M8{_V1yCr z=rr0FzWKsuAUIgX+B%gZQm48DCH0@tVc3oYoWMBoYSw&XdK^|I!Ax*dFn^QQu zzDT4w>+pHL+~~OPu!x6s2d+gJb5*ryn}x`k`^;41Y8gLkQH@JHCw}(8JXr9mH_CHQ zJmfoNX<>DHCa;UOdeDh8c~8-5{(4l8^{1_T6^!nMA&pbN$|t$b|H!`|OWVgLUQ-)`Z;pZc*b)jk0;I zpSgb6!2G_z*@+JcJMUZ_&WPDhcJEWrJ4k-D3$kZ`w;K$eE$BWMEiV7+NEV!MOY~3; zQ1?K_HjX|HI@{hlR>9GP_ohFcvo+WrT-ok(c#343{ie&B|48q4v$w~fkiQ+%-xNCz zi}idpT-T=76uQEv>|8CY@^q8*L>G2T%NM%ME4Eg6N;dg6fODt1&Qqu!-evetUZv)$ z`Fdt?xiIDdgJzvpGLhKQeq^JPgc!^}cVbpa&4Jpy#GFL=PAOhWAmX8|jgfA1U_N6! zH_RpBdS>p7#`Zfh%T&lMqCB1LnBg+meRMl_clsDd0O3p20oy3t0cEbiSB>hsybpP!Hl0@?`wveRUu8?h&Df7Cu!x&z*!D;e;h;REp^#MH zqDv0TMW6JsKWe)UrJ7jX(mp-x?<#Zb>CIA9rQ%j>ttaf}N(VNqDrWdPaS7V4TVgkH z$<;?EHbm!5gQp`yaSUz5!V*vFiFM6&sbO}D;pWQf=#8SXjb{nH?#@vECfuVI?TG=a#WibjQi7Yy$5dCTujxokj)@ z|GxPR>JY3PP)6;=TU0!O!SCfvA**wdjgO}j^2pmOv9>JWS$Vg;0U0Y(`XwUZKa{T$ zc`wPFGvzeDEBH+xy~OOQ_=e9ZG1C(xdU=o5Y8Lk=GFpYd#v1fgN%*Ok^ghvRP`2kt|42XC z3wt-@lK10QOp!6>KBEkjvn@Tj{^eD9(dmWK?QXl0$<2tn=kW9=_w+&C5*)>Uk(x)j z_}kY^H;r&mN;f1-wR65YE0|{eHgHTfdTa?axLSTJy?m;W)Wz_opj(ksg)*w=66f!C z)~ePJF4s?OAqmW1BJ}j97seQLd+8LPky*X=Bud1s^DTBy;A#*ygtbGI;CN@X@2n-$ zX7JW7uOM>TCh8a2xE*ytIkjM5^y5ZKFD9d=rcO#})Qhbi7xOosh+@e9B6_F%mH^T} zux6yTw3+;N^$3zQd2;y;5KB@&6V|cY3(m46EZ_<~dffIo^8%ooe_7`lzA0DQ;i2;5 zVre_Raq0WRTkh*-yXzJ5a4jYzpk5Ex2A5%1=St&{4zXc7p-H63VWCKgc?c1)etBf2 z1C|wST4f&zN%Pjcrp>qOizgn+XC6(e^QH$MTP#AZLN~Hv+hvY~shSRTrOwVS1x3q9 z@DT}ei|Ij~_xPQJ(3#0lH~~OvPh3%hBlCrh^3K zRvre1@g|_l2(*1i1)3B#MmN<;F*%VNsL8&eoa?1YzV6G7SUYq&J9Babo_|F_UjI+u zjmFvcAxX^#n1TlW=8tK^DV{vcm~;;AQ~+ou4|?mJGFz$btD z8T_alX7j{V|%@Q(ZEtb>`UVZF>j{-&*p7ytOp zNooZ2U?3zfE*a9q;=W+0AqUA zIPacS_$S!RvfGl50WbVeLcW(B;Ok3d_;ZAdQ(sxW)Fq`fKWk&0YHKLQ2~PlI+W;|r`oK|w~ZNnhs`6bxYlwJ=G?5STLU`ZU`i534P8 z_rYlV2~4b))MEo9Bk@?E>R;vMXh5j+@iYP=`|i_2)WT{@pL60HxM!^sy*VeBzniI) zzk5v~IPZn1mhcO-p@|F_(1-Wcz#c7D9Y$>D;pN3J?I@XAkBIhu*pLD~=qt7ZAXa7G z?g~UoV$#h>OUvuvjMe7>eWVYY<}$o#D%Wn|W?<&NgKlolCKXykdS*9~`|O7VlFz2C z?&%6)x-87hc9$9*uq|Zd<%fX}a7sqG5pl=Bzzetd`DTWm+v7HIxmmEzYZ*_zKF!)( zaXX{kQD3AxX}6pO5nTrgh1#}5ukS8)fc%r^!T!;e>BC1V{*}hgp7@i-`PB3A$L0=)?x>~GBN}s^*`!_1b=<1w#;nNG#i&Elist!dZypgIt{0>=@7wI)v>%(As$u>7 zA$ukCyIeUJhjYn0ZMkoV(r>WS?TefHupe&W58%S$e^Od1-z_1v0O+I+ETiP~bot}H zswuDgyzN+pDkB;+kjVIOSJe{EYfhG_u$%knM@AFN-A=bHN_{#$-wc&1(%7E~6O|TY zX=Y1-u;9;!(&a_e3ZLmzwrBxaBP8ud1ZyHL&h$$BQ@33|OyLE{@QHUV$XoNXtF&Sa zi_88w`IEb`RB{>_hDnLMyzU9H*{Kae{*mX$ZS-!L)~SUTLy4|*!p0O^p*r|ZPNi{u z)4M10mhZPuWhPK3_AAw)1vSdGxJWTYajCfK@k)~&JiqK)T(JA)Zk*LvJvdGQfTA&A z86$1ibzR&Gwn%)~mDtJfINxmwUXf{$9n-V2TX)KKOrkdWA#~z@ncowI^OK#ZQBod&bCe{ANJ`U9rnd zq6TxPRb5q*dP-+~nQT&VnvMr8#fnJTUGvT>#Y*bQZ^?uY<18)b&HeMqM_+!5fD9N}%?A-gwp)?p9n?98EmqoAgVe~U zRf&SsrF}Q%kAC3eU491Et!;CsqfoU;Qqyn~B!N+?yls2p=-qXg^3ikI`LKA{rR#h} zBn<^4!)q8YHThUWpJ@?QWc~H;lKpd5EkFR0!R)r{JKH#^t7}`FA8cx7(7%7@KhvsA zw6M6A_6v1p95c!bmKfnpC5<&YAwTA{3DOGn+FQwSAvC#@4x!Up_3_*(jj?@bWGK+s zMbFo?&L0=oi?&aH;01RbdAhMoYwFkD8N=kKPyCm7JvjVw}3jx{5viR6NRFrNlYrjmiF& zhWqfHm4IuPJE5o$1BqTXfs{gpm|W70#5F^{(OB&#VCs zsy^Ry4w5Yr$y4Gcz>61zO|J$%4M-3(P&cIeMXar@CF!KNUQO@athj58g`1WpyfObE zU9%c!YilbnEj>Iml+!LLDH$3XIt0A^haqT@RYP<2Zi^|HdcbufaYhq)7n&pEZHtmJwgYc{yenc>+ z<$pf^${|??L^#j~r2nQE)_T%97$5&G19O|0k`e~4eE|vpt!BcYV?Q5!k$wD!4*9IB z0dnO3x(I5X88Z4=rEC%y#PQ`hfvRi}NULh#5R0hCZJX>vz2{7%0Y-|lj!fhRmsC-} zoNYPXQ49N4KTgNa>N&kAtx2V!mQjFRIDL#<`alW11}jW99y03pyCx0vO?I zyC6BCn9|%|OIO61H_Q!9@|zIvvv!{O)*MUpKS*?1#c7G(_6fKSRol9u~g^Vb^0aA{T zUp$-Hfdc^1Vah+pdl$pRvO2qw8!Zik@*}+wSO7E#hVbEa-IqnneK`07 zi$kx>NsRR{7Hke~i-cW!^?NrAtazXk?MLICk9`Ur2*1SZd{ia(=+oT6dG&P>Wb~_RER=98Q=EnY>PHZAD<^ zdlrF1Kt1?8u=uS~oT4lwJY<5>DLR#-3*&lM`#5&MHYpjTg?w1*H@g3#K<8%4B`_kq zN~j-^69G4qRYKNhanA6;sgT%x%U3)YnZY${;?FXnQinwA5J>;TBHO#BDz( zxzhB-x}b3XljpFqveK-5<%&;3uq>6ap|L+m^5Lc?^M&8?^z=MBIx;smS65fRD1(6JK zssxP0CWE= z&Ues4?P)3_{b8z3eu9BQgXB284l`5nbRAMb@*&xq@GyTgVzyn@Hv zUmH_dX5k)+OXc`wy25S93UC4BN#W%AyuYr0Vfa45npN+6rKm+NnE^%|W5cW)7-3lI zUW{%6%n}K(v6?gd^-4Z2J#YdMbPs3I>fy9 zJ**h^YwU8o;?o+>k8tn2@cyJK=jO!1Iptc|E!VLo)zs;k0nGdIV;aVkl@uK!r)mn_ z!^ZoM#vcKQRRq}u>F(jH)F%05=p92T1@g+7#;g_GnO`j+08n!;e5>-iF4B^m`q5 z>*E`wL>D2b4!>Nbp9(v0_)(}&wt*$?^8zGF5I(gRFL@Ce9X*U~IM^JNHeI|Gpqrka zo}8Q<|CNhS3e^Wdt}b7OA5LrKMX}a=Oc;6Qw&tPOEQ@dfg#9 zNCZ|&*j38gN(FTx8hJiQt|t;DpQ(70dJMeeyR6O`Y0r3U0Rv`v2IcotSL7C@BmdRL z1T!W^{d%h+f8Yq@6WZT=>aG<^v1C%r@VR^#HfKyE;%JIg^g_%HT&_E5tytp-)rg?f z6p^%V{Pejg*P{IX`&B#0T4h-tt2l<>sA!*Il3{y?e1s=DXAckv z6$wU{&*_A5x4FVSlaT_P)y5N=IN%Q6w0F+#?edozy{-`g+ySxu!cu4MC{dlY0ZQw( z{bSmV$2&JBs|Hy)25}*bz!!kypyjhB`R*IC3VUlZT~wSWv|QxIvs8zb-V)Yiplst$ z_xdHs2jOFyKJ8-(sxmx3&9Z;|K=ok#6FI5|=oYk6>84Uvs{#Y^nMXIhO~}w!cE^A_ zuvmh~KJ1za(5|qB*TK(EW@VvN1>tUy_19Bx7yRAzyp(K>y;uDyKV~7eCxIyS-;R1r zTBWu!-{5r4p2~?Lz2<28<&fJ#0|z3t0iXbwuL5y2Y^}lJ3mVg29VjKN7)LkR_r@8W z#{%wTwA52Gc>aC`jCbyMDK|4sV-!K{{$C1E@_- z_%i#4M3y)1i4HBmOZPfQWTdzVQ7Pa_&oMDw z6;@_vXIEA-5)%^>62!dYVq-C}uo3|O*FmuGf5qbe63Q=o(A?ah$Gdvk*$-DUpsq)P z-RjHS{Rf`}D4e>FIxQ7|U;My!w0AgSKaL)GChsiV5_zhG1iV2ca_}G@%V4hVxapyk z==~RwGl_7iqm;laAU!yAQ&){zL1WNe)6?h>vx z)cVwGDK1kayK>&V*z7}@FFOo4N`-#+oiuN-p5fpI-qqQ z)OBQASh2bw+`CPIg^{q?12^>77X1N~nm}+dsjsUn$f2T{C3Dtqi)cA%jF3TBcU)RE zDVzrJ1Ck!?<@haaz8Z7jxrFAY{!q)j&M~IZ{94L2^Gv2*1Oj#?zO~`bD9MN?Ddo~& zK;z_FW}%{djIZ-)1@;5|bMFK__;3J!q4Q^R{ZKLLndN7dL_NW;?r;_J$${IOv^f~n zuRjc+K^zSRFiHPmJ(X^5y&UtpBFWe&n*%70ml@kI3c;hLW*+#OF;%*4l)6#_rDb@- zinn<<357>5?RWNH*jP5QQu`8{>i8YQV<$Z{d^{+oCPzU3TW>hyT z0>0u_)lEZ&{(W_B{)XBp^mZ#LC0JAR-T>HWN{{f5!26^tq+=gMZ6`{B?9O9P%82yi zqXF$&Kg=$cmHxWN1mA;=tCPaD)V|9^)6d0 zny@WmVOhlTmoM+{=8K(|hEoj1sF7@hiQ@E82$?ieb`T9m(CuSXk-465 z+7KzLP2wy*&0)LK7;XjyZ2@QOUk&Ye(pk*g&d%(T4d}nket*ugJ1wrR2FO($CTg(A zpzmq6YoUoUUK_*vihx(d@i$jjwe|Id`T54i#uKY~d3ilOqQ<~toCaP0dq@+(U6zHb z%M2(`1^*CI|M$h3bw!!N11-(jgXc}dgogQ7tDt1S8nQ*w)}s2~aJMe@<+(Y>KW)0H z{hu)OwQriq9uAJibFRTNuLJatZB)$|eZA}h>7VfoggKr$%G=?I zuiL)!%;rM7^(j zLew)sH*FZ!t`#l-D4ByRFZ}G^;Gu;`nY~2EsOr~wQ|D!v^|MKZ*jSraSWkH&)@C`E z4E8;%I--`LMQha>H@~FmESu%eOWE3sZ)gK?)t5xmU4Ho)6^9>C%pn^ou*_xw@HfLgMa+mqSps; z0$yln-t7^@STxOY_X(l2mvnYvm;fjCP7jGa&H%?!#DCgdK}0AX=(qFhU(Sou` zXvn=($~}mOG5)%{{(u>1yQH%*hx{qxb@|yhK%)h*>ithf5sG?QQ?5SkGy;*7VbusT zS@Fa$Uf-bZ`k%s&_e-}~L31R$_#_g5$yB4*iN6W8{W)OHs3OphQ4F*I%#Ai{^%W`g zE+-5SF8rT;({r4FwCt^`J-Vjbcf=g-%7j)O^2qH6t<(UxKXMO#rz9XYnw(CRY=6AP zO!0fCDT4F@1>|Gq$Mteu0$48Ie_Xx))WiXI=3kIkVe?T2$-<;cXsUIGZy}L9X`1OH z>wmB_mf2P3P9;FgaYsq<14NEznzs&fA{_03_BSiOfcY~xWx6qbUTdkB6<`k#|EL$R z)+=h(Fkspu<$@F|6odJhR{L-dn3Q=V!^Y_vIEEt*X)Ck`Nq{0*3xs_HLJN(*p~WfV z<$wz(!1_y9-Vxtj%EUR)C?P3Gz2$L}r<-4Tw(v!c=oq3ZArTYuRBHOz@@yYYnNCgh?_H)}OPv;=0vk32*su_vPVtA4 z7q)LuUjOZCvqcZwcLyX~Pq5G!m|n zowUs45|l41u(9WV+ht``lOp_Wg`HlmP>FJsQ$T=GDT3nUt-VTlB9@nvv$Khb$>*-M zuhiTim>LyaR4c?2ybN;k)2x>A^77VJeg*~xI=b*jN(u@JN=jPbu*#>N8{2fL0)oW? zTdDUDqiRIU^Irv~4wb9q3vV}tm@J->pAW;(U;ItP@=-VV$-lu3;iI5p(~S0zkvyC~ z<)wg8q~>`_wkoC?2h{z4)kHT1EXhaxzb|%)tXtge^6xD?B)7%WsQb!t?WNeys~?7% zFQPNE^V;pN4_VY^xAKE)ac&+CYetZFM_AoA%U&XSNdl76OMnYCG&k&hJ{nH4a1nGp zj|p}+GTB`AgzObAWzI-=S3``GH-Fo6@bl*}?IfENigLQ~jCljJEZ-uS(Qz(B!L^n@yP#Ux0jW0UihMRULD+^qRP6rwSV|w#E5>2E;_%-5A+)2uvfQHRc`O>c7vJS zk;~fKcR9J<;M)q`9Fl~1Jl|;Y`||d?KSY`FN?Hp+yeA3<*mhh@=Eeox*=g%>hg;j2 z`FMTMj%kXY9XXs5n$p^TBIq*PFSP3PUi{ntH>def`A?$RbeZxgkrOL-BNQS#oC?B<` zp451*;_w{;9pu_AxsX8|<`txIxt3;{s5ogbetT=J-Zv zqGy63+O9a=;Z5X%r_CoLnw=LOj;vRQv?k4BZ#tvDghyt$AC$r{>uM7L1H)cNes7NE zeTUI}pW%K@J&MW1?{HWXp@DqbhDJgE=cU-{f@kpV548vRW?d8FY)swH)})H38Q2G- zHlyU5m-AnVZluvpOh@y}Vg=RuG`V_)t0MtgwvM%qY&hJ0t44bwkYywu=J7qe6Mg*& zCa+Y+^I~E(gzA0(oDo}m3X`fKIKbMUfj9alD4CINhTqKEYg4f{p$j1zM>O>niNg8i zswLWa(klIR2<`36B}vYjHpgL%#BYJ{q^)tq6MaH5o`s^5DGUi7NH!p8i{h>$>&|%J zW6V4(n~HC4sN>gkA`6`9>v{fs)BLgc;fJS?wy`G-i7#1Qw*)PEv&S70dZg1kH2~8Z z0KF9%SnJ}*{)ls8tls<29_m~G9D)8#PoYQ@uw8#vC&!=RR>}YX+xSfgFPPECjBD{#_MxC|d0q|4-rH3k&3fK61tNlJwJaZDAka#{Y11@ZTLP{O7Y) zK=@DUY7$BYWP1=9pi+_5H(AQq0SAxUuz?2HqLjdGn}6Z=D;QicP(s#|W$U7VUuc$O zC4QF5l(zP*0ya4aaOHpAW_G>|>V)B~#-WK30fISAi4*gfg5J82CBJtB)o6NZfY#)L z@h|<=3vk2gBH=9S1{GxmLe`52A0daKE&xR6p#l@o1x|?)$@(le+3;NM@I4e2jJmmi z6l4(R|0E$3`V2^a`XlrW_{S9P?(P~I8Y(KdP+2J{DH)kBxIhE8X5gL5k3nnI_zIJ+43fY zl~1eTtG=08QG0vlqfUz}hVBY1MxEo{HLxS@UsIs!h}0jHYetSswu&gGK-_mJX`EN5P;A5@#Lc6;5DeAW1Pf K(K2B@zyA;CxqYSp literal 0 HcmV?d00001 diff --git a/lin_conj_exprs.hpp b/lin_conj_exprs.hpp new file mode 100644 index 0000000..b32effd --- /dev/null +++ b/lin_conj_exprs.hpp @@ -0,0 +1,297 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include +#include "linear_exprs.hpp" +#include "mcode_emu.hpp" + +typedef qvector coeff_vector_t; +typedef qvector eval_trace_t; +const int LIN_CONJ_MAX_VARS = 16; + +// represents a linear combination of conjunctions +class lin_conj_expr_t : public candidate_expr_t +{ +protected: + mopvec_t mops; + coeff_vector_t coeffs; + eval_trace_t eval_trace; + +public: + //------------------------------------------------------------------------- + const char *dstr() const override + { + static char buf[MAXSTR]; + char *ptr = buf; + char *end = buf + sizeof(buf); + + ptr += qsnprintf(ptr, end-ptr, "0x%" FMT_64 "x", coeffs[0].val); + for ( uint32 i = 1; i < coeffs.size(); i++ ) + { + if ( coeffs[i].val == 0 ) + continue; + ptr += qsnprintf(ptr, end-ptr, " + 0x%" FMT_64 "x(", coeffs[i].val); + ptr = print_assignment(ptr, end, i); + APPEND(ptr, end, ")"); + } + return buf; + } + + //------------------------------------------------------------------------- + // each boolean assignment is represented as a uint32, where the nth bit + // represents the 0/1 value of the corresponding variable + char *print_assignment(char *ptr, char *end, uint32 assn) const + { + bool first_printed = false; + for ( int i = 0; i < mops.size(); i++ ) + { + if ( ((assn >> i) & 1) != 0 ) + { + if ( first_printed ) + APPCHAR(ptr, end, '&'); + APPEND(ptr, end, mops[i].dstr()); + first_printed = true; + } + } + return ptr; + } + + //------------------------------------------------------------------------- + // each boolean assignment is represented as a uint32, where the nth bit + // represents the 0/1 value of the corresponding variable + void apply_assignment(uint32 assn, std::map &dest) + { + // recall std::map keeps keys in sorted order + int curr_idx = 0; + for ( auto &kv : dest ) + { + kv.second.val = (assn >> curr_idx) & 1; + curr_idx++; + } + } + + //------------------------------------------------------------------------- + // the i'th index in output_vals contains the output value corresponding to + // the i'th assignment, where the i'th assignment is defined as in + // apply_assignment. + // the return value of this function is the corresponding coefficients in + // the linear combination of conjunctions that would yield the output + // behavior. The coefficients are ordered based on the same indexing pattern. + void compute_coeffs(coeff_vector_t &dest, const qvector &output_vals) + { + dest = coeff_vector_t(); + dest.reserve(output_vals.size()); + dest.push_back(output_vals[0]); // the zero coeff = the zero assignment + + // we can think of the problem as solving the linear equation Ax = y, + // where y is the output_vals and x is the desired coefficient set. + // A is defined as the binary matrix where row numbers represent + // assignments and columns represent conjunctions. See the SiMBA paper + // for more details. + // We do an additional simplification, noting that + // A_{ij} = (i & j) == j. Also, we use forward substitution since A is a + // lower-triangular matrix. + + for ( uint32 i = 1; i < output_vals.size(); i++ ) + { + mcode_val_t curr_coeff = output_vals[i]; + for ( uint32 j = 0; j < i; j++ ) + { + if ( (i & j) == j ) + curr_coeff = curr_coeff - dest[j]; + } + dest.push_back(curr_coeff); + } + } + + //------------------------------------------------------------------------- + void recompute_coeffs() + { + compute_coeffs(coeffs, eval_trace); + } + + //------------------------------------------------------------------------- + mcode_val_t evaluate(mcode_emulator_t &emu) const override + { + minsn_t *minsn = to_minsn(0); + mcode_val_t res = emu.minsn_value(*minsn); + delete minsn; + return res; + } + + //------------------------------------------------------------------------- + // eliminates all variables that are not needed in the expression + void eliminate_variables() + { + for ( int i = 0; i < mops.size(); i++ ) + { + if ( can_eliminate_variable(i) ) + { + eliminate_variable(i); + i--; // the mop at mop[i] no longer exists + } + } + } + + //------------------------------------------------------------------------- + // creates a linear combination of conjunctions based on the minsn behavior + lin_conj_expr_t(const minsn_t &insn) + { + default_zero_mcode_emu_t emu; + mcode_val_t const_term = emu.minsn_value(insn); + + int nvars = emu.assigned_vals.size(); + if ( nvars > LIN_CONJ_MAX_VARS ) + throw "lin_conj_expr_t: too many input variables"; + + uint32 max_assignment = 1 << nvars; + // we have already gotten the value for the all-zeroes assignment, which is const_term + eval_trace.push_back(const_term); + eval_trace.reserve(max_assignment); + + for ( uint32 assn = 1; assn < max_assignment; assn++ ) + { + apply_assignment(assn, emu.assigned_vals); + mcode_val_t output_val = emu.minsn_value(insn); + + eval_trace.push_back(output_val); + } + + compute_coeffs(coeffs, eval_trace); + mops.reserve(emu.assigned_vals.size()); + for ( const auto &kv : emu.assigned_vals ) + mops.push_back(kv.first); + + QASSERT(30679, coeffs.size() == (1ull << mops.size())); + } + + //------------------------------------------------------------------------- + z3::expr to_smt(z3_converter_t &cvtr) const override + { + minsn_t *minsn = to_minsn(0); + z3::expr res = cvtr.minsn_to_expr(*minsn); + delete minsn; + return res; + } + + //------------------------------------------------------------------------- + // converts an assignment to the corresponding conjunction. e.g. + // 0b1101 => x0 & x2 & x3 + minsn_t *assn_to_minsn(uint32 assn, int size, ea_t ea) const + { + QASSERT(30680, assn != 0); + minsn_t *res = nullptr; + + for ( int i = 0; i < mops.size(); i++ ) + { + if ( ((assn >> i) & 1) != 0 ) + { + if ( res == nullptr ) + { + res = resize_mop(ea, mops[i], size, false); + } + else + { + minsn_t *new_res = new minsn_t(ea); + new_res->opcode = m_and; + new_res->l.create_from_insn(res); + minsn_t *rsz = resize_mop(ea, mops[i], size, false); + new_res->r.create_from_insn(rsz); + delete rsz; + new_res->d.size = size; + + delete res; + res = new_res; + } + } + } + + QASSERT(30681, res->opcode != m_ldc); + + return res; + } + + //------------------------------------------------------------------------- + minsn_t *to_minsn(ea_t ea) const override + { + minsn_t *res = new minsn_t(ea); + res->opcode = m_ldc; + res->l.make_number(coeffs[0].val, coeffs[0].size, ea); + res->r.zero(); + res->d.size = coeffs[0].size; + + for ( uint32 assn = 1; assn < coeffs.size(); assn++ ) + { + auto coeff = coeffs[assn]; + if ( coeff.val == 0 ) + continue; + + // mul = coeff * F(mops) + minsn_t mul(ea); + mul.opcode = m_mul; + mul.l.make_number(coeff.val, coeff.size); + minsn_t *F = assn_to_minsn(assn, coeff.size, ea); + mul.r.create_from_insn(F); + delete F; + mul.d.size = coeff.size; + + // add = res + mul + minsn_t *add = new minsn_t(ea); + add->opcode = m_add; + add->l.create_from_insn(res); + add->r.create_from_insn(&mul); + add->d.size = coeff.size; + + delete res; // mop_t::create_from_insn makes a copy of the insn + res = add; + } + + return res; + } + +private: + //------------------------------------------------------------------------- + // returns true if the variable can be eliminated safely + // i.e. all terms containing it have coeff = 0 + bool can_eliminate_variable(int idx) + { + for ( uint32 assn = 0; assn < coeffs.size(); assn++ ) + { + if ( ((assn >> idx) & 1) != 0 && coeffs[assn].val != 0 ) + return false; + } + return true; + } + + //------------------------------------------------------------------------- + // removes the variable from the expression + // make sure to check can_eliminate_variable before calling + void eliminate_variable(int idx) + { + coeff_vector_t new_coeffs; + eval_trace_t new_evals; + new_coeffs.reserve(coeffs.size() / 2); + new_evals.reserve(coeffs.size() / 2); + for ( uint32 assn = 0; assn < coeffs.size(); assn++ ) + { + if ( ((assn >> idx) & 1) == 0 ) + { + new_coeffs.push_back(coeffs[assn]); + new_evals.push_back(eval_trace[assn]); + } + else + { + QASSERT(30682, coeffs[assn].val == 0); + } + } + coeffs = new_coeffs; + eval_trace = new_evals; + mops.erase(mops.begin() + idx); + } +}; diff --git a/linear_exprs.cpp b/linear_exprs.cpp new file mode 100644 index 0000000..f82c030 --- /dev/null +++ b/linear_exprs.cpp @@ -0,0 +1,149 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "linear_exprs.hpp" + +//------------------------------------------------------------------------- +const char *linear_expr_t::dstr() const +{ + static char buf[MAXSTR]; + char *ptr = buf; + char *end = buf + sizeof(buf); + + ptr += qsnprintf(ptr, end-ptr, "0x%" FMT_64 "x", const_term.val); + for ( const auto &term : coeffs ) + { + if ( term.second.val == 0 ) + continue; + ptr += qsnprintf(ptr, end-ptr, " + 0x%" FMT_64 "x*", term.second.val); + if ( term.first.size < const_term.size ) + { + ptr += qsnprintf(ptr, end-ptr, "%s(%s)", + sext.count(term.first) ? "SEXT" : "ZEXT", + term.first.dstr()); + } + else if ( term.first.size > const_term.size ) + { + ptr += qsnprintf(ptr, end-ptr, "TRUNC(%s)", term.first.dstr()); + } + else + { + APPEND(ptr, end, term.first.dstr()); + } + } + return buf; +} + +//------------------------------------------------------------------------- +linear_expr_t::linear_expr_t(const minsn_t &insn) // creates a linear expression based on the instruction behavior +{ + default_zero_mcode_emu_t emu; + const_term = emu.minsn_value(insn); // the value when all variables are assigned to zero + + for ( auto &p : emu.assigned_vals ) + { + mop_t mop = p.first; + p.second = mcode_val_t(1, mop.size); + mcode_val_t coeff = emu.minsn_value(insn) - const_term; + + if ( mop.size < const_term.size ) + { + // check if a sign extension is necessary + p.second = mcode_val_t(-1, mop.size); + mcode_val_t eval = emu.minsn_value(insn); // eval = const + (-1)*coeff if x was sign extended + + if ( const_term - eval == coeff ) + sext.insert(mop); + } + + coeffs.insert( { mop, emu.minsn_value(insn) - const_term } ); + p.second = mcode_val_t(0, mop.size); + } +} + +//------------------------------------------------------------------------- +mcode_val_t linear_expr_t::evaluate(mcode_emulator_t &emu) const +{ + mcode_val_t res = const_term; + + for ( const auto &term : coeffs ) + { + const mop_t &mop = term.first; + const mcode_val_t &coeff = term.second; + mcode_val_t mop_val = emu.get_var_val(mop); + + // extend the value to 64 bits first + uint64 ext_val = sext.count(mop) ? mop_val.signed_val() : mop_val.val; + + res = res + coeff * mcode_val_t(ext_val, coeff.size); + } + + return res; +} + +//------------------------------------------------------------------------- +z3::expr linear_expr_t::to_smt(z3_converter_t &cvtr) const +{ + z3::expr res = cvtr.mcode_val_to_expr(const_term); + + for ( const auto &term : coeffs ) + { + const mop_t &mop = term.first; + const mcode_val_t &coeff = term.second; + z3::expr mop_expr = cvtr.mop_to_expr(mop); + + z3::expr ext_expr = cvtr.bv_resize_to_len(mop_expr, const_term.size * 8, sext.count(mop) != 0); + + res = res + + cvtr.mcode_val_to_expr(coeff) * ext_expr; + } + + return res; +} + +//------------------------------------------------------------------------- +minsn_t *linear_expr_t::to_minsn(ea_t ea) const +{ + minsn_t *res = new minsn_t(ea); + res->opcode = m_ldc; + res->l.make_number(const_term.val, const_term.size); + res->r.zero(); + res->d.size = const_term.size; + + for ( const auto &term : coeffs ) + { + const mop_t &mop = term.first; + const mcode_val_t &coeff = term.second; + + if ( coeff.val == 0 ) + continue; + + // mul = coeff * ext(mop) + minsn_t mul(ea); + mul.opcode = m_mul; + mul.l.make_number(coeff.val, coeff.size); + minsn_t *rsz = resize_mop(ea, mop, const_term.size, sext.count(mop) != 0); + mul.r.create_from_insn(rsz); + delete rsz; + + mul.d.size = const_term.size; + + // add = res + mul + minsn_t *add = new minsn_t(ea); + add->opcode = m_add; + add->l.create_from_insn(res); + add->r.create_from_insn(&mul); + add->d.size = const_term.size; + + delete res; // mop_t::create_from_insn makes a copy of the insn + res = add; + } + + return res; +} diff --git a/linear_exprs.hpp b/linear_exprs.hpp new file mode 100644 index 0000000..c7ee1de --- /dev/null +++ b/linear_exprs.hpp @@ -0,0 +1,81 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include + +#include "smt_convert.hpp" +#include "mcode_emu.hpp" + +//------------------------------------------------------------------------- +class candidate_expr_t +{ +public: + virtual ~candidate_expr_t() {} + virtual mcode_val_t evaluate(mcode_emulator_t &emu) const = 0; + virtual z3::expr to_smt(z3_converter_t &converter) const = 0; + virtual minsn_t *to_minsn(ea_t ea) const = 0; + virtual const char *dstr() const = 0; +}; + +//------------------------------------------------------------------------- +// resize_mop generates a minsn that resizes the source operand (truncates or extends) +inline minsn_t *resize_mop(ea_t ea, const mop_t &mop, int dest_sz, bool sext) +{ + minsn_t *res = new minsn_t(ea); + if ( dest_sz == mop.size ) + res->opcode = m_mov; + else if ( dest_sz < mop.size ) + res->opcode = m_low; + else + res->opcode = sext ? m_xds : m_xdu; + + res->l = mop; + res->d.size = dest_sz; + return res; +} + +//------------------------------------------------------------------------- +// this emulator automatically assigns variables to 0 +// after the first run, the assigned_vals field can be modified +// and the emulation can be rerun to obtain coefficients +class default_zero_mcode_emu_t : public mcode_emulator_t +{ +public: + std::map assigned_vals; + + mcode_val_t get_var_val(const mop_t &mop) override + { + // check that the mop is indeed a variable + mopt_t t = mop.t; + QASSERT(30695, t == mop_r || t == mop_S || t == mop_v || t == mop_l); + + auto p = assigned_vals.find(mop); + if ( p != assigned_vals.end() ) + return p->second; + + mcode_val_t new_val = mcode_val_t(0, mop.size); + assigned_vals.insert( { mop, new_val } ); + return new_val; + } +}; + +//------------------------------------------------------------------------- +class linear_expr_t : public candidate_expr_t +{ +public: + mcode_val_t const_term { 0, 1 }; + std::map coeffs; + std::set sext; + + const char *dstr() const override; + linear_expr_t(const minsn_t &insn); + mcode_val_t evaluate(mcode_emulator_t &emu) const override; + z3::expr to_smt(z3_converter_t &cvtr) const override; + minsn_t *to_minsn(ea_t ea) const override; +}; diff --git a/makefile b/makefile new file mode 100644 index 0000000..f724544 --- /dev/null +++ b/makefile @@ -0,0 +1,139 @@ +PROC=goomba + +GOALS += $(R)libz3$(DLLEXT) +O2=heuristics +O3=smt_convert +O4=linear_exprs +O5=msynth_parser +O6=bitwise_expr_lookup_tbl +O7=optimizer +O8=equiv_class +O9=file + +CONFIGS=goomba.cfg +include ../plugin.mak + +ifeq ($(THIRD_PARTY),) + # building outside of Hex-Rays tree, use a local z3 build + Z3VER=4.11.2 + Z3BIN-$(__LINUX__) = z3/z3-$(Z3VER)-x64-glibc-2.31/bin/ + Z3BIN-$(__NT__) = z3/z3-$(Z3VER)-x64-win/bin/ + ifdef __ARM__ + Z3BIN-$(__MAC__) = z3/z3-$(Z3VER)-arm64-osx-11.0/bin/ + else + Z3BIN-$(__MAC__) = z3/z3-$(Z3VER)-osx-10.16/ + endif + Z3_BIN = $(Z3BIN-1) + Z3_INCLUDE = $(Z3_BIN)../include/ +endif + +ifdef __NT__ + # link to the import library on Windows + STDLIBS += $(Z3_BIN)libz3.lib +else + # link directly to dylib/shared object on Unix + STDLIBS += -L$(R) -lz3 +endif + +$(F)$(PROC)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O2)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O3)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O4)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O5)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O6)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O7)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O8)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(O9)$(O): CC_INCP += $(Z3_INCLUDE) $(Z3_INCLUDE)c++ +$(F)$(PROC)$(O): $(R)libz3$(DLLEXT) + +$(R)libz3$(DLLEXT): $(Z3_BIN)libz3$(DLLEXT) + $(Q)$(CP) $? $@ + +# MAKEDEP dependency list ------------------ +$(F)bitwise_expr_lookup_tbl$(O): $(I)bitrange.hpp $(I)bytes.hpp \ + $(I)config.hpp $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp \ + $(I)hexrays.hpp $(I)ida.hpp $(I)idp.hpp $(I)ieee.h \ + $(I)kernwin.hpp $(I)lines.hpp $(I)llong.hpp \ + $(I)loader.hpp $(I)nalt.hpp $(I)name.hpp $(I)netnode.hpp \ + $(I)pro.h $(I)range.hpp $(I)segment.hpp $(I)typeinf.hpp \ + $(I)ua.hpp $(I)xref.hpp bitwise_expr_lookup_tbl.cpp \ + bitwise_expr_lookup_tbl.hpp consts.hpp linear_exprs.hpp \ + mcode_emu.hpp minsn_template.hpp smt_convert.hpp \ + z3++_no_warn.h +$(F)equiv_class$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + bitwise_expr_lookup_tbl.hpp consts.hpp equiv_class.cpp \ + equiv_class.hpp heuristics.hpp lin_conj_exprs.hpp \ + linear_exprs.hpp mcode_emu.hpp minsn_template.hpp \ + msynth_parser.hpp optimizer.hpp simp_lin_conj_exprs.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)file$(O) : $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp $(I)fpro.h \ + $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp $(I)ida.hpp \ + $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp $(I)lines.hpp \ + $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp $(I)name.hpp \ + $(I)netnode.hpp $(I)pro.h $(I)range.hpp $(I)segment.hpp \ + $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + bitwise_expr_lookup_tbl.hpp consts.hpp equiv_class.hpp \ + file.cpp file.hpp heuristics.hpp lin_conj_exprs.hpp \ + linear_exprs.hpp mcode_emu.hpp minsn_template.hpp \ + msynth_parser.hpp simp_lin_conj_exprs.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)goomba$(O) : $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp $(I)err.h \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + bitwise_expr_lookup_tbl.hpp consts.hpp equiv_class.hpp \ + file.hpp goomba.cpp heuristics.hpp lin_conj_exprs.hpp \ + linear_exprs.hpp mcode_emu.hpp minsn_template.hpp \ + msynth_parser.hpp optimizer.hpp simp_lin_conj_exprs.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)heuristics$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + heuristics.cpp heuristics.hpp linear_exprs.hpp \ + mcode_emu.hpp smt_convert.hpp z3++_no_warn.h +$(F)linear_exprs$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + linear_exprs.cpp linear_exprs.hpp mcode_emu.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)msynth_parser$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + consts.hpp linear_exprs.hpp mcode_emu.hpp \ + minsn_template.hpp msynth_parser.cpp msynth_parser.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)optimizer$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + bitwise_expr_lookup_tbl.hpp consts.hpp equiv_class.hpp \ + heuristics.hpp lin_conj_exprs.hpp linear_exprs.hpp \ + mcode_emu.hpp minsn_template.hpp msynth_parser.hpp \ + optimizer.cpp optimizer.hpp simp_lin_conj_exprs.hpp \ + smt_convert.hpp z3++_no_warn.h +$(F)smt_convert$(O): $(I)bitrange.hpp $(I)bytes.hpp $(I)config.hpp \ + $(I)fpro.h $(I)funcs.hpp $(I)gdl.hpp $(I)hexrays.hpp \ + $(I)ida.hpp $(I)idp.hpp $(I)ieee.h $(I)kernwin.hpp \ + $(I)lines.hpp $(I)llong.hpp $(I)loader.hpp $(I)nalt.hpp \ + $(I)name.hpp $(I)netnode.hpp $(I)pro.h $(I)range.hpp \ + $(I)segment.hpp $(I)typeinf.hpp $(I)ua.hpp $(I)xref.hpp \ + mcode_emu.hpp smt_convert.cpp smt_convert.hpp \ + z3++_no_warn.h diff --git a/mba.cfg b/mba.cfg new file mode 100644 index 0000000..8d00f3d --- /dev/null +++ b/mba.cfg @@ -0,0 +1,17 @@ + +// This configuration file is used by the mixed_bool_arith plugin, which +// provides deobfuscation functionality for expressions obfuscated with +// mixed boolean arithmetic expressions. + +// By default, the plugin only engages through a right-click menu option. +// Set the below option to YES to make the plugin engage automatically +// when the decompiler is invoked. +MBA_RUN_AUTOMATICALLY = NO +// The timeout in ms for z3 proofs. Set this to 0 to disable z3 proofs +// entirely and assume simplifications are correct after heuristic checks. +MBA_Z3_TIMEOUT = 1000 +// When z3 times out, should the simplification be assumed correct? +MBA_Z3_ASSUME_TIMEOUTS_CORRECT = YES +// Path to an MBA oracle. Leave this empty to disable the function +// fingerprinting algorithm and use only linear methods. +MBA_ORACLE_PATH = ""; diff --git a/mcode_emu.hpp b/mcode_emu.hpp new file mode 100644 index 0000000..7a5695d --- /dev/null +++ b/mcode_emu.hpp @@ -0,0 +1,337 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * This file implements a simple microcode emulator class + * + */ + +#pragma once +#include + +//------------------------------------------------------------------------- +// truncate v to w bytes +inline uint64 trunc(uint64 v, int w) +{ + QASSERT(30660, w == 1 || w == 2 || w == 4 || w == 8); + return v & make_mask(w * 8); +} + +//------------------------------------------------------------------------- +struct mcode_val_t +{ + uint64 val; + int size; // in bytes + + //------------------------------------------------------------------------- + void check_size_equal(const mcode_val_t &o) const + { + QASSERT(30661, size == o.size); + } + + //------------------------------------------------------------------------- + mcode_val_t(uint64 v, int s) : val(trunc(v, s)), size(s) {} + + //------------------------------------------------------------------------- + int64 signed_val() const + { + return extend_sign(val, size, true); + } + + //------------------------------------------------------------------------- + mcode_val_t sext(int target_sz) const + { + QASSERT(30662, target_sz >= size); + return mcode_val_t(signed_val(), target_sz); + } + + //------------------------------------------------------------------------- + mcode_val_t zext(int target_sz) const + { + QASSERT(30663, target_sz >= size); + return mcode_val_t(val, target_sz); + } + + //------------------------------------------------------------------------- + mcode_val_t low(int target_sz) const + { + QASSERT(30664, target_sz <= size); + return mcode_val_t(val, target_sz); + } + + //------------------------------------------------------------------------- + mcode_val_t high(int target_sz) const + { + QASSERT(30665, target_sz <= size); + int bytes_to_remove = size - target_sz; + return mcode_val_t(right_ushift(val, 8 * bytes_to_remove), target_sz); + } + + //------------------------------------------------------------------------- + bool operator==(const mcode_val_t &o) const + { + return size == o.size && val == o.val; + } + + //------------------------------------------------------------------------- + bool operator!=(const mcode_val_t &o) const + { + return !(*this == o); + } + + //------------------------------------------------------------------------- + bool operator<(const mcode_val_t &o) const + { + QASSERT(30702, size == o.size); + return val < o.val; + } + + //------------------------------------------------------------------------- + mcode_val_t operator+(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val + o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator-(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val - o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator*(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val * o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator/(const mcode_val_t &o) const + { + check_size_equal(o); + if ( o.val == 0 ) + throw "division by zero occurred when emulating instruction"; + return mcode_val_t(val / o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t sdiv(const mcode_val_t &o) const + { + check_size_equal(o); + if ( o.val == 0 ) + throw "division by zero occurred when emulating instruction"; + int64 res; + uint64 l = val; + uint64 r = o.val; + switch ( size ) + { + case 1: res = int8(l) / int8(r); break; + case 2: res = int16(l) / int16(r); break; + case 4: res = int32(l) / int32(r); break; + case 8: res = int64(l) / int64(r); break; + default: INTERR(30666); + } + + return mcode_val_t(res, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator%(const mcode_val_t &o) const + { + check_size_equal(o); + if ( o.val == 0 ) + throw "division by zero occurred when emulating instruction"; + return mcode_val_t(val % o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t smod(const mcode_val_t &o) const + { + check_size_equal(o); + if ( o.val == 0 ) + throw "division by zero occurred when emulating instruction"; + int64 res = -1; + uint64 l = val; + uint64 r = o.val; + switch ( size ) + { + case 1: res = int8(l) % int8(r); break; + case 2: res = int16(l) % int16(r); break; + case 4: res = int32(l) % int32(r); break; + case 8: res = int64(l) % int64(r); break; + default: QASSERT(30667, false); + } + + return mcode_val_t(res, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator<<(const mcode_val_t &o) const + { + return mcode_val_t(left_shift(val, o.val), size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator>>(const mcode_val_t &o) const + { + return mcode_val_t(right_ushift(val, o.val), size); + } + + //------------------------------------------------------------------------- + mcode_val_t sar(const mcode_val_t &o) const + { + return mcode_val_t(right_sshift(signed_val(), o.val), size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator|(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val | o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator&(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val & o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator^(const mcode_val_t &o) const + { + check_size_equal(o); + return mcode_val_t(val ^ o.val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator-() const + { + return mcode_val_t(-val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator!() const + { + return mcode_val_t(!val, size); + } + + //------------------------------------------------------------------------- + mcode_val_t operator~() const + { + return mcode_val_t(~val, size); + } +}; + +//------------------------------------------------------------------------- +class mcode_emulator_t +{ +public: + // base classes with virtual functions should have a virtual dtr + virtual ~mcode_emulator_t() {} + // returns the value assigned to a register, stack, global, or local variable + virtual mcode_val_t get_var_val(const mop_t &mop) = 0; + + //------------------------------------------------------------------------- + mcode_val_t mop_value(const mop_t &mop) + { + switch ( mop.t ) + { + case mop_n: + return mcode_val_t(mop.nnn->value, mop.size); + case mop_d: + return minsn_value(*mop.d); + case mop_r: // register + case mop_S: // stack variable + case mop_v: // global variable + case mop_l: + return get_var_val(mop); + default: + throw "unhandled mop type in mcode emulator"; + } + } + + //------------------------------------------------------------------------- + mcode_val_t minsn_value(const minsn_t &insn) + { + if ( insn.is_fpinsn() ) + { + msg("Emulator does not support floating point\n"); + throw "Emulator does not support floating point"; + } + switch ( insn.opcode ) + { + case m_ldc: + case m_mov: + return mop_value(insn.l); + case m_neg: + return -mop_value(insn.l); + case m_lnot: + return !mop_value(insn.l); + case m_bnot: + return ~mop_value(insn.l); + case m_xds: + return mop_value(insn.l).sext(insn.d.size); + case m_xdu: + return mop_value(insn.l).zext(insn.d.size); + case m_low: + return mop_value(insn.l).low(insn.d.size); + case m_high: + return mop_value(insn.l).high(insn.d.size); + case m_add: + return mop_value(insn.l) + mop_value(insn.r); + case m_sub: + return mop_value(insn.l) - mop_value(insn.r); + case m_mul: + return mop_value(insn.l) * mop_value(insn.r); + case m_udiv: + return mop_value(insn.l) / mop_value(insn.r); + case m_sdiv: + return mop_value(insn.l).sdiv(mop_value(insn.r)); + case m_umod: + return mop_value(insn.l) & mop_value(insn.r); + case m_smod: + return mop_value(insn.l).smod(mop_value(insn.r)); + case m_or: + return mop_value(insn.l) | mop_value(insn.r); + case m_and: + return mop_value(insn.l) & mop_value(insn.r); + case m_xor: + return mop_value(insn.l) ^ mop_value(insn.r); + case m_shl: + return mop_value(insn.l) << mop_value(insn.r); + case m_shr: + return mop_value(insn.l) >> mop_value(insn.r); + case m_sar: + return mop_value(insn.l).sar(mop_value(insn.r)); + case m_sets: + return mcode_val_t(mop_value(insn.l).signed_val() < 0, insn.d.size); + case m_setnz: + return mcode_val_t(mop_value(insn.l) != mop_value(insn.r), insn.d.size); + case m_setz: + return mcode_val_t(mop_value(insn.l) == mop_value(insn.r), insn.d.size); + case m_setae: + return mcode_val_t(mop_value(insn.l).val >= mop_value(insn.r).val, insn.d.size); + case m_setb: + return mcode_val_t(mop_value(insn.l).val < mop_value(insn.r).val, insn.d.size); + case m_seta: + return mcode_val_t(mop_value(insn.l).val > mop_value(insn.r).val, insn.d.size); + case m_setbe: + return mcode_val_t(mop_value(insn.l).val <= mop_value(insn.r).val, insn.d.size); + case m_setg: + return mcode_val_t(mop_value(insn.l).signed_val() > mop_value(insn.r).signed_val(), insn.d.size); + case m_setge: + return mcode_val_t(mop_value(insn.l).signed_val() >= mop_value(insn.r).signed_val(), insn.d.size); + case m_setl: + return mcode_val_t(mop_value(insn.l).signed_val() < mop_value(insn.r).signed_val(), insn.d.size); + case m_setle: + return mcode_val_t(mop_value(insn.l).signed_val() <= mop_value(insn.r).signed_val(), insn.d.size); + default: + msg("Unhandled opcode in emulator %d\n", insn.opcode); + throw "Unhandled opcode"; + } + } +}; \ No newline at end of file diff --git a/minsn_template.hpp b/minsn_template.hpp new file mode 100644 index 0000000..f508a04 --- /dev/null +++ b/minsn_template.hpp @@ -0,0 +1,163 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include +#include "linear_exprs.hpp" +#include "consts.hpp" + +//------------------------------------------------------------------------- +struct default_mops_t +{ + mopvec_t mops; + + static default_mops_t *get_instance() + { + if ( instance == nullptr ) + instance = new default_mops_t(); + return instance; + } + +private: + static default_mops_t *instance; + default_mops_t() + { + for ( int i = 0; i < CANDIDATE_EXPR_NUMINPUTS; i++ ) + { + mop_t new_var; + new_var.t = mop_l; + new_var.l = new lvar_ref_t(nullptr, i); + new_var.size = 8; + mops.push_back(new_var); + } + } +}; + +//------------------------------------------------------------------------- +// a minsn template has no defined size or assigned terminal mops +class minsn_template_t +{ +public: + // caller is responsible for freeing the minsn_t * + virtual minsn_t *synthesize(ea_t ea, int size, const qvector &mops) const = 0; + virtual ~minsn_template_t() {} + + const char *dstr() const + { + minsn_t *insn = synthesize(0, 8, default_mops_t::get_instance()->mops); + const char *res = insn->dstr(); + delete insn; + return res; + } +}; + +typedef std::shared_ptr minsn_template_ptr_t; +typedef qvector minsn_templates_t; + +//------------------------------------------------------------------------- +struct mt_constant_t : public minsn_template_t +{ + uint64_t val; + + mt_constant_t(uint64_t v) : val(v) {} + minsn_t *synthesize(ea_t ea, int size, const qvector&) const override + { + minsn_t *res = new minsn_t(ea); + res->opcode = m_ldc; + res->l.make_number(val, size, ea); + res->r.zero(); + res->d.size = size; + return res; + } +}; + +//------------------------------------------------------------------------- +struct mt_varref_t : public minsn_template_t +{ + int var_idx; + + mt_varref_t(int v) : var_idx(v) {} + minsn_t *synthesize(ea_t ea, int size, const qvector &mops) const override + { + QASSERT(30704, var_idx < mops.size()); + return resize_mop(ea, mops[var_idx], size, false); + } +}; + +//------------------------------------------------------------------------- +struct mt_comp_t : public minsn_template_t +{ + mcode_t opc; + minsn_templates_t operands; + + mt_comp_t(mcode_t op, minsn_templates_t opr) : opc(op), operands(opr) {} + + minsn_t *synthesize(ea_t ea, int size, const qvector &mops) const override + { + minsn_t *res = new minsn_t(ea); + res->opcode = opc; + res->l.zero(); + res->r.zero(); + + if ( operands.size() >= 1 ) + { + minsn_t *l = operands[0]->synthesize(ea, size, mops); + res->l.create_from_insn(l); + delete l; + } + if ( operands.size() >= 2 ) + { + minsn_t *r = operands[1]->synthesize(ea, size, mops); + res->r.create_from_insn(r); + delete r; + } + + res->d.size = size; + return res; + } +}; + +inline minsn_template_ptr_t make_un(mcode_t opc, minsn_template_ptr_t a) +{ + minsn_templates_t operands; + operands.push_back(a); + return std::make_shared(opc, operands); +} + +inline minsn_template_ptr_t make_bin(mcode_t opc, minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + minsn_templates_t operands; + operands.push_back(a); + operands.push_back(b); + return std::make_shared(opc, operands); +} + +inline minsn_template_ptr_t operator+(minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + return make_bin(m_add, a, b); +} +inline minsn_template_ptr_t operator*(minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + return make_bin(m_mul, a, b); +} +inline minsn_template_ptr_t operator&(minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + return make_bin(m_and, a, b); +} +inline minsn_template_ptr_t operator|(minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + return make_bin(m_or, a, b); +} +inline minsn_template_ptr_t operator^(minsn_template_ptr_t a, minsn_template_ptr_t b) +{ + return make_bin(m_xor, a, b); +} +inline minsn_template_ptr_t operator~(minsn_template_ptr_t a) +{ + return make_un(m_bnot, a); +} diff --git a/msynth_parser.cpp b/msynth_parser.cpp new file mode 100644 index 0000000..a2b2e72 --- /dev/null +++ b/msynth_parser.cpp @@ -0,0 +1,128 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "msynth_parser.hpp" +#include "minsn_template.hpp" + +default_mops_t *default_mops_t::instance = nullptr; + +minsn_t *msynth_expr_parser_t::parse_next_expr() +{ + if ( *next == '~' ) + { + next++; + minsn_t *res = new minsn_t(0); + res->opcode = m_bnot; + minsn_t *next_expr = parse_next_expr(); + res->l.create_from_insn(next_expr); + delete next_expr; + next_expr = nullptr; + res->d.size = res->l.size; + return res; + } + + // ExprInt(val: uint64, bitw: int) + { + int nread; + uint64 val; + int bitw; + int sr = qsscanf(next, "ExprInt(%" FMT_64 "u, %d)%n", &val, &bitw, &nread); + if ( sr == 2 ) + { + next += nread; + + minsn_t *res = new minsn_t(0); + res->opcode = m_ldc; + res->l.make_number(val, bitw/8); + res->r.zero(); + res->d.size = bitw/8; + return res; + } + } + + // ExprId(id: str, bitw: int) + { + int nread; + int varnum, bitw; + int sr = qsscanf(next, "ExprId(\"p%d\", %d)%n", &varnum, &bitw, &nread); + if ( sr == 2 ) + { + next += nread; + minsn_t *res = new minsn_t(0); + res->opcode = bitw == 64 ? m_mov : m_low; + res->l = vars[varnum]; + res->d.size = bitw/8; + return res; + } + } + + // ExprOp(op: str, expr*) + { + int sc = strncmp(next, "ExprOp", 6); + if ( sc == 0 ) + { + int nread; + next += 6; + char op[3]; + int sr = qsscanf(next, "(\"%2[^\"]\"%n", op, &nread); + QASSERT(30688, sr == 1); + next += nread; + + minsnptrs_t args; + while ( *next != ')' ) + { + sc = strncmp(next, ", ", 2); + QASSERT(30689, sc == 0); + next += 2; + + args.push_back(parse_next_expr()); + } + + next++; // consume the ')' + + // - can be either unary or binary + if ( streq(op, "-") ) + { + if ( args.size() == 1 ) + return make_un(m_neg, &args); + if ( args.size() == 2 ) + return make_bin(m_sub, &args); + INTERR(30690); + } + else + { + mcode_t code = get_binop(op); + if ( code != m_nop ) + return make_bin(code, &args); + } + INTERR(30691); + } + } + + // ExprSlice(expr, low, hi) + { + int sc = strncmp(next, "ExprSlice", 9); + if ( sc == 0 ) + { + next += 9; + QASSERT(30692, *next == '('); + next++; + minsn_t *to_slice = parse_next_expr(); + int lo, hi, nread; + int sr = qsscanf(next, ", %d, %d)%n", &lo, &hi, &nread); + QASSERT(30693, sr == 2); + next += nread; + minsn_t *res = make_slice(to_slice, lo, hi); + delete to_slice; + return res; + } + } + + INTERR(30694); +} diff --git a/msynth_parser.hpp b/msynth_parser.hpp new file mode 100644 index 0000000..1d4cac8 --- /dev/null +++ b/msynth_parser.hpp @@ -0,0 +1,99 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include +#include "linear_exprs.hpp" + +//------------------------------------------------------------------------- +struct bin_op_t +{ + const char *text; + mcode_t opcode; +}; + +static const bin_op_t bin_ops[] = +{ + { "+", m_add }, // "-" is handled separately since it can also be unary + { "*", m_mul }, + { "/", m_udiv }, + { "&", m_and }, + { "|", m_or }, + { "^", m_xor }, + { "<<", m_shl }, +}; + +//------------------------------------------------------------------------- +inline mcode_t get_binop(const char *op) +{ + for ( size_t i=0; i < qnumber(bin_ops); i++ ) + if ( streq(bin_ops[i].text, op) ) + return bin_ops[i].opcode; + return m_nop; +} + +//------------------------------------------------------------------------- +class msynth_expr_parser_t +{ +public: + const char *next; + const mopvec_t &vars; + + + //------------------------------------------------------------------------- + void init_from_arg(mop_t *op, minsn_t **pp_ins) + { + minsn_t *ins = *pp_ins; + op->create_from_insn(ins); + delete ins; + *pp_ins = nullptr; + } + + //------------------------------------------------------------------------- + minsn_t *make_un(mcode_t opcode, minsnptrs_t *args) + { + QASSERT(30683, args->size() == 1); + minsn_t *res = new minsn_t(0); + res->opcode = opcode; + init_from_arg(&res->l, args->begin() + 0); + res->d.size = res->l.size; + return res; + } + + //------------------------------------------------------------------------- + minsn_t *make_bin(mcode_t opcode, minsnptrs_t *args) + { + QASSERT(30684, args->size() == 2); + minsn_t *res = new minsn_t(0); + res->opcode = opcode; + init_from_arg(&res->l, args->begin() + 0); + init_from_arg(&res->r, args->begin() + 1); + if ( opcode == m_shl && res->r.size != 1 ) + res->r.change_size(1); + res->d.size = res->l.size; + return res; + } + + //------------------------------------------------------------------------- + minsn_t *make_slice(minsn_t *src, int lo, int hi) + { + QASSERT(30686, lo == 0); + QASSERT(30687, hi == 8 || hi == 16 || hi == 32); + + minsn_t *res = new minsn_t(0); + res->opcode = m_low; + res->l.create_from_insn(src); + res->d.size = hi / 8; + return res; + } + + minsn_t *parse_next_expr(); + +public: + msynth_expr_parser_t(const char *s, const mopvec_t &v) : next(s), vars(v) {} +}; diff --git a/optimizer.cpp b/optimizer.cpp new file mode 100644 index 0000000..de3ed09 --- /dev/null +++ b/optimizer.cpp @@ -0,0 +1,174 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ +#include + +#include "z3++_no_warn.h" + +#include "optimizer.hpp" + +//-------------------------------------------------------------------------- +// check whether or not we should skip the proving step of optimization +inline bool skip_proofs() +{ + return qgetenv("VD_MBA_SKIP_PROOFS"); +} + +//-------------------------------------------------------------------------- +inline void set_cmt(ea_t ea, const char *cmt) +{ + func_t *pfn = get_func(ea); + set_func_cmt(pfn, cmt, false); +} + +//-------------------------------------------------------------------------- +bool check_and_substitute(minsn_t *insn, minsn_t *cand_insn, uint z3_timeout, bool z3_assume_timeouts_correct) +{ + bool ok = false; + int original_score = score_complexity(*insn); + int candidate_score = score_complexity(*cand_insn); + msg("Testing candidate %s\n", cand_insn->dstr()); + if ( candidate_score > original_score ) + { + msg("Candidate (%d) is not simpler than original (%d), skipping\n", candidate_score, original_score); + } + else + { + z3_converter_t converter; + if ( probably_equivalent(*insn, *cand_insn) ) + { + msg("Instruction is probably equivalent to candidate\n"); + if ( skip_proofs() || z3_timeout == 0 ) + { + set_cmt(insn->ea, "goomba: z3 proof skipped, simplification assumed correct"); + ok = true; + } + else + { + z3::expr lge = converter.minsn_to_expr(*cand_insn); + z3::expr ie = converter.minsn_to_expr(*insn); + z3::solver s(converter.context); + s.set("timeout", z3_timeout); + s.add(lge != ie); + z3::check_result res = s.check(); + msg("SMT check result: %d\n", res); + + if ( res == z3::check_result::unsat ) + { + ok = true; + } + + if ( z3_assume_timeouts_correct && res == z3::check_result::unknown ) + { + set_cmt(insn->ea, "goomba: z3 proof timed out, simplification assumed correct"); + ok = true; + } + } + } + else + { + msg("Candidate not equivalent, skipping\n"); + } + } + + if ( ok ) + substitute(insn, cand_insn); + + return ok; +} + +//-------------------------------------------------------------------------- +bool optimizer_t::optimize_insn_recurse(minsn_t *insn) +{ + if ( optimize_insn(insn) ) + return true; + + bool result = false; + + if ( insn->l.is_insn() ) + result |= optimize_insn_recurse(insn->l.d); + + if ( insn->r.is_insn() ) + result |= optimize_insn_recurse(insn->r.d); + + return result; +} + +//-------------------------------------------------------------------------- +bool optimizer_t::optimize_insn(minsn_t *insn) +{ + bool success = false; + auto start_time = std::chrono::high_resolution_clock::now(); + minsn_set_t candidate_set; // recall minsn_set_t is automatically sorted by complexity + + if ( insn->has_side_effects(true) ) + { +// msg("Instruction has side effects, skipping\n"); + } + else + { + if ( is_mba(*insn) ) + { + msg("Found MBA instruction %s\n", insn->dstr()); + + try + { + auto equiv_class_start = std::chrono::high_resolution_clock::now(); + if ( equiv_classes != nullptr ) + equiv_classes->find_candidates(candidate_set, *insn); + auto equiv_class_end = std::chrono::high_resolution_clock::now(); + + auto linear_start = equiv_class_end; + linear_expr_t linear_guess(*insn); +// msg("Linear guess %s\n", linear_guess.dstr()); + candidate_set.insert(linear_guess.to_minsn(insn->ea)); + auto linear_end = std::chrono::high_resolution_clock::now(); + + auto lin_conj_start = linear_end; + lin_conj_expr_t lin_conj_guess(*insn); + simp_lin_conj_expr_t simp_lin_conj_expr_t(lin_conj_guess); +// msg("Simplified lin conj guess %s\n", simp_lin_conj_expr_t.dstr()); + candidate_set.insert(simp_lin_conj_expr_t.to_minsn(insn->ea)); + auto lin_conj_end = std::chrono::high_resolution_clock::now(); + + for ( minsn_t *cand : candidate_set ) + { + if ( check_and_substitute(insn, cand, z3_timeout, z3_assume_timeouts_correct) ) + { + if ( qgetenv("VD_MBA_LOG_PERF") ) + { + int nvars = get_input_mops(*insn).size(); + msg("Equiv class time: %d %" FMT_64 "d us\n", nvars, + std::chrono::duration_cast(equiv_class_end - equiv_class_start).count()); + msg("Linear time: %d %" FMT_64 "d us\n", nvars, + std::chrono::duration_cast(linear_end - linear_start).count()); + msg("Lin conj time: %d %" FMT_64 "d us\n", nvars, + std::chrono::duration_cast(lin_conj_end - lin_conj_start).count()); + } + success = true; + goto finish; + } + } + } + catch ( const char *&e ) + { + msg("err: %s\n", e); + return false; + } + } + } + +finish: + if ( success ) + { + auto end_time = std::chrono::high_resolution_clock::now(); + msg("Time taken: %" FMT_64 "d us\n", + std::chrono::duration_cast(end_time - start_time).count()); + } + + return success; +} diff --git a/optimizer.hpp b/optimizer.hpp new file mode 100644 index 0000000..f654424 --- /dev/null +++ b/optimizer.hpp @@ -0,0 +1,35 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once + +#include "equiv_class.hpp" +#include "smt_convert.hpp" +#include "heuristics.hpp" +#include "lin_conj_exprs.hpp" +#include "simp_lin_conj_exprs.hpp" + +//-------------------------------------------------------------------------- +inline void substitute(minsn_t *insn, minsn_t *cand) +{ + cand->d = insn->d; + insn->swap(*cand); +} + +bool check_and_substitute(minsn_t *insn, const candidate_expr_t &cand); + +//-------------------------------------------------------------------------- +class optimizer_t +{ +public: + uint z3_timeout = 1000; + bool z3_assume_timeouts_correct = true; + equiv_class_finder_t *equiv_classes = nullptr; + bool optimize_insn(minsn_t *insn); // attempts to replace the instruction with a simpler version + bool optimize_insn_recurse(minsn_t *insn); // attempts to optimize the instruction, and if it fails, optimizes its subinstructions +}; diff --git a/simp_lin_conj_exprs.hpp b/simp_lin_conj_exprs.hpp new file mode 100644 index 0000000..9705977 --- /dev/null +++ b/simp_lin_conj_exprs.hpp @@ -0,0 +1,311 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include +#include +#include "lin_conj_exprs.hpp" +#include "minsn_template.hpp" +#include "bitwise_expr_lookup_tbl.hpp" + +//------------------------------------------------------------------------- +// represents a simplified linear combination of conjunctions, +// essentially just a lin_conj_expr with more bitwise expressions +// other than just conjunctions +class simp_lin_conj_expr_t : public lin_conj_expr_t +{ + minsn_template_ptr_t non_conj_term = std::make_shared(0ull); + qvector range; // sorted lowest to highest + + //------------------------------------------------------------------------- + void recompute_range() + { + std::set new_range; + + for ( const auto &mval : eval_trace ) + new_range.insert(mval); + + range.qclear(); + for ( auto &mval : new_range ) + range.push_back(mval); + } + + //------------------------------------------------------------------------- + // returns a bitfield where the i'th bit indicates whether the i'th evaluation + // returns the value of pos + uint64 eval_trace_to_bit_trace(const eval_trace_t &src_trace, mcode_val_t pos) + { + QASSERT(30703, src_trace.size() <= 64); + + uint64 res = 0; + for ( int i = 0; i < src_trace.size(); i++ ) + { + if ( src_trace[i] == pos ) + res |= (1ull << i); + } + + return res; + } + + //------------------------------------------------------------------------- + bool reset_eval_trace() + { + for ( auto &et : eval_trace ) + et.val = 0; + recompute_coeffs(); + recompute_range(); + return true; + } + +public: + //------------------------------------------------------------------------- + simp_lin_conj_expr_t(const lin_conj_expr_t &o) : lin_conj_expr_t(o) + { + eliminate_variables(); + recompute_range(); + simplify(); + } + + //------------------------------------------------------------------------- + const char *dstr() const override + { + static char res[MAXSTR]; + + minsn_t *ins = non_conj_term->synthesize(0, coeffs[0].size, mops); + qsnprintf(res, sizeof(res), "%s + %s", lin_conj_expr_t::dstr(), ins->dstr()); + delete ins; + return res; + } + + // (1) A constant expression would lead to all variables getting eliminated by eliminate_variables, + // so there's no need for a simplification step here. + + //------------------------------------------------------------------------- + // (2) If F has two unique entries and its first entry is zero, we replace the nonzero element a by + // 1, find the lookup table's entry for the corresponding truth vector and multiply the found + // expression by a. + bool simp_2() + { + if ( range.size() != 2 ) + return false; + if ( eval_trace[0].val != 0 ) + return false; + + mcode_val_t a = range[1]; + + uint64 bit_trace = eval_trace_to_bit_trace(eval_trace, a); + auto minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(a.val) * minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + // (3) If F has two unique entries a and b, both of them are nonzero, w.l.o.g., b = 2a mod 2^n, and + // F's first entry is a, we can express the result in terms of a negated single expression. We + // replace all occurences of a by zeros and that of b by ones, find the corresponding expression + // in the lookup table, negate it, and multiply it by -a. + bool simp_3() + { + if ( range.size() != 2 ) + return false; + + mcode_val_t a = eval_trace[0]; + mcode_val_t b = range[0] == a ? range[1] : range[0]; + + if ( a * mcode_val_t(2, b.size) != b ) + return false; + + uint64 bit_trace = eval_trace_to_bit_trace(eval_trace, b); + auto minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(-a.val) * ~minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + // (4) If F has two unique entries a and b, but the previous cases do not apply, and F's very first + // entry is a, we first identify a as the constant term. Then we find an expression with ones + // exactly where F has the entry b in the lookup table, multiply it by b - a and add the term to + // the constant. + bool simp_4() + { + if ( range.size() != 2 ) + return false; + + mcode_val_t a = eval_trace[0]; + mcode_val_t b = range[0] == a? range[1] : range[0]; + + uint64 bit_trace = eval_trace_to_bit_trace(eval_trace, b); + auto minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(a.val) + + std::make_shared((b-a).val) * minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + // (5) If F has two unique nonzero entries a and b and its first one is zero, we split it into two vectors + // with ones where F has entries a or b, resp., find the corresponding expressions in the lookup + // table, multiply them by a and b, resp., and add the terms together. + bool simp_5() + { + if ( range.size() != 3 ) + return false; + if ( eval_trace[0].val != 0ull ) + return false; + + mcode_val_t a = range[1]; + mcode_val_t b = range[2]; + + uint64 a_bit_trace = eval_trace_to_bit_trace(eval_trace, a); + uint64 b_bit_trace = eval_trace_to_bit_trace(eval_trace, b); + auto a_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), a_bit_trace); + auto b_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), b_bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(a.val) * a_minsn_template + + std::make_shared(b.val) * b_minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + // (6) If F has three unique nonzero entries a, b and c and its first one is 0, we try to express one + // of them as a sum of the others modulo 2n, e.g., a = b + c. In that case we split F into two + // vectors with ones where F has entries b or c, resp., or a, find the corresponding expressions in + // the lookup table, multiply them by b and c, resp., and add the terms together. + bool simp_6() + { + if ( range.size() != 4 ) + return false; + if ( eval_trace[0].val != 0ull ) + return false; + + mcode_val_t a = range[1]; + mcode_val_t b = range[2]; + mcode_val_t c = range[3]; + + // make sure that a = b + c + if ( b == a + c ) + qswap(a, b); + else if ( c == a + b ) + qswap(a, c); + else if ( a != b + c ) + return false; + + QASSERT(30705, a == b + c); + + uint64 a_bit_trace = eval_trace_to_bit_trace(eval_trace, a); + uint64 b_bit_trace = eval_trace_to_bit_trace(eval_trace, b); + uint64 c_bit_trace = eval_trace_to_bit_trace(eval_trace, c); + auto ab_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), a_bit_trace | b_bit_trace); + auto ac_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), a_bit_trace | c_bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(b.val) * ab_minsn_template + + std::make_shared(c.val) * ac_minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + // (7) If F has three unique nonzero entries a, b and c, its first one is 0 and the previous case does + // not apply, we split it into three vectors with ones where F has entries a, b or c, resp., find the + // corresponding expressions in the lookup table, multiply them by a, b and c, resp., and add the + // terms together. + bool simp_7() + { + if ( range.size() != 4 ) + return false; + if ( eval_trace[0].val != 0ull ) + return false; + + mcode_val_t a = range[1]; + mcode_val_t b = range[2]; + mcode_val_t c = range[3]; + + uint64 a_bit_trace = eval_trace_to_bit_trace(eval_trace, a); + uint64 b_bit_trace = eval_trace_to_bit_trace(eval_trace, b); + uint64 c_bit_trace = eval_trace_to_bit_trace(eval_trace, c); + auto a_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), a_bit_trace); + auto b_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), b_bit_trace); + auto c_minsn_template = bw_expr_tbl_t::instance.lookup(mops.size(), c_bit_trace); + + non_conj_term = non_conj_term + + std::make_shared(a.val) * a_minsn_template + + std::make_shared(b.val) * b_minsn_template + + std::make_shared(c.val) * c_minsn_template; + + return reset_eval_trace(); + } + + //------------------------------------------------------------------------- + bool simp_8() + { + if ( range.size() != 4 ) + return false; + if ( eval_trace[0].val == 0ull ) + return false; + + mcode_val_t a = eval_trace[0]; + + non_conj_term = non_conj_term + std::make_shared(a.val); + + for ( int i = 0; i < eval_trace.size(); i++ ) + eval_trace[i] = eval_trace[i] - a; + recompute_coeffs(); + recompute_range(); + return simplify(); // start again + } + + //------------------------------------------------------------------------- + bool simplify() + { + if ( mops.size() < 1 || mops.size() > 3 ) + return false; + if ( simp_2() ) + return true; + if ( simp_3() ) + return true; + if ( simp_4() ) + return true; + if ( simp_5() ) + return true; + if ( simp_6() ) + return true; + if ( simp_7() ) + return true; + if ( simp_8() ) + return true; + return false; + } + + //------------------------------------------------------------------------- + minsn_t *to_minsn(ea_t ea) const override + { + minsn_t *res = new minsn_t(ea); + minsn_t *l = lin_conj_expr_t::to_minsn(ea); + minsn_t *r = non_conj_term->synthesize(ea, coeffs[0].size, mops); + + res->opcode = m_add; + res->l.create_from_insn(l); + res->r.create_from_insn(r); + res->d.size = coeffs[0].size; + + delete l; + delete r; + return res; + } +}; \ No newline at end of file diff --git a/smt_convert.cpp b/smt_convert.cpp new file mode 100644 index 0000000..ab76660 --- /dev/null +++ b/smt_convert.cpp @@ -0,0 +1,167 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#include "z3++_no_warn.h" +#include "smt_convert.hpp" + +//-------------------------------------------------------------------------- +z3::expr z3_converter_t::create_new_z3_var(const mop_t &mop) +{ + const char *name = build_new_varname(); + return context.bv_const(name, mop.size * 8); +} + +//-------------------------------------------------------------------------- +z3::expr z3_converter_t::var_to_expr(const mop_t &mop) +{ + if ( assigned_vars.count(mop) ) + return assigned_vars.at(mop); + + // mop has not yet been assigned a z3 var, make one now + z3::expr new_var = create_new_z3_var(mop); + input_vars.push_back(new_var); + assigned_vars.insert( { mop, new_var } ); + return new_var; +} + +//-------------------------------------------------------------------------- +z3::expr z3_converter_t::mop_to_expr(const mop_t &mop) +{ + switch ( mop.t ) + { + case mop_n: // immediate value + { + int bytesz = mop.size; + uint64_t value = mop.nnn->value; + return context.bv_val(value, bytesz * 8); // z3 counts size in bits + } + + case mop_d: // result of another instruction + return minsn_to_expr(*mop.d); + + case mop_r: // register + case mop_S: // stack variable + case mop_v: // global variable + { + auto p = assigned_vars.find(mop); + if ( p != assigned_vars.end() ) + return p->second; + + // mop has not yet been assigned a z3 var, make one now + const char *name = build_new_varname(); + z3::expr new_var = context.bv_const(name, mop.size * 8); + input_vars.push_back(new_var); + assigned_vars.insert( { mop, new_var } ); + return new_var; + } + default: + INTERR(30696); // it is better to check this before running z3, when detecting mba + } +} + +//-------------------------------------------------------------------------- +z3::expr z3_converter_t::minsn_to_expr(const minsn_t &insn) +{ + switch ( insn.opcode ) + { + case m_ldc: // load constant + case m_mov: // move + return mop_to_expr(insn.l); + case m_neg: + return -mop_to_expr(insn.l); + case m_lnot: + { + int bitsz = insn.l.size * 8; + z3::expr bool_res = mop_to_expr(insn.l) == context.bv_val(0, bitsz); + // !x === (x == 0) + return bool_to_bv(bool_res, bitsz); + } + case m_bnot: + return ~mop_to_expr(insn.l); + case m_xds: // signed extension + case m_xdu: // unsigned (zero) extension + { + auto e = mop_to_expr(insn.l); + int orig_bitsz = e.get_sort().bv_size(); + int dest_bitsz = insn.d.size * 8; + QASSERT(30674, dest_bitsz >= orig_bitsz); + if ( insn.opcode == m_xdu ) + return z3::zext(e, dest_bitsz - orig_bitsz); + else + return z3::sext(e, dest_bitsz - orig_bitsz); + } + case m_low: + { + auto dest_bitsz = insn.d.size * 8; + return mop_to_expr(insn.l).extract(dest_bitsz - 1, 0); + } + case m_high: + { + auto src_bitsz = insn.l.size * 8; + auto dest_bitsz = insn.d.size * 8; + return mop_to_expr(insn.l).extract(src_bitsz - 1, src_bitsz - dest_bitsz); + } + case m_add: + return mop_to_expr(insn.l) + mop_to_expr(insn.r); + case m_sub: + return mop_to_expr(insn.l) - mop_to_expr(insn.r); + case m_mul: + return mop_to_expr(insn.l) * mop_to_expr(insn.r); + case m_udiv: + return z3::udiv(mop_to_expr(insn.l), mop_to_expr(insn.r)); + case m_sdiv: + return mop_to_expr(insn.l) / mop_to_expr(insn.r); + case m_umod: + return mop_to_expr(insn.l) % mop_to_expr(insn.r); + case m_smod: + return z3::smod(mop_to_expr(insn.l), mop_to_expr(insn.r)); + case m_or: + return mop_to_expr(insn.l) | mop_to_expr(insn.r); + case m_and: + return mop_to_expr(insn.l) & mop_to_expr(insn.r); + case m_xor: + return mop_to_expr(insn.l) ^ mop_to_expr(insn.r); + case m_shl: + return z3::shl( + mop_to_expr(insn.l), + bv_zext_to_len(mop_to_expr(insn.r), insn.l.size * 8)); + case m_shr: + return z3::lshr( + mop_to_expr(insn.l), + bv_zext_to_len(mop_to_expr(insn.r), insn.l.size * 8)); + case m_sar: + return z3::ashr( + mop_to_expr(insn.l), + bv_zext_to_len(mop_to_expr(insn.r), insn.l.size * 8)); + case m_sets: // get sign bit of expression + return bool_to_bv(mop_to_expr(insn.l) < 0, insn.d.size * 8); + // TODO: m_seto, m_setp + case m_setnz: + return bool_to_bv(mop_to_expr(insn.l) != mop_to_expr(insn.r), insn.d.size * 8); + case m_setz: + return bool_to_bv(mop_to_expr(insn.l) == mop_to_expr(insn.r), insn.d.size * 8); + case m_setae: + return bool_to_bv(z3::uge(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setb: + return bool_to_bv(z3::ult(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_seta: + return bool_to_bv(z3::ugt(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setbe: + return bool_to_bv(z3::ule(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setg: + return bool_to_bv(z3::sgt(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setge: + return bool_to_bv(z3::sge(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setl: + return bool_to_bv(z3::slt(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + case m_setle: + return bool_to_bv(z3::sle(mop_to_expr(insn.l), mop_to_expr(insn.r)), insn.d.size * 8); + default: + INTERR(30697); // it is better to check this before running z3, when detecting mba + } +} diff --git a/smt_convert.hpp b/smt_convert.hpp new file mode 100644 index 0000000..c99b154 --- /dev/null +++ b/smt_convert.hpp @@ -0,0 +1,83 @@ +/* + * Copyright (c) 2023 by Hex-Rays, support@hex-rays.com + * ALL RIGHTS RESERVED. + * + * gooMBA plugin for Hex-Rays Decompiler. + * + */ + +#pragma once +#include "z3++_no_warn.h" +#include "mcode_emu.hpp" + +//------------------------------------------------------------------------- +class z3_converter_t +{ + char namebuf[12]; + int next_free_varnum = 0; + const char *build_new_varname() + { + qsnprintf(namebuf, sizeof(namebuf), "y%d", next_free_varnum++); + return namebuf; + } + +public: + z3::context context; + z3::expr_vector input_vars; + + // the next integer we can use to generate a z3 variable name + std::map assigned_vars; + + z3_converter_t() : input_vars(context) { namebuf[0] = '\0'; } + virtual ~z3_converter_t() {} + + // create_new_z3_var is called when var_to_expr fails to find an assigned_var in the cache + virtual z3::expr create_new_z3_var(const mop_t &mop); + z3::expr var_to_expr(const mop_t &mop); // for terminal mops, i.e. stack vars, registers, global vars + z3::expr mop_to_expr(const mop_t &mop); + z3::expr minsn_to_expr(const minsn_t &insn); + + //------------------------------------------------------------------------- + z3::expr bool_to_bv(z3::expr boolean, uint bitsz) + { + return z3::ite(boolean, context.bv_val(1, bitsz), context.bv_val(0, bitsz)); + } + + //------------------------------------------------------------------------- + z3::expr bv_zext_to_len(z3::expr bv, uint target_bitsz) + { + uint orig_bitsz = bv.get_sort().bv_size(); + if ( target_bitsz == orig_bitsz ) + return bv; // no need to extend + return z3::zext(bv, target_bitsz - orig_bitsz); + } + + //------------------------------------------------------------------------- + z3::expr bv_sext_to_len(z3::expr bv, uint target_bitsz) + { + uint orig_bitsz = bv.get_sort().bv_size(); + if ( target_bitsz == orig_bitsz ) + return bv; // no need to extend + return z3::sext(bv, target_bitsz - orig_bitsz); + } + + //------------------------------------------------------------------------- + z3::expr bv_resize_to_len(z3::expr bv, uint target_bitsz, bool sext) + { + uint orig_bitsz = bv.get_sort().bv_size(); + if ( target_bitsz == orig_bitsz ) + return bv; + if ( target_bitsz < orig_bitsz ) + return bv.extract(target_bitsz - 1, 0); + else + return sext + ? bv_sext_to_len(bv, target_bitsz) + : bv_zext_to_len(bv, target_bitsz); + } + + //------------------------------------------------------------------------- + z3::expr mcode_val_to_expr(mcode_val_t v) + { + return context.bv_val(uint64_t(v.val), v.size * 8); + } +}; diff --git a/tests/idb/mba_challenge.i64 b/tests/idb/mba_challenge.i64 new file mode 100644 index 0000000000000000000000000000000000000000..a617f9e0ebde2f9793d1a944f4790100e71f58d6 GIT binary patch literal 19642 zcmc$_V{~Rg*DczyI<{?foOGN{I(G8J=-9Sx+qP}nwrxDIlau#+-#vGnU-zD0XYVm< zuUS>Qc8#&?$Er0~i3C##Hsqm!7U38iNnlCbgdQ*ODmQwkYKAWC;Ueb!6lJ>Mg`=!}3#BVE!o^Xf%mfjH=q% zsP+?#VI+ZCn&L`~M>h$~N6saY--}YCsZ&{cOXqq92oX0l6a@0kefo6RcR9~?CUq2i zeB5jupHg(Cy-aZ#Pi1gBUu|$38wKR_TjkC#!v;_tsIHgYtI`>5AE8jh^52Snju5_( zdLKl;|NkRjqEUrd$6xz;1Rvg}wW(823`Pek($80#k%DEST; zdmDp;4p%=8g@nQe(!Cfq+rj(DAs@0=L)w(>EUstsew!UnG~C4^A6 z3+-cD!lwdBq>n*uAu}sU1dPK~#fQw4inV+Ya=R~#kIZhmw>Q|BXjQezRN8jj7?t5fs z55Mp+RfkMDPwT^QA2A)S-lZ@@k0suz3gO$(0{N#5-&^<9!!3b+K*zD)sOP`_}AfYIX3|{{$O&nA7AG5 z``uNB@9vFsyBgmZ|Hhem5>mP07`vPoUV`#B@5dS1F8lZXf-}@D-;dG-=ttpG>F-GP zIkK3kfSjDeX^K|rN7*VrTKHJZcvWI6-cp%F=~A6Uu_`yhA1YUqL8Qvesen3!Ql{G# zK;Q4K(0hMVj@VWnM6s&YgW)b$73v5hcksETl1uWv)g_m7X^p!fRAK%UAm8Uut_v`y zRqG2(q}#2KNV4IfIv1c8c=-z<`Rod@oF_`#g0ZRC+jvq2dxTS>TcrzOPhY9apaEh3 z(VEfvn8@;Jz_qVKZ~XphH}!O8H{}dEa(ZY{ZX~zlck9nQ^rZ@r+TBiKI-EC*;0J%_ zA5*=x+F2&y0R*KXrtJ&VBXu<9Fn#~ngqx4T2p+{T&22ivs_6u~GxmbVWaj1595t{F z_;)Iz!yUKofL3kl-33tz&WCdHiHAUxqE?Vnn1ZZ8C4S%_xka-dO4Ir|d(*o8H#jV% zzD#lFb&T|1E7_Z-x!99j<04)0dyc^v!R%U6*tnD?Mz+H&9X|gstpkk(vZ##GtbLEX zh@Sk8<_GDHVTslSSisY$Vps%GAtMn-YID@YSSgq=6VP**{EsX{O|@fFj*d}^Kfy=h zQRY2V^wQdWHz3o>$&>7{m<1R`a-J z?d3?-8S*l3wz{qy9Oyb3aAeWKeKL%+{-IE$yG&Hi0MvKUMCl4i*7%U&2T^BtpCM|0 z_RIY8;7!jJ6K2yc2tUXEEPXc4xb8)X>F({VW z3l(&iZE)uN%c`X$IhmJ}=q05`IhD_8J)}0I;uCV$GC|=)tEP@1uY?kOh&5W9GO#QT zN3tPJJ($O@FBmVrQzsd+J|Lqk8%`#Z_$L@XPpq&^Z44(C0I8m5-L4h5+KU~9BbSm!qjN_;F9_E&NpH_=o%6;2SPK})`SyY@6omQ8O-PokSza>*5oHc>m>t_n|OGDIBzQ$S03VRX>zMTF1tW~8UZwNXb05fq3 zlipKL=PapJ3X{I6y>E%?r$8_%EhHJ>B8P%hU|M=|q%V{U2+H@TR&DjG*jSt;#a+2_ zu!So?22iP3_rEHC%E{V*kzb|v;V@1Zz^A*oQRrV}PGPa%02?5-Sqyuxv!#18gKvN!WFH#ApY^ueQkU#S{dpqCLbN`+mbAx&O&suNTKNsn%NQ@Io#93KW2(L%fDyf87braiJ zBB@$I>=p{C*Xel^?ZymunJkH}%N13fg)+{U&NAk~_=;=0d1@=YrY1dOXxtU>icoFi zGY;7FOsw_fO%n#8ll67r-ZOJ_vuu^*zl$1#iN;YVZjxq^5U`B1-U*H!*V~8U{Pky% z-9_ov2yy4TCrc9x%Sn3}u`AEG)iAe4W#&$jLagEl{2e@IY7ohWFQ{M4wQ;s_?(y5* zkO>G+BO_y%bi;-fESTd24ayxq+9DPb-i0pG#s6X&xHvMmQH`Y@C&{f5CGw88h+em8sTISDet!g*#s=HN1^dY9X zLEK3m&fjDUh3tjxrll_N@dh!;RK_J|!eB%}+*?1N&~3H*!jh{GuUOsN-)532?@!aVfFpIoBsvs=$) z!pxPxZcAd=*AG<1ApKe|W;^2!XF7>xyBC{|=4z%yi+konLKT$3HR0dv?7uPc>pfp= z``>T&TXsK{``=&m6FuNldk247bA=Ko;NgZAU2+0wof)!A|2RZ#Q2by*$aOR6fcNF{LjCnKi zt{CpZdK)CdQ`Y2&99@>#5F)x*hIv!6CKv(qwkD1)+iZwAw9pyZ7wU&oQy&*fa-xgL z$GD|Z#5b7`_(Wjz;n+n6nt>I6qVR!6gS41$_Ls~(6V!D8I zwE5f+_HgfjxWI0JyvO$}gFS)qV?2}Wcn3xI&;lV`Ahp4wCyd|!?r{5L!@XPVjQdPy zPABpFB=qfGWceiHfgtb`?XlWv2E`6?7J%w2k8S%|de`Gv6Lqt_T-#twZGjQJ#Pmr7 zobD6dfec^_lN>FyB>jvLN+{FiCxc4CU zd-rw%iJn<`5UR3=TXp;v9kU?BKG>OM|1Hq8?!NIILl+Vre_%7xCurX?u?JJ1 zKeV;*vq69gF%RNDxW4Ni!d>NOe4cRN6H*t{ZaQ)o(ym}YJ2FC_MlYNJSBzUgIP$0U zGie8ecYw}<4Ys!u7+k;ouGKSzX7GY7(J|46Zw=-@?!H3kFKZXt4$$fVW28@p4y-O; zAa9Sgz_ZZKJ~SdIKl*OGZ!?hx9q>01#A3zb8_>`NE(@+Z=(sOmx#DiQob$n|U<>wL zBA{8>b`sBLx!)A%cJiYdlXZNTuohelBIb!!ZA~MQ?$XeO_Z@8uKAN}#iU7&EA8Zf9 zML-h-G2~8Q9!@8;-p2!UF7U=H+;)S$btvlvUn{q2dq@rBY zAn6kgdJVA^X@jJVt}UhkX=+b237YmamU`~!BKwZXL*ex^I`q0Heh;q48p@7520R9< zZxdM02_lASlJtWSL=WUv#YMK`=XGdyue%;&4AgkaQxtR4Zlf5!Xc^cirl`LWL5yC& z7ff_$vt%n;w}1BF^p5Ne=R5TkqaoY|n02_U?=6m;j1M!y*u20g;~`$UK&$FapHDEf z2kn;6@nH4tzZ(M>^IJKX^B0I64zOX`{0-R;wM+ejR-Rs_h`e!G2)zGld6L6__29 z2Nk4mHb?<#X|LYVEl4WVfv3yg4)R()#y*xk(Qh{z|9KM&r4!+qyeHTv8-(Xa2lg}Q zj$zMsFs8r9XZ{t>oBo_?g)9e#dlKFp{8d&d;l?3{kASR!rHiHPK=(iYFNZgSf3#7; zs!VWju?=)gj-qryj%j2?!Wm?fRKe~}cZq^6J&(c;0osyF6bB5rPt}eu3wC_Fy1$Tq zt~4@GMK_C+mh66sI^CFv5on-k_s^-NJlr04@XY6!C^Au$*EXcBa7#?R_@(@8B zr82jj9AFuWRV>dySRR^EczZV&T*kV1Pj!{DhvrIyeiSy#`DsO`!ft|*}+$q#1UVGmB6U!GVsa!x-ri)38Aw4#74Ot zg*x4I6Ee7H;lHO48x$0FVzr?+;)5J$6%L`|1b`^vmMzg&g?*$f>Rm=4jJ^`1x`N2C zLmr%u#ahJzRkZlRituy*N?|h5S%Z`TjcVd9X>*`ijIzh!EEt(yrMjHCFOk6BHFenn zf!ITd0ta!MLg?)uLCQxWG@TNOdU=c?#Pc>4YZ+E^$XPliY7c`;2~e6+kK1hY@ zdzw?;C_=W|Y}dJMgK|61Db)vZ%_p4L`HE|qTPkV{i5FUaQLbEN3G(3PK@w7?^p(WB zylu|YF{F5rne_^3PP;k6OlfPw*CG`8%yK&;+ETj~2L=JiARX!6orcg(F6^%4L)AOW zM$lFH%mwvYK$Ar1Od}zCEv0VDlC$yR;wG&3B0wpBy}qtpu#~=%FaDQ#V{;r0AW`~4 zskQmM-02*{6QAb=sqB%2Wf3F2MN_4gke{qz0<#Jbd{e7J)HfA(NX3qI7r$;ev)ciw%Axl#Gp=%O%yi| zmxAp#J2D_~?Wdnl*{xv7Mv?5~%3v^0@^MFSY>Bd8nYI6{%b)eqT*7epA;kr;zjLIq zUAqP(Np+#G6+#JurN5O^U}np{%~G=^-<~`SJwo)nfR+2vc*&bj3yE6P#bMPj|6TQ2 z!g1v&XNtvBDYgq{rTz~)HoD@lMpe4JaXwKxbo+-tJeuTB=j8^5m{}HeRqBIuNTjoz z-c}xLqKykK=E7FmR-mCzg{H2e_IG=s#;DyRqvg1kn1#}O^ZizlftM}!z`(d+&Fi=_4j7j z?C5yq`V8Gll+;{%VFl1V2+4x9!nWfiNSQVF@_U~|6gCiDT6^}i5LaS|e>^&{#A z^^vpQp4O#NqKY&6dt>c_z=R)_90nrmv8SM&VKmEz7a*yIjWY5NHMj&-L&5&|m1_(< z?~H%pmEr6eeknFm>5`(4veWwztA3%#t1IgoUTTT_)=&!{(2k?|byz0GTC_7-Z4a8v z{SX#5d<>}V&(XurYAI7k95EBm6Z4AnVHU|-&@otAmzOV)Q8YlC2anKdjv%3}|IIF1 zzN$jv&PLIzU3}6mlQ_Izx86u=GPqbD3Za&n+e#zJrfRkb8l4AFDPKwnR}%NU#hby+ zF(RKe(l#%v*ER?G#ORm|HST*sH~?6w}U@0Lcj z;$qv2>^(KecCKqhNjy>Iy^?f`#tx#%1LtB#bW$Zh*RmXu8{y{at1`KXxHi8KKi|l) z@x&<(jJ3&_)!w^Ek-O=NT{>b%_hwU56Z*GEM{{jy6b)a^=dsVbNJq>0;xQL_yrb6|MC0{M>Q=PAnpBJD)9Ib`032fecK$UrrqPjy4$OM-h8bYkj0U4KlRvrCIaq{KKl6S*C=yTOMn?~>z*DfPIeviWg~U~EIpzyu zU2iNcv1OXCuaQ>$RmmUT8MckkRYX|7q(10!OVd!eUY4glShA|yiLf8eqw5{wo}tjh zxzvkw{F1`Bm@%a1aEhnKVGGl@PcjX256*H}TU6zFSdjWAaoytR*!>i@5&pG3tDyuo1V(fd#VKw_rIWa83pUW1>G%sV~f(xiQln3@Reh(v97Ni#j@RtoCP~TStlmpBgw;Zy=PZ=z$*9?@u z#|-poxqkgdW(Sjs7U7o{JJ4x|U}yY$I1UhROmpye5Ob(^OaS3CJAkkS^EtDpde971 zg~$=B^q8m-&K#q~7Z1Jw;T#!FpV!Y@Z_$VU-=fd068JIdd)rR$5CR&nzIf15k+0g=S8J8m*07_MEa*4Loh>K9E zHiM&Fb?U23Z%ni-XbDT=&%(G5%?Uo&3RJsQG9-o^mTc z(eI5^+8*l$r%)~Y9SBDN<-#AK7LfTd2R#s__OY1K|0O|v{47j;>>^7&-cgodh>*nW z30?n`tj`fZQqZN=SIW<@yHKrL^g+pl`=v=#{6h`q04jy$OKl>RaFFMP1xY(N^^Oum z%@?Q{U20c>{GIj*ym2 zxVwgBIab4`xT)rolithG;Bku~$T4KjkHn@$Z*5dGHpQSMuo<^klyuBMXR%Kkh!MRY zKuLDgeT3(%G?IL=;C$QEbMCG&k`RwbT1`+O`I{AO6>m?cJ5;xtFvk$0*rUPUul5^P zi*jRc35MAmS(7oew#R}YRXT}ne}IdjMH8bnVZby?n!24wPbIl!k4m1(UOi==9oO*E zs&j1))Y6m@QF?wEwM-Je1mGsjNJiweT__gWaM^I-7i>fRhh7P@G z!X|9FM-9eDc9o}^J=4H&bXE`tU^$&t-}4GvG^y=GOV1yCM7uKpyX=#ns17ZyQ*02C zucw6;Ze9xrLpNgzCLUs5Y-(5iS%N|8;0pjUup%p?Q&5~Lh?z-;>Ax|* zHN_&o`P98av4LyFt!$N1OMkEU&{g45ox`L7*UB=4U7QBq+JMe%6_y0!-omi~6V^pc z{HT%Z2>>(cG$byTj6$CB$nqfO=`cG1K;C!ZE#Gwa9& zeS}oJsClo82EDji1Jl-xGz{7yg$j&ZU3X;jr>zyeb2+gyoSn0w9f#njky=-tU@nPH zXcEyGpuV0MEIA1z2@HiC|9r_Zij(ws)NDMNQq%AkA){hy8B!C1{|n8c2-xA@AIn9Y zn$j8iwZ1NTM5csc6tBVh`qUHTsz$OA4#Ptwp^U)tX5k`F4mk4`)k2up$v%`S1AMCD zE>`QBxR64zsUj|tW4}<0-LEan=8#5^?o|a&6iHFhH#!xJ%a$m{8i(gZ6$CW~?uBfvF>CTWrj|cT^A=?#RPU?2(eQkW5<~Q5n#gBu6qb2b!tkrh zXoXvaR6NrX^!{pbz^d6=eNIP?YHg1FIr{q zUQ#bwMehWK?=jXZ+wCE5HItzCsp4uepPnPl{?j~$2?v9i%#G%x;pK{w6>Z?|wN zbGR!){~A*!lKdihbCvl*r)8{-k$fpsjAzJ>)B>w##RKy=){6C=wcPfTGibf;?((g^ zHhPyOr1cP{N7>Q=O6o!#HZp>h@X`7-53p9RYwCxMHfyA@sGGy0B$xP~@Ucyeyl4;j z{8=Hg87E{5NI7H(klcTu<%d4e_gZ?py7q?@^@smSOxxZFZv$PtFI?aOKdx#s7>?2c zI$FrL1w152IWpfj;%yXRHn7QCvcYjcx)xuKj^EH3ll+o#Vz{L?YNpU%3F1scQ*19~ zCpuSSq>3(g4ZJ4?So$U~9*$l@ezW?jX5+ocp-iq>KKK@FYEay4$BEIaI@jX87#}T_ zDo`e;F20?`kU3>n)CHaoCZM)7xbjktn_Ha}mzHB26akmU%Ci&T_B$#gV!+gBpG$;7 zEPYdqrj-8%br4U^ID{!_Rq3>YqNY#NGOyQk$-NYqT4DFz7L?Gt^^Q#(Nx^6wj-Ip@ z*`MFCOq>n%!BFo5EO`EH6s!|UafJVlUj}iFa*C(g8MUN{he6#5KS(5jbphCcRIljH zFIm+X0y1W(@0b`m4DwN@WxN>&(C8l<5Lx_IzVq1 z>{Rs^T2?j7J0gTd5l)R}ahhNm;-ni4=&5o${alLFx5LX~Iv$toG<56?95|Dr9yoqm z#A5L`fdkG$h20dXTW2V2!5U#G3`vgdP&pJjdJr3>uhSjis+7k#{6F`btzMfIsGwHx z7phhq&N-=R69Oe&W7CzGN%%n~nOlz!+EiDcfzO)6K-=nkcfLaE)!4SW_Y03%^-hJ&wZa zK;}n-CfGrw@1oySGbu_^p+re1sW6Nz3G4W}>>!$<78hkwI;pUD){Do^pXbOfsU*H> z{Ek@B5X$wYH@AmOIo&aLWDuAz$V5TQI(VBh4}EraF-m^Y6AMi<4n6j-!1F6i#(c?G zr>QtvI3^MT!p{}oZpUB7IxNuZ`(XY0xi%E=64iIG+2ck++?xKu+AHF3V*H$%5GdS0$= zx=hgsnH?#^1{LA1Qb*VkquU{~&&Ux&+5W&a5h?F?k|GPufdokbHL#8!yMN%g-iHIF z?%KZr`gg}0`h8vC6Ktdy^R`cJ8Km2W`25$;s`_sUesUCR^o!F3Cq~^@$raP*siyA> z7c2D(zHgfS7yLD-F3R=~FGQd$$STZ%ALNuX*0UOX#`SNTOz`g%1AUdh&$Z3(pfbEI zK8ia1R3FtCzdrQ?x}$*~IWM3lRv=#FKudu=fhow=hJM6UQF7zKm(pF907&pQCCZ z+%xarXYa61NP_C)1?wgIv*cJeD4;oV7xXT;NnXw=2m$C7m>peA;6sKr1hC&RO$%9#e%nyFd-Fjqg#5DF97av9_ZNvh!5z#x&ZGWt< zZT{%Hj~AY!*Ik~X7mP>z7*8lZhH-S zniMjH_NAPGQ{*IK#_61{1dRHN%+V^B=6Uw9sv^fiwH^e~OAM*Q`HgTni+Bgxz8m4O z`4C>PP`f%cgr5-nspARJeYF1&J5a8CRr)UNU+hN?ft=qPVx-;pBRhr%d#>cCqhHr| z_GLSsKFodBx+Vz8v;hnGF=m2ioCjwHqFGQ$HmAKcI#zMWuRk-QLmij(FeI`Wf@$)#pR*fW=WI|6537id6ykJNTd zFOcMZMj~GzPCz;mgXnWM5W%I>uez_A_L=6r;M>SY_dtJC0xGu@f0Ijei)?e+6+TSm zn$J<#rS4|GhwTuyFYX;%8xp{?P7wO1xVp4=mv2k>q5lY2ORyZS1}pD10wpOS!! zt6JZL<-693_8+e`-9KLEq?)Yce&byd7b*+?;6AE@;oe24s`_3>oE8~~W$GPRzjFhd zMqLhHvlG+6tm_`*fBf&5S%0480|*DAet-$M`M4l!N7-Qa5&qNhS+4o~3J1D9!^H3k zT>X7E3z!ylfqsKn@l61G!TsJ$!y`Tyf9o)P*@Dl%1LC2x!JF(I;9;}^BW+|dv#12ybk=ExNBUW@kis(-z2fSSm71i&`Z^ymEHXW{)O zVb-`1>4Hhv$SeG1ny6Mg4&Ohmsd=PK{_oMX*Agz;2y+H*RP0G2+%fSO`EzP+!**po z8qN9}>oH1nOQnA~wKa_xcY68CSIjY&%0RGet;r#vSbB*AbH>%tr)MzMguAUCC?u0) zJa@U;BEE&tIhdk}ybJhcBgMF)`4yftNzUuyB*P*4)_^DSIkkXT8!h(SI__06+94Nt z_k46xYJqV z+cHm)S$^3&+BCY-mei~EzvbsfZP4Rp3>TN$;R(1i%HXzn-0c88{$1hiT-PyD)N$3^ zQS-r14X@ zTRWy9#czgDQ%a|ljORG<*AatUPQ9mME;Y0tiYhktGdA#3zqz1N&9!Lt|DArhsAisQ zM48ShT}h~6w-_z0p4-+O%~~{vyj3$(L59mek~%nK(-`Zb;o!pamUNmbm4qX4FN-yj zG^g`qPNio*GLY=rl(YA1S`3UwCb7tP~S87w}!|!P##d196Ni)?c zpccuHh{XjV0YxGAZY^uZ0AGRycs*w*w7TY$1~-e>cIWL+P6 z$>yp!lc0u&NEvYA^4nBabie;me(ZN_QNUtbz-2y@J7KimumTphn$Z)gjB_m+A2F@d z3fWZ5fI9sgc_;!sO56Yry`3MKkoo|5Xby%Nap@mKG%j_NOZ5Z&IFosjd%mk>l7~2x zMUuuiIY>0b^S@>#+jen&I7vx>A-c&vOl>Lhv*_r;VZGXYxA@UY(%IU|QZYIvKIY$e zm*FCFt=Q@Pl6K4r+jtY&j`=wnln~lc;|EL_At;~mc&k_xCM{Fl5u1ULM38vIcg*d z4DZFH_{fO}&IO6Jx+5p=+AIo&a11=zcZXDM#ISw9{|}H)zlgWTX+5?uK#V+iJDfyQ zxTq9q@q&sJhiX8tD+=xLS8bo`WY|TJPm@AFFa&Ha5${uR>Y=K6lg!wNg4rRyy%odTic%Qc9a^`v!4PD zUDUK%jfYcaZK%Ej{S=S%B6^NQ1R`Sbkh>z)x?Q0~yIn$LT4&*feqZXQ(PEju?-9Gx z{VHf3Jxi=5PaN`AXm#efEr!V_q_DO7@oGXl0e{gDY!RrOj&gL1xk!-r zOky-M6-Pb;_l`aa5EV63?GEA09m3fa_0zO_p;p>)}PaEk)GnvB= zO@7$)(_W|E#uJm9N*9wUO-rCgSCvaLrQgGmr3Y}`4dPD0pOsCs%a^wg%PPy2{b?C) zhS!C=M8lIwS}iRVSNOw%a*dlW`h>uVtx4AIp2nPh{|LJ6cgMw<9e9_@neBT=k)h(_ zg*^q&Io;oibIhDk3FMb!7l?h5@9(lcnV55BARBGBRDxNo5<9CIb!Oi--q;mtKv(f= z9}9Wab-D^6ZUgO-!`Mnguyr~WdOz@tbMeT=%a2m8Wf$~wUy0*61qq-eh&c%TNrXoO zpr9mLVk|{Ppuv`S4F;3V$UAZp-Sz%@Ot z0h(h5b2Wo#z)-t)U^SXfsh_pdt)Hcy?`lSwTD+v2rS9))_Hb0nmhwMI=l??h*8j5w z{-|^@z4*V0<0odCtJz(nsE+$9MJlDYJ@&+WI>)rbQK(URu-Jj<2Ue%J=pjNAGx`-! zJJvIXtFw&juvI3JorM?u_$X&m&+?(HD47zVbPLE4u{YWQE1xdcE~05cKsC>8Rn4?y zyA-ZQ*M5i_+j_Y5=uS&jd%1OA9M{R+ugps2a6k2le`-A}Q>=K@*@{Sg zw@ewm?%nu=43NaQ6I&Mj_C&z`etOr3#2WitfZUQ3HG{MwiJ^#ri$RZ=5fMTuKotBK z*=Az-GK{$7??&R50efMNkp*kT`0hg(V?{(S002>g9soV~fc(2Pknx_acmD}PwEe>l z>OYw^(85{k-N<4{Been;9KaAA5wPgz4^NQduArBfXp3`Rw;crz;vQ);2+%?EB4~LbVf(c6Ej{l$&a7u ziF5?MWB=$M2qshhjn130Ri3#^#S||EVuJ^R+ZfvGLwPNc3jhQ9gP{*d6GWEOo;Cdc2nl` zkNVcs$E8r?W3G=b^hOcszTFx_3DpTV^v@pH#e9IFQp5z?^e5K<>z=9$Ori~)Ax1D> zLrr>6LyvejByGUZ?Xl00CP11ExH)GQ_kxoty@y%2A#g!&NO)77SQq4+P&aj){EdV@ zt3n>8!xRMf|k-EB4Dp}KsOW~%%HEe4pmoYyQvZi+Hh1J#D1~^IUSNnM%3JwDh$4!6Vu;%P zU-DhKlLLAJ^4UVVJYCdO_*C**(Q&D)G7^|_Es>_^`=R`TnRtvwssAJj$MP7~}fsFY!I5ax;>x)=)IS-eDfg*7?iP2MHyYz%Yc9~7NtGfYvVt#YjXzV#%D4Mvr*5fl99AV$7`IJbS&|nC)GRe9?){s$KI5pEg9Tk1FN$QraLFe=r+g7D z#u^$?SsScNsfzOBZ9jCxh34;~z{=u=oissQz;7SwP_h5cimi)tvTQg_ ziFXUKw!@&HTj7n-bzBx^bq5 zdKlhWSF3I^3-u|ratbjaHMwJ(!W5o*9qsDi`7)6v^8m7h^vJSeW*VAZ_kiLxYkJ<0+R6n!1OjrQL zPb=IwPQiBeS0-a|+#&{)KeaGsZ7^+reChOliL1DF0+=N(7|sMRwl>(n=P`g?}zdbs3QzbLfJ$la)KQ1tf()fZ0l z7Q!P+G0iH7B|3UiTC^nZ<@N%YZam1bha`GHo-P%Blj!Ox$u&H*)QRBM#yX#wC@kF&ng1>Rlo8BPs z5}HUNAE94g7}zvfI1xBVXpxYY7Yg?g1SLbF|Cm=RVu;^Fk+8@hM8;jm2`dK2|Q^US1?ho|?u*(KhkU*T$t)*NeYB?4QbydE2#3 z*UlXh#kBLp_Nv-}9}S&j4(r{&3M)xZ#_VgZ&h4p-M@pgElC``sR}|Z!g2=aqjEyQW z!Nq;$M*(;|J-afi(;mnP<02(AjV1|0?J9A}<0PZhs zNj9|qzz!u;#a_&KVrFh1jK`;!tL(#%m?&ZjZ{VyynL+Mzlik(*=KE#}vV> z(~v-r8NVeR#Jps=dCol1t#yroMXg+S#?!%dB0zRAA)N5`mp-JyRw- zd9K5YWWc{{5Z~q{y(B|g2``yrVT%CBnRc?f=gCSRnT2Idi?Mlx^!r1Wj{MVC}MgklRb>?;Hti% z9leZs-`pH&MLmx#^-9EVM9OqI!eV#uotr$+bW7~R~dti3wma%1&+<#7# zVn>me^w>lpJA-c5`kY$a!dceYZ)dA9T-UR9W$3#i;NX$s7Sn8=8LPoG8_bPpSKUWv z~0&dLxRJN^%q1E;km zxzuJe$BrvPvt#4n;cpdgfb3zL%&uJ{RtuFGYBsB#R`Te%dSdzL$fB?&cckXBQA?G4 zYXnZ4YJd4RGia$&Xvq)+!xXXHlOSDI#;&4Os&XP#;kMPXI%p&5cT62yG&(RNt-}9X zHO{P=T&Af_nw;FiFxw&#az6KSevl@9eB^+nDEy}srf~{`QVJe180z;}pkVWX*hQB# z@xvnr#6>V*^N&C0UufcQ)VZG3Em?kLW|y{5%N0HsZV!YLVQke&rtCygRRk$>Nmysf zp;`dBl|FDS_jo=mAjuQ3a|veyHb|uGD>BbNK+Jo#_nVul5y9br*!^pqzcUz2q=qR@ zCbDtDafajGg>+`R_%=2bm#}cdMi6ImKWp{q0dpxYF>2q1u&L!ivIgI%omyODEk|Nq zgQGJhTh!c}KwftYb9f~AC!!+Y-4?X;=l?pqtnL|+Fo>PK`t)ce*!-kGq@CEOC*eQf zKUkdu>4|uSV3I>;6B2q-*>e*Mv?VFR#C1^2q0Vi1i=O**mR>6mPd|FiHWjKDkQC2< zoDr)nx*P`RgK))-@8{TmtyVyYae|}+zj(v!^PT6|#T*S1$OLD&B+CFpa z0j&pix4+-kv|D~z-5Hq{iF(&L;N;hGdHO)5&o1%yM0k6}`)mbXBD`tdLI!)_zq`ZT zdY)Ln5NdX3^mixhze{pW$zpot_wyxhGPmT8{^wmqt;uH{}K3&g@eETgM0OgS0K_EM!)p5g)C ztCA#7%J<9m{IM8$Js#wHirYb7WjY35P%B@8Ny%zglBG9s|Ldk>l*D)E?|lZ}M^!hr z7COvPkuph#L~(wEN0JFIp_|C|=|#ys=7|MGoAKT(f-gqq=%J+zY76nJBJ z|AJeSdHzCLa|C`duU+?lMVf3=d^szh-_d`}{fn+SfFFUnbl0vF^$*jDJ=|aJpF&(! z?A$gGb;6@hAGV`cK{z}m?QeZcdLnZushQ&{8s{0=et&s$I6~}hK=;{U){L>BjgGj_4no$ z%Ztiv|UN6h4tn7HSd zogTh7!+2~1$1W9Tx{E0uMUF==$0Nt_Ae#m&>#zb`UEo>;?rv~n9=P-1%Su{{Ct(Z4 zv7BHu7a&g!9{DZ2i%A$Fujlk@^R?dq}~WwUp2`Ok;Ln0Th~PgD{s$xY8!diW=lL^KC%;!G|8SlB4R!LD z>*Q~&lYgX6{-!$lTUw*@r^(_^)XAT5wN*z1#n4jpIHan1%6x-@l_9L~%|H{Prdhgl}YBeerj24v|jG(KV>x|4;)j zYv2bh{DBQ3Hwqd38_KhgQ@apt2`%~Dc1++t@Wn5hWiZ*|TMzj<)a8&J!Pqk@RywYS z@qH0>VY3wf#Mm&#&Qg5IXI1?Q?(3N6S9ApILq^3n#A{Ap{F=FbY5AeKe8trQ&RX_{ zTr1c88+i@FoGFCASyYVFo)Q-~ROdf&yh}bdYkMi?k2R|`QvElzFUajIax){! z=;wgxf_!B&`H;t6$%yBnBT-q4JmHmpY4|jYewUj2h;fTCcf0Z{^es>OpfDYCK2Yzg zvHbiHI*agY`35mPj9c6I{aLZ+K9%2wJ;2|KIV1G@7vIx)jgIjAmzBQi`G-7T#h2z! z;=MkEHY&cSkpEF~)BY(}u%F(PlWW+28|GX#_DdO+*5(Ap-oy8Ue4d?9erB*Y^?647 z`ZTZOS&U!i^J`iq2Kv1Fk$Mkb`MgURG1v+pDUZm{cHS?9bNO%QU!h3`^xk<1*!h*c zr}aMtU3c=i0b7CtDsFl44P|E_%-`+detV18E3NZPtuN)-&#d(g^Q_m(v*BYBzYD7O z_i5-(0`o)6(HxpbVvP14?Kz6ae98?KldL$%@zDPCvj0UDADX)r{rTX~^8=orXYK;q z)6en}pZ`PS;zwunHp||q_#a*-{7>-xF`uuKxIGFV+tJ>u{K_gh-D|VCB{`kzQ&=u} zJoNp_{$#^DS@}cyN0_(FXWV7Yul}vBlh41CJm(V6`Aua`Mr=TJ>#dF>%_|~~r2l=x z|JmG?RiQ3L*$O+a(vAYfJ86$>Q zlRu&Tp`D*rzB4#8_5D*e{L{Ak;#F-=a1?y2)f$f3e+hNAF@F-z4`ULpQ72l$Ps4or z_rj&zzYF~vD!ymLS>`*#cAP`o!Et%ru=fnlJ7?HA$Z?bEOwO>4dOVD=WFNzO_Z-g) z;~v@@#{c&mf8sgGCwM$umnV3y(!agj#OqvblU|>8*7GOEFXZviu5eG3 zD{D6vFZLy%dyLNh`{_Ke;@!b{6y|_=mYC~k?vvjd`^#L1c6Ik@zh%?dTXSsBWYj%$ zuyQ9gDIkMn`X|EBC;QyArZ`m@#-(EINc=aYU*WyBv*>5itqG1$L< z=zVIwOR0U7+sC-=_UgYs?DZS_o#iVZFRpg}z8m*DO|B6FzbZvS>UPd+BDV!|CiDGC z@>?+Oq27`bVvej=vEu)TdEn4#BmV5@PG~_Q>@;(bs^7jq-3zq!6C4bS9k67{{ zOFkF%14I6yCI6NsPg(YlSn}nTd^_qzD?X;&{+rJ!-jU|_iM<$WcBZ|`UTVr27k5&$LE;4lfNm)zJiJ;uDAj9YwTNr z=Rb&gv())I5A{yAct&{Iy4Y|qpATEgEcLsz?{`yH$QW6S@Z8uoS?I=;&`tT1f&4%^#d*n5=i4aerPuSvFv#Pxu>f_qA#XGAZ3h1mLx1?)Vtm(%k)0p3|IPDf(27s8MtrJjTXlb6 ze=a+v>b?xBejDcz^5GelEeN< z6I}mKfgg?7Kj!+UYTz$B@PWhsQ3qZ+>@Pd;w>$KI;=p?j{bGXqC-ScQKd9SZ%VmRz z`#I;3_d4W#4td@oAL)qxKda(7$N$-N$d^ACt^Z+%T&#$WZ+5){zfr^`E^&!VT;dX! zxct|ae*+Jk8hrxO000000001ZobAr7YJzbTfbruO7^fDaYhrriitHU2jHY4q5*8M` z058A`u&fz`c?IJQ3kwFL41-CGM&pG4173sd`N837=bYDPO@HWyZt0Hh=|`14^pk$kE&ZiOTCSxwXgs83G^Zn4 z&@=5cQYUmx3wof@WG|i5Xr;W-DUD7_mDcI%G4<5v4|<`yXYSGyJ<|(~Jf%xB`b2X& zq$4_}k|arzBuSDaNs^@h=?}fYB=!On0RR910001ZoMn(rYr`-MhSja#qlaxU*sV0l zVaGw~eb5~W-DMlQ8dJ-O!Bs}=gmjnv#qAfRRzhKA2BAl`^jgwp{q(-s-T(mG-8SDz zJNJiAoGa9Zj5j&CX-cJ~TGXp0-1d8YIGtgzL9mw|K+`ne&sMLN;_a}9Z~?Q&-*~Zz zk_2Gvydb$p_J(vm2|o8377Q*URWnr5mTihNUkHCCU(rgqV9om^2|rE>k!$VHkBUyO z5K<{5byl@L5L|N6HTN)7!pn4^L`i2^A6O8g0v>Dj@DoLG90OccBq}Uin12*-M}8cf zHWoRQWz8XB?f+?ow{|H(D`v6KZADUK(q&TyZDs0O>Ndc{yXl})Je?y~ih7j-O#lD@ z00000c%1WeaSWDS8XC&Lbb!IZl7WMPoxy^E0nGltfq@0cWe4#X7=Th27{Y-hBSSNg gM;tjgbsS&_1k;T~leD+v|NsB{8~%d;0N|!FgiS$>G5`Po literal 0 HcmV?d00001 diff --git a/tests/idb/nonlinear.o.i64 b/tests/idb/nonlinear.o.i64 new file mode 100644 index 0000000000000000000000000000000000000000..89c1b9e7ea26d73ce9c146062a79fe8334e3e69a GIT binary patch literal 9434 zcmc(Fbxp@QVew5ai@_n!N z_g-z)?w>nVbNY0Dy8F|8re z9~9U=s(-P1WS;n-y1vs+{(TgiuRbzAm;h9)$&WEJ1H_+H93Gz90+0_Y=~(JN`a>5E;vXoG-I$r64_cqr2Z{Wa-*nTFnk#<{ z#?)3QJ?voQB(3d&MP;e_e-6*dUF=NW&P~KUXK2e*kAbFrLP9HVHvpmf=~?9x*5;8| zTma6EaTvGX`z6rFgT3NR(%vilKCnH^7sNh)ujqw+H5hb<)K8HM1u%iV z*>!E$^$r$=f4xA+`%?cPL=^R`)zD<(|hDLe9>8>2ZqN&DFcg zb`SUO2ht-#bCH=8XVQ^RGVDuM<%B1BI4?}OYYG?NhG%lxAN<4@x70~o7v?_gdAy~M0I#}4c8P#j@#L)Vsgstw64x!$VA{S=BDE<7KoWv&$ zhNX==<+@&D*IX@%Lt1?|>b*PVQMUjN1%~;H0*pSBj{Kojk7nqGRd%7`X7erI~Fb%5lRVfRpr)IxdLil{J zqS)ace7+?k7-Msch3fYzGO~xe)SDx4mY>@hPSt4?^rhi#uVVv;@Z)XBWPop$iIuGx z`|{a%apc^NMg6ui;icl@jxE!tA%aU#iu^H*ZLuCxlcMc=7vg~xDNK{$ z-^p)^T;=>U^H>fn`x?KI8lt^AYNI%p=f03P zV_1@+$x@h=%+#zT-pI#@^yOsMjJAo8`;8^v(JUu|1!y|kKQ)O+dts%~Voots8f#%d zYqnmAgx?i?oa95*5ecoHxJ--QF#fb^q`IL6k!W7{bp?63YF=r(hW*$G#Sf#Xft$!HlPg`QnsH?OluEqb8=f$qb#j+HLGizgJ8m)3Nt}xe43Z?piINI=kV@ZAyI+nQ2U9X=s{o+~;goe;jY|XfXDh?l+0j~7$RaQoPLn;UW@OR({a!`NTtW^4 zYdx=tRT0jK^#~AIlwG7nrz{EGo4U51m#n1N4&UmtAc>t|g8V1-acgUlZJ`<+Hb9Sy zOS$Z9^0qoMa0M@2d30=f5p8v&rUi{)Y&Ug8PhU%WW${tHyT9;8|ImcDb!@=EyewJW z5}H(KH9_z=@A$(Mo`fbpD}AG~{>Wtse}N44r#rO01eDD3bGe z?hk}u^V9M!PW93lI*$#xx#LW}WBK&f(x=4$!iIeNGMlJ7lH#!QZUp{$zlDKJbD$=T zM+4T`bj7oM&}?N4CrC`g`KR-lS#)<2yFV3M1dlatxRVE^P<06qA`3y@^vK8fjbnY7+Wc zIAoeM($OrN1g6mU@halpmjE$>OYTsxVn~rvBTE5U!#kRpYq(=e2`CLGuz(@v8gcH8 z!=%8y#kz@nYHvyENyS!y@N-F|%UR`TIJc z71&m1qh#`UNWk5kQ>3MYhjVexET_(f*V$PM4G5y2LHo2dfY2aZ>5hA*&Xdi?r~W1* zFdkD$3&hD}VD4IF$h*u-99`;?D6ZwaTn6ya(sAyYbFlg@RU|I<)=JPitMSBKw!XF9 z?Rc9Wpny{OnVXm=o2B4#+QgLAw}R zt6WM=?YCmk&hZzK;Gbr0_EKm5K>?HApwpGHdGbu$=E_dx^MoDzsh zjHDFE+$sTfv14LkOHL#&a|SG;5r8@5EUq9r47Sp0rt)v-6sh;8U;N!B; z1WI2{ck+bQ&ux*4AFfmCFE=Xiet$2soS`G?`?FZA)SVr9!lel*Tp(V`jYez9UA1xNzai~p^;0&QE(u?7tL)cPtdNq5bR@-)LmJkG zfs#vy3*(^aFi&T<k`UXqXi^e`cjblece2XT-uDhu z5Am@nANq{}k>|ydYZCuJVKoxc75T*kbrIFrtxG`aQp%PnpN?0Q)2QNBndu1GwK-O$ zkB49{0VQOouMfGxgj~^*@UGnj*tgb0g-Qj>@|k6+rz@H*feNXI16RIp79zG}j&5NMc@au9%^kJ|{#Ml`gVG!Ly%VCHjWLbW1)iFdFGw_os5sNnRhO zRxQ>PG9bvT(6W5@BK#cnO^~rc%y*m67A4^7{-AGb*BSYrR2~0_LH9 zARXpUL!$SfDsQUnk=@tZQ|?U^#r-CtZ>*A(BuJLK%txcYZflj54Jh0*a5dowtRo`5 zdJ*9Og=}<^J_FS7@+&G_f=?P^VsKcB9tQg$l>13O?%v zxTU!PGY8OmB4VO(#`@ipOMG*OFZ2($oj$wy9JMavOQdWqVK4V%7 z$ROC=3dMgTIVDP*7p9#NwFn_+(1`hsnd|Oelf%#f?sC~$7k)l`v|qnJNNkwloj-!L zTeL?6kU1Mj^4^Fo$#@+H@@It%>TrFfuEvt5cZ`o^NQ}Rj1ab*+V#@D$@MIgdO2Z!) zBE@l_0NzK4cjp8i?|%{WsncU4>sR`8YR#KH{)zk0nXH`3>D_6MY=QT6KgQALfsOm< zM%!yjiw4!=CfvH_zz{q4*%nCU+dum2Po5bJM!1m5oAF!bt;AYmlw<$c&gmZ9%6WY- z;f#!~SGoS9go$tEm}AJ-?*#PbJX!i=z|UwhF&j%*>;1CCI+(p~veiQ(0k|lv@q&vY zA!n*aBxZxFE_EQcLDS$}kzEnhGo=H#uFG6Fo!|F~c}~$YzmMtpcRS`+%eH)vd)pW( zvR~AU%(Dx!XpE5>=Kp|zQS-XcT^TuQ5P4)%~+g{PPlcYdaRorP~C(3a{S)JGWOM1oZ;T}!8h4H3FHCZem!m|+Kl-V z7&^?smA^msf#o*1@xUoP3{2ihJ*apXs!(#=Ip;nhPF_yc z_eb#ltK;#c0LVw(a!VAO{qRspSpE5PHZ9*e)~Xp2Et9HN%Cd{`g>@{XM&LP zatR4+$f~CVfsVT32kvJhx#IFLf3zi=*lyl;$6>9sRe<{ZtbYG14A!~6ee|fV@dG5! z9@g1=j8W|+5#wUvr9jv_0CNs69*jnS=vQnAC%T1>SHmH@Mb*y@$v+nv$oq2>DEYRr zkA`KMM~1vx%g99-0XwbV+-%!hhRZp}c5-*GULSzNnPyXu(H#~l;y{R+GlrVE64Vi0;PB!ld1iC-9s z+2Ef28Pu=!`BZtS3FY|hUYgbDmLID5y3-cTv||&eLoc3J_h|#54oOyACdVzWY3s7} zv}JFtyTt3%d{y#^Y(Zts9CHcc19;;yfyCyB2$@s<)8Tb$g9B`$2CZy)B<-Th38Rd7 z>f5Pcj;^-?ae8_D`&y{{7N;>#eYyvplggls%9x*99e*$3+&~l+P>8++4;oc*14O%#YmYud)Dx3O&oRUPHZ@Z9cAa) z>qZ8O{&A;FD59z%w6!}E9ALA<^xH>9J?OY-_kAeHZq}hPO5`60GW@wHNVb=Wy#8~+ ztnAznmqN6W;J`TzJQfAny5Ss`*H=XR++~;W7Y%?|6taV6n1dyBSy!?3XUJ`{%Bp+S zN2WH-?hs<(&?Er5m?kRXW%S;Wzr*Jc01c;DFBJiTV=0zN9Y{%hU z%dg3yK>|#fu>SP>kXJH#dUrUj>_tlTic4S1_SU>hl`zx9@a*>!C6ATIf=~W2@iVA5 z=Z6X!ywIBU5iB>daoM*Vpd-muf z#CkG=5MJCT>oD%$ywAlUFn>dVM;e$L&~3s(ba_Y1gcbHcBhE-k9Z`dG8v?7!Bpr31 z_Z=$^zp@xAOeL@xJ<#5fHnE5QWHiOVY`RDjX%b&d6z=h;swRySm;mpa@a`?r9c;p8 z_?2mO^1o%mr`=bD;c_?Pj#_ z^f!z~jQa7M1mU4QM#dZ@sGfb+eH55?7RDcwo+23Dp-F9w`)%L}kS8ZK(MnJw%>B9F zRBJji{q;i%j>;G7)C*}T81H;2mw`yN4aXWQ`tA|z+jW*`Rzno)xn9*3(vaXyY&h#O6a3m-x;R3Mo=pORt~~5*VzeK9<|&%5#;33$$g%Id_I|0e zeUi6)|2Aq%Ki=D7J8hqWj0w*84AOJPGDC$)Nr`ZRArCZ_vPs+~))#y|mI zyCLG-ATg*wvm%N*OuZt1dXFbFWHT3)a1Li)jQJuWGHap8Yu9^Ej?JxEwcO<3X9|TcOct9m^PWCeD zJ^7^7=N3Jtfbxdvr{Q94SXz;Uk8D4KKiQH%C8E`B3tWktFqrc~`_-msyktzH&S8AX zZ{-ANFwqF|z$U7&-D>-X;wD_`?RjwvTW|GLrSt?0)#to%N^6Q!ij&I<=WBj0x|`?^ zEDH2WwWu{J5X`C9 zsPo4bb`ykf#`HN10Jy+X@tRjZoOwG9&O*Z~bcrYm=_Vu<>6og-lrIqzyL>D(^6bir zukZ19POg79zLD0IEpq2Cm!Ebv^}us~L5w>K-vz3K@>I=+psIK7&#Z|tjN;B0!PEK)#6 zqx(8fF)X`@t4YUw-XImgld$y!ZM?cHG?B%px=-JRWuCsF6Yx zP|7;jr(kEprMz3bs3&A)_G38quT^bL41w`5GD2i+8zBy>m8|3of|v z`J(uOr+04FL9Pq@3^*=VwW#rT;Rk(PQfx(RlA>d~cMtkl;5wK<#7yGuz(wL3(*$Z&Ds| z>3%ZEzPwXg0c(i;n;iISMxwW6f@4VHqh-Pi9>d$w{4N#-Cd&k_L3wd*CVrKCzdwQ>Lp?new>mAcz| z{eiJJ`vFXrRH`YaL{ubW)0LH;l~!Shd37-abgR5YdTr!1Irg>AL!<1_#8Iu=d+FEG zR!QUd|KgiFw6$~X;^}fV&FI7A6b$LhKUnSshE@<>-{4>S{ACpU+FINW0 znQWbVpknoXZ&I||fXL^(7=aFs8KLjP?Annag}{Zfo=8X4{}diQ?s?Nr5WY? z0)yM1-2>}C;$HN`am@gX1AJztqm6BcT51HuO-%M*yk9O!k0Bm+&s>gsHrI zqB9kV=M4CvE#X+{A>VMAx_+crmZp=(kY-2ykvcy}AiW(_y}CvLucsgE)a)|gthSUX z>~O7=n$>@?Zj{L~+Fz7norKGi^eWa>`gkTb78(3S05$NzXxN3GtF{X9d36@@WpNG| z>=2Qm#_f|yBjWyGtl4}dVz=vu~>+VWaWmHMYf|+Dhy_xpGB31iX?HJ)|Ia(&d=5`lUA$3*jq2;yQv!l zd9Dbi-&R!!RFFwIQqIUohT~Q*J~u0t-RRc#IT#8tb^>Mn1B_nV+C7%a;E=L2GbdeD2v1 z5dWQ~Li&;d>@QR-Dn&j^!Ju-GO^10{iPd4ww;4KQ)fy{QH*qTSh_bPO^aAejP2i}+ z-mPwjehX)hW52I_JslI-?~UWx?+Zn)=_h5LPrMkxGic6#Se3W3mj&dQb8PI&Ur z$??-eSpmZEdr867-|V5B&&?aWUA{mf!v!I(C04~#TzW>ZE0Is_3AxM*07&HK z@fGP}0xidGZ9?J~Bs4Vc{#=#R&McMEwT2Ff42U5CK*cm=k`1j&>ZVFMCh4gGbB28Z zbA)ldj8M+SZ~96>2NA0a&*&aWOi$?#k$XItz^jzQ&e%7E+ZY?N4;;@t5u)vwo*rmVBB1!umdtk9k@Fk0gks43c| z??u0Zh_&;Z{)X||*)C7>$JI?sx1WUbc3)OY0iNY|K65Kw4tsQ#XCx=nnp*UKkF?=1uW@nUStU%fBpkD0*>_Y`Z0)-@wXX0_=UJeJyS{h+tNDt* zWtWkGGMy)BrDT-TefuBb{V_g?Nii&YLf}Q~P;C$w>%SM%RmmH!%}e6J3s(8Z6IwnA zN&2(yBXDN*&{gTX_1amnB7Fq-fy^0}T|qy(EZvMwjw$@frb(?Ne$2e*Hv|ZYn~b-( z-AMMq^A_+$ExnP3CF2-887|_=*=P4PGxv0b zTpwuk1FFP66ueX-O}bjPq4uNkVEV8F;cY{1>M*7@{=O@^1NDg?kw1pxMsaw?oEDEJ zbL4_-b7sh~iT?aY*pZ{gB`1@tt{A(0HcP=>WxswJhG+J4fpY-t*}r#?yl&|}c{-UR$@!!hYZAz> z5PF74al0G0y%zeoWX2ttH0SMRZ_I5>f&L%6Qyyh|;|tnpA++Pba{8gRD}tgw<)8<` zu?}yM+2ff#xG`SajG*W8&X?~&-UW+VCx1xCa@W6F<>*QaAC(o@z9j?a{xF(*>b}w` z=;+jRD=^ko8uRXWc`m)~yu8ZwOvP`}&jH|HMAyfzP-!cPUP(%q{vz@A`&4PNU;+Qr_dqu~3>FN0cdsmK%Vf~A;)X07n0tu6byrSNUHL$M>_+52;{Q(1 zClLJeV5VU+|96fnS7)?~Yiu(U6Btv@?8oiCcfkq60h+-{vvs3wqY0yrZDtkMZPS@; z5l|FvTm(}B83F_%69hAQN(cDOmzS4?!NF9zfxXWJseP%mh1?vl(qHlC=9-C`{XSM) z2S6X|>NaO_Dn1Y?GIp}mGqN&t3W-!Rl7(sD-bJX-Y(?UZsCNq$S04-waRheH%X2SY z=I8~Z!PwLa!of29SCJ`(BqYOKjDuZ$U6d2&zHo4;a5TNXlpZkD&u}pLy%@Ux3u{mN AdjJ3c literal 0 HcmV?d00001 diff --git a/z3++_no_warn.h b/z3++_no_warn.h new file mode 100644 index 0000000..91002df --- /dev/null +++ b/z3++_no_warn.h @@ -0,0 +1,10 @@ +#pragma once +// using z3++.h directly leads to compiler warnings about shadowing declaractions +#ifdef __GNUC__ +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wshadow" +#endif +#include +#ifdef __GNUC__ +# pragma GCC diagnostic pop +#endif diff --git a/z3/readme.txt b/z3/readme.txt new file mode 100644 index 0000000..275c874 --- /dev/null +++ b/z3/readme.txt @@ -0,0 +1,5 @@ +z3 builds should be extracted here, for example: + +z3-4.11.2-x64-win +z3-4.11.2-x64-glibc-2.31 +z3-4.11.2-x64-osx-10.16