v6.4.0

Chernobog 6.4.0

Changes in v6.3.1...v6.4.0.

• Semantic MBA synthesis beyond the rule catalog — a bounded Z3-backed
  pass simplifies typed 8-, 16-, 32-, and 64-bit expressions across basic blocks,
  with explicit conversions, overlapping register views, byte-addressed memory,
  and proven loop invariants. Replacements require an equivalence proof, followed
  by an independent check of the emitted microcode. Unsupported effects,
  inconclusive proofs, and exhausted budgets preserve the original expression.
• Nested arithmetic and Boolean reconstruction — bottom-up linear MBA
  reconstruction exposes identities inside larger expressions and cancels
  arithmetic across Boolean subexpressions. Boolean synthesis, modular affine
  fitting, known-bit comparison reduction, and bounded unsigned division
  simplification recover smaller expressions beyond fixed patterns. Constant
  division can become a constant or a threshold comparison when the proven
  quotient range permits it.
• Caller-context simplification — pure scalar helper calls can become
  constants or smaller symbolic expressions after substituting their actual
  arguments. Local value propagation and facts from both sides of a branch
  expose opaque predicates and constant branches, including after a helper result
  is assigned to a local. Emitted ctree expressions are checked with their casts
  and integer promotions; unsupported or effectful helpers remain calls.
• Deep deobfuscation — the new Deep deobfuscation (Chernobog) action
  raises the shared semantic-analysis budget from 1 s to 30 s per function.
  Scripts can use chernobog_deep_deobfuscate(ea),
  chernobog_deep_deobfuscate_text(ea), and chernobog_mba_smt_stats(ea).
  These are analysis budgets, not hard limits on total decompiler runtime.
  See semantic MBA synthesis
  for the model and limits.
• 32-bit saved-register stack stubs — native analysis recognizes bounded
  PE32-style dispatch stubs ending in RET 4 or XCHG [ESP], reg; RET,
  including supported PUSH substitutions. It records the handler target and
  continuation with dependency-tracked proof ownership. When the complete stub
  and handler belong to the same function, early Hex-Rays lowering replaces the
  final return with an explicit pop, any required stack adjustment, and a direct
  jump while retaining preceding stack accesses and register restorations.
  See stack-stub recovery.
• Call-boundary string inspection — strings observed when rax stops before
  an unmodeled call are available through IDC, inspection JSON, and the evidence
  workspace's Observed strings table. They remain inspection observations;
  decompiler rewrites and proof consumers still require their existing
  completed-run evidence. Entry-input collection examines at most 256 incoming
  references, reports truncation, and supports cooperative cancellation through
  static analysis, input planning, and call-summary collection.
• WARBIRD diagnostic exploration — a bounded symbolic explorer supports
  native admission profiles for ci, ClipSp, and PEAuth through four IDC functions:
  chernobog_warbird_profiles, chernobog_warbird_start,
  chernobog_warbird_poll, and chernobog_warbird_cancel. It models finite
  successor-key splits, aliased byte memory, supported scalar and legacy 128-bit
  XMM operations, native setup and dispatcher execution, bounded stack growth,
  and selected pool-allocation effects. Counted-store loop relations and guarded
  forward-state joins retain correlated state and memory-effect histories.
  Reports expose unsupported paths and resource limits; database changes
  invalidate results. This is diagnostic exploration only: all corpus entries
  remain partial, no pseudocode is replaced, and whole-entry semantic equivalence
  is not established. See WARBIRD implementation status.
• Pseudocode stability — caller-context updates run after view navigation
  completes and keep the displayed function, microcode, and text synchronized.
  Pending updates are discarded on function changes or plugin shutdown. Empty
  branch bodies retain the SDK's required placeholder, and zero-width integer
  terms are rejected during call simplification.