Releases: cksystemsgroup/monster
Releases · cksystemsgroup/monster
v0.4.1
v0.4.0
0.4.0 (2021-06-14)
Bug Fixes
- symbolic: print actual progam exit status codes (05d692e)
- inverse value calculation for LHS of REMU (#131) (c24270a)
- invertibility condition for SLTU (when
t != 0) (6947f52) - invertibility conditions DIVU and REMU (#141) (9c03995)
- represent empty path condition as single true constant (e1afdd6)
- use ite to convert booleans to bitvectors (5411f15)
- smt: zero extend bitvectors for comp ops in external solver (2576441)
- test: syntax errors in C* examples (dc60453)
Features
- symbolic: add support for openat system call (#20) (de71a0c)
- create custom CLI command for SMT-lib file generation (2e8eb46)
- handle exit points with unknown satisfiability (8891c64)
Performance Improvements
- switch rarity simulation to segmented memory (7d31865)
v0.3.0
0.3.0 (2021-03-10)
Bug Fixes
- ordering for harmonic mean (less is always better) (#114) (8ae2be8)
- rarity: use right amount of values for mean calculation (#114) (c365767)
- broken build due to wrong Selfie repo URL (883821b)
- enforce unique input variable names for Z3/Boolector (#111) (a0ed9d4)
- swapped handling of --iterations and --selection (#113) (c05c743)
- rarity: Add warning message to ignored partial read (43e8297)
- rarity: detect REMU with 0 remainder as bug (8e989cb)
- rarity: Fix filtering before enumerating skewing scoring counter index (6e99b15)
- rarity: Fix rarity scoring (ba7d0ed)
- rarity: implemented score algorithm exactly as in the paper (afe4e9d)
- rarity: push the raw input values only (d6448bb)
- rarity: update dependencies to be compatible with Selfie (0e86d8d)
- rarity: Use correct format string flag for Format trait (13cd96c)
- rarity: Use f64 for rarity score instead of u64 (bd363e1)
Features
- add coin-flip execution path exploration strategy (081ec28)
- create api for rarity simulation (10aded4)
- implement write syscall in engine (#20) (#109) (d2fffde)
- rarity: adapt engine file for rarity simulation (aa39116)
- rarity: add benchmarks as submodule (d4cb2be)
- rarity: Add bytewise state comparator (ef72317)
- rarity: Add CLI parser config for rarity simulation (7b9e001)
- rarity: CLI option to switch between harmonic and arithmetic mean (90c4174)
- rarity: detect bugs during concrete execution (01ace2a)
- rarity: Implement copy-create ratio for newly created states (00e3f10)
- rarity: implement search algorithm (breadth-first) (09e5d64)
- rarity: Use harmonic mean as metric (f30f41e)
v0.2.0
faf9b33
This commit was signed with the committer’s verified signature.
ChristianMoesl
Christian Mösl
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)
- red...