_____ __ ______ ___ __ __
/ __(_) |/ / _ )/ _ |__/ /___/ /_
_\ \/ / /|_/ / _ / __ /_ __/_ __/
/___/_/_/ /_/____/_/ |_|/_/ /_/v1.0
°°SiMBA ported to C/C++/LLVM ~pgarba~
SiMBA (Tool for the simplification of linear mixed Boolean-arithmetic expressions (MBAs)) ported to C/C++ with some enhancements and multithreading support.
- Able to directly work on LLVM IR!
- Compiles as standlone tool and plug-in for Clang/Opt
Ported from: https://github.com/DenuvoSoftwareSolutions/SiMBA
MBA evaluation and verification will be run in parallel, if the MBA has more than 3 variables.
Not supported in LLVM, as LLVM does not support multithreading!
Use an external simplfier like GAMBA to crunch non linear MBAs on LLVM IR!
--mba=<mba> - MBA that will be verfied/simplified
--mbadb=<mbadb> - MBA database that will be verfied/simplified
--ir=<ir> - LLVM Module that contains MBA functions that will be verfied/simplified
--bitcount=<BitCount> - Bitcount of the variables (Default 64)
--checklinear - Check if MBA is a linear expresssion (Default true)
--convert-to-llvm - Converts the MBA database to LLVM
--detect-simplify - Search for MBAs in LLVM Module and try to simplify (Default false)
--fastcheck - Verify MBA with random values (Default true)
--prove - Prove with Z3 that the MBA is correct (Default false)
--simplify-expected - Simplify the expected value to match it (Default false)
--ignore-expected - Ignores the expected string (Default false)
--stop=<stop> - Stop after N MBAs are solved (Default 0)
--parallel - Evaluate/Check MBA expressions in parallel
--optimize - Optimize LLVM IR before simplification (Default true)
--external-simplifier - Use SiMBA or GAMBA as simplifier instead of internal (Path to simplify.py/simplify_general.py)
All Tests are done on a MacBook Air M2 24GB
