v0.1.0

0.1.0 (2021-01-20)

Bug Fixes

• BEQ for concrete conditions does not create a constrain (#44) (#45) (8ca6ec9)
• beq/jal edges (870bf6e)
• bug in z3 interface where wrong symbolic constants are used (0fd3de6)
• CFG computation for loops (#57) (80b8859)
• command line parsing (#37) (d20c954)
• constraints are now properly displayed in data-flow graphs (9fa61d0)
• data segment loading (#54) (4ec4f1d)
• dead code elimination now working properly for data-flow graphs (114e75d)
• divu now properly implemented (#105) (b4ee0aa)
• fixing divu exit point collection for candidate path generation (c531663)
• fold all constants in SMT query (#100) (#101) (a2dfc0a), closes #102 #103 #102
• implemented fix for exit ecall edge (4cfb9e0)
• minor mistakes (#26) (a8e6fbc)
• operand side edges (#70) (c7b9c00)
• recursion support for shortest path heursitic (#69) (#76) (914f24e)
• small mistakes fixed (83b637d)
• use ugt SMT-lib operator for SLTU (94213cd)

Features

• ability to print SMT-lib format (c8c6898)
• add "execution depth" as abort criteria (#90) (4b4829d)
• add banch decisions to test DFG generation with BEQ constrains (f5e96e2)
• add candidate path algorithm and generation of a formula graph (WIP) (83cf753)
• add CLI argument for CFG (0a5493b)
• add CLI option for symbolic execution (#43) (#48) (ce3f6fe)
• add CLI option to configure memory size of executor (f30f4f7)
• add command line argument parsing (7f21061)
• add smt generation and solving (#38) (fab1457), closes #16
• add support for division by zero and memory access errors (#77) (#79) (e7dc16f)
• add Z3 SMT solver support (#68) (af9ef1b)
• basic facilities for candidate path generation (64a9fe8)
• candidate path generation (Needs testing) (43723a2)
• compute edges for BEQ instruction (6ff5ebc)
• dead code elimination updated (97caddd)
• eagerly evaluate PC in BEQ instructions (0ef582c)
• first attempt to build a CFG and enabled formatter/linter (a09a934)
• functions for finding candidate path root nodes (WIP) (9fd31ab)
• generate all candidate paths for a given binary (#7) (#46) (c00b605)
• generate dataflow graph from RISC-U path and add Selfie as compiler (5f36c4d)
• implement bit vector remainder operand in monster solver (#107) (5cb4f26)
• implement dataflow graph generation (WIP) (5078ccd)
• implement DIVU in Monster solver and tests (#72) (c8f9d3d)
• implement Propagation Based Local Search for simple Formula (#25) (396fbbe)
• implement shortest path heuristic for path exploration (#60) (#61) (453a615)
• implement SLTU in Monster solver (#58) (#73) (bf7f8f7)
• implement SUB in the native solver (#62) (#63) (8ccfd5d)
• implemented sltu in boolector and z3 (#75) (#80) (af5b364)
• implemented timeout correctly (#74) (#97) (867a240)
• improve command line argument parsing and handling (a50c59d)
• improve terminal output by using a logging library (#66) (#67) (465e35c)
• naive implementation of a RISC-U disassembler (db125f6)
• prototypical implementation to load ELF object files (4caf390)
• reduce executed candidate paths (#55) (#64) (31420ed)
• remove log header on default terminal output (#94) (92cce66)
• some stubs for (ternary) bit vectors (#9) (b89220d)
• started working on dead code elimination (WIP) (a81708c)
• stubs for dataflow graph (11aa224)